mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-11 06:14:41 +03:00
[ unify, fix #589 ] Postpone when instantiating if type is unknown
This commit is contained in:
Ruslan Feizerakhmanov
parent
a00fc25109
commit
217c44291a
@ -15,6 +15,7 @@ import Libraries.Data.Bool.Extra
|
||||
import Libraries.Data.IntMap
|
||||
import Data.List
|
||||
import Data.List.Views
|
||||
import Data.Maybe
|
||||
import Libraries.Data.NameMap
|
||||
|
||||
%default covering
|
||||
@ -461,7 +462,7 @@ getIVars (ICons v vs) = v :: getIVars vs
|
||||
-- and returning the term
|
||||
-- If the type of the metavariable doesn't have enough arguments, fail, because
|
||||
-- this wasn't valid for pattern unification
|
||||
instantiate : {auto c : Ref Ctxt Defs} ->
|
||||
tryInstantiate : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{vars, newvars : _} ->
|
||||
FC -> UnifyInfo -> Env Term vars ->
|
||||
@ -470,8 +471,8 @@ instantiate : {auto c : Ref Ctxt Defs} ->
|
||||
List (Var newvars) -> -- Variable each argument maps to
|
||||
Term vars -> -- original, just for error message
|
||||
Term newvars -> -- shrunk environment
|
||||
Core ()
|
||||
instantiate {newvars} loc mode env mname mref num mdef locs otm tm
|
||||
Core Bool -- postpone if the type is yet unknown
|
||||
tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
|
||||
= do logTerm "unify.instantiate" 5 ("Instantiating in " ++ show newvars) tm
|
||||
-- let Hole _ _ = definition mdef
|
||||
-- | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def)
|
||||
@ -486,7 +487,11 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
|
||||
log "unify.instantiate" 5 ("From vars: " ++ show newvars)
|
||||
|
||||
defs <- get Ctxt
|
||||
rhs <- mkDef locs INil tm ty
|
||||
-- Try to instantiate the hole
|
||||
Just rhs <- mkDef locs INil tm ty
|
||||
| _ => do
|
||||
log "unify.instantiate" 5 "Postponed"
|
||||
pure False
|
||||
|
||||
logTerm "unify.instantiate" 5 "Definition" rhs
|
||||
let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs)
|
||||
@ -495,6 +500,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
|
||||
} mdef
|
||||
ignore $ addDef (Resolved mref) newdef
|
||||
removeHole mref
|
||||
pure True
|
||||
where
|
||||
precise : Bool
|
||||
precise
|
||||
@ -579,22 +585,22 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
|
||||
mkDef : {vs, newvars : _} ->
|
||||
List (Var newvars) ->
|
||||
IVars vs newvars -> Term newvars -> Term vs ->
|
||||
Core (Term vs)
|
||||
Core (Maybe (Term vs))
|
||||
mkDef (v :: vs) vars soln (Bind bfc x (Pi fc c _ ty) sc)
|
||||
= do sc' <- mkDef vs (ICons (Just v) vars) soln sc
|
||||
pure $ Bind bfc x (Lam fc c Explicit (Erased bfc False)) sc'
|
||||
pure $ (Bind bfc x (Lam fc c Explicit (Erased bfc False)) <$> sc')
|
||||
mkDef vs vars soln (Bind bfc x b@(Let _ c val ty) sc)
|
||||
= do sc' <- mkDef vs (ICons Nothing vars) soln sc
|
||||
let Just scs = shrinkTerm sc' (DropCons SubRefl)
|
||||
| Nothing => pure $ Bind bfc x b sc'
|
||||
pure scs
|
||||
mkDef [] vars soln ty
|
||||
= do mbsc' <- mkDef vs (ICons Nothing vars) soln sc
|
||||
flip traverseOpt mbsc' \sc' =>
|
||||
case shrinkTerm sc' (DropCons SubRefl) of
|
||||
Just scs => pure scs
|
||||
Nothing => pure $ Bind bfc x b sc'
|
||||
mkDef [] vars soln _
|
||||
= do let Just soln' = updateIVars vars soln
|
||||
| Nothing => ufail loc ("Can't make solution for " ++ show mname
|
||||
++ " " ++ show (getIVars vars, soln))
|
||||
pure soln'
|
||||
mkDef _ _ _ ty = ufail loc $ "Can't make solution for " ++ show mname
|
||||
++ " at " ++ show ty
|
||||
pure (Just soln')
|
||||
mkDef _ _ _ _ = pure Nothing
|
||||
|
||||
export
|
||||
solveIfUndefined : {vars : _} ->
|
||||
@ -613,8 +619,7 @@ solveIfUndefined env (Meta fc mname idx args) soln
|
||||
Just stm =>
|
||||
do Just hdef <- lookupCtxtExact (Resolved idx) (gamma defs)
|
||||
| Nothing => throw (InternalError "Can't happen: no definition")
|
||||
instantiate fc inTerm env mname idx (length args) hdef locs soln stm
|
||||
pure True
|
||||
tryInstantiate fc inTerm env mname idx (length args) hdef locs soln stm
|
||||
solveIfUndefined env metavar soln
|
||||
= pure False
|
||||
|
||||
@ -804,14 +809,14 @@ mutual
|
||||
(solfull : Term vars) -> -- Original solution
|
||||
(soln : Term newvars) -> -- Solution with shrunk environment
|
||||
(solnf : NF vars) ->
|
||||
Core UnifyResult
|
||||
Core (Maybe UnifyResult)
|
||||
solveHole loc mode env mname mref margs margs' locs submv solfull stm solnf
|
||||
= do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
-- if the terms are the same, this isn't a solution
|
||||
-- but they are already unifying, so just return
|
||||
if solutionHeadSame solnf
|
||||
then pure success
|
||||
then pure $ Just success
|
||||
else -- Rather than doing the occurs check here immediately,
|
||||
-- we'll wait until all metavariables are resolved, and in
|
||||
-- the meantime look out for cycles when normalising (which
|
||||
@ -819,8 +824,8 @@ mutual
|
||||
-- metavariables)
|
||||
do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
|
||||
| Nothing => throw (InternalError ("Can't happen: Lost hole " ++ show mname))
|
||||
instantiate loc mode env mname mref (length margs) hdef locs solfull stm
|
||||
pure $ solvedHole mref
|
||||
progress <- tryInstantiate loc mode env mname mref (length margs) hdef locs solfull stm
|
||||
pure $ toMaybe progress (solvedHole mref)
|
||||
where
|
||||
-- Only need to check the head metavar is the same, we've already
|
||||
-- checked the rest if they are the same (and we couldn't instantiate it
|
||||
@ -871,19 +876,24 @@ mutual
|
||||
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
|
||||
tmnf
|
||||
|
||||
let solveOrElsePostpone : Term newvars -> Core UnifyResult
|
||||
solveOrElsePostpone stm = do
|
||||
mbResult <- solveHole fc mode env mname mref
|
||||
margs margs' locs submv
|
||||
tm stm tmnf
|
||||
flip fromMaybe (pure <$> mbResult) $
|
||||
postponeS True swap loc mode "Can't instantiate" env
|
||||
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') tmnf
|
||||
|
||||
case shrinkTerm tm submv of
|
||||
Just stm => solveHole fc mode env mname mref
|
||||
margs margs' locs submv
|
||||
tm stm tmnf
|
||||
Just stm => solveOrElsePostpone stm
|
||||
Nothing =>
|
||||
do tm' <- normalise defs env tm
|
||||
case shrinkTerm tm' submv of
|
||||
Nothing => postponeS True swap loc mode "Can't shrink" env
|
||||
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
|
||||
tmnf
|
||||
Just stm => solveHole fc mode env mname mref
|
||||
margs margs' locs submv
|
||||
tm stm tmnf
|
||||
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
|
||||
tmnf
|
||||
Just stm => solveOrElsePostpone stm
|
||||
|
||||
-- Unify an application with something else
|
||||
unifyApp : {auto c : Ref Ctxt Defs} ->
|
||||
|
||||
@ -161,7 +161,9 @@ idrisTests = MkTestPool []
|
||||
-- The 'with' rule
|
||||
"with001", "with002", "with004",
|
||||
-- with-disambiguation
|
||||
"with003"]
|
||||
"with003",
|
||||
-- unification
|
||||
"unify001"]
|
||||
|
||||
typeddTests : TestPool
|
||||
typeddTests = MkTestPool []
|
||||
|
||||
31
tests/idris2/unify001/Postpone.idr
Normal file
31
tests/idris2/unify001/Postpone.idr
Normal file
@ -0,0 +1,31 @@
|
||||
|
||||
------------- Example 1 ----------------
|
||||
natInjective : (x, y : Nat) -> S x === S y -> x === y
|
||||
natInjective x x Refl = Refl
|
||||
|
||||
succNotZero : (x : Nat) -> Not (S x === Z)
|
||||
succNotZero x Refl impossible
|
||||
|
||||
peanoNat : (a : Type
|
||||
** n0 : a
|
||||
** ns : a -> a
|
||||
** inj : ((x, y : a) -> ns x === ns y -> x === y)
|
||||
** (x : a) -> Not (ns x === n0))
|
||||
peanoNat = MkDPair
|
||||
Nat
|
||||
$ MkDPair
|
||||
Z
|
||||
$ MkDPair -- {a = Nat -> Nat}
|
||||
S
|
||||
$ MkDPair
|
||||
natInjective
|
||||
succNotZero
|
||||
|
||||
------------- Example 2 ----------------
|
||||
ac : forall r. ((x : a) -> (y : b ** r x y)) -> (f : a -> b ** (x : a) -> r x (f x))
|
||||
ac g = (\x => fst (g x) ** \x => snd (g x))
|
||||
|
||||
------------- Example 3 ----------------
|
||||
idid1 : forall A. (f : A -> A ** (x : A) -> f x = x)
|
||||
idid1 = MkDPair id (\x => Refl)
|
||||
|
||||
2
tests/idris2/unify001/expected
Normal file
2
tests/idris2/unify001/expected
Normal file
@ -0,0 +1,2 @@
|
||||
1/1: Building Postpone (Postpone.idr)
|
||||
Main> Bye for now!
|
||||
1
tests/idris2/unify001/input
Normal file
1
tests/idris2/unify001/input
Normal file
@ -0,0 +1 @@
|
||||
:q
|
||||
3
tests/idris2/unify001/run
Executable file
3
tests/idris2/unify001/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 --no-color --console-width 0 --no-banner Postpone.idr < input
|
||||
|
||||
rm -rf build
|
||||
Loading…
Reference in New Issue
Block a user