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