8c64728 · Idris-dev · git.iko.soy

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

41getUName _ = Nothing

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) =

27 TyConIndex (record {type = f (type a) } a)

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

41 | Ty

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 [])

7

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

11 (Nat, Void)

12