git.iko.soy/Idris-dev
on master help sign in
Generalize the types of mkApp and unApply
0f00278David Christiansen
libs/base/Language/Reflection/Utils.idr+23−10
compare with master
unifiedsplit
@@ -40,17 +40,30 @@ getUName (UN n) = Just n
40getUName (NS n ns) = getUName n
40getUName (NS n ns) = getUName n
41getUName _ = Nothing
41getUName _ = Nothing
42
42
43+namespace TT
43−total
44+ total
44−unApply : TT -> (TT, List TT)
45+ unApply : TT -> (TT, List TT)
45−unApply t = unA t []
46+ unApply t = unA t []
46− where unA : TT -> List TT -> (TT, List TT)
47+ where unA : TT -> List TT -> (TT, List TT)
47− unA (App fn arg) args = unA fn (arg::args)
48+ unA (App fn arg) args = unA fn (arg::args)
48− unA tm args = (tm, 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
49
66
50−total
51−mkApp : TT -> List TT -> TT
52−mkApp tm [] = tm
53−mkApp tm (a::as) = mkApp (App tm a) as
54
67
55total
68total
56binderTy : Binder t -> t
69binderTy : Binder t -> t
libs/pruviloj/Pruviloj/Internals.idr−10
@@ -26,16 +26,6 @@ updateTyConArgTy f (TyConParameter a) =
26updateTyConArgTy f (TyConIndex a) =
26updateTyConArgTy f (TyConIndex a) =
27 TyConIndex (record {type = f (type a) } a)
27 TyConIndex (record {type = f (type a) } a)
28
28
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−
39||| Grab the binders from around a term, alpha-converting to make
29||| Grab the binders from around a term, alpha-converting to make
40||| their names unique
30||| their names unique
41partial
31partial
test/meta002/AgdaStyleReflection.idr−7
@@ -40,13 +40,6 @@ data Term
40 | Constant Const
40 | Constant Const
41 | Ty
41 | Ty
42
42
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−
50implementation Quotable Plicity Raw where
43implementation Quotable Plicity Raw where
51 quotedTy = `(Plicity)
44 quotedTy = `(Plicity)
52 quote Explicit = `(Explicit)
45 quote Explicit = `(Explicit)
test/meta002/expected+1−1
@@ -6,7 +6,7 @@ When checking right hand side of testElab3 with expected type
6 DPair Ty (Tm [])
6 DPair Ty (Tm [])
7
7
8Unifying ty and ARR ty t would lead to infinite value
8Unifying ty and ARR ty t would lead to infinite value
9−AgdaStyleReflection.idr:328:5:
9+AgdaStyleReflection.idr:321:5:
10When checking right hand side of baz with expected type
10When checking right hand side of baz with expected type
11 (Nat, Void)
11 (Nat, Void)
12
12