mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 15:07:37 +03:00
Store postponed unification problems as values
We stored them as equations between terms, I think because terms are easy to re-evaluate with new information, and because I thought we might want to save them out. It's not usually a problem to do that. However... Going back and forth between terms and values can be expensive if we're stuck in the middle of a complicated unification problem, the like of which can turn up a lot if your types are complicated. So, we need to be able to handle this. Now store the postponed problems as NF, rather than Term, and add a fuction to resume evaluating a NF with an updated context.
This commit is contained in:
Edwin Brady
parent
c87a6d52bb
commit
45fc100f6c
@ -708,6 +708,26 @@ export
|
||||
Quote Closure where
|
||||
quoteGen q defs env c = quoteGen q defs env !(evalClosure defs c)
|
||||
|
||||
-- Resume a previously blocked normalisation with a new environment
|
||||
export
|
||||
continueNF : {auto c : Ref Ctxt Defs} ->
|
||||
{vars : _} ->
|
||||
Defs -> Env Term vars -> NF vars -> Core (NF vars)
|
||||
continueNF defs env stuck@(NApp fc (NRef nt fn) stk)
|
||||
= evalRef defs defaultOpts env False fc nt fn stk stuck
|
||||
continueNF defs env (NApp fc (NMeta name idx args) stk)
|
||||
= evalMeta defs defaultOpts env fc name idx args stk
|
||||
-- Next batch are already in normal form
|
||||
continueNF defs env nf@(NDCon fc x tag arity xs) = pure nf
|
||||
continueNF defs env nf@(NTCon fc x tag arity xs) = pure nf
|
||||
continueNF defs env nf@(NPrimVal fc x) = pure nf
|
||||
continueNF defs env nf@(NErased fc imp) = pure nf
|
||||
continueNF defs env nf@(NType fc) = pure nf
|
||||
-- For the rest, easiest just to quote and reevaluate
|
||||
continueNF defs env tm
|
||||
= do empty <- clearDefs defs
|
||||
nf defs env !(quote empty env tm)
|
||||
|
||||
export
|
||||
glueBack : {auto c : Ref Ctxt Defs} ->
|
||||
{vars : _} ->
|
||||
|
||||
@ -226,24 +226,21 @@ postpone blockedMetas loc mode logstr env x y
|
||||
checkDefined defs x
|
||||
checkDefined defs y
|
||||
|
||||
xtm <- quote empty env x
|
||||
ytm <- quote empty env y
|
||||
-- Need to find all the metas in the constraint since solving any one
|
||||
-- of them might stop the constraint being blocked.
|
||||
metas <-
|
||||
if blockedMetas
|
||||
then let xmetas = getMetas xtm in
|
||||
chaseMetas (keys (addMetas xmetas ytm)) NameMap.empty
|
||||
then do let xmetas = getMetas x
|
||||
let ymetas = addMetas xmetas y
|
||||
chaseMetas (keys ymetas) NameMap.empty
|
||||
else pure []
|
||||
blocked <- filterM undefinedN metas
|
||||
c <- addConstraint (MkConstraint loc (atTop mode) blocked env
|
||||
xtm
|
||||
ytm)
|
||||
c <- addConstraint (MkConstraint loc (atTop mode) blocked env x y)
|
||||
log "unify.postpone" 10 $
|
||||
show c ++ " NEW CONSTRAINT " ++ show loc ++
|
||||
" blocked on " ++ show metas
|
||||
logTerm "unify.postpone" 10 "X" xtm
|
||||
logTerm "unify.postpone" 10 "Y" ytm
|
||||
logNF "unify.postpone" 10 "X" env x
|
||||
logNF "unify.postpone" 10 "Y" env y
|
||||
pure (constrain c)
|
||||
where
|
||||
checkDefined : Defs -> NF vars -> Core ()
|
||||
@ -1203,6 +1200,12 @@ mutual
|
||||
= do cs <- unify (lower mode) loc env x y
|
||||
cs' <- unifyArgs mode loc env (map snd axs) (map snd ays)
|
||||
pure (union cs cs')
|
||||
unifyNoEta mode loc env x@(NApp xfc fx@(NMeta _ _ _) axs)
|
||||
y@(NApp yfc fy@(NMeta _ _ _) ays)
|
||||
= do defs <- get Ctxt
|
||||
if !(convert defs env x y)
|
||||
then pure success
|
||||
else unifyBothApps (lower mode) loc env xfc fx axs yfc fy ays
|
||||
unifyNoEta mode loc env (NApp xfc fx axs) (NApp yfc fy ays)
|
||||
= unifyBothApps (lower mode) loc env xfc fx axs yfc fy ays
|
||||
unifyNoEta mode loc env (NApp xfc hd args) y
|
||||
@ -1241,7 +1244,9 @@ mutual
|
||||
logNF "unify" 10 "EtaR" env tmx
|
||||
logNF "unify" 10 "...with" env tmy
|
||||
if isHoleApp tmy
|
||||
then unifyNoEta (lower mode) loc env tmx tmy
|
||||
then if not !(convert defs env tmx tmy)
|
||||
then unifyNoEta (lower mode) loc env tmx tmy
|
||||
else pure success
|
||||
else do empty <- clearDefs defs
|
||||
domty <- quote empty env tx
|
||||
etay <- nf defs env
|
||||
@ -1255,7 +1260,9 @@ mutual
|
||||
logNF "unify" 10 "EtaL" env tmx
|
||||
logNF "unify" 10 "...with" env tmy
|
||||
if isHoleApp tmx
|
||||
then unifyNoEta (lower mode) loc env tmx tmy
|
||||
then if not !(convert defs env tmx tmy)
|
||||
then unifyNoEta (lower mode) loc env tmx tmy
|
||||
else pure success
|
||||
else do empty <- clearDefs defs
|
||||
domty <- quote empty env ty
|
||||
etax <- nf defs env
|
||||
@ -1287,7 +1294,7 @@ mutual
|
||||
unifyD _ _ mode loc env x y
|
||||
= do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
if !(convert empty env x y)
|
||||
if x == y
|
||||
then do log "unify.equal" 10 $
|
||||
"Skipped unification (equal already): "
|
||||
++ show x ++ " and " ++ show y
|
||||
@ -1298,7 +1305,7 @@ mutual
|
||||
unifyWithLazyD _ _ mode loc env x y
|
||||
= do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
if !(convert empty env x y)
|
||||
if x == y
|
||||
then do log "unify.equal" 10 $
|
||||
"Skipped unification (equal already): "
|
||||
++ show x ++ " and " ++ show y
|
||||
@ -1348,14 +1355,17 @@ retry mode c
|
||||
case lookup c (constraints ust) of
|
||||
Nothing => pure success
|
||||
Just Resolved => pure success
|
||||
Just (MkConstraint loc withLazy blocked env x y)
|
||||
=> if umode mode /= InTerm ||
|
||||
Just (MkConstraint loc withLazy blocked env xold yold)
|
||||
=> do defs <- get Ctxt
|
||||
x <- continueNF defs env xold
|
||||
y <- continueNF defs env yold
|
||||
if umode mode /= InTerm ||
|
||||
!(anyM definedN blocked) || isNil blocked
|
||||
-- only go if any of the blocked names are defined now
|
||||
then
|
||||
catch
|
||||
(do logTermNF "unify.retry" 5 ("Retrying " ++ show c ++ " " ++ show (umode mode)) env x
|
||||
logTermNF "unify.retry" 5 "....with" env y
|
||||
(do logNF "unify.retry" 5 ("Retrying " ++ show c ++ " " ++ show (umode mode)) env x
|
||||
logNF "unify.retry" 5 "....with" env y
|
||||
log "unify.retry" 5 $ if withLazy
|
||||
then "(lazy allowed)"
|
||||
else "(no lazy)"
|
||||
@ -1368,14 +1378,19 @@ retry mode c
|
||||
pure cs
|
||||
_ => do log "unify.retry" 5 $ "Constraints " ++ show (addLazy cs)
|
||||
pure cs)
|
||||
(\err => throw (WhenUnifying loc env x y err))
|
||||
(\err => do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
throw (WhenUnifying loc env !(quote empty env x) !(quote empty env y) err))
|
||||
else
|
||||
do log "unify.retry" 10 $ show c ++ " still blocked on " ++ show blocked
|
||||
logTermNF "unify.retry" 10 "X" env x
|
||||
logTermNF "unify.retry" 10 "Y" env y
|
||||
logNF "unify.retry" 10 "X" env x
|
||||
logNF "unify.retry" 10 "Y" env y
|
||||
pure (constrain c)
|
||||
Just (MkSeqConstraint loc env xs ys)
|
||||
=> do cs <- unifyArgs mode loc env xs ys
|
||||
Just (MkSeqConstraint loc env xsold ysold)
|
||||
=> do defs <- get Ctxt
|
||||
xs <- traverse (continueNF defs env) xsold
|
||||
ys <- traverse (continueNF defs env) ysold
|
||||
cs <- unifyArgs mode loc env xs ys
|
||||
case constraints cs of
|
||||
[] => do deleteConstraint c
|
||||
pure cs
|
||||
@ -1578,9 +1593,12 @@ checkDots
|
||||
pure (Just n')
|
||||
|
||||
checkConstraint : (Name, DotReason, Constraint) -> Core ()
|
||||
checkConstraint (n, reason, MkConstraint fc wl blocked env x y)
|
||||
= do logTermNF "unify.constraint" 10 "Dot" env y
|
||||
logTermNF "unify.constraint" 10 " =" env x
|
||||
checkConstraint (n, reason, MkConstraint fc wl blocked env xold yold)
|
||||
= do defs <- get Ctxt
|
||||
x <- continueNF defs env xold
|
||||
y <- continueNF defs env yold
|
||||
logNF "unify.constraint" 10 "Dot" env y
|
||||
logNF "unify.constraint" 10 " =" env x
|
||||
-- A dot is okay if the constraint is solvable *without solving
|
||||
-- any additional holes*
|
||||
ust <- get UST
|
||||
@ -1628,9 +1646,10 @@ checkDots
|
||||
-- Clear constraints so we don't report again
|
||||
-- later
|
||||
put UST (record { dotConstraints = [] } ust)
|
||||
empty <- clearDefs defs
|
||||
throw (BadDotPattern fc env reason
|
||||
!(normaliseHoles defs env x)
|
||||
!(normaliseHoles defs env y))
|
||||
!(quote empty env x)
|
||||
!(quote empty env y))
|
||||
_ => do put UST (record { dotConstraints = [] } ust)
|
||||
throw err)
|
||||
checkConstraint _ = pure ()
|
||||
|
||||
@ -10,6 +10,7 @@ import Core.Normalise
|
||||
import Core.Options
|
||||
import Core.TT
|
||||
import Core.TTC
|
||||
import Core.Value
|
||||
import Libraries.Utils.Binary
|
||||
|
||||
import Libraries.Data.IntMap
|
||||
@ -28,7 +29,7 @@ data Constraint : Type where
|
||||
(withLazy : Bool) ->
|
||||
(blockedOn : List Name) ->
|
||||
(env : Env Term vars) ->
|
||||
(x : Term vars) -> (y : Term vars) ->
|
||||
(x : NF vars) -> (y : NF vars) ->
|
||||
Constraint
|
||||
-- An unsolved sequence of constraints, arising from arguments in an
|
||||
-- application where solving later constraints relies on solving earlier
|
||||
@ -36,37 +37,12 @@ data Constraint : Type where
|
||||
MkSeqConstraint : {vars : _} ->
|
||||
FC ->
|
||||
(env : Env Term vars) ->
|
||||
(xs : List (Term vars)) ->
|
||||
(ys : List (Term vars)) ->
|
||||
(xs : List (NF vars)) ->
|
||||
(ys : List (NF vars)) ->
|
||||
Constraint
|
||||
-- A resolved constraint
|
||||
Resolved : Constraint
|
||||
|
||||
export
|
||||
TTC Constraint where
|
||||
toBuf b (MkConstraint {vars} fc l block env x y)
|
||||
= do tag 0; toBuf b vars; toBuf b l
|
||||
toBuf b block
|
||||
toBuf b fc; toBuf b env; toBuf b x; toBuf b y
|
||||
toBuf b (MkSeqConstraint {vars} fc env xs ys)
|
||||
= do tag 1; toBuf b vars; toBuf b fc; toBuf b env; toBuf b xs; toBuf b ys
|
||||
toBuf b Resolved = tag 2
|
||||
|
||||
fromBuf b
|
||||
= case !getTag of
|
||||
0 => do vars <- fromBuf b
|
||||
fc <- fromBuf b; l <- fromBuf b
|
||||
block <- fromBuf b
|
||||
env <- fromBuf b
|
||||
x <- fromBuf b; y <- fromBuf b
|
||||
pure (MkConstraint {vars} fc l block env x y)
|
||||
1 => do vars <- fromBuf b
|
||||
fc <- fromBuf b; env <- fromBuf b
|
||||
xs <- fromBuf b; ys <- fromBuf b
|
||||
pure (MkSeqConstraint {vars} fc env xs ys)
|
||||
2 => pure Resolved
|
||||
_ => corrupt "Constraint"
|
||||
|
||||
public export
|
||||
record UState where
|
||||
constructor MkUState
|
||||
@ -292,13 +268,17 @@ addConstraint constr
|
||||
|
||||
export
|
||||
addDot : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> Env Term vars -> Name -> Term vars -> DotReason -> Term vars ->
|
||||
Core ()
|
||||
addDot fc env dotarg x reason y
|
||||
= do ust <- get UST
|
||||
defs <- get Ctxt
|
||||
xnf <- nf defs env x
|
||||
ynf <- nf defs env y
|
||||
put UST (record { dotConstraints $=
|
||||
((dotarg, reason, MkConstraint fc False [] env x y) ::)
|
||||
((dotarg, reason, MkConstraint fc False [] env xnf ynf) ::)
|
||||
} ust)
|
||||
|
||||
mkConstantAppArgs : {vars : _} ->
|
||||
@ -599,13 +579,15 @@ checkValidHole base (idx, (fc, n))
|
||||
case c of
|
||||
MkConstraint fc l blocked env x y =>
|
||||
do put UST (record { guesses = empty } ust)
|
||||
xnf <- normaliseHoles defs env x
|
||||
ynf <- normaliseHoles defs env y
|
||||
empty <- clearDefs defs
|
||||
xnf <- quote empty env x
|
||||
ynf <- quote empty env y
|
||||
throw (CantSolveEq fc env xnf ynf)
|
||||
MkSeqConstraint fc env (x :: _) (y :: _) =>
|
||||
do put UST (record { guesses = empty } ust)
|
||||
xnf <- normaliseHoles defs env x
|
||||
ynf <- normaliseHoles defs env y
|
||||
empty <- clearDefs defs
|
||||
xnf <- quote empty env x
|
||||
ynf <- quote empty env y
|
||||
throw (CantSolveEq fc env xnf ynf)
|
||||
_ => pure ()
|
||||
_ => traverse_ checkRef !(traverse getFullName
|
||||
@ -706,11 +688,12 @@ dumpHole' lvl hole
|
||||
Nothing => pure ()
|
||||
Just Resolved => log' lvl "\tResolved"
|
||||
Just (MkConstraint _ lazy _ env x y) =>
|
||||
do log' lvl $ "\t " ++ show !(toFullNames !(normalise defs env x))
|
||||
++ " =?= " ++ show !(toFullNames !(normalise defs env y))
|
||||
do log' lvl $ "\t " ++ show !(toFullNames !(quote defs env x))
|
||||
++ " =?= " ++ show !(toFullNames !(quote defs env y))
|
||||
empty <- clearDefs defs
|
||||
log' (withVerbosity 5 lvl)
|
||||
$ "\t from " ++ show !(toFullNames x)
|
||||
++ " =?= " ++ show !(toFullNames y) ++
|
||||
$ "\t from " ++ show !(toFullNames !(quote empty env x))
|
||||
++ " =?= " ++ show !(toFullNames !(quote empty env y)) ++
|
||||
if lazy then "\n\t(lazy allowed)" else ""
|
||||
Just (MkSeqConstraint _ _ xs ys) =>
|
||||
log' lvl $ "\t\t" ++ show xs ++ " =?= " ++ show ys
|
||||
|
||||
@ -6,6 +6,7 @@ import Core.Env
|
||||
import Core.TT
|
||||
|
||||
import Libraries.Data.IntMap
|
||||
import Libraries.Data.NameMap
|
||||
|
||||
%default covering
|
||||
|
||||
@ -99,6 +100,64 @@ ntCon fc n tag Z [] = case isConstantType n of
|
||||
Nothing => NTCon fc n tag Z []
|
||||
ntCon fc n tag arity args = NTCon fc n tag arity args
|
||||
|
||||
-- Look for metavariables which, if later defined, will help unblock
|
||||
-- reduction
|
||||
mutual
|
||||
export
|
||||
addMetas : NameMap Bool -> NF vars -> NameMap Bool
|
||||
addMetas ns (NBind fc x b sc)
|
||||
= addMetas ns (binderType b) -- we won't be blocked on the scope
|
||||
-- Arguments might be the cause of the blockage here
|
||||
addMetas ns (NApp fc (NMeta n i args) xs)
|
||||
= addMetaArgs (insert n False ns) (args ++ map snd xs)
|
||||
addMetas ns (NApp fc x xs)
|
||||
= addMetaArgs ns (map snd xs)
|
||||
addMetas ns (NDCon fc x tag arity xs)
|
||||
= addMetaArgs ns (map snd xs)
|
||||
addMetas ns (NTCon fc x tag arity xs)
|
||||
= addMetaArgs ns (map snd xs)
|
||||
addMetas ns (NAs fc _ p t)
|
||||
= addMetas (addMetas ns p) t
|
||||
addMetas ns (NDelayed fc x tm)
|
||||
= addMetas ns tm
|
||||
addMetas ns (NDelay fc x t y)
|
||||
= addMetaC (addMetaC ns t) y
|
||||
addMetas ns (NForce fc x t xs)
|
||||
= addMetas (addMetaArgs ns (map snd xs)) t
|
||||
addMetas ns (NPrimVal fc x) = ns
|
||||
addMetas ns (NErased fc imp) = ns
|
||||
addMetas ns (NType fc) = ns
|
||||
|
||||
addEnvMetas : NameMap Bool -> Env Term vars -> NameMap Bool
|
||||
addEnvMetas ns [] = ns
|
||||
addEnvMetas ns (Let _ _ val _ :: env) = addEnvMetas (addMetas ns val) env
|
||||
addEnvMetas ns (_ :: env) = addEnvMetas ns env
|
||||
|
||||
addMetaC : NameMap Bool -> Closure vars ->
|
||||
NameMap Bool
|
||||
addMetaC ns (MkClosure {vars=tvars} opts locs env' tm) = addMetas ns tm
|
||||
addMetaC ns (MkNFClosure x) = addMetas ns x
|
||||
|
||||
addMetaLocalEnv : NameMap Bool -> List (Closure vars) -> NameMap Bool
|
||||
addMetaLocalEnv ns (MkClosure _ locs _ _ :: _)
|
||||
= addMetaArgs ns (getClosures locs)
|
||||
where
|
||||
getClosures : LocalEnv f vs -> List (Closure f)
|
||||
getClosures [] = []
|
||||
getClosures (c :: ls) = c :: getClosures ls
|
||||
addMetaLocalEnv ns (_ :: cs) = addMetaLocalEnv ns cs
|
||||
addMetaLocalEnv ns [] = ns
|
||||
|
||||
addMetaArgs : NameMap Bool -> List (Closure vars) ->
|
||||
NameMap Bool
|
||||
addMetaArgs ns [] = ns
|
||||
addMetaArgs ns (c :: xs)
|
||||
= addMetaLocalEnv (addMetaArgs (addMetaC ns c) xs) (c :: xs)
|
||||
|
||||
export
|
||||
getMetas : NF vars -> NameMap Bool
|
||||
getMetas tm = addMetas empty tm
|
||||
|
||||
export
|
||||
getLoc : NF vars -> FC
|
||||
getLoc (NBind fc _ _ _) = fc
|
||||
|
||||
@ -56,7 +56,7 @@ processDecls decls
|
||||
| Just err => pure (case mapMaybe id xs of
|
||||
[] => [err]
|
||||
errs => errs)
|
||||
errs <- getTotalityErrors
|
||||
errs <- logTime ("+++ Totality check overall") getTotalityErrors
|
||||
pure (mapMaybe id xs ++ errs)
|
||||
|
||||
readModule : {auto c : Ref Ctxt Defs} ->
|
||||
|
||||
@ -129,11 +129,11 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
|
||||
logTerm "elab" 5 "Looking for delayed in " chktm
|
||||
ust <- get UST
|
||||
catch (retryDelayed (sortBy (\x, y => compare (fst x) (fst y))
|
||||
(delayedElab ust)))
|
||||
(\err =>
|
||||
do ust <- get UST
|
||||
put UST (record { delayedElab = olddelayed } ust)
|
||||
throw err)
|
||||
(delayedElab ust)))
|
||||
(\err =>
|
||||
do ust <- get UST
|
||||
put UST (record { delayedElab = olddelayed } ust)
|
||||
throw err)
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab = olddelayed } ust)
|
||||
solveConstraintsAfter constart solvemode MatchArgs
|
||||
|
||||
@ -445,7 +445,8 @@ checkClause {vars} mult vis totreq hashit n opts nest env (PatClause fc lhs_in r
|
||||
log "declare.def.clause" 5 $ "Checking RHS " ++ show rhs
|
||||
logEnv "declare.def.clause" 5 "In env" env'
|
||||
|
||||
rhstm <- wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
|
||||
rhstm <- logTime ("+++ Check RHS " ++ show fc) $
|
||||
wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
|
||||
checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
|
||||
clearHoleLHS
|
||||
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit (Just m) Main.Nat (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just {k:26}) Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit (Just _) Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit (Just m) Main.Nat (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just {k:25}) Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:25}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit (Just _) Main.Nat ((Main.Vect ((Main.plus {k:25}) m)) a))))))))
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTC
|
||||
Read TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit (Just m) Main.Nat (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just {k:26}) Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit (Just _) Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit (Just m) Main.Nat (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just {k:25}) Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:25}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit (Just _) Main.Nat ((Main.Vect ((Main.plus {k:25}) m)) a))))))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -2,5 +2,5 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((Main.Just [a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [k = Main.Z]) [a = Integer]) 1) (Main.Vect.Nil [a = Integer])))
|
||||
Yaffle> ((Main.MkInfer [a = (Main.List.List Integer)]) (((Main.List.Cons [a = Integer]) 1) (Main.List.Nil [a = Integer])))
|
||||
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved383 ?Main.{a:62}_[]), ($resolved363 ?Main.{a:62}_[])]
|
||||
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved381 ?Main.{a:59}_[]), ($resolved362 ?Main.{a:59}_[])]
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -2,6 +2,6 @@ Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.lookup: All cases covered
|
||||
Yaffle> Main.lookup':
|
||||
($resolved410 [__] [__] ($resolved376 [__]) {_:62})
|
||||
($resolved408 [__] [__] ($resolved376 [__]) {_:59})
|
||||
Yaffle> Main.lookup'': Calls non covering function Main.lookup'
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((Main.Refl [{b:10} = Main.Nat]) [x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
|
||||
Yaffle> ((Main.Refl [{b:9} = Main.Nat]) [x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
|
||||
Yaffle> Main.etaGood1 : ((((Main.Eq [b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit (Just x) Integer (%lam RigW Explicit (Just y) Integer ((Main.MkTest x) y))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
Processing as TTImp
|
||||
Eta.yaff:16:1--17:1:When elaborating right hand side of Main.etaBad:
|
||||
Eta.yaff:16:10--17:1:When unifying: (Main.Eq ({arg:11} : Integer) -> ({arg:12} : Integer) -> Main.Test)) ({arg:11} : Integer) -> ({arg:12} : Integer) -> Main.Test)) \(x : Char) => \(y : ?Main.{_:15}_[x[0]]) => (Main.MkTest x[1] y[0]) \(x : Char) => \(y : ?Main.{_:15}_[x[0]]) => (Main.MkTest x[1] y[0])) and (Main.Eq (x : Char) -> (y : ?Main.{_:15}_[x[0]]) -> Main.Test)) ({arg:11} : Integer) -> ({arg:12} : Integer) -> Main.Test)) Main.MkTest \(x : Char) => \(y : ?Main.{_:15}_[x[0]]) => (Main.MkTest x[1] y[0]))
|
||||
Eta.yaff:16:10--17:1:When unifying: (Main.Eq ({arg:10} : Integer) -> ({arg:11} : Integer) -> Main.Test)) ({arg:10} : Integer) -> ({arg:11} : Integer) -> Main.Test)) \(x : Char) => \(y : ?Main.{_:14}_[x[0]]) => (Main.MkTest x[1] y[0]) \(x : Char) => \(y : ?Main.{_:14}_[x[0]]) => (Main.MkTest x[1] y[0])) and (Main.Eq (x : Char) -> (y : ?Main.{_:14}_[x[0]]) -> Main.Test)) ({arg:10} : Integer) -> ({arg:11} : Integer) -> Main.Test)) Main.MkTest \(x : Char) => \(y : ?Main.{_:14}_[x[0]]) => (Main.MkTest x[1] y[0]))
|
||||
Eta.yaff:16:10--17:1:Type mismatch: Integer and Char
|
||||
Yaffle> Bye for now!
|
||||
|
||||
Loading…
Reference in New Issue
Block a user