git.iko.soy/Idris-dev
on master help sign in
Update test for improved reflection API
d7db8caDavid Raymond Christiansen
test/meta001/Finite.idr+16−16
compare with master
unifiedsplit
@@ -28,7 +28,7 @@ mkFin (S k) (S j) = do i <- mkFin k j
28 return `(FS {k=~(quote k)} ~i)
28 return `(FS {k=~(quote k)} ~i)
29
29
30mkToClause : TTName -> (size, i : Nat) ->
30mkToClause : TTName -> (size, i : Nat) ->
31− (constr : (TTName, List Arg, Raw)) ->
31+ (constr : (TTName, List CtorArg, Raw)) ->
32 Elab FunClause
32 Elab FunClause
33mkToClause fn size i (n, [], Var ty) =
33mkToClause fn size i (n, [], Var ty) =
34 MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
34 MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
@@ -37,7 +37,7 @@ mkToClause fn size i (n, _, ty) =
37
37
38
38
39mkFromClause : TTName -> (size, i : Nat) ->
39mkFromClause : TTName -> (size, i : Nat) ->
40− (constr : (TTName, List Arg, Raw)) ->
40+ (constr : (TTName, List CtorArg, Raw)) ->
41 Elab FunClause
41 Elab FunClause
42mkFromClause fn size i (n, [], Var ty) =
42mkFromClause fn size i (n, [], Var ty) =
43 return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
43 return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
@@ -45,7 +45,7 @@ mkFromClause fn size i (n, _, ty) =
45 fail [TextPart "unsupported constructor", NamePart n]
45 fail [TextPart "unsupported constructor", NamePart n]
46
46
47
47
48−mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List Arg, Raw)) -> Elab FunClause
48+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause
49mkOk1Clause fn size i (n, [], Var ty) =
49mkOk1Clause fn size i (n, [], Var ty) =
50 return $ MkFunClause (RApp (Var fn) (Var n))
50 return $ MkFunClause (RApp (Var fn) (Var n))
51 [| (Var (UN "Refl")) (Var ty) (Var n) |]
51 [| (Var (UN "Refl")) (Var ty) (Var n) |]
@@ -53,7 +53,7 @@ mkOk1Clause fn size i (n, _, ty) =
53 fail [TextPart "unsupported constructor", NamePart n]
53 fail [TextPart "unsupported constructor", NamePart n]
54
54
55
55
56−mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List Arg, Raw)) -> Elab FunClause
56+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause
57mkOk2Clause fn size i (n, [], Var ty) =
57mkOk2Clause fn size i (n, [], Var ty) =
58 return $ MkFunClause (RApp (Var fn) !(mkFin size i))
58 return $ MkFunClause (RApp (Var fn) !(mkFin size i))
59 [| (Var "Refl") `(Fin ~(quote size))
59 [| (Var "Refl") `(Fin ~(quote size))
@@ -62,9 +62,9 @@ mkOk2Clause fn size i (n, _, ty) =
62 fail [TextPart "unsupported constructor", NamePart n]
62 fail [TextPart "unsupported constructor", NamePart n]
63
63
64
64
65−mkToClauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
65+mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
66mkToClauses fn size xs = mkToClauses' Z xs
66mkToClauses fn size xs = mkToClauses' Z xs
67− where mkToClauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
67+ where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
68 mkToClauses' k [] = return []
68 mkToClauses' k [] = return []
69 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
69 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
70 clause <- mkToClause fn size k x
70 clause <- mkToClause fn size k x
@@ -92,26 +92,26 @@ mkAbsurdFinClause fn goal size =
92
92
93
93
94mkFromClauses : TTName -> TTName -> Nat ->
94mkFromClauses : TTName -> TTName -> Nat ->
95− List (TTName, List Arg, Raw) -> Elab (List FunClause)
95+ List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
96mkFromClauses fn ty size xs = mkFromClauses' Z xs
96mkFromClauses fn ty size xs = mkFromClauses' Z xs
97− where mkFromClauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
97+ where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
98 mkFromClauses' k [] =
98 mkFromClauses' k [] =
99 return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
99 return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
100 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
100 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
101 clause <- mkFromClause fn size k x
101 clause <- mkFromClause fn size k x
102 return $ clause :: rest
102 return $ clause :: rest
103
103
104−mkOk1Clauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
104+mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
105mkOk1Clauses fn size xs = mkOk1Clauses' Z xs
105mkOk1Clauses fn size xs = mkOk1Clauses' Z xs
106− where mkOk1Clauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
106+ where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
107 mkOk1Clauses' k [] = return []
107 mkOk1Clauses' k [] = return []
108 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
108 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
109 clause <- mkOk1Clause fn size k x
109 clause <- mkOk1Clause fn size k x
110 return $ clause :: rest
110 return $ clause :: rest
111
111
112−mkOk2Clauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
112+mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
113mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs
113mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs
114− where mkOk2Clauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
114+ where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
115 mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]
115 mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]
116 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
116 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
117 clause <- mkOk2Clause fn size k x
117 clause <- mkOk2Clause fn size k x
@@ -123,19 +123,19 @@ genToFin to from ok1 ok2 ty =
123 do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty
123 do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty
124 let size = length constrs
124 let size = length constrs
125 argn <- gensym "arg"
125 argn <- gensym "arg"
126− declareType $ Declare to [Explicit argn NotErased (Var ty)]
126+ declareType $ Declare to [MkFunArg argn (Var ty) Explicit NotErased]
127 `(Fin ~(quote size))
127 `(Fin ~(quote size))
128 toClauses <- mkToClauses to size constrs
128 toClauses <- mkToClauses to size constrs
129 defineFunction $ DefineFun to toClauses
129 defineFunction $ DefineFun to toClauses
130
130
131 argn' <- gensym "arg"
131 argn' <- gensym "arg"
132− declareType $ Declare from [Explicit argn' NotErased `(Fin ~(quote size))]
132+ declareType $ Declare from [MkFunArg argn' `(Fin ~(quote size)) Explicit NotErased ]
133 (Var ty)
133 (Var ty)
134 fromClauses <- mkFromClauses from ty size constrs
134 fromClauses <- mkFromClauses from ty size constrs
135 defineFunction $ DefineFun from fromClauses
135 defineFunction $ DefineFun from fromClauses
136
136
137 argn'' <- gensym "arg"
137 argn'' <- gensym "arg"
138− declareType $ Declare ok1 [Explicit argn'' NotErased (Var ty)]
138+ declareType $ Declare ok1 [MkFunArg argn'' (Var ty) Explicit NotErased]
139 `((=) {A=~(Var ty)} {B=~(Var ty)}
139 `((=) {A=~(Var ty)} {B=~(Var ty)}
140 ~(RApp (Var from) (RApp (Var to) (Var argn'')))
140 ~(RApp (Var from) (RApp (Var to) (Var argn'')))
141 ~(Var argn''))
141 ~(Var argn''))
@@ -148,7 +148,7 @@ genToFin to from ok1 ok2 ty =
148 (\n => `((=) {A=~fty} {B=~fty}
148 (\n => `((=) {A=~fty} {B=~fty}
149 ~(RApp (Var to) (RApp (Var from) n))
149 ~(RApp (Var to) (RApp (Var from) n))
150 ~n))
150 ~n))
151− declareType $ Declare ok2 [Explicit argn''' NotErased fty]
151+ declareType $ Declare ok2 [MkFunArg argn''' fty Explicit NotErased]
152 (ok2ResTy (Var argn'''))
152 (ok2ResTy (Var argn'''))
153 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy
153 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy
154 defineFunction $ DefineFun ok2 ok2Clauses
154 defineFunction $ DefineFun ok2 ok2Clauses
test/tactics001/Tactics.idr+1−1
@@ -33,7 +33,7 @@ plusSuccRightSuccNew (S j) k =
33
33
34mkDecl : ()
34mkDecl : ()
35mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
35mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
36− [Implicit (UN "z") NotErased `(Nat)]
36+ [MkFunArg (UN "z") `(Nat) Implicit NotErased]
37 `(Vect ~(Var (UN "z")) ())
37 `(Vect ~(Var (UN "z")) ())
38 fill `(() : ())
38 fill `(() : ())
39 solve)
39 solve)