git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/libs/base/Language/Reflection/Utils.idr
271 lines 10 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 (AType x) = "(AType ...)"
97 show StrType = "StrType"
98 show VoidType = "VoidType"
99 show Forgot = "Forgot"
101instance Eq NativeTy where
102 IT8 == IT8 = True
103 IT16 == IT16 = True
104 IT32 == IT32 = True
105 IT64 == IT64 = True
106 _ == _ = False
108instance Eq Reflection.IntTy where
109 (ITFixed x) == (ITFixed y) = x == y
110 ITNative == ITNative = True
111 ITBig == ITBig = True
112 ITChar == ITChar = True
113 _ == _ = False
115instance Eq ArithTy where
116 (ATInt x) == (ATInt y) = x == y
117 ATFloat == ATFloat = True
118 _ == _ = False
120instance Eq Const where
121 (I x) == (I y) = x == y
122 (BI x) == (BI y) = x == y
123 (Fl x) == (Fl y) = x == y
124 (Ch x) == (Ch y) = x == y
125 (Str x) == (Str y) = x == y
126 (B8 x) == (B8 y) = x == y
127 (B16 x) == (B16 y) = x == y
128 (B32 x) == (B32 y) = x == y
129 (B64 x) == (B64 y) = x == y
130 (AType x) == (AType y) = x == y
131 StrType == StrType = True
132 VoidType == VoidType = True
133 Forgot == Forgot = True
134 _ == _ = False
137instance Show NameType where
138 show Bound = "Bound"
139 show Ref = "Ref"
140 show (DCon t ar) = "(DCon " ++ show t ++ " " ++ show ar ++ ")"
141 show (TCon t ar) = "(TCon " ++ show t ++ " " ++ show ar ++ ")"
143instance Eq NameType where
144 Bound == Bound = True
145 Ref == Ref = True
146 (DCon t ar) == (DCon t' ar') = t == t' && ar == ar'
147 (TCon t ar) == (TCon t' ar') = t == t' && ar == ar'
148 x == y = False
150instance (Show a) => Show (Binder a) where
151 show (Lam t) = "(Lam " ++ show t ++ ")"
152 show (Pi t _) = "(Pi " ++ show t ++ ")"
153 show (Let t1 t2) = "(Let " ++ show t1 ++ " " ++ show t2 ++ ")"
154 show (NLet t1 t2) = "(NLet " ++ show t1 ++ " " ++ show t2 ++ ")"
155 show (Hole t) = "(Hole " ++ show t ++ ")"
156 show (GHole t) = "(GHole " ++ show t ++ ")"
157 show (Guess t1 t2) = "(Guess " ++ show t1 ++ " " ++ show t2 ++ ")"
158 show (PVar t) = "(PVar " ++ show t ++ ")"
159 show (PVTy t) = "(PVTy " ++ show t ++ ")"
161instance (Eq a) => Eq (Binder a) where
162 (Lam t) == (Lam t') = t == t'
163 (Pi t k) == (Pi t' k') = t == t' && k == k'
164 (Let t1 t2) == (Let t1' t2') = t1 == t1' && t2 == t2'
165 (NLet t1 t2) == (NLet t1' t2') = t1 == t1' && t2 == t2'
166 (Hole t) == (Hole t') = t == t'
167 (GHole t) == (GHole t') = t == t'
168 (Guess t1 t2) == (Guess t1' t2') = t1 == t1' && t2 == t2'
169 (PVar t) == (PVar t') = t == t'
170 (PVTy t) == (PVTy t') = t == t'
171 x == y = False
173instance Show TT where
174 show = my_show
175 where %assert_total my_show : TT -> String
176 my_show (P nt n t) = "(P " ++ show nt ++ " " ++ show n ++ " " ++ show t ++ ")"
177 my_show (V i) = "(V " ++ show i ++ ")"
178 my_show (Bind n b t) = "(Bind " ++ show n ++ " " ++ show b ++ " " ++ show t ++ ")"
179 my_show (App t1 t2) = "(App " ++ show t1 ++ " " ++ show t2 ++ ")"
180 my_show (TConst c) = "(TConst " ++ show c ++ ")"
181 my_show (Proj tm i) = "(Proj " ++ show tm ++ " " ++ show i ++ ")"
182 my_show Erased = "Erased"
183 my_show Impossible = "Impossible"
184 my_show (TType u) = "(TType " ++ show u ++ ")"
186instance Eq TT where
187 a == b = equalp a b
188 where %assert_total equalp : TT -> TT -> Bool
189 equalp (P nt n t) (P nt' n' t') = nt == nt' && n == n' && t == t'
190 equalp (V i) (V i') = i == i'
191 equalp (Bind n b t) (Bind n' b' t') = n == n' && b == b' && t == t'
192 equalp (App t1 t2) (App t1' t2') = t1 == t1' && t2 == t2'
193 equalp (TConst c) (TConst c') = c == c'
194 equalp (Proj tm i) (Proj tm' i') = tm == tm' && i == i'
195 equalp Erased Erased = True
196 equalp Impossible Impossible = True
197 equalp (TType u) (TType u') = u == u'
198 equalp x y = False
200total
201forget : TT -> Maybe Raw
202forget tm = fe [] tm
203 where
204 atIndex : List a -> Int -> Maybe a
205 atIndex [] _ = Nothing
206 atIndex (x::xs) n =
207 case compare n 0 of
208 EQ => Just x
209 LT => Nothing
210 GT => atIndex xs (n-1)
212 %assert_total
213 fe : List TTName -> TT -> Maybe Raw
214 fe env (P _ n _) = Just $ Var n
215 fe env (V i) = map Var (atIndex env i)
216 fe env (Bind n b sc) = [| RBind (pure n) (traverse (fe env) b) (fe (n::env) sc) |]
217 fe env (App f a) = [| RApp (fe env f) (fe env a) |]
218 fe env (TConst c) = Just $ RConstant c
219 fe env (Proj tm i) = Nothing -- runtime only, not useful for metaprogramming
220 fe env (TType i) = Just RType
221 fe env Erased = Just $ RConstant Forgot
222 fe env Impossible = Nothing
224instance Show Raw where
225 show r = my_show r
226 where %assert_total my_show : Raw -> String
227 my_show (Var n) = "Var " ++ show n
228 my_show (RBind n b tm) = "RBind " ++ show n ++ " " ++ show b ++ " (" ++ my_show tm ++ ")"
229 my_show (RApp tm tm') = "RApp " ++ my_show tm ++ " " ++ my_show tm'
230 my_show RType = "RType"
231 my_show (RForce tm) = "RForce " ++ my_show tm
232 my_show (RConstant c) = "RConstant " ++ show c
234instance Show SourceLocation where
235 show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col
237instance Show Err where
238 show (Msg x) = "Msg \"" ++ x ++ "\""
239 show (InternalMsg x) = "InternalMsg \"" ++ x ++ "\""
240 show (CantUnify x tm tm' err xs y) = "CantUnify " ++ show x ++
241 " ( " ++ show tm ++ ") (" ++ show tm' ++ ") (" ++ show err ++ ") " ++
242 show xs ++ " " ++ show y
243 show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs
244 show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs
245 show (CantSolveGoal tm ctxt) = "CantSolveGoal " ++ show tm ++ " " ++ show ctxt
246 show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs
247 show (CantInferType x) = "CantInferType " ++ show x
248 show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'
249 show (NotEquality tm tm') = "NotEquality " ++ show tm ++ " " ++ show tm'
250 show (TooManyArguments n) = "TooManyArguments " ++ show n
251 show (CantIntroduce tm) = "CantIntroduce " ++ show tm
252 show (NoSuchVariable n) = "NoSuchVariable " ++ show n
253 show (WithFnType tm) = "WithFnType " ++ show tm
254 show (CantMatch tm) = "CantMatch " ++ show tm
255 show (NoTypeDecl n) = "NoTypeDecl " ++ show n
256 show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'
257 show (CantResolve tm) = "CantResolve " ++ show tm
258 show (InvalidTCArg n tm) = "InvalidTCName " ++ show n ++ " (" ++ show tm ++ ")"
259 show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs
260 show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm
261 show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm
262 show UniverseError = "UniverseError"
263 show ProgramLineComment = "ProgramLineComment"
264 show (Inaccessible n) = "Inaccessible " ++ show n
265 show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n
266 show (AlreadyDefined n) = "AlreadyDefined " ++ show n
267 show (ProofSearchFail err) = "ProofSearchFail " ++ show err
268 show (NoRewriting tm) = "NoRewriting " ++ show tm
269 show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""
270 show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"