From f6d1e48cb8bcb7c235365d78098cf72cd9879922 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Jun 2022 17:19:54 -0700 Subject: [PATCH] fix: `constant` => `opaque` issues --- src/Init/Data/Array/Subarray.lean | 2 +- src/Init/Meta.lean | 6 +++--- src/Init/System/IO.lean | 6 +++--- src/Init/System/Platform.lean | 6 +++--- src/Lean/Compiler/FFI.lean | 4 ++-- src/Lean/Compiler/InitAttr.lean | 4 ++-- src/Lean/Elab/Quotation/Precheck.lean | 2 +- src/Lean/Elab/Tactic/Basic.lean | 2 +- src/Lean/Elab/Tactic/Config.lean | 2 +- src/Lean/Level.lean | 2 +- src/Lean/Meta/Basic.lean | 10 +++++----- src/Lean/Meta/Constructions.lean | 16 ++++++++-------- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 4 ++-- src/Lean/PrettyPrinter/Formatter.lean | 4 ++-- src/Lean/PrettyPrinter/Parenthesizer.lean | 6 +++--- src/Std/ShareCommon.lean | 4 ++-- src/lake | 2 +- 17 files changed, 41 insertions(+), 41 deletions(-) diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean index 12673e94d7..dfdb0a598b 100644 --- a/src/Init/Data/Array/Subarray.lean +++ b/src/Init/Data/Array/Subarray.lean @@ -58,7 +58,7 @@ def popFront (s : Subarray α) : Subarray α := -- TODO: provide reference implementation @[implementedBy Subarray.forInUnsafe] -protected constant forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β := +protected opaque forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β := pure b instance : ForIn m (Subarray α) α where diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 9f80fa21f5..655849f222 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -11,15 +11,15 @@ import Init.Data.Array.Basic namespace Lean @[extern c inline "lean_box(LEAN_VERSION_MAJOR)"] -private constant version.getMajor (u : Unit) : Nat +private opaque version.getMajor (u : Unit) : Nat def version.major : Nat := version.getMajor () @[extern c inline "lean_box(LEAN_VERSION_MINOR)"] -private constant version.getMinor (u : Unit) : Nat +private opaque version.getMinor (u : Unit) : Nat def version.minor : Nat := version.getMinor () @[extern c inline "lean_box(LEAN_VERSION_PATCH)"] -private constant version.getPatch (u : Unit) : Nat +private opaque version.getPatch (u : Unit) : Nat def version.patch : Nat := version.getPatch () @[extern "lean_get_githash"] diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index c861406cfd..b58810557b 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -88,15 +88,15 @@ set_option compiler.extract_closed false in @[inline] unsafe def unsafeIO (fn : IO α) : Except IO.Error α := unsafeEIO fn -@[extern "lean_io_timeit"] constant timeit (msg : @& String) (fn : IO α) : IO α -@[extern "lean_io_allocprof"] constant allocprof (msg : @& String) (fn : IO α) : IO α +@[extern "lean_io_timeit"] opaque timeit (msg : @& String) (fn : IO α) : IO α +@[extern "lean_io_allocprof"] opaque allocprof (msg : @& String) (fn : IO α) : IO α /- Programs can execute IO actions during initialization that occurs before the `main` function is executed. The attribute `[init ]` specifies which IO action is executed to set the value of an opaque constant. The action `initializing` returns `true` iff it is invoked during initialization. -/ -@[extern "lean_io_initializing"] constant IO.initializing : BaseIO Bool +@[extern "lean_io_initializing"] opaque IO.initializing : BaseIO Bool namespace BaseIO diff --git a/src/Init/System/Platform.lean b/src/Init/System/Platform.lean index 64c5d4f8cb..4835512d32 100644 --- a/src/Init/System/Platform.lean +++ b/src/Init/System/Platform.lean @@ -9,9 +9,9 @@ import Init.Data.Nat.Basic namespace System namespace Platform -@[extern "lean_system_platform_windows"] constant getIsWindows : Unit → Bool -@[extern "lean_system_platform_osx"] constant getIsOSX : Unit → Bool -@[extern "lean_system_platform_emscripten"] constant getIsEmscripten : Unit → Bool +@[extern "lean_system_platform_windows"] opaque getIsWindows : Unit → Bool +@[extern "lean_system_platform_osx"] opaque getIsOSX : Unit → Bool +@[extern "lean_system_platform_emscripten"] opaque getIsEmscripten : Unit → Bool def isWindows : Bool := getIsWindows () def isOSX : Bool := getIsOSX () diff --git a/src/Lean/Compiler/FFI.lean b/src/Lean/Compiler/FFI.lean index a74815ffda..f0480df81f 100644 --- a/src/Lean/Compiler/FFI.lean +++ b/src/Lean/Compiler/FFI.lean @@ -9,14 +9,14 @@ open System namespace Lean.Compiler.FFI @[extern "lean_get_leanc_extra_flags"] -private constant getLeancExtraFlags : Unit → String +private opaque getLeancExtraFlags : Unit → String /-- Return C compiler flags for including Lean's headers. -/ def getCFlags (leanSysroot : FilePath) : Array String := #["-I", (leanSysroot / "include").toString] ++ (getLeancExtraFlags ()).trim.splitOn @[extern "lean_get_linker_flags"] -private constant getBuiltinLinkerFlags (linkStatic : Bool) : String +private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String /-- Return linker flags for linking against Lean's libraries. -/ def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) : Array String := diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index 68b300d32f..5ead5894f3 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/src/Lean/Compiler/InitAttr.lean @@ -26,11 +26,11 @@ private def isIOUnit (type : Expr) : Bool := Return `false` if the initializer is not available as native code. Initializers do not have corresponding Lean definitions, so they cannot be interpreted in this case. -/ @[extern "lean_run_mod_init"] -unsafe constant runModInit (mod : Name) : IO Bool +unsafe opaque runModInit (mod : Name) : IO Bool /-- Run the initializer for `decl` and store its value for global access. Should only be used while importing. -/ @[extern "lean_run_init"] -unsafe constant runInit (env : @& Environment) (opts : @& Options) (decl initDecl : @& Name) : IO Unit +unsafe opaque runInit (env : @& Environment) (opts : @& Options) (decl initDecl : @& Name) : IO Unit unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) : IO (ParametricAttribute Name) := registerParametricAttribute { diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean index e971b878b2..b701cf71a6 100644 --- a/src/Lean/Elab/Quotation/Precheck.lean +++ b/src/Lean/Elab/Quotation/Precheck.lean @@ -48,7 +48,7 @@ and calling `precheck` recursively on nested terms, potentially with an extended Macros without registered precheck hook are unfolded, and identifier-less syntax is ultimately assumed to be well-formed.", valueTypeName := ``Precheck } `Lean.Elab.Term.Quotation.precheckAttribute -@[builtinInit mkPrecheckAttribute] constant precheckAttribute : KeyedDeclsAttribute Precheck +@[builtinInit mkPrecheckAttribute] opaque precheckAttribute : KeyedDeclsAttribute Precheck partial def precheck : Precheck := fun stx => do if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 9c75cf3b15..8a53d25144 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -110,7 +110,7 @@ protected def getMainModule : TacticM Name := do pure (← getEnv).mai unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) := mkElabAttribute Tactic `Lean.Elab.Tactic.tacticElabAttribute `builtinTactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic" -@[builtinInit mkTacticAttribute] constant tacticElabAttribute : KeyedDeclsAttribute Tactic +@[builtinInit mkTacticAttribute] opaque tacticElabAttribute : KeyedDeclsAttribute Tactic def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info := return Info.ofTacticInfo { diff --git a/src/Lean/Elab/Tactic/Config.lean b/src/Lean/Elab/Tactic/Config.lean index 3c949b5f3e..1e58147578 100644 --- a/src/Lean/Elab/Tactic/Config.lean +++ b/src/Lean/Elab/Tactic/Config.lean @@ -11,7 +11,7 @@ open Meta macro "declare_config_elab" elabName:ident type:ident : command => `(unsafe def evalUnsafe (e : Expr) : TermElabM $type := Term.evalExpr $type ``$type e - @[implementedBy evalUnsafe] constant eval (e : Expr) : TermElabM $type + @[implementedBy evalUnsafe] opaque eval (e : Expr) : TermElabM $type def $elabName (optConfig : Syntax) : TermElabM $type := do if optConfig.isNone then return { : $type } diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index c692cd8811..4ec9e052d2 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -231,7 +231,7 @@ def toNat (lvl : Level) : Option Nat := | _ => none @[extern "lean_level_eq"] -protected constant beq (a : @& Level) (b : @& Level) : Bool +protected opaque beq (a : @& Level) (b : @& Level) : Bool instance : BEq Level := ⟨Level.beq⟩ diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 5485e50996..bc4ec31f8b 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -307,12 +307,12 @@ def useEtaStruct (inductName : Name) : MetaM Bool := do /-- Reduces an expression to its Weak Head Normal Form. This is when the topmost expression has been fully reduced, but may contain subexpressions which have not been reduced. -/ -@[extern 6 "lean_whnf"] constant whnf : Expr → MetaM Expr +@[extern 6 "lean_whnf"] opaque whnf : Expr → MetaM Expr /-- Returns the inferred type of the given expression, or fails if it is not type-correct. -/ -@[extern 6 "lean_infer_type"] constant inferType : Expr → MetaM Expr -@[extern 7 "lean_is_expr_def_eq"] constant isExprDefEqAux : Expr → Expr → MetaM Bool -@[extern 7 "lean_is_level_def_eq"] constant isLevelDefEqAux : Level → Level → MetaM Bool -@[extern 6 "lean_synth_pending"] protected constant synthPending : MVarId → MetaM Bool +@[extern 6 "lean_infer_type"] opaque inferType : Expr → MetaM Expr +@[extern 7 "lean_is_expr_def_eq"] opaque isExprDefEqAux : Expr → Expr → MetaM Bool +@[extern 7 "lean_is_level_def_eq"] opaque isLevelDefEqAux : Level → Level → MetaM Bool +@[extern 6 "lean_synth_pending"] protected opaque synthPending : MVarId → MetaM Bool def whnfForall (e : Expr) : MetaM Expr := do let e' ← whnf e diff --git a/src/Lean/Meta/Constructions.lean b/src/Lean/Meta/Constructions.lean index ee9ecfcdb7..5c99f73bcb 100644 --- a/src/Lean/Meta/Constructions.lean +++ b/src/Lean/Meta/Constructions.lean @@ -8,15 +8,15 @@ import Lean.Meta.AppBuilder namespace Lean -@[extern "lean_mk_cases_on"] constant mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment -@[extern "lean_mk_rec_on"] constant mkRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment -@[extern "lean_mk_no_confusion"] constant mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Environment -@[extern "lean_mk_below"] constant mkBelowImp (env : Environment) (declName : @& Name) : Except KernelException Environment -@[extern "lean_mk_ibelow"] constant mkIBelowImp (env : Environment) (declName : @& Name) : Except KernelException Environment -@[extern "lean_mk_brec_on"] constant mkBRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment -@[extern "lean_mk_binduction_on"] constant mkBInductionOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_rec_on"] opaque mkRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_below"] opaque mkBelowImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_ibelow"] opaque mkIBelowImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_brec_on"] opaque mkBRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment +@[extern "lean_mk_binduction_on"] opaque mkBInductionOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment -variable {m} [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] +variable [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] @[inline] private def adaptFn (f : Environment → Name → Except KernelException Environment) (declName : Name) : m Unit := do match f (← getEnv) declName with diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 6bcd336b6c..b2ee14cabb 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -113,7 +113,7 @@ unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) := is tried first.", valueTypeName := `Lean.PrettyPrinter.Delaborator.Delab } `Lean.PrettyPrinter.Delaborator.delabAttribute -@[builtinInit mkDelabAttribute] constant delabAttribute : KeyedDeclsAttribute Delab +@[builtinInit mkDelabAttribute] opaque delabAttribute : KeyedDeclsAttribute Delab def getExprKind : DelabM Name := do let e ← getExpr @@ -267,7 +267,7 @@ to true or `pp.notation` is set to false, it will not be called at all.", evalKey := fun _ stx => do resolveGlobalConstNoOverloadCore (← Attribute.Builtin.getId stx) } `Lean.PrettyPrinter.Delaborator.appUnexpanderAttribute -@[builtinInit mkAppUnexpanderAttribute] constant appUnexpanderAttribute : KeyedDeclsAttribute Unexpander +@[builtinInit mkAppUnexpanderAttribute] opaque appUnexpanderAttribute : KeyedDeclsAttribute Unexpander end Delaborator diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 90833ecb11..b8e8177110 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -70,7 +70,7 @@ unsafe def mkFormatterAttribute : IO (KeyedDeclsAttribute Formatter) := if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id else throwError "invalid [formatter] argument, unknown syntax kind '{id}'" } `Lean.PrettyPrinter.formatterAttribute -@[builtinInit mkFormatterAttribute] constant formatterAttribute : KeyedDeclsAttribute Formatter +@[builtinInit mkFormatterAttribute] opaque formatterAttribute : KeyedDeclsAttribute Formatter unsafe def mkCombinatorFormatterAttribute : IO ParserCompiler.CombinatorAttribute := ParserCompiler.registerCombinatorAttribute @@ -81,7 +81,7 @@ unsafe def mkCombinatorFormatterAttribute : IO ParserCompiler.CombinatorAttribut Note that, unlike with [formatter], this is not a node kind since combinators usually do not introduce their own node kinds. The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced with `Formatter` in the parameter types." -@[builtinInit mkCombinatorFormatterAttribute] constant combinatorFormatterAttribute : ParserCompiler.CombinatorAttribute +@[builtinInit mkCombinatorFormatterAttribute] opaque combinatorFormatterAttribute : ParserCompiler.CombinatorAttribute namespace Formatter diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 748617dd03..79530d0103 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -127,7 +127,7 @@ unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) := if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id else throwError "invalid [parenthesizer] argument, unknown syntax kind '{id}'" } `Lean.PrettyPrinter.parenthesizerAttribute -@[builtinInit mkParenthesizerAttribute] constant parenthesizerAttribute : KeyedDeclsAttribute Parenthesizer +@[builtinInit mkParenthesizerAttribute] opaque parenthesizerAttribute : KeyedDeclsAttribute Parenthesizer abbrev CategoryParenthesizer := (prec : Nat) → Parenthesizer @@ -148,7 +148,7 @@ unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryPa if Parser.isParserCategory env id then pure id else throwError "invalid [categoryParenthesizer] argument, unknown parser category '{toString id}'" } `Lean.PrettyPrinter.categoryParenthesizerAttribute -@[builtinInit mkCategoryParenthesizerAttribute] constant categoryParenthesizerAttribute : KeyedDeclsAttribute CategoryParenthesizer +@[builtinInit mkCategoryParenthesizerAttribute] opaque categoryParenthesizerAttribute : KeyedDeclsAttribute CategoryParenthesizer unsafe def mkCombinatorParenthesizerAttribute : IO ParserCompiler.CombinatorAttribute := ParserCompiler.registerCombinatorAttribute @@ -159,7 +159,7 @@ unsafe def mkCombinatorParenthesizerAttribute : IO ParserCompiler.CombinatorAttr Note that, unlike with [parenthesizer], this is not a node kind since combinators usually do not introduce their own node kinds. The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced with `Parenthesizer` in the parameter types." -@[builtinInit mkCombinatorParenthesizerAttribute] constant combinatorParenthesizerAttribute : ParserCompiler.CombinatorAttribute +@[builtinInit mkCombinatorParenthesizerAttribute] opaque combinatorParenthesizerAttribute : ParserCompiler.CombinatorAttribute namespace Parenthesizer diff --git a/src/Std/ShareCommon.lean b/src/Std/ShareCommon.lean index 4c107bddb3..d10a871793 100644 --- a/src/Std/ShareCommon.lean +++ b/src/Std/ShareCommon.lean @@ -27,10 +27,10 @@ unsafe abbrev Object.ptrHash (a : Object) : UInt64 := ptrAddrUnsafe a |>.toUInt64 @[extern "lean_sharecommon_eq"] -unsafe constant Object.eq (a b : @& Object) : Bool +unsafe opaque Object.eq (a b : @& Object) : Bool @[extern "lean_sharecommon_hash"] -unsafe constant Object.hash (a : @& Object) : UInt64 +unsafe opaque Object.hash (a : @& Object) : UInt64 unsafe def ObjectMap : Type := @HashMap Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩ unsafe def ObjectSet : Type := @HashSet Object ⟨Object.eq⟩ ⟨Object.hash⟩ diff --git a/src/lake b/src/lake index 535822481d..3fb0c2f110 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit 535822481d9a289b482d7c725bf588ad55f00642 +Subproject commit 3fb0c2f110d0ff95c1bd41da0259e8f7e77003c0