git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/Reflection.hs
1114 lines 50 kB history raw
1{-| Code related to Idris's reflection system. This module contains
2quoters and unquoters along with some supporting datatypes.
3-}
4{-# LANGUAGE PatternGuards #-}
5{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
6module Idris.Reflection where
8import Control.Applicative ((<$>), (<*>), pure)
9import Control.Monad (liftM, liftM2, liftM3)
10import Data.Maybe (catMaybes)
11import Data.List ((\\))
12import qualified Data.Text as T
14import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
15 movelast, runElab, solve)
16import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)
17import Idris.Core.TT
19import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes),
20 PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..),
21 initEState, pairCon, pairTy)
22import Idris.Delaborate (delab)
24data RErasure = RErased | RNotErased deriving Show
26data RArg = RExplicit { argName :: Name, argErased :: RErasure, argTy :: Raw }
27 | RImplicit { argName :: Name, argErased :: RErasure, argTy :: Raw }
28 | RConstraint { argName :: Name, argErased :: RErasure, argTy :: Raw }
29 deriving Show
31data RTyDecl = RDeclare Name [RArg] Raw deriving Show
33data RTyConArg = RParameter { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }
34 | RIndex { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }
35 deriving Show
37data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RArg], Raw)] deriving Show
39rArgOpts :: RErasure -> [ArgOpt]
40rArgOpts RErased = [InaccessibleArg]
41rArgOpts _ = []
43rArgToPArg :: RArg -> PArg
44rArgToPArg (RExplicit n e _) = PExp 0 (rArgOpts e) n Placeholder
45rArgToPArg (RImplicit n e _) = PImp 0 False (rArgOpts e) n Placeholder
46rArgToPArg (RConstraint n e _) = PConstraint 0 (rArgOpts e) n Placeholder
48data RFunClause = RMkFunClause Raw Raw
49 | RMkImpossibleClause Raw
50 deriving Show
52data RFunDefn = RDefineFun Name [RFunClause] deriving Show
54-- | Prefix a name with the "Language.Reflection" namespace
55reflm :: String -> Name
56reflm n = sNS (sUN n) ["Reflection", "Language"]
58-- | Prefix a name with the "Language.Reflection.Elab" namespace
59tacN :: String -> Name
60tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]
62-- | Reify tactics from their reflected representation
63reify :: IState -> Term -> ElabD PTactic
64reify _ (P _ n _) | n == reflm "Intros" = return Intros
65reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
66reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
67reify _ (P _ n _) | n == reflm "Solve" = return Solve
68reify _ (P _ n _) | n == reflm "Compute" = return Compute
69reify _ (P _ n _) | n == reflm "Skip" = return Skip
70reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
71reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
72reify ist t@(App _ _ _)
73 | (P _ f _, args) <- unApply t = reifyApp ist f args
74reify _ t = fail ("Unknown tactic " ++ show t)
76reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
77reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
78reifyApp _ t [Constant (I i)]
79 | t == reflm "Search" = return (ProofSearch True True i Nothing [])
80reifyApp _ t [x]
81 | t == reflm "Refine" = do n <- reifyTTName x
82 return $ Refine n []
83reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
84 goal <- reifyTT ty
85 return $ Claim n' (delab ist goal)
86reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
87reifyApp ist t [Constant (Str n), x]
88 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
89reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
90reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
91reifyApp ist t [t'] | t == reflm "Case" = liftM (CaseTac . delab ist) (reifyTT t')
92reifyApp ist t [t']
93 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
94reifyApp ist t [t']
95 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
96reifyApp ist t [t']
97 | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
98reifyApp _ t [t']
99 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
100reifyApp ist t [t']
101 | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
102reifyApp ist t [x]
103 | t == reflm "Focus" = liftM Focus (reifyTTName x)
104reifyApp ist t [t']
105 | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
106reifyApp ist t [n, t']
107 | t == reflm "LetTac" = do n' <- reifyTTName n
108 t'' <- reifyTT t'
109 return $ LetTac n' (delab ist t')
110reifyApp ist t [n, tt', t']
111 | t == reflm "LetTacTy" = do n' <- reifyTTName n
112 tt'' <- reifyTT tt'
113 t'' <- reifyTT t'
114 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
115reifyApp ist t [errs]
116 | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
117reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
119reifyBool :: Term -> ElabD Bool
120reifyBool (P _ n _) | n == sNS (sUN "True") ["Bool", "Prelude"] = return True
121 | n == sNS (sUN "False") ["Bool", "Prelude"] = return False
122reifyBool tm = fail $ "Not a Boolean: " ++ show tm
124reifyInt :: Term -> ElabD Int
125reifyInt (Constant (I i)) = return i
126reifyInt tm = fail $ "Not an Int: " ++ show tm
128reifyPair :: (Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
129reifyPair left right (App _ (App _ (App _ (App _ (P _ n _) _) _) x) y)
130 | n == pairCon = liftM2 (,) (left x) (right y)
131reifyPair left right tm = fail $ "Not a pair: " ++ show tm
133reifyList :: (Term -> ElabD a) -> Term -> ElabD [a]
134reifyList getElt lst =
135 case unList lst of
136 Nothing -> fail "Couldn't reify a list"
137 Just xs -> mapM getElt xs
139reifyReportParts :: Term -> ElabD [ErrorReportPart]
140reifyReportParts errs =
141 case unList errs of
142 Nothing -> fail "Failed to reify errors"
143 Just errs' ->
144 let parts = mapM reifyReportPart errs' in
145 case parts of
146 Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
147 Right errs'' ->
148 return errs''
150-- | Reify terms from their reflected representation
151reifyTT :: Term -> ElabD Term
152reifyTT t@(App _ _ _)
153 | (P _ f _, args) <- unApply t = reifyTTApp f args
154reifyTT t@(P _ n _)
155 | n == reflm "Erased" = return $ Erased
156reifyTT t@(P _ n _)
157 | n == reflm "Impossible" = return $ Impossible
158reifyTT t = fail ("Unknown reflection term: " ++ show t)
160reifyTTApp :: Name -> [Term] -> ElabD Term
161reifyTTApp t [nt, n, x]
162 | t == reflm "P" = do nt' <- reifyTTNameType nt
163 n' <- reifyTTName n
164 x' <- reifyTT x
165 return $ P nt' n' x'
166reifyTTApp t [Constant (I i)]
167 | t == reflm "V" = return $ V i
168reifyTTApp t [n, b, x]
169 | t == reflm "Bind" = do n' <- reifyTTName n
170 b' <- reifyTTBinder reifyTT (reflm "TT") b
171 x' <- reifyTT x
172 return $ Bind n' b' x'
173reifyTTApp t [f, x]
174 | t == reflm "App" = do f' <- reifyTT f
175 x' <- reifyTT x
176 return $ App Complete f' x'
177reifyTTApp t [c]
178 | t == reflm "TConst" = liftM Constant (reifyTTConst c)
179reifyTTApp t [t', Constant (I i)]
180 | t == reflm "Proj" = do t'' <- reifyTT t'
181 return $ Proj t'' i
182reifyTTApp t [tt]
183 | t == reflm "TType" = liftM TType (reifyTTUExp tt)
184reifyTTApp t [tt]
185 | t == reflm "UType" = liftM UType (reifyUniverse tt)
186reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
188reifyUniverse :: Term -> ElabD Universe
189reifyUniverse (P _ n _) | n == reflm "AllTypes" = return AllTypes
190 | n == reflm "UniqueType" = return UniqueType
191 | n == reflm "NullType" = return NullType
192reifyUniverse tm = fail ("Unknown reflection universe: " ++ show tm)
194-- | Reify raw terms from their reflected representation
195reifyRaw :: Term -> ElabD Raw
196reifyRaw t@(App _ _ _)
197 | (P _ f _, args) <- unApply t = reifyRawApp f args
198reifyRaw t@(P _ n _)
199 | n == reflm "RType" = return $ RType
200reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)
202reifyRawApp :: Name -> [Term] -> ElabD Raw
203reifyRawApp t [n]
204 | t == reflm "Var" = liftM Var (reifyTTName n)
205reifyRawApp t [n, b, x]
206 | t == reflm "RBind" = do n' <- reifyTTName n
207 b' <- reifyTTBinder reifyRaw (reflm "Raw") b
208 x' <- reifyRaw x
209 return $ RBind n' b' x'
210reifyRawApp t [f, x]
211 | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
212reifyRawApp t [t']
213 | t == reflm "RForce" = liftM RForce (reifyRaw t')
214reifyRawApp t [c]
215 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
216reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
218reifyTTName :: Term -> ElabD Name
219reifyTTName t
220 | (P _ f _, args) <- unApply t = reifyTTNameApp f args
221reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
223reifyTTNameApp :: Name -> [Term] -> ElabD Name
224reifyTTNameApp t [Constant (Str n)]
225 | t == reflm "UN" = return $ sUN n
226reifyTTNameApp t [n, ns]
227 | t == reflm "NS" = do n' <- reifyTTName n
228 ns' <- reifyTTNamespace ns
229 return $ sNS n' ns'
230reifyTTNameApp t [Constant (I i), Constant (Str n)]
231 | t == reflm "MN" = return $ sMN i n
232reifyTTNameApp t [sn]
233 | t == reflm "SN"
234 , (P _ f _, args) <- unApply sn = SN <$> reifySN f args
235 where reifySN :: Name -> [Term] -> ElabD SpecialName
236 reifySN t [Constant (I i), n1, n2]
237 | t == reflm "WhereN" = WhereN i <$> reifyTTName n1 <*> reifyTTName n2
238 reifySN t [Constant (I i), n]
239 | t == reflm "WithN" = WithN i <$> reifyTTName n
240 reifySN t [n, ss]
241 | t == reflm "InstanceN" =
242 case unList ss of
243 Nothing -> fail "Can't reify InstanceN strings"
244 Just ss' -> InstanceN <$> reifyTTName n <*>
245 pure [T.pack s | Constant (Str s) <- ss']
246 reifySN t [n, Constant (Str s)]
247 | t == reflm "ParentN" =
248 ParentN <$> reifyTTName n <*> pure (T.pack s)
249 reifySN t [n]
250 | t == reflm "MethodN" =
251 MethodN <$> reifyTTName n
252 reifySN t [n]
253 | t == reflm "CaseN" =
254 CaseN <$> reifyTTName n
255 reifySN t [n]
256 | t == reflm "ElimN" =
257 ElimN <$> reifyTTName n
258 reifySN t [n]
259 | t == reflm "InstanceCtorN" =
260 InstanceCtorN <$> reifyTTName n
261 reifySN t [n1, n2]
262 | t == reflm "MetaN" =
263 MetaN <$> reifyTTName n1 <*> reifyTTName n2
264 reifySN t args = fail $ "Can't reify special name " ++ show t ++ show args
265reifyTTNameApp t []
266 | t == reflm "NErased" = return NErased
267reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
269reifyTTNamespace :: Term -> ElabD [String]
270reifyTTNamespace t@(App _ _ _)
271 = case unApply t of
272 (P _ f _, [Constant StrType])
273 | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
274 (P _ f _, [Constant StrType, Constant (Str n), ns])
275 | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
276 _ -> fail ("Unknown reflection namespace arg: " ++ show t)
277reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
279reifyTTNameType :: Term -> ElabD NameType
280reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
281reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
282reifyTTNameType t@(App _ _ _)
283 = case unApply t of
284 (P _ f _, [Constant (I tag), Constant (I num)])
285 | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!
286 | f == reflm "TCon" -> return $ TCon tag num
287 _ -> fail ("Unknown reflection name type: " ++ show t)
288reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
290reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
291reifyTTBinder reificator binderType t@(App _ _ _)
292 = case unApply t of
293 (P _ f _, bt:args) | forget bt == Var binderType
294 -> reifyTTBinderApp reificator f args
295 _ -> fail ("Mismatching binder reflection: " ++ show t)
296reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
298reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
299reifyTTBinderApp reif f [t]
300 | f == reflm "Lam" = liftM Lam (reif t)
301reifyTTBinderApp reif f [t, k]
302 | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)
303reifyTTBinderApp reif f [x, y]
304 | f == reflm "Let" = liftM2 Let (reif x) (reif y)
305reifyTTBinderApp reif f [x, y]
306 | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
307reifyTTBinderApp reif f [t]
308 | f == reflm "Hole" = liftM Hole (reif t)
309reifyTTBinderApp reif f [t]
310 | f == reflm "GHole" = liftM (GHole 0) (reif t)
311reifyTTBinderApp reif f [x, y]
312 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
313reifyTTBinderApp reif f [t]
314 | f == reflm "PVar" = liftM PVar (reif t)
315reifyTTBinderApp reif f [t]
316 | f == reflm "PVTy" = liftM PVTy (reif t)
317reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
319reifyTTConst :: Term -> ElabD Const
320reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
321reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
322reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
323reifyTTConst t@(App _ _ _)
324 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
325reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
327reifyTTConstApp :: Name -> Term -> ElabD Const
328reifyTTConstApp f aty
329 | f == reflm "AType" = fmap AType (reifyArithTy aty)
330reifyTTConstApp f (Constant c@(I _))
331 | f == reflm "I" = return $ c
332reifyTTConstApp f (Constant c@(BI _))
333 | f == reflm "BI" = return $ c
334reifyTTConstApp f (Constant c@(Fl _))
335 | f == reflm "Fl" = return $ c
336reifyTTConstApp f (Constant c@(I _))
337 | f == reflm "Ch" = return $ c
338reifyTTConstApp f (Constant c@(Str _))
339 | f == reflm "Str" = return $ c
340reifyTTConstApp f (Constant c@(B8 _))
341 | f == reflm "B8" = return $ c
342reifyTTConstApp f (Constant c@(B16 _))
343 | f == reflm "B16" = return $ c
344reifyTTConstApp f (Constant c@(B32 _))
345 | f == reflm "B32" = return $ c
346reifyTTConstApp f (Constant c@(B64 _))
347 | f == reflm "B64" = return $ c
348reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
350reifyArithTy :: Term -> ElabD ArithTy
351reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
352reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
353reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
355reifyNativeTy :: Term -> ElabD NativeTy
356reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
357reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
358reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
359reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
360reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
362reifyIntTy :: Term -> ElabD IntTy
363reifyIntTy (App _ (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
364reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
365reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
366reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
367reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
369reifyTTUExp :: Term -> ElabD UExp
370reifyTTUExp t@(App _ _ _)
371 = case unApply t of
372 (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
373 (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
374 _ -> fail ("Unknown reflection type universe expression: " ++ show t)
375reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
377-- | Create a reflected call to a named function/constructor
378reflCall :: String -> [Raw] -> Raw
379reflCall funName args
380 = raw_apply (Var (reflm funName)) args
382-- | Lift a term into its Language.Reflection.TT representation
383reflect :: Term -> Raw
384reflect = reflectTTQuote []
386-- | Lift a term into its Language.Reflection.Raw representation
387reflectRaw :: Raw -> Raw
388reflectRaw = reflectRawQuote []
390claimTy :: Name -> Raw -> ElabD Name
391claimTy n ty = do n' <- getNameFrom n
392 claim n' ty
393 return n'
395-- | Convert a reflected term to a more suitable form for pattern-matching.
396-- In particular, the less-interesting bits are elaborated to _ patterns. This
397-- happens to NameTypes, universe levels, names that are bound but not used,
398-- and the type annotation field of the P constructor.
399reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
400reflectTTQuotePattern unq (P _ n _)
401 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
402 do fill (Var n) ; solve
403 | otherwise =
404 do tyannot <- claimTy (sMN 0 "pTyAnnot") (Var (reflm "TT"))
405 movelast tyannot -- use a _ pattern here
406 nt <- getNameFrom (sMN 0 "nt")
407 claim nt (Var (reflm "NameType"))
408 movelast nt -- use a _ pattern here
409 n' <- getNameFrom (sMN 0 "n")
410 claim n' (Var (reflm "TTName"))
411 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
412 solve
413 focus n'; reflectNameQuotePattern n
414reflectTTQuotePattern unq (V n)
415 = do fill $ reflCall "V" [RConstant (I n)]
416 solve
417reflectTTQuotePattern unq (Bind n b x)
418 = do x' <- claimTy (sMN 0 "sc") (Var (reflm "TT"))
419 movelast x'
420 b' <- getNameFrom (sMN 0 "binder")
421 claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
422 (Var (sNS (sUN "TT") ["Reflection", "Language"])))
423 if n `elem` freeNames x
424 then do fill $ reflCall "Bind"
425 [reflectName n,
426 Var b',
427 Var x']
428 solve
429 else do any <- getNameFrom (sMN 0 "anyName")
430 claim any (Var (reflm "TTName"))
431 movelast any
432 fill $ reflCall "Bind"
433 [Var any,
434 Var b',
435 Var x']
436 solve
437 focus x'; reflectTTQuotePattern unq x
438 focus b'; reflectBinderQuotePattern reflectTTQuotePattern (Var $ reflm "TT") unq b
439reflectTTQuotePattern unq (App _ f x)
440 = do f' <- claimTy (sMN 0 "f") (Var (reflm "TT")) ; movelast f'
441 x' <- claimTy (sMN 0 "x") (Var (reflm "TT")) ; movelast x'
442 fill $ reflCall "App" [Var f', Var x']
443 solve
444 focus f'; reflectTTQuotePattern unq f
445 focus x'; reflectTTQuotePattern unq x
446reflectTTQuotePattern unq (Constant c)
447 = do fill $ reflCall "TConst" [reflectConstant c]
448 solve
449reflectTTQuotePattern unq (Proj t i)
450 = do t' <- claimTy (sMN 0 "t") (Var (reflm "TT")) ; movelast t'
451 fill $ reflCall "Proj" [Var t', RConstant (I i)]
452 solve
453 focus t'; reflectTTQuotePattern unq t
454reflectTTQuotePattern unq (Erased)
455 = do erased <- claimTy (sMN 0 "erased") (Var (reflm "TT"))
456 movelast erased
457 fill $ (Var erased)
458 solve
459reflectTTQuotePattern unq (Impossible)
460 = do fill $ Var (reflm "Impossible")
461 solve
462reflectTTQuotePattern unq (TType exp)
463 = do ue <- getNameFrom (sMN 0 "uexp")
464 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
465 movelast ue
466 fill $ reflCall "TType" [Var ue]
467 solve
468reflectTTQuotePattern unq (UType u)
469 = do uH <- getNameFrom (sMN 0 "someUniv")
470 claim uH (Var (reflm "Universe"))
471 movelast uH
472 fill $ reflCall "UType" [Var uH]
473 solve
474 focus uH
475 fill (Var (reflm (case u of
476 NullType -> "NullType"
477 UniqueType -> "UniqueType"
478 AllTypes -> "AllTypes")))
479 solve
481reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
482reflectRawQuotePattern unq (Var n)
483 -- the unquoted names already have types, just use them
484 | n `elem` unq = do fill (Var n); solve
485 | otherwise = do fill (reflCall "Var" [reflectName n]); solve
486reflectRawQuotePattern unq (RBind n b sc) =
487 do scH <- getNameFrom (sMN 0 "sc")
488 claim scH (Var (reflm "Raw"))
489 movelast scH
490 bH <- getNameFrom (sMN 0 "binder")
491 claim bH (RApp (Var (reflm "Binder"))
492 (Var (reflm "Raw")))
493 if n `elem` freeNamesR sc
494 then do fill $ reflCall "RBind" [reflectName n,
495 Var bH,
496 Var scH]
497 solve
498 else do any <- getNameFrom (sMN 0 "anyName")
499 claim any (Var (reflm "TTName"))
500 movelast any
501 fill $ reflCall "RBind" [Var any, Var bH, Var scH]
502 solve
503 focus scH; reflectRawQuotePattern unq sc
504 focus bH; reflectBinderQuotePattern reflectRawQuotePattern (Var $ reflm "Raw") unq b
505 where freeNamesR (Var n) = [n]
506 freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
507 freeNamesR body \\ [n],
508 freeNamesR t]
509 freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
510 (freeNamesR body \\ [n])
511 freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
512 freeNamesR RType = []
513 freeNamesR (RUType _) = []
514 freeNamesR (RForce r) = freeNamesR r
515 freeNamesR (RConstant _) = []
516reflectRawQuotePattern unq (RApp f x) =
517 do fH <- getNameFrom (sMN 0 "f")
518 claim fH (Var (reflm "Raw"))
519 movelast fH
520 xH <- getNameFrom (sMN 0 "x")
521 claim xH (Var (reflm "Raw"))
522 movelast xH
523 fill $ reflCall "RApp" [Var fH, Var xH]
524 solve
525 focus fH; reflectRawQuotePattern unq f
526 focus xH; reflectRawQuotePattern unq x
527reflectRawQuotePattern unq RType =
528 do fill (Var (reflm "RType"))
529 solve
530reflectRawQuotePattern unq (RUType univ) =
531 do uH <- getNameFrom (sMN 0 "universe")
532 claim uH (Var (reflm "Universe"))
533 movelast uH
534 fill $ reflCall "RUType" [Var uH]
535 solve
536 focus uH; fill (reflectUniverse univ); solve
537reflectRawQuotePattern unq (RForce r) =
538 do rH <- getNameFrom (sMN 0 "raw")
539 claim rH (Var (reflm "Raw"))
540 movelast rH
541 fill $ reflCall "RForce" [Var rH]
542 solve
543 focus rH; reflectRawQuotePattern unq r
544reflectRawQuotePattern unq (RConstant c) =
545 do cH <- getNameFrom (sMN 0 "const")
546 claim cH (Var (reflm "Constant"))
547 movelast cH
548 fill (reflCall "RConstant" [Var cH]); solve
549 focus cH
550 fill (reflectConstant c); solve
552reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()
553reflectBinderQuotePattern q ty unq (Lam t)
554 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
555 fill $ reflCall "Lam" [ty, Var t']
556 solve
557 focus t'; q unq t
558reflectBinderQuotePattern q ty unq (Pi _ t k)
559 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
560 k' <- claimTy (sMN 0 "k") ty; movelast k';
561 fill $ reflCall "Pi" [ty, Var t', Var k']
562 solve
563 focus t'; q unq t
564reflectBinderQuotePattern q ty unq (Let x y)
565 = do x' <- claimTy (sMN 0 "ty") ty; movelast x';
566 y' <- claimTy (sMN 0 "v")ty; movelast y';
567 fill $ reflCall "Let" [ty, Var x', Var y']
568 solve
569 focus x'; q unq x
570 focus y'; q unq y
571reflectBinderQuotePattern q ty unq (NLet x y)
572 = do x' <- claimTy (sMN 0 "ty") ty; movelast x'
573 y' <- claimTy (sMN 0 "v") ty; movelast y'
574 fill $ reflCall "NLet" [ty, Var x', Var y']
575 solve
576 focus x'; q unq x
577 focus y'; q unq y
578reflectBinderQuotePattern q ty unq (Hole t)
579 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
580 fill $ reflCall "Hole" [ty, Var t']
581 solve
582 focus t'; q unq t
583reflectBinderQuotePattern q ty unq (GHole _ t)
584 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
585 fill $ reflCall "GHole" [ty, Var t']
586 solve
587 focus t'; q unq t
588reflectBinderQuotePattern q ty unq (Guess x y)
589 = do x' <- claimTy (sMN 0 "ty") ty; movelast x'
590 y' <- claimTy (sMN 0 "v") ty; movelast y'
591 fill $ reflCall "Guess" [ty, Var x', Var y']
592 solve
593 focus x'; q unq x
594 focus y'; q unq y
595reflectBinderQuotePattern q ty unq (PVar t)
596 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
597 fill $ reflCall "PVar" [ty, Var t']
598 solve
599 focus t'; q unq t
600reflectBinderQuotePattern q ty unq (PVTy t)
601 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
602 fill $ reflCall "PVTy" [ty, Var t']
603 solve
604 focus t'; q unq t
606reflectUniverse :: Universe -> Raw
607reflectUniverse u =
608 (Var (reflm (case u of
609 NullType -> "NullType"
610 UniqueType -> "UniqueType"
611 AllTypes -> "AllTypes")))
613-- | Create a reflected TT term, but leave refs to the provided name intact
614reflectTTQuote :: [Name] -> Term -> Raw
615reflectTTQuote unq (P nt n t)
616 | n `elem` unq = Var n
617 | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
618reflectTTQuote unq (V n)
619 = reflCall "V" [RConstant (I n)]
620reflectTTQuote unq (Bind n b x)
621 = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]
622reflectTTQuote unq (App _ f x)
623 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
624reflectTTQuote unq (Constant c)
625 = reflCall "TConst" [reflectConstant c]
626reflectTTQuote unq (Proj t i)
627 = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
628reflectTTQuote unq (Erased) = Var (reflm "Erased")
629reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
630reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
631reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
633reflectRawQuote :: [Name] -> Raw -> Raw
634reflectRawQuote unq (Var n)
635 | n `elem` unq = Var n
636 | otherwise = reflCall "Var" [reflectName n]
637reflectRawQuote unq (RBind n b r) =
638 reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]
639reflectRawQuote unq (RApp f x) =
640 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
641reflectRawQuote unq RType = Var (reflm "RType")
642reflectRawQuote unq (RUType u) =
643 reflCall "RUType" [reflectUniverse u]
644reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
645reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
647reflectNameType :: NameType -> Raw
648reflectNameType (Bound) = Var (reflm "Bound")
649reflectNameType (Ref) = Var (reflm "Ref")
650reflectNameType (DCon x y _)
651 = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!
652reflectNameType (TCon x y)
653 = reflCall "TCon" [RConstant (I x), RConstant (I y)]
655reflectName :: Name -> Raw
656reflectName (UN s)
657 = reflCall "UN" [RConstant (Str (str s))]
658reflectName (NS n ns)
659 = reflCall "NS" [ reflectName n
660 , foldr (\ n s ->
661 raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
662 [ RConstant StrType, RConstant (Str n), s ])
663 ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
664 [ RConstant StrType ])
665 (map str ns)
666 ]
667reflectName (MN i n)
668 = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
669reflectName NErased = Var (reflm "NErased")
670reflectName (SN sn) = raw_apply (Var (reflm "SN")) [reflectSpecialName sn]
671reflectName (SymRef _) = error "The impossible happened: symbol table ref survived IBC loading"
673reflectSpecialName :: SpecialName -> Raw
674reflectSpecialName (WhereN i n1 n2) =
675 reflCall "WhereN" [RConstant (I i), reflectName n1, reflectName n2]
676reflectSpecialName (WithN i n) = reflCall "WithN" [ RConstant (I i)
677 , reflectName n
678 ]
679reflectSpecialName (InstanceN inst ss) =
680 reflCall "InstanceN" [ reflectName inst
681 , mkList (RConstant StrType) $
682 map (RConstant . Str . T.unpack) ss
683 ]
684reflectSpecialName (ParentN n s) =
685 reflCall "ParentN" [reflectName n, RConstant (Str (T.unpack s))]
686reflectSpecialName (MethodN n) =
687 reflCall "MethodN" [reflectName n]
688reflectSpecialName (CaseN n) =
689 reflCall "CaseN" [reflectName n]
690reflectSpecialName (ElimN n) =
691 reflCall "ElimN" [reflectName n]
692reflectSpecialName (InstanceCtorN n) =
693 reflCall "InstanceCtorN" [reflectName n]
694reflectSpecialName (MetaN parent meta) =
695 reflCall "MetaN" [reflectName parent, reflectName meta]
697-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
698-- MNs corresponding to will care about the string but not the number. All
699-- others become _.
700reflectNameQuotePattern :: Name -> ElabD ()
701reflectNameQuotePattern n@(UN s)
702 = do fill $ reflectName n
703 solve
704reflectNameQuotePattern n@(NS _ _)
705 = do fill $ reflectName n
706 solve
707reflectNameQuotePattern (MN _ n)
708 = do i <- getNameFrom (sMN 0 "mnCounter")
709 claim i (RConstant (AType (ATInt ITNative)))
710 movelast i
711 fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
712 solve
713reflectNameQuotePattern _ -- for all other names, match any
714 = do nameHole <- getNameFrom (sMN 0 "name")
715 claim nameHole (Var (reflm "TTName"))
716 movelast nameHole
717 fill (Var nameHole)
718 solve
720reflectBinder :: Binder Term -> Raw
721reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []
723reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
724reflectBinderQuote q ty unq (Lam t)
725 = reflCall "Lam" [Var ty, q unq t]
726reflectBinderQuote q ty unq (Pi _ t k)
727 = reflCall "Pi" [Var ty, q unq t, q unq k]
728reflectBinderQuote q ty unq (Let x y)
729 = reflCall "Let" [Var ty, q unq x, q unq y]
730reflectBinderQuote q ty unq (NLet x y)
731 = reflCall "NLet" [Var ty, q unq x, q unq y]
732reflectBinderQuote q ty unq (Hole t)
733 = reflCall "Hole" [Var ty, q unq t]
734reflectBinderQuote q ty unq (GHole _ t)
735 = reflCall "GHole" [Var ty, q unq t]
736reflectBinderQuote q ty unq (Guess x y)
737 = reflCall "Guess" [Var ty, q unq x, q unq y]
738reflectBinderQuote q ty unq (PVar t)
739 = reflCall "PVar" [Var ty, q unq t]
740reflectBinderQuote q ty unq (PVTy t)
741 = reflCall "PVTy" [Var ty, q unq t]
743mkList :: Raw -> [Raw] -> Raw
744mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
745mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
746 x)
747 (mkList ty xs)
749reflectConstant :: Const -> Raw
750reflectConstant c@(I _) = reflCall "I" [RConstant c]
751reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
752reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
753reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
754reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
755reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
756reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
757reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
758reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
759reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
760reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
761reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
762reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
763reflectConstant StrType = Var (reflm "StrType")
764reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
765reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
766reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
767reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
768reflectConstant VoidType = Var (reflm "VoidType")
769reflectConstant Forgot = Var (reflm "Forgot")
770reflectConstant WorldType = Var (reflm "WorldType")
771reflectConstant TheWorld = Var (reflm "TheWorld")
773reflectUExp :: UExp -> Raw
774reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
775reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
777-- | Reflect the environment of a proof into a List (TTName, Binder TT)
778reflectEnv :: Env -> Raw
779reflectEnv = foldr consToEnvList emptyEnvList
780 where
781 consToEnvList :: (Name, Binder Term) -> Raw -> Raw
782 consToEnvList (n, b) l
783 = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
784 [ envTupleType
785 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
786 , (RApp (Var $ reflm "Binder")
787 (Var $ reflm "TT"))
788 , reflectName n
789 , reflectBinder b
790 ]
791 , l
792 ]
794 emptyEnvList :: Raw
795 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
796 [envTupleType]
798-- | Reflect an error into the internal datatype of Idris -- TODO
799rawBool :: Bool -> Raw
800rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
801rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
803rawNil :: Raw -> Raw
804rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
806rawCons :: Raw -> Raw -> Raw -> Raw
807rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
809rawList :: Raw -> [Raw] -> Raw
810rawList ty = foldr (rawCons ty) (rawNil ty)
812rawPairTy :: Raw -> Raw -> Raw
813rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
815rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
816rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
818-- | Idris tuples nest to the right
819rawTripleTy :: Raw -> Raw -> Raw -> Raw
820rawTripleTy a b c = rawPairTy a (rawPairTy b c)
822rawTriple :: (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw
823rawTriple (a, b, c) (x, y, z) = rawPair (a, rawPairTy b c) (x, rawPair (b, c) (y, z))
825reflectCtxt :: [(Name, Type)] -> Raw
826reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
827 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
828 (reflectName n, reflect t)))
829 ctxt)
831reflectErr :: Err -> Raw
832reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
833reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
834reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =
835 raw_apply (Var $ reflErrName "CantUnify")
836 [ rawBool b
837 , reflect t1
838 , reflect t2
839 , reflectErr e
840 , reflectCtxt ctxt
841 , RConstant (I i)]
842reflectErr (InfiniteUnify n tm ctxt) =
843 raw_apply (Var $ reflErrName "InfiniteUnify")
844 [ reflectName n
845 , reflect tm
846 , reflectCtxt ctxt
847 ]
848reflectErr (CantConvert t t' ctxt) =
849 raw_apply (Var $ reflErrName "CantConvert")
850 [ reflect t
851 , reflect t'
852 , reflectCtxt ctxt
853 ]
854reflectErr (CantSolveGoal t ctxt) =
855 raw_apply (Var $ reflErrName "CantSolveGoal")
856 [ reflect t
857 , reflectCtxt ctxt
858 ]
859reflectErr (UnifyScope n n' t ctxt) =
860 raw_apply (Var $ reflErrName "UnifyScope")
861 [ reflectName n
862 , reflectName n'
863 , reflect t
864 , reflectCtxt ctxt
865 ]
866reflectErr (CantInferType str) =
867 raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
868reflectErr (NonFunctionType t t') =
869 raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
870reflectErr (NotEquality t t') =
871 raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
872reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
873reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
874reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
875reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
876reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
877reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
878reflectErr (NotInjective t1 t2 t3) =
879 raw_apply (Var $ reflErrName "NotInjective")
880 [ reflect t1
881 , reflect t2
882 , reflect t3
883 ]
884reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
885reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
886reflectErr (CantResolveAlts ss) =
887 raw_apply (Var $ reflErrName "CantResolveAlts")
888 [rawList (Var $ reflm "TTName") (map reflectName ss)]
889reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
890reflectErr (NoEliminator str t)
891 = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),
892 reflect t]
893reflectErr (UniverseError fc ue old new tys) =
894 -- NB: loses information, but OK because this is not likely to be rewritten
895 Var $ reflErrName "UniverseError"
896reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
897reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
898reflectErr (UnknownImplicit n f) = raw_apply (Var $ reflErrName "UnknownImplicit") [reflectName n, reflectName f]
899reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
900reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
901reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
902reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
903reflectErr (ProviderError str) =
904 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
905reflectErr (LoadingFailed str err) =
906 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
907reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
909-- | Reflect a file context
910reflectFC :: FC -> Raw
911reflectFC fc = raw_apply (Var (reflm "FileLoc"))
912 [ RConstant (Str (fc_fname fc))
913 , raw_apply (Var pairCon) $
914 [intTy, intTy] ++
915 map (RConstant . I)
916 [ fst (fc_start fc)
917 , snd (fc_start fc)
918 ]
919 , raw_apply (Var pairCon) $
920 [intTy, intTy] ++
921 map (RConstant . I)
922 [ fst (fc_end fc)
923 , snd (fc_end fc)
924 ]
925 ]
926 where intTy = RConstant (AType (ATInt ITNative))
928fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
929fromTTMaybe (App _ (App _ (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
930 | just == txt "Just" = Just tm
931fromTTMaybe x = Nothing
933reflErrName :: String -> Name
934reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
936-- | Attempt to reify a report part from TT to the internal
937-- representation. Not in Idris or ElabD monads because it should be usable
938-- from either.
939reifyReportPart :: Term -> Either Err ErrorReportPart
940reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
941 Right (TextPart msg)
942reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
943 | n == reflm "NamePart" =
944 case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext emptyContext Erased) of
945 Error e -> Left . InternalMsg $
946 "could not reify name term " ++
947 show ttn ++
948 " when reflecting an error:" ++ show e
949 OK (n', _)-> Right $ NamePart n'
950reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
951 | n == reflm "TermPart" =
952 case runElab initEState (reifyTT tm) (initElaborator NErased initContext emptyContext Erased) of
953 Error e -> Left . InternalMsg $
954 "could not reify reflected term " ++
955 show tm ++
956 " when reflecting an error:" ++ show e
957 OK (tm', _) -> Right $ TermPart tm'
958reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
959 | n == reflm "RawPart" =
960 case runElab initEState (reifyRaw tm) (initElaborator NErased initContext emptyContext Erased) of
961 Error e -> Left . InternalMsg $
962 "could not reify reflected raw term " ++
963 show tm ++
964 " when reflecting an error: " ++ show e
965 OK (tm', _) -> Right $ RawPart tm'
966reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
967 | n == reflm "SubReport" =
968 case unList tm of
969 Just xs -> do subParts <- mapM reifyReportPart xs
970 Right (SubReport subParts)
971 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
972reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
974reifyErasure :: Term -> ElabD RErasure
975reifyErasure (P (DCon _ _ _) n _)
976 | n == tacN "Erased" = return RErased
977 | n == tacN "NotErased" = return RNotErased
978reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."
980reifyTyDecl :: Term -> ElabD RTyDecl
981reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
982 | n == tacN "Declare" =
983 do tyN' <- reifyTTName tyN
984 args' <- case unList args of
985 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
986 Just xs -> mapM reifyRArg xs
987 ret' <- reifyRaw ret
988 return $ RDeclare tyN' args' ret'
989 where reifyRArg :: Term -> ElabD RArg
990 reifyRArg (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argE) argTy)
991 | n == tacN "Explicit" = liftM3 RExplicit
992 (reifyTTName argN)
993 (reifyErasure argE)
994 (reifyRaw argTy)
995 | n == tacN "Implicit" = liftM3 RImplicit
996 (reifyTTName argN)
997 (reifyErasure argE)
998 (reifyRaw argTy) | n == tacN "Constraint" = liftM3 RConstraint
999 (reifyTTName argN)
1000 (reifyErasure argE)
1001 (reifyRaw argTy)
1002 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
1003reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
1005reifyFunDefn :: Term -> ElabD RFunDefn
1006reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)
1007 | n == tacN "DefineFun" =
1008 do fnN' <- reifyTTName fnN
1009 clauses' <- case unList clauses of
1010 Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
1011 Just cs -> mapM reifyC cs
1012 return $ RDefineFun fnN' clauses'
1013 where reifyC :: Term -> ElabD RFunClause
1014 reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)
1015 | n == tacN "MkFunClause" = liftM2 RMkFunClause
1016 (reifyRaw lhs)
1017 (reifyRaw rhs)
1018 reifyC (App _ (P (DCon _ _ _) n _) lhs)
1019 | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs
1020 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
1021reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
1023envTupleType :: Raw
1024envTupleType
1025 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
1026 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
1029-- | Apply Idris's implicit info to get a signature. The [PArg] should
1030-- come from a lookup in idris_implicits on IState.
1031getArgs :: [PArg] -> Raw -> ([RArg], Raw)
1032getArgs [] r = ([], r)
1033getArgs (a:as) (RBind n (Pi _ ty _) sc) =
1034 let (args, res) = getArgs as sc
1035 erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased
1036 arg' = case a of
1037 PImp {} -> RImplicit n erased ty
1038 PExp {} -> RExplicit n erased ty
1039 PConstraint {} -> RConstraint n erased ty
1040 PTacImplicit {} -> RImplicit n erased ty -- TODO?
1041 in (arg':args, res)
1042getArgs _ r = ([], r)
1044-- | Build the reflected datatype definition(s) that correspond(s) to
1045-- a provided unqualified name
1046buildDatatypes :: IState -> Name -> [RDatatype]
1047buildDatatypes ist n =
1048 catMaybes [ mkDataType dn ti
1049 | (dn, ti) <- lookupCtxtName n datatypes
1051 where datatypes = idris_datatypes ist
1052 ctxt = tt_ctxt ist
1053 impls = idris_implicits ist
1055 ctorSig cn = do cty <- fmap forget (lookupTyExact cn ctxt)
1056 argInfo <- lookupCtxtExact cn impls
1057 let (args, res) = getArgs argInfo cty
1058 return (cn, args, res)
1060 mkDataType name (TI {param_pos = params, con_names = constrs}) =
1061 do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
1062 implInfo <- lookupCtxtExact name impls
1063 let (tcargs, tcres) = getTCArgs params implInfo (forget ty) 0
1064 ctors <- mapM ctorSig constrs
1065 return $ RDatatype name tcargs tcres ctors
1067 getTCArgs params implInfo (RBind an (Pi _ ty _) body) i =
1068 let (erased, implInfo') = case implInfo of
1069 [] -> (RNotErased, [])
1070 (a:as) -> (if InaccessibleArg `elem` argopts a
1071 then RErased
1072 else RNotErased,
1073 as)
1074 (args, res) = getTCArgs params implInfo' body (i+1)
1075 in if i `elem` params
1076 then (RParameter an erased ty : args, res )
1077 else (RIndex an erased ty : args, res)
1078 getTCArgs _ implInfo tm _ = ([], tm)
1080reflectErasure :: RErasure -> Raw
1081reflectErasure RErased = Var (tacN "Erased")
1082reflectErasure RNotErased = Var (tacN "NotErased")
1084reflectArg :: RArg -> Raw
1085reflectArg arg =
1086 RApp (RApp (RApp (Var con) (reflectName $ argName arg))
1087 (reflectErasure $ argErased arg))
1088 (reflectRaw $ argTy arg)
1089 where con = case arg of
1090 RExplicit{} -> tacN "Explicit"
1091 RImplicit{} -> tacN "Implicit"
1092 RConstraint{} -> tacN "Constraint"
1094reflectDatatype :: RDatatype -> Raw
1095reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
1096 raw_apply (Var $ tacN "MkDatatype") [ reflectName tyn
1097 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
1098 , reflectRaw tyConRes
1099 , rawList (rawTripleTy (Var $ reflm "TTName")
1100 (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg"))
1101 (Var $ reflm "Raw"))
1102 [ rawTriple ((Var $ reflm "TTName"),
1103 (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg")),
1104 (Var $ reflm "Raw"))
1105 (reflectName cn,
1106 rawList (Var $ tacN "Arg") (map reflectArg cargs),
1107 reflectRaw cty)
1108 | (cn, cargs, cty) <- constrs
1111 where reflectConArg (RParameter n e t) =
1112 raw_apply (Var $ tacN "Parameter") [reflectName n, reflectErasure e, reflectRaw t]
1113 reflectConArg (RIndex n e t) =
1114 raw_apply (Var $ tacN "Index") [reflectName n, reflectErasure e, reflectRaw t]