@@ -1,6 +1,6 @@
1−{-# LANGUAGE PatternGuards, ViewPatterns #-}
1+{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}
22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3−module Idris.ElabTerm where
3+module Idris.Elab.Term where
44
55import Idris.AbsSyntax
66import Idris.AbsSyntaxTree
@@ -10,11 +10,13 @@ import Idris.Error
1010import Idris.ProofSearch
1111import Idris.Output (pshow)
1212
13+import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)
1314import Idris.Core.Elaborate hiding (Tactic(..))
1415import Idris.Core.TT
1516import Idris.Core.Evaluate
1617import 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)
1820import Idris.ErrReverse (errReverse)
1921import Idris.ElabQuasiquote (extractUnquotes)
2022import Idris.Elab.Utils
@@ -26,7 +28,7 @@ import Control.Monad
2628import Control.Monad.State.Strict
2729import Data.List
2830import qualified Data.Map as M
29−import Data.Maybe (mapMaybe, fromMaybe)
31+import Data.Maybe (mapMaybe, fromMaybe, catMaybes)
3032import qualified Data.Set as S
3133import qualified Data.Text as T
3234
@@ -35,6 +37,7 @@ import Debug.Trace
3537data ElabMode = ETyDecl | ELHS | ERHS
3638 deriving Eq
3739
40+
3841data ElabResult =
3942 ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
4043 , resultMetavars :: [(Name, (Int, Maybe Name, Type))]
@@ -43,23 +46,10 @@ data ElabResult =
4346 -- ^ Deferred declarations as the meaning of case blocks
4447 , resultContext :: Context
4548 -- ^ The potentially extended context from new definitions
46− , resultTyDecls :: [(Name, FC, [PArg], Type)]
49+ , resultTyDecls :: [RDeclInstructions]
4750 -- ^ Meta-info about the new type declarations
4851 }
4952
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) }
57− addIBC (IBCImp n)
58− ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]
59− addIBC (IBCDef n)
60− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
61− addDeferred ds'
62−
6353
6454-- Using the elaborator, convert a term in raw syntax to a fully
6555-- elaborated, typechecked term.
@@ -122,11 +112,11 @@ build ist info emode opts fn tm
122112 update_term orderPats)
123113 EState is _ impls <- getAux
124114 tt <- get_term
125− let (tm, ds) = runState (collectDeferred (Just fn) tt) []
126− log <- getLog
127115 ctxt <- get_context
128− if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
129− else return (ElabResult tm ds is ctxt impls)
116+ let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
117+ log <- getLog
118+ if (log /= "") then trace log $ return (ElabResult tm ds (map snd is) ctxt impls)
119+ else return (ElabResult tm ds (map snd is) ctxt impls)
130120 where pattern = emode == ELHS
131121 tydecl = emode == ETyDecl
132122
@@ -164,11 +154,11 @@ buildTC ist info emode opts fn tm
164154 lift (Error (CantMatch (getInferTerm tm)))
165155 EState is _ impls <- getAux
166156 tt <- get_term
167− let (tm, ds) = runState (collectDeferred (Just fn) tt) []
168− log <- getLog
169157 ctxt <- get_context
170− if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
171− else return (ElabResult tm ds is ctxt impls)
158+ let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
159+ log <- getLog
160+ if (log /= "") then trace log $ return (ElabResult tm ds (map snd is) ctxt impls)
161+ else return (ElabResult tm ds (map snd is) ctxt impls)
172162 where pattern = emode == ELHS
173163
174164-- return whether arguments of the given constructor name can be
@@ -213,7 +203,7 @@ goal_polymorphic =
213203
214204-- | Returns the set of declarations we need to add to complete the
215205-- 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)
217207elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
218208 ElabD ()
219209elab ist info emode opts fn tm
@@ -262,9 +252,7 @@ elab ist info emode opts fn tm
262252 -- normally correct to call elabE - the ones that don't are desugarings
263253 -- typically
264254 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
265− elabE ina fc' t =
266− --do g <- goal
267− --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
255+ elabE ina fc' t =
268256 do solved <- get_recents
269257 as <- get_autos
270258 -- If any of the autos use variables which have recently been solved,
@@ -430,7 +418,7 @@ elab ist info emode opts fn tm
430418 [pimp (sMN 0 "a") t False,
431419 pimp (sMN 0 "P") Placeholder True,
432420 pexp l, pexp r])
433− elab' ina fc (PAlternative True as)
421+ elab' ina fc (PAlternative True as)
434422 = do hnf_compute
435423 ty <- goal
436424 ctxt <- get_context
@@ -953,7 +941,7 @@ elab ist info emode opts fn tm
953941 (caseBlock fc cname'
954942 (map (isScr scr) (reverse args')) opts)
955943 -- elaborate case
956− updateAux (\e -> e { case_decls = newdef : case_decls e } )
944+ updateAux (\e -> e { case_decls = (cname', newdef) : case_decls e } )
957945 -- if we haven't got the type yet, hopefully we'll get it later!
958946 movelast tyn
959947 solve
@@ -967,7 +955,7 @@ elab ist info emode opts fn tm
967955 _ -> n
968956
969957 inApp (P _ n _) = [n]
970− inApp (App f a) = inApp f ++ inApp a
958+ inApp (App _ f a) = inApp f ++ inApp a
971959 inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
972960 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc
973961 inApp (Bind n b sc) = inApp sc
@@ -1012,9 +1000,10 @@ elab ist info emode opts fn tm
10121000 -- Save the old state - we need a fresh proof state to avoid
10131001 -- capturing lexically available variables in the quoted term.
10141002 ctxt <- get_context
1003+ datatypes <- get_datatypes
10151004 saveState
10161005 updatePS (const .
1017− newProof (sMN 0 "q") ctxt $
1006+ newProof (sMN 0 "q") ctxt datatypes $
10181007 P Ref (reflm "TT") Erased)
10191008
10201009 -- Re-add the unquotes, letting Idris infer the (fictional)
@@ -1085,6 +1074,17 @@ elab ist info emode opts fn tm
10851074
10861075
10871076 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
1077+ elab' ina fc (PQuoteName n) =
1078+ do ctxt <- get_context
1079+ env <- get_env
1080+ case lookup n env of
1081+ Just _ -> do fill $ reflectName n ; solve
1082+ Nothing ->
1083+ case lookupNameDef n ctxt of
1084+ [(n', _)] -> do fill $ reflectName n'
1085+ solve
1086+ [] -> lift . tfail . NoSuchVariable $ n
1087+ more -> lift . tfail . CantResolveAlts $ map fst more
10881088 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
10891089 elab' ina fc (PHidden t)
10901090 | reflection = elab' ina fc t
@@ -1100,11 +1100,13 @@ elab ist info emode opts fn tm
11001100 delayElab $ do focus h
11011101 dotterm
11021102 elab' ina fc t
1103− elab' ina fc (PRunTactics fc' tm) =
1103+ elab' ina fc (PRunElab fc' tm) =
11041104 do attack
11051105 n <- getNameFrom (sMN 0 "tacticScript")
11061106 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"]))
1109+ (Var unitTy)
11081110 claim n scriptTy
11091111 movelast n
11101112 letbind n' scriptTy (Var n)
@@ -1112,11 +1114,10 @@ elab ist info emode opts fn tm
11121114 elab' ina (Just fc') tm
11131115 env <- get_env
11141116 runTactical (maybe fc' id fc) env (P Bound n' Erased)
1115− EState _ _ todo <- getAux
11161117 solve
11171118 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
11181119
1119− delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
1120+ delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
11201121
11211122 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
11221123 isScr (PRef _ n) (n', b) = (n', (n == n', b))
@@ -1378,7 +1379,7 @@ pruneByType _ t _ as = as
13781379
13791380findInstances :: IState -> Term -> [Name]
13801381findInstances ist t
1381− | (P _ n _, _) <- unApply t
1382+ | (P _ n _, _) <- unApply (getRetTy t)
13821383 = case lookupCtxt n (idris_classes ist) of
13831384 [CI _ _ _ _ _ ins _] -> filter accessible ins
13841385 _ -> []
@@ -1429,17 +1430,17 @@ resTC' tcs defaultOn topholes depth topg fn ist
14291430 = do compute
14301431 g <- goal
14311432 let argsok = tcArgsOK g topholes
1432−-- trace (show (g,hs,argsok,topholes)) $
14331433 if not argsok -- && not mvok)
14341434 then lift $ tfail $ CantResolve True topg
14351435 else do
14361436 ptm <- get_term
14371437 ulog <- getUnifyLog
14381438 hs <- get_holes
1439− traceWhen ulog ("Resolving class " ++ show g) $
1439+ env <- get_env
1440+ traceWhen ulog ("Resolving class " ++ show g ++ "\nin" ++ show env) $
14401441 try' (trivial' ist)
14411442 (do t <- goal
1442− let (tc, ttypes) = unApply t
1443+ let (tc, ttypes) = unApply (getRetTy t)
14431444 scopeOnly <- needsDefault t tc ttypes
14441445 let stk = elab_stack ist
14451446 let insts_in = findInstances ist t
@@ -1449,10 +1450,10 @@ resTC' tcs defaultOn topholes depth topg fn ist
14491450 let depth' = if scopeOnly then 2 else depth
14501451 blunderbuss t depth' stk (stk ++ insts)) True
14511452 where
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
14531454 = True
14541455 tcArgsOK ty hs -- if any arguments are metavariables, postpone
1455− = let (f, as) = unApply ty in
1456+ = let (f, as) = unApply (getRetTy ty) in
14561457 case f of
14571458 P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of
14581459 Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as
@@ -1469,7 +1470,7 @@ resTC' tcs defaultOn topholes depth topg fn ist
14691470 isMeta _ _ = False
14701471
14711472 notHole hs (P _ n _, c)
1472− | (P _ cn _, _) <- unApply c,
1473+ | (P _ cn _, _) <- unApply (getRetTy c),
14731474 n `elem` hs && isConName cn (tt_ctxt ist) = False
14741475 | Constant _ <- c = not (n `elem` hs)
14751476 notHole _ _ = True
@@ -1510,11 +1511,22 @@ resTC' tcs defaultOn topholes depth topg fn ist
15101511 _ -> blunderbuss t d stk ns)
15111512 | otherwise = blunderbuss t d stk ns
15121513
1514+ introImps = do g <- goal
1515+ case g of
1516+ (Bind _ (Pi _ _ _) sc) -> do attack; intro Nothing
1517+ num <- introImps
1518+ return (num + 1)
1519+ _ -> return 0
1520+
1521+ solven 0 = return ()
1522+ solven n = do solve; solven (n - 1)
1523+
15131524 resolve n depth
15141525 | depth == 0 = fail $ "Can't resolve type class"
15151526 | otherwise
1516− = do t <- goal
1517− let (tc, ttypes) = unApply t
1527+ = do lams <- introImps
1528+ t <- goal
1529+ let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)
15181530-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
15191531-- else do
15201532 -- if there's a hole in the goal, don't even try
@@ -1526,14 +1538,15 @@ resTC' tcs defaultOn topholes depth topg fn ist
15261538 tm <- get_term
15271539 args <- map snd <$> try' (apply (Var n) imps)
15281540 (match_apply (Var n) imps) True
1541+ solven lams -- close any implicit lambdas we introduced
15291542 ps' <- get_probs
15301543 when (length ps < length ps' || unrecoverable ps') $
15311544 fail "Can't apply type class"
15321545-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
15331546 mapM_ (\ (_,n) -> do focus n
15341547 t' <- goal
1535− let (tc', ttype) = unApply t'
1536− let got = fst (unApply t)
1548+ let (tc', ttype) = unApply (getRetTy t')
1549+ let got = fst (unApply (getRetTy t))
15371550 let depth' = if tc' `elem` tcs
15381551 then depth - 1 else depth
15391552 resTC' (got : tcs) defaultOn topholes depth' topg fn ist)
@@ -1546,23 +1559,49 @@ resTC' tcs defaultOn topholes depth topg fn ist
15461559 where isImp (PImp p _ _ _ _) = (True, p)
15471560 isImp arg = (False, priority arg)
15481561
1549−collectDeferred :: Maybe Name ->
1562+collectDeferred :: Maybe Name -> [Name] -> Context ->
15501563 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) =
15521565 do ds <- get
1553− t' <- collectDeferred top t
1554− when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])
1555− collectDeferred top app
1556−collectDeferred top (Bind n b t) = do b' <- cdb b
1557− t' <- collectDeferred top t
1558− return (Bind n b' t')
1566+ t' <- collectDeferred top casenames ctxt t
1567+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t'))])
1568+ collectDeferred top casenames ctxt app
1569+ where
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
1573+ -- can be done
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)
1577+ tidyArg env t = t
1578+
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
1589+
1590+ getFn (Bind n (Lam _) t) = getFn t
1591+ getFn t | (f, a) <- unApply t = f
1592+
1593+collectDeferred top ns ctxt (Bind n b t)
1594+ = do b' <- cdb b
1595+ t' <- collectDeferred top ns ctxt t
1596+ return (Bind n b' t')
15591597 where
1560− cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v)
1561− cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)
1562− cdb b = do ty' <- collectDeferred top (binderTy b)
1598+ cdb (Let t v) = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
1599+ cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
1600+ cdb b = do ty' <- collectDeferred top ns ctxt (binderTy b)
15631601 return (b { binderTy = ty' })
1564−collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)
1565−collectDeferred top t = return t
1602+collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f)
1603+ (collectDeferred top ns ctxt a)
1604+collectDeferred top ns ctxt t = return t
15661605
15671606case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
15681607case_ ind autoSolve ist fn tm = do
@@ -1582,8 +1621,6 @@ case_ ind autoSolve ist fn tm = do
15821621 else casetac (forget val)
15831622 when autoSolve solveAll
15841623
1585−tacN :: String -> Name
1586−tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
15871624
15881625runTactical :: FC -> Env -> Term -> ElabD ()
15891626runTactical fc env tm = do tm' <- eval tm
@@ -1591,10 +1628,50 @@ runTactical fc env tm = do tm' <- eval tm
15911628 return ()
15921629 where
15931630 eval tm = do ctxt <- get_context
1631+ env <- get_env
15941632 return $ normaliseAll ctxt env (finalise tm)
15951633
15961634 returnUnit = fmap fst $ get_type_val (Var unitCon)
15971635
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)
1639+
1640+ pullVars :: (Term, Term) -> ([Name], Term, Term)
1641+ pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
1642+
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))
1659+ clauses'
1660+ set_context $
1661+ addCasedef n (const [])
1662+ info False (STerm Erased)
1663+ True False -- TODO what are these?
1664+ (map snd $ getArgTys ty) [] -- TODO inaccessible types
1665+ clauses'
1666+ clauses''
1667+ clauses''
1668+ clauses''
1669+ clauses''
1670+ ty
1671+ ctxt
1672+ updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
1673+ return ()
1674+
15981675 -- | Do a step in the reflected elaborator monad. The input is the
15991676 -- step, the output is the (reflected) term returned.
16001677 runTacTm :: Term -> ElabD Term
@@ -1623,6 +1700,35 @@ runTactical fc env tm = do tm' <- eval tm
16231700 else fmap fst . get_type_val $
16241701 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
16251702 (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")]
1714+ , x
1715+ , raw_apply (Var pairCon) [ Var (reflm "NameType"), Var (reflm "TT")
1716+ , y, z]]
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")]])
1724+ defs
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'))
16261732 | n == tacN "prim__SourceLocation", [] <- args
16271733 = fmap fst . get_type_val $
16281734 reflectFC fc
@@ -1633,19 +1739,23 @@ runTactical fc env tm = do tm' <- eval tm
16331739 = do errs' <- eval errs
16341740 parts <- reifyReportParts errs'
16351741 lift . tfail $ ReflectionError [parts] (Msg "")
1636− | n == tacN "prim__PureTactical", [_a, tm] <- args
1742+ | n == tacN "prim__PureElab", [_a, tm] <- args
16371743 = return tm
1638− | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1744+ | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args
16391745 = do first' <- eval first
1640− res <- runTacTm first'
1641− next <- eval (App andThen res)
1746+ res <- eval =<< runTacTm first'
1747+ next <- eval (App Complete andThen res)
16421748 runTacTm next
16431749 | n == tacN "prim__Try", [_a, first, alt] <- args
16441750 = do first' <- eval first
16451751 alt' <- eval alt
16461752 try' (runTacTm first') (runTacTm alt') True
16471753 | n == tacN "prim__Fill", [raw] <- args
1648− = do raw' <- reifyRaw raw
1754+ = do raw' <- reifyRaw =<< eval raw
1755+ fill raw'
1756+ returnUnit
1757+ | n == tacN "prim__Apply", [raw] <- args
1758+ = do raw' <- reifyRaw =<< eval raw
16491759 apply raw' []
16501760 returnUnit
16511761 | n == tacN "prim__Gensym", [hint] <- args
@@ -1662,7 +1772,7 @@ runTactical fc env tm = do tm' <- eval tm
16621772 returnUnit
16631773 | n == tacN "prim__Forget", [tt] <- args
16641774 = do tt' <- reifyTT tt
1665− fmap fst . get_type_val $ reflect tt'
1775+ fmap fst . get_type_val . reflectRaw $ forget tt'
16661776 | n == tacN "prim__Attack", [] <- args
16671777 = do attack
16681778 returnUnit
@@ -1684,6 +1794,21 @@ runTactical fc env tm = do tm' <- eval tm
16841794 Just name -> fmap Just $ reifyTTName name
16851795 intro n
16861796 returnUnit
1797+ | n == tacN "prim__Forall", [n, ty] <- args
1798+ = do n' <- reifyTTName n
1799+ ty' <- reifyRaw ty
1800+ forall n' Nothing ty'
1801+ returnUnit
1802+ | n == tacN "prim__PatVar", [n] <- args
1803+ = do n' <- reifyTTName n
1804+ patvar n'
1805+ returnUnit
1806+ | n == tacN "prim__PatBind", [n] <- args
1807+ = do n' <- reifyTTName n
1808+ patbind n'
1809+ returnUnit
1810+ | n == tacN "prim__Compute", [] <- args
1811+ = do compute ; returnUnit
16871812 | n == tacN "prim__DeclareType", [decl] <- args
16881813 = do (RDeclare n args res) <- reifyTyDecl decl
16891814 ctxt <- get_context
@@ -1693,9 +1818,10 @@ runTactical fc env tm = do tm' <- eval tm
16931818 rty = foldr mkPi res args
16941819 (checked, ty') <- lift $ check ctxt [] rty
16951820 case normaliseAll ctxt [] (finalise ty') of
1696− TType _ -> lift . tfail . InternalMsg $
1697− show checked ++ " is not a type: it's " ++ show ty'
1698− _ -> return ()
1821+ UType _ -> return ()
1822+ TType _ -> return ()
1823+ ty'' -> lift . tfail . InternalMsg $
1824+ show checked ++ " is not a type: it's " ++ show ty''
16991825 case lookupDefExact n ctxt of
17001826 Just _ -> lift . tfail . InternalMsg $
17011827 show n ++ " is already defined."
@@ -1703,17 +1829,41 @@ runTactical fc env tm = do tm' <- eval tm
17031829 let decl = TyDecl Ref checked
17041830 ctxt' = addCtxtDef n decl ctxt
17051831 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) :
17071833 new_tyDecls e }
17081834 aux <- getAux
17091835 returnUnit
1836+ | n == tacN "prim__DefineFunction", [decl] <- args
1837+ = do defn <- reifyFunDefn decl
1838+ defineFunction defn
1839+ returnUnit
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")
1847+ aux <- getAux
1848+ datatypes <- get_datatypes
1849+ env <- get_env
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'
1854+ env' <- get_env
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")
1859+ (tm', ty')
17101860 | n == tacN "prim__Debug", [ty, msg] <- args
17111861 = do let msg' = fromTTMaybe msg
17121862 case msg' of
17131863 Nothing -> debugElaborator Nothing
17141864 Just (Constant (Str m)) -> debugElaborator (Just m)
17151865 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
17171867
17181868-- Running tactics directly
17191869-- if a tactic adds unification problems, return an error
@@ -1968,781 +2118,6 @@ runTac autoSolve ist perhapsFC fn tac
19682118 runReflected t = do t' <- reify ist t
19692119 runTac autoSolve ist perhapsFC fn t'
19702120
1971−-- | Prefix a name with the "Language.Reflection" namespace
1972−reflm :: String -> Name
1973−reflm n = sNS (sUN n) ["Reflection", "Language"]
1974−
1975−
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)
1989−
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 [])
1994−reifyApp _ t [x]
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
1998− goal <- reifyTT ty
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')
2006−reifyApp ist t [t']
2007− | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
2008−reifyApp ist t [t']
2009− | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
2010−reifyApp ist t [t']
2011− | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
2012−reifyApp _ t [t']
2013− | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
2014−reifyApp ist t [t']
2015− | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
2016−reifyApp ist t [x]
2017− | t == reflm "Focus" = liftM Focus (reifyTTName x)
2018−reifyApp ist t [t']
2019− | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
2020−reifyApp ist t [n, t']
2021− | t == reflm "LetTac" = do n' <- reifyTTName n
2022− t'' <- reifyTT t'
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'
2027− t'' <- reifyTT t'
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
2032−
2033−reifyReportParts :: Term -> ElabD [ErrorReportPart]
2034−reifyReportParts errs =
2035− case unList errs of
2036− Nothing -> fail "Failed to reify errors"
2037− Just errs' ->
2038− let parts = mapM reifyReportPart errs' in
2039− case parts of
2040− Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
2041− Right errs'' ->
2042− return errs''
2043−
2044−-- | Reify terms from their reflected representation
2045−reifyTT :: Term -> ElabD Term
2046−reifyTT t@(App _ _)
2047− | (P _ f _, args) <- unApply t = reifyTTApp f args
2048−reifyTT t@(P _ n _)
2049− | n == reflm "Erased" = return $ Erased
2050−reifyTT t@(P _ n _)
2051− | n == reflm "Impossible" = return $ Impossible
2052−reifyTT t = fail ("Unknown reflection term: " ++ show t)
2053−
2054−reifyTTApp :: Name -> [Term] -> ElabD Term
2055−reifyTTApp t [nt, n, x]
2056− | t == reflm "P" = do nt' <- reifyTTNameType nt
2057− n' <- reifyTTName n
2058− x' <- reifyTT x
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
2065− x' <- reifyTT x
2066− return $ Bind n' b' x'
2067−reifyTTApp t [f, x]
2068− | t == reflm "App" = do f' <- reifyTT f
2069− x' <- reifyTT x
2070− return $ App f' x'
2071−reifyTTApp t [c]
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
2076−reifyTTApp t [tt]
2077− | t == reflm "TType" = liftM TType (reifyTTUExp tt)
2078−reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
2079−
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)
2087−
2088−reifyRawApp :: Name -> [Term] -> ElabD Raw
2089−reifyRawApp t [n]
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
2094− x' <- reifyRaw x
2095− return $ RBind n' b' x'
2096−reifyRawApp t [f, x]
2097− | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
2098−reifyRawApp t [t']
2099− | t == reflm "RForce" = liftM RForce (reifyRaw t')
2100−reifyRawApp t [c]
2101− | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
2102−reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
2103−
2104−reifyTTName :: Term -> ElabD Name
2105−reifyTTName t
2106− | (P _ f _, args) <- unApply t = reifyTTNameApp f args
2107−reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
2108−
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
2118−reifyTTNameApp t []
2119− | t == reflm "NErased" = return NErased
2120−reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
2121−
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)
2131−
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)
2142−
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)
2150−
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))
2171−
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)
2179−
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))
2202−
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)
2207−
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
2214−
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"
2221−
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)
2229−
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
2234−
2235−-- | Lift a term into its Language.Reflection.TT representation
2236−reflect :: Term -> Raw
2237−reflect = reflectTTQuote []
2238−
2239−-- | Lift a term into its Language.Reflection.Raw representation
2240−reflectRaw :: Raw -> Raw
2241−reflectRaw = reflectRawQuote []
2242−
2243−claimTT :: Name -> ElabD Name
2244−claimTT n = do n' <- getNameFrom n
2245− claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
2246− return n'
2247−
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
2256− | otherwise =
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]
2265− solve
2266− focus n'; reflectNameQuotePattern n
2267−reflectTTQuotePattern unq (V n)
2268− = do fill $ reflCall "V" [RConstant (I n)]
2269− solve
2270−reflectTTQuotePattern unq (Bind n b x)
2271− = do x' <- claimTT (sMN 0 "sc")
2272− movelast x'
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"
2278− [reflectName n,
2279− Var b',
2280− Var x']
2281− solve
2282− else do any <- getNameFrom (sMN 0 "anyName")
2283− claim any (Var (reflm "TTName"))
2284− movelast any
2285− fill $ reflCall "Bind"
2286− [Var any,
2287− Var b',
2288− Var x']
2289− solve
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']
2296− solve
2297− focus f'; reflectTTQuotePattern unq f
2298− focus x'; reflectTTQuotePattern unq x
2299−reflectTTQuotePattern unq (Constant c)
2300− = do fill $ reflCall "TConst" [reflectConstant c]
2301− solve
2302−reflectTTQuotePattern unq (Proj t i)
2303− = do t' <- claimTT (sMN 0 "t"); movelast t'
2304− fill $ reflCall "Proj" [Var t', RConstant (I i)]
2305− solve
2306− focus t'; reflectTTQuotePattern unq t
2307−reflectTTQuotePattern unq (Erased)
2308− = do erased <- claimTT (sMN 0 "erased")
2309− movelast erased
2310− fill $ (Var erased)
2311− solve
2312−reflectTTQuotePattern unq (Impossible)
2313− = do fill $ Var (reflm "Impossible")
2314− solve
2315−reflectTTQuotePattern unq (TType exp)
2316− = do ue <- getNameFrom (sMN 0 "uexp")
2317− claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
2318− movelast ue
2319− fill $ reflCall "TType" [Var ue]
2320− solve
2321−reflectTTQuotePattern unq (UType u)
2322− = do uH <- getNameFrom (sMN 0 "someUniv")
2323− claim uH (Var (reflm "Universe"))
2324− movelast uH
2325− fill $ reflCall "UType" [Var uH]
2326− solve
2327− focus uH
2328− fill (Var (reflm (case u of
2329− NullType -> "NullType"
2330− UniqueType -> "UniqueType"
2331− AllTypes -> "AllTypes")))
2332− solve
2333−
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"))
2342− movelast scH
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,
2348− Var bH,
2349− Var scH]
2350− solve
2351− else do any <- getNameFrom (sMN 0 "anyName")
2352− claim any (Var (reflm "TTName"))
2353− movelast any
2354− fill $ reflCall "RBind" [Var any, Var bH, Var scH]
2355− solve
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],
2361− freeNamesR t]
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"))
2372− movelast fH
2373− xH <- getNameFrom (sMN 0 "x")
2374− claim xH (Var (reflm "Raw"))
2375− movelast xH
2376− fill $ reflCall "RApp" [Var fH, Var xH]
2377− solve
2378− focus fH; reflectRawQuotePattern unq f
2379− focus xH; reflectRawQuotePattern unq x
2380−reflectRawQuotePattern unq RType =
2381− do fill (Var (reflm "RType"))
2382− solve
2383−reflectRawQuotePattern unq (RUType univ) =
2384− do uH <- getNameFrom (sMN 0 "universe")
2385− claim uH (Var (reflm "Universe"))
2386− movelast uH
2387− fill $ reflCall "RUType" [Var uH]
2388− solve
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"))
2393− movelast rH
2394− fill $ reflCall "RForce" [Var rH]
2395− solve
2396− focus rH; reflectRawQuotePattern unq r
2397−reflectRawQuotePattern unq (RConstant c) =
2398− do cH <- getNameFrom (sMN 0 "const")
2399− claim cH (Var (reflm "Constant"))
2400− movelast cH
2401− fill (reflCall "RConstant" [Var cH]); solve
2402− focus cH
2403− fill (reflectConstant c); solve
2404−
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']
2409− solve
2410− focus t'; q unq 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']
2415− solve
2416− focus t'; q unq t
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']
2421− solve
2422− focus x'; q unq x
2423− focus y'; q unq 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']
2428− solve
2429− focus x'; q unq x
2430− focus y'; q unq 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']
2434− solve
2435− focus t'; q unq 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']
2439− solve
2440− focus t'; q unq 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']
2445− solve
2446− focus x'; q unq x
2447− focus y'; q unq 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']
2451− solve
2452− focus t'; q unq 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']
2456− solve
2457− focus t'; q unq t
2458−
2459−reflectUniverse :: Universe -> Raw
2460−reflectUniverse u =
2461− (Var (reflm (case u of
2462− NullType -> "NullType"
2463− UniqueType -> "UniqueType"
2464− AllTypes -> "AllTypes")))
2465−
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]
2485−
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]
2499−
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)]
2507−
2508−reflectName :: Name -> Raw
2509−reflectName (UN s)
2510− = reflCall "UN" [RConstant (Str (str s))]
2511−reflectName (NS n ns)
2512− = reflCall "NS" [ reflectName n
2513− , foldr (\ n s ->
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 ])
2518− (map str ns)
2519− ]
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
2524−
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
2527−-- others become _.
2528−reflectNameQuotePattern :: Name -> ElabD ()
2529−reflectNameQuotePattern n@(UN s)
2530− = do fill $ reflectName n
2531− solve
2532−reflectNameQuotePattern n@(NS _ _)
2533− = do fill $ reflectName n
2534− solve
2535−reflectNameQuotePattern (MN _ n)
2536− = do i <- getNameFrom (sMN 0 "mnCounter")
2537− claim i (RConstant (AType (ATInt ITNative)))
2538− movelast i
2539− fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
2540− solve
2541−reflectNameQuotePattern _ -- for all other names, match any
2542− = do nameHole <- getNameFrom (sMN 0 "name")
2543− claim nameHole (Var (reflm "TTName"))
2544− movelast nameHole
2545− fill (Var nameHole)
2546− solve
2547−
2548−reflectBinder :: Binder Term -> Raw
2549−reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []
2550−
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]
2570−
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)
2574− x)
2575− (mkList ty xs)
2576−
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")
2600−
2601−reflectUExp :: UExp -> Raw
2602−reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
2603−reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
2604−
2605−-- | Reflect the environment of a proof into a List (TTName, Binder TT)
2606−reflectEnv :: Env -> Raw
2607−reflectEnv = foldr consToEnvList emptyEnvList
2608− where
2609− consToEnvList :: (Name, Binder Term) -> Raw -> Raw
2610− consToEnvList (n, b) l
2611− = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
2612− [ envTupleType
2613− , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
2614− , (RApp (Var $ reflm "Binder")
2615− (Var $ reflm "TT"))
2616− , reflectName n
2617− , reflectBinder b
2618− ]
2619− , l
2620− ]
2621−
2622− emptyEnvList :: Raw
2623− emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
2624− [envTupleType]
2625−
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"])
2630−
2631−rawNil :: Raw -> Raw
2632−rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
2633−
2634−rawCons :: Raw -> Raw -> Raw -> Raw
2635−rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
2636−
2637−rawList :: Raw -> [Raw] -> Raw
2638−rawList ty = foldr (rawCons ty) (rawNil ty)
2639−
2640−rawPairTy :: Raw -> Raw -> Raw
2641−rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
2642−
2643−rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
2644−rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
2645−
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)))
2650− ctxt)
2651−
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")
2657− [ rawBool b
2658− , reflect t1
2659− , reflect t2
2660− , reflectErr e
2661− , reflectCtxt ctxt
2662− , RConstant (I i)]
2663−reflectErr (InfiniteUnify n tm ctxt) =
2664− raw_apply (Var $ reflErrName "InfiniteUnify")
2665− [ reflectName n
2666− , reflect tm
2667− , reflectCtxt ctxt
2668− ]
2669−reflectErr (CantConvert t t' ctxt) =
2670− raw_apply (Var $ reflErrName "CantConvert")
2671− [ reflect t
2672− , reflect t'
2673− , reflectCtxt ctxt
2674− ]
2675−reflectErr (CantSolveGoal t ctxt) =
2676− raw_apply (Var $ reflErrName "CantSolveGoal")
2677− [ reflect t
2678− , reflectCtxt ctxt
2679− ]
2680−reflectErr (UnifyScope n n' t ctxt) =
2681− raw_apply (Var $ reflErrName "UnifyScope")
2682− [ reflectName n
2683− , reflectName n'
2684− , reflect t
2685− , reflectCtxt ctxt
2686− ]
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")
2701− [ reflect t1
2702− , reflect t2
2703− , reflect t3
2704− ]
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),
2713− reflect t]
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]
2726−
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) $
2732− [intTy, intTy] ++
2733− map (RConstant . I)
2734− [ fst (fc_start fc)
2735− , snd (fc_start fc)
2736− ]
2737− , raw_apply (Var pairCon) $
2738− [intTy, intTy] ++
2739− map (RConstant . I)
2740− [ fst (fc_end fc)
2741− , snd (fc_end fc)
2742− ]
2743− ]
2744− where intTy = RConstant (AType (ATInt ITNative))
2745−
27462121elaboratingArgErr :: [(Name, Name)] -> Err -> Err
27472122elaboratingArgErr [] err = err
27482123elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
@@ -2813,70 +2188,108 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
28132188 [] -> e
28142189 parts -> ReflectionError errorparts e
28152190
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
2820−
2821−reflErrName :: String -> Name
2822−reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
2823−
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
2826−-- from either.
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 " ++
2835− show ttn ++
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 " ++
2843− show tm ++
2844− " when reflecting an error:" ++ show e
2845− OK (tm', _) -> Right $ TermPart tm'
2846−reifyReportPart (App (P (DCon _ _ _) n _) tm)
2847− | n == reflm "SubReport" =
2848− case unList tm of
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
2853−
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
2866− (reifyTTName argN)
2867− (reifyRaw argTy)
2868− | n == tacN "Implicit" = liftM2 RImplicit
2869− (reifyTTName argN)
2870− (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint
2871− (reifyTTName argN)
2872− (reifyRaw argTy)
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."
2875−
2876−envTupleType :: Raw
2877−envTupleType
2878− = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
2879− , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
2880− ]
2881−
28822191solveAll = try (do solve; solveAll) (return ())
2192+
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) }
2205+ addIBC (IBCImp n)
2206+ ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]
2207+ addIBC (IBCDef n)
2208+ ctxt <- getContext
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
2216+ in addDeferred ds'
2217+ _ -> return ()
2218+ RClausesInstrs n cs ->
2219+ do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n
2220+ solveDeferred n
2221+ let lhss = map (\(_, lhs, _) -> lhs) cs
2222+ let fc = fileFC "elab_reflected"
2223+ pmissing <-
2224+ do ist <- getIState
2225+ possible <- genClauses fc n lhss
2226+ (map (\lhs ->
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
2233+ setTotality n tot
2234+ updateIState $ \i -> i { idris_patdefs =
2235+ addDef n (cs, pmissing) $ idris_patdefs i }
2236+ addIBC (IBCDef n)
2237+
2238+ ctxt <- getContext
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
2243+ -- thing won't be.
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
2250+ addToCG n cg
2251+ addToCalledG n (nub (map fst calls))
2252+ addIBC $ IBCCG n
2253+ Just _ -> return () -- TODO throw internal error
2254+ Nothing -> return ()
2255+
2256+ -- checkDeclTotality requires that the call graph be present
2257+ -- before calling it.
2258+ -- TODO: reduce code duplication with Idris.Elab.Clause
2259+ buildSCG (fc, n)
2260+
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)
2265+ setTotality n tot'
2266+ when (tot' /= Unchecked) $ addIBC (IBCTotal n tot')
2267+ where
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
2273+ ist <- getIState
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)
2290+
2291+
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
2294+ Right _ -> False
2295+ Left _ -> True) cs