mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Rabbit hole
Sorry for the less than informative title :). Lots going on here. It started as an attempt to fix unification to deal with laziness coercions in trickier places, but unearthed a couple of tricky and interconnected issues that are hard to unpick into a single patch. So, this fixes a few things: - default hints should only be resolved on the current elaboration (e.g. nested function definitions, not the outer definition which might not yet be complete) - delayed elaborators should be allowed to have nested delayed elaborators, which means disambiguation is a little bit better - we should delay elaborating arguments where the type isn't known yet, because later arguments may resolve the type, and we can use this to help with disambiguation/laziness coercions - other bits and pieces arising
This commit is contained in:
Edwin Brady
parent
bba4b347b9
commit
ed5b53d97f
@ -15,52 +15,66 @@ import Data.List.Views
|
||||
|
||||
%default covering
|
||||
|
||||
-- Need to record if we're at the top level or not, because top level things
|
||||
-- can have Force and Delay inserted, and may have been postponed.
|
||||
public export
|
||||
data UnifyLoc = Top Bool -- True == precise, False = generalise to RigW in Pi
|
||||
| Lower Bool
|
||||
|
||||
public export
|
||||
data UnifyMode = InLHS
|
||||
| InTerm UnifyLoc
|
||||
| InTerm
|
||||
| InMatch
|
||||
| InSearch
|
||||
|
||||
-- Need to record if we're at the top level or not, because top level things
|
||||
-- can have Force and Delay inserted, and may have been postponed.
|
||||
public export
|
||||
record UnifyInfo where
|
||||
constructor MkUnifyInfo
|
||||
atTop : Bool
|
||||
precise : Bool -- False == generalise to RigW in Pi
|
||||
umode : UnifyMode
|
||||
|
||||
export
|
||||
inTerm : UnifyMode
|
||||
inTerm = InTerm (Top True)
|
||||
inTerm : UnifyInfo
|
||||
inTerm = MkUnifyInfo True True InTerm
|
||||
|
||||
lam : UnifyMode -> UnifyMode
|
||||
lam (InTerm (Top _)) = InTerm (Top True)
|
||||
lam (InTerm (Lower _)) = InTerm (Lower True)
|
||||
lam m = m
|
||||
export
|
||||
inLHS : UnifyInfo
|
||||
inLHS = MkUnifyInfo True True InLHS
|
||||
|
||||
inLam : UnifyMode -> Bool
|
||||
inLam (InTerm (Top t)) = t
|
||||
inLam (InTerm (Lower t)) = t
|
||||
inLam _ = False
|
||||
export
|
||||
inTermP : Bool -> UnifyInfo
|
||||
inTermP p = MkUnifyInfo True p InTerm
|
||||
|
||||
lower : UnifyMode -> UnifyMode
|
||||
lower (InTerm (Top t)) = InTerm (Lower t)
|
||||
lower t = t
|
||||
export
|
||||
inMatch : UnifyInfo
|
||||
inMatch = MkUnifyInfo True True InMatch
|
||||
|
||||
atTop : UnifyMode -> Bool
|
||||
atTop (InTerm (Top _)) = True
|
||||
atTop _ = False
|
||||
export
|
||||
inSearch : UnifyInfo
|
||||
inSearch = MkUnifyInfo True True InSearch
|
||||
|
||||
Eq UnifyLoc where
|
||||
(Top s) == (Top t) = s == t
|
||||
(Lower s) == (Lower t) = s == t
|
||||
_ == _ = False
|
||||
lam : UnifyInfo -> UnifyInfo
|
||||
lam = record { precise = True }
|
||||
|
||||
inLam : UnifyInfo -> Bool
|
||||
inLam = precise
|
||||
|
||||
lower : UnifyInfo -> UnifyInfo
|
||||
lower = record { atTop = False }
|
||||
|
||||
Eq UnifyMode where
|
||||
InLHS == InLHS = True
|
||||
(InTerm s) == (InTerm t) = s == t
|
||||
InTerm == InTerm = True
|
||||
InMatch == InMatch = True
|
||||
InSearch == InSearch = True
|
||||
_ == _ = False
|
||||
|
||||
Eq UnifyInfo where
|
||||
x == y = atTop x == atTop y && precise x == precise y && umode x == umode y
|
||||
|
||||
Show UnifyMode where
|
||||
show InLHS = "InLHS"
|
||||
show InTerm = "InTerm"
|
||||
show InMatch = "InMatch"
|
||||
show InSearch = "InSearch"
|
||||
|
||||
-- If we're unifying a Lazy type with a non-lazy type, we need to add an
|
||||
-- explicit force or delay to the first argument to unification. This says
|
||||
-- which to add, if any. Can only added at the very top level.
|
||||
@ -106,7 +120,7 @@ interface Unify (tm : List Name -> Type) where
|
||||
-- Unify returns a list of ids referring to newly added constraints
|
||||
unifyD : Ref Ctxt Defs ->
|
||||
Ref UST UState ->
|
||||
UnifyMode ->
|
||||
UnifyInfo ->
|
||||
FC -> Env Term vars ->
|
||||
tm vars -> tm vars ->
|
||||
Core UnifyResult
|
||||
@ -114,7 +128,7 @@ interface Unify (tm : List Name -> Type) where
|
||||
-- order to infer annotations
|
||||
unifyWithLazyD : Ref Ctxt Defs ->
|
||||
Ref UST UState ->
|
||||
UnifyMode ->
|
||||
UnifyInfo ->
|
||||
FC -> Env Term vars ->
|
||||
tm vars -> tm vars ->
|
||||
Core UnifyResult
|
||||
@ -127,7 +141,7 @@ export
|
||||
unify : Unify tm =>
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
UnifyMode ->
|
||||
UnifyInfo ->
|
||||
FC -> Env Term vars ->
|
||||
tm vars -> tm vars ->
|
||||
Core UnifyResult
|
||||
@ -137,7 +151,7 @@ export
|
||||
unifyWithLazy : Unify tm =>
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
UnifyMode ->
|
||||
UnifyInfo ->
|
||||
FC -> Env Term vars ->
|
||||
tm vars -> tm vars ->
|
||||
Core UnifyResult
|
||||
@ -171,7 +185,7 @@ convertErrorS s loc env x y
|
||||
|
||||
postpone : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> UnifyMode -> String ->
|
||||
FC -> UnifyInfo -> String ->
|
||||
Env Term vars -> NF vars -> NF vars -> Core UnifyResult
|
||||
postpone loc mode logstr env x y
|
||||
= do defs <- get Ctxt
|
||||
@ -188,7 +202,7 @@ postpone loc mode logstr env x y
|
||||
|
||||
postponeS : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Bool -> FC -> UnifyMode -> String -> Env Term vars ->
|
||||
Bool -> FC -> UnifyInfo -> String -> Env Term vars ->
|
||||
NF vars -> NF vars ->
|
||||
Core UnifyResult
|
||||
postponeS s loc mode logstr env x y
|
||||
@ -198,7 +212,7 @@ postponeS s loc mode logstr env x y
|
||||
unifyArgs : (Unify tm, Quote tm) =>
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
UnifyMode -> FC -> Env Term vars ->
|
||||
UnifyInfo -> FC -> Env Term vars ->
|
||||
List (tm vars) -> List (tm vars) ->
|
||||
Core UnifyResult
|
||||
unifyArgs mode loc env [] [] = pure success
|
||||
@ -341,7 +355,7 @@ patternEnvTm {vars} env args
|
||||
instantiate : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{newvars : _} ->
|
||||
FC -> UnifyMode -> Env Term vars ->
|
||||
FC -> UnifyInfo -> Env Term vars ->
|
||||
(metavar : Name) -> (mref : Int) -> (numargs : Nat) ->
|
||||
(mdef : GlobalDef) ->
|
||||
List (Var newvars) -> -- Variable each argument maps to
|
||||
@ -475,14 +489,15 @@ mutual
|
||||
{auto u : Ref UST UState} ->
|
||||
{vars : _} ->
|
||||
(postpone : Bool) ->
|
||||
FC -> UnifyMode -> Env Term vars -> NF vars -> NF vars ->
|
||||
FC -> UnifyInfo -> Env Term vars -> NF vars -> NF vars ->
|
||||
Core UnifyResult
|
||||
unifyIfEq post loc mode env x y
|
||||
= do defs <- get Ctxt
|
||||
if !(convert defs env x y)
|
||||
then pure success
|
||||
else if post
|
||||
then postpone loc mode "Postponing unifyIfEq" env x y
|
||||
then postpone loc mode ("Postponing unifyIfEq " ++
|
||||
show (atTop mode)) env x y
|
||||
else convertError loc env x y
|
||||
|
||||
getArgTypes : Defs -> (fnType : NF vars) -> List (Closure vars) ->
|
||||
@ -514,7 +529,7 @@ mutual
|
||||
{auto u : Ref UST UState} ->
|
||||
{vars : _} ->
|
||||
(swaporder : Bool) ->
|
||||
UnifyMode -> FC -> Env Term vars ->
|
||||
UnifyInfo -> FC -> Env Term vars ->
|
||||
(metaname : Name) -> (metaref : Int) ->
|
||||
(margs : List (Closure vars)) ->
|
||||
(margs' : List (Closure vars)) ->
|
||||
@ -574,7 +589,7 @@ mutual
|
||||
{auto u : Ref UST UState} ->
|
||||
{vars : _} ->
|
||||
(swaporder : Bool) ->
|
||||
UnifyMode -> FC -> Env Term vars ->
|
||||
UnifyInfo -> FC -> Env Term vars ->
|
||||
(metaname : Name) -> (metaref : Int) ->
|
||||
(margs : List (Closure vars)) ->
|
||||
(margs' : List (Closure vars)) ->
|
||||
@ -614,7 +629,7 @@ mutual
|
||||
{auto u : Ref UST UState} ->
|
||||
{vars : _} ->
|
||||
(swaporder : Bool) ->
|
||||
UnifyMode -> FC -> Env Term vars ->
|
||||
UnifyInfo -> FC -> Env Term vars ->
|
||||
(metaname : Name) -> (metaref : Int) ->
|
||||
(margs : List (Closure vars)) ->
|
||||
(margs' : List (Closure vars)) ->
|
||||
@ -631,7 +646,7 @@ mutual
|
||||
solveHole : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{vars : _} ->
|
||||
FC -> UnifyMode -> Env Term vars ->
|
||||
FC -> UnifyInfo -> Env Term vars ->
|
||||
(metaname : Name) -> (metaref : Int) ->
|
||||
(margs : List (Closure vars)) ->
|
||||
(margs' : List (Closure vars)) ->
|
||||
@ -669,7 +684,7 @@ mutual
|
||||
{auto u : Ref UST UState} ->
|
||||
{vars : _} ->
|
||||
(swaporder : Bool) ->
|
||||
UnifyMode -> FC -> Env Term vars ->
|
||||
UnifyInfo -> FC -> Env Term vars ->
|
||||
FC -> (metaname : Name) -> (metaref : Int) ->
|
||||
(args : List (Closure vars)) ->
|
||||
(args' : List (Closure vars)) ->
|
||||
@ -721,7 +736,7 @@ mutual
|
||||
{vars : _} ->
|
||||
(swaporder : Bool) -> -- swap the order when postponing
|
||||
-- (this is to preserve second arg being expected type)
|
||||
UnifyMode -> FC -> Env Term vars -> FC ->
|
||||
UnifyInfo -> FC -> Env Term vars -> FC ->
|
||||
NHead vars -> List (Closure vars) -> NF vars ->
|
||||
Core UnifyResult
|
||||
unifyApp swap mode loc env fc (NMeta n i margs) args tm
|
||||
@ -769,7 +784,7 @@ mutual
|
||||
unifyBothApps : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{vars : _} ->
|
||||
UnifyMode -> FC -> Env Term vars ->
|
||||
UnifyInfo -> FC -> Env Term vars ->
|
||||
FC -> NHead vars -> List (Closure vars) ->
|
||||
FC -> NHead vars -> List (Closure vars) ->
|
||||
Core UnifyResult
|
||||
@ -780,10 +795,10 @@ mutual
|
||||
(NApp yfc (NLocal yr y yp) [])
|
||||
-- Locally bound things, in a term (not LHS). Since we have to unify
|
||||
-- for *all* possible values, we can safely unify the arguments.
|
||||
unifyBothApps (InTerm t) loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
|
||||
unifyBothApps mode@(MkUnifyInfo p t InTerm) loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
|
||||
= if x == y
|
||||
then unifyArgs (InTerm t) loc env xargs yargs
|
||||
else postpone loc (InTerm t) "Postponing local app"
|
||||
then unifyArgs mode loc env xargs yargs
|
||||
else postpone loc mode "Postponing local app"
|
||||
env (NApp xfc (NLocal xr x xp) xargs)
|
||||
(NApp yfc (NLocal yr y yp) yargs)
|
||||
unifyBothApps mode loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
|
||||
@ -792,7 +807,7 @@ mutual
|
||||
-- If they're both holes, solve the one with the bigger context
|
||||
unifyBothApps mode loc env xfc (NMeta xn xi xargs) xargs' yfc (NMeta yn yi yargs) yargs'
|
||||
= do invx <- isDefInvertible xi
|
||||
if xi == yi && (invx || mode == InSearch)
|
||||
if xi == yi && (invx || umode mode == InSearch)
|
||||
-- Invertible, (from auto implicit search)
|
||||
-- so we can also unify the arguments.
|
||||
then unifyArgs mode loc env (xargs ++ xargs')
|
||||
@ -805,7 +820,7 @@ mutual
|
||||
let xbigger = xlocs > ylocs
|
||||
|| (xlocs == ylocs &&
|
||||
length xargs' <= length yargs')
|
||||
if (xbigger || mode == InMatch) && not (pv xn)
|
||||
if (xbigger || umode mode == InMatch) && not (pv xn)
|
||||
then unifyApp False mode loc env xfc (NMeta xn xi xargs) xargs'
|
||||
(NApp yfc (NMeta yn yi yargs) yargs')
|
||||
else unifyApp True mode loc env yfc (NMeta yn yi yargs) yargs'
|
||||
@ -827,23 +842,23 @@ mutual
|
||||
= unifyApp False mode loc env xfc (NMeta xn xi xargs) xargs'
|
||||
(NApp yfc fy yargs')
|
||||
unifyBothApps mode loc env xfc fx xargs' yfc (NMeta yn yi yargs) yargs'
|
||||
= if mode /= InMatch
|
||||
= if umode mode /= InMatch
|
||||
then unifyApp True mode loc env xfc (NMeta yn yi yargs) yargs'
|
||||
(NApp xfc fx xargs')
|
||||
else unifyApp False mode loc env xfc fx xargs'
|
||||
(NApp yfc (NMeta yn yi yargs) yargs')
|
||||
unifyBothApps InSearch loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
|
||||
unifyBothApps mode@(MkUnifyInfo p t InSearch) loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
|
||||
= if hdx == hdy
|
||||
then unifyArgs InSearch loc env xargs yargs
|
||||
else unifyApp False InSearch loc env xfc fx xargs (NApp yfc fy yargs)
|
||||
unifyBothApps InMatch loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
|
||||
then unifyArgs mode loc env xargs yargs
|
||||
else unifyApp False mode loc env xfc fx xargs (NApp yfc fy yargs)
|
||||
unifyBothApps mode@(MkUnifyInfo p t InMatch) loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
|
||||
= if hdx == hdy
|
||||
then do logC 5 (do defs <- get Ctxt
|
||||
xs <- traverse (quote defs env) xargs
|
||||
ys <- traverse (quote defs env) yargs
|
||||
pure ("Matching args " ++ show xs ++ " " ++ show ys))
|
||||
unifyArgs InMatch loc env xargs yargs
|
||||
else unifyApp False InMatch loc env xfc fx xargs (NApp yfc fy yargs)
|
||||
unifyArgs mode loc env xargs yargs
|
||||
else unifyApp False mode loc env xfc fx xargs (NApp yfc fy yargs)
|
||||
unifyBothApps mode loc env xfc fx ax yfc fy ay
|
||||
= unifyApp False mode loc env xfc fx ax (NApp yfc fy ay)
|
||||
|
||||
@ -855,7 +870,7 @@ mutual
|
||||
unifyBothBinders: {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{vars : _} ->
|
||||
UnifyMode -> FC -> Env Term vars ->
|
||||
UnifyInfo -> FC -> Env Term vars ->
|
||||
FC -> Name -> Binder (NF vars) ->
|
||||
(Defs -> Closure vars -> Core (NF vars)) ->
|
||||
FC -> Name -> Binder (NF vars) ->
|
||||
@ -945,7 +960,7 @@ mutual
|
||||
unifyNoEta : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{vars : _} ->
|
||||
UnifyMode -> FC -> Env Term vars ->
|
||||
UnifyInfo -> FC -> Env Term vars ->
|
||||
NF vars -> NF vars ->
|
||||
Core UnifyResult
|
||||
unifyNoEta mode loc env (NDCon xfc x tagx ax xs) (NDCon yfc y tagy ay ys)
|
||||
@ -997,7 +1012,7 @@ mutual
|
||||
unifyNoEta mode loc env (NDelay xfc _ xty x) (NDelay yfc _ yty y)
|
||||
= unifyArgs mode loc env [xty, x] [yty, y]
|
||||
unifyNoEta mode loc env (NForce xfc _ x axs) (NForce yfc _ y ays)
|
||||
= do cs <- unify mode loc env x y
|
||||
= do cs <- unify (lower mode) loc env x y
|
||||
cs' <- unifyArgs mode loc env axs ays
|
||||
pure (union cs cs')
|
||||
unifyNoEta mode loc env (NApp xfc fx axs) (NApp yfc fy ays)
|
||||
@ -1005,7 +1020,7 @@ mutual
|
||||
unifyNoEta mode loc env (NApp xfc hd args) y
|
||||
= unifyApp False (lower mode) loc env xfc hd args y
|
||||
unifyNoEta mode loc env y (NApp yfc hd args)
|
||||
= if mode /= InMatch
|
||||
= if umode mode /= InMatch
|
||||
then unifyApp True mode loc env yfc hd args y
|
||||
else unifyIfEq True loc mode env y (NApp yfc hd args)
|
||||
-- Only try stripping as patterns as a last resort
|
||||
@ -1156,21 +1171,21 @@ Eq SolveMode where
|
||||
|
||||
retry : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
UnifyMode -> Int -> Core UnifyResult
|
||||
UnifyInfo -> Int -> Core UnifyResult
|
||||
retry mode c
|
||||
= do ust <- get UST
|
||||
case lookup c (constraints ust) of
|
||||
Nothing => pure success
|
||||
Just Resolved => pure success
|
||||
Just (MkConstraint loc withLazy env x y)
|
||||
=> catch (do logTermNF 5 "Retrying" env x
|
||||
=> catch (do logTermNF 5 ("Retrying " ++ show c) env x
|
||||
logTermNF 5 "....with" env y
|
||||
log 5 $ if withLazy
|
||||
then "(lazy allowed)"
|
||||
else "(no lazy)"
|
||||
cs <- if withLazy
|
||||
then unifyWithLazy mode loc env x y
|
||||
else unify mode loc env x y
|
||||
else unify (lower mode) loc env x y
|
||||
case constraints cs of
|
||||
[] => do log 5 $ "Success " ++ show (addLazy cs)
|
||||
deleteConstraint c
|
||||
@ -1198,7 +1213,7 @@ forceMeta r envb tm = TForce (getLoc tm) r tm
|
||||
-- Retry the given constraint, return True if progress was made
|
||||
retryGuess : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
UnifyMode -> (smode : SolveMode) -> (hole : (Int, (FC, Name))) ->
|
||||
UnifyInfo -> (smode : SolveMode) -> (hole : (Int, (FC, Name))) ->
|
||||
Core Bool
|
||||
retryGuess mode smode (hid, (loc, hname))
|
||||
= do defs <- get Ctxt
|
||||
@ -1229,7 +1244,7 @@ retryGuess mode smode (hid, (loc, hname))
|
||||
_ => pure False) -- Postpone again
|
||||
Guess tm envb [constr] =>
|
||||
do let umode = case smode of
|
||||
MatchArgs => InMatch
|
||||
MatchArgs => inMatch
|
||||
_ => mode
|
||||
cs <- retry umode constr
|
||||
case constraints cs of
|
||||
@ -1258,7 +1273,7 @@ retryGuess mode smode (hid, (loc, hname))
|
||||
pure False
|
||||
Guess tm envb constrs =>
|
||||
do let umode = case smode of
|
||||
MatchArgs => InMatch
|
||||
MatchArgs => inMatch
|
||||
_ => mode
|
||||
cs' <- traverse (retry umode) constrs
|
||||
let csAll = unionAll cs'
|
||||
@ -1280,13 +1295,27 @@ retryGuess mode smode (hid, (loc, hname))
|
||||
export
|
||||
solveConstraints : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
UnifyMode -> (smode : SolveMode) -> Core ()
|
||||
UnifyInfo -> (smode : SolveMode) -> Core ()
|
||||
solveConstraints umode smode
|
||||
= do ust <- get UST
|
||||
progress <- traverse (retryGuess umode smode) (toList (guesses ust))
|
||||
when (or (map Delay progress)) $
|
||||
solveConstraints umode Normal
|
||||
|
||||
export
|
||||
solveConstraintsAfter : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Int -> UnifyInfo -> (smode : SolveMode) -> Core ()
|
||||
solveConstraintsAfter start umode smode
|
||||
= do ust <- get UST
|
||||
progress <- traverse (retryGuess umode smode)
|
||||
(filter afterStart (toList (guesses ust)))
|
||||
when (or (map Delay progress)) $
|
||||
solveConstraintsAfter start umode Normal
|
||||
where
|
||||
afterStart : (Int, a) -> Bool
|
||||
afterStart (x, _) = x >= start
|
||||
|
||||
-- Replace any 'BySearch' with 'Hole', so that we don't keep searching
|
||||
-- fruitlessly while elaborating the rest of a source file
|
||||
export
|
||||
@ -1364,7 +1393,7 @@ checkDots
|
||||
-- In 'InMatch' mode, only metavariables in 'x' can
|
||||
-- be solved, so everything in the dotted metavariable
|
||||
-- must be complete.
|
||||
cs <- unify InMatch fc env x y
|
||||
cs <- unify inMatch fc env x y
|
||||
defs <- get Ctxt
|
||||
Just ndef <- lookupDefExact n (gamma defs)
|
||||
| Nothing => throw (UndefinedName fc n)
|
||||
|
||||
@ -105,18 +105,20 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
|
||||
ust <- get UST
|
||||
let olddelayed = delayedElab ust
|
||||
put UST (record { delayedElab = [] } ust)
|
||||
constart <- getNextEntry
|
||||
|
||||
defs <- get Ctxt
|
||||
e <- newRef EST (initEStateSub defining env' sub)
|
||||
let rigc = getRigNeeded mode
|
||||
|
||||
(chktm, chkty) <- check {e} rigc (initElabInfo mode) nest env tm ty
|
||||
-- Final retry of constraints and delayed elaborations
|
||||
-- - Solve any constraints, then retry any delayed elaborations
|
||||
-- - Finally, last attempts at solving constraints, but this
|
||||
-- is most likely just to be able to display helpful errors
|
||||
let solvemode = case mode of
|
||||
InLHS _ => InLHS
|
||||
_ => InTerm (Top False)
|
||||
InLHS _ => inLHS
|
||||
_ => inTermP False
|
||||
solveConstraints solvemode Normal
|
||||
logTerm 5 "Looking for delayed in " chktm
|
||||
ust <- get UST
|
||||
@ -127,16 +129,17 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
|
||||
throw err)
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab = olddelayed } ust)
|
||||
solveConstraints solvemode MatchArgs
|
||||
solveConstraintsAfter constart solvemode MatchArgs
|
||||
|
||||
-- As long as we're not in a case block, finish off constraint solving
|
||||
when (not incase) $
|
||||
-- resolve any default hints
|
||||
do solveConstraints solvemode Defaults
|
||||
do log 5 "Resolving default hints"
|
||||
solveConstraintsAfter constart solvemode Defaults
|
||||
-- perhaps resolving defaults helps...
|
||||
-- otherwise, this last go is most likely just to give us more
|
||||
-- helpful errors.
|
||||
solveConstraints solvemode LastChance
|
||||
solveConstraintsAfter constart solvemode LastChance
|
||||
|
||||
dumpConstraints 4 False
|
||||
defs <- get Ctxt
|
||||
|
||||
@ -274,7 +274,6 @@ export
|
||||
ambiguous : Error -> Bool
|
||||
ambiguous (AmbiguousElab _ _ _) = True
|
||||
ambiguous (AmbiguousName _ _) = True
|
||||
ambiguous (AllFailed _) = True
|
||||
ambiguous (InType _ _ err) = ambiguous err
|
||||
ambiguous (InCon _ _ err) = ambiguous err
|
||||
ambiguous (InLHS _ _ err) = ambiguous err
|
||||
@ -304,8 +303,8 @@ checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected
|
||||
pure (gnf env ty))
|
||||
pure mexpected
|
||||
let solvemode = case elabMode elabinfo of
|
||||
InLHS c => InLHS
|
||||
_ => InTerm (Top False)
|
||||
InLHS c => inLHS
|
||||
_ => inTermP False
|
||||
delayOnFailure fc rig env expected ambiguous $
|
||||
\delayed =>
|
||||
do solveConstraints solvemode Normal
|
||||
@ -318,11 +317,12 @@ checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected
|
||||
then gnf env exp
|
||||
else expected
|
||||
|
||||
alts' <- pruneByType env !(getNF exp') alts
|
||||
|
||||
logGlueNF 5 ("Ambiguous elaboration " ++ show alts' ++
|
||||
logGlueNF 5 ("Ambiguous elaboration " ++ show alts ++
|
||||
" at " ++ show fc ++
|
||||
"\nWith default. Target type ") env exp'
|
||||
alts' <- pruneByType env !(getNF exp') alts
|
||||
log 5 ("Pruned alts " ++ show alts')
|
||||
|
||||
if delayed -- use the default if there's still ambiguity
|
||||
then try
|
||||
(exactlyOne fc env
|
||||
@ -348,8 +348,8 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected
|
||||
pure (gnf env ty))
|
||||
pure mexpected
|
||||
let solvemode = case elabMode elabinfo of
|
||||
InLHS c => InLHS
|
||||
_ => InTerm (Top False)
|
||||
InLHS c => inLHS
|
||||
_ => inTermP False
|
||||
delayOnFailure fc rig env expected ambiguous $
|
||||
\delayed =>
|
||||
do defs <- get Ctxt
|
||||
@ -363,7 +363,8 @@ checkAlternative rig elabinfo nest env fc uniq alts mexpected
|
||||
|
||||
alts' <- pruneByType env !(getNF exp') alts
|
||||
|
||||
logGlueNF 5 ("Ambiguous elaboration " ++ show alts' ++
|
||||
logGlueNF 5 ("Ambiguous elaboration " ++ show delayed ++ " " ++
|
||||
show alts' ++
|
||||
" at " ++ show fc ++
|
||||
"\nTarget type ") env exp'
|
||||
let tryall = case uniq of
|
||||
|
||||
@ -360,7 +360,7 @@ mutual
|
||||
then pure True
|
||||
else do sc' <- sc defs (toClosure defaultOpts env (Erased fc False))
|
||||
concrete defs env sc'
|
||||
if !(needsDelay (elabMode elabinfo) kr arg_in) then do
|
||||
if (isHole aty && kr) || !(needsDelay (elabMode elabinfo) kr arg_in) then do
|
||||
nm <- genMVName x
|
||||
empty <- clearDefs defs
|
||||
metaty <- quote empty env aty
|
||||
@ -385,12 +385,16 @@ mutual
|
||||
-- better way that leads to good code...)
|
||||
logTerm 5 ("Solving " ++ show metaval ++ " with") argv
|
||||
ok <- solveIfUndefined env metaval argv
|
||||
when (not ok) $
|
||||
do res <- convert fc elabinfo env (gnf env metaval)
|
||||
-- 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)
|
||||
(gnf env argv)
|
||||
let [] = constraints res
|
||||
| cs => throw (CantConvert fc env metaval argv)
|
||||
pure ()
|
||||
let [] = constraints res
|
||||
| cs => do tmty <- getTerm gty
|
||||
newConstant fc rig env tm tmty cs
|
||||
pure tm
|
||||
else pure tm
|
||||
case elabMode elabinfo of
|
||||
InLHS _ => -- reset hole and redo it with the unexpanded definition
|
||||
do updateDef (Resolved idx) (const (Just (Hole 0 False)))
|
||||
|
||||
@ -10,6 +10,7 @@ import Core.TT
|
||||
import Core.Value
|
||||
|
||||
import TTImp.Elab.Check
|
||||
import TTImp.Elab.Delayed
|
||||
import TTImp.TTImp
|
||||
|
||||
%default covering
|
||||
@ -192,13 +193,13 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty
|
||||
-- try checking at Rig1 (meaning that we're using a linear variable
|
||||
-- so the resulting binding should be linear)
|
||||
(valv, valt, rigb) <- handle
|
||||
(do c <- check (rigMult rigl rigc)
|
||||
(do c <- runDelays $ check (rigMult rigl rigc)
|
||||
(record { preciseInf = True } elabinfo)
|
||||
nest env nVal (Just (gnf env tyv))
|
||||
pure (fst c, snd c, rigMult rigl rigc))
|
||||
(\err => case err of
|
||||
LinearMisuse _ _ Rig1 _
|
||||
=> do c <- check Rig1 elabinfo
|
||||
=> do c <- runDelays $ check Rig1 elabinfo
|
||||
nest env nVal (Just (gnf env tyv))
|
||||
pure (fst c, snd c, Rig1)
|
||||
e => do c <- check (rigMult rigl rigc)
|
||||
|
||||
@ -315,7 +315,6 @@ checkCase rig elabinfo nest env fc scr scrty_exp alts exp
|
||||
= delayElab fc rig env exp $
|
||||
do (scrtyv, scrtyt) <- check Rig0 elabinfo nest env scrty_exp
|
||||
(Just (gType fc))
|
||||
|
||||
logTerm 10 "Expected scrutinee type" scrtyv
|
||||
-- Try checking at the given multiplicity; if that doesn't work,
|
||||
-- try checking at Rig1 (meaning that we're using a linear variable
|
||||
@ -326,14 +325,15 @@ checkCase rig elabinfo nest env fc scr scrty_exp alts exp
|
||||
log 5 $ "Checking " ++ show scr ++ " at " ++ show chrig
|
||||
|
||||
(scrtm_in, gscrty, caseRig) <- handle
|
||||
(do c <- check chrig elabinfo nest env scr (Just (gnf env scrtyv))
|
||||
(do c <- runDelays $ check chrig elabinfo nest env scr (Just (gnf env scrtyv))
|
||||
pure (fst c, snd c, chrig))
|
||||
(\err => case err of
|
||||
LinearMisuse _ _ Rig1 _
|
||||
=> do c <- check Rig1 elabinfo nest env scr
|
||||
=> do c <- runDelays $ check Rig1 elabinfo nest env scr
|
||||
(Just (gnf env scrtyv))
|
||||
pure (fst c, snd c, Rig1)
|
||||
e => throw e)
|
||||
|
||||
scrty <- getTerm gscrty
|
||||
logTermNF 5 "Scrutinee type" env scrty
|
||||
defs <- get Ctxt
|
||||
@ -347,4 +347,3 @@ checkCase rig elabinfo nest env fc scr scrty_exp alts exp
|
||||
checkConcrete (NApp _ (NMeta n i _) _)
|
||||
= throw (GenericMsg (getFC scr) "Can't infer type for case scrutinee")
|
||||
checkConcrete _ = pure ()
|
||||
|
||||
|
||||
@ -22,6 +22,11 @@ import Data.StringMap
|
||||
public export
|
||||
data ElabMode = InType | InLHS RigCount | InExpr
|
||||
|
||||
Show ElabMode where
|
||||
show InType = "InType"
|
||||
show (InLHS c) = "InLHS " ++ show c
|
||||
show InExpr = "InExpr"
|
||||
|
||||
public export
|
||||
data ElabOpt
|
||||
= HolesOkay
|
||||
@ -444,6 +449,7 @@ successful ((tm, elab) :: elabs)
|
||||
est' <- get EST
|
||||
md' <- get MD
|
||||
defs' <- get Ctxt
|
||||
|
||||
-- Reset to previous state and try the rest
|
||||
put UST ust
|
||||
put EST est
|
||||
@ -549,13 +555,14 @@ convertWithLazy
|
||||
FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->
|
||||
Core UnifyResult
|
||||
convertWithLazy withLazy prec fc elabinfo env x y
|
||||
= let umode : UnifyMode
|
||||
= let umode : UnifyInfo
|
||||
= case elabMode elabinfo of
|
||||
InLHS _ => InLHS
|
||||
_ => InTerm (Top prec) in
|
||||
InLHS _ => inLHS
|
||||
_ => inTermP prec in
|
||||
catch
|
||||
(do let lazy = !isLazyActive && withLazy
|
||||
logGlueNF 5 ("Unifying " ++ show withLazy) env x
|
||||
logGlueNF 5 ("Unifying " ++ show withLazy ++ " "
|
||||
++ show (elabMode elabinfo)) env x
|
||||
logGlueNF 5 "....with" env y
|
||||
vs <- if isFromTerm x && isFromTerm y
|
||||
then do xtm <- getTerm x
|
||||
|
||||
@ -66,13 +66,7 @@ delayOnFailure fc rig env expected pred elab
|
||||
log 10 ("Due to error " ++ show err)
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab $=
|
||||
((ci, mkClosedElab fc env
|
||||
(do est <- get EST
|
||||
put EST (record { allowDelay = False } est)
|
||||
tm <- elab True
|
||||
est <- get EST
|
||||
put EST (record { allowDelay = True } est)
|
||||
pure tm)) :: ) }
|
||||
((ci, mkClosedElab fc env (elab True)) :: ) }
|
||||
ust)
|
||||
pure (dtm, expected)
|
||||
else throw err)
|
||||
@ -98,13 +92,7 @@ delayElab {vars} fc rig env exp elab
|
||||
" for") env expected
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab $=
|
||||
((ci, mkClosedElab fc env
|
||||
(do est <- get EST
|
||||
put EST (record { allowDelay = False } est)
|
||||
tm <- elab
|
||||
est <- get EST
|
||||
put EST (record { allowDelay = True } est)
|
||||
pure tm)) :: ) }
|
||||
((ci, mkClosedElab fc env elab) :: ) }
|
||||
ust)
|
||||
pure (dtm, expected)
|
||||
where
|
||||
@ -127,11 +115,37 @@ retryDelayed ((i, elab) :: ds)
|
||||
Just Delayed <- lookupDefExact (Resolved i) (gamma defs)
|
||||
| _ => retryDelayed ds
|
||||
log 5 ("Retrying delayed hole " ++ show !(getFullName (Resolved i)))
|
||||
-- elab itself might have delays internally, so keep track of them
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab = [] } ust)
|
||||
tm <- elab
|
||||
ust <- get UST
|
||||
let ds' = reverse (delayedElab ust) ++ ds
|
||||
|
||||
updateDef (Resolved i) (const (Just
|
||||
(PMDef (MkPMDefInfo NotHole True) [] (STerm tm) (STerm tm) [])))
|
||||
logTerm 5 ("Resolved delayed hole " ++ show i) tm
|
||||
logTermNF 5 ("Resolved delayed hole NF " ++ show i) [] tm
|
||||
removeHole i
|
||||
retryDelayed ds
|
||||
retryDelayed ds'
|
||||
|
||||
-- Run an elaborator, then all the delayed elaborators arising from it
|
||||
export
|
||||
runDelays : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
Core a -> Core a
|
||||
runDelays elab
|
||||
= do ust <- get UST
|
||||
let olddelayed = delayedElab ust
|
||||
put UST (record { delayedElab = [] } ust)
|
||||
tm <- elab
|
||||
ust <- get UST
|
||||
catch (retryDelayed (reverse (delayedElab ust)))
|
||||
(\err =>
|
||||
do ust <- get UST
|
||||
put UST (record { delayedElab = olddelayed } ust)
|
||||
throw err)
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab = olddelayed } ust)
|
||||
pure tm
|
||||
|
||||
@ -139,8 +139,8 @@ bindUnsolved {vars} fc elabmode _
|
||||
!(normaliseHoles defs env exp)
|
||||
logTerm 5 ("Added unbound implicit") bindtm
|
||||
unify (case elabmode of
|
||||
InLHS _ => InLHS
|
||||
_ => InTerm (Top False))
|
||||
InLHS _ => inLHS
|
||||
_ => inTermP False)
|
||||
fc env tm bindtm
|
||||
pure ()
|
||||
|
||||
@ -292,12 +292,12 @@ getToBind fc elabmode NONE env excepts
|
||||
= pure [] -- We should probably never get here, but for completeness...
|
||||
getToBind {vars} fc elabmode impmode env excepts
|
||||
= do solveConstraints (case elabmode of
|
||||
InLHS _ => InLHS
|
||||
_ => InTerm (Top False)) Normal
|
||||
InLHS _ => inLHS
|
||||
_ => inTermP False) Normal
|
||||
bindUnsolved fc elabmode impmode
|
||||
solveConstraints (case elabmode of
|
||||
InLHS _ => InLHS
|
||||
_ => InTerm (Top False)) Normal
|
||||
InLHS _ => inLHS
|
||||
_ => inTermP False) Normal
|
||||
defs <- get Ctxt
|
||||
est <- get EST
|
||||
let tob = reverse $ filter (\x => not (fst x `elem` excepts)) $
|
||||
@ -459,16 +459,18 @@ checkBindHere rig elabinfo nest env fc bindmode tm exp
|
||||
-- Set the binding environment in the elab state - unbound
|
||||
-- implicits should have access to whatever is in scope here
|
||||
put EST (updateEnv env SubRefl [] est)
|
||||
constart <- getNextEntry
|
||||
(tmv, tmt) <- check rig (record { implicitMode = bindmode,
|
||||
bindingVars = True }
|
||||
elabinfo)
|
||||
nest env tm exp
|
||||
solveConstraints (case elabMode elabinfo of
|
||||
InLHS c => InLHS
|
||||
_ => InTerm (Top False)) Normal
|
||||
solveConstraints (case elabMode elabinfo of
|
||||
InLHS c => InLHS
|
||||
_ => InTerm (Top False)) Defaults
|
||||
InLHS c => inLHS
|
||||
_ => inTermP False) Normal
|
||||
solveConstraintsAfter constart
|
||||
(case elabMode elabinfo of
|
||||
InLHS c => inLHS
|
||||
_ => inTermP False) Defaults
|
||||
ust <- get UST
|
||||
catch (retryDelayed (delayedElab ust))
|
||||
(\err =>
|
||||
|
||||
@ -45,8 +45,8 @@ checkDelay rig elabinfo nest env fc tm mexpected
|
||||
pure (gnf env ty))
|
||||
pure mexpected
|
||||
let solvemode = case elabMode elabinfo of
|
||||
InLHS c => InLHS
|
||||
_ => InTerm (Top False)
|
||||
InLHS c => inLHS
|
||||
_ => inTermP False
|
||||
solveConstraints solvemode Normal
|
||||
-- Can only check if we know the expected type already because we
|
||||
-- need to infer the delay reason
|
||||
|
||||
@ -185,8 +185,8 @@ checkUpdate rig elabinfo nest env fc upds rec expected
|
||||
nest env rec Nothing
|
||||
pure ty
|
||||
let solvemode = case elabMode elabinfo of
|
||||
InLHS c => InLHS
|
||||
_ => InTerm (Top False)
|
||||
InLHS c => inLHS
|
||||
_ => inTermP False
|
||||
delayOnFailure fc rig env recty needType $
|
||||
\delayed =>
|
||||
do solveConstraints solvemode Normal
|
||||
|
||||
@ -124,7 +124,7 @@ searchName fc rigc opts env target topty defining (n, ndef)
|
||||
(args, appTy) <- mkArgs fc rigc env nty
|
||||
logNF 5 "Target" env target
|
||||
logNF 10 "App type" env appTy
|
||||
ures <- unify InSearch fc env target appTy
|
||||
ures <- unify inSearch fc env target appTy
|
||||
let [] = constraints ures
|
||||
| _ => pure []
|
||||
-- Search the explicit arguments first, they may resolve other holes
|
||||
|
||||
@ -2,7 +2,6 @@ test3ok : Nat
|
||||
test3ok = case (the Nat 1, the Nat 2) of
|
||||
(x, y) => x + y
|
||||
|
||||
test3bad : Nat
|
||||
test3bad = case (1, 2) of
|
||||
test3ok' : Nat
|
||||
test3ok' = case (1, 2) of
|
||||
(x, y) => x + y
|
||||
|
||||
|
||||
@ -1,10 +1,4 @@
|
||||
1/1: Building CaseInf (CaseInf.idr)
|
||||
CaseInf.idr:7:24--9:1:While processing right hand side of test3bad at CaseInf.idr:6:1--9:1:
|
||||
While processing right hand side of case block in test3bad at CaseInf.idr:7:14--9:1:
|
||||
When unifying Integer and Nat
|
||||
Mismatch between:
|
||||
Integer
|
||||
and
|
||||
Nat
|
||||
Main> S (S (S Z))
|
||||
Main> S (S (S Z))
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,2 +1,3 @@
|
||||
test3ok
|
||||
test3ok'
|
||||
:q
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
1/1: Building Error (Error.idr)
|
||||
Error.idr:6:19--7:1:While processing right hand side of wrong at Error.idr:6:1--7:1:
|
||||
When unifying a and Vect ?k a
|
||||
When unifying a and Vect ?k ?a
|
||||
Mismatch between:
|
||||
a
|
||||
and
|
||||
Vect ?k a
|
||||
Vect ?k ?a
|
||||
|
||||
@ -3,4 +3,4 @@ data Vect : Nat -> Type -> Type where
|
||||
(::) : a -> Vect k a -> Vect (S k) a
|
||||
|
||||
wrong : a -> Vect (S n) a -> Vect (S n) a
|
||||
wrong xs = x :: xs
|
||||
wrong xs = x :: ys
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
1/1: Building Error (Error.idr)
|
||||
Error.idr:6:12--6:14:While processing right hand side of wrong at Error.idr:6:1--7:1:
|
||||
Undefined name x
|
||||
Error.idr:6:17--7:1:While processing right hand side of wrong at Error.idr:6:1--7:1:
|
||||
Undefined name ys
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
1/1: Building IEdit (IEdit.idr)
|
||||
Main> empties : (m : Nat) -> Vect m (Vect Z a)
|
||||
empties m
|
||||
Main> transposeHelper : Vect k (Vect m a) -> Vect m a -> Vect m (Vect k a) -> Vect m (Vect (S k) a)
|
||||
transposeHelper xs x xs_trans
|
||||
Main> transposeHelper : Vect m a -> Vect k (Vect m a) -> Vect m (Vect k a) -> Vect m (Vect (S k) a)
|
||||
transposeHelper x xs xs_trans
|
||||
Main> Bye for now!
|
||||
|
||||
@ -3,14 +3,14 @@ Main> (y @@ res) => ?now_4
|
||||
Main> (True @@ d) => ?now_4
|
||||
(False @@ d) => ?now_5
|
||||
Main> 0 m : Type -> Type
|
||||
x : Integer
|
||||
1 d : Door Open
|
||||
x : Integer
|
||||
0 r : Res Bool (\r => (Door (if r then Open else Closed)))
|
||||
-------------------------------------
|
||||
now_2 : Use Many m ()
|
||||
Main> 0 m : Type -> Type
|
||||
x : Integer
|
||||
1 d : Door Closed
|
||||
x : Integer
|
||||
0 r : Res Bool (\r => (Door (if r then Open else Closed)))
|
||||
-------------------------------------
|
||||
now_3 : Use Many m ()
|
||||
|
||||
@ -6,10 +6,10 @@ IFace> Bye for now!
|
||||
2/2: Building IFace1 (IFace1.idr)
|
||||
IFace1> 0 a : Type
|
||||
0 p : a -> Type
|
||||
l' : a
|
||||
r : p l'
|
||||
r' : p l'
|
||||
l : a
|
||||
r' : p l
|
||||
r : p l
|
||||
l' : a
|
||||
-------------------------------------
|
||||
foo : Bool
|
||||
IFace1> Bye for now!
|
||||
|
||||
@ -2,9 +2,9 @@
|
||||
Main> 0 v : Type
|
||||
0 k' : Type
|
||||
0 k : Type
|
||||
z : List (k', v)
|
||||
y : v
|
||||
x : k'
|
||||
y : v
|
||||
z : List (k', v)
|
||||
-------------------------------------
|
||||
bang : List (k', v)
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
1/1: Building Main (Main.idr)
|
||||
Main.idr:27:37--27:72:While processing right hand side of dpairWithExtraInfoBad at Main.idr:27:1--28:1:
|
||||
Main.idr:27:26--27:72:While processing right hand side of dpairWithExtraInfoBad at Main.idr:27:1--28:1:
|
||||
When unifying [MN (fromInteger 0), MN (fromInteger 0)] and [MN (fromInteger 0)]
|
||||
Mismatch between:
|
||||
[MN (fromInteger 0)]
|
||||
|
||||
@ -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:24} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect {k:24}) a) (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:24}) 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 n 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:24} Main.Nat (%pi RigW Explicit Nothing ((Main.Vect {k:24}) a) (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus {k:24}) 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 n 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 [Just a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Integer]) 1) (Main.Vect.Nil [Just a = Integer])))
|
||||
Yaffle> ((Main.MkInfer [Just a = (Main.List.List Integer)]) (((Main.List.Cons [Just a = Integer]) 1) (Main.List.Nil [Just a = Integer])))
|
||||
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved116 ?Main.{a:54}_[]), ($resolved98 ?Main.{a:54}_[])]
|
||||
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved117 ?Main.{a:59}_[]), ($resolved98 ?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':
|
||||
($resolved142 [__] [__] (Main.FZ [__]) {arg:3})
|
||||
($resolved144 [__] [__] (Main.FZ [__]) {arg:3})
|
||||
Yaffle> Main.lookup'': Calls non covering function Main.lookup'
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
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:17} Main.Nat (%pi Rig0 Explicit Just ws ((Main.Vect {k:17}) a) (%pi Rig0 Explicit Just y a (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:17})) a) (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:17}))) m)) a))))))))))
|
||||
Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:45} Main.Nat (%pi Rig1 Explicit Just zs ((Main.Vect {k:45}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:45})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:45})) m)) a)))))))))
|
||||
Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:74} Main.Nat (%pi Rig0 Explicit Just zs ((Main.Vect {k:74}) a) (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:74})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:74}) a) ((Main.Vect ((Main.plus (Main.S {k:74})) m)) a))))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:19} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just y a (%pi Rig0 Explicit Just ws ((Main.Vect {k:19}) a) (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:19})) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:19}))) m)) a))))))))))
|
||||
Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:48} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect {k:48}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:48})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:48})) m)) a)))))))))
|
||||
Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:78} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just zs ((Main.Vect {k:78}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:78})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:78}) a) ((Main.Vect ((Main.plus (Main.S {k:78})) m)) a))))))))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> (((((Main.There [Just {type_of_y:14} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:8} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
|
||||
Yaffle> (((Main.Here [Just {a:8} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
|
||||
Yaffle> (((((Main.There [Just {a:15} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:9} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
|
||||
Yaffle> (((Main.Here [Just {a:9} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
|
||||
Yaffle> ((((Main.MkPair [Just b = Integer]) [Just a = String]) "b") 94)
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \ys : (Main.Vect m[1] a[0]) => \0 n : Main.Nat => ys[1]
|
||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:28} : Main.Nat => \xs : (Main.Vect {k:28}[0] a[1]) => \x : a[2] => \ys : (Main.Vect m[4] a[3]) => \0 n : Main.Nat => (Main.Cons (Main.plus {k:28}[4] m[6]) a[5] x[2] (Main.append m[6] a[5] {k:28}[4] xs[3] ys[1]))
|
||||
Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:199}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:199}]) z) y))]
|
||||
Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:309}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:309}]) z) w))]
|
||||
Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:459}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:459}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))]
|
||||
Yaffle> \0 m : Main.Nat => \0 a : Type => \0 {k:29} : Main.Nat => \x : a[1] => \xs : (Main.Vect {k:29}[1] a[2]) => \ys : (Main.Vect m[4] a[3]) => \0 n : Main.Nat => (Main.Cons (Main.plus {k:29}[4] m[6]) a[5] x[3] (Main.append m[6] a[5] {k:29}[4] xs[2] ys[1]))
|
||||
Yaffle> [((Main.app2 (Main.Nil [Just a = _])) $y) = y, ((Main.app2 ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) $y) = ((((Main.Cons [Just k = ((Main.plus {_:201}) m)]) [Just a = a]) x) (((((Main.app2 [Just m = m]) [Just a = a]) [Just n = {_:201}]) z) y))]
|
||||
Yaffle> [((Main.zip (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = ((Main.Pair a) b)]), ((Main.zip ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:314}]) [Just a = ((Main.Pair a) b)]) ((((Main.MkPair [Just b = b]) [Just a = a]) x) y)) (((((Main.zip [Just b = b]) [Just a = a]) [Just n = {_:314}]) z) w))]
|
||||
Yaffle> [(((Main.zipWith $f) (Main.Nil [Just a = _])) $y) = (Main.Nil [Just a = c]), (((Main.zipWith $f) ((((Main.Cons [Just k = _]) [Just a = _]) $x) $z)) ((((Main.Cons [Just k = _]) [Just a = _]) $y) $w)) = ((((Main.Cons [Just k = {_:464}]) [Just a = c]) ((f x) y)) (((((((Main.zipWith [Just n = {_:464}]) [Just c = c]) [Just b = b]) [Just a = a]) f) z) w))]
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -13,4 +13,3 @@ fourNotInVector (There (There (There (There _)))) impossible
|
||||
peteNotInVector : Elem "Pete" ["John", "Paul", "George", "Ringo"] -> Void
|
||||
peteNotInVector (There (There (There (There Here)))) impossible
|
||||
peteNotInVector (There (There (There (There (There _))))) impossible
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user