Skip to content

Commit

Permalink
Fix ordering of unification rules
Browse files Browse the repository at this point in the history
  • Loading branch information
@edwinb
edwinb committed May 15, 2023
1 parent 4c1e2ff commit 74d70b3
Show file tree
Hide file tree
Showing 3 changed files with 149 additions and 72 deletions.
3 changes: 0 additions & 3 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,9 +102,6 @@ papers: contrib linear
bootstrap-libs : prelude base linear network
libs: prelude base contrib linear network test-lib
#libs : prelude base contrib network test-lib linear papers
# TODO: no libs yet! Put clean-libs and install-libs back too
# (or maybe placeholder libs directories?)
libs :

libdocs:
${MAKE} -C libs/prelude docs IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
Expand Down
68 changes: 68 additions & 0 deletions src/Core/Unify/State.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -623,3 +623,71 @@ parameters {auto c : Ref Ctxt Defs} {auto u : Ref UST UState}
export
checkNoGuards : Core ()
checkNoGuards = checkUserHoles False

export
dumpHole : (s : String) ->
{auto 0 _ : KnownTopic s} ->
Nat -> (hole : Int) -> Core ()
dumpHole str n hole
= do ust <- get UST
defs <- get Ctxt
case !(lookupCtxtExact (Resolved hole) (gamma defs)) of
Nothing => pure ()
Just gdef => case (definition gdef, type gdef) of
(Guess tm envb constraints, ty) =>
do logString str n $
"!" ++ show !(getFullName (Resolved hole)) ++ " : "
++ show !(toFullNames !(normaliseHoles [<] ty))
++ "\n\t = "
++ show !(normaliseHoles [<] tm)
++ "\n\twhen"
traverse_ dumpConstraint constraints
(Hole _ p, ty) =>
logString str n $
"?" ++ show (fullname gdef) ++ " : "
++ show !(normaliseHoles [<] ty)
++ if implbind p then " (ImplBind)" else ""
++ if invertible gdef then " (Invertible)" else ""
(BySearch _ _ _, ty) =>
logString str n $
"Search " ++ show hole ++ " : " ++
show !(toFullNames !(normaliseHoles [<] ty))
(ImpBind, ty) =>
log str 4 $
"Bound: " ++ show hole ++ " : " ++
show !(normalise [<] ty)
(Delayed, ty) =>
log str 4 $
"Delayed elaborator : " ++
show !(normalise [<] ty)
_ => pure ()
where
dumpConstraint : Int -> Core ()
dumpConstraint cid
= do ust <- get UST
defs <- get Ctxt
case lookup cid (constraints ust) of
Nothing => pure ()
Just Resolved => logString str n "\tResolved"
Just (MkConstraint _ lazy env x y) =>
do logString str n $
"\t " ++ show !(toFullNames x)
++ " =?= " ++ show !(toFullNames y)
Just (MkSeqConstraint _ _ xs ys) =>
logString str n $ "\t\t" ++ show xs ++ " =?= " ++ show ys

export
dumpConstraints : (topics : String) ->
{auto 0 _ : KnownTopic topics} ->
(verbosity : Nat) ->
(all : Bool) ->
Core ()
dumpConstraints str n all
= do ust <- get UST
defs <- get Ctxt
when !(logging str n) $ do
let hs = toList (guesses ust) ++
toList (if all then holes ust else currentHoles ust)
unless (isNil hs) $
do logString str n "--- CONSTRAINTS AND HOLES ---"
traverse_ (dumpHole str n) (map fst hs)
150 changes: 81 additions & 69 deletions src/Core/Unify/Unify.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -440,111 +440,71 @@ parameters {auto c : Ref Ctxt Defs} {auto u : Ref UST UState}
unifyNoEta : {vars : _} ->
UnifyInfo -> FC -> Env Term vars ->
Value f vars -> Value f' vars -> Core UnifyResult
unifyNoEta mode fc env (VAs _ _ _ x) y = unifyNoEta mode fc env !(expand x) y
unifyNoEta mode fc env x (VAs _ _ _ y) = unifyNoEta mode fc env x !(expand y)
-- Deal with metavariable cases first
-- If they're both holes, solve the one with the bigger context
unifyNoEta mode fc env x@(VMeta fcx nx ix margsx argsx _) y@(VMeta fcy ny iy margsy argsy _)
= do -- First check if they're convertible already, in which case
-- we've won already
log "elab" 10 ("Unifying metas " ++ show nx ++ " and " ++ show ny)
False <- convert env x y
| _ => pure success
invx <- isDefInvertible fc ix
if ix == iy && (invx || umode mode == InSearch)
-- Invertible, (from auto implicit search)
-- so we can also unify the arguments.
then unifyArgs mode fc env
(map snd margsx ++ spineToValues argsx)
(map snd margsy ++ spineToValues argsy)
else do xvs <- traverse (\ (c, t) => pure (c, asGlued !(expand !t))) margsx
yvs <- traverse (\ (c, t) => pure (c, asGlued !(expand !t))) margsy
let xlocs = localsIn (map snd xvs)
let ylocs = localsIn (map snd yvs)
-- Solve the one with the bigger context, and if they're
-- equal, the one that's applied to fewest things (because
-- then the arguments get substituted in)
let xbigger = xlocs > ylocs
|| (xlocs == ylocs &&
length argsx <= length argsy)
if (xbigger || umode mode == InMatch) && not (pv nx)
then unifyHole False mode fc env fcx nx ix (map toCore xvs) argsx (asGlued y)
else unifyHole True mode fc env fcy ny iy (map toCore yvs) argsy (asGlued x)
where
toCore : (a, b) -> (a, Core b)
toCore (x, y) = (x, pure y)

pv : Name -> Bool
pv (PV _ _) = True
pv _ = False

localsIn : List (Value f vars) -> Nat
localsIn [] = 0
localsIn (VLocal{} :: xs) = 1 + localsIn xs
localsIn (_ :: xs) = localsIn xs
unifyNoEta mode fc env (VMeta fcm n i margs args _) tm
= unifyHole False mode fc env fcm n i margs args (asGlued tm)
unifyNoEta mode fc env tm (VMeta fcm n i margs args _)
= unifyHole True mode fc env fcm n i margs args (asGlued tm)
unifyNotMetavar : {vars : _} ->
UnifyInfo -> FC -> Env Term vars ->
Value f vars -> Value f' vars -> Core UnifyResult
unifyNotMetavar mode fc env (VAs _ _ _ x) y = unifyNoEta mode fc env !(expand x) y
unifyNotMetavar mode fc env x (VAs _ _ _ y) = unifyNoEta mode fc env x !(expand y)
-- Unifying applications means we're stuck and need to postpone, since we've
-- already checked convertibility
-- In 'match' or 'search' mode, we can nevertheless unify the arguments
-- if the names match.
unifyNoEta mode@(MkUnifyInfo p InSearch) fc env x@(VApp _ _ nx spx _) y@(VApp _ _ ny spy _)
unifyNotMetavar mode@(MkUnifyInfo p InSearch) fc env x@(VApp _ _ nx spx _) y@(VApp _ _ ny spy _)
= if nx == ny
then unifySpine mode fc env spx spy
else postpone fc mode "Postponing application (search)" env x y
unifyNoEta mode@(MkUnifyInfo p InMatch) fc env x@(VApp _ _ nx spx _) y@(VApp _ _ ny spy _)
unifyNotMetavar mode@(MkUnifyInfo p InMatch) fc env x@(VApp _ _ nx spx _) y@(VApp _ _ ny spy _)
= if nx == ny
then unifySpine mode fc env spx spy
else postpone fc mode "Postponing application (match)" env x y
unifyNoEta mode fc env x@(VApp{}) y
-- conversion check first, in case app is a blocked case
= if !(convert env x y)
then pure success
else postpone fc mode "Postponing application (left)" env x y
unifyNoEta mode fc env x y@(VApp{})
= if !(convert env x y)
then pure success
else postpone fc mode "Postponing application (right)" env x y
-- Now the cases where we're decomposing into smaller problems
unifyNoEta mode@(MkUnifyInfo p InTerm) fc env x@(VLocal fcx idx _ spx)
unifyNotMetavar mode@(MkUnifyInfo p InTerm) fc env x@(VLocal fcx idx _ spx)
y@(VLocal fcy idy _ spy)
= if idx == idy
then unifySpine mode fc env spx spy
else postpone fc mode "Postponing local app"
env x y
unifyNoEta mode@(MkUnifyInfo p InMatch) fc env x@(VLocal fcx idx _ spx)
unifyNotMetavar mode@(MkUnifyInfo p InMatch) fc env x@(VLocal fcx idx _ spx)
y@(VLocal fcy idy _ spy)
= if idx == idy
then unifySpine mode fc env spx spy
else postpone fc mode "Postponing local app"
env x y
unifyNoEta mode fc env x@(VDCon fcx nx tx ax spx) y@(VDCon fcy ny ty ay spy)
unifyNotMetavar mode fc env x@(VDCon fcx nx tx ax spx) y@(VDCon fcy ny ty ay spy)
= if tx == ty
then unifySpine mode fc env spx spy
else convertError fc env x y
unifyNoEta mode fc env x@(VTCon fcx nx ax spx) y@(VTCon fcy ny ay spy)
unifyNotMetavar mode fc env x@(VTCon fcx nx ax spx) y@(VTCon fcy ny ay spy)
= if nx == ny
then unifySpine mode fc env spx spy
else convertError fc env x y
unifyNoEta mode fc env (VDelayed _ _ x) (VDelayed _ _ y)
unifyNotMetavar mode fc env (VDelayed _ _ x) (VDelayed _ _ y)
= unify (lower mode) fc env x y
unifyNoEta mode fc env (VDelay _ _ tx ax) (VDelay _ _ ty ay)
unifyNotMetavar mode fc env (VDelay _ _ tx ax) (VDelay _ _ ty ay)
= unifyArgs (lower mode) fc env [pure tx,pure ax] [pure ty,pure ay]
unifyNoEta mode fc env (VForce _ _ vx spx) (VForce _ _ vy spy)
unifyNotMetavar mode fc env (VForce _ _ vx spx) (VForce _ _ vy spy)
= do cs <- unify (lower mode) fc env vx vy
cs' <- unifySpine (lower mode) fc env spx spy
pure (union cs cs')
unifyNoEta mode fc env x@(VCase{}) y@(VCase{})
unifyNotMetavar mode fc env x@(VCase{}) y@(VCase{})
= unifyIfEq True fc mode env (asGlued x) (asGlued y)
unifyNoEta mode fc env (VErased _ (Dotted x)) (VErased _ (Dotted y))
unifyNotMetavar mode fc env (VErased _ (Dotted x)) (VErased _ (Dotted y))
= unifyNoEta mode fc env !(expand x) !(expand y)
unifyNoEta mode fc env x (VErased _ (Dotted y))
unifyNotMetavar mode fc env x (VErased _ (Dotted y))
= unifyNoEta mode fc env x !(expand y)
unifyNoEta mode fc env (VErased _ (Dotted x)) y
unifyNotMetavar mode fc env (VErased _ (Dotted x)) y
= unifyNoEta mode fc env !(expand x) y
unifyNoEta mode fc env x_in y_in
unifyNotMetavar mode fc env x@(VApp{}) y
-- conversion check first, in case app is a blocked case
= if !(convert env x y)
then pure success
else postpone fc mode "Postponing application (left)" env x y
unifyNotMetavar mode fc env x y@(VApp{})
= if !(convert env x y)
then pure success
else postpone fc mode "Postponing application (right)" env x y
unifyNotMetavar mode fc env x_in y_in
= do x <- expand x_in
y <- expand y_in
unifyIfEq (isPostponable x || isPostponable y) fc mode env (asGlued x) (asGlued y)
Expand All @@ -555,8 +515,55 @@ parameters {auto c : Ref Ctxt Defs} {auto u : Ref UST UState}
isPostponable : NF vars -> Bool
isPostponable (VDelayed{}) = True
isPostponable (VCase{}) = True
isPostponable (VForce{}) = True
isPostponable _ = False

-- Deal with metavariable cases first
-- If they're both holes, solve the one with the bigger context
unifyNoEta mode fc env x@(VMeta fcx nx ix margsx argsx _) y@(VMeta fcy ny iy margsy argsy _)
= do -- First check if they're convertible already, in which case
-- we've won already
log "elab" 10 ("Unifying metas " ++ show nx ++ " and " ++ show ny)
False <- convert env x y
| _ => pure success
invx <- isDefInvertible fc ix
if ix == iy && (invx || umode mode == InSearch)
-- Invertible, (from auto implicit search)
-- so we can also unify the arguments.
then unifyArgs mode fc env
(map snd margsx ++ spineToValues argsx)
(map snd margsy ++ spineToValues argsy)
else do xvs <- traverse (\ (c, t) => pure (c, asGlued !(expand !t))) margsx
yvs <- traverse (\ (c, t) => pure (c, asGlued !(expand !t))) margsy
let xlocs = localsIn (map snd xvs)
let ylocs = localsIn (map snd yvs)
-- Solve the one with the bigger context, and if they're
-- equal, the one that's applied to fewest things (because
-- then the arguments get substituted in)
let xbigger = xlocs > ylocs
|| (xlocs == ylocs &&
length argsx <= length argsy)
if (xbigger || umode mode == InMatch) && not (pv nx)
then unifyHole False mode fc env fcx nx ix (map toCore xvs) argsx (asGlued y)
else unifyHole True mode fc env fcy ny iy (map toCore yvs) argsy (asGlued x)
where
toCore : (a, b) -> (a, Core b)
toCore (x, y) = (x, pure y)

pv : Name -> Bool
pv (PV _ _) = True
pv _ = False

localsIn : List (Value f vars) -> Nat
localsIn [] = 0
localsIn (VLocal{} :: xs) = 1 + localsIn xs
localsIn (_ :: xs) = localsIn xs
unifyNoEta mode fc env (VMeta fcm n i margs args _) tm
= unifyHole False mode fc env fcm n i margs args (asGlued tm)
unifyNoEta mode fc env tm (VMeta fcm n i margs args _)
= unifyHole True mode fc env fcm n i margs args (asGlued tm)
unifyNoEta mode fc env tm tm' = unifyNotMetavar mode fc env tm tm'

mkArg : FC -> Name -> Core (Glued vars)
mkArg fc var = pure $ VApp fc Bound var [<] (pure Nothing)

Expand Down Expand Up @@ -800,7 +807,8 @@ parameters {auto c : Ref Ctxt Defs} {auto c : Ref UST UState}
x <- nf env xold
y <- nf env yold
log "unify" 10 (show loc)
logNF "unify" 5 "Retrying" env x
logNF "unify" 5 ("Retrying " ++ show c ++ " " ++ show (umode mode))
env x
logNF "unify" 5 "....with" env y

catch
Expand Down Expand Up @@ -1018,6 +1026,10 @@ parameters {auto c : Ref Ctxt Defs} {auto c : Ref UST UState}
checkDots
= do ust <- get UST
hs <- getCurrentHoles
log "unify.constraint" 5 ("Dot with " ++
show (length (toList (guesses ust))) ++
" constraints")
dumpConstraints "unify.constraint" 15 True
traverse_ checkConstraint (reverse (dotConstraints ust))
hs <- getCurrentHoles
update UST { dotConstraints := [] }
Expand Down

0 comments on commit 74d70b3

Please sign in to comment.