@@ -1,6 +1,6 @@
1−{-# LANGUAGE PatternGuards, ViewPatterns #-}
1+{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3−module Idris.ElabTerm where
3+module Idris.Elab.Term where
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6import Idris.AbsSyntaxTree
6import Idris.AbsSyntaxTree
@@ -10,11 +10,13 @@ import Idris.Error
10import Idris.ProofSearch
10import Idris.ProofSearch
11import Idris.Output (pshow)
11import Idris.Output (pshow)
13+import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)
13import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.TT
15import Idris.Core.TT
15import Idris.Core.Evaluate
16import Idris.Core.Evaluate
16import Idris.Core.Unify
17import Idris.Core.Unify
17−import Idris.Core.Typecheck (check, recheck)
18+import Idris.Core.Typecheck (check, recheck, isType)
19+import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)
18import Idris.ErrReverse (errReverse)
20import Idris.ErrReverse (errReverse)
19import Idris.ElabQuasiquote (extractUnquotes)
21import Idris.ElabQuasiquote (extractUnquotes)
20import Idris.Elab.Utils
22import Idris.Elab.Utils
@@ -26,7 +28,7 @@ import Control.Monad
26import Control.Monad.State.Strict
28import Control.Monad.State.Strict
27import Data.List
29import Data.List
28import qualified Data.Map as M
30import qualified Data.Map as M
29−import Data.Maybe (mapMaybe, fromMaybe)
31+import Data.Maybe (mapMaybe, fromMaybe, catMaybes)
30import qualified Data.Set as S
32import qualified Data.Set as S
31import qualified Data.Text as T
33import qualified Data.Text as T
@@ -35,6 +37,7 @@ import Debug.Trace
35data ElabMode = ETyDecl | ELHS | ERHS
37data ElabMode = ETyDecl | ELHS | ERHS
36 deriving Eq
38 deriving Eq
38data ElabResult =
41data ElabResult =
39 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
42 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
40 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
43 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
@@ -43,23 +46,10 @@ data ElabResult =
43 -- ^ Deferred declarations as the meaning of case blocks
46 -- ^ Deferred declarations as the meaning of case blocks
44 , resultContext :: Context
47 , resultContext :: Context
45 -- ^ The potentially extended context from new definitions
48 -- ^ The potentially extended context from new definitions
46− , resultTyDecls :: [(Name, FC, [PArg], Type)]
49+ , resultTyDecls :: [RDeclInstructions]
47 -- ^ Meta-info about the new type declarations
50 -- ^ Meta-info about the new type declarations
50−processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()
51−processTacticDecls info =
52− forM_ info $ \(n, fc, impls, ty) ->
53− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
54− logLvl 3 $ " It has impls " ++ show impls
55− updateIState $ \i -> i { idris_implicits =
56− addDef n impls (idris_implicits i) }
58− ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]
60− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
64-- Using the elaborator, convert a term in raw syntax to a fully
54-- Using the elaborator, convert a term in raw syntax to a fully
65-- elaborated, typechecked term.
55-- elaborated, typechecked term.
@@ -122,11 +112,11 @@ build ist info emode opts fn tm
122 update_term orderPats)
112 update_term orderPats)
123 EState is _ impls <- getAux
113 EState is _ impls <- getAux
124 tt <- get_term
114 tt <- get_term
125− let (tm, ds) = runState (collectDeferred (Just fn) tt) []
127 ctxt <- get_context
115 ctxt <- get_context
116+ let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
128− if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
118+ if (log /= "") then trace log $ return (ElabResult tm ds (map snd is) ctxt impls)
129− else return (ElabResult tm ds is ctxt impls)
119+ else return (ElabResult tm ds (map snd is) ctxt impls)
130 where pattern = emode == ELHS
120 where pattern = emode == ELHS
131 tydecl = emode == ETyDecl
121 tydecl = emode == ETyDecl
@@ -164,11 +154,11 @@ buildTC ist info emode opts fn tm
164 lift (Error (CantMatch (getInferTerm tm)))
154 lift (Error (CantMatch (getInferTerm tm)))
165 EState is _ impls <- getAux
155 EState is _ impls <- getAux
166 tt <- get_term
156 tt <- get_term
167− let (tm, ds) = runState (collectDeferred (Just fn) tt) []
169 ctxt <- get_context
157 ctxt <- get_context
158+ let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
170− if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
160+ if (log /= "") then trace log $ return (ElabResult tm ds (map snd is) ctxt impls)
171− else return (ElabResult tm ds is ctxt impls)
161+ else return (ElabResult tm ds (map snd is) ctxt impls)
172 where pattern = emode == ELHS
162 where pattern = emode == ELHS
174-- return whether arguments of the given constructor name can be
164-- return whether arguments of the given constructor name can be
@@ -213,7 +203,7 @@ goal_polymorphic =
214-- | Returns the set of declarations we need to add to complete the
204-- | Returns the set of declarations we need to add to complete the
215-- definition (most likely case blocks to elaborate) as well as
205-- definition (most likely case blocks to elaborate) as well as
216−-- declarations resulting from user tactic scripts (%runTactics)
206+-- declarations resulting from user tactic scripts (%runElab)
217elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
207elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
219elab ist info emode opts fn tm
209elab ist info emode opts fn tm
@@ -262,9 +252,7 @@ elab ist info emode opts fn tm
262 -- normally correct to call elabE - the ones that don't are desugarings
252 -- normally correct to call elabE - the ones that don't are desugarings
263 -- typically
253 -- typically
264 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
254 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
265− elabE ina fc' t =
255+ elabE ina fc' t =
267− --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
268 do solved <- get_recents
256 do solved <- get_recents
269 as <- get_autos
257 as <- get_autos
270 -- If any of the autos use variables which have recently been solved,
258 -- If any of the autos use variables which have recently been solved,
@@ -430,7 +418,7 @@ elab ist info emode opts fn tm
430 [pimp (sMN 0 "a") t False,
418 [pimp (sMN 0 "a") t False,
431 pimp (sMN 0 "P") Placeholder True,
419 pimp (sMN 0 "P") Placeholder True,
432 pexp l, pexp r])
420 pexp l, pexp r])
433− elab' ina fc (PAlternative True as)
421+ elab' ina fc (PAlternative True as)
434 = do hnf_compute
422 = do hnf_compute
435 ty <- goal
423 ty <- goal
436 ctxt <- get_context
424 ctxt <- get_context
@@ -953,7 +941,7 @@ elab ist info emode opts fn tm
953 (caseBlock fc cname'
941 (caseBlock fc cname'
954 (map (isScr scr) (reverse args')) opts)
942 (map (isScr scr) (reverse args')) opts)
955 -- elaborate case
943 -- elaborate case
956− updateAux (\e -> e { case_decls = newdef : case_decls e } )
944+ updateAux (\e -> e { case_decls = (cname', newdef) : case_decls e } )
957 -- if we haven't got the type yet, hopefully we'll get it later!
945 -- if we haven't got the type yet, hopefully we'll get it later!
958 movelast tyn
946 movelast tyn
@@ -967,7 +955,7 @@ elab ist info emode opts fn tm
969 inApp (P _ n _) = [n]
957 inApp (P _ n _) = [n]
970− inApp (App f a) = inApp f ++ inApp a
958+ inApp (App _ f a) = inApp f ++ inApp a
971 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
959 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
972 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc
960 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc
973 inApp (Bind n b sc) = inApp sc
961 inApp (Bind n b sc) = inApp sc
@@ -1012,9 +1000,10 @@ elab ist info emode opts fn tm
1012 -- Save the old state - we need a fresh proof state to avoid
1000 -- Save the old state - we need a fresh proof state to avoid
1013 -- capturing lexically available variables in the quoted term.
1001 -- capturing lexically available variables in the quoted term.
1014 ctxt <- get_context
1002 ctxt <- get_context
1003+ datatypes <- get_datatypes
1015 saveState
1004 saveState
1016 updatePS (const .
1005 updatePS (const .
1017− newProof (sMN 0 "q") ctxt $
1006+ newProof (sMN 0 "q") ctxt datatypes $
1018 P Ref (reflm "TT") Erased)
1007 P Ref (reflm "TT") Erased)
1020 -- Re-add the unquotes, letting Idris infer the (fictional)
1009 -- Re-add the unquotes, letting Idris infer the (fictional)
@@ -1085,6 +1074,17 @@ elab ist info emode opts fn tm
1087 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
1076 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
1077+ elab' ina fc (PQuoteName n) =
1078+ do ctxt <- get_context
1080+ case lookup n env of
1081+ Just _ -> do fill $ reflectName n ; solve
1083+ case lookupNameDef n ctxt of
1084+ [(n', _)] -> do fill $ reflectName n'
1086+ [] -> lift . tfail . NoSuchVariable $ n
1087+ more -> lift . tfail . CantResolveAlts $ map fst more
1088 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
1088 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
1089 elab' ina fc (PHidden t)
1089 elab' ina fc (PHidden t)
1090 | reflection = elab' ina fc t
1090 | reflection = elab' ina fc t
@@ -1100,11 +1100,13 @@ elab ist info emode opts fn tm
1100 delayElab $ do focus h
1100 delayElab $ do focus h
1102 elab' ina fc t
1102 elab' ina fc t
1103− elab' ina fc (PRunTactics fc' tm) =
1103+ elab' ina fc (PRunElab fc' tm) =
1104 do attack
1104 do attack
1105 n <- getNameFrom (sMN 0 "tacticScript")
1105 n <- getNameFrom (sMN 0 "tacticScript")
1106 n' <- getNameFrom (sMN 0 "tacticExpr")
1106 n' <- getNameFrom (sMN 0 "tacticExpr")
1107− let scriptTy = RApp (Var (sNS (sUN "Tactical") ["Tactical", "Reflection", "Language"])) (Var unitTy)
1107+ let scriptTy = RApp (Var (sNS (sUN "Elab")
1108+ ["Elab", "Reflection", "Language"]))
1108 claim n scriptTy
1110 claim n scriptTy
1109 movelast n
1111 movelast n
1110 letbind n' scriptTy (Var n)
1112 letbind n' scriptTy (Var n)
@@ -1112,11 +1114,10 @@ elab ist info emode opts fn tm
1112 elab' ina (Just fc') tm
1114 elab' ina (Just fc') tm
1113 env <- get_env
1115 env <- get_env
1114 runTactical (maybe fc' id fc) env (P Bound n' Erased)
1116 runTactical (maybe fc' id fc) env (P Bound n' Erased)
1115− EState _ _ todo <- getAux
1117 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
1118 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
1119− delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
1120+ delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
1121 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
1122 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
1122 isScr (PRef _ n) (n', b) = (n', (n == n', b))
1123 isScr (PRef _ n) (n', b) = (n', (n == n', b))
@@ -1378,7 +1379,7 @@ pruneByType _ t _ as = as
1379findInstances :: IState -> Term -> [Name]
1380findInstances :: IState -> Term -> [Name]
1380findInstances ist t
1381findInstances ist t
1381− | (P _ n _, _) <- unApply t
1382+ | (P _ n _, _) <- unApply (getRetTy t)
1382 = case lookupCtxt n (idris_classes ist) of
1383 = case lookupCtxt n (idris_classes ist) of
1383 [CI _ _ _ _ _ ins _] -> filter accessible ins
1384 [CI _ _ _ _ _ ins _] -> filter accessible ins
@@ -1429,17 +1430,17 @@ resTC' tcs defaultOn topholes depth topg fn ist
1429 = do compute
1430 = do compute
1430 g <- goal
1431 g <- goal
1431 let argsok = tcArgsOK g topholes
1432 let argsok = tcArgsOK g topholes
1432−-- trace (show (g,hs,argsok,topholes)) $
1433 if not argsok -- && not mvok)
1433 if not argsok -- && not mvok)
1434 then lift $ tfail $ CantResolve True topg
1434 then lift $ tfail $ CantResolve True topg
1436 ptm <- get_term
1436 ptm <- get_term
1437 ulog <- getUnifyLog
1437 ulog <- getUnifyLog
1438 hs <- get_holes
1438 hs <- get_holes
1439− traceWhen ulog ("Resolving class " ++ show g) $
1440+ traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env) $
1440 try' (trivial' ist)
1441 try' (trivial' ist)
1441 (do t <- goal
1442 (do t <- goal
1442− let (tc, ttypes) = unApply t
1443+ let (tc, ttypes) = unApply (getRetTy t)
1443 scopeOnly <- needsDefault t tc ttypes
1444 scopeOnly <- needsDefault t tc ttypes
1444 let stk = elab_stack ist
1445 let stk = elab_stack ist
1445 let insts_in = findInstances ist t
1446 let insts_in = findInstances ist t
@@ -1449,10 +1450,10 @@ resTC' tcs defaultOn topholes depth topg fn ist
1449 let depth' = if scopeOnly then 2 else depth
1450 let depth' = if scopeOnly then 2 else depth
1450 blunderbuss t depth' stk (stk ++ insts)) True
1451 blunderbuss t depth' stk (stk ++ insts)) True
1452− tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn
1453+ tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn
1454 tcArgsOK ty hs -- if any arguments are metavariables, postpone
1455 tcArgsOK ty hs -- if any arguments are metavariables, postpone
1455− = let (f, as) = unApply ty in
1456+ = let (f, as) = unApply (getRetTy ty) in
1456 case f of
1457 case f of
1457 P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of
1458 P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of
1458 Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as
1459 Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as
@@ -1469,7 +1470,7 @@ resTC' tcs defaultOn topholes depth topg fn ist
1469 isMeta _ _ = False
1470 isMeta _ _ = False
1471 notHole hs (P _ n _, c)
1472 notHole hs (P _ n _, c)
1472− | (P _ cn _, _) <- unApply c,
1473+ | (P _ cn _, _) <- unApply (getRetTy c),
1473 n `elem` hs && isConName cn (tt_ctxt ist) = False
1474 n `elem` hs && isConName cn (tt_ctxt ist) = False
1474 | Constant _ <- c = not (n `elem` hs)
1475 | Constant _ <- c = not (n `elem` hs)
1475 notHole _ _ = True
1476 notHole _ _ = True
@@ -1510,11 +1511,22 @@ resTC' tcs defaultOn topholes depth topg fn ist
1510 _ -> blunderbuss t d stk ns)
1511 _ -> blunderbuss t d stk ns)
1511 | otherwise = blunderbuss t d stk ns
1512 | otherwise = blunderbuss t d stk ns
1514+ introImps = do g <- goal
1516+ (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing
1521+ solven 0 = return ()
1522+ solven n = do solve; solven (n - 1)
1513 resolve n depth
1524 resolve n depth
1514 | depth == 0 = fail $ "Can't resolve type class"
1525 | depth == 0 = fail $ "Can't resolve type class"
1515 | otherwise
1526 | otherwise
1527+ = do lams <- introImps
1516− = do t <- goal
1528+ t <- goal
1517− let (tc, ttypes) = unApply t
1529+ let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)
1518-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
1530-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
1519-- else do
1531-- else do
1520 -- if there's a hole in the goal, don't even try
1532 -- if there's a hole in the goal, don't even try
@@ -1526,14 +1538,15 @@ resTC' tcs defaultOn topholes depth topg fn ist
1526 tm <- get_term
1538 tm <- get_term
1527 args <- map snd <$> try' (apply (Var n) imps)
1539 args <- map snd <$> try' (apply (Var n) imps)
1528 (match_apply (Var n) imps) True
1540 (match_apply (Var n) imps) True
1541+ solven lams -- close any implicit lambdas we introduced
1529 ps' <- get_probs
1542 ps' <- get_probs
1530 when (length ps < length ps' || unrecoverable ps') $
1543 when (length ps < length ps' || unrecoverable ps') $
1531 fail "Can't apply type class"
1544 fail "Can't apply type class"
1532-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
1545-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
1533 mapM_ (\ (_,n) -> do focus n
1546 mapM_ (\ (_,n) -> do focus n
1534 t' <- goal
1547 t' <- goal
1535− let (tc', ttype) = unApply t'
1548+ let (tc', ttype) = unApply (getRetTy t')
1536− let got = fst (unApply t)
1549+ let got = fst (unApply (getRetTy t))
1537 let depth' = if tc' `elem` tcs
1550 let depth' = if tc' `elem` tcs
1538 then depth - 1 else depth
1551 then depth - 1 else depth
1539 resTC' (got : tcs) defaultOn topholes depth' topg fn ist)
1552 resTC' (got : tcs) defaultOn topholes depth' topg fn ist)
@@ -1546,23 +1559,49 @@ resTC' tcs defaultOn topholes depth topg fn ist
1546 where isImp (PImp p _ _ _ _) = (True, p)
1559 where isImp (PImp p _ _ _ _) = (True, p)
1547 isImp arg = (False, priority arg)
1560 isImp arg = (False, priority arg)
1549−collectDeferred :: Maybe Name ->
1562+collectDeferred :: Maybe Name -> [Name] -> Context ->
1550 Term -> State [(Name, (Int, Maybe Name, Type))] Term
1563 Term -> State [(Name, (Int, Maybe Name, Type))] Term
1551−collectDeferred top (Bind n (GHole i t) app) =
1564+collectDeferred top casenames ctxt (Bind n (GHole i t) app) =
1552 do ds <- get
1565 do ds <- get
1553− t' <- collectDeferred top t
1566+ t' <- collectDeferred top casenames ctxt t
1554− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])
1567+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t'))])
1555− collectDeferred top app
1568+ collectDeferred top casenames ctxt app
1570+ -- Evaluate the top level functions in arguments, if possible, and if it's
1571+ -- not a name we're immediately going to define in a case block, so that
1572+ -- any immediate specialisation of the function applied to constructors
1574+ tidyArg env (Bind n b@(Pi im t k) sc)
1575+ = Bind n (Pi im (tidy ctxt env t) k)
1576+ (tidyArg ((n, b) : env) sc)
1579+ tidy ctxt env t | (f, args) <- unApply t,
1580+ P _ specn _ <- getFn f,
1581+ n `notElem` casenames
1582+ = fst $ specialise ctxt env [(specn, 99999)] t
1583+ tidy ctxt env t@(Bind n (Let _ _) sct)
1584+ | (f, args) <- unApply sct,
1585+ P _ specn _ <- getFn f,
1586+ n `notElem` casenames
1587+ = fst $ specialise ctxt env [(specn, 99999)] t
1588+ tidy ctxt env t = t
1590+ getFn (Bind n (Lam _) t) = getFn t
1591+ getFn t | (f, a) <- unApply t = f
1556−collectDeferred top (Bind n b t) = do b' <- cdb b
1593+collectDeferred top ns ctxt (Bind n b t)
1557− t' <- collectDeferred top t
1595+ t' <- collectDeferred top ns ctxt t
1558− return (Bind n b' t')
1596+ return (Bind n b' t')
1560− cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v)
1598+ cdb (Let t v) = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
1561− cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)
1599+ cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
1562− cdb b = do ty' <- collectDeferred top (binderTy b)
1600+ cdb b = do ty' <- collectDeferred top ns ctxt (binderTy b)
1563 return (b { binderTy = ty' })
1601 return (b { binderTy = ty' })
1564−collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)
1602+collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f)
1603+ (collectDeferred top ns ctxt a)
1565−collectDeferred top t = return t
1604+collectDeferred top ns ctxt t = return t
1567case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
1606case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
1568case_ ind autoSolve ist fn tm = do
1607case_ ind autoSolve ist fn tm = do
@@ -1582,8 +1621,6 @@ case_ ind autoSolve ist fn tm = do
1582 else casetac (forget val)
1621 else casetac (forget val)
1583 when autoSolve solveAll
1622 when autoSolve solveAll
1585−tacN :: String -> Name
1586−tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1588runTactical :: FC -> Env -> Term -> ElabD ()
1625runTactical :: FC -> Env -> Term -> ElabD ()
1589runTactical fc env tm = do tm' <- eval tm
1626runTactical fc env tm = do tm' <- eval tm
@@ -1591,10 +1628,50 @@ runTactical fc env tm = do tm' <- eval tm
1591 return ()
1628 return ()
1593 eval tm = do ctxt <- get_context
1630 eval tm = do ctxt <- get_context
1594 return $ normaliseAll ctxt env (finalise tm)
1632 return $ normaliseAll ctxt env (finalise tm)
1596 returnUnit = fmap fst $ get_type_val (Var unitCon)
1634 returnUnit = fmap fst $ get_type_val (Var unitCon)
1636+ patvars :: [Name] -> Term -> ([Name], Term)
1637+ patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)
1638+ patvars ns tm = (ns, tm)
1640+ pullVars :: (Term, Term) -> ([Name], Term, Term)
1641+ pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
1643+ defineFunction :: RFunDefn -> ElabD ()
1644+ defineFunction (RDefineFun n clauses) =
1645+ do ctxt <- get_context
1646+ ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
1647+ let info = CaseInfo True True False -- TODO document and figure out
1648+ clauses' <- forM clauses (\case
1649+ RMkFunClause lhs rhs ->
1650+ do lhs' <- fmap fst . lift $ check ctxt [] lhs
1651+ rhs' <- fmap fst . lift $ check ctxt [] rhs
1652+ return $ Right (lhs', rhs')
1653+ RMkImpossibleClause lhs ->
1654+ do lhs' <- fmap fst . lift $ check ctxt [] lhs
1655+ return $ Left lhs')
1656+ let clauses'' = map (\case Right c -> pullVars c
1657+ Left lhs -> let (ns, lhs') = patvars [] lhs'
1658+ in (ns, lhs', Impossible))
1661+ addCasedef n (const [])
1662+ info False (STerm Erased)
1663+ True False -- TODO what are these?
1664+ (map snd $ getArgTys ty) [] -- TODO inaccessible types
1672+ updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
1598 -- | Do a step in the reflected elaborator monad. The input is the
1675 -- | Do a step in the reflected elaborator monad. The input is the
1599 -- step, the output is the (reflected) term returned.
1676 -- step, the output is the (reflected) term returned.
1600 runTacTm :: Term -> ElabD Term
1677 runTacTm :: Term -> ElabD Term
@@ -1623,6 +1700,35 @@ runTactical fc env tm = do tm' <- eval tm
1623 else fmap fst . get_type_val $
1700 else fmap fst . get_type_val $
1624 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1701 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1625 (Var (reflm "TT"))
1702 (Var (reflm "TT"))
1703+ | n == tacN "prim__LookupTy", [n] <- args
1704+ = do n' <- reifyTTName n
1705+ ctxt <- get_context
1706+ let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
1707+ TyDecl nt ty -> (nt, ty)
1708+ Operator ty _ _ -> (Ref, ty)
1709+ CaseOp _ ty _ _ _ _ -> (Ref, ty)
1710+ -- Idris tuples nest to the right
1711+ reflectTriple (x, y, z) =
1712+ raw_apply (Var pairCon) [ Var (reflm "TTName")
1713+ , raw_apply (Var pairTy) [Var (reflm "NameType"), Var (reflm "TT")]
1715+ , raw_apply (Var pairCon) [ Var (reflm "NameType"), Var (reflm "TT")
1717+ let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty)
1718+ | (n, def) <- lookupNameDef n' ctxt
1719+ , let (nt, ty) = getNameTypeAndType def ]
1720+ fmap fst . get_type_val $
1721+ rawList (raw_apply (Var pairTy) [ Var (reflm "TTName")
1722+ , raw_apply (Var pairTy) [ Var (reflm "NameType")
1723+ , Var (reflm "TT")]])
1725+ | n == tacN "prim__LookupDatatype", [name] <- args
1726+ = do n' <- reifyTTName name
1727+ datatypes <- get_datatypes
1728+ ctxt <- get_context
1729+ fmap fst . get_type_val $
1730+ rawList (Var (tacN "Datatype"))
1731+ (map reflectDatatype (buildDatatypes ctxt datatypes n'))
1626 | n == tacN "prim__SourceLocation", [] <- args
1732 | n == tacN "prim__SourceLocation", [] <- args
1627 = fmap fst . get_type_val $
1733 = fmap fst . get_type_val $
1628 reflectFC fc
1734 reflectFC fc
@@ -1633,19 +1739,23 @@ runTactical fc env tm = do tm' <- eval tm
1633 = do errs' <- eval errs
1739 = do errs' <- eval errs
1634 parts <- reifyReportParts errs'
1740 parts <- reifyReportParts errs'
1635 lift . tfail $ ReflectionError [parts] (Msg "")
1741 lift . tfail $ ReflectionError [parts] (Msg "")
1636− | n == tacN "prim__PureTactical", [_a, tm] <- args
1742+ | n == tacN "prim__PureElab", [_a, tm] <- args
1637 = return tm
1743 = return tm
1638− | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1744+ | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args
1639 = do first' <- eval first
1745 = do first' <- eval first
1640− res <- runTacTm first'
1746+ res <- eval =<< runTacTm first'
1641− next <- eval (App andThen res)
1747+ next <- eval (App Complete andThen res)
1642 runTacTm next
1748 runTacTm next
1643 | n == tacN "prim__Try", [_a, first, alt] <- args
1749 | n == tacN "prim__Try", [_a, first, alt] <- args
1644 = do first' <- eval first
1750 = do first' <- eval first
1645 alt' <- eval alt
1751 alt' <- eval alt
1646 try' (runTacTm first') (runTacTm alt') True
1752 try' (runTacTm first') (runTacTm alt') True
1647 | n == tacN "prim__Fill", [raw] <- args
1753 | n == tacN "prim__Fill", [raw] <- args
1648− = do raw' <- reifyRaw raw
1754+ = do raw' <- reifyRaw =<< eval raw
1757+ | n == tacN "prim__Apply", [raw] <- args
1758+ = do raw' <- reifyRaw =<< eval raw
1649 apply raw' []
1759 apply raw' []
1650 returnUnit
1760 returnUnit
1651 | n == tacN "prim__Gensym", [hint] <- args
1761 | n == tacN "prim__Gensym", [hint] <- args
@@ -1662,7 +1772,7 @@ runTactical fc env tm = do tm' <- eval tm
1662 returnUnit
1772 returnUnit
1663 | n == tacN "prim__Forget", [tt] <- args
1773 | n == tacN "prim__Forget", [tt] <- args
1664 = do tt' <- reifyTT tt
1774 = do tt' <- reifyTT tt
1665− fmap fst . get_type_val $ reflect tt'
1775+ fmap fst . get_type_val . reflectRaw $ forget tt'
1666 | n == tacN "prim__Attack", [] <- args
1776 | n == tacN "prim__Attack", [] <- args
1667 = do attack
1777 = do attack
1668 returnUnit
1778 returnUnit
@@ -1684,6 +1794,21 @@ runTactical fc env tm = do tm' <- eval tm
1684 Just name -> fmap Just $ reifyTTName name
1794 Just name -> fmap Just $ reifyTTName name
1686 returnUnit
1796 returnUnit
1797+ | n == tacN "prim__Forall", [n, ty] <- args
1798+ = do n' <- reifyTTName n
1800+ forall n' Nothing ty'
1802+ | n == tacN "prim__PatVar", [n] <- args
1803+ = do n' <- reifyTTName n
1806+ | n == tacN "prim__PatBind", [n] <- args
1807+ = do n' <- reifyTTName n
1810+ | n == tacN "prim__Compute", [] <- args
1811+ = do compute ; returnUnit
1687 | n == tacN "prim__DeclareType", [decl] <- args
1812 | n == tacN "prim__DeclareType", [decl] <- args
1688 = do (RDeclare n args res) <- reifyTyDecl decl
1813 = do (RDeclare n args res) <- reifyTyDecl decl
1689 ctxt <- get_context
1814 ctxt <- get_context
@@ -1693,9 +1818,10 @@ runTactical fc env tm = do tm' <- eval tm
1693 rty = foldr mkPi res args
1818 rty = foldr mkPi res args
1694 (checked, ty') <- lift $ check ctxt [] rty
1819 (checked, ty') <- lift $ check ctxt [] rty
1695 case normaliseAll ctxt [] (finalise ty') of
1820 case normaliseAll ctxt [] (finalise ty') of
1821+ UType _ -> return ()
1822+ TType _ -> return ()
1696− TType _ -> lift . tfail . InternalMsg $
1823+ ty'' -> lift . tfail . InternalMsg $
1697− show checked ++ " is not a type: it's " ++ show ty'
1824+ show checked ++ " is not a type: it's " ++ show ty''
1699 case lookupDefExact n ctxt of
1825 case lookupDefExact n ctxt of
1700 Just _ -> lift . tfail . InternalMsg $
1826 Just _ -> lift . tfail . InternalMsg $
1701 show n ++ " is already defined."
1827 show n ++ " is already defined."
@@ -1703,17 +1829,41 @@ runTactical fc env tm = do tm' <- eval tm
1703 let decl = TyDecl Ref checked
1829 let decl = TyDecl Ref checked
1704 ctxt' = addCtxtDef n decl ctxt
1830 ctxt' = addCtxtDef n decl ctxt
1705 set_context ctxt'
1831 set_context ctxt'
1706− updateAux $ \e -> e { new_tyDecls = (n, fc, map rArgToPArg args, checked) :
1832+ updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rArgToPArg args) checked) :
1707 new_tyDecls e }
1833 new_tyDecls e }
1708 aux <- getAux
1834 aux <- getAux
1709 returnUnit
1835 returnUnit
1836+ | n == tacN "prim__DefineFunction", [decl] <- args
1837+ = do defn <- reifyFunDefn decl
1838+ defineFunction defn
1840+ | n == tacN "prim__RecursiveElab", [goal, script] <- args
1841+ = do goal' <- reifyRaw goal
1842+ ctxt <- get_context
1843+ script <- eval script
1844+ (goalTT, goalTy) <- lift $ check ctxt [] goal'
1845+ lift $ isType ctxt [] goalTy
1846+ recH <- getNameFrom (sMN 0 "recElabHole")
1848+ datatypes <- get_datatypes
1850+ (tm_out, ES (_, aux') _ _) <-
1851+ lift $ runElab aux (runTactical fc env script >> solve >> get_term)
1852+ (newProof recH ctxt datatypes goalTT)
1853+ updateAux $ const aux'
1855+ (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out
1856+ let (tm', ty') = (reflect tm, reflect ty)
1857+ fmap fst . get_type_val $
1858+ rawPair (Var $ reflm "TT", Var $ reflm "TT")
1710 | n == tacN "prim__Debug", [ty, msg] <- args
1860 | n == tacN "prim__Debug", [ty, msg] <- args
1711 = do let msg' = fromTTMaybe msg
1861 = do let msg' = fromTTMaybe msg
1712 case msg' of
1862 case msg' of
1713 Nothing -> debugElaborator Nothing
1863 Nothing -> debugElaborator Nothing
1714 Just (Constant (Str m)) -> debugElaborator (Just m)
1864 Just (Constant (Str m)) -> debugElaborator (Just m)
1715 Just x -> lift . tfail . InternalMsg $ "Can't reify message for debugging: " ++ show x
1865 Just x -> lift . tfail . InternalMsg $ "Can't reify message for debugging: " ++ show x
1716− runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x
1866+ runTacTm x = lift . tfail $ ElabScriptStuck x
1718-- Running tactics directly
1868-- Running tactics directly
1719-- if a tactic adds unification problems, return an error
1869-- if a tactic adds unification problems, return an error
@@ -1968,781 +2118,6 @@ runTac autoSolve ist perhapsFC fn tac
1968 runReflected t = do t' <- reify ist t
2118 runReflected t = do t' <- reify ist t
1969 runTac autoSolve ist perhapsFC fn t'
2119 runTac autoSolve ist perhapsFC fn t'
1971−-- | Prefix a name with the "Language.Reflection" namespace
1972−reflm :: String -> Name
1973−reflm n = sNS (sUN n) ["Reflection", "Language"]
1976−-- | Reify tactics from their reflected representation
1977−reify :: IState -> Term -> ElabD PTactic
1978−reify _ (P _ n _) | n == reflm "Intros" = return Intros
1979−reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
1980−reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
1981−reify _ (P _ n _) | n == reflm "Solve" = return Solve
1982−reify _ (P _ n _) | n == reflm "Compute" = return Compute
1983−reify _ (P _ n _) | n == reflm "Skip" = return Skip
1984−reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
1985−reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
1986−reify ist t@(App _ _)
1987− | (P _ f _, args) <- unApply t = reifyApp ist f args
1988−reify _ t = fail ("Unknown tactic " ++ show t)
1990−reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
1991−reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
1992−reifyApp _ t [Constant (I i)]
1993− | t == reflm "Search" = return (ProofSearch True True i Nothing [])
1995− | t == reflm "Refine" = do n <- reifyTTName x
1996− return $ Refine n []
1997−reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
1999− return $ Claim n' (delab ist goal)
2000−reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
2001−reifyApp ist t [Constant (Str n), x]
2002− | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
2003−reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
2004−reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
2005−reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')
2007− | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
2009− | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
2011− | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
2013− | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
2015− | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
2017− | t == reflm "Focus" = liftM Focus (reifyTTName x)
2019− | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
2020−reifyApp ist t [n, t']
2021− | t == reflm "LetTac" = do n' <- reifyTTName n
2023− return $ LetTac n' (delab ist t')
2024−reifyApp ist t [n, tt', t']
2025− | t == reflm "LetTacTy" = do n' <- reifyTTName n
2026− tt'' <- reifyTT tt'
2028− return $ LetTacTy n' (delab ist tt'') (delab ist t'')
2029−reifyApp ist t [errs]
2030− | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
2031−reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
2033−reifyReportParts :: Term -> ElabD [ErrorReportPart]
2034−reifyReportParts errs =
2035− case unList errs of
2036− Nothing -> fail "Failed to reify errors"
2038− let parts = mapM reifyReportPart errs' in
2040− Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
2044−-- | Reify terms from their reflected representation
2045−reifyTT :: Term -> ElabD Term
2047− | (P _ f _, args) <- unApply t = reifyTTApp f args
2049− | n == reflm "Erased" = return $ Erased
2051− | n == reflm "Impossible" = return $ Impossible
2052−reifyTT t = fail ("Unknown reflection term: " ++ show t)
2054−reifyTTApp :: Name -> [Term] -> ElabD Term
2055−reifyTTApp t [nt, n, x]
2056− | t == reflm "P" = do nt' <- reifyTTNameType nt
2057− n' <- reifyTTName n
2059− return $ P nt' n' x'
2060−reifyTTApp t [Constant (I i)]
2061− | t == reflm "V" = return $ V i
2062−reifyTTApp t [n, b, x]
2063− | t == reflm "Bind" = do n' <- reifyTTName n
2064− b' <- reifyTTBinder reifyTT (reflm "TT") b
2066− return $ Bind n' b' x'
2068− | t == reflm "App" = do f' <- reifyTT f
2072− | t == reflm "TConst" = liftM Constant (reifyTTConst c)
2073−reifyTTApp t [t', Constant (I i)]
2074− | t == reflm "Proj" = do t'' <- reifyTT t'
2075− return $ Proj t'' i
2077− | t == reflm "TType" = liftM TType (reifyTTUExp tt)
2078−reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
2080−-- | Reify raw terms from their reflected representation
2081−reifyRaw :: Term -> ElabD Raw
2082−reifyRaw t@(App _ _)
2083− | (P _ f _, args) <- unApply t = reifyRawApp f args
2084−reifyRaw t@(P _ n _)
2085− | n == reflm "RType" = return $ RType
2086−reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)
2088−reifyRawApp :: Name -> [Term] -> ElabD Raw
2090− | t == reflm "Var" = liftM Var (reifyTTName n)
2091−reifyRawApp t [n, b, x]
2092− | t == reflm "RBind" = do n' <- reifyTTName n
2093− b' <- reifyTTBinder reifyRaw (reflm "Raw") b
2095− return $ RBind n' b' x'
2096−reifyRawApp t [f, x]
2097− | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
2099− | t == reflm "RForce" = liftM RForce (reifyRaw t')
2101− | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
2102−reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
2104−reifyTTName :: Term -> ElabD Name
2106− | (P _ f _, args) <- unApply t = reifyTTNameApp f args
2107−reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
2109−reifyTTNameApp :: Name -> [Term] -> ElabD Name
2110−reifyTTNameApp t [Constant (Str n)]
2111− | t == reflm "UN" = return $ sUN n
2112−reifyTTNameApp t [n, ns]
2113− | t == reflm "NS" = do n' <- reifyTTName n
2114− ns' <- reifyTTNamespace ns
2115− return $ sNS n' ns'
2116−reifyTTNameApp t [Constant (I i), Constant (Str n)]
2117− | t == reflm "MN" = return $ sMN i n
2119− | t == reflm "NErased" = return NErased
2120−reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
2122−reifyTTNamespace :: Term -> ElabD [String]
2123−reifyTTNamespace t@(App _ _)
2124− = case unApply t of
2125− (P _ f _, [Constant StrType])
2126− | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
2127− (P _ f _, [Constant StrType, Constant (Str n), ns])
2128− | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
2129− _ -> fail ("Unknown reflection namespace arg: " ++ show t)
2130−reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
2132−reifyTTNameType :: Term -> ElabD NameType
2133−reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
2134−reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
2135−reifyTTNameType t@(App _ _)
2136− = case unApply t of
2137− (P _ f _, [Constant (I tag), Constant (I num)])
2138− | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!
2139− | f == reflm "TCon" -> return $ TCon tag num
2140− _ -> fail ("Unknown reflection name type: " ++ show t)
2141−reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
2143−reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
2144−reifyTTBinder reificator binderType t@(App _ _)
2145− = case unApply t of
2146− (P _ f _, bt:args) | forget bt == Var binderType
2147− -> reifyTTBinderApp reificator f args
2148− _ -> fail ("Mismatching binder reflection: " ++ show t)
2149−reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
2151−reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
2152−reifyTTBinderApp reif f [t]
2153− | f == reflm "Lam" = liftM Lam (reif t)
2154−reifyTTBinderApp reif f [t, k]
2155− | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)
2156−reifyTTBinderApp reif f [x, y]
2157− | f == reflm "Let" = liftM2 Let (reif x) (reif y)
2158−reifyTTBinderApp reif f [x, y]
2159− | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
2160−reifyTTBinderApp reif f [t]
2161− | f == reflm "Hole" = liftM Hole (reif t)
2162−reifyTTBinderApp reif f [t]
2163− | f == reflm "GHole" = liftM (GHole 0) (reif t)
2164−reifyTTBinderApp reif f [x, y]
2165− | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
2166−reifyTTBinderApp reif f [t]
2167− | f == reflm "PVar" = liftM PVar (reif t)
2168−reifyTTBinderApp reif f [t]
2169− | f == reflm "PVTy" = liftM PVTy (reif t)
2170−reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
2172−reifyTTConst :: Term -> ElabD Const
2173−reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
2174−reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
2175−reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
2176−reifyTTConst t@(App _ _)
2177− | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
2178−reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
2180−reifyTTConstApp :: Name -> Term -> ElabD Const
2181−reifyTTConstApp f aty
2182− | f == reflm "AType" = fmap AType (reifyArithTy aty)
2183−reifyTTConstApp f (Constant c@(I _))
2184− | f == reflm "I" = return $ c
2185−reifyTTConstApp f (Constant c@(BI _))
2186− | f == reflm "BI" = return $ c
2187−reifyTTConstApp f (Constant c@(Fl _))
2188− | f == reflm "Fl" = return $ c
2189−reifyTTConstApp f (Constant c@(I _))
2190− | f == reflm "Ch" = return $ c
2191−reifyTTConstApp f (Constant c@(Str _))
2192− | f == reflm "Str" = return $ c
2193−reifyTTConstApp f (Constant c@(B8 _))
2194− | f == reflm "B8" = return $ c
2195−reifyTTConstApp f (Constant c@(B16 _))
2196− | f == reflm "B16" = return $ c
2197−reifyTTConstApp f (Constant c@(B32 _))
2198− | f == reflm "B32" = return $ c
2199−reifyTTConstApp f (Constant c@(B64 _))
2200− | f == reflm "B64" = return $ c
2201−reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
2203−reifyArithTy :: Term -> ElabD ArithTy
2204−reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
2205−reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
2206−reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
2208−reifyNativeTy :: Term -> ElabD NativeTy
2209−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2210−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2211−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2212−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2213−reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
2215−reifyIntTy :: Term -> ElabD IntTy
2216−reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
2217−reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
2218−reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
2219−reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
2220−reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
2222−reifyTTUExp :: Term -> ElabD UExp
2223−reifyTTUExp t@(App _ _)
2224− = case unApply t of
2225− (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
2226− (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
2227− _ -> fail ("Unknown reflection type universe expression: " ++ show t)
2228−reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
2230−-- | Create a reflected call to a named function/constructor
2231−reflCall :: String -> [Raw] -> Raw
2232−reflCall funName args
2233− = raw_apply (Var (reflm funName)) args
2235−-- | Lift a term into its Language.Reflection.TT representation
2236−reflect :: Term -> Raw
2237−reflect = reflectTTQuote []
2239−-- | Lift a term into its Language.Reflection.Raw representation
2240−reflectRaw :: Raw -> Raw
2241−reflectRaw = reflectRawQuote []
2243−claimTT :: Name -> ElabD Name
2244−claimTT n = do n' <- getNameFrom n
2245− claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
2248−-- | Convert a reflected term to a more suitable form for pattern-matching.
2249−-- In particular, the less-interesting bits are elaborated to _ patterns. This
2250−-- happens to NameTypes, universe levels, names that are bound but not used,
2251−-- and the type annotation field of the P constructor.
2252−reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
2253−reflectTTQuotePattern unq (P _ n _)
2254− | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
2255− do fill (Var n) ; solve
2257− do tyannot <- claimTT (sMN 0 "pTyAnnot")
2258− movelast tyannot -- use a _ pattern here
2259− nt <- getNameFrom (sMN 0 "nt")
2260− claim nt (Var (reflm "NameType"))
2261− movelast nt -- use a _ pattern here
2262− n' <- getNameFrom (sMN 0 "n")
2263− claim n' (Var (reflm "TTName"))
2264− fill $ reflCall "P" [Var nt, Var n', Var tyannot]
2266− focus n'; reflectNameQuotePattern n
2267−reflectTTQuotePattern unq (V n)
2268− = do fill $ reflCall "V" [RConstant (I n)]
2270−reflectTTQuotePattern unq (Bind n b x)
2271− = do x' <- claimTT (sMN 0 "sc")
2273− b' <- getNameFrom (sMN 0 "binder")
2274− claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
2275− (Var (sNS (sUN "TT") ["Reflection", "Language"])))
2276− if n `elem` freeNames x
2277− then do fill $ reflCall "Bind"
2282− else do any <- getNameFrom (sMN 0 "anyName")
2283− claim any (Var (reflm "TTName"))
2285− fill $ reflCall "Bind"
2290− focus x'; reflectTTQuotePattern unq x
2291− focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
2292−reflectTTQuotePattern unq (App f x)
2293− = do f' <- claimTT (sMN 0 "f"); movelast f'
2294− x' <- claimTT (sMN 0 "x"); movelast x'
2295− fill $ reflCall "App" [Var f', Var x']
2297− focus f'; reflectTTQuotePattern unq f
2298− focus x'; reflectTTQuotePattern unq x
2299−reflectTTQuotePattern unq (Constant c)
2300− = do fill $ reflCall "TConst" [reflectConstant c]
2302−reflectTTQuotePattern unq (Proj t i)
2303− = do t' <- claimTT (sMN 0 "t"); movelast t'
2304− fill $ reflCall "Proj" [Var t', RConstant (I i)]
2306− focus t'; reflectTTQuotePattern unq t
2307−reflectTTQuotePattern unq (Erased)
2308− = do erased <- claimTT (sMN 0 "erased")
2310− fill $ (Var erased)
2312−reflectTTQuotePattern unq (Impossible)
2313− = do fill $ Var (reflm "Impossible")
2315−reflectTTQuotePattern unq (TType exp)
2316− = do ue <- getNameFrom (sMN 0 "uexp")
2317− claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
2319− fill $ reflCall "TType" [Var ue]
2321−reflectTTQuotePattern unq (UType u)
2322− = do uH <- getNameFrom (sMN 0 "someUniv")
2323− claim uH (Var (reflm "Universe"))
2325− fill $ reflCall "UType" [Var uH]
2328− fill (Var (reflm (case u of
2329− NullType -> "NullType"
2330− UniqueType -> "UniqueType"
2331− AllTypes -> "AllTypes")))
2334−reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
2335−reflectRawQuotePattern unq (Var n)
2336− -- the unquoted names already have types, just use them
2337− | n `elem` unq = do fill (Var n); solve
2338− | otherwise = do fill (reflCall "Var" [reflectName n]); solve
2339−reflectRawQuotePattern unq (RBind n b sc) =
2340− do scH <- getNameFrom (sMN 0 "sc")
2341− claim scH (Var (reflm "Raw"))
2343− bH <- getNameFrom (sMN 0 "binder")
2344− claim bH (RApp (Var (reflm "Binder"))
2345− (Var (reflm "Raw")))
2346− if n `elem` freeNamesR sc
2347− then do fill $ reflCall "RBind" [reflectName n,
2351− else do any <- getNameFrom (sMN 0 "anyName")
2352− claim any (Var (reflm "TTName"))
2354− fill $ reflCall "RBind" [Var any, Var bH, Var scH]
2356− focus scH; reflectRawQuotePattern unq sc
2357− focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b
2358− where freeNamesR (Var n) = [n]
2359− freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
2360− freeNamesR body \\ [n],
2362− freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
2363− (freeNamesR body \\ [n])
2364− freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
2365− freeNamesR RType = []
2366− freeNamesR (RUType _) = []
2367− freeNamesR (RForce r) = freeNamesR r
2368− freeNamesR (RConstant _) = []
2369−reflectRawQuotePattern unq (RApp f x) =
2370− do fH <- getNameFrom (sMN 0 "f")
2371− claim fH (Var (reflm "Raw"))
2373− xH <- getNameFrom (sMN 0 "x")
2374− claim xH (Var (reflm "Raw"))
2376− fill $ reflCall "RApp" [Var fH, Var xH]
2378− focus fH; reflectRawQuotePattern unq f
2379− focus xH; reflectRawQuotePattern unq x
2380−reflectRawQuotePattern unq RType =
2381− do fill (Var (reflm "RType"))
2383−reflectRawQuotePattern unq (RUType univ) =
2384− do uH <- getNameFrom (sMN 0 "universe")
2385− claim uH (Var (reflm "Universe"))
2387− fill $ reflCall "RUType" [Var uH]
2389− focus uH; fill (reflectUniverse univ); solve
2390−reflectRawQuotePattern unq (RForce r) =
2391− do rH <- getNameFrom (sMN 0 "raw")
2392− claim rH (Var (reflm "Raw"))
2394− fill $ reflCall "RForce" [Var rH]
2396− focus rH; reflectRawQuotePattern unq r
2397−reflectRawQuotePattern unq (RConstant c) =
2398− do cH <- getNameFrom (sMN 0 "const")
2399− claim cH (Var (reflm "Constant"))
2401− fill (reflCall "RConstant" [Var cH]); solve
2403− fill (reflectConstant c); solve
2405−reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()
2406−reflectBinderQuotePattern q unq (Lam t)
2407− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2408− fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
2411−reflectBinderQuotePattern q unq (Pi _ t k)
2412− = do t' <- claimTT (sMN 0 "ty") ; movelast t'
2413− k' <- claimTT (sMN 0 "k"); movelast k';
2414− fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
2417−reflectBinderQuotePattern q unq (Let x y)
2418− = do x' <- claimTT (sMN 0 "ty"); movelast x';
2419− y' <- claimTT (sMN 0 "v"); movelast y';
2420− fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
2424−reflectBinderQuotePattern q unq (NLet x y)
2425− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2426− y' <- claimTT (sMN 0 "v"); movelast y'
2427− fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
2431−reflectBinderQuotePattern q unq (Hole t)
2432− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2433− fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
2436−reflectBinderQuotePattern q unq (GHole _ t)
2437− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2438− fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2441−reflectBinderQuotePattern q unq (Guess x y)
2442− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2443− y' <- claimTT (sMN 0 "v"); movelast y'
2444− fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2448−reflectBinderQuotePattern q unq (PVar t)
2449− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2450− fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2453−reflectBinderQuotePattern q unq (PVTy t)
2454− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2455− fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2459−reflectUniverse :: Universe -> Raw
2461− (Var (reflm (case u of
2462− NullType -> "NullType"
2463− UniqueType -> "UniqueType"
2464− AllTypes -> "AllTypes")))
2466−-- | Create a reflected TT term, but leave refs to the provided name intact
2467−reflectTTQuote :: [Name] -> Term -> Raw
2468−reflectTTQuote unq (P nt n t)
2469− | n `elem` unq = Var n
2470− | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
2471−reflectTTQuote unq (V n)
2472− = reflCall "V" [RConstant (I n)]
2473−reflectTTQuote unq (Bind n b x)
2474− = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]
2475−reflectTTQuote unq (App f x)
2476− = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
2477−reflectTTQuote unq (Constant c)
2478− = reflCall "TConst" [reflectConstant c]
2479−reflectTTQuote unq (Proj t i)
2480− = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
2481−reflectTTQuote unq (Erased) = Var (reflm "Erased")
2482−reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
2483−reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2484−reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
2486−reflectRawQuote :: [Name] -> Raw -> Raw
2487−reflectRawQuote unq (Var n)
2488− | n `elem` unq = Var n
2489− | otherwise = reflCall "Var" [reflectName n]
2490−reflectRawQuote unq (RBind n b r) =
2491− reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]
2492−reflectRawQuote unq (RApp f x) =
2493− reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
2494−reflectRawQuote unq RType = Var (reflm "RType")
2495−reflectRawQuote unq (RUType u) =
2496− reflCall "RUType" [reflectUniverse u]
2497−reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
2498−reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
2500−reflectNameType :: NameType -> Raw
2501−reflectNameType (Bound) = Var (reflm "Bound")
2502−reflectNameType (Ref) = Var (reflm "Ref")
2503−reflectNameType (DCon x y _)
2504− = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!
2505−reflectNameType (TCon x y)
2506− = reflCall "TCon" [RConstant (I x), RConstant (I y)]
2508−reflectName :: Name -> Raw
2510− = reflCall "UN" [RConstant (Str (str s))]
2511−reflectName (NS n ns)
2512− = reflCall "NS" [ reflectName n
2514− raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
2515− [ RConstant StrType, RConstant (Str n), s ])
2516− ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
2517− [ RConstant StrType ])
2520−reflectName (MN i n)
2521− = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
2522−reflectName (NErased) = Var (reflm "NErased")
2523−reflectName n = Var (reflm "NErased") -- special name, not yet implemented
2525−-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
2526−-- MNs corresponding to will care about the string but not the number. All
2528−reflectNameQuotePattern :: Name -> ElabD ()
2529−reflectNameQuotePattern n@(UN s)
2530− = do fill $ reflectName n
2532−reflectNameQuotePattern n@(NS _ _)
2533− = do fill $ reflectName n
2535−reflectNameQuotePattern (MN _ n)
2536− = do i <- getNameFrom (sMN 0 "mnCounter")
2537− claim i (RConstant (AType (ATInt ITNative)))
2539− fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
2541−reflectNameQuotePattern _ -- for all other names, match any
2542− = do nameHole <- getNameFrom (sMN 0 "name")
2543− claim nameHole (Var (reflm "TTName"))
2545− fill (Var nameHole)
2548−reflectBinder :: Binder Term -> Raw
2549−reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []
2551−reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
2552−reflectBinderQuote q ty unq (Lam t)
2553− = reflCall "Lam" [Var ty, q unq t]
2554−reflectBinderQuote q ty unq (Pi _ t k)
2555− = reflCall "Pi" [Var ty, q unq t, q unq k]
2556−reflectBinderQuote q ty unq (Let x y)
2557− = reflCall "Let" [Var ty, q unq x, q unq y]
2558−reflectBinderQuote q ty unq (NLet x y)
2559− = reflCall "NLet" [Var ty, q unq x, q unq y]
2560−reflectBinderQuote q ty unq (Hole t)
2561− = reflCall "Hole" [Var ty, q unq t]
2562−reflectBinderQuote q ty unq (GHole _ t)
2563− = reflCall "GHole" [Var ty, q unq t]
2564−reflectBinderQuote q ty unq (Guess x y)
2565− = reflCall "Guess" [Var ty, q unq x, q unq y]
2566−reflectBinderQuote q ty unq (PVar t)
2567− = reflCall "PVar" [Var ty, q unq t]
2568−reflectBinderQuote q ty unq (PVTy t)
2569− = reflCall "PVTy" [Var ty, q unq t]
2571−mkList :: Raw -> [Raw] -> Raw
2572−mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
2573−mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
2577−reflectConstant :: Const -> Raw
2578−reflectConstant c@(I _) = reflCall "I" [RConstant c]
2579−reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
2580−reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
2581−reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
2582−reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
2583−reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
2584−reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
2585−reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
2586−reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
2587−reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
2588−reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
2589−reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
2590−reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
2591−reflectConstant StrType = Var (reflm "StrType")
2592−reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
2593−reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
2594−reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
2595−reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
2596−reflectConstant VoidType = Var (reflm "VoidType")
2597−reflectConstant Forgot = Var (reflm "Forgot")
2598−reflectConstant WorldType = Var (reflm "WorldType")
2599−reflectConstant TheWorld = Var (reflm "TheWorld")
2601−reflectUExp :: UExp -> Raw
2602−reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
2603−reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
2605−-- | Reflect the environment of a proof into a List (TTName, Binder TT)
2606−reflectEnv :: Env -> Raw
2607−reflectEnv = foldr consToEnvList emptyEnvList
2609− consToEnvList :: (Name, Binder Term) -> Raw -> Raw
2610− consToEnvList (n, b) l
2611− = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
2613− , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
2614− , (RApp (Var $ reflm "Binder")
2615− (Var $ reflm "TT"))
2622− emptyEnvList :: Raw
2623− emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
2626−-- | Reflect an error into the internal datatype of Idris -- TODO
2627−rawBool :: Bool -> Raw
2628−rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
2629−rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
2631−rawNil :: Raw -> Raw
2632−rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
2634−rawCons :: Raw -> Raw -> Raw -> Raw
2635−rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
2637−rawList :: Raw -> [Raw] -> Raw
2638−rawList ty = foldr (rawCons ty) (rawNil ty)
2640−rawPairTy :: Raw -> Raw -> Raw
2641−rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
2643−rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
2644−rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
2646−reflectCtxt :: [(Name, Type)] -> Raw
2647−reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
2648− (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
2649− (reflectName n, reflect t)))
2652−reflectErr :: Err -> Raw
2653−reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
2654−reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
2655−reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =
2656− raw_apply (Var $ reflErrName "CantUnify")
2663−reflectErr (InfiniteUnify n tm ctxt) =
2664− raw_apply (Var $ reflErrName "InfiniteUnify")
2669−reflectErr (CantConvert t t' ctxt) =
2670− raw_apply (Var $ reflErrName "CantConvert")
2675−reflectErr (CantSolveGoal t ctxt) =
2676− raw_apply (Var $ reflErrName "CantSolveGoal")
2680−reflectErr (UnifyScope n n' t ctxt) =
2681− raw_apply (Var $ reflErrName "UnifyScope")
2687−reflectErr (CantInferType str) =
2688− raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
2689−reflectErr (NonFunctionType t t') =
2690− raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
2691−reflectErr (NotEquality t t') =
2692− raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
2693−reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
2694−reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
2695−reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
2696−reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
2697−reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
2698−reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
2699−reflectErr (NotInjective t1 t2 t3) =
2700− raw_apply (Var $ reflErrName "NotInjective")
2705−reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
2706−reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
2707−reflectErr (CantResolveAlts ss) =
2708− raw_apply (Var $ reflErrName "CantResolveAlts")
2709− [rawList (Var $ reflm "TTName") (map reflectName ss)]
2710−reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
2711−reflectErr (NoEliminator str t)
2712− = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),
2714−reflectErr UniverseError = Var $ reflErrName "UniverseError"
2715−reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
2716−reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
2717−reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
2718−reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
2719−reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
2720−reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
2721−reflectErr (ProviderError str) =
2722− raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
2723−reflectErr (LoadingFailed str err) =
2724− raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
2725−reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
2727−-- | Reflect a file context
2728−reflectFC :: FC -> Raw
2729−reflectFC fc = raw_apply (Var (reflm "FileLoc"))
2730− [ RConstant (Str (fc_fname fc))
2731− , raw_apply (Var pairCon) $
2733− map (RConstant . I)
2734− [ fst (fc_start fc)
2735− , snd (fc_start fc)
2737− , raw_apply (Var pairCon) $
2739− map (RConstant . I)
2744− where intTy = RConstant (AType (ATInt ITNative))
2746elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2121elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2747elaboratingArgErr [] err = err
2122elaboratingArgErr [] err = err
2748elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
2123elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
@@ -2813,70 +2188,108 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
2814 parts -> ReflectionError errorparts e
2189 parts -> ReflectionError errorparts e
2816−fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
2817−fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
2818− | just == txt "Just" = Just tm
2819−fromTTMaybe x = Nothing
2821−reflErrName :: String -> Name
2822−reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
2824−-- | Attempt to reify a report part from TT to the internal
2825−-- representation. Not in Idris or ElabD monads because it should be usable
2827−reifyReportPart :: Term -> Either Err ErrorReportPart
2828−reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
2829− Right (TextPart msg)
2830−reifyReportPart (App (P (DCon _ _ _) n _) ttn)
2831− | n == reflm "NamePart" =
2832− case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of
2833− Error e -> Left . InternalMsg $
2834− "could not reify name term " ++
2836− " when reflecting an error:" ++ show e
2837− OK (n', _)-> Right $ NamePart n'
2838−reifyReportPart (App (P (DCon _ _ _) n _) tm)
2839− | n == reflm "TermPart" =
2840− case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of
2841− Error e -> Left . InternalMsg $
2842− "could not reify reflected term " ++
2844− " when reflecting an error:" ++ show e
2845− OK (tm', _) -> Right $ TermPart tm'
2846−reifyReportPart (App (P (DCon _ _ _) n _) tm)
2847− | n == reflm "SubReport" =
2849− Just xs -> do subParts <- mapM reifyReportPart xs
2850− Right (SubReport subParts)
2851− Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
2852−reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
2854−reifyTyDecl :: Term -> ElabD RTyDecl
2855−reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)
2856− | n == tacN "Declare" =
2857− do tyN' <- reifyTTName tyN
2858− args' <- case unList args of
2859− Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
2860− Just xs -> mapM reifyRArg xs
2861− ret' <- reifyRaw ret
2862− return $ RDeclare tyN' args' ret'
2863− where reifyRArg :: Term -> ElabD RArg
2864− reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)
2865− | n == tacN "Explicit" = liftM2 RExplicit
2868− | n == tacN "Implicit" = liftM2 RImplicit
2870− (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint
2873− reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
2874−reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
2878− = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
2879− , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
2882solveAll = try (do solve; solveAll) (return ())
2191solveAll = try (do solve; solveAll) (return ())
2193+-- | Do the left-over work after creating declarations in reflected
2194+-- elaborator scripts
2195+processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()
2196+processTacticDecls info steps =
2197+ -- The order of steps is important: type declarations might
2198+ -- establish metavars that later function bodies resolve.
2199+ forM_ (reverse steps) $ \case
2200+ RTyDeclInstrs n fc impls ty ->
2201+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
2202+ logLvl 3 $ " It has impls " ++ show impls
2203+ updateIState $ \i -> i { idris_implicits =
2204+ addDef n impls (idris_implicits i) }
2206+ ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]
2209+ case lookupDef n ctxt of
2210+ (TyDecl _ _ : _) ->
2211+ -- If the function isn't defined at the end of the elab script,
2212+ -- then it must be added as a metavariable. This needs guarding
2213+ -- to prevent overwriting case defs with a metavar, if the case
2214+ -- defs come after the type decl in the same script!
2215+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
2218+ RClausesInstrs n cs ->
2219+ do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n
2221+ let lhss = map (\(_, lhs, _) -> lhs) cs
2222+ let fc = fileFC "elab_reflected"
2224+ do ist <- getIState
2225+ possible <- genClauses fc n lhss
2227+ delab' ist lhs True True) lhss)
2228+ missing <- filterM (checkPossible n) possible
2229+ return (filter (noMatch ist lhss) missing)
2230+ let tot = if null pmissing
2231+ then Unchecked -- still need to check recursive calls
2232+ else Partial NotCovering -- missing cases implies not total
2234+ updateIState $ \i -> i { idris_patdefs =
2235+ addDef n (cs, pmissing) $ idris_patdefs i }
2239+ case lookupDefExact n ctxt of
2240+ Just (CaseOp _ _ _ _ _ cd) ->
2241+ -- Here, we populate the call graph with a list of things
2242+ -- we refer to, so that if they aren't total, the whole
2244+ let (scargs, sc) = cases_compiletime cd
2245+ (scargs', sc') = cases_runtime cd
2246+ calls = findCalls sc' scargs
2247+ used = findUsedArgs sc' scargs'
2248+ cg = CGInfo scargs' calls [] used []
2249+ in do logLvl 2 $ "Called names in reflected elab: " ++ show cg
2251+ addToCalledG n (nub (map fst calls))
2253+ Just _ -> return () -- TODO throw internal error
2254+ Nothing -> return ()
2256+ -- checkDeclTotality requires that the call graph be present
2257+ -- before calling it.
2258+ -- TODO: reduce code duplication with Idris.Elab.Clause
2261+ -- Actually run the totality checker. In the main clause
2262+ -- elaborator, this is deferred until after. Here, we run it
2263+ -- now to get totality information as early as possible.
2264+ tot' <- checkDeclTotality (fc, n)
2266+ when (tot' /= Unchecked) $ addIBC (IBCTotal n tot')
2268+ -- TODO: see if the code duplication with Idris.Elab.Clause can be
2269+ -- reduced or eliminated.
2270+ checkPossible :: Name -> PTerm -> Idris Bool
2271+ checkPossible fname lhs_in =
2272+ do ctxt <- getContext
2274+ let lhs = addImplPat ist lhs_in
2275+ let fc = fileFC "elab_reflected_totality"
2276+ let tcgen = False -- TODO: later we may support dictionary generation
2277+ case elaborate ctxt (idris_datatypes ist) (sMN 0 "refPatLHS") infP initEState
2278+ (erun fc (buildTC ist info ELHS [] fname (infTerm lhs))) of
2279+ OK (ElabResult lhs' _ _ _ _, _) ->
2280+ do -- not recursively calling here, because we don't
2281+ -- want to run infinitely many times
2282+ let lhs_tm = orderPats (getInferTerm lhs')
2283+ case recheck ctxt [] (forget lhs_tm) lhs_tm of
2284+ OK _ -> return True
2285+ err -> return False
2286+ -- if it's a recoverable error, the case may become possible
2287+ Error err -> if tcgen then return (recoverableCoverage ctxt err)
2288+ else return (validCoverageCase ctxt err ||
2289+ recoverableCoverage ctxt err)
2292+ -- TODO: Attempt to reduce/eliminate code duplication with Idris.Elab.Clause
2293+ noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of