@@ -0,0 +1,185 @@
1+module Language.Reflection.Utils
2+
3+--------------------------------------------------------
4+-- Tactic construction conveniences
5+--------------------------------------------------------
6+
7+seq : List Tactic -> Tactic
8+seq [] = GoalType "This is an impossible case" Trivial
9+seq [t] = t
10+seq (t::ts) = t `Seq` seq ts
11+
12+try : List Tactic -> Tactic
13+try [] = GoalType "This is an impossible case" Trivial
14+try [t] = t
15+try (t::ts) = t `Try` seq ts
16+
17+
18+--------------------------------------------------------
19+-- For use in tactic scripts
20+--------------------------------------------------------
21+mkPair : a -> b -> (a, b)
22+mkPair a b = (a, b)
23+
24+
25+--------------------------------------------------------
26+-- Tools for constructing proof terms directly
27+--------------------------------------------------------
28+
29+getUName : TTName -> Maybe String
30+getUName (UN n) = Just n
31+getUName (NS n ns) = getUName n
32+getUName _ = Nothing
33+
34+unApply : TT -> (TT, List TT)
35+unApply t = unA t []
36+ where unA : TT -> List TT -> (TT, List TT)
37+ unA (App fn arg) args = unA fn (arg::args)
38+ unA tm args = (tm, args)
39+
40+mkApp : TT -> List TT -> TT
41+mkApp tm [] = tm
42+mkApp tm (a::as) = mkApp (App tm a) as
43+
44+binderTy : (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
51+binderTy (Guess t1 t2) = t1
52+binderTy (PVar t) = t
53+binderTy (PVTy t) = t
54+
55+instance Show TTName where
56+ show (UN str) = "(UN " ++ str ++ ")"
57+ show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
58+ show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
59+ show NErased = "NErased"
60+
61+instance 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
67+
68+instance Show TTUExp where
69+ show (UVar i) = "(UVar " ++ show i ++ ")"
70+ show (UVal i) = "(UVal " ++ show i ++ ")"
71+
72+instance Eq TTUExp where
73+ (UVar i) == (UVar j) = i == j
74+ (UVal i) == (UVal j) = i == j
75+ x == y = False
76+
77+instance Show Const where
78+ show (I i) = "(I " ++ show i ++ ")"
79+ show (BI n) = "(BI " ++ show n ++ ")"
80+ show (Fl f) = "(Fl " ++ show f ++ ")"
81+ show (Ch c) = "(Ch " ++ show c ++ ")"
82+ show (Str str) = "(Str " ++ show str ++ ")"
83+ show IType = "IType"
84+ show BIType = "BIType"
85+ show FlType = "FlType"
86+ show ChType = "ChType"
87+ show StrType = "StrType"
88+ show (B8 b) = "(B8 ...)"
89+ show (B16 b) = "(B16 ...)"
90+ show (B32 b) = "(B32 ...)"
91+ show (B64 b) = "(B64 ...)"
92+ show B8Type = "B8Type"
93+ show B16Type = "B16Type"
94+ show B32Type = "B32Type"
95+ show B64Type = "B64Type"
96+ show PtrType = "PtrType"
97+ show VoidType = "VoidType"
98+ show Forgot = "Forgot"
99+
100+instance Eq Const where
101+ (I i) == (I i') = i == i'
102+ (BI n) == (BI n') = n == n'
103+ (Fl f) == (Fl f') = f == f'
104+ (Ch c) == (Ch c') = c == c'
105+ (Str str) == (Str str') = str == str'
106+ IType == IType = True
107+ BIType == BIType = True
108+ FlType == FlType = True
109+ ChType == ChType = True
110+ StrType == StrType = True
111+ (B8 b) == (B8 b') = False -- FIXME: b == b'
112+ (B16 b) == (B16 b') = False -- FIXME: b == b'
113+ (B32 b) == (B32 b') = False -- FIXME: b == b'
114+ (B64 b) == (B64 b') = False -- FIXME: b == b'
115+ B8Type == B8Type = True
116+ B16Type == B16Type = True
117+ B32Type == B32Type = True
118+ B64Type == B64Type = True
119+ PtrType == PtrType = True
120+ VoidType == VoidType = True
121+ Forgot == Forgot = True
122+ x == y = False
123+
124+instance Show NameType where
125+ show Bound = "Bound"
126+ show Ref = "Ref"
127+ show (DCon t ar) = "(DCon " ++ show t ++ " " ++ show ar ++ ")"
128+ show (TCon t ar) = "(TCon " ++ show t ++ " " ++ show ar ++ ")"
129+
130+instance Eq NameType where
131+ Bound == Bound = True
132+ Ref == Ref = True
133+ (DCon t ar) == (DCon t' ar') = t == t' && ar == ar'
134+ (TCon t ar) == (TCon t' ar') = t == t' && ar == ar'
135+ x == y = False
136+
137+instance (Show a) => Show (Binder a) where
138+ show (Lam t) = "(Lam " ++ show t ++ ")"
139+ show (Pi t) = "(Pi " ++ show t ++ ")"
140+ show (Let t1 t2) = "(Let " ++ show t1 ++ " " ++ show t2 ++ ")"
141+ show (NLet t1 t2) = "(NLet " ++ show t1 ++ " " ++ show t2 ++ ")"
142+ show (Hole t) = "(Hole " ++ show t ++ ")"
143+ show (GHole t) = "(GHole " ++ show t ++ ")"
144+ show (Guess t1 t2) = "(Guess " ++ show t1 ++ " " ++ show t2 ++ ")"
145+ show (PVar t) = "(PVar " ++ show t ++ ")"
146+ show (PVTy t) = "(PVTy " ++ show t ++ ")"
147+
148+instance (Eq a) => Eq (Binder a) where
149+ (Lam t) == (Lam t') = t == t'
150+ (Pi t) == (Pi t') = t == t'
151+ (Let t1 t2) == (Let t1' t2') = t1 == t1' && t2 == t2'
152+ (NLet t1 t2) == (NLet t1' t2') = t1 == t1' && t2 == t2'
153+ (Hole t) == (Hole t') = t == t'
154+ (GHole t) == (GHole t') = t == t'
155+ (Guess t1 t2) == (Guess t1' t2') = t1 == t1' && t2 == t2'
156+ (PVar t) == (PVar t') = t == t'
157+ (PVTy t) == (PVTy t') = t == t'
158+ x == y = False
159+
160+instance Show TT where
161+ show = my_show
162+ where %assert_total my_show : TT -> String
163+ my_show (P nt n t) = "(P " ++ show nt ++ " " ++ show n ++ " " ++ show t ++ ")"
164+ my_show (V i) = "(V " ++ show i ++ ")"
165+ my_show (Bind n b t) = "(Bind " ++ show n ++ " " ++ show b ++ " " ++ show t ++ ")"
166+ my_show (App t1 t2) = "(App " ++ show t1 ++ " " ++ show t2 ++ ")"
167+ my_show (TConst c) = "(TConst " ++ show c ++ ")"
168+ my_show (Proj tm i) = "(Proj " ++ show tm ++ " " ++ show i ++ ")"
169+ my_show Erased = "Erased"
170+ my_show Impossible = "Impossible"
171+ my_show (TType u) = "(TType " ++ show u ++ ")"
172+
173+instance Eq TT where
174+ a == b = equalp a b
175+ 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