From 608a306ef094875d69f92a9cb6a3afb03fa1547a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Jul 2022 13:26:17 -0700 Subject: [PATCH] refactor: simplify/cleanup `DelayedMetavarAssignment` --- src/Lean/Elab/Term.lean | 2 +- src/Lean/Meta/CollectMVars.lean | 2 +- src/Lean/Meta/WHNF.lean | 4 +- src/Lean/MetavarContext.lean | 87 ++++++++++++++++----------------- src/Lean/Util/OccursCheck.lean | 2 +- 5 files changed, 46 insertions(+), 51 deletions(-) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index d8b57fba80..ac60723dc5 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -691,7 +691,7 @@ partial def visit (e : Expr) : M Unit := do visit e' else match (← getDelayedMVarAssignment? mvarId) with - | some d => visit d.val + | some d => visit (mkMVar d.mvarIdPending) | none => failure | _ => return () diff --git a/src/Lean/Meta/CollectMVars.lean b/src/Lean/Meta/CollectMVars.lean index bb3fdcbd94..aebdddb8f8 100644 --- a/src/Lean/Meta/CollectMVars.lean +++ b/src/Lean/Meta/CollectMVars.lean @@ -26,7 +26,7 @@ partial def collectMVars (e : Expr) : StateRefT CollectMVars.State MetaM Unit := for mvarId in s.result[resultSavedSize:] do match (← getDelayedMVarAssignment? mvarId) with | none => pure () - | some d => collectMVars d.val + | some d => collectMVars (mkMVar d.mvarIdPending) /-- Return metavariables in occuring the given expression. See `collectMVars` -/ def getMVars (e : Expr) : MetaM (Array MVarId) := do diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index d5e0c33be9..7bc422c619 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -452,13 +452,13 @@ private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) := if f'.isMVar then match (← getDelayedMVarAssignment? f'.mvarId!) with | none => return none - | some { fvars, val } => + | some { fvars, mvarIdPending } => let args := e.getAppArgs if fvars.size > args.size then -- Insufficient number of argument to expand delayed assignment return none else - let newVal ← instantiateMVars val + let newVal ← instantiateMVars (mkMVar mvarIdPending) if newVal.hasExprMVar then -- Delayed assignment still contains metavariables return none diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index d1e0e19c2f..f24341ddd1 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -260,11 +260,14 @@ structure MetavarDecl where deriving Inhabited /-- - A delayed assignment for a metavariable `?m`. It represents an assignment of the form `?m := (fun fvars => val)`. + A delayed assignment for a metavariable `?m`. It represents an assignment of the form `?m := (fun fvars => (mkMVar mvarIdPending))`. + `mvarIdPending` is a `syntheticOpaque` metavariable that has not been synthesized yet. The delayed assignment becomes a real one + as soon as `mvarIdPending` has been fully synthesized. + `fvars` are variables in the `mvarIdPending` local context. -/ structure DelayedMetavarAssignment where - fvars : Array Expr - val : Expr + fvars : Array Expr + mvarIdPending : MVarId open Std (HashMap PersistentHashMap) @@ -326,9 +329,7 @@ def getDelayedMVarAssignment? [Monad m] [MonadMCtx m] (mvarId : MVarId) : m (Opt If `mvarId₁` is not delayed assigned then return `mvarId₁` -/ partial def getDelayedMVarRoot [Monad m] [MonadMCtx m] (mvarId : MVarId) : m MVarId := do match (← getDelayedMVarAssignment? mvarId) with - | some d => match d.val.getAppFn with - | Expr.mvar mvarId _ => getDelayedMVarRoot mvarId - | _ => return mvarId + | some d => getDelayedMVarRoot d.mvarIdPending | none => return mvarId def isLevelMVarAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do @@ -422,8 +423,8 @@ def assignLevelMVar [MonadMCtx m] (mvarId : MVarId) (val : Level) : m Unit := def assignExprMVar [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit := modifyMCtx fun m => { m with eAssignment := m.eAssignment.insert mvarId val, usedAssignment := true } -def assignDelayedMVar [MonadMCtx m] (mvarId : MVarId) (fvars : Array Expr) (val : Expr) : m Unit := - modifyMCtx fun m => { m with dAssignment := m.dAssignment.insert mvarId { fvars, val }, usedAssignment := true } +def assignDelayedMVar [MonadMCtx m] (mvarId : MVarId) (fvars : Array Expr) (mvarIdPending : MVarId) : m Unit := + modifyMCtx fun m => { m with dAssignment := m.dAssignment.insert mvarId { fvars, mvarIdPending }, usedAssignment := true } /- Notes on artificial eta-expanded terms due to metavariables. @@ -486,7 +487,7 @@ partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLi | Expr.mvar mvarId _ => match (← getDelayedMVarAssignment? mvarId) with | none => instApp - | some { fvars, val } => + | some { fvars, mvarIdPending } => /- Apply "delayed substitution" (i.e., delayed assignment + application). That is, `f` is some metavariable `?m`, that is delayed assigned to `val`. @@ -500,7 +501,7 @@ partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLi when we are checking for unassigned metavariables in an elaborated term. -/ instArgs f else - let newVal ← instantiateExprMVars val + let newVal ← instantiateExprMVars (mkMVar mvarIdPending) if newVal.hasExprMVar then instArgs f else do @@ -1018,43 +1019,37 @@ mutual That being said, we should try this approach as soon as we have an extensive test suite. -/ let newMVarKind := if !(← isExprMVarAssignable mvarId) then MetavarKind.syntheticOpaque else mvarDecl.kind - /- If `mvarId` is the lhs of a delayed assignment `?m #[x_1, ... x_n] := val`, - then `nestedFVars` is `#[x_1, ..., x_n]`. - In this case, we produce a new `syntheticOpaque` metavariable `?n` and a delayed assignment - ``` - ?n #[y_1, ..., y_m, x_1, ... x_n] := ?m x_1 ... x_n - ``` - where `#[y_1, ..., y_m]` is `toRevert` after `collectForwardDeps`. - - Remark: `newMVarKind != MetavarKind.syntheticOpaque ==> nestedFVars == #[]` - -/ - let rec cont (nestedFVars : Array Expr) : M (Expr × Array Expr) := do - let args ← args.mapM (visit xs) - -- Note that `toRevert` only contains free variables since it is the result of `getInScope` - let toRevert ← collectForwardDeps mvarLCtx toRevert - let newMVarLCtx := reduceLocalContext mvarLCtx toRevert - let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x - -- Remark: we must reset the before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs` - let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type - let newMVarId := { name := (← get).ngen.curr } - let newMVar := mkMVar newMVarId - let result := mkMVarApp mvarLCtx newMVar toRevert newMVarKind - let numScopeArgs := mvarDecl.numScopeArgs + result.getAppNumArgs - modify fun s => { s with - mctx := s.mctx.addExprMVarDecl newMVarId Name.anonymous newMVarLCtx newLocalInsts newMVarType newMVarKind numScopeArgs, - ngen := s.ngen.next - } - match newMVarKind with - | MetavarKind.syntheticOpaque => - assignDelayedMVar newMVarId (toRevert ++ nestedFVars) (mkAppN (mkMVar mvarId) nestedFVars) - | _ => - assignExprMVar mvarId result - return (mkAppN result args, toRevert) + let args ← args.mapM (visit xs) + let toRevert ← collectForwardDeps mvarLCtx toRevert + let newMVarLCtx := reduceLocalContext mvarLCtx toRevert + -- Note that `toRevert` only contains free variables since it is the result of `getInScope` + let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x + -- Remark: we must reset the before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs` + let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type + let newMVarId := { name := (← get).ngen.curr } + let newMVar := mkMVar newMVarId + let result := mkMVarApp mvarLCtx newMVar toRevert newMVarKind + let numScopeArgs := mvarDecl.numScopeArgs + result.getAppNumArgs + modify fun s => { s with + mctx := s.mctx.addExprMVarDecl newMVarId Name.anonymous newMVarLCtx newLocalInsts newMVarType newMVarKind numScopeArgs, + ngen := s.ngen.next + } if !mvarDecl.kind.isSyntheticOpaque then - cont #[] - else match (← getDelayedMVarAssignment? mvarId) with - | none => cont #[] - | some { fvars, .. } => cont fvars + assignExprMVar mvarId result + else + /- If `mvarId` is the lhs of a delayed assignment `?m #[x_1, ... x_n] := ?mvarPending`, + then `nestedFVars` is `#[x_1, ..., x_n]`. + In this case, `newMVarId` is also `syntheticOpaque` and we add the delayed assignment delayed assignment + ``` + ?newMVar #[y_1, ..., y_m, x_1, ... x_n] := ?m + ``` + where `#[y_1, ..., y_m]` is `toRevert` after `collectForwardDeps`. + -/ + let (mvarIdPending, nestedFVars) ← match (← getDelayedMVarAssignment? mvarId) with + | none => pure (mvarId, #[]) + | some { fvars, mvarIdPending } => pure (mvarIdPending, fvars) + assignDelayedMVar newMVarId (toRevert ++ nestedFVars) mvarIdPending + return (mkAppN result args, toRevert) private partial def elimApp (xs : Array Expr) (f : Expr) (args : Array Expr) : M Expr := do match f with diff --git a/src/Lean/Util/OccursCheck.lean b/src/Lean/Util/OccursCheck.lean index e48c0a6e60..6094457e1f 100644 --- a/src/Lean/Util/OccursCheck.lean +++ b/src/Lean/Util/OccursCheck.lean @@ -26,7 +26,7 @@ where | some v => visit v | none => match (← getDelayedMVarAssignment? mvarId') with - | some d => visit d.val + | some d => visitMVar d.mvarIdPending | none => return () visit (e : Expr) : ExceptT Unit (StateT ExprSet m) Unit := do