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