git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Reflection.hs
1230 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.
5License : BSD3
6Maintainer : The Idris Community.
7-}
9{-# LANGUAGE CPP, PatternGuards #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
11module Idris.Reflection (RConstructorDefn(..), RDataDefn(..),RFunArg(..),
12 RFunClause(..), RFunDefn(..), RTyDecl(..),
13 buildDatatypes, buildFunDefns, envTupleType, fromTTMaybe,
14 getArgs, mkList, rawList, rawPair, rawPairTy, reflect,
15 reflectArg, reflectDatatype, reflectEnv, reflectErr,
16 reflectFC, reflectFixity, reflectFunDefn, reflectList,
17 reflectName, reflectNameType, reflectRaw,
18 reflectRawQuotePattern, reflectRawQuote, reflectTTQuote,
19 reflectTTQuotePattern, reflm, reify, reifyBool, reifyEnv,
20 reifyFunDefn, reifyList, reifyRDataDefn, reifyRaw,
21 reifyReportPart, reifyReportParts, reifyTT, reifyTTName,
22 reifyTyDecl, rFunArgToPArg, tacN
23 ) where
25import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
26 movelast, runElab, solve)
27import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact,
28 lookupTyExact)
29import Idris.Core.TT
31import Idris.AbsSyntaxTree (ArgOpt(..), ElabD, Fixity(..), IState(idris_datatypes, idris_implicits, idris_patdefs, tt_ctxt),
32 PArg, PArg'(..), PTactic, PTactic'(..), PTerm(..),
33 initEState, pairCon, pairTy)
34import Idris.Delaborate (delab)
36import Control.Monad (liftM, liftM2, liftM4)
37import Control.Monad.State.Strict (lift)
38import Data.List (findIndex, (\\))
39import Data.Maybe (catMaybes)
40import qualified Data.Text as T
42data RErasure = RErased | RNotErased deriving Show
44data RPlicity = RExplicit | RImplicit | RConstraint deriving Show
46data RFunArg = RFunArg { argName :: Name
47 , argTy :: Raw
48 , argPlicity :: RPlicity
49 , erasure :: RErasure
50 }
51 deriving Show
53data RTyDecl = RDeclare Name [RFunArg] Raw deriving Show
55data RTyConArg = RParameter RFunArg
56 | RIndex RFunArg
57 deriving Show
59data RCtorArg = RCtorParameter RFunArg | RCtorField RFunArg deriving Show
61data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RCtorArg], Raw)] deriving Show
63data RConstructorDefn = RConstructor Name [RFunArg] Raw
65data RDataDefn = RDefineDatatype Name [RConstructorDefn]
67rArgOpts :: RErasure -> [ArgOpt]
68rArgOpts RErased = [InaccessibleArg]
69rArgOpts _ = []
71rFunArgToPArg :: RFunArg -> PArg
72rFunArgToPArg (RFunArg n _ RExplicit e) = PExp 0 (rArgOpts e) n Placeholder
73rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder
74rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder
76data RFunClause a = RMkFunClause a a
77 | RMkImpossibleClause a
78 deriving Show
80data RFunDefn a = RDefineFun Name [RFunClause a] deriving Show
82-- | Prefix a name with the "Language.Reflection" namespace
83reflm :: String -> Name
84reflm n = sNS (sUN n) ["Reflection", "Language"]
86-- | Prefix a name with the "Language.Reflection.Elab" namespace
87tacN :: String -> Name
88tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]
90-- | Reify tactics from their reflected representation
91reify :: IState -> Term -> ElabD PTactic
92reify _ (P _ n _) | n == reflm "Intros" = return Intros
93reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
94reify _ (P _ n _) | n == reflm "Implementation" = return TCImplementation
95reify _ (P _ n _) | n == reflm "Solve" = return Solve
96reify _ (P _ n _) | n == reflm "Compute" = return Compute
97reify _ (P _ n _) | n == reflm "Skip" = return Skip
98reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
99reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
100reify ist t@(App _ _ _)
101 | (P _ f _, args) <- unApply t = reifyApp ist f args
102reify _ t = fail ("Unknown tactic " ++ show t)
104reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
105reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
106reifyApp _ t [Constant (I i)]
107 | t == reflm "Search" = return (ProofSearch True True i Nothing [] [])
108reifyApp _ t [x]
109 | t == reflm "Refine" = do n <- reifyTTName x
110 return $ Refine n []
111reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
112 goal <- reifyTT ty
113 return $ Claim n' (delab ist goal)
114reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
115reifyApp ist t [Constant (Str n), x]
116 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
117reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
118reifyApp ist t [t']
119 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
120reifyApp ist t [t']
121 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
122reifyApp ist t [t']
123 | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
124reifyApp _ t [t']
125 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
126reifyApp ist t [t']
127 | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
128reifyApp ist t [x]
129 | t == reflm "Focus" = liftM Focus (reifyTTName x)
130reifyApp ist t [t']
131 | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
132reifyApp ist t [n, t']
133 | t == reflm "LetTac" = do n' <- reifyTTName n
134 t'' <- reifyTT t'
135 return $ LetTac n' (delab ist t')
136reifyApp ist t [n, tt', t']
137 | t == reflm "LetTacTy" = do n' <- reifyTTName n
138 tt'' <- reifyTT tt'
139 t'' <- reifyTT t'
140 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
141reifyApp ist t [errs]
142 | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
143reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
145reifyBool :: Term -> ElabD Bool
146reifyBool (P _ n _) | n == sNS (sUN "True") ["Bool", "Prelude"] = return True
147 | n == sNS (sUN "False") ["Bool", "Prelude"] = return False
148reifyBool tm = fail $ "Not a Boolean: " ++ show tm
150reifyInt :: Term -> ElabD Int
151reifyInt (Constant (I i)) = return i
152reifyInt tm = fail $ "Not an Int: " ++ show tm
154reifyPair :: (Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
155reifyPair left right (App _ (App _ (App _ (App _ (P _ n _) _) _) x) y)
156 | n == pairCon = liftM2 (,) (left x) (right y)
157reifyPair left right tm = fail $ "Not a pair: " ++ show tm
159reifyList :: (Term -> ElabD a) -> Term -> ElabD [a]
160reifyList getElt lst =
161 case unList lst of
162 Nothing -> fail "Couldn't reify a list"
163 Just xs -> mapM getElt xs
165reifyReportParts :: Term -> ElabD [ErrorReportPart]
166reifyReportParts errs =
167 case unList errs of
168 Nothing -> fail "Failed to reify errors"
169 Just errs' ->
170 let parts = mapM reifyReportPart errs' in
171 case parts of
172 Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
173 Right errs'' ->
174 return errs''
176-- | Reify terms from their reflected representation
177reifyTT :: Term -> ElabD Term
178reifyTT t@(App _ _ _)
179 | (P _ f _, args) <- unApply t = reifyTTApp f args
180reifyTT t@(P _ n _)
181 | n == reflm "Erased" = return Erased
182reifyTT t@(P _ n _)
183 | n == reflm "Impossible" = return Impossible
184reifyTT t = fail ("Unknown reflection term: " ++ show t)
186reifyTTApp :: Name -> [Term] -> ElabD Term
187reifyTTApp t [nt, n, x]
188 | t == reflm "P" = do nt' <- reifyTTNameType nt
189 n' <- reifyTTName n
190 x' <- reifyTT x
191 return $ P nt' n' x'
192reifyTTApp t [Constant (I i)]
193 | t == reflm "V" = return $ V i
194reifyTTApp t [n, b, x]
195 | t == reflm "Bind" = do n' <- reifyTTName n
196 b' <- reifyTTBinder reifyTT (reflm "TT") b
197 x' <- reifyTT x
198 return $ Bind n' b' x'
199reifyTTApp t [f, x]
200 | t == reflm "App" = do f' <- reifyTT f
201 x' <- reifyTT x
202 return $ App Complete f' x'
203reifyTTApp t [c]
204 | t == reflm "TConst" = liftM Constant (reifyTTConst c)
205reifyTTApp t [t', Constant (I i)]
206 | t == reflm "Proj" = do t'' <- reifyTT t'
207 return $ Proj t'' i
208reifyTTApp t [tt]
209 | t == reflm "TType" = liftM TType (reifyTTUExp tt)
210reifyTTApp t [tt]
211 | t == reflm "UType" = liftM UType (reifyUniverse tt)
212reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
214reifyUniverse :: Term -> ElabD Universe
215reifyUniverse (P _ n _) | n == reflm "AllTypes" = return AllTypes
216 | n == reflm "UniqueType" = return UniqueType
217 | n == reflm "NullType" = return NullType
218reifyUniverse tm = fail ("Unknown reflection universe: " ++ show tm)
220-- | Reify raw terms from their reflected representation
221reifyRaw :: Term -> ElabD Raw
222reifyRaw t@(App _ _ _)
223 | (P _ f _, args) <- unApply t = reifyRawApp f args
224reifyRaw t@(P _ n _)
225 | n == reflm "RType" = return RType
226reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)
228reifyRawApp :: Name -> [Term] -> ElabD Raw
229reifyRawApp t [n]
230 | t == reflm "Var" = liftM Var (reifyTTName n)
231reifyRawApp t [n, b, x]
232 | t == reflm "RBind" = do n' <- reifyTTName n
233 b' <- reifyTTBinder reifyRaw (reflm "Raw") b
234 x' <- reifyRaw x
235 return $ RBind n' b' x'
236reifyRawApp t [f, x]
237 | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
238reifyRawApp t [c]
239 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
240reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
242reifyTTName :: Term -> ElabD Name
243reifyTTName t
244 | (P _ f _, args) <- unApply t = reifyTTNameApp f args
245reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
247reifyTTNameApp :: Name -> [Term] -> ElabD Name
248reifyTTNameApp t [Constant (Str n)]
249 | t == reflm "UN" = return $ sUN n
250reifyTTNameApp t [n, ns]
251 | t == reflm "NS" = do n' <- reifyTTName n
252 ns' <- reifyTTNamespace ns
253 return $ sNS n' ns'
254reifyTTNameApp t [Constant (I i), Constant (Str n)]
255 | t == reflm "MN" = return $ sMN i n
256reifyTTNameApp t [sn]
257 | t == reflm "SN"
258 , (P _ f _, args) <- unApply sn = SN <$> reifySN f args
259 where reifySN :: Name -> [Term] -> ElabD SpecialName
260 reifySN t [Constant (I i), n1, n2]
261 | t == reflm "WhereN" = WhereN i <$> reifyTTName n1 <*> reifyTTName n2
262 reifySN t [Constant (I i), n]
263 | t == reflm "WithN" = WithN i <$> reifyTTName n
264 reifySN t [n, ss]
265 | t == reflm "ImplementationN" =
266 case unList ss of
267 Nothing -> fail "Can't reify ImplementationN strings"
268 Just ss' -> ImplementationN <$> reifyTTName n <*>
269 pure [T.pack s | Constant (Str s) <- ss']
270 reifySN t [n, Constant (Str s)]
271 | t == reflm "ParentN" =
272 ParentN <$> reifyTTName n <*> pure (T.pack s)
273 reifySN t [n]
274 | t == reflm "MethodN" =
275 MethodN <$> reifyTTName n
276 reifySN t [fc, n]
277 | t == reflm "CaseN" =
278 CaseN <$> (FC' <$> reifyFC fc) <*> reifyTTName n
279 reifySN t [n]
280 | t == reflm "ImplementationCtorN" =
281 ImplementationCtorN <$> reifyTTName n
282 reifySN t [n1, n2]
283 | t == reflm "MetaN" =
284 MetaN <$> reifyTTName n1 <*> reifyTTName n2
285 reifySN t args = fail $ "Can't reify special name " ++ show t ++ show args
286reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
288reifyTTNamespace :: Term -> ElabD [String]
289reifyTTNamespace t@(App _ _ _)
290 = case unApply t of
291 (P _ f _, [Constant StrType])
292 | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
293 (P _ f _, [Constant StrType, Constant (Str n), ns])
294 | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
295 _ -> fail ("Unknown reflection namespace arg: " ++ show t)
296reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
298reifyTTNameType :: Term -> ElabD NameType
299reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
300reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
301reifyTTNameType t@(App _ _ _)
302 = case unApply t of
303 (P _ f _, [Constant (I tag), Constant (I num)])
304 | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!
305 | f == reflm "TCon" -> return $ TCon tag num
306 _ -> fail ("Unknown reflection name type: " ++ show t)
307reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
309reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
310reifyTTBinder reificator binderType t@(App _ _ _)
311 = case unApply t of
312 (P _ f _, bt:args) | forget bt == Var binderType
313 -> reifyTTBinderApp reificator f args
314 _ -> fail ("Mismatching binder reflection: " ++ show t)
315reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
317reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
318reifyTTBinderApp reif f [t]
319 | f == reflm "Lam" = liftM (Lam RigW) (reif t)
320reifyTTBinderApp reif f [t, k]
321 | f == reflm "Pi" = liftM2 (Pi RigW Nothing) (reif t) (reif k)
322reifyTTBinderApp reif f [x, y]
323 | f == reflm "Let" = liftM2 (Let RigW) (reif x) (reif y)
324reifyTTBinderApp reif f [t]
325 | f == reflm "Hole" = liftM Hole (reif t)
326reifyTTBinderApp reif f [t]
327 | f == reflm "GHole" = liftM (GHole 0 []) (reif t)
328reifyTTBinderApp reif f [x, y]
329 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
330reifyTTBinderApp reif f [t]
331 | f == reflm "PVar" = liftM (PVar RigW) (reif t)
332reifyTTBinderApp reif f [t]
333 | f == reflm "PVTy" = liftM PVTy (reif t)
334reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
336reifyTTConst :: Term -> ElabD Const
337reifyTTConst (P _ n _) | n == reflm "StrType" = return StrType
338reifyTTConst (P _ n _) | n == reflm "VoidType" = return VoidType
339reifyTTConst (P _ n _) | n == reflm "Forgot" = return Forgot
340reifyTTConst t@(App _ _ _)
341 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
342reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
344reifyTTConstApp :: Name -> Term -> ElabD Const
345reifyTTConstApp f aty
346 | f == reflm "AType" = fmap AType (reifyArithTy aty)
347reifyTTConstApp f (Constant c@(I _))
348 | f == reflm "I" = return c
349reifyTTConstApp f (Constant c@(BI _))
350 | f == reflm "BI" = return c
351reifyTTConstApp f (Constant c@(Fl _))
352 | f == reflm "Fl" = return c
353reifyTTConstApp f (Constant c@(Ch _))
354 | f == reflm "Ch" = return c
355reifyTTConstApp f (Constant c@(Str _))
356 | f == reflm "Str" = return c
357reifyTTConstApp f (Constant c@(B8 _))
358 | f == reflm "B8" = return c
359reifyTTConstApp f (Constant c@(B16 _))
360 | f == reflm "B16" = return c
361reifyTTConstApp f (Constant c@(B32 _))
362 | f == reflm "B32" = return c
363reifyTTConstApp f (Constant c@(B64 _))
364 | f == reflm "B64" = return c
365reifyTTConstApp f v@(P _ _ _) =
366 lift . tfail . Msg $
367 "Can't reify the variable " ++
368 show v ++
369 " as a constant, because its value is not statically known."
370reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
372reifyArithTy :: Term -> ElabD ArithTy
373reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
374reifyArithTy (P _ n _) | n == reflm "ATDouble" = return ATFloat
375reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
377reifyNativeTy :: Term -> ElabD NativeTy
378reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
379reifyNativeTy (P _ n _) | n == reflm "IT16" = return IT16
380reifyNativeTy (P _ n _) | n == reflm "IT32" = return IT32
381reifyNativeTy (P _ n _) | n == reflm "IT64" = return IT64
382reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
384reifyIntTy :: Term -> ElabD IntTy
385reifyIntTy (App _ (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
386reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
387reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
388reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
389reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
391reifyTTUExp :: Term -> ElabD UExp
392reifyTTUExp t@(App _ _ _)
393 = case unApply t of
394 (P _ f _, [Constant (Str str), Constant (I i)])
395 | f == reflm "UVar" -> return $ UVar str i
396 (P _ f _, [Constant (I i)])
397 | f == reflm "UVal" -> return $ UVal i
398 _ -> fail ("Unknown reflection type universe expression: " ++ show t)
399reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
401-- | Create a reflected call to a named function/constructor
402reflCall :: String -> [Raw] -> Raw
403reflCall funName args
404 = raw_apply (Var (reflm funName)) args
406-- | Lift a term into its Language.Reflection.TT representation
407reflect :: Term -> Raw
408reflect = reflectTTQuote []
410-- | Lift a term into its Language.Reflection.Raw representation
411reflectRaw :: Raw -> Raw
412reflectRaw = reflectRawQuote []
414claimTy :: Name -> Raw -> ElabD Name
415claimTy n ty = do n' <- getNameFrom n
416 claim n' ty
417 return n'
419intToReflectedNat :: Int -> Raw
420intToReflectedNat i = if i <= 0
421 then Var (natN "Z")
422 else RApp (Var (natN "S")) (intToReflectedNat (i - 1))
423 where natN :: String -> Name
424 natN n = sNS (sUN n) ["Nat", "Prelude"]
426reflectFixity :: Fixity -> Raw
427reflectFixity (Infixl p) = RApp (Var (tacN "Infixl")) (intToReflectedNat p)
428reflectFixity (Infixr p) = RApp (Var (tacN "Infixr")) (intToReflectedNat p)
429reflectFixity (InfixN p) = RApp (Var (tacN "InfixN")) (intToReflectedNat p)
430reflectFixity (PrefixN p) = RApp (Var (tacN "PrefixN")) (intToReflectedNat p)
432-- | Convert a reflected term to a more suitable form for pattern-matching.
433-- In particular, the less-interesting bits are elaborated to _ patterns. This
434-- happens to NameTypes, universe levels, names that are bound but not used,
435-- and the type annotation field of the P constructor.
436reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
437reflectTTQuotePattern unq (P _ n _)
438 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
439 do fill (Var n) ; solve
440 | otherwise =
441 do tyannot <- claimTy (sMN 0 "pTyAnnot") (Var (reflm "TT"))
442 movelast tyannot -- use a _ pattern here
443 nt <- getNameFrom (sMN 0 "nt")
444 claim nt (Var (reflm "NameType"))
445 movelast nt -- use a _ pattern here
446 n' <- getNameFrom (sMN 0 "n")
447 claim n' (Var (reflm "TTName"))
448 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
449 solve
450 focus n'; reflectNameQuotePattern n
451reflectTTQuotePattern unq (V n)
452 = do fill $ reflCall "V" [RConstant (I n)]
453 solve
454reflectTTQuotePattern unq (Bind n b x)
455 = do x' <- claimTy (sMN 0 "sc") (Var (reflm "TT"))
456 movelast x'
457 b' <- getNameFrom (sMN 0 "binder")
458 claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
459 (Var (sNS (sUN "TT") ["Reflection", "Language"])))
460 if n `elem` freeNames x
461 then do fill $ reflCall "Bind"
462 [reflectName n,
463 Var b',
464 Var x']
465 solve
466 else do any <- getNameFrom (sMN 0 "anyName")
467 claim any (Var (reflm "TTName"))
468 movelast any
469 fill $ reflCall "Bind"
470 [Var any,
471 Var b',
472 Var x']
473 solve
474 focus x'; reflectTTQuotePattern unq x
475 focus b'; reflectBinderQuotePattern reflectTTQuotePattern (Var $ reflm "TT") unq b
476reflectTTQuotePattern unq (App _ f x)
477 = do f' <- claimTy (sMN 0 "f") (Var (reflm "TT")) ; movelast f'
478 x' <- claimTy (sMN 0 "x") (Var (reflm "TT")) ; movelast x'
479 fill $ reflCall "App" [Var f', Var x']
480 solve
481 focus f'; reflectTTQuotePattern unq f
482 focus x'; reflectTTQuotePattern unq x
483reflectTTQuotePattern unq (Constant c)
484 = do fill $ reflCall "TConst" [reflectConstant c]
485 solve
486reflectTTQuotePattern unq (Proj t i)
487 = lift . tfail . InternalMsg $
488 "Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."
489reflectTTQuotePattern unq Erased
490 = do erased <- claimTy (sMN 0 "erased") (Var (reflm "TT"))
491 movelast erased
492 fill (Var erased)
493reflectTTQuotePattern unq Impossible
494 = lift . tfail . InternalMsg $
495 "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."
496reflectTTQuotePattern unq (Inferred t)
497 = lift . tfail . InternalMsg $
498 "Phase error! The Inferred constructor is for coverage checking only and should not have been reflected during elaboration."
499reflectTTQuotePattern unq (TType exp)
500 = do ue <- getNameFrom (sMN 0 "uexp")
501 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
502 movelast ue
503 fill $ reflCall "TType" [Var ue]
504 solve
505reflectTTQuotePattern unq (UType u)
506 = do uH <- getNameFrom (sMN 0 "someUniv")
507 claim uH (Var (reflm "Universe"))
508 movelast uH
509 fill $ reflCall "UType" [Var uH]
510 solve
511 focus uH
512 fill (Var (reflm (case u of
513 NullType -> "NullType"
514 UniqueType -> "UniqueType"
515 AllTypes -> "AllTypes")))
516 solve
518reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
519reflectRawQuotePattern unq (Var n)
520 -- the unquoted names already have types, just use them
521 | n `elem` unq = do fill (Var n); solve
522 | otherwise = do fill (reflCall "Var" [reflectName n]); solve
523reflectRawQuotePattern unq (RBind n b sc) =
524 do scH <- getNameFrom (sMN 0 "sc")
525 claim scH (Var (reflm "Raw"))
526 movelast scH
527 bH <- getNameFrom (sMN 0 "binder")
528 claim bH (RApp (Var (reflm "Binder"))
529 (Var (reflm "Raw")))
530 if n `elem` freeNamesR sc
531 then do fill $ reflCall "RBind" [reflectName n,
532 Var bH,
533 Var scH]
534 solve
535 else do any <- getNameFrom (sMN 0 "anyName")
536 claim any (Var (reflm "TTName"))
537 movelast any
538 fill $ reflCall "RBind" [Var any, Var bH, Var scH]
539 solve
540 focus scH; reflectRawQuotePattern unq sc
541 focus bH; reflectBinderQuotePattern reflectRawQuotePattern (Var $ reflm "Raw") unq b
542 where freeNamesR (Var n) = [n]
543 freeNamesR (RBind n (Let rc t v) body) = concat [freeNamesR v,
544 freeNamesR body \\ [n],
545 freeNamesR t]
546 freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
547 (freeNamesR body \\ [n])
548 freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
549 freeNamesR RType = []
550 freeNamesR (RUType _) = []
551 freeNamesR (RConstant _) = []
552reflectRawQuotePattern unq (RApp f x) =
553 do fH <- getNameFrom (sMN 0 "f")
554 claim fH (Var (reflm "Raw"))
555 movelast fH
556 xH <- getNameFrom (sMN 0 "x")
557 claim xH (Var (reflm "Raw"))
558 movelast xH
559 fill $ reflCall "RApp" [Var fH, Var xH]
560 solve
561 focus fH; reflectRawQuotePattern unq f
562 focus xH; reflectRawQuotePattern unq x
563reflectRawQuotePattern unq RType =
564 do fill (Var (reflm "RType"))
565 solve
566reflectRawQuotePattern unq (RUType univ) =
567 do uH <- getNameFrom (sMN 0 "universe")
568 claim uH (Var (reflm "Universe"))
569 movelast uH
570 fill $ reflCall "RUType" [Var uH]
571 solve
572 focus uH; fill (reflectUniverse univ); solve
573reflectRawQuotePattern unq (RConstant c) =
574 do cH <- getNameFrom (sMN 0 "const")
575 claim cH (Var (reflm "Constant"))
576 movelast cH
577 fill (reflCall "RConstant" [Var cH]); solve
578 focus cH
579 fill (reflectConstant c); solve
581reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()
582reflectBinderQuotePattern q ty unq (Lam _ t)
583 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
584 fill $ reflCall "Lam" [ty, Var t']
585 solve
586 focus t'; q unq t
587reflectBinderQuotePattern q ty unq (Pi _ _ t k)
588 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
589 k' <- claimTy (sMN 0 "k") ty; movelast k';
590 fill $ reflCall "Pi" [ty, Var t', Var k']
591 solve
592 focus t'; q unq t
593reflectBinderQuotePattern q ty unq (Let rc 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 (NLet x y)
601 = do x' <- claimTy (sMN 0 "ty") ty; movelast x'
602 y' <- claimTy (sMN 0 "v") ty; movelast y'
603 fill $ reflCall "Let" [ty, Var x', Var y']
604 solve
605 focus x'; q unq x
606 focus y'; q unq y
607reflectBinderQuotePattern q ty unq (Hole t)
608 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
609 fill $ reflCall "Hole" [ty, Var t']
610 solve
611 focus t'; q unq t
612reflectBinderQuotePattern q ty unq (GHole _ _ t)
613 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
614 fill $ reflCall "GHole" [ty, Var t']
615 solve
616 focus t'; q unq t
617reflectBinderQuotePattern q ty unq (Guess x y)
618 = do x' <- claimTy (sMN 0 "ty") ty; movelast x'
619 y' <- claimTy (sMN 0 "v") ty; movelast y'
620 fill $ reflCall "Guess" [ty, Var x', Var y']
621 solve
622 focus x'; q unq x
623 focus y'; q unq y
624reflectBinderQuotePattern q ty unq (PVar _ t)
625 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
626 fill $ reflCall "PVar" [ty, Var t']
627 solve
628 focus t'; q unq t
629reflectBinderQuotePattern q ty unq (PVTy t)
630 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
631 fill $ reflCall "PVTy" [ty, Var t']
632 solve
633 focus t'; q unq t
635reflectUniverse :: Universe -> Raw
636reflectUniverse u =
637 (Var (reflm (case u of
638 NullType -> "NullType"
639 UniqueType -> "UniqueType"
640 AllTypes -> "AllTypes")))
642-- | Create a reflected TT term, but leave refs to the provided name intact
643reflectTTQuote :: [Name] -> Term -> Raw
644reflectTTQuote unq (P nt n t)
645 | n `elem` unq = Var n
646 | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
647reflectTTQuote unq (V n)
648 = reflCall "V" [RConstant (I n)]
649reflectTTQuote unq (Bind n b x)
650 = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]
651reflectTTQuote unq (App _ f x)
652 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
653reflectTTQuote unq (Constant c)
654 = reflCall "TConst" [reflectConstant c]
655reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
656reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
657reflectTTQuote _ (Proj _ _) =
658 error "Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."
659reflectTTQuote unq Erased = Var (reflm "Erased")
660reflectTTQuote _ Impossible =
661 error "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."
662reflectTTQuote _ (Inferred tm) =
663 error "Phase error! The Inferred constructor is for coverage checking only and should not have been reflected during elaboration."
665reflectRawQuote :: [Name] -> Raw -> Raw
666reflectRawQuote unq (Var n)
667 | n `elem` unq = Var n
668 | otherwise = reflCall "Var" [reflectName n]
669reflectRawQuote unq (RBind n b r) =
670 reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]
671reflectRawQuote unq (RApp f x) =
672 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
673reflectRawQuote unq RType = Var (reflm "RType")
674reflectRawQuote unq (RUType u) =
675 reflCall "RUType" [reflectUniverse u]
676reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
678reflectNameType :: NameType -> Raw
679reflectNameType (Bound) = Var (reflm "Bound")
680reflectNameType (Ref) = Var (reflm "Ref")
681reflectNameType (DCon x y _)
682 = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!
683reflectNameType (TCon x y)
684 = reflCall "TCon" [RConstant (I x), RConstant (I y)]
686reflectName :: Name -> Raw
687reflectName (UN s)
688 = reflCall "UN" [RConstant (Str (str s))]
689reflectName (NS n ns)
690 = reflCall "NS" [ reflectName n
691 , foldr (\ n s ->
692 raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
693 [ RConstant StrType, RConstant (Str n), s ])
694 ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
695 [ RConstant StrType ])
696 (map str ns)
697 ]
698reflectName (MN i n)
699 = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
700reflectName (SN sn) = raw_apply (Var (reflm "SN")) [reflectSpecialName sn]
701reflectName (SymRef _) = error "The impossible happened: symbol table ref survived IBC loading"
703reflectSpecialName :: SpecialName -> Raw
704reflectSpecialName (WhereN i n1 n2) =
705 reflCall "WhereN" [RConstant (I i), reflectName n1, reflectName n2]
706reflectSpecialName (WithN i n) = reflCall "WithN" [ RConstant (I i)
707 , reflectName n
708 ]
709reflectSpecialName (ImplementationN impl ss) =
710 reflCall "ImplementationN" [ reflectName impl
711 , mkList (RConstant StrType) $
712 map (RConstant . Str . T.unpack) ss
713 ]
714reflectSpecialName (ParentN n s) =
715 reflCall "ParentN" [reflectName n, RConstant (Str (T.unpack s))]
716reflectSpecialName (MethodN n) =
717 reflCall "MethodN" [reflectName n]
718reflectSpecialName (CaseN fc n) =
719 reflCall "CaseN" [reflectFC (unwrapFC fc), 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 rc 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 (UniverseError fc ue old new tys) =
925 -- NB: loses information, but OK because this is not likely to be rewritten
926 Var $ reflErrName "UniverseError"
927reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
928reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
929reflectErr (UnknownImplicit n f) = raw_apply (Var $ reflErrName "UnknownImplicit") [reflectName n, reflectName f]
930reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
931reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
932reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
933reflectErr (NoRewriting l r tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect l, reflect r, reflect tm]
934reflectErr (ProviderError str) =
935 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
936reflectErr (LoadingFailed str err) =
937 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
938reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
940-- | Reflect a file context
941reflectFC :: FC -> Raw
942reflectFC fc = raw_apply (Var (reflm "FileLoc"))
943 [ RConstant (Str (fc_fname fc))
944 , raw_apply (Var pairCon) $
945 [intTy, intTy] ++
946 map (RConstant . I)
947 [ fst (fc_start fc)
948 , snd (fc_start fc)
949 ]
950 , raw_apply (Var pairCon) $
951 [intTy, intTy] ++
952 map (RConstant . I)
953 [ fst (fc_end fc)
954 , snd (fc_end fc)
955 ]
956 ]
957 where intTy = RConstant (AType (ATInt ITNative))
959reifyFC :: Term -> ElabD FC
960reifyFC tm
961 | (P (DCon _ _ _) cn _, [Constant (Str fn), st, end]) <- unApply tm
962 , cn == reflm "FileLoc" = FC fn <$> reifyPair reifyInt reifyInt st <*> reifyPair reifyInt reifyInt end
963 | otherwise = fail $ "Not a source location: " ++ show tm
965fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
966fromTTMaybe (App _ (App _ (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
967 | just == txt "Just" = Just tm
968fromTTMaybe x = Nothing
970reflErrName :: String -> Name
971reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
973-- | Attempt to reify a report part from TT to the internal
974-- representation. Not in Idris or ElabD monads because it should be usable
975-- from either.
976reifyReportPart :: Term -> Either Err ErrorReportPart
977reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
978 Right (TextPart msg)
979reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
980 | n == reflm "NamePart" =
981 case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 Erased) of
982 Error e -> Left . InternalMsg $
983 "could not reify name term " ++
984 show ttn ++
985 " when reflecting an error:" ++ show e
986 OK (n', _)-> Right $ NamePart n'
987reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
988 | n == reflm "TermPart" =
989 case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 Erased) of
990 Error e -> Left . InternalMsg $
991 "could not reify reflected term " ++
992 show tm ++
993 " when reflecting an error:" ++ show e
994 OK (tm', _) -> Right $ TermPart tm'
995reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
996 | n == reflm "RawPart" =
997 case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 Erased) of
998 Error e -> Left . InternalMsg $
999 "could not reify reflected raw term " ++
1000 show tm ++
1001 " when reflecting an error: " ++ show e
1002 OK (tm', _) -> Right $ RawPart tm'
1003reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
1004 | n == reflm "SubReport" =
1005 case unList tm of
1006 Just xs -> do subParts <- mapM reifyReportPart xs
1007 Right (SubReport subParts)
1008 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
1009reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
1011reifyErasure :: Term -> ElabD RErasure
1012reifyErasure (P (DCon _ _ _) n _)
1013 | n == tacN "Erased" = return RErased
1014 | n == tacN "NotErased" = return RNotErased
1015reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."
1017reifyPlicity :: Term -> ElabD RPlicity
1018reifyPlicity (P (DCon _ _ _) n _)
1019 | n == tacN "Explicit" = return RExplicit
1020 | n == tacN "Implicit" = return RImplicit
1021 | n == tacN "Constraint" = return RConstraint
1022reifyPlicity tm = fail $ "Couldn't reify " ++ show tm ++ " as RPlicity."
1024reifyRFunArg :: Term -> ElabD RFunArg
1025reifyRFunArg (App _ (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argTy) argPl) argE)
1026 | n == tacN "MkFunArg" = liftM4 RFunArg
1027 (reifyTTName argN)
1028 (reifyRaw argTy)
1029 (reifyPlicity argPl)
1030 (reifyErasure argE)
1031reifyRFunArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
1033reifyTyDecl :: Term -> ElabD RTyDecl
1034reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
1035 | n == tacN "Declare" =
1036 do tyN' <- reifyTTName tyN
1037 args' <- case unList args of
1038 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
1039 Just xs -> mapM reifyRFunArg xs
1040 ret' <- reifyRaw ret
1041 return $ RDeclare tyN' args' ret'
1042reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
1044reifyFunDefn :: Term -> ElabD (RFunDefn Raw)
1045reifyFunDefn (App _ (App _ (App _ (P _ n _) (P _ t _)) fnN) clauses)
1046 | n == tacN "DefineFun" && t == reflm "Raw" =
1047 do fnN' <- reifyTTName fnN
1048 clauses' <- case unList clauses of
1049 Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
1050 Just cs -> mapM reifyC cs
1051 return $ RDefineFun fnN' clauses'
1052 where reifyC :: Term -> ElabD (RFunClause Raw)
1053 reifyC (App _ (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs) rhs)
1054 | n == tacN "MkFunClause" && t == reflm "Raw" = liftM2 RMkFunClause
1055 (reifyRaw lhs)
1056 (reifyRaw rhs)
1057 reifyC (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs)
1058 | n == tacN "MkImpossibleClause" && t == reflm "Raw" = fmap RMkImpossibleClause $ reifyRaw lhs
1059 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
1060reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
1062reifyRConstructorDefn :: Term -> ElabD RConstructorDefn
1063reifyRConstructorDefn (App _ (App _ (App _ (P _ n _) cn) args) retTy)
1064 | n == tacN "Constructor", Just args' <- unList args
1065 = RConstructor <$> reifyTTName cn <*> mapM reifyRFunArg args' <*> reifyRaw retTy
1066reifyRConstructorDefn aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RConstructorDefn"
1068reifyRDataDefn :: Term -> ElabD RDataDefn
1069reifyRDataDefn (App _ (App _ (P _ n _) tyn) ctors)
1070 | n == tacN "DefineDatatype", Just ctors' <- unList ctors
1071 = RDefineDatatype <$> reifyTTName tyn <*> mapM reifyRConstructorDefn ctors'
1072reifyRDataDefn aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RDataDefn"
1074envTupleType :: Raw
1075envTupleType
1076 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
1077 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
1080reflectList :: Raw -> [Raw] -> Raw
1081reflectList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
1082reflectList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
1083 x)
1084 (reflectList ty xs)
1086-- | Apply Idris's implicit info to get a signature. The [PArg] should
1087-- come from a lookup in idris_implicits on IState.
1088getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)
1089getArgs [] r = ([], r)
1090getArgs (a:as) (RBind n (Pi _ _ ty _) sc) =
1091 let (args, res) = getArgs as sc
1092 erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased
1093 arg' = case a of
1094 PImp {} -> RFunArg n ty RImplicit erased
1095 PExp {} -> RFunArg n ty RExplicit erased
1096 PConstraint {} -> RFunArg n ty RConstraint erased
1097 PTacImplicit {} -> RFunArg n ty RImplicit erased
1098 in (arg':args, res)
1099getArgs _ r = ([], r)
1101unApplyRaw :: Raw -> (Raw, [Raw])
1102unApplyRaw tm = ua [] tm
1103 where
1104 ua args (RApp f a) = ua (a:args) f
1105 ua args t = (t, args)
1107-- | Build the reflected function definition(s) that correspond(s) to
1108-- a provided unqualified name
1109buildFunDefns :: IState -> Name -> [RFunDefn Term]
1110buildFunDefns ist n =
1111 [ mkFunDefn name clauses
1112 | (name, (clauses, _)) <- lookupCtxtName n $ idris_patdefs ist
1115 where mkFunDefn name clauses = RDefineFun name (map mkFunClause clauses)
1117 mkFunClause ([], lhs, Impossible) = RMkImpossibleClause lhs
1118 mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs
1119 mkFunClause (((n, ty) : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where
1120 bind Impossible = Impossible
1121 bind tm = Bind n (PVar RigW ty) tm
1123-- | Build the reflected datatype definition(s) that correspond(s) to
1124-- a provided unqualified name
1125buildDatatypes :: IState -> Name -> [RDatatype]
1126buildDatatypes ist n =
1127 catMaybes [ mkDataType dn ti
1128 | (dn, ti) <- lookupCtxtName n datatypes
1130 where datatypes = idris_datatypes ist
1131 ctxt = tt_ctxt ist
1132 impls = idris_implicits ist
1134 ctorSig params cn = do cty <- fmap forget (lookupTyExact cn ctxt)
1135 argInfo <- lookupCtxtExact cn impls
1136 let (args, res) = getArgs argInfo cty
1137 return (cn, ctorArgsStatus args res params, res)
1139 argPos n [] res = findPos n res
1140 where findPos n app = case unApplyRaw app of
1141 (_, argL) -> findIndex (== Var n) argL
1142 argPos n (arg:args) res = if n == argName arg
1143 then Nothing
1144 else argPos n args res
1146 ctorArgsStatus :: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
1147 ctorArgsStatus [] _ _ = []
1148 ctorArgsStatus (arg:args) res params =
1149 case argPos (argName arg) args res of
1150 Nothing -> RCtorField arg : ctorArgsStatus args res params
1151 Just i -> if i `elem` params
1152 then RCtorParameter arg : ctorArgsStatus args res params
1153 else RCtorField arg : ctorArgsStatus args res params
1155 mkDataType name (TI {param_pos = params, con_names = constrs}) =
1156 do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
1157 implInfo <- lookupCtxtExact name impls
1158 let (tcargs, tcres) = getTCArgs params implInfo (forget ty)
1159 ctors <- mapM (ctorSig params) constrs
1160 return $ RDatatype name tcargs tcres ctors
1162 getTCArgs :: [Int] -> [PArg] -> Raw -> ([RTyConArg], Raw)
1163 getTCArgs params implInfo tcTy =
1164 let (args, res) = getArgs implInfo tcTy
1165 in (tcArg args 0, res)
1166 where tcArg [] _ = []
1167 tcArg (arg:args) i | i `elem` params = RParameter arg : tcArg args (i+1)
1168 | otherwise = RIndex arg : tcArg args (i+1)
1171reflectErasure :: RErasure -> Raw
1172reflectErasure RErased = Var (tacN "Erased")
1173reflectErasure RNotErased = Var (tacN "NotErased")
1175reflectPlicity :: RPlicity -> Raw
1176reflectPlicity RExplicit = Var (tacN "Explicit")
1177reflectPlicity RImplicit = Var (tacN "Implicit")
1178reflectPlicity RConstraint = Var (tacN "Constraint")
1180reflectArg :: RFunArg -> Raw
1181reflectArg (RFunArg n ty plic erasure) =
1182 RApp (RApp (RApp (RApp (Var $ tacN "MkFunArg") (reflectName n))
1183 (reflectRaw ty))
1184 (reflectPlicity plic))
1185 (reflectErasure erasure)
1187reflectCtorArg :: RCtorArg -> Raw
1188reflectCtorArg (RCtorParameter arg) = RApp (Var $ tacN "CtorParameter") (reflectArg arg)
1189reflectCtorArg (RCtorField arg) = RApp (Var $ tacN "CtorField") (reflectArg arg)
1191reflectDatatype :: RDatatype -> Raw
1192reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
1193 raw_apply (Var $ tacN "MkDatatype") [ reflectName tyn
1194 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
1195 , reflectRaw tyConRes
1196 , rawList (rawTripleTy (Var $ reflm "TTName")
1197 (RApp (Var (sNS (sUN "List") ["List", "Prelude"]))
1198 (Var $ tacN "CtorArg"))
1199 (Var $ reflm "Raw"))
1200 [ rawTriple ((Var $ reflm "TTName")
1201 ,(RApp (Var (sNS (sUN "List") ["List", "Prelude"]))
1202 (Var $ tacN "CtorArg"))
1203 ,(Var $ reflm "Raw"))
1204 (reflectName cn
1205 ,rawList (Var $ tacN "CtorArg")
1206 (map reflectCtorArg cargs)
1207 ,reflectRaw cty)
1208 | (cn, cargs, cty) <- constrs
1211 where reflectConArg (RParameter a) =
1212 RApp (Var $ tacN "TyConParameter") (reflectArg a)
1213 reflectConArg (RIndex a) =
1214 RApp (Var $ tacN "TyConIndex") (reflectArg a)
1216reflectFunClause :: RFunClause Term -> Raw
1217reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause")
1218 $ (Var $ reflm "TT") : map reflect [ lhs, rhs ]
1220reflectFunClause (RMkImpossibleClause lhs) = raw_apply (Var $ tacN "MkImpossibleClause")
1221 [ Var $ reflm "TT", reflect lhs ]
1223reflectFunDefn :: RFunDefn Term -> Raw
1224reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun")
1225 [ Var $ reflm "TT"
1226 , reflectName name
1227 , rawList (RApp (Var $ tacN "FunClause")
1228 (Var $ reflm "TT"))
1229 (map reflectFunClause clauses)