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