idris-0.11: src/Idris/Elab/Term.hs
{-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Idris.Elab.Term where
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.DSL
import Idris.Delaborate
import Idris.Error
import Idris.ProofSearch
import Idris.Output (pshow)
import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Core.Unify
import Idris.Core.ProofTerm (getProofTerm)
import Idris.Core.Typecheck (check, recheck, converts, isType)
import Idris.Core.WHNF (whnf)
import Idris.Coverage (buildSCG, checkDeclTotality, checkPositive, genClauses, recoverableCoverage, validCoverageCase)
import Idris.ErrReverse (errReverse)
import Idris.Elab.Quasiquote (extractUnquotes)
import Idris.Elab.Utils
import Idris.Reflection
import qualified Util.Pretty as U
import Control.Applicative ((<$>))
import Control.Monad
import Control.Monad.State.Strict
import Data.Foldable (for_)
import Data.List
import qualified Data.Map as M
import Data.Maybe (mapMaybe, fromMaybe, catMaybes, maybeToList)
import qualified Data.Set as S
import qualified Data.Text as T
import Debug.Trace
data ElabMode = ETyDecl | ETransLHS | ELHS | ERHS
deriving Eq
data ElabResult =
ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration
, resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]
-- ^ Information about new metavariables
, resultCaseDecls :: [PDecl]
-- ^ Deferred declarations as the meaning of case blocks
, resultContext :: Context
-- ^ The potentially extended context from new definitions
, resultTyDecls :: [RDeclInstructions]
-- ^ Meta-info about the new type declarations
, resultHighlighting :: [(FC, OutputAnnotation)]
-- ^ Saved highlights from elaboration
, resultName :: Int
-- ^ The new global name counter
}
-- Using the elaborator, convert a term in raw syntax to a fully
-- elaborated, typechecked term.
--
-- If building a pattern match, we convert undeclared variables from
-- holes to pattern bindings.
-- Also find deferred names in the term and their types
build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
ElabD ElabResult
build ist info emode opts fn tm
= do elab ist info emode opts fn tm
let tmIn = tm
let inf = case lookupCtxt fn (idris_tyinfodata ist) of
[TIPartial] -> True
_ -> False
hs <- get_holes
ivs <- get_instances
ptm <- get_term
-- Resolve remaining type classes. Two passes - first to get the
-- default Num instances, second to clean up the rest
when (not pattern) $
mapM_ (\n -> when (n `elem` hs) $
do focus n
g <- goal
try (resolveTC' True False 10 g fn ist)
(movelast n)) ivs
ivs <- get_instances
hs <- get_holes
when (not pattern) $
mapM_ (\n -> when (n `elem` hs) $
do focus n
g <- goal
ptm <- get_term
resolveTC' True True 10 g fn ist) ivs
when (not pattern) $ solveAutos ist fn False
tm <- get_term
ctxt <- get_context
probs <- get_probs
u <- getUnifyLog
hs <- get_holes
when (not pattern) $
traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++
"Remaining problems:\n" ++ qshow probs) $
do unify_all; matchProblems True; unifyProblems
when (not pattern) $ solveAutos ist fn True
probs <- get_probs
case probs of
[] -> return ()
((_,_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ qshow probs ++ "\nin\n" ++ show tm) $
if inf then return ()
else lift (Error e)
when tydecl (do mkPat
update_term liftPats
update_term orderPats)
EState is _ impls highlights _ _ <- getAux
tt <- get_term
ctxt <- get_context
let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
log <- getLog
g_nextname <- get_global_nextname
if log /= ""
then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
where pattern = emode == ELHS
tydecl = emode == ETyDecl
mkPat = do hs <- get_holes
tm <- get_term
case hs of
(h: hs) -> do patvar h; mkPat
[] -> return ()
-- Build a term autogenerated as a typeclass method definition
-- (Separate, so we don't go overboard resolving things that we don't
-- know about yet on the LHS of a pattern def)
buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->
[Name] -> -- Cached names in the PTerm, before adding PAlternatives
PTerm ->
ElabD ElabResult
buildTC ist info emode opts fn ns tm
= do let tmIn = tm
let inf = case lookupCtxt fn (idris_tyinfodata ist) of
[TIPartial] -> True
_ -> False
-- set name supply to begin after highest index in tm
initNextNameFrom ns
elab ist info emode opts fn tm
probs <- get_probs
tm <- get_term
case probs of
[] -> return ()
((_,_,_,_,e,_,_):es) -> if inf then return ()
else lift (Error e)
dots <- get_dotterm
-- 'dots' are the PHidden things which have not been solved by
-- unification
when (not (null dots)) $
lift (Error (CantMatch (getInferTerm tm)))
EState is _ impls highlights _ _ <- getAux
tt <- get_term
ctxt <- get_context
let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
log <- getLog
g_nextname <- get_global_nextname
if (log /= "")
then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
where pattern = emode == ELHS
-- return whether arguments of the given constructor name can be
-- matched on. If they're polymorphic, no, unless the type has beed made
-- concrete by the time we get around to elaborating the argument.
getUnmatchable :: Context -> Name -> [Bool]
getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
= case lookupTyExact n ctxt of
Nothing -> []
Just ty -> checkArgs [] [] ty
where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
checkArgs env ns (Bind n (Pi _ t _) sc)
= let env' = case t of
TType _ -> n : env
_ -> env in
checkArgs env' (intersect env (refsIn t) : ns)
(instantiate (P Bound n t) sc)
checkArgs env ns t
= map (not . null) (reverse ns)
getUnmatchable ctxt n = []
data ElabCtxt = ElabCtxt { e_inarg :: Bool,
e_isfn :: Bool, -- ^ Function part of application
e_guarded :: Bool,
e_intype :: Bool,
e_qq :: Bool,
e_nomatching :: Bool -- ^ can't pattern match
}
initElabCtxt = ElabCtxt False False False False False False
goal_polymorphic :: ElabD Bool
goal_polymorphic =
do ty <- goal
case ty of
P _ n _ -> do env <- get_env
case lookup n env of
Nothing -> return False
_ -> return True
_ -> return False
-- | Returns the set of declarations we need to add to complete the
-- definition (most likely case blocks to elaborate) as well as
-- declarations resulting from user tactic scripts (%runElab)
elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
ElabD ()
elab ist info emode opts fn tm
= do let loglvl = opt_logLevel (idris_options ist)
when (loglvl > 5) $ unifyLog True
compute -- expand type synonyms, etc
let fc = maybe "(unknown)"
elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)
est <- getAux
sequence_ (get_delayed_elab est)
end_unify
ptm <- get_term
when (pattern || intransform) -- convert remaining holes to pattern vars
(do unify_all
matchProblems False -- only the ones we matched earlier
unifyProblems
mkPat
update_term liftPats)
where
pattern = emode == ELHS
intransform = emode == ETransLHS
bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS
autoimpls = opt_autoimpls (idris_options ist)
get_delayed_elab est =
let ds = delayed_elab est in
map snd $ sortBy (\(p1, _) (p2, _) -> compare p1 p2) ds
tcgen = Dictionary `elem` opts
reflection = Reflection `elem` opts
isph arg = case getTm arg of
Placeholder -> (True, priority arg)
tm -> (False, priority arg)
toElab ina arg = case getTm arg of
Placeholder -> Nothing
v -> Just (priority arg, elabE ina (elabFC info) v)
toElab' ina arg = case getTm arg of
Placeholder -> Nothing
v -> Just (elabE ina (elabFC info) v)
mkPat = do hs <- get_holes
tm <- get_term
case hs of
(h: hs) -> do patvar h; mkPat
[] -> return ()
-- | elabE elaborates an expression, possibly wrapping implicit coercions
-- and forces/delays. If you make a recursive call in elab', it is
-- normally correct to call elabE - the ones that don't are desugarings
-- typically
elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
elabE ina fc' t =
do solved <- get_recents
as <- get_autos
hs <- get_holes
-- If any of the autos use variables which have recently been solved,
-- have another go at solving them now.
mapM_ (\(a, (failc, ns)) ->
if any (\n -> n `elem` solved) ns && head hs /= a
then solveAuto ist fn False (a, failc)
else return ()) as
itm <- if not pattern then insertImpLam ina t else return t
ct <- insertCoerce ina itm
t' <- insertLazy ct
g <- goal
tm <- get_term
ps <- get_probs
hs <- get_holes
--trace ("Elaborating " ++ show t' ++ " in " ++ show g
-- ++ "\n" ++ show tm
-- ++ "\nholes " ++ show hs
-- ++ "\nproblems " ++ show ps
-- ++ "\n-----------\n") $
--trace ("ELAB " ++ show t') $
let fc = fileFC "Force"
env <- get_env
handleError (forceErr t' env)
(elab' ina fc' t')
(elab' ina fc' (PApp fc (PRef fc [] (sUN "Force"))
[pimp (sUN "t") Placeholder True,
pimp (sUN "a") Placeholder True,
pexp ct]))
forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
| (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
ht == txt "Lazy'" = notDelay orig
forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
| (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
ht == txt "Lazy'" = notDelay orig
forceErr orig env (InfiniteUnify _ t _)
| (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
ht == txt "Lazy'" = notDelay orig
forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t
forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t
forceErr orig env (At _ t) = forceErr orig env t
forceErr orig env t = False
notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False
notDelay _ = True
local f = do e <- get_env
return (f `elem` map fst e)
-- | Is a constant a type?
constType :: Const -> Bool
constType (AType _) = True
constType StrType = True
constType VoidType = True
constType _ = False
-- "guarded" means immediately under a constructor, to help find patvars
elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)
-> Maybe FC -- ^ The closest FC in the syntax tree, if applicable
-> PTerm -- ^ The term to elaborate
-> ElabD ()
elab' ina fc (PNoImplicits t) = elab' ina fc t -- skip elabE step
elab' ina fc (PType fc') =
do apply RType []
solve
highlightSource fc' (AnnType "Type" "The type of types")
elab' ina fc (PUniverse u) = do apply (RUType u) []; solve
-- elab' (_,_,inty) (PConstant c)
-- | constType c && pattern && not reflection && not inty
-- = lift $ tfail (Msg "Typecase is not allowed")
elab' ina fc tm@(PConstant fc' c)
| pattern && not reflection && not (e_qq ina) && not (e_intype ina)
&& isTypeConst c
= lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
| pattern && not reflection && not (e_qq ina) && e_nomatching ina
= lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
| otherwise = do apply (RConstant c) []
solve
highlightSource fc' (AnnConst c)
elab' ina fc (PQuote r) = do fill r; solve
elab' ina _ (PTrue fc _) =
do hnf_compute
g <- goal
case g of
TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)
UType _ -> elab' ina (Just fc) (PRef fc [] unitTy)
_ -> elab' ina (Just fc) (PRef fc [] unitCon)
elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
= do g <- goal; resolveTC' False False 5 g fn ist
elab' ina fc (PResolveTC fc')
= do c <- getNameFrom (sMN 0 "__class")
instanceArg c
-- Elaborate the equality type first homogeneously, then
-- heterogeneously as a fallback
elab' ina _ (PApp fc (PRef _ _ n) args)
| n == eqTy, [Placeholder, Placeholder, l, r] <- map getTm args
= try (do tyn <- getNameFrom (sMN 0 "aqty")
claim tyn RType
movelast tyn
elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)
[pimp (sUN "A") (PRef NoFC [] tyn) True,
pimp (sUN "B") (PRef NoFC [] tyn) False,
pexp l, pexp r]))
(do atyn <- getNameFrom (sMN 0 "aqty")
btyn <- getNameFrom (sMN 0 "bqty")
claim atyn RType
movelast atyn
claim btyn RType
movelast btyn
elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)
[pimp (sUN "A") (PRef NoFC [] atyn) True,
pimp (sUN "B") (PRef NoFC [] btyn) False,
pexp l, pexp r]))
elab' ina _ (PPair fc hls _ l r)
= do hnf_compute
g <- goal
let (tc, _) = unApply g
case g of
TType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls pairTy)
[pexp l,pexp r])
UType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairTy)
[pexp l,pexp r])
_ -> case tc of
P _ n _ | n == upairTy
-> elab' ina (Just fc) (PApp fc (PRef fc hls upairCon)
[pimp (sUN "A") Placeholder False,
pimp (sUN "B") Placeholder False,
pexp l, pexp r])
_ -> elab' ina (Just fc) (PApp fc (PRef fc hls pairCon)
[pimp (sUN "A") Placeholder False,
pimp (sUN "B") Placeholder False,
pexp l, pexp r])
elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r)
= case t of
Placeholder ->
do hnf_compute
g <- goal
case g of
TType _ -> asType
_ -> asValue
_ -> asType
where asType = elab' ina (Just fc) (PApp fc (PRef NoFC hls sigmaTy)
[pexp t,
pexp (PLam fc n nfc Placeholder r)])
asValue = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)
[pimp (sMN 0 "a") t False,
pimp (sMN 0 "P") Placeholder True,
pexp l, pexp r])
elab' ina _ (PDPair fc hls p l t r) = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)
[pimp (sMN 0 "a") t False,
pimp (sMN 0 "P") Placeholder True,
pexp l, pexp r])
elab' ina fc (PAlternative ms (ExactlyOne delayok) as)
= do as_pruned <- doPrune as
-- Finish the mkUniqueNames job with the pruned set, rather than
-- the full set.
uns <- get_usedns
let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned
(h : hs) <- get_holes
ty <- goal
case as' of
[] -> do hds <- mapM showHd as
lift $ tfail $ NoValidAlts hds
[x] -> elab' ina fc x
-- If there's options, try now, and if that fails, postpone
-- to later.
_ -> handleError isAmbiguous
(do hds <- mapM showHd as'
tryAll (zip (map (elab' ina fc) as')
hds))
(do movelast h
delayElab 5 $ do
hs <- get_holes
when (h `elem` hs) $ do
focus h
as'' <- doPrune as'
case as'' of
[x] -> elab' ina fc x
_ -> do hds <- mapM showHd as''
tryAll' False (zip (map (elab' ina fc) as'')
hds))
where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])
| l == txt "Delay" = showHd (getTm arg)
showHd (PApp _ (PRef _ _ n) _) = return n
showHd (PRef _ _ n) = return n
showHd (PApp _ h _) = showHd h
showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
doPrune as =
do compute
ty <- goal
let (tc, _) = unApply (unDelay ty)
env <- get_env
return $ pruneByType env tc ist as
unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
l == txt "Lazy'" = unDelay arg
| otherwise = t
isAmbiguous (CantResolveAlts _) = delayok
isAmbiguous (Elaborating _ _ _ e) = isAmbiguous e
isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e
isAmbiguous (At _ e) = isAmbiguous e
isAmbiguous _ = False
elab' ina fc (PAlternative ms FirstSuccess as_in)
= do -- finish the mkUniqueNames job
uns <- get_usedns
let as = map (mkUniqueNames (uns ++ map snd ms) ms) as_in
trySeq as
where -- if none work, take the error from the first
trySeq (x : xs) = let e1 = elab' ina fc x in
try' e1 (trySeq' e1 xs) True
trySeq [] = fail "Nothing to try in sequence"
trySeq' deferr [] = proofFail deferr
trySeq' deferr (x : xs)
= try' (do elab' ina fc x
solveAutos ist fn False) (trySeq' deferr xs) True
elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do
env <- get_env
compute
ty <- goal
let doelab = elab' ina fc orig
tryCatch doelab
(\err ->
if recoverableErr err
then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++
-- show alts ++ "\n" ++
-- showQuick err) $
-- Prune the coercions so that only the ones
-- with the right type to fix the error will be tried!
case pruneAlts err alts env of
[] -> lift $ tfail err
alts' -> do
try' (elab' ina fc (PAlternative ms (ExactlyOne False) alts'))
(lift $ tfail err) -- take error from original if all fail
True
else lift $ tfail err)
where
recoverableErr (CantUnify _ _ _ _ _ _) = True
recoverableErr (TooManyArguments _) = False
recoverableErr (CantSolveGoal _ _) = False
recoverableErr (CantResolveAlts _) = False
recoverableErr (NoValidAlts _) = True
recoverableErr (ProofSearchFail (Msg _)) = True
recoverableErr (ProofSearchFail _) = False
recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e
recoverableErr (At _ e) = recoverableErr e
recoverableErr (ElabScriptDebug _ _ _) = False
recoverableErr _ = True
pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env
= case unApply (normalise (tt_ctxt ist) env inc) of
(P (TCon _ _) n _, _) -> filter (hasArg n env) alts
(Constant _, _) -> alts
_ -> filter isLend alts -- special case hack for 'Borrowed'
pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env
pruneAlts (At _ e) alts env = pruneAlts e alts env
pruneAlts (NoValidAlts as) alts env = alts
pruneAlts err alts _ = filter isLend alts
hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'
hasArg n env (PApp _ (PRef _ _ a) _)
= case lookupTyExact a (tt_ctxt ist) of
Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in
any (fnIs n) args
Nothing -> False
hasArg n env (PAlternative _ _ as) = any (hasArg n env) as
hasArg n _ tm = False
isLend (PApp _ (PRef _ _ l) _) = l == sNS (sUN "lend") ["Ownership"]
isLend _ = False
fnIs n ty = case unApply ty of
(P _ n' _, _) -> n == n'
_ -> False
showQuick (CantUnify _ (l, _) (r, _) _ _ _)
= show (l, r)
showQuick (ElaboratingArg _ _ _ e) = showQuick e
showQuick (At _ e) = showQuick e
showQuick (ProofSearchFail (Msg _)) = "search fail"
showQuick _ = "No chance"
elab' ina _ (PPatvar fc n) | bindfree
= do patvar n
update_term liftPats
highlightSource fc (AnnBoundName n False)
-- elab' (_, _, inty) (PRef fc f)
-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
-- = lift $ tfail (Msg "Typecase is not allowed")
elab' ec _ tm@(PRef fc hl n)
| pattern && not reflection && not (e_qq ec) && not (e_intype ec)
&& isTConName n (tt_ctxt ist)
= lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
| pattern && not reflection && not (e_qq ec) && e_nomatching ec
= lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
| (pattern || intransform || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
= do ty <- goal
testImplicitWarning fc n ty
let ina = e_inarg ec
guarded = e_guarded ec
inty = e_intype ec
ctxt <- get_context
let defined = case lookupTy n ctxt of
[] -> False
_ -> True
-- this is to stop us resolve type classes recursively
-- trace (show (n, guarded)) $
if (tcname n && ina && not intransform)
then erun fc $
do patvar n
update_term liftPats
highlightSource fc (AnnBoundName n False)
else if (defined && not guarded)
then do apply (Var n) []
annot <- findHighlight n
solve
highlightSource fc annot
else try (do apply (Var n) []
annot <- findHighlight n
solve
highlightSource fc annot)
(do patvar n
update_term liftPats
highlightSource fc (AnnBoundName n False))
where inparamBlock n = case lookupCtxtName n (inblock info) of
[] -> False
_ -> True
bindable (NS _ _) = False
bindable (MN _ _) = True
bindable n = implicitable n && autoimpls
elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])
elab' ina fc' tm@(PRef fc hls n)
| pattern && not reflection && not (e_qq ina) && not (e_intype ina)
&& isTConName n (tt_ctxt ist)
= lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
| pattern && not reflection && not (e_qq ina) && e_nomatching ina
= lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
| otherwise =
do fty <- get_type (Var n) -- check for implicits
ctxt <- get_context
env <- get_env
let a' = insertScopedImps fc (normalise ctxt env fty) []
if null a'
then erun fc $
do apply (Var n) []
hilite <- findHighlight n
solve
mapM_ (uncurry highlightSource) $
(fc, hilite) : map (\f -> (f, hilite)) hls
else elab' ina fc' (PApp fc tm [])
elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"
elab' ina _ (PLam fc n nfc Placeholder sc)
= do -- if n is a type constructor name, this makes no sense...
ctxt <- get_context
when (isTConName n ctxt) $
lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
checkPiGoal n
attack; intro (Just n);
addPSname n -- okay for proof search
-- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
elabE (ina { e_inarg = True } ) (Just fc) sc; solve
highlightSource nfc (AnnBoundName n False)
elab' ec _ (PLam fc n nfc ty sc)
= do tyn <- getNameFrom (sMN 0 "lamty")
-- if n is a type constructor name, this makes no sense...
ctxt <- get_context
when (isTConName n ctxt) $
lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
checkPiGoal n
claim tyn RType
explicit tyn
attack
ptm <- get_term
hs <- get_holes
introTy (Var tyn) (Just n)
addPSname n -- okay for proof search
focus tyn
elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty
elabE (ec { e_inarg = True }) (Just fc) sc
solve
highlightSource nfc (AnnBoundName n False)
elab' ina fc (PPi p n nfc Placeholder sc)
= do attack; arg n (is_scoped p) (sMN 0 "ty")
addAutoBind p n
addPSname n -- okay for proof search
elabE (ina { e_inarg = True, e_intype = True }) fc sc
solve
highlightSource nfc (AnnBoundName n False)
elab' ina fc (PPi p n nfc ty sc)
= do attack; tyn <- getNameFrom (sMN 0 "ty")
claim tyn RType
n' <- case n of
MN _ _ -> unique_hole n
_ -> return n
forall n' (is_scoped p) (Var tyn)
addAutoBind p n'
addPSname n' -- okay for proof search
focus tyn
let ec' = ina { e_inarg = True, e_intype = True }
elabE ec' fc ty
elabE ec' fc sc
solve
highlightSource nfc (AnnBoundName n False)
elab' ina _ tm@(PLet fc n nfc ty val sc)
= do attack
ivs <- get_instances
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
explicit valn
letbind n (Var tyn) (Var valn)
addPSname n
case ty of
Placeholder -> return ()
_ -> do focus tyn
explicit tyn
elabE (ina { e_inarg = True, e_intype = True })
(Just fc) ty
focus valn
elabE (ina { e_inarg = True, e_intype = True })
(Just fc) val
ivs' <- get_instances
env <- get_env
elabE (ina { e_inarg = True }) (Just fc) sc
when (not (pattern || intransform)) $
mapM_ (\n -> do focus n
g <- goal
hs <- get_holes
if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
then handleError (tcRecoverable emode)
(resolveTC' True False 10 g fn ist)
(movelast n)
else movelast n)
(ivs' \\ ivs)
-- HACK: If the name leaks into its type, it may leak out of
-- scope outside, so substitute in the outer scope.
expandLet n (case lookup n env of
Just (Let t v) -> v
other -> error ("Value not a let binding: " ++ show other))
solve
highlightSource nfc (AnnBoundName n False)
elab' ina _ (PGoal fc r n sc) = do
rty <- goal
attack
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
letbind n (Var tyn) (Var valn)
focus valn
elabE (ina { e_inarg = True, e_intype = True }) (Just fc) (PApp fc r [pexp (delab ist rty)])
env <- get_env
computeLet n
elabE (ina { e_inarg = True }) (Just fc) sc
solve
-- elab' ina fc (PLet n Placeholder
-- (PApp fc r [pexp (delab ist rty)]) sc)
elab' ina _ tm@(PApp fc (PInferRef _ _ f) args) = do
rty <- goal
ds <- get_deferred
ctxt <- get_context
-- make a function type a -> b -> c -> ... -> rty for the
-- new function name
env <- get_env
argTys <- claimArgTys env args
fn <- getNameFrom (sMN 0 "inf_fn")
let fty = fnTy argTys rty
-- trace (show (ptm, map fst argTys)) $ focus fn
-- build and defer the function application
attack; deferType (mkN f) fty (map fst argTys); solve
-- elaborate the arguments, to unify their types. They all have to
-- be explicit.
mapM_ elabIArg (zip argTys args)
where claimArgTys env [] = return []
claimArgTys env (arg : xs) | Just n <- localVar env (getTm arg)
= do nty <- get_type (Var n)
ans <- claimArgTys env xs
return ((n, (False, forget nty)) : ans)
claimArgTys env (_ : xs)
= do an <- getNameFrom (sMN 0 "inf_argTy")
aval <- getNameFrom (sMN 0 "inf_arg")
claim an RType
claim aval (Var an)
ans <- claimArgTys env xs
return ((aval, (True, (Var an))) : ans)
fnTy [] ret = forget ret
fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret)
localVar env (PRef _ _ x)
= case lookup x env of
Just _ -> Just x
_ -> Nothing
localVar env _ = Nothing
elabIArg ((n, (True, ty)), def) =
do focus n; elabE ina (Just fc) (getTm def)
elabIArg _ = return () -- already done, just a name
mkN n@(NS _ _) = n
mkN n@(SN _) = n
mkN n = case namespace info of
Just xs@(_:_) -> sNS n xs
_ -> n
elab' ina _ (PMatchApp fc fn)
= do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
[(n, args)] -> return (n, map (const True) args)
_ -> lift $ tfail (NoSuchVariable fn)
ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
solve
-- if f is local, just do a simple_app
-- FIXME: Anyone feel like refactoring this mess? - EB
elab' ina topfc tm@(PApp fc (PRef ffc hls f) args_in)
| pattern && not reflection && not (e_qq ina) && e_nomatching ina
= lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
| otherwise = implicitApp $
do env <- get_env
ty <- goal
fty <- get_type (Var f)
ctxt <- get_context
annot <- findHighlight f
mapM_ checkKnownImplicit args_in
let args = insertScopedImps fc (normalise ctxt env fty) args_in
let unmatchableArgs = if pattern
then getUnmatchable (tt_ctxt ist) f
else []
-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $
when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
&& isTConName f (tt_ctxt ist)) $
lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
-- trace (show (f, args_in, args)) $
if (f `elem` map fst env && length args == 1 && length args_in == 1)
then -- simple app, as below
do simple_app False
(elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))
(elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
(show tm)
solve
mapM (uncurry highlightSource) $
(ffc, annot) : map (\f -> (f, annot)) hls
return []
else
do ivs <- get_instances
ps <- get_probs
-- HACK: we shouldn't resolve type classes if we're defining an instance
-- function or default definition.
let isinf = f == inferCon || tcname f
-- if f is a type class, we need to know its arguments so that
-- we can unify with them
case lookupCtxt f (idris_classes ist) of
[] -> return ()
_ -> do mapM_ setInjective (map getTm args)
-- maybe more things are solvable now
unifyProblems
let guarded = isConName f ctxt
-- trace ("args is " ++ show args) $ return ()
ns <- apply (Var f) (map isph args)
-- trace ("ns is " ++ show ns) $ return ()
-- mark any type class arguments as injective
when (not pattern) $ mapM_ checkIfInjective (map snd ns)
unifyProblems -- try again with the new information,
-- to help with disambiguation
ulog <- getUnifyLog
annot <- findHighlight f
mapM (uncurry highlightSource) $
(ffc, annot) : map (\f -> (f, annot)) hls
elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
[] fc False f
(zip ns (unmatchableArgs ++ repeat False))
(f == sUN "Force")
(map (\x -> getTm x) args) -- TODO: remove this False arg
imp <- if (e_isfn ina) then
do guess <- get_guess
env <- get_env
case safeForgetEnv (map fst env) guess of
Nothing ->
return []
Just rguess -> do
gty <- get_type rguess
let ty_n = normalise ctxt env gty
return $ getReqImps ty_n
else return []
-- Now we find out how many implicits we needed at the
-- end of the application by looking at the goal again
-- - Have another go, but this time add the
-- implicits (can't think of a better way than this...)
case imp of
rs@(_:_) | not pattern -> return rs -- quit, try again
_ -> do solve
hs <- get_holes
ivs' <- get_instances
-- Attempt to resolve any type classes which have 'complete' types,
-- i.e. no holes in them
when (not pattern || (e_inarg ina && not tcgen &&
not (e_guarded ina))) $
mapM_ (\n -> do focus n
g <- goal
env <- get_env
hs <- get_holes
if all (\n -> not (n `elem` hs)) (freeNames g)
then handleError (tcRecoverable emode)
(resolveTC' False False 10 g fn ist)
(movelast n)
else movelast n)
(ivs' \\ ivs)
return []
where
-- Run the elaborator, which returns how many implicit
-- args were needed, then run it again with those args. We need
-- this because we have to elaborate the whole application to
-- find out whether any computations have caused more implicits
-- to be needed.
implicitApp :: ElabD [ImplicitInfo] -> ElabD ()
implicitApp elab
| pattern || intransform = do elab; return ()
| otherwise
= do s <- get
imps <- elab
case imps of
[] -> return ()
es -> do put s
elab' ina topfc (PAppImpl tm es)
checkKnownImplicit imp
| UnknownImp `elem` argopts imp
= lift $ tfail $ UnknownImplicit (pname imp) f
checkKnownImplicit _ = return ()
getReqImps (Bind x (Pi (Just i) ty _) sc)
= i : getReqImps sc
getReqImps _ = []
checkIfInjective n = do
env <- get_env
case lookup n env of
Nothing -> return ()
Just b ->
case unApply (normalise (tt_ctxt ist) env (binderTy b)) of
(P _ c _, args) ->
case lookupCtxtExact c (idris_classes ist) of
Nothing -> return ()
Just ci -> -- type class, set as injective
do mapM_ setinjArg (getDets 0 (class_determiners ci) args)
-- maybe we can solve more things now...
ulog <- getUnifyLog
probs <- get_probs
traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $
unifyProblems
probs <- get_probs
traceWhen ulog (qshow probs) $ return ()
_ -> return ()
setinjArg (P _ n _) = setinj n
setinjArg _ = return ()
getDets i ds [] = []
getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as
| otherwise = getDets (i + 1) ds as
tacTm (PTactics _) = True
tacTm (PProof _) = True
tacTm _ = False
setInjective (PRef _ _ n) = setinj n
setInjective (PApp _ (PRef _ _ n) _) = setinj n
setInjective _ = return ()
elab' ina _ tm@(PApp fc f [arg]) =
erun fc $
do simple_app (not $ headRef f)
(elabE (ina { e_isfn = True }) (Just fc) f)
(elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
(show tm)
solve
where headRef (PRef _ _ _) = True
headRef (PApp _ f _) = headRef f
headRef (PAlternative _ _ as) = all headRef as
headRef _ = False
elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...
solve
where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits
appImpl (e : es) = simple_app False
(appImpl es)
(elab' ina fc Placeholder)
(show f)
elab' ina fc Placeholder
= do (h : hs) <- get_holes
movelast h
elab' ina fc (PMetavar nfc n) =
do ptm <- get_term
-- When building the metavar application, leave out the unique
-- names which have been used elsewhere in the term, since we
-- won't be able to use them in the resulting application.
let unique_used = getUniqueUsed (tt_ctxt ist) ptm
let n' = metavarName (namespace info) n
attack
psns <- getPSnames
n' <- defer unique_used n'
solve
highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)
elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts
elab' ina fc (PTactics ts)
| not pattern = do mapM_ (runTac False ist fc fn) ts
| otherwise = elab' ina fc Placeholder
elab' ina fc (PElabError e) = lift $ tfail e
elab' ina _ (PRewrite fc r sc newg)
= do attack
tyn <- getNameFrom (sMN 0 "rty")
claim tyn RType
valn <- getNameFrom (sMN 0 "rval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "_rewrite_rule")
letbind letn (Var tyn) (Var valn)
focus valn
elab' ina (Just fc) r
compute
g <- goal
rewrite (Var letn)
g' <- goal
when (g == g') $ lift $ tfail (NoRewriting g)
case newg of
Nothing -> elab' ina (Just fc) sc
Just t -> doEquiv t sc
solve
where doEquiv t sc =
do attack
tyn <- getNameFrom (sMN 0 "ety")
claim tyn RType
valn <- getNameFrom (sMN 0 "eqval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "equiv_val")
letbind letn (Var tyn) (Var valn)
focus tyn
elab' ina (Just fc) t
focus valn
elab' ina (Just fc) sc
elab' ina (Just fc) (PRef fc [] letn)
solve
elab' ina _ c@(PCase fc scr opts)
= do attack
tyn <- getNameFrom (sMN 0 "scty")
claim tyn RType
valn <- getNameFrom (sMN 0 "scval")
scvn <- getNameFrom (sMN 0 "scvar")
claim valn (Var tyn)
letbind scvn (Var tyn) (Var valn)
-- Start filling in the scrutinee type, if we can work one
-- out from the case options
let scrTy = getScrType (map fst opts)
case scrTy of
Nothing -> return ()
Just ty -> do focus tyn
elabE ina (Just fc) ty
focus valn
elabE (ina { e_inarg = True }) (Just fc) scr
-- Solve any remaining implicits - we need to solve as many
-- as possible before making the 'case' type
unifyProblems
matchProblems True
args <- get_env
envU <- mapM (getKind args) args
let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
-- Drop the unique arguments used in the term already
-- and in the scrutinee (since it's
-- not valid to use them again anyway)
--
-- Also drop unique arguments which don't appear explicitly
-- in either case branch so they don't count as used
-- unnecessarily (can only do this for unique things, since we
-- assume they don't appear implicitly in types)
ptm <- get_term
let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
let argsDropped = filter (isUnique envU)
(nub $ allNamesIn scr ++ inApp ptm ++
inOpts)
let args' = filter (\(n, _) -> n `notElem` argsDropped) args
attack
cname' <- defer argsDropped (mkN (mkCaseName fc fn))
solve
-- if the scrutinee is one of the 'args' in env, we should
-- inspect it directly, rather than adding it as a new argument
let newdef = PClauses fc [] cname'
(caseBlock fc cname' scr
(map (isScr scr) (reverse args')) opts)
-- elaborate case
updateAux (\e -> e { case_decls = (cname', newdef) : case_decls e } )
-- if we haven't got the type yet, hopefully we'll get it later!
movelast tyn
solve
where mkCaseName fc (NS n ns) = NS (mkCaseName fc n) ns
mkCaseName fc n = SN (CaseN (FC' fc) n)
-- mkCaseName (UN x) = UN (x ++ "_case")
-- mkCaseName (MN i x) = MN i (x ++ "_case")
mkN n@(NS _ _) = n
mkN n = case namespace info of
Just xs@(_:_) -> sNS n xs
_ -> n
getScrType [] = Nothing
getScrType (f : os) = maybe (getScrType os) Just (getAppType f)
getAppType (PRef _ _ n) =
case lookupTyName n (tt_ctxt ist) of
[(n', ty)] | isDConName n' (tt_ctxt ist) ->
case unApply (getRetTy ty) of
(P _ tyn _, args) ->
Just (PApp fc (PRef fc [] tyn)
(map pexp (map (const Placeholder) args)))
_ -> Nothing
_ -> Nothing -- ambiguity is no help to us!
getAppType (PApp _ t as) = getAppType t
getAppType _ = Nothing
inApp (P _ n _) = [n]
inApp (App _ f a) = inApp f ++ inApp a
inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc
inApp (Bind n b sc) = inApp sc
inApp _ = []
isUnique envk n = case lookup n envk of
Just u -> u
_ -> False
getKind env (n, _)
= case lookup n env of
Nothing -> return (n, False) -- can't happen, actually...
Just b ->
do ty <- get_type (forget (binderTy b))
case ty of
UType UniqueType -> return (n, True)
UType AllTypes -> return (n, True)
_ -> return (n, False)
tcName tm | (P _ n _, _) <- unApply tm
= case lookupCtxt n (idris_classes ist) of
[_] -> True
_ -> False
tcName _ = False
usedIn ns (n, b)
= n `elem` ns
|| any (\x -> x `elem` ns) (allTTNames (binderTy b))
elab' ina fc (PUnifyLog t) = do unifyLog True
elab' ina fc t
unifyLog False
elab' ina fc (PQuasiquote t goalt)
= do -- First extract the unquoted subterms, replacing them with fresh
-- names in the quasiquoted term. Claim their reflections to be
-- an inferred type (to support polytypic quasiquotes).
finalTy <- goal
(t, unq) <- extractUnquotes 0 t
let unquoteNames = map fst unq
mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames
-- Save the old state - we need a fresh proof state to avoid
-- capturing lexically available variables in the quoted term.
ctxt <- get_context
datatypes <- get_datatypes
g_nextname <- get_global_nextname
saveState
updatePS (const .
newProof (sMN 0 "q") ctxt datatypes g_nextname $
P Ref (reflm "TT") Erased)
-- Re-add the unquotes, letting Idris infer the (fictional)
-- types. Here, they represent the real type rather than the type
-- of their reflection.
mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
claim ty RType
movelast ty
claim n (Var ty)
movelast n)
unquoteNames
-- Determine whether there's an explicit goal type, and act accordingly
-- Establish holes for the type and value of the term to be
-- quasiquoted
qTy <- getNameFrom (sMN 0 "qquoteTy")
claim qTy RType
movelast qTy
qTm <- getNameFrom (sMN 0 "qquoteTm")
claim qTm (Var qTy)
-- Let-bind the result of elaborating the contained term, so that
-- the hole doesn't disappear
nTm <- getNameFrom (sMN 0 "quotedTerm")
letbind nTm (Var qTy) (Var qTm)
-- Fill out the goal type, if relevant
case goalt of
Nothing -> return ()
Just gTy -> do focus qTy
elabE (ina { e_qq = True }) fc gTy
-- Elaborate the quasiquoted term into the hole
focus qTm
elabE (ina { e_qq = True }) fc t
end_unify
-- We now have an elaborated term. Reflect it and solve the
-- original goal in the original proof state, preserving highlighting
env <- get_env
EState _ _ _ hs _ _ <- getAux
loadState
updateAux (\aux -> aux { highlighting = hs })
let quoted = fmap (explicitNames . binderVal) $ lookup nTm env
isRaw = case unApply (normaliseAll ctxt env finalTy) of
(P _ n _, []) | n == reflm "Raw" -> True
_ -> False
case quoted of
Just q -> do ctxt <- get_context
(q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
if pattern
then if isRaw
then reflectRawQuotePattern unquoteNames (forget q')
else reflectTTQuotePattern unquoteNames q'
else do if isRaw
then -- we forget q' instead of using q to ensure rechecking
fill $ reflectRawQuote unquoteNames (forget q')
else fill $ reflectTTQuote unquoteNames q'
solve
Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
-- Finally fill in the terms or patterns from the unquotes. This
-- happens last so that their holes still exist while elaborating
-- the main quotation.
mapM_ elabUnquote unq
where elabUnquote (n, tm)
= do focus n
elabE (ina { e_qq = False }) fc tm
elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
elab' ina fc (PQuoteName n False nfc) =
do fill $ reflectName n
solve
elab' ina fc (PQuoteName n True nfc) =
do ctxt <- get_context
env <- get_env
case lookup n env of
Just _ -> do fill $ reflectName n
solve
highlightSource nfc (AnnBoundName n False)
Nothing ->
case lookupNameDef n ctxt of
[(n', _)] -> do fill $ reflectName n'
solve
highlightSource nfc (AnnName n' Nothing Nothing Nothing)
[] -> lift . tfail . NoSuchVariable $ n
more -> lift . tfail . CantResolveAlts $ map fst more
elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
elab' ina fc (PHidden t)
| reflection = elab' ina fc t
| otherwise
= do (h : hs) <- get_holes
-- Dotting a hole means that either the hole or any outer
-- hole (a hole outside any occurrence of it)
-- must be solvable by unification as well as being filled
-- in directly.
-- Delay dotted things to the end, then when we elaborate them
-- we can check the result against what was inferred
movelast h
delayElab 10 $ do focus h
dotterm
elab' ina fc t
elab' ina fc (PRunElab fc' tm ns) =
do attack
n <- getNameFrom (sMN 0 "tacticScript")
let scriptTy = RApp (Var (sNS (sUN "Elab")
["Elab", "Reflection", "Language"]))
(Var unitTy)
claim n scriptTy
focus n
attack -- to get an extra hole
elab' ina (Just fc') tm
script <- get_guess
fullyElaborated script
solve -- eliminate the hole. Becuase there are no references, the script is only in the binding
env <- get_env
runElabAction ist (maybe fc' id fc) env script ns
solve
elab' ina fc (PConstSugar constFC tm) =
-- Here we elaborate the contained term, then calculate
-- highlighting for constFC. The highlighting is the
-- highlighting for the outermost constructor of the result of
-- evaluating the elaborated term, if one exists (it always
-- should, but better to fail gracefully for something silly
-- like highlighting info). This is how implicit applications of
-- fromInteger get highlighted.
do saveState -- so we don't pollute the elaborated term
n <- getNameFrom (sMN 0 "cstI")
n' <- getNameFrom (sMN 0 "cstIhole")
g <- forget <$> goal
claim n' g
movelast n'
-- In order to intercept the elaborated value, we need to
-- let-bind it.
attack
letbind n g (Var n')
focus n'
elab' ina fc tm
env <- get_env
ctxt <- get_context
let v = fmap (normaliseAll ctxt env . finalise . binderVal)
(lookup n env)
loadState -- we have the highlighting - re-elaborate the value
elab' ina fc tm
case v of
Just val -> highlightConst constFC val
Nothing -> return ()
where highlightConst fc (P _ n _) =
highlightSource fc (AnnName n Nothing Nothing Nothing)
highlightConst fc (App _ f _) =
highlightConst fc f
highlightConst fc (Constant c) =
highlightSource fc (AnnConst c)
highlightConst _ _ = return ()
elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
-- delay elaboration of 't', with priority 'pri' until after everything
-- else is done.
-- The delayed things with lower numbered priority will be elaborated
-- first. (In practice, this means delayed alternatives, then PHidden
-- things.)
delayElab pri t
= updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })
isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
isScr (PRef _ _ n) (n', b) = (n', (n == n', b))
isScr _ (n', b) = (n', (False, b))
caseBlock :: FC -> Name
-> PTerm -- original scrutinee
-> [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]
caseBlock fc n scr env opts
= let args' = findScr env
args = map mkarg (map getNmScr args') in
map (mkClause args) opts
where -- Find the variable we want as the scrutinee and mark it as
-- 'True'. If the scrutinee is in the environment, match on that
-- otherwise match on the new argument we're adding.
findScr ((n, (True, t)) : xs)
= (n, (True, t)) : scrName n xs
findScr [(n, (_, t))] = [(n, (True, t))]
findScr (x : xs) = x : findScr xs
-- [] can't happen since scrutinee is in the environment!
findScr [] = error "The impossible happened - the scrutinee was not in the environment"
-- To make sure top level pattern name remains in scope, put
-- it at the end of the environment
scrName n [] = []
scrName n [(_, t)] = [(n, t)]
scrName n (x : xs) = x : scrName n xs
getNmScr (n, (s, _)) = (n, s)
mkarg (n, s) = (PRef fc [] n, s)
-- may be shadowed names in the new pattern - so replace the
-- old ones with an _
-- Also, names which don't appear on the rhs should not be
-- fixed on the lhs, or this restricts the kind of matching
-- we can do to non-dependent types.
mkClause args (l, r)
= let args' = map (shadowed (allNamesIn l)) args
args'' = map (implicitable (allNamesIn r ++
keepscrName scr)) args'
lhs = PApp (getFC fc l) (PRef NoFC [] n)
(map (mkLHSarg l) args'') in
PClause (getFC fc l) n lhs [] r []
-- Keep scrutinee available if it's just a name (this makes
-- the names in scope look better when looking at a hole on
-- the rhs of a case)
keepscrName (PRef _ _ n) = [n]
keepscrName _ = []
mkLHSarg l (tm, True) = pexp l
mkLHSarg l (tm, False) = pexp tm
shadowed new (PRef _ _ n, s) | n `elem` new = (Placeholder, s)
shadowed new t = t
implicitable rhs (PRef _ _ n, s) | n `notElem` rhs = (Placeholder, s)
implicitable rhs t = t
getFC d (PApp fc _ _) = fc
getFC d (PRef fc _ _) = fc
getFC d (PAlternative _ _ (x:_)) = getFC d x
getFC d x = d
-- Fail if a term is not yet fully elaborated (e.g. if it contains
-- case block functions that don't yet exist)
fullyElaborated :: Term -> ElabD ()
fullyElaborated (P _ n _) =
do estate <- getAux
case lookup n (case_decls estate) of
Nothing -> return ()
Just _ -> lift . tfail $ ElabScriptStaging n
fullyElaborated (Bind n b body) = fullyElaborated body >> for_ b fullyElaborated
fullyElaborated (App _ l r) = fullyElaborated l >> fullyElaborated r
fullyElaborated (Proj t _) = fullyElaborated t
fullyElaborated _ = return ()
insertLazy :: PTerm -> ElabD PTerm
insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t
insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t
insertLazy (PCoerced t) = return t
insertLazy t =
do ty <- goal
env <- get_env
let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t]
case tyh of
P _ (UN l) _ | l == txt "Lazy'"
-> return (PAlternative [] FirstSuccess tries)
_ -> return t
where
mkDelay env (PAlternative ms b xs) = PAlternative ms b (map (mkDelay env) xs)
mkDelay env t
= let fc = fileFC "Delay" in
addImplBound ist (map fst env) (PApp fc (PRef fc [] (sUN "Delay"))
[pexp t])
-- Don't put implicit coercions around applications which are marked
-- as '%noImplicit', or around case blocks, otherwise we get exponential
-- blowup especially where there are errors deep in large expressions.
notImplicitable (PApp _ f _) = notImplicitable f
-- TMP HACK no coercing on bind (make this configurable)
notImplicitable (PRef _ _ n)
| [opts] <- lookupCtxt n (idris_flags ist)
= NoImplicit `elem` opts
notImplicitable (PAlternative _ _ as) = any notImplicitable as
-- case is tricky enough without implicit coercions! If they are needed,
-- they can go in the branches separately.
notImplicitable (PCase _ _ _) = True
notImplicitable _ = False
insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs
| tcinstance i && not (toplevel_imp i)
= pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
| not (toplevel_imp i)
= pimp n Placeholder True : insertScopedImps fc sc xs
insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)
= x : insertScopedImps fc sc xs
insertScopedImps _ _ xs = xs
insertImpLam ina t =
do ty <- goal
env <- get_env
let ty' = normalise (tt_ctxt ist) env ty
addLam ty' t
where
-- just one level at a time
addLam (Bind n (Pi (Just _) _ _) sc) t =
do impn <- unique_hole n -- (sMN 0 "scoped_imp")
if e_isfn ina -- apply to an implicit immediately
then return (PApp emptyFC
(PLam emptyFC impn NoFC Placeholder t)
[pexp Placeholder])
else return (PLam emptyFC impn NoFC Placeholder t)
addLam _ t = return t
insertCoerce ina t@(PCase _ _ _) = return t
insertCoerce ina t | notImplicitable t = return t
insertCoerce ina t =
do ty <- goal
-- Check for possible coercions to get to the goal
-- and add them as 'alternatives'
env <- get_env
let ty' = normalise (tt_ctxt ist) env ty
let cs = getCoercionsTo ist ty'
let t' = case (t, cs) of
(PCoerced tm, _) -> tm
(_, []) -> t
(_, cs) -> PAlternative [] TryImplicit
(t : map (mkCoerce env t) cs)
return t'
where
mkCoerce env (PAlternative ms aty tms) n
= PAlternative ms aty (map (\t -> mkCoerce env t n) tms)
mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in
addImplBound ist (map fst env)
(PApp fc (PRef fc [] n) [pexp (PCoerced t)])
-- | Elaborate the arguments to a function
elabArgs :: IState -- ^ The current Idris state
-> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote)
-> [Bool]
-> FC -- ^ Source location
-> Bool
-> Name -- ^ Name of the function being applied
-> [((Name, Name), Bool)] -- ^ (Argument Name, Hole Name, unmatchable)
-> Bool -- ^ under a 'force'
-> [PTerm] -- ^ argument
-> ElabD ()
elabArgs ist ina failed fc retry f [] force _ = return ()
elabArgs ist ina failed fc r f (((argName, holeName), unm):ns) force (t : args)
= do hs <- get_holes
if holeName `elem` hs then
do focus holeName
case t of
Placeholder -> do movelast holeName
elabArgs ist ina failed fc r f ns force args
_ -> elabArg t
else elabArgs ist ina failed fc r f ns force args
where elabArg t =
do -- solveAutos ist fn False
now_elaborating fc f argName
wrapErr f argName $ do
hs <- get_holes
tm <- get_term
-- No coercing under an explicit Force (or it can Force/Delay
-- recursively!)
let elab = if force then elab' else elabE
failed' <- -- trace (show (n, t, hs, tm)) $
-- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
do focus holeName;
g <- goal
-- Can't pattern match on polymorphic goals
poly <- goal_polymorphic
ulog <- getUnifyLog
traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
elab (ina { e_nomatching = unm && poly }) (Just fc) t
return failed
done_elaborating_arg f argName
elabArgs ist ina failed fc r f ns force args
wrapErr f argName action =
do elabState <- get
while <- elaborating_app
let while' = map (\(x, y, z)-> (y, z)) while
(result, newState) <- case runStateT action elabState of
OK (res, newState) -> return (res, newState)
Error e -> do done_elaborating_arg f argName
lift (tfail (elaboratingArgErr while' e))
put newState
return result
elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =
fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
addAutoBind :: Plicity -> Name -> ElabD ()
addAutoBind (Imp _ _ _ _ False) n
= updateAux (\est -> est { auto_binds = n : auto_binds est })
addAutoBind _ _ = return ()
testImplicitWarning :: FC -> Name -> Type -> ElabD ()
testImplicitWarning fc n goal
| implicitable n && emode == ETyDecl
= do env <- get_env
est <- getAux
when (n `elem` auto_binds est) $
tryUnify env (lookupTyName n (tt_ctxt ist))
| otherwise = return ()
where
tryUnify env [] = return ()
tryUnify env ((nm, ty) : ts)
= do inj <- get_inj
hs <- get_holes
case unify (tt_ctxt ist) env (ty, Nothing) (goal, Nothing)
inj hs [] [] of
OK _ ->
updateAux (\est -> est { implicit_warnings =
(fc, nm) : implicit_warnings est })
_ -> tryUnify env ts
-- For every alternative, look at the function at the head. Automatically resolve
-- any nested alternatives where that function is also at the head
pruneAlt :: [PTerm] -> [PTerm]
pruneAlt xs = map prune xs
where
prune (PApp fc1 (PRef fc2 hls f) as)
= PApp fc1 (PRef fc2 hls f) (fmap (fmap (choose f)) as)
prune t = t
choose f (PAlternative ms a as)
= let as' = fmap (choose f) as
fs = filter (headIs f) as' in
case fs of
[a] -> a
_ -> PAlternative ms a as'
choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)
choose f t = t
headIs f (PApp _ (PRef _ _ f') _) = f == f'
headIs f (PApp _ f' _) = headIs f f'
headIs f _ = True -- keep if it's not an application
-- Rule out alternatives that don't return the same type as the head of the goal
-- (If there are none left as a result, do nothing)
pruneByType :: Env -> Term -> -- head of the goal
IState -> [PTerm] -> [PTerm]
-- if an alternative has a locally bound name at the head, take it
pruneByType env t c as
| Just a <- locallyBound as = [a]
where
locallyBound [] = Nothing
locallyBound (t:ts)
| Just n <- getName t,
n `elem` map fst env = Just t
| otherwise = locallyBound ts
getName (PRef _ _ n) = Just n
getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays
| l == txt "Delay" = getName (getTm arg)
getName (PApp _ f _) = getName f
getName (PHidden t) = getName t
getName _ = Nothing
-- 'n' is the name at the head of the goal type
pruneByType env (P _ n _) ist as
-- if the goal type is polymorphic, keep everything
| Nothing <- lookupTyExact n ctxt = as
-- if the goal type is a ?metavariable, keep everything
| Just _ <- lookup n (idris_metavars ist) = as
| otherwise
= let asV = filter (headIs True n) as
as' = filter (headIs False n) as in
case as' of
[] -> asV
_ -> as'
where
ctxt = tt_ctxt ist
headIs var f (PRef _ _ f') = typeHead var f f'
headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
| l == txt "Delay" = headIs var f (getTm arg)
headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'
headIs var f (PApp _ f' _) = headIs var f f'
headIs var f (PPi _ _ _ _ sc) = headIs var f sc
headIs var f (PHidden t) = headIs var f t
headIs var f t = True -- keep if it's not an application
typeHead var f f'
= -- trace ("Trying " ++ show f' ++ " for " ++ show n) $
case lookupTyExact f' ctxt of
Just ty -> case unApply (getRetTy ty) of
(P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f
_ -> let ty' = normalise ctxt [] ty in
case unApply (getRetTy ty') of
(P _ ftyn _, _) -> ftyn == f
(V _, _) ->
-- keep, variable
-- trace ("Keeping " ++ show (f', ty')
-- ++ " for " ++ show n) $
isPlausible ist var env n ty
_ -> False
_ -> False
pruneByType _ t _ as = as
-- Could the name feasibly be the return type?
-- If there is a type class constraint on the return type, and no instance
-- in the environment or globally for that name, then no
-- Otherwise, yes
-- (FIXME: This isn't complete, but I'm leaving it here and coming back
-- to it later - just returns 'var' for now. EB)
isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
isPlausible ist var env n ty
= let (hvar, classes) = collectConstraints [] [] ty in
case hvar of
Nothing -> True
Just rth -> var -- trace (show (rth, classes)) var
where
collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
(Maybe Name, [(Term, [Name])])
collectConstraints env tcs (Bind n (Pi _ ty _) sc)
= let tcs' = case unApply ty of
(P _ c _, _) ->
case lookupCtxtExact c (idris_classes ist) of
Just tc -> ((ty, map fst (class_instances tc))
: tcs)
Nothing -> tcs
_ -> tcs
in
collectConstraints (n : env) tcs' sc
collectConstraints env tcs t
| (V i, _) <- unApply t = (Just (env !! i), tcs)
| otherwise = (Nothing, tcs)
-- | Use the local elab context to work out the highlighting for a name
findHighlight :: Name -> ElabD OutputAnnotation
findHighlight n = do ctxt <- get_context
env <- get_env
case lookup n env of
Just _ -> return $ AnnBoundName n False
Nothing -> case lookupTyExact n ctxt of
Just _ -> return $ AnnName n Nothing Nothing Nothing
Nothing -> lift . tfail . InternalMsg $
"Can't find name " ++ show n
-- Try again to solve auto implicits
solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()
solveAuto ist fn ambigok (n, failc)
= do hs <- get_holes
when (not (null hs)) $ do
env <- get_env
g <- goal
handleError cantsolve (when (n `elem` hs) $ do
focus n
isg <- is_guess -- if it's a guess, we're working on it recursively, so stop
when (not isg) $
proofSearch' ist True ambigok 100 True Nothing fn [] [])
(lift $ Error (addLoc failc
(CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))))
return ()
where addLoc (FailContext fc f x : prev) err
= At fc (ElaboratingArg f x
(map (\(FailContext _ f' x') -> (f', x')) prev) err)
addLoc _ err = err
cantsolve (CantSolveGoal _ _) = True
cantsolve (InternalMsg _) = True
cantsolve (At _ e) = cantsolve e
cantsolve (Elaborating _ _ _ e) = cantsolve e
cantsolve (ElaboratingArg _ _ _ e) = cantsolve e
cantsolve _ = False
solveAutos :: IState -> Name -> Bool -> ElabD ()
solveAutos ist fn ambigok
= do autos <- get_autos
mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)
-- Return true if the given error suggests a type class failure is
-- recoverable
tcRecoverable :: ElabMode -> Err -> Bool
tcRecoverable ERHS (CantResolve f g _) = f
tcRecoverable ETyDecl (CantResolve f g _) = f
tcRecoverable e (ElaboratingArg _ _ _ err) = tcRecoverable e err
tcRecoverable e (At _ err) = tcRecoverable e err
tcRecoverable _ _ = True
trivial' ist
= trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
trivialHoles' psn h ist
= trivialHoles psn h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
proofSearch' ist rec ambigok depth prv top n psns hints
= do unifyProblems
proofSearch rec prv ambigok (not prv) depth
(elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist
resolveTC' di mv depth tm n ist
= resolveTC di mv depth tm n (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
collectDeferred :: Maybe Name -> [Name] -> Context ->
Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term
collectDeferred top casenames ctxt tm = cd [] tm
where
cd env (Bind n (GHole i psns t) app) =
do ds <- get
t' <- collectDeferred top casenames ctxt t
when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])
cd env app
cd env (Bind n b t)
= do b' <- cdb b
t' <- cd ((n, b) : env) t
return (Bind n b' t')
where
cdb (Let t v) = liftM2 Let (cd env t) (cd env v)
cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)
cdb b = do ty' <- cd env (binderTy b)
return (b { binderTy = ty' })
cd env (App s f a) = liftM2 (App s) (cd env f)
(cd env a)
cd env t = return t
case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
case_ ind autoSolve ist fn tm = do
attack
tyn <- getNameFrom (sMN 0 "ity")
claim tyn RType
valn <- getNameFrom (sMN 0 "ival")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "irule")
letbind letn (Var tyn) (Var valn)
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") tm
env <- get_env
let (Just binding) = lookup letn env
let val = binderVal binding
if ind then induction (forget val)
else casetac (forget val)
when autoSolve solveAll
-- | Compute the appropriate name for a top-level metavariable
metavarName :: Maybe [String] -> Name -> Name
metavarName _ n@(NS _ _) = n
metavarName (Just (ns@(_:_))) n = sNS n ns
metavarName _ n = n
runElabAction :: IState -> FC -> Env -> Term -> [String] -> ElabD Term
runElabAction ist fc env tm ns = do tm' <- eval tm
runTacTm tm'
where
eval tm = do ctxt <- get_context
return $ normaliseAll ctxt env (finalise tm)
returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)
patvars ns (Bind n (PVar t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)
patvars ns tm = (ns, tm)
pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)
pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
requireError :: Err -> ElabD a -> ElabD ()
requireError orErr elab =
do state <- get
case runStateT elab state of
OK (_, state') -> lift (tfail orErr)
Error e -> return ()
-- create a fake TT term for the LHS of an impossible case
fakeTT :: Raw -> Term
fakeTT (Var n) =
case lookupNameDef n (tt_ctxt ist) of
[(n', TyDecl nt _)] -> P nt n' Erased
_ -> P Ref n Erased
fakeTT (RBind n b body) = Bind n (fmap fakeTT b) (fakeTT body)
fakeTT (RApp f a) = App Complete (fakeTT f) (fakeTT a)
fakeTT RType = TType (UVar (-1))
fakeTT (RUType u) = UType u
fakeTT (RConstant c) = Constant c
defineFunction :: RFunDefn Raw -> ElabD ()
defineFunction (RDefineFun n clauses) =
do ctxt <- get_context
ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
let info = CaseInfo True True False -- TODO document and figure out
clauses' <- forM clauses (\case
RMkFunClause lhs rhs ->
do (lhs', lty) <- lift $ check ctxt [] lhs
(rhs', rty) <- lift $ check ctxt [] rhs
lift $ converts ctxt [] lty rty
return $ Right (lhs', rhs')
RMkImpossibleClause lhs ->
do requireError (Msg "Not an impossible case") . lift $
check ctxt [] lhs
return $ Left (fakeTT lhs))
let clauses'' = map (\case Right c -> pullVars c
Left lhs -> let (ns, lhs') = patvars [] lhs
in (ns, lhs', Impossible))
clauses'
let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''
ctxt'<- lift $
addCasedef n (const [])
info False (STerm Erased)
True False -- TODO what are these?
(map snd $ getArgTys ty) [] -- TODO inaccessible types
clauses'
clauses'''
clauses'''
clauses'''
clauses'''
ty
ctxt
set_context ctxt'
updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
return ()
checkClosed :: Raw -> Elab' aux (Term, Type)
checkClosed tm = do ctxt <- get_context
(val, ty) <- lift $ check ctxt [] tm
return $! (finalise val, finalise ty)
-- | Add another argument to a Pi
mkPi :: RFunArg -> Raw -> Raw
mkPi arg rTy = RBind (argName arg) (Pi Nothing (argTy arg) (RUType AllTypes)) rTy
mustBeType ctxt tm ty =
case normaliseAll ctxt [] (finalise ty) of
UType _ -> return ()
TType _ -> return ()
ty' -> lift . tfail . InternalMsg $
show tm ++ " is not a type: it's " ++ show ty'
mustNotBeDefined ctxt n =
case lookupDefExact n ctxt of
Just _ -> lift . tfail . InternalMsg $
show n ++ " is already defined."
Nothing -> return ()
-- | Prepare a constructor to be added to a datatype being defined here
prepareConstructor :: Name -> RConstructorDefn -> ElabD (Name, [PArg], Type)
prepareConstructor tyn (RConstructor cn args resTy) =
do ctxt <- get_context
-- ensure the constructor name is not qualified, and
-- construct a qualified one
notQualified cn
let qcn = qualify cn
-- ensure that the constructor name is not defined already
mustNotBeDefined ctxt qcn
-- construct the actual type for the constructor
let cty = foldr mkPi resTy args
(checkedTy, ctyTy) <- lift $ check ctxt [] cty
mustBeType ctxt checkedTy ctyTy
-- ensure that the constructor builds the right family
case unApply (getRetTy (normaliseAll ctxt [] (finalise checkedTy))) of
(P _ n _, _) | n == tyn -> return ()
t -> lift . tfail . Msg $ "The constructor " ++ show cn ++
" doesn't construct " ++ show tyn ++
" (return type is " ++ show t ++ ")"
-- add temporary type declaration for constructor (so it can
-- occur in later constructor types)
set_context (addTyDecl qcn (DCon 0 0 False) checkedTy ctxt)
-- Save the implicits for high-level Idris
let impls = map rFunArgToPArg args
return (qcn, impls, checkedTy)
where
notQualified (NS _ _) = lift . tfail . Msg $ "Constructor names may not be qualified"
notQualified _ = return ()
qualify n = case tyn of
(NS _ ns) -> NS n ns
_ -> n
getRetTy :: Type -> Type
getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc
getRetTy ty = ty
-- | Do a step in the reflected elaborator monad. The input is the
-- step, the output is the (reflected) term returned.
runTacTm :: Term -> ElabD Term
runTacTm (unApply -> tac@(P _ n _, args))
| n == tacN "Prim__Solve", [] <- args
= do solve
returnUnit
| n == tacN "Prim__Goal", [] <- args
= do hs <- get_holes
case hs of
(h : _) -> do t <- goal
fmap fst . checkClosed $
rawPair (Var (reflm "TTName"), Var (reflm "TT"))
(reflectName h, reflect t)
[] -> lift . tfail . Msg $
"Elaboration is complete. There are no goals."
| n == tacN "Prim__Holes", [] <- args
= do hs <- get_holes
fmap fst . checkClosed $
mkList (Var $ reflm "TTName") (map reflectName hs)
| n == tacN "Prim__Guess", [] <- args
= do g <- get_guess
fmap fst . checkClosed $ reflect g
| n == tacN "Prim__LookupTy", [n] <- args
= do n' <- reifyTTName n
ctxt <- get_context
let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
TyDecl nt ty -> (nt, ty)
Operator ty _ _ -> (Ref, ty)
CaseOp _ ty _ _ _ _ -> (Ref, ty)
-- Idris tuples nest to the right
reflectTriple (x, y, z) =
raw_apply (Var pairCon) [ Var (reflm "TTName")
, raw_apply (Var pairTy) [Var (reflm "NameType"), Var (reflm "TT")]
, x
, raw_apply (Var pairCon) [ Var (reflm "NameType"), Var (reflm "TT")
, y, z]]
let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty)
| (n, def) <- lookupNameDef n' ctxt
, let (nt, ty) = getNameTypeAndType def ]
fmap fst . checkClosed $
rawList (raw_apply (Var pairTy) [ Var (reflm "TTName")
, raw_apply (Var pairTy) [ Var (reflm "NameType")
, Var (reflm "TT")]])
defs
| n == tacN "Prim__LookupDatatype", [name] <- args
= do n' <- reifyTTName name
datatypes <- get_datatypes
ctxt <- get_context
fmap fst . checkClosed $
rawList (Var (tacN "Datatype"))
(map reflectDatatype (buildDatatypes ist n'))
| n == tacN "Prim__LookupFunDefn", [name] <- args
= do n' <- reifyTTName name
fmap fst . checkClosed $
rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
(map reflectFunDefn (buildFunDefns ist n'))
| n == tacN "Prim__LookupArgs", [name] <- args
= do n' <- reifyTTName name
let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
listFunArg = RApp listTy (Var (tacN "FunArg"))
-- Idris tuples nest to the right
let reflectTriple (x, y, z) =
raw_apply (Var pairCon) [ Var (reflm "TTName")
, raw_apply (Var pairTy) [listFunArg, Var (reflm "Raw")]
, x
, raw_apply (Var pairCon) [listFunArg, Var (reflm "Raw")
, y, z]]
let out =
[ reflectTriple (reflectName fn, reflectList (Var (tacN "FunArg")) (map reflectArg args), reflectRaw res)
| (fn, pargs) <- lookupCtxtName n' (idris_implicits ist)
, (args, res) <- getArgs pargs . forget <$>
maybeToList (lookupTyExact fn (tt_ctxt ist))
]
fmap fst . checkClosed $
rawList (raw_apply (Var pairTy) [Var (reflm "TTName")
, raw_apply (Var pairTy) [ RApp listTy
(Var (tacN "FunArg"))
, Var (reflm "Raw")]])
out
| n == tacN "Prim__SourceLocation", [] <- args
= fmap fst . checkClosed $
reflectFC fc
| n == tacN "Prim__Namespace", [] <- args
= fmap fst . checkClosed $
rawList (RConstant StrType) (map (RConstant . Str) ns)
| n == tacN "Prim__Env", [] <- args
= do env <- get_env
fmap fst . checkClosed $ reflectEnv env
| n == tacN "Prim__Fail", [_a, errs] <- args
= do errs' <- eval errs
parts <- reifyReportParts errs'
lift . tfail $ ReflectionError [parts] (Msg "")
| n == tacN "Prim__PureElab", [_a, tm] <- args
= return tm
| n == tacN "Prim__BindElab", [_a, _b, first, andThen] <- args
= do first' <- eval first
res <- eval =<< runTacTm first'
next <- eval (App Complete andThen res)
runTacTm next
| n == tacN "Prim__Try", [_a, first, alt] <- args
= do first' <- eval first
alt' <- eval alt
try' (runTacTm first') (runTacTm alt') True
| n == tacN "Prim__Fill", [raw] <- args
= do raw' <- reifyRaw =<< eval raw
apply raw' []
returnUnit
| n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
, [raw, argSpec] <- args
= do raw' <- reifyRaw =<< eval raw
argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
let op = if n == tacN "Prim__Apply"
then apply
else match_apply
ns <- op raw' argSpec'
fmap fst . checkClosed $
rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TTName"))
[ rawPair (Var $ reflm "TTName", Var $ reflm "TTName")
(reflectName n1, reflectName n2)
| (n1, n2) <- ns
]
| n == tacN "Prim__Gensym", [hint] <- args
= do hintStr <- eval hint
case hintStr of
Constant (Str h) -> do
n <- getNameFrom (sMN 0 h)
fmap fst $ get_type_val (reflectName n)
_ -> fail "no hint"
| n == tacN "Prim__Claim", [n, ty] <- args
= do n' <- reifyTTName n
ty' <- reifyRaw ty
claim n' ty'
returnUnit
| n == tacN "Prim__Check", [env', raw] <- args
= do env <- reifyEnv env'
raw' <- reifyRaw =<< eval raw
ctxt <- get_context
(tm, ty) <- lift $ check ctxt env raw'
fmap fst . checkClosed $
rawPair (Var (reflm "TT"), Var (reflm "TT"))
(reflect tm, reflect ty)
| n == tacN "Prim__Attack", [] <- args
= do attack
returnUnit
| n == tacN "Prim__Rewrite", [rule] <- args
= do r <- reifyRaw rule
rewrite r
returnUnit
| n == tacN "Prim__Focus", [what] <- args
= do n' <- reifyTTName what
hs <- get_holes
if elem n' hs
then focus n' >> returnUnit
else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
| n == tacN "Prim__Unfocus", [what] <- args
= do n' <- reifyTTName what
movelast n'
returnUnit
| n == tacN "Prim__Intro", [mn] <- args
= do n <- case fromTTMaybe mn of
Nothing -> return Nothing
Just name -> fmap Just $ reifyTTName name
intro n
returnUnit
| n == tacN "Prim__Forall", [n, ty] <- args
= do n' <- reifyTTName n
ty' <- reifyRaw ty
forall n' Nothing ty'
returnUnit
| n == tacN "Prim__PatVar", [n] <- args
= do n' <- reifyTTName n
patvar' n'
returnUnit
| n == tacN "Prim__PatBind", [n] <- args
= do n' <- reifyTTName n
patbind n'
returnUnit
| n == tacN "Prim__LetBind", [n, ty, tm] <- args
= do n' <- reifyTTName n
ty' <- reifyRaw ty
tm' <- reifyRaw tm
letbind n' ty' tm'
returnUnit
| n == tacN "Prim__Compute", [] <- args
= do compute ; returnUnit
| n == tacN "Prim__Normalise", [env, tm] <- args
= do env' <- reifyEnv env
tm' <- reifyTT tm
ctxt <- get_context
let out = normaliseAll ctxt env' (finalise tm')
fmap fst . checkClosed $ reflect out
| n == tacN "Prim__Whnf", [tm] <- args
= do tm' <- reifyTT tm
ctxt <- get_context
fmap fst . checkClosed . reflect $ whnf ctxt tm'
| n == tacN "Prim__Converts", [env, tm1, tm2] <- args
= do env' <- reifyEnv env
tm1' <- reifyTT tm1
tm2' <- reifyTT tm2
ctxt <- get_context
lift $ converts ctxt env' tm1' tm2'
returnUnit
| n == tacN "Prim__DeclareType", [decl] <- args
= do (RDeclare n args res) <- reifyTyDecl decl
ctxt <- get_context
let rty = foldr mkPi res args
(checked, ty') <- lift $ check ctxt [] rty
mustBeType ctxt checked ty'
mustNotBeDefined ctxt n
let decl = TyDecl Ref checked
ctxt' = addCtxtDef n decl ctxt
set_context ctxt'
updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
new_tyDecls e }
returnUnit
| n == tacN "Prim__DefineFunction", [decl] <- args
= do defn <- reifyFunDefn decl
defineFunction defn
returnUnit
| n == tacN "Prim__DeclareDatatype", [decl] <- args
= do RDeclare n args resTy <- reifyTyDecl decl
ctxt <- get_context
let tcTy = foldr mkPi resTy args
(checked, ty') <- lift $ check ctxt [] tcTy
mustBeType ctxt checked ty'
mustNotBeDefined ctxt n
let ctxt' = addTyDecl n (TCon 0 0) checked ctxt
set_context ctxt'
updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }
returnUnit
| n == tacN "Prim__DefineDatatype", [defn] <- args
= do RDefineDatatype n ctors <- reifyRDataDefn defn
ctxt <- get_context
tyconTy <- case lookupTyExact n ctxt of
Just t -> return t
Nothing -> lift . tfail . Msg $ "Type not previously declared"
datatypes <- get_datatypes
case lookupCtxtName n datatypes of
[] -> return ()
_ -> lift . tfail . Msg $ show n ++ " is already defined as a datatype."
-- Prepare the constructors
ctors' <- mapM (prepareConstructor n) ctors
ttag <- do ES (ps, aux) str prev <- get
let i = global_nextname ps
put $ ES (ps { global_nextname = global_nextname ps + 1 },
aux)
str
prev
return i
let ctxt' = addDatatype (Data n ttag tyconTy False (map (\(cn, _, cty) -> (cn, cty)) ctors')) ctxt
set_context ctxt'
-- the rest happens in a bit
updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }
returnUnit
| n == tacN "Prim__AddInstance", [cls, inst] <- args
= do className <- reifyTTName cls
instName <- reifyTTName inst
updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
new_tyDecls e }
returnUnit
| n == tacN "Prim__IsTCName", [n] <- args
= do n' <- reifyTTName n
case lookupCtxtExact n' (idris_classes ist) of
Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
| n == tacN "Prim__ResolveTC", [fn] <- args
= do g <- goal
fn <- reifyTTName fn
resolveTC' False True 100 g fn ist
returnUnit
| n == tacN "Prim__Search", [depth, hints] <- args
= do d <- eval depth
hints' <- eval hints
case (d, unList hints') of
(Constant (I i), Just hs) ->
do actualHints <- mapM reifyTTName hs
unifyProblems
let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")
proofSearch True True False False i psElab Nothing (sMN 0 "search ") [] actualHints ist
returnUnit
(Constant (I _), Nothing ) ->
lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
(_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
| n == tacN "Prim__RecursiveElab", [goal, script] <- args
= do goal' <- reifyRaw goal
ctxt <- get_context
script <- eval script
(goalTT, goalTy) <- lift $ check ctxt [] goal'
lift $ isType ctxt [] goalTy
recH <- getNameFrom (sMN 0 "recElabHole")
aux <- getAux
datatypes <- get_datatypes
env <- get_env
g_next <- get_global_nextname
(ctxt', ES (p, aux') _ _) <-
do (ES (current_p, _) _ _) <- get
lift $ runElab aux
(do runElabAction ist fc [] script ns
ctxt' <- get_context
return ctxt')
((newProof recH ctxt datatypes g_next goalTT)
{ nextname = nextname current_p })
set_context ctxt'
let tm_out = getProofTerm (pterm p)
do (ES (prf, _) s e) <- get
let p' = prf { nextname = nextname p
, global_nextname = global_nextname p
}
put (ES (p', aux') s e)
env' <- get_env
(tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out
let (tm', ty') = (reflect tm, reflect ty)
fmap fst . checkClosed $
rawPair (Var $ reflm "TT", Var $ reflm "TT")
(tm', ty')
| n == tacN "Prim__Metavar", [n] <- args
= do n' <- reifyTTName n
ctxt <- get_context
ptm <- get_term
-- See documentation above in the elab case for PMetavar
let unique_used = getUniqueUsed ctxt ptm
let mvn = metavarName (Just ns) n'
attack
defer unique_used mvn
solve
returnUnit
| n == tacN "Prim__Fixity", [op'] <- args
= do opTm <- eval op'
case opTm of
Constant (Str op) ->
let opChars = ":!#$%&*+./<=>?@\\^|-~"
invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]
fixities = idris_infixes ist
in if not (all (flip elem opChars) op) || elem op invalidOperators
then lift . tfail . Msg $ "'" ++ op ++ "' is not a valid operator name."
else case nub [f | Fix f someOp <- fixities, someOp == op] of
[] -> lift . tfail . Msg $ "No fixity found for operator '" ++ op ++ "'."
[f] -> fmap fst . checkClosed $ reflectFixity f
many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
_ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
| n == tacN "Prim__Debug", [ty, msg] <- args
= do msg' <- eval msg
parts <- reifyReportParts msg
debugElaborator parts
runTacTm x = lift . tfail $ ElabScriptStuck x
-- Running tactics directly
-- if a tactic adds unification problems, return an error
runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()
runTac autoSolve ist perhapsFC fn tac
= do env <- get_env
g <- goal
let tac' = fmap (addImplBound ist (map fst env)) tac
if autoSolve
then runT tac'
else no_errors (runT tac')
(Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
where
runT (Intro []) = do g <- goal
attack; intro (bname g)
where
bname (Bind n _ _) = Just n
bname _ = Nothing
runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
runT Intros = do g <- goal
attack;
intro (bname g)
try' (runT Intros)
(return ()) True
where
bname (Bind n _ _) = Just n
bname _ = Nothing
runT (Exact tm) = do elab ist toplevel ERHS [] (sMN 0 "tac") tm
when autoSolve solveAll
runT (MatchRefine fn)
= do fnimps <-
case lookupCtxtName fn (idris_implicits ist) of
[] -> do a <- envArgs fn
return [(fn, a)]
ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)
let tacs = map (\ (fn', imps) ->
(match_apply (Var fn') (map (\x -> (x, 0)) imps),
fn')) fnimps
tryAll tacs
when autoSolve solveAll
where envArgs n = do e <- get_env
case lookup n e of
Just t -> return $ map (const False)
(getArgTys (binderTy t))
_ -> return []
runT (Refine fn [])
= do fnimps <-
case lookupCtxtName fn (idris_implicits ist) of
[] -> do a <- envArgs fn
return [(fn, a)]
ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)
let tacs = map (\ (fn', imps) ->
(apply (Var fn') (map (\x -> (x, 0)) imps),
fn')) fnimps
tryAll tacs
when autoSolve solveAll
where isImp (PImp _ _ _ _ _) = True
isImp _ = False
envArgs n = do e <- get_env
case lookup n e of
Just t -> return $ map (const False)
(getArgTys (binderTy t))
_ -> return []
runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)
when autoSolve solveAll
runT DoUnify = do unify_all
when autoSolve solveAll
runT (Claim n tm) = do tmHole <- getNameFrom (sMN 0 "newGoal")
claim tmHole RType
claim n (Var tmHole)
focus tmHole
elab ist toplevel ERHS [] (sMN 0 "tac") tm
focus n
runT (Equiv tm) -- let bind tm, then
= do attack
tyn <- getNameFrom (sMN 0 "ety")
claim tyn RType
valn <- getNameFrom (sMN 0 "eqval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "equiv_val")
letbind letn (Var tyn) (Var valn)
focus tyn
elab ist toplevel ERHS [] (sMN 0 "tac") tm
focus valn
when autoSolve solveAll
runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
= do attack; -- (h:_) <- get_holes
tyn <- getNameFrom (sMN 0 "rty")
-- start_unify h
claim tyn RType
valn <- getNameFrom (sMN 0 "rval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "rewrite_rule")
letbind letn (Var tyn) (Var valn)
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") tm
rewrite (Var letn)
when autoSolve solveAll
runT (Induction tm) -- let bind tm, similar to the others
= case_ True autoSolve ist fn tm
runT (CaseTac tm)
= case_ False autoSolve ist fn tm
runT (LetTac n tm)
= do attack
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
letn <- unique_hole n
letbind letn (Var tyn) (Var valn)
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") tm
when autoSolve solveAll
runT (LetTacTy n ty tm)
= do attack
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
letn <- unique_hole n
letbind letn (Var tyn) (Var valn)
focus tyn
elab ist toplevel ERHS [] (sMN 0 "tac") ty
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") tm
when autoSolve solveAll
runT Compute = compute
runT Trivial = do trivial' ist; when autoSolve solveAll
runT TCInstance = runT (Exact (PResolveTC emptyFC))
runT (ProofSearch rec prover depth top psns hints)
= do proofSearch' ist rec False depth prover top fn psns hints
when autoSolve solveAll
runT (Focus n) = focus n
runT Unfocus = do hs <- get_holes
case hs of
[] -> return ()
(h : _) -> movelast h
runT Solve = solve
runT (Try l r) = do try' (runT l) (runT r) True
runT (TSeq l r) = do runT l; runT r
runT (ApplyTactic tm) = do tenv <- get_env -- store the environment
tgoal <- goal -- store the goal
attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
script <- getNameFrom (sMN 0 "script")
claim script scriptTy
scriptvar <- getNameFrom (sMN 0 "scriptvar" )
letbind scriptvar scriptTy (Var script)
focus script
elab ist toplevel ERHS [] (sMN 0 "tac") tm
(script', _) <- get_type_val (Var scriptvar)
-- now that we have the script apply
-- it to the reflected goal and context
restac <- getNameFrom (sMN 0 "restac")
claim restac tacticTy
focus restac
fill (raw_apply (forget script')
[reflectEnv tenv, reflect tgoal])
restac' <- get_guess
solve
-- normalise the result in order to
-- reify it
ctxt <- get_context
env <- get_env
let tactic = normalise ctxt env restac'
runReflected tactic
where tacticTy = Var (reflm "Tactic")
listTy = Var (sNS (sUN "List") ["List", "Prelude"])
scriptTy = (RBind (sMN 0 "__pi_arg")
(Pi Nothing (RApp listTy envTupleType) RType)
(RBind (sMN 1 "__pi_arg")
(Pi Nothing (Var $ reflm "TT") RType) tacticTy))
runT (ByReflection tm) -- run the reflection function 'tm' on the
-- goal, then apply the resulting reflected Tactic
= do tgoal <- goal
attack
script <- getNameFrom (sMN 0 "script")
claim script scriptTy
scriptvar <- getNameFrom (sMN 0 "scriptvar" )
letbind scriptvar scriptTy (Var script)
focus script
ptm <- get_term
elab ist toplevel ERHS [] (sMN 0 "tac")
(PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
(script', _) <- get_type_val (Var scriptvar)
-- now that we have the script apply
-- it to the reflected goal
restac <- getNameFrom (sMN 0 "restac")
claim restac tacticTy
focus restac
fill (forget script')
restac' <- get_guess
solve
-- normalise the result in order to
-- reify it
ctxt <- get_context
env <- get_env
let tactic = normalise ctxt env restac'
runReflected tactic
where tacticTy = Var (reflm "Tactic")
scriptTy = tacticTy
runT (Reflect v) = do attack -- let x = reflect v in ...
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "letvar")
letbind letn (Var tyn) (Var valn)
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") v
(value, _) <- get_type_val (Var letn)
ctxt <- get_context
env <- get_env
let value' = hnf ctxt env value
runTac autoSolve ist perhapsFC fn (Exact $ PQuote (reflect value'))
runT (Fill v) = do attack -- let x = fill x in ...
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "letvar")
letbind letn (Var tyn) (Var valn)
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") v
(value, _) <- get_type_val (Var letn)
ctxt <- get_context
env <- get_env
let value' = normalise ctxt env value
rawValue <- reifyRaw value'
runTac autoSolve ist perhapsFC fn (Exact $ PQuote rawValue)
runT (GoalType n tac) = do g <- goal
case unApply g of
(P _ n' _, _) ->
if nsroot n' == sUN n
then runT tac
else fail "Wrong goal type"
_ -> fail "Wrong goal type"
runT ProofState = do g <- goal
return ()
runT Skip = return ()
runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "")
runT SourceFC =
case perhapsFC of
Nothing -> lift . tfail $ Msg "There is no source location available."
Just fc ->
do fill $ reflectFC fc
solve
runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"
runT x = fail $ "Not implemented " ++ show x
runReflected t = do t' <- reify ist t
runTac autoSolve ist perhapsFC fn t'
elaboratingArgErr :: [(Name, Name)] -> Err -> Err
elaboratingArgErr [] err = err
elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
where rewrite (ElaboratingArg _ _ _ _) = Nothing
rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e)
rewrite (At fc e) = fmap (At fc) (rewrite e)
rewrite err = Just (ElaboratingArg f x during err)
withErrorReflection :: Idris a -> Idris a
withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
where handle :: Err -> Idris Err
handle e@(ReflectionError _ _) = do logElab 3 "Skipping reflection of error reflection result"
return e -- Don't do meta-reflection of errors
handle e@(ReflectionFailed _ _) = do logElab 3 "Skipping reflection of reflection failure"
return e
-- At and Elaborating are just plumbing - error reflection shouldn't rewrite them
handle e@(At fc err) = do logElab 3 "Reflecting body of At"
err' <- handle err
return (At fc err')
handle e@(Elaborating what n ty err) = do logElab 3 "Reflecting body of Elaborating"
err' <- handle err
return (Elaborating what n ty err')
handle e@(ElaboratingArg f a prev err) = do logElab 3 "Reflecting body of ElaboratingArg"
hs <- getFnHandlers f a
err' <- if null hs
then handle err
else applyHandlers err hs
return (ElaboratingArg f a prev err')
-- ProofSearchFail is an internal detail - so don't expose it
handle (ProofSearchFail e) = handle e
-- TODO: argument-specific error handlers go here for ElaboratingArg
handle e = do ist <- getIState
logElab 2 "Starting error reflection"
logElab 5 (show e)
let handlers = idris_errorhandlers ist
applyHandlers e handlers
getFnHandlers :: Name -> Name -> Idris [Name]
getFnHandlers f arg = do ist <- getIState
let funHandlers = maybe M.empty id .
lookupCtxtExact f .
idris_function_errorhandlers $ ist
return . maybe [] S.toList . M.lookup arg $ funHandlers
applyHandlers e handlers =
do ist <- getIState
let err = fmap (errReverse ist) e
logElab 3 $ "Using reflection handlers " ++
concat (intersperse ", " (map show handlers))
let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
-- Typecheck error handlers - if this fails, then something else was wrong earlier!
handlers <- case mapM (check (tt_ctxt ist) []) reports of
Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
OK hs -> return hs
-- Normalize error handler terms to produce the new messages
-- Need to use 'normaliseAll' since we have to reduce private
-- names in error handlers too
ctxt <- getContext
let results = map (normaliseAll ctxt []) (map fst handlers)
logElab 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
-- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
Left err -> ierror err
Right ok -> return ok
return $ case errorparts of
[] -> e
parts -> ReflectionError errorparts e
solveAll = try (do solve; solveAll) (return ())
-- | Do the left-over work after creating declarations in reflected
-- elaborator scripts
processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls info steps =
-- The order of steps is important: type declarations might
-- establish metavars that later function bodies resolve.
forM_ (reverse steps) $ \case
RTyDeclInstrs n fc impls ty ->
do logElab 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
logElab 3 $ " It has impls " ++ show impls
updateIState $ \i -> i { idris_implicits =
addDef n impls (idris_implicits i) }
addIBC (IBCImp n)
ds <- checkDef fc (\_ e -> e) True [(n, (-1, Nothing, ty, []))]
addIBC (IBCDef n)
ctxt <- getContext
case lookupDef n ctxt of
(TyDecl _ _ : _) ->
-- If the function isn't defined at the end of the elab script,
-- then it must be added as a metavariable. This needs guarding
-- to prevent overwriting case defs with a metavar, if the case
-- defs come after the type decl in the same script!
let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) ds
in addDeferred ds'
_ -> return ()
RDatatypeDeclInstrs n impls ->
do addIBC (IBCDef n)
updateIState $ \i -> i { idris_implicits = addDef n impls (idris_implicits i) }
addIBC (IBCImp n)
RDatatypeDefnInstrs tyn tyconTy ctors ->
do let cn (n, _, _) = n
cimpls (_, impls, _) = impls
cty (_, _, t) = t
addIBC (IBCDef tyn)
mapM_ (addIBC . IBCDef . cn) ctors
let params = findParams tyn (map cty ctors)
let typeInfo = TI (map cn ctors) False [] params []
-- implicit precondition to IBCData is that idris_datatypes on the IState is populated.
-- otherwise writing the IBC just fails silently!
updateIState $ \i -> i { idris_datatypes =
addDef tyn typeInfo (idris_datatypes i) }
addIBC (IBCData tyn)
ttag <- getName -- from AbsSyntax.hs, really returns a disambiguating Int
let metainf = DataMI params
addIBC (IBCMetaInformation tyn metainf)
updateContext (setMetaInformation tyn metainf)
for_ ctors $ \(cn, impls, _) ->
do updateIState $ \i -> i { idris_implicits = addDef cn impls (idris_implicits i) }
addIBC (IBCImp cn)
for_ ctors $ \(ctorN, _, _) ->
do totcheck (NoFC, ctorN)
ctxt <- tt_ctxt <$> getIState
case lookupTyExact ctorN ctxt of
Just cty -> do checkPositive (tyn : map cn ctors) (ctorN, cty)
return ()
Nothing -> return ()
case ctors of
[ctor] -> do setDetaggable (cn ctor); setDetaggable tyn
addIBC (IBCOpt (cn ctor)); addIBC (IBCOpt tyn)
_ -> return ()
-- TODO: inaccessible
RAddInstance className instName ->
do -- The type class resolution machinery relies on a special
logElab 2 $ "Adding elab script instance " ++ show instName ++
" for " ++ show className
addInstance False True className instName
addIBC (IBCInstance False True className instName)
RClausesInstrs n cs ->
do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n
solveDeferred emptyFC n
let lhss = map (\(_, lhs, _) -> lhs) cs
let fc = fileFC "elab_reflected"
pmissing <-
do ist <- getIState
possible <- genClauses fc n lhss
(map (\lhs ->
delab' ist lhs True True) lhss)
missing <- filterM (checkPossible n) possible
return (filter (noMatch ist lhss) missing)
let tot = if null pmissing
then Unchecked -- still need to check recursive calls
else Partial NotCovering -- missing cases implies not total
setTotality n tot
updateIState $ \i -> i { idris_patdefs =
addDef n (cs, pmissing) $ idris_patdefs i }
addIBC (IBCDef n)
ctxt <- getContext
case lookupDefExact n ctxt of
Just (CaseOp _ _ _ _ _ cd) ->
-- Here, we populate the call graph with a list of things
-- we refer to, so that if they aren't total, the whole
-- thing won't be.
let (scargs, sc) = cases_compiletime cd
calls = map fst $ findCalls sc scargs
in do logElab 2 $ "Called names in reflected elab: " ++ show calls
addCalls n calls
addIBC $ IBCCG n
Just _ -> return () -- TODO throw internal error
Nothing -> return ()
-- checkDeclTotality requires that the call graph be present
-- before calling it.
-- TODO: reduce code duplication with Idris.Elab.Clause
buildSCG (fc, n)
-- Actually run the totality checker. In the main clause
-- elaborator, this is deferred until after. Here, we run it
-- now to get totality information as early as possible.
tot' <- checkDeclTotality (fc, n)
setTotality n tot'
when (tot' /= Unchecked) $ addIBC (IBCTotal n tot')
where
-- TODO: see if the code duplication with Idris.Elab.Clause can be
-- reduced or eliminated.
checkPossible :: Name -> PTerm -> Idris Bool
checkPossible fname lhs_in =
do ctxt <- getContext
ist <- getIState
let lhs = addImplPat ist lhs_in
let fc = fileFC "elab_reflected_totality"
let tcgen = False -- TODO: later we may support dictionary generation
case elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState
(erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)
(infTerm lhs))) of
OK (ElabResult lhs' _ _ _ _ _ name', _) ->
do -- not recursively calling here, because we don't
-- want to run infinitely many times
let lhs_tm = orderPats (getInferTerm lhs')
updateIState $ \i -> i { idris_name = name' }
case recheck ctxt [] (forget lhs_tm) lhs_tm of
OK _ -> return True
err -> return False
-- if it's a recoverable error, the case may become possible
Error err -> if tcgen then return (recoverableCoverage ctxt err)
else return (validCoverageCase ctxt err ||
recoverableCoverage ctxt err)
-- TODO: Attempt to reduce/eliminate code duplication with Idris.Elab.Clause
noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
Right _ -> False
Left _ -> True) cs