From 2e98726973099499cd96b40bc504507befb6a82e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 26 Aug 2022 10:54:23 +0200 Subject: [PATCH] fix: `levelMVarToParam` must update `levelNames` --- src/Lean/Elab/BuiltinCommand.lean | 6 ++--- src/Lean/Elab/Declaration.lean | 2 +- src/Lean/Elab/Inductive.lean | 19 +++++++--------- src/Lean/Elab/MutualDef.lean | 5 +++-- src/Lean/Elab/PreDefinition/Basic.lean | 7 ++---- src/Lean/Elab/Structure.lean | 31 ++++++++++++-------------- src/Lean/Elab/Term.lean | 19 +++++----------- tests/lean/levelNGen.lean | 2 ++ tests/lean/levelNGen.lean.expected.out | 2 ++ tests/lean/run/PPTopDownAnalyze.lean | 2 +- 10 files changed, 41 insertions(+), 54 deletions(-) diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index a7b09849a3..70785f8adf 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -233,7 +233,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab | `(#check%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check do let e ← Term.elabTerm term none Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := ignoreStuckTC) - let (e, _) ← Term.levelMVarToParam (← instantiateMVars e) + let e ← Term.levelMVarToParam (← instantiateMVars e) let type ← inferType e unless e.isSyntheticSorry do logInfoAt tk m!"{e} : {type}" @@ -245,7 +245,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab | `(#reduce%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do let e ← Term.elabTerm term none Term.synthesizeSyntheticMVarsNoPostponing - let (e, _) ← Term.levelMVarToParam (← instantiateMVars e) + let e ← Term.levelMVarToParam (← instantiateMVars e) -- TODO: add options or notation for setting the following parameters withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := false) (skipTypes := false) @@ -318,7 +318,7 @@ unsafe def elabEvalUnsafe : CommandElab | `(#eval%$tk $term) => do let declName := `_eval let addAndCompile (value : Expr) : TermElabM Unit := do - let (value, _) ← Term.levelMVarToParam (← instantiateMVars value) + let value ← Term.levelMVarToParam (← instantiateMVars value) let type ← inferType value let us := collectLevelParams {} value |>.params let value ← instantiateMVars value diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index aeef19c154..8f6d2a2c55 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -112,7 +112,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do let type ← instantiateMVars type let type ← mkForallFVars xs type let type ← mkForallFVars vars type (usedOnly := true) - let (type, _) ← Term.levelMVarToParam type + let type ← Term.levelMVarToParam type let usedParams := collectLevelParams {} type |>.params match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with | Except.error msg => throwErrorAt stx msg diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 8d714f76f8..d29dddc4d5 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -408,18 +408,15 @@ def shouldInferResultUniverse (u : Level) : TermElabM (Option LMVarId) := do it should be inferred later using `inferResultingUniverse`. -/ private def levelMVarToParam (indTypes : List InductiveType) (univToInfer? : Option LMVarId) : TermElabM (List InductiveType) := - go |>.run' 1 + indTypes.mapM fun indType => do + let type ← levelMVarToParam' indType.type + let ctors ← indType.ctors.mapM fun ctor => do + let ctorType ← levelMVarToParam' ctor.type + return { ctor with type := ctorType } + return { indType with ctors, type } where - levelMVarToParam' (type : Expr) : StateRefT Nat TermElabM Expr := do - Term.levelMVarToParam' type (except := fun mvarId => univToInfer? == some mvarId) - - go : StateRefT Nat TermElabM (List InductiveType) := do - indTypes.mapM fun indType => do - let type ← levelMVarToParam' indType.type - let ctors ← indType.ctors.mapM fun ctor => do - let ctorType ← levelMVarToParam' ctor.type - return { ctor with type := ctorType } - return { indType with ctors, type } + levelMVarToParam' (type : Expr) : TermElabM Expr := do + Term.levelMVarToParam type (except := fun mvarId => univToInfer? == some mvarId) def mkResultUniverse (us : Array Level) (rOffset : Nat) : Level := if us.isEmpty && rOffset == 0 then diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 4e196e29a9..9a105609ac 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -710,8 +710,9 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def let mut newHeaders := #[] for view in views, header in headers do if view.kind.isTheorem then - newHeaders := newHeaders.push { header with type := - (← monadMap (@withLevelNames (levelNames := header.levelNames)) (levelMVarToParam' header.type)) } + newHeaders ← + withLevelNames header.levelNames do + return newHeaders.push { header with type := (← levelMVarToParam header.type), levelNames := (← getLevelNames) } else newHeaders := newHeaders.push header return newHeaders diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index bc75208e54..de87fc6ab7 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -33,12 +33,9 @@ def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Arra preDefs.mapM fun preDef => do pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) } -private def levelMVarToParamPreDeclsAux (preDefs : Array PreDefinition) : StateRefT Nat TermElabM (Array PreDefinition) := - preDefs.mapM fun preDef => do - pure { preDef with type := (← levelMVarToParam' preDef.type), value := (← levelMVarToParam' preDef.value) } - def levelMVarToParamPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) := - (levelMVarToParamPreDeclsAux preDefs).run' 1 + preDefs.mapM fun preDef => do + pure { preDef with type := (← levelMVarToParam preDef.type), value := (← levelMVarToParam preDef.value) } private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (List Name) := do let mut s : CollectLevelParams.State := {} diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index b0a91900fe..bc4a1af71e 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -595,27 +595,24 @@ private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldI let (lctx, localInsts, vars) ← removeUnused scopeVars params fieldInfos withLCtx lctx localInsts <| k vars -private def levelMVarToParam (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (univToInfer? : Option LMVarId) : TermElabM (Array StructFieldInfo) := - go |>.run' 1 +private def levelMVarToParam (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (univToInfer? : Option LMVarId) : TermElabM (Array StructFieldInfo) := do + levelMVarToParamFVars scopeVars + levelMVarToParamFVars params + fieldInfos.mapM fun info => do + levelMVarToParamFVar info.fvar + match info.value? with + | none => pure info + | some value => + let value ← levelMVarToParam' value + pure { info with value? := value } where - levelMVarToParam' (type : Expr) : StateRefT Nat TermElabM Expr := do - Term.levelMVarToParam' type (except := fun mvarId => univToInfer? == some mvarId) + levelMVarToParam' (type : Expr) : TermElabM Expr := do + Term.levelMVarToParam type (except := fun mvarId => univToInfer? == some mvarId) - go : StateRefT Nat TermElabM (Array StructFieldInfo) := do - levelMVarToParamFVars scopeVars - levelMVarToParamFVars params - fieldInfos.mapM fun info => do - levelMVarToParamFVar info.fvar - match info.value? with - | none => pure info - | some value => - let value ← levelMVarToParam' value - pure { info with value? := value } - - levelMVarToParamFVars (fvars : Array Expr) : StateRefT Nat TermElabM Unit := + levelMVarToParamFVars (fvars : Array Expr) : TermElabM Unit := fvars.forM levelMVarToParamFVar - levelMVarToParamFVar (fvar : Expr) : StateRefT Nat TermElabM Unit := do + levelMVarToParamFVar (fvar : Expr) : TermElabM Unit := do let type ← inferType fvar discard <| levelMVarToParam' type diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 789145fafa..fd7a34a63a 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -582,22 +582,13 @@ def mkExplicitBinder (ident : Syntax) (type : Syntax) : Syntax := /-- Convert unassigned universe level metavariables into parameters. - The new parameter names are of the form `u_i` where `i >= nextParamIdx`. - The method returns the updated expression and new `nextParamIdx`. - - Remark: we make sure the generated parameter names do not clash with the universe at `ctx.levelNames`. -/ -def levelMVarToParam (e : Expr) (nextParamIdx : Nat := 1) (except : LMVarId → Bool := fun _ => false) : TermElabM (Expr × Nat) := do + The new parameter names are fresh names of the form `u_i` with regard to `ctx.levelNames`, which is updated with the new names. -/ +def levelMVarToParam (e : Expr) (except : LMVarId → Bool := fun _ => false) : TermElabM Expr := do let levelNames ← getLevelNames - let r := (← getMCtx).levelMVarToParam (fun n => levelNames.elem n) except e `u nextParamIdx + let r := (← getMCtx).levelMVarToParam (fun n => levelNames.elem n) except e `u 1 + setLevelNames (levelNames ++ r.newParamNames.toList) setMCtx r.mctx - return (r.expr, r.nextParamIdx) - -/-- Variant of `levelMVarToParam` where `nextParamIdx` is stored in a state monad. -/ -def levelMVarToParam' (e : Expr) (except : LMVarId → Bool := fun _ => false) : StateRefT Nat TermElabM Expr := do - let nextParamIdx ← get - let (e, nextParamIdx) ← levelMVarToParam e nextParamIdx except - set nextParamIdx - return e + return r.expr /-- Auxiliary method for creating fresh binder names. diff --git a/tests/lean/levelNGen.lean b/tests/lean/levelNGen.lean index cf342aedc9..46153e2075 100644 --- a/tests/lean/levelNGen.lean +++ b/tests/lean/levelNGen.lean @@ -2,3 +2,5 @@ opaque test1 {α : Sort _} : α → Sort u_1 #check @test1 def test2 {α : Sort _} : α → Sort u_1 := sorry #check @test2 +variable {α : Sort _} in theorem test3 : α → Sort _ := sorry +#check @test3 diff --git a/tests/lean/levelNGen.lean.expected.out b/tests/lean/levelNGen.lean.expected.out index b5c2833e23..bc952cb9b7 100644 --- a/tests/lean/levelNGen.lean.expected.out +++ b/tests/lean/levelNGen.lean.expected.out @@ -1,3 +1,5 @@ @test1 : {α : Sort u_2} → α → Sort u_1 levelNGen.lean:3:4-3:9: warning: declaration uses 'sorry' @test2 : {α : Sort u_2} → α → Sort u_1 +levelNGen.lean:5:33-5:38: warning: declaration uses 'sorry' +@test3 : {α : Sort u_2} → α → Sort u_1 diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 87911ee48e..ef94f280af 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -43,7 +43,7 @@ syntax (name := testDelabTD) "#testDelab " term " expecting " term : command @[commandElab testDelabTD] def elabTestDelabTD : CommandElab | `(#testDelab $stx:term expecting $tgt:term) => liftTermElabM do withDeclName `delabTD do let e ← elabTerm stx none - let ⟨e, _⟩ ← levelMVarToParam e + let e ← levelMVarToParam e let e ← instantiateMVars e checkDelab e (some tgt) | _ => throwUnsupportedSyntax