module Idris.Elab.Clause where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.WHNF
import Idris.Coverage
import Idris.DataOpts
import Idris.DeepSeq ()
import Idris.Delaborate
import Idris.Docstrings hiding (Unchecked)
import Idris.Elab.AsPat
import Idris.Elab.Term
import Idris.Elab.Transform
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Error
import Idris.Options
import Idris.Output (iWarn, pshow, sendHighlighting)
import Idris.PartialEval
import Idris.Termination
import Idris.Transforms
import Util.Pretty hiding ((<$>))
import Prelude hiding (id, (.))
import Control.Category
import Control.DeepSeq
import Control.Monad
import qualified Control.Monad.State.Lazy as LState
import Control.Monad.State.Strict as State
import Data.List
import Data.Maybe
import Data.Word
import Debug.Trace
import Numeric
elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
elabClauses info' fc opts n_in cs =
do let n = liftname info n_in
info = info' { elabFC = Just fc }
ctxt <- getContext
ist <- getIState
optimise <- getOptimise
let petrans = PETransform `elem` optimise
inacc <- map fst <$> fgetState (opt_inaccessible . ist_optimisation n)
let tys = lookupTy n ctxt
let reflect = Reflection `elem` opts
when (reflect && FCReflection `notElem` idris_language_extensions ist) $
ierror $ At fc (Msg "You must turn on the FirstClassReflection extension to use %reflection")
checkUndefined n ctxt
unless (length tys > 1) $ do
fty <- case tys of
[] ->
tclift $ tfail $ At fc (NoTypeDecl n)
[ty] -> return ty
let atys_in = map snd (getArgTys (normalise ctxt [] fty))
let atys = map (\x -> (x, isCanonical x ctxt)) atys_in
cs_elab <- mapM (elabClause info opts)
(zip [0..] cs)
ctxt <- getContext
let optinfo = idris_optimisation ist
let (pats_in, cs_full) = unzip cs_elab
let pats_raw = map (simple_lhs ctxt) pats_in
let pats_forced = map (force_lhs optinfo) pats_raw
logElab 3 $ "Elaborated patterns:\n" ++ show pats_raw
logElab 5 $ "Forced patterns:\n" ++ show pats_forced
solveDeferred fc n
fmodifyState (ist_optimisation n) id
addIBC (IBCOpt n)
ist <- getIState
ctxt <- getContext
let tpats = case specNames opts of
Nothing -> transformPats ist pats_in
_ -> pats_in
pe_tm <- doPartialEval ist tpats
let pats_pe = if petrans
then map (force_lhs optinfo . simple_lhs ctxt) pe_tm
else pats_forced
let tcase = opt_typecase (idris_options ist)
newrules <- if petrans
then mapM (\ e -> case e of
Left _ -> return []
Right (l, r) -> elabPE info fc n r) pats_pe
else return []
ist <- getIState
let pats_transformed = if petrans
then transformPats ist pats_pe
else pats_pe
let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $
map debind pats_forced
let pdef_pe = map debind pats_transformed
logElab 5 $ "Initial typechecked patterns:\n" ++ show pats_raw
logElab 5 $ "Initial typechecked pattern def:\n" ++ show pdef
ist <- getIState
numArgs <- tclift $ sameLength pdef
case specNames opts of
Just _ ->
do logElab 3 $ "Partially evaluated:\n" ++ show pats_pe
_ -> return ()
logElab 3 $ "Transformed:\n" ++ show pats_transformed
erInfo <- getErasureInfo <$> getIState
tree@(CaseDef scargs sc _) <- tclift $
simpleCase tcase (UnmatchedCase "Error") reflect CompileTime fc inacc atys pdef erInfo
cov <- coverage
pmissing <-
if cov && not (hasDefault pats_raw)
then do
missing <- genClauses fc n
(map (\ (ns,tm,_) -> (ns, tm)) pdef)
cs_full
missing' <- checkPossibles info fc True n missing
logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++
showSep "\n" (map showTmImpls missing') ++
"\nAgainst: " ++
showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))
return missing'
else return []
let pcover = null pmissing
pdef_in' <- applyOpts $ map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) pdef_pe
ctxt <- getContext
let pdef' = map (simple_rt ctxt) pdef_in'
logElab 5 $ "After data structure transformations:\n" ++ show pdef'
ist <- getIState
let tot | pcover = Unchecked
| AssertTotal `elem` opts = Total []
| PEGenerated `elem` opts = Generated
| otherwise = Partial NotCovering
case tree of
CaseDef _ _ [] -> return ()
CaseDef _ _ xs -> mapM_ (\x ->
iWarn fc $ text "Unreachable case:" </> text (show (delab ist x))
) xs
let knowncovering = (pcover && cov) || AssertTotal `elem` opts
let defaultcase = if knowncovering
then STerm Erased
else UnmatchedCase $ "*** " ++
show fc ++
":unmatched case in " ++ show n ++
" ***"
tree' <- tclift $ simpleCase tcase defaultcase reflect
RunTime fc inacc atys pdef' erInfo
logElab 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree
logElab 3 $ "Optimised: " ++ show tree'
ctxt <- getContext
ist <- getIState
putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)
(idris_patdefs ist) })
let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)
case lookupTyExact n ctxt of
Just ty ->
do ctxt' <- do ctxt <- getContext
tclift $
addCasedef n erInfo caseInfo
tcase defaultcase
reflect
(AssertTotal `elem` opts)
atys
inacc
pats_forced
pdef
pdef' ty
ctxt
setContext ctxt'
addIBC (IBCDef n)
addDefinedName n
setTotality n tot
when (not reflect && PEGenerated `notElem` opts) $
do totcheck (fc, n)
defer_totcheck (fc, n)
when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
i <- getIState
ctxt <- getContext
case lookupDef n ctxt of
(CaseOp _ _ _ _ _ cd : _) ->
let (scargs, sc) = cases_compiletime cd in
do let calls = map fst $ findCalls sc scargs
logElab 2 $ "Called names: " ++ show calls
nvis <- getFromHideList n
case nvis of
Just Public -> mapM_ (checkVisibility fc n Public Public) calls
_ -> return ()
addCalls n calls
let rig = if linearArg (whnfArgs ctxt [] ty)
then Rig1
else RigW
updateContext (setRigCount n (minRig ctxt rig calls))
addIBC (IBCCG n)
_ -> return ()
return ()
_ -> return ()
when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
checkIfGuarded n
ist <- getIState
let statics = case lookupCtxtExact n (idris_statics ist) of
Just ns -> ns
Nothing -> []
when (or statics) $ do getAllNames n
return ()
where
checkUndefined n ctxt = case lookupDef n ctxt of
[] -> return ()
[TyDecl _ _] -> return ()
_ -> tclift $ tfail (At fc (AlreadyDefined n))
debind (Right (x, y)) = let (vs, x') = depat [] x
(_, y') = depat [] y in
(vs, x', y')
debind (Left x) = let (vs, x') = depat [] x in
(vs, x', Impossible)
depat acc (Bind n (PVar rig t) sc) = depat ((n, t) : acc) (instantiate (P Bound n t) sc)
depat acc x = (acc, x)
getPVs (Bind x (PVar rig _) tm) = let (vs, tm') = getPVs tm
in (x:vs, tm')
getPVs tm = ([], tm)
isPatVar vs (P Bound n _) = n `elem` vs
isPatVar _ _ = False
hasDefault cs | (Right (lhs, rhs) : _) <- reverse cs
, (pvs, tm) <- getPVs (explicitNames lhs)
, (f, args) <- unApply tm = all (isPatVar pvs) args
hasDefault _ = False
getLHS (_, l, _) = l
simple_lhs ctxt (Right (x, y))
= Right (Idris.Core.Evaluate.simplify ctxt [] x, y)
simple_lhs ctxt t = t
force_lhs opts (Right (x, y)) = Right (forceWith opts x, y)
force_lhs opts t = t
simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p
(rt_simplify ctxt [] y)))
specNames [] = Nothing
specNames (Specialise ns : _) = Just ns
specNames (_ : xs) = specNames xs
sameLength ((_, x, _) : xs)
= do l <- sameLength xs
let (_, as) = unApply x
if (null xs || l == length as) then return (length as)
else tfail (At fc (Msg "Clauses have differing numbers of arguments "))
sameLength [] = return 0
doPartialEval ist pats =
case specNames opts of
Nothing -> return pats
Just ns -> case partial_eval (tt_ctxt ist) ns pats of
Just t -> return t
Nothing -> ierror (At fc (Msg "No specialisation achieved"))
minRig :: Context -> RigCount -> [Name] -> RigCount
minRig c minr [] = minr
minRig c minr (r : rs) = case lookupRigCountExact r c of
Nothing -> minRig c minr rs
Just rc -> minRig c (min minr rc) rs
forceWith :: Ctxt OptInfo -> Term -> Term
forceWith opts lhs =
force lhs
where
force ap@(App _ _ _)
| (fn@(P _ c _), args) <- unApply ap,
Just copt <- lookupCtxtExact c opts
= let args' = eraseArg 0 (forceable copt) args in
mkApp fn (map force args')
force (App t f a)
= App t (force f) (force a)
force (Bind n b sc) = Bind n b (force sc)
force t = t
eraseArg i fs (n : ns) | i `elem` fs = Erased : eraseArg (i + 1) fs ns
| otherwise = n : eraseArg (i + 1) fs ns
eraseArg i _ [] = []
elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]
elabPE info fc caller r | pe_depth info > 5 = return []
elabPE info fc caller r =
do ist <- getIState
let sa = filter (\ap -> fst ap /= caller) $ getSpecApps ist [] r
rules <- mapM mkSpecialised sa
return $ concat rules
where
mkSpecialised :: (Name, [(PEArgType, Term)]) -> Idris [(Term, Term)]
mkSpecialised specapp_in = do
ist <- getIState
ctxt <- getContext
(specTy, specapp) <- getSpecTy ist specapp_in
let (n, newnm, specdecl) = getSpecClause ist specapp specTy
let lhs = pe_app specdecl
let rhs = pe_def specdecl
let undef = case lookupDefExact newnm ctxt of
Nothing -> True
_ -> False
logElab 5 $ show (newnm, undef, map (concreteArg ist) (snd specapp))
idrisCatch
(if (undef && all (concreteArg ist) (snd specapp)) then do
cgns <- getAllNames n
let cgns' = filter (\x -> x /= n &&
notStatic ist x) cgns
let maxred = case lookupTotal n ctxt of
[Total _] -> 65536
[Productive] -> 16
_ -> 1
let specnames = mapMaybe (specName (pe_simple specdecl))
(snd specapp)
descs <- mapM getStaticsFrom (map fst specnames)
let opts = [Specialise ((if pe_simple specdecl
then map (\x -> (x, Nothing)) cgns'
else []) ++
(n, Just maxred) : specnames ++
concat descs)]
logElab 3 $ "Specialising application: " ++ show specapp
++ "\n in \n" ++ show caller ++
"\n with \n" ++ show opts
++ "\nCalling: " ++ show cgns
logElab 3 $ "New name: " ++ show newnm
logElab 3 $ "PE definition type : " ++ (show specTy)
++ "\n" ++ show opts
logElab 2 $ "PE definition " ++ show newnm ++ ":\n" ++
showSep "\n"
(map (\ (lhs, rhs) ->
(showTmImpls lhs ++ " = " ++
showTmImpls rhs)) (pe_clauses specdecl))
logElab 5 $ show n ++ " transformation rule: " ++
showTmImpls rhs ++ " ==> " ++ showTmImpls lhs
elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy
let def = map (\(lhs, rhs) ->
let lhs' = mapPT hiddenToPH $ stripUnmatchable ist lhs in
PClause fc newnm lhs' [] rhs [])
(pe_clauses specdecl)
trans <- elabTransform info fc False rhs lhs
elabClauses (info {pe_depth = pe_depth info + 1}) fc
(PEGenerated:opts) newnm def
return [trans]
else return [])
(\e -> do logElab 5 $ "Couldn't specialise: " ++ (pshow ist e)
return [])
hiddenToPH (PHidden _) = Placeholder
hiddenToPH x = x
specName simpl (ImplicitS _, tm)
| (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
specName simpl (ExplicitS, tm)
| (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
specName simpl (ConstraintS, tm)
| (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
specName simpl _ = Nothing
getStaticsFrom :: Name -> Idris [(Name, Maybe Int)]
getStaticsFrom n = do ns <- getAllNames n
i <- getIState
let statics = filter (staticFn i) ns
return (map (\n -> (n, Nothing)) statics)
staticFn :: IState -> Name -> Bool
staticFn i n = case lookupCtxt n (idris_flags i) of
[opts] -> elem StaticFn opts
_ -> False
notStatic ist n = case lookupCtxtExact n (idris_statics ist) of
Just s -> not (or s)
_ -> True
concreteArg ist (ImplicitS _, tm) = concreteTm ist tm
concreteArg ist (ExplicitS, tm) = concreteTm ist tm
concreteArg ist _ = True
concreteTm ist tm | (P _ n _, _) <- unApply tm =
case lookupTy n (tt_ctxt ist) of
[] -> False
_ -> True
concreteTm ist (Constant _) = True
concreteTm ist (Bind n (Lam _ _) sc) = True
concreteTm ist (Bind n (Pi _ _ _ _) sc) = True
concreteTm ist (Bind n (Let _ _ _) sc) = concreteTm ist sc
concreteTm ist _ = False
getSpecTy ist (n, args)
= case lookupTy n (tt_ctxt ist) of
[ty] -> let (specty_in, args') = specType args (explicitNames ty)
specty = normalise (tt_ctxt ist) [] (finalise specty_in)
t = mkPE_TyDecl ist args' (explicitNames specty) in
return (t, (n, args'))
_ -> ifail $ "Ambiguous name " ++ show n ++ " (getSpecTy)"
getSpecClause ist (n, args) specTy
= let newnm = sUN ("PE_" ++ show (nsroot n) ++ "_" ++
qhash 5381 (showSep "_" (map showArg args))) in
(n, newnm, mkPE_TermDecl ist newnm n specTy args)
where showArg (ExplicitS, n) = qshow n
showArg (ImplicitS _, n) = qshow n
showArg _ = ""
qshow (Bind _ _ _) = "fn"
qshow (App _ f a) = qshow f ++ qshow a
qshow (P _ n _) = show n
qshow (Constant c) = show c
qshow _ = ""
qhash :: Word64 -> String -> String
qhash hash [] = showHex (abs hash `mod` 0xffffffff) ""
qhash hash (x:xs) = qhash (hash * 33 + fromIntegral(fromEnum x)) xs
checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)
checkPossible info fc tcgen fname lhs_in
= do ctxt <- getContext
i <- getIState
let lhs = addImplPat i lhs_in
logElab 10 $ "Trying missing case: " ++ showTmImpls lhs
case elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
(erun fc (buildTC i info EImpossible [] fname
(allNamesIn lhs_in)
(infTerm lhs))) of
OK (ElabResult lhs' _ _ ctxt' newDecls highlights newGName, _) ->
do setContext ctxt'
processTacticDecls info newDecls
sendHighlighting highlights
updateIState $ \i -> i { idris_name = newGName }
let lhs_tm = normalise ctxt [] (orderPats (getInferTerm lhs'))
let emptyPat = hasEmptyPat ctxt (idris_datatypes i) lhs_tm
if emptyPat then
do logElab 10 $ "Empty type in pattern "
return Nothing
else
case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of
OK (tm, _, _) ->
do logElab 10 $ "Valid " ++ show tm ++ "\n"
++ " from " ++ show lhs
return (Just (delab' i tm True True))
err -> do logElab 10 $ "Conversion failure"
return Nothing
Error err -> do logLvl 10 $ "Impossible case " ++ (pshow i err)
++ "\n" ++ show (recoverableCoverage ctxt err,
validCoverageCase ctxt err)
if tcgen then returnTm i err (recoverableCoverage ctxt err)
else returnTm i err (validCoverageCase ctxt err ||
recoverableCoverage ctxt err)
where returnTm i err True = do logLvl 10 $ "Possibly resolvable error on " ++
pshow i (fmap (normalise (tt_ctxt i) []) err)
++ " on " ++ showTmImpls lhs_in
return $ Just lhs_in
returnTm i err False = return $ Nothing
checkPossibles :: ElabInfo -> FC -> Bool -> Name -> [PTerm] -> Idris [PTerm]
checkPossibles info fc tcgen fname (lhs : rest)
= do ok <- checkPossible info fc tcgen fname lhs
i <- getIState
let rest' = filter (\x -> not (qmatch x lhs)) (take 200 rest) ++ drop 200 rest
restpos <- checkPossibles info fc tcgen fname rest'
case ok of
Nothing -> return restpos
Just lhstm -> return (lhstm : restpos)
where
qmatch _ Placeholder = True
qmatch (PApp _ f args) (PApp _ f' args')
| length args == length args'
= qmatch f f' && and (zipWith qmatch (map getTm args)
(map getTm args'))
qmatch (PRef _ _ n) (PRef _ _ n') = n == n'
qmatch (PPair _ _ _ l r) (PPair _ _ _ l' r') = qmatch l l' && qmatch r r'
qmatch (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r')
= qmatch l l' && qmatch t t' && qmatch r r'
qmatch x y = x == y
checkPossibles _ _ _ _ [] = return []
findUnique :: Context -> Env -> Term -> [Name]
findUnique ctxt env (Bind n b sc)
= let rawTy = forgetEnv (map fstEnv env) (binderTy b)
uniq = case check ctxt env rawTy of
OK (_, UType UniqueType) -> True
OK (_, UType NullType) -> True
OK (_, UType AllTypes) -> True
_ -> False in
if uniq then n : findUnique ctxt ((n, RigW, b) : env) sc
else findUnique ctxt ((n, RigW, b) : env) sc
findUnique _ _ _ = []
elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
Idris (Either Term (Term, Term), PTerm)
elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
= do let tcgen = Dictionary `elem` opts
i <- get
let lhs = addImpl [] i lhs_in
b <- checkPossible info fc tcgen fname lhs_in
case b of
Just _ -> tclift $ tfail (At fc
(Msg $ show lhs_in ++ " is a valid case"))
Nothing -> do ptm <- mkPatTm lhs_in
logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++
"\n" ++ show ptm
return (Left ptm, lhs)
elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock_as)
= do push_estack fname False
ctxt <- getContext
let (lhs_in, rhs_in, whereblock) = desugarAs lhs_in_as rhs_in_as whereblock_as
i <- getIState
inf <- isTyInferred fname
when (isOutsideWith lhs_in && (not $ null withs)) $
ierror (At (fromMaybe NoFC $ highestFC lhs_in_as)
(Elaborating "left hand side of " fname Nothing
(Msg "unexpected patterns outside of \"with\" block")))
let fn_ty = case lookupTy fname ctxt of
[t] -> t
_ -> error "Can't happen (elabClause function type)"
let fn_is = case lookupCtxt fname (idris_implicits i) of
[t] -> t
_ -> []
let norm_ty = normalise ctxt [] fn_ty
let params = getParamsInType i [] fn_is norm_ty
let tcparams = getTCParamsInType i [] fn_is norm_ty
let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $
propagateParams i params norm_ty (allNamesIn lhs_in) (addImplPat i lhs_in)
logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))
logElab 5 ("LHS: " ++ show opts ++ "\n" ++ show fc ++ " " ++ showTmImpls lhs)
logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ showTmImpls lhs_in ++
"\n" ++ show (fn_ty, fn_is))
((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-
tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
(do res <- errAt "left hand side of " fname Nothing
(erun (fromMaybe NoFC $ highestFC lhs_in_as)
(buildTC i info ELHS opts fname
(allNamesIn lhs_in)
(infTerm lhs)))
probs <- get_probs
inj <- get_inj
return (res, probs, inj))
setContext ctxt'
processTacticDecls info newDecls
sendHighlighting highlights
updateIState $ \i -> i { idris_name = newGName }
when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)
let lhs_tm = orderPats (getInferTerm lhs')
let lhs_ty = getInferType lhs'
let static_names = getStaticNames i lhs_tm
logElab 3 ("Elaborated: " ++ show lhs_tm)
logElab 3 ("Elaborated type: " ++ show lhs_ty)
logElab 5 ("Injective: " ++ show fname ++ " " ++ show inj)
ctxt <- getContext
(clhs_c, clhsty) <- if not inf
then recheckC_borrowing False (PEGenerated `notElem` opts)
[] (constraintNS info) fc id [] lhs_tm
else return (lhs_tm, lhs_ty)
let clhs = normalise ctxt [] clhs_c
let borrowed = borrowedNames [] clhs
when (not (null borrowed)) $
logElab 5 ("Borrowed names on LHS: " ++ show borrowed)
logElab 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))
rep <- useREPL
when rep $ do
addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs)
addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))
logElab 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)
ist <- getIState
ctxt <- getContext
windex <- getName
let decls = nub (concatMap declared whereblock)
let defs = nub (decls ++ concatMap defined whereblock)
let newargs_all = pvars ist lhs_tm
let uniqargs = findUnique ctxt [] lhs_tm
let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all
let winfo = (pinfo info newargs defs windex) { elabFC = Just fc }
let wb = map (mkStatic static_names) $
map (expandImplementationScope ist decorate newargs defs) $
map (expandParamsD False ist decorate newargs defs) whereblock
let (wbefore, wafter) = sepBlocks wb
logElab 5 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
mapM_ (rec_elabDecl info EAll winfo) wbefore
i <- getIState
logElab 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
let rhs = rhs_trans info $
addImplBoundInf i (map fst newargs_all) (defs \\ decls)
(expandParams decorate newargs defs (defs \\ decls) rhs_in)
logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs
ctxt <- getContext
logElab 5 "STARTING CHECK"
((rhsElab, defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-
tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState
(do pbinds ist lhs_tm
mapM_ addPSname (allNamesIn lhs_in)
ulog <- getUnifyLog
traceWhen ulog ("Setting injective: " ++ show (nub (tcparams ++ inj))) $
mapM_ setinj (nub (tcparams ++ inj))
setNextName
(ElabResult _ _ is ctxt' newDecls highlights newGName) <-
errAt "right hand side of " fname (Just clhsty)
(erun fc (build i winfo ERHS opts fname rhs))
errAt "right hand side of " fname (Just clhsty)
(erun fc $ psolve lhs_tm)
tt <- get_term
aux <- getAux
let (tm, ds) = runState (collectDeferred (Just fname)
(map fst $ case_decls aux) ctxt tt) []
probs <- get_probs
hs <- get_holes
return (tm, ds, hs, is, probs, ctxt', newDecls, highlights, newGName))
setContext ctxt'
processTacticDecls info newDecls
sendHighlighting highlights
updateIState $ \i -> i { idris_name = newGName }
when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)
logElab 3 "DONE CHECK"
logElab 3 $ "---> " ++ show rhsElab
ctxt <- getContext
let rhs' = rhsElab
when (not (null defer)) $ logElab 2 $ "DEFERRED " ++
show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
def' <- checkDef info fc (\n -> Elaborating "deferred type of " n Nothing) (null holes) defer
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, null holes))) def'
addDeferred def''
mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
when (not (null def')) $ do
mapM_ defer_totcheck (map (\x -> (fc, fst x)) def'')
mapM_ (rec_elabDecl info EAll winfo) wafter
mapM_ (elabCaseBlock winfo opts) is
ctxt <- getContext
logElab 5 "Rechecking"
logElab 6 $ " ==> " ++ show (forget rhs')
(crhs, crhsty)
<- if (null holes || null def') && not inf
then recheckC_borrowing True (PEGenerated `notElem` opts)
borrowed (constraintNS info) fc id [] rhs'
else return (rhs', clhsty)
logElab 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty
when (not (null holes)) $ do
logElab 5 $ "Making " ++ show fname ++ " frozen due to " ++ show holes
setAccessibility fname Frozen
ctxt <- getContext
let constv = next_tvar ctxt
tit <- typeInType
case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of
OK (_, cs) -> when (PEGenerated `notElem` opts && not tit) $ do
addConstraints fc cs
mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)
logElab 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)
return ()
Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))
i <- getIState
checkInferred fc (delab' i crhs True True) rhs
let (ret_fam, _) = unApply (getRetTy crhsty)
rev <- case ret_fam of
P _ rfamn _ ->
case lookupCtxt rfamn (idris_datatypes i) of
[TI _ _ dopts _ _ _] ->
return (DataErrRev `elem` dopts &&
size clhs <= size crhs)
_ -> return False
_ -> return False
when (rev || ErrorReverse `elem` opts) $ do
addIBC (IBCErrRev (crhs, clhs))
addErrRev (crhs, clhs)
when (rev || ErrorReduce `elem` opts) $ do
addIBC (IBCErrReduce fname)
addErrReduce fname
pop_estack
return (Right (clhs, crhs), lhs)
where
pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo
pinfo info ns ds i
= let newps = params info ++ ns
dsParams = map (\n -> (n, map fst newps)) ds
newb = addAlist dsParams (inblock info) in
info { params = newps,
inblock = newb,
liftname = id
}
borrowedNames :: [Name] -> Term -> [Name]
borrowedNames env (App _ (App _ (P _ (NS (UN lend) [owner]) _) _) arg)
| owner == txt "Ownership" &&
(lend == txt "lend" || lend == txt "Read") = getVs arg
where
getVs (V i) = [env!!i]
getVs (App _ f a) = nub $ getVs f ++ getVs a
getVs _ = []
borrowedNames env (App _ f a) = nub $ borrowedNames env f ++ borrowedNames env a
borrowedNames env (Bind n b sc) = nub $ borrowedB b ++ borrowedNames (n:env) sc
where borrowedB (Let _ t v) = nub $ borrowedNames env t ++ borrowedNames env v
borrowedB b = borrowedNames env (binderTy b)
borrowedNames _ _ = []
mkLHSapp t@(PRef _ _ _) = PApp fc t []
mkLHSapp t = t
decorate (NS x ns)
= NS (SN (WhereN cnum fname x)) ns
decorate x
= SN (WhereN cnum fname x)
sepBlocks bs = sepBlocks' [] bs where
sepBlocks' ns (d@(PTy _ _ _ _ _ n _ t) : bs)
= let (bf, af) = sepBlocks' (n : ns) bs in
(d : bf, af)
sepBlocks' ns (d@(PClauses _ _ n _) : bs)
| not (n `elem` ns) = let (bf, af) = sepBlocks' ns bs in
(bf, d : af)
sepBlocks' ns (b : bs) = let (bf, af) = sepBlocks' ns bs in
(b : bf, af)
sepBlocks' ns [] = ([], [])
isOutsideWith :: PTerm -> Bool
isOutsideWith (PApp _ (PRef _ _ (SN (WithN _ _))) _) = False
isOutsideWith _ = True
elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
= do ctxt <- getContext
i <- getIState
let fn_ty = case lookupTy fname ctxt of
[t] -> t
_ -> error "Can't happen (elabClause function type)"
let fn_is = case lookupCtxt fname (idris_implicits i) of
[t] -> t
_ -> []
let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)
let lhs = stripLinear i $ stripUnmatchable i $
propagateParams i params fn_ty (allNamesIn lhs_in)
(addImplPat i lhs_in)
logElab 2 ("LHS: " ++ show lhs)
(ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-
tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
(errAt "left hand side of with in " fname Nothing
(erun (fromMaybe NoFC $ highestFC lhs_in)
(buildTC i info ELHS opts fname
(allNamesIn lhs_in)
(infTerm lhs))) )
setContext ctxt'
processTacticDecls info newDecls
sendHighlighting highlights
updateIState $ \i -> i { idris_name = newGName }
ctxt <- getContext
let lhs_tm = orderPats (getInferTerm lhs')
let lhs_ty = getInferType lhs'
let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))
let static_names = getStaticNames i lhs_tm
logElab 5 (show lhs_tm ++ "\n" ++ show static_names)
(clhs_c, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm
let clhs = normalise ctxt [] clhs_c
logElab 5 ("Checked " ++ show clhs)
let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))
wval <- case wval_in of
Placeholder -> ierror $ At fc $
Msg "No expression for the with block to inspect.\nYou need to replace the _ with an expression."
_ -> return $
rhs_trans info $
addImplBound i (map fst bargs) wval_in
logElab 5 ("Checking " ++ showTmImpls wval)
((wvalElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-
tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")
(bindTyArgs PVTy bargs infP) initEState
(do pbinds i lhs_tm
mapM_ addPSname (allNamesIn lhs_in)
setNextName
(ElabResult _ d is ctxt' newDecls highlights newGName) <- errAt "with value in " fname Nothing
(erun fc (build i info ERHS opts fname (infTerm wval)))
erun fc $ psolve lhs_tm
tt <- get_term
return (tt, d, is, ctxt', newDecls, highlights, newGName))
setContext ctxt'
processTacticDecls info newDecls
sendHighlighting highlights
updateIState $ \i -> i { idris_name = newGName }
def' <- checkDef info fc iderr True defer
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
addDeferred def''
mapM_ (elabCaseBlock info opts) is
let wval' = wvalElab
logElab 5 ("Checked wval " ++ show wval')
ctxt <- getContext
(cwval, cwvalty) <- recheckC (constraintNS info) fc id [] (getInferTerm wval')
let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
let cwvalN = explicitNames (normalise ctxt [] cwval)
logElab 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
case getArgTys cwvaltyN of
[] -> return ()
(_:_) -> ierror $ At fc (WithFnType cwvalty)
let pvars = map fst (getPBtys cwvalty)
let pdeps = usedNamesIn pvars i (delab i cwvalty)
let (bargs_pre, bargs_post) = split pdeps bargs []
let mpn = case pn_in of
Nothing -> Nothing
Just (n, nfc) -> Just (uniqueName n (map fst bargs))
sendHighlighting [(fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]
logElab 10 ("With type " ++ show (getRetTy cwvaltyN) ++
" depends on " ++ show pdeps ++ " from " ++ show pvars)
logElab 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)
windex <- getName
let wargval = getRetTy cwvalN
let wargtype = getRetTy cwvaltyN
let wargname = sMN windex "warg"
logElab 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)
let wtype = bindTyArgs (flip (Pi RigW Nothing) (TType (UVar [] 0))) (bargs_pre ++
(wargname, wargtype) :
map (abstract wargname wargval wargtype) bargs_post ++
case mpn of
Just pn -> [(pn, mkApp (P Ref eqTy Erased)
[wargtype, wargtype,
P Bound wargname Erased, wargval])]
Nothing -> [])
(substTerm wargval (P Bound wargname wargtype) ret_ty)
logElab 3 ("New function type " ++ show wtype)
let wname = SN (WithN windex fname)
let imps = getImps wtype
putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })
let statics = getStatics static_names wtype
logElab 5 ("Static positions " ++ show statics)
i <- getIState
putIState (i { idris_statics = addDef wname statics (idris_statics i) })
addIBC (IBCDef wname)
addIBC (IBCImp wname)
addIBC (IBCStatic wname)
def' <- checkDef info fc iderr True [(wname, (1, Nothing, wtype, []))]
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
addDeferred def''
wb <- mapM (mkAuxC mpn wname lhs (map fst bargs_pre) (map fst bargs_post))
withblock
logElab 3 ("with block " ++ show wb)
setFlags wname [Inlinable]
when (AssertTotal `elem` opts) $
setFlags wname [Inlinable, AssertTotal]
i <- getIState
let rhstrans' = updateWithTerm i mpn wname lhs (map fst bargs_pre) (map fst (bargs_post))
. rhs_trans info
mapM_ (rec_elabDecl info EAll (info { rhs_trans = rhstrans' })) wb
let rhs = PApp fc (PRef fc [] wname)
(map (pexp . (PRef fc []) . fst) bargs_pre ++
pexp wval :
(map (pexp . (PRef fc []) . fst) bargs_post) ++
case mpn of
Nothing -> []
Just _ -> [pexp (PApp NoFC (PRef NoFC [] eqCon)
[ pimp (sUN "A") Placeholder False
, pimp (sUN "x") Placeholder False
])])
logElab 5 ("New RHS " ++ showTmImpls rhs)
ctxt <- getContext
i <- getIState
((rhsElab, defer, is, ctxt', newDecls, highlights, newGName), _) <-
tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState
(do pbinds i lhs_tm
setNextName
(ElabResult _ d is ctxt' newDecls highlights newGName) <-
erun fc (build i info ERHS opts fname rhs)
psolve lhs_tm
tt <- get_term
return (tt, d, is, ctxt', newDecls, highlights, newGName))
setContext ctxt'
processTacticDecls info newDecls
sendHighlighting highlights
updateIState $ \i -> i { idris_name = newGName }
ctxt <- getContext
let rhs' = rhsElab
def' <- checkDef info fc iderr True defer
let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
addDeferred def''
mapM_ (elabCaseBlock info opts) is
logElab 5 ("Checked RHS " ++ show rhs')
(crhs, crhsty) <- recheckC (constraintNS info) fc id [] rhs'
return (Right (clhs, crhs), lhs)
where
getImps (Bind n (Pi _ _ _ _) t) = pexp Placeholder : getImps t
getImps _ = []
mkAuxC pn wname lhs ns ns' (PClauses fc o n cs)
= do cs' <- mapM (mkAux pn wname lhs ns ns') cs
return $ PClauses fc o wname cs'
mkAuxC pn wname lhs ns ns' d = return d
mkAux pn wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
= do i <- getIState
let tm = addImplPat i tm_in
logElab 2 ("Matching " ++ showTmImpls tm ++ " against " ++
showTmImpls toplhs)
case matchClause i toplhs tm of
Left (a,b) -> ifail $ show fc ++ ":with clause does not match top level"
Right mvars ->
do logElab 3 ("Match vars : " ++ show mvars)
lhs <- updateLHS n pn wname mvars ns ns' (fullApp tm) w
return $ PClause fc wname lhs ws rhs wheres
mkAux pn wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval pn' withs)
= do i <- getIState
let tm = addImplPat i tm_in
logElab 2 ("Matching " ++ showTmImpls tm ++ " against " ++
showTmImpls toplhs)
withs' <- mapM (mkAuxC pn wname toplhs ns ns') withs
case matchClause i toplhs tm of
Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")
Right mvars ->
do lhs <- updateLHS n pn wname mvars ns ns' (fullApp tm) w
return $ PWith fc wname lhs ws wval pn' withs'
mkAux pn wname toplhs ns ns' c
= ifail $ show fc ++ ":badly formed with clause"
updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w
= let ns = map (keepMvar (map fst mvars) fc') ns_in
ns' = map (keepMvar (map fst mvars) fc') ns_in' in
return $ substMatches mvars $
PApp fc (PRef fc' [] wname)
(map pexp ns ++ pexp w : (map pexp ns') ++
case pn of
Nothing -> []
Just pnm -> [pexp (PRef fc [] pnm)])
updateLHS n pn wname mvars ns_in ns_in' tm w
= updateLHS n pn wname mvars ns_in ns_in' (PApp fc tm []) w
keepMvar mvs fc v | v `elem` mvs = PRef fc [] v
| otherwise = Placeholder
updateWithTerm :: IState -> Maybe Name -> Name -> PTerm -> [Name] -> [Name] -> PTerm -> PTerm
updateWithTerm ist pn wname toplhs ns_in ns_in' tm
= mapPT updateApp tm
where
currentFn fname (PAlternative _ _ as)
| Just tm <- getApp as = tm
where getApp (tm@(PApp _ (PRef _ _ f) _) : as)
| f == fname = Just tm
getApp (_ : as) = getApp as
getApp [] = Nothing
currentFn _ tm = tm
updateApp wtm@(PWithApp fcw tm_in warg) =
let tm = currentFn fname tm_in in
case matchClause ist toplhs tm of
Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level "))
Right mvars ->
let ns = map (keepMvar (map fst mvars) fcw) ns_in
ns' = map (keepMvar (map fst mvars) fcw) ns_in'
wty = lookupTyExact wname (tt_ctxt ist)
res = substMatches mvars $
PApp fcw (PRef fcw [] wname)
(map pexp ns ++ pexp warg : (map pexp ns') ++
case pn of
Nothing -> []
Just pnm -> [pexp (PRef fc [] pnm)]) in
case wty of
Nothing -> res
Just ty -> addResolves ty res
updateApp tm = tm
addResolves ty (PApp fc f args) = PApp fc f (addResolvesArgs fc ty args)
addResolves ty tm = tm
addResolvesArgs :: FC -> Term -> [PArg] -> [PArg]
addResolvesArgs fc (Bind n (Pi _ _ ty _) sc) (a : args)
| (P _ cn _, _) <- unApply ty,
getTm a == Placeholder
= case lookupCtxtExact cn (idris_interfaces ist) of
Just _ -> a { getTm = PResolveTC fc } : addResolvesArgs fc sc args
Nothing -> a : addResolvesArgs fc sc args
addResolvesArgs fc (Bind n (Pi _ _ ty _) sc) (a : args)
= a : addResolvesArgs fc sc args
addResolvesArgs fc _ args = args
fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
fullApp x = x
split [] rest pre = (reverse pre, rest)
split deps ((n, ty) : rest) pre
| n `elem` deps = split (deps \\ [n]) rest ((n, ty) : pre)
| otherwise = split deps rest ((n, ty) : pre)
split deps [] pre = (reverse pre, [])
abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)
mapRHS :: (PTerm -> PTerm) -> PClause -> PClause
mapRHS f (PClause fc n lhs args rhs ws)
= PClause fc n lhs args (f rhs) (map (mapRHSdecl f) ws)
mapRHS f (PWith fc n lhs args warg prf ws)
= PWith fc n lhs args (f warg) prf (map (mapRHSdecl f) ws)
mapRHS f (PClauseR fc args rhs ws)
= PClauseR fc args (f rhs) (map (mapRHSdecl f) ws)
mapRHS f (PWithR fc args warg prf ws)
= PWithR fc args (f warg) prf (map (mapRHSdecl f) ws)
mapRHSdecl :: (PTerm -> PTerm) -> PDecl -> PDecl
mapRHSdecl f (PClauses fc opt n cs)
= PClauses fc opt n (map (mapRHS f) cs)
mapRHSdecl f t = t