git.iko.soy/Idris-dev
on master help sign in
more suggested changes
ae9484aMartin Baker
docs/proofs/elabReflection.rst+4−2
compare with master
unifiedsplit
@@ -16,7 +16,7 @@ Compilation of Idris proceeds through a number of stages.
16 :height: 147px
16 :height: 147px
17 :alt: diagram showing these stages of Idris compilation
17 :alt: diagram showing these stages of Idris compilation
18
18
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.
20
20
21.. list-table::
21.. list-table::
22
22
@@ -32,6 +32,8 @@ During elaboration TT (Raw) structure contains:
32- holes - placeholders for terms that have not yet been filled in.
32- holes - placeholders for terms that have not yet been filled in.
33- 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.
33- 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.
34
34
35+For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
36+
35Type checker:
37Type checker:
36
38
37- include universe levels
39- include universe levels
@@ -61,6 +63,6 @@ As already mentioned the TT core language is kept syntactically very simple. Par
61.. _`Edwin Brady's 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf
63.. _`Edwin Brady's 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf
62.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932
64.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932
63.. _`David Christiansen's PhD thesis`: https://davidchristiansen.dk/david-christiansen-phd.pdf
65.. _`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
65
67
66
68
docs/proofs/tactics.rst+1−5
@@ -5,17 +5,13 @@ The Idris part of the code for elaborator reflection is in
5Elab.idr `<https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Language/Reflection/Elab.idr>`_
5Elab.idr `<https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Language/Reflection/Elab.idr>`_
6Before looking at the Elab monad we need to know how to construct terms.
6Before looking at the Elab monad we need to know how to construct terms.
7
7
8−Holes
9−=====
10−
11−For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
12
8
13Proof State
9Proof State
14===========
10===========
15
11
16Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are:
12Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are:
17
13
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`_.
19- A goal type - The type of the term that is under construction for the current goal.
15- A goal type - The type of the term that is under construction for the current goal.
20- A possibly incomplete proof term, which is being calculated and should be the goal type at the end of elaboration.
16- A possibly incomplete proof term, which is being calculated and should be the goal type at the end of elaboration.
21- Context - A collection of open unification problems, representing recoverable failures of unification that may yet unify once more variables are solved.
17- Context - A collection of open unification problems, representing recoverable failures of unification that may yet unify once more variables are solved.