0 | module Derive.Enum
  1 |
  2 | import public Data.Enum
  3 | import public Derive.Finite
  4 | import Language.Reflection.Util
  5 |
  6 | %default total
  7 |
  8 | --------------------------------------------------------------------------------
  9 | --          Claims
 10 | --------------------------------------------------------------------------------
 11 |
 12 | export
 13 | conIndexLtName : Named a => a -> Name
 14 | conIndexLtName v = funName v "conIndexLt"
 15 |
 16 | export
 17 | toIndexName : Named a => a -> Name
 18 | toIndexName v = funName v "toIndex"
 19 |
 20 | export
 21 | toIndexInjectiveName : Named a => a -> Name
 22 | toIndexInjectiveName v = funName v "toIndexInjective"
 23 |
 24 | export
 25 | valuesCompleteName : Named a => a -> Name
 26 | valuesCompleteName v = funName v "valuesComplete"
 27 |
 28 | ||| Top-level function declaration of a proof that all constructor indexes
 29 | ||| are less than the total number of constructors.
 30 | export
 31 | conIndexLtClaim : Visibility -> (cifun, fun : Name) -> (p : TypeInfo) -> Decl
 32 | conIndexLtClaim vis cifun fun p =
 33 |   let civ := var cifun
 34 |       tot := primVal (B32 $ cast $ length p.cons)
 35 |       arg := MkArg MW ExplicitArg (Just "v") p.applied
 36 |       tpe := piAll `(cast {to = Bits32} (~(civ) v) < ~(tot)) (p.implicits ++ [arg])
 37 |    in claim M0 vis [] fun tpe
 38 |
 39 | ||| Top-level function declaration of a proof that all the `conIndexXY`
 40 | ||| function is injective.
 41 | export
 42 | toIndexInjectiveClaim : Visibility -> (tifun, fun : Name) -> (p : TypeInfo) -> Decl
 43 | toIndexInjectiveClaim vis tifun fun p =
 44 |   let civ := var tifun
 45 |       a1  := MkArg MW ExplicitArg (Just "x") p.applied
 46 |       a2  := MkArg MW ExplicitArg (Just "y") p.applied
 47 |       prf := MkArg MW ExplicitArg (Just "prf") `(~(civ) x === ~(civ) y)
 48 |       tpe := piAll `(x === y) (p.implicits ++ [a1,a2,prf])
 49 |    in claim M0 vis [] fun tpe
 50 |
 51 | ||| Top-level function declaration of a proof that every value is
 52 | ||| indeed included in `Data.Finite.values`.
 53 | export
 54 | valuesCompleteClaim : Visibility -> (fun : Name) -> (p : TypeInfo) -> Decl
 55 | valuesCompleteClaim vis fun p =
 56 |   let arg := MkArg MW ExplicitArg (Just "v") p.applied
 57 |       tpe := piAll `(Data.List.Elem.Elem v Data.Finite.values) (p.implicits ++ [arg])
 58 |    in claim M0 vis [] fun tpe
 59 |
 60 | ||| Top-level function declaration for a conversion of a data constructor
 61 | ||| to a value of type `Index n`, where `n` is the number of data constructors
 62 | ||| of the type.
 63 | export
 64 | toIndexClaim : Visibility -> (fun : Name) -> (p : TypeInfo) -> Decl
 65 | toIndexClaim vis fun p =
 66 |   let tot := primVal (B32 $ cast $ length p.cons)
 67 |       arg := MkArg MW ExplicitArg (Just "v") p.applied
 68 |       tpe := piAll `(Index ~(tot)) (p.implicits ++ [arg])
 69 |    in simpleClaim vis fun tpe
 70 |
 71 | ||| Top-level `Enum` implementation declaration
 72 | export
 73 | enumClaim : Visibility -> (fun : Name) -> (p : TypeInfo) -> Decl
 74 | enumClaim vis fun p =
 75 |   let tot := primVal (B32 $ cast $ length p.cons)
 76 |    in implClaimVis vis fun `(Enum ~(p.applied) ~(tot))
 77 |
 78 | --------------------------------------------------------------------------------
 79 | --          Definitions
 80 | --------------------------------------------------------------------------------
 81 |
 82 | export
 83 | conIndexLtDef : (fun : Name) -> TypeInfo -> Decl
 84 | conIndexLtDef f p = def f $ map cclause p.cons
 85 |   where
 86 |     cclause : Con p.arty p.args -> Clause
 87 |     cclause c = patClause (var f `app` bindAny c) `(Data.Prim.Bits32.mkLT Refl)
 88 |
 89 | export
 90 | toIndexDef : (fun, cif, ltp : Name) -> Decl
 91 | toIndexDef f cif ltp =
 92 |  let rhs := `(I (cast {to = Bits32} (~(var cif) v)) @{~(var ltp) v})
 93 |   in def f [patClause (var f `app` var "v") rhs]
 94 |
 95 | export
 96 | toIndexInjectiveDef : (fun : Name) -> TypeInfo -> Decl
 97 | toIndexInjectiveDef f p = def f $ map cclause p.cons
 98 |   where
 99 |     cclause : Con p.arty p.args -> Clause
100 |     cclause c = patClause (appAll f [bindAny c, bindAny c, `(Refl)]) `(Refl)
101 |
102 | export
103 | valuesCompleteDef : (fun : Name) -> TypeInfo -> Decl
104 | valuesCompleteDef f p = def f (clauses [<] `(Here) p.cons)
105 |   where
106 |     clauses : SnocList Clause -> TTImp -> List (Con p.arty p.args) -> List Clause
107 |     clauses sc prf []        = sc <>> []
108 |     clauses sc prf (x :: xs) =
109 |      let c := patClause (var f `app` bindAny x) prf
110 |       in clauses (sc:<c) `(There ~(prf)) xs
111 |
112 | export
113 | enumDef : (f, ti, inj, comp : Name) -> Decl
114 | enumDef f ti inj comp =
115 |   def f [patClause (var f) `(MkEnum ~(var ti) ~(var inj) ~(var comp))]
116 |
117 | --------------------------------------------------------------------------------
118 | --          Deriving
119 | --------------------------------------------------------------------------------
120 |
121 | ||| Generates a proof that the constructor index returned by `conIndexXY` is
122 | ||| strictly less than the number of constructors.
123 | export
124 | ConIndexLtVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
125 | ConIndexLtVis vis nms p =
126 |   let ci   := conIndexName p
127 |       fun  := conIndexLtName p
128 |    in Right
129 |         [ TL (conIndexLtClaim vis ci fun p.info) (conIndexLtDef fun p.info)
130 |         ]
131 |
132 | ||| Alias for `ConIndexLtVis Export`
133 | export %inline
134 | ConIndexLt : List Name -> ParamTypeInfo -> Res (List TopLevel)
135 | ConIndexLt = ConIndexLtVis Export
136 |
137 | ||| Generates a conversion of data constructors to values of type `Index n`,
138 | ||| where `n` is the number of data constructors of the given type.
139 | |||
140 | ||| This includes `ConIndexLtVis`
141 | export
142 | ToIndexVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
143 | ToIndexVis vis nms p =
144 |   let fun  := toIndexName p
145 |       cif  := conIndexName p
146 |       ltp  := conIndexLtName p
147 |    in sequenceJoin
148 |         [ ConIndexLtVis vis nms p
149 |         , Right [TL (toIndexClaim vis fun p.info) (toIndexDef fun cif ltp)]
150 |         ]
151 |
152 | ||| Alias for `ToIndexVis Export`
153 | export %inline
154 | ToIndex : List Name -> ParamTypeInfo -> Res (List TopLevel)
155 | ToIndex = ToIndexVis Export
156 |
157 | ||| Generates a proof that the `toIndexXY` function is injective.
158 | export
159 | ToIndexInjectiveVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
160 | ToIndexInjectiveVis vis nms p =
161 |   let ti   := toIndexName p
162 |       fun  := toIndexInjectiveName p
163 |    in Right
164 |         [ TL (toIndexInjectiveClaim vis ti fun p.info) (toIndexInjectiveDef fun p.info)
165 |         ]
166 |
167 | ||| Alias for `ToIndexInjectiveVis Export`
168 | export %inline
169 | ToIndexInjective : List Name -> ParamTypeInfo -> Res (List TopLevel)
170 | ToIndexInjective = ToIndexInjectiveVis Export
171 |
172 | ||| Generates a proof that the `Data.Finite.values` indeed contains every
173 | ||| possible value. This currently only works for enum types.
174 | export
175 | ValuesCompleteVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
176 | ValuesCompleteVis vis nms p =
177 |   let fun := valuesCompleteName p
178 |    in Right
179 |         [ TL (valuesCompleteClaim vis fun p.info) (valuesCompleteDef fun p.info)
180 |         ]
181 |
182 | ||| Alias for `ValuesCompleteVis Export`
183 | export %inline
184 | ValuesComplete : List Name -> ParamTypeInfo -> Res (List TopLevel)
185 | ValuesComplete = ValuesCompleteVis Export
186 |
187 | ||| Derives interfaces `Eq`, `Ord`, `Finite`, and `Enum` plus utility
188 | ||| functions with the relevant proofs for the given type.
189 | |||
190 | ||| Erased proofs are generated at `export` visibility.
191 | export
192 | EnumVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
193 | EnumVis vis nms p =
194 |   let fun := implName p "Enum"
195 |       ti  := toIndexName p
196 |       inj := toIndexInjectiveName p
197 |       cmp := valuesCompleteName p
198 |    in sequenceJoin
199 |         [ EqVis vis nms p
200 |         , OrdVis vis nms p
201 |         , FiniteVis vis nms p
202 |         , ToIndex nms p
203 |         , ToIndexInjective nms p
204 |         , ValuesComplete nms p
205 |         , Right [TL (enumClaim vis fun p.info) (enumDef fun ti inj cmp)]
206 |         ]
207 |
208 | ||| Alias for `ValuesCompleteVis Export`
209 | export %inline
210 | Enum : List Name -> ParamTypeInfo -> Res (List TopLevel)
211 | Enum = EnumVis Public
212 |