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