idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-29 14:44:03 +03:00
Code Issues Projects Releases Wiki Activity

Use Closures instead of NF in binders for normal forms (#1823)

Browse Source 
* Skip forced arguments in conversion check

This isn't always safe - we have to have also checked the type of the
things we're converting - but in the place where it is safe it can be a
pretty significant saving.

* Use Closures, not NF, in Binders for normal forms

This means we don't need to reduce argument types during unification if
we don't need to. Also, we now try to avoid reducing closures during
unification if they are unified with a metavariable. Together, this
saves a huge amount of unnecessary evaluation in programs that do a lot
of compile time evaluation.

* Didn't mean to update idris2api.ipkg

* Fix dodgy merge
This commit is contained in:
Edwin Brady 2021-08-08 17:05:29 +01:00 committed by GitHub
parent cd86340311
commit 170af1e87a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
23 changed files with 222 additions and 114 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
CHANGELOG.md
View File

@ -32,11 +32,18 @@
and reverts to whole program compilation. Incremental compilation is currently
supported only by the Chez Scheme back end.
This is currently supported only on Unix-like platforms (not yet Windows)
* The type checker now tries a lot harder to avoid reducing expressions where
it is not needed. This gives a huge performance improvement in programs
that potentially do a lot of compile time evaluation. However, sometimes
reducing expressions can help in totality and quantity checking, so this may
cause some programs not to type check which previously did - in these cases,
you will need to give the reduced expressions explicitly.
### Library Changes
#### Prelude
Changed
- Removed `Data.Strings`. Use `Data.String` instead.

6
src/Compiler/CompileExpr.idr
View File

@ -609,7 +609,7 @@ nfToCFType _ _ (NPrimVal _ CharType) = pure CFChar
nfToCFType _ _ (NPrimVal _ WorldType) = pure CFWorld
nfToCFType _ False (NBind fc _ (Pi _ _ _ ty) sc)
= do defs <- get Ctxt
sty <- nfToCFType fc False ty
sty <- nfToCFType fc False !(evalClosure defs ty)
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
tty <- nfToCFType fc False sc'
pure (CFFun sty tty)
@ -654,8 +654,8 @@ getCFTypes : {auto c : Ref Ctxt Defs} ->
List CFType -> NF [] ->
Core (List CFType, CFType)
getCFTypes args (NBind fc _ (Pi _ _ _ ty) sc)
= do aty <- nfToCFType fc False ty
defs <- get Ctxt
= do defs <- get Ctxt
aty <- nfToCFType fc False !(evalClosure defs ty)
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
getCFTypes (aty :: args) sc'
getCFTypes args t

2
src/Core/AutoSearch.idr
View File

@ -33,7 +33,7 @@ record ArgInfo (vars : List Name) where
constructor MkArgInfo
holeID : Int
argRig : RigCount
plicit : PiInfo (NF vars)
plicit : PiInfo (Closure vars)
metaApp : Term vars
argType : Term vars

22
src/Core/CaseBuilder.idr
View File

@ -434,12 +434,14 @@ nextNames {vars} fc root (p :: pats) fty
fa_tys <- the (Core (Maybe (NF vars), ArgType vars)) $
case fty of
Nothing => pure (Nothing, Unknown)
Just (NBind pfc _ (Pi _ _ _ (NErased _ _)) fsc) =>
pure (Just !(fsc defs (toClosure defaultOpts env (Ref pfc Bound n))),
Unknown)
Just (NBind pfc _ (Pi _ c _ farg) fsc) =>
pure (Just !(fsc defs (toClosure defaultOpts env (Ref pfc Bound n))),
Known c !(quote empty env farg))
Just (NBind pfc _ (Pi _ c _ fargc) fsc) =>
do farg <- evalClosure defs fargc
case farg of
NErased _ _ =>
pure (Just !(fsc defs (toClosure defaultOpts env (Ref pfc Bound n))),
Unknown)
_ => pure (Just !(fsc defs (toClosure defaultOpts env (Ref pfc Bound n))),
Known c !(quote empty env farg))
Just t =>
pure (Nothing, Stuck !(quote empty env t))
(args ** (l, ps)) <- nextNames {vars} fc root pats (fst fa_tys)
@ -506,8 +508,8 @@ groupCons fc fn pvars cs
-- the same name in each of the clauses
addConG {vars'} {todo'} n tag pargs pats pid rhs []
= do cty <- if n == UN "->"
then pure $ NBind fc (MN "_" 0) (Pi fc top Explicit (NType fc)) $
(\d, a => pure $ NBind fc (MN "_" 1) (Pi fc top Explicit (NErased fc False))
then pure $ NBind fc (MN "_" 0) (Pi fc top Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NType fc))) $
(\d, a => pure $ NBind fc (MN "_" 1) (Pi fc top Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NErased fc False)))
(\d, a => pure $ NType fc))
else do defs <- get Ctxt
Just t <- lookupTyExact n (gamma defs)
@ -554,10 +556,10 @@ groupCons fc fn pvars cs
(acc : List (Group vars' todo')) ->
Core (List (Group vars' todo'))
addDelayG {vars'} {todo'} pty parg pats pid rhs []
= do let dty = NBind fc (MN "a" 0) (Pi fc erased Explicit (NType fc)) $
= do let dty = NBind fc (MN "a" 0) (Pi fc erased Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NType fc))) $
(\d, a =>
do a' <- evalClosure d a
pure (NBind fc (MN "x" 0) (Pi fc top Explicit a')
pure (NBind fc (MN "x" 0) (Pi fc top Explicit a)
(\dv, av => pure (NDelayed fc LUnknown a'))))
([tyname, argname] ** (l, newargs)) <- nextNames {vars=vars'} fc "e" [pty, parg]
(Just dty)

2
src/Core/LinearCheck.idr
View File

@ -335,7 +335,7 @@ mutual
opts <- getSession
when (debugElabCheck opts) $ do
aty <- getNF gaty
when (not !(convert defs env aty ty)) $
when (not !(convert defs env aty !(evalClosure defs ty))) $
do ty' <- quote defs env ty
aty' <- quote defs env aty
throw (CantConvert fc env ty' aty')

93
src/Core/Normalise.idr
View File

@ -106,13 +106,13 @@ parameters (defs : Defs, topopts : EvalOpts)
= eval env (snd thunk :: locs) scope stk
eval env locs (Bind fc x b@(Let _ r val ty) scope) stk
= if (holesOnly topopts || argHolesOnly topopts) && not (tcInline topopts)
then do b' <- traverse (\tm => eval env locs tm []) b
then do let b' = map (MkClosure topopts locs env) b
pure $ NBind fc x b'
(\defs', arg => evalWithOpts defs' topopts
env (arg :: locs) scope stk)
else eval env (MkClosure topopts locs env val :: locs) scope stk
eval env locs (Bind fc x b scope) stk
= do b' <- traverse (\tm => eval env locs tm []) b
= do let b' = map (MkClosure topopts locs env) b
pure $ NBind fc x b'
(\defs', arg => evalWithOpts defs' topopts
env (arg :: locs) scope stk)
@ -154,18 +154,11 @@ parameters (defs : Defs, topopts : EvalOpts)
applyToStack env cont arg' stk
applyToStack env cont (NBind fc x b@(Let _ r val ty) sc) stk
= if (holesOnly topopts || argHolesOnly topopts) && not (tcInline topopts)
then do b' <- if cont
then traverse (\t => applyToStack env cont t []) b
else pure b
pure (NBind fc x b'
then pure (NBind fc x b
(\defs', arg => applyToStack env cont !(sc defs' arg) stk))
else do val' <- applyToStack env cont val []
applyToStack env cont !(sc defs (MkNFClosure topopts env val')) stk
else applyToStack env cont !(sc defs val) stk
applyToStack env cont (NBind fc x b sc) stk
= do b' <- if cont
then traverse (\t => applyToStack env cont t []) b
else pure b
pure (NBind fc x b'
= pure (NBind fc x b
(\defs', arg => applyToStack env cont !(sc defs' arg) stk))
applyToStack env cont (NApp fc (NRef nt fn) args) stk
= evalRef env False fc nt fn (args ++ stk)
@ -358,7 +351,7 @@ parameters (defs : Defs, topopts : EvalOpts)
tryAlt {more}
env loc opts fc stk (NBind pfc x (Pi fc' r e aty) scty) (ConCase (UN "->") tag [s,t] sc)
= evalConAlt {more} env loc opts fc stk [s,t]
[MkNFClosure opts env aty,
[aty,
MkNFClosure opts env (NBind pfc x (Lam fc' r e aty) scty)]
sc
-- Delay matching
@ -655,42 +648,42 @@ mutual
quotePi : {auto c : Ref Ctxt Defs} ->
{bound, free : _} ->
Ref QVar Int -> Defs -> Bounds bound ->
Env Term free -> PiInfo (NF free) ->
Env Term free -> PiInfo (Closure free) ->
Core (PiInfo (Term (bound ++ free)))
quotePi q defs bounds env Explicit = pure Explicit
quotePi q defs bounds env Implicit = pure Implicit
quotePi q defs bounds env AutoImplicit = pure AutoImplicit
quotePi q defs bounds env (DefImplicit t)
= do t' <- quoteGenNF q defs bounds env t
= do t' <- quoteGenNF q defs bounds env !(evalClosure defs t)
pure (DefImplicit t')
quoteBinder : {auto c : Ref Ctxt Defs} ->
{bound, free : _} ->
Ref QVar Int -> Defs -> Bounds bound ->
Env Term free -> Binder (NF free) ->
Env Term free -> Binder (Closure free) ->
Core (Binder (Term (bound ++ free)))
quoteBinder q defs bounds env (Lam fc r p ty)
= do ty' <- quoteGenNF q defs bounds env ty
= do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
p' <- quotePi q defs bounds env p
pure (Lam fc r p' ty')
quoteBinder q defs bounds env (Let fc r val ty)
= do val' <- quoteGenNF q defs bounds env val
ty' <- quoteGenNF q defs bounds env ty
= do val' <- quoteGenNF q defs bounds env !(evalClosure defs val)
ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
pure (Let fc r val' ty')
quoteBinder q defs bounds env (Pi fc r p ty)
= do ty' <- quoteGenNF q defs bounds env ty
= do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
p' <- quotePi q defs bounds env p
pure (Pi fc r p' ty')
quoteBinder q defs bounds env (PVar fc r p ty)
= do ty' <- quoteGenNF q defs bounds env ty
= do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
p' <- quotePi q defs bounds env p
pure (PVar fc r p' ty')
quoteBinder q defs bounds env (PLet fc r val ty)
= do val' <- quoteGenNF q defs bounds env val
ty' <- quoteGenNF q defs bounds env ty
= do val' <- quoteGenNF q defs bounds env !(evalClosure defs val)
ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
pure (PLet fc r val' ty')
quoteBinder q defs bounds env (PVTy fc r ty)
= do ty' <- quoteGenNF q defs bounds env ty
= do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
pure (PVTy fc r ty')
quoteGenNF : {auto c : Ref Ctxt Defs} ->
@ -758,6 +751,44 @@ export
Quote Closure where
quoteGen q defs env c = quoteGen q defs env !(evalClosure defs c)
quoteWithPiGen : {auto _ : Ref Ctxt Defs} ->
{bound, vars : _} ->
Ref QVar Int -> Defs -> Bounds bound ->
Env Term vars -> NF vars -> Core (Term (bound ++ vars))
quoteWithPiGen q defs bound env (NBind fc n (Pi bfc c p ty) sc)
= do var <- genName "qv"
empty <- clearDefs defs
sc' <- quoteWithPiGen q defs (Add n var bound) env
!(sc defs (toClosure defaultOpts env (Ref fc Bound var)))
ty' <- quoteGenNF q empty bound env !(evalClosure empty ty)
p' <- quotePi q empty bound env p
pure (Bind fc n (Pi bfc c p' ty') sc')
quoteWithPiGen q defs bound env tm
= do empty <- clearDefs defs
quoteGenNF q empty bound env tm
-- Quote back to a term, but only to find out how many Pi bindings there
-- are, don't reduce anything else
export
quoteWithPi : {auto c : Ref Ctxt Defs} ->
{vars : List Name} ->
Defs -> Env Term vars -> NF vars -> Core (Term vars)
quoteWithPi defs env tm
= do q <- newRef QVar 0
quoteWithPiGen q defs None env tm
-- Expand all the pi bindings at the start of a term, but otherwise don't
-- reduce
export
normalisePis : {auto c : Ref Ctxt Defs} ->
{vars : List Name} ->
Defs -> Env Term vars -> Term vars -> Core (Term vars)
normalisePis defs env tm
= do tmnf <- nf defs env tm
case tmnf of
NBind _ _ (Pi _ _ _ _) _ => quoteWithPi defs env tmnf
_ => pure tm
-- Resume a previously blocked normalisation with a new environment
export
continueNF : {auto c : Ref Ctxt Defs} ->
@ -776,6 +807,16 @@ glueBack defs env nf
quote empty env nf)
(const (pure nf))
export
glueClosure : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> Env Term vars -> Closure vars -> Glued vars
glueClosure defs env clos
= MkGlue False
(do empty <- clearDefs defs
quote empty env clos)
(const (evalClosure defs clos))
export
normalise : {auto c : Ref Ctxt Defs} ->
{free : _} ->
@ -1168,7 +1209,7 @@ mutual
convBinders : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Ref QVar Int -> Bool -> Defs -> Env Term vars ->
Binder (NF vars) -> Binder (NF vars) -> Core Bool
Binder (Closure vars) -> Binder (Closure vars) -> Core Bool
convBinders q i defs env (Pi _ cx ix tx) (Pi _ cy iy ty)
= if cx /= cy
then pure False
@ -1404,7 +1445,7 @@ replace' {vars} tmpi defs env lhs parg tm
repSub : NF vars -> Core (Term vars)
repSub (NBind fc x b scfn)
= do b' <- traverse repSub b
= do b' <- traverse (\c => repSub !(evalClosure defs c)) b
let x' = MN "tmp" tmpi
sc' <- replace' (tmpi + 1) defs env lhs parg
!(scfn defs (toClosure defaultOpts env (Ref fc Bound x')))

6
src/Core/Termination.idr
View File

@ -606,7 +606,7 @@ checkTerminating loc n
nameIn : {auto c : Ref Ctxt Defs} ->
Defs -> List Name -> NF [] -> Core Bool
nameIn defs tyns (NBind fc x b sc)
= if !(nameIn defs tyns (binderType b))
= if !(nameIn defs tyns !(evalClosure defs (binderType b)))
then pure True
else do let nm = Ref fc Bound (MN ("NAMEIN_" ++ show x) 0)
let arg = toClosure defaultOpts [] nm
@ -667,7 +667,7 @@ posArg defs tyns nf@(NTCon loc tc _ _ args) =
-- a tyn can not appear as part of ty
posArg defs tyns nf@(NBind fc x (Pi _ _ e ty) sc)
= do logNF "totality.positivity" 50 "Found a Pi-type" [] nf
if !(nameIn defs tyns ty)
if !(nameIn defs tyns !(evalClosure defs ty))
then pure (NotTerminating NotStrictlyPositive)
else do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 1)
let arg = toClosure defaultOpts [] nm
@ -686,7 +686,7 @@ posArg defs tyn nf
checkPosArgs : {auto c : Ref Ctxt Defs} ->
Defs -> List Name -> NF [] -> Core Terminating
checkPosArgs defs tyns (NBind fc x (Pi _ _ e ty) sc)
= case !(posArg defs tyns ty) of
= case !(posArg defs tyns !(evalClosure defs ty)) of
IsTerminating =>
do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 0)
let arg = toClosure defaultOpts [] nm

83
src/Core/Unify.idr
View File

@ -465,9 +465,11 @@ tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
case fullname mdef of
PV pv pi => throw (PatternVariableUnifies loc env (PV pv pi) otm)
_ => pure ()
let ty = type mdef -- assume all pi binders we need are there since
-- it was built from an environment, so no need
-- to normalise
defs <- get Ctxt
ty <- normalisePis defs [] $ type mdef
-- make sure we have all the pi binders we need in the
-- type to make the metavariable definition
logTerm "unify.instantiate" 5 ("Type: " ++ show mname) (type mdef)
logTerm "unify.instantiate" 5 ("Type: " ++ show mname) ty
log "unify.instantiate" 5 ("With locs: " ++ show locs)
log "unify.instantiate" 5 ("From vars: " ++ show newvars)
@ -604,15 +606,15 @@ tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
pure (Just soln')
mkDef _ _ _ _ = pure Nothing
-- update a solution that the machine found with the thing the programmer
-- actually wrote! We assume that we've already checked that they unify.
export
solveIfUndefined : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Env Term vars -> Term vars -> Term vars -> Core Bool
solveIfUndefined env (Meta fc mname idx args) soln
updateSolution : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Env Term vars -> Term vars -> Term vars -> Core Bool
updateSolution env (Meta fc mname idx args) soln
= do defs <- get Ctxt
Just (Hole _ _) <- lookupDefExact (Resolved idx) (gamma defs)
| _ => pure False
case !(patternEnvTm env args) of
Nothing => pure False
Just (newvars ** (locs, submv)) =>
@ -622,6 +624,19 @@ solveIfUndefined env (Meta fc mname idx args) soln
do Just hdef <- lookupCtxtExact (Resolved idx) (gamma defs)
| Nothing => throw (InternalError "Can't happen: no definition")
tryInstantiate fc inTerm env mname idx (length args) hdef locs soln stm
updateSolution env metavar soln
= pure False
export
solveIfUndefined : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Env Term vars -> Term vars -> Term vars -> Core Bool
solveIfUndefined env metavar@(Meta fc mname idx args) soln
= do defs <- get Ctxt
Just (Hole _ _) <- lookupDefExact (Resolved idx) (gamma defs)
| _ => pure False
updateSolution env metavar soln
solveIfUndefined env metavar soln
= pure False
@ -674,12 +689,14 @@ mutual
show (atTop mode)) env x y
else convertError loc env x y
getArgTypes : Defs -> (fnType : NF vars) -> List (Closure vars) ->
getArgTypes : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
Defs -> (fnType : NF vars) -> List (Closure vars) ->
Core (Maybe (List (NF vars)))
getArgTypes defs (NBind _ n (Pi _ _ _ ty) sc) (a :: as)
= do Just scTys <- getArgTypes defs !(sc defs a) as
| Nothing => pure Nothing
pure (Just (ty :: scTys))
pure (Just (!(evalClosure defs ty) :: scTys))
getArgTypes _ _ [] = pure (Just [])
getArgTypes _ _ _ = pure Nothing
@ -1071,9 +1088,9 @@ mutual
{auto u : Ref UST UState} ->
{vars : _} ->
UnifyInfo -> FC -> Env Term vars ->
FC -> Name -> Binder (NF vars) ->
FC -> Name -> Binder (Closure vars) ->
(Defs -> Closure vars -> Core (NF vars)) ->
FC -> Name -> Binder (NF vars) ->
FC -> Name -> Binder (Closure vars) ->
(Defs -> Closure vars -> Core (NF vars)) ->
Core UnifyResult
unifyBothBinders mode loc env xfc x (Pi fcx cx ix tx) scx yfc y (Pi fcy cy iy ty) scy
@ -1124,13 +1141,11 @@ mutual
(NBind yfc y (Lam fcy cy iy ty) scy)
else
do empty <- clearDefs defs
tx' <- quote empty env tx
ct <- unify (lower mode) loc env tx ty
xn <- genVarName "x"
let env' : Env Term (x :: _)
= Lam fcx cx Explicit tx' :: env
txtm <- quote empty env tx
tytm <- quote empty env ty
let env' : Env Term (x :: _)
= Lam fcx cx Explicit txtm :: env
tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
tscy <- scy defs (toClosure defaultOpts env (Ref loc Bound xn))
@ -1340,9 +1355,35 @@ mutual
empty <- clearDefs defs
if !(convert empty env x y)
then pure success
else do xnf <- evalClosure defs x
ynf <- evalClosure defs y
unify mode loc env xnf ynf
else
do xnf <- evalClosure defs x
ynf <- evalClosure defs y
-- If one's a meta and the other isn't, don't reduce at
-- all
case (xnf, ynf) of
-- They might be equal, don't want to make a cycle
(NApp _ (NMeta _ _ _) _, NApp _ (NMeta _ _ _) _)
=> unify mode loc env xnf ynf
(NApp _ (NMeta _ i _) _, _) =>
do ynf' <- evalClosure empty y
xtm <- quote empty env xnf
ytm <- quote empty env ynf'
cs <- unify mode loc env !(nf empty env xtm)
!(nf empty env ytm)
case constraints cs of
[] => pure cs
_ => do ynf <- evalClosure defs y
unify mode loc env xnf ynf
(_, NApp _ (NMeta _ i _ ) _) =>
do xnf' <- evalClosure empty x
xtm <- quote empty env xnf'
ytm <- quote empty env ynf
cs <- unify mode loc env !(nf empty env ytm)
!(nf empty env xtm)
case constraints cs of
[] => pure cs
_ => unify mode loc env xnf ynf
_ => unify mode loc env xnf ynf
export
setInvertible : {auto c : Ref Ctxt Defs} ->

5
src/Core/Value.idr
View File

@ -85,7 +85,7 @@ mutual
-- we can wait until necessary to reduce constructor arguments
public export
data NF : List Name -> Type where
NBind : FC -> (x : Name) -> Binder (NF vars) ->
NBind : FC -> (x : Name) -> Binder (Closure vars) ->
(Defs -> Closure vars -> Core (NF vars)) -> NF vars
-- Each closure is associated with the file context of the App node that
-- had it as an argument. It's necessary so as to not lose file context
@ -131,6 +131,9 @@ export
show (NRef _ n) = show n
show (NMeta n _ args) = "?" ++ show n ++ "_[" ++ show (length args) ++ " closures]"
Show (Closure free) where
show _ = "[closure]"
export
{free : _} -> Show (NF free) where
show (NBind _ x (Lam _ c info ty) _)

27
src/TTImp/Elab/App.idr
View File

@ -162,7 +162,7 @@ mutual
RigCount -> RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> (fntm : Term vars) ->
Name -> NF vars -> (Defs -> Closure vars -> Core (NF vars)) ->
Name -> Closure vars -> (Defs -> Closure vars -> Core (NF vars)) ->
(argdata : (Maybe Name, Nat)) ->
(expargs : List RawImp) ->
(autoargs : List RawImp) ->
@ -192,7 +192,7 @@ mutual
RigCount -> RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> (fntm : Term vars) ->
Name -> NF vars -> (Defs -> Closure vars -> Core (NF vars)) ->
Name -> Closure vars -> (Defs -> Closure vars -> Core (NF vars)) ->
(argpos : (Maybe Name, Nat)) ->
(expargs : List RawImp) ->
(autoargs : List RawImp) ->
@ -242,7 +242,7 @@ mutual
RigCount -> RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> (fntm : Term vars) ->
Name -> NF vars -> NF vars ->
Name -> Closure vars -> Closure vars ->
(Defs -> Closure vars -> Core (NF vars)) ->
(argpos : (Maybe Name, Nat)) ->
(expargs : List RawImp) ->
@ -345,21 +345,22 @@ mutual
Bind _ _ (Lam _ _ _ _) _ => registerDot rig env fc NotConstructor tm ty
_ => pure (tm, ty)
dotErased : {auto c : Ref Ctxt Defs} -> (argty : NF vars) ->
dotErased : {vars : _} ->
{auto c : Ref Ctxt Defs} -> (argty : Closure vars) ->
Maybe Name -> Nat -> ElabMode -> RigCount -> RawImp -> Core RawImp
dotErased argty mn argpos (InLHS lrig ) rig tm
= if not (isErased lrig) && isErased rig
then do
-- if the argument type aty has a single constructor, there's no need
-- to dot it
mconsCount <- countConstructors argty
defs <- get Ctxt
mconsCount <- countConstructors !(evalClosure defs argty)
if mconsCount == Just 1 || mconsCount == Just 0
then pure tm
else
-- if argpos is an erased position of 'n', leave it, otherwise dot if
-- necessary
do defs <- get Ctxt
Just gdef <- maybe (pure Nothing) (\n => lookupCtxtExact n (gamma defs)) mn
do Just gdef <- maybe (pure Nothing) (\n => lookupCtxtExact n (gamma defs)) mn
| Nothing => pure (dotTerm tm)
if argpos `elem` safeErase gdef
then pure tm
@ -405,7 +406,7 @@ mutual
RigCount -> RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars ->
FC -> (fntm : Term vars) -> Name ->
(aty : NF vars) -> (sc : Defs -> Closure vars -> Core (NF vars)) ->
(aty : Closure vars) -> (sc : Defs -> Closure vars -> Core (NF vars)) ->
(argdata : (Maybe Name, Nat)) ->
(arg : RawImp) ->
(expargs : List RawImp) ->
@ -427,7 +428,7 @@ mutual
-- first to give ambiguity resolution more to work with. So
-- we do that if the target type is unknown, or if we see that
-- the raw term is otherwise worth delaying.
if (isHole aty && kr) || !(needsDelay (elabMode elabinfo) kr arg_in)
if (isHole !(evalClosure defs aty) && kr) || !(needsDelay (elabMode elabinfo) kr arg_in)
then handle (checkRtoL kr arg)
-- if the type isn't resolved, we might encounter an
-- implicit that we can't use yet because we don't know
@ -451,7 +452,6 @@ mutual
metaty <- quote empty env aty
(idx, metaval) <- argVar (getFC arg) argRig env nm metaty
let fntm = App fc tm metaval
logNF "elab" 10 ("Delaying " ++ show nm ++ " " ++ show arg) env aty
logTerm "elab" 10 "...as" metaval
fnty <- sc defs (toClosure defaultOpts env metaval)
(tm, gty) <- checkAppWith rig elabinfo nest env fc
@ -492,11 +492,13 @@ mutual
-- If there's a constraint, make a constant, but otherwise
-- just return the term as expected
tm <- if not ok
then do res <- convert fc elabinfo env (gnf env metaval)
then do res <- convert fc elabinfo env
(gnf env metaval)
(gnf env argv)
let [] = constraints res
| cs => do tmty <- getTerm gty
newConstant fc rig env tm tmty cs
ignore $ updateSolution env metaval argv
pure tm
else pure tm
case elabMode elabinfo of
@ -512,7 +514,6 @@ mutual
Core (Term vars, Glued vars)
checkLtoR kr arg
= do defs <- get Ctxt
logNF "elab" 10 ("Argument type " ++ show x) env aty
logNF "elab" 10 ("Full function type") env
(NBind fc x (Pi fc argRig Explicit aty) sc)
logC "elab" 10
@ -521,7 +522,7 @@ mutual
expty
pure ("Overall expected type: " ++ show ety))
res <- check argRig (record { topLevel = False } elabinfo)
nest env arg (Just (glueBack defs env aty))
nest env arg (Just (glueClosure defs env aty))
(argv, argt) <-
if not (onLHS (elabMode elabinfo))
then pure res

2
src/TTImp/Elab/Record.idr
View File

@ -82,7 +82,7 @@ findFields defs con
let imp = case p of
Explicit => Nothing
_ => Just x
pure $ (nameRoot x, imp, getRecordType [] ty) :: rest
pure $ (nameRoot x, imp, getRecordType [] !(evalClosure defs ty)) :: rest
getExpNames _ = pure []
genFieldName : {auto u : Ref UST UState} ->

2
src/TTImp/Elab/RunElab.idr
View File

@ -114,7 +114,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
!(nf defs env' lamsc) Nothing -- (map weaken exp)
nf empty env (Bind bfc x (Lam fc' c qp qty) !(quote empty env' runsc))
where
quotePi : PiInfo (NF vars) -> Core (PiInfo (Term vars))
quotePi : PiInfo (Closure vars) -> Core (PiInfo (Term vars))
quotePi Explicit = pure Explicit
quotePi Implicit = pure Implicit
quotePi AutoImplicit = pure AutoImplicit

2
src/TTImp/Elab/Utils.idr
View File

@ -40,7 +40,7 @@ findErasedFrom defs pos (NBind fc x (Pi _ c _ aty) scf)
-- argument position is available
sc <- scf defs (toClosure defaultOpts [] (Erased fc (isErased c)))
(erest, dtrest) <- findErasedFrom defs (1 + pos) sc
let dt' = if !(detagSafe defs aty)
let dt' = if !(detagSafe defs !(evalClosure defs aty))
then (pos :: dtrest) else dtrest
pure $ if isErased c
then (pos :: erest, dt')

6
src/TTImp/Impossible.idr
View File

@ -122,7 +122,7 @@ mutual
buildApp : {auto c : Ref Ctxt Defs} ->
{auto q : Ref QVar Int} ->
FC -> Name -> Maybe (NF []) ->
FC -> Name -> Maybe (Closure []) ->
(expargs : List RawImp) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
@ -134,7 +134,7 @@ mutual
throw (InternalError "Can't deal with constants here yet")
gdefs <- lookupNameBy id n (gamma defs)
[(n', i, gdef)] <- dropNoMatch mty gdefs
[(n', i, gdef)] <- dropNoMatch !(traverseOpt (evalClosure defs) mty) gdefs
| [] => undefinedName fc n
| ts => throw (AmbiguousName fc (map fst ts))
tynf <- nf defs [] (type gdef)
@ -152,7 +152,7 @@ mutual
mkTerm : {auto c : Ref Ctxt Defs} ->
{auto q : Ref QVar Int} ->
RawImp -> Maybe (NF []) ->
RawImp -> Maybe (Closure []) ->
(expargs : List RawImp) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->

8
src/TTImp/Interactive/CaseSplit.idr
View File

@ -133,7 +133,8 @@ defaultNames : List String
defaultNames = ["x", "y", "z", "w", "v", "s", "t", "u"]
export
getArgName : {auto c : Ref Ctxt Defs} ->
getArgName : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
Defs -> Name ->
List Name -> -- explicitly bound names (possibly coming later),
-- so we don't invent a default
@ -168,12 +169,13 @@ getArgName defs x bound allvars ty
getName _ defs used = unique defs defs 0 used
export
getArgNames : {auto c : Ref Ctxt Defs} ->
getArgNames : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
Defs -> List Name -> List Name -> Env Term vars -> NF vars ->
Core (List String)
getArgNames defs bound allvars env (NBind fc x (Pi _ _ p ty) sc)
= do ns <- case p of
Explicit => pure [!(getArgName defs x bound allvars ty)]
Explicit => pure [!(getArgName defs x bound allvars !(evalClosure defs ty))]
_ => pure []
sc' <- sc defs (toClosure defaultOpts env (Erased fc False))
pure $ ns ++ !(getArgNames defs bound (map UN ns ++ allvars) env sc')

4
src/TTImp/Interactive/MakeLemma.idr
View File

@ -5,6 +5,7 @@ import Core.Env
import Core.Metadata
import Core.Normalise
import Core.TT
import Core.Value
import TTImp.Unelab
import TTImp.TTImp
@ -86,5 +87,6 @@ makeLemma : {auto m : Ref MD Metadata} ->
FC -> Name -> Nat -> ClosedTerm ->
Core (RawImp, RawImp)
makeLemma loc n nlocs ty
= do (args, ret) <- getArgs [] nlocs ty
= do defs <- get Ctxt
(args, ret) <- getArgs [] nlocs !(normalise defs [] ty)
pure (mkType loc args ret, mkApp loc n args)

22
src/TTImp/PartialEval.idr
View File

@ -505,13 +505,13 @@ mutual
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
Ref QVar Int -> Defs -> Bounds bound ->
Env Term free -> PiInfo (NF free) ->
Env Term free -> PiInfo (Closure free) ->
Core (PiInfo (Term (bound ++ free)))
quotePi q defs bounds env Explicit = pure Explicit
quotePi q defs bounds env Implicit = pure Implicit
quotePi q defs bounds env AutoImplicit = pure AutoImplicit
quotePi q defs bounds env (DefImplicit t)
= do t' <- quoteGenNF q defs bounds env t
= do t' <- quoteGenNF q defs bounds env !(evalClosure defs t)
pure (DefImplicit t')
quoteBinder : {bound, free : _} ->
@ -519,30 +519,30 @@ mutual
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
Ref QVar Int -> Defs -> Bounds bound ->
Env Term free -> Binder (NF free) ->
Env Term free -> Binder (Closure free) ->
Core (Binder (Term (bound ++ free)))
quoteBinder q defs bounds env (Lam fc r p ty)
= do ty' <- quoteGenNF q defs bounds env ty
= do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
p' <- quotePi q defs bounds env p
pure (Lam fc r p' ty')
quoteBinder q defs bounds env (Let fc r val ty)
= do val' <- quoteGenNF q defs bounds env val
ty' <- quoteGenNF q defs bounds env ty
= do val' <- quoteGenNF q defs bounds env !(evalClosure defs val)
ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
pure (Let fc r val' ty')
quoteBinder q defs bounds env (Pi fc r p ty)
= do ty' <- quoteGenNF q defs bounds env ty
= do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
p' <- quotePi q defs bounds env p
pure (Pi fc r p' ty')
quoteBinder q defs bounds env (PVar fc r p ty)
= do ty' <- quoteGenNF q defs bounds env ty
= do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
p' <- quotePi q defs bounds env p
pure (PVar fc r p' ty')
quoteBinder q defs bounds env (PLet fc r val ty)
= do val' <- quoteGenNF q defs bounds env val
ty' <- quoteGenNF q defs bounds env ty
= do val' <- quoteGenNF q defs bounds env !(evalClosure defs val)
ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
pure (PLet fc r val' ty')
quoteBinder q defs bounds env (PVTy fc r ty)
= do ty' <- quoteGenNF q defs bounds env ty
= do ty' <- quoteGenNF q defs bounds env !(evalClosure defs ty)
pure (PVTy fc r ty')
quoteGenNF : {bound, vars : _} ->

5
src/TTImp/ProcessData.idr
View File

@ -201,12 +201,13 @@ getDetags fc tys
else pure rest
-- If exactly one argument is unerased, return its position
getRelevantArg : Defs -> Nat -> Maybe Nat -> Bool -> NF [] ->
getRelevantArg : {auto c : Ref Ctxt Defs} ->
Defs -> Nat -> Maybe Nat -> Bool -> NF [] ->
Core (Maybe (Bool, Nat))
getRelevantArg defs i rel world (NBind fc _ (Pi _ rig _ val) sc)
= branchZero (getRelevantArg defs (1 + i) rel world
!(sc defs (toClosure defaultOpts [] (Erased fc False))))
(case val of
(case !(evalClosure defs val) of
-- %World is never inspected, so might as well be deleted from data types,
-- although it needs care when compiling to ensure that the function that
-- returns the IO/%World type isn't erased

12
src/TTImp/ProcessType.idr
View File

@ -108,13 +108,13 @@ processFnOpt fc _ ndef (SpecArgs ns)
getDeps : Bool -> NF [] -> NameMap Bool ->
Core (NameMap Bool)
getDeps inparam (NBind _ x (Pi _ _ _ pty) sc) ns
= do ns' <- getDeps inparam pty ns
defs <- get Ctxt
= do defs <- get Ctxt
ns' <- getDeps inparam !(evalClosure defs pty) ns
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
getDeps inparam sc' ns'
getDeps inparam (NBind _ x b sc) ns
= do ns' <- getDeps False (binderType b) ns
defs <- get Ctxt
= do defs <- get Ctxt
ns' <- getDeps False !(evalClosure defs (binderType b)) ns
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
getDeps False sc' ns
getDeps inparam (NApp _ (NRef Bound n) args) ns
@ -158,7 +158,7 @@ processFnOpt fc _ ndef (SpecArgs ns)
empty <- clearDefs defs
sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x))
if x `elem` ns
then do deps <- getDeps True nty NameMap.empty
then do deps <- getDeps True !(evalClosure defs nty) NameMap.empty
-- Get names depended on by nty
-- Keep the ones which are either:
-- * parameters
@ -249,7 +249,7 @@ findInferrable defs ty = fi 0 0 [] [] ty
fi pos i args acc (NBind fc x (Pi _ _ _ aty) sc)
= do let argn = MN "inf" i
sc' <- sc defs (toClosure defaultOpts [] (Ref fc Bound argn))
acc' <- findInf acc args aty
acc' <- findInf acc args !(evalClosure defs aty)
rest <- fi (1 + pos) (1 + i) ((argn, pos) :: args) acc' sc'
pure rest
fi pos i args acc ret = findInf acc args ret

6
tests/idris2/basic044/expected
View File

@ -122,7 +122,7 @@ LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not de
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
Target type : ({arg:N} : (Data.Fin.Fin ?Vec.{n:N}_[])) -> ?Vec.{a:N}_[])
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
(($resolvedN (fromInteger 0)) Nil)
(($resolvedN (fromInteger 0)) Nil)
@ -135,7 +135,7 @@ With default. Target type : ?Vec.{a:N}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
$resolvedN
Target type : ({arg:N} : (Data.Fin.Fin ?Vec.{n:N}_[])) -> ?Vec.{a:N}_[])
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
($resolvedN 0)
($resolvedN 0)
@ -143,7 +143,7 @@ With default. Target type : ?Vec.{a:N}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
$resolvedN
Target type : ({arg:N} : (Data.Fin.Fin ?Vec.{n:N}_[])) -> ?Vec.{a:N}_[])
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:L:C--L:C:
(($resolvedN (fromInteger 0)) Nil)
Target type : (Prelude.Basics.List Prelude.Types.Nat)

2
tests/idris2/interface021/LocalHint.idr
View File

@ -13,7 +13,6 @@ mkFoo gnu = A
gnat : {auto startHere : (a : Foo ** a = A)} -> Unit
gnat = ()
%logging 0
pathology : (gnu : Gnu) -> Unit
pathology gnu =
let %hint foo : Foo
@ -22,4 +21,3 @@ pathology gnu =
-> (a : Foo ** a = A)
bar _ Refl = (A ** Refl)
in gnat
%logging 0

10
tests/idris2/positivity004/expected
View File

@ -67,6 +67,16 @@ Issue1771-3:10:3--10:6
10 | MkF : Wrap (Not F) -> F
^^^
Error: notF is not total, possibly not terminating due to call to Main.F
Issue1771-3:15:1--15:13
11 |
12 | yesF : Not F -> F
13 | yesF = MkF . MkWrap
14 |
15 | notF : Not F
^^^^^^^^^^^^
Error: yesF is not total, possibly not terminating due to calls to Main.F, Main.MkF
Issue1771-3:12:1--12:18

2
tests/idris2/record001/expected
View File

@ -1,5 +1,5 @@
1/1: Building Record (Record.idr)
Main> [1, 2, 3, 4, 5]
Main> [1, 2, 3, 4, 5]
Main> some_fn testPerson : Nat -> Nat
Main> some_fn testPerson : b testPerson -> Nat
Main> Bye for now!