git.iko.soy/Idris-dev
on d3fa352 help sign in
Idris-dev/libs/base/Language/Reflection/Utils.idr
389 lines 16 kB history raw
1module Language.Reflection.Utils
3import Language.Reflection
4import Language.Reflection.Elab
5import Language.Reflection.Errors
7%access public export
9--------------------------------------------------------
10-- Tactic construction conveniences
11--------------------------------------------------------
13total
14seq : List Tactic -> Tactic
15seq [] = GoalType "This is an impossible case" Trivial
16seq [t] = t
17seq (t::ts) = t `Seq` seq ts
19total
20try : List Tactic -> Tactic
21try [] = GoalType "This is an impossible case" Trivial
22try [t] = t
23try (t::ts) = t `Try` seq ts
26--------------------------------------------------------
27-- For use in tactic scripts
28--------------------------------------------------------
29total
30mkPair : a -> b -> (a, b)
31mkPair a b = (a, b)
34--------------------------------------------------------
35-- Tools for constructing proof terms directly
36--------------------------------------------------------
37total
38getUName : TTName -> Maybe String
39getUName (UN n) = Just n
40getUName (NS n ns) = getUName n
41getUName _ = Nothing
43namespace TT
44 total
45 unApply : TT -> (TT, List TT)
46 unApply t = unA t []
47 where unA : TT -> List TT -> (TT, List TT)
48 unA (App fn arg) args = unA fn (arg::args)
49 unA tm args = (tm, args)
51 total
52 mkApp : Foldable f => TT -> f TT -> TT
53 mkApp f args = foldl App f args
55namespace Raw
56 total
57 unApply : Raw -> (Raw, List Raw)
58 unApply tm = unApply' tm []
59 where unApply' : Raw -> List Raw -> (Raw, List Raw)
60 unApply' (RApp f x) xs = unApply' f (x::xs)
61 unApply' notApp xs = (notApp, xs)
63 total
64 mkApp : Foldable f => Raw -> f Raw -> Raw
65 mkApp f args = foldl RApp f args
68total
69binderTy : Binder t -> t
70binderTy (Lam t) = t
71binderTy (Pi t _) = t
72binderTy (Let t1 t2) = t1
73binderTy (Hole t) = t
74binderTy (GHole t) = t
75binderTy (Guess t1 t2) = t1
76binderTy (PVar t) = t
77binderTy (PVTy t) = t
79implementation Show SourceLocation where
80 showPrec d (FileLoc filename line col) = showCon d "FileLoc" $ showArg filename ++ showArg line ++ showArg col
82implementation Eq SourceLocation where
83 (FileLoc fn s e) == (FileLoc fn' s' e') = fn == fn' && s == s' && e == e'
85mutual
86 implementation Show SpecialName where
87 showPrec d (WhereN i n1 n2) = showCon d "WhereN" $ showArg i ++
88 showArg n1 ++ showArg n2
89 showPrec d (WithN i n) = showCon d "WithN" $ showArg i ++ showArg n
90 showPrec d (ImplementationN i ss) = showCon d "ImplementationN" $ showArg i ++ showArg ss
91 showPrec d (ParentN n s) = showCon d "ParentN" $ showArg n ++ showArg s
92 showPrec d (MethodN n) = showCon d "MethodN" $ showArg n
93 showPrec d (CaseN fc n) = showCon d "CaseN" $ showArg fc ++ showArg n
94 showPrec d (ElimN n) = showCon d "ElimN" $ showArg n
95 showPrec d (ImplementationCtorN n) = showCon d "ImplementationCtorN" $ showArg n
96 showPrec d (MetaN parent meta) = showCon d "MetaN" $ showArg parent ++ showArg meta
98 implementation Show TTName where
99 showPrec d (UN str) = showCon d "UN" $ showArg str
100 showPrec d (NS n ns) = showCon d "NS" $ showArg n ++ showArg ns
101 showPrec d (MN i str) = showCon d "MN" $ showArg i ++ showArg str
102 showPrec d (SN sn) = showCon d "SN" $ assert_total (showArg sn)
104mutual
105 implementation Eq TTName where
106 (UN str1) == (UN str2) = str1 == str2
107 (NS n ns) == (NS n' ns') = n == n' && ns == ns'
108 (MN i str) == (MN i' str') = i == i' && str == str'
109 (SN sn) == (SN sn') = assert_total $ sn == sn'
110 x == y = False
112 implementation Eq SpecialName where
113 (WhereN i n1 n2) == (WhereN i' n1' n2') = i == i' && n1 == n1' && n2 == n2'
114 (WithN i n) == (WithN i' n') = i == i' && n == n'
115 (ImplementationN i ss) == (ImplementationN i' ss') = i == i' && ss == ss'
116 (ParentN n s) == (ParentN n' s') = n == n' && s == s'
117 (MethodN n) == (MethodN n') = n == n'
118 (CaseN fc n) == (CaseN fc' n') = fc == fc' && n == n'
119 (ElimN n) == (ElimN n') = n == n'
120 (ImplementationCtorN n) == (ImplementationCtorN n') = n == n'
121 (MetaN parent meta) == (MetaN parent' meta') = parent == parent' && meta == meta'
122 _ == _ = False
124implementation Show TTUExp where
125 showPrec d (UVar ns i) = showCon d "UVar" $ showArg ns ++ showArg i
126 showPrec d (UVal i) = showCon d "UVal" $ showArg i
128implementation Eq TTUExp where
129 (UVar nsi i) == (UVar nsj j) = nsi == nsj && i == j
130 (UVal i) == (UVal j) = i == j
131 x == y = False
133implementation Show NativeTy where
134 show IT8 = "IT8"
135 show IT16 = "IT16"
136 show IT32 = "IT32"
137 show IT64 = "IT64"
139implementation Show IntTy where
140 showPrec d (ITFixed t) = showCon d "ITFixed" $ showArg t
141 showPrec d ITNative = "ITNative"
142 showPrec d ITBig = "ITBig"
143 showPrec d ITChar = "ITChar"
145implementation Show ArithTy where
146 showPrec d (ATInt t) = showCon d "ATInt" $ showArg t
147 showPrec d ATDouble = "ATDouble"
149implementation Show Const where
150 showPrec d (I i) = showCon d "I" $ showArg i
151 showPrec d (BI n) = showCon d "BI" $ showArg n
152 showPrec d (Fl f) = showCon d "Fl" $ showArg f
153 showPrec d (Ch c) = showCon d "Ch" $ showArg c
154 showPrec d (Str str) = showCon d "Str" $ showArg str
155 showPrec d (B8 b) = showCon d "B8" $ showArg b
156 showPrec d (B16 b) = showCon d "B16" $ showArg b
157 showPrec d (B32 b) = showCon d "B32" $ showArg b
158 showPrec d (B64 b) = showCon d "B64" $ showArg b
159 showPrec d (AType x) = showCon d "AType" $ showArg x
160 showPrec d StrType = "StrType"
161 showPrec d VoidType = "VoidType"
162 showPrec d Forgot = "Forgot"
163 showPrec d WorldType = "WorldType"
164 showPrec d TheWorld = "TheWorld"
166implementation Eq NativeTy where
167 IT8 == IT8 = True
168 IT16 == IT16 = True
169 IT32 == IT32 = True
170 IT64 == IT64 = True
171 _ == _ = False
173implementation Eq Reflection.IntTy where
174 (ITFixed x) == (ITFixed y) = x == y
175 ITNative == ITNative = True
176 ITBig == ITBig = True
177 ITChar == ITChar = True
178 _ == _ = False
180implementation Eq ArithTy where
181 (ATInt x) == (ATInt y) = x == y
182 ATDouble == ATDouble = True
183 _ == _ = False
185implementation Eq Const where
186 (I x) == (I y) = x == y
187 (BI x) == (BI y) = x == y
188 (Fl x) == (Fl y) = x == y
189 (Ch x) == (Ch y) = x == y
190 (Str x) == (Str y) = x == y
191 (B8 x) == (B8 y) = x == y
192 (B16 x) == (B16 y) = x == y
193 (B32 x) == (B32 y) = x == y
194 (B64 x) == (B64 y) = x == y
195 (AType x) == (AType y) = x == y
196 StrType == StrType = True
197 VoidType == VoidType = True
198 Forgot == Forgot = True
199 _ == _ = False
202implementation Show NameType where
203 showPrec d Bound = "Bound"
204 showPrec d Ref = "Ref"
205 showPrec d (DCon t ar) = showCon d "DCon" $ showArg t ++ showArg ar
206 showPrec d (TCon t ar) = showCon d "TCon" $ showArg t ++ showArg ar
208implementation Eq NameType where
209 Bound == Bound = True
210 Ref == Ref = True
211 (DCon t ar) == (DCon t' ar') = t == t' && ar == ar'
212 (TCon t ar) == (TCon t' ar') = t == t' && ar == ar'
213 x == y = False
215implementation (Show a) => Show (Binder a) where
216 showPrec d (Lam t) = showCon d "Lam" $ showArg t
217 showPrec d (Pi t1 t2) = showCon d "Pi" $ showArg t1 ++ showArg t2
218 showPrec d (Let t1 t2) = showCon d "Let" $ showArg t1 ++ showArg t2
219 showPrec d (Hole t) = showCon d "Hole" $ showArg t
220 showPrec d (GHole t) = showCon d "GHole" $ showArg t
221 showPrec d (Guess t1 t2) = showCon d "Guess" $ showArg t1 ++ showArg t2
222 showPrec d (PVar t) = showCon d "PVar" $ showArg t
223 showPrec d (PVTy t) = showCon d "PVTy" $ showArg t
225implementation (Eq a) => Eq (Binder a) where
226 (Lam t) == (Lam t') = t == t'
227 (Pi t k) == (Pi t' k') = t == t' && k == k'
228 (Let t1 t2) == (Let t1' t2') = t1 == t1' && t2 == t2'
229 (Hole t) == (Hole t') = t == t'
230 (GHole t) == (GHole t') = t == t'
231 (Guess t1 t2) == (Guess t1' t2') = t1 == t1' && t2 == t2'
232 (PVar t) == (PVar t') = t == t'
233 (PVTy t) == (PVTy t') = t == t'
234 x == y = False
236implementation Show TT where
237 showPrec = my_show
238 where my_show : Prec -> TT -> String
239 my_show d (P nt n t) = assert_total $ showCon d "P" $ showArg nt ++ showArg n ++ showArg t
240 my_show d (V i) = assert_total $ showCon d "V" $ showArg i
241 my_show d (Bind n b t) = assert_total $ showCon d "Bind" $ showArg n ++ showArg b ++ showArg t
242 my_show d (App t1 t2) = assert_total $ showCon d "App" $ showArg t1 ++ showArg t2
243 my_show d (TConst c) = assert_total $ showCon d "TConst" $ showArg c
244 my_show d Erased = "Erased"
245 my_show d (TType u) = assert_total $ showCon d "TType" $ showArg u
246 my_show d (UType u) = "UType"
248implementation Eq Universe where
249 Reflection.NullType == Reflection.NullType = True
250 Reflection.UniqueType == Reflection.UniqueType = True
251 Reflection.AllTypes == Reflection.AllTypes = True
252 _ == _ = False
254implementation Eq TT where
255 a == b = equalp a b
256 where equalp : TT -> TT -> Bool
257 equalp (P nt n t) (P nt' n' t') = assert_total $ nt == nt' && n == n' && t == t'
258 equalp (V i) (V i') = assert_total $ i == i'
259 equalp (Bind n b t) (Bind n' b' t') = assert_total $ n == n' && b == b' && t == t'
260 equalp (App t1 t2) (App t1' t2') = assert_total $ t1 == t1' && t2 == t2'
261 equalp (TConst c) (TConst c') = c == c'
262 equalp Erased Erased = True
263 equalp (TType u) (TType u') = u == u'
264 equalp (UType u) (UType u') = u == u'
265 equalp x y = False
267implementation Eq Raw where
268 a == b = equalp a b
269 where equalp : Raw -> Raw -> Bool
270 equalp (Var x) (Var y) = assert_total $ x == y
271 equalp (RBind x b1 e1) (RBind y b2 e2) = assert_total $ x == y && b1 == b2 && e1 == e2
272 equalp (RApp f1 a1) (RApp f2 a2) = assert_total $ f1 == f2 && a1 == a2
273 equalp RType RType = True
274 equalp (RUType u1) (RUType u2) = u1 == u2
275 equalp (RConstant c1) (RConstant c2) = c1 == c2
276 equalp _ _ = False
279total
280forget : TT -> Maybe Raw
281forget tm = fe [] tm
282 where
283 atIndex : List a -> Int -> Maybe a
284 atIndex [] _ = Nothing
285 atIndex (x::xs) n =
286 case compare n 0 of
287 EQ => Just x
288 LT => Nothing
289 GT => atIndex xs (n-1)
291 fe : List TTName -> TT -> Maybe Raw
292 fe env (P _ n _) = Just $ Var n
293 fe env (V i) = [| Var (atIndex env i) |]
294 fe env (Bind n b sc) = [| RBind (pure n)
295 (assert_total $ traverse (fe env) b)
296 (fe (n::env) sc) |]
297 fe env (App f a) = [| RApp (fe env f) (fe env a) |]
298 fe env (TConst c) = Just $ RConstant c
299 fe env (TType i) = Just RType
300 fe env (UType uni) = Just (RUType uni)
301 fe env Erased = Just $ RConstant Forgot
303implementation Show Raw where
304 showPrec = my_show
305 where my_show : Prec -> Raw -> String
306 my_show d (Var n) = assert_total $ showCon d "Var" $ showArg n
307 my_show d (RBind n b tm) = assert_total $ showCon d "RBind" $ showArg n ++ showArg b ++ " " ++ my_show App tm
308 my_show d (RApp tm tm') = assert_total $ showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'
309 my_show d RType = "RType"
310 my_show d (RConstant c) = assert_total $ showCon d "RConstant" $ showArg c
311 my_show d (RUType u) = "RUType"
314implementation Show Err where
315 showPrec d (Msg x) = showCon d "Msg" $ showArg x
316 showPrec d (InternalMsg x) = showCon d "InternalMsg" $ showArg x
317 showPrec d (CantUnify x tm tm' err xs y) = showCon d "CantUnify" $ showArg x ++
318 showArg tm ++ showArg tm' ++ showArg err ++
319 showArg xs ++ showArg y
320 showPrec d (InfiniteUnify n tm xs) = showCon d "InfiniteUnify" $ showArg n ++ showArg tm ++ showArg xs
321 showPrec d (CantConvert tm tm' xs) = showCon d "CantConvert" $ showArg tm ++ showArg tm' ++ showArg xs
322 showPrec d (CantSolveGoal tm ctxt) = showCon d "CantSolveGoal" $ showArg tm ++ showArg ctxt
323 showPrec d (UnifyScope n n' tm xs) = showCon d "UnifyScope" $ showArg n ++ showArg n' ++ showArg tm ++ showArg xs
324 showPrec d (CantInferType x) = showCon d "CantInferType" $ showArg x
325 showPrec d (NonFunctionType tm tm') = showCon d "NonFunctionType" $ showArg tm ++ showArg tm'
326 showPrec d (NotEquality tm tm') = showCon d "NotEquality" $ showArg tm ++ showArg tm'
327 showPrec d (TooManyArguments n) = showCon d "TooManyArguments" $ showArg n
328 showPrec d (CantIntroduce tm) = showCon d "CantIntroduce" $ showArg tm
329 showPrec d (NoSuchVariable n) = showCon d "NoSuchVariable" $ showArg n
330 showPrec d (WithFnType tm) = showCon d "WithFnType" $ showArg tm
331 showPrec d (CantMatch tm) = showCon d "CantMatch" $ showArg tm
332 showPrec d (NoTypeDecl n) = showCon d "NoTypeDecl" $ showArg n
333 showPrec d (NotInjective tm tm' x) = showCon d "NotInjective" $ showArg tm ++ showArg tm'
334 showPrec d (CantResolve tm e) = showCon d "CantResolve" $ showArg tm ++ showArg e
335 showPrec d (InvalidTCArg n tm) = showCon d "InvalidTCName" $ showArg n ++ showArg tm
336 showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs
337 showPrec d (NoValidAlts xs) = showCon d "NoValidAlts" $ showArg xs
338 showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm
339 showPrec d (NoEliminator s tm) = showCon d "NoEliminator" $ showArg s ++ showArg tm
340 showPrec d UniverseError = "UniverseError"
341 showPrec d ProgramLineComment = "ProgramLineComment"
342 showPrec d (Inaccessible n) = showCon d "Inaccessible" $ showArg n
343 showPrec d (UnknownImplicit n f) = showCon d "UnknownImplicit" $ showArg n ++ showArg f
344 showPrec d (NonCollapsiblePostulate n) = showCon d "NonCollapsiblePostulate" $ showArg n
345 showPrec d (AlreadyDefined n) = showCon d "AlreadyDefined" $ showArg n
346 showPrec d (ProofSearchFail err) = showCon d "ProofSearchFail" $ showArg err
347 showPrec d (NoRewriting ltm rtm typ) = showCon d "NoRewriting" $ showArg ltm ++ showArg rtm ++ showArg typ
348 showPrec d (ProviderError x) = showCon d "ProviderError" $ showArg x
349 showPrec d (LoadingFailed x err) = showCon d "LoadingFailed" $ showArg x ++ showArg err
351-------------------------
352-- Idiom brackets for Raw
353-------------------------
355(<*>) : Raw -> Raw -> Raw
356(<*>) = RApp
358pure : Raw -> Raw
359pure = id
361--------------------------------------
362-- Implementations for definition reflection
363--------------------------------------
364implementation Show Erasure where
365 show Erased = "Erased"
366 show NotErased = "NotErased"
368implementation Show Plicity where
369 show Explicit = "Explicit"
370 show Implicit = "Implicit"
371 show Constraint = "Constraint"
373implementation Show FunArg where
374 showPrec d (MkFunArg n ty plic era) = showCon d "MkFunArg" $ showArg n ++
375 showArg ty ++ showArg plic ++ showArg era
377implementation Show CtorArg where
378 showPrec d (CtorParameter fa) = showCon d "CtorParameter" $ showArg fa
379 showPrec d (CtorField fa) = showCon d "CtorField" $ showArg fa
381implementation Show TyDecl where
382 showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn ++
383 showArg args ++ showArg ret
385implementation Show tm => Show (FunClause tm) where
386 showPrec d (MkFunClause lhs rhs) =
387 showCon d "MkFunClause" $ showArg lhs ++ showArg rhs
388 showPrec d (MkImpossibleClause lhs) =
389 showCon d "MkImpossibleClause" $ showArg lhs