max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: replace constant with opaque

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-14 16:56:38 -07:00
parent ac33193b30
commit 02c4e548df
34 changed files with 177 additions and 177 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Control/Basic.lean
View file

@ -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

4
src/Init/Core.lean
View file

@ -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

76
src/Init/Data/Float.lean
View file

@ -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

4
src/Init/Data/String/Extra.lean
View file

@ -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]

8
src/Init/Meta.lean
View file

@ -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 :=

26
src/Init/Prelude.lean
View file

@ -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

80
src/Init/System/IO.lean
View file

@ -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

14
src/Init/System/ST.lean
View file

@ -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

2
src/Lean/Attributes.lean
View file

@ -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

2
src/Lean/Compiler/ExternAttr.lean
View file

@ -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 {

6
src/Lean/Compiler/IR/Checker.lean
View file

@ -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

2
src/Lean/Compiler/IR/CtorLayout.lean
View file

@ -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

2
src/Lean/Compiler/InitAttr.lean
View file

@ -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

4
src/Lean/Declaration.lean
View file

@ -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

2
src/Lean/Elab/BuiltinCommand.lean
View file

@ -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]

2
src/Lean/Elab/Command.lean
View file

@ -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

2
src/Lean/Elab/Term.lean
View file

@ -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

4
src/Lean/Elab/Util.lean
View file

@ -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

30
src/Lean/Environment.lean
View file

@ -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

30
src/Lean/Expr.lean
View file

@ -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 :=

2
src/Lean/LoadDynlib.lean
View file

@ -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

2
src/Lean/Meta/ACLt.lean
View file

@ -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

2
src/Lean/Meta/Match/MatchEqsExt.lean
View file

@ -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

6
src/Lean/Meta/WHNF.lean
View file

@ -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

4
src/Lean/Parser/Extension.lean
View file

@ -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

6
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -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 :=

6
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -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

4
src/Lean/Runtime.lean
View file

@ -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 ()

2
src/Lean/ScopedEnvExtension.lean
View file

@ -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

2
src/Lean/Util/FindExpr.lean
View file

@ -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

2
src/Lean/Util/FoldConsts.lean
View file

@ -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

2
src/Lean/Util/HasConstCache.lean
View file

@ -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

8
src/Std/ShareCommon.lean
View file

@ -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

2
src/lake

@ -1 +1 @@
Subproject commit e4f0574f383616e8e784fb7d0959170f97b15f76
Subproject commit 535822481d9a289b482d7c725bf588ad55f00642