@@ -42,10 +42,12 @@ This was generated by the following code:
43 addTwo : Elab ()
43 addTwo : Elab ()
44 addTwo = do let twoname : TTName = `{{TwoDef.Two}}
44 addTwo = do let twoname : TTName = `{{TwoDef.Two}}
45+ let F2 = `{{TwoDef.F}}
46+ let T2 = `{{TwoDef.T}}
45 declareDatatype $ Declare twoname [] `(Type)
47 declareDatatype $ Declare twoname [] `(Type)
46 defineDatatype $ DefineDatatype twoname [
48 defineDatatype $ DefineDatatype twoname [
47− Constructor `{{F}} [] (Var `{{TwoDef.Two}}),
49+ Constructor `{{F}} [] (Var `{{TwoDef.Two}}),
48− Constructor `{{T}} [] (Var `{{TwoDef.Two}})
50+ Constructor `{{T}} [] (Var `{{TwoDef.Two}})
51 %runElab addTwo
53 %runElab addTwo
@@ -96,31 +98,29 @@ Note: The left hand side (lhs) and right hand side (rhs) of FunClause typically
97 λΠ> :printdef perm1
99 λΠ> :printdef perm1
98 perm1 : Two -> Two
100 perm1 : Two -> Two
99− F = F
101+ perm1 F = F
100− T = T
102+ perm1 T = T
101 λΠ> :printdef perm2
103 λΠ> :printdef perm2
102 perm2 : Two -> Two
104 perm2 : Two -> Two
103− F = F
105+ perm1 F = T
104− T = T
106+ perm1 T = F
106This was generated with the following code:
108This was generated with the following code:
108.. code-block:: idris
110.. code-block:: idris
110 let perm1 = `{{TwoDef.perm1}}
112 let perm1 = `{{TwoDef.perm1}}
111− let F2 = `{{TwoDef.F}}
112− let T2 = `{{TwoDef.T}}
113 declareType (Declare perm1 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname))
113 declareType (Declare perm1 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname))
114 defineFunction $ DefineFun perm1 [
114 defineFunction $ DefineFun perm1 [
115− MkFunClause (Var F2) (Var F2),
115+ MkFunClause (RApp (Var perm1) (Var `{{TwoDef.F}})) (Var F2),
116− MkFunClause (Var T2) (Var T2)
116+ MkFunClause (RApp (Var perm1) (Var `{{TwoDef.T}})) (Var T2)
119 let perm2 = `{{TwoDef.perm2}}
119 let perm2 = `{{TwoDef.perm2}}
120 declareType (Declare perm2 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname))
120 declareType (Declare perm2 [MkFunArg `{{code}} (Var twoname) Explicit NotErased] (Var twoname))
121 defineFunction $ DefineFun perm2 [
121 defineFunction $ DefineFun perm2 [
122− MkFunClause (Var F2) (Var T2),
122+ MkFunClause (RApp (Var perm1) (Var `{{TwoDef.F}})) (Var T2),
123− MkFunClause (Var T2) (Var F2)
123+ MkFunClause (RApp (Var perm1) (Var `{{TwoDef.T}})) (Var F2)
126.. list-table::
126.. list-table::
@@ -128,10 +128,14 @@ This was generated with the following code:
128 * - This is what happens when we call the functions:
128 * - This is what happens when we call the functions:
129 - .. code-block:: idris
129 - .. code-block:: idris
131 λΠ> perm1 T
133 λΠ> perm1 T
132− F T : Two
136+ T : Two
133 λΠ> perm2 T
137 λΠ> perm2 T
134− F T : Two
138+ F : Two
136So 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.
140So 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.