@@ -5,13 +5,13 @@ module Language.Reflection.Utils
55--------------------------------------------------------
66
77seq : List Tactic -> Tactic
8−seq [] = GoalType "This is an impossible case" Trivial
9−seq [t] = t
8+seq [] = GoalType "This is an impossible case" Trivial
9+seq [t] = t
1010seq (t::ts) = t `Seq` seq ts
1111
1212try : List Tactic -> Tactic
13−try [] = GoalType "This is an impossible case" Trivial
14−try [t] = t
13+try [] = GoalType "This is an impossible case" Trivial
14+try [t] = t
1515try (t::ts) = t `Try` seq ts
1616
1717
@@ -27,43 +27,43 @@ mkPair a b = (a, b)
2727--------------------------------------------------------
2828
2929getUName : TTName -> Maybe String
30−getUName (UN n) = Just n
30+getUName (UN n) = Just n
3131getUName (NS n ns) = getUName n
32−getUName _ = Nothing
32+getUName _ = Nothing
3333
3434unApply : TT -> (TT, List TT)
3535unApply t = unA t []
3636 where unA : TT -> List TT -> (TT, List TT)
3737 unA (App fn arg) args = unA fn (arg::args)
38− unA tm args = (tm, args)
38+ unA tm args = (tm, args)
3939
4040mkApp : TT -> List TT -> TT
4141mkApp tm [] = tm
4242mkApp tm (a::as) = mkApp (App tm a) as
4343
4444binderTy : (Eq t) => Binder t -> t
45−binderTy (Lam t) = t
46−binderTy (Pi t) = t
47−binderTy (Let t1 t2) = t1
48−binderTy (NLet t1 t2) = t1
49−binderTy (Hole t) = t
50−binderTy (GHole t) = t
45+binderTy (Lam t) = t
46+binderTy (Pi t) = t
47+binderTy (Let t1 t2) = t1
48+binderTy (NLet t1 t2) = t1
49+binderTy (Hole t) = t
50+binderTy (GHole t) = t
5151binderTy (Guess t1 t2) = t1
52−binderTy (PVar t) = t
53−binderTy (PVTy t) = t
52+binderTy (PVar t) = t
53+binderTy (PVTy t) = t
5454
5555instance Show TTName where
56− show (UN str) = "(UN " ++ str ++ ")"
57− show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
56+ show (UN str) = "(UN " ++ str ++ ")"
57+ show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
5858 show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
59− show NErased = "NErased"
59+ show NErased = "NErased"
6060
6161instance Eq TTName where
62− (UN str1) == (UN str2) = str1 == str2
63− (NS n ns) == (NS n' ns') = n == n' && ns == ns'
64− (MN i str) == (MN i' str') = i == i' && str == str'
65− NErased == NErased = True
66− x == y = False
62+ (UN str1) == (UN str2) = str1 == str2
63+ (NS n ns) == (NS n' ns') = n == n' && ns == ns'
64+ (MN i str) == (MN i' str') = i == i' && str == str'
65+ NErased == NErased = True
66+ x == y = False
6767
6868instance Show TTUExp where
6969 show (UVar i) = "(UVar " ++ show i ++ ")"
@@ -72,7 +72,7 @@ instance Show TTUExp where
7272instance Eq TTUExp where
7373 (UVar i) == (UVar j) = i == j
7474 (UVal i) == (UVal j) = i == j
75− x == y = False
75+ x == y = False
7676
7777instance Show Const where
7878 show (I i) = "(I " ++ show i ++ ")"
@@ -173,13 +173,13 @@ instance Show TT where
173173instance Eq TT where
174174 a == b = equalp a b
175175 where %assert_total equalp : TT -> TT -> Bool
176− equalp (P nt n t) (P nt' n' t') = nt == nt' && n == n' && t == t'
177− equalp (V i) (V i') = i == i'
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'
180− equalp (TConst c) (TConst c') = c == c'
181− equalp (Proj tm i) (Proj tm' i') = tm == tm' && i == i'
182− equalp Erased Erased = True
183− equalp Impossible Impossible = True
184− equalp (TType u) (TType u') = u == u'
185− equalp x y = False
176+ equalp (P nt n t) (P nt' n' t') = nt == nt' && n == n' && t == t'
177+ equalp (V i) (V i') = i == i'
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'
180+ equalp (TConst c) (TConst c') = c == c'
181+ equalp (Proj tm i) (Proj tm' i') = tm == tm' && i == i'
182+ equalp Erased Erased = True
183+ equalp Impossible Impossible = True
184+ equalp (TType u) (TType u') = u == u'
185+ equalp x y = False