2019-04-06 15:53:59 +03:00
|
|
|
module TTImp.ProcessDef
|
|
|
|
|
2019-04-20 18:54:09 +03:00
|
|
|
import Core.CaseBuilder
|
|
|
|
import Core.CaseTree
|
2019-04-06 15:53:59 +03:00
|
|
|
import Core.Context
|
|
|
|
import Core.Core
|
2019-06-02 22:03:41 +03:00
|
|
|
import Core.Coverage
|
2019-04-06 15:53:59 +03:00
|
|
|
import Core.Env
|
2019-05-31 13:42:11 +03:00
|
|
|
import Core.Hash
|
2019-06-14 20:35:31 +03:00
|
|
|
import Core.LinearCheck
|
2019-05-31 07:52:54 +03:00
|
|
|
import Core.Metadata
|
2019-04-06 15:53:59 +03:00
|
|
|
import Core.Normalise
|
2019-06-05 17:59:35 +03:00
|
|
|
import Core.Termination
|
2019-04-19 18:35:06 +03:00
|
|
|
import Core.Value
|
2019-04-06 15:53:59 +03:00
|
|
|
import Core.UnifyState
|
|
|
|
|
2019-05-27 01:51:20 +03:00
|
|
|
import TTImp.BindImplicits
|
2019-04-06 15:53:59 +03:00
|
|
|
import TTImp.Elab
|
|
|
|
import TTImp.Elab.Check
|
2020-02-24 00:40:23 +03:00
|
|
|
import TTImp.Impossible
|
2019-04-06 15:53:59 +03:00
|
|
|
import TTImp.TTImp
|
2019-06-03 01:43:21 +03:00
|
|
|
import TTImp.Unelab
|
2019-05-29 13:57:07 +03:00
|
|
|
import TTImp.Utils
|
2019-07-30 14:32:33 +03:00
|
|
|
import TTImp.WithClause
|
2019-04-06 15:53:59 +03:00
|
|
|
|
2019-06-03 01:43:21 +03:00
|
|
|
import Data.NameMap
|
|
|
|
|
2019-06-01 21:05:02 +03:00
|
|
|
mutual
|
|
|
|
mismatchNF : Defs -> NF vars -> NF vars -> Core Bool
|
2019-10-26 00:24:25 +03:00
|
|
|
mismatchNF defs (NTCon _ xn xt _ xargs) (NTCon _ yn yt _ yargs)
|
2019-06-05 19:28:55 +03:00
|
|
|
= if xn /= yn
|
2019-06-01 21:05:02 +03:00
|
|
|
then pure True
|
2019-10-26 00:24:25 +03:00
|
|
|
else anyM (mismatch defs) (zip xargs yargs)
|
|
|
|
mismatchNF defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
|
2019-06-01 21:05:02 +03:00
|
|
|
= if xt /= yt
|
|
|
|
then pure True
|
2019-10-26 00:24:25 +03:00
|
|
|
else anyM (mismatch defs) (zip xargs yargs)
|
2019-06-01 21:05:02 +03:00
|
|
|
mismatchNF defs (NPrimVal _ xc) (NPrimVal _ yc) = pure (xc /= yc)
|
|
|
|
mismatchNF defs (NDelayed _ _ x) (NDelayed _ _ y) = mismatchNF defs x y
|
2019-10-26 00:24:25 +03:00
|
|
|
mismatchNF defs (NDelay _ _ _ x) (NDelay _ _ _ y)
|
2019-06-01 21:05:02 +03:00
|
|
|
= mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
|
|
|
|
mismatchNF _ _ _ = pure False
|
|
|
|
|
|
|
|
mismatch : Defs -> (Closure vars, Closure vars) -> Core Bool
|
2019-10-26 00:24:25 +03:00
|
|
|
mismatch defs (x, y)
|
2019-06-01 21:05:02 +03:00
|
|
|
= mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
|
|
|
|
|
|
|
|
-- If the terms have the same type constructor at the head, and one of
|
|
|
|
-- the argument positions has different constructors at its head, then this
|
|
|
|
-- is an impossible case, so return True
|
|
|
|
export
|
|
|
|
impossibleOK : Defs -> NF vars -> NF vars -> Core Bool
|
2019-06-05 19:28:55 +03:00
|
|
|
impossibleOK defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
|
|
|
|
= if xn == yn
|
2019-06-13 21:33:10 +03:00
|
|
|
then anyM (mismatch defs) (zip xargs yargs)
|
2019-06-05 19:28:55 +03:00
|
|
|
else pure False
|
|
|
|
-- If it's a data constructor, any mismatch will do
|
|
|
|
impossibleOK defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
|
|
|
|
= if xt /= yt
|
|
|
|
then pure True
|
2019-06-13 21:33:10 +03:00
|
|
|
else anyM (mismatch defs) (zip xargs yargs)
|
2019-07-05 13:26:45 +03:00
|
|
|
impossibleOK defs (NPrimVal _ x) (NPrimVal _ y) = pure (x /= y)
|
|
|
|
impossibleOK defs (NDCon _ _ _ _ _) (NPrimVal _ _) = pure True
|
|
|
|
impossibleOK defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure True
|
2019-06-05 19:28:55 +03:00
|
|
|
impossibleOK defs x y = pure False
|
2019-10-26 00:24:25 +03:00
|
|
|
|
2019-07-01 01:54:50 +03:00
|
|
|
export
|
|
|
|
impossibleErrOK : {auto c : Ref Ctxt Defs} ->
|
|
|
|
Defs -> Error -> Core Bool
|
|
|
|
impossibleErrOK defs (CantConvert fc env l r)
|
|
|
|
= do logTerm 10 "Impossible" !(normalise defs env l)
|
|
|
|
logTerm 10 " ...and" !(normalise defs env r)
|
|
|
|
impossibleOK defs !(nf defs env l)
|
|
|
|
!(nf defs env r)
|
|
|
|
impossibleErrOK defs (CantSolveEq fc env l r)
|
|
|
|
= do logTerm 10 "Impossible" !(normalise defs env l)
|
|
|
|
logTerm 10 " ...and" !(normalise defs env r)
|
|
|
|
impossibleOK defs !(nf defs env l)
|
|
|
|
!(nf defs env r)
|
2020-01-24 19:16:31 +03:00
|
|
|
impossibleErrOK defs (BadDotPattern _ _ ErasedArg _ _) = pure True
|
2019-07-05 13:26:45 +03:00
|
|
|
impossibleErrOK defs (CyclicMeta _ _) = pure True
|
2019-07-01 01:54:50 +03:00
|
|
|
impossibleErrOK defs (AllFailed errs)
|
|
|
|
= anyM (impossibleErrOK defs) (map snd errs)
|
|
|
|
impossibleErrOK defs (WhenUnifying _ _ _ _ err)
|
|
|
|
= impossibleErrOK defs err
|
|
|
|
impossibleErrOK defs _ = pure False
|
2019-06-01 21:05:02 +03:00
|
|
|
|
2019-04-19 18:06:26 +03:00
|
|
|
-- Given a type checked LHS and its type, return the environment in which we
|
|
|
|
-- should check the RHS, the LHS and its type in that environment,
|
|
|
|
-- and a function which turns a checked RHS into a
|
|
|
|
-- pattern clause
|
2019-05-17 15:52:09 +03:00
|
|
|
-- The 'SubVars' proof contains a proof that refers to the *inner* environment,
|
|
|
|
-- so all the outer things are marked as 'DropCons'
|
|
|
|
extendEnv : Env Term vars -> SubVars inner vars ->
|
|
|
|
NestedNames vars ->
|
2019-10-26 00:24:25 +03:00
|
|
|
Term vars -> Term vars ->
|
|
|
|
Core (vars' **
|
2019-05-17 15:52:09 +03:00
|
|
|
(SubVars inner vars',
|
2019-10-26 00:24:25 +03:00
|
|
|
Env Term vars', NestedNames vars',
|
2019-05-17 15:52:09 +03:00
|
|
|
Term vars', Term vars'))
|
2019-07-08 13:55:55 +03:00
|
|
|
extendEnv env p nest (Bind _ n (PVar c pi tmty) sc) (Bind _ n' (PVTy _ _) tysc) with (nameEq n n')
|
|
|
|
extendEnv env p nest (Bind _ n (PVar c pi tmty) sc) (Bind _ n' (PVTy _ _) tysc) | Nothing
|
2019-04-19 18:06:26 +03:00
|
|
|
= throw (InternalError "Can't happen: names don't match in pattern type")
|
2019-07-08 13:55:55 +03:00
|
|
|
extendEnv env p nest (Bind _ n (PVar c pi tmty) sc) (Bind _ n (PVTy _ _) tysc) | (Just Refl)
|
|
|
|
= extendEnv (PVar c pi tmty :: env) (DropCons p) (weaken nest) sc tysc
|
2019-05-17 15:52:09 +03:00
|
|
|
extendEnv env p nest (Bind _ n (PLet c tmval tmty) sc) (Bind _ n' (PLet _ _ _) tysc) with (nameEq n n')
|
|
|
|
extendEnv env p nest (Bind _ n (PLet c tmval tmty) sc) (Bind _ n' (PLet _ _ _) tysc) | Nothing
|
2019-05-09 18:46:16 +03:00
|
|
|
= throw (InternalError "Can't happen: names don't match in pattern type")
|
|
|
|
-- PLet on the left becomes Let on the right, to give it computational force
|
2019-05-17 15:52:09 +03:00
|
|
|
extendEnv env p nest (Bind _ n (PLet c tmval tmty) sc) (Bind _ n (PLet _ _ _) tysc) | (Just Refl)
|
|
|
|
= extendEnv (Let c tmval tmty :: env) (DropCons p) (weaken nest) sc tysc
|
2019-10-26 00:24:25 +03:00
|
|
|
extendEnv env p nest tm ty
|
2019-05-17 15:52:09 +03:00
|
|
|
= pure (_ ** (p, env, nest, tm, ty))
|
2019-04-19 18:06:26 +03:00
|
|
|
|
2019-04-19 18:35:06 +03:00
|
|
|
-- Find names which are applied to a function in a Rig1/Rig0 position,
|
|
|
|
-- so that we know how they should be bound on the right hand side of the
|
|
|
|
-- pattern.
|
|
|
|
-- 'bound' counts the number of variables locally bound; these are the
|
|
|
|
-- only ones we're checking linearity of (we may be shadowing names if this
|
|
|
|
-- is a local definition, so we need to leave the earlier ones alone)
|
|
|
|
findLinear : {auto c : Ref Ctxt Defs} ->
|
2019-10-26 00:24:25 +03:00
|
|
|
Bool -> Nat -> RigCount -> Term vars ->
|
2019-04-19 18:35:06 +03:00
|
|
|
Core (List (Name, RigCount))
|
2019-10-26 00:24:25 +03:00
|
|
|
findLinear top bound rig (Bind fc n b sc)
|
2019-04-19 18:35:06 +03:00
|
|
|
= findLinear top (S bound) rig sc
|
2020-02-09 16:46:58 +03:00
|
|
|
findLinear top bound rig (As fc _ _ p)
|
2019-06-16 23:33:59 +03:00
|
|
|
= findLinear top bound rig p
|
2019-04-19 18:35:06 +03:00
|
|
|
findLinear top bound rig tm
|
|
|
|
= case getFnArgs tm of
|
|
|
|
(Ref _ _ n, []) => pure []
|
2019-06-13 21:33:10 +03:00
|
|
|
(Ref _ nt n, args)
|
|
|
|
=> do defs <- get Ctxt
|
2019-04-19 18:35:06 +03:00
|
|
|
Just nty <- lookupTyExact n (gamma defs)
|
|
|
|
| Nothing => pure []
|
|
|
|
findLinArg (accessible nt rig) !(nf defs [] nty) args
|
|
|
|
_ => pure []
|
|
|
|
where
|
|
|
|
accessible : NameType -> RigCount -> RigCount
|
|
|
|
accessible Func r = if top then r else Rig0
|
|
|
|
accessible _ r = r
|
|
|
|
|
2019-10-26 00:24:25 +03:00
|
|
|
findLinArg : RigCount -> NF [] -> List (Term vars) ->
|
2019-04-19 18:35:06 +03:00
|
|
|
Core (List (Name, RigCount))
|
2020-02-09 16:46:58 +03:00
|
|
|
findLinArg rig ty (As fc UseLeft _ p :: as)
|
|
|
|
= findLinArg rig ty (p :: as)
|
|
|
|
findLinArg rig ty (As fc UseRight p _ :: as)
|
|
|
|
= findLinArg rig ty (p :: as)
|
2019-10-26 00:24:25 +03:00
|
|
|
findLinArg rig (NBind _ x (Pi c _ _) sc) (Local {name=a} fc _ idx prf :: as)
|
2019-05-03 04:43:47 +03:00
|
|
|
= do defs <- get Ctxt
|
|
|
|
if idx < bound
|
|
|
|
then do sc' <- sc defs (toClosure defaultOpts [] (Ref fc Bound x))
|
2019-10-26 00:24:25 +03:00
|
|
|
pure $ (a, rigMult c rig) ::
|
2019-05-03 04:43:47 +03:00
|
|
|
!(findLinArg rig sc' as)
|
|
|
|
else do sc' <- sc defs (toClosure defaultOpts [] (Ref fc Bound x))
|
|
|
|
findLinArg rig sc' as
|
2019-10-26 00:24:25 +03:00
|
|
|
findLinArg rig (NBind fc x (Pi c _ _) sc) (a :: as)
|
2019-05-03 04:43:47 +03:00
|
|
|
= do defs <- get Ctxt
|
|
|
|
pure $ !(findLinear False bound (rigMult c rig) a) ++
|
|
|
|
!(findLinArg rig !(sc defs (toClosure defaultOpts [] (Ref fc Bound x))) as)
|
2019-10-26 00:24:25 +03:00
|
|
|
findLinArg rig ty (a :: as)
|
2019-04-19 18:35:06 +03:00
|
|
|
= pure $ !(findLinear False bound rig a) ++ !(findLinArg rig ty as)
|
|
|
|
findLinArg _ _ [] = pure []
|
|
|
|
|
|
|
|
setLinear : List (Name, RigCount) -> Term vars -> Term vars
|
2019-07-08 13:55:55 +03:00
|
|
|
setLinear vs (Bind fc x (PVar c p ty) sc)
|
2019-04-19 18:35:06 +03:00
|
|
|
= case lookup x vs of
|
2019-07-08 13:55:55 +03:00
|
|
|
Just c' => Bind fc x (PVar c' p ty) (setLinear vs sc)
|
|
|
|
_ => Bind fc x (PVar c p ty) (setLinear vs sc)
|
2019-04-19 18:35:06 +03:00
|
|
|
setLinear vs (Bind fc x (PVTy c ty) sc)
|
|
|
|
= case lookup x vs of
|
|
|
|
Just c' => Bind fc x (PVTy c' ty) (setLinear vs sc)
|
|
|
|
_ => Bind fc x (PVTy c ty) (setLinear vs sc)
|
|
|
|
setLinear vs tm = tm
|
|
|
|
|
|
|
|
-- Combining multiplicities on LHS:
|
|
|
|
-- Rig1 + Rig1/W not valid, since it means we have repeated use of name
|
|
|
|
-- Rig0 + RigW = RigW
|
|
|
|
-- Rig0 + Rig1 = Rig1
|
|
|
|
combineLinear : FC -> List (Name, RigCount) ->
|
|
|
|
Core (List (Name, RigCount))
|
|
|
|
combineLinear loc [] = pure []
|
|
|
|
combineLinear loc ((n, count) :: cs)
|
|
|
|
= case lookupAll n cs of
|
|
|
|
[] => pure $ (n, count) :: !(combineLinear loc cs)
|
|
|
|
counts => do count' <- combineAll count counts
|
2019-10-26 00:24:25 +03:00
|
|
|
pure $ (n, count') ::
|
2019-04-19 18:35:06 +03:00
|
|
|
!(combineLinear loc (filter notN cs))
|
|
|
|
where
|
|
|
|
notN : (Name, RigCount) -> Bool
|
|
|
|
notN (n', _) = n /= n'
|
|
|
|
|
|
|
|
lookupAll : Name -> List (Name, RigCount) -> List RigCount
|
|
|
|
lookupAll n [] = []
|
2019-10-26 00:24:25 +03:00
|
|
|
lookupAll n ((n', c) :: cs)
|
2019-04-19 18:35:06 +03:00
|
|
|
= if n == n' then c :: lookupAll n cs else lookupAll n cs
|
|
|
|
|
|
|
|
combine : RigCount -> RigCount -> Core RigCount
|
|
|
|
combine Rig1 Rig1 = throw (LinearUsed loc 2 n)
|
|
|
|
combine Rig1 RigW = throw (LinearUsed loc 2 n)
|
|
|
|
combine RigW Rig1 = throw (LinearUsed loc 2 n)
|
|
|
|
combine RigW RigW = pure RigW
|
|
|
|
combine Rig0 c = pure c
|
|
|
|
combine c Rig0 = pure c
|
|
|
|
|
|
|
|
combineAll : RigCount -> List RigCount -> Core RigCount
|
|
|
|
combineAll c [] = pure c
|
|
|
|
combineAll c (c' :: cs)
|
|
|
|
= do newc <- combine c c'
|
|
|
|
combineAll newc cs
|
|
|
|
|
2019-05-29 13:57:07 +03:00
|
|
|
checkLHS : {vars : _} ->
|
|
|
|
{auto c : Ref Ctxt Defs} ->
|
2019-05-31 07:52:54 +03:00
|
|
|
{auto m : Ref MD Metadata} ->
|
2019-05-29 13:57:07 +03:00
|
|
|
{auto u : Ref UST UState} ->
|
|
|
|
(mult : RigCount) -> (hashit : Bool) ->
|
|
|
|
Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
|
2019-10-26 00:24:25 +03:00
|
|
|
FC -> RawImp ->
|
2019-07-30 14:32:33 +03:00
|
|
|
Core (RawImp, -- checked LHS with implicits added
|
|
|
|
(vars' ** (SubVars vars vars',
|
2019-10-26 00:24:25 +03:00
|
|
|
Env Term vars', NestedNames vars',
|
2019-07-30 14:32:33 +03:00
|
|
|
Term vars', Term vars')))
|
2019-06-09 13:58:29 +03:00
|
|
|
checkLHS {vars} mult hashit n opts nest env fc lhs_in
|
|
|
|
= do defs <- get Ctxt
|
2019-10-26 00:24:25 +03:00
|
|
|
lhs_raw <- lhsInCurrentNS nest lhs_in
|
2020-01-27 20:31:53 +03:00
|
|
|
autoimp <- isUnboundImplicits
|
|
|
|
setUnboundImplicits True
|
2019-06-10 01:12:11 +03:00
|
|
|
(_, lhs_bound) <- bindNames False lhs_raw
|
2020-01-27 20:31:53 +03:00
|
|
|
setUnboundImplicits autoimp
|
2019-06-10 01:12:11 +03:00
|
|
|
lhs <- implicitsAs defs vars lhs_bound
|
2019-05-27 01:51:20 +03:00
|
|
|
|
2019-07-22 13:19:10 +03:00
|
|
|
log 5 $ "Checking LHS of " ++ show !(getFullName (Resolved n)) ++
|
|
|
|
" " ++ show lhs
|
2019-05-17 20:47:20 +03:00
|
|
|
logEnv 5 "In env" env
|
2019-10-26 00:24:25 +03:00
|
|
|
(lhstm, lhstyg) <-
|
2019-06-24 02:12:58 +03:00
|
|
|
wrapError (InLHS fc !(getFullName (Resolved n))) $
|
2019-10-26 00:24:25 +03:00
|
|
|
elabTerm n (InLHS mult) opts nest env
|
2019-04-18 16:51:04 +03:00
|
|
|
(IBindHere fc PATTERN lhs) Nothing
|
2020-02-09 16:46:58 +03:00
|
|
|
logTerm 5 "Checked LHS term" lhstm
|
2019-04-19 18:06:26 +03:00
|
|
|
lhsty <- getTerm lhstyg
|
|
|
|
|
2019-04-19 18:35:06 +03:00
|
|
|
-- Normalise the LHS to get any functions or let bindings evaluated
|
|
|
|
-- (this might be allowed, e.g. for 'fromInteger')
|
|
|
|
defs <- get Ctxt
|
2019-05-18 13:47:57 +03:00
|
|
|
lhstm <- normaliseLHS defs (letToLam env) lhstm
|
2019-04-19 18:35:06 +03:00
|
|
|
lhsty <- normaliseHoles defs env lhsty
|
|
|
|
linvars_in <- findLinear True 0 Rig1 lhstm
|
2019-06-16 23:33:59 +03:00
|
|
|
logTerm 10 "Checked LHS term after normalise" lhstm
|
2019-10-26 00:24:25 +03:00
|
|
|
log 5 $ "Linearity of names in " ++ show n ++ ": " ++
|
2019-04-19 18:35:06 +03:00
|
|
|
show linvars_in
|
|
|
|
|
|
|
|
linvars <- combineLinear fc linvars_in
|
|
|
|
let lhstm_lin = setLinear linvars lhstm
|
|
|
|
let lhsty_lin = setLinear linvars lhsty
|
|
|
|
|
2020-02-09 16:46:58 +03:00
|
|
|
logTerm 3 "LHS term" lhstm_lin
|
2019-04-21 00:00:58 +03:00
|
|
|
logTerm 5 "LHS type" lhsty_lin
|
2019-05-31 13:42:11 +03:00
|
|
|
setHoleLHS (bindEnv fc env lhstm_lin)
|
2019-04-19 18:06:26 +03:00
|
|
|
|
2019-07-30 14:32:33 +03:00
|
|
|
ext <- extendEnv env SubRefl nest lhstm_lin lhsty_lin
|
|
|
|
pure (lhs, ext)
|
2019-05-29 13:57:07 +03:00
|
|
|
|
2019-07-08 13:55:55 +03:00
|
|
|
plicit : Binder (Term vars) -> PiInfo
|
|
|
|
plicit (Pi _ p _) = p
|
|
|
|
plicit (PVar _ p _) = p
|
|
|
|
plicit _ = Explicit
|
|
|
|
|
2019-07-09 00:05:04 +03:00
|
|
|
bindNotReq : {vs : _} ->
|
2019-10-26 00:24:25 +03:00
|
|
|
FC -> Int -> Env Term vs -> (sub : SubVars pre vs) ->
|
2019-07-08 13:55:55 +03:00
|
|
|
List (PiInfo, Name) ->
|
|
|
|
Term vs -> (List (PiInfo, Name), Term pre)
|
|
|
|
bindNotReq fc i [] SubRefl ns tm = (ns, embed tm)
|
2019-10-26 00:24:25 +03:00
|
|
|
bindNotReq fc i (b :: env) SubRefl ns tm
|
|
|
|
= let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
|
2019-07-08 13:55:55 +03:00
|
|
|
(ns', btm) = bindNotReq fc (1 + i) env SubRefl ns tmptm in
|
|
|
|
(ns', refToLocal (MN "arg" i) _ btm)
|
2019-10-26 00:24:25 +03:00
|
|
|
bindNotReq fc i (b :: env) (KeepCons p) ns tm
|
|
|
|
= let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
|
2019-07-08 13:55:55 +03:00
|
|
|
(ns', btm) = bindNotReq fc (1 + i) env p ns tmptm in
|
|
|
|
(ns', refToLocal (MN "arg" i) _ btm)
|
2019-10-26 00:24:25 +03:00
|
|
|
bindNotReq {vs = n :: _} fc i (b :: env) (DropCons p) ns tm
|
2019-07-08 13:55:55 +03:00
|
|
|
= bindNotReq fc i env p ((plicit b, n) :: ns)
|
2019-05-29 13:57:07 +03:00
|
|
|
(Bind fc _ (Pi (multiplicity b) Explicit (binderType b)) tm)
|
|
|
|
|
2019-07-09 00:05:04 +03:00
|
|
|
bindReq : {vs : _} ->
|
2019-10-26 00:24:25 +03:00
|
|
|
FC -> Env Term vs -> (sub : SubVars pre vs) ->
|
2019-07-08 13:55:55 +03:00
|
|
|
List (PiInfo, Name) ->
|
2019-07-09 00:05:04 +03:00
|
|
|
Term pre -> Maybe (List (PiInfo, Name), List Name, ClosedTerm)
|
2019-10-26 00:24:25 +03:00
|
|
|
bindReq {vs} fc env SubRefl ns tm
|
2019-07-09 17:51:54 +03:00
|
|
|
= pure (ns, notLets [] _ env, abstractEnvType fc env tm)
|
|
|
|
where
|
|
|
|
notLets : List Name -> (vars : List Name) -> Env Term vars -> List Name
|
|
|
|
notLets acc [] _ = acc
|
|
|
|
notLets acc (v :: vs) (Let _ _ _ :: env) = notLets acc vs env
|
|
|
|
notLets acc (v :: vs) (_ :: env) = notLets (v :: acc) vs env
|
2019-10-26 00:24:25 +03:00
|
|
|
bindReq {vs = n :: _} fc (b :: env) (KeepCons p) ns tm
|
2019-07-09 00:05:04 +03:00
|
|
|
= do b' <- shrinkBinder b p
|
|
|
|
bindReq fc env p ((plicit b, n) :: ns)
|
|
|
|
(Bind fc _ (Pi (multiplicity b) Explicit (binderType b')) tm)
|
2019-10-26 00:24:25 +03:00
|
|
|
bindReq fc (b :: env) (DropCons p) ns tm
|
2019-07-08 13:55:55 +03:00
|
|
|
= bindReq fc env p ns tm
|
2019-05-29 13:57:07 +03:00
|
|
|
|
2019-06-02 23:21:07 +03:00
|
|
|
-- Return whether any of the pattern variables are in a trivially empty
|
|
|
|
-- type, where trivally empty means one of:
|
|
|
|
-- * No constructors
|
2019-10-26 00:24:25 +03:00
|
|
|
-- * Every constructor of the family has a return type which conflicts with
|
2019-06-02 23:21:07 +03:00
|
|
|
-- the given constructor's type
|
|
|
|
hasEmptyPat : Defs -> Env Term vars -> Term vars -> Core Bool
|
2019-07-08 13:55:55 +03:00
|
|
|
hasEmptyPat defs env (Bind fc x (PVar c p ty) sc)
|
2019-10-26 00:24:25 +03:00
|
|
|
= pure $ !(isEmpty defs !(nf defs env ty))
|
2019-07-08 13:55:55 +03:00
|
|
|
|| !(hasEmptyPat defs (PVar c p ty :: env) sc)
|
2019-06-02 23:21:07 +03:00
|
|
|
hasEmptyPat defs env _ = pure False
|
2019-10-26 00:24:25 +03:00
|
|
|
|
2019-07-09 00:05:04 +03:00
|
|
|
-- For checking with blocks as nested names
|
|
|
|
applyEnv : {auto c : Ref Ctxt Defs} ->
|
2019-10-26 00:24:25 +03:00
|
|
|
Env Term vars -> Name ->
|
2020-02-01 22:51:56 +03:00
|
|
|
Core (Name, (Maybe Name, Nat, FC -> NameType -> Term vars))
|
2019-07-09 00:05:04 +03:00
|
|
|
applyEnv env withname
|
|
|
|
= do n' <- resolveName withname
|
2020-02-01 22:51:56 +03:00
|
|
|
pure (withname, (Just withname, lengthNoLet env,
|
2019-10-26 00:24:25 +03:00
|
|
|
\fc, nt => applyTo fc
|
2019-07-09 00:05:04 +03:00
|
|
|
(Ref fc nt (Resolved n')) env))
|
2019-06-02 23:21:07 +03:00
|
|
|
|
2019-05-29 13:57:07 +03:00
|
|
|
-- Check a pattern clause, returning the component of the 'Case' expression it
|
|
|
|
-- represents, or Nothing if it's an impossible clause
|
|
|
|
export
|
|
|
|
checkClause : {vars : _} ->
|
|
|
|
{auto c : Ref Ctxt Defs} ->
|
2019-05-31 07:52:54 +03:00
|
|
|
{auto m : Ref MD Metadata} ->
|
2019-05-29 13:57:07 +03:00
|
|
|
{auto u : Ref UST UState} ->
|
|
|
|
(mult : RigCount) -> (hashit : Bool) ->
|
|
|
|
Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
|
2020-02-24 00:40:23 +03:00
|
|
|
ImpClause -> Core (Either RawImp Clause)
|
2019-05-29 13:57:07 +03:00
|
|
|
checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
|
2020-01-12 23:06:02 +03:00
|
|
|
= do lhs_raw <- lhsInCurrentNS nest lhs
|
|
|
|
handleUnify
|
2020-01-27 20:31:53 +03:00
|
|
|
(do autoimp <- isUnboundImplicits
|
|
|
|
setUnboundImplicits True
|
2020-01-12 23:06:02 +03:00
|
|
|
(_, lhs) <- bindNames False lhs_raw
|
2020-01-27 20:31:53 +03:00
|
|
|
setUnboundImplicits autoimp
|
2020-01-12 23:06:02 +03:00
|
|
|
|
|
|
|
log 5 $ "Checking " ++ show lhs
|
|
|
|
logEnv 5 "In env" env
|
|
|
|
(lhstm, lhstyg) <-
|
|
|
|
elabTerm n (InLHS mult) opts nest env
|
|
|
|
(IBindHere fc PATTERN lhs) Nothing
|
|
|
|
defs <- get Ctxt
|
|
|
|
lhs <- normaliseHoles defs env lhstm
|
|
|
|
if !(hasEmptyPat defs env lhs)
|
2020-02-24 00:40:23 +03:00
|
|
|
then pure (Left lhs_raw)
|
2020-01-12 23:06:02 +03:00
|
|
|
else throw (ValidCase fc env (Left lhs)))
|
|
|
|
(\err =>
|
|
|
|
case err of
|
|
|
|
ValidCase _ _ _ => throw err
|
|
|
|
_ => do defs <- get Ctxt
|
|
|
|
if !(impossibleErrOK defs err)
|
2020-02-24 00:40:23 +03:00
|
|
|
then pure (Left lhs_raw)
|
2020-01-12 23:06:02 +03:00
|
|
|
else throw (ValidCase fc env (Right err)))
|
2019-05-29 13:57:07 +03:00
|
|
|
checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
|
2019-10-26 00:24:25 +03:00
|
|
|
= do (_, (vars' ** (sub', env', nest', lhstm', lhsty'))) <-
|
2019-05-29 13:57:07 +03:00
|
|
|
checkLHS mult hashit n opts nest env fc lhs_in
|
2019-05-27 01:51:20 +03:00
|
|
|
let rhsMode = case mult of
|
|
|
|
Rig0 => InType
|
|
|
|
_ => InExpr
|
2019-06-14 20:35:31 +03:00
|
|
|
log 5 $ "Checking RHS " ++ show rhs
|
2020-02-09 16:46:58 +03:00
|
|
|
logEnv 5 "In env" env'
|
|
|
|
|
2019-06-25 23:46:28 +03:00
|
|
|
rhstm <- wrapError (InRHS fc !(getFullName (Resolved n))) $
|
|
|
|
checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
|
2019-05-31 13:42:11 +03:00
|
|
|
clearHoleLHS
|
2019-04-19 18:06:26 +03:00
|
|
|
|
2020-02-09 16:46:58 +03:00
|
|
|
logTerm 3 "RHS term" rhstm
|
2019-10-26 00:24:25 +03:00
|
|
|
when hashit $
|
2019-05-31 13:42:11 +03:00
|
|
|
do addHash lhstm'
|
|
|
|
addHash rhstm
|
|
|
|
|
2019-10-26 00:24:25 +03:00
|
|
|
-- If the rhs is a hole, record the lhs in the metadata because we
|
2019-05-31 13:42:11 +03:00
|
|
|
-- might want to split it interactively
|
|
|
|
case rhstm of
|
2019-10-26 00:24:25 +03:00
|
|
|
Meta _ _ _ _ =>
|
2019-05-31 13:42:11 +03:00
|
|
|
addLHS (getFC lhs_in) (length env) env' lhstm'
|
|
|
|
_ => pure ()
|
|
|
|
|
2020-01-12 23:06:02 +03:00
|
|
|
pure (Right (MkClause env' lhstm' rhstm))
|
2019-07-09 00:05:04 +03:00
|
|
|
-- TODO: (to decide) With is complicated. Move this into its own module?
|
2019-05-29 13:57:07 +03:00
|
|
|
checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs)
|
2019-10-26 00:24:25 +03:00
|
|
|
= do (lhs, (vars' ** (sub', env', nest', lhspat, reqty))) <-
|
2019-05-29 13:57:07 +03:00
|
|
|
checkLHS mult hashit n opts nest env fc lhs_in
|
|
|
|
let wmode
|
|
|
|
= case mult of
|
|
|
|
Rig0 => InType -- treat as used in type only
|
|
|
|
_ => InExpr
|
|
|
|
|
2019-06-24 02:12:58 +03:00
|
|
|
(wval, gwvalTy) <- wrapError (InRHS fc !(getFullName (Resolved n))) $
|
2019-05-29 13:57:07 +03:00
|
|
|
elabTermSub n wmode opts nest' env' env sub' wval_raw Nothing
|
2019-05-31 13:42:11 +03:00
|
|
|
clearHoleLHS
|
2019-10-26 00:24:25 +03:00
|
|
|
|
2019-05-29 13:57:07 +03:00
|
|
|
logTerm 5 "With value" wval
|
2019-07-09 00:05:04 +03:00
|
|
|
logTerm 3 "Required type" reqty
|
2019-05-29 13:57:07 +03:00
|
|
|
wvalTy <- getTerm gwvalTy
|
|
|
|
defs <- get Ctxt
|
|
|
|
wval <- normaliseHoles defs env' wval
|
|
|
|
wvalTy <- normaliseHoles defs env' wvalTy
|
|
|
|
|
|
|
|
let (wevars ** withSub) = keepOldEnv sub' (snd (findSubEnv env' wval))
|
|
|
|
logTerm 5 "With value type" wvalTy
|
|
|
|
log 5 $ "Using vars " ++ show wevars
|
|
|
|
|
|
|
|
let Just wval = shrinkTerm wval withSub
|
|
|
|
| Nothing => throw (InternalError "Impossible happened: With abstraction failure #1")
|
|
|
|
let Just wvalTy = shrinkTerm wvalTy withSub
|
|
|
|
| Nothing => throw (InternalError "Impossible happened: With abstraction failure #2")
|
2019-05-31 07:52:54 +03:00
|
|
|
-- Should the env be normalised too? If the following 'impossible'
|
|
|
|
-- error is ever thrown, that might be the cause!
|
2019-05-29 13:57:07 +03:00
|
|
|
let Just wvalEnv = shrinkEnv env' withSub
|
|
|
|
| Nothing => throw (InternalError "Impossible happened: With abstraction failure #3")
|
|
|
|
|
|
|
|
-- Abstracting over 'wval' in the scope of bNotReq in order
|
|
|
|
-- to get the 'magic with' behaviour
|
|
|
|
let wargn = MN "warg" 0
|
|
|
|
let scenv = Pi RigW Explicit wvalTy :: wvalEnv
|
|
|
|
|
2019-07-08 13:55:55 +03:00
|
|
|
let bnr = bindNotReq fc 0 env' withSub [] reqty
|
|
|
|
let notreqns = fst bnr
|
|
|
|
let notreqty = snd bnr
|
|
|
|
|
2019-05-29 13:57:07 +03:00
|
|
|
wtyScope <- replace defs scenv !(nf defs scenv (weaken wval))
|
2019-06-24 01:12:27 +03:00
|
|
|
(Local fc (Just False) _ First)
|
2019-10-26 00:24:25 +03:00
|
|
|
!(nf defs scenv
|
2019-07-08 13:55:55 +03:00
|
|
|
(weaken {n=wargn} notreqty))
|
2019-05-29 13:57:07 +03:00
|
|
|
let bNotReq = Bind fc wargn (Pi RigW Explicit wvalTy) wtyScope
|
|
|
|
|
2019-07-09 00:05:04 +03:00
|
|
|
let Just (reqns, envns, wtype) = bindReq fc env' withSub [] bNotReq
|
2019-05-29 13:57:07 +03:00
|
|
|
| Nothing => throw (InternalError "Impossible happened: With abstraction failure #4")
|
|
|
|
|
|
|
|
-- list of argument names - 'Just' means we need to match the name
|
|
|
|
-- in the with clauses to find out what the pattern should be.
|
|
|
|
-- 'Nothing' means it's the with pattern (so wargn)
|
2019-10-26 00:24:25 +03:00
|
|
|
let wargNames
|
|
|
|
= map Just reqns ++
|
2019-07-08 13:55:55 +03:00
|
|
|
Nothing :: map Just notreqns
|
2019-05-29 13:57:07 +03:00
|
|
|
|
2019-10-26 00:24:25 +03:00
|
|
|
logTerm 3 "With function type" wtype
|
2019-05-29 13:57:07 +03:00
|
|
|
log 5 $ "Argument names " ++ show wargNames
|
|
|
|
|
|
|
|
wname <- genWithName n
|
2019-06-01 17:05:04 +03:00
|
|
|
widx <- addDef wname (newDef fc wname mult vars wtype Private None)
|
2019-05-29 13:57:07 +03:00
|
|
|
let rhs_in = apply (IVar fc wname)
|
2019-07-09 00:05:04 +03:00
|
|
|
(map (IVar fc) envns ++
|
|
|
|
map (maybe wval_raw (\pn => IVar fc (snd pn))) wargNames)
|
2019-05-29 13:57:07 +03:00
|
|
|
|
2019-07-09 00:05:04 +03:00
|
|
|
log 3 $ "Applying to with argument " ++ show rhs_in
|
2019-06-24 02:12:58 +03:00
|
|
|
rhs <- wrapError (InRHS fc !(getFullName (Resolved n))) $
|
2019-10-26 00:24:25 +03:00
|
|
|
checkTermSub n wmode opts nest' env' env sub' rhs_in
|
2019-05-29 13:57:07 +03:00
|
|
|
(gnf env' reqty)
|
|
|
|
|
|
|
|
-- Generate new clauses by rewriting the matched arguments
|
2019-07-30 14:32:33 +03:00
|
|
|
cs' <- traverse (mkClauseWith 1 wname wargNames lhs) cs
|
2019-07-09 00:05:04 +03:00
|
|
|
log 3 $ "With clauses: " ++ show cs'
|
2019-05-29 13:57:07 +03:00
|
|
|
|
|
|
|
-- Elaborate the new definition here
|
2019-07-09 00:05:04 +03:00
|
|
|
nestname <- applyEnv env wname
|
|
|
|
let nest'' = record { names $= (nestname ::) } nest
|
|
|
|
|
2019-05-29 13:57:07 +03:00
|
|
|
let wdef = IDef fc wname cs'
|
2019-07-09 00:05:04 +03:00
|
|
|
processDecl [] nest'' env wdef
|
2019-05-29 13:57:07 +03:00
|
|
|
|
2020-01-12 23:06:02 +03:00
|
|
|
pure (Right (MkClause env' lhspat rhs))
|
2019-05-29 13:57:07 +03:00
|
|
|
where
|
|
|
|
-- If it's 'KeepCons/SubRefl' in 'outprf', that means it was in the outer
|
|
|
|
-- environment so we need to keep it in the same place in the 'with'
|
|
|
|
-- function. Hence, turn it to KeepCons whatever
|
|
|
|
keepOldEnv : (outprf : SubVars outer vs) -> SubVars vs' vs ->
|
|
|
|
(vs'' : List Name ** SubVars vs'' vs)
|
|
|
|
keepOldEnv {vs} SubRefl p = (vs ** SubRefl)
|
|
|
|
keepOldEnv {vs} p SubRefl = (vs ** SubRefl)
|
|
|
|
keepOldEnv (DropCons p) (DropCons p')
|
|
|
|
= let (_ ** rest) = keepOldEnv p p' in
|
|
|
|
(_ ** DropCons rest)
|
|
|
|
keepOldEnv (DropCons p) (KeepCons p')
|
|
|
|
= let (_ ** rest) = keepOldEnv p p' in
|
|
|
|
(_ ** KeepCons rest)
|
|
|
|
keepOldEnv (KeepCons p) (DropCons p')
|
|
|
|
= let (_ ** rest) = keepOldEnv p p' in
|
|
|
|
(_ ** KeepCons rest)
|
|
|
|
keepOldEnv (KeepCons p) (KeepCons p')
|
|
|
|
= let (_ ** rest) = keepOldEnv p p' in
|
|
|
|
(_ ** KeepCons rest)
|
2019-10-26 00:24:25 +03:00
|
|
|
|
2019-05-29 13:57:07 +03:00
|
|
|
-- Rewrite the clauses in the block to use an updated LHS.
|
|
|
|
-- 'drop' is the number of additional with arguments we expect (i.e.
|
|
|
|
-- the things to drop from the end before matching LHSs)
|
2019-07-08 13:55:55 +03:00
|
|
|
mkClauseWith : (drop : Nat) -> Name -> List (Maybe (PiInfo, Name)) ->
|
2019-10-26 00:24:25 +03:00
|
|
|
RawImp -> ImpClause ->
|
2019-05-29 13:57:07 +03:00
|
|
|
Core ImpClause
|
|
|
|
mkClauseWith drop wname wargnames lhs (PatClause ploc patlhs rhs)
|
2019-07-30 14:32:33 +03:00
|
|
|
= do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
|
2019-07-07 02:07:59 +03:00
|
|
|
newrhs <- withRHS ploc drop wname wargnames rhs lhs
|
|
|
|
pure (PatClause ploc newlhs newrhs)
|
2019-05-29 13:57:07 +03:00
|
|
|
mkClauseWith drop wname wargnames lhs (WithClause ploc patlhs rhs ws)
|
2019-07-30 14:32:33 +03:00
|
|
|
= do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
|
2019-07-07 02:07:59 +03:00
|
|
|
newrhs <- withRHS ploc drop wname wargnames rhs lhs
|
2019-05-29 13:57:07 +03:00
|
|
|
ws' <- traverse (mkClauseWith (S drop) wname wargnames lhs) ws
|
2019-07-07 02:07:59 +03:00
|
|
|
pure (WithClause ploc newlhs newrhs ws')
|
2019-05-29 13:57:07 +03:00
|
|
|
mkClauseWith drop wname wargnames lhs (ImpossibleClause ploc patlhs)
|
2019-07-30 14:32:33 +03:00
|
|
|
= do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
|
2019-05-29 13:57:07 +03:00
|
|
|
pure (ImpossibleClause ploc newlhs)
|
|
|
|
|
2019-05-19 22:24:14 +03:00
|
|
|
|
|
|
|
nameListEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys)
|
|
|
|
nameListEq [] [] = Just Refl
|
|
|
|
nameListEq (x :: xs) (y :: ys) with (nameEq x y)
|
|
|
|
nameListEq (x :: xs) (x :: ys) | (Just Refl) with (nameListEq xs ys)
|
|
|
|
nameListEq (x :: xs) (x :: xs) | (Just Refl) | Just Refl= Just Refl
|
|
|
|
nameListEq (x :: xs) (x :: ys) | (Just Refl) | Nothing = Nothing
|
|
|
|
nameListEq (x :: xs) (y :: ys) | Nothing = Nothing
|
|
|
|
nameListEq _ _ = Nothing
|
2019-04-18 16:51:04 +03:00
|
|
|
|
2019-06-14 20:35:31 +03:00
|
|
|
-- Compile run time case trees for the given name
|
|
|
|
mkRunTime : {auto c : Ref Ctxt Defs} ->
|
|
|
|
{auto u : Ref UST UState} ->
|
|
|
|
Name -> Core ()
|
|
|
|
mkRunTime n
|
|
|
|
= do defs <- get Ctxt
|
|
|
|
Just gdef <- lookupCtxtExact n (gamma defs)
|
|
|
|
| _ => pure ()
|
2019-07-01 18:50:11 +03:00
|
|
|
let PMDef r cargs tree_ct _ pats = definition gdef
|
2019-06-14 20:35:31 +03:00
|
|
|
| _ => pure () -- not a function definition
|
|
|
|
let ty = type gdef
|
2019-10-26 00:24:25 +03:00
|
|
|
(rargs ** tree_rt) <- getPMDef (location gdef) RunTime n ty
|
2019-06-14 20:35:31 +03:00
|
|
|
!(traverse (toClause (location gdef)) pats)
|
|
|
|
let Just Refl = nameListEq cargs rargs
|
|
|
|
| Nothing => throw (InternalError "WAT")
|
2019-10-26 00:24:25 +03:00
|
|
|
addDef n (record { definition = PMDef r cargs tree_ct tree_rt pats
|
2019-06-14 20:35:31 +03:00
|
|
|
} gdef)
|
|
|
|
pure ()
|
|
|
|
where
|
|
|
|
toClause : FC -> (vars ** (Env Term vars, Term vars, Term vars)) ->
|
|
|
|
Core Clause
|
2019-10-26 00:24:25 +03:00
|
|
|
toClause fc (_ ** (env, lhs, rhs))
|
2019-06-14 20:35:31 +03:00
|
|
|
= do rhs_erased <- linearCheck fc Rig1 True env rhs
|
|
|
|
pure $ MkClause env lhs rhs_erased
|
|
|
|
|
|
|
|
compileRunTime : {auto c : Ref Ctxt Defs} ->
|
|
|
|
{auto u : Ref UST UState} ->
|
|
|
|
Core ()
|
|
|
|
compileRunTime
|
|
|
|
= do defs <- get Ctxt
|
|
|
|
traverse_ mkRunTime (toCompile defs)
|
|
|
|
defs <- get Ctxt
|
|
|
|
put Ctxt (record { toCompile = [] } defs)
|
|
|
|
|
2019-06-27 11:01:59 +03:00
|
|
|
-- Calculate references for the given name, and recursively if they haven't
|
|
|
|
-- been calculated already
|
|
|
|
calcRefs : {auto c : Ref Ctxt Defs} ->
|
|
|
|
(aTotal : Name) -> (fn : Name) -> Core ()
|
|
|
|
calcRefs at fn
|
|
|
|
= do defs <- get Ctxt
|
|
|
|
Just gdef <- lookupCtxtExact fn (gamma defs)
|
|
|
|
| _ => pure ()
|
2019-07-01 18:50:11 +03:00
|
|
|
let PMDef r cargs tree_ct _ pats = definition gdef
|
2019-06-27 11:01:59 +03:00
|
|
|
| _ => pure () -- not a function definition
|
|
|
|
let Nothing = refersToM gdef
|
|
|
|
| Just _ => pure () -- already done
|
|
|
|
let metas = getMetas tree_ct
|
2019-06-30 14:49:11 +03:00
|
|
|
traverse_ addToSave (keys metas)
|
2019-08-06 15:19:30 +03:00
|
|
|
let refs = addRefs at metas tree_ct
|
2019-06-30 14:49:11 +03:00
|
|
|
|
|
|
|
logC 5 (do fulln <- getFullName fn
|
|
|
|
refns <- traverse getFullName (keys refs)
|
|
|
|
pure (show fulln ++ " refers to " ++ show refns))
|
2019-06-27 11:01:59 +03:00
|
|
|
addDef fn (record { refersToM = Just refs } gdef)
|
|
|
|
traverse_ (calcRefs at) (keys refs)
|
|
|
|
|
2019-04-20 18:54:09 +03:00
|
|
|
toPats : Clause -> (vs ** (Env Term vs, Term vs, Term vs))
|
2019-10-26 00:24:25 +03:00
|
|
|
toPats (MkClause {vars} env lhs rhs)
|
2019-04-20 18:54:09 +03:00
|
|
|
= (_ ** (env, lhs, rhs))
|
|
|
|
|
2019-04-06 15:53:59 +03:00
|
|
|
export
|
|
|
|
processDef : {auto c : Ref Ctxt Defs} ->
|
2019-05-31 07:52:54 +03:00
|
|
|
{auto m : Ref MD Metadata} ->
|
2019-04-06 15:53:59 +03:00
|
|
|
{auto u : Ref UST UState} ->
|
2019-05-18 21:08:43 +03:00
|
|
|
List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
|
2019-04-18 16:51:04 +03:00
|
|
|
Name -> List ImpClause -> Core ()
|
2019-06-03 01:43:21 +03:00
|
|
|
processDef opts nest env fc n_in cs_in
|
2019-04-06 15:53:59 +03:00
|
|
|
= do n <- inCurrentNS n_in
|
|
|
|
defs <- get Ctxt
|
|
|
|
Just gdef <- lookupCtxtExact n (gamma defs)
|
|
|
|
| Nothing => throw (NoDeclaration fc n)
|
2019-04-18 16:51:04 +03:00
|
|
|
let None = definition gdef
|
|
|
|
| _ => throw (AlreadyDefined fc n)
|
|
|
|
let ty = type gdef
|
|
|
|
let hashit = visibility gdef == Public
|
|
|
|
let mult = if multiplicity gdef == Rig0
|
|
|
|
then Rig0
|
|
|
|
else Rig1
|
2019-05-11 15:00:12 +03:00
|
|
|
nidx <- resolveName n
|
2019-05-18 21:08:43 +03:00
|
|
|
cs <- traverse (checkClause mult hashit nidx opts nest env) cs_in
|
2020-01-12 23:06:02 +03:00
|
|
|
let pats = map toPats (rights cs)
|
2019-05-19 22:24:14 +03:00
|
|
|
|
2020-01-12 23:06:02 +03:00
|
|
|
(cargs ** tree_ct) <- getPMDef fc CompileTime n ty (rights cs)
|
2019-10-26 00:24:25 +03:00
|
|
|
|
2020-02-09 16:46:58 +03:00
|
|
|
logC 2 (do t <- toFullNames tree_ct
|
2019-06-23 22:36:06 +03:00
|
|
|
pure ("Case tree for " ++ show n ++ ": " ++ show t))
|
2019-06-15 20:28:41 +03:00
|
|
|
|
2019-06-14 20:35:31 +03:00
|
|
|
-- Add compile time tree as a placeholder for the runtime tree,
|
|
|
|
-- but we'll rebuild that in a later pass once all the case
|
|
|
|
-- blocks etc are resolved
|
2019-06-27 11:01:59 +03:00
|
|
|
addDef (Resolved nidx)
|
2020-02-22 18:04:35 +03:00
|
|
|
(record { definition = PMDef defaultPI cargs tree_ct tree_ct pats
|
2019-06-27 11:01:59 +03:00
|
|
|
} gdef)
|
2019-06-15 20:28:41 +03:00
|
|
|
|
2019-06-27 11:01:59 +03:00
|
|
|
let rmetas = getMetas tree_ct
|
2019-06-15 20:28:41 +03:00
|
|
|
traverse_ addToSave (keys rmetas)
|
2019-06-28 14:43:55 +03:00
|
|
|
let tymetas = getMetas (type gdef)
|
|
|
|
traverse_ addToSave (keys tymetas)
|
2019-06-15 20:28:41 +03:00
|
|
|
addToSave n
|
2019-06-16 15:47:20 +03:00
|
|
|
log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys rmetas)
|
2019-06-03 01:43:21 +03:00
|
|
|
|
2019-06-14 20:35:31 +03:00
|
|
|
-- Flag this name as one which needs compiling
|
|
|
|
defs <- get Ctxt
|
|
|
|
put Ctxt (record { toCompile $= (n ::) } defs)
|
|
|
|
|
2019-06-27 11:01:59 +03:00
|
|
|
when (not (InCase `elem` opts)) $
|
|
|
|
do atotal <- toResolvedNames (NS ["Builtin"] (UN "assert_total"))
|
|
|
|
calcRefs atotal (Resolved nidx)
|
|
|
|
|
|
|
|
sc <- calculateSizeChange fc n
|
|
|
|
setSizeChange fc n sc
|
|
|
|
|
2019-09-22 16:19:24 +03:00
|
|
|
md <- get MD -- don't need the metadata collected on the coverage check
|
2020-01-12 23:06:02 +03:00
|
|
|
cov <- checkCoverage nidx ty mult cs
|
2019-06-27 11:01:59 +03:00
|
|
|
setCovering fc n cov
|
2019-09-22 16:19:24 +03:00
|
|
|
put MD md
|
2019-06-27 11:01:59 +03:00
|
|
|
|
2020-01-12 23:06:02 +03:00
|
|
|
-- If we're not in a case tree, compile all the outstanding case
|
|
|
|
-- trees. TODO: Take into account coverage, and add error cases
|
|
|
|
-- if we're not covering.
|
|
|
|
when (not (elem InCase opts)) $
|
|
|
|
compileRunTime
|
|
|
|
|
2019-06-03 01:43:21 +03:00
|
|
|
where
|
|
|
|
simplePat : Term vars -> Bool
|
|
|
|
simplePat (Local _ _ _ _) = True
|
2020-01-12 23:06:02 +03:00
|
|
|
simplePat (Erased _ _) = True
|
2020-02-09 16:46:58 +03:00
|
|
|
simplePat (As _ _ _ p) = simplePat p
|
2019-06-03 01:43:21 +03:00
|
|
|
simplePat _ = False
|
|
|
|
|
|
|
|
-- Is the clause returned from 'checkClause' a catch all clause, i.e.
|
|
|
|
-- one where all the arguments are variables? If so, no need to do the
|
|
|
|
-- (potentially expensive) coverage check
|
2020-01-12 23:06:02 +03:00
|
|
|
catchAll : Clause -> Bool
|
|
|
|
catchAll (MkClause env lhs _)
|
2019-06-13 21:33:10 +03:00
|
|
|
= all simplePat (getArgs lhs)
|
2019-10-26 00:24:25 +03:00
|
|
|
|
2019-06-03 01:43:21 +03:00
|
|
|
-- Return 'Nothing' if the clause is impossible, otherwise return the
|
|
|
|
-- original
|
2019-10-26 00:24:25 +03:00
|
|
|
checkImpossible : Int -> RigCount -> ClosedTerm ->
|
2019-06-03 01:43:21 +03:00
|
|
|
Core (Maybe ClosedTerm)
|
|
|
|
checkImpossible n mult tm
|
|
|
|
= do itm <- unelabNoPatvars [] tm
|
|
|
|
handleUnify
|
|
|
|
(do ctxt <- get Ctxt
|
|
|
|
log 3 $ "Checking for impossibility: " ++ show itm
|
|
|
|
ok <- checkClause mult False n [] (MkNested []) []
|
|
|
|
(ImpossibleClause fc itm)
|
|
|
|
put Ctxt ctxt
|
2020-01-12 23:06:02 +03:00
|
|
|
either (\e => pure Nothing)
|
|
|
|
(\chktm => pure (Just tm)) ok)
|
2019-06-03 01:43:21 +03:00
|
|
|
(\err => case err of
|
|
|
|
WhenUnifying _ env l r err
|
|
|
|
=> do defs <- get Ctxt
|
2019-10-26 00:24:25 +03:00
|
|
|
if !(impossibleOK defs !(nf defs env l)
|
2019-06-03 01:43:21 +03:00
|
|
|
!(nf defs env r))
|
|
|
|
then pure Nothing
|
|
|
|
else pure (Just tm)
|
|
|
|
_ => pure (Just tm))
|
|
|
|
|
2020-02-24 00:40:23 +03:00
|
|
|
getClause : {auto c : Ref Ctxt Defs} ->
|
|
|
|
Either RawImp Clause -> Core (Maybe Clause)
|
|
|
|
getClause (Left rawlhs)
|
|
|
|
= catch (do lhsp <- getImpossibleTerm rawlhs
|
|
|
|
log 3 $ "Generated impossible LHS: " ++ show lhsp
|
|
|
|
pure $ Just $ MkClause [] lhsp (Erased (getFC rawlhs) True))
|
|
|
|
(\e => pure Nothing)
|
|
|
|
getClause (Right c) = pure (Just c)
|
|
|
|
|
2020-01-12 23:06:02 +03:00
|
|
|
checkCoverage : Int -> ClosedTerm -> RigCount ->
|
2020-02-24 00:40:23 +03:00
|
|
|
List (Either RawImp Clause) ->
|
2020-01-12 23:06:02 +03:00
|
|
|
Core Covering
|
|
|
|
checkCoverage n ty mult cs
|
2020-02-24 00:40:23 +03:00
|
|
|
= do covcs' <- traverse getClause cs -- Make stand in LHS for impossible clauses
|
|
|
|
let covcs = mapMaybe id covcs'
|
2020-01-12 23:06:02 +03:00
|
|
|
(_ ** ctree) <- getPMDef fc CompileTime (Resolved n) ty covcs
|
|
|
|
missCase <- if any catchAll covcs
|
2019-06-03 01:43:21 +03:00
|
|
|
then do log 3 $ "Catch all case in " ++ show n
|
|
|
|
pure []
|
|
|
|
else getMissing fc (Resolved n) ctree
|
2019-06-23 22:36:06 +03:00
|
|
|
logC 3 (do mc <- traverse toFullNames missCase
|
2019-10-26 00:24:25 +03:00
|
|
|
pure ("Initially missing in " ++
|
|
|
|
show !(getFullName (Resolved n)) ++ ":\n" ++
|
2019-06-23 22:36:06 +03:00
|
|
|
showSep "\n" (map show mc)))
|
2019-06-03 01:43:21 +03:00
|
|
|
missImp <- traverse (checkImpossible n mult) missCase
|
|
|
|
let miss = mapMaybe id missImp
|
|
|
|
if isNil miss
|
|
|
|
then do [] <- getNonCoveringRefs fc (Resolved n)
|
2019-06-25 14:57:49 +03:00
|
|
|
| ns => toFullNames (NonCoveringCall ns)
|
2019-06-03 01:43:21 +03:00
|
|
|
pure IsCovering
|
|
|
|
else pure (MissingCases miss)
|
|
|
|
|