git.iko.soy/Idris-dev
on 2b0224a help sign in
Idris-dev/src/Idris/Reflection.hs
1004 lines 45 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)
10import Data.Maybe (catMaybes)
11import Data.List ((\\))
12import qualified Data.Text as T
14import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
15 movelast, runElab, solve)
16import Idris.Core.Evaluate (Context, Def(TyDecl), initContext, lookupDefExact, lookupTyExact)
17import Idris.Core.TT
19import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),
20 PTerm(..), initEState, pairCon, pairTy)
21import Idris.Delaborate (delab)
23data RArg = RExplicit { argName :: Name, argTy :: Raw }
24 | RImplicit { argName :: Name, argTy :: Raw }
25 | RConstraint { argName :: Name, argTy :: Raw }
26 deriving Show
28data RTyDecl = RDeclare Name [RArg] Raw deriving Show
30data RTyConArg = RParameter { tcArgName :: Name, tcArgTy :: Raw }
31 | RIndex { tcArgName :: Name, tcArgTy :: Raw }
32 deriving Show
34data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, Raw)] deriving Show
36rArgToPArg :: RArg -> PArg
37rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
38rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
39rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder
41data RFunClause = RMkFunClause Raw Raw
42 | RMkImpossibleClause Raw
43 deriving Show
45data RFunDefn = RDefineFun Name [RFunClause] deriving Show
47-- | Prefix a name with the "Language.Reflection" namespace
48reflm :: String -> Name
49reflm n = sNS (sUN n) ["Reflection", "Language"]
51-- | Prefix a name with the "Language.Reflection.Elab" namespace
52tacN :: String -> Name
53tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]
55-- | Reify tactics from their reflected representation
56reify :: IState -> Term -> ElabD PTactic
57reify _ (P _ n _) | n == reflm "Intros" = return Intros
58reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
59reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
60reify _ (P _ n _) | n == reflm "Solve" = return Solve
61reify _ (P _ n _) | n == reflm "Compute" = return Compute
62reify _ (P _ n _) | n == reflm "Skip" = return Skip
63reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
64reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
65reify ist t@(App _ _ _)
66 | (P _ f _, args) <- unApply t = reifyApp ist f args
67reify _ t = fail ("Unknown tactic " ++ show t)
69reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
70reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
71reifyApp _ t [Constant (I i)]
72 | t == reflm "Search" = return (ProofSearch True True i Nothing [])
73reifyApp _ t [x]
74 | t == reflm "Refine" = do n <- reifyTTName x
75 return $ Refine n []
76reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
77 goal <- reifyTT ty
78 return $ Claim n' (delab ist goal)
79reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
80reifyApp ist t [Constant (Str n), x]
81 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
82reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
83reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
84reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')
85reifyApp ist t [t']
86 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
87reifyApp ist t [t']
88 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
89reifyApp ist t [t']
90 | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
91reifyApp _ t [t']
92 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
93reifyApp ist t [t']
94 | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
95reifyApp ist t [x]
96 | t == reflm "Focus" = liftM Focus (reifyTTName x)
97reifyApp ist t [t']
98 | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
99reifyApp ist t [n, t']
100 | t == reflm "LetTac" = do n' <- reifyTTName n
101 t'' <- reifyTT t'
102 return $ LetTac n' (delab ist t')
103reifyApp ist t [n, tt', t']
104 | t == reflm "LetTacTy" = do n' <- reifyTTName n
105 tt'' <- reifyTT tt'
106 t'' <- reifyTT t'
107 return $ LetTacTy n' (delab ist tt'') (delab ist t'')
108reifyApp ist t [errs]
109 | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
110reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
112reifyReportParts :: Term -> ElabD [ErrorReportPart]
113reifyReportParts errs =
114 case unList errs of
115 Nothing -> fail "Failed to reify errors"
116 Just errs' ->
117 let parts = mapM reifyReportPart errs' in
118 case parts of
119 Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
120 Right errs'' ->
121 return errs''
123-- | Reify terms from their reflected representation
124reifyTT :: Term -> ElabD Term
125reifyTT t@(App _ _ _)
126 | (P _ f _, args) <- unApply t = reifyTTApp f args
127reifyTT t@(P _ n _)
128 | n == reflm "Erased" = return $ Erased
129reifyTT t@(P _ n _)
130 | n == reflm "Impossible" = return $ Impossible
131reifyTT t = fail ("Unknown reflection term: " ++ show t)
133reifyTTApp :: Name -> [Term] -> ElabD Term
134reifyTTApp t [nt, n, x]
135 | t == reflm "P" = do nt' <- reifyTTNameType nt
136 n' <- reifyTTName n
137 x' <- reifyTT x
138 return $ P nt' n' x'
139reifyTTApp t [Constant (I i)]
140 | t == reflm "V" = return $ V i
141reifyTTApp t [n, b, x]
142 | t == reflm "Bind" = do n' <- reifyTTName n
143 b' <- reifyTTBinder reifyTT (reflm "TT") b
144 x' <- reifyTT x
145 return $ Bind n' b' x'
146reifyTTApp t [f, x]
147 | t == reflm "App" = do f' <- reifyTT f
148 x' <- reifyTT x
149 return $ App Complete f' x'
150reifyTTApp t [c]
151 | t == reflm "TConst" = liftM Constant (reifyTTConst c)
152reifyTTApp t [t', Constant (I i)]
153 | t == reflm "Proj" = do t'' <- reifyTT t'
154 return $ Proj t'' i
155reifyTTApp t [tt]
156 | t == reflm "TType" = liftM TType (reifyTTUExp tt)
157reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
159-- | Reify raw terms from their reflected representation
160reifyRaw :: Term -> ElabD Raw
161reifyRaw t@(App _ _ _)
162 | (P _ f _, args) <- unApply t = reifyRawApp f args
163reifyRaw t@(P _ n _)
164 | n == reflm "RType" = return $ RType
165reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)
167reifyRawApp :: Name -> [Term] -> ElabD Raw
168reifyRawApp t [n]
169 | t == reflm "Var" = liftM Var (reifyTTName n)
170reifyRawApp t [n, b, x]
171 | t == reflm "RBind" = do n' <- reifyTTName n
172 b' <- reifyTTBinder reifyRaw (reflm "Raw") b
173 x' <- reifyRaw x
174 return $ RBind n' b' x'
175reifyRawApp t [f, x]
176 | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
177reifyRawApp t [t']
178 | t == reflm "RForce" = liftM RForce (reifyRaw t')
179reifyRawApp t [c]
180 | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
181reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
183reifyTTName :: Term -> ElabD Name
184reifyTTName t
185 | (P _ f _, args) <- unApply t = reifyTTNameApp f args
186reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
188reifyTTNameApp :: Name -> [Term] -> ElabD Name
189reifyTTNameApp t [Constant (Str n)]
190 | t == reflm "UN" = return $ sUN n
191reifyTTNameApp t [n, ns]
192 | t == reflm "NS" = do n' <- reifyTTName n
193 ns' <- reifyTTNamespace ns
194 return $ sNS n' ns'
195reifyTTNameApp t [Constant (I i), Constant (Str n)]
196 | t == reflm "MN" = return $ sMN i n
197reifyTTNameApp t [sn]
198 | t == reflm "SN"
199 , (P _ f _, args) <- unApply sn = SN <$> reifySN f args
200 where reifySN :: Name -> [Term] -> ElabD SpecialName
201 reifySN t [Constant (I i), n1, n2]
202 | t == reflm "WhereN" = WhereN i <$> reifyTTName n1 <*> reifyTTName n2
203 reifySN t [Constant (I i), n]
204 | t == reflm "WithN" = WithN i <$> reifyTTName n
205 reifySN t [n, ss]
206 | t == reflm "InstanceN" =
207 case unList ss of
208 Nothing -> fail "Can't reify InstanceN strings"
209 Just ss' -> InstanceN <$> reifyTTName n <*>
210 pure [T.pack s | Constant (Str s) <- ss']
211 reifySN t [n, Constant (Str s)]
212 | t == reflm "ParentN" =
213 ParentN <$> reifyTTName n <*> pure (T.pack s)
214 reifySN t [n]
215 | t == reflm "MethodN" =
216 MethodN <$> reifyTTName n
217 reifySN t [n]
218 | t == reflm "CaseN" =
219 CaseN <$> reifyTTName n
220 reifySN t [n]
221 | t == reflm "ElimN" =
222 ElimN <$> reifyTTName n
223 reifySN t [n]
224 | t == reflm "InstanceCtorN" =
225 InstanceCtorN <$> reifyTTName n
226 reifySN t [n1, n2]
227 | t == reflm "MetaN" =
228 MetaN <$> reifyTTName n1 <*> reifyTTName n2
229 reifySN t args = fail $ "Can't reify special name " ++ show t ++ show args
230reifyTTNameApp t []
231 | t == reflm "NErased" = return NErased
232reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
234reifyTTNamespace :: Term -> ElabD [String]
235reifyTTNamespace t@(App _ _ _)
236 = case unApply t of
237 (P _ f _, [Constant StrType])
238 | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
239 (P _ f _, [Constant StrType, Constant (Str n), ns])
240 | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
241 _ -> fail ("Unknown reflection namespace arg: " ++ show t)
242reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
244reifyTTNameType :: Term -> ElabD NameType
245reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
246reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
247reifyTTNameType t@(App _ _ _)
248 = case unApply t of
249 (P _ f _, [Constant (I tag), Constant (I num)])
250 | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!
251 | f == reflm "TCon" -> return $ TCon tag num
252 _ -> fail ("Unknown reflection name type: " ++ show t)
253reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
255reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
256reifyTTBinder reificator binderType t@(App _ _ _)
257 = case unApply t of
258 (P _ f _, bt:args) | forget bt == Var binderType
259 -> reifyTTBinderApp reificator f args
260 _ -> fail ("Mismatching binder reflection: " ++ show t)
261reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
263reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
264reifyTTBinderApp reif f [t]
265 | f == reflm "Lam" = liftM Lam (reif t)
266reifyTTBinderApp reif f [t, k]
267 | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)
268reifyTTBinderApp reif f [x, y]
269 | f == reflm "Let" = liftM2 Let (reif x) (reif y)
270reifyTTBinderApp reif f [x, y]
271 | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
272reifyTTBinderApp reif f [t]
273 | f == reflm "Hole" = liftM Hole (reif t)
274reifyTTBinderApp reif f [t]
275 | f == reflm "GHole" = liftM (GHole 0) (reif t)
276reifyTTBinderApp reif f [x, y]
277 | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
278reifyTTBinderApp reif f [t]
279 | f == reflm "PVar" = liftM PVar (reif t)
280reifyTTBinderApp reif f [t]
281 | f == reflm "PVTy" = liftM PVTy (reif t)
282reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
284reifyTTConst :: Term -> ElabD Const
285reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
286reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
287reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
288reifyTTConst t@(App _ _ _)
289 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
290reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
292reifyTTConstApp :: Name -> Term -> ElabD Const
293reifyTTConstApp f aty
294 | f == reflm "AType" = fmap AType (reifyArithTy aty)
295reifyTTConstApp f (Constant c@(I _))
296 | f == reflm "I" = return $ c
297reifyTTConstApp f (Constant c@(BI _))
298 | f == reflm "BI" = return $ c
299reifyTTConstApp f (Constant c@(Fl _))
300 | f == reflm "Fl" = return $ c
301reifyTTConstApp f (Constant c@(I _))
302 | f == reflm "Ch" = return $ c
303reifyTTConstApp f (Constant c@(Str _))
304 | f == reflm "Str" = return $ c
305reifyTTConstApp f (Constant c@(B8 _))
306 | f == reflm "B8" = return $ c
307reifyTTConstApp f (Constant c@(B16 _))
308 | f == reflm "B16" = return $ c
309reifyTTConstApp f (Constant c@(B32 _))
310 | f == reflm "B32" = return $ c
311reifyTTConstApp f (Constant c@(B64 _))
312 | f == reflm "B64" = return $ c
313reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
315reifyArithTy :: Term -> ElabD ArithTy
316reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
317reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
318reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
320reifyNativeTy :: Term -> ElabD NativeTy
321reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
322reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
323reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
324reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
325reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
327reifyIntTy :: Term -> ElabD IntTy
328reifyIntTy (App _ (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
329reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
330reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
331reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
332reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
334reifyTTUExp :: Term -> ElabD UExp
335reifyTTUExp t@(App _ _ _)
336 = case unApply t of
337 (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
338 (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
339 _ -> fail ("Unknown reflection type universe expression: " ++ show t)
340reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
342-- | Create a reflected call to a named function/constructor
343reflCall :: String -> [Raw] -> Raw
344reflCall funName args
345 = raw_apply (Var (reflm funName)) args
347-- | Lift a term into its Language.Reflection.TT representation
348reflect :: Term -> Raw
349reflect = reflectTTQuote []
351-- | Lift a term into its Language.Reflection.Raw representation
352reflectRaw :: Raw -> Raw
353reflectRaw = reflectRawQuote []
355claimTT :: Name -> ElabD Name
356claimTT n = do n' <- getNameFrom n
357 claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
358 return n'
360-- | Convert a reflected term to a more suitable form for pattern-matching.
361-- In particular, the less-interesting bits are elaborated to _ patterns. This
362-- happens to NameTypes, universe levels, names that are bound but not used,
363-- and the type annotation field of the P constructor.
364reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
365reflectTTQuotePattern unq (P _ n _)
366 | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
367 do fill (Var n) ; solve
368 | otherwise =
369 do tyannot <- claimTT (sMN 0 "pTyAnnot")
370 movelast tyannot -- use a _ pattern here
371 nt <- getNameFrom (sMN 0 "nt")
372 claim nt (Var (reflm "NameType"))
373 movelast nt -- use a _ pattern here
374 n' <- getNameFrom (sMN 0 "n")
375 claim n' (Var (reflm "TTName"))
376 fill $ reflCall "P" [Var nt, Var n', Var tyannot]
377 solve
378 focus n'; reflectNameQuotePattern n
379reflectTTQuotePattern unq (V n)
380 = do fill $ reflCall "V" [RConstant (I n)]
381 solve
382reflectTTQuotePattern unq (Bind n b x)
383 = do x' <- claimTT (sMN 0 "sc")
384 movelast x'
385 b' <- getNameFrom (sMN 0 "binder")
386 claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
387 (Var (sNS (sUN "TT") ["Reflection", "Language"])))
388 if n `elem` freeNames x
389 then do fill $ reflCall "Bind"
390 [reflectName n,
391 Var b',
392 Var x']
393 solve
394 else do any <- getNameFrom (sMN 0 "anyName")
395 claim any (Var (reflm "TTName"))
396 movelast any
397 fill $ reflCall "Bind"
398 [Var any,
399 Var b',
400 Var x']
401 solve
402 focus x'; reflectTTQuotePattern unq x
403 focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
404reflectTTQuotePattern unq (App _ f x)
405 = do f' <- claimTT (sMN 0 "f"); movelast f'
406 x' <- claimTT (sMN 0 "x"); movelast x'
407 fill $ reflCall "App" [Var f', Var x']
408 solve
409 focus f'; reflectTTQuotePattern unq f
410 focus x'; reflectTTQuotePattern unq x
411reflectTTQuotePattern unq (Constant c)
412 = do fill $ reflCall "TConst" [reflectConstant c]
413 solve
414reflectTTQuotePattern unq (Proj t i)
415 = do t' <- claimTT (sMN 0 "t"); movelast t'
416 fill $ reflCall "Proj" [Var t', RConstant (I i)]
417 solve
418 focus t'; reflectTTQuotePattern unq t
419reflectTTQuotePattern unq (Erased)
420 = do erased <- claimTT (sMN 0 "erased")
421 movelast erased
422 fill $ (Var erased)
423 solve
424reflectTTQuotePattern unq (Impossible)
425 = do fill $ Var (reflm "Impossible")
426 solve
427reflectTTQuotePattern unq (TType exp)
428 = do ue <- getNameFrom (sMN 0 "uexp")
429 claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
430 movelast ue
431 fill $ reflCall "TType" [Var ue]
432 solve
433reflectTTQuotePattern unq (UType u)
434 = do uH <- getNameFrom (sMN 0 "someUniv")
435 claim uH (Var (reflm "Universe"))
436 movelast uH
437 fill $ reflCall "UType" [Var uH]
438 solve
439 focus uH
440 fill (Var (reflm (case u of
441 NullType -> "NullType"
442 UniqueType -> "UniqueType"
443 AllTypes -> "AllTypes")))
444 solve
446reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
447reflectRawQuotePattern unq (Var n)
448 -- the unquoted names already have types, just use them
449 | n `elem` unq = do fill (Var n); solve
450 | otherwise = do fill (reflCall "Var" [reflectName n]); solve
451reflectRawQuotePattern unq (RBind n b sc) =
452 do scH <- getNameFrom (sMN 0 "sc")
453 claim scH (Var (reflm "Raw"))
454 movelast scH
455 bH <- getNameFrom (sMN 0 "binder")
456 claim bH (RApp (Var (reflm "Binder"))
457 (Var (reflm "Raw")))
458 if n `elem` freeNamesR sc
459 then do fill $ reflCall "RBind" [reflectName n,
460 Var bH,
461 Var scH]
462 solve
463 else do any <- getNameFrom (sMN 0 "anyName")
464 claim any (Var (reflm "TTName"))
465 movelast any
466 fill $ reflCall "RBind" [Var any, Var bH, Var scH]
467 solve
468 focus scH; reflectRawQuotePattern unq sc
469 focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b
470 where freeNamesR (Var n) = [n]
471 freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
472 freeNamesR body \\ [n],
473 freeNamesR t]
474 freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
475 (freeNamesR body \\ [n])
476 freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
477 freeNamesR RType = []
478 freeNamesR (RUType _) = []
479 freeNamesR (RForce r) = freeNamesR r
480 freeNamesR (RConstant _) = []
481reflectRawQuotePattern unq (RApp f x) =
482 do fH <- getNameFrom (sMN 0 "f")
483 claim fH (Var (reflm "Raw"))
484 movelast fH
485 xH <- getNameFrom (sMN 0 "x")
486 claim xH (Var (reflm "Raw"))
487 movelast xH
488 fill $ reflCall "RApp" [Var fH, Var xH]
489 solve
490 focus fH; reflectRawQuotePattern unq f
491 focus xH; reflectRawQuotePattern unq x
492reflectRawQuotePattern unq RType =
493 do fill (Var (reflm "RType"))
494 solve
495reflectRawQuotePattern unq (RUType univ) =
496 do uH <- getNameFrom (sMN 0 "universe")
497 claim uH (Var (reflm "Universe"))
498 movelast uH
499 fill $ reflCall "RUType" [Var uH]
500 solve
501 focus uH; fill (reflectUniverse univ); solve
502reflectRawQuotePattern unq (RForce r) =
503 do rH <- getNameFrom (sMN 0 "raw")
504 claim rH (Var (reflm "Raw"))
505 movelast rH
506 fill $ reflCall "RForce" [Var rH]
507 solve
508 focus rH; reflectRawQuotePattern unq r
509reflectRawQuotePattern unq (RConstant c) =
510 do cH <- getNameFrom (sMN 0 "const")
511 claim cH (Var (reflm "Constant"))
512 movelast cH
513 fill (reflCall "RConstant" [Var cH]); solve
514 focus cH
515 fill (reflectConstant c); solve
517reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()
518reflectBinderQuotePattern q unq (Lam t)
519 = do t' <- claimTT (sMN 0 "ty"); movelast t'
520 fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
521 solve
522 focus t'; q unq t
523reflectBinderQuotePattern q unq (Pi _ t k)
524 = do t' <- claimTT (sMN 0 "ty") ; movelast t'
525 k' <- claimTT (sMN 0 "k"); movelast k';
526 fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
527 solve
528 focus t'; q unq t
529reflectBinderQuotePattern q unq (Let x y)
530 = do x' <- claimTT (sMN 0 "ty"); movelast x';
531 y' <- claimTT (sMN 0 "v"); movelast y';
532 fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
533 solve
534 focus x'; q unq x
535 focus y'; q unq y
536reflectBinderQuotePattern q unq (NLet x y)
537 = do x' <- claimTT (sMN 0 "ty"); movelast x'
538 y' <- claimTT (sMN 0 "v"); movelast y'
539 fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
540 solve
541 focus x'; q unq x
542 focus y'; q unq y
543reflectBinderQuotePattern q unq (Hole t)
544 = do t' <- claimTT (sMN 0 "ty"); movelast t'
545 fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
546 solve
547 focus t'; q unq t
548reflectBinderQuotePattern q unq (GHole _ t)
549 = do t' <- claimTT (sMN 0 "ty"); movelast t'
550 fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
551 solve
552 focus t'; q unq t
553reflectBinderQuotePattern q unq (Guess x y)
554 = do x' <- claimTT (sMN 0 "ty"); movelast x'
555 y' <- claimTT (sMN 0 "v"); movelast y'
556 fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
557 solve
558 focus x'; q unq x
559 focus y'; q unq y
560reflectBinderQuotePattern q unq (PVar t)
561 = do t' <- claimTT (sMN 0 "ty"); movelast t'
562 fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
563 solve
564 focus t'; q unq t
565reflectBinderQuotePattern q unq (PVTy t)
566 = do t' <- claimTT (sMN 0 "ty"); movelast t'
567 fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
568 solve
569 focus t'; q unq t
571reflectUniverse :: Universe -> Raw
572reflectUniverse u =
573 (Var (reflm (case u of
574 NullType -> "NullType"
575 UniqueType -> "UniqueType"
576 AllTypes -> "AllTypes")))
578-- | Create a reflected TT term, but leave refs to the provided name intact
579reflectTTQuote :: [Name] -> Term -> Raw
580reflectTTQuote unq (P nt n t)
581 | n `elem` unq = Var n
582 | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
583reflectTTQuote unq (V n)
584 = reflCall "V" [RConstant (I n)]
585reflectTTQuote unq (Bind n b x)
586 = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]
587reflectTTQuote unq (App _ f x)
588 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
589reflectTTQuote unq (Constant c)
590 = reflCall "TConst" [reflectConstant c]
591reflectTTQuote unq (Proj t i)
592 = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
593reflectTTQuote unq (Erased) = Var (reflm "Erased")
594reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
595reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
596reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
598reflectRawQuote :: [Name] -> Raw -> Raw
599reflectRawQuote unq (Var n)
600 | n `elem` unq = Var n
601 | otherwise = reflCall "Var" [reflectName n]
602reflectRawQuote unq (RBind n b r) =
603 reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]
604reflectRawQuote unq (RApp f x) =
605 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
606reflectRawQuote unq RType = Var (reflm "RType")
607reflectRawQuote unq (RUType u) =
608 reflCall "RUType" [reflectUniverse u]
609reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
610reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
612reflectNameType :: NameType -> Raw
613reflectNameType (Bound) = Var (reflm "Bound")
614reflectNameType (Ref) = Var (reflm "Ref")
615reflectNameType (DCon x y _)
616 = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!
617reflectNameType (TCon x y)
618 = reflCall "TCon" [RConstant (I x), RConstant (I y)]
620reflectName :: Name -> Raw
621reflectName (UN s)
622 = reflCall "UN" [RConstant (Str (str s))]
623reflectName (NS n ns)
624 = reflCall "NS" [ reflectName n
625 , foldr (\ n s ->
626 raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
627 [ RConstant StrType, RConstant (Str n), s ])
628 ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
629 [ RConstant StrType ])
630 (map str ns)
631 ]
632reflectName (MN i n)
633 = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
634reflectName NErased = Var (reflm "NErased")
635reflectName (SN sn) = raw_apply (Var (reflm "SN")) [reflectSpecialName sn]
636reflectName (SymRef _) = error "The impossible happened: symbol table ref survived IBC loading"
638reflectSpecialName :: SpecialName -> Raw
639reflectSpecialName (WhereN i n1 n2) =
640 reflCall "WhereN" [RConstant (I i), reflectName n1, reflectName n2]
641reflectSpecialName (WithN i n) = reflCall "WithN" [ RConstant (I i)
642 , reflectName n
643 ]
644reflectSpecialName (InstanceN inst ss) =
645 reflCall "InstanceN" [ reflectName inst
646 , mkList (RConstant StrType) $
647 map (RConstant . Str . T.unpack) ss
648 ]
649reflectSpecialName (ParentN n s) =
650 reflCall "ParentN" [reflectName n, RConstant (Str (T.unpack s))]
651reflectSpecialName (MethodN n) =
652 reflCall "MethodN" [reflectName n]
653reflectSpecialName (CaseN n) =
654 reflCall "CaseN" [reflectName n]
655reflectSpecialName (ElimN n) =
656 reflCall "ElimN" [reflectName n]
657reflectSpecialName (InstanceCtorN n) =
658 reflCall "InstanceCtorN" [reflectName n]
659reflectSpecialName (MetaN parent meta) =
660 reflCall "MetaN" [reflectName parent, reflectName meta]
662-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
663-- MNs corresponding to will care about the string but not the number. All
664-- others become _.
665reflectNameQuotePattern :: Name -> ElabD ()
666reflectNameQuotePattern n@(UN s)
667 = do fill $ reflectName n
668 solve
669reflectNameQuotePattern n@(NS _ _)
670 = do fill $ reflectName n
671 solve
672reflectNameQuotePattern (MN _ n)
673 = do i <- getNameFrom (sMN 0 "mnCounter")
674 claim i (RConstant (AType (ATInt ITNative)))
675 movelast i
676 fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
677 solve
678reflectNameQuotePattern _ -- for all other names, match any
679 = do nameHole <- getNameFrom (sMN 0 "name")
680 claim nameHole (Var (reflm "TTName"))
681 movelast nameHole
682 fill (Var nameHole)
683 solve
685reflectBinder :: Binder Term -> Raw
686reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []
688reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
689reflectBinderQuote q ty unq (Lam t)
690 = reflCall "Lam" [Var ty, q unq t]
691reflectBinderQuote q ty unq (Pi _ t k)
692 = reflCall "Pi" [Var ty, q unq t, q unq k]
693reflectBinderQuote q ty unq (Let x y)
694 = reflCall "Let" [Var ty, q unq x, q unq y]
695reflectBinderQuote q ty unq (NLet x y)
696 = reflCall "NLet" [Var ty, q unq x, q unq y]
697reflectBinderQuote q ty unq (Hole t)
698 = reflCall "Hole" [Var ty, q unq t]
699reflectBinderQuote q ty unq (GHole _ t)
700 = reflCall "GHole" [Var ty, q unq t]
701reflectBinderQuote q ty unq (Guess x y)
702 = reflCall "Guess" [Var ty, q unq x, q unq y]
703reflectBinderQuote q ty unq (PVar t)
704 = reflCall "PVar" [Var ty, q unq t]
705reflectBinderQuote q ty unq (PVTy t)
706 = reflCall "PVTy" [Var ty, q unq t]
708mkList :: Raw -> [Raw] -> Raw
709mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
710mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
711 x)
712 (mkList ty xs)
714reflectConstant :: Const -> Raw
715reflectConstant c@(I _) = reflCall "I" [RConstant c]
716reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
717reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
718reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
719reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
720reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
721reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
722reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
723reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
724reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
725reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
726reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
727reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
728reflectConstant StrType = Var (reflm "StrType")
729reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
730reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
731reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
732reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
733reflectConstant VoidType = Var (reflm "VoidType")
734reflectConstant Forgot = Var (reflm "Forgot")
735reflectConstant WorldType = Var (reflm "WorldType")
736reflectConstant TheWorld = Var (reflm "TheWorld")
738reflectUExp :: UExp -> Raw
739reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
740reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
742-- | Reflect the environment of a proof into a List (TTName, Binder TT)
743reflectEnv :: Env -> Raw
744reflectEnv = foldr consToEnvList emptyEnvList
745 where
746 consToEnvList :: (Name, Binder Term) -> Raw -> Raw
747 consToEnvList (n, b) l
748 = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
749 [ envTupleType
750 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
751 , (RApp (Var $ reflm "Binder")
752 (Var $ reflm "TT"))
753 , reflectName n
754 , reflectBinder b
755 ]
756 , l
757 ]
759 emptyEnvList :: Raw
760 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
761 [envTupleType]
763-- | Reflect an error into the internal datatype of Idris -- TODO
764rawBool :: Bool -> Raw
765rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
766rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
768rawNil :: Raw -> Raw
769rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
771rawCons :: Raw -> Raw -> Raw -> Raw
772rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
774rawList :: Raw -> [Raw] -> Raw
775rawList ty = foldr (rawCons ty) (rawNil ty)
777rawPairTy :: Raw -> Raw -> Raw
778rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
780rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
781rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
783reflectCtxt :: [(Name, Type)] -> Raw
784reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
785 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
786 (reflectName n, reflect t)))
787 ctxt)
789reflectErr :: Err -> Raw
790reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
791reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
792reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =
793 raw_apply (Var $ reflErrName "CantUnify")
794 [ rawBool b
795 , reflect t1
796 , reflect t2
797 , reflectErr e
798 , reflectCtxt ctxt
799 , RConstant (I i)]
800reflectErr (InfiniteUnify n tm ctxt) =
801 raw_apply (Var $ reflErrName "InfiniteUnify")
802 [ reflectName n
803 , reflect tm
804 , reflectCtxt ctxt
805 ]
806reflectErr (CantConvert t t' ctxt) =
807 raw_apply (Var $ reflErrName "CantConvert")
808 [ reflect t
809 , reflect t'
810 , reflectCtxt ctxt
811 ]
812reflectErr (CantSolveGoal t ctxt) =
813 raw_apply (Var $ reflErrName "CantSolveGoal")
814 [ reflect t
815 , reflectCtxt ctxt
816 ]
817reflectErr (UnifyScope n n' t ctxt) =
818 raw_apply (Var $ reflErrName "UnifyScope")
819 [ reflectName n
820 , reflectName n'
821 , reflect t
822 , reflectCtxt ctxt
823 ]
824reflectErr (CantInferType str) =
825 raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
826reflectErr (NonFunctionType t t') =
827 raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
828reflectErr (NotEquality t t') =
829 raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
830reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
831reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
832reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
833reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
834reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
835reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
836reflectErr (NotInjective t1 t2 t3) =
837 raw_apply (Var $ reflErrName "NotInjective")
838 [ reflect t1
839 , reflect t2
840 , reflect t3
841 ]
842reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
843reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
844reflectErr (CantResolveAlts ss) =
845 raw_apply (Var $ reflErrName "CantResolveAlts")
846 [rawList (Var $ reflm "TTName") (map reflectName ss)]
847reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
848reflectErr (NoEliminator str t)
849 = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),
850 reflect t]
851reflectErr (UniverseError fc ue old new tys) =
852 -- NB: loses information, but OK because this is not likely to be rewritten
853 Var $ reflErrName "UniverseError"
854reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
855reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
856reflectErr (UnknownImplicit n f) = raw_apply (Var $ reflErrName "UnknownImplicit") [reflectName n, reflectName f]
857reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
858reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
859reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
860reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
861reflectErr (ProviderError str) =
862 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
863reflectErr (LoadingFailed str err) =
864 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
865reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
867-- | Reflect a file context
868reflectFC :: FC -> Raw
869reflectFC fc = raw_apply (Var (reflm "FileLoc"))
870 [ RConstant (Str (fc_fname fc))
871 , raw_apply (Var pairCon) $
872 [intTy, intTy] ++
873 map (RConstant . I)
874 [ fst (fc_start fc)
875 , snd (fc_start fc)
876 ]
877 , raw_apply (Var pairCon) $
878 [intTy, intTy] ++
879 map (RConstant . I)
880 [ fst (fc_end fc)
881 , snd (fc_end fc)
882 ]
883 ]
884 where intTy = RConstant (AType (ATInt ITNative))
886fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
887fromTTMaybe (App _ (App _ (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
888 | just == txt "Just" = Just tm
889fromTTMaybe x = Nothing
891reflErrName :: String -> Name
892reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
894-- | Attempt to reify a report part from TT to the internal
895-- representation. Not in Idris or ElabD monads because it should be usable
896-- from either.
897reifyReportPart :: Term -> Either Err ErrorReportPart
898reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
899 Right (TextPart msg)
900reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
901 | n == reflm "NamePart" =
902 case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext emptyContext Erased) of
903 Error e -> Left . InternalMsg $
904 "could not reify name term " ++
905 show ttn ++
906 " when reflecting an error:" ++ show e
907 OK (n', _)-> Right $ NamePart n'
908reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
909 | n == reflm "TermPart" =
910 case runElab initEState (reifyTT tm) (initElaborator NErased initContext emptyContext Erased) of
911 Error e -> Left . InternalMsg $
912 "could not reify reflected term " ++
913 show tm ++
914 " when reflecting an error:" ++ show e
915 OK (tm', _) -> Right $ TermPart tm'
916reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
917 | n == reflm "SubReport" =
918 case unList tm of
919 Just xs -> do subParts <- mapM reifyReportPart xs
920 Right (SubReport subParts)
921 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
922reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
924reifyTyDecl :: Term -> ElabD RTyDecl
925reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
926 | n == tacN "Declare" =
927 do tyN' <- reifyTTName tyN
928 args' <- case unList args of
929 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
930 Just xs -> mapM reifyRArg xs
931 ret' <- reifyRaw ret
932 return $ RDeclare tyN' args' ret'
933 where reifyRArg :: Term -> ElabD RArg
934 reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)
935 | n == tacN "Explicit" = liftM2 RExplicit
936 (reifyTTName argN)
937 (reifyRaw argTy)
938 | n == tacN "Implicit" = liftM2 RImplicit
939 (reifyTTName argN)
940 (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint
941 (reifyTTName argN)
942 (reifyRaw argTy)
943 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
944reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
946reifyFunDefn :: Term -> ElabD RFunDefn
947reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)
948 | n == tacN "DefineFun" =
949 do fnN' <- reifyTTName fnN
950 clauses' <- case unList clauses of
951 Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
952 Just cs -> mapM reifyC cs
953 return $ RDefineFun fnN' clauses'
954 where reifyC :: Term -> ElabD RFunClause
955 reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)
956 | n == tacN "MkFunClause" = liftM2 RMkFunClause
957 (reifyRaw lhs)
958 (reifyRaw rhs)
959 reifyC (App _ (P (DCon _ _ _) n _) lhs)
960 | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs
961 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
962reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
964envTupleType :: Raw
965envTupleType
966 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
967 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
968 ]
970-- | Build the reflected datatype definition(s) that correspond(s) to
971-- a provided unqualified name
972buildDatatypes :: Context -> Ctxt TypeInfo -> Name -> [RDatatype]
973buildDatatypes ctxt datatypes n =
974 catMaybes [ mkDataType dn ti
975 | (dn, ti) <- lookupCtxtName n datatypes
976 ]
977 where mkDataType name (TI {param_pos = params, con_names = constrs}) =
978 do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
979 let (tcargs, tcres) = getArgs params (forget ty) 0
980 conTys <- mapM (fmap forget . flip lookupTyExact ctxt) constrs
981 return $ RDatatype name tcargs tcres $ zip constrs conTys
983 getArgs params (RBind an (Pi _ ty _) body) i =
984 let (args, res) = getArgs params body (i+1)
985 in if i `elem` params
986 then (RParameter an ty : args, res )
987 else (RIndex an ty : args, res)
988 getArgs _ tm _ = ([], tm)
990reflectDatatype :: RDatatype -> Raw
991reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
992 raw_apply (Var $ tacN "MkDatatype") [ reflectName tyn
993 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
994 , reflectRaw tyConRes
995 , rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "Raw"))
996 [ rawPair ((Var $ reflm "TTName"), (Var $ reflm "Raw"))
997 (reflectName cn, reflectRaw cty)
998 | (cn, cty) <- constrs
999 ]
1001 where reflectConArg (RParameter n t) =
1002 raw_apply (Var $ tacN "Parameter") [reflectName n, reflectRaw t]
1003 reflectConArg (RIndex n t) =
1004 raw_apply (Var $ tacN "Index") [reflectName n, reflectRaw t]