diff --git a/docs/_static/theme_overrides.css b/docs/_static/theme_overrides.css new file mode 100644 index 0000000000..63ee6cc74c --- /dev/null +++ b/docs/_static/theme_overrides.css @@ -0,0 +1,13 @@ +/* override table width restrictions */ +@media screen and (min-width: 767px) { + + .wy-table-responsive table td { + /* !important prevents the common CSS stylesheets from overriding + this as on RTD they are loaded after this stylesheet */ + white-space: normal !important; + } + + .wy-table-responsive { + overflow: visible !important; + } +} diff --git a/docs/conf.py b/docs/conf.py index c3cb639980..d8b246f702 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -51,7 +51,7 @@ # General information about the project. project = u'Idris' -copyright = u'2017, The Idris Community' +copyright = u'2017-2019, The Idris Community' author = u'The Idris Community' # The version info for the project you're documenting, acts as replacement for @@ -151,6 +151,12 @@ # so a file named "default.css" will overwrite the builtin "default.css". html_static_path = ['_static'] +html_context = { + 'css_files': [ + '_static/theme_overrides.css', # override wide tables in RTD theme + ], + } + # Add any extra paths that contain custom files (such as robots.txt or # .htaccess) here, relative to this directory. These files are copied # directly to the root of the documentation. diff --git a/docs/image/README.md b/docs/image/README.md new file mode 100644 index 0000000000..6e2d3f87f0 --- /dev/null +++ b/docs/image/README.md @@ -0,0 +1,16 @@ +Many of the images in this directory have two files with the same name but a different extension: + +* The SVG file, being vector graphics, is best for drawing and modifying. +* The PNG file, being raster graphics, gives more consistent rendering. + +The image has therefore been generated as an SVG file and then exported to the PNG file. + +So, if you need to modify an image, I suggest the following sequence: + +* Edit the SVG file using a suitable editor (I use Inkscape). +* Export the changes to the PNG file, overwriting the old version. +* upload both files. + +Note, when exporting in Inkscape: +* Select everything first, this stops an enormous boundary being exported. +* After selecting the file to export to and clicking OK, don't forget to click on export button as well. diff --git a/docs/image/attack.png b/docs/image/attack.png new file mode 100644 index 0000000000..e6b1844ca4 Binary files /dev/null and b/docs/image/attack.png differ diff --git a/docs/image/attack.svg b/docs/image/attack.svg new file mode 100644 index 0000000000..57a0840373 --- /dev/null +++ b/docs/image/attack.svg @@ -0,0 +1,199 @@ + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + ?h ∶ t1→t2 . f h + ?h ≈ (?h' ∶ t1→t2 . h')∶ t1→t2 . f h + attack + + focus + + focus + + + diff --git a/docs/image/binders.png b/docs/image/binders.png new file mode 100644 index 0000000000..da5c47797f Binary files /dev/null and b/docs/image/binders.png differ diff --git a/docs/image/binders.svg b/docs/image/binders.svg new file mode 100644 index 0000000000..bf763e22ea --- /dev/null +++ b/docs/image/binders.svg @@ -0,0 +1,326 @@ + + + + + + + + + + image/svg+xml + + + + + + + Code + Logic + + + + + + Abstraction + letbinding + functionspace + λ x:t + Γ ⊢ S : Type + let x ↦ t : t + + Γ ; λ x:S ⊢ valid + Γ ⊢ S : Type + + Γ ; ∀ x:S ⊢ valid + ∀ x:t + Γ ⊢ S : Type Γ ⊢ s:S + + Γ ; let x ↦ s : S ⊢ valid + + diff --git a/docs/image/compareToProofAssist.png b/docs/image/compareToProofAssist.png new file mode 100644 index 0000000000..b8363e8ad9 Binary files /dev/null and b/docs/image/compareToProofAssist.png differ diff --git a/docs/image/compareToProofAssist.svg b/docs/image/compareToProofAssist.svg new file mode 100644 index 0000000000..76cfe93d42 --- /dev/null +++ b/docs/image/compareToProofAssist.svg @@ -0,0 +1,260 @@ + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + Human + Tactics + fill holes + Proof assistant + + + Idris source + fill holes(implicit variables, etc) + Idris Elaborator + + + Tactics + + diff --git a/docs/image/elab.png b/docs/image/elab.png new file mode 100644 index 0000000000..f2436cad22 Binary files /dev/null and b/docs/image/elab.png differ diff --git a/docs/image/elab.svg b/docs/image/elab.svg new file mode 100644 index 0000000000..bb7715767a --- /dev/null +++ b/docs/image/elab.svg @@ -0,0 +1,139 @@ + + + + + + + + + + + + + + image/svg+xml + + + + + + + + + + Definition Elaborator + definition context + Term Elaborator + + diff --git a/docs/image/elabLogicEx1_1.png b/docs/image/elabLogicEx1_1.png new file mode 100644 index 0000000000..603082aba9 Binary files /dev/null and b/docs/image/elabLogicEx1_1.png differ diff --git a/docs/image/elabLogicEx1_1.svg b/docs/image/elabLogicEx1_1.svg new file mode 100644 index 0000000000..a7861538f4 --- /dev/null +++ b/docs/image/elabLogicEx1_1.svg @@ -0,0 +1,99 @@ + + + + + + + + + + image/svg+xml + + + + + + + hole_2 : pi_arg : Nat -> Nat + hole_0 : pi_arg : Nat -> Nat + + + + diff --git a/docs/image/elabLogicEx1_2.png b/docs/image/elabLogicEx1_2.png new file mode 100644 index 0000000000..b536872416 Binary files /dev/null and b/docs/image/elabLogicEx1_2.png differ diff --git a/docs/image/elabLogicEx1_2.svg b/docs/image/elabLogicEx1_2.svg new file mode 100644 index 0000000000..cf9c8f6702 --- /dev/null +++ b/docs/image/elabLogicEx1_2.svg @@ -0,0 +1,112 @@ + + + + + + + + + + image/svg+xml + + + + + + + hole_2 : Nat + hole_0 : (pi_arg : Nat) -> Nat + + + x : Nat + + diff --git a/docs/image/elabLogicEx1_3.png b/docs/image/elabLogicEx1_3.png new file mode 100644 index 0000000000..0fb2abfffd Binary files /dev/null and b/docs/image/elabLogicEx1_3.png differ diff --git a/docs/image/elabLogicEx1_3.svg b/docs/image/elabLogicEx1_3.svg new file mode 100644 index 0000000000..aa24105818 --- /dev/null +++ b/docs/image/elabLogicEx1_3.svg @@ -0,0 +1,112 @@ + + + + + + + + + + image/svg+xml + + + + + + + hole_2 : Nat + hole_0 : (pi_arg : Nat) -> Nat + + + x : Nat + + diff --git a/docs/image/elabLogicEx1_4.png b/docs/image/elabLogicEx1_4.png new file mode 100644 index 0000000000..ccdfe84cf0 Binary files /dev/null and b/docs/image/elabLogicEx1_4.png differ diff --git a/docs/image/elabLogicEx1_4.svg b/docs/image/elabLogicEx1_4.svg new file mode 100644 index 0000000000..dee42baa4c --- /dev/null +++ b/docs/image/elabLogicEx1_4.svg @@ -0,0 +1,80 @@ + + + + + + + + + + image/svg+xml + + + + + + + hole_0 : (pi_arg : Nat) -> Nat + + + diff --git a/docs/image/elabOverview.png b/docs/image/elabOverview.png new file mode 100644 index 0000000000..b1adcc3417 Binary files /dev/null and b/docs/image/elabOverview.png differ diff --git a/docs/image/elabOverview.svg b/docs/image/elabOverview.svg new file mode 100644 index 0000000000..2e299b30a2 --- /dev/null +++ b/docs/image/elabOverview.svg @@ -0,0 +1,585 @@ + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + data TT : Type where P : NameType -> TTName -> TT -> TT V : Int -> TT Bind : TTName -> Binder TT -> TT -> TT App : TT -> TT -> TT TConst : Const -> TT Erased : TT TType : TTUExp -> TT UType : Universe -> TT + globally defined variable from name + + local (de Bruijn) variable + + any kind of binderlambda, let etc. + + function application + + intager, char, string, etc. + + unknown term for erasing types + + type of types + + unique universe + + elements of core language + + TT + envgoalholesguess + Elab (List (TTName, Binder TT)Elab (TTName,TT)Elab (List TTName)Elab (TT) + + state + + Elab Monad + + + + + + solvefillapplyfocus... + tactics + + diff --git a/docs/image/elabProofState.png b/docs/image/elabProofState.png new file mode 100644 index 0000000000..4cd9ea1b0b Binary files /dev/null and b/docs/image/elabProofState.png differ diff --git a/docs/image/elabProofState.svg b/docs/image/elabProofState.svg new file mode 100644 index 0000000000..e65bea07d7 --- /dev/null +++ b/docs/image/elabProofState.svg @@ -0,0 +1,356 @@ + + + + + + + + + + image/svg+xml + + + + + + + current proof term + (TTName, TT) + original goal + pathsubtermupdates + Contexts used for global definitions and for proof state.They contain universe constraints and existing definitions.Also store maximum RigCount of the namel + Environment + Holes + Guess + Goal + + + + + + + + + focus + + + List (TTName, Binder TT)Open unification constaints. + List TTName + TT + + diff --git a/docs/image/elabProofStateEx1_1.png b/docs/image/elabProofStateEx1_1.png new file mode 100644 index 0000000000..72c79da49f Binary files /dev/null and b/docs/image/elabProofStateEx1_1.png differ diff --git a/docs/image/elabProofStateEx1_1.svg b/docs/image/elabProofStateEx1_1.svg new file mode 100644 index 0000000000..862c3f3684 --- /dev/null +++ b/docs/image/elabProofStateEx1_1.svg @@ -0,0 +1,312 @@ + + + + + + + + + + image/svg+xml + + + + + + + hole_2 + Environment + Holes + Guess + Goal + + + + + + + hole_0 + [ ] + starts off empty + + (hole_2 , pi_arg : Nat->Nat) + this is the signaturewe are looking for + + machine chosennames for the holes + + no guess yet + + diff --git a/docs/image/elabProofStateEx1_2.png b/docs/image/elabProofStateEx1_2.png new file mode 100644 index 0000000000..8dc1aee483 Binary files /dev/null and b/docs/image/elabProofStateEx1_2.png differ diff --git a/docs/image/elabProofStateEx1_2.svg b/docs/image/elabProofStateEx1_2.svg new file mode 100644 index 0000000000..3a38cc2005 --- /dev/null +++ b/docs/image/elabProofStateEx1_2.svg @@ -0,0 +1,281 @@ + + + + + + + + + + + + + + image/svg+xml + + + + + + + hole_2 + Environment + Holes + Guess + Goal + + + + + + + hole_0 + (x, λ Nat) + (hole_2 , Nat) + replace the focussed holewith a lambda + + x:Nat + + diff --git a/docs/image/elabProofStateEx1_3.png b/docs/image/elabProofStateEx1_3.png new file mode 100644 index 0000000000..53204fd52c Binary files /dev/null and b/docs/image/elabProofStateEx1_3.png differ diff --git a/docs/image/elabProofStateEx1_3.svg b/docs/image/elabProofStateEx1_3.svg new file mode 100644 index 0000000000..4c4aee2643 --- /dev/null +++ b/docs/image/elabProofStateEx1_3.svg @@ -0,0 +1,244 @@ + + + + + + + + + + image/svg+xml + + + + + + + hole_2 + Environment + Holes + Guess + Goal + + + + + + hole_0 + (x, λ Nat) + (hole_2 , Nat) + x:Nat + + diff --git a/docs/image/fill.png b/docs/image/fill.png new file mode 100644 index 0000000000..a8356715ed Binary files /dev/null and b/docs/image/fill.png differ diff --git a/docs/image/fill.svg b/docs/image/fill.svg new file mode 100644 index 0000000000..271e39a060 --- /dev/null +++ b/docs/image/fill.svg @@ -0,0 +1,163 @@ + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + ? {hole} . {hole} + ?{hole} ≈ Prelude.Nat.Z . {hole} + fill `(Z) + + focus + + + diff --git a/docs/image/generateDatatype.png b/docs/image/generateDatatype.png new file mode 100644 index 0000000000..8c67974eb9 Binary files /dev/null and b/docs/image/generateDatatype.png differ diff --git a/docs/image/generateDatatype.svg b/docs/image/generateDatatype.svg new file mode 100644 index 0000000000..5e7e34420d --- /dev/null +++ b/docs/image/generateDatatype.svg @@ -0,0 +1,540 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + + + declareDatatype + defineDatatype + + Declare + name:TTNamearguments:List FunArgreturnType:Raw + TyDecl + + + MkFunArg + name:TTNametype:Rawplicity:Plicityerasure:Erasure + FunArg + ExplicitImplicitConstraint + + + ErasedNotErased + + + DefineDatatype + name:TTNameconstructors : List ConstructorDefn + DataDefn + + + Constructor + name:TTNamearguments:List FunArgreturnType:Raw + ConstructorDefn + MkFunArg + + + diff --git a/docs/image/generateFunction.png b/docs/image/generateFunction.png new file mode 100644 index 0000000000..9e1b7277bc Binary files /dev/null and b/docs/image/generateFunction.png differ diff --git a/docs/image/generateFunction.svg b/docs/image/generateFunction.svg new file mode 100644 index 0000000000..a5c37e0eb4 --- /dev/null +++ b/docs/image/generateFunction.svg @@ -0,0 +1,588 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + + + declareType + defineFunction + + Declare + name:TTNamearguments:List FunArgreturnType:Raw + TyDecl + + + MkFunArg + name:TTNametype:Rawplicity:Plicityerasure:Erasure + FunArg + ExplicitImplicitConstraint + + + ErasedNotErased + + + DefineFun + name:TTNameclauses : List (FunClause a) + FunDefn + + + MkFunClause + lhs:arhs:a + FunClause + MkImpossibleClause + + lhs:a + FunClause + + + diff --git a/docs/image/generateFunction2.png b/docs/image/generateFunction2.png new file mode 100644 index 0000000000..70ccd22b08 Binary files /dev/null and b/docs/image/generateFunction2.png differ diff --git a/docs/image/generateFunction2.svg b/docs/image/generateFunction2.svg new file mode 100644 index 0000000000..10008bf4a6 --- /dev/null +++ b/docs/image/generateFunction2.svg @@ -0,0 +1,430 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + RBind TTName (Binder TT) TT + lhs:arhs:a + FunClause + + Raw + + PVar a (Binder a) + + RApp Raw Raw + + + Binder a + `{{code}} + `{{body}} + + + + + diff --git a/docs/image/idrisTopLevel.png b/docs/image/idrisTopLevel.png new file mode 100644 index 0000000000..f3d20f35e0 Binary files /dev/null and b/docs/image/idrisTopLevel.png differ diff --git a/docs/image/idrisTopLevel.svg b/docs/image/idrisTopLevel.svg new file mode 100644 index 0000000000..16287cea90 --- /dev/null +++ b/docs/image/idrisTopLevel.svg @@ -0,0 +1,524 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + Idris + Idris + ~ + TT + Executable + desugaring + + elaboration + compilation + + C + JS + + + Add implicitly quantified variables.Conditional expressions replaced by function calls. + + proof tactics + + + + during elaborationmay contain holesand guesses + + Make explicit all types.Make explicit function and pattern match variables. + + + type checkerRaw -> TT + + Raw + PTerm + + diff --git a/docs/image/solve.png b/docs/image/solve.png new file mode 100644 index 0000000000..a1b7081c81 Binary files /dev/null and b/docs/image/solve.png differ diff --git a/docs/image/solve.svg b/docs/image/solve.svg new file mode 100644 index 0000000000..314be94cbd --- /dev/null +++ b/docs/image/solve.svg @@ -0,0 +1,163 @@ + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + Prelude.Nat.Z + solve + + focus + + ?{hole} ≈ Prelude.Nat.Z . {hole} + + diff --git a/docs/image/tree.png b/docs/image/tree.png new file mode 100644 index 0000000000..edfa6d71e6 Binary files /dev/null and b/docs/image/tree.png differ diff --git a/docs/image/tree.svg b/docs/image/tree.svg new file mode 100644 index 0000000000..a80014f6ad --- /dev/null +++ b/docs/image/tree.svg @@ -0,0 +1,212 @@ + + + + + + + + + + + + + + image/svg+xml + + + + + + + {hole2} :Nat->Nat + intro `{{x}} + solve + fill (Var `{{x}}) + + + + state + state + state + λ x:Nat . ? {hole 2} + λ x:Nat . x + + diff --git a/docs/proofs/elabReflection.rst b/docs/proofs/elabReflection.rst new file mode 100644 index 0000000000..f2866f93ae --- /dev/null +++ b/docs/proofs/elabReflection.rst @@ -0,0 +1,60 @@ +Extending Idris using Elaborator Reflection +=========================================== + +Idris provides a mechanism to modify the language without having to recompile Idris itself. We can think of this in terms of metaprogramming or domain specific languages or just building in new capabilities. + +In order to extend the language we need to know something about how Idris is compiled. This page explains only what is needed to customise the elaboration. For more information about the compiler's implementation see `Edwin Brady's 2013 paper`_ and for customising the elaboration process see `Elaborator reflection: extending Idris in Idris`_ and `David Christiansen's PhD thesis`_. + +Compilation of Idris proceeds through a number of stages. + +- First, Idris is desugared by inserting placeholders for terms to be guessed by the compiler and replacing certain syntactic forms, such as do-notation, with the functions that implement them. +- Then, this desugared Idris is translated into a much simpler core language, called TT. This translation process is called elaboration. +- Finally, TT is type checked a second time to rule out errors, and then compiled into the target language. + +.. image:: ../image/idrisTopLevel.png + :width: 484px + :height: 147px + :alt: diagram illustrating these stages of Idris compilation + +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. + +.. list-table:: + + * - There are some similarities with a proof assistant but in Idris the elaborator is an interpreter of Idris source in the elaboration monad, where each syntactic construct of Idris is interpreted as a sequence of tactics. + - .. image:: ../image/compareToProofAssist.png + :width: 206px + :height: 112px + :alt: diagram comparing elaboration with proof assistant + +The primitives in the elaboration library are not just useful for the implementors of Idris itself. They can also be used by authors of extensions to the compiler, using a mechanism known as elaborator reflection. +During elaboration TT (Raw) structure contains: + +- holes - placeholders for terms that have not yet been filled in. +- 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. + +For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_. + +The following diagram is intended to illustrate a high level view of the tactics and how this eventually results in the TT language being generated. It is not necessary to understand the details at this stage. The intention is to help build up some intuition so that, when we get into the details, we can recognise how this fits into the big picture. + +.. image:: ../image/elabOverview.png + :width: 410px + :height: 282px + :alt: diagram illustrating overview of TT language being generated from tactics. + +As already mentioned the TT core language is kept syntactically very simple, for instance, here are the binders in TT with corresponding code and logic type validity rules: + +.. list-table:: + + * - This diagram illustrates the basis of the compilation process in logic (in this case for binders). It is not necessary to be an expert logician to understand elaborator reflection. However, when learning about tactics, they may appear arbitrary without knowing some theory. For more information about this see `Edwin Brady's 2013 paper`_. + - .. image:: ../image/binders.png + :width: 310px + :height: 203px + :alt: diagram illustrating basis of code in logic + +.. target-notes:: +.. _`Edwin Brady's 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf +.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932 +.. _`David Christiansen's PhD thesis`: https://davidchristiansen.dk/david-christiansen-phd.pdf +.. _`Dependently Typed Functional Programs and their Proofs by McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374 + + diff --git a/docs/proofs/example1.rst b/docs/proofs/example1.rst new file mode 100644 index 0000000000..9ba1e97e2c --- /dev/null +++ b/docs/proofs/example1.rst @@ -0,0 +1,192 @@ +Elaborator Reflection - Identity Example +======================================== + +.. list-table:: + + * - This example of elaborator reflection steps through this metaprogram that generates the identity function: + - .. code-block:: idris + + %language ElabReflection + + idNat : Nat -> Nat + idNat = %runElab (do intro `{{x}} + fill (Var `{{x}}) + solve) + +.. list-table:: + :widths: 200 100 + + * - At the beginning of executing the elaboration script, the initial state consists of a single hole of type Nat -> Nat. + + As a first approximation, the state consists of a term with holes in it, an indicator of which hole is focused, a queue of the next holes to focus on, and miscellaneous information like a source of fresh names. The intro tactic modifies this state, replacing the focused hole with a lambda and focusing on the lambda's body. + - .. image:: ../image/tree.png + :width: 119px + :height: 109px + +The following is a walkthough looking at the state after each tactic: + +.. list-table:: + + * - Start with the type signature like this: + - .. code-block:: idris + + %language ElabReflection + + idNat : Nat -> Nat + idNat = %runElab (do + + * - In order to investigate how the program works this table shows the proof state at each stage as the tactics are applied. So here is the proof state at the start: + - .. image:: ../image/elabProofStateEx1_1.png + :width: 310px + :height: 115px + + * - This table shows the hole types and what they depend on. The aim is to illustrate the types by analogy with proofs, as a line with the premises above it and the conclusion below it. + - .. image:: ../image/elabLogicEx1_1.png + :width: 277px + :height: 15px + + * - The term is: + - ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0} + + * - It is possible to read the state from the script by calling getEnv, getGoal and getHoles. + + - The output of these calls contain structures with TT code. To show the results I hacked this: `my code`_. TT code is not really designed to be readable by humans, all the names are fully expanded, everything has a type down to universes (type of types). This is shown here to illustrate the information available. + + .. code-block:: idris + + getEnv=[] + + getGoal=(hole_2, __pi_arg:(Nat.["Nat", "Prelude"]:{ + type constructor tag=8 number=0}.Type:U=(20:./Prelude/Nat.idr)->. + {name ref{type constructor tag=8 number=0}Nat.["Nat","Prelude"]: + Type:U=(20:./Prelude/Nat.idr) + }) + }) + + getHoles=[{hole_2},{hole_0}] + + * - getGuess + - error no guess + + * - Introduce a lambda binding around the current hole and focus on the body. + - intro \`{{x}} + + * - The state now looks like this: + - .. image:: ../image/elabProofStateEx1_2.png + :width: 312px + :height: 84px + + * - The hole types now looks like this: + - .. image:: ../image/elabLogicEx1_2.png + :width: 279px + :height: 26px + + * - The term now looks like this: + - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0} + + * - Again we can check the state by calling getEnv, getGoal and getHoles: see `my code`_ + + - .. code-block:: idris + + getEnv=[(x, {λ (Nat.["Nat", "Prelude"]:{ + type constructor tag=8 number=0}). + Type:U=(20:./Prelude/Nat.idr) + })] + + getGoal=(hole_2, {name ref{type constructor tag=8 number=0} + Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr) + }) + + getHoles=[{hole_2},{hole_0}] + + * - getGuess + - error no guess + + * - Place a term into a hole, unifying its type + - fill (Var \`{{x}}) + + * - The state still looks like this: + - .. image:: ../image/elabProofStateEx1_3.png + :width: 312px + :height: 57px + + * - The hole types now looks like this: + - .. image:: ../image/elabLogicEx1_3.png + :width: 290px + :height: 26px + + * - The term now looks like this: + - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0} + + * - Again we can check the state by calling getEnv, getGoal and getHoles: see `my code`_ + + - .. code-block:: idris + + getEnv=[(x, {λ (Nat.["Nat", "Prelude"]: + {type constructor tag=8 number=0}). + Type:U=(20:./Prelude/Nat.idr) + })] + + getGoal=(hole_2, {name ref{type constructor tag=8 number=0} + Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr) + }) + + getHoles=[{hole_2}, {hole_0}] + + * - getGuess + - .. code-block:: idris + + {name ref bound x: + {name ref{type constructor tag=8 number=0} + Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr) + } + } + + * - Substitute a guess into a hole. + - solve + + * - The hole types now looks like this: + - .. image:: ../image/elabLogicEx1_4.png + :width: 131px + :height: 14px + + * - The term now looks like this: + - ?{hole_0} ≈ λ x . x . {hole_0} + + * - getEnv + + getGoal + + getHoles + + - .. code-block:: idris + + getEnv=[] + + getGoal=(hole_0, __pi_arg:(Nat.["Nat", "Prelude"]:{ + type constructor tag=8 number=0}. + Type:U=(20:./Prelude/Nat.idr) + ->.{name ref + {type constructor tag=8 number=0} + Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr) + }) + }) + + getHoles=[{hole_0}] + + * - getGuess + - .. code-block:: idris + + x:({λ (Nat.["Nat", "Prelude"]:{ + type constructor tag=8 number=0}). + Type:U=(20:./Prelude/Nat.idr) + }.{ + name ref bound + x:{name ref {type constructor tag=8 number=0} + Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr) + } + }) + } + +.. target-notes:: +.. _`my code`: https://github.com/martinbaker/Idris-dev/blob/uglyTTPrinter/libs/prelude/Language/Reflection/TTPrinter.idr diff --git a/docs/proofs/generatingData.rst b/docs/proofs/generatingData.rst new file mode 100644 index 0000000000..9c43e7bb6d --- /dev/null +++ b/docs/proofs/generatingData.rst @@ -0,0 +1,385 @@ +Generating Datatypes and Functions at Compile Time +================================================== + +Program elements, such as datatypes and functions can be constructed at compile-time in the Elab monad. +This can allow proofs to be generated for user defined types or it could allow types to be automatically generated to support user defined types. +An example is the code, from `Elaborator reflection: extending Idris in Idris`_, that automatically generates accessibility predicates using the Bove-Capretta method. + +Generating Datatypes +-------------------- + +There are two main 'tactics' associated with generating datatypes: + +- declareDatatype +- defineDatatype + +Which declare and define the datatype as the names suggest. + +.. list-table:: + + * - These 'tactics' and the data structures associated with them are listed in the tables later on this page, for now, here is a summary: + - .. image:: ../image/generateDatatype.png + :width: 332px + :height: 246px + :alt: diagram illustrating data structures associated with declareDatatype defineDatatype. + +.. list-table:: + + * - As a first example, the following boolean-like type can be constructed. When the compiler has run it will be available to us as if we had compiled it in the usual way: + - .. code-block:: idris + + λΠ> :printdef Two + data Two : Type where + F : Two + T : Two + +This was generated by the following code: + +.. code-block:: idris + + module TwoDef + %language ElabReflection + + addTwo : Elab () + addTwo = do let twoname : TTName = `{{TwoDef.Two}} + let F2 = `{{TwoDef.F}} + let T2 = `{{TwoDef.T}} + declareDatatype $ Declare twoname [] `(Type) + defineDatatype $ DefineDatatype twoname [ + Constructor `{{F}} [] (Var `{{TwoDef.Two}}), + Constructor `{{T}} [] (Var `{{TwoDef.Two}}) + ] + + %runElab addTwo + +.. list-table:: + + * - The constructors T and F can be called as would be expected: + - .. code-block:: idris + + λΠ> F + F : Two + λΠ> T + T : Two + +Generating Functions +-------------------- + +There are two main 'tactics' associated with generating functions: + +- declareType +- defineFunction + +Which declare and define the function as the names suggest. + +.. list-table:: + + * - These 'tactics' and the data structures associated with them are listed in the tables later on this page, for now, here is a summary: + - .. image:: ../image/generateFunction.png + :width: 332px + :height: 246px + :alt: diagram illustrating data structures associated with function declare and define. + +Note: The left hand side (lhs) and right hand side (rhs) of FunClause typically is of type 'Raw'. + +.. list-table:: + + * - Bound pattern variables are represented by 'PVar' binders: + This diagram shows an example of a possible Raw structure that might be used in a function definition. + - .. image:: ../image/generateFunction2.png + :width: 264px + :height: 239px + :alt: diagram illustrating data structures associated with functions. + +.. list-table:: + + * - Some function definitions can now be added to the above datatype. This is what they will look like: + - .. code-block:: idris + + λΠ> :printdef perm1 + perm1 : Two -> Two + perm1 F = F + perm1 T = T + λΠ> :printdef perm2 + perm2 : Two -> Two + perm1 F = T + perm1 T = F + +This was generated with the following code: + +.. code-block:: idris + + let perm1 = `{{TwoDef.perm1}} + declareType (Declare perm1 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname)) + defineFunction $ DefineFun perm1 [ + MkFunClause (RApp (Var perm1) (Var `{{TwoDef.F}})) (Var F2), + MkFunClause (RApp (Var perm1) (Var `{{TwoDef.T}})) (Var T2) + ] + + let perm2 = `{{TwoDef.perm2}} + declareType (Declare perm2 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname)) + defineFunction $ DefineFun perm2 [ + MkFunClause (RApp (Var perm1) (Var `{{TwoDef.F}})) (Var T2), + MkFunClause (RApp (Var perm1) (Var `{{TwoDef.T}})) (Var F2) + ] + +.. list-table:: + + * - This is what happens when we call the functions: + - .. code-block:: idris + + λΠ> perm1 F + F : Two + λΠ> perm1 T + T : Two + λΠ> perm2 F + T : Two + λΠ> perm2 T + F : Two + +So far these datatypes and functions could have been written, statically, in the usual way. However, it is possible to imagine situations where we may need a lot of functions to be generated automatically at compile time. For example, if we extend this Boolean datatype to a datatype with more simple constructors (a finite set), we could generate a function for every possible permutation of that datatype back to itself. + +A Different Example which has Type Parameters +--------------------------------------------- + +.. list-table:: + + * - Here is an example of a datatype with type parameters: + - .. code-block:: idris + + data N : Nat -> Type where + MkN : N x + MkN' : (x : Nat) -> N (S x) + +This was produced by the following code: + +.. code-block:: idris + + module DataDef + %language ElabReflection + + addData : Elab () + addData = do + let dataname : TTName = `{{DataDef.N}} + declareDatatype $ Declare dataname [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type) + defineDatatype $ DefineDatatype dataname [ + Constructor `{{MkN}} [MkFunArg `{{x}} `(Nat) Implicit NotErased] + (RApp (Var dataname) (Var `{{x}})), + Constructor `{{MkN'}} [MkFunArg `{{x}} `(Nat) Explicit NotErased] + (RApp (Var dataname) (RApp (Var `{S}) (Var `{{x}}))) + ] + + %runElab addData + +So this declares and defines the following data structure 'N' with a constructor 'MkN' which can have an implicit or an explicit Nat argument. Which can be used like this: + +.. code-block:: idris + + λΠ> :t N + N : Nat -> Type + λΠ> N 2 + N 2 : Type + λΠ> N 0 + N 0 : Type + λΠ> :t MkN + MkN : N x + +Table of 'tactics' for Generating Data and Functions +---------------------------------------------------- + +These are the functions that we can use to create data and functions in the Elab monad: + +.. list-table:: + :widths: 10 30 + :stub-columns: 1 + + * - declareType + - Add a type declaration to the global context. + + Signature: + + declareType : TyDecl -> Elab () + * - defineFunction + - Define a function in the global context. The function must have already been declared, either in ordinary Idris code or using `declareType`. + + Signature: + + defineFunction : FunDefn Raw -> Elab () + + * - declareDatatype + - Declare a datatype in the global context. This step only establishes the type constructor; use `defineDatatype` to give it constructors. + + Signature: + + declareDatatype : TyDecl -> Elab () + + * - defineDatatype + - Signature: + + defineDatatype : DataDefn -> Elab () + + * - addImplementation + - Register a new implementation for interface resolution. + + Arguments: + + - ifaceName the name of the interface for which an implementation is being registered + - implName the name of the definition to use in implementation search + + Signature: + + addImplementation : (ifaceName, implName : TTName) -> Elab () + + * - isTCName + - Determine whether a name denotes an interface. + + Arguments: + + - name - a name that might denote an interface. + + Signature: + + isTCName : (name : TTName) -> Elab Bool + +Table of Datatypes Associated with Generating Data and Functions +---------------------------------------------------------------- + +The above functions use the following data/records: + +.. list-table:: + :widths: 10 30 + :stub-columns: 1 + + * - Plicity + - How an argument is provided in high-level Idris + + .. code-block:: idris + + data Plicity= + ||| The argument is directly provided at the application site + Explicit | + ||| The argument is found by Idris at the application site + Implicit | + ||| The argument is solved using interface resolution + Constraint + + * - FunArg + - Function arguments + + These are the simplest representation of argument lists, and are used for functions. Additionally, because a FunArg provides enough + information to build an application, a generic type lookup of a top-level identifier will return its FunArgs, if applicable. + + .. code-block:: idris + + record FunArg where + constructor MkFunArg + name : TTName + type : Raw + plicity : Plicity + erasure : Erasure + + * - TyConArg + - Type constructor arguments + + Each argument is identified as being either a parameter that is + + consistent in all constructors, or an index that varies based on + + which constructor is selected. + + .. code-block:: idris + + data TyConArg = + ||| Parameters are uniform across the constructors + TyConParameter FunArg | + ||| Indices are not uniform + TyConIndex FunArg + + * - TyDecl + - A type declaration for a function or datatype + + .. code-block:: idris + + record TyDecl where + constructor Declare + ||| The fully-qualified name of the function or datatype being declared. + name : TTName + ||| Each argument is in the scope of the names of previous arguments. + arguments : List FunArg + ||| The return type is in the scope of all the argument names. + returnType : Raw + + * - FunClause + - A single pattern-matching clause + + .. code-block:: idris + + data FunClause : Type -> Type where + MkFunClause : (lhs, rhs : a) -> FunClause a + MkImpossibleClause : (lhs : a) -> FunClause a + + * - FunDefn + - A reflected function definition. + + .. code-block:: idris + + record FunDefn a where + constructor DefineFun + name : TTName + clauses : List (FunClause a) + + * - ConstructorDefn + - A constructor to be associated with a new datatype. + + .. code-block:: idris + + record ConstructorDefn where + constructor Constructor + ||| The name of the constructor. The name must _not_ be qualified - + ||| that is, it should begin with the `UN` or `MN` constructors. + name : TTName + ||| The constructor arguments. Idris will infer which arguments are + ||| datatype parameters. + arguments : List FunArg + ||| The specific type constructed by the constructor. + returnType : Raw + + * - DataDefn + - A definition of a datatype to be added during an elaboration script. + + .. code-block:: idris + + record DataDefn where + constructor DefineDatatype + ||| The name of the datatype being defined. It must be + ||| fully-qualified, and it must have been previously declared as a + ||| datatype. + name : TTName + ||| A list of constructors for the datatype. + constructors : List ConstructorDefn + + * - CtorArg + - CtorParameter + + .. code-block:: idris + + data CtorArg = CtorParameter FunArg | CtorField FunArg + + * - Datatype + - A reflected datatype definition + + .. code-block:: idris + + record Datatype where + constructor MkDatatype + ||| The name of the type constructor + name : TTName + ||| The arguments to the type constructor + tyConArgs : List TyConArg + ||| The result of the type constructor + tyConRes : Raw + ||| The constructors for the family + constructors : List (TTName, List CtorArg, Raw) + +.. target-notes:: +.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932 diff --git a/docs/proofs/holes.rst b/docs/proofs/holes.rst new file mode 100644 index 0000000000..731b0a8b4c --- /dev/null +++ b/docs/proofs/holes.rst @@ -0,0 +1,196 @@ +Elaborator Reflection - Holes +============================= + +The process of doing proofs and elaborator reflection tends to involve stating with a desired conclusion and working back to known premises. This often needs intermediate sub-goals which may only be partially solved, these are encoded using 'holes' and 'guesses'. + +* A hole is a term (an expression - a chunk of code) which is yet to be determined. We do have information about its type (this process tends to be type driven). +* A guess is like a hole that is not yet bound. + +The theory around this was developed in `Dependently Typed Functional Programs and their Proofs by McBride 1999`_. + +Notation for Holes and Guesses +------------------------------ + +There is a notation used in the McBride 1999 thesis which is adapted for the TT language. When working on elaborator reflection it is useful to know this notation, for instance when reading the output of the 'debug' tactic. + +* A focused hole is notated like this ?x:t . t +* A guess is notated like this ?x ≈ t:t . t + +The following example shows how this is used: + +Simple Example +-------------- + +Start with a code file that just contains: + +.. code-block:: idris + + %language ElabReflection + + testFn : Nat + testFn = %runElab (do debug {a = ()}) + +when this is loaded the following is displayed: + +.. code-block:: idris + + Holes: + ---------------------------------- + {hole_2} : Prelude.Nat.Nat + + ---------------------------------- + {hole_0} : Prelude.Nat.Nat + + Term: + ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0} + +This shows information about the state when debug is encountered, during tactic execution, which allows us to investigate what is happening at each stage. + +* The "Holes" part shows the types of the holes and the local context of each +* The "Term" part shows where these holes are in the expression being constructed. + +So starting with the "Term" part we have. + +.. code-block:: idris + + ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0} + +.. sidebar:: attack tactic + + This kind of thing tends to arise from "attack", which helps keep binding forms in order. + +The meaning of this is not immediately apparent so it helps to add some parentheses to make the structure clearer: + +.. code-block:: idris + + (?{hole_0} ≈ (? {hole_2} . {hole_2}) . {hole_0}) + +First lets look at the inner part: + +.. code-block:: idris + + ? {hole_2} . {hole_2} + +We can substitute in the type from the "Holes" part: + +.. code-block:: idris + + ? {hole_2}:Nat . {hole_2}:Nat + +So we are looking for a hole of type Nat and all we know is it has type Nat. + +Going back to the full term, the above is wrapped in a guess, so it means: 'a guess that is itself a hole'. + +Since the elaborator does not have any further information it has to be given a value: + +.. code-block:: idris + + %language ElabReflection + + testFn : Nat + testFn = %runElab (do fill `(Z) + debug {a = ()} + solve) + +Now we have a guess for hole_2 which is itself a guess for hole_0: + +.. code-block:: idris + + ?{hole_0} ≈ ?{hole_2} ≈ Prelude.Nat.Z . {hole_2} . {hole_0} + +The guesses can be accepted by calling the 'solve' tactic. + +Example Showing Patterns +------------------------ + +In this next example a parameter 'n' has been added to the function. This allows us to see how patterns are used. Starting with this file: + +.. code-block:: idris + + %language ElabReflection + + testFn : Nat -> Nat + testFn n = %runElab (do debug {a = ()}) + +when loaded gives: + +.. code-block:: idris + + Holes: + n : Prelude.Nat.Nat + ---------------------------------- + {hole_3} : Prelude.Nat.Nat + + n : Prelude.Nat.Nat + ---------------------------------- + {hole_1} : Prelude.Nat.Nat + + ---------------------------------- + {hole_0} : patTy n : Prelude.Nat.Nat . Prelude.Nat.Nat + + Term: + ?{hole_0} ≈ pat n : Prelude.Nat.Nat . + ?{hole_1} ≈ ? {hole_3} . {hole_3} . {hole_1} . + {hole_0} + +The ns above the lines show the context of the holes on the right hand side - they include the variable n that is an argument! + +patTy is a binding form in Idris's core language that introduces a pattern variable. The idea is that the left-hand side and right-hand side of each pattern should have the same type. Because pattern variables may occur multiple times on either side of the equation, we can achieve this by documenting their types with a binding form that wraps each side. This new binding form is why an "attack" was necessary prior to elaborating the RHS. + +patTy is a type former, and pat is the corresponding introduction form. So you can think of patTy as being a bit like a dependent function type, and pat as being a bit like lambda, except they don't introduce functions (they instead are used for pattern-matching definitions). + +More Complicated Example +------------------------ + +This example does not introduce any new notation but the extra complexity gives a more realistic idea of how it is used. Here we start with this file: + +.. code-block:: idris + + %language ElabReflection + + testFn : (n : Nat) -> (n = plus n Z) -> (S n = S (plus n Z)) + testFn k ih = %runElab (do debug {a = ()}) + +when loaded gives: + +.. code-block:: idris + + Holes: + k : Prelude.Nat.Nat + ih : = Prelude.Nat.Nat Prelude.Nat.Nat k + (Prelude.Nat.plus k Prelude.Nat.Z) + ---------------------------------- + {hole_4} : = Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k) + (Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z)) + + k : Prelude.Nat.Nat + ih : = Prelude.Nat.Nat Prelude.Nat.Nat k + (Prelude.Nat.plus k Prelude.Nat.Z) + ---------------------------------- + {hole_2} : = Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k) + (Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z)) + + k : Prelude.Nat.Nat + ---------------------------------- + {hole_1} : patTy ih : = Prelude.Nat.Nat Prelude.Nat.Nat k + (Prelude.Nat.plus k Prelude.Nat.Z) . + = Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k) + (Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z)) + + ---------------------------------- + {hole_0} : patTy k : Prelude.Nat.Nat . + patTy ih : = Prelude.Nat.Nat Prelude.Nat.Nat k + (Prelude.Nat.plus k Prelude.Nat.Z) . + = Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k) + (Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z)) + + Term: + ?{hole_0} ≈ pat k : Prelude.Nat.Nat . + ?{hole_1} ≈ pat ih : = Prelude.Nat.Nat Prelude.Nat.Nat k + (Prelude.Nat.plus k Prelude.Nat.Z) . + ?{hole_2} ≈ ? {hole_4} . {hole_4} . {hole_2} . + {hole_1} . + {hole_0} + +.. target-notes:: +.. _`Dependently Typed Functional Programs and their Proofs by McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374 diff --git a/docs/proofs/index.rst b/docs/proofs/index.rst index 9123651cc5..a4db17a478 100644 --- a/docs/proofs/index.rst +++ b/docs/proofs/index.rst @@ -1,10 +1,10 @@ .. _proofs-index: -############### -Theorem Proving -############### +######################################### +Theorem Proving and Elaborator Reflection +######################################### -A tutorial on theorem proving in Idris. +A tutorial on theorem proving in Idris. .. note:: @@ -25,4 +25,9 @@ A tutorial on theorem proving in Idris. propositional interactive interactiveOld - + elabReflection + tactics + holes + example1 + primitive + generatingData diff --git a/docs/proofs/primitive.rst b/docs/proofs/primitive.rst new file mode 100644 index 0000000000..89b87ab3fb --- /dev/null +++ b/docs/proofs/primitive.rst @@ -0,0 +1,518 @@ +Primitive Operators +=================== + +.. list-table:: + :widths: 10 30 + :stub-columns: 1 + + * - gensym + - Generate a unique name based on some hint. + + Useful when establishing a new binder. + + **NB**: the generated name is unique **for this run of the elaborator**. + + Do not assume that they are globally unique. + + Signature: + + gensym : (hint : String) -> Elab TTName + + * - solve + - Substitute a guess into a hole. + + + .. image:: ../image/solve.png + :width: 141px + :height: 74px + :alt: diagram illustrating solve tactic + + + Substitute the focused guess throughout its scope, eliminating it and moving focus to the next element of the hole queue. Fail if the focus is not a guess. + + Signature: + + solve : Elab () + + Example: + + .. code-block:: idris + + %language ElabReflection + + testFn : Nat + testFn = %runElab (do fill `(Z) + solve) + + * - fill + - Place a term into a hole, unifying its type. Fails if the focus is not a hole. + + + .. image:: ../image/fill.png + :width: 140px + :height: 74px + :alt: diagram illustrating fill tactic + + + Signature: + + fill : (e : Raw) -> Elab () + + Place a term e with type tc into the focused hole: + + ?h : th.e' + + and convert it to a guess: + + ?h ≈ e:t.e' + + and fail if the current focus is not a hole. The type t of the guess is constructed by unifying tc and th, which may instantiate holes that they refer to. Fail if the current focus is not a hole or if unification fails. + + This unification can result in the solution of further holes or the establishment of additional unsolved unification constraints. + + Example: + + .. code-block:: idris + + %language ElabReflection + + testFn : Nat + testFn = %runElab (do fill `(Z) + solve) + + * - apply + - Attempt to apply an operator to fill the current hole, potentially solving arguments by unification. + + A hole is established for each argument. + + The return value is the list of holes established for the arguments to the function. + + Note that not all of the returned hole names still exist, as they may have been solved. + + - @ op the term to apply + - @ argSpec - A list of booleans, one for each argument that the operator will be applied to. If true then attempt to solve the argument by unification. + + Signature: + + apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName) + + Example: elaborating an application of a function f that takes one implicit and two explicit arguments might invoke: + + apply \`(f) [False, True, True] + + Here is an example of an elab script that uses apply to insert the term plus Z (S Z) into a goal of type Nat. + + .. code-block:: idris + + do [x,y] <- apply `(plus) [False, False] + solve + focus x; fill `(Z); solve + focus y; fill `(S Z); solve + + The names of the established holes are returned. + + Note: This was added to the original tactic language to allow elaborator reflection. + + * - matchApply + - Attempt to apply an operator to fill the current hole, potentially solving arguments by matching. + + The return value is the list of holes established for the arguments to the function. + + Note that not all of the returned hole names still exist, as they may have been solved. + + - @ op the term to apply + - @ argSpec instructions for finding the arguments to the term, where the Boolean states whether or not to attempt to solve the argument by matching. + + Signature: + + matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName) + + * - focus + - Move the focus to the specified hole, bringing it to the front of the hole queue. Fails if the hole does not exist. + + @ hole the hole to focus on + + Signature: + + focus : (hole : TTName) -> Elab () + + * - unfocus + - Send the currently-focused hole to the end of the hole queue and focus on the next hole. + + Signature: + + unfocus : TTName -> Elab () + + * - attack + - Convert a hole to make it suitable for bindings. + + + .. image:: ../image/attack.png + :width: 152px + :height: 70px + :alt: diagram illustrating attack tactic + + + The binding tactics require that a hole be directly under its binding, or else the scopes of the generated terms won't make sense. This tactic creates a new hole of the proper form, and points the old hole at it. + + Signature: + + attack : Elab () + + * - claim + - Establish a new hole binding named n with type t, surrounding the current focus. + + Introduce a new hole with a specified name and type. + + The new hole will be focused, and the previously-focused hole will be immediately after it in the hole queue. Because this tactic introduces a new binding, you may need to 'attack' first. + + Signature: + + claim : TTName -> Raw -> Elab () + + * - patvar + - Convert a hole into a pattern variable. + + Signature: + + patvar : TTName -> Elab () + + * - compute + - Normalise the goal. + + Often this is not necessary because normanisation is applied during other tactics. + + Signature: + + compute : Elab () + + * - normalise + - Normalise a term in some lexical environment + + - @ env the environment in which to compute (get one of these from `getEnv`) + - @ term the term to normalise + + Signature: + + normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT + + * - whnf + - Reduce a closed term to weak-head normal form + + @ term the term to reduce + + Signature: + + whnf : (term : TT) -> Elab TT + + * - convertsInEnv + - Check that two terms are convertible in the current context and in some environment. + + - @ env a lexical environment to compare the terms in (see `getEnv`) + - @ term1 the first term to convert + - @ term2 the second term to convert + + Signature: + + convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab () + + * - converts + - Check that two terms are convertable in the current context and environment + + - @ term1 the first term to convert + - @ term2 the second term to convertconverts : (term1, term2 : TT) -> Elab () + + converts term1 term2 = convertsInEnv !getEnv term1 term2 + + * - getSourceLocation + - Find the source context for the elaboration script + + Signature: + + getSourceLocation : Elab SourceLocation + + * - sourceLocation + - Attempt to solve the current goal with the source code + + locationsourceLocation : Elab () + + .. code-block:: idris + + sourceLocation = do loc <- getSourceLocation + fill (quote loc) + solve + + * - currentNamespace + - Get the current namespace at the point of tactic execution. This allows scripts to define top-level names conveniently. + + The namespace is represented as a reverse-order list of strings, just as in the representation of names. + + Signature: + + currentNamespace : Elab (List String) + + * - rewriteWith + - Attempt to rewrite the goal using an equality. + + The tactic searches the goal for applicable subterms, and constructs a context for `replace` using them. In some cases, this is not possible, and `replace` must be called manually with an appropriate context. + + Because this tactic internally introduces a `let` binding, it requires that the hole be immediately under its binder (use 'attack' if it might not be). + + Signature: + + rewriteWith : Raw -> Elab () + + * - resolveTC + - Attempt to solve the current goal with an interface dictionary + + @ fn the name of the definition being elaborated (to prevent Idris from looping) + + Signature: + + resolveTC : (fn : TTName) -> Elab () + + * - search + - Use Idris's internal proof search. + + Signature: + + search : Elab () + + * - search' + - Use Idris's internal proof search, with more control. + + - @ depth the search depth + - @ hints additional names to try + + Signature: + + search' : (depth : Int) -> (hints : List TTName) -> Elab () + + * - operatorFixity + - Look up the declared fixity for an operator. + + The lookup fails if the operator does not yet have a fixity or if the string is not a valid operator. + + @ operator the operator string to look up + + Signature: + + operatorFixity : (operator : String) -> Elab Fixity + + * - debug + - Halt elaboration, dumping the internal state for inspection. + + This is intended for elaboration script developers, not for end-users. Use `fail` for final scripts. + + Signature: + + debug : Elab a + + If 'debug' is not the last tactic then make sure its type is sufficiently constrained. In particular, its type is Elab a, but there's no way for Idris to find out which type was meant for a. This can be fixed by either writing an explicit type (e.g. debug {a = ()}) or by using a helper that constrains the type (such as simple in Pruviloj, e.g. simple debug as a line). + + .. code-block:: idris + + %language ElabReflection + + idNat : Nat -> Nat + idNat = %runElab (do intro `{{x}} + debug {a = ()} + fill (Var `{{x}}) + solve) + + * - debugMessage + - Halt elaboration, dumping the internal state and displaying a message. + + This is intended for elaboration script developers, not for end-users. Use `fail` for final scripts. + + @ msg the message to display + + Signature: + + debugMessage : (msg : List ErrorReportPart) -> Elab a + + If 'debugMessage' is not the last tactic then make sure its type is sufficiently constrained. In particular, its type is Elab a, but there's no way for Idris to find out which type was meant for a. This can be fixed by either writing an explicit type (e.g. debugMessage [TextPart "message"] {a = ()}) or by using a helper that constrains the type (such as simple in Pruviloj, e.g. simple debug as a line). + + .. code-block:: idris + + %language ElabReflection + idNat : Nat -> Nat + idNat = %runElab (do intro `{{x}} + debugMessage [TextPart "error message"] {a = ()} + fill (Var `{{x}}) + solve) + + * - metavar + - Create a new top-level metavariable to solve the current hole. + + @ name the name for the top-level variable + + Signature: + + metavar : (name : TTName) -> Elab () + + * - runElab + - Recursively invoke the reflected elaborator with some goal. + + The result is the final term and its type. + + Signature: + + runElab : Raw -> Elab () -> Elab (TT, TT) + + +Read and Write State +-------------------- + +.. list-table:: + :widths: 10 30 + :stub-columns: 1 + + * - getEnv + - Look up the lexical binding at the focused hole. Fails if no holes are present. + + Signature: + + getEnv : Elab (List (TTName, Binder TT)) + + * - getGoal + - Get the name and type of the focused hole. Fails if not holes are present. + + Signature: + + getGoal : Elab (TTName, TT) + + * - getHoles + - Get the hole queue, in order. + + Signature: + + getHoles : Elab (List TTName) + + * - getGuess + - If the current hole contains a guess, return it. Otherwise, fail. + + Signature: + + getGuess : Elab TT + + * - lookupTy + - Look up the types of every overloading of a name. + + Signature: + + lookupTy : TTName -> Elab (List (TTName, NameType, TT)) + + * - lookupTyExact + - Get the type of a fully-qualified name. Fail if it doesn't resolve uniquely. + + Signature: + + lookupTyExact : TTName -> Elab (TTName, NameType, TT) + + * - lookupDatatype + - Find the reflected representation of all datatypes whose names are overloadings of some name. + + Signature: + + lookupDatatype : TTName -> Elab (List Datatype) + + * - lookupDatatypeExact + - Find the reflected representation of a datatype, given its fully-qualified name. Fail if the name does not uniquely resolve to a datatype. + + Signature: + + lookupDatatypeExact : TTName -> Elab Datatype + + * - lookupFunDefn + - Find the reflected function definition of all functions whose names are overloadings of some name. + + Signature: + + lookupFunDefn : TTName -> Elab (List (FunDefn TT)) + + * - lookupFunDefnExact + - Find the reflected function definition of a function, given its fully-qualified name. Fail if the name does not uniquely resolve to a function. + + Signature: + + lookupFunDefnExact : TTName -> Elab (FunDefn TT) + + * - lookupArgs + - Get the argument specification for each overloading of a name. + + Signature: + + lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw)) + + * - lookupArgsExact + - Get the argument specification for a name. Fail if the name does not uniquely resolve. + + Signature: + + lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw) + + * - check + - Attempt to type-check a term, getting back itself and its type. + + - @ env the environment within which to check the type + - @ tm the term to check + + Signature: + + check : (env : List (TTName, Binder TT)) -> (tm : Raw) -> Elab (TT, TT) + +Error Handling +-------------- + +.. list-table:: + :widths: 10 30 + :stub-columns: 1 + + * - tryCatch + - `tryCatch t (\err => t')` will run `t`, and if it fails, roll back the elaboration state and run `t'`, + but with access to the knowledge of why `t` failed. + + Signature: + + tryCatch : Elab a -> (Err -> Elab a) -> Elab a + + .. code-block:: idris + + %language ElabReflection + + f : Err -> Elab () + f (Msg _) = fill `("message error") + f (CantUnify _ _ _ _ _ _) = fill `("unification error") + f _ = fill `("other") + + s2 : String + s2 = %runElab (do tryCatch (fill `(True)) f ; solve) + + * - fail + - Halt elaboration with an error + + Signature: + + fail : List ErrorReportPart -> Elab a + + Note: we may need to make sure the return type 'a' is sufficiently constrained. If required add an explicit type {a = ()}. + + Below is some code which includes 'fail'. This will always fail but we could replace 'True' with some more useful condition. + + .. code-block:: idris + + %language ElabReflection + + id1 : Elab () + id1 = do + intro `{{x}} + fill (Var `{{x}}) + if True + then + fail [TextPart "put error message here"] + else + solve + + idNat : Nat -> Nat + idNat = %runElab id1 diff --git a/docs/proofs/tactics.rst b/docs/proofs/tactics.rst new file mode 100644 index 0000000000..be34a4e6a3 --- /dev/null +++ b/docs/proofs/tactics.rst @@ -0,0 +1,430 @@ +Elaborator Reflection - Tactics +=============================== + +The Idris part of the code for elaborator reflection is in +Elab.idr ``_ +Before looking at the Elab monad we need to know how to construct terms. + + +Proof State +----------- + +The terminology 'Proof State' is used by analogy to proof assistants but, as used here, it's really more of a metaprogramming state. + +Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are: + +- 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`_. +- A goal type - The type of the term that is under construction for the current goal. +- A possibly incomplete proof term, which is being calculated and should be the goal type at the end of elaboration. +- Context - A collection of open unification problems, representing recoverable failures of unification that may yet unify once more variables are solved. + +There are many other pieces of information in the proof state such as the names used , such as the bodies of case blocks that need to be elaborated.but, for now, we will leave the system to handle these. + +.. image:: ../image/elabProofState.png + :width: 283px + :height: 232px + +Names TTName +------------ + +Names in an Idris program are evaluated at runtime but sometimes a 'variable name' is needed, which can be referred to as an unevaluated symbol. +The names used in terms have different constructors depending on their type: + ++---------------------------+-----------------------------------------------+ +| UN String | A user-provided name | ++---------------------------+-----------------------------------------------+ +| NS (UN "foo") ["B", "A"]) | A name in some namespace | ++---------------------------+-----------------------------------------------+ +| MN Int String | Machine-chosen names | ++---------------------------+-----------------------------------------------+ +| SN SpecialName | Special names, to make conflicts impossible | +| | and language features predictable | ++---------------------------+-----------------------------------------------+ + + +A user defined name can be constructed like this: + +.. code-block:: idris + + Idris> UN "x" + UN "x" : TTName + +.. code-block:: idris + + Idris> NS (UN "x") ["b","a"] + NS (UN "x") ["b", "a"] : TTName + +.. list-table:: machine-chosen names + + * - A machine-chosen name needs to be generated within an Elab monad (see below for details) and is unique within that monad. This produced: {abc_140}{abc_141} so although gensym "abc" was called twice each one had a different integer: + - example of unique names: + + .. code-block:: idris + + implementation Show TTName where + show (UN s) = "`{{"++s++"}}" + show (NS t a) = "{"++(show t)++ + "."++(show a)++"}" + show (MN i s) = "{"++s++"_"++(show i)++"}" + show (SN sn) = "TTName special name" + + showGensym : String + showGensym = %runElab (do + debugMessage [TextPart ( + show !(gensym "abc") ++ + show !(gensym "abc") + )] + ) + +Quasiquotation +-------------- + +Since names are used frequently in elaborator reflection there is a shortcut for constructing them: + +.. list-table:: + + * - An unresolved variable "x" is wrapped in backtick and double braces: + - .. code-block:: idris + + Idris> `{{x}} + UN "x" : TTName + + + * - Single braces are used for existing variables: + - .. code-block:: idris + + Idris> `{x} + No such variable x + Idris> :let x=2 + Idris> `{x} + UN "x" : TTName + + + * - brackets are used for an expression: + + here type is inferable + - .. code-block:: idris + + Idris> :let a=2 + Idris> `(a) + P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT + + + * - Expression with explicit type: + - .. code-block:: idris + + Idris> `(a:Integer) + P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT + + + * - If we want the value we can escape from quasiquotation by using anti-quotation (tilde) + - .. code-block:: idris + + Idris> `(~a) + 2 : Integer + +quasiquotation summary: + ++------------+-----------+----------------------------------------------------------+ +| |Reification| | ++============+===========+==========================================================+ +| \`{{n}} | TTName | Use for new names. Unresolved quotation of the name n. | ++------------+-----------+----------------------------------------------------------+ +| \`{n} | TTName | Use for existing names. Resolved quotation of the name | +| | | n. n is a reference to a unique name in scope. | ++------------+-----------+----------------------------------------------------------+ +| \`(e) | | expression e for which a type is inferable. | ++------------+-----------+----------------------------------------------------------+ +| \`(e:t) | | expression e with a given type e. | ++------------+-----------+----------------------------------------------------------+ +| ~a | | anti-quotation - sub region which can be evaluated rather| +| | | than quoted. | ++------------+-----------+----------------------------------------------------------+ +|(Var\`{{x}})| Raw | | ++------------+-----------+----------------------------------------------------------+ + +TT +-- + +There is a notation for a term in TT as it is being constructed (based on a BNF-like grammar), this is used for example in the debug output, it is a compact way to see the state of the term so it is used here. +So internally the program is stored as a tree structure using the following syntax: + ++------------+-------+-------------+---------------------------------------------+ +| | | Syntax | More Information | ++============+=======+=============+=============================================+ +| term | | t | | ++------------+-------+-------------+---------------------------------------------+ +| binding | | b | | ++------------+-------+-------------+---------------------------------------------+ +| constant | t ::= | c | | ++------------+-------+-------------+---------------------------------------------+ +| variable | t ::= | x | | ++------------+-------+-------------+---------------------------------------------+ +| variable | t ::= | b.t | so a dot '.' tells us this is some sort of | +| binding | | | binding. | ++------------+-------+-------------+---------------------------------------------+ +| application| t ::= | t t | As with Idris, juxtaposition indicates | +| | | | function application. Note: the same symbol | +| | | | 't' is used for both terms, this does not | +| | | | imply they are the same term. | ++------------+-------+-------------+---------------------------------------------+ +| Type | t ::= | T | | +| constructor| | | | ++------------+-------+-------------+---------------------------------------------+ +| Data | t ::= | C | | +| constructor| | | | ++------------+-------+-------------+---------------------------------------------+ +| function | b::= | λ c:t | colon ':' separates parameters from body of | +| | | | binding. | ++------------+-------+-------------+---------------------------------------------+ +| let binding| b::= | let\|-> t:t | | ++------------+-------+-------------+---------------------------------------------+ +| function | b::= | ∀ x:t | | ++------------+-------+-------------+---------------------------------------------+ +| Type | c::= | \*i | The universe hierarchy is usually handled | +| universe | | | automatically so we can just use\* for the | +| | | | type of types. | ++------------+-------+-------------+---------------------------------------------+ +| integer | c:== | i | | +| literal | | | | ++------------+-------+-------------+---------------------------------------------+ +|integer type| c:== | Integer | | ++------------+-------+-------------+---------------------------------------------+ +| string | c:== | s | | +| literal | | | | ++------------+-------+-------------+---------------------------------------------+ +| string type| c:== | String | | ++------------+-------+-------------+---------------------------------------------+ +|focused hole| | ?x : t | Conor McBride 1999 thesis. | ++------------+-------+-------------+---------------------------------------------+ +| guess | | ?x ≈ t : t | Conor McBride 1999 thesis. | ++------------+-------+-------------+---------------------------------------------+ + +Sometimes the part of the term in focus is underlined. + +Reflection of the well typed core language + +.. code-block:: idris + + data TT = + ||| A reference to some name (P for Parameter) + P NameType TTName TT | + ||| de Bruijn variables + V Int | + ||| Bind a variable + Bind TTName (Binder TT) TT | + ||| Apply one term to another + App TT TT | + ||| Embed a constant + TConst Const | + ||| Erased terms + Erased | + ||| The type of types along (with universe constraints) + TType TTUExp | + ||| Alternative universes for dealing with uniqueness + UType Universe | + +TT stores local bound variables using De Bruijn index, when working in Idris this does not concern the user because string names are used for variables. Converting bound variables internally to index values means that the same variable name can be used, in different lambda terms, without ambiguity and without the need for α-substitution. +De Bruijn index which is a integer where: + +- 0=inside current (inner) lambda term +- 1= next outer lambda term +- 2= next outer and so on + +Raw +--- + +Raw is similar to TT except it is used before types are known. The types should be resolved by the type checker. + +.. code-block:: idris + + data Raw = + ||| Variables, global or local + Var TTName | + ||| Bind a variable + RBind TTName (Binder Raw) Raw | + ||| Application + RApp Raw Raw | + ||| The type of types + RType | + ||| Alternative universes for dealing with uniqueness + RUType Universe | + ||| Embed a constant + RConstant Const | + +Expression Syntax +----------------- + +There is a way of notating expressions such as those used in the proof state (example: goal type and proof terms) which is reasonably standard in the papers written about this subject. + +This notation is not entered directly by metaprogrammers but it is seen, for example in debug output. So this notation is explained here because it is useful to be familiar with it. + +The notation assumes right-associativity, in the absence of brackets, the term to the right binds more tightly than the one on the left. +So, for nested lambda terms: + ++---------------+--------+-------------------+ +| λ a . λ b . f | means | λ a .( λ b . f) | ++---------------+--------+-------------------+ + +and the same for function application: + ++---------------+--------+-------------------+ +| f g x | means | f (g x) | ++---------------+--------+-------------------+ + +In contrast, in lambda calculus, function application is usually regarded as left-associative, +Here are some typical examples of the notation used for expressions: + ++-----------------------+ +| ? {hole_0} . {hole_0} | ++-----------------------+ + +The term, to be derived, may start off in this state following something like this: + +.. code-block:: idris + + myScript : Elab () + myScript= do + +The dot '.' tells us this is some sort of binding. + ++----------------------------------------------+ +| ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0} | ++----------------------------------------------+ + +This is a slightly more complicated example arising from: + +.. code-block:: idris + + idNat : Nat -> Nat + idNat = %runElab (do + +This introduces a guess that hole_0 = hole_2 . + ++----------------------------------------------------+ +| ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0} | ++----------------------------------------------------+ + +Following on from the previous example a lambda function is introduced like this: + +.. code-block:: idris + + intro `{{x}} + +So now the expression is wrapped in a lambda binding. + ++-------------------------------------------------------+ +| ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0} | ++-------------------------------------------------------+ + +Following on, we can use the fill tactic like this: + +.. code-block:: idris + + fill (Var `{{x}}) + +which introduces another guess. + ++--------------------------------+ +| ?{hole_0} ≈ λ x . x . {hole_0} | ++--------------------------------+ + +The solve tactic completes the proof + +Binders +------- + +Here we look at each tactic in turn to see how they affect the proof state. + +Introduction tactics for binders. The binder types are: + +- lambda function (intro) +- dependent function (forall) +- let (letBind) +- pattern (patbind) + +A precondition of these tactics is that the focused hole is of the form: + ++-----------+ +| ?h : t.h | ++-----------+ + +that is, that the body of its scope consists directly of a reference to the hole-bound variable. If a hole binder were of the form: + ++--------------------+ +| ?h : t1 -> t2.f h | ++--------------------+ + +and a tactic such as + ++------------------+ +| intro \`{{x}} | ++------------------+ + +were applied, the result would be the term + ++---------------------------+ +| ?h : t2 . λ x:t1. f h | ++---------------------------+ + +However this would cause the application of f to be ill-typed, as it expects an argument of type t1->t2, not an argument of type t2. Additionally, some binding tactics require that t, the type of the hole h, have a specific form, because the binder to be established may have a typing rule associated with it. + +.. list-table:: Binders + :widths: 10 30 + :stub-columns: 1 + + * - intro + - Introduce a lambda binding around the current hole and focus on the body. + + Requires that the hole be in binding form (use 'attack' if it might not be). + + @ n the name to use for the argument. + + Signature: + + intro : (n : TTName) -> Elab () + + Result + + λn:t1.?h:[n/x]t2.h + + * - intro' + - Introduce a lambda binding around the current hole and focus on the body, using the name provided by the type of the hole. + + Requires that the hole be immediately under its binder (use 'attack' if it might not be). + + Signature: + + intro' : Elab () + + * - forall + - Introduce a dependent function type binding into the current hole, and focus on the body. Requires that the hole be immediately under its binder + + (use 'attack' if it might not be). + + Signature: + + forall : TTName -> Raw -> Elab () + + * - patbind + - Introduce a new pattern binding. Requires that the hole be immediately under its binder (use 'attack' if it might not be). + + Signature: + + patbind : TTName -> Elab () + + * - letbind + - Introduce a new let binding. + + Requires that the hole be immediately under its binder (use 'attack' if it might not be). + + - @ n the name to let bind + - @ ty the type of the term to be let-bound + - @ tm the term to be bound + + Signature: + + letbind : (n : TTName) -> (ty, tm : Raw) -> Elab () + +.. target-notes:: +.. _`Dependently Typed Functional Programs and their Proofs by McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374