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