@@ -27,42 +27,44 @@ mkFin (S k) Z = return `(FZ {k=~(quote k)})
2727mkFin (S k) (S j) = do i <- mkFin k j
2828 return `(FS {k=~(quote k)} ~i)
2929
30−mkToClause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
31−mkToClause fn size i (n, Var ty) =
30+mkToClause : TTName -> (size, i : Nat) ->
31+ (constr : (TTName, List Arg, Raw)) ->
32+ Elab FunClause
33+mkToClause fn size i (n, [], Var ty) =
3234 MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
33−mkToClause fn size i (n, ty) =
35+mkToClause fn size i (n, _, ty) =
3436 fail [TextPart "unsupported constructor", NamePart n]
3537
3638
3739mkFromClause : TTName -> (size, i : Nat) ->
38− (constr : (TTName, Raw)) ->
40+ (constr : (TTName, List Arg, Raw)) ->
3941 Elab FunClause
40−mkFromClause fn size i (n, Var ty) =
42+mkFromClause fn size i (n, [], Var ty) =
4143 return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
42−mkFromClause fn size i (n, ty) =
44+mkFromClause fn size i (n, _, ty) =
4345 fail [TextPart "unsupported constructor", NamePart n]
4446
4547
46−mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
47−mkOk1Clause fn size i (n, Var ty) =
48+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List Arg, Raw)) -> Elab FunClause
49+mkOk1Clause fn size i (n, [], Var ty) =
4850 return $ MkFunClause (RApp (Var fn) (Var n))
4951 [| (Var (UN "Refl")) (Var ty) (Var n) |]
50−mkOk1Clause fn size i (n, ty) =
52+mkOk1Clause fn size i (n, _, ty) =
5153 fail [TextPart "unsupported constructor", NamePart n]
5254
5355
54−mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
55−mkOk2Clause fn size i (n, Var ty) =
56+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List Arg, Raw)) -> Elab FunClause
57+mkOk2Clause fn size i (n, [], Var ty) =
5658 return $ MkFunClause (RApp (Var fn) !(mkFin size i))
5759 [| (Var "Refl") `(Fin ~(quote size))
5860 !(mkFin size i) |]
59−mkOk2Clause fn size i (n, ty) =
61+mkOk2Clause fn size i (n, _, ty) =
6062 fail [TextPart "unsupported constructor", NamePart n]
6163
6264
63−mkToClauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
65+mkToClauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
6466mkToClauses fn size xs = mkToClauses' Z xs
65− where mkToClauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
67+ where mkToClauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
6668 mkToClauses' k [] = return []
6769 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
6870 clause <- mkToClause fn size k x
@@ -90,26 +92,26 @@ mkAbsurdFinClause fn goal size =
9092
9193
9294mkFromClauses : TTName -> TTName -> Nat ->
93− List (TTName, Raw) -> Elab (List FunClause)
95+ List (TTName, List Arg, Raw) -> Elab (List FunClause)
9496mkFromClauses fn ty size xs = mkFromClauses' Z xs
95− where mkFromClauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
97+ where mkFromClauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
9698 mkFromClauses' k [] =
9799 return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
98100 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
99101 clause <- mkFromClause fn size k x
100102 return $ clause :: rest
101103
102−mkOk1Clauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
104+mkOk1Clauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
103105mkOk1Clauses fn size xs = mkOk1Clauses' Z xs
104− where mkOk1Clauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
106+ where mkOk1Clauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
105107 mkOk1Clauses' k [] = return []
106108 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
107109 clause <- mkOk1Clause fn size k x
108110 return $ clause :: rest
109111
110−mkOk2Clauses : TTName -> Nat -> List (TTName, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
112+mkOk2Clauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
111113mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs
112− where mkOk2Clauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
114+ where mkOk2Clauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
113115 mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]
114116 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
115117 clause <- mkOk2Clause fn size k x
@@ -121,19 +123,19 @@ genToFin to from ok1 ok2 ty =
121123 do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty
122124 let size = length constrs
123125 argn <- gensym "arg"
124− declareType $ Declare to [Explicit argn (Var ty)]
126+ declareType $ Declare to [Explicit argn NotErased (Var ty)]
125127 `(Fin ~(quote size))
126128 toClauses <- mkToClauses to size constrs
127129 defineFunction $ DefineFun to toClauses
128130
129131 argn' <- gensym "arg"
130− declareType $ Declare from [Explicit argn' `(Fin ~(quote size))]
132+ declareType $ Declare from [Explicit argn' NotErased `(Fin ~(quote size))]
131133 (Var ty)
132134 fromClauses <- mkFromClauses from ty size constrs
133135 defineFunction $ DefineFun from fromClauses
134136
135137 argn'' <- gensym "arg"
136− declareType $ Declare ok1 [Explicit argn'' (Var ty)]
138+ declareType $ Declare ok1 [Explicit argn'' NotErased (Var ty)]
137139 `((=) {A=~(Var ty)} {B=~(Var ty)}
138140 ~(RApp (Var from) (RApp (Var to) (Var argn'')))
139141 ~(Var argn''))
@@ -146,7 +148,7 @@ genToFin to from ok1 ok2 ty =
146148 (\n => `((=) {A=~fty} {B=~fty}
147149 ~(RApp (Var to) (RApp (Var from) n))
148150 ~n))
149− declareType $ Declare ok2 [Explicit argn''' fty]
151+ declareType $ Declare ok2 [Explicit argn''' NotErased fty]
150152 (ok2ResTy (Var argn'''))
151153 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy
152154 defineFunction $ DefineFun ok2 ok2Clauses