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