git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3470 from xekoukou/remove_util_fun

Pruviloj: Use binderTy from Language.Reflection.Utils.

commit59287a72b6e13262c13ac43dd1f85852f9c4ecfc authorDavid Christiansen <david@davidchristiansen.dk> dateSat 1 Oct 2016, 08:43 (10 years ago) parent692d610fc7c458
2 files changed+5−15
compare with master
unifiedsplit
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+2−2 libs/pruviloj/Pruviloj/Internals.idr+3−13
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+2−2
@@ -63,7 +63,7 @@ mkIh info motiveName recArg argty fam =
6363 focus ihT
6464 attack
6565 for_ {b=()} argArgs $ \(n, b) =>
66− forall n (getBinderTy b)
66+ forall n (binderTy b)
6767 let argTm : Raw = mkApp (Var recArg) (map (Var . fst) argArgs)
6868 argTmTy <- forget (snd !(check !getEnv argTm))
6969 argHoles <- apply (Var motiveName)
@@ -239,7 +239,7 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =
239239
240240 where bindLam : List (TTName, Binder Raw) -> Raw -> Raw
241241 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
243243
244244getElimClauses : TyConInfo -> (elimn : TTName) ->
245245 List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
libs/pruviloj/Pruviloj/Internals.idr+3−13
@@ -1,7 +1,7 @@
11||| Internal details of the library, not for public consumption.
22module Pruviloj.Internals
33
4−
4+import Language.Reflection.Utils
55import Pruviloj.Core
66import Pruviloj.Renamers
77
@@ -50,16 +50,6 @@ extractBinders (RBind n b tm) = let (bs, res) = extractBinders tm
5050extractBinders tm = ([], tm)
5151
5252
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
6353
6454||| Map a list `[x1, x2, ..., xn]` to `[(0, x1), (1, x2), ..., (n-1, xn)]`
6555enumerate : List a -> List (Nat, a)
@@ -70,11 +60,11 @@ enumerate xs = enumerate' xs 0
7060
7161bindPats : List (TTName, Binder Raw) -> Raw -> Raw
7262bindPats [] 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
7464
7565bindPatTys : List (TTName, Binder Raw) -> Raw -> Raw
7666bindPatTys [] 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
7868
7969
8070||| Helper for elaborating pattern clauses. This helper takes care of