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