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.Elab.Rewrite
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
, resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]
, resultCaseDecls :: [PDecl]
, resultContext :: Context
, resultTyDecls :: [RDeclInstructions]
, resultHighlighting :: [(FC, OutputAnnotation)]
, resultName :: Int
}
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
when (not pattern) $
mapM_ (\n -> when (n `elem` hs) $
do focus n
g <- goal
try (resolveTC' True True 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 ()
buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->
[Name] ->
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
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
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
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,
e_guarded :: Bool,
e_intype :: Bool,
e_qq :: Bool,
e_nomatching :: Bool
}
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
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
let fc = maybe "(unknown)"
elabE initElabCtxt (elabFC info) tm
est <- getAux
sequence_ (get_delayed_elab est)
end_unify
ptm <- get_term
when (pattern || intransform)
(do unify_all
matchProblems False
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 ()
elabRec = elabE initElabCtxt Nothing
elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
elabE ina fc' t =
do solved <- get_recents
as <- get_autos
hs <- get_holes
mapM_ (\(a, (failc, ns)) ->
if any (\n -> n `elem` solved) ns && head hs /= a
then solveAuto ist fn False (a, failc)
else return ()) as
apt <- expandToArity t
itm <- if not pattern then insertImpLam ina apt else return apt
ct <- insertCoerce ina itm
t' <- insertLazy ina ct
g <- goal
tm <- get_term
ps <- get_probs
hs <- get_holes
env <- get_env
let fc = fileFC "Force"
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 "Delayed" = notDelay orig
forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
| (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
ht == txt "Delayed" = notDelay orig
forceErr orig env (InfiniteUnify _ t _)
| (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
ht == txt "Delayed" = 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)
constType :: Const -> Bool
constType (AType _) = True
constType StrType = True
constType VoidType = True
constType _ = False
elab' :: ElabCtxt
-> Maybe FC
-> PTerm
-> ElabD ()
elab' ina fc (PNoImplicits t) = elab' ina fc t
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' 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" _ _))
= do g <- goal; resolveTC False False 5 g fn elabRec ist
elab' ina fc (PResolveTC fc')
= do c <- getNameFrom (sMN 0 "__class")
instanceArg c
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 p of
IsType -> asType
IsTerm -> asValue
TypeOrTerm ->
do hnf_compute
g <- goal
case g of
TType _ -> asType
_ -> asValue
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
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
_ -> 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 "_")
doPrune as =
do compute
ty <- goal
let (tc, _) = unApply (unDelay ty)
env <- get_env
return $ pruneByType env tc (unDelay ty) ist as
unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
l == txt "Delayed" = 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
uns <- get_usedns
let as = map (mkUniqueNames (uns ++ map snd ms) ms) as_in
trySeq as
where
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 [] = do deferr; unifyProblems
trySeq' deferr (x : xs)
= try' (tryCatch (do elab' ina fc x
solveAutos ist fn False
unifyProblems)
(\_ -> trySeq' deferr []))
(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
case pruneAlts err alts env of
[] -> lift $ tfail err
alts' -> do
try' (elab' ina fc (PAlternative ms (ExactlyOne False) alts'))
(lift $ tfail err)
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
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
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' 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
if (tcname n && ina && not intransform)
then erun fc $
do patvar n
update_term liftPats
highlightSource fc (AnnBoundName n False)
else if defined
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)
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
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
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")
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
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
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'
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 elabRec ist)
(movelast n)
else movelast n)
(ivs' \\ ivs)
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 _ tm@(PApp fc (PInferRef _ _ f) args) = do
rty <- goal
ds <- get_deferred
ctxt <- get_context
env <- get_env
argTys <- claimArgTys env args
fn <- getNameFrom (sMN 0 "inf_fn")
let fty = fnTy argTys rty
attack; deferType (mkN f) fty (map fst argTys); solve
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 ()
mkN n@(NS _ _) = n
mkN n@(SN _) = n
mkN n = case namespace info of
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
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
let dataCon = isDConName f ctxt
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 []
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)
if (f `elem` map fst env && length args == 1 && length args_in == 1)
then
do simple_app False
(elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))
(elabE (ina { e_inarg = True,
e_guarded = dataCon }) (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
let isinf = f == inferCon || tcname f
case lookupCtxt f (idris_classes ist) of
[] -> return ()
_ -> do mapM_ setInjective (map getTm args)
unifyProblems
let guarded = isConName f ctxt
ns <- apply (Var f) (map isph args)
mapM_ checkIfInjective (map snd ns)
unifyProblems
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,
e_guarded = dataCon })
[] fc False f
(zip ns (unmatchableArgs ++ repeat False))
(f == sUN "Force")
(map (\x -> getTm x) args)
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 []
case imp of
rs@(_:_) | not pattern -> return rs
_ -> do solve
hs <- get_holes
ivs' <- get_instances
when (not pattern || (e_inarg ina && not tcgen)) $
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 elabRec ist)
(movelast n)
else movelast n)
(ivs' \\ ivs)
return []
where
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 ->
do mapM_ setinjArg (getDets 0 (class_determiners ci) args)
ulog <- getUnifyLog
probs <- get_probs
inj <- get_inj
traceWhen ulog ("Injective now " ++ show args ++ "\nAll: " ++ show inj
++ "\nProblems: " ++ 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)
solve
where appImpl [] = elab' (ina { e_isfn = False }) fc f
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
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 mfc (PRewrite fc substfn rule sc newg)
= elabRewrite (elab' ina mfc) ist fc substfn rule sc newg
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)
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
unifyProblems
matchProblems True
args <- get_env
envU <- mapM (getKind args) args
let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
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
let newdef = PClauses fc [] cname'
(caseBlock fc cname' scr
(map (isScr scr) (reverse args')) opts)
updateAux (\e -> e { case_decls = (cname', newdef) : case_decls e } )
movelast tyn
solve
where mkCaseName fc (NS n ns) = NS (mkCaseName fc n) ns
mkCaseName fc n = SN (CaseN (FC' fc) n)
mkN n@(NS _ _) = n
mkN n = case namespace info of
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
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)
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
finalTy <- goal
(t, unq) <- extractUnquotes 0 t
let unquoteNames = map fst unq
mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames
ctxt <- get_context
datatypes <- get_datatypes
g_nextname <- get_global_nextname
saveState
updatePS (const .
newProof (sMN 0 "q") (constraintNS info) ctxt datatypes g_nextname $
P Ref (reflm "TT") Erased)
mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
claim ty RType
movelast ty
claim n (Var ty)
movelast n)
unquoteNames
qTy <- getNameFrom (sMN 0 "qquoteTy")
claim qTy RType
movelast qTy
qTm <- getNameFrom (sMN 0 "qquoteTm")
claim qTm (Var qTy)
nTm <- getNameFrom (sMN 0 "quotedTerm")
letbind nTm (Var qTy) (Var qTm)
case goalt of
Nothing -> return ()
Just gTy -> do focus qTy
elabE (ina { e_qq = True }) fc gTy
focus qTm
elabE (ina { e_qq = True }) fc t
end_unify
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 (constraintNS info) 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
fill $ reflectRawQuote unquoteNames (forget q')
else fill $ reflectTTQuote unquoteNames q'
solve
Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
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
movelast h
delayElab 10 $ do hs <- get_holes
when (h `elem` hs) $ 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
elab' ina (Just fc') tm
script <- get_guess
fullyElaborated script
solve
env <- get_env
runElabAction info ist (maybe fc' id fc) env script ns
solve
elab' ina fc (PConstSugar constFC tm) =
do saveState
n <- getNameFrom (sMN 0 "cstI")
n' <- getNameFrom (sMN 0 "cstIhole")
g <- forget <$> goal
claim n' g
movelast n'
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
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
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
-> [(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
findScr ((n, (True, t)) : xs)
= (n, (True, t)) : scrName n xs
findScr [(n, (_, t))] = [(n, (True, t))]
findScr (x : xs) = x : findScr xs
findScr [] = error "The impossible happened - the scrutinee was not in 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)
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 []
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
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 :: ElabCtxt -> PTerm -> ElabD PTerm
insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t
insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t
insertLazy ina (PCoerced t) = return t
insertLazy ina t@(PPatvar _ _) | pattern && not (e_guarded ina) = return t
insertLazy ina t =
do ty <- goal
env <- get_env
let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
let tries = [mkDelay env t, t]
case tyh of
P _ (UN l) _ | l == txt "Delayed"
-> 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])
notImplicitable (PApp _ f _) = notImplicitable f
notImplicitable (PRef _ _ n)
| [opts] <- lookupCtxt n (idris_flags ist)
= NoImplicit `elem` opts
notImplicitable (PAlternative _ _ as) = any notImplicitable as
notImplicitable (PCase _ _ _) = True
notImplicitable _ = False
expandToArity tm@(PApp fc f a) = do
env <- get_env
case fullApp tm of
PApp fc ftm@(PRef _ _ f) args | Just aty <- lookup f env ->
do let a = length (getArgTys (normalise (tt_ctxt ist) env (binderTy aty)))
return (mkPApp fc a ftm args)
_ -> return tm
expandToArity t = return t
fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
fullApp x = x
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
addLam (Bind n (Pi (Just _) _ _) sc) t =
do impn <- unique_hole n
if e_isfn ina
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
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)])
elabArgs :: IState
-> ElabCtxt
-> [Bool]
-> FC
-> Bool
-> Name
-> [((Name, Name), Bool)]
-> Bool
-> [PTerm]
-> 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
now_elaborating fc f argName
wrapErr f argName $ do
hs <- get_holes
tm <- get_term
let elab = if force then elab' else elabE
failed' <-
do focus holeName;
g <- goal
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
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
pruneByType :: Env -> Term ->
Type ->
IState -> [PTerm] -> [PTerm]
pruneByType env t goalty 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])
| l == txt "Delay" = getName (getTm arg)
getName (PApp _ f _) = getName f
getName (PHidden t) = getName t
getName _ = Nothing
pruneByType env (P _ n _) goalty ist as
| Nothing <- lookupTyExact n ctxt = as
| 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
typeHead var f f'
=
case lookupTyExact f' ctxt of
Just ty -> case unApply (getRetTy ty) of
(P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)
-> False
_ -> let ty' = normalise ctxt [] ty in
case unApply (getRetTy ty') of
(V _, _) ->
isPlausible ist var env n ty
_ -> matching (getRetTy ty') goalty
|| isCoercion (getRetTy ty') goalty
_ -> False
matching (P _ ctyn _) (P _ n' _)
| isTConName n' ctxt = ctyn == n'
| otherwise = True
matching (V _) _ = True
matching _ (V _) = True
matching _ (P _ n _) = not (isTConName n ctxt)
matching (P _ n _) _ = not (isTConName n ctxt)
matching (Bind n _ sc) _ = True
matching _ (Bind n _ sc) = True
matching (App _ (P _ f _) _) _ | not (isConName f ctxt) = True
matching _ (App _ (P _ f _) _) | not (isConName f ctxt) = True
matching (App _ f a) (App _ f' a') = matching f f' && matching a a'
matching (TType _) (TType _) = True
matching (UType _) (UType _) = True
matching l r = l == r
isCoercion rty gty | (P _ r _, _) <- unApply rty
= not (null (getCoercionsBetween r gty))
isCoercion _ _ = False
getCoercionsBetween :: Name -> Type -> [Name]
getCoercionsBetween r goal
= let cs = getCoercionsTo ist goal in
findCoercions r cs
where findCoercions t [] = []
findCoercions t (n : ns) =
let ps = case lookupTy n (tt_ctxt ist) of
[ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in
[n | any useR as]
_ -> [] in
ps ++ findCoercions t ns
useR ty =
case unApply (getRetTy ty) of
(P _ t _, _) -> t == r
_ -> False
pruneByType _ t _ _ as = as
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
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)
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
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
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)
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
metavarName :: [String] -> Name -> Name
metavarName _ n@(NS _ _) = n
metavarName (ns@(_:_)) n = sNS n ns
metavarName _ n = n
runElabAction :: ElabInfo -> IState -> FC -> Env -> Term -> [String] -> ElabD Term
runElabAction info 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))
requireError :: Err -> ElabD a -> ElabD ()
requireError orErr elab =
do state <- get
case runStateT elab state of
OK (_, state') -> lift (tfail orErr)
Error e -> return ()
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
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''
let argtys = map (\x -> (x, isCanonical x ctxt))
(map snd (getArgTys (normalise ctxt [] ty)))
ctxt'<- lift $
addCasedef n (const [])
info False (STerm Erased)
True False
argtys []
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)
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 ()
prepareConstructor :: Name -> RConstructorDefn -> ElabD (Name, [PArg], Type)
prepareConstructor tyn (RConstructor cn args resTy) =
do ctxt <- get_context
notQualified cn
let qcn = qualify cn
mustNotBeDefined ctxt qcn
let cty = foldr mkPi resTy args
(checkedTy, ctyTy) <- lift $ check ctxt [] cty
mustBeType ctxt checkedTy ctyTy
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 ++ ")"
set_context (addTyDecl qcn (DCon 0 0 False) checkedTy ctxt)
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
elabScriptStuck :: Term -> ElabD a
elabScriptStuck x = lift . tfail $ ElabScriptStuck x
tacTmArgs :: Int -> Term -> [Term] -> ElabD [Term]
tacTmArgs l t args | length args == l = return args
| otherwise = elabScriptStuck t
runTacTm :: Term -> ElabD Term
runTacTm tac@(unApply -> (P _ n _, args))
| n == tacN "Prim__Solve"
= do ~[] <- tacTmArgs 0 tac args
solve
returnUnit
| n == tacN "Prim__Goal"
= do ~[] <- tacTmArgs 0 tac args
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"
= do ~[] <- tacTmArgs 0 tac args
hs <- get_holes
fmap fst . checkClosed $
mkList (Var $ reflm "TTName") (map reflectName hs)
| n == tacN "Prim__Guess"
= do ~[] <- tacTmArgs 0 tac args
g <- get_guess
fmap fst . checkClosed $ reflect g
| n == tacN "Prim__LookupTy"
= do ~[name] <- tacTmArgs 1 tac args
n' <- reifyTTName name
ctxt <- get_context
let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
TyDecl nt ty -> (nt, ty)
Operator ty _ _ -> (Ref, ty)
CaseOp _ ty _ _ _ _ -> (Ref, ty)
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"
= do ~[name] <- tacTmArgs 1 tac args
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"
= do ~[name] <- tacTmArgs 1 tac args
n' <- reifyTTName name
fmap fst . checkClosed $
rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
(map reflectFunDefn (buildFunDefns ist n'))
| n == tacN "Prim__LookupArgs"
= do ~[name] <- tacTmArgs 1 tac args
n' <- reifyTTName name
let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
listFunArg = RApp listTy (Var (tacN "FunArg"))
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"
= do ~[] <- tacTmArgs 0 tac args
fmap fst . checkClosed $
reflectFC fc
| n == tacN "Prim__Namespace"
= do ~[] <- tacTmArgs 0 tac args
fmap fst . checkClosed $
rawList (RConstant StrType) (map (RConstant . Str) ns)
| n == tacN "Prim__Env"
= do ~[] <- tacTmArgs 0 tac args
env <- get_env
fmap fst . checkClosed $ reflectEnv env
| n == tacN "Prim__Fail"
= do ~[_a, errs] <- tacTmArgs 2 tac args
errs' <- eval errs
parts <- reifyReportParts errs'
lift . tfail $ ReflectionError [parts] (Msg "")
| n == tacN "Prim__PureElab"
= do ~[_a, tm] <- tacTmArgs 2 tac args
return tm
| n == tacN "Prim__BindElab"
= do ~[_a, _b, first, andThen] <- tacTmArgs 4 tac args
first' <- eval first
res <- eval =<< runTacTm first'
next <- eval (App Complete andThen res)
runTacTm next
| n == tacN "Prim__Try"
= do ~[_a, first, alt] <- tacTmArgs 3 tac args
first' <- eval first
alt' <- eval alt
try' (runTacTm first') (runTacTm alt') True
| n == tacN "Prim__Fill"
= do ~[raw] <- tacTmArgs 1 tac args
raw' <- reifyRaw =<< eval raw
apply raw' []
returnUnit
| n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
= do ~[raw, argSpec] <- tacTmArgs 2 tac args
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"
= do ~[hint] <- tacTmArgs 1 tac args
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"
= do ~[n, ty] <- tacTmArgs 2 tac args
n' <- reifyTTName n
ty' <- reifyRaw ty
claim n' ty'
returnUnit
| n == tacN "Prim__Check"
= do ~[env', raw] <- tacTmArgs 2 tac args
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"
= do ~[] <- tacTmArgs 0 tac args
attack
returnUnit
| n == tacN "Prim__Rewrite"
= do ~[rule] <- tacTmArgs 1 tac args
r <- reifyRaw rule
rewrite r
returnUnit
| n == tacN "Prim__Focus"
= do ~[what] <- tacTmArgs 1 tac args
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"
= do ~[what] <- tacTmArgs 1 tac args
n' <- reifyTTName what
movelast n'
returnUnit
| n == tacN "Prim__Intro"
= do ~[mn] <- tacTmArgs 1 tac args
n <- case fromTTMaybe mn of
Nothing -> return Nothing
Just name -> fmap Just $ reifyTTName name
intro n
returnUnit
| n == tacN "Prim__Forall"
= do ~[n, ty] <- tacTmArgs 2 tac args
n' <- reifyTTName n
ty' <- reifyRaw ty
forall n' Nothing ty'
returnUnit
| n == tacN "Prim__PatVar"
= do ~[n] <- tacTmArgs 1 tac args
n' <- reifyTTName n
patvar' n'
returnUnit
| n == tacN "Prim__PatBind"
= do ~[n] <- tacTmArgs 1 tac args
n' <- reifyTTName n
patbind n'
returnUnit
| n == tacN "Prim__LetBind"
= do ~[n, ty, tm] <- tacTmArgs 3 tac args
n' <- reifyTTName n
ty' <- reifyRaw ty
tm' <- reifyRaw tm
letbind n' ty' tm'
returnUnit
| n == tacN "Prim__Compute"
= do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit
| n == tacN "Prim__Normalise"
= do ~[env, tm] <- tacTmArgs 2 tac args
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"
= do ~[tm] <- tacTmArgs 1 tac args
tm' <- reifyTT tm
ctxt <- get_context
fmap fst . checkClosed . reflect $ whnf ctxt tm'
| n == tacN "Prim__Converts"
= do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
env' <- reifyEnv env
tm1' <- reifyTT tm1
tm2' <- reifyTT tm2
ctxt <- get_context
lift $ converts ctxt env' tm1' tm2'
returnUnit
| n == tacN "Prim__DeclareType"
= do ~[decl] <- tacTmArgs 1 tac args
(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"
= do ~[decl] <- tacTmArgs 1 tac args
defn <- reifyFunDefn decl
defineFunction defn
returnUnit
| n == tacN "Prim__DeclareDatatype"
= do ~[decl] <- tacTmArgs 1 tac args
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"
= do ~[defn] <- tacTmArgs 1 tac args
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."
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'
updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }
returnUnit
| n == tacN "Prim__AddInstance"
= do ~[cls, inst] <- tacTmArgs 2 tac args
className <- reifyTTName cls
instName <- reifyTTName inst
updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
new_tyDecls e }
returnUnit
| n == tacN "Prim__IsTCName"
= do ~[n] <- tacTmArgs 1 tac args
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"
= do ~[fn] <- tacTmArgs 1 tac args
g <- goal
fn <- reifyTTName fn
resolveTC' False True 100 g fn ist
returnUnit
| n == tacN "Prim__Search"
= do ~[depth, hints] <- tacTmArgs 2 tac args
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"
= do ~[goal, script] <- tacTmArgs 2 tac args
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 info ist fc [] script ns
ctxt' <- get_context
return ctxt')
((newProof recH (constraintNS info) 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 (constraintNS info) 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"
= do ~[n] <- tacTmArgs 1 tac args
n' <- reifyTTName n
ctxt <- get_context
ptm <- get_term
let unique_used = getUniqueUsed ctxt ptm
let mvn = metavarName ns n'
attack
defer unique_used mvn
solve
returnUnit
| n == tacN "Prim__Fixity"
= do ~[op'] <- tacTmArgs 1 tac args
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"
= do ~[ty, msg] <- tacTmArgs 2 tac args
msg' <- eval msg
parts <- reifyReportParts msg
debugElaborator parts
runTacTm x = elabScriptStuck x
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)
= 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)
= 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 ist toplevel ERHS [] (sMN 0 "tac") tm
rewrite (Var letn)
when autoSolve solveAll
runT (Induction tm)
= 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
tgoal <- goal
attack
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)
restac <- getNameFrom (sMN 0 "restac")
claim restac tacticTy
focus restac
fill (raw_apply (forget script')
[reflectEnv tenv, reflect tgoal])
restac' <- get_guess
solve
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)
= 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 True)])
(script', _) <- get_type_val (Var scriptvar)
restac <- getNameFrom (sMN 0 "restac")
claim restac tacticTy
focus restac
fill (forget script')
restac' <- get_guess
solve
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
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
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
handle e@(ReflectionFailed _ _) = do logElab 3 "Skipping reflection of reflection failure"
return e
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')
handle (ProofSearchFail e) = handle e
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
handlers <- case mapM (check (tt_ctxt ist) []) reports of
Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
OK hs -> return hs
ctxt <- getContext
let results = map (normaliseAll ctxt []) (map fst handlers)
logElab 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
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 ())
processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls info steps =
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 info fc (\_ e -> e) True [(n, (1, Nothing, ty, []))]
addIBC (IBCDef n)
ctxt <- getContext
case lookupDef n ctxt of
(TyDecl _ _ : _) ->
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
ctxt <- getContext
let params = findParams tyn (normalise ctxt [] tyconTy) (map cty ctors)
let typeInfo = TI (map cn ctors) False [] params []
updateIState $ \i -> i { idris_datatypes =
addDef tyn typeInfo (idris_datatypes i) }
addIBC (IBCData tyn)
ttag <- getName
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 ()
RAddInstance className instName ->
do
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
else Partial NotCovering
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) ->
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 ()
Nothing -> return ()
buildSCG (fc, n)
tot' <- checkDeclTotality (fc, n)
setTotality n tot'
when (tot' /= Unchecked) $ addIBC (IBCTotal n tot')
where
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
case elaborate (constraintNS info) 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
let lhs_tm = orderPats (getInferTerm lhs')
updateIState $ \i -> i { idris_name = name' }
case recheck (constraintNS info) ctxt [] (forget lhs_tm) lhs_tm of
OK _ -> return True
err -> return False
Error err -> if tcgen then return (recoverableCoverage ctxt err)
else return (validCoverageCase ctxt err ||
recoverableCoverage ctxt err)
noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
Right _ -> False
Left _ -> True) cs