git.iko.soy/Idris-dev
on b4dbebd help sign in
Idris-dev/src/Idris/Reflection.hs
1002 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 n = Var (reflm "NErased") -- special name, not yet implemented
637reflectSpecialName :: SpecialName -> Raw
638reflectSpecialName (WhereN i n1 n2) =
639 reflCall "WhereN" [RConstant (I i), reflectName n1, reflectName n2]
640reflectSpecialName (WithN i n) = reflCall "WithN" [ RConstant (I i)
641 , reflectName n
642 ]
643reflectSpecialName (InstanceN inst ss) =
644 reflCall "InstanceN" [ reflectName inst
645 , mkList (RConstant StrType) $
646 map (RConstant . Str . T.unpack) ss
647 ]
648reflectSpecialName (ParentN n s) =
649 reflCall "ParentN" [reflectName n, RConstant (Str (T.unpack s))]
650reflectSpecialName (MethodN n) =
651 reflCall "MethodN" [reflectName n]
652reflectSpecialName (CaseN n) =
653 reflCall "CaseN" [reflectName n]
654reflectSpecialName (ElimN n) =
655 reflCall "ElimN" [reflectName n]
656reflectSpecialName (InstanceCtorN n) =
657 reflCall "InstanceCtorN" [reflectName n]
658reflectSpecialName (MetaN parent meta) =
659 reflCall "MetaN" [reflectName parent, reflectName meta]
661-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
662-- MNs corresponding to will care about the string but not the number. All
663-- others become _.
664reflectNameQuotePattern :: Name -> ElabD ()
665reflectNameQuotePattern n@(UN s)
666 = do fill $ reflectName n
667 solve
668reflectNameQuotePattern n@(NS _ _)
669 = do fill $ reflectName n
670 solve
671reflectNameQuotePattern (MN _ n)
672 = do i <- getNameFrom (sMN 0 "mnCounter")
673 claim i (RConstant (AType (ATInt ITNative)))
674 movelast i
675 fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
676 solve
677reflectNameQuotePattern _ -- for all other names, match any
678 = do nameHole <- getNameFrom (sMN 0 "name")
679 claim nameHole (Var (reflm "TTName"))
680 movelast nameHole
681 fill (Var nameHole)
682 solve
684reflectBinder :: Binder Term -> Raw
685reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []
687reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
688reflectBinderQuote q ty unq (Lam t)
689 = reflCall "Lam" [Var ty, q unq t]
690reflectBinderQuote q ty unq (Pi _ t k)
691 = reflCall "Pi" [Var ty, q unq t, q unq k]
692reflectBinderQuote q ty unq (Let x y)
693 = reflCall "Let" [Var ty, q unq x, q unq y]
694reflectBinderQuote q ty unq (NLet x y)
695 = reflCall "NLet" [Var ty, q unq x, q unq y]
696reflectBinderQuote q ty unq (Hole t)
697 = reflCall "Hole" [Var ty, q unq t]
698reflectBinderQuote q ty unq (GHole _ t)
699 = reflCall "GHole" [Var ty, q unq t]
700reflectBinderQuote q ty unq (Guess x y)
701 = reflCall "Guess" [Var ty, q unq x, q unq y]
702reflectBinderQuote q ty unq (PVar t)
703 = reflCall "PVar" [Var ty, q unq t]
704reflectBinderQuote q ty unq (PVTy t)
705 = reflCall "PVTy" [Var ty, q unq t]
707mkList :: Raw -> [Raw] -> Raw
708mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
709mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
710 x)
711 (mkList ty xs)
713reflectConstant :: Const -> Raw
714reflectConstant c@(I _) = reflCall "I" [RConstant c]
715reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
716reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
717reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
718reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
719reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
720reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
721reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
722reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
723reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
724reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
725reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
726reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
727reflectConstant StrType = Var (reflm "StrType")
728reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
729reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
730reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
731reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
732reflectConstant VoidType = Var (reflm "VoidType")
733reflectConstant Forgot = Var (reflm "Forgot")
734reflectConstant WorldType = Var (reflm "WorldType")
735reflectConstant TheWorld = Var (reflm "TheWorld")
737reflectUExp :: UExp -> Raw
738reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
739reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
741-- | Reflect the environment of a proof into a List (TTName, Binder TT)
742reflectEnv :: Env -> Raw
743reflectEnv = foldr consToEnvList emptyEnvList
744 where
745 consToEnvList :: (Name, Binder Term) -> Raw -> Raw
746 consToEnvList (n, b) l
747 = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
748 [ envTupleType
749 , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
750 , (RApp (Var $ reflm "Binder")
751 (Var $ reflm "TT"))
752 , reflectName n
753 , reflectBinder b
754 ]
755 , l
756 ]
758 emptyEnvList :: Raw
759 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
760 [envTupleType]
762-- | Reflect an error into the internal datatype of Idris -- TODO
763rawBool :: Bool -> Raw
764rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
765rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
767rawNil :: Raw -> Raw
768rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
770rawCons :: Raw -> Raw -> Raw -> Raw
771rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
773rawList :: Raw -> [Raw] -> Raw
774rawList ty = foldr (rawCons ty) (rawNil ty)
776rawPairTy :: Raw -> Raw -> Raw
777rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
779rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
780rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
782reflectCtxt :: [(Name, Type)] -> Raw
783reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
784 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
785 (reflectName n, reflect t)))
786 ctxt)
788reflectErr :: Err -> Raw
789reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
790reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
791reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =
792 raw_apply (Var $ reflErrName "CantUnify")
793 [ rawBool b
794 , reflect t1
795 , reflect t2
796 , reflectErr e
797 , reflectCtxt ctxt
798 , RConstant (I i)]
799reflectErr (InfiniteUnify n tm ctxt) =
800 raw_apply (Var $ reflErrName "InfiniteUnify")
801 [ reflectName n
802 , reflect tm
803 , reflectCtxt ctxt
804 ]
805reflectErr (CantConvert t t' ctxt) =
806 raw_apply (Var $ reflErrName "CantConvert")
807 [ reflect t
808 , reflect t'
809 , reflectCtxt ctxt
810 ]
811reflectErr (CantSolveGoal t ctxt) =
812 raw_apply (Var $ reflErrName "CantSolveGoal")
813 [ reflect t
814 , reflectCtxt ctxt
815 ]
816reflectErr (UnifyScope n n' t ctxt) =
817 raw_apply (Var $ reflErrName "UnifyScope")
818 [ reflectName n
819 , reflectName n'
820 , reflect t
821 , reflectCtxt ctxt
822 ]
823reflectErr (CantInferType str) =
824 raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
825reflectErr (NonFunctionType t t') =
826 raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
827reflectErr (NotEquality t t') =
828 raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
829reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
830reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
831reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
832reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
833reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
834reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
835reflectErr (NotInjective t1 t2 t3) =
836 raw_apply (Var $ reflErrName "NotInjective")
837 [ reflect t1
838 , reflect t2
839 , reflect t3
840 ]
841reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
842reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
843reflectErr (CantResolveAlts ss) =
844 raw_apply (Var $ reflErrName "CantResolveAlts")
845 [rawList (Var $ reflm "TTName") (map reflectName ss)]
846reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
847reflectErr (NoEliminator str t)
848 = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),
849 reflect t]
850reflectErr (UniverseError fc ue old new tys) =
851 -- NB: loses information, but OK because this is not likely to be rewritten
852 Var $ reflErrName "UniverseError"
853reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
854reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
855reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
856reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
857reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
858reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
859reflectErr (ProviderError str) =
860 raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
861reflectErr (LoadingFailed str err) =
862 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
863reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
865-- | Reflect a file context
866reflectFC :: FC -> Raw
867reflectFC fc = raw_apply (Var (reflm "FileLoc"))
868 [ RConstant (Str (fc_fname fc))
869 , raw_apply (Var pairCon) $
870 [intTy, intTy] ++
871 map (RConstant . I)
872 [ fst (fc_start fc)
873 , snd (fc_start fc)
874 ]
875 , raw_apply (Var pairCon) $
876 [intTy, intTy] ++
877 map (RConstant . I)
878 [ fst (fc_end fc)
879 , snd (fc_end fc)
880 ]
881 ]
882 where intTy = RConstant (AType (ATInt ITNative))
884fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
885fromTTMaybe (App _ (App _ (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
886 | just == txt "Just" = Just tm
887fromTTMaybe x = Nothing
889reflErrName :: String -> Name
890reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
892-- | Attempt to reify a report part from TT to the internal
893-- representation. Not in Idris or ElabD monads because it should be usable
894-- from either.
895reifyReportPart :: Term -> Either Err ErrorReportPart
896reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
897 Right (TextPart msg)
898reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
899 | n == reflm "NamePart" =
900 case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext emptyContext Erased) of
901 Error e -> Left . InternalMsg $
902 "could not reify name term " ++
903 show ttn ++
904 " when reflecting an error:" ++ show e
905 OK (n', _)-> Right $ NamePart n'
906reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
907 | n == reflm "TermPart" =
908 case runElab initEState (reifyTT tm) (initElaborator NErased initContext emptyContext Erased) of
909 Error e -> Left . InternalMsg $
910 "could not reify reflected term " ++
911 show tm ++
912 " when reflecting an error:" ++ show e
913 OK (tm', _) -> Right $ TermPart tm'
914reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
915 | n == reflm "SubReport" =
916 case unList tm of
917 Just xs -> do subParts <- mapM reifyReportPart xs
918 Right (SubReport subParts)
919 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
920reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
922reifyTyDecl :: Term -> ElabD RTyDecl
923reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
924 | n == tacN "Declare" =
925 do tyN' <- reifyTTName tyN
926 args' <- case unList args of
927 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
928 Just xs -> mapM reifyRArg xs
929 ret' <- reifyRaw ret
930 return $ RDeclare tyN' args' ret'
931 where reifyRArg :: Term -> ElabD RArg
932 reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)
933 | n == tacN "Explicit" = liftM2 RExplicit
934 (reifyTTName argN)
935 (reifyRaw argTy)
936 | n == tacN "Implicit" = liftM2 RImplicit
937 (reifyTTName argN)
938 (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint
939 (reifyTTName argN)
940 (reifyRaw argTy)
941 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
942reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
944reifyFunDefn :: Term -> ElabD RFunDefn
945reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)
946 | n == tacN "DefineFun" =
947 do fnN' <- reifyTTName fnN
948 clauses' <- case unList clauses of
949 Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
950 Just cs -> mapM reifyC cs
951 return $ RDefineFun fnN' clauses'
952 where reifyC :: Term -> ElabD RFunClause
953 reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)
954 | n == tacN "MkFunClause" = liftM2 RMkFunClause
955 (reifyRaw lhs)
956 (reifyRaw rhs)
957 reifyC (App _ (P (DCon _ _ _) n _) lhs)
958 | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs
959 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
960reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
962envTupleType :: Raw
963envTupleType
964 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
965 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
966 ]
968-- | Build the reflected datatype definition(s) that correspond(s) to
969-- a provided unqualified name
970buildDatatypes :: Context -> Ctxt TypeInfo -> Name -> [RDatatype]
971buildDatatypes ctxt datatypes n =
972 catMaybes [ mkDataType dn ti
973 | (dn, ti) <- lookupCtxtName n datatypes
974 ]
975 where mkDataType name (TI {param_pos = params, con_names = constrs}) =
976 do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
977 let (tcargs, tcres) = getArgs params (forget ty) 0
978 conTys <- mapM (fmap forget . flip lookupTyExact ctxt) constrs
979 return $ RDatatype name tcargs tcres $ zip constrs conTys
981 getArgs params (RBind an (Pi _ ty _) body) i =
982 let (args, res) = getArgs params body (i+1)
983 in if i `elem` params
984 then (RParameter an ty : args, res )
985 else (RIndex an ty : args, res)
986 getArgs _ tm _ = ([], tm)
988reflectDatatype :: RDatatype -> Raw
989reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
990 raw_apply (Var $ tacN "MkDatatype") [ reflectName tyn
991 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
992 , reflectRaw tyConRes
993 , rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "Raw"))
994 [ rawPair ((Var $ reflm "TTName"), (Var $ reflm "Raw"))
995 (reflectName cn, reflectRaw cty)
996 | (cn, cty) <- constrs
997 ]
998 ]
999 where reflectConArg (RParameter n t) =
1000 raw_apply (Var $ tacN "Parameter") [reflectName n, reflectRaw t]
1001 reflectConArg (RIndex n t) =
1002 raw_apply (Var $ tacN "Index") [reflectName n, reflectRaw t]