git.iko.soy/Idris-dev
on master help sign in
more suggested changes
commitae9484a31645b2b7689c2a050355e7fc64cca98f authorMartin Baker <git87465@martinb.com> dateThu 16 May 2019, 08:25 (7 years ago) parent5cd37d8
2 files changed+5−7
compare with master
unifiedsplit
docs/proofs/elabReflection.rst+4−2 docs/proofs/tactics.rst+1−5
docs/proofs/elabReflection.rst+4−2
@@ -16,7 +16,7 @@ Compilation of Idris proceeds through a number of stages.
1616 :height: 147px
1717 :alt: diagram showing these stages of Idris compilation
1818
19−TT is a core language which is syntactically very simple, this makes it easy for computers to process but very verbose and hard for humans to read. This elaboration is done by a logic language (proof tactics) similar to LTac in Coq. Here the word 'tactics' is used to refer to these elaboration tactics - not to be confused with the old tactics mechanism.
19+TT is a core language which is syntactically very simple. This makes it easy for computers to process but very verbose and hard for humans to read. The Idris elaborator is written in Haskell using an elaboration library that was inspired by the tactics in interactive proof assistants such as Coq.
2020
2121.. list-table::
2222
@@ -32,6 +32,8 @@ During elaboration TT (Raw) structure contains:
3232- holes - placeholders for terms that have not yet been filled in.
3333- guesses - similar to let bindings, except with no reduction rule, so that elaboration programs can control the precise shape of terms that are under construction.
3434
35+For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
36+
3537Type checker:
3638
3739- include universe levels
@@ -61,6 +63,6 @@ As already mentioned the TT core language is kept syntactically very simple. Par
6163.. _`Edwin Brady's 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf
6264.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932
6365.. _`David Christiansen's PhD thesis`: https://davidchristiansen.dk/david-christiansen-phd.pdf
64−
66+.. _`Dependently Typed Functional Programs and their Proofs by McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374
6567
6668
docs/proofs/tactics.rst+1−5
@@ -5,17 +5,13 @@ The Idris part of the code for elaborator reflection is in
55Elab.idr `<https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Language/Reflection/Elab.idr>`_
66Before looking at the Elab monad we need to know how to construct terms.
77
8−Holes
9−=====
10−
11−For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
128
139Proof State
1410===========
1511
1612Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are:
1713
18−- A hole queue - This contains a list of the names of the holes used in the proof term. The solution to each hole may depend on the other holes.
14+- A hole queue - This contains a list of the names of the holes used in the proof term. The solution to each hole may depend on the other holes. For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
1915- A goal type - The type of the term that is under construction for the current goal.
2016- A possibly incomplete proof term, which is being calculated and should be the goal type at the end of elaboration.
2117- Context - A collection of open unification problems, representing recoverable failures of unification that may yet unify once more variables are solved.