idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-20 09:48:38 +03:00
Code Issues Projects Releases Wiki Activity

[ log ] stuck functions found during evaluation

Browse Source
This commit is contained in:
Guillaume ALLAIS 2020-08-27 18:09:39 +01:00 committed by G. Allais
parent 5d156167d3
commit c17c6fc522
21 changed files with 207 additions and 85 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/Compiler/CompileExpr.idr
View File

@ -465,7 +465,8 @@ data NArgs : Type where
NBuffer : NArgs
NIORes : Closure [] -> NArgs
getPArgs : Defs -> Closure [] -> Core (String, Closure [])
getPArgs : {auto c : Ref Ctxt Defs} ->
Defs -> Closure [] -> Core (String, Closure [])
getPArgs defs cl
= do NDCon fc _ _ _ args <- evalClosure defs cl
| nf => throw (GenericMsg (getLoc nf) "Badly formed struct type")
@ -476,7 +477,8 @@ getPArgs defs cl
pure (n', tydesc)
_ => throw (GenericMsg fc "Badly formed struct type")
getFieldArgs : Defs -> Closure [] -> Core (List (String, Closure []))
getFieldArgs : {auto c : Ref Ctxt Defs} ->
Defs -> Closure [] -> Core (List (String, Closure []))
getFieldArgs defs cl
= do NDCon fc _ _ _ args <- evalClosure defs cl
| nf => throw (GenericMsg (getLoc nf) "Badly formed struct type")
@ -489,7 +491,8 @@ getFieldArgs defs cl
-- nil
_ => pure []
getNArgs : Defs -> Name -> List (Closure []) -> Core NArgs
getNArgs : {auto c : Ref Ctxt Defs} ->
Defs -> Name -> List (Closure []) -> Core NArgs
getNArgs defs (NS _ (UN "IORes")) [arg] = pure $ NIORes arg
getNArgs defs (NS _ (UN "Ptr")) [arg] = pure NPtr
getNArgs defs (NS _ (UN "AnyPtr")) [] = pure NPtr

4
src/Core/Core.idr
View File

@ -460,6 +460,10 @@ when : Bool -> Lazy (Core ()) -> Core ()
when True f = f
when False f = pure ()
export %inline
unless : Bool -> Lazy (Core ()) -> Core ()
unless = when . not
-- Control.Catchable in Idris 1, just copied here (but maybe no need for
-- it since we'll only have the one instance for Core Error...)
public export

12
src/Core/Coverage.idr
View File

@ -134,7 +134,8 @@ freeEnv fc (n :: ns) = PVar fc top Explicit (Erased fc False) :: freeEnv fc ns
-- Given a normalised type, get all the possible constructors for that
-- type family, with their type, name, tag, and arity
getCons : {vars : _} ->
getCons : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> Core (List (NF [], Name, Int, Nat))
getCons defs (NTCon _ tn _ _ _)
= case !(lookupDefExact tn (gamma defs)) of
@ -179,7 +180,8 @@ altMatch _ _ = False
-- Given a type and a list of case alternatives, return the
-- well-typed alternatives which were *not* in the list
getMissingAlts : {vars : _} ->
getMissingAlts : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
FC -> Defs -> NF vars -> List (CaseAlt vars) ->
Core (List (CaseAlt vars))
-- If it's a primitive other than WorldVal, there's too many to reasonably
@ -267,7 +269,8 @@ tagIsNot ts (DefaultCase _) = False
-- Replace a default case with explicit branches for the constructors.
-- This is easier than checking whether a default is needed when traversing
-- the tree (just one constructor lookup up front).
replaceDefaults : {vars : _} ->
replaceDefaults : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
FC -> Defs -> NF vars -> List (CaseAlt vars) ->
Core (List (CaseAlt vars))
-- Leave it alone if it's a primitive type though, since we need the catch
@ -296,7 +299,8 @@ replaceDefaults fc defs nfty cs
-- when we reach a leaf we know what patterns were used to get there,
-- and return those patterns.
-- The returned patterns are those arising from the *missing* cases
buildArgs : {vars : _} ->
buildArgs : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
FC -> Defs ->
KnownVars vars Int -> -- Things which have definitely match
KnownVars vars (List Int) -> -- Things an argument *can't* be

146
src/Core/Normalise.idr
View File

@ -41,16 +41,18 @@ getNF {c} (MkGlue _ _ nf) = nf c
Stack : List Name -> Type
Stack vars = List (Closure vars)
evalWithOpts : {free, vars : _} ->
evalWithOpts : {auto c : Ref Ctxt Defs} ->
{free, vars : _} ->
Defs -> EvalOpts ->
Env Term free -> LocalEnv free vars ->
Term (vars ++ free) -> Stack free -> Core (NF free)
export
evalClosure : {free : _} -> Defs -> Closure free -> Core (NF free)
evalClosure : {auto c : Ref Ctxt Defs} ->
{free : _} -> Defs -> Closure free -> Core (NF free)
export
evalArg : {free : _} -> Defs -> Closure free -> Core (NF free)
evalArg : {auto c : Ref Ctxt Defs} -> {free : _} -> Defs -> Closure free -> Core (NF free)
evalArg defs c = evalClosure defs c
export
@ -93,7 +95,8 @@ data CaseResult a
parameters (defs : Defs, topopts : EvalOpts)
mutual
eval : {free, vars : _} ->
eval : {auto c : Ref Ctxt Defs} ->
{free, vars : _} ->
Env Term free -> LocalEnv free vars ->
Term (vars ++ free) -> Stack free -> Core (NF free)
eval env locs (Local fc mrig idx prf) stk
@ -147,7 +150,8 @@ parameters (defs : Defs, topopts : EvalOpts)
eval env locs (Erased fc i) stk = pure $ NErased fc i
eval env locs (TType fc) stk = pure $ NType fc
evalLocClosure : {free : _} ->
evalLocClosure : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Env Term free ->
FC -> Maybe Bool ->
Stack free ->
@ -173,7 +177,8 @@ parameters (defs : Defs, topopts : EvalOpts)
= pure $ NTCon fc n t a (args ++ stk)
applyToStack nf _ = pure nf
evalLocal : {free, vars : _} ->
evalLocal : {auto c : Ref Ctxt Defs} ->
{free, vars : _} ->
Env Term free ->
FC -> Maybe Bool ->
(idx : Nat) -> (0 p : IsVar name idx (vars ++ free)) ->
@ -204,7 +209,8 @@ parameters (defs : Defs, topopts : EvalOpts)
updateLocal (S idx) (Later p) (x :: locs) nf = x :: updateLocal idx p locs nf
updateLocal _ _ locs nf = locs
evalMeta : {free : _} ->
evalMeta : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Env Term free ->
FC -> Name -> Int -> List (Closure free) ->
Stack free -> Core (NF free)
@ -212,7 +218,8 @@ parameters (defs : Defs, topopts : EvalOpts)
= evalRef env True fc Func (Resolved i) (args ++ stk)
(NApp fc (NMeta nm i args) stk)
evalRef : {free : _} ->
evalRef : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Env Term free ->
(isMeta : Bool) ->
FC -> NameType -> Name -> Stack free -> (def : Lazy (NF free)) ->
@ -223,19 +230,22 @@ parameters (defs : Defs, topopts : EvalOpts)
= pure $ NTCon fc fn tag arity stk
evalRef env meta fc Bound fn stk def
= pure def
evalRef env meta fc nt n stk def
evalRef env meta fc nt@Func n stk def
= do Just res <- lookupCtxtExact n (gamma defs)
| Nothing => pure def
let redok = evalAll topopts ||
reducibleInAny (currentNS defs :: nestedNS defs)
(fullname res)
(visibility res)
let redok1 = evalAll topopts
let redok2 = reducibleInAny (currentNS defs :: nestedNS defs)
(fullname res)
(visibility res)
let redok = redok1 || redok2
unless redok2 $ logC "eval.stuck" 5 $ pure $ "Stuck function: " ++ show !(toFullNames n)
if redok
then do
Just opts' <- useMeta (noCycles res) fc n defs topopts
| Nothing => pure def
Just opts' <- updateLimit nt n opts'
| Nothing => pure def -- name is past reduction limit
| Nothing => do log "eval.stuck" 10 $ "Function " ++ show n ++ " past reduction limit"
pure def -- name is past reduction limit
evalDef env opts' meta fc
(multiplicity res) (definition res) (flags res) stk def
else pure def
@ -249,7 +259,8 @@ parameters (defs : Defs, topopts : EvalOpts)
getCaseBound (arg :: args) [] loc = Nothing -- mismatched arg length
getCaseBound (arg :: args) (n :: ns) loc = (arg ::) <$> getCaseBound args ns loc
evalConAlt : {more, free : _} ->
evalConAlt : {auto c : Ref Ctxt Defs} ->
{more, free : _} ->
Env Term free ->
LocalEnv free more -> EvalOpts -> FC ->
Stack free ->
@ -262,7 +273,8 @@ parameters (defs : Defs, topopts : EvalOpts)
| Nothing => pure GotStuck
evalTree env bound opts fc stk sc
tryAlt : {free, more : _} ->
tryAlt : {auto c : Ref Ctxt Defs} ->
{free, more : _} ->
Env Term free ->
LocalEnv free more -> EvalOpts -> FC ->
Stack free -> NF free -> CaseAlt more ->
@ -314,7 +326,8 @@ parameters (defs : Defs, topopts : EvalOpts)
concrete _ = False
tryAlt _ _ _ _ _ _ _ = pure GotStuck
findAlt : {args, free : _} ->
findAlt : {auto c : Ref Ctxt Defs} ->
{args, free : _} ->
Env Term free ->
LocalEnv free args -> EvalOpts -> FC ->
Stack free -> NF free -> List (CaseAlt args) ->
@ -326,7 +339,8 @@ parameters (defs : Defs, topopts : EvalOpts)
| GotStuck => pure GotStuck
pure (Result val)
evalTree : {args, free : _} -> Env Term free -> LocalEnv free args ->
evalTree : {auto c : Ref Ctxt Defs} ->
{args, free : _} -> Env Term free -> LocalEnv free args ->
EvalOpts -> FC ->
Stack free -> CaseTree args ->
Core (CaseResult (NF free))
@ -370,7 +384,8 @@ parameters (defs : Defs, topopts : EvalOpts)
= do (loc', stk') <- argsFromStack ns args
pure (arg :: loc', stk')
evalOp : {arity, free : _} ->
evalOp : {auto c : Ref Ctxt Defs} ->
{arity, free : _} ->
(Vect arity (NF free) -> Maybe (NF free)) ->
Stack free -> (def : Lazy (NF free)) ->
Core (NF free)
@ -389,7 +404,8 @@ parameters (defs : Defs, topopts : EvalOpts)
evalAll [] = pure []
evalAll (c :: cs) = pure $ !(evalClosure defs c) :: !(evalAll cs)
evalDef : {free : _} ->
evalDef : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Env Term free -> EvalOpts ->
(isMeta : Bool) -> FC ->
RigCount -> Def -> List DefFlag ->
@ -432,12 +448,14 @@ evalClosure defs (MkClosure opts locs env tm)
evalClosure defs (MkNFClosure nf) = pure nf
export
nf : {vars : _} ->
nf : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> Env Term vars -> Term vars -> Core (NF vars)
nf defs env tm = eval defs defaultOpts env [] tm []
export
nfOpts : {vars : _} ->
nfOpts : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
EvalOpts -> Defs -> Env Term vars -> Term vars -> Core (NF vars)
nfOpts opts defs env tm = eval defs opts env [] tm []
@ -472,9 +490,11 @@ data QVar : Type where
public export
interface Quote (tm : List Name -> Type) where
quote : {vars : _} ->
quote : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> Env Term vars -> tm vars -> Core (Term vars)
quoteGen : {vars : _} ->
quoteGen : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Ref QVar Int -> Defs -> Env Term vars -> tm vars -> Core (Term vars)
quote defs env tm
@ -488,7 +508,8 @@ genName n
pure (MN n i)
mutual
quoteArgs : {bound, free : _} ->
quoteArgs : {auto c : Ref Ctxt Defs} ->
{bound, free : _} ->
Ref QVar Int -> Defs -> Bounds bound ->
Env Term free -> List (Closure free) ->
Core (List (Term (bound ++ free)))
@ -497,7 +518,8 @@ mutual
= pure $ (!(quoteGenNF q defs bounds env !(evalClosure defs a)) ::
!(quoteArgs q defs bounds env args))
quoteHead : {bound, free : _} ->
quoteHead : {auto c : Ref Ctxt Defs} ->
{bound, free : _} ->
Ref QVar Int -> Defs ->
FC -> Bounds bound -> Env Term free -> NHead free ->
Core (Term (bound ++ free))
@ -533,7 +555,8 @@ mutual
= do args' <- quoteArgs q defs bounds env args
pure $ Meta fc n i args'
quotePi : {bound, free : _} ->
quotePi : {auto c : Ref Ctxt Defs} ->
{bound, free : _} ->
Ref QVar Int -> Defs -> Bounds bound ->
Env Term free -> PiInfo (NF free) ->
Core (PiInfo (Term (bound ++ free)))
@ -544,7 +567,8 @@ mutual
= do t' <- quoteGenNF q defs bounds env t
pure (DefImplicit t')
quoteBinder : {bound, free : _} ->
quoteBinder : {auto c : Ref Ctxt Defs} ->
{bound, free : _} ->
Ref QVar Int -> Defs -> Bounds bound ->
Env Term free -> Binder (NF free) ->
Core (Binder (Term (bound ++ free)))
@ -572,7 +596,8 @@ mutual
= do ty' <- quoteGenNF q defs bounds env ty
pure (PVTy fc r ty')
quoteGenNF : {bound, vars : _} ->
quoteGenNF : {auto c : Ref Ctxt Defs} ->
{bound, vars : _} ->
Ref QVar Int ->
Defs -> Bounds bound ->
Env Term vars -> NF vars -> Core (Term (bound ++ vars))
@ -637,7 +662,8 @@ Quote Closure where
quoteGen q defs env c = quoteGen q defs env !(evalClosure defs c)
export
glueBack : {vars : _} ->
glueBack : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> Env Term vars -> NF vars -> Glued vars
glueBack defs env nf
= MkGlue False
@ -646,24 +672,28 @@ glueBack defs env nf
(const (pure nf))
export
normalise : {free : _} ->
normalise : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Defs -> Env Term free -> Term free -> Core (Term free)
normalise defs env tm = quote defs env !(nf defs env tm)
export
normaliseOpts : {free : _} ->
normaliseOpts : {auto c : Ref Ctxt Defs} ->
{free : _} ->
EvalOpts -> Defs -> Env Term free -> Term free -> Core (Term free)
normaliseOpts opts defs env tm
= quote defs env !(nfOpts opts defs env tm)
export
normaliseHoles : {free : _} ->
normaliseHoles : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Defs -> Env Term free -> Term free -> Core (Term free)
normaliseHoles defs env tm
= quote defs env !(nfOpts withHoles defs env tm)
export
normaliseLHS : {free : _} ->
normaliseLHS : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Defs -> Env Term free -> Term free -> Core (Term free)
normaliseLHS defs env (Bind fc n b sc)
= pure $ Bind fc n b !(normaliseLHS defs (b :: env) sc)
@ -671,13 +701,15 @@ normaliseLHS defs env tm
= quote defs env !(nfOpts onLHS defs env tm)
export
normaliseArgHoles : {free : _} ->
normaliseArgHoles : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Defs -> Env Term free -> Term free -> Core (Term free)
normaliseArgHoles defs env tm
= quote defs env !(nfOpts withArgHoles defs env tm)
export
normaliseAll : {free : _} ->
normaliseAll : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Defs -> Env Term free -> Term free -> Core (Term free)
normaliseAll defs env tm
= quote defs env !(nfOpts withAll defs env tm)
@ -686,7 +718,8 @@ normaliseAll defs env tm
-- binders is the slow part of normalisation so whenever we can avoid it, it's
-- a big win
export
normaliseScope : {free : _} ->
normaliseScope : {auto c : Ref Ctxt Defs} ->
{free : _} ->
Defs -> Env Term free -> Term free -> Core (Term free)
normaliseScope defs env (Bind fc n b sc)
= pure $ Bind fc n b !(normaliseScope defs (b :: env) sc)
@ -694,10 +727,12 @@ normaliseScope defs env tm = normalise defs env tm
public export
interface Convert (tm : List Name -> Type) where
convert : {vars : _} ->
convert : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> Env Term vars ->
tm vars -> tm vars -> Core Bool
convGen : {vars : _} ->
convGen : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Ref QVar Int ->
Defs -> Env Term vars ->
tm vars -> tm vars -> Core Bool
@ -748,7 +783,8 @@ tryUpdate ms (Erased fc i) = pure $ Erased fc i
tryUpdate ms (TType fc) = pure $ TType fc
mutual
allConv : {vars : _} ->
allConv : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Ref QVar Int -> Defs -> Env Term vars ->
List (Closure vars) -> List (Closure vars) -> Core Bool
allConv q defs env [] [] = pure True
@ -758,7 +794,8 @@ mutual
-- If the case trees match in structure, get the list of variables which
-- have to match in the call
getMatchingVarAlt : {args, args' : _} ->
getMatchingVarAlt : {auto c : Ref Ctxt Defs} ->
{args, args' : _} ->
Defs ->
List (Var args, Var args') ->
CaseAlt args -> CaseAlt args' ->
@ -808,7 +845,8 @@ mutual
= getMatchingVars defs ms t t'
getMatchingVarAlt defs _ _ _ = pure Nothing
getMatchingVarAlts : {args, args' : _} ->
getMatchingVarAlts : {auto c : Ref Ctxt Defs} ->
{args, args' : _} ->
Defs ->
List (Var args, Var args') ->
List (CaseAlt args) -> List (CaseAlt args') ->
@ -820,7 +858,8 @@ mutual
getMatchingVarAlts defs ms as as'
getMatchingVarAlts defs _ _ _ = pure Nothing
getMatchingVars : {args, args' : _} ->
getMatchingVars : {auto c : Ref Ctxt Defs} ->
{args, args' : _} ->
Defs ->
List (Var args, Var args') ->
CaseTree args -> CaseTree args' ->
@ -837,7 +876,8 @@ mutual
getMatchingVars defs ms Impossible Impossible = pure (Just ms)
getMatchingVars _ _ _ _ = pure Nothing
chkSameDefs : {vars : _} ->
chkSameDefs : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Ref QVar Int -> Defs -> Env Term vars ->
Name -> Name ->
List (Closure vars) -> List (Closure vars) -> Core Bool
@ -875,7 +915,8 @@ mutual
-- If two names are standing for case blocks, check the blocks originate
-- from the same place, and have the same scrutinee
chkConvCaseBlock : {vars : _} ->
chkConvCaseBlock : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
FC -> Ref QVar Int -> Defs -> Env Term vars ->
NHead vars -> List (Closure vars) ->
NHead vars -> List (Closure vars) -> Core Bool
@ -923,7 +964,8 @@ mutual
getScrutinee _ _ = Nothing
chkConvCaseBlock _ _ _ _ _ _ _ _ = pure False
chkConvHead : {vars : _} ->
chkConvHead : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Ref QVar Int -> Defs -> Env Term vars ->
NHead vars -> NHead vars -> Core Bool
chkConvHead q defs env (NLocal _ idx _) (NLocal _ idx' _) = pure $ idx == idx'
@ -939,7 +981,8 @@ mutual
subRig x y = (isLinear x && isRigOther y) ||
x == y
convBinders : {vars : _} ->
convBinders : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Ref QVar Int -> Defs -> Env Term vars ->
Binder (NF vars) -> Binder (NF vars) -> Core Bool
convBinders q defs env (Pi _ cx ix tx) (Pi _ cy iy ty)
@ -1042,7 +1085,8 @@ getValArity defs env (NBind fc x (Pi _ _ _ _) sc)
getValArity defs env val = pure 0
export
getArity : {vars : _} ->
getArity : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> Env Term vars -> Term vars -> Core Nat
getArity defs env tm = getValArity defs env !(nf defs env tm)
@ -1143,7 +1187,8 @@ logEnv str n msg env
show x) bs (binderType b)
dumpEnv bs
replace' : {vars : _} ->
replace' : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Int -> Defs -> Env Term vars ->
(lhs : NF vars) -> (parg : Term vars) -> (exp : NF vars) ->
Core (Term vars)
@ -1203,7 +1248,8 @@ replace' {vars} tmpi defs env lhs parg tm
quote empty env tm
export
replace : {vars : _} ->
replace : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> Env Term vars ->
(orig : NF vars) -> (new : Term vars) -> (tm : NF vars) ->
Core (Term vars)

3
src/Core/Reflect.idr
View File

@ -12,7 +12,8 @@ import Core.Value
public export
interface Reify a where
reify : {vars : _} ->
reify : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> Core a
public export

9
src/Core/Termination.idr
View File

@ -553,7 +553,8 @@ checkTerminating loc n
pure tot'
t => pure t
nameIn : Defs -> List Name -> NF [] -> Core Bool
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))
then pure True
@ -574,7 +575,8 @@ nameIn defs tyns _ = pure False
-- Check an argument type doesn't contain a negative occurrence of any of
-- the given type names
posArg : Defs -> List Name -> NF [] -> Core Terminating
posArg : {auto c : Ref Ctxt Defs} ->
Defs -> List Name -> NF [] -> Core Terminating
-- a tyn can only appear in the parameter positions of
-- tc; report positivity failure if it appears anywhere else
posArg defs tyns (NTCon _ tc _ _ args)
@ -602,7 +604,8 @@ posArg defs tyns (NBind fc x (Pi _ _ e ty) sc)
posArg defs tyns sc'
posArg defs tyn _ = pure IsTerminating
checkPosArgs : Defs -> List Name -> NF [] -> Core Terminating
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
IsTerminating =>

3
src/Idris/REPL.idr
View File

@ -633,12 +633,13 @@ process (Eval itm)
(\err => pure ())
(tm, gty) <- elabTerm inidx (emode (evalMode opts)) [] (MkNested [])
[] ttimp Nothing
logTerm "repl.eval" 10 "Elaborated input" tm
defs <- get Ctxt
opts <- get ROpts
let norm = nfun (evalMode opts)
ntm <- norm defs [] tm
logTermNF "repl.eval" 5 "Normalised" [] ntm
itm <- resugar [] ntm
logTermNF "" 5 "Normalised" [] ntm
if showTypes opts
then do ty <- getTerm gty
ity <- resugar [] !(norm defs [] ty)

21
src/TTImp/Elab/Ambiguity.idr
View File

@ -162,12 +162,14 @@ Show TypeMatch where
show NoMatch = "NoMatch"
mutual
mightMatchD : {vars : _} ->
mightMatchD : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> NF [] -> Core TypeMatch
mightMatchD defs l r
= mightMatch defs (stripDelay l) (stripDelay r)
mightMatchArg : {vars : _} ->
mightMatchArg : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs ->
Closure vars -> Closure [] ->
Core Bool
@ -176,7 +178,8 @@ mutual
NoMatch => False
_ => True
mightMatchArgs : {vars : _} ->
mightMatchArgs : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs ->
List (Closure vars) -> List (Closure []) ->
Core Bool
@ -188,7 +191,8 @@ mutual
else pure False
mightMatchArgs _ _ _ = pure False
mightMatch : {vars : _} ->
mightMatch : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> NF [] -> Core TypeMatch
mightMatch defs target (NBind fc n (Pi _ _ _ _) sc)
= mightMatchD defs target !(sc defs (toClosure defaultOpts [] (Erased fc False)))
@ -212,14 +216,16 @@ mutual
mightMatch _ _ _ = pure NoMatch
-- Return true if the given name could return something of the given target type
couldBeName : {vars : _} ->
couldBeName : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> Name -> Core TypeMatch
couldBeName defs target n
= case !(lookupTyExact n (gamma defs)) of
Nothing => pure Poly -- could be a local name, don't rule it out
Just ty => mightMatchD defs target !(nf defs [] ty)
couldBeFn : {vars : _} ->
couldBeFn : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> RawImp -> Core TypeMatch
couldBeFn defs ty (IVar _ n) = couldBeName defs ty n
couldBeFn defs ty (IAlternative _ _ _) = pure Concrete
@ -229,7 +235,8 @@ couldBeFn defs ty _ = pure Poly
-- the target type
-- Just (True, app) if it's a match on concrete return type
-- Just (False, app) if it might be a match due to being polymorphic
couldBe : {vars : _} ->
couldBe : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> RawImp -> Core (Maybe (Bool, RawImp))
couldBe {vars} defs ty@(NTCon _ n _ _ _) app
= case !(couldBeFn {vars} defs ty (getFn app)) of

11
src/TTImp/Elab/Delayed.idr
View File

@ -130,7 +130,8 @@ ambiguous (WhenUnifying _ _ _ _ err) = ambiguous err
ambiguous _ = False
mutual
mismatchNF : {vars : _} ->
mismatchNF : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> NF vars -> Core Bool
mismatchNF defs (NTCon _ xn xt _ xargs) (NTCon _ yn yt _ yargs)
= if xn /= yn
@ -146,13 +147,15 @@ mutual
= mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
mismatchNF _ _ _ = pure False
mismatch : {vars : _} ->
mismatch : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> (Closure vars, Closure vars) -> Core Bool
mismatch defs (x, y)
= mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
contra : {vars : _} ->
Defs -> NF vars -> NF vars -> Core Bool
contra : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> NF vars -> Core Bool
-- Unlike 'impossibleOK', any mismatch indicates an unrecoverable error
contra defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
= if xn /= yn

6
src/TTImp/Elab/ImplicitBind.idr
View File

@ -259,7 +259,8 @@ bindImplVars {vars} fc mode gam env imps_in scope scty
(Bind fc _ (PLet fc c bpat' bty') tm',
Bind fc _ (PLet fc c bpat' bty') ty')
normaliseHolesScope : {vars : _} ->
normaliseHolesScope : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> Env Term vars -> Term vars -> Core (Term vars)
normaliseHolesScope defs env (Bind fc n b sc)
= pure $ Bind fc n b
@ -269,7 +270,8 @@ normaliseHolesScope defs env (Bind fc n b sc)
normaliseHolesScope defs env tm = normaliseHoles defs env tm
export
bindImplicits : {vars : _} ->
bindImplicits : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
FC -> BindMode ->
Defs -> Env Term vars ->
List (Name, ImplBinding vars) ->

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

@ -66,7 +66,8 @@ findConName defs tyn
Just (TCon _ _ _ _ _ _ [con] _) => pure (Just con)
_ => pure Nothing
findFields : Defs -> Name ->
findFields : {auto c : Ref Ctxt Defs} ->
Defs -> Name ->
Core (Maybe (List (String, Maybe Name, Maybe Name)))
findFields defs con
= case !(lookupTyExact con (gamma defs)) of

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

@ -12,7 +12,8 @@ import TTImp.TTImp
%default covering
detagSafe : Defs -> NF [] -> Core Bool
detagSafe : {auto c : Ref Ctxt Defs} ->
Defs -> NF [] -> Core Bool
detagSafe defs (NTCon _ n _ _ args)
= do Just (TCon _ _ _ _ _ _ _ (Just detags)) <- lookupDefExact n (gamma defs)
| _ => pure False
@ -30,7 +31,8 @@ detagSafe defs (NTCon _ n _ _ args)
= elem i ns || notErased (i + 1) ns rest
detagSafe defs _ = pure False
findErasedFrom : Defs -> Nat -> NF [] -> Core (List Nat, List Nat)
findErasedFrom : {auto c : Ref Ctxt Defs} ->
Defs -> Nat -> NF [] -> Core (List Nat, List Nat)
findErasedFrom defs pos (NBind fc x (Pi _ c _ aty) scf)
= do -- In the scope, use 'Erased fc True' to mean 'argument is erased'.
-- It's handy here, because we can use it to tell if a detaggable

12
src/TTImp/ProcessDef.idr
View File

@ -33,7 +33,8 @@ import Data.NameMap
%default covering
mutual
mismatchNF : {vars : _} ->
mismatchNF : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> NF vars -> Core Bool
mismatchNF defs (NTCon _ xn xt _ xargs) (NTCon _ yn yt _ yargs)
= if xn /= yn
@ -49,7 +50,8 @@ mutual
= mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
mismatchNF _ _ _ = pure False
mismatch : {vars : _} ->
mismatch : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> (Closure vars, Closure vars) -> Core Bool
mismatch defs (x, y)
= mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
@ -58,7 +60,8 @@ mutual
-- the argument positions has different constructors at its head, then this
-- is an impossible case, so return True
export
impossibleOK : {vars : _} ->
impossibleOK : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> NF vars -> Core Bool
impossibleOK defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
= if xn == yn
@ -95,7 +98,8 @@ impossibleErrOK defs _ = pure False
-- is, if we have a concrete thing, and we're expecting the same concrete
-- thing, or a function of something, then we might have a match.
export
recoverable : {vars : _} ->
recoverable : {auto c : Ref Ctxt Defs} ->
{vars : _} ->
Defs -> NF vars -> NF vars -> Core Bool
-- Unlike the above, any mismatch will do
recoverable defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)

3
src/TTImp/ProcessType.idr
View File

@ -212,7 +212,8 @@ initDef n env ty (_ :: opts) = initDef n env ty opts
-- Find the inferrable argument positions in a type. This is useful for
-- generalising partially evaluated definitions and (potentially) in interactive
-- editing
findInferrable : Defs -> NF [] -> Core (List Nat)
findInferrable : {auto c : Ref Ctxt Defs} ->
Defs -> NF [] -> Core (List Nat)
findInferrable defs ty = fi 0 0 [] [] ty
where
mutual

3
src/TTImp/TTImp.idr
View File

@ -464,7 +464,8 @@ findImplicits tm = []
-- IBindVar anywhere else in the pattern) so that they will be available on the
-- rhs
export
implicitsAs : Defs -> List Name -> RawImp -> Core RawImp
implicitsAs : {auto c : Ref Ctxt Defs} ->
Defs -> List Name -> RawImp -> Core RawImp
implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) tm
where
setAs : List (Maybe Name) -> RawImp -> Core RawImp

2
tests/Main.idr
View File

@ -41,7 +41,7 @@ idrisTests
"basic026", "basic027", "basic028", "basic029", "basic030",
"basic031", "basic032", "basic033", "basic034", "basic035",
"basic036", "basic037", "basic038", "basic039", "basic040",
"basic041", "basic042", "basic043", "basic044",
"basic041", "basic042", "basic043", "basic044", "basic045",
-- Coverage checking
"coverage001", "coverage002", "coverage003", "coverage004",
"coverage005", "coverage006", "coverage007", "coverage008",

14
tests/idris2/basic045/Lib.idr Normal file
View File

@ -0,0 +1,14 @@
module Lib
import Data.List
%default total
export
accMapAux : (a -> b) -> List a -> List b -> List b
accMapAux f [] acc = reverse acc
accMapAux f (x :: xs) acc = accMapAux f xs (f x :: acc)
public export
accMap : (a -> b) -> List a -> List b
accMap f xs = accMapAux f xs []

11
tests/idris2/basic045/Main.idr Normal file
View File

@ -0,0 +1,11 @@
module Main
import Lib
%logging eval 10
test : List Int
test = accMap (1+) [1,2,3]
-- refl : Main.test = [2,3,4]
-- refl = Refl

9
tests/idris2/basic045/expected Normal file
View File

@ -0,0 +1,9 @@
1/2: Building Lib (Lib.idr)
2/2: Building Main (Main.idr)
Main> LOG eval.stuck:5: Stuck function: Lib.accMapAux
LOG eval.stuck:5: Stuck function: Lib.accMapAux
LOG eval.stuck:5: Stuck function: Lib.accMapAux
LOG eval.stuck:5: Stuck function: Lib.accMapAux
[2, 3, 4]
Main>
Bye for now!

2
tests/idris2/basic045/input Normal file
View File

@ -0,0 +1,2 @@
test
:q

3
tests/idris2/basic045/run Normal file
View File

@ -0,0 +1,3 @@
$1 --no-banner --no-color --console-width 0 --log eval.stuck:5 Main.idr < input
rm -rf build