git.iko.soy/Idris-dev
on master help sign in
changes to generatingData.rst
566daf7Martin Baker
docs/proofs/generatingData.rst+90−81
compare with master
unifiedsplit
@@ -1,11 +1,88 @@
1Generating Data and Functions at Compile Time
1Generating Data and Functions at Compile Time
2=============================================
2=============================================
3
3
4−We can construct a data structure at compile-time in an Elab monad.
4+We can construct a datatype at compile-time in an Elab monad.
5This can allow proofs to be generated for user defined types or it could allow types to be automatically generated to support user defined types.
5This can allow proofs to be generated for user defined types or it could allow types to be automatically generated to support user defined types.
6An example is the code, from `Elaborator reflection: extending Idris in Idris`_, that automatically generates accessibility predicates using the Bove-Capretta method.
6An example is the code, from `Elaborator reflection: extending Idris in Idris`_, that automatically generates accessibility predicates using the Bove-Capretta method.
7−The following simple outline example is adapted from
7+
8−`<https://github.com/idris-lang/Idris-dev/blob/master/test/meta002/DataDef.idr>`_
8+Here is a simple example constucting a boolean type:
9+
10+.. code-block:: idris
11+
12+ module TwoDef
13+ %language ElabReflection
14+
15+ addTwo : Elab ()
16+ addTwo = do let twoname : TTName = `{{TwoDef.Two}}
17+ declareDatatype $ Declare twoname [] `(Type)
18+ defineDatatype $ DefineDatatype twoname [
19+ Constructor `{{F}} [] (Var `{{TwoDef.Two}}),
20+ Constructor `{{T}} [] (Var `{{TwoDef.Two}})
21+ ]
22+
23+ %runElab addTwo
24+
25+.. list-table::
26+
27+ * - This type is now availible to us as if we had compiled it in the usual way:
28+ - .. code-block:: idris
29+
30+ λΠ> :printdef Two
31+ data Two : Type where
32+ F : Two
33+ T : Two
34+
35+ * - The constructors are T and F:
36+ - .. code-block:: idris
37+
38+ λΠ> F
39+ F : Two
40+ λΠ> T
41+ T : Two
42+
43+We can now add some function definitions to the above code:
44+
45+.. code-block:: idris
46+
47+ let perm1 = `{{TwoDef.perm1}}
48+ let F2 = `{{TwoDef.F}}
49+ let T2 = `{{TwoDef.T}}
50+ declareType (Declare perm1 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname))
51+ defineFunction $ DefineFun perm1 [
52+ MkFunClause (Var F2) (Var F2),
53+ MkFunClause (Var T2) (Var T2)
54+ ]
55+
56+ let perm2 = `{{TwoDef.perm2}}
57+ declareType (Declare perm2 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname))
58+ defineFunction $ DefineFun perm2 [
59+ MkFunClause (Var F2) (Var T2),
60+ MkFunClause (Var T2) (Var F2)
61+ ]
62+
63+.. list-table::
64+
65+ * - Here are the functions:
66+ - .. code-block:: idris
67+
68+ λΠ> :printdef perm1
69+ perm1 : Two -> Two
70+ F = F
71+ T = T
72+ λΠ> :printdef perm2
73+ perm2 : Two -> Two
74+ F = F
75+ T = T
76+
77+ * - This is what happens when we call the functions:
78+ - .. code-block:: idris
79+
80+ λΠ> perm1 T
81+ F T : Two
82+ λΠ> perm2 T
83+ F T : Two
84+
85+Here is an example with parameters:
9
86
10.. code-block:: idris
87.. code-block:: idris
11
88
@@ -18,9 +95,9 @@ The following simple outline example is adapted from
18 declareDatatype $ Declare dataname [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)
95 declareDatatype $ Declare dataname [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)
19 defineDatatype $ DefineDatatype dataname [
96 defineDatatype $ DefineDatatype dataname [
20 Constructor `{{MkN}} [MkFunArg `{{x}} `(Nat) Implicit NotErased]
97 Constructor `{{MkN}} [MkFunArg `{{x}} `(Nat) Implicit NotErased]
21− (RApp (Var `{{DataDef.N}}) (Var `{{x}})),
98+ (RApp (Var dataname) (Var `{{x}})),
22 Constructor `{{MkN'}} [MkFunArg `{{x}} `(Nat) Explicit NotErased]
99 Constructor `{{MkN'}} [MkFunArg `{{x}} `(Nat) Explicit NotErased]
23− (RApp (Var `{{DataDef.N}}) (RApp (Var `{S}) (Var `{{x}})))
100+ (RApp (Var dataname) (RApp (Var `{S}) (Var `{{x}})))
24 ]
101 ]
25
102
26 %runElab addData
103 %runElab addData
@@ -46,80 +123,8 @@ Which can be used like this:
46 λΠ> :t MkN
123 λΠ> :t MkN
47 MkN : N x
124 MkN : N x
48
125
49−Here is another, more complicated, example from the same test file. This also creates a function.
50
126
51−.. code-block:: idris
52−
53− module DataDef
54− %language ElabReflection
55−
56− mkU : Elab ()
57− mkU = do
58− let U = `{{DataDef.U}}
59− let el = `{{DataDef.el}}
60− declareDatatype $ Declare U [] `(Type)
61− declareType $ Declare el [MkFunArg `{{code}} (Var U) Explicit NotErased] `(Type)
62− defineDatatype $ DefineDatatype U [
63− Constructor `{{Base}} [] (Var U),
64− Constructor `{{Pi}}
65− [MkFunArg `{{code}} (Var U) Explicit NotErased,
66− MkFunArg `{{body}} `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)) Explicit NotErased]
67− (Var U)
68− ]
69− defineFunction $ DefineFun el [
70− MkFunClause (RBind `{{code}} (PVar (Var U))
71− (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))
72− (RApp (Var el)
73− (RApp (RApp (Var `{{DataDef.Pi}})
74− (Var `{{code}}))
75− (Var `{{body}})))))
76− (RBind `{{code}} (PVar (Var U))
77− (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))
78− (RBind `{{x}} (Pi (RApp (Var el) (Var `{{code}})) `(Type))
79− (RApp (Var el) (RApp (Var `{{body}}) (Var `{{x}})))))),
80− MkFunClause (RApp (Var el) (Var `{{DataDef.Base}})) `(Bool)
81− ]
82−
83− %runElab mkU
84−
85−This code generates the following data and function:
86−
87−.. code-block:: idris
88−
89− data U : Type where
90− Base : U
91− Pi : (code : U) -> (el code -> U) -> U
92− el : U -> Type
93− el (Pi code body) = (x : el code) -> el (body x)
94− el Base = Bool
95−
96−.. list-table:: Usage
97−
98− * - We can then use U the data structure, like this:
99− - examples
100−
101− .. code-block:: idris
102−
103− λΠ> :t U
104− U : Type
105− λΠ> :doc U
106− No documentation for U
107− λΠ> Base
108− Base : U
109− λΠ> DataDef.Pi
110− Pi : (code : U) -> (el code -> U) -> U
111−
112− * - el is the function that has been defined:
113− - examples
114−
115− .. code-block:: idris
116−
117− λΠ> :t el
118− el : U -> Type
119− λΠ> el Base
120− Bool : Type
121−
122−So these are the functions that we can use to create data and functions in the Elab monad:
127+These are the functions that we can use to create data and functions in the Elab monad:
123
128
124.. list-table:: Generating Data and Functions
129.. list-table:: Generating Data and Functions
125 :widths: 10 30
130 :widths: 10 30
@@ -153,8 +158,10 @@ So these are the functions that we can use to create data and functions in the E
153 * - addImplementation
158 * - addImplementation
154 - Register a new implementation for interface resolution.
159 - Register a new implementation for interface resolution.
155
160
161+ Arguments:
162+
156− - @ ifaceName the name of the interface for which an implementation is being registered
163+ - ifaceName the name of the interface for which an implementation is being registered
157− - @ implName the name of the definition to use in implementation search
164+ - implName the name of the definition to use in implementation search
158
165
159 Signature:
166 Signature:
160
167
@@ -163,7 +170,9 @@ So these are the functions that we can use to create data and functions in the E
163 * - isTCName
170 * - isTCName
164 - Determine whether a name denotes an interface.
171 - Determine whether a name denotes an interface.
165
172
173+ Arguments:
174+
166− @ name a name that might denote an interface.
175+ - name - a name that might denote an interface.
167
176
168 Signature:
177 Signature:
169
178