diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index 96cf72c0ca..a4c46826de 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -84,10 +84,10 @@ instance : Language.ToSnapshotTree HeaderProcessedSnapshot where /-- State before elaboration of a mutual definition. -/ structure DefParsed where /-- - Input substring uniquely identifying header elaboration result given the same `Environment`. - If missing, results should never be reused. + Unstructured syntax object comprising the full "header" of the definition from the modifiers + (incl. docstring) up to the value, used for determining header elaboration reuse. -/ - headerSubstr? : Option Substring + fullHeaderRef : Syntax /-- Elaboration result, unless fatal exception occurred. -/ headerProcessedSnap : SnapshotTask (Option HeaderProcessedSnapshot) deriving Nonempty @@ -106,6 +106,11 @@ end Snapshots structure DefView where kind : DefKind ref : Syntax + /-- + An unstructured syntax object that comprises the "header" of the definition, i.e. everything up + to the value. Used as a more specific ref for header elaboration. + -/ + headerRef : Syntax modifiers : Modifiers declId : Syntax binders : Syntax @@ -132,20 +137,20 @@ def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView := let (binders, type) := expandOptDeclSig stx[2] let modifiers := modifiers.addAttribute { name := `inline } let modifiers := modifiers.addAttribute { name := `reducible } - { ref := stx, kind := DefKind.abbrev, modifiers, + { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.abbrev, modifiers, declId := stx[1], binders, type? := type, value := stx[3] } def mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView := -- leading_parser "def " >> declId >> optDeclSig >> declVal >> optDefDeriving let (binders, type) := expandOptDeclSig stx[2] let deriving? := if stx[4].isNone then none else some stx[4][1].getSepArgs - { ref := stx, kind := DefKind.def, modifiers, + { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.def, modifiers, declId := stx[1], binders, type? := type, value := stx[3], deriving? } def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView := -- leading_parser "theorem " >> declId >> declSig >> declVal let (binders, type) := expandDeclSig stx[2] - { ref := stx, kind := DefKind.theorem, modifiers, + { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.theorem, modifiers, declId := stx[1], binders, type? := some type, value := stx[3] } def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do @@ -166,7 +171,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De trace[Elab.instance.mkInstanceName] "generated {(← getCurrNamespace) ++ id}" pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode] return { - ref := stx, kind := DefKind.def, modifiers := modifiers, + ref := stx, headerRef := mkNullNode stx.getArgs[:5], kind := DefKind.def, modifiers := modifiers, declId := declId, binders := binders, type? := type, value := stx[5] } @@ -179,7 +184,7 @@ def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefV let val ← if modifiers.isUnsafe then `(default_or_ofNonempty% unsafe) else `(default_or_ofNonempty%) `(Parser.Command.declValSimple| := $val) return { - ref := stx, kind := DefKind.opaque, modifiers := modifiers, + ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.opaque, modifiers := modifiers, declId := stx[1], binders := binders, type? := some type, value := val } @@ -188,7 +193,7 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView := let (binders, type) := expandOptDeclSig stx[1] let id := mkIdentFrom stx `_example let declId := mkNode ``Parser.Command.declId #[id, mkNullNode] - { ref := stx, kind := DefKind.example, modifiers := modifiers, + { ref := stx, headerRef := mkNullNode stx.getArgs[:2], kind := DefKind.example, modifiers := modifiers, declId := declId, binders := binders, type? := type, value := stx[2] } def isDefLike (stx : Syntax) : Bool := diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 134d922f19..87f4ccfac6 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -131,7 +131,7 @@ private def elabHeaders (views : Array DefView) (bodyPromises : Array (IO.Promise (Option BodyProcessedSnapshot))) (tacPromises : Array (IO.Promise Tactic.TacticParsedSnapshot)) : TermElabM (Array DefViewElabHeader) := do - let expandedDeclIds ← views.mapM fun view => withRef view.ref do + let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers withAutoBoundImplicitForbiddenPred (fun n => expandedDeclIds.any (·.shortName == n)) do let mut headers := #[] @@ -181,9 +181,13 @@ private def elabHeaders (views : Array DefView) reuseBody := false let header ← withRestoreOrSaveFull reusableResult? fun save => do - withRef view.ref do - addDeclarationRanges declName view.ref + withRef view.headerRef do + addDeclarationRanges declName view.ref -- NOTE: this should be the full `ref` applyAttributesAt declName view.modifiers.attrs .beforeElaboration + -- do not hide header errors on partial body syntax as these two elaboration parts are + -- sufficiently independent + withTheReader Core.Context ({ · with suppressElabErrors := + view.headerRef.hasMissing && !Command.showPartialSyntaxErrors.get (← getOptions) }) do withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <| elabBindersEx view.binders.getArgs fun xs => do let refForElabFunType := view.value @@ -961,40 +965,41 @@ end Term namespace Command def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do + let opts ← getOptions withAlwaysResolvedPromises ds.size fun headerPromises => do - let substr? := (mkNullNode ds).getSubstring? let snap? := (← read).snap? let mut views := #[] let mut defs := #[] + let mut reusedAllHeaders := true for h : i in [0:ds.size], headerPromise in headerPromises do let d := ds[i] let modifiers ← elabModifiers d[0] if ds.size > 1 && modifiers.isNonrec then throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block" let mut view ← mkDefView modifiers d[1] + let fullHeaderRef := mkNullNode #[d[0], view.headerRef] if let some snap := snap? then - -- overapproximation: includes previous bodies as well - let headerSubstr? := return { (← substr?) with stopPos := (← view.value.getPos?) } view := { view with headerSnap? := some { old? := do - -- transitioning from `Context.snap?` to `DefView.snap?` invariant: if the elaboration - -- context and state are unchanged, and the substring from the beginning of the first - -- header to the beginning of the current body is unchanged, then the elaboration result for - -- this header (which includes state from elaboration of previous headers!) should be - -- unchanged. + -- transitioning from `Context.snap?` to `DefView.headerSnap?` invariant: if the + -- elaboration context and state are unchanged, and the syntax of this as well as all + -- previous headers is unchanged, then the elaboration result for this header (which + -- includes state from elaboration of previous headers!) should be unchanged. + guard reusedAllHeaders let old ← snap.old? -- blocking wait, `HeadersParsedSnapshot` (and hopefully others) should be quick let old ← old.val.get.toTyped? DefsParsedSnapshot let oldParsed ← old.defs[i]? - guard <| (← headerSubstr?).sameAs (← oldParsed.headerSubstr?) + guard <| fullHeaderRef.structRangeEqWithTraceReuse opts oldParsed.fullHeaderRef -- no syntax guard to store, we already did the necessary checks return ⟨.missing, oldParsed.headerProcessedSnap⟩ new := headerPromise } } defs := defs.push { - headerSubstr? + fullHeaderRef headerProcessedSnap := { range? := d.getRange?, task := headerPromise.result } } + reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome) views := views.push view if let some snap := snap? then -- no non-fatal diagnostics at this point diff --git a/tests/lean/3989_1.lean.expected.out b/tests/lean/3989_1.lean.expected.out index 188b2bb20a..43c02370bf 100644 --- a/tests/lean/3989_1.lean.expected.out +++ b/tests/lean/3989_1.lean.expected.out @@ -1 +1,5 @@ 3989_1.lean:4:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...` +3989_1.lean:1:22-1:32: error: function expected at + MetaM +term has type + ?m diff --git a/tests/lean/3989_2.lean.expected.out b/tests/lean/3989_2.lean.expected.out index 4e1569eb91..96ce3ea923 100644 --- a/tests/lean/3989_2.lean.expected.out +++ b/tests/lean/3989_2.lean.expected.out @@ -1,2 +1,6 @@ 3989_2.lean:6:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...` +3989_2.lean:1:22-1:32: error: function expected at + MetaM +term has type + ?m Nat : Type diff --git a/tests/lean/799.lean.expected.out b/tests/lean/799.lean.expected.out index 1f0068ad78..1bf6a65e18 100644 --- a/tests/lean/799.lean.expected.out +++ b/tests/lean/799.lean.expected.out @@ -1,5 +1,5 @@ -799.lean:3:0-3:11: error: invalid declaration name 'p', there is a section variable with the same name +799.lean:3:0-3:5: error: invalid declaration name 'p', there is a section variable with the same name p : Prop -799.lean:7:0-7:13: error: invalid declaration name 'p', there is a section variable with the same name +799.lean:7:0-7:5: error: invalid declaration name 'p', there is a section variable with the same name p : Prop p : Nat diff --git a/tests/lean/mutualdef1.lean.expected.out b/tests/lean/mutualdef1.lean.expected.out index 5c3a088c17..28e7d4ebc0 100644 --- a/tests/lean/mutualdef1.lean.expected.out +++ b/tests/lean/mutualdef1.lean.expected.out @@ -1,3 +1,3 @@ -mutualdef1.lean:9:0-11:12: error: invalid mutually recursive definitions, cannot mix theorems and definitions -mutualdef1.lean:21:0-22:4: error: invalid mutually recursive definitions, cannot mix examples and definitions -mutualdef1.lean:32:7-34:12: error: invalid mutually recursive definitions, cannot mix unsafe and safe definitions +mutualdef1.lean:9:0-9:31: error: invalid mutually recursive definitions, cannot mix theorems and definitions +mutualdef1.lean:21:0-21:13: error: invalid mutually recursive definitions, cannot mix examples and definitions +mutualdef1.lean:32:7-32:34: error: invalid mutually recursive definitions, cannot mix unsafe and safe definitions diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out index 0e2eeb68d6..4baa88d004 100644 --- a/tests/lean/sanitychecks.lean.expected.out +++ b/tests/lean/sanitychecks.lean.expected.out @@ -4,8 +4,8 @@ with errors structural recursion cannot be used well-founded recursion cannot be used, 'unsound' does not take any (non-fixed) arguments -sanitychecks.lean:4:8-5:10: error: 'partial' theorems are not allowed, 'partial' is a code generation directive -sanitychecks.lean:7:7-8:10: error: 'unsafe' theorems are not allowed +sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial' is a code generation directive +sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed sanitychecks.lean:10:0-10:23: error: failed to synthesize Inhabited False use `set_option diagnostics true` to get diagnostic information diff --git a/tests/lean/syntheticOpaqueReadOnly.lean.expected.out b/tests/lean/syntheticOpaqueReadOnly.lean.expected.out index 1fe92a5d80..c508d5366f 100644 --- a/tests/lean/syntheticOpaqueReadOnly.lean.expected.out +++ b/tests/lean/syntheticOpaqueReadOnly.lean.expected.out @@ -1 +1 @@ -false +false