@@ -0,0 +1,184 @@
1+module Finite
2+
3+import Data.Fin
4+import Language.Reflection.Elab
5+import Language.Reflection.Utils
6+
7+-- Test various features of reflected elaboration, including looking
8+-- up datatypes, defining functions, and totality checking
9+
10+%default total
11+
12+||| A bijection between some type and bounded numbers
13+data Finite : Type -> Nat -> Type where
14+ IsFinite : (toFin : a -> Fin n) ->
15+ (fromFin : Fin n -> a) ->
16+ (ok1 : (x : a) -> fromFin (toFin x) = x) ->
17+ (ok2 : (y : Fin n) -> toFin (fromFin y) = y) ->
18+ Finite a n
19+
20+acceptableConstructor : Raw -> Bool
21+acceptableConstructor (Var _) = True
22+acceptableConstructor _ = False
23+
24+mkFin : Nat -> Nat -> Elab Raw
25+mkFin Z j = fail [TermPart `(Fin Z), TextPart "is uninhabitable!"]
26+mkFin (S k) Z = return `(FZ {k=~(quote k)})
27+mkFin (S k) (S j) = do i <- mkFin k j
28+ return `(FS {k=~(quote k)} ~i)
29+
30+mkToClause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
31+mkToClause fn size i (n, Var ty) =
32+ MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
33+mkToClause fn size i (n, ty) =
34+ fail [TextPart "unsupported constructor", NamePart n]
35+
36+
37+mkFromClause : TTName -> (size, i : Nat) ->
38+ (constr : (TTName, Raw)) ->
39+ Elab FunClause
40+mkFromClause fn size i (n, Var ty) =
41+ return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
42+mkFromClause fn size i (n, ty) =
43+ fail [TextPart "unsupported constructor", NamePart n]
44+
45+
46+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
47+mkOk1Clause fn size i (n, Var ty) =
48+ return $ MkFunClause (RApp (Var fn) (Var n))
49+ [| (Var (UN "Refl")) (Var ty) (Var n) |]
50+mkOk1Clause fn size i (n, ty) =
51+ fail [TextPart "unsupported constructor", NamePart n]
52+
53+
54+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
55+mkOk2Clause fn size i (n, Var ty) =
56+ return $ MkFunClause (RApp (Var fn) !(mkFin size i))
57+ [| (Var "Refl") `(Fin ~(quote size))
58+ !(mkFin size i) |]
59+mkOk2Clause fn size i (n, ty) =
60+ fail [TextPart "unsupported constructor", NamePart n]
61+
62+
63+mkToClauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
64+mkToClauses fn size xs = mkToClauses' Z xs
65+ where mkToClauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
66+ mkToClauses' k [] = return []
67+ mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
68+ clause <- mkToClause fn size k x
69+ return $ clause :: rest
70+
71+||| Generate a clause for the end of a pattern-match on Fins that
72+||| declares its own impossibility.
73+|||
74+||| This is to satisfy the totality checker, because `impossible`
75+||| clauses are still
76+mkAbsurdFinClause : (fn : TTName) -> (goal : Raw -> Raw) -> (size : Nat) ->
77+ Elab FunClause
78+mkAbsurdFinClause fn goal size =
79+ do pv <- gensym "badfin"
80+ lhsArg <- lhsBody pv size
81+ let lhs = RBind pv (PVar `(Fin Z : Type))
82+ (RApp (Var fn) lhsArg)
83+ let rhs = RBind pv (PVar `(Fin Z : Type))
84+ `(FinZElim {a=~(goal lhsArg)} ~(Var pv))
85+ return $ MkFunClause lhs rhs
86+ where lhsBody : TTName -> Nat -> Elab Raw
87+ lhsBody f Z = return $ Var f
88+ lhsBody f (S k) = do smaller <- lhsBody f k
89+ return `(FS {k=~(quote k)} ~smaller)
90+
91+
92+mkFromClauses : TTName -> TTName -> Nat ->
93+ List (TTName, Raw) -> Elab (List FunClause)
94+mkFromClauses fn ty size xs = mkFromClauses' Z xs
95+ where mkFromClauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
96+ mkFromClauses' k [] =
97+ return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
98+ mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
99+ clause <- mkFromClause fn size k x
100+ return $ clause :: rest
101+
102+mkOk1Clauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
103+mkOk1Clauses fn size xs = mkOk1Clauses' Z xs
104+ where mkOk1Clauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
105+ mkOk1Clauses' k [] = return []
106+ mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
107+ clause <- mkOk1Clause fn size k x
108+ return $ clause :: rest
109+
110+mkOk2Clauses : TTName -> Nat -> List (TTName, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
111+mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs
112+ where mkOk2Clauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
113+ mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]
114+ mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
115+ clause <- mkOk2Clause fn size k x
116+ return $ clause :: rest
117+
118+
119+genToFin : (to, from, ok1, ok2, ty : TTName) -> Elab ()
120+genToFin to from ok1 ok2 ty =
121+ do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty
122+ let size = length constrs
123+ argn <- gensym "arg"
124+ declareType $ Declare to [Explicit argn (Var ty)]
125+ `(Fin ~(quote size))
126+ toClauses <- mkToClauses to size constrs
127+ defineFunction $ DefineFun to toClauses
128+
129+ argn' <- gensym "arg"
130+ declareType $ Declare from [Explicit argn' `(Fin ~(quote size))]
131+ (Var ty)
132+ fromClauses <- mkFromClauses from ty size constrs
133+ defineFunction $ DefineFun from fromClauses
134+
135+ argn'' <- gensym "arg"
136+ declareType $ Declare ok1 [Explicit argn'' (Var ty)]
137+ `((=) {A=~(Var ty)} {B=~(Var ty)}
138+ ~(RApp (Var from) (RApp (Var to) (Var argn'')))
139+ ~(Var argn''))
140+ ok1Clauses <- mkOk1Clauses ok1 size constrs
141+ defineFunction $ DefineFun ok1 ok1Clauses
142+
143+ argn''' <- gensym "arg"
144+ let fty : Raw = `(Fin ~(quote size))
145+ let ok2ResTy = the (Raw -> Raw)
146+ (\n => `((=) {A=~fty} {B=~fty}
147+ ~(RApp (Var to) (RApp (Var from) n))
148+ ~n))
149+ declareType $ Declare ok2 [Explicit argn''' fty]
150+ (ok2ResTy (Var argn'''))
151+ ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy
152+ defineFunction $ DefineFun ok2 ok2Clauses
153+
154+ return ()
155+
156+
157+deriveFinite : Elab ()
158+deriveFinite =
159+ do (App (App (P _ `{Finite} _) (P _ tyn _)) _) <- snd <$> getGoal
160+ | ty => fail [TextPart "inapplicable goal type", TermPart ty]
161+ (MkDatatype _ _ _ constrs) <- lookupDatatypeExact tyn
162+ let size = length constrs
163+ let to = SN (MetaN tyn (UN "toFinite"))
164+ let from = SN (MetaN tyn (UN "fromFinite"))
165+ let ok1 = SN (MetaN tyn (UN "finiteOk1"))
166+ let ok2 = SN (MetaN tyn (UN "finiteOk2"))
167+ genToFin to from ok1 ok2 tyn
168+ fill `(IsFinite {a=~(Var tyn)} {n=~(quote size)}
169+ ~(Var to) ~(Var from)
170+ ~(Var ok1) ~(Var ok2))
171+ solve
172+
173+data TwoStateModel = Alive | Dead
174+data ThreeStateModel = Working | Disabled | Deceased
175+
176+
177+twoStateFinite : Finite TwoStateModel 2
178+twoStateFinite = %runElab deriveFinite
179+
180+threeStateFinite : Finite ThreeStateModel 3
181+threeStateFinite = %runElab deriveFinite
182+
183+boolFinite : Finite Bool 2
184+boolFinite = %runElab deriveFinite