From 91d51d06e02be8c2f61ad1fbe559bef33132f8ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 26 Oct 2020 14:00:13 -0700 Subject: [PATCH] chore: cleanup --- src/Lean/Meta/AbstractMVars.lean | 164 ++++++++++++++++--------------- 1 file changed, 83 insertions(+), 81 deletions(-) diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean index 9dec7f346a..e87e5b2344 100644 --- a/src/Lean/Meta/AbstractMVars.lean +++ b/src/Lean/Meta/AbstractMVars.lean @@ -8,14 +8,14 @@ import Lean.Meta.Basic namespace Lean.Meta structure AbstractMVarsResult := -(paramNames : Array Name) -(numMVars : Nat) -(expr : Expr) + (paramNames : Array Name) + (numMVars : Nat) + (expr : Expr) instance : Inhabited AbstractMVarsResult := ⟨⟨#[], 0, arbitrary _⟩⟩ def AbstractMVarsResult.beq (r₁ r₂ : AbstractMVarsResult) : Bool := -r₁.paramNames == r₂.paramNames && r₁.numMVars == r₂.numMVars && r₁.expr == r₂.expr + r₁.paramNames == r₂.paramNames && r₁.numMVars == r₂.numMVars && r₁.expr == r₂.expr instance : HasBeq AbstractMVarsResult := ⟨AbstractMVarsResult.beq⟩ @@ -24,83 +24,85 @@ namespace AbstractMVars open Std (HashMap) structure State := -(ngen : NameGenerator) -(lctx : LocalContext) -(nextParamIdx : Nat := 0) -(paramNames : Array Name := #[]) -(fvars : Array Expr := #[]) -(lmap : HashMap Name Level := {}) -(emap : HashMap Name Expr := {}) + (ngen : NameGenerator) + (lctx : LocalContext) + (nextParamIdx : Nat := 0) + (paramNames : Array Name := #[]) + (fvars : Array Expr := #[]) + (lmap : HashMap Name Level := {}) + (emap : HashMap Name Expr := {}) abbrev M := ReaderT MetavarContext (StateM State) def mkFreshId : M Name := do -let s ← get -let fresh := s.ngen.curr -modify fun s => { s with ngen := s.ngen.next } -pure fresh + let s ← get + let fresh := s.ngen.curr + modify fun s => { s with ngen := s.ngen.next } + pure fresh -@[inline] private def visitLevel (f : Level → M Level) (u : Level) : M Level := -if !u.hasMVar then pure u -else f u - -@[inline] private def visitExpr (f : Expr → M Expr) (e : Expr) : M Expr := -if !e.hasMVar then pure e -else f e - -private partial def abstractLevelMVars : Level → M Level -| u@(Level.zero _) => pure u -| u@(Level.param _ _) => pure u -| u@(Level.succ v _) => do return u.updateSucc! (← visitLevel abstractLevelMVars v) -| u@(Level.max v w _) => do return u.updateMax! (← visitLevel abstractLevelMVars v) (← visitLevel abstractLevelMVars w) -| u@(Level.imax v w _) => do return u.updateIMax! (← visitLevel abstractLevelMVars v) (← visitLevel abstractLevelMVars w) -| u@(Level.mvar mvarId _) => do - let mctx ← read - let depth := mctx.getLevelDepth mvarId; - if depth != mctx.depth then pure u -- metavariables from lower depths are treated as constants +private partial def abstractLevelMVars (u : Level) : M Level := do + if !u.hasMVar then + return u else - let s ← get - match s.lmap.find? mvarId with - | some u => pure u - | none => - let paramId := mkNameNum `_abstMVar s.nextParamIdx - let u := mkLevelParam paramId - modify fun s => { s with nextParamIdx := s.nextParamIdx + 1, lmap := s.lmap.insert mvarId u, paramNames := s.paramNames.push paramId } - pure u + match u with + | Level.zero _ => return u + | Level.param _ _ => return u + | Level.succ v _ => return u.updateSucc! (← abstractLevelMVars v) + | Level.max v w _ => return u.updateMax! (← abstractLevelMVars v) (← abstractLevelMVars w) + | Level.imax v w _ => return u.updateIMax! (← abstractLevelMVars v) (← abstractLevelMVars w) + | Level.mvar mvarId _ => + let mctx ← read + let depth := mctx.getLevelDepth mvarId; + if depth != mctx.depth then + return u -- metavariables from lower depths are treated as constants + else + let s ← get + match s.lmap.find? mvarId with + | some u => pure u + | none => + let paramId := mkNameNum `_abstMVar s.nextParamIdx + let u := mkLevelParam paramId + modify fun s => { s with nextParamIdx := s.nextParamIdx + 1, lmap := s.lmap.insert mvarId u, paramNames := s.paramNames.push paramId } + return u -partial def abstractExprMVars : Expr → M Expr -| e@(Expr.lit _ _) => pure e -| e@(Expr.bvar _ _) => pure e -| e@(Expr.fvar _ _) => pure e -| e@(Expr.sort u _) => do return e.updateSort! (← visitLevel abstractLevelMVars u) -| e@(Expr.const _ us _) => do return e.updateConst! (← us.mapM (visitLevel abstractLevelMVars)) -| e@(Expr.proj _ _ s _) => do return e.updateProj! (← visitExpr abstractExprMVars s) -| e@(Expr.app f a _) => do return e.updateApp! (← visitExpr abstractExprMVars f) (← visitExpr abstractExprMVars a) -| e@(Expr.mdata _ b _) => do return e.updateMData! (← visitExpr abstractExprMVars b) -| e@(Expr.lam _ d b _) => do return e.updateLambdaE! (← visitExpr abstractExprMVars d) (← visitExpr abstractExprMVars b) -| e@(Expr.forallE _ d b _) => do return e.updateForallE! (← visitExpr abstractExprMVars d) (← visitExpr abstractExprMVars b) -| e@(Expr.letE _ t v b _) => do return e.updateLet! (← visitExpr abstractExprMVars t) (← visitExpr abstractExprMVars v) (← visitExpr abstractExprMVars b) -| e@(Expr.mvar mvarId _) => do - let mctx ← read - let decl := mctx.getDecl mvarId - if decl.depth != mctx.depth then - pure e -- metavariables from lower depths are treated as constants +partial def abstractExprMVars (e : Expr) : M Expr := do + if !e.hasMVar then + return e else - let s ← get - match s.emap.find? mvarId with - | some e => pure e - | none => - let type ← visitExpr abstractExprMVars decl.type - let fvarId ← mkFreshId - let fvar := mkFVar fvarId; - let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter s.fvars.size else decl.userName - modify fun s => { - s with - emap := s.emap.insert mvarId fvar, - fvars := s.fvars.push fvar, - lctx := s.lctx.mkLocalDecl fvarId userName type } - pure fvar -| Expr.localE .. => unreachable! + match e with + | e@(Expr.lit _ _) => return e + | e@(Expr.bvar _ _) => return e + | e@(Expr.fvar _ _) => return e + | e@(Expr.sort u _) => return e.updateSort! (← abstractLevelMVars u) + | e@(Expr.const _ us _) => return e.updateConst! (← us.mapM abstractLevelMVars) + | e@(Expr.proj _ _ s _) => return e.updateProj! (← abstractExprMVars s) + | e@(Expr.app f a _) => return e.updateApp! (← abstractExprMVars f) (← abstractExprMVars a) + | e@(Expr.mdata _ b _) => return e.updateMData! (← abstractExprMVars b) + | e@(Expr.lam _ d b _) => return e.updateLambdaE! (← abstractExprMVars d) (← abstractExprMVars b) + | e@(Expr.forallE _ d b _) => return e.updateForallE! (← abstractExprMVars d) (← abstractExprMVars b) + | e@(Expr.letE _ t v b _) => return e.updateLet! (← abstractExprMVars t) (← abstractExprMVars v) (← abstractExprMVars b) + | e@(Expr.mvar mvarId _) => + let mctx ← read + let decl := mctx.getDecl mvarId + if decl.depth != mctx.depth then + return e + else + let s ← get + match s.emap.find? mvarId with + | some e => + return e + | none => + let type ← abstractExprMVars decl.type + let fvarId ← mkFreshId + let fvar := mkFVar fvarId; + let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter s.fvars.size else decl.userName + modify fun s => { + s with + emap := s.emap.insert mvarId fvar, + fvars := s.fvars.push fvar, + lctx := s.lctx.mkLocalDecl fvarId userName type } + return fvar + | Expr.localE .. => unreachable! end AbstractMVars @@ -123,15 +125,15 @@ end AbstractMVars Application: we use this method to cache the results of type class resolution. -/ def abstractMVars (e : Expr) : MetaM AbstractMVarsResult := do -let e ← instantiateMVars e -let (e, s) := AbstractMVars.abstractExprMVars e (← getMCtx) { lctx := (← getLCtx), ngen := (← getNGen) } -setNGen s.ngen -let e := s.lctx.mkLambda s.fvars e -pure { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e } + let e ← instantiateMVars e + let (e, s) := AbstractMVars.abstractExprMVars e (← getMCtx) { lctx := (← getLCtx), ngen := (← getNGen) } + setNGen s.ngen + let e := s.lctx.mkLambda s.fvars e + pure { paramNames := s.paramNames, numMVars := s.fvars.size, expr := e } def openAbstractMVarsResult (a : AbstractMVarsResult) : MetaM (Array Expr × Array BinderInfo × Expr) := do -let us ← a.paramNames.mapM fun _ => mkFreshLevelMVar -let e := a.expr.instantiateLevelParamsArray a.paramNames us -lambdaMetaTelescope e (some a.numMVars) + let us ← a.paramNames.mapM fun _ => mkFreshLevelMVar + let e := a.expr.instantiateLevelParamsArray a.paramNames us + lambdaMetaTelescope e (some a.numMVars) end Lean.Meta