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