@@ -1,6 +1,7 @@
11module Language.Reflection.Utils
22
33import Language.Reflection
4+import Language.Reflection.Errors
45
56--------------------------------------------------------
67-- Tactic construction conveniences
@@ -185,3 +186,73 @@ instance Eq TT where
185186 equalp Impossible Impossible = True
186187 equalp (TType u) (TType u') = u == u'
187188 equalp x y = False
189+
190+total
191+forget : TT -> Maybe Raw
192+forget tm = fe [] tm
193+ where
194+ atIndex : List a -> Int -> Maybe a
195+ atIndex [] _ = Nothing
196+ atIndex (x::xs) n =
197+ case compare n 0 of
198+ EQ => Just x
199+ LT => Nothing
200+ GT => atIndex xs (n-1)
201+
202+ %assert_total
203+ fe : List TTName -> TT -> Maybe Raw
204+ fe env (P _ n _) = Just $ Var n
205+ fe env (V i) = map Var (atIndex env i)
206+ fe env (Bind n b sc) = [| RBind (pure n) (traverse (fe env) b) (fe (n::env) sc) |]
207+ fe env (App f a) = [| RApp (fe env f) (fe env a) |]
208+ fe env (TConst c) = Just $ RConstant c
209+ fe env (Proj tm i) = Nothing -- runtime only, not useful for metaprogramming
210+ fe env (TType i) = Just RType
211+ fe env Erased = Just $ RConstant Forgot
212+ fe env Impossible = Nothing
213+
214+instance Show Raw where
215+ show r = my_show r
216+ where %assert_total my_show : Raw -> String
217+ my_show (Var n) = "Var " ++ show n
218+ my_show (RBind n b tm) = "RBind " ++ show n ++ " " ++ show b ++ " (" ++ my_show tm ++ ")"
219+ my_show (RApp tm tm') = "RApp " ++ my_show tm ++ " " ++ my_show tm'
220+ my_show RType = "RType"
221+ my_show (RForce tm) = "RForce " ++ my_show tm
222+ my_show (RConstant c) = "RConstant " ++ show c
223+
224+instance Show SourceLocation where
225+ show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col
226+
227+instance Show Err where
228+ show (Msg x) = "Msg \"" ++ x ++ "\""
229+ show (InternalMsg x) = "InternalMsg \"" ++ x ++ "\""
230+ show (CantUnify x tm tm' err xs y) = "CantUnify " ++ show x ++
231+ " ( " ++ show tm ++ ") (" ++ show tm' ++ ") (" ++ show err ++ ") " ++
232+ show xs ++ " " ++ show y
233+ show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs
234+ show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs
235+ show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs
236+ show (CantInferType x) = "CantInferType " ++ show x
237+ show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'
238+ show (NotEquality tm tm') = "NotEquality " ++ show tm ++ " " ++ show tm'
239+ show (TooManyArguments n) = "TooManyArguments " ++ show n
240+ show (CantIntroduce tm) = "CantIntroduce " ++ show tm
241+ show (NoSuchVariable n) = "NoSuchVariable " ++ show n
242+ show (NoTypeDecl n) = "NoTypeDecl " ++ show n
243+ show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'
244+ show (CantResolve tm) = "CantResolve " ++ show tm
245+ show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs
246+ show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm
247+ show UniverseError = "UniverseError"
248+ show ProgramLineComment = "ProgramLineComment"
249+ show (Inaccessible n) = "Inaccessible " ++ show n
250+ show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n
251+ show (AlreadyDefined n) = "AlreadyDefined " ++ show n
252+ show (ProofSearchFail err) = "ProofSearchFail " ++ show err
253+ show (NoRewriting tm) = "NoRewriting " ++ show tm
254+ show (At loc err) = "At " ++ show loc ++ " " ++ show err
255+ show (Elaborating x n err) = "Elaborating " ++ show x ++ " " ++ show x ++ " " ++ show n ++ " (" ++ show err ++ ")"
256+ show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""
257+ show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"
258+