From 02c4e548dfe511f08e6542a3d002454cc15a4803 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Jun 2022 16:56:38 -0700 Subject: [PATCH] feat: replace `constant` with `opaque` --- src/Init/Control/Basic.lean | 4 +- src/Init/Core.lean | 4 +- src/Init/Data/Float.lean | 76 ++++++++++----------- src/Init/Data/String/Extra.lean | 4 +- src/Init/Meta.lean | 8 +-- src/Init/Prelude.lean | 26 ++++---- src/Init/System/IO.lean | 80 +++++++++++------------ src/Init/System/ST.lean | 14 ++-- src/Lean/Attributes.lean | 2 +- src/Lean/Compiler/ExternAttr.lean | 2 +- src/Lean/Compiler/IR/Checker.lean | 6 +- src/Lean/Compiler/IR/CtorLayout.lean | 2 +- src/Lean/Compiler/InitAttr.lean | 2 +- src/Lean/Declaration.lean | 4 +- src/Lean/Elab/BuiltinCommand.lean | 2 +- src/Lean/Elab/Command.lean | 2 +- src/Lean/Elab/Term.lean | 2 +- src/Lean/Elab/Util.lean | 4 +- src/Lean/Environment.lean | 30 ++++----- src/Lean/Expr.lean | 30 ++++----- src/Lean/LoadDynlib.lean | 2 +- src/Lean/Meta/ACLt.lean | 2 +- src/Lean/Meta/Match/MatchEqsExt.lean | 2 +- src/Lean/Meta/WHNF.lean | 6 +- src/Lean/Parser/Extension.lean | 4 +- src/Lean/PrettyPrinter/Formatter.lean | 6 +- src/Lean/PrettyPrinter/Parenthesizer.lean | 6 +- src/Lean/Runtime.lean | 4 +- src/Lean/ScopedEnvExtension.lean | 2 +- src/Lean/Util/FindExpr.lean | 2 +- src/Lean/Util/FoldConsts.lean | 2 +- src/Lean/Util/HasConstCache.lean | 2 +- src/Std/ShareCommon.lean | 8 +-- src/lake | 2 +- 34 files changed, 177 insertions(+), 177 deletions(-) diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean index f4630fb3e0..23394c7b76 100644 --- a/src/Init/Control/Basic.lean +++ b/src/Init/Control/Basic.lean @@ -75,8 +75,8 @@ Suppose we have `foo : ∀ α, IO α → IO α` and `bar : StateT σ IO β` (ie, We might want to 'map' `bar` by `foo`. Concretely we would write this as: ```lean -constant foo : ∀ {α}, IO α → IO α -constant bar : StateT σ IO β +opaque foo : ∀ {α}, IO α → IO α +opaque bar : StateT σ IO β def mapped_foo : StateT σ IO β := do let s ← get diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 91ed3a4d6e..8b07a1e298 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1109,7 +1109,7 @@ namespace Lean If an extern function is executed, then the trusted code base will also include the implementation of the associated foreign function. -/ -constant reduceBool (b : Bool) : Bool := b +opaque reduceBool (b : Bool) : Bool := b /-- Similar to `Lean.reduceBool` for closed `Nat` terms. @@ -1117,7 +1117,7 @@ constant reduceBool (b : Bool) : Bool := b Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α) : α := a`. The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression. We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection). -/ -constant reduceNat (n : Nat) : Nat := n +opaque reduceNat (n : Nat) : Nat := n axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index 6743d7675a..c63ec5d339 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -17,7 +17,7 @@ structure FloatSpec where decLe : DecidableRel le -- Just show FloatSpec is inhabited. -constant floatSpec : FloatSpec := { +opaque floatSpec : FloatSpec := { float := Unit, val := (), lt := fun _ _ => True, @@ -31,11 +31,11 @@ structure Float where instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩ -@[extern "lean_float_add"] constant Float.add : Float → Float → Float -@[extern "lean_float_sub"] constant Float.sub : Float → Float → Float -@[extern "lean_float_mul"] constant Float.mul : Float → Float → Float -@[extern "lean_float_div"] constant Float.div : Float → Float → Float -@[extern "lean_float_negate"] constant Float.neg : Float → Float +@[extern "lean_float_add"] opaque Float.add : Float → Float → Float +@[extern "lean_float_sub"] opaque Float.sub : Float → Float → Float +@[extern "lean_float_mul"] opaque Float.mul : Float → Float → Float +@[extern "lean_float_div"] opaque Float.div : Float → Float → Float +@[extern "lean_float_negate"] opaque Float.neg : Float → Float set_option bootstrap.genMatcherCode false def Float.lt : Float → Float → Prop := fun a b => @@ -53,28 +53,28 @@ instance : Neg Float := ⟨Float.neg⟩ instance : LT Float := ⟨Float.lt⟩ instance : LE Float := ⟨Float.le⟩ -@[extern "lean_float_beq"] constant Float.beq (a b : Float) : Bool +@[extern "lean_float_beq"] opaque Float.beq (a b : Float) : Bool instance : BEq Float := ⟨Float.beq⟩ -@[extern "lean_float_decLt"] constant Float.decLt (a b : Float) : Decidable (a < b) := +@[extern "lean_float_decLt"] opaque Float.decLt (a b : Float) : Decidable (a < b) := match a, b with | ⟨a⟩, ⟨b⟩ => floatSpec.decLt a b -@[extern "lean_float_decLe"] constant Float.decLe (a b : Float) : Decidable (a ≤ b) := +@[extern "lean_float_decLe"] opaque Float.decLe (a b : Float) : Decidable (a ≤ b) := match a, b with | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b -@[extern "lean_float_to_string"] constant Float.toString : Float → String +@[extern "lean_float_to_string"] opaque Float.toString : Float → String -@[extern "lean_float_to_uint8"] constant Float.toUInt8 : Float → UInt8 -@[extern "lean_float_to_uint16"] constant Float.toUInt16 : Float → UInt16 -@[extern "lean_float_to_uint32"] constant Float.toUInt32 : Float → UInt32 -@[extern "lean_float_to_uint64"] constant Float.toUInt64 : Float → UInt64 -@[extern "lean_float_to_usize"] constant Float.toUSize : Float → USize +@[extern "lean_float_to_uint8"] opaque Float.toUInt8 : Float → UInt8 +@[extern "lean_float_to_uint16"] opaque Float.toUInt16 : Float → UInt16 +@[extern "lean_float_to_uint32"] opaque Float.toUInt32 : Float → UInt32 +@[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → UInt64 +@[extern "lean_float_to_usize"] opaque Float.toUSize : Float → USize instance : ToString Float where toString := Float.toString @@ -84,29 +84,29 @@ instance : Repr Float where instance : ReprAtom Float := ⟨⟩ -@[extern "lean_uint64_to_float"] constant UInt64.toFloat (n : UInt64) : Float +@[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float -@[extern "sin"] constant Float.sin : Float → Float -@[extern "cos"] constant Float.cos : Float → Float -@[extern "tan"] constant Float.tan : Float → Float -@[extern "asin"] constant Float.asin : Float → Float -@[extern "acos"] constant Float.acos : Float → Float -@[extern "atan"] constant Float.atan : Float → Float -@[extern "atan2"] constant Float.atan2 : Float → Float → Float -@[extern "sinh"] constant Float.sinh : Float → Float -@[extern "cosh"] constant Float.cosh : Float → Float -@[extern "tanh"] constant Float.tanh : Float → Float -@[extern "asinh"] constant Float.asinh : Float → Float -@[extern "acosh"] constant Float.acosh : Float → Float -@[extern "atanh"] constant Float.atanh : Float → Float -@[extern "exp"] constant Float.exp : Float → Float -@[extern "exp2"] constant Float.exp2 : Float → Float -@[extern "log"] constant Float.log : Float → Float -@[extern "log2"] constant Float.log2 : Float → Float -@[extern "log10"] constant Float.log10 : Float → Float -@[extern "pow"] constant Float.pow : Float → Float → Float -@[extern "sqrt"] constant Float.sqrt : Float → Float -@[extern "cbrt"] constant Float.cbrt : Float → Float +@[extern "sin"] opaque Float.sin : Float → Float +@[extern "cos"] opaque Float.cos : Float → Float +@[extern "tan"] opaque Float.tan : Float → Float +@[extern "asin"] opaque Float.asin : Float → Float +@[extern "acos"] opaque Float.acos : Float → Float +@[extern "atan"] opaque Float.atan : Float → Float +@[extern "atan2"] opaque Float.atan2 : Float → Float → Float +@[extern "sinh"] opaque Float.sinh : Float → Float +@[extern "cosh"] opaque Float.cosh : Float → Float +@[extern "tanh"] opaque Float.tanh : Float → Float +@[extern "asinh"] opaque Float.asinh : Float → Float +@[extern "acosh"] opaque Float.acosh : Float → Float +@[extern "atanh"] opaque Float.atanh : Float → Float +@[extern "exp"] opaque Float.exp : Float → Float +@[extern "exp2"] opaque Float.exp2 : Float → Float +@[extern "log"] opaque Float.log : Float → Float +@[extern "log2"] opaque Float.log2 : Float → Float +@[extern "log10"] opaque Float.log10 : Float → Float +@[extern "pow"] opaque Float.pow : Float → Float → Float +@[extern "sqrt"] opaque Float.sqrt : Float → Float +@[extern "cbrt"] opaque Float.cbrt : Float → Float instance : Pow Float Float := ⟨Float.pow⟩ @@ -114,4 +114,4 @@ instance : Pow Float Float := ⟨Float.pow⟩ Efficiently computes `x * 2^i`. -/ @[extern "lean_float_scaleb"] -constant Float.scaleB (x : Float) (i : @& Int) : Float +opaque Float.scaleB (x : Float) (i : @& Int) : Float diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean index 935faaf1c8..18709a010a 100644 --- a/src/Init/Data/String/Extra.lean +++ b/src/Init/Data/String/Extra.lean @@ -23,10 +23,10 @@ def toNat! (s : String) : Nat := Convert a UTF-8 encoded `ByteArray` string to `String`. The result is unspecified if `a` is not properly UTF-8 encoded. -/ @[extern "lean_string_from_utf8_unchecked"] -constant fromUTF8Unchecked (a : @& ByteArray) : String +opaque fromUTF8Unchecked (a : @& ByteArray) : String @[extern "lean_string_to_utf8"] -constant toUTF8 (a : @& String) : ByteArray +opaque toUTF8 (a : @& String) : ByteArray theorem one_le_csize (c : Char) : 1 ≤ csize c := by simp [csize, Char.utf8Size] diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index ebc3b487bd..9f80fa21f5 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -23,16 +23,16 @@ private constant version.getPatch (u : Unit) : Nat def version.patch : Nat := version.getPatch () @[extern "lean_get_githash"] -constant getGithash (u : Unit) : String +opaque getGithash (u : Unit) : String def githash : String := getGithash () @[extern c inline "LEAN_VERSION_IS_RELEASE"] -constant version.getIsRelease (u : Unit) : Bool +opaque version.getIsRelease (u : Unit) : Bool def version.isRelease : Bool := version.getIsRelease () /-- Additional version description like "nightly-2018-03-11" -/ @[extern c inline "lean_mk_string(LEAN_SPECIAL_VERSION_DESC)"] -constant version.getSpecialDesc (u : Unit) : String +opaque version.getSpecialDesc (u : Unit) : String def version.specialDesc : String := version.getSpecialDesc () def versionStringCore := @@ -61,7 +61,7 @@ def toolchain := "" @[extern c inline "LEAN_IS_STAGE0"] -constant Internal.isStage0 (u : Unit) : Bool +opaque Internal.isStage0 (u : Unit) : Bool /- Valid identifier names -/ def isGreek (c : Char) : Bool := diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index c0f1466fee..17f767d578 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -89,14 +89,14 @@ theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} ( /- Initialize the Quotient Module, which effectively adds the following definitions: -constant Quot {α : Sort u} (r : α → α → Prop) : Sort u +opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u -constant Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r +opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r -constant Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) : +opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) : (∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β -constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} : +opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} : (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q -/ init_quot @@ -795,7 +795,7 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat instance : Sub Nat where sub := Nat.sub -@[extern "lean_system_platform_nbits"] constant System.Platform.getNumBits : Unit → Subtype fun (n : Nat) => Or (Eq n 32) (Eq n 64) := +@[extern "lean_system_platform_nbits"] opaque System.Platform.getNumBits : Unit → Subtype fun (n : Nat) => Or (Eq n 32) (Eq n 64) := fun _ => ⟨64, Or.inr rfl⟩ -- inhabitant def System.Platform.numBits : Nat := @@ -1207,7 +1207,7 @@ unsafe def unsafeCast {α : Type u} {β : Type v} (a : α) : β := ULift.down.{max u v} (cast lcProof (ULift.up.{max u v} a)) @[neverExtract, extern "lean_panic_fn"] -constant panicCore {α : Type u} [Inhabited α] (msg : String) : α +opaque panicCore {α : Type u} [Inhabited α] (msg : String) : α /- This is workaround for `panic` occurring in monadic code. See issue #695. @@ -1714,16 +1714,16 @@ class Hashable (α : Sort u) where export Hashable (hash) @[extern "lean_uint64_to_usize"] -constant UInt64.toUSize (u : UInt64) : USize +opaque UInt64.toUSize (u : UInt64) : USize @[extern "lean_usize_to_uint64"] -constant USize.toUInt64 (u : USize) : UInt64 +opaque USize.toUInt64 (u : USize) : UInt64 @[extern "lean_uint64_mix_hash"] -constant mixHash (u₁ u₂ : UInt64) : UInt64 +opaque mixHash (u₁ u₂ : UInt64) : UInt64 @[extern "lean_string_hash"] -protected constant String.hash (s : @& String) : UInt64 +protected opaque String.hash (s : @& String) : UInt64 instance : Hashable String where hash := String.hash @@ -2226,7 +2226,7 @@ end Syntax namespace Macro /- References -/ -private constant MethodsRefPointed : NonemptyType.{0} +private opaque MethodsRefPointed : NonemptyType.{0} private def MethodsRef : Type := MethodsRefPointed.type @@ -2302,7 +2302,7 @@ unsafe def mkMethodsImp (methods : Methods) : MethodsRef := unsafeCast methods @[implementedBy mkMethodsImp] -constant mkMethods (methods : Methods) : MethodsRef +opaque mkMethods (methods : Methods) : MethodsRef instance : Inhabited MethodsRef where default := mkMethods default @@ -2310,7 +2310,7 @@ instance : Inhabited MethodsRef where unsafe def getMethodsImp : MacroM Methods := bind read fun ctx => pure (unsafeCast (ctx.methods)) -@[implementedBy getMethodsImp] constant getMethods : MacroM Methods +@[implementedBy getMethodsImp] opaque getMethods : MacroM Methods /-- `expandMacro? stx` return `some stxNew` if `stx` is a macro, and `stxNew` is its expansion. -/ def expandMacro? (stx : Syntax) : MacroM (Option Syntax) := do diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 747896b959..c861406cfd 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -109,17 +109,17 @@ namespace BaseIO to the task is dropped. The `act` should manually check for cancellation via `IO.checkCanceled` if it wants to react to that. -/ @[extern "lean_io_as_task"] -constant asTask (act : BaseIO α) (prio := Task.Priority.default) : BaseIO (Task α) := +opaque asTask (act : BaseIO α) (prio := Task.Priority.default) : BaseIO (Task α) := Task.pure <$> act /-- See `BaseIO.asTask`. -/ @[extern "lean_io_map_task"] -constant mapTask (f : α → BaseIO β) (t : Task α) (prio := Task.Priority.default) : BaseIO (Task β) := +opaque mapTask (f : α → BaseIO β) (t : Task α) (prio := Task.Priority.default) : BaseIO (Task β) := Task.pure <$> f t.get /-- See `BaseIO.asTask`. -/ @[extern "lean_io_bind_task"] -constant bindTask (t : Task α) (f : α → BaseIO (Task β)) (prio := Task.Priority.default) : BaseIO (Task β) := +opaque bindTask (t : Task α) (f : α → BaseIO (Task β)) (prio := Task.Priority.default) : BaseIO (Task β) := f t.get def mapTasks (f : List α → BaseIO β) (tasks : List (Task α)) (prio := Task.Priority.default) : BaseIO (Task β) := @@ -163,14 +163,14 @@ def lazyPure (fn : Unit → α) : IO α := pure (fn ()) /-- Monotonically increasing time since an unspecified past point in milliseconds. No relation to wall clock time. -/ -@[extern "lean_io_mono_ms_now"] constant monoMsNow : BaseIO Nat +@[extern "lean_io_mono_ms_now"] opaque monoMsNow : BaseIO Nat /-- Monotonically increasing time since an unspecified past point in nanoseconds. No relation to wall clock time. -/ -@[extern "lean_io_mono_nanos_now"] constant monoNanosNow : BaseIO Nat +@[extern "lean_io_mono_nanos_now"] opaque monoNanosNow : BaseIO Nat /-- Read bytes from a system entropy source. Not guaranteed to be cryptographically secure. If `nBytes = 0`, return immediately with an empty buffer. -/ -@[extern "lean_io_get_random_bytes"] constant getRandomBytes (nBytes : USize) : IO ByteArray +@[extern "lean_io_get_random_bytes"] opaque getRandomBytes (nBytes : USize) : IO ByteArray def sleep (ms : UInt32) : IO Unit := -- TODO: add a proper primitive for IO.sleep @@ -193,28 +193,28 @@ def sleep (ms : UInt32) : IO Unit := EIO.mapTasks f tasks prio /-- Check if the task's cancellation flag has been set by calling `IO.cancel` or dropping the last reference to the task. -/ -@[extern "lean_io_check_canceled"] constant checkCanceled : BaseIO Bool +@[extern "lean_io_check_canceled"] opaque checkCanceled : BaseIO Bool /-- Request cooperative cancellation of the task. The task must explicitly call `IO.checkCanceled` to react to the cancellation. -/ -@[extern "lean_io_cancel"] constant cancel : @& Task α → BaseIO Unit +@[extern "lean_io_cancel"] opaque cancel : @& Task α → BaseIO Unit /-- Check if the task has finished execution, at which point calling `Task.get` will return immediately. -/ -@[extern "lean_io_has_finished"] constant hasFinished : @& Task α → BaseIO Bool +@[extern "lean_io_has_finished"] opaque hasFinished : @& Task α → BaseIO Bool /-- Wait for the task to finish, then return its result. -/ -@[extern "lean_io_wait"] constant wait (t : Task α) : BaseIO α := +@[extern "lean_io_wait"] opaque wait (t : Task α) : BaseIO α := return t.get /-- Wait until any of the tasks in the given list has finished, then return its result. -/ -@[extern "lean_io_wait_any"] constant waitAny : @& List (Task α) → IO α +@[extern "lean_io_wait_any"] opaque waitAny : @& List (Task α) → IO α /-- Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread. -/ -@[extern "lean_io_get_num_heartbeats"] constant getNumHeartbeats : BaseIO Nat +@[extern "lean_io_get_num_heartbeats"] opaque getNumHeartbeats : BaseIO Nat inductive FS.Mode where | read | write | readWrite | append -constant FS.Handle : Type := Unit +opaque FS.Handle : Type := Unit /-- A pure-Lean abstraction of POSIX streams. We use `Stream`s for the standard streams stdin/stdout/stderr so we can @@ -230,16 +230,16 @@ structure FS.Stream where open FS -@[extern "lean_get_stdin"] constant getStdin : BaseIO FS.Stream -@[extern "lean_get_stdout"] constant getStdout : BaseIO FS.Stream -@[extern "lean_get_stderr"] constant getStderr : BaseIO FS.Stream +@[extern "lean_get_stdin"] opaque getStdin : BaseIO FS.Stream +@[extern "lean_get_stdout"] opaque getStdout : BaseIO FS.Stream +@[extern "lean_get_stderr"] opaque getStderr : BaseIO FS.Stream /-- Replaces the stdin stream of the current thread and returns its previous value. -/ -@[extern "lean_get_set_stdin"] constant setStdin : FS.Stream → BaseIO FS.Stream +@[extern "lean_get_set_stdin"] opaque setStdin : FS.Stream → BaseIO FS.Stream /-- Replaces the stdout stream of the current thread and returns its previous value. -/ -@[extern "lean_get_set_stdout"] constant setStdout : FS.Stream → BaseIO FS.Stream +@[extern "lean_get_set_stdout"] opaque setStdout : FS.Stream → BaseIO FS.Stream /-- Replaces the stderr stream of the current thread and returns its previous value. -/ -@[extern "lean_get_set_stderr"] constant setStderr : FS.Stream → BaseIO FS.Stream +@[extern "lean_get_set_stderr"] opaque setStderr : FS.Stream → BaseIO FS.Stream @[specialize] partial def iterate (a : α) (f : α → IO (Sum α β)) : IO β := do let v ← f a @@ -261,7 +261,7 @@ private def fopenFlags (m : FS.Mode) (b : Bool) : String := let bin := if b then "b" else "t" mode ++ bin -@[extern "lean_io_prim_handle_mk"] constant mkPrim (fn : @& FilePath) (mode : @& String) : IO Handle +@[extern "lean_io_prim_handle_mk"] opaque mkPrim (fn : @& FilePath) (mode : @& String) : IO Handle def mk (fn : FilePath) (Mode : Mode) (bin : Bool := true) : IO Handle := mkPrim fn (fopenFlags Mode bin) @@ -271,27 +271,27 @@ Returns whether the end of the file has been reached while reading a file. `h.isEof` returns true /after/ the first attempt at reading past the end of `h`. Once `h.isEof` is true, reading `h` will always return an empty array. -/ -@[extern "lean_io_prim_handle_is_eof"] constant isEof (h : @& Handle) : BaseIO Bool -@[extern "lean_io_prim_handle_flush"] constant flush (h : @& Handle) : IO Unit -@[extern "lean_io_prim_handle_read"] constant read (h : @& Handle) (bytes : USize) : IO ByteArray -@[extern "lean_io_prim_handle_write"] constant write (h : @& Handle) (buffer : @& ByteArray) : IO Unit +@[extern "lean_io_prim_handle_is_eof"] opaque isEof (h : @& Handle) : BaseIO Bool +@[extern "lean_io_prim_handle_flush"] opaque flush (h : @& Handle) : IO Unit +@[extern "lean_io_prim_handle_read"] opaque read (h : @& Handle) (bytes : USize) : IO ByteArray +@[extern "lean_io_prim_handle_write"] opaque write (h : @& Handle) (buffer : @& ByteArray) : IO Unit -@[extern "lean_io_prim_handle_get_line"] constant getLine (h : @& Handle) : IO String -@[extern "lean_io_prim_handle_put_str"] constant putStr (h : @& Handle) (s : @& String) : IO Unit +@[extern "lean_io_prim_handle_get_line"] opaque getLine (h : @& Handle) : IO String +@[extern "lean_io_prim_handle_put_str"] opaque putStr (h : @& Handle) (s : @& String) : IO Unit end Handle -@[extern "lean_io_realpath"] constant realPath (fname : FilePath) : IO FilePath -@[extern "lean_io_remove_file"] constant removeFile (fname : @& FilePath) : IO Unit +@[extern "lean_io_realpath"] opaque realPath (fname : FilePath) : IO FilePath +@[extern "lean_io_remove_file"] opaque removeFile (fname : @& FilePath) : IO Unit /-- Remove given directory. Fails if not empty; see also `IO.FS.removeDirAll`. -/ -@[extern "lean_io_remove_dir"] constant removeDir : @& FilePath → IO Unit -@[extern "lean_io_create_dir"] constant createDir : @& FilePath → IO Unit +@[extern "lean_io_remove_dir"] opaque removeDir : @& FilePath → IO Unit +@[extern "lean_io_create_dir"] opaque createDir : @& FilePath → IO Unit end FS -@[extern "lean_io_getenv"] constant getEnv (var : @& String) : BaseIO (Option String) -@[extern "lean_io_app_path"] constant appPath : IO FilePath -@[extern "lean_io_current_dir"] constant currentDir : IO FilePath +@[extern "lean_io_getenv"] opaque getEnv (var : @& String) : BaseIO (Option String) +@[extern "lean_io_app_path"] opaque appPath : IO FilePath +@[extern "lean_io_current_dir"] opaque currentDir : IO FilePath namespace FS @@ -391,10 +391,10 @@ namespace System.FilePath open IO @[extern "lean_io_read_dir"] -constant readDir : @& FilePath → IO (Array IO.FS.DirEntry) +opaque readDir : @& FilePath → IO (Array IO.FS.DirEntry) @[extern "lean_io_metadata"] -constant metadata : @& FilePath → IO IO.FS.Metadata +opaque metadata : @& FilePath → IO IO.FS.Metadata def isDir (p : FilePath) : BaseIO Bool := do match (← p.metadata.toBaseIO) with @@ -534,9 +534,9 @@ structure Child (cfg : StdioConfig) where stdout : cfg.stdout.toHandleType stderr : cfg.stderr.toHandleType -@[extern "lean_io_process_spawn"] constant spawn (args : SpawnArgs) : IO (Child args.toStdioConfig) +@[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig) -@[extern "lean_io_process_child_wait"] constant Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32 +@[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32 /-- Extract the `stdin` field from a `Child` object, allowing them to be freed independently. @@ -544,7 +544,7 @@ This operation is necessary for closing the child process' stdin while still hol e.g. for `Child.wait`. A file handle is closed when all references to it are dropped, which without this operation includes the `Child` object. -/ -@[extern "lean_io_process_child_take_stdin"] constant Child.takeStdin {cfg : @& StdioConfig} : Child cfg → +@[extern "lean_io_process_child_take_stdin"] opaque Child.takeStdin {cfg : @& StdioConfig} : Child cfg → IO (cfg.stdin.toHandleType × Child { cfg with stdin := Stdio.null }) structure Output where @@ -568,7 +568,7 @@ def run (args : SpawnArgs) : IO String := do throw <| IO.userError <| "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode pure out.stdout -@[extern "lean_io_exit"] constant exit : UInt8 → IO α +@[extern "lean_io_exit"] opaque exit : UInt8 → IO α end Process @@ -594,7 +594,7 @@ def FileRight.flags (acc : FileRight) : UInt32 := let o : UInt32 := acc.other.flags u.lor <| g.lor o -@[extern "lean_chmod"] constant Prim.setAccessRights (filename : @& FilePath) (mode : UInt32) : IO Unit +@[extern "lean_chmod"] opaque Prim.setAccessRights (filename : @& FilePath) (mode : UInt32) : IO Unit def setAccessRights (filename : FilePath) (mode : FileRight) : IO Unit := Prim.setAccessRights filename mode.flags diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean index e9ba87bb90..f5550bcb56 100644 --- a/src/Init/System/ST.lean +++ b/src/Init/System/ST.lean @@ -42,7 +42,7 @@ instance {ε σ} : MonadLift (ST σ) (EST ε σ) := ⟨fun x s => namespace ST /- References -/ -constant RefPointed : NonemptyType.{0} +opaque RefPointed : NonemptyType.{0} structure Ref (σ : Type) (α : Type) : Type where ref : RefPointed.type @@ -59,17 +59,17 @@ private noncomputable def inhabitedFromRef {σ α} (r : Ref σ α) : ST σ α := pure default @[extern "lean_st_mk_ref"] -constant mkRef {σ α} (a : α) : ST σ (Ref σ α) := pure { ref := Classical.choice RefPointed.property, h := Nonempty.intro a } +opaque mkRef {σ α} (a : α) : ST σ (Ref σ α) := pure { ref := Classical.choice RefPointed.property, h := Nonempty.intro a } @[extern "lean_st_ref_get"] -constant Ref.get {σ α} (r : @& Ref σ α) : ST σ α := inhabitedFromRef r +opaque Ref.get {σ α} (r : @& Ref σ α) : ST σ α := inhabitedFromRef r @[extern "lean_st_ref_set"] -constant Ref.set {σ α} (r : @& Ref σ α) (a : α) : ST σ Unit +opaque Ref.set {σ α} (r : @& Ref σ α) (a : α) : ST σ Unit @[extern "lean_st_ref_swap"] -constant Ref.swap {σ α} (r : @& Ref σ α) (a : α) : ST σ α := inhabitedFromRef r +opaque Ref.swap {σ α} (r : @& Ref σ α) (a : α) : ST σ α := inhabitedFromRef r @[extern "lean_st_ref_take"] -unsafe constant Ref.take {σ α} (r : @& Ref σ α) : ST σ α := inhabitedFromRef r +unsafe opaque Ref.take {σ α} (r : @& Ref σ α) : ST σ α := inhabitedFromRef r @[extern "lean_st_ref_ptr_eq"] -constant Ref.ptrEq {σ α} (r1 r2 : @& Ref σ α) : ST σ Bool +opaque Ref.ptrEq {σ α} (r1 r2 : @& Ref σ α) : ST σ Bool @[inline] unsafe def Ref.modifyUnsafe {σ α : Type} (r : Ref σ α) (f : α → α) : ST σ Unit := do let v ← Ref.take r diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index fe825aa107..7e374c3f0f 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -327,7 +327,7 @@ unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options) | _ => throw ("unexpected attribute implementation type at '" ++ toString declName ++ "' (`AttributeImpl` expected") @[implementedBy mkAttributeImplOfConstantUnsafe] -constant mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl +opaque mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl def mkAttributeImplOfEntry (env : Environment) (opts : Options) (e : AttributeExtensionOLeanEntry) : IO AttributeImpl := match e with diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean index 8b8bc43bc0..3095d13e53 100644 --- a/src/Lean/Compiler/ExternAttr.lean +++ b/src/Lean/Compiler/ExternAttr.lean @@ -56,7 +56,7 @@ private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do return { arity? := arity?, entries := entries.toList } @[extern "lean_add_extern"] -constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environment +opaque addExtern (env : Environment) (n : Name) : ExceptT String Id Environment builtin_initialize externAttr : ParametricAttribute ExternAttrData ← registerParametricAttribute { diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean index 91dbf94989..fcd325fba9 100644 --- a/src/Lean/Compiler/IR/Checker.lean +++ b/src/Lean/Compiler/IR/Checker.lean @@ -9,15 +9,15 @@ import Lean.Compiler.IR.Format namespace Lean.IR.Checker @[extern c inline "lean_box(LEAN_MAX_CTOR_FIELDS)"] -constant getMaxCtorFields : Unit → Nat +opaque getMaxCtorFields : Unit → Nat def maxCtorFields := getMaxCtorFields () @[extern c inline "lean_box(LEAN_MAX_CTOR_SCALARS_SIZE)"] -constant getMaxCtorScalarsSize : Unit → Nat +opaque getMaxCtorScalarsSize : Unit → Nat def maxCtorScalarsSize := getMaxCtorScalarsSize () @[extern c inline "lean_box(sizeof(size_t))"] -constant getUSizeSize : Unit → Nat +opaque getUSizeSize : Unit → Nat def usizeSize := getUSizeSize () structure CheckerContext where diff --git a/src/Lean/Compiler/IR/CtorLayout.lean b/src/Lean/Compiler/IR/CtorLayout.lean index 63e472a3b4..94c9d2ed6e 100644 --- a/src/Lean/Compiler/IR/CtorLayout.lean +++ b/src/Lean/Compiler/IR/CtorLayout.lean @@ -35,7 +35,7 @@ structure CtorLayout where scalarSize : Nat @[extern "lean_ir_get_ctor_layout"] -constant getCtorLayout (env : @& Environment) (ctorName : @& Name) : Except String CtorLayout +opaque getCtorLayout (env : @& Environment) (ctorName : @& Name) : Except String CtorLayout end IR end Lean diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index f7dd662a4f..68b300d32f 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/src/Lean/Compiler/InitAttr.lean @@ -70,7 +70,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) : IO } @[implementedBy registerInitAttrUnsafe] -constant registerInitAttr (attrName : Name) (runAfterImport : Bool) : IO (ParametricAttribute Name) +opaque registerInitAttr (attrName : Name) (runAfterImport : Bool) : IO (ParametricAttribute Name) builtin_initialize regularInitAttr : ParametricAttribute Name ← registerInitAttr `init true builtin_initialize builtinInitAttr : ParametricAttribute Name ← registerInitAttr `builtinInit false diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 6b7a7af92a..04e5c5769e 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -403,10 +403,10 @@ def isInductive : ConstantInfo → Bool | _ => false @[extern "lean_instantiate_type_lparams"] -constant instantiateTypeLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr +opaque instantiateTypeLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr @[extern "lean_instantiate_value_lparams"] -constant instantiateValueLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr +opaque instantiateValueLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr end ConstantInfo diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index fc215261c6..776032e3d4 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -355,7 +355,7 @@ unsafe def elabEvalUnsafe : CommandElab | _ => throwUnsupportedSyntax @[builtinCommandElab «eval», implementedBy elabEvalUnsafe] -constant elabEval : CommandElab +opaque elabEval : CommandElab @[builtinCommandElab «synth»] def elabSynth : CommandElab := fun stx => do let term := stx[1] diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index eb05141d39..1befba23f8 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -218,7 +218,7 @@ unsafe def mkCommandElabAttributeUnsafe : IO (KeyedDeclsAttribute CommandElab) : mkElabAttribute CommandElab `Lean.Elab.Command.commandElabAttribute `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" @[implementedBy mkCommandElabAttributeUnsafe] -constant mkCommandElabAttribute : IO (KeyedDeclsAttribute CommandElab) +opaque mkCommandElabAttribute : IO (KeyedDeclsAttribute CommandElab) builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ← mkCommandElabAttribute diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 450207edc0..f08f935a3c 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -320,7 +320,7 @@ unsafe def mkTermElabAttributeUnsafe : IO (KeyedDeclsAttribute TermElab) := mkElabAttribute TermElab `Lean.Elab.Term.termElabAttribute `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" @[implementedBy mkTermElabAttributeUnsafe] -constant mkTermElabAttribute : IO (KeyedDeclsAttribute TermElab) +opaque mkTermElabAttribute : IO (KeyedDeclsAttribute TermElab) builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermElabAttribute diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index b489094361..b79d90f43a 100644 --- a/src/Lean/Elab/Util.lean +++ b/src/Lean/Elab/Util.lean @@ -95,7 +95,7 @@ private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options) env.evalConstCheck Syntax opts `Lean.Syntax constName @[implementedBy evalSyntaxConstantUnsafe] -constant evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw "" +opaque evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw "" unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (parserNamespace : Name) (typeName : Name) (kind : String) : IO (KeyedDeclsAttribute γ) := @@ -117,7 +117,7 @@ unsafe def mkMacroAttributeUnsafe : IO (KeyedDeclsAttribute Macro) := mkElabAttribute Macro `Lean.Elab.macroAttribute `builtinMacro `macro Name.anonymous `Lean.Macro "macro" @[implementedBy mkMacroAttributeUnsafe] -constant mkMacroAttribute : IO (KeyedDeclsAttribute Macro) +opaque mkMacroAttribute : IO (KeyedDeclsAttribute Macro) builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index ab86a7b9ad..7a568fbb98 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -14,7 +14,7 @@ import Lean.Util.Profile namespace Lean /- Opaque environment extension state. -/ -constant EnvExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩ +opaque EnvExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩ def EnvExtensionState : Type := EnvExtensionStateSpec.fst instance : Inhabited EnvExtensionState := EnvExtensionStateSpec.snd @@ -37,14 +37,14 @@ instance : ToString Import := ⟨fun imp => toString imp.module ++ if imp.runtim def CompactedRegion := USize @[extern "lean_compacted_region_is_memory_mapped"] -constant CompactedRegion.isMemoryMapped : CompactedRegion → Bool +opaque CompactedRegion.isMemoryMapped : CompactedRegion → Bool /-- Free a compacted region and its contents. No live references to the contents may exist at the time of invocation. -/ @[extern "lean_compacted_region_free"] -unsafe constant CompactedRegion.free : CompactedRegion → IO Unit +unsafe opaque CompactedRegion.free : CompactedRegion → IO Unit /- Opaque persistent environment extension entry. -/ -constant EnvExtensionEntrySpec : NonemptyType.{0} +opaque EnvExtensionEntrySpec : NonemptyType.{0} def EnvExtensionEntry : Type := EnvExtensionEntrySpec.type instance : Nonempty EnvExtensionEntry := EnvExtensionEntrySpec.property @@ -146,11 +146,11 @@ namespace Environment /- Type check given declaration and add it to the environment -/ @[extern "lean_add_decl"] -constant addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment +opaque addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment /- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/ @[extern "lean_compile_decl"] -constant compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment +opaque compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment def addAndCompile (env : Environment) (opt : Options) (decl : Declaration) : Except KernelException Environment := do let env ← addDecl env decl @@ -265,7 +265,7 @@ unsafe def imp : EnvExtensionInterface := { end EnvExtensionInterfaceUnsafe @[implementedBy EnvExtensionInterfaceUnsafe.imp] -constant EnvExtensionInterfaceImp : EnvExtensionInterface +opaque EnvExtensionInterfaceImp : EnvExtensionInterface def EnvExtension (σ : Type) : Type := EnvExtensionInterfaceImp.ext σ @@ -401,7 +401,7 @@ unsafe def registerPersistentEnvExtensionUnsafe {α β σ : Type} [Inhabited σ] return pExt @[implementedBy registerPersistentEnvExtensionUnsafe] -constant registerPersistentEnvExtension {α β σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α β σ) : IO (PersistentEnvExtension α β σ) +opaque registerPersistentEnvExtension {α β σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α β σ) : IO (PersistentEnvExtension α β σ) /- Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries. -/ @@ -512,9 +512,9 @@ def contains [Inhabited α] (ext : MapDeclarationExtension α) (env : Environmen end MapDeclarationExtension @[extern "lean_save_module_data"] -constant saveModuleData (fname : @& System.FilePath) (mod : @& Name) (data : @& ModuleData) : IO Unit +opaque saveModuleData (fname : @& System.FilePath) (mod : @& Name) (data : @& ModuleData) : IO Unit @[extern "lean_read_module_data"] -constant readModuleData (fname : @& System.FilePath) : IO (ModuleData × CompactedRegion) +opaque readModuleData (fname : @& System.FilePath) : IO (ModuleData × CompactedRegion) /-- Free compacted regions of imports. No live references to imported objects may exist at the time of invocation; in @@ -582,9 +582,9 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st When we a new user-defined attribute declaration is imported, `attributeMapRef` is updated. Later, we set this method with code that adds the user-defined attributes that were imported after we initialized `attributeExtension`. -/ -@[extern 2 "lean_update_env_attributes"] constant updateEnvAttributes : Environment → IO Environment +@[extern 2 "lean_update_env_attributes"] opaque updateEnvAttributes : Environment → IO Environment /-- "Forward declaration" for retrieving the number of builtin attributes. -/ -@[extern 1 "lean_get_num_attributes"] constant getNumBuiltiAttributes : IO Nat +@[extern 1 "lean_get_num_attributes"] opaque getNumBuiltiAttributes : IO Nat private partial def finalizePersistentExtensions (env : Environment) (mods : Array ModuleData) (opts : Options) : IO Environment := do loop 0 env @@ -736,7 +736,7 @@ def displayStats (env : Environment) : IO Unit := do This function is only safe to use if the type matches the declaration's type in the environment and if `enableInitializersExecution` has been used before importing any modules. -/ @[extern "lean_eval_const"] -unsafe constant evalConst (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) : Except String α +unsafe opaque evalConst (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) : Except String α private def throwUnexpectedType {α} (typeName : Name) (constName : Name) : ExceptT String Id α := throw ("unexpected type at '" ++ toString constName ++ "', `" ++ toString typeName ++ "` expected") @@ -772,14 +772,14 @@ namespace Kernel Recall that the Kernel type checker does not support metavariables. When implementing automation, consider using the `MetaM` methods. -/ @[extern "lean_kernel_is_def_eq"] -constant isDefEq (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool +opaque isDefEq (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool /-- Kernel WHNF function. We use it mainly for debugging purposes. Recall that the Kernel type checker does not support metavariables. When implementing automation, consider using the `MetaM` methods. -/ @[extern "lean_kernel_whnf"] -constant whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Expr +opaque whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Expr end Kernel diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index b24d2fdd13..1492e85cd8 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -461,18 +461,18 @@ def mkAppRev (fn : Expr) (revArgs : Array Expr) : Expr := namespace Expr -- TODO: implement it in Lean @[extern "lean_expr_dbg_to_string"] -constant dbgToString (e : @& Expr) : String +opaque dbgToString (e : @& Expr) : String @[extern "lean_expr_quick_lt"] -constant quickLt (a : @& Expr) (b : @& Expr) : Bool +opaque quickLt (a : @& Expr) (b : @& Expr) : Bool @[extern "lean_expr_lt"] -constant lt (a : @& Expr) (b : @& Expr) : Bool +opaque lt (a : @& Expr) (b : @& Expr) : Bool /-- Return true iff `a` and `b` are alpha equivalent. Binder annotations are ignored. -/ @[extern "lean_expr_eqv"] -constant eqv (a : @& Expr) (b : @& Expr) : Bool +opaque eqv (a : @& Expr) (b : @& Expr) : Bool instance : BEq Expr where beq := Expr.eqv @@ -483,7 +483,7 @@ protected unsafe def ptrEq (a b : Expr) : Bool := /- Return true iff `a` and `b` are equal. Binder names and annotations are taking into account. -/ @[extern "lean_expr_equal"] -constant equal (a : @& Expr) (b : @& Expr) : Bool +opaque equal (a : @& Expr) (b : @& Expr) : Bool def isSort : Expr → Bool | sort .. => true @@ -770,7 +770,7 @@ def isArrow (e : Expr) : Bool := | _ => false @[extern "lean_expr_has_loose_bvar"] -constant hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool +opaque hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool /-- Return true if `e` contains the loose bound variable `bvarIdx` in an explicit parameter, or in the range if `tryRange == true`. -/ def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool @@ -784,12 +784,12 @@ def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool Remark: if `s < d`, then result is `e` -/ @[extern "lean_expr_lower_loose_bvars"] -constant lowerLooseBVars (e : @& Expr) (s d : @& Nat) : Expr +opaque lowerLooseBVars (e : @& Expr) (s d : @& Nat) : Expr /-- Lift loose bound variables `>= s` in `e` by `d`. -/ @[extern "lean_expr_lift_loose_bvars"] -constant liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr +opaque liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr /-- `inferImplicit e numParams considerRange` updates the first `numParams` parameter binder annotations of the `e` forall type. @@ -810,32 +810,32 @@ def inferImplicit : Expr → Nat → Bool → Expr /-- Instantiate the loose bound variables in `e` using `subst`. That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/ @[extern "lean_expr_instantiate"] -constant instantiate (e : @& Expr) (subst : @& Array Expr) : Expr +opaque instantiate (e : @& Expr) (subst : @& Array Expr) : Expr @[extern "lean_expr_instantiate1"] -constant instantiate1 (e : @& Expr) (subst : @& Expr) : Expr +opaque instantiate1 (e : @& Expr) (subst : @& Expr) : Expr /-- Similar to instantiate, but `Expr.bvar i` is replaced with `subst[subst.size - i - 1]` -/ @[extern "lean_expr_instantiate_rev"] -constant instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr +opaque instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr /-- Similar to `instantiate`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`. Function panics if `beginIdx <= endIdx <= xs.size` does not hold. -/ @[extern "lean_expr_instantiate_range"] -constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr +opaque instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr /-- Similar to `instantiateRev`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`. Function panics if `beginIdx <= endIdx <= xs.size` does not hold. -/ @[extern "lean_expr_instantiate_rev_range"] -constant instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr +opaque instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr /-- Replace free (or meta) variables `xs` with loose bound variables. -/ @[extern "lean_expr_abstract"] -constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr +opaque abstract (e : @& Expr) (xs : @& Array Expr) : Expr /-- Similar to `abstract`, but consider only the first `min n xs.size` entries in `xs`. -/ @[extern "lean_expr_abstract_range"] -constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr +opaque abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr /-- Replace occurrences of the free variable `fvar` in `e` with `v` -/ def replaceFVar (e : Expr) (fvar : Expr) (v : Expr) : Expr := diff --git a/src/Lean/LoadDynlib.lean b/src/Lean/LoadDynlib.lean index cdcac4dcf2..f076d7c596 100644 --- a/src/Lean/LoadDynlib.lean +++ b/src/Lean/LoadDynlib.lean @@ -14,4 +14,4 @@ Equivalent to passing `--load-dynlib=lib` to `lean`. Note that Lean never unloads libraries. -/ @[extern "lean_load_dynlib"] -constant loadDynlib (path : @& System.FilePath) : IO Unit +opaque loadDynlib (path : @& System.FilePath) : IO Unit diff --git a/src/Lean/Meta/ACLt.lean b/src/Lean/Meta/ACLt.lean index e348263996..e5808ae23b 100644 --- a/src/Lean/Meta/ACLt.lean +++ b/src/Lean/Meta/ACLt.lean @@ -155,6 +155,6 @@ end end ACLt @[implementedBy ACLt.lt] -constant Expr.acLt : Expr → Expr → MetaM Bool +opaque Expr.acLt : Expr → Expr → MetaM Bool end Lean.Meta diff --git a/src/Lean/Meta/Match/MatchEqsExt.lean b/src/Lean/Meta/Match/MatchEqsExt.lean index 36b3ef6901..6484dbc3b7 100644 --- a/src/Lean/Meta/Match/MatchEqsExt.lean +++ b/src/Lean/Meta/Match/MatchEqsExt.lean @@ -31,6 +31,6 @@ def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Uni Forward definition. We want to use `getEquationsFor` in the simplifier, `getEquationsFor` depends on `mkEquationsfor` which uses the simplifier. -/ @[extern "lean_get_match_equations_for"] -constant getEquationsFor (matchDeclName : Name) : MetaM MatchEqns +opaque getEquationsFor (matchDeclName : Name) : MetaM MatchEqns end Lean.Meta.Match diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index c94a451e2f..873603dd60 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -25,7 +25,7 @@ It is possible to avoid this hack if we move `Structural.EqnInfo` and `Structura to this module. -/ @[extern "lean_get_structural_rec_arg_pos"] -constant getStructuralRecArgPos? (declName : Name) : CoreM (Option Nat) +opaque getStructuralRecArgPos? (declName : Name) : CoreM (Option Nat) def smartUnfoldingSuffix := "_sunfold" @@ -720,8 +720,8 @@ def reduceRecMatcher? (e : Expr) : MetaM (Option Expr) := do unsafe def reduceBoolNativeUnsafe (constName : Name) : MetaM Bool := evalConstCheck Bool `Bool constName unsafe def reduceNatNativeUnsafe (constName : Name) : MetaM Nat := evalConstCheck Nat `Nat constName -@[implementedBy reduceBoolNativeUnsafe] constant reduceBoolNative (constName : Name) : MetaM Bool -@[implementedBy reduceNatNativeUnsafe] constant reduceNatNative (constName : Name) : MetaM Nat +@[implementedBy reduceBoolNativeUnsafe] opaque reduceBoolNative (constName : Name) : MetaM Bool +@[implementedBy reduceNatNativeUnsafe] opaque reduceNatNative (constName : Name) : MetaM Nat def reduceNative? (e : Expr) : MetaM (Option Expr) := match e with diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index c5d0e28a6e..e58948fce9 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -250,7 +250,7 @@ unsafe def mkParserOfConstantUnsafe (constName : Name) (compileParserDescr : Par | _ => throw ↑s!"unexpected parser type at '{constName}' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected)" @[implementedBy mkParserOfConstantUnsafe] -constant mkParserOfConstantAux (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser) +opaque mkParserOfConstantAux (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser) partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) : ImportM Parser := let rec visit : ParserDescr → ImportM Parser @@ -345,7 +345,7 @@ unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s => un | .error e => return s.mkUnexpectedError e.toString @[implementedBy evalParserConstUnsafe] -constant evalParserConst (declName : Name) : ParserFn +opaque evalParserConst (declName : Name) : ParserFn register_builtin_option internal.parseQuotWithCurrentStage : Bool := { defValue := false diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 25c860b4f8..90833ecb11 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -177,11 +177,11 @@ def withMaybeTag (pos? : Option String.Pos) (x : FormatterM Unit) : Formatter := -- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere -- anyway. @[extern "lean_mk_antiquot_formatter"] -constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter +opaque mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter -- break up big mutual recursion @[extern "lean_pretty_printer_formatter_interpret_parser_descr"] -constant interpretParserDescr' : ParserDescr → CoreM Formatter +opaque interpretParserDescr' : ParserDescr → CoreM Formatter private def SourceInfo.getExprPos? : SourceInfo → Option String.Pos | SourceInfo.synthetic pos _ => pos @@ -203,7 +203,7 @@ unsafe def formatterForKindUnsafe (k : SyntaxNodeKind) : Formatter := do withMaybeTag (getExprPos? stx) f @[implementedBy formatterForKindUnsafe] -constant formatterForKind (k : SyntaxNodeKind) : Formatter +opaque formatterForKind (k : SyntaxNodeKind) : Formatter @[combinatorFormatter Lean.Parser.withAntiquot] def withAntiquot.formatter (antiP p : Formatter) : Formatter := diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 9475b47798..748617dd03 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -258,14 +258,14 @@ def visitToken : Parenthesizer := do -- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere -- anyway. @[extern 8 "lean_mk_antiquot_parenthesizer"] -constant mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer +opaque mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer @[inline] def liftCoreM {α} (x : CoreM α) : ParenthesizerM α := liftM x -- break up big mutual recursion @[extern "lean_pretty_printer_parenthesizer_interpret_parser_descr"] -constant interpretParserDescr' : ParserDescr → CoreM Parenthesizer +opaque interpretParserDescr' : ParserDescr → CoreM Parenthesizer unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do if k == `missing then @@ -275,7 +275,7 @@ unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do p @[implementedBy parenthesizerForKindUnsafe] -constant parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer +opaque parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer @[combinatorParenthesizer Lean.Parser.withAntiquot] def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer := do diff --git a/src/Lean/Runtime.lean b/src/Lean/Runtime.lean index 30a82e8598..b570f0bf52 100644 --- a/src/Lean/Runtime.lean +++ b/src/Lean/Runtime.lean @@ -7,10 +7,10 @@ Authors: Leonardo de Moura namespace Lean @[extern "lean_closure_max_args"] -constant closureMaxArgsFn : Unit → Nat +opaque closureMaxArgsFn : Unit → Nat @[extern "lean_max_small_nat"] -constant maxSmallNatFn : Unit → Nat +opaque maxSmallNatFn : Unit → Nat def closureMaxArgs : Nat := closureMaxArgsFn () diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean index 3a9d33a7d1..0b8c7740a3 100644 --- a/src/Lean/ScopedEnvExtension.lean +++ b/src/Lean/ScopedEnvExtension.lean @@ -117,7 +117,7 @@ unsafe def registerScopedEnvExtensionUnsafe (descr : Descr α β σ) : IO (Scope return ext @[implementedBy registerScopedEnvExtensionUnsafe] -constant registerScopedEnvExtension (descr : Descr α β σ) : IO (ScopedEnvExtension α β σ) +opaque registerScopedEnvExtension (descr : Descr α β σ) : IO (ScopedEnvExtension α β σ) def ScopedEnvExtension.pushScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment := let s := ext.ext.getState env diff --git a/src/Lean/Util/FindExpr.lean b/src/Lean/Util/FindExpr.lean index 5044cca631..f1595b1f13 100644 --- a/src/Lean/Util/FindExpr.lean +++ b/src/Lean/Util/FindExpr.lean @@ -114,7 +114,7 @@ end FindExtImpl Similar to `find?`, but `p` can return `FindStep.done` to interrupt the search on subterms. Remark: Differently from `find?`, we do not invoke `p` for partial applications of an application. -/ @[implementedBy FindExtImpl.findUnsafe?] -constant findExt? (p : Expr → FindStep) (e : Expr) : Option Expr +opaque findExt? (p : Expr → FindStep) (e : Expr) : Option Expr end Expr end Lean diff --git a/src/Lean/Util/FoldConsts.lean b/src/Lean/Util/FoldConsts.lean index 9111e152c2..b0feef9fd7 100644 --- a/src/Lean/Util/FoldConsts.lean +++ b/src/Lean/Util/FoldConsts.lean @@ -61,7 +61,7 @@ end FoldConstsImpl /-- Apply `f` to every constant occurring in `e` once. -/ @[implementedBy FoldConstsImpl.foldUnsafe] -constant foldConsts {α : Type} (e : Expr) (init : α) (f : Name → α → α) : α := init +opaque foldConsts {α : Type} (e : Expr) (init : α) (f : Name → α → α) : α := init def getUsedConstants (e : Expr) : Array Name := e.foldConsts #[] fun c cs => cs.push c diff --git a/src/Lean/Util/HasConstCache.lean b/src/Lean/Util/HasConstCache.lean index 0f52ecc8a8..1db7571c05 100644 --- a/src/Lean/Util/HasConstCache.lean +++ b/src/Lean/Util/HasConstCache.lean @@ -32,6 +32,6 @@ where Return true iff `e` contains the constant `declName`. Remark: the results for visited expressions are stored in the state cache. -/ @[implementedBy HasConstCache.containsUnsafe] -constant HasConstCache.contains (e : Expr) : StateM (HasConstCache declName) Bool +opaque HasConstCache.contains (e : Expr) : StateM (HasConstCache declName) Bool end Lean diff --git a/src/Std/ShareCommon.lean b/src/Std/ShareCommon.lean index 07694cf9c2..4c107bddb3 100644 --- a/src/Std/ShareCommon.lean +++ b/src/Std/ShareCommon.lean @@ -86,18 +86,18 @@ unsafe def ObjectPersistentSet.insert (s : ObjectPersistentSet) (o : Object) : O @PersistentHashSet.insert Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o /- Internally `State` is implemented as a pair `ObjectMap` and `ObjectSet` -/ -constant StatePointed : NonemptyType +opaque StatePointed : NonemptyType abbrev State : Type u := StatePointed.type @[extern "lean_sharecommon_mk_state"] -constant mkState : Unit → State := fun _ => Classical.choice StatePointed.property +opaque mkState : Unit → State := fun _ => Classical.choice StatePointed.property def State.empty : State := mkState () instance State.inhabited : Inhabited State := ⟨State.empty⟩ /- Internally `PersistentState` is implemented as a pair `ObjectPersistentMap` and `ObjectPersistentSet` -/ -constant PersistentStatePointed : NonemptyType +opaque PersistentStatePointed : NonemptyType abbrev PersistentState : Type u := PersistentStatePointed.type @[extern "lean_sharecommon_mk_pstate"] -constant mkPersistentState : Unit → PersistentState := fun _ => Classical.choice PersistentStatePointed.property +opaque mkPersistentState : Unit → PersistentState := fun _ => Classical.choice PersistentStatePointed.property def PersistentState.empty : PersistentState := mkPersistentState () instance PersistentState.inhabited : Inhabited PersistentState := ⟨PersistentState.empty⟩ abbrev PState : Type u := PersistentState diff --git a/src/lake b/src/lake index e4f0574f38..535822481d 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit e4f0574f383616e8e784fb7d0959170f97b15f76 +Subproject commit 535822481d9a289b482d7c725bf588ad55f00642