git.iko.soy/Idris-dev
on master help sign in
changes to generatingData.rst
ff054c1Martin Baker
docs/proofs/generatingData.rst+45−33
compare with master
unifiedsplit
@@ -23,7 +23,17 @@ Which declare and define the datatype as the names suggest.
23 :height: 246px
23 :height: 246px
24 :alt: diagram illustrating data structures associated with declareDatatype defineDatatype.
24 :alt: diagram illustrating data structures associated with declareDatatype defineDatatype.
25
25
26−Here is a simple example constructing a boolean type:
26+.. list-table::
27+
28+ * - 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:
29+ - .. code-block:: idris
30+
31+ λΠ> :printdef Two
32+ data Two : Type where
33+ F : Two
34+ T : Two
35+
36+This was generated by the following code:
27
37
28.. code-block:: idris
38.. code-block:: idris
29
39
@@ -42,15 +52,7 @@ Here is a simple example constructing a boolean type:
42
52
43.. list-table::
53.. list-table::
44
54
45− * - This type is now available to us as if we had compiled it in the usual way:
46− - .. code-block:: idris
47−
48− λΠ> :printdef Two
49− data Two : Type where
50− F : Two
51− T : Two
52−
53− * - The constructors are T and F:
55+ * - The constructors T and F can be called as would be expected:
54 - .. code-block:: idris
56 - .. code-block:: idris
55
57
56 λΠ> F
58 λΠ> F
@@ -76,7 +78,23 @@ Which declare and define the function as the names suggest.
76 :height: 246px
78 :height: 246px
77 :alt: diagram illustrating data structures associated with declareDatatype defineDatatype.
79 :alt: diagram illustrating data structures associated with declareDatatype defineDatatype.
78
80
81+Note: FunClause - holds a 'let' clause, the left hand side (lhs) and right hand side (rhs) must have the same type. TT does not have 'where' clauses because they are desugared out.
82+
83+.. list-table::
84+
79−We can now add some function definitions to the above datatype:
85+ * - Some function definitions can now be added to the above datatype. This is what they will look like:
86+ - .. code-block:: idris
87+
88+ λΠ> :printdef perm1
89+ perm1 : Two -> Two
90+ F = F
91+ T = T
92+ λΠ> :printdef perm2
93+ perm2 : Two -> Two
94+ F = F
95+ T = T
96+
97+This was generated with the following code:
80
98
81.. code-block:: idris
99.. code-block:: idris
82
100
@@ -98,18 +116,6 @@ We can now add some function definitions to the above datatype:
98
116
99.. list-table::
117.. list-table::
100
118
101− * - Here are the functions:
102− - .. code-block:: idris
103−
104− λΠ> :printdef perm1
105− perm1 : Two -> Two
106− F = F
107− T = T
108− λΠ> :printdef perm2
109− perm2 : Two -> Two
110− F = F
111− T = T
112−
113 * - This is what happens when we call the functions:
119 * - This is what happens when we call the functions:
114 - .. code-block:: idris
120 - .. code-block:: idris
115
121
@@ -118,7 +124,21 @@ We can now add some function definitions to the above datatype:
118 λΠ> perm2 T
124 λΠ> perm2 T
119 F T : Two
125 F T : Two
120
126
127+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.
128+
129+A Different Example which has Type Parameters
130+---------------------------------------------
131+
132+.. list-table::
133+
121−Here is an example with parameters:
134+ * - Here is an example of a datatype with type parameters:
135+ - .. code-block:: idris
136+
137+ data N : Nat -> Type where
138+ MkN : N x
139+ MkN' : (x : Nat) -> N (S x)
140+
141+This was produced by the following code:
122
142
123.. code-block:: idris
143.. code-block:: idris
124
144
@@ -138,15 +158,7 @@ Here is an example with parameters:
138
158
139 %runElab addData
159 %runElab addData
140
160
141−So this declares and defines the following data structure 'N' with a constructor 'MkN' which can have an implicit or an explicit Nat argument.
161+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:
142−
143−.. code-block:: idris
144−
145− data N : Nat -> Type where
146− MkN : N x
147− MkN' : (x : Nat) -> N (S x)
148−
149−Which can be used like this:
150
162
151.. code-block:: idris
163.. code-block:: idris
152
164