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