git.iko.soy/Idris-dev
on master help sign in
Pruviloj: Use binderTy from Language.Reflection.Utils.
fc7c458Apostolis Xekoukoulotakis
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+2−2
compare with master
unifiedsplit
@@ -63,7 +63,7 @@ mkIh info motiveName recArg argty fam =
63 focus ihT
63 focus ihT
64 attack
64 attack
65 for_ {b=()} argArgs $ \(n, b) =>
65 for_ {b=()} argArgs $ \(n, b) =>
66− forall n (getBinderTy b)
66+ forall n (binderTy b)
67 let argTm : Raw = mkApp (Var recArg) (map (Var . fst) argArgs)
67 let argTm : Raw = mkApp (Var recArg) (map (Var . fst) argArgs)
68 argTmTy <- forget (snd !(check !getEnv argTm))
68 argTmTy <- forget (snd !(check !getEnv argTm))
69 argHoles <- apply (Var motiveName)
69 argHoles <- apply (Var motiveName)
@@ -239,7 +239,7 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
239
239
240 where bindLam : List (TTName, Binder Raw) -> Raw -> Raw
240 where bindLam : List (TTName, Binder Raw) -> Raw -> Raw
241 bindLam [] x = x
241 bindLam [] x = x
242− bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x
242+ bindLam ((n, b)::rest) x = RBind n (Lam (binderTy b)) $ bindLam rest x
243
243
244getElimClauses : TyConInfo -> (elimn : TTName) ->
244getElimClauses : TyConInfo -> (elimn : TTName) ->
245 List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
245 List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
libs/pruviloj/Pruviloj/Internals.idr+3−13
@@ -1,7 +1,7 @@
1||| Internal details of the library, not for public consumption.
1||| Internal details of the library, not for public consumption.
2module Pruviloj.Internals
2module Pruviloj.Internals
3
3
4−
4+import Language.Reflection.Utils
5import Pruviloj.Core
5import Pruviloj.Core
6import Pruviloj.Renamers
6import Pruviloj.Renamers
7
7
@@ -50,16 +50,6 @@ extractBinders (RBind n b tm) = let (bs, res) = extractBinders tm
50extractBinders tm = ([], tm)
50extractBinders tm = ([], tm)
51
51
52
52
53−||| Get the type annotation from a binder
54−getBinderTy : Binder t -> t
55−getBinderTy (Lam t) = t
56−getBinderTy (Pi t _) = t
57−getBinderTy (Let t _) = t
58−getBinderTy (Hole t) = t
59−getBinderTy (GHole t) = t
60−getBinderTy (Guess t _) = t
61−getBinderTy (PVar t) = t
62−getBinderTy (PVTy t) = t
63
53
64||| Map a list `[x1, x2, ..., xn]` to `[(0, x1), (1, x2), ..., (n-1, xn)]`
54||| Map a list `[x1, x2, ..., xn]` to `[(0, x1), (1, x2), ..., (n-1, xn)]`
65enumerate : List a -> List (Nat, a)
55enumerate : List a -> List (Nat, a)
@@ -70,11 +60,11 @@ enumerate xs = enumerate' xs 0
70
60
71bindPats : List (TTName, Binder Raw) -> Raw -> Raw
61bindPats : List (TTName, Binder Raw) -> Raw -> Raw
72bindPats [] res = res
62bindPats [] res = res
73−bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res
63+bindPats ((n, b)::bs) res = RBind n (PVar (binderTy b)) $ bindPats bs res
74
64
75bindPatTys : List (TTName, Binder Raw) -> Raw -> Raw
65bindPatTys : List (TTName, Binder Raw) -> Raw -> Raw
76bindPatTys [] res = res
66bindPatTys [] res = res
77−bindPatTys ((n, b)::bs) res = RBind n (PVTy (getBinderTy b)) $ bindPatTys bs res
67+bindPatTys ((n, b)::bs) res = RBind n (PVTy (binderTy b)) $ bindPatTys bs res
78
68
79
69
80||| Helper for elaborating pattern clauses. This helper takes care of
70||| Helper for elaborating pattern clauses. This helper takes care of