@@ -27,42 +27,44 @@ mkFin (S k) Z = return `(FZ {k=~(quote k)})
27mkFin (S k) (S j) = do i <- mkFin k j
27mkFin (S k) (S j) = do i <- mkFin k j
28 return `(FS {k=~(quote k)} ~i)
28 return `(FS {k=~(quote k)} ~i)
30−mkToClause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
30+mkToClause : TTName -> (size, i : Nat) ->
31+ (constr : (TTName, List Arg, Raw)) ->
31−mkToClause fn size i (n, Var ty) =
33+mkToClause fn size i (n, [], Var ty) =
32 MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
34 MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
33−mkToClause fn size i (n, ty) =
35+mkToClause fn size i (n, _, ty) =
34 fail [TextPart "unsupported constructor", NamePart n]
36 fail [TextPart "unsupported constructor", NamePart n]
37mkFromClause : TTName -> (size, i : Nat) ->
39mkFromClause : TTName -> (size, i : Nat) ->
38− (constr : (TTName, Raw)) ->
40+ (constr : (TTName, List Arg, Raw)) ->
39 Elab FunClause
41 Elab FunClause
40−mkFromClause fn size i (n, Var ty) =
42+mkFromClause fn size i (n, [], Var ty) =
41 return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
43 return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
42−mkFromClause fn size i (n, ty) =
44+mkFromClause fn size i (n, _, ty) =
43 fail [TextPart "unsupported constructor", NamePart n]
45 fail [TextPart "unsupported constructor", NamePart n]
46−mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
48+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List Arg, Raw)) -> Elab FunClause
47−mkOk1Clause fn size i (n, Var ty) =
49+mkOk1Clause fn size i (n, [], Var ty) =
48 return $ MkFunClause (RApp (Var fn) (Var n))
50 return $ MkFunClause (RApp (Var fn) (Var n))
49 [| (Var (UN "Refl")) (Var ty) (Var n) |]
51 [| (Var (UN "Refl")) (Var ty) (Var n) |]
50−mkOk1Clause fn size i (n, ty) =
52+mkOk1Clause fn size i (n, _, ty) =
51 fail [TextPart "unsupported constructor", NamePart n]
53 fail [TextPart "unsupported constructor", NamePart n]
54−mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
56+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List Arg, Raw)) -> Elab FunClause
55−mkOk2Clause fn size i (n, Var ty) =
57+mkOk2Clause fn size i (n, [], Var ty) =
56 return $ MkFunClause (RApp (Var fn) !(mkFin size i))
58 return $ MkFunClause (RApp (Var fn) !(mkFin size i))
57 [| (Var "Refl") `(Fin ~(quote size))
59 [| (Var "Refl") `(Fin ~(quote size))
58 !(mkFin size i) |]
60 !(mkFin size i) |]
59−mkOk2Clause fn size i (n, ty) =
61+mkOk2Clause fn size i (n, _, ty) =
60 fail [TextPart "unsupported constructor", NamePart n]
62 fail [TextPart "unsupported constructor", NamePart n]
63−mkToClauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
65+mkToClauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
64mkToClauses fn size xs = mkToClauses' Z xs
66mkToClauses 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)
66 mkToClauses' k [] = return []
68 mkToClauses' k [] = return []
67 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
69 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
68 clause <- mkToClause fn size k x
70 clause <- mkToClause fn size k x
@@ -90,26 +92,26 @@ mkAbsurdFinClause fn goal size =
92mkFromClauses : TTName -> TTName -> Nat ->
94mkFromClauses : TTName -> TTName -> Nat ->
93− List (TTName, Raw) -> Elab (List FunClause)
95+ List (TTName, List Arg, Raw) -> Elab (List FunClause)
94mkFromClauses fn ty size xs = mkFromClauses' Z xs
96mkFromClauses 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)
96 mkFromClauses' k [] =
98 mkFromClauses' k [] =
97 return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
99 return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
98 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
100 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
99 clause <- mkFromClause fn size k x
101 clause <- mkFromClause fn size k x
100 return $ clause :: rest
102 return $ clause :: rest
102−mkOk1Clauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
104+mkOk1Clauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
103mkOk1Clauses fn size xs = mkOk1Clauses' Z xs
105mkOk1Clauses 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)
105 mkOk1Clauses' k [] = return []
107 mkOk1Clauses' k [] = return []
106 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
108 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
107 clause <- mkOk1Clause fn size k x
109 clause <- mkOk1Clause fn size k x
108 return $ clause :: rest
110 return $ clause :: rest
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)
111mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs
113mkOk2Clauses 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)
113 mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]
115 mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]
114 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
116 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
115 clause <- mkOk2Clause fn size k x
117 clause <- mkOk2Clause fn size k x
@@ -121,19 +123,19 @@ genToFin to from ok1 ok2 ty =
121 do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty
123 do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty
122 let size = length constrs
124 let size = length constrs
123 argn <- gensym "arg"
125 argn <- gensym "arg"
124− declareType $ Declare to [Explicit argn (Var ty)]
126+ declareType $ Declare to [Explicit argn NotErased (Var ty)]
125 `(Fin ~(quote size))
127 `(Fin ~(quote size))
126 toClauses <- mkToClauses to size constrs
128 toClauses <- mkToClauses to size constrs
127 defineFunction $ DefineFun to toClauses
129 defineFunction $ DefineFun to toClauses
129 argn' <- gensym "arg"
131 argn' <- gensym "arg"
130− declareType $ Declare from [Explicit argn' `(Fin ~(quote size))]
132+ declareType $ Declare from [Explicit argn' NotErased `(Fin ~(quote size))]
132 fromClauses <- mkFromClauses from ty size constrs
134 fromClauses <- mkFromClauses from ty size constrs
133 defineFunction $ DefineFun from fromClauses
135 defineFunction $ DefineFun from fromClauses
135 argn'' <- gensym "arg"
137 argn'' <- gensym "arg"
136− declareType $ Declare ok1 [Explicit argn'' (Var ty)]
138+ declareType $ Declare ok1 [Explicit argn'' NotErased (Var ty)]
137 `((=) {A=~(Var ty)} {B=~(Var ty)}
139 `((=) {A=~(Var ty)} {B=~(Var ty)}
138 ~(RApp (Var from) (RApp (Var to) (Var argn'')))
140 ~(RApp (Var from) (RApp (Var to) (Var argn'')))
139 ~(Var argn''))
141 ~(Var argn''))
@@ -146,7 +148,7 @@ genToFin to from ok1 ok2 ty =
146 (\n => `((=) {A=~fty} {B=~fty}
148 (\n => `((=) {A=~fty} {B=~fty}
147 ~(RApp (Var to) (RApp (Var from) n))
149 ~(RApp (Var to) (RApp (Var from) n))
149− declareType $ Declare ok2 [Explicit argn''' fty]
151+ declareType $ Declare ok2 [Explicit argn''' NotErased fty]
150 (ok2ResTy (Var argn'''))
152 (ok2ResTy (Var argn'''))
151 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy
153 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy
152 defineFunction $ DefineFun ok2 ok2Clauses
154 defineFunction $ DefineFun ok2 ok2Clauses