git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/libs/base/Language/Reflection/Utils.idr
343 lines 14 kB history raw
1module Language.Reflection.Utils
3import Language.Reflection
4import Language.Reflection.Elab
5import Language.Reflection.Errors
7--------------------------------------------------------
8-- Tactic construction conveniences
9--------------------------------------------------------
11total
12seq : List Tactic -> Tactic
13seq [] = GoalType "This is an impossible case" Trivial
14seq [t] = t
15seq (t::ts) = t `Seq` seq ts
17total
18try : List Tactic -> Tactic
19try [] = GoalType "This is an impossible case" Trivial
20try [t] = t
21try (t::ts) = t `Try` seq ts
24--------------------------------------------------------
25-- For use in tactic scripts
26--------------------------------------------------------
27total
28mkPair : a -> b -> (a, b)
29mkPair a b = (a, b)
32--------------------------------------------------------
33-- Tools for constructing proof terms directly
34--------------------------------------------------------
35total
36getUName : TTName -> Maybe String
37getUName (UN n) = Just n
38getUName (NS n ns) = getUName n
39getUName _ = Nothing
41total
42unApply : TT -> (TT, List TT)
43unApply t = unA t []
44 where unA : TT -> List TT -> (TT, List TT)
45 unA (App fn arg) args = unA fn (arg::args)
46 unA tm args = (tm, args)
48total
49mkApp : TT -> List TT -> TT
50mkApp tm [] = tm
51mkApp tm (a::as) = mkApp (App tm a) as
53total
54binderTy : Binder t -> t
55binderTy (Lam t) = t
56binderTy (Pi t _) = t
57binderTy (Let t1 t2) = t1
58binderTy (NLet t1 t2) = t1
59binderTy (Hole t) = t
60binderTy (GHole t) = t
61binderTy (Guess t1 t2) = t1
62binderTy (PVar t) = t
63binderTy (PVTy t) = t
65mutual
66 instance Show SpecialName where
67 showPrec d (WhereN i n1 n2) = showCon d "WhereN" $ showArg i ++
68 showArg n1 ++ showArg n2
69 showPrec d (WithN i n) = showCon d "WithN" $ showArg i ++ showArg n
70 showPrec d (InstanceN i ss) = showCon d "InstanceN" $ showArg i ++ showArg ss
71 showPrec d (ParentN n s) = showCon d "ParentN" $ showArg n ++ showArg s
72 showPrec d (MethodN n) = showCon d "MethodN" $ showArg n
73 showPrec d (CaseN n) = showCon d "CaseN" $ showArg n
74 showPrec d (ElimN n) = showCon d "ElimN" $ showArg n
75 showPrec d (InstanceCtorN n) = showCon d "InstanceCtorN" $ showArg n
76 showPrec d (MetaN parent meta) = showCon d "MetaN" $ showArg parent ++ showArg meta
78 instance Show TTName where
79 showPrec d (UN str) = showCon d "UN" $ showArg str
80 showPrec d (NS n ns) = showCon d "NS" $ showArg n ++ showArg ns
81 showPrec d (MN i str) = showCon d "MN" $ showArg i ++ showArg str
82 showPrec d (SN sn) = showCon d "SN" $ assert_total (showArg sn)
83 showPrec d NErased = "NErased"
85mutual
86 instance Eq TTName where
87 (UN str1) == (UN str2) = str1 == str2
88 (NS n ns) == (NS n' ns') = n == n' && ns == ns'
89 (MN i str) == (MN i' str') = i == i' && str == str'
90 NErased == NErased = True
91 (SN sn) == (SN sn') = assert_total $ sn == sn'
92 x == y = False
94 instance Eq SpecialName where
95 (WhereN i n1 n2) == (WhereN i' n1' n2') = i == i' && n1 == n1' && n2 == n2'
96 (WithN i n) == (WithN i' n') = i == i' && n == n'
97 (InstanceN i ss) == (InstanceN i' ss') = i == i' && ss == ss'
98 (ParentN n s) == (ParentN n' s') = n == n' && s == s'
99 (MethodN n) == (MethodN n') = n == n'
100 (CaseN n) == (CaseN n') = n == n'
101 (ElimN n) == (ElimN n') = n == n'
102 (InstanceCtorN n) == (InstanceCtorN n') = n == n'
103 (MetaN parent meta) == (MetaN parent' meta') = parent == parent' && meta == meta'
104 _ == _ = False
106instance Show TTUExp where
107 showPrec d (UVar i) = showCon d "UVar" $ showArg i
108 showPrec d (UVal i) = showCon d "UVal" $ showArg i
110instance Eq TTUExp where
111 (UVar i) == (UVar j) = i == j
112 (UVal i) == (UVal j) = i == j
113 x == y = False
115instance Show NativeTy where
116 show IT8 = "IT8"
117 show IT16 = "IT16"
118 show IT32 = "IT32"
119 show IT64 = "IT64"
121instance Show IntTy where
122 showPrec d (ITFixed t) = showCon d "ITFixed" $ showArg t
123 showPrec d ITNative = "ITNative"
124 showPrec d ITBig = "ITBig"
125 showPrec d ITChar = "ITChar"
127instance Show ArithTy where
128 showPrec d (ATInt t) = showCon d "ATInt" $ showArg t
129 showPrec d ATFloat = "ATFloat"
131instance Show Const where
132 showPrec d (I i) = showCon d "I" $ showArg i
133 showPrec d (BI n) = showCon d "BI" $ showArg n
134 showPrec d (Fl f) = showCon d "Fl" $ showArg f
135 showPrec d (Ch c) = showCon d "Ch" $ showArg c
136 showPrec d (Str str) = showCon d "Str" $ showArg str
137 showPrec d (B8 b) = showCon d "B8" $ showArg b
138 showPrec d (B16 b) = showCon d "B16" $ showArg b
139 showPrec d (B32 b) = showCon d "B32" $ showArg b
140 showPrec d (B64 b) = showCon d "B64" $ showArg b
141 showPrec d (AType x) = showCon d "AType" $ showArg x
142 showPrec d StrType = "StrType"
143 showPrec d VoidType = "VoidType"
144 showPrec d Forgot = "Forgot"
146instance Eq NativeTy where
147 IT8 == IT8 = True
148 IT16 == IT16 = True
149 IT32 == IT32 = True
150 IT64 == IT64 = True
151 _ == _ = False
153instance Eq Reflection.IntTy where
154 (ITFixed x) == (ITFixed y) = x == y
155 ITNative == ITNative = True
156 ITBig == ITBig = True
157 ITChar == ITChar = True
158 _ == _ = False
160instance Eq ArithTy where
161 (ATInt x) == (ATInt y) = x == y
162 ATFloat == ATFloat = True
163 _ == _ = False
165instance Eq Const where
166 (I x) == (I y) = x == y
167 (BI x) == (BI y) = x == y
168 (Fl x) == (Fl y) = x == y
169 (Ch x) == (Ch y) = x == y
170 (Str x) == (Str y) = x == y
171 (B8 x) == (B8 y) = x == y
172 (B16 x) == (B16 y) = x == y
173 (B32 x) == (B32 y) = x == y
174 (B64 x) == (B64 y) = x == y
175 (AType x) == (AType y) = x == y
176 StrType == StrType = True
177 VoidType == VoidType = True
178 Forgot == Forgot = True
179 _ == _ = False
182instance Show NameType where
183 showPrec d Bound = "Bound"
184 showPrec d Ref = "Ref"
185 showPrec d (DCon t ar) = showCon d "DCon" $ showArg t ++ showArg ar
186 showPrec d (TCon t ar) = showCon d "TCon" $ showArg t ++ showArg ar
188instance Eq NameType where
189 Bound == Bound = True
190 Ref == Ref = True
191 (DCon t ar) == (DCon t' ar') = t == t' && ar == ar'
192 (TCon t ar) == (TCon t' ar') = t == t' && ar == ar'
193 x == y = False
195instance (Show a) => Show (Binder a) where
196 showPrec d (Lam t) = showCon d "Lam" $ showArg t
197 showPrec d (Pi t1 t2) = showCon d "Pi" $ showArg t1 ++ showArg t2
198 showPrec d (Let t1 t2) = showCon d "Let" $ showArg t1 ++ showArg t2
199 showPrec d (NLet t1 t2) = showCon d "NLet" $ showArg t1 ++ showArg t2
200 showPrec d (Hole t) = showCon d "Hole" $ showArg t
201 showPrec d (GHole t) = showCon d "GHole" $ showArg t
202 showPrec d (Guess t1 t2) = showCon d "Guess" $ showArg t1 ++ showArg t2
203 showPrec d (PVar t) = showCon d "PVar" $ showArg t
204 showPrec d (PVTy t) = showCon d "PVTy" $ showArg t
206instance (Eq a) => Eq (Binder a) where
207 (Lam t) == (Lam t') = t == t'
208 (Pi t k) == (Pi t' k') = t == t' && k == k'
209 (Let t1 t2) == (Let t1' t2') = t1 == t1' && t2 == t2'
210 (NLet t1 t2) == (NLet t1' t2') = t1 == t1' && t2 == t2'
211 (Hole t) == (Hole t') = t == t'
212 (GHole t) == (GHole t') = t == t'
213 (Guess t1 t2) == (Guess t1' t2') = t1 == t1' && t2 == t2'
214 (PVar t) == (PVar t') = t == t'
215 (PVTy t) == (PVTy t') = t == t'
216 x == y = False
218instance Show TT where
219 showPrec = my_show
220 where %assert_total my_show : Prec -> TT -> String
221 my_show d (P nt n t) = showCon d "P" $ showArg nt ++ showArg n ++ showArg t
222 my_show d (V i) = showCon d "V" $ showArg i
223 my_show d (Bind n b t) = showCon d "Bind" $ showArg n ++ showArg b ++ showArg t
224 my_show d (App t1 t2) = showCon d "App" $ showArg t1 ++ showArg t2
225 my_show d (TConst c) = showCon d "TConst" $ showArg c
226 my_show d (Proj tm i) = showCon d "Proj" $ showArg tm ++ showArg i
227 my_show d Erased = "Erased"
228 my_show d Impossible = "Impossible"
229 my_show d (TType u) = showCon d "TType" $ showArg u
231instance Eq TT where
232 a == b = equalp a b
233 where %assert_total equalp : TT -> TT -> Bool
234 equalp (P nt n t) (P nt' n' t') = nt == nt' && n == n' && t == t'
235 equalp (V i) (V i') = i == i'
236 equalp (Bind n b t) (Bind n' b' t') = n == n' && b == b' && t == t'
237 equalp (App t1 t2) (App t1' t2') = t1 == t1' && t2 == t2'
238 equalp (TConst c) (TConst c') = c == c'
239 equalp (Proj tm i) (Proj tm' i') = tm == tm' && i == i'
240 equalp Erased Erased = True
241 equalp Impossible Impossible = True
242 equalp (TType u) (TType u') = u == u'
243 equalp x y = False
245total
246forget : TT -> Maybe Raw
247forget tm = fe [] tm
248 where
249 atIndex : List a -> Int -> Maybe a
250 atIndex [] _ = Nothing
251 atIndex (x::xs) n =
252 case compare n 0 of
253 EQ => Just x
254 LT => Nothing
255 GT => atIndex xs (n-1)
257 %assert_total
258 fe : List TTName -> TT -> Maybe Raw
259 fe env (P _ n _) = Just $ Var n
260 fe env (V i) = map Var (atIndex env i)
261 fe env (Bind n b sc) = [| RBind (pure n) (traverse (fe env) b) (fe (n::env) sc) |]
262 fe env (App f a) = [| RApp (fe env f) (fe env a) |]
263 fe env (TConst c) = Just $ RConstant c
264 fe env (Proj tm i) = Nothing -- runtime only, not useful for metaprogramming
265 fe env (TType i) = Just RType
266 fe env Erased = Just $ RConstant Forgot
267 fe env Impossible = Nothing
269instance Show Raw where
270 showPrec = my_show
271 where %assert_total my_show : Prec -> Raw -> String
272 my_show d (Var n) = showCon d "Var" $ showArg n
273 my_show d (RBind n b tm) = showCon d "RBind" $ showArg n ++ showArg b ++ " " ++ my_show App tm
274 my_show d (RApp tm tm') = showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'
275 my_show d RType = "RType"
276 my_show d (RForce tm) = showCon d "RForce" $ " " ++ my_show App tm
277 my_show d (RConstant c) = showCon d "RConstant" $ showArg c
279instance Show SourceLocation where
280 showPrec d (FileLoc filename line col) = showCon d "FileLoc" $ showArg filename ++ showArg line ++ showArg col
282instance Show Err where
283 showPrec d (Msg x) = showCon d "Msg" $ showArg x
284 showPrec d (InternalMsg x) = showCon d "InternalMsg" $ showArg x
285 showPrec d (CantUnify x tm tm' err xs y) = showCon d "CantUnify" $ showArg x ++
286 showArg tm ++ showArg tm' ++ showArg err ++
287 showArg xs ++ showArg y
288 showPrec d (InfiniteUnify n tm xs) = showCon d "InfiniteUnify" $ showArg n ++ showArg tm ++ showArg xs
289 showPrec d (CantConvert tm tm' xs) = showCon d "CantConvert" $ showArg tm ++ showArg tm' ++ showArg xs
290 showPrec d (CantSolveGoal tm ctxt) = showCon d "CantSolveGoal" $ showArg tm ++ showArg ctxt
291 showPrec d (UnifyScope n n' tm xs) = showCon d "UnifyScope" $ showArg n ++ showArg n' ++ showArg tm ++ showArg xs
292 showPrec d (CantInferType x) = showCon d "CantInferType" $ showArg x
293 showPrec d (NonFunctionType tm tm') = showCon d "NonFunctionType" $ showArg tm ++ showArg tm'
294 showPrec d (NotEquality tm tm') = showCon d "NotEquality" $ showArg tm ++ showArg tm'
295 showPrec d (TooManyArguments n) = showCon d "TooManyArguments" $ showArg n
296 showPrec d (CantIntroduce tm) = showCon d "CantIntroduce" $ showArg tm
297 showPrec d (NoSuchVariable n) = showCon d "NoSuchVariable" $ showArg n
298 showPrec d (WithFnType tm) = showCon d "WithFnType" $ showArg tm
299 showPrec d (CantMatch tm) = showCon d "CantMatch" $ showArg tm
300 showPrec d (NoTypeDecl n) = showCon d "NoTypeDecl" $ showArg n
301 showPrec d (NotInjective tm tm' x) = showCon d "NotInjective" $ showArg tm ++ showArg tm'
302 showPrec d (CantResolve tm) = showCon d "CantResolve" $ showArg tm
303 showPrec d (InvalidTCArg n tm) = showCon d "InvalidTCName" $ showArg n ++ showArg tm
304 showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs
305 showPrec d (NoValidAlts xs) = showCon d "NoValidAlts" $ showArg xs
306 showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm
307 showPrec d (NoEliminator s tm) = showCon d "NoEliminator" $ showArg s ++ showArg tm
308 showPrec d UniverseError = "UniverseError"
309 showPrec d ProgramLineComment = "ProgramLineComment"
310 showPrec d (Inaccessible n) = showCon d "Inaccessible" $ showArg n
311 showPrec d (UnknownImplicit n f) = showCon d "UnknownImplicit" $ showArg n ++ showArg f
312 showPrec d (NonCollapsiblePostulate n) = showCon d "NonCollapsiblePostulate" $ showArg n
313 showPrec d (AlreadyDefined n) = showCon d "AlreadyDefined" $ showArg n
314 showPrec d (ProofSearchFail err) = showCon d "ProofSearchFail" $ showArg err
315 showPrec d (NoRewriting tm) = showCon d "NoRewriting" $ showArg tm
316 showPrec d (ProviderError x) = showCon d "ProviderError" $ showArg x
317 showPrec d (LoadingFailed x err) = showCon d "LoadingFailed" $ showArg x ++ showArg err
319-------------------------
320-- Idiom brackets for Raw
321-------------------------
323(<*>) : Raw -> Raw -> Raw
324(<*>) = RApp
326pure : Raw -> Raw
327pure = id
329--------------------------------------
330-- Instances for definition reflection
331--------------------------------------
332instance Show Erasure where
333 show Erased = "Erased"
334 show NotErased = "NotErased"
336instance Show Arg where
337 showPrec d (Explicit n e t) = showCon d "Explicit" $ showArg n ++ showArg e ++ showArg t
338 showPrec d (Implicit n e t) = showCon d "Implicit" $ showArg n ++ showArg e ++ showArg t
339 showPrec d (Constraint n e t) = showCon d "Constraint" $ showArg n ++ showArg e ++ showArg t
341instance Show TyDecl where
342 showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn ++
343 showArg args ++ showArg ret