Skip to content

Commit 0b36e36

Browse files
nomeatanomeata
committed
Sanity restored to some extend, stage2 builds
1 parent 524567e commit 0b36e36

15 files changed

Lines changed: 341 additions & 67 deletions

File tree

‎src/Lean/Elab/DeclModifiers.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
2828
match privateToUserName? declName with
2929
| none => throwError "'{.ofConstName declName true}' has already been declared"
3030
| some declName => throwError "private declaration '{.ofConstName declName true}' has already been declared"
31-
if isReservedName env declName then
31+
if isReservedName env (privateToUserName declName) || isReservedName env (mkPrivateName (← getEnv) declName) then
3232
throwError "'{declName}' is a reserved name"
3333
if env.contains (mkPrivateName env declName) then
3434
addInfo (mkPrivateName env declName)

‎src/Lean/Elab/PreDefinition/EqUnfold.lean‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ This is not extensible, and always builds on the unfold theorem (`f.eq_def`).
2424
def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
2525
if (← getUnfoldEqnFor? (nonRec := true) declName).isNone then
2626
return none
27-
let name := .str declName eqUnfoldThmSuffix
27+
let name := mkEqLikeNameFor (← getEnv) declName eqUnfoldThmSuffix
2828
realizeConst declName name do
2929
-- we have to call `getUnfoldEqnFor?` again to make `unfoldEqnName` available in this context
3030
let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) declName | unreachable!
@@ -58,9 +58,11 @@ def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
5858
builtin_initialize
5959
registerReservedNameAction fun name => do
6060
let .str p s := name | return false
61-
unless (← getEnv).isSafeDefinition p do return false
6261
if s == eqUnfoldThmSuffix then
63-
return (← MetaM.run' <| getConstUnfoldEqnFor? p).isSome
62+
let env := (← getEnv).setExporting false
63+
for p in [p, privateToUserName p] do
64+
if env.isSafeDefinition p then
65+
return (← MetaM.run' <| getConstUnfoldEqnFor? p).isSome
6466
return false
6567

6668
end Lean.Meta

‎src/Lean/Elab/PreDefinition/Eqns.lean‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -402,7 +402,6 @@ but not for structural recursion.
402402
-/
403403
def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (Array Name) := do
404404
let info ← getConstInfoDefn declName
405-
let isExposedDef ← withExporting do (·.hasValue) <$> getConstInfo declName
406405
let us := info.levelParams.map mkLevelParam
407406
withOptions (tactic.hygienic.set · false) do
408407
let target ← unfoldThmType declName
@@ -415,9 +414,7 @@ def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (
415414
for h : i in [: eqnTypes.size] do
416415
let type := eqnTypes[i]
417416
trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]}"
418-
let mut name := (Name.str declName eqnThmSuffixBase).appendIndexAfter (i+1)
419-
unless isExposedDef do
420-
name := mkPrivateName (← getEnv) name
417+
let name := mkEqLikeNameFor (← getEnv) declName s!"{eqnThmSuffixBasePrefix}{i+1}"
421418
thmNames := thmNames.push name
422419
-- determinism: `type` should be independent of the environment changes since `baseName` was
423420
-- added

‎src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,9 @@ open Eqns
1818
/--
1919
Simple, coarse-grained equation theorem for nonrecursive definitions.
2020
-/
21-
private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSuffix) : MetaM (Option Name) := do
21+
private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
2222
if let some (.defnInfo info) := (← getEnv).find? declName then
23-
let mut name := declName ++ suffix
24-
let isExposedDef ← withExporting do (·.hasValue) <$> getConstInfo declName
25-
unless isExposedDef do
26-
name := mkPrivateName (← getEnv) name
23+
let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
2724
realizeConst declName name (doRealize name info)
2825
return some name
2926
else

‎src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -72,11 +72,7 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
7272

7373
/-- Generate the "unfold" lemma for `declName`. -/
7474
def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
75-
let isExposedDef ← withExporting do (·.hasValue) <$> getConstInfo declName
76-
let baseName := declName
77-
let mut name := Name.str baseName unfoldThmSuffix
78-
unless isExposedDef do
79-
name := mkPrivateName (← getEnv) name
75+
let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
8076
realizeConst declName name (doRealize name)
8177
return name
8278
where
@@ -108,7 +104,7 @@ where
108104
}
109105

110106
def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
111-
let name := Name.str declName unfoldThmSuffix
107+
let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
112108
let env ← getEnv
113109
if env.contains name then return name
114110
let some info := eqnInfoExt.find? env declName | return none

‎src/Lean/Elab/PreDefinition/Structural/Eqns.lean‎

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -68,15 +68,11 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
6868
let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
6969
let goal ← mkFreshExprSyntheticOpaqueMVar target
7070
mkEqnTypes info.declNames goal.mvarId!
71-
let isExposedDef ← withExporting do (·.hasValue) <$> getConstInfo info.declName
72-
let baseName := info.declName
7371
let mut thmNames := #[]
7472
for h : i in [: eqnTypes.size] do
7573
let type := eqnTypes[i]
7674
trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
77-
let mut name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
78-
unless isExposedDef do
79-
name := mkPrivateName (← getEnv) name
75+
let name := mkEqLikeNameFor (← getEnv) info.declName s!"{eqnThmSuffixBasePrefix}{i+1}"
8076
thmNames := thmNames.push name
8177
-- determinism: `type` should be independent of the environment changes since `baseName` was
8278
-- added
@@ -107,10 +103,7 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
107103

108104
/-- Generate the "unfold" lemma for `declName`. -/
109105
def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
110-
let mut name := Name.str declName unfoldThmSuffix
111-
let isExposedDef ← withExporting do (·.hasValue) <$> getConstInfo declName
112-
unless isExposedDef do
113-
name := mkPrivateName (← getEnv) name
106+
let name := mkEqLikeNameFor (← getEnv) info.declName unfoldThmSuffix
114107
realizeConst info.declNames[0]! name (doRealize name)
115108
return name
116109
where

‎src/Lean/Elab/PreDefinition/WF/Unfold.lean‎

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -73,11 +73,7 @@ private partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Un
7373
throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
7474

7575
def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessProof : Simp.Result) : MetaM Unit := do
76-
let isExposedDef ← withExporting do (·.hasValue) <$> getConstInfo preDef.declName
77-
let baseName := preDef.declName
78-
let mut name := Name.str baseName unfoldThmSuffix
79-
unless isExposedDef do
80-
name := mkPrivateName (← getEnv) name
76+
let name := mkEqLikeNameFor (← getEnv) preDef.declName unfoldThmSuffix
8177
prependError m!"Cannot derive {name}" do
8278
withOptions (tactic.hygienic.set · false) do
8379
lambdaTelescope preDef.value fun xs body => do
@@ -109,9 +105,8 @@ theorem of `foo._unary` or `foo._binary`.
109105
It should just be a specialization of that one, due to defeq.
110106
-/
111107
def mkBinaryUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM Unit := do
112-
let baseName := preDef.declName
113-
let name := Name.str baseName unfoldThmSuffix
114-
let unaryEqName := Name.str unaryPreDefName unfoldThmSuffix
108+
let name := mkEqLikeNameFor (← getEnv) preDef.declName unfoldThmSuffix
109+
let unaryEqName:= mkEqLikeNameFor (← getEnv) unaryPreDefName unfoldThmSuffix
115110
prependError m!"Cannot derive {name} from {unaryEqName}" do
116111
withOptions (tactic.hygienic.set · false) do
117112
lambdaTelescope preDef.value fun xs body => do

‎src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -355,6 +355,9 @@ builtin_initialize
355355
builtin_initialize
356356
registerReservedNameAction fun name => do
357357
let .str p s := name | return false
358+
unless s == enumToBitVecSuffix ||
359+
s == eqIffEnumToBitVecEqSuffix ||
360+
s == enumToBitVecLeSuffix do return false
358361
if ← isEnumType p then
359362
if s == enumToBitVecSuffix then
360363
discard <| MetaM.run' (getEnumToBitVecFor p)

‎src/Lean/Meta/Eqns.lean‎

Lines changed: 60 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,27 @@ def isEqnReservedNameSuffix (s : String) : Bool :=
6969
def unfoldThmSuffix := "eq_def"
7070
def eqUnfoldThmSuffix := "eq_unfold"
7171

72+
def isEqnLikeSuffix (s : String) : Bool :=
73+
s == unfoldThmSuffix || s == eqUnfoldThmSuffix || isEqnReservedNameSuffix s
74+
75+
/--
76+
The equational theorem for a definition can be private even if the definition itself is not.
77+
So un-private the name here when looking for a declaratin
78+
-/
79+
def declFromEqLikeName (env : Environment) (name : Name) : Option (Name × String) := Id.run do
80+
if let .str p s := name then
81+
if isEqnLikeSuffix s then
82+
for p in [p, privateToUserName p] do
83+
if (env.setExporting false).isSafeDefinition p && !isMatcherCore env p then
84+
return some (p, s)
85+
return none
86+
87+
def mkEqLikeNameFor (env : Environment) (declName : Name) (suffix : String) : Name :=
88+
let isExposed := !env.header.isModule || ((env.setExporting true).find? declName).elim false (·.hasValue)
89+
let name := .str declName suffix
90+
let name := if isExposed then name else mkPrivateName env name
91+
name
92+
7293
/--
7394
Throw an error if names for equation theorems for `declName` are not available.
7495
-/
@@ -82,14 +103,14 @@ def ensureEqnReservedNamesAvailable (declName : Name) : CoreM Unit := do
82103
/--
83104
Ensures that `f.eq_def`, `f.unfold` and `f.eq_<idx>` are reserved names if `f` is a safe definition.
84105
-/
85-
builtin_initialize registerReservedNamePredicate fun env n =>
86-
match n with
87-
| .str p s =>
88-
(isEqnReservedNameSuffix s || s == unfoldThmSuffix || s == eqUnfoldThmSuffix)
89-
&& env.isSafeDefinition p
90-
-- Remark: `f.match_<idx>.eq_<idx>` are handled separately in `Lean.Meta.Match.MatchEqs`.
91-
&& !isMatcherCore env p
92-
| _ => false
106+
builtin_initialize registerReservedNamePredicate fun env n => Id.run do
107+
if let some (declName, suffix) := declFromEqLikeName env n then
108+
-- The reserved name predicate has to be precise, as `resolveExact`
109+
-- will believe it. So make sure that `n` is exactly the name we expect,
110+
-- including the privat prefix.
111+
n == mkEqLikeNameFor env declName suffix
112+
else
113+
false
93114

94115
def GetEqnsFn := Name → MetaM (Option (Array Name))
95116

@@ -144,9 +165,9 @@ builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
144165
/--
145166
Simple equation theorem for nonrecursive definitions.
146167
-/
147-
private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSuffix) : MetaM (Option Name) := do
168+
private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
148169
if let some (.defnInfo info) := (← getEnv).find? declName then
149-
let name := declName ++ suffix
170+
let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
150171
realizeConst declName name (doRealize name info)
151172
return some name
152173
else
@@ -271,28 +292,38 @@ By default, we do not create unfold theorems for nonrecursive definitions.
271292
You can use `nonRec := true` to override this behavior.
272293
-/
273294
def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) := withLCtx {} {} do
274-
let env ← getEnv
275-
let unfoldName := Name.str declName unfoldThmSuffix
276-
if env.contains unfoldName then
277-
return some unfoldName
278-
if (← shouldGenerateEqnThms declName) then
279-
for f in (← getUnfoldEqnFnsRef.get) do
280-
if let some r ← f declName then
281-
unless r == unfoldName do
282-
throwError "invalid unfold theorem name `{r}` has been generated expected `{unfoldName}`"
283-
return some r
284-
if nonRec then
285-
return (← mkSimpleEqThm declName)
286-
return none
295+
withoutExporting do
296+
let env := (← getEnv)
297+
let unfoldName := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
298+
299+
-- Search in the name space of the defininig module, can happen with `import all`.
300+
-- TODO: Should we always use `mkPrivateName` with as if we are in that module
301+
-- for realizable names?
302+
if let some mod ← findModuleOf? declName then
303+
let unfoldName' := mkPrivateNameCore mod (privateToUserName unfoldName)
304+
if env.contains unfoldName' then
305+
return some unfoldName'
306+
307+
if env.contains unfoldName then
308+
return some unfoldName
309+
if (← shouldGenerateEqnThms declName) then
310+
for f in (← getUnfoldEqnFnsRef.get) do
311+
if let some r ← f declName then
312+
unless r == unfoldName do
313+
throwError "invalid unfold theorem name `{r}` has been generated expected `{unfoldName}`"
314+
return some r
315+
if nonRec then
316+
return (← mkSimpleEqThm declName)
317+
return none
287318

288319
builtin_initialize
289320
registerReservedNameAction fun name => do
290-
let .str p s := name | return false
291-
unless (← getEnv).isSafeDefinition p && !isMatcherCore (← getEnv) p do return false
292-
if isEqnReservedNameSuffix s then
293-
return (← MetaM.run' <| getEqnsFor? p).isSome
294-
if s == unfoldThmSuffix then
295-
return (← MetaM.run' <| getUnfoldEqnFor? p (nonRec := true)).isSome
321+
if let some (declName, suffix) := declFromEqLikeName (← getEnv) name then
322+
if name == mkEqLikeNameFor (← getEnv) declName suffix then
323+
if isEqnReservedNameSuffix suffix then
324+
return (← MetaM.run' <| getEqnsFor? declName).isSome
325+
if suffix == unfoldThmSuffix then
326+
return (← MetaM.run' <| getUnfoldEqnFor? declName (nonRec := true)).isSome
296327
return false
297328

298329
end Lean.Meta

‎src/Lean/ReservedNameAction.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ def realizeGlobalName (id : Name) : CoreM (List (Name × List String)) := do
4949
return (← getEnv).containsOnBranch c
5050
catch ex =>
5151
-- We record the error produced by the reserved name action generator
52-
logError m!"Failed to realize constant {id}:{indentD ex.toMessageData}"
52+
logError m!"Failed to realize constant {id} (resolved to {c}):{indentD ex.toMessageData}"
5353
return false
5454

5555
/--

0 commit comments

Comments
 (0)