git.iko.soy/Idris-dev
on master help sign in
Formatting improvements
979be1fDavid Christiansen
lib/Language/Reflection/Utils.idr+34−34
compare with master
unifiedsplit
@@ -5,13 +5,13 @@ module Language.Reflection.Utils
5--------------------------------------------------------
5--------------------------------------------------------
6
6
7seq : List Tactic -> Tactic
7seq : List Tactic -> Tactic
8−seq [] = GoalType "This is an impossible case" Trivial
8+seq [] = GoalType "This is an impossible case" Trivial
9−seq [t] = t
9+seq [t] = t
10seq (t::ts) = t `Seq` seq ts
10seq (t::ts) = t `Seq` seq ts
11
11
12try : List Tactic -> Tactic
12try : List Tactic -> Tactic
13−try [] = GoalType "This is an impossible case" Trivial
13+try [] = GoalType "This is an impossible case" Trivial
14−try [t] = t
14+try [t] = t
15try (t::ts) = t `Try` seq ts
15try (t::ts) = t `Try` seq ts
16
16
17
17
@@ -27,43 +27,43 @@ mkPair a b = (a, b)
27--------------------------------------------------------
27--------------------------------------------------------
28
28
29getUName : TTName -> Maybe String
29getUName : TTName -> Maybe String
30−getUName (UN n) = Just n
30+getUName (UN n) = Just n
31getUName (NS n ns) = getUName n
31getUName (NS n ns) = getUName n
32−getUName _ = Nothing
32+getUName _ = Nothing
33
33
34unApply : TT -> (TT, List TT)
34unApply : TT -> (TT, List TT)
35unApply t = unA t []
35unApply t = unA t []
36 where unA : TT -> List TT -> (TT, List TT)
36 where unA : TT -> List TT -> (TT, List TT)
37 unA (App fn arg) args = unA fn (arg::args)
37 unA (App fn arg) args = unA fn (arg::args)
38− unA tm args = (tm, args)
38+ unA tm args = (tm, args)
39
39
40mkApp : TT -> List TT -> TT
40mkApp : TT -> List TT -> TT
41mkApp tm [] = tm
41mkApp tm [] = tm
42mkApp tm (a::as) = mkApp (App tm a) as
42mkApp tm (a::as) = mkApp (App tm a) as
43
43
44binderTy : (Eq t) => Binder t -> t
44binderTy : (Eq t) => Binder t -> t
45−binderTy (Lam t) = t
45+binderTy (Lam t) = t
46−binderTy (Pi t) = t
46+binderTy (Pi t) = t
47−binderTy (Let t1 t2) = t1
47+binderTy (Let t1 t2) = t1
48−binderTy (NLet t1 t2) = t1
48+binderTy (NLet t1 t2) = t1
49−binderTy (Hole t) = t
49+binderTy (Hole t) = t
50−binderTy (GHole t) = t
50+binderTy (GHole t) = t
51binderTy (Guess t1 t2) = t1
51binderTy (Guess t1 t2) = t1
52−binderTy (PVar t) = t
52+binderTy (PVar t) = t
53−binderTy (PVTy t) = t
53+binderTy (PVTy t) = t
54
54
55instance Show TTName where
55instance Show TTName where
56− show (UN str) = "(UN " ++ str ++ ")"
56+ show (UN str) = "(UN " ++ str ++ ")"
57− show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
57+ show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
58 show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
58 show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
59− show NErased = "NErased"
59+ show NErased = "NErased"
60
60
61instance Eq TTName where
61instance Eq TTName where
62− (UN str1) == (UN str2) = str1 == str2
62+ (UN str1) == (UN str2) = str1 == str2
63− (NS n ns) == (NS n' ns') = n == n' && ns == ns'
63+ (NS n ns) == (NS n' ns') = n == n' && ns == ns'
64− (MN i str) == (MN i' str') = i == i' && str == str'
64+ (MN i str) == (MN i' str') = i == i' && str == str'
65− NErased == NErased = True
65+ NErased == NErased = True
66− x == y = False
66+ x == y = False
67
67
68instance Show TTUExp where
68instance Show TTUExp where
69 show (UVar i) = "(UVar " ++ show i ++ ")"
69 show (UVar i) = "(UVar " ++ show i ++ ")"
@@ -72,7 +72,7 @@ instance Show TTUExp where
72instance Eq TTUExp where
72instance Eq TTUExp where
73 (UVar i) == (UVar j) = i == j
73 (UVar i) == (UVar j) = i == j
74 (UVal i) == (UVal j) = i == j
74 (UVal i) == (UVal j) = i == j
75− x == y = False
75+ x == y = False
76
76
77instance Show Const where
77instance Show Const where
78 show (I i) = "(I " ++ show i ++ ")"
78 show (I i) = "(I " ++ show i ++ ")"
@@ -173,13 +173,13 @@ instance Show TT where
173instance Eq TT where
173instance Eq TT where
174 a == b = equalp a b
174 a == b = equalp a b
175 where %assert_total equalp : TT -> TT -> Bool
175 where %assert_total equalp : TT -> TT -> Bool
176− equalp (P nt n t) (P nt' n' t') = nt == nt' && n == n' && t == t'
176+ equalp (P nt n t) (P nt' n' t') = nt == nt' && n == n' && t == t'
177− equalp (V i) (V i') = i == i'
177+ equalp (V i) (V i') = i == i'
178− equalp (Bind n b t) (Bind n' b' t') = n == n' && b == b' && t == t'
178+ equalp (Bind n b t) (Bind n' b' t') = n == n' && b == b' && t == t'
179− equalp (App t1 t2) (App t1' t2') = t1 == t1' && t2 == t2'
179+ equalp (App t1 t2) (App t1' t2') = t1 == t1' && t2 == t2'
180− equalp (TConst c) (TConst c') = c == c'
180+ equalp (TConst c) (TConst c') = c == c'
181− equalp (Proj tm i) (Proj tm' i') = tm == tm' && i == i'
181+ equalp (Proj tm i) (Proj tm' i') = tm == tm' && i == i'
182− equalp Erased Erased = True
182+ equalp Erased Erased = True
183− equalp Impossible Impossible = True
183+ equalp Impossible Impossible = True
184− equalp (TType u) (TType u') = u == u'
184+ equalp (TType u) (TType u') = u == u'
185− equalp x y = False
185+ equalp x y = False