git.iko.soy/Idris-dev
on master help sign in
Generalize the types of mkApp and unApply

Now, they accept any Foldable and work for both the TT and Raw representations.

commit0f00278f916ea428b4a77e51dca6291dc6e827da authorDavid Christiansen <david@davidchristiansen.dk> dateThu 10 Mar 2016, 10:54 (11 years ago) parent449089d
4 files changed+24−28
compare with master
unifiedsplit
libs/base/Language/Reflection/Utils.idr+23−10 libs/pruviloj/Pruviloj/Internals.idr−10 test/meta002/AgdaStyleReflection.idr−7 test/meta002/expected+1−1
libs/base/Language/Reflection/Utils.idr+23−10
@@ -40,17 +40,30 @@ getUName (UN n) = Just n
4040getUName (NS n ns) = getUName n
4141getUName _ = Nothing
4242
43−total
44−unApply : TT -> (TT, List TT)
45−unApply t = unA t []
46− where unA : TT -> List TT -> (TT, List TT)
47− unA (App fn arg) args = unA fn (arg::args)
48− unA tm args = (tm, args)
43+namespace TT
44+ total
45+ unApply : TT -> (TT, List TT)
46+ unApply t = unA t []
47+ where unA : TT -> List TT -> (TT, List TT)
48+ unA (App fn arg) args = unA fn (arg::args)
49+ unA tm args = (tm, args)
50+
51+ total
52+ mkApp : Foldable f => TT -> f TT -> TT
53+ mkApp f args = foldl App f args
54+
55+namespace Raw
56+ total
57+ unApply : Raw -> (Raw, List Raw)
58+ unApply tm = unApply' tm []
59+ where unApply' : Raw -> List Raw -> (Raw, List Raw)
60+ unApply' (RApp f x) xs = unApply' f (x::xs)
61+ unApply' notApp xs = (notApp, xs)
62+
63+ total
64+ mkApp : Foldable f => Raw -> f Raw -> Raw
65+ mkApp f args = foldl RApp f args
4966
50−total
51−mkApp : TT -> List TT -> TT
52−mkApp tm [] = tm
53−mkApp tm (a::as) = mkApp (App tm a) as
5467
5568total
5669binderTy : Binder t -> t
libs/pruviloj/Pruviloj/Internals.idr−10
@@ -26,16 +26,6 @@ updateTyConArgTy f (TyConParameter a) =
2626updateTyConArgTy f (TyConIndex a) =
2727 TyConIndex (record {type = f (type a) } a)
2828
29−unApply : Raw -> (Raw, List Raw)
30−unApply tm = unApply' tm []
31− where unApply' : Raw -> List Raw -> (Raw, List Raw)
32− unApply' (RApp f x) xs = unApply' f (x::xs)
33− unApply' notApp xs = (notApp, xs)
34−
35−mkApp : Raw -> List Raw -> Raw
36−mkApp f [] = f
37−mkApp f (x :: xs) = mkApp (RApp f x) xs
38−
3929||| Grab the binders from around a term, alpha-converting to make
4030||| their names unique
4131partial
test/meta002/AgdaStyleReflection.idr−7
@@ -40,13 +40,6 @@ data Term
4040 | Constant Const
4141 | Ty
4242
43−unApply : Raw -> (Raw, List Raw)
44−unApply tm = unApply' tm []
45− where unApply' : Raw -> List Raw -> (Raw, List Raw)
46− unApply' (RApp f x) xs = unApply' f (x::xs)
47− unApply' notApp xs = (notApp, xs)
48−
49−
5043implementation Quotable Plicity Raw where
5144 quotedTy = `(Plicity)
5245 quote Explicit = `(Explicit)
test/meta002/expected+1−1
@@ -6,7 +6,7 @@ When checking right hand side of testElab3 with expected type
66 DPair Ty (Tm [])
77
88Unifying ty and ARR ty t would lead to infinite value
9−AgdaStyleReflection.idr:328:5:
9+AgdaStyleReflection.idr:321:5:
1010When checking right hand side of baz with expected type
1111 (Nat, Void)
1212