git.iko.soy/Idris-dev
on 465cc1c help sign in
Idris-dev/libs/base/Language/Reflection/Utils.idr
286 lines 11 kB history raw
1module Language.Reflection.Utils
3import Language.Reflection
4import Language.Reflection.Errors
6--------------------------------------------------------
7-- Tactic construction conveniences
8--------------------------------------------------------
10total
11seq : List Tactic -> Tactic
12seq [] = GoalType "This is an impossible case" Trivial
13seq [t] = t
14seq (t::ts) = t `Seq` seq ts
16total
17try : List Tactic -> Tactic
18try [] = GoalType "This is an impossible case" Trivial
19try [t] = t
20try (t::ts) = t `Try` seq ts
23--------------------------------------------------------
24-- For use in tactic scripts
25--------------------------------------------------------
26total
27mkPair : a -> b -> (a, b)
28mkPair a b = (a, b)
31--------------------------------------------------------
32-- Tools for constructing proof terms directly
33--------------------------------------------------------
34total
35getUName : TTName -> Maybe String
36getUName (UN n) = Just n
37getUName (NS n ns) = getUName n
38getUName _ = Nothing
40total
41unApply : TT -> (TT, List TT)
42unApply t = unA t []
43 where unA : TT -> List TT -> (TT, List TT)
44 unA (App fn arg) args = unA fn (arg::args)
45 unA tm args = (tm, args)
47total
48mkApp : TT -> List TT -> TT
49mkApp tm [] = tm
50mkApp tm (a::as) = mkApp (App tm a) as
52total
53binderTy : (Eq t) => Binder t -> t
54binderTy (Lam t) = t
55binderTy (Pi t _) = t
56binderTy (Let t1 t2) = t1
57binderTy (NLet t1 t2) = t1
58binderTy (Hole t) = t
59binderTy (GHole t) = t
60binderTy (Guess t1 t2) = t1
61binderTy (PVar t) = t
62binderTy (PVTy t) = t
64instance Show TTName where
65 show (UN str) = "(UN " ++ str ++ ")"
66 show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"
67 show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"
68 show NErased = "NErased"
70instance Eq TTName where
71 (UN str1) == (UN str2) = str1 == str2
72 (NS n ns) == (NS n' ns') = n == n' && ns == ns'
73 (MN i str) == (MN i' str') = i == i' && str == str'
74 NErased == NErased = True
75 x == y = False
77instance Show TTUExp where
78 show (UVar i) = "(UVar " ++ show i ++ ")"
79 show (UVal i) = "(UVal " ++ show i ++ ")"
81instance Eq TTUExp where
82 (UVar i) == (UVar j) = i == j
83 (UVal i) == (UVal j) = i == j
84 x == y = False
86instance Show Const where
87 show (I i) = "(I " ++ show i ++ ")"
88 show (BI n) = "(BI " ++ show n ++ ")"
89 show (Fl f) = "(Fl " ++ show f ++ ")"
90 show (Ch c) = "(Ch " ++ show c ++ ")"
91 show (Str str) = "(Str " ++ show str ++ ")"
92 show (B8 b) = "(B8 ...)"
93 show (B16 b) = "(B16 ...)"
94 show (B32 b) = "(B32 ...)"
95 show (B64 b) = "(B64 ...)"
96 show (B8V xs) = "(B8V ...)"
97 show (B16V xs) = "(B16V ...)"
98 show (B32V xs) = "(B32V ...)"
99 show (B64V xs) = "(B64V ...)"
100 show (AType x) = "(AType ...)"
101 show StrType = "StrType"
102 show PtrType = "PtrType"
103 show ManagedPtrType = "ManagedPtrType"
104 show BufferType = "BufferType"
105 show VoidType = "VoidType"
106 show Forgot = "Forgot"
108instance Eq NativeTy where
109 IT8 == IT8 = True
110 IT16 == IT16 = True
111 IT32 == IT32 = True
112 IT64 == IT64 = True
113 _ == _ = False
115instance Eq Reflection.IntTy where
116 (ITFixed x) == (ITFixed y) = x == y
117 ITNative == ITNative = True
118 ITBig == ITBig = True
119 ITChar == ITChar = True
120 (ITVec x i) == (ITVec y j) = x == y && i == j
121 _ == _ = False
123instance Eq ArithTy where
124 (ATInt x) == (ATInt y) = x == y
125 ATFloat == ATFloat = True
126 _ == _ = False
128instance Eq Const where
129 (I x) == (I y) = x == y
130 (BI x) == (BI y) = x == y
131 (Fl x) == (Fl y) = x == y
132 (Ch x) == (Ch y) = x == y
133 (Str x) == (Str y) = x == y
134 (B8 x) == (B8 y) = x == y
135 (B16 x) == (B16 y) = x == y
136 (B32 x) == (B32 y) = x == y
137 (B64 x) == (B64 y) = x == y
138 (B8V xs) == (B8V ys) = False -- TODO
139 (B16V xs) == (B16V ys) = False -- TODO
140 (B32V xs) == (B32V ys) = False -- TODO
141 (B64V xs) == (B64V ys) = False -- TODO
142 (AType x) == (AType y) = x == y
143 StrType == StrType = True
144 PtrType == PtrType = True
145 ManagedPtrType == ManagedPtrType = True
146 BufferType == BufferType = True
147 VoidType == VoidType = True
148 Forgot == Forgot = True
149 _ == _ = False
152instance Show NameType where
153 show Bound = "Bound"
154 show Ref = "Ref"
155 show (DCon t ar) = "(DCon " ++ show t ++ " " ++ show ar ++ ")"
156 show (TCon t ar) = "(TCon " ++ show t ++ " " ++ show ar ++ ")"
158instance Eq NameType where
159 Bound == Bound = True
160 Ref == Ref = True
161 (DCon t ar) == (DCon t' ar') = t == t' && ar == ar'
162 (TCon t ar) == (TCon t' ar') = t == t' && ar == ar'
163 x == y = False
165instance (Show a) => Show (Binder a) where
166 show (Lam t) = "(Lam " ++ show t ++ ")"
167 show (Pi t _) = "(Pi " ++ show t ++ ")"
168 show (Let t1 t2) = "(Let " ++ show t1 ++ " " ++ show t2 ++ ")"
169 show (NLet t1 t2) = "(NLet " ++ show t1 ++ " " ++ show t2 ++ ")"
170 show (Hole t) = "(Hole " ++ show t ++ ")"
171 show (GHole t) = "(GHole " ++ show t ++ ")"
172 show (Guess t1 t2) = "(Guess " ++ show t1 ++ " " ++ show t2 ++ ")"
173 show (PVar t) = "(PVar " ++ show t ++ ")"
174 show (PVTy t) = "(PVTy " ++ show t ++ ")"
176instance (Eq a) => Eq (Binder a) where
177 (Lam t) == (Lam t') = t == t'
178 (Pi t k) == (Pi t' k') = t == t' && k == k'
179 (Let t1 t2) == (Let t1' t2') = t1 == t1' && t2 == t2'
180 (NLet t1 t2) == (NLet t1' t2') = t1 == t1' && t2 == t2'
181 (Hole t) == (Hole t') = t == t'
182 (GHole t) == (GHole t') = t == t'
183 (Guess t1 t2) == (Guess t1' t2') = t1 == t1' && t2 == t2'
184 (PVar t) == (PVar t') = t == t'
185 (PVTy t) == (PVTy t') = t == t'
186 x == y = False
188instance Show TT where
189 show = my_show
190 where %assert_total my_show : TT -> String
191 my_show (P nt n t) = "(P " ++ show nt ++ " " ++ show n ++ " " ++ show t ++ ")"
192 my_show (V i) = "(V " ++ show i ++ ")"
193 my_show (Bind n b t) = "(Bind " ++ show n ++ " " ++ show b ++ " " ++ show t ++ ")"
194 my_show (App t1 t2) = "(App " ++ show t1 ++ " " ++ show t2 ++ ")"
195 my_show (TConst c) = "(TConst " ++ show c ++ ")"
196 my_show (Proj tm i) = "(Proj " ++ show tm ++ " " ++ show i ++ ")"
197 my_show Erased = "Erased"
198 my_show Impossible = "Impossible"
199 my_show (TType u) = "(TType " ++ show u ++ ")"
201instance Eq TT where
202 a == b = equalp a b
203 where %assert_total equalp : TT -> TT -> Bool
204 equalp (P nt n t) (P nt' n' t') = nt == nt' && n == n' && t == t'
205 equalp (V i) (V i') = i == i'
206 equalp (Bind n b t) (Bind n' b' t') = n == n' && b == b' && t == t'
207 equalp (App t1 t2) (App t1' t2') = t1 == t1' && t2 == t2'
208 equalp (TConst c) (TConst c') = c == c'
209 equalp (Proj tm i) (Proj tm' i') = tm == tm' && i == i'
210 equalp Erased Erased = True
211 equalp Impossible Impossible = True
212 equalp (TType u) (TType u') = u == u'
213 equalp x y = False
215total
216forget : TT -> Maybe Raw
217forget tm = fe [] tm
218 where
219 atIndex : List a -> Int -> Maybe a
220 atIndex [] _ = Nothing
221 atIndex (x::xs) n =
222 case compare n 0 of
223 EQ => Just x
224 LT => Nothing
225 GT => atIndex xs (n-1)
227 %assert_total
228 fe : List TTName -> TT -> Maybe Raw
229 fe env (P _ n _) = Just $ Var n
230 fe env (V i) = map Var (atIndex env i)
231 fe env (Bind n b sc) = [| RBind (pure n) (traverse (fe env) b) (fe (n::env) sc) |]
232 fe env (App f a) = [| RApp (fe env f) (fe env a) |]
233 fe env (TConst c) = Just $ RConstant c
234 fe env (Proj tm i) = Nothing -- runtime only, not useful for metaprogramming
235 fe env (TType i) = Just RType
236 fe env Erased = Just $ RConstant Forgot
237 fe env Impossible = Nothing
239instance Show Raw where
240 show r = my_show r
241 where %assert_total my_show : Raw -> String
242 my_show (Var n) = "Var " ++ show n
243 my_show (RBind n b tm) = "RBind " ++ show n ++ " " ++ show b ++ " (" ++ my_show tm ++ ")"
244 my_show (RApp tm tm') = "RApp " ++ my_show tm ++ " " ++ my_show tm'
245 my_show RType = "RType"
246 my_show (RForce tm) = "RForce " ++ my_show tm
247 my_show (RConstant c) = "RConstant " ++ show c
249instance Show SourceLocation where
250 show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col
252instance Show Err where
253 show (Msg x) = "Msg \"" ++ x ++ "\""
254 show (InternalMsg x) = "InternalMsg \"" ++ x ++ "\""
255 show (CantUnify x tm tm' err xs y) = "CantUnify " ++ show x ++
256 " ( " ++ show tm ++ ") (" ++ show tm' ++ ") (" ++ show err ++ ") " ++
257 show xs ++ " " ++ show y
258 show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs
259 show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs
260 show (CantSolveGoal tm ctxt) = "CantSolveGoal " ++ show tm ++ " " ++ show ctxt
261 show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs
262 show (CantInferType x) = "CantInferType " ++ show x
263 show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'
264 show (NotEquality tm tm') = "NotEquality " ++ show tm ++ " " ++ show tm'
265 show (TooManyArguments n) = "TooManyArguments " ++ show n
266 show (CantIntroduce tm) = "CantIntroduce " ++ show tm
267 show (NoSuchVariable n) = "NoSuchVariable " ++ show n
268 show (WithFnType tm) = "WithFnType " ++ show tm
269 show (CantMatch tm) = "CantMatch " ++ show tm
270 show (NoTypeDecl n) = "NoTypeDecl " ++ show n
271 show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'
272 show (CantResolve tm) = "CantResolve " ++ show tm
273 show (InvalidTCArg n tm) = "InvalidTCName " ++ show n ++ " (" ++ show tm ++ ")"
274 show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs
275 show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm
276 show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm
277 show UniverseError = "UniverseError"
278 show ProgramLineComment = "ProgramLineComment"
279 show (Inaccessible n) = "Inaccessible " ++ show n
280 show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n
281 show (AlreadyDefined n) = "AlreadyDefined " ++ show n
282 show (ProofSearchFail err) = "ProofSearchFail " ++ show err
283 show (NoRewriting tm) = "NoRewriting " ++ show tm
284 show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""
285 show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"