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