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

Merge pull request #1718 from edwinb/Russoul-unification

Browse Source 
Postpone when instantiating if type is unknown
This commit is contained in:
Edwin Brady 2021-07-15 21:16:00 +01:00 committed by GitHub
commit 50c0116780
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 81 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
Makefile
View File

@ -107,11 +107,11 @@ ${TEST_PREFIX}/${NAME_VERSION} :
else else
${TEST_PREFIX}/${NAME_VERSION} : ${TEST_PREFIX}/${NAME_VERSION} :
${MAKE} install-support PREFIX=${TEST_PREFIX} ${MAKE} install-support PREFIX=${TEST_PREFIX}
ln -s ${IDRIS2_CURDIR}/libs/prelude/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/prelude-${IDRIS2_VERSION} ln -sf ${IDRIS2_CURDIR}/libs/prelude/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/prelude-${IDRIS2_VERSION}
ln -s ${IDRIS2_CURDIR}/libs/base/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/base-${IDRIS2_VERSION} ln -sf ${IDRIS2_CURDIR}/libs/base/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/base-${IDRIS2_VERSION}
ln -s ${IDRIS2_CURDIR}/libs/test/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/test-${IDRIS2_VERSION} ln -sf ${IDRIS2_CURDIR}/libs/test/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/test-${IDRIS2_VERSION}
ln -s ${IDRIS2_CURDIR}/libs/contrib/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/contrib-${IDRIS2_VERSION} ln -sf ${IDRIS2_CURDIR}/libs/contrib/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/contrib-${IDRIS2_VERSION}
ln -s ${IDRIS2_CURDIR}/libs/network/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/network-${IDRIS2_VERSION} ln -sf ${IDRIS2_CURDIR}/libs/network/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/network-${IDRIS2_VERSION}
endif endif
.PHONY: ${TEST_PREFIX}/${NAME_VERSION} .PHONY: ${TEST_PREFIX}/${NAME_VERSION}

60
src/Core/Unify.idr
View File

@ -14,6 +14,7 @@ import Core.Value
import Data.List import Data.List
import Data.List.Views import Data.List.Views
import Data.Maybe
import Libraries.Data.IntMap import Libraries.Data.IntMap
import Libraries.Data.NameMap import Libraries.Data.NameMap
@ -447,7 +448,7 @@ getIVars (ICons v vs) = v :: getIVars vs
-- and returning the term -- and returning the term
-- If the type of the metavariable doesn't have enough arguments, fail, because -- If the type of the metavariable doesn't have enough arguments, fail, because
-- this wasn't valid for pattern unification -- this wasn't valid for pattern unification
instantiate : {auto c : Ref Ctxt Defs} -> tryInstantiate : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
{vars, newvars : _} -> {vars, newvars : _} ->
FC -> UnifyInfo -> Env Term vars -> FC -> UnifyInfo -> Env Term vars ->
@ -456,8 +457,8 @@ instantiate : {auto c : Ref Ctxt Defs} ->
List (Var newvars) -> -- Variable each argument maps to List (Var newvars) -> -- Variable each argument maps to
Term vars -> -- original, just for error message Term vars -> -- original, just for error message
Term newvars -> -- shrunk environment Term newvars -> -- shrunk environment
Core () Core Bool -- postpone if the type is yet unknown
instantiate {newvars} loc mode env mname mref num mdef locs otm tm tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
= do logTerm "unify.instantiate" 5 ("Instantiating in " ++ show newvars) tm = do logTerm "unify.instantiate" 5 ("Instantiating in " ++ show newvars) tm
-- let Hole _ _ = definition mdef -- let Hole _ _ = definition mdef
-- | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def) -- | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def)
@ -472,7 +473,11 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
log "unify.instantiate" 5 ("From vars: " ++ show newvars) log "unify.instantiate" 5 ("From vars: " ++ show newvars)
defs <- get Ctxt 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 logTerm "unify.instantiate" 5 "Definition" rhs
let simpleDef = MkPMDefInfo (SolvedHole num) let simpleDef = MkPMDefInfo (SolvedHole num)
@ -483,6 +488,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
} mdef } mdef
ignore $ addDef (Resolved mref) newdef ignore $ addDef (Resolved mref) newdef
removeHole mref removeHole mref
pure True
where where
precise : Bool precise : Bool
precise precise
@ -581,22 +587,22 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
mkDef : {vs, newvars : _} -> mkDef : {vs, newvars : _} ->
List (Var newvars) -> List (Var newvars) ->
IVars vs newvars -> Term newvars -> Term vs -> 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) mkDef (v :: vs) vars soln (Bind bfc x (Pi fc c _ ty) sc)
= do sc' <- mkDef vs (ICons (Just v) vars) soln 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) mkDef vs vars soln (Bind bfc x b@(Let _ c val ty) sc)
= do sc' <- mkDef vs (ICons Nothing vars) soln sc = do mbsc' <- mkDef vs (ICons Nothing vars) soln sc
let Just scs = shrinkTerm sc' (DropCons SubRefl) flip traverseOpt mbsc' \sc' =>
| Nothing => pure $ Bind bfc x b sc' case shrinkTerm sc' (DropCons SubRefl) of
pure scs Just scs => pure scs
mkDef [] vars soln ty Nothing => pure $ Bind bfc x b sc'
mkDef [] vars soln _
= do let Just soln' = updateIVars vars soln = do let Just soln' = updateIVars vars soln
| Nothing => ufail loc ("Can't make solution for " ++ show mname | Nothing => ufail loc ("Can't make solution for " ++ show mname
++ " " ++ show (getIVars vars, soln)) ++ " " ++ show (getIVars vars, soln))
pure soln' pure (Just soln')
mkDef _ _ _ ty = ufail loc $ "Can't make solution for " ++ show mname mkDef _ _ _ _ = pure Nothing
++ " at " ++ show ty
export export
solveIfUndefined : {vars : _} -> solveIfUndefined : {vars : _} ->
@ -615,8 +621,7 @@ solveIfUndefined env (Meta fc mname idx args) soln
Just stm => Just stm =>
do Just hdef <- lookupCtxtExact (Resolved idx) (gamma defs) do Just hdef <- lookupCtxtExact (Resolved idx) (gamma defs)
| Nothing => throw (InternalError "Can't happen: no definition") | Nothing => throw (InternalError "Can't happen: no definition")
instantiate fc inTerm env mname idx (length args) hdef locs soln stm tryInstantiate fc inTerm env mname idx (length args) hdef locs soln stm
pure True
solveIfUndefined env metavar soln solveIfUndefined env metavar soln
= pure False = pure False
@ -829,7 +834,7 @@ mutual
(solfull : Term vars) -> -- Original solution (solfull : Term vars) -> -- Original solution
(soln : Term newvars) -> -- Solution with shrunk environment (soln : Term newvars) -> -- Solution with shrunk environment
(solnf : NF vars) -> (solnf : NF vars) ->
Core UnifyResult Core (Maybe UnifyResult)
solveHole loc mode env mname mref margs margs' locs submv solfull stm solnf solveHole loc mode env mname mref margs margs' locs submv solfull stm solnf
= do defs <- get Ctxt = do defs <- get Ctxt
ust <- get UST ust <- get UST
@ -837,7 +842,7 @@ mutual
-- if the terms are the same, this isn't a solution -- if the terms are the same, this isn't a solution
-- but they are already unifying, so just return -- but they are already unifying, so just return
if solutionHeadSame solnf || inNoSolve mref (noSolve ust) if solutionHeadSame solnf || inNoSolve mref (noSolve ust)
then pure success then pure $ Just success
else -- Rather than doing the occurs check here immediately, else -- Rather than doing the occurs check here immediately,
-- we'll wait until all metavariables are resolved, and in -- we'll wait until all metavariables are resolved, and in
-- the meantime look out for cycles when normalising (which -- the meantime look out for cycles when normalising (which
@ -845,8 +850,8 @@ mutual
-- metavariables) -- metavariables)
do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs) do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
| Nothing => throw (InternalError ("Can't happen: Lost hole " ++ show mname)) | Nothing => throw (InternalError ("Can't happen: Lost hole " ++ show mname))
instantiate loc mode env mname mref (length margs) hdef locs solfull stm progress <- tryInstantiate loc mode env mname mref (length margs) hdef locs solfull stm
pure $ solvedHole mref pure $ toMaybe progress (solvedHole mref)
where where
inNoSolve : Int -> IntMap () -> Bool inNoSolve : Int -> IntMap () -> Bool
inNoSolve i ns inNoSolve i ns
@ -908,19 +913,24 @@ mutual
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
tmnf tmnf
case shrinkTerm tm submv of let solveOrElsePostpone : Term newvars -> Core UnifyResult
Just stm => solveHole fc mode env mname mref solveOrElsePostpone stm = do
mbResult <- solveHole fc mode env mname mref
margs margs' locs submv margs margs' locs submv
tm stm tmnf tm stm tmnf
flip fromMaybe (pure <$> mbResult) $
postponeS swap loc mode "Can't instantiate" env
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') tmnf
case shrinkTerm tm submv of
Just stm => solveOrElsePostpone stm
Nothing => Nothing =>
do tm' <- quote defs env tmnf do tm' <- quote defs env tmnf
case shrinkTerm tm' submv of case shrinkTerm tm' submv of
Nothing => postponeS swap loc mode "Can't shrink" env Nothing => postponeS swap loc mode "Can't shrink" env
(NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs') (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
tmnf tmnf
Just stm => solveHole fc mode env mname mref Just stm => solveOrElsePostpone stm
margs margs' locs submv
tm stm tmnf
-- Unify an application with something else -- Unify an application with something else
unifyApp : {auto c : Ref Ctxt Defs} -> unifyApp : {auto c : Ref Ctxt Defs} ->

2
tests/Main.idr
View File

@ -124,7 +124,7 @@ idrisTestsRegression = MkTestPool "Various regressions" [] Nothing
"reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028", "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
"reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035", "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
"reg036", "reg037", "reg038", "reg039", "reg040", "reg041", "reg042", "reg036", "reg037", "reg038", "reg039", "reg040", "reg041", "reg042",
"reg043", "reg044", "reg045"] "reg043", "reg044", "reg045", "reg046"]
idrisTestsData : TestPool idrisTestsData : TestPool
idrisTestsData = MkTestPool "Data and record types" [] Nothing idrisTestsData = MkTestPool "Data and record types" [] Nothing

31
tests/idris2/reg046/Postpone.idr Normal file
View 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/reg046/expected Normal file
View File

@ -0,0 +1,2 @@
1/1: Building Postpone (Postpone.idr)
Main> Bye for now!

1
tests/idris2/reg046/input Normal file
View File

@ -0,0 +1 @@
:q

3
tests/idris2/reg046/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 --no-banner Postpone.idr < input
rm -rf build