@@ -1,11 +1,88 @@
11Generating Data and Functions at Compile Time
22=============================================
33
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.
55This can allow proofs to be generated for user defined types or it could allow types to be automatically generated to support user defined types.
66An 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
8−`<https://github.com/idris-lang/Idris-dev/blob/master/test/meta002/DataDef.idr>`_
7+
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:
986
1087.. code-block:: idris
1188
@@ -18,9 +95,9 @@ The following simple outline example is adapted from
1895 declareDatatype $ Declare dataname [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)
1996 defineDatatype $ DefineDatatype dataname [
2097 Constructor `{{MkN}} [MkFunArg `{{x}} `(Nat) Implicit NotErased]
21− (RApp (Var `{{DataDef.N}}) (Var `{{x}})),
98+ (RApp (Var dataname) (Var `{{x}})),
2299 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}})))
24101 ]
25102
26103 %runElab addData
@@ -46,80 +123,8 @@ Which can be used like this:
46123 λΠ> :t MkN
47124 MkN : N x
48125
49−Here is another, more complicated, example from the same test file. This also creates a function.
50126
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:
123128
124129.. list-table:: Generating Data and Functions
125130 :widths: 10 30
@@ -153,8 +158,10 @@ So these are the functions that we can use to create data and functions in the E
153158 * - addImplementation
154159 - Register a new implementation for interface resolution.
155160
156− - @ 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
161+ Arguments:
162+
163+ - ifaceName the name of the interface for which an implementation is being registered
164+ - implName the name of the definition to use in implementation search
158165
159166 Signature:
160167
@@ -163,7 +170,9 @@ So these are the functions that we can use to create data and functions in the E
163170 * - isTCName
164171 - Determine whether a name denotes an interface.
165172
166− @ name a name that might denote an interface.
173+ Arguments:
174+
175+ - name - a name that might denote an interface.
167176
168177 Signature:
169178