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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-03 18:10:10 -08:00
parent 1684cfec83
commit 95aec2cf93
189 changed files with 7759 additions and 7523 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Data/Array/Basic.lean generated
View file

@ -540,7 +540,7 @@ def filter (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Ar
@[inline]
def filterM [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
as.foldlM (init := #[]) (start := start) (stop := stop) fun r a => do
if (← p a) then r.push a else r
if (← p a) then return r.push a else return r
@[specialize]
def filterMapM [Monad m] (f : α → m (Option β)) (as : Array α) (start := 0) (stop := as.size) : m (Array β) :=

2
stage0/src/Init/Meta.lean generated
View file

@ -779,7 +779,7 @@ instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[qu
-- in contrast to `Name.toString`, we can, and want to be, precise here
private def getEscapedNameParts? (acc : List String) : Name → OptionM (List String)
| Name.anonymous => acc
| Name.anonymous => return acc
| Name.str n s _ => do
let s ← Name.escapePart s
getEscapedNameParts? (s::acc) n

6
stage0/src/Init/Notation.lean generated
View file

@ -23,7 +23,7 @@ end Lean.Parser.Syntax
macro "max" : prec => `(1024) -- maximum precedence used in term parsers, in particular for terms in function position (`ident`, `paren`, ...)
macro "arg" : prec => `(1023) -- precedence used for application arguments (`do`, `by`, ...)
macro "lead" : prec => `(1022) -- precedence used for terms not supposed to be used as arguments (`let`, `have`, ...)
macro "(" p:prec ")" : prec => p
macro "(" p:prec ")" : prec => return p
macro "min" : prec => `(10) -- minimum precedence used in term parsers
macro "min1" : prec => `(11) -- `(min+1) we can only `min+1` after `Meta.lean`
/-
@ -35,7 +35,7 @@ macro "default" : prio => `(1000)
macro "low" : prio => `(100)
macro "mid" : prio => `(1000)
macro "high" : prio => `(10000)
macro "(" p:prio ")" : prio => p
macro "(" p:prio ")" : prio => return p
-- Basic notation for defining parsers
-- NOTE: precedence must be at least `arg` to be used in `macro` without parentheses
@ -208,7 +208,7 @@ notation:50 e:51 " matches " p:51 => ((match e with | p => true | _ => false) :
-- Declare `this` as a keyword that unhygienically binds to a scope-less `this` assumption (or other binding).
-- The keyword prevents declaring a `this` binding except through metapgrogramming, as is done by `have`/`show`.
/-- Special identifier introduced by "anonymous" `have : ...`, `suffices p ...` etc. -/
macro tk:"this" : term => Syntax.ident tk.getHeadInfo "this".toSubstring `this []
macro tk:"this" : term => return Syntax.ident tk.getHeadInfo "this".toSubstring `this []
namespace Parser.Tactic
/--

6
stage0/src/Init/Prelude.lean generated
View file

@ -1308,7 +1308,7 @@ def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
match i with
| 0 => pure bs
| Nat.succ i' => Bind.bind (f (as.get ⟨j, hlt⟩)) fun b => loop i' (hAdd j 1) (bs.push b))
(fun _ => bs)
(fun _ => pure bs)
loop as.size 0 Array.empty
/-- A Function for lifting a computation from an inner Monad to an outer Monad.
@ -2032,8 +2032,8 @@ class MonadQuotation (m : Type → Type) extends MonadRef m where
export MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)
def MonadRef.mkInfoFromRefPos [Monad m] [MonadRef m] : m SourceInfo := do
SourceInfo.fromRef (← getRef)
def MonadRef.mkInfoFromRefPos [Monad m] [MonadRef m] : m SourceInfo :=
return SourceInfo.fromRef (← getRef)
instance {m n : Type → Type} [MonadFunctor m n] [MonadLift m n] [MonadQuotation m] : MonadQuotation n where
getCurrMacroScope := liftM (m := m) getCurrMacroScope

16
stage0/src/Init/System/IO.lean generated
View file

@ -144,7 +144,7 @@ namespace EIO
/-- `EIO` specialization of `BaseIO.bindTask`. -/
@[inline] def bindTask (t : Task α) (f : α → EIO ε (Task (Except ε β))) (prio := Task.Priority.default) : BaseIO (Task (Except ε β)) :=
BaseIO.bindTask t (fun a => f a |>.catchExceptions fun e => Task.pure <| Except.error e) prio
BaseIO.bindTask t (fun a => f a |>.catchExceptions fun e => return Task.pure <| Except.error e) prio
/-- `EIO` specialization of `BaseIO.mapTasks`. -/
@[inline] def mapTasks (f : List α → EIO ε β) (tasks : List (Task α)) (prio := Task.Priority.default) : BaseIO (Task (Except ε β)) :=
@ -200,7 +200,7 @@ def sleep (ms : UInt32) : IO Unit :=
/-- Wait for the task to finish, then return its result. -/
@[extern "lean_io_wait"] constant wait (t : Task α) : BaseIO α :=
t.get
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 α
@ -395,16 +395,16 @@ constant metadata : @& FilePath → IO IO.FS.Metadata
def isDir (p : FilePath) : BaseIO Bool := do
match (← p.metadata.toBaseIO) with
| Except.ok m => m.type == IO.FS.FileType.dir
| Except.error _ => false
| Except.ok m => return m.type == IO.FS.FileType.dir
| Except.error _ => return false
def pathExists (p : FilePath) : BaseIO Bool := do
(← p.metadata.toBaseIO).toBool
def pathExists (p : FilePath) : BaseIO Bool :=
return (← p.metadata.toBaseIO).toBool
/--
Return all filesystem entries of a preorder traversal of all directories satisfying `enter`, starting at `p`.
Symbolic links are visited as well by default. -/
partial def walkDir (p : FilePath) (enter : FilePath → IO Bool := fun _ => true) : IO (Array FilePath) :=
partial def walkDir (p : FilePath) (enter : FilePath → IO Bool := fun _ => pure true) : IO (Array FilePath) :=
Prod.snd <$> StateT.run (go p) #[]
where
go p := do
@ -421,7 +421,7 @@ where
if (← enter p) then
go p'
| FS.FileType.dir => go d.path
| _ => ()
| _ => return ()
end System.FilePath

2
stage0/src/Lean/Attributes.lean generated
View file

@ -418,7 +418,7 @@ def Attribute.erase (declName : Name) (attrName : Name) : AttrM Unit := do
@[export lean_update_env_attributes]
def updateEnvAttributesImpl (env : Environment) : IO Environment := do
let map ← attributeMapRef.get
let s ← attributeExtension.getState env
let s := attributeExtension.getState env
let s := map.foldl (init := s) fun s attrName attrImpl =>
if s.map.contains attrName then
s

18
stage0/src/Lean/Data/Json/Basic.lean generated
View file

@ -183,44 +183,44 @@ def isNull : Json -> Bool
| _ => false
def getObj? : Json → Except String (RBNode String (fun _ => Json))
| obj kvs => kvs
| obj kvs => return kvs
| _ => throw "object expected"
def getArr? : Json → Except String (Array Json)
| arr a => a
| arr a => return a
| _ => throw "array expected"
def getStr? : Json → Except String String
| str s => s
| str s => return s
| _ => throw "String expected"
def getNat? : Json → Except String Nat
| (n : Nat) => n
| (n : Nat) => return n
| _ => throw "Natural number expected"
def getInt? : Json → Except String Int
| (i : Int) => i
| (i : Int) => return i
| _ => throw "Integer expected"
def getBool? : Json → Except String Bool
| (b : Bool) => b
| (b : Bool) => return b
| _ => throw "Bool expected"
def getNum? : Json → Except String JsonNumber
| num n => n
| num n => return n
| _ => throw "number expected"
def getObjVal? : Json → String → Except String Json
| obj kvs, k =>
match kvs.find compare k with
| some v => v
| some v => return v
| none => throw s!"property not found: {k}"
| _ , _ => throw "object expected"
def getArrVal? : Json → Nat → Except String Json
| arr a, i =>
match a.get? i with
| some v => v
| some v => return v
| none => throw s!"index out of bounds: {i}"
| _ , _ => throw "array expected"

8
stage0/src/Lean/Data/Json/FromToJson.lean generated
View file

@ -81,7 +81,7 @@ instance : FromJson Name where
if s == "[anonymous]" then
return Name.anonymous
else
let some n ← Syntax.decodeNameLit ("`" ++ s)
let some n := Syntax.decodeNameLit ("`" ++ s)
| throw s!"expected a `Name`, got '{j}'"
return n
@ -92,7 +92,7 @@ instance : ToJson Name where
cannot represent 64-bit numbers. -/
def bignumFromJson? (j : Json) : Except String Nat := do
let s ← j.getStr?
let some v ← Syntax.decodeNatLitVal? s -- TODO maybe this should be in Std
let some v := Syntax.decodeNatLitVal? s -- TODO maybe this should be in Std
| throw s!"expected a string-encoded number, got '{j}'"
return v
@ -122,8 +122,8 @@ instance : ToJson UInt64 where
namespace Json
instance : FromJson Structured := ⟨fun
| arr a => Structured.arr a
| obj o => Structured.obj o
| arr a => return Structured.arr a
| obj o => return Structured.obj o
| j => throw s!"expected structured object, got '{j}'"⟩
instance : ToJson Structured := ⟨fun

70
stage0/src/Lean/Data/Json/Parser.lean generated
View file

@ -30,24 +30,24 @@ def hexChar : Parsec Nat := do
def escapedChar : Parsec Char := do
let c ← anyChar
match c with
| '\\' => '\\'
| '"' => '"'
| '/' => '/'
| 'b' => '\x08'
| 'f' => '\x0c'
| 'n' => '\n'
| 'r' => '\x0d'
| 't' => '\t'
| '\\' => return '\\'
| '"' => return '"'
| '/' => return '/'
| 'b' => return '\x08'
| 'f' => return '\x0c'
| 'n' => return '\n'
| 'r' => return '\x0d'
| 't' => return '\t'
| 'u' =>
let u1 ← hexChar; let u2 ← hexChar; let u3 ← hexChar; let u4 ← hexChar
Char.ofNat $ 4096*u1 + 256*u2 + 16*u3 + u4
return Char.ofNat $ 4096*u1 + 256*u2 + 16*u3 + u4
| _ => fail "illegal \\u escape"
partial def strCore (acc : String) : Parsec String := do
let c ← peek!
if c = '"' then -- "
skip
acc
return acc
else
let c ← anyChar
let ec ←
@ -57,7 +57,7 @@ partial def strCore (acc : String) : Parsec String := do
-- the JSON standard is not definite: both directly printing the character
-- and encoding it with multiple \u is allowed. we choose the former.
else if 0x0020 ≤ c.val ∧ c.val ≤ 0x10ffff then
c
pure c
else
fail "unexpected character in string"
strCore (acc.push ec)
@ -65,27 +65,27 @@ partial def strCore (acc : String) : Parsec String := do
def str : Parsec String := strCore ""
partial def natCore (acc digits : Nat) : Parsec (Nat × Nat) := do
let some c ← peek? | (acc, digits)
let some c ← peek? | return (acc, digits)
if '0' ≤ c ∧ c ≤ '9' then
skip
let acc' := 10*acc + (c.val.toNat - '0'.val.toNat)
natCore acc' (digits+1)
else
(acc, digits)
return (acc, digits)
@[inline]
def lookahead (p : Char → Prop) (desc : String) [DecidablePred p] : Parsec Unit := do
let c ← peek!
if p c then
()
return ()
else
fail $ "expected " ++ desc
fail <| "expected " ++ desc
@[inline]
def natNonZero : Parsec Nat := do
lookahead (fun c => '1' ≤ c ∧ c ≤ '9') "1-9"
let (n, _) ← natCore 0 0
n
return n
@[inline]
def natNumDigits : Parsec (Nat × Nat) := do
@ -95,7 +95,7 @@ def natNumDigits : Parsec (Nat × Nat) := do
@[inline]
def natMaybeZero : Parsec Nat := do
let (n, _) ← natNumDigits
n
return n
def num : Parsec JsonNumber := do
let c ← peek!
@ -120,9 +120,9 @@ def num : Parsec JsonNumber := do
if d > USize.size then fail "too many decimals"
let mantissa' := sign * (res * (10^d : Nat) + n)
let exponent' := d
JsonNumber.mk mantissa' exponent'
pure <| JsonNumber.mk mantissa' exponent'
else
JsonNumber.fromInt (sign * res)
pure <| JsonNumber.fromInt (sign * res)
let c? ← peek?
if c? = some 'e' ∨ c? = some 'E' then
skip
@ -130,14 +130,14 @@ def num : Parsec JsonNumber := do
if c = '-' then
skip
let n ← natMaybeZero
res.shiftr n
return res.shiftr n
else
if c = '+' then skip
let n ← natMaybeZero
if n > USize.size then fail "exp too large"
res.shiftl n
return res.shiftl n
else
res
return res
partial def arrayCore (anyCore : Unit → Parsec Json) (acc : Array Json) : Parsec (Array Json) := do
let hd ← anyCore ()
@ -145,7 +145,7 @@ partial def arrayCore (anyCore : Unit → Parsec Json) (acc : Array Json) : Pars
let c ← anyChar
if c = ']' then
ws
acc'
return acc'
else if c = ',' then
ws
arrayCore anyCore acc'
@ -160,11 +160,11 @@ partial def objectCore (anyCore : Unit → Parsec Json) : Parsec (RBNode String
let c ← anyChar
if c = '}' then
ws
RBNode.singleton k v
return RBNode.singleton k v
else if c = ',' then
ws
let kvs ← objectCore anyCore
kvs.insert compare k v
return kvs.insert compare k v
else
fail "unexpected character in object"
@ -177,37 +177,37 @@ partial def anyCore (u : Unit) : Parsec Json := do
let c ← peek!
if c = ']' then
skip; ws
Json.arr (Array.mkEmpty 0)
return Json.arr (Array.mkEmpty 0)
else
let a ← arrayCore anyCore (Array.mkEmpty 4)
Json.arr a
return Json.arr a
else if c = '{' then
skip; ws
let c ← peek!
if c = '}' then
skip; ws
Json.obj (RBNode.leaf)
return Json.obj (RBNode.leaf)
else
let kvs ← objectCore anyCore
Json.obj kvs
return Json.obj kvs
else if c = '\"' then
skip
let s ← strCore ""
ws
Json.str s
return Json.str s
else if c = 'f' then
skipString "false"; ws
Json.bool false
return Json.bool false
else if c = 't' then
skipString "true"; ws
Json.bool true
return Json.bool true
else if c = 'n' then
skipString "null"; ws
Json.null
return Json.null
else if c = '-' ∨ ('0' ≤ c ∧ c ≤ '9') then
let n ← num
ws
Json.num n
return Json.num n
else
fail "unexpected input"
@ -216,7 +216,7 @@ def any : Parsec Json := do
ws
let res ← anyCore ()
eof
res
return res
end Json.Parser

26
stage0/src/Lean/Data/JsonRpc.lean generated
View file

@ -48,16 +48,16 @@ inductive ErrorCode where
deriving Inhabited, BEq
instance : FromJson ErrorCode := ⟨fun
| num (-32700 : Int) => ErrorCode.parseError
| num (-32600 : Int) => ErrorCode.invalidRequest
| num (-32601 : Int) => ErrorCode.methodNotFound
| num (-32602 : Int) => ErrorCode.invalidParams
| num (-32603 : Int) => ErrorCode.internalError
| num (-32002 : Int) => ErrorCode.serverNotInitialized
| num (-32001 : Int) => ErrorCode.unknownErrorCode
| num (-32801 : Int) => ErrorCode.contentModified
| num (-32800 : Int) => ErrorCode.requestCancelled
| num (-32900 : Int) => ErrorCode.rpcNeedsReconnect
| num (-32700 : Int) => return ErrorCode.parseError
| num (-32600 : Int) => return ErrorCode.invalidRequest
| num (-32601 : Int) => return ErrorCode.methodNotFound
| num (-32602 : Int) => return ErrorCode.invalidParams
| num (-32603 : Int) => return ErrorCode.internalError
| num (-32002 : Int) => return ErrorCode.serverNotInitialized
| num (-32001 : Int) => return ErrorCode.unknownErrorCode
| num (-32801 : Int) => return ErrorCode.contentModified
| num (-32800 : Int) => return ErrorCode.requestCancelled
| num (-32900 : Int) => return ErrorCode.rpcNeedsReconnect
| _ => throw "expected error code"⟩
instance : ToJson ErrorCode := ⟨fun
@ -141,8 +141,8 @@ instance (a b : RequestID) : Decidable (a < b) :=
instance : FromJson RequestID := ⟨fun j =>
match j with
| str s => RequestID.str s
| num n => RequestID.num n
| str s => return RequestID.str s
| num n => return RequestID.num n
| _ => throw "a request id needs to be a number or a string"⟩
instance : ToJson RequestID := ⟨fun rid =>
@ -196,7 +196,7 @@ instance [FromJson α] : FromJson (Notification α) where
fromJson? j := do
let msg : Message ← fromJson? j
if let Message.notification method params? := msg then
let params ← params?
let params := params?
let param : α ← fromJson? (toJson params)
pure $ ⟨method, param⟩
else throw "not a notfication"

16
stage0/src/Lean/Data/Lsp/Diagnostics.lean generated
View file

@ -24,10 +24,10 @@ inductive DiagnosticSeverity where
instance : FromJson DiagnosticSeverity := ⟨fun j =>
match j.getNat? with
| Except.ok 1 => DiagnosticSeverity.error
| Except.ok 2 => DiagnosticSeverity.warning
| Except.ok 3 => DiagnosticSeverity.information
| Except.ok 4 => DiagnosticSeverity.hint
| Except.ok 1 => return DiagnosticSeverity.error
| Except.ok 2 => return DiagnosticSeverity.warning
| Except.ok 3 => return DiagnosticSeverity.information
| Except.ok 4 => return DiagnosticSeverity.hint
| _ => throw s!"unknown DiagnosticSeverity '{j}'"⟩
instance : ToJson DiagnosticSeverity := ⟨fun
@ -42,8 +42,8 @@ inductive DiagnosticCode where
deriving Inhabited, BEq
instance : FromJson DiagnosticCode := ⟨fun
| num (i : Int) => DiagnosticCode.int i
| str s => DiagnosticCode.string s
| num (i : Int) => return DiagnosticCode.int i
| str s => return DiagnosticCode.string s
| j => throw s!"expected string or integer diagnostic code, got '{j}'"⟩
instance : ToJson DiagnosticCode := ⟨fun
@ -57,8 +57,8 @@ inductive DiagnosticTag where
instance : FromJson DiagnosticTag := ⟨fun j =>
match j.getNat? with
| Except.ok 1 => DiagnosticTag.unnecessary
| Except.ok 2 => DiagnosticTag.deprecated
| Except.ok 1 => return DiagnosticTag.unnecessary
| Except.ok 2 => return DiagnosticTag.deprecated
| _ => throw "unknown DiagnosticTag"⟩
instance : ToJson DiagnosticTag := ⟨fun

6
stage0/src/Lean/Data/Lsp/Extra.lean generated
View file

@ -30,7 +30,7 @@ structure WaitForDiagnosticsParams where
structure WaitForDiagnostics
instance : FromJson WaitForDiagnostics :=
⟨fun j => WaitForDiagnostics.mk⟩
⟨fun j => pure WaitForDiagnostics.mk⟩
instance : ToJson WaitForDiagnostics :=
⟨fun o => mkObj []⟩
@ -41,8 +41,8 @@ inductive LeanFileProgressKind
instance : FromJson LeanFileProgressKind := ⟨fun j =>
match j.getNat? with
| Except.ok 1 => LeanFileProgressKind.processing
| Except.ok 2 => LeanFileProgressKind.fatalError
| Except.ok 1 => return LeanFileProgressKind.processing
| Except.ok 2 => return LeanFileProgressKind.fatalError
| _ => throw s!"unknown LeanFileProgressKind '{j}'"⟩
instance : ToJson LeanFileProgressKind := ⟨fun

8
stage0/src/Lean/Data/Lsp/InitShutdown.lean generated
View file

@ -28,9 +28,9 @@ inductive Trace where
instance : FromJson Trace := ⟨fun j =>
match j.getStr? with
| Except.ok "off" => Trace.off
| Except.ok "messages" => Trace.messages
| Except.ok "verbose" => Trace.verbose
| Except.ok "off" => return Trace.off
| Except.ok "messages" => return Trace.messages
| Except.ok "verbose" => return Trace.verbose
| _ => throw "uknown trace"⟩
instance Trace.hasToJson : ToJson Trace :=
@ -92,7 +92,7 @@ inductive InitializedParams where
| mk
instance : FromJson InitializedParams :=
⟨fun _ => InitializedParams.mk⟩
⟨fun _ => pure InitializedParams.mk⟩
instance : ToJson InitializedParams :=
⟨fun _ => Json.null⟩

12
stage0/src/Lean/Data/Lsp/Internal.lean generated
View file

@ -34,13 +34,13 @@ def fromString (s : String) : Except String RefIdent := do
let sName := s.drop 2
-- See `FromJson Name`
let name ← match sName with
| "[anonymous]" => Name.anonymous
| "[anonymous]" => pure Name.anonymous
| _ => match Syntax.decodeNameLit ("`" ++ sName) with
| some n => n
| some n => pure n
| none => throw s!"expected a Name, got {sName}"
match sPrefix with
| "c:" => RefIdent.const name
| "f:" => RefIdent.fvar <| FVarId.mk name
| "c:" => return RefIdent.const name
| "f:" => return RefIdent.fvar <| FVarId.mk name
| _ => throw "string must start with 'c:' or 'f:'"
end RefIdent
@ -80,8 +80,8 @@ instance : ToJson ModuleRefs where
instance : FromJson ModuleRefs where
fromJson? j := do
let node ← j.getObj?
node.foldM (init := HashMap.empty) fun m k v => do
m.insert (← RefIdent.fromString k) (← fromJson? v)
node.foldM (init := HashMap.empty) fun m k v =>
return m.insert (← RefIdent.fromString k) (← fromJson? v)
/-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.

8
stage0/src/Lean/Data/Lsp/Ipc.lean generated
View file

@ -28,10 +28,10 @@ abbrev IpcM := ReaderT (Process.Child ipcStdioConfig) IO
variable [ToJson α]
def stdin : IpcM FS.Stream := do
FS.Stream.ofHandle (←read).stdin
return FS.Stream.ofHandle (←read).stdin
def stdout : IpcM FS.Stream := do
FS.Stream.ofHandle (←read).stdout
return FS.Stream.ofHandle (←read).stdout
def writeRequest (r : Request α) : IpcM Unit := do
(←stdin).writeLspRequest r
@ -59,7 +59,7 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target :
let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do
match (←readMessage) with
| Message.response id _ =>
if id == waitForDiagnosticsId then []
if id == waitForDiagnosticsId then return []
else loop
| Message.responseError id code msg _ =>
if id == waitForDiagnosticsId then
@ -67,7 +67,7 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target :
else loop
| Message.notification "textDocument/publishDiagnostics" (some param) =>
match fromJson? (toJson param) with
| Except.ok diagnosticParam => ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop)
| Except.ok diagnosticParam => return ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop)
| Except.error inner => throw $ userError s!"Cannot decode publishDiagnostics parameters\n{inner}"
| _ => loop
loop

6
stage0/src/Lean/Data/Lsp/TextSync.lean generated
View file

@ -21,9 +21,9 @@ inductive TextDocumentSyncKind where
instance : FromJson TextDocumentSyncKind := ⟨fun j =>
match j.getNat? with
| Except.ok 0 => TextDocumentSyncKind.none
| Except.ok 1 => TextDocumentSyncKind.full
| Except.ok 2 => TextDocumentSyncKind.incremental
| Except.ok 0 => return TextDocumentSyncKind.none
| Except.ok 1 => return TextDocumentSyncKind.full
| Except.ok 2 => return TextDocumentSyncKind.incremental
| _ => throw "unknown TextDocumentSyncKind"⟩
instance : ToJson TextDocumentSyncKind := ⟨fun

6
stage0/src/Lean/Data/Lsp/Workspace.lean generated
View file

@ -48,9 +48,9 @@ inductive FileChangeType
instance : FromJson FileChangeType where
fromJson? j := do
match (← fromJson? j : Nat) with
| 1 => FileChangeType.Created
| 2 => FileChangeType.Changed
| 3 => FileChangeType.Deleted
| 1 => return FileChangeType.Created
| 2 => return FileChangeType.Changed
| 3 => return FileChangeType.Deleted
| _ => throw s!"expected 1, 2, or 3, got {j}"
instance : ToJson FileChangeType where

10
stage0/src/Lean/Data/Parsec.lean generated
View file

@ -112,24 +112,24 @@ def skipChar (c : Char) : Parsec Unit := pchar c *> pure ()
@[inline]
def digit : Parsec Char := attempt do
let c ← anyChar
if '0' ≤ c ∧ c ≤ '9' then c else fail s!"digit expected"
if '0' ≤ c ∧ c ≤ '9' then return c else fail s!"digit expected"
@[inline]
def hexDigit : Parsec Char := attempt do
let c ← anyChar
if ('0' ≤ c ∧ c ≤ '9')
∨ ('a' ≤ c ∧ c ≤ 'a')
∨ ('A' ≤ c ∧ c ≤ 'A') then c else fail s!"hex digit expected"
∨ ('A' ≤ c ∧ c ≤ 'A') then return c else fail s!"hex digit expected"
@[inline]
def asciiLetter : Parsec Char := attempt do
let c ← anyChar
if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then c else fail s!"ASCII letter expected"
if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then return c else fail s!"ASCII letter expected"
@[inline]
def satisfy (p : Char → Bool) : Parsec Char := attempt do
let c ← anyChar
if p c then c else fail "condition not satisfied"
if p c then return c else fail "condition not satisfied"
@[inline]
def notFollowedBy (p : Parsec α) : Parsec Unit := λ it =>
@ -157,7 +157,7 @@ def peek? : Parsec (Option Char) := fun it =>
@[inline]
def peek! : Parsec Char := do
let some c ← peek? | fail unexpectedEndOfInput
c
return c
@[inline]
def skip : Parsec Unit := fun it =>

194
stage0/src/Lean/Data/Xml/Parser.lean generated
View file

@ -23,28 +23,28 @@ abbrev LeanChar := Char
https://www.w3.org/TR/xml/#sec-line-ends -/
def endl : Parsec LeanChar := (skipString "\r\n" <|> skipChar '\r' <|> skipChar '\n') *> pure '\n'
def quote (p : Parsec α) : Parsec α :=
def quote (p : Parsec α) : Parsec α :=
skipChar '\'' *> p <* skipChar '\''
<|> skipChar '"' *> p <* skipChar '"'
/-- https://www.w3.org/TR/xml/#NT-Char -/
def Char : Parsec LeanChar :=
def Char : Parsec LeanChar :=
(attempt do
let c ← anyChar
let cNat ← c.toNat
if (0x20 ≤ cNat ∧ cNat ≤ 0xD7FF)
∨ (0xE000 ≤ cNat ∧ cNat ≤ 0xFFFD)
∨ (0x10000 ≤ cNat ∧ cNat ≤ 0x10FFFF) then c else fail "expected xml char")
let cNat := c.toNat
if (0x20 ≤ cNat ∧ cNat ≤ 0xD7FF)
∨ (0xE000 ≤ cNat ∧ cNat ≤ 0xFFFD)
∨ (0x10000 ≤ cNat ∧ cNat ≤ 0x10FFFF) then pure c else fail "expected xml char")
<|> pchar '\t' <|> endl
/-- https://www.w3.org/TR/xml/#NT-S -/
def S : Parsec String :=
def S : Parsec String :=
many1Chars (pchar ' ' <|> endl <|> pchar '\t')
/-- https://www.w3.org/TR/xml/#NT-Eq -/
def Eq : Parsec Unit :=
optional S *> skipChar '=' <* optional S
private def nameStartCharRanges : Array (Nat × Nat) :=
#[(0xC0, 0xD6),
(0xD8, 0xF6),
@ -62,32 +62,32 @@ private def nameStartCharRanges : Array (Nat × Nat) :=
/-- https://www.w3.org/TR/xml/#NT-NameStartChar -/
def NameStartChar : Parsec LeanChar := attempt do
let c ← anyChar
if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then c
else if c = ':' ∨ c = '_' then c
if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then pure c
else if c = ':' ∨ c = '_' then pure c
else
let cNum := c.toNat
if nameStartCharRanges.any (fun (lo, hi) => lo ≤ cNum ∧ cNum ≤ hi) then c
if nameStartCharRanges.any (fun (lo, hi) => lo ≤ cNum ∧ cNum ≤ hi) then pure c
else fail "expected a name character"
/-- https://www.w3.org/TR/xml/#NT-NameChar -/
def NameChar : Parsec LeanChar :=
NameStartChar <|> digit <|> pchar '-' <|> pchar '.' <|> pchar '\xB7'
NameStartChar <|> digit <|> pchar '-' <|> pchar '.' <|> pchar '\xB7'
<|> satisfy (λ c => ('\u0300' ≤ c ∧ c ≤ '\u036F') ∨ ('\u203F' ≤ c ∧ c ≤ '\u2040'))
/-- https://www.w3.org/TR/xml/#NT-Name -/
def Name : Parsec String := do
let x ← NameStartChar
manyCharsCore NameChar x.toString
/-- https://www.w3.org/TR/xml/#NT-VersionNum -/
def VersionNum : Parsec Unit :=
def VersionNum : Parsec Unit :=
skipString "1." <* (many1 digit)
/-- https://www.w3.org/TR/xml/#NT-VersionInfo -/
def VersionInfo : Parsec Unit := do
S *>
skipString "version"
Eq
S *>
skipString "version"
Eq
quote VersionNum
/-- https://www.w3.org/TR/xml/#NT-EncName -/
@ -116,56 +116,56 @@ def XMLdecl : Parsec Unit := do
skipString "?>"
/-- https://www.w3.org/TR/xml/#NT-Comment -/
def Comment : Parsec String :=
def Comment : Parsec String :=
let notDash := Char.toString <$> satisfy (λ c => c ≠ '-')
skipString "<!--" *>
Array.foldl String.append "" <$> many (notDash <|> (do
let d ← pchar '-'
Array.foldl String.append "" <$> many (notDash <|> (do
let d ← pchar '-'
let c ← notDash
pure $ d.toString ++ c))
pure $ d.toString ++ c))
<* skipString "-->"
/-- https://www.w3.org/TR/xml/#NT-PITarget -/
def PITarget : Parsec String :=
def PITarget : Parsec String :=
Name <* (skipChar 'X' <|> skipChar 'x') <* (skipChar 'M' <|> skipChar 'm') <* (skipChar 'L' <|> skipChar 'l')
/-- https://www.w3.org/TR/xml/#NT-PI -/
def PI : Parsec Unit := do
def PI : Parsec Unit := do
skipString "<?"
<* PITarget <*
optional (S *> manyChars (notFollowedBy (skipString "?>") *> Char))
skipString "?>"
/-- https://www.w3.org/TR/xml/#NT-Misc -/
def Misc : Parsec Unit :=
def Misc : Parsec Unit :=
Comment *> pure () <|> PI <|> S *> pure ()
/-- https://www.w3.org/TR/xml/#NT-SystemLiteral -/
def SystemLiteral : Parsec String :=
pchar '"' *> manyChars (satisfy λ c => c ≠ '"') <* pchar '"'
<|> pchar '\'' *> manyChars (satisfy λ c => c ≠ '\'') <* '\''
<|> pchar '\'' *> manyChars (satisfy λ c => c ≠ '\'') <* pure '\''
/-- https://www.w3.org/TR/xml/#NT-PubidChar -/
def PubidChar : Parsec LeanChar :=
asciiLetter <|> digit <|> endl <|> attempt do
let c ← anyChar
if "-'()+,./:=?;!*#@$_%".contains c then c else fail "PublidChar expected"
if "-'()+,./:=?;!*#@$_%".contains c then pure c else fail "PublidChar expected"
/-- https://www.w3.org/TR/xml/#NT-PubidLiteral -/
def PubidLiteral : Parsec String :=
pchar '"' *> manyChars PubidChar <* pchar '"'
<|> pchar '\'' *> manyChars (attempt do
<|> pchar '\'' *> manyChars (attempt do
let c ← PubidChar
if c = '\'' then fail "'\\'' not expected" else c) <* pchar '\''
if c = '\'' then fail "'\\'' not expected" else pure c) <* pchar '\''
/-- https://www.w3.org/TR/xml/#NT-ExternalID -/
def ExternalID : Parsec Unit :=
def ExternalID : Parsec Unit :=
skipString "SYSTEM" *> S *> SystemLiteral *> pure ()
<|> skipString "PUBLIC" *> S *> PubidLiteral *> S *> SystemLiteral *> pure ()
/-- https://www.w3.org/TR/xml/#NT-Mixed -/
def Mixed : Parsec Unit :=
(do
def Mixed : Parsec Unit :=
(do
skipChar '('
optional S *>
skipString "#PCDATA" *>
@ -173,17 +173,17 @@ def Mixed : Parsec Unit :=
optional S *>
skipString ")*")
<|> skipChar '(' *> (optional S) *> skipString "#PCDATA" <* (optional S) <* skipChar ')'
mutual
/-- https://www.w3.org/TR/xml/#NT-cp -/
partial def cp : Parsec Unit :=
partial def cp : Parsec Unit :=
(Name *> pure () <|> choice <|> seq) <* optional (skipChar '?' <|> skipChar '*' <|> skipChar '+')
/-- https://www.w3.org/TR/xml/#NT-choice -/
partial def choice : Parsec Unit := do
skipChar '('
optional S *>
cp
cp
many1 (optional S *> skipChar '|' *> optional S *> cp) *>
optional S *>
skipChar ')'
@ -192,7 +192,7 @@ mutual
partial def seq : Parsec Unit := do
skipChar '('
optional S *>
cp
cp
many (optional S *> skipChar ',' *> optional S *> cp) *>
optional S *>
skipChar ')'
@ -205,7 +205,7 @@ def children : Parsec Unit :=
/-- https://www.w3.org/TR/xml/#NT-contentspec -/
def contentspec : Parsec Unit := do
skipString "EMPTY" <|> skipString "ANY" <|> Mixed <|> children
/-- https://www.w3.org/TR/xml/#NT-elementdecl -/
def elementDecl : Parsec Unit := do
skipString "<!ELEMENT"
@ -216,48 +216,48 @@ def elementDecl : Parsec Unit := do
skipChar '>'
/-- https://www.w3.org/TR/xml/#NT-StringType -/
def StringType : Parsec Unit :=
def StringType : Parsec Unit :=
skipString "CDATA"
/-- https://www.w3.org/TR/xml/#NT-TokenizedType -/
def TokenizedType : Parsec Unit :=
skipString "ID"
skipString "ID"
<|> skipString "IDREF"
<|> skipString "IDREFS"
<|> skipString "ENTITY"
<|> skipString "ENTITIES"
<|> skipString "NMTOKEN"
<|> skipString "NMTOKENS"
/-- https://www.w3.org/TR/xml/#NT-NotationType -/
def NotationType : Parsec Unit := do
skipString "NOTATION"
S *>
S *>
skipChar '(' <*
optional S
Name *> many (optional S *> skipChar '|' *> optional S *> Name) *>
optional S *>
skipChar ')'
/-- https://www.w3.org/TR/xml/#NT-Nmtoken -/
def Nmtoken : Parsec String := do
many1Chars NameChar
/-- https://www.w3.org/TR/xml/#NT-Enumeration -/
def Enumeration : Parsec Unit := do
skipChar '('
skipChar '('
optional S *>
Nmtoken *> many (optional S *> skipChar '|' *> optional S *> Nmtoken) *>
optional S *>
skipChar ')'
/-- https://www.w3.org/TR/xml/#NT-EnumeratedType -/
def EnumeratedType : Parsec Unit :=
NotationType <|> Enumeration
/-- https://www.w3.org/TR/xml/#NT-AttType -/
def AttType : Parsec Unit :=
StringType <|> TokenizedType <|> EnumeratedType
StringType <|> TokenizedType <|> EnumeratedType
def predefinedEntityToChar : String → Option LeanChar
| "lt" => some '<'
@ -268,7 +268,7 @@ def predefinedEntityToChar : String → Option LeanChar
| _ => none
/-- https://www.w3.org/TR/xml/#NT-EntityRef -/
def EntityRef : Parsec $ Option LeanChar := attempt $
def EntityRef : Parsec $ Option LeanChar := attempt $
skipChar '&' *> predefinedEntityToChar <$> Name <* skipChar ';'
@[inline]
@ -276,23 +276,23 @@ def hexDigitToNat (c : LeanChar) : Nat :=
if '0' ≤ c ∧ c ≤ '9' then c.toNat - '0'.toNat
else if 'a' ≤ c ∧ c ≤ 'f' then c.toNat - 'a'.toNat + 10
else c.toNat - 'A'.toNat + 10
def digitsToNat (base : Nat) (digits : Array Nat) : Nat :=
digits.foldl (λ r d => r * base + d) 0
/-- https://www.w3.org/TR/xml/#NT-CharRef -/
def CharRef : Parsec LeanChar := do
skipString "&#"
let charCode ←
let charCode ←
digitsToNat 10 <$> many1 (hexDigitToNat <$> digit)
<|> skipChar 'x' *> digitsToNat 16 <$> many1 (hexDigitToNat <$> hexDigit)
skipChar ';'
Char.ofNat charCode
return Char.ofNat charCode
/-- https://www.w3.org/TR/xml/#NT-Reference -/
def Reference : Parsec $ Option LeanChar :=
def Reference : Parsec $ Option LeanChar :=
EntityRef <|> some <$> CharRef
/-- https://www.w3.org/TR/xml/#NT-AttValue -/
def AttValue : Parsec String := do
let chars ←
@ -300,56 +300,56 @@ def AttValue : Parsec String := do
skipChar '"'
many (some <$> satisfy (λ c => c ≠ '<' ∧ c ≠ '&' ∧ c ≠ '"') <|> Reference) <*
skipChar '"')
<|> (do
<|> (do
skipChar '\''
many (some <$> satisfy (λ c => c ≠ '<' ∧ c ≠ '&' ∧ c ≠ '\'') <|> Reference) <*
many (some <$> satisfy (λ c => c ≠ '<' ∧ c ≠ '&' ∧ c ≠ '\'') <|> Reference) <*
skipChar '\'')
return chars.foldl (λ s c => if let some c := c then s.push c else s) ""
/-- https://www.w3.org/TR/xml/#NT-DefaultDecl -/
def DefaultDecl : Parsec Unit :=
skipString "#REQUIRED"
def DefaultDecl : Parsec Unit :=
skipString "#REQUIRED"
<|> skipString "#IMPLIED"
<|> optional (skipString "#FIXED" <* S) *> AttValue *> pure ()
/-- https://www.w3.org/TR/xml/#NT-AttDef -/
def AttDef : Parsec Unit :=
S *> Name *> S *> AttType *> S *> DefaultDecl
/-- https://www.w3.org/TR/xml/#NT-AttlistDecl -/
def AttlistDecl : Parsec Unit :=
skipString "<!ATTLIST" *> S *> Name *> many AttDef *> optional S *> skipChar '>'
/-- https://www.w3.org/TR/xml/#NT-PEReference -/
def PEReference : Parsec Unit :=
def PEReference : Parsec Unit :=
skipChar '%' *> Name *> skipChar ';'
/-- https://www.w3.org/TR/xml/#NT-EntityValue -/
def EntityValue : Parsec String := do
let chars ←
(do
skipChar '"'
(do
skipChar '"'
many (some <$> satisfy (λ c => c ≠ '%' ∧ c ≠ '&' ∧ c ≠ '"') <|> PEReference *> pure none <|> Reference) <*
skipChar '"')
<|> (do
skipChar '\''
<|> (do
skipChar '\''
many (some <$> satisfy (λ c => c ≠ '%' ∧ c ≠ '&' ∧ c ≠ '\'') <|> PEReference *> pure none <|> Reference) <*
skipChar '\'')
return chars.foldl (λ s c => if let some c := c then s.push c else s) ""
/-- https://www.w3.org/TR/xml/#NT-NDataDecl -/
def NDataDecl : Parsec Unit :=
S *> skipString "NDATA" <* S <* Name
/-- https://www.w3.org/TR/xml/#NT-EntityDef -/
def EntityDef : Parsec Unit :=
def EntityDef : Parsec Unit :=
EntityValue *> pure () <|> (ExternalID <* optional NDataDecl)
/-- https://www.w3.org/TR/xml/#NT-GEDecl -/
def GEDecl : Parsec Unit :=
def GEDecl : Parsec Unit :=
skipString "<!ENTITY" *> S *> Name *> S *> EntityDef *> optional S *> skipChar '>'
/-- https://www.w3.org/TR/xml/#NT-PEDef -/
def PEDef : Parsec Unit :=
EntityValue *> pure () <|> ExternalID
@ -361,7 +361,7 @@ def PEDecl : Parsec Unit :=
/-- https://www.w3.org/TR/xml/#NT-EntityDecl -/
def EntityDecl : Parsec Unit :=
GEDecl <|> PEDecl
/-- https://www.w3.org/TR/xml/#NT-PublicID -/
def PublicID : Parsec Unit :=
skipString "PUBLIC" <* S <* PubidLiteral
@ -371,7 +371,7 @@ def NotationDecl : Parsec Unit :=
skipString "<!NOTATION" *> S *> Name *> (ExternalID <|> PublicID) *> optional S *> skipChar '>'
/-- https://www.w3.org/TR/xml/#NT-markupdecl -/
def markupDecl : Parsec Unit :=
def markupDecl : Parsec Unit :=
elementDecl <|> AttlistDecl <|> EntityDecl <|> NotationDecl <|> PI <|> (Comment *> pure ())
/-- https://www.w3.org/TR/xml/#NT-DeclSep -/
@ -393,33 +393,33 @@ def doctypedecl : Parsec Unit := do
skipChar '>'
/-- https://www.w3.org/TR/xml/#NT-prolog -/
def prolog : Parsec Unit :=
def prolog : Parsec Unit :=
optional XMLdecl *>
many Misc *>
optional (doctypedecl <* many Misc) *> pure ()
/-- https://www.w3.org/TR/xml/#NT-Attribute -/
def Attribute : Parsec (String × String) := do
let name ← Name
Eq
let value ← AttValue
(name, value)
return (name, value)
protected def elementPrefix : Parsec (Array Content → Element) := do
skipChar '<'
skipChar '<'
let name ← Name
let attributes ← many (S *> Attribute)
let attributes ← many (S *> Attribute)
optional S *> pure ()
Element.Element name (Std.RBMap.fromList attributes.toList compare)
return Element.Element name (Std.RBMap.fromList attributes.toList compare)
/-- https://www.w3.org/TR/xml/#NT-EmptyElemTag -/
def EmptyElemTag (elem : Array Content → Element) : Parsec Element := do
skipString "/>" *> pure (elem #[])
/-- https://www.w3.org/TR/xml/#NT-STag -/
def STag (elem : Array Content → Element) : Parsec (Array Content → Element) := do
skipChar '>' *> pure elem
/-- https://www.w3.org/TR/xml/#NT-ETag -/
def ETag : Parsec Unit :=
skipString "</" *> Name *> optional S *> skipChar '>'
@ -439,35 +439,35 @@ def CData : Parsec String :=
/-- https://www.w3.org/TR/xml/#NT-CDSect -/
def CDSect : Parsec String :=
CDStart *> CData <* CDEnd
/-- https://www.w3.org/TR/xml/#NT-CharData -/
def CharData : Parsec String :=
notFollowedBy (skipString "]]>") *> manyChars (satisfy λ c => c ≠ '<' ∧ c ≠ '&')
mutual
mutual
/-- https://www.w3.org/TR/xml/#NT-content -/
partial def content : Parsec (Array Content) := do
let x ← optional (Content.Character <$> CharData)
let xs ← many do
let y ←
let y ←
attempt (some <$> Content.Element <$> element)
<|> (do let c ← Reference; c.map (Content.Character ∘ Char.toString))
<|> (do let c ← Reference; pure <| c.map (Content.Character ∘ Char.toString))
<|> some <$> Content.Character <$> CDSect
<|> PI *> none
<|> PI *> pure none
<|> some <$> Content.Comment <$> Comment
let z ← optional (Content.Character <$> CharData)
#[y, z]
pure #[y, z]
let xs := #[x] ++ xs.concatMap id |>.filterMap id
let mut res := #[]
for x in xs do
if res.size > 0 then
match res.back, x with
| Content.Character x, Content.Character y => res ← res.set! (res.size - 1) (Content.Character $ x ++ y)
| _, x => res ← res.push x
else res ← res.push x
res
| Content.Character x, Content.Character y => res := res.set! (res.size - 1) (Content.Character $ x ++ y)
| _, x => res := res.push x
else res := res.push x
return res
/-- https://www.w3.org/TR/xml/#NT-element -/
partial def element : Parsec Element := do
let elem ← Parser.elementPrefix

4
stage0/src/Lean/DocString.lean generated
View file

@ -21,8 +21,8 @@ def addDocString' [Monad m] [MonadEnv m] (declName : Name) (docString? : Option
| some docString => addDocString declName docString
| none => return ()
def findDocString? (env : Environment) (declName : Name) : IO (Option String) := do
(← builtinDocStrings.get).find? declName |>.orElse fun _ => docStringExt.find? env declName
def findDocString? (env : Environment) (declName : Name) : IO (Option String) :=
return (← builtinDocStrings.get).find? declName |>.orElse fun _ => docStringExt.find? env declName
private builtin_initialize moduleDocExt : SimplePersistentEnvExtension String (Std.PersistentArray String) ← registerSimplePersistentEnvExtension {
name := `moduleDocExt

4
stage0/src/Lean/Elab/Binders.lean generated
View file

@ -212,7 +212,7 @@ def elabBinder {α} (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α
-- elaborate independently from each other
let dom ← elabType dom
let rng ← elabType rng
mkForall (← MonadQuotation.addMacroScope `a) BinderInfo.default dom rng
return mkForall (← MonadQuotation.addMacroScope `a) BinderInfo.default dom rng
| _ => throwUnsupportedSyntax
/--
@ -391,7 +391,7 @@ def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
def expandWhereDeclsOpt (whereDeclsOpt : Syntax) (body : Syntax) : MacroM Syntax :=
if whereDeclsOpt.isNone then
body
return body
else
expandWhereDecls whereDeclsOpt[0] body

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

@ -283,7 +283,7 @@ private def mkRunMetaEval (e : Expr) : MetaM Expr :=
let α ← inferType e
let u ← getDecLevel α
let instVal ← mkEvalInstCore ``Lean.MetaEval e
let e ← mkAppN (mkConst ``Lean.runMetaEval [u]) #[α, instVal, env, opts, e]
let e := mkAppN (mkConst ``Lean.runMetaEval [u]) #[α, instVal, env, opts, e]
instantiateMVars (← mkLambdaFVars #[env, opts] e)
private def mkRunEval (e : Expr) : MetaM Expr := do

2
stage0/src/Lean/Elab/BuiltinNotation.lean generated
View file

@ -264,7 +264,7 @@ where
| `(($e)) => return (← expandCDot? e).getD e
| `(($e, $es,*)) => do
let pairs ← mkPairs (#[e] ++ es)
(← expandCDot? pairs).getD pairs
return (← expandCDot? pairs).getD pairs
| stx =>
if !stx[1][0].isMissing && stx[1][1].isMissing then
-- parsed `(` and `term`, assume it's a basic parenthesis to get any elaboration output at all

4
stage0/src/Lean/Elab/BuiltinTerm.lean generated
View file

@ -215,8 +215,8 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
/--
A resolved name literal. Evaluates to the full name of the given constant if
existent in the current context, or else fails. -/
@[builtinTermElab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ => do
toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
@[builtinTermElab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ =>
return toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
@[builtinTermElab typeOf] def elabTypeOf : TermElab := fun stx _ => do
inferType (← elabTerm stx[1] none)

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

@ -298,7 +298,7 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do
-- note the order: first process current messages & info trees, then add back old messages & trees,
-- then convert new traces to messages
let mut msgs ← (← get).messages
let mut msgs := (← get).messages
-- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check in general
if !showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors && stx.hasMissing then
-- discard elaboration errors, except for a few important and unlikely misleading ones, on parse error

22
stage0/src/Lean/Elab/Declaration.lean generated
View file

@ -28,7 +28,7 @@ private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × S
let (id, optUnivDeclStx) := expandDeclIdCore declId
let scpView := extractMacroScopes id
match scpView.name with
| Name.str Name.anonymous s _ => none
| Name.str Name.anonymous s _ => return none
| Name.str pre s _ =>
ensureValidNamespace pre
let nameNew := { scpView with name := Name.mkSimple s }.review
@ -36,15 +36,15 @@ private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × S
-- name access the info tree node of the declaration name
let id := mkIdent nameNew |>.setInfo declId.getHeadInfo
if declId.isIdent then
some (pre, id)
return some (pre, id)
else
some (pre, declId.setArg 0 id)
| _ => none
return some (pre, declId.setArg 0 id)
| _ => return none
/- given declarations such as `@[...] def Foo.Bla.f ...` return `some (Foo.Bla, @[...] def f ...)` -/
private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax)) := do
if !stx.isOfKind `Lean.Parser.Command.declaration then
none
return none
else
let decl := stx[1]
let k := decl.getKind
@ -57,16 +57,16 @@ private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax
k == ``Lean.Parser.Command.classInductive ||
k == ``Lean.Parser.Command.structure then
match (← expandDeclIdNamespace? decl[1]) with
| some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 1 declId))
| none => none
| some (ns, declId) => return some (ns, stx.setArg 1 (decl.setArg 1 declId))
| none => return none
else if k == ``Lean.Parser.Command.instance then
let optDeclId := decl[3]
if optDeclId.isNone then none
if optDeclId.isNone then return none
else match (← expandDeclIdNamespace? optDeclId[0]) with
| some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 3 (optDeclId.setArg 0 declId)))
| none => none
| some (ns, declId) => return some (ns, stx.setArg 1 (decl.setArg 3 (optDeclId.setArg 0 declId)))
| none => return none
else
none
return none
def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-- leading_parser "axiom " >> declId >> declSig

6
stage0/src/Lean/Elab/Deriving/BEq.lean generated
View file

@ -69,8 +69,8 @@ where
return alts
def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
let auxFunName ← ctx.auxFunNames[i]
let indVal ← ctx.typeInfos[i]
let auxFunName := ctx.auxFunNames[i]
let indVal := ctx.typeInfos[i]
let header ← mkBEqHeader ctx indVal
let mut body ← mkMatch ctx header indVal auxFunName
if ctx.usePartial then
@ -98,7 +98,7 @@ private def mkBEqInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax
return cmds
private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do
let auxFunName ← ctx.auxFunNames[0]
let auxFunName := ctx.auxFunNames[0]
`(private def $(mkIdent auxFunName):ident (x y : $(mkIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx)
private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do

6
stage0/src/Lean/Elab/Deriving/DecEq.lean generated
View file

@ -75,12 +75,12 @@ where
else if (← compatibleCtors ctorName₁ ctorName₂) then
patterns := patterns ++ #[(← `($(mkIdent ctorName₁) ..)), (← `($(mkIdent ctorName₂) ..))]
let rhs ← `(isFalse (by intro h; injection h))
alts ← alts.push (← `(matchAltExpr| | $[$patterns:term],* => $rhs:term))
alts := alts.push (← `(matchAltExpr| | $[$patterns:term],* => $rhs:term))
return alts
def mkAuxFunction (ctx : Context) : TermElabM Syntax := do
let auxFunName ← ctx.auxFunNames[0]
let indVal ← ctx.typeInfos[0]
let auxFunName := ctx.auxFunNames[0]
let indVal :=ctx.typeInfos[0]
let header ← mkDecEqHeader ctx indVal
let mut body ← mkMatch ctx header indVal auxFunName header.argNames
let binders := header.binders

10
stage0/src/Lean/Elab/Deriving/FromToJson.lean generated
View file

@ -21,13 +21,13 @@ def mkJsonField (n : Name) : Bool × Syntax :=
def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
if declNames.size == 1 then
if (← isStructure (← getEnv) declNames[0]) then
if isStructure (← getEnv) declNames[0] then
let cmds ← liftTermElabM none <| do
let ctx ← mkContext "toJson" declNames[0]
let header ← mkHeader ctx ``ToJson 1 ctx.typeInfos[0]
let fields := getStructureFieldsFlattened (← getEnv) declNames[0] (includeSubobjectFields := false)
let fields : Array Syntax ← fields.mapM fun field => do
let (isOptField, nm) ← mkJsonField field
let (isOptField, nm) := mkJsonField field
if isOptField then `(opt $nm $(mkIdent <| header.targetNames[0] ++ field))
else `([($nm, toJson $(mkIdent <| header.targetNames[0] ++ field))])
let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:explicitBinder* :=
@ -102,7 +102,7 @@ where
def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
if declNames.size == 1 then
if (← isStructure (← getEnv) declNames[0]) then
if isStructure (← getEnv) declNames[0] then
let cmds ← liftTermElabM none <| do
let ctx ← mkContext "fromJson" declNames[0]
let header ← mkHeader ctx ``FromJson 0 ctx.typeInfos[0]
@ -178,10 +178,10 @@ where
(fun jsons => do
$[let $identNames:ident ← $fromJsons]*
return $(mkIdent ctor):ident $identNames*))
(stx, ctorInfo.numFields)
pure (stx, ctorInfo.numFields)
-- the smaller cases, especially the ones without fields are likely faster
let alts := alts.qsort (fun (_, x) (_, y) => x < y)
alts.map Prod.fst
return alts.map Prod.fst
builtin_initialize
registerBuiltinDerivingHandler ``ToJson mkToJsonInstanceHandler

6
stage0/src/Lean/Elab/Deriving/Hashable.lean generated
View file

@ -54,8 +54,8 @@ where
return alts
def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
let auxFunName ← ctx.auxFunNames[i]
let indVal ← ctx.typeInfos[i]
let auxFunName := ctx.auxFunNames[i]
let indVal := ctx.typeInfos[i]
let header ← mkHashableHeader ctx indVal
let body ← mkMatch ctx header indVal i
let binders := header.binders
@ -87,4 +87,4 @@ def mkHashableHandler (declNames : Array Name) : CommandElabM Bool := do
builtin_initialize
registerBuiltinDerivingHandler ``Hashable mkHashableHandler
registerTraceClass `Elab.Deriving.hashable
registerTraceClass `Elab.Deriving.hashable

2
stage0/src/Lean/Elab/Deriving/Inhabited.lean generated
View file

@ -92,7 +92,7 @@ where
trace[Elab.Deriving.inhabited] "checking {instType} for '{ctorName}'"
match (← trySynthInstance instType) with
| LOption.some e =>
usedInstIdxs ← collectUsedLocalsInsts usedInstIdxs localInst2Index e
usedInstIdxs := collectUsedLocalsInsts usedInstIdxs localInst2Index e
| _ =>
trace[Elab.Deriving.inhabited] "failed to generate instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
ok := false

10
stage0/src/Lean/Elab/Deriving/Ord.lean generated
View file

@ -58,15 +58,15 @@ where
let ltPatterns := indPatterns ++ #[lPat, ←`(_)]
let gtPatterns := indPatterns ++ #[←`(_), rPat]
let rhs ← rhsCont (← `(Ordering.eq))
#[←`(matchAltExpr| | $[$(patterns):term],* => $rhs:term),
←`(matchAltExpr| | $[$(ltPatterns):term],* => Ordering.lt),
←`(matchAltExpr| | $[$(gtPatterns):term],* => Ordering.gt)]
pure #[←`(matchAltExpr| | $[$(patterns):term],* => $rhs:term),
←`(matchAltExpr| | $[$(ltPatterns):term],* => Ordering.lt),
←`(matchAltExpr| | $[$(gtPatterns):term],* => Ordering.gt)]
alts := alts ++ alt
return alts.pop.pop
def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
let auxFunName ← ctx.auxFunNames[i]
let indVal ← ctx.typeInfos[i]
let auxFunName := ctx.auxFunNames[i]
let indVal := ctx.typeInfos[i]
let header ← mkOrdHeader ctx indVal
let mut body ← mkMatch ctx header indVal auxFunName
if ctx.usePartial || indVal.isRec then

10
stage0/src/Lean/Elab/Deriving/Repr.lean generated
View file

@ -22,9 +22,9 @@ def mkReprHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := d
def mkBodyForStruct (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do
let ctorVal ← getConstInfoCtor indVal.ctors.head!
let fieldNames ← getStructureFields (← getEnv) indVal.name
let numParams := indVal.numParams
let target := mkIdent header.targetNames[0]
let fieldNames := getStructureFields (← getEnv) indVal.name
let numParams := indVal.numParams
let target := mkIdent header.targetNames[0]
forallTelescopeReducing ctorVal.type fun xs _ => do
let mut fields : Syntax ← `(Format.nil)
let mut first := true
@ -84,8 +84,8 @@ def mkBody (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName
mkBodyForInduct ctx header indVal auxFunName
def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
let auxFunName ← ctx.auxFunNames[i]
let indVal ← ctx.typeInfos[i]
let auxFunName := ctx.auxFunNames[i]
let indVal := ctx.typeInfos[i]
let header ← mkReprHeader ctx indVal
let mut body ← mkBody ctx header indVal auxFunName
if ctx.usePartial then

2
stage0/src/Lean/Elab/Deriving/Util.lean generated
View file

@ -55,7 +55,7 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
let indVal ← getConstInfoInduct typeName
let mut typeInfos := #[]
for typeName in indVal.all do
typeInfos ← typeInfos.push (← getConstInfoInduct typeName)
typeInfos := typeInfos.push (← getConstInfoInduct typeName)
let mut auxFunNames := #[]
for typeName in indVal.all do
match typeName.eraseMacroScopes with

59
stage0/src/Lean/Elab/Do.lean generated
View file

@ -274,19 +274,19 @@ def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax
/- Convert `action _ e` instructions in `c` into `let y ← e; jmp _ jp (xs y)`. -/
partial def convertTerminalActionIntoJmp (code : Code) (jp : Name) (xs : Array Name) : MacroM Code :=
let rec loop : Code → MacroM Code
| Code.decl xs stx k => do Code.decl xs stx (← loop k)
| Code.reassign xs stx k => do Code.reassign xs stx (← loop k)
| Code.joinpoint n ps b k => do Code.joinpoint n ps (← loop b) (← loop k)
| Code.seq e k => do Code.seq e (← loop k)
| Code.ite ref x? h c t e => do Code.ite ref x? h c (← loop t) (← loop e)
| Code.«match» ref g ds t alts => do Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
| Code.decl xs stx k => return Code.decl xs stx (← loop k)
| Code.reassign xs stx k => return Code.reassign xs stx (← loop k)
| Code.joinpoint n ps b k => return Code.joinpoint n ps (← loop b) (← loop k)
| Code.seq e k => return Code.seq e (← loop k)
| Code.ite ref x? h c t e => return Code.ite ref x? h c (← loop t) (← loop e)
| Code.«match» ref g ds t alts => return Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
| Code.action e => mkAuxDeclFor e fun y =>
let ref := e
-- We jump to `jp` with xs **and** y
let jmpArgs := xs.map $ mkIdentFrom ref
let jmpArgs := jmpArgs.push y
pure $ Code.jmp ref jp jmpArgs
| c => pure c
return Code.jmp ref jp jmpArgs
| c => return c
loop code
structure JPDecl where
@ -358,14 +358,13 @@ def mkJmp (ref : Syntax) (rs : NameSet) (val : Syntax) (mkJPBody : Syntax → Ma
/- `pullExitPointsAux rs c` auxiliary method for `pullExitPoints`, `rs` is the set of update variable in the current path. -/
partial def pullExitPointsAux : NameSet → Code → StateRefT (Array JPDecl) TermElabM Code
| rs, Code.decl xs stx k => do Code.decl xs stx (← pullExitPointsAux (eraseVars rs xs) k)
| rs, Code.reassign xs stx k => do Code.reassign xs stx (← pullExitPointsAux (insertVars rs xs) k)
| rs, Code.joinpoint j ps b k => do Code.joinpoint j ps (← pullExitPointsAux rs b) (← pullExitPointsAux rs k)
| rs, Code.seq e k => do Code.seq e (← pullExitPointsAux rs k)
| rs, Code.ite ref x? o c t e => do Code.ite ref x? o c (← pullExitPointsAux (eraseOptVar rs x?) t) (← pullExitPointsAux (eraseOptVar rs x?) e)
| rs, Code.«match» ref g ds t alts => do
Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) })
| rs, c@(Code.jmp _ _ _) => pure c
| rs, Code.decl xs stx k => return Code.decl xs stx (← pullExitPointsAux (eraseVars rs xs) k)
| rs, Code.reassign xs stx k => return Code.reassign xs stx (← pullExitPointsAux (insertVars rs xs) k)
| rs, Code.joinpoint j ps b k => return Code.joinpoint j ps (← pullExitPointsAux rs b) (← pullExitPointsAux rs k)
| rs, Code.seq e k => return Code.seq e (← pullExitPointsAux rs k)
| rs, Code.ite ref x? o c t e => return Code.ite ref x? o c (← pullExitPointsAux (eraseOptVar rs x?) t) (← pullExitPointsAux (eraseOptVar rs x?) e)
| rs, Code.«match» ref g ds t alts => return Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) })
| rs, c@(Code.jmp _ _ _) => return c
| rs, Code.«break» ref => mkSimpleJmp ref rs (Code.«break» ref)
| rs, Code.«continue» ref => mkSimpleJmp ref rs (Code.«continue» ref)
| rs, Code.«return» ref val => mkJmp ref rs val (fun y => pure $ Code.«return» ref y)
@ -433,29 +432,29 @@ def pullExitPoints (c : Code) : TermElabM Code := do
partial def extendUpdatedVarsAux (c : Code) (ws : NameSet) : TermElabM Code :=
let rec update : Code → TermElabM Code
| Code.joinpoint j ps b k => do Code.joinpoint j ps (← update b) (← update k)
| Code.seq e k => do Code.seq e (← update k)
| Code.joinpoint j ps b k => return Code.joinpoint j ps (← update b) (← update k)
| Code.seq e k => return Code.seq e (← update k)
| c@(Code.«match» ref g ds t alts) => do
if alts.any fun alt => alt.vars.any fun x => ws.contains x then
-- If a pattern variable is shadowing a variable in ws, we `pullExitPoints`
pullExitPoints c
else
Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) })
| Code.ite ref none o c t e => do Code.ite ref none o c (← update t) (← update e)
return Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) })
| Code.ite ref none o c t e => return Code.ite ref none o c (← update t) (← update e)
| c@(Code.ite ref (some h) o cond t e) => do
if ws.contains h then
-- if the `h` at `if h:c then t else e` shadows a variable in `ws`, we `pullExitPoints`
pullExitPoints c
else
Code.ite ref (some h) o cond (← update t) (← update e)
| Code.reassign xs stx k => do Code.reassign xs stx (← update k)
return Code.ite ref (some h) o cond (← update t) (← update e)
| Code.reassign xs stx k => return Code.reassign xs stx (← update k)
| c@(Code.decl xs stx k) => do
if xs.any fun x => ws.contains x then
-- One the declared variables is shadowing a variable in `ws`
pullExitPoints c
else
Code.decl xs stx (← update k)
| c => pure c
return Code.decl xs stx (← update k)
| c => return c
update c
/-
@ -540,7 +539,7 @@ private def mkPureUnit : MacroM Syntax :=
``(pure PUnit.unit)
def mkPureUnitAction : MacroM CodeBlock := do
mkTerminalAction (← mkPureUnit)
return mkTerminalAction (← mkPureUnit)
def mkUnless (cond : Syntax) (c : CodeBlock) : MacroM CodeBlock := do
let thenBranch ← mkPureUnitAction
@ -677,7 +676,7 @@ private def expandDoIf? (stx : Syntax) : MacroM (Option Syntax) := match stx wit
let mut e := e?.getD (← `(doSeq|pure PUnit.unit))
let mut eIsSeq := true
for (i, cond, t) in Array.zip (is.reverse.push i) (Array.zip (conds.reverse.push cond) (ts.reverse.push t)) do
e ← if eIsSeq then e else `(doSeq|$e:doElem)
e ← if eIsSeq then pure e else `(doSeq|$e:doElem)
e ← withRef cond <| match cond with
| `(doIfCond|let $pat := $d) => `(doElem| match%$i $d:term with | $pat:term => $t | _ => $e)
| `(doIfCond|let $pat ← $d) => `(doElem| match%$i ← $d with | $pat:term => $t | _ => $e)
@ -1084,14 +1083,14 @@ def matchNestedTermResult (term : Syntax) (uvars : Array Name) (a r bc : Bool) :
match a, r, bc with
| true, false, false =>
if uvars.isEmpty then
toDoElems (← `(do $term:term))
return toDoElems (← `(do $term:term))
else
toDoElems (← `(do let r ← $term:term; $u:term := r.2; pure r.1))
return toDoElems (← `(do let r ← $term:term; $u:term := r.2; pure r.1))
| false, true, false =>
if uvars.isEmpty then
toDoElems (← `(do let r ← $term:term; return r))
return toDoElems (← `(do let r ← $term:term; return r))
else
toDoElems (← `(do let r ← $term:term; $u:term := r.2; return r.1))
return toDoElems (← `(do let r ← $term:term; $u:term := r.2; return r.1))
| false, false, true => toDoElems <$>
`(do let r ← $term:term;
match r with

4
stage0/src/Lean/Elab/ElabRules.lean generated
View file

@ -37,8 +37,8 @@ def elabElabRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNodeK
throwErrorAt alt "invalid elab_rules alternative, unexpected syntax node kind '{k'}'"
| _ => throwUnsupportedSyntax
let catName ← match cat?, expty? with
| some cat, _ => cat.getId
| _, some _ => `term
| some cat, _ => pure cat.getId
| _, some _ => pure `term
-- TODO: infer category from quotation kind, possibly even kind of quoted syntax?
| _, _ => throwError "invalid elab_rules command, specify category using `elab_rules : <cat> ...`"
if let some expId := expty? then

2
stage0/src/Lean/Elab/Extra.lean generated
View file

@ -156,7 +156,7 @@ where
match s with
| `(binop% $f $lhs $rhs) => processOp (lazy := false) f lhs rhs
| `(binop_lazy% $f $lhs $rhs) => processOp (lazy := true) f lhs rhs
| `(($e)) => (← go e)
| `(($e)) => go e
| _ =>
return Tree.term s (← elabTerm s none)

2
stage0/src/Lean/Elab/InfoTree.lean generated
View file

@ -327,7 +327,7 @@ def withSaveInfoContext [MonadFinally m] [MonadEnv m] [MonadOptions m] [MonadMCt
let st ← getInfoState
let trees ← st.trees.mapM fun tree => do
let tree := tree.substitute st.assignment
InfoTree.context {
pure <| InfoTree.context {
env := (← getEnv), fileMap := (← getFileMap), mctx := (← getMCtx), currNamespace := (← getCurrNamespace), openDecls := (← getOpenDecls), options := (← getOptions)
} tree
modifyInfoTrees fun _ => treesSaved ++ trees

22
stage0/src/Lean/Elab/MacroArgUtil.lean generated
View file

@ -13,25 +13,25 @@ open Lean.Parser.Command
/- Convert `macro` arg into a `syntax` command item and a pattern element -/
def expandMacroArg (stx : Syntax) : MacroM (Syntax × Syntax) := do
let (id?, id, stx) ← match (← expandMacros stx) with
| `(macroArg| $id:ident:$stx) => (some id, id, stx)
| `(macroArg| $stx:stx) => (none, (← `(x)), stx)
| `(macroArg| $id:ident:$stx) => pure (some id, id, stx)
| `(macroArg| $stx:stx) => pure (none, (← `(x)), stx)
| _ => Macro.throwUnsupported
let pat ← match stx with
| `(stx| $s:strLit) => mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
| `(stx| &$s:strLit) => mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
| `(stx| optional($stx)) => mkSplicePat `optional id "?"
| `(stx| many($stx)) => mkSplicePat `many id "*"
| `(stx| many1($stx)) => mkSplicePat `many id "*"
| `(stx| $s:strLit) => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
| `(stx| &$s:strLit) => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
| `(stx| optional($stx)) => pure <| mkSplicePat `optional id "?"
| `(stx| many($stx)) => pure <| mkSplicePat `many id "*"
| `(stx| many1($stx)) => pure <| mkSplicePat `many id "*"
| `(stx| sepBy($stx, $sep:strLit $[, $stxsep]? $[, allowTrailingSep]?)) =>
mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
| `(stx| sepBy1($stx, $sep:strLit $[, $stxsep]? $[, allowTrailingSep]?)) =>
mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
| _ => match id? with
-- if there is a binding, we assume the user knows what they are doing
| some id => mkAntiquotNode id
| some id => pure <| mkAntiquotNode id
-- otherwise `group` the syntax to enforce arity 1, e.g. for `noWs`
| none => return (← `(stx| group($stx)), mkAntiquotNode id)
(stx, pat)
pure (stx, pat)
where mkSplicePat kind id suffix :=
mkNullNode #[mkAntiquotSuffixSpliceNode kind (mkAntiquotNode id) suffix]

8
stage0/src/Lean/Elab/Match.lean generated
View file

@ -103,7 +103,7 @@ private partial def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptT
trace[Elab.match] "discr #{i} {discr} : {d}"
if b.hasLooseBVars then
isDep := true
matchType ← b.instantiate1 discr
matchType := b.instantiate1 discr
discrs := discrs.push discr
| _ =>
throwError "invalid type provided to match-expression, function type with arity #{discrStxs.size} expected"
@ -956,14 +956,14 @@ private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermEla
private def isPatternVar (stx : Syntax) : TermElabM Bool := do
match (← resolveId? stx "pattern") with
| none => isAtomicIdent stx
| none => return isAtomicIdent stx
| some f => match f with
| Expr.const fName _ _ =>
match (← getEnv).find? fName with
| some (ConstantInfo.ctorInfo _) => return false
| some _ => return !hasMatchPatternAttribute (← getEnv) fName
| _ => isAtomicIdent stx
| _ => isAtomicIdent stx
| _ => return isAtomicIdent stx
| _ => return isAtomicIdent stx
where
isAtomicIdent (stx : Syntax) : Bool :=
stx.isIdent && stx.getId.eraseMacroScopes.isAtomic

2
stage0/src/Lean/Elab/MutualDef.lean generated
View file

@ -169,7 +169,7 @@ private def expandWhereStructInst : Macro
let mut val := val
if let some ty := ty? then
val ← `(($val : $ty))
val ← if binders.size > 0 then `(fun $[$binders]* => $val:term) else val
val ← if binders.size > 0 then `(fun $[$binders]* => $val:term) else pure val
`(structInstField|$id:ident := $val)
| _ => Macro.throwUnsupported
`({ $[$structInstFields,]* })

6
stage0/src/Lean/Elab/Notation.lean generated
View file

@ -37,7 +37,7 @@ def expandNotationItemIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind
if k == `Lean.Parser.Command.identPrec then
mkAntiquotNode stx[0]
return mkAntiquotNode stx[0]
else if k == strLitKind then
strLitToPattern stx
else
@ -96,8 +96,8 @@ private def expandNotationAux (ref : Syntax)
-- Make sure the quotation pre-checker takes section variables into account for local notation.
macroDecl ← `(section set_option quotPrecheck.allowSectionVars true $macroDecl end)
match (← mkSimpleDelab attrKind vars pat qrhs |>.run) with
| some delabDecl => mkNullNode #[stxDecl, macroDecl, delabDecl]
| none => mkNullNode #[stxDecl, macroDecl]
| some delabDecl => return mkNullNode #[stxDecl, macroDecl, delabDecl]
| none => return mkNullNode #[stxDecl, macroDecl]
@[builtinMacro Lean.Parser.Command.notation] def expandNotation : Macro
| stx@`($attrKind:attrKind notation $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) => do

2
stage0/src/Lean/Elab/PreDefinition/Basic.lean generated
View file

@ -130,7 +130,7 @@ def addNonRec (preDef : PreDefinition) (applyAttrAfterCompilation := true) : Ter
Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module
to produce better error messages. -/
def eraseRecAppSyntaxExpr (e : Expr) : CoreM Expr :=
Core.transform e (post := fun e => TransformStep.done <| if (getRecAppSyntax? e).isSome then e.mdataExpr! else e)
Core.transform e (post := fun e => pure <| TransformStep.done <| if (getRecAppSyntax? e).isSome then e.mdataExpr! else e)
def eraseRecAppSyntax (preDef : PreDefinition) : CoreM PreDefinition :=
return { preDef with value := (← eraseRecAppSyntaxExpr preDef.value) }

18
stage0/src/Lean/Elab/PreDefinition/Eqns.lean generated
View file

@ -25,13 +25,13 @@ partial def expand : Expr → Expr
def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do
let target ← getMVarType' mvarId
let some (_, lhs, rhs) ← target.eq? | return none
let some (_, lhs, rhs) := target.eq? | return none
unless rhs.isLet || rhs.isMData do return none
return some (← replaceTargetDefEq mvarId (← mkEq lhs (expand rhs)))
def funext? (mvarId : MVarId) : MetaM (Option MVarId) := do
let target ← getMVarType' mvarId
let some (_, lhs, rhs) ← target.eq? | return none
let some (_, lhs, rhs) := target.eq? | return none
unless rhs.isLambda do return none
commitWhenSome? do
let [mvarId] ← apply mvarId (← mkConstWithFreshMVarLevels ``funext) | return none
@ -66,7 +66,7 @@ structure Context where
-/
private def keepGoing (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Bool := do
let target ← getMVarType' mvarId
let some (_, lhs, rhs) ← target.eq? | return false
let some (_, lhs, rhs) := target.eq? | return false
let ctx ← read
return Option.isSome <| rhs.find? fun e => ctx.declNames.any e.isAppOf && e.hasLooseBVars
@ -122,9 +122,9 @@ private def saveEqn (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := wit
let fvarState := collectFVars {} target
let fvarState ← (← getLCtx).foldrM (init := fvarState) fun decl fvarState => do
if fvarState.fvarSet.contains decl.fvarId then
collectFVars fvarState (← instantiateMVars decl.type)
return collectFVars fvarState (← instantiateMVars decl.type)
else
fvarState
return fvarState
let mut fvarIds ← sortFVarIds <| fvarState.fvarSet.toArray
-- Include propositions that are not in fvarState.fvarSet, and only contains variables in
for decl in (← getLCtx) do
@ -176,13 +176,13 @@ def tryURefl (mvarId : MVarId) : MetaM Bool :=
/-- Delta reduce the equation left-hand-side -/
def deltaLHS (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
let target ← getMVarType' mvarId
let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaLHS mvarId "equality expected"
let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaLHS mvarId "equality expected"
let some lhs ← delta? lhs | throwTacticEx `deltaLHS mvarId "failed to delta reduce lhs"
replaceTargetDefEq mvarId (← mkEq lhs rhs)
def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := withMVarContext mvarId do
let target ← getMVarType' mvarId
let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaRHS mvarId "equality expected"
let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaRHS mvarId "equality expected"
let some rhs ← delta? rhs.consumeMData (. == declName) | return none
replaceTargetDefEq mvarId (← mkEq lhs rhs)
@ -190,13 +190,13 @@ private partial def whnfAux (e : Expr) : MetaM Expr := do
let e ← whnfI e -- Must reduce instances too, otherwise it will not be able to reduce `(Nat.rec ... ... (OfNat.ofNat 0))`
let f := e.getAppFn
match f with
| Expr.proj _ _ s _ => mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
| Expr.proj _ _ s _ => return mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
| _ => return e
/-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/
def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := withMVarContext mvarId do
let target ← getMVarType' mvarId
let some (_, lhs, rhs) ← target.eq? | throwTacticEx `whnfReducibleLHS mvarId "equality expected"
let some (_, lhs, rhs) := target.eq? | throwTacticEx `whnfReducibleLHS mvarId "equality expected"
let lhs' ← whnfAux lhs
if lhs' != lhs then
return some (← replaceTargetDefEq mvarId (← mkEq lhs' rhs))

2
stage0/src/Lean/Elab/PreDefinition/Main.lean generated
View file

@ -67,7 +67,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
for preDef in preDefs do
trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef
let cliques ← partitionPreDefs preDefs
let cliques := partitionPreDefs preDefs
let mut terminationBy ← liftMacroM <| WF.expandTerminationBy hints.terminationBy? (cliques.map fun ds => ds.map (·.declName))
let mut decreasingBy ← liftMacroM <| WF.expandTerminationHint hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
for preDefs in cliques do

4
stage0/src/Lean/Elab/PreDefinition/Structural/IndPred.lean generated
View file

@ -32,7 +32,7 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
let ty ← inferType e
let main ← mkFreshExprSyntheticOpaqueMVar ty
if (← IndPredBelow.backwardsChaining main.mvarId! maxDepth) then
main
pure main
else
throwError "could not solve using backwards chaining {MessageData.ofGoal main.mvarId!}"
else
@ -49,7 +49,7 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
modify fun s => { s with addMatchers := s.addMatchers.push addMatcher }
let some newApp ← matchMatcherApp? newApp | throwError "not a matcherApp: {newApp}"
addBelow newApp
else matcherApp.toExpr
else pure matcherApp.toExpr
let newApp ← addBelow matcherApp
if newApp == matcherApp.toExpr then

2
stage0/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean generated
View file

@ -52,7 +52,7 @@ where
let containsSUnfoldMatch := Option.isSome <| altBody.find? fun e => smartUnfoldingMatch? e |>.isSome
if !containsSUnfoldMatch then
let altBody ← mkLambdaFVars xs[numParams:xs.size] altBody
let altBody ← markSmartUnfoldigMatchAlt altBody
let altBody := markSmartUnfoldigMatchAlt altBody
mkLambdaFVars xs[0:numParams] altBody
else
mkLambdaFVars xs altBody

4
stage0/src/Lean/Elab/PreDefinition/WF/Eqns.lean generated
View file

@ -18,7 +18,7 @@ structure EqnInfo extends EqnInfoCore where
private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
let target ← getMVarType' mvarId
let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected"
let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected"
if lhs.isAppOf ``WellFounded.fix then
return mvarId
else
@ -26,7 +26,7 @@ private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := withMVa
private def rwFixEq (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
let target ← getMVarType' mvarId
let some (_, lhs, rhs) ← target.eq? | unreachable!
let some (_, lhs, rhs) := target.eq? | unreachable!
let h := mkAppN (mkConst ``WellFounded.fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs
let r ← rewrite mvarId target h
replaceTargetEq mvarId r.eNew r.eqProof

8
stage0/src/Lean/Elab/PreDefinition/WF/Fix.lean generated
View file

@ -85,7 +85,7 @@ private partial def processSumCasesOn (x F val : Expr) (k : (x : Expr) → (F :
return (← mkLambdaFVars xs type, ← getLevel type)
let mkMinorNew (ctorName : Name) (minor : Expr) : TermElabM Expr :=
lambdaTelescope minor fun xs body => do
let xNew ← xs[0]
let xNew := xs[0]
let valNew ← mkLambdaFVars xs[1:] body
let FTypeNew := FDecl.type.replaceFVar x (← mkAppOptM ctorName #[α, β, xNew])
withLocalDeclD FDecl.userName FTypeNew fun FNew => do
@ -101,7 +101,7 @@ private partial def processSumCasesOn (x F val : Expr) (k : (x : Expr) → (F :
private partial def processPSigmaCasesOn (x F val : Expr) (k : (F : Expr) → (val : Expr) → TermElabM Expr) : TermElabM Expr := do
if x.isFVar && val.isAppOfArity ``PSigma.casesOn 5 && val.getArg! 3 == x && (val.getArg! 4).isLambda && (val.getArg! 4).bindingBody!.isLambda then
let args := val.getAppArgs
let [_, u, v] ← val.getAppFn.constLevels! | unreachable!
let [_, u, v] := val.getAppFn.constLevels! | unreachable!
let α := args[0]
let β := args[1]
let FDecl ← getLocalDecl F.fvarId!
@ -109,8 +109,8 @@ private partial def processPSigmaCasesOn (x F val : Expr) (k : (F : Expr) → (v
let type ← mkArrow (FDecl.type.replaceFVar x xs[0]) type
return (← mkLambdaFVars xs type, ← getLevel type)
let minor ← lambdaTelescope args[4] fun xs body => do
let a ← xs[0]
let xNew ← xs[1]
let a := xs[0]
let xNew := xs[1]
let valNew ← mkLambdaFVars xs[2:] body
let FTypeNew := FDecl.type.replaceFVar x (← mkAppOptM `PSigma.mk #[α, β, a, xNew])
withLocalDeclD FDecl.userName FTypeNew fun FNew => do

2
stage0/src/Lean/Elab/PreDefinition/WF/Main.lean generated
View file

@ -24,7 +24,7 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) : MetaM Bool := do
private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) : TermElabM Unit := do
if (← isOnlyOneUnaryDef preDefs) then
return ()
let Expr.forallE _ domain _ _ ← preDefNonRec.type | unreachable!
let Expr.forallE _ domain _ _ := preDefNonRec.type | unreachable!
let us := preDefNonRec.levelParams.map mkLevelParam
for fidx in [:preDefs.size] do
let preDef := preDefs[fidx]

30
stage0/src/Lean/Elab/Quotation.lean generated
View file

@ -26,8 +26,8 @@ private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermEl
return ← withFreshMacroScope do
let a ← `(a)
modify (fun cont stx => (`(let $a:ident := $e; $stx) : TermElabM _))
stx.setArg 2 a
Syntax.node i k (← args.mapM floatOutAntiquotTerms)
pure <| stx.setArg 2 a
return Syntax.node i k (← args.mapM floatOutAntiquotTerms)
| stx => pure stx
private def getSepFromSplice (splice : Syntax) : Syntax :=
@ -38,7 +38,7 @@ private def getSepFromSplice (splice : Syntax) : Syntax :=
partial def mkTuple : Array Syntax → TermElabM Syntax
| #[] => `(Unit.unit)
| #[e] => e
| #[e] => return e
| es => do
let stx ← mkTuple (es.eraseIdx 0)
`(Prod.mk $(es[0]) $stx)
@ -95,7 +95,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
-- if antiquotation, insert contents as-is, else recurse
| stx@(Syntax.node _ k _) => do
if isAntiquot stx && !isEscapedAntiquot stx then
getAntiquotTerm stx
return getAntiquotTerm stx
else if isTokenAntiquot stx && !isEscapedAntiquot stx then
match stx[0] with
| Syntax.atom _ val => `(Syntax.atom (Option.getD (getHeadInfo? $(getAntiquotTerm stx)) info) $(quote val))
@ -118,7 +118,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
| `optional => `(match $(getAntiquotTerm antiquot):term with
| some x => Array.empty.push x
| none => Array.empty)
| `many => getAntiquotTerm antiquot
| `many => return getAntiquotTerm antiquot
| `sepBy => `(@SepArray.elemsAndSeps $(getSepFromSplice arg) $(getAntiquotTerm antiquot))
| k => throwErrorAt arg "invalid antiquotation suffix splice kind '{k}'"
else if k == nullKind && isAntiquotSplice arg then
@ -138,7 +138,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
let arr ←
if k == `sepBy then
`(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))
else arr
else pure arr
let arr ← bindLets arr
args := args.append arr
else do
@ -253,7 +253,7 @@ private def noOpMatchAdaptPats : HeadCheck → Alt → Alt
| _, alt => alt
private def adaptRhs (fn : Syntax → TermElabM Syntax) : Alt → TermElabM Alt
| (pats, rhs) => do (pats, ← fn rhs)
| (pats, rhs) => return (pats, ← fn rhs)
private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
let pat := alt.fst.head!
@ -334,7 +334,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
let tuple ← mkTuple ids
let mut yes := yes
let resId ← match ids with
| #[id] => id
| #[id] => pure id
| _ =>
for id in ids do
yes ← `(let $id := tuples.map (fun $tuple => $id); $yes)
@ -368,7 +368,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
let argPats := quoted.getArgs.mapIdx fun i arg =>
let arg := if (i : Nat) == idx then mkNullNode #[arg] else arg
Unhygienic.run `(`($(arg)))
covered (fun (pats, rhs) => (argPats.toList ++ pats, rhs)) (exhaustive := true)
covered (fun (pats, rhs) => pure (argPats.toList ++ pats, rhs)) (exhaustive := true)
else uncovered
| _ => uncovered
doMatch := fun yes no => do
@ -405,7 +405,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
uncovered
| shape k' sz =>
if k' == kind && sz == argPats.size then
covered (fun (pats, rhs) => (argPats.toList ++ pats, rhs)) (exhaustive := true)
covered (fun (pats, rhs) => pure (argPats.toList ++ pats, rhs)) (exhaustive := true)
else
uncovered
| _ => uncovered,
@ -428,7 +428,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
| `($id:ident) => unconditionally (`(let $id := discr; $(·)))
| `($id:ident@$pat) => do
let info ← getHeadInfo (pat::alt.1.tail!, alt.2)
{ info with onMatch := fun taken => match info.onMatch taken with
return { info with onMatch := fun taken => match info.onMatch taken with
| covered f exh => covered (fun alt => f alt >>= adaptRhs (`(let $id := discr; $(·)))) exh
| r => r }
| _ => throwErrorAt pat "match (syntax) : unexpected pattern kind {pat}"
@ -445,10 +445,10 @@ private def deduplicate (floatedLetDecls : Array Syntax) : Alt → TermElabM (Ar
| #[] =>
-- no antiquotations => introduce Unit parameter to preserve evaluation order
let rhs' ← `(rhs Unit.unit)
(floatedLetDecls.push (← `(letDecl|rhs _ := $rhs)), (pats, rhs'))
pure (floatedLetDecls.push (← `(letDecl|rhs _ := $rhs)), (pats, rhs'))
| vars =>
let rhs' ← `(rhs $vars*)
(floatedLetDecls.push (← `(letDecl|rhs $vars:ident* := $rhs)), (pats, rhs'))
pure (floatedLetDecls.push (← `(letDecl|rhs $vars:ident* := $rhs)), (pats, rhs'))
private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : TermElabM Syntax := do
trace[Elab.match_syntax] "match {discrs} with {alts}"
@ -460,7 +460,7 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T
| discr::discrs, alt::alts => do
let info ← getHeadInfo alt
let pat := alt.1.head!
let alts ← (alt::alts).mapM fun alt => do ((← getHeadInfo alt).onMatch info.check, alt)
let alts ← (alt::alts).mapM fun alt => return ((← getHeadInfo alt).onMatch info.check, alt)
let mut yesAlts := #[]
let mut undecidedAlts := #[]
let mut nonExhaustiveAlts := #[]
@ -512,7 +512,7 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
throwUnsupportedSyntax
let stx ← compileStxMatch discrs.toList (patss.map (·.toList) |>.zip rhss).toList
trace[Elab.match_syntax.result] "{stx}"
stx
return stx
| _ => throwUnsupportedSyntax
/--

4
stage0/src/Lean/Elab/Quotation/Precheck.lean generated
View file

@ -52,7 +52,7 @@ Macros without registered precheck hook are unfolded, and identifier-less syntax
partial def precheck : Precheck := fun stx => do
if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then
if ← catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; true) (fun _ => false) then
if ← catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; pure true) (fun _ => pure false) then
return
if stx.isAnyAntiquot then
return
@ -131,6 +131,6 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
@[builtinTermElab precheckedQuot] def elabPrecheckedQuot : TermElab := fun stx expectedType? => do
let singleQuot := stx[1]
runPrecheck singleQuot.getQuotContent
adaptExpander (fun _ => singleQuot) stx expectedType?
adaptExpander (fun _ => pure singleQuot) stx expectedType?
end Lean.Elab.Term.Quotation

6
stage0/src/Lean/Elab/Quotation/Util.lean generated
View file

@ -27,9 +27,9 @@ partial def getPatternVars (stx : Syntax) : TermElabM (Array Syntax) :=
if stx.isQuot then
getAntiquotationIds stx
else match stx with
| `(_) => #[]
| `($id:ident) => #[id]
| `($id:ident@$e) => do (← getPatternVars e).push id
| `(_) => return #[]
| `($id:ident) => return #[id]
| `($id:ident@$e) => return (← getPatternVars e).push id
| _ => throwErrorAt stx "unsupported pattern in syntax match{indentD stx}"
partial def getPatternsVars (pats : Array Syntax) : TermElabM (Array Syntax) :=

2
stage0/src/Lean/Elab/StructInst.lean generated
View file

@ -450,7 +450,7 @@ private def getFieldIdx (structName : Name) (fieldNames : Array Name) (fieldName
| none => throwError "field '{fieldName}' is not a valid field of '{structName}'"
def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do
if (← findField? (← getEnv) structName fieldName).isNone then
if (findField? (← getEnv) structName fieldName).isNone then
return none
return some $ mkNode ``Lean.Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]

14
stage0/src/Lean/Elab/Structure.lean generated
View file

@ -291,18 +291,18 @@ private def getFieldType (infos : Array StructFieldInfo) (parentStructName : Nam
let visit (e : Expr) : MetaM TransformStep := do
if let Expr.const subProjName .. := e.getAppFn then
if let some { ctorName, numParams, .. } ← getProjectionFnInfo? subProjName then
let Name.str subStructName subFieldName .. ← subProjName
let Name.str subStructName subFieldName .. := subProjName
| throwError "invalid projection name {subProjName}"
let args := e.getAppArgs
if args.get? numParams == parent then
let some existingFieldInfo ← findFieldInfo? infos subFieldName
let some existingFieldInfo := findFieldInfo? infos subFieldName
| throwError "unexpected field access to {fieldName} in{indentExpr e}"
return TransformStep.done <| mkAppN existingFieldInfo.fvar args[numParams+1:args.size]
return TransformStep.done e
let projType ← Meta.transform projType (post := visit)
if projType.containsFVar parent.fvarId! then
throwError "unsupported dependent field in {fieldName} : {projType}"
projType
return projType
private def toVisibility (fieldInfo : StructureFieldInfo) : CoreM Visibility := do
if isProtected (← getEnv) fieldInfo.projFn then
@ -394,7 +394,7 @@ where
if h : i < fieldNames.size then
let fieldName := fieldNames.get ⟨i, h⟩
let fieldType ← getFieldType infos parentStructName parentType fieldName
match (← findFieldInfo? infos fieldName) with
match findFieldInfo? infos fieldName with
| some existingFieldInfo =>
let existingFieldType ← inferType existingFieldInfo.fvar
unless (← isDefEq fieldType existingFieldType) do
@ -402,7 +402,7 @@ where
/- Remark: if structure has a default value for this field, it will be set at the `processOveriddenDefaultValues` below. -/
copy (i+1) infos (fieldMap.insert fieldName existingFieldInfo.fvar) expandedStructNames
| none =>
let some fieldInfo ← getFieldInfo? (← getEnv) parentStructName fieldName | unreachable!
let some fieldInfo := getFieldInfo? (← getEnv) parentStructName fieldName | unreachable!
let addNewField : TermElabM α := do
let value? ← copyDefaultValue? fieldMap expandedStructNames parentStructName fieldName
withLocalDecl fieldName fieldInfo.binderInfo fieldType fun fieldFVar => do
@ -727,7 +727,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
let env ← getEnv
let structName := view.declName
let sourceFieldNames := getStructureFieldsFlattened env structName
let structType ← mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params
let structType := mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params
let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable!
let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
withLocalDecl `self binfo structType fun source => do
@ -743,7 +743,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
result := mkApp result fieldVal
else
-- fieldInfo must be a field of `parentStructName`
let some fieldInfo ← getFieldInfo? env parentStructName fieldName | unreachable!
let some fieldInfo := getFieldInfo? env parentStructName fieldName | unreachable!
if fieldInfo.subobject?.isNone then throwError "failed to build coercion to parent structure"
let resultType ← whnfD (← inferType result)
unless resultType.isForall do throwError "failed to build coercion to parent structure, unexpect type{indentExpr resultType}"

8
stage0/src/Lean/Elab/Syntax.lean generated
View file

@ -115,7 +115,7 @@ where
/- Convert `candidates` in a list of pairs `(c, isDescr)`, where `c` is the parser name,
and `isDescr` is true iff `c` has type `Lean.ParserDescr` or `Lean.TrailingParser` -/
let env ← getEnv
candidates.filterMap fun c =>
return candidates.filterMap fun c =>
match env.find? c with
| none => none
| some info =>
@ -312,7 +312,7 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
let precDefault := if isAtomLikeSyntax syntaxParser then Parser.maxPrec else Parser.leadPrec
let prec ← match prec? with
| some prec => liftMacroM <| evalPrec prec
| none => precDefault
| none => pure precDefault
let name ← match name? with
| some name => pure name.getId
| none => liftMacroM <| mkNameFromParserSyntax cat syntaxParser
@ -366,11 +366,11 @@ def expandNoKindMacroRulesAux (alts : Array Syntax) (cmdName : String) (mkCmd :
if altsNotK.isEmpty then
mkCmd k altsK
else
mkNullNode #[← mkCmd k altsK, ← mkCmd none altsNotK]
return mkNullNode #[← mkCmd k altsK, ← mkCmd none altsNotK]
def strLitToPattern (stx: Syntax) : MacroM Syntax :=
match stx.isStrLit? with
| some str => pure $ mkAtomFrom stx str
| some str => return mkAtomFrom stx str
| none => Macro.throwUnsupported
builtin_initialize

2
stage0/src/Lean/Elab/Tactic/Conv/Pattern.lean generated
View file

@ -28,7 +28,7 @@ partial def matchPattern? (pattern : AbstractMVarsResult) (e : Expr) : MetaM (Op
else if (← isDefEqGuarded pattern e) then
return some (e, #[])
else if e.isApp then
(← go? e.appFn!).map fun (f, extra) => (f, extra.push e.appArg!)
return (← go? e.appFn!).map fun (f, extra) => (f, extra.push e.appArg!)
else
return none
withReducible <| go? e

6
stage0/src/Lean/Elab/Tactic/Induction.lean generated
View file

@ -194,7 +194,7 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (optPreTac :
let hasAlts := altsSyntax.size > 0
if hasAlts then
-- default to initial state outside of alts
withInfoContext go initialInfo
withInfoContext go (pure initialInfo)
else go
where
go := do
@ -243,7 +243,7 @@ where
else
throwError "alternative '{altName}' is not needed"
let altVarNames := getAltVarNames altStx
let numFieldsToName ← if altHasExplicitModifier altStx then numFields else getNumExplicitFields altMVarId numFields
let numFieldsToName ← if altHasExplicitModifier altStx then pure numFields else getNumExplicitFields altMVarId numFields
trace[Meta.debug] "numFields: {numFields}, numFieldsToName: {numFieldsToName}, altNames: {altVarNames.size}"
if altVarNames.size > numFieldsToName then
logError m!"too many variable names provided at alternative '{altName}', #{altVarNames.size} provided, but #{numFieldsToName} expected"
@ -408,7 +408,7 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) :=
return args.map (·.expr)
else
liftMetaTacticAux fun mvarId => do
let argsToGeneralize ← args.filter fun arg => !(arg.expr.isFVar && arg.hName?.isNone)
let argsToGeneralize := args.filter fun arg => !(arg.expr.isFVar && arg.hName?.isNone)
let (fvarIdsNew, mvarId) ← generalize mvarId argsToGeneralize
let mut result := #[]
let mut j := 0

2
stage0/src/Lean/Elab/Tactic/Simp.lean generated
View file

@ -132,7 +132,7 @@ private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool)
if arg.getKind == ``Lean.Parser.Tactic.simpErase then
if eraseLocal && (← Term.isLocalIdent? arg[1]).isSome then
-- We use `eraseCore` because the simp lemma for the hypothesis was not added yet
lemmas ← lemmas.eraseCore arg[1].getId
lemmas := lemmas.eraseCore arg[1].getId
else
let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
lemmas ← lemmas.erase declName

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

@ -831,7 +831,7 @@ private def tryLiftAndCoe (errorMsgHeader? : Option String) (expectedType : Expr
let v ← getLevel β
let coeTInstType := Lean.mkForall `a BinderInfo.default α $ mkAppN (mkConst ``CoeT [u, v]) #[α, mkBVar 0, β]
let coeTInstVal ← synthesizeInst coeTInstType
let eNew ← expandCoe (← mkAppN (Lean.mkConst ``Lean.Internal.liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e])
let eNew ← expandCoe (mkAppN (Lean.mkConst ``Lean.Internal.liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e])
let eNewType ← inferType eNew
unless (← isDefEq expectedType eNewType) do throwMismatch
return eNew -- approach 3 worked

6
stage0/src/Lean/Elab/Util.lean generated
View file

@ -153,8 +153,8 @@ def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEn
-- TODO: record recursive expansions in info tree?
expandMacro? := fun stx => do
match (← expandMacroImpl? env stx) with
| some (_, Except.ok stx) => some stx
| _ => none
| some (_, Except.ok stx) => return some stx
| _ => return none
hasDecl := fun declName => return env.contains declName
getCurrNamespace := return currNamespace
resolveNamespace? := fun n => return ResolveName.resolveNamespace? env currNamespace openDecls n
@ -190,7 +190,7 @@ partial def mkUnusedBaseName (baseName : Name) : MacroM Name := do
if ← Macro.hasDecl (currNamespace ++ name) then
loop (idx+1)
else
name
return name
loop 1
else
return baseName

4
stage0/src/Lean/Environment.lean generated
View file

@ -564,7 +564,7 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
for mod in mods do
for extDescr in pExtDescrs[startingAt:] do
let entries := getEntriesFor mod extDescr.name 0
env ← extDescr.toEnvExtension.modifyState env fun s => { s with importedEntries := s.importedEntries.push entries }
env := extDescr.toEnvExtension.modifyState env fun s => { s with importedEntries := s.importedEntries.push entries }
return env
/--
@ -592,7 +592,7 @@ where
let prevSize := (← persistentEnvExtensionsRef.get).size
let prevAttrSize ← getNumBuiltiAttributes
let newState ← extDescr.addImportedFn s.importedEntries { env := env, opts := opts }
let mut env ← extDescr.toEnvExtension.setState env { s with state := newState }
let mut env := extDescr.toEnvExtension.setState env { s with state := newState }
env ← ensureExtensionsArraySize env
if (← persistentEnvExtensionsRef.get).size > prevSize || (← getNumBuiltiAttributes) > prevAttrSize then
-- This branch is executed when `pExtDescrs[i]` is the extension associated with the `init` attribute, and

4
stage0/src/Lean/Hygiene.lean generated
View file

@ -30,9 +30,9 @@ structure Unhygienic.Context where
abbrev Unhygienic := ReaderT Lean.Unhygienic.Context <| StateM MacroScope
namespace Unhygienic
instance : MonadQuotation Unhygienic where
getRef := do (← read).ref
getRef := return (← read).ref
withRef := fun ref => withReader ({ · with ref := ref })
getCurrMacroScope := do (← read).scope
getCurrMacroScope := return (← read).scope
getMainModule := pure `UnhygienicMain
withFreshMacroScope := fun x => do
let fresh ← modifyGet fun n => (n, n + 1)

2
stage0/src/Lean/KeyedDeclsAttribute.lean generated
View file

@ -135,7 +135,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe
name := df.name
descr := df.descr
erase := fun declName => do
let s ← ext.getState (← getEnv)
let s := ext.getState (← getEnv)
let s ← s.erase df.name declName
modifyEnv fun env => ext.modifyState env fun _ => s
add := fun declName stx attrKind => do

2
stage0/src/Lean/LocalContext.lean generated
View file

@ -284,7 +284,7 @@ def getAt? (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
instance : ForIn m LocalContext LocalDecl where
forIn lctx init f := lctx.decls.forIn init fun d? b => match d? with
| none => ForInStep.yield b
| none => return ForInStep.yield b
| some d => f d b
@[inline] def foldl (lctx : LocalContext) (f : β → LocalDecl → β) (init : β) (start : Nat := 0) : β :=

16
stage0/src/Lean/Meta/ACLt.lean generated
View file

@ -45,7 +45,7 @@ mutual
-/
unsafe def lt (a b : Expr) : MetaM Bool :=
if ptrAddrUnsafe a == ptrAddrUnsafe b then
false
return false
-- We ignore metadata
else if a.isMData then
lt a.mdataExpr! b
@ -95,14 +95,14 @@ where
lexSameCtor (a b : Expr) : MetaM Bool :=
match a with
-- Atomic
| Expr.bvar i .. => i < b.bvarIdx!
| Expr.fvar id .. => Name.lt id.name b.fvarId!.name
| Expr.mvar id .. => Name.lt id.name b.mvarId!.name
| Expr.sort u .. => Level.normLt u b.sortLevel!
| Expr.const n .. => Name.lt n b.constName! -- We igore the levels
| Expr.lit v .. => Literal.lt v b.litValue!
| Expr.bvar i .. => return i < b.bvarIdx!
| Expr.fvar id .. => return Name.lt id.name b.fvarId!.name
| Expr.mvar id .. => return Name.lt id.name b.mvarId!.name
| Expr.sort u .. => return Level.normLt u b.sortLevel!
| Expr.const n .. => return Name.lt n b.constName! -- We igore the levels
| Expr.lit v .. => return Literal.lt v b.litValue!
-- Composite
| Expr.proj _ i e .. => if i != b.projIdx! then i < b.projIdx! else lt e b.projExpr!
| Expr.proj _ i e .. => if i != b.projIdx! then return i < b.projIdx! else lt e b.projExpr!
| Expr.app .. => ltApp a b
| Expr.lam _ d e .. => ltPair d e b.bindingDomain! b.bindingBody!
| Expr.forallE _ d e .. => ltPair d e b.bindingDomain! b.bindingBody!

2
stage0/src/Lean/Meta/AbstractMVars.lean generated
View file

@ -84,7 +84,7 @@ partial def abstractExprMVars (e : Expr) : M Expr := do
if decl.depth != s.mctx.depth then
return e
else
let (eNew, mctxNew) ← s.mctx.instantiateMVars e
let (eNew, mctxNew) := s.mctx.instantiateMVars e
if e != eNew then
modify fun s => { s with mctx := mctxNew }
abstractExprMVars eNew

4
stage0/src/Lean/Meta/Check.lean generated
View file

@ -120,10 +120,10 @@ def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr) : MetaM MessageDat
let expectedTypeType ← inferType expectedType
let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
let (givenTypeType, expectedTypeType) ← addPPExplicitToExposeDiff givenTypeType expectedTypeType
m!"has type{indentD m!"{givenType} : {givenTypeType}"}\nbut is expected to have type{indentD m!"{expectedType} : {expectedTypeType}"}"
return m!"has type{indentD m!"{givenType} : {givenTypeType}"}\nbut is expected to have type{indentD m!"{expectedType} : {expectedTypeType}"}"
catch _ =>
let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}"
return m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}"
def throwAppTypeMismatch {α} (f a : Expr) (extraMsg : MessageData := Format.nil) : MetaM α := do
let (expectedType, binfo) ← getFunctionDomain f

6
stage0/src/Lean/Meta/DiscrTree.lean generated
View file

@ -446,11 +446,11 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
return result
let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
match findKey cs k with
| none => result
| none => return result
| some c => getMatchLoop (todo ++ args) c.2 result
let result ← visitStar result
match k with
| Key.star => result
| Key.star => return result
/-
Recall that dependent arrows are `(Key.other, #[])`, and non-dependent arrows are `(Key.arrow, #[a, b])`.
A non-dependent arrow may be an instance of a dependent arrow (stored at `DiscrTree`). Thus, we also visit the `Key.other` child.
@ -534,7 +534,7 @@ where
return result
let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
match findKey cs k with
| none => result
| none => return result
| some c => process 0 (todo ++ args) c.2 result
match k with
| Key.star => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result

6
stage0/src/Lean/Meta/ExprDefEq.lean generated
View file

@ -341,9 +341,9 @@ where
| _ => pure ()
return false
if xs.size <= 1 then
pure false
return false
else
check (← getLCtx)
return check (← getLCtx)
/- Traverse `e` and stores in the state `NameHashSet` any let-declaration with index greater than `(← read)`.
The context `Nat` is the position of `xs[0]` in the local context. -/
@ -1511,7 +1511,7 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
whenUndefDo (isDefEqDelta t s) do
if t.isConst && s.isConst then
if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
else if (← t.isApp <&&> s.isApp <&&> isDefEqApp t s) then
else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
return true
else
whenUndefDo (isDefEqStringLit t s) do

80
stage0/src/Lean/Meta/IndPredBelow.lean generated
View file

@ -55,15 +55,15 @@ def mkContext (declName : Name) : MetaM Context := do
let indVal ← getConstInfoInduct declName
let typeInfos ← indVal.all.toArray.mapM getConstInfoInduct
let motiveTypes ← typeInfos.mapM motiveType
let motives ← motiveTypes.mapIdxM fun j motive => do
(← motiveName motiveTypes j.val, motive)
let motives ← motiveTypes.mapIdxM fun j motive =>
return (← motiveName motiveTypes j.val, motive)
let headers ← typeInfos.mapM $ mkHeader motives indVal.numParams
return {
motives := motives
typeInfos := typeInfos
numParams := indVal.numParams
headers := headers
belowNames := (← indVal.all.toArray.map (· ++ `below))
belowNames := indVal.all.toArray.map (· ++ `below)
}
where
motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name :=
@ -108,14 +108,14 @@ partial def mkCtorType
where
addHeaderVars (vars : Variables) := do
let headersWithNames ← ctx.headers.mapIdxM fun idx header =>
(ctx.belowNames[idx], fun _ : Array Expr => pure header)
return (ctx.belowNames[idx], fun _ : Array Expr => pure header)
withLocalDeclsD headersWithNames fun xs =>
addMotives { vars with indVal := xs }
addMotives (vars : Variables) := do
let motiveBuilders ← ctx.motives.mapM fun (motiveName, motiveType) =>
(motiveName, BinderInfo.implicit, fun _ : Array Expr =>
return (motiveName, BinderInfo.implicit, fun _ : Array Expr =>
instantiateForall motiveType vars.params)
withLocalDecls motiveBuilders fun xs =>
modifyBinders { vars with target := vars.target ++ xs, motives := xs } 0
@ -141,7 +141,7 @@ where
let innerType := mkAppN vars.indVal[belowIdx] $
vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp]
let x ← mkForallFVars vars.target innerType
replaceTempVars vars x
return replaceTempVars vars x
replaceTempVars (vars : Variables) (ctor : Expr) :=
let levelParams :=
@ -152,11 +152,11 @@ where
checkCount (domain : Expr) : MetaM Bool := do
let run (x : StateRefT Nat MetaM Expr) : MetaM (Expr × Nat) := StateRefT'.run x 0
let (_, cnt) ← run $ transform domain fun e => do
let (_, cnt) ← run <| transform domain fun e => do
if let some name := e.constName? then
if let some idx := ctx.typeInfos.findIdx? fun indVal => indVal.name == name then
modify (. + 1)
TransformStep.visit e
return TransformStep.visit e
if cnt > 1 then
throwError "only arrows are allowed as premises. Multiple recursive occurrences detected:{indentExpr domain}"
@ -225,21 +225,21 @@ def mkInductiveType
def mkBelowDecl (ctx : Context) : MetaM Declaration := do
let lparams := ctx.typeInfos[0].levelParams
Declaration.inductDecl
return Declaration.inductDecl
lparams
(ctx.numParams + ctx.motives.size)
(←ctx.typeInfos.mapIdxM $ mkInductiveType ctx).toList
ctx.typeInfos[0].isUnsafe
partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do
if depth = 0 then false
if depth = 0 then return false
else
withMVarContext m do
let lctx ← getLCtx
let mTy ← getMVarType m
lctx.anyM fun localDecl =>
if localDecl.isAuxDecl then
false
return false
else
commitWhen do
let (mvars, _, t) ← forallMetaTelescope localDecl.type
@ -247,7 +247,7 @@ partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do
assignExprMVar m (mkAppN localDecl.toExpr mvars)
mvars.allM fun v =>
isExprMVarAssigned v.mvarId! <||> backwardsChaining v.mvarId! (depth - 1)
else false
else return false
partial def proveBrecOn (ctx : Context) (indVal : InductiveVal) (type : Expr) : MetaM Expr := do
let main ← mkFreshExprSyntheticOpaqueMVar type
@ -270,8 +270,8 @@ where
applyIH (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do
match (← vars.indHyps.findSomeM?
fun ih => do try some $ (←apply m $ mkFVar ih) catch ex => none) with
| some goals => goals
fun ih => do try pure <| some <| (←apply m $ mkFVar ih) catch ex => pure none) with
| some goals => pure goals
| none => throwError "cannot apply induction hypothesis: {MessageData.ofGoal m}"
induction (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do
@ -287,7 +287,7 @@ where
if recursorInfo.numLevelParams > levelParams.length
then levelZero::levelParams
else levelParams
let recursor ← mkAppN (mkConst recursorInfo.name $ recLevels) $ params ++ motives
let recursor := mkAppN (mkConst recursorInfo.name $ recLevels) $ params ++ motives
apply m recursor
applyCtors (ms : List MVarId) : MetaM $ List MVarId := do
@ -305,7 +305,7 @@ where
return mss.foldr List.append []
introNPRec (m : MVarId) : MetaM MVarId := do
if (← getMVarType m).isForall then introNPRec (←intro1P m).2 else m
if (← getMVarType m).isForall then introNPRec (←intro1P m).2 else return m
closeGoal (vars : BrecOnVariables) (maxDepth : Nat) (m : MVarId) : MetaM Unit := do
unless (← isExprMVarAssigned m) do
@ -318,7 +318,7 @@ def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do
let type ← mkType
let indVal := ctx.typeInfos[idx]
let name := indVal.name ++ brecOnSuffix
Declaration.thmDecl {
return Declaration.thmDecl {
name := name
levelParams := indVal.levelParams
type := type
@ -352,7 +352,7 @@ where
let conclusion :=
mkAppN motives[idx] ys
mkForallFVars ys (←mkArrow premise conclusion)
(←name, mkDomain)
return (←name, mkDomain)
/-- Given a constructor name, find the indices of the corresponding `below` version thereof. -/
partial def getBelowIndices (ctorName : Name) : MetaM $ Array Nat := do
@ -368,7 +368,7 @@ where
(rest : Expr)
(belowIndices : Array Nat)
(xIdx yIdx : Nat) : MetaM $ Array Nat := do
if xIdx ≥ xs.size then belowIndices else
if xIdx ≥ xs.size then return belowIndices else
let x := xs[xIdx]
let xTy ← inferType x
let yTy := rest.bindingDomain!
@ -385,7 +385,7 @@ private def belowType (motive : Expr) (xs : Array Expr) (idx : Nat) : MetaM $ Na
let indInfo ← getConstInfoInduct indName
let belowArgs := args[:indInfo.numParams] ++ #[motive] ++ args[indInfo.numParams:] ++ #[xs[idx]]
let belowType := mkAppN (mkConst (indName ++ `below) type.constLevels!) belowArgs
(indName, belowType)
return (indName, belowType)
/-- This function adds an additional `below` discriminant to a matcher application.
It is used for modifying the patterns, such that the structural recursion can use the new
@ -414,7 +414,7 @@ partial def mkBelowMatcher
withLocalDeclD (←mkFreshUserName `h_below) belowType fun h_below => do
mkForallFVars (xs.push h_below) t
let motive ← newMotive belowType xs
(indName, belowType.replaceFVars xs matcherApp.discrs, motive, matchType)
pure (indName, belowType.replaceFVars xs matcherApp.discrs, motive, matchType)
let lhss ← mkMatcherInput.lhss.mapM $ addBelowPattern indName
let alts ← mkMatcherInput.lhss.zip lhss |>.toArray.zip matcherApp.alts |>.mapIdxM fun idx ((oldLhs, lhs), alt) => do
@ -431,12 +431,12 @@ partial def mkBelowMatcher
trace[Meta.IndPredBelow.match] "xs = {xs}; oldFVars = {oldFVars.map (·.toExpr)}; fvars = {fvars}; new = {fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:]}"
let newAlt ← mkLambdaFVars (fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:]) t
trace[Meta.IndPredBelow.match] "alt {idx}:\n{alt} ↦ {newAlt}"
newAlt
pure newAlt
let matcherName ← mkFreshUserName mkMatcherInput.matcherName
withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
for lhs in lhss do
trace[Meta.IndPredBelow.match] "{←lhs.patterns.mapM (·.toMessageData)}"
trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
let res ← Match.mkMatcher { matcherName, matchType, numDiscrs := (mkMatcherInput.numDiscrs + 1), lhss }
res.addMatcher
-- if a wrong index is picked, the resulting matcher can be type-incorrect.
@ -446,7 +446,7 @@ partial def mkBelowMatcher
let newApp := mkApp res.matcher motive
let newApp := mkAppN newApp $ matcherApp.discrs.push below
let newApp := mkAppN newApp alts
(newApp, res.addMatcher)
return (newApp, res.addMatcher)
where
addBelowPattern (indName : Name) (lhs : AltLHS) : MetaM AltLHS := do
@ -457,7 +457,7 @@ where
withExistingLocalDecls fVars.toList do
let patterns := patterns.push belowPattern
let patterns := patterns.set! idx (←toInaccessible originalPattern)
{ lhs with patterns := patterns.toList, fvarDecls := lhs.fvarDecls ++ fVars.toList }
return { lhs with patterns := patterns.toList, fvarDecls := lhs.fvarDecls ++ fVars.toList }
/--
this function changes the type of the pattern from the original type to the `below` version thereof.
@ -500,18 +500,18 @@ where
withExistingLocalDecls additionalFVars.toList do
let ctor := Pattern.ctor belowCtor.name us belowParams.toList belowFields.toList
trace[Meta.IndPredBelow.match] "{originalPattern.toMessageData} ↦ {ctor.toMessageData}"
(additionalFVars, ctor)
return (additionalFVars, ctor)
| Pattern.as varId p hId =>
let (additionalFVars, p) ← convertToBelow indName p
(additionalFVars, Pattern.as varId p hId)
return (additionalFVars, Pattern.as varId p hId)
| Pattern.var varId =>
let var := mkFVar varId
(←inferType var).withApp fun ind args => do
let (_, tgtType) ← belowType belowMotive #[var] 0
withLocalDeclD (←mkFreshUserName `h) tgtType fun h => do
let localDecl ← getFVarLocalDecl h
(#[localDecl], Pattern.var h.fvarId!)
| p => (#[], p)
return (#[localDecl], Pattern.var h.fvarId!)
| p => return (#[], p)
transformFields belowCtor indName belowFieldOpts :=
let rec loop
@ -519,7 +519,7 @@ where
(belowFieldOpts : Array $ Option Pattern)
(belowFields : Array Pattern)
(additionalFVars : Array LocalDecl) : MetaM (Array LocalDecl × Array Pattern) := do
if belowFields.size ≥ belowFieldOpts.size then (additionalFVars, belowFields) else
if belowFields.size ≥ belowFieldOpts.size then pure (additionalFVars, belowFields) else
if let some belowField := belowFieldOpts[belowFields.size] then
let belowFieldExpr ← belowField.toExpr
let belowCtor := mkApp belowCtor belowFieldExpr
@ -545,17 +545,17 @@ where
loop belowCtor belowFieldOpts #[] #[]
toInaccessible : Pattern → MetaM Pattern
| Pattern.inaccessible p => Pattern.inaccessible p
| Pattern.var v => Pattern.var v
| p => do Pattern.inaccessible $ ←p.toExpr
| Pattern.inaccessible p => return Pattern.inaccessible p
| Pattern.var v => return Pattern.var v
| p => return Pattern.inaccessible $ ←p.toExpr
newMotive (belowType : Expr) (ys : Array Expr) : MetaM Expr :=
lambdaTelescope matcherApp.motive fun xs t => do
let numDiscrs := matcherApp.discrs.size
withLocalDeclD (←mkFreshUserName `h_below) (←belowType.replaceFVars ys xs) fun h_below => do
withLocalDeclD (←mkFreshUserName `h_below) (belowType.replaceFVars ys xs) fun h_below => do
let motive ← mkLambdaFVars (xs[:numDiscrs] ++ #[h_below] ++ xs[numDiscrs:]) t
trace[Meta.IndPredBelow.match] "motive := {motive}"
motive
return motive
def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat) := do
xs.findSomeM? fun x => do
@ -570,13 +570,13 @@ def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat
trace[Meta.IndPredBelow.match] "{←Meta.ppGoal below.mvarId!}"
if (← backwardsChaining below.mvarId! 10) then
trace[Meta.IndPredBelow.match] "Found below term in the local context: {below}"
if (← xs.anyM (isDefEq below)) then none else (below, idx.val)
if (← xs.anyM (isDefEq below)) then pure none else pure (below, idx.val)
else
trace[Meta.IndPredBelow.match] "could not find below term in the local context"
none
catch _ => none
else none
| _, _ => none
pure none
catch _ => pure none
else pure none
| _, _ => pure none
def mkBelow (declName : Name) : MetaM Unit := do
if (← isInductivePredicate declName) then

2
stage0/src/Lean/Meta/Injective.lean generated
View file

@ -46,7 +46,7 @@ private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useE
eqs := eqs.push (← mkEq arg1 arg2)
else
eqs := eqs.push (← mkHEq arg1 arg2)
if let some andEqs ← mkAnd? eqs then
if let some andEqs := mkAnd? eqs then
let result ←
if useEq then
mkEq eq andEqs

4
stage0/src/Lean/Meta/Instances.lean generated
View file

@ -41,7 +41,7 @@ def Instances.eraseCore (d : Instances) (declName : Name) : Instances :=
def Instances.erase [Monad m] [MonadError m] (d : Instances) (declName : Name) : m Instances := do
unless d.instanceNames.contains declName do
throwError "'{declName}' does not have [instance] attribute"
d.eraseCore declName
return d.eraseCore declName
builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry Instances ←
registerSimpleScopedEnvExtension {
@ -70,7 +70,7 @@ builtin_initialize
let prio ← getAttrParamOptPrio stx[1]
discard <| addInstance declName attrKind prio |>.run {} {}
erase := fun declName => do
let s ← instanceExtension.getState (← getEnv)
let s := instanceExtension.getState (← getEnv)
let s ← s.erase declName
modifyEnv fun env => instanceExtension.modifyState env fun _ => s
}

2
stage0/src/Lean/Meta/LevelDefEq.lean generated
View file

@ -66,7 +66,7 @@ mutual
return LBool.true
else
return LBool.undef
| _, Level.mvar .. => LBool.undef -- Let `solve v u` to handle this case
| _, Level.mvar .. => return LBool.undef -- Let `solve v u` to handle this case
| Level.zero _, Level.max v₁ v₂ _ =>
Bool.toLBool <$> (isLevelDefEqAux levelZero v₁ <&&> isLevelDefEqAux levelZero v₂)
| Level.zero _, Level.imax _ v₂ _ =>

9
stage0/src/Lean/Meta/Match/Match.lean generated
View file

@ -186,7 +186,7 @@ private def processAsPattern (p : Problem) : MetaM Problem :=
we the pattern `(vec.cons n h t)`. TODO: try to find a cleaner solution.
-/
let r ← mkEqRefl x
{ alt with patterns := p :: ps }.replaceFVarId fvarId x |>.replaceFVarId h r
pure <| { alt with patterns := p :: ps }.replaceFVarId fvarId x |>.replaceFVarId h r
| _ => pure alt
pure { p with alts := alts }
@ -715,7 +715,7 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
let mkMatcherConst name :=
mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
match (matcherExt.getState env).find? (result.value, compile) with
| some nameNew => (mkMatcherConst nameNew, none)
| some nameNew => pure (mkMatcherConst nameNew, none)
| none =>
let decl := Declaration.defnDecl {
name
@ -733,8 +733,7 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
setInlineAttribute name
if compile then
compileDecl decl
(mkMatcherConst name, some addMatcher)
return (mkMatcherConst name, some addMatcher)
structure MkMatcherInput where
matcherName : Name
@ -798,7 +797,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult :=
altNumParams := minors.map Prod.snd,
uElimPos? }
|> addMatcher
| none => ()
| none => pure ()
trace[Meta.Match.debug] "matcher: {matcher}"
let unusedAltIdxs := lhss.length.fold (init := []) fun i r =>

4
stage0/src/Lean/Meta/Match/MatchEqs.lean generated
View file

@ -103,7 +103,7 @@ where
let typeNew := b.instantiate1 y
if let some (_, lhs, rhs) ← matchEq? d then
if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
let some i ← ys.getIdx? lhs | unreachable!
let some i := ys.getIdx? lhs | unreachable!
let ys := ys.eraseIdx i
let mask := mask.set! i false
let args := args.map fun arg => if arg == lhs then rhs else arg
@ -445,7 +445,7 @@ private partial def mkEquationsFor (matchDeclName : Name) : MetaM MatchEqns :=
let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
let splitterType ← mkForallFVars splitterParams matchResultType
trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
let template ← mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
let template ← deltaExpand template (. == constInfo.name)
let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew altArgMasks)
let splitterName := baseName ++ `splitter

4
stage0/src/Lean/Meta/Offset.lean generated
View file

@ -99,8 +99,8 @@ private partial def isOffset : Expr → OptionT MetaM (Expr × Nat)
private def isNatZero (e : Expr) : MetaM Bool := do
match (← evalNat e) with
| some v => v == 0
| _ => false
| some v => return v == 0
| _ => return false
private def mkOffset (e : Expr) (offset : Nat) : MetaM Expr := do
if offset == 0 then

4
stage0/src/Lean/Meta/Reduce.lean generated
View file

@ -12,9 +12,9 @@ namespace Lean.Meta
partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr :=
let rec visit (e : Expr) : MonadCacheT Expr Expr MetaM Expr :=
checkCache e fun _ => Core.withIncRecDepth do
if (← (skipTypes <&&> isType e)) then
if (← (pure skipTypes <&&> isType e)) then
return e
else if (← (skipProofs <&&> isProof e)) then
else if (← (pure skipProofs <&&> isProof e)) then
return e
else
let e ← whnf e

2
stage0/src/Lean/Meta/SizeOf.lean generated
View file

@ -17,7 +17,7 @@ where
let param := params[i]
let paramType ← inferType param
let instType? ← forallTelescopeReducing paramType fun xs _ => do
let type ← mkAppN param xs
let type := mkAppN param xs
try
let sizeOf ← mkAppM `SizeOf #[type]
let instType ← mkForallFVars xs sizeOf

8
stage0/src/Lean/Meta/SynthInstance.lean generated
View file

@ -396,7 +396,7 @@ def isNewAnswer (oldAnswers : Array Answer) (answer : Answer) : Bool :=
private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
withMCtx cNode.mctx do
traceM `Meta.synthInstance.newAnswer do m!"size: {cNode.size}, {← inferType cNode.mvar}"
traceM `Meta.synthInstance.newAnswer do pure m!"size: {cNode.size}, {← inferType cNode.mvar}"
let val ← instantiateMVars cNode.mvar
trace[Meta.synthInstance.newAnswer] "val: {val}"
let result ← abstractMVars val -- assignable metavariables become parameters
@ -409,7 +409,7 @@ private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
And then, store it in the tabled entries map, and wakeup waiters. -/
def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
if cNode.size ≥ (← read).maxResultSize then
traceM `Meta.synthInstance.discarded do withMCtx cNode.mctx do m!"size: {cNode.size} ≥ {(← read).maxResultSize}, {← inferType cNode.mvar}"
traceM `Meta.synthInstance.discarded do withMCtx cNode.mctx do pure m!"size: {cNode.size} ≥ {(← read).maxResultSize}, {← inferType cNode.mvar}"
return ()
else
let answer ← mkAnswer cNode
@ -487,7 +487,7 @@ def consume (cNode : ConsumerNode) : SynthM Unit :=
match (← removeUnusedArguments? cNode.mctx mvar) with
| none => newSubgoal cNode.mctx key mvar waiter
| some (mvarType', transformer) =>
let key' ← mkTableKey cNode.mctx mvarType'
let key' := mkTableKey cNode.mctx mvarType'
match (← findEntry? key') with
| none => do
let (mctx', mvar') ← withMCtx cNode.mctx do
@ -498,7 +498,7 @@ def consume (cNode : ConsumerNode) : SynthM Unit :=
let answers' ← entry'.answers.mapM fun a => withMCtx cNode.mctx do
let trAnswr := Expr.betaRev transformer #[← instantiateMVars a.result.expr]
let trAnswrType ← inferType trAnswr
{ a with result.expr := trAnswr, resultType := trAnswrType }
pure { a with result.expr := trAnswr, resultType := trAnswrType }
modify fun s =>
{ s with
resumeStack := answers'.foldl (fun s answer => s.push (cNode, answer)) s.resumeStack,

4
stage0/src/Lean/Meta/Tactic/AuxLemma.lean generated
View file

@ -25,7 +25,7 @@ builtin_initialize auxLemmasExt : EnvExtension AuxLemmas ← registerEnvExtensio
-/
def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) : MetaM Name := do
let env ← getEnv
let s ← auxLemmasExt.getState env
let s := auxLemmasExt.getState env
let mkNewAuxLemma := do
let auxName := Name.mkNum (env.mainModule ++ `_auxLemma) s.idx
addDecl <| Declaration.thmDecl {
@ -40,4 +40,4 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) : MetaM Na
| some (name, levelParams') => if levelParams == levelParams' then return name else mkNewAuxLemma
| none => mkNewAuxLemma
end Lean.Meta
end Lean.Meta

4
stage0/src/Lean/Meta/Tactic/Delta.lean generated
View file

@ -20,8 +20,8 @@ def delta? (e : Expr) (p : Name → Bool := fun _ => true) : CoreM (Option Expr)
def deltaExpand (e : Expr) (p : Name → Bool) : CoreM Expr :=
Core.transform e fun e => do
match (← delta? e p) with
| some e' => TransformStep.visit e'
| none => TransformStep.visit e
| some e' => return TransformStep.visit e'
| none => return TransformStep.visit e
def deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM MVarId :=
withMVarContext mvarId do

6
stage0/src/Lean/Meta/Tactic/Simp/Main.lean generated
View file

@ -361,7 +361,7 @@ where
let q := e.bindingBody!
let rp ← simp p
trace[Debug.Meta.Tactic.simp] "arrow [{(← getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]"
if (← (← getConfig).contextual <&&> isProp p <&&> isProp q) then
if (← pure (← getConfig).contextual <&&> isProp p <&&> isProp q) then
trace[Debug.Meta.Tactic.simp] "ctx arrow {rp.expr} -> {q}"
withLocalDeclD e.bindingName! rp.expr fun h => do
let s ← getSimpLemmas
@ -392,7 +392,7 @@ where
return { expr := (← dsimp e) }
simpLet (e : Expr) : M Result := do
let Expr.letE n t v b _ ← e | unreachable!
let Expr.letE n t v b _ := e | unreachable!
if (← getConfig).zeta then
return { expr := b.instantiate1 v }
else
@ -598,7 +598,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
let type ← instantiateMVars localDecl.type
let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
| none => pure ctx
| some lemmaId => pure { ctx with simpLemmas := (← ctx.simpLemmas.eraseCore lemmaId) }
| some lemmaId => pure { ctx with simpLemmas := ctx.simpLemmas.eraseCore lemmaId }
match (← simpStep mvarId (mkFVar fvarId) type ctx discharge?) with
| none => return none
| some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }

4
stage0/src/Lean/Meta/Tactic/Simp/Rewrite.lean generated
View file

@ -181,11 +181,11 @@ def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndIn
x
def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
let lemmas ← (← read).simpLemmas
let lemmas := (← read).simpLemmas
return Step.visit (← rewrite e lemmas.pre lemmas.erased discharge? (tag := "pre"))
def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
let lemmas ← (← read).simpLemmas
let lemmas := (← read).simpLemmas
return Step.visit (← rewrite e lemmas.post lemmas.erased discharge? (tag := "post"))
def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step :=

2
stage0/src/Lean/Meta/Tactic/Simp/SimpAll.lean generated
View file

@ -50,7 +50,7 @@ private partial def loop : M Bool := do
let entry := (← get).entries[i]
let ctx := (← get).ctx
-- We disable the current entry to prevent it to be simplified to `True`
let simpLemmasWithoutEntry ← (← getSimpLemmas).eraseCore entry.id
let simpLemmasWithoutEntry := (← getSimpLemmas).eraseCore entry.id
let ctx := { ctx with simpLemmas := simpLemmasWithoutEntry }
match (← simpStep (← get).mvarId entry.proof entry.type ctx) with
| none => return true -- closed the goal

12
stage0/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean generated
View file

@ -92,7 +92,7 @@ partial def SimpLemmas.eraseCore (d : SimpLemmas) (declName : Name) : SimpLemmas
def SimpLemmas.erase [Monad m] [MonadError m] (d : SimpLemmas) (declName : Name) : m SimpLemmas := do
unless d.isLemma declName || d.isDeclToUnfold declName || d.toUnfoldThms.contains declName do
throwError "'{declName}' does not have [simp] attribute"
d.eraseCore declName
return d.eraseCore declName
private partial def isPerm : Expr → Expr → MetaM Bool
| Expr.app f₁ a₁ _, Expr.app f₂ a₂ _ => isPerm f₁ f₂ <&&> isPerm a₁ a₂
@ -103,8 +103,8 @@ private partial def isPerm : Expr → Expr → MetaM Bool
| Expr.lam n₁ d₁ b₁ _, Expr.lam n₂ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
| Expr.letE n₁ t₁ v₁ b₁ _, Expr.letE n₂ t₂ v₂ b₂ _ =>
isPerm t₁ t₂ <&&> isPerm v₁ v₂ <&&> withLetDecl n₁ t₁ v₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
| Expr.proj _ i₁ b₁ _, Expr.proj _ i₂ b₂ _ => i₁ == i₂ <&&> isPerm b₁ b₂
| s, t => s == t
| Expr.proj _ i₁ b₁ _, Expr.proj _ i₂ b₂ _ => pure (i₁ == i₂) <&&> isPerm b₁ b₂
| s, t => return s == t
private def checkBadRewrite (lhs rhs : Expr) : MetaM Unit := do
let lhs ← DiscrTree.whnfDT lhs (root := true)
@ -201,7 +201,7 @@ private def mkSimpLemmasFromConst (declName : Name) (post : Bool) (inv : Bool) (
r := r.push <| (← mkSimpLemmaCore (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio declName)
return r
else
#[← mkSimpLemmaCore (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio declName]
return #[← mkSimpLemmaCore (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio declName]
inductive SimpEntry where
| lemma : SimpLemma → SimpEntry
@ -244,7 +244,7 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension) : IO
throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
discard <| go.run {} {}
erase := fun declName => do
let s ← ext.getState (← getEnv)
let s := ext.getState (← getEnv)
let s ← s.erase declName
modifyEnv fun env => ext.modifyState env fun _ => s
}
@ -285,7 +285,7 @@ def SimpLemma.getValue (simpLemma : SimpLemma) : MetaM Expr := do
return simpLemma.proof.updateConst! (← info.levelParams.mapM (fun _ => mkFreshLevelMVar))
else
let us ← simpLemma.levelParams.mapM fun _ => mkFreshLevelMVar
simpLemma.proof.instantiateLevelParamsArray simpLemma.levelParams us
return simpLemma.proof.instantiateLevelParamsArray simpLemma.levelParams us
private def preprocessProof (val : Expr) (inv : Bool) : MetaM (Array Expr) := do
let type ← inferType val

12
stage0/src/Lean/Meta/WHNF.lean generated
View file

@ -508,13 +508,13 @@ where
match e with
| Expr.letE n t v b _ => withLetDecl n t (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x))
| Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← go b)
| Expr.app f a .. => mkApp (← go f) (← go a)
| Expr.proj _ _ s _ => e.updateProj! (← go s)
| Expr.app f a .. => return mkApp (← go f) (← go a)
| Expr.proj _ _ s _ => return e.updateProj! (← go s)
| Expr.mdata _ b _ =>
if let some m := smartUnfoldingMatch? e then
goMatch m
else
e.updateMData! (← go b)
return e.updateMData! (← go b)
| _ => return e
goMatch (e : Expr) : OptionT MetaM Expr := do
@ -706,9 +706,9 @@ def reduceNat? (e : Expr) : MetaM (Option Expr) :=
return false
else
match (← getConfig).transparency with
| TransparencyMode.default => true
| TransparencyMode.all => true
| _ => false
| TransparencyMode.default => return true
| TransparencyMode.all => return true
| _ => return false
@[inline] private def cached? (useCache : Bool) (e : Expr) : MetaM (Option Expr) := do
if useCache then

2
stage0/src/Lean/MonadEnv.lean generated
View file

@ -77,7 +77,7 @@ def getConstInfo [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m Co
def mkConstWithLevelParams [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m Expr := do
let info ← getConstInfo constName
mkConst constName (info.levelParams.map mkLevelParam)
return mkConst constName (info.levelParams.map mkLevelParam)
def getConstInfoInduct [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m InductiveVal := do
match (← getConstInfo constName) with

6
stage0/src/Lean/Parser/Extension.lean generated
View file

@ -313,7 +313,7 @@ private def ParserExtension.OLeanEntry.toEntry (s : State) : OLeanEntry → Impo
| category c l => return Entry.category c l
| parser catName declName prio => do
let (leading, p) ← mkParserOfConstant s.categories declName
Entry.parser catName declName leading p prio
return Entry.parser catName declName leading p prio
builtin_initialize parserExtension : ParserExtension ←
registerScopedEnvExtension {
@ -341,8 +341,8 @@ def leadingIdentBehavior (env : Environment) (catName : Name) : LeadingIdentBeha
unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s => unsafeBaseIO do
let categories := (parserExtension.getState ctx.env).categories
match (← (mkParserOfConstant categories declName { env := ctx.env, opts := ctx.options }).toBaseIO) with
| Except.ok (bool, p) => p.fn ctx s
| Except.error e => s.mkUnexpectedError e.toString
| Except.ok (bool, p) => return p.fn ctx s
| Except.error e => return s.mkUnexpectedError e.toString
@[implementedBy evalParserConstUnsafe]
constant evalParserConst (declName : Name) : ParserFn

4
stage0/src/Lean/ParserCompiler.lean generated
View file

@ -35,7 +35,7 @@ open Meta Parser in
/-- Takes an expression of type `Parser`, and determines the syntax kind of the root node it produces. -/
partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do
let reduceEval? e : MetaM (Option Name) := do
try some (← reduceEval e) catch _ => none
try pure <| some (← reduceEval e) catch _ => pure none
let e ← whnfCore e
if e matches Expr.lam .. then
lambdaLetTelescope e fun xs e => parserNodeKind? e
@ -46,7 +46,7 @@ partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do
else if e.isAppOfArity ``leadingNode 3 || e.isAppOfArity ``trailingNode 4 || e.isAppOfArity ``node 2 then
reduceEval? (e.getArg! 0)
else
none
return none
section
open Meta

27
stage0/src/Lean/PrettyPrinter/Delaborator/Basic.lean generated
View file

@ -138,10 +138,10 @@ def getExprKind : DelabM Name := do
def getOptionsAtCurrPos : DelabM Options := do
let ctx ← read
let mut opts := ctx.defaultOptions
if let some opts' ← ctx.optionsPerPos.find? (← getPos) then
if let some opts' := ctx.optionsPerPos.find? (← getPos) then
for (k, v) in opts' do
opts := opts.insert k v
opts
return opts
/-- Evaluate option accessor, using subterm-specific options if set. -/
def getPPOption (opt : Options → Bool) : DelabM Bool := do
@ -158,8 +158,8 @@ def whenNotPPOption (opt : Options → Bool) (d : Delab) : Delab := do
def annotatePos (pos : Nat) (stx : Syntax) : Syntax :=
stx.setInfo (SourceInfo.synthetic pos pos)
def annotateCurPos (stx : Syntax) : Delab := do
annotatePos (← getPos) stx
def annotateCurPos (stx : Syntax) : Delab :=
return annotatePos (← getPos) stx
def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do
-- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
@ -193,7 +193,7 @@ def addTermInfo (pos : Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false)
let info ← mkTermInfo stx e isBinder
modify fun s => { s with infos := s.infos.insert pos info }
where
mkTermInfo stx e isBinder := do Info.ofTermInfo {
mkTermInfo stx e isBinder := return Info.ofTermInfo {
elaborator := `Delab,
stx := stx,
lctx := (← getLCtx),
@ -206,7 +206,7 @@ def addFieldInfo (pos : Pos) (projName fieldName : Name) (stx : Syntax) (val : E
let info ← mkFieldInfo projName fieldName stx val
modify fun s => { s with infos := s.infos.insert pos info }
where
mkFieldInfo projName fieldName stx val := do Info.ofFieldInfo {
mkFieldInfo projName fieldName stx val := return Info.ofFieldInfo {
projName := projName,
fieldName := fieldName,
lctx := (← getLCtx),
@ -220,7 +220,7 @@ partial def delabFor : Name → Delab
(do let stx ← (delabAttribute.getValues (← getEnv) k).firstM id
let stx ← annotateCurPos stx
addTermInfo (← getPos) stx (← getExpr)
stx)
pure stx)
-- have `app.Option.some` fall back to `app` etc.
<|> if k.isAtomic then failure else delabFor k.getRoot
@ -229,7 +229,7 @@ partial def delab : Delab := do
let e ← getExpr
-- no need to hide atomic proofs
if ← !e.isAtomic <&&> !(← getPPOption getPPProofs) <&&> (try Meta.isProof e catch ex => false) then
if ← pure !e.isAtomic <&&> pure !(← getPPOption getPPProofs) <&&> (try Meta.isProof e catch ex => pure false) then
if ← getPPOption getPPProofsWithType then
let stx ← withType delab
return ← ``((_ : $stx))
@ -237,10 +237,11 @@ partial def delab : Delab := do
return ← ``(_)
let k ← getExprKind
let stx ← delabFor k <|> (liftM $ show MetaM Syntax from throwError "don't know how to delaborate '{k}'")
if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> !e.isMData then
if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> pure !e.isMData then
let typeStx ← withType delab
`(($stx:term : $typeStx:term)) >>= annotateCurPos
else stx
else
return stx
unsafe def mkAppUnexpanderAttribute : IO (KeyedDeclsAttribute Unexpander) :=
KeyedDeclsAttribute.init {
@ -267,11 +268,11 @@ def delabCore (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (opt
if pp.proofs.get? opts == none then
try if ← Meta.isProof e then opts := pp.proofs.set opts true
catch _ => pure ()
let e ← if getPPInstantiateMVars opts then ← Meta.instantiateMVars e else e
let e ← if getPPInstantiateMVars opts then Meta.instantiateMVars e else pure e
let optionsPerPos ←
if !getPPAll opts && getPPAnalyze opts && optionsPerPos.isEmpty then
withTheReader Core.Context (fun ctx => { ctx with options := opts }) do topDownAnalyze e
else optionsPerPos
else pure optionsPerPos
let (stx, {infos := infos, ..}) ← catchInternalId Delaborator.delabFailureId
(Delaborator.delab
{ defaultOptions := opts
@ -286,7 +287,7 @@ def delabCore (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (opt
/-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
let (stx, _) ← delabCore currNamespace openDecls e optionsPerPos
stx
return stx
builtin_initialize registerTraceClass `PrettyPrinter.delab

62
stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean generated
View file

@ -15,7 +15,7 @@ open Lean.Parser.Term
open SubExpr
def maybeAddBlockImplicit (ident : Syntax) : DelabM Syntax := do
if ← getPPOption getPPAnalysisBlockImplicit then `(@$ident:ident) else ident
if ← getPPOption getPPAnalysisBlockImplicit then `(@$ident:ident) else pure ident
def unfoldMDatas : Expr → Expr
| Expr.mdata _ e _ => unfoldMDatas e
@ -100,7 +100,7 @@ def delabConst : Delab := do
c := `_root_ ++ c
else
c := c₀
mkIdent c
pure <| mkIdent c
else
`($(mkIdent c).{$[$(ls.toArray.map quote)],*})
@ -108,7 +108,7 @@ def delabConst : Delab := do
if (← getPPOption getPPTagAppFns) then
stx ← annotateCurPos stx
addTermInfo (← getPos) stx (← getExpr)
stx
return stx
def withMDataOptions [Inhabited α] (x : DelabM α) : DelabM α := do
match ← getExpr with
@ -179,15 +179,15 @@ def delabAppExplicit : Delab := do
if ← getPPOption getPPInstanceTypes then
let typeStx ← withType delab
`(($stx : $typeStx))
else stx
else pure stx
else delab
pure (fnStx, paramKinds.tailD [], argStxs.push argStx))
Syntax.mkApp fnStx argStxs
return Syntax.mkApp fnStx argStxs
def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
getPPMotivesAll opts
<||> (← getPPMotivesPi opts <&&> returnsPi motive)
<||> (← getPPMotivesNonConst opts <&&> isNonConstFun motive)
pure (getPPMotivesAll opts)
<||> (pure (getPPMotivesPi opts) <&&> returnsPi motive)
<||> (pure (getPPMotivesNonConst opts) <&&> isNonConstFun motive)
def isRegularApp : DelabM Bool := do
let e ← getExpr
@ -198,8 +198,8 @@ def isRegularApp : DelabM Bool := do
return true
def unexpandRegularApp (stx : Syntax) : Delab := do
let Expr.const c .. ← pure (unfoldMDatas (← getExpr).getAppFn) | unreachable!
let fs ← appUnexpanderAttribute.getValues (← getEnv) c
let Expr.const c .. := (unfoldMDatas (← getExpr).getAppFn) | unreachable!
let fs := appUnexpanderAttribute.getValues (← getEnv) c
let ref ← getRef
fs.firstM fun f =>
match f stx |>.run ref |>.run () with
@ -209,10 +209,10 @@ def unexpandRegularApp (stx : Syntax) : Delab := do
-- abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β
-- abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
def unexpandCoe (stx : Syntax) : Delab := whenPPOption getPPCoercions do
if not (← isCoe (← getExpr)) then failure
if not (isCoe (← getExpr)) then failure
let e ← getExpr
match stx with
| `($fn $arg) => arg
| `($fn $arg) => return arg
| `($fn $args*) => `($(args.get! 0) $(args.eraseIdx 0)*)
| _ => failure
@ -256,8 +256,8 @@ def delabAppImplicit : Delab := do
-- This is e.g. necessary for `@Eq`.
let isImplicitApp ← try
let ty ← whnf (← inferType (← getExpr))
ty.isForall && (ty.binderInfo == BinderInfo.implicit || ty.binderInfo == BinderInfo.instImplicit)
catch _ => false
pure <| ty.isForall && (ty.binderInfo == BinderInfo.implicit || ty.binderInfo == BinderInfo.instImplicit)
catch _ => pure false
if isImplicitApp then failure
let (fnStx, _, argStxs) ← withAppFnArgs
@ -266,7 +266,7 @@ def delabAppImplicit : Delab := do
let arg ← getExpr
let opts ← getOptions
let mkNamedArg (name : Name) (argStx : Syntax) : DelabM Syntax := do
`(Parser.Term.namedArgument| ($(← mkIdent name):ident := $argStx:term))
`(Parser.Term.namedArgument| ($(mkIdent name):ident := $argStx:term))
let argStx? : Option Syntax ←
if ← getPPOption getPPAnalysisSkip then pure none
else if ← getPPOption getPPAnalysisHole then `(_)
@ -276,9 +276,9 @@ def delabAppImplicit : Delab := do
| param :: rest =>
if param.defVal.isSome && rest.isEmpty then
let v := param.defVal.get!
if !v.hasLooseBVars && v == arg then none else delab
if !v.hasLooseBVars && v == arg then pure none else delab
else if !param.isRegularExplicit && param.defVal.isNone then
if ← getPPOption getPPAnalysisNamedArg <||> (param.name == `motive <&&> shouldShowMotive arg opts) then mkNamedArg param.name (← delab) else none
if ← getPPOption getPPAnalysisNamedArg <||> (pure (param.name == `motive) <&&> shouldShowMotive arg opts) then mkNamedArg param.name (← delab) else pure none
else delab
let argStxs := match argStx? with
| none => argStxs
@ -339,7 +339,7 @@ where
| 0, varNames => x varNames
| n+1, varNames => do
let rec visitLambda : DelabM α := do
let varName ← (← getExpr).bindingName!.eraseMacroScopes
let varName := (← getExpr).bindingName!.eraseMacroScopes
-- Pattern variables cannot shadow each other
if varNames.contains varName then
let varName := (← getLCtx).getUnusedName varName
@ -379,7 +379,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
(do
let (Expr.const c us _) ← getExpr | failure
let (some info) ← getMatcherInfo? c | failure
{ matcherTy := (← getConstInfo c).instantiateTypeLevelParams us, info := info : AppMatchState })
return { matcherTy := (← getConstInfo c).instantiateTypeLevelParams us, info := info : AppMatchState })
(fun st => do
if st.params.size < st.info.numParams then
pure { st with params := st.params.push (← getExpr) }
@ -411,7 +411,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
match st.discrs, st.rhss with
| #[discr], #[] =>
let stx ← `(nomatch $discr)
Syntax.mkApp stx st.moreArgs
return Syntax.mkApp stx st.moreArgs
| _, #[] => failure
| _, _ =>
let pats ← delabPatterns st
@ -419,11 +419,11 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
let (piStx, lamMotive) := st.motive.get!
let opts ← getOptions
-- TODO: disable the match if other implicits are needed?
if ← st.motiveNamed <||> shouldShowMotive lamMotive opts then
if ← pure st.motiveNamed <||> shouldShowMotive lamMotive opts then
`(match $[$st.discrs:term],* : $piStx with $[| $pats,* => $st.rhss]*)
else
`(match $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*)
Syntax.mkApp stx st.moreArgs
return Syntax.mkApp stx st.moreArgs
/--
Delaborate applications of the form `(fun x => b) v` as `let_fun x := v; b`
@ -501,7 +501,7 @@ private partial def delabBinders (delabGroup : Array Syntax → Syntax → Delab
withBindingBodyUnusedName fun stxN => delabBinders delabGroup (curNames.push stxN)
else
-- don't group => delab body and prepend current binder group
let (stx, stxN) ← withBindingBodyUnusedName fun stxN => do (← delab, stxN)
let (stx, stxN) ← withBindingBodyUnusedName fun stxN => return (← delab, stxN)
delabGroup (curNames.push stxN) stx
@[builtinDelab lam]
@ -511,7 +511,7 @@ def delabLam : Delab :=
let stxT ← withBindingDomain delab
let ppTypes ← getPPOption getPPFunBinderTypes
let expl ← getPPOption getPPExplicit
let usedDownstream ← curNames.any (fun n => hasIdent n.getId stxBody)
let usedDownstream := curNames.any (fun n => hasIdent n.getId stxBody)
-- leave lambda implicit if possible
-- TODO: for now we just always block implicit lambdas when delaborating. We can revisit.
@ -561,7 +561,7 @@ def delabLam : Delab :=
def delabForall : Delab :=
delabBinders fun curNames stxBody => do
let e ← getExpr
let prop ← try isProp e catch _ => false
let prop ← try isProp e catch _ => pure false
let stxT ← withBindingDomain delab
let group ← match e.binderInfo with
| BinderInfo.implicit => `(bracketedBinderF|{$curNames* : $stxT})
@ -745,7 +745,7 @@ partial def delabDoElems : DelabM (List Syntax) := do
prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV)
else
let stx ← delab
[←`(doElem|$stx:term)]
return [←`(doElem|$stx:term)]
where
prependAndRec x : DelabM _ := List.cons <$> x <*> delabDoElems
@ -757,18 +757,16 @@ def delabDo : Delab := whenPPOption getPPNotation do
`(do $items:doSeqItem*)
def reifyName : Expr → DelabM Name
| Expr.const ``Lean.Name.anonymous .. => Name.anonymous
| Expr.app (Expr.app (Expr.const ``Lean.Name.mkStr ..) n _) (Expr.lit (Literal.strVal s) _) _ => do
(← reifyName n).mkStr s
| Expr.app (Expr.app (Expr.const ``Lean.Name.mkNum ..) n _) (Expr.lit (Literal.natVal i) _) _ => do
(← reifyName n).mkNum i
| Expr.const ``Lean.Name.anonymous .. => return Name.anonymous
| Expr.app (Expr.app (Expr.const ``Lean.Name.mkStr ..) n _) (Expr.lit (Literal.strVal s) _) _ => return (← reifyName n).mkStr s
| Expr.app (Expr.app (Expr.const ``Lean.Name.mkNum ..) n _) (Expr.lit (Literal.natVal i) _) _ => return (← reifyName n).mkNum i
| _ => failure
@[builtinDelab app.Lean.Name.mkStr]
def delabNameMkStr : Delab := whenPPOption getPPNotation do
let n ← reifyName (← getExpr)
-- not guaranteed to be a syntactically valid name, but usually more helpful than the explicit version
mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{n}"]
return mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{n}"]
@[builtinDelab app.Lean.Name.mkNum]
def delabNameMkNum : Delab := delabNameMkStr

6
stage0/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean generated
View file

@ -41,8 +41,8 @@ variable [MonadLiftT IO m]
def mkRoot (e : Expr) : SubExpr := ⟨e, 1⟩
def getExpr : m Expr := do (← readThe SubExpr).expr
def getPos : m Pos := do (← readThe SubExpr).pos
def getExpr : m Expr := return (← readThe SubExpr).expr
def getPos : m Pos := return (← readThe SubExpr).pos
def descend (child : Expr) (childIdx : Pos) (x : m α) : m α :=
withTheReader SubExpr (fun cfg => { cfg with expr := child, pos := cfg.pos * maxChildren + childIdx }) x
@ -128,7 +128,7 @@ def nextExtraPos : m Pos := do
let iter ← getThe HoleIterator
let pos := iter.toPos
modifyThe HoleIterator HoleIterator.next
pos
return pos
end Hole
end SubExpr

54
stage0/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean generated
View file

@ -134,24 +134,24 @@ def getPPAnalysisBlockImplicit (o : Options) : Bool := o.get `pp.analysis.bloc
namespace PrettyPrinter.Delaborator
def returnsPi (motive : Expr) : MetaM Bool := do
lambdaTelescope motive fun xs b => b.isForall
lambdaTelescope motive fun xs b => return b.isForall
def isNonConstFun (motive : Expr) : MetaM Bool := do
match motive with
| Expr.lam name d b _ => isNonConstFun b
| _ => motive.hasLooseBVars
| _ => return motive.hasLooseBVars
def isSimpleHOFun (motive : Expr) : MetaM Bool := do
not (← returnsPi motive) && not (← isNonConstFun motive)
def isSimpleHOFun (motive : Expr) : MetaM Bool :=
return not (← returnsPi motive) && not (← isNonConstFun motive)
def isType2Type (motive : Expr) : MetaM Bool := do
match ← inferType motive with
| Expr.forallE _ (Expr.sort ..) (Expr.sort ..) .. => true
| _ => false
| Expr.forallE _ (Expr.sort ..) (Expr.sort ..) .. => return true
| _ => return false
def isFOLike (motive : Expr) : MetaM Bool := do
let f := motive.getAppFn
f.isFVar || f.isConst
return f.isFVar || f.isConst
def isIdLike (arg : Expr) : Bool :=
-- TODO: allow `id` constant as well?
@ -168,21 +168,21 @@ def isCoe (e : Expr) : Bool :=
def isStructureInstance (e : Expr) : MetaM Bool := do
match e.isConstructorApp? (← getEnv) with
| some s => isStructure (← getEnv) s.induct
| none => false
| some s => return isStructure (← getEnv) s.induct
| none => return false
namespace TopDownAnalyze
partial def hasMVarAtCurrDepth (e : Expr) : MetaM Bool := do
let mctx ← getMCtx
Option.isSome $ e.findMVar? fun mvarId =>
return Option.isSome <| e.findMVar? fun mvarId =>
match mctx.findDecl? mvarId with
| some mdecl => mdecl.depth == mctx.depth
| _ => false
partial def hasLevelMVarAtCurrDepth (e : Expr) : MetaM Bool := do
let mctx ← getMCtx
Option.isSome $ e.findLevelMVar? fun mvarId =>
return Option.isSome <| e.findLevelMVar? fun mvarId =>
mctx.findLevelDepth? mvarId == some mctx.depth
private def valUnknown (e : Expr) : MetaM Bool := do
@ -225,10 +225,10 @@ def checkpointDefEq (t s : Expr) : MetaM Bool := do
isDefEqAssigning t s
def isHigherOrder (type : Expr) : MetaM Bool := do
forallTelescopeReducing type fun xs b => xs.size > 0 && b.isSort
forallTelescopeReducing type fun xs b => return xs.size > 0 && b.isSort
def isFunLike (e : Expr) : MetaM Bool := do
forallTelescopeReducing (← inferType e) fun xs b => xs.size > 0
forallTelescopeReducing (← inferType e) fun xs b => return xs.size > 0
def isSubstLike (e : Expr) : Bool :=
e.isAppOfArity `Eq.ndrec 6 || e.isAppOfArity `Eq.rec 6
@ -241,8 +241,8 @@ where
| Name.num .. => true
| Name.anonymous => false
def mvarName (mvar : Expr) : MetaM Name := do
(← getMVarDecl mvar.mvarId!).userName
def mvarName (mvar : Expr) : MetaM Name :=
return (← getMVarDecl mvar.mvarId!).userName
def containsBadMax : Level → Bool
| Level.succ u .. => containsBadMax u
@ -312,7 +312,7 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat :=
-- These are incomplete (and possibly unsound) heuristics.
-- TODO: do I need to snapshot the state before calling this?
match fuel with
| 0 => false
| 0 => return false
| fuel + 1 =>
if ← isTrivialBottomUp e then return true
let f := e.getAppFn
@ -323,10 +323,10 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat :=
for i in [:mvars.size] do
if bInfos[i] == BinderInfo.instImplicit then
inspectOutParams args[i] mvars[i]
else if ← bInfos[i] == BinderInfo.default then
else if bInfos[i] == BinderInfo.default then
if ← isTrivialBottomUp args[i] then tryUnify args[i] mvars[i]
else if ← typeUnknown mvars[i] <&&> canBottomUp args[i] mvars[i] fuel then tryUnify args[i] mvars[i]
if ← (isHBinOp e <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then tryUnify mvars[0] mvars[1]
if ← (pure (isHBinOp e) <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then tryUnify mvars[0] mvars[1]
if mvar?.isSome then tryUnify resultType (← inferType mvar?.get!)
return !(← valUnknown resultType)
@ -371,7 +371,7 @@ mutual
trace[pp.analyze] "{(← read).knowsType}.{(← read).knowsLevel}"
let e ← getExpr
let opts ← getOptions
if ← !e.isAtomic <&&> !(getPPProofs opts) <&&> (try Meta.isProof e catch ex => false) then
if ← (pure !e.isAtomic) <&&> pure !(getPPProofs opts) <&&> (try Meta.isProof e catch ex => pure false) then
if getPPProofsWithType opts then
withType $ withKnowing true true $ analyze
return ()
@ -398,7 +398,7 @@ mutual
withType $ withKnowing true false $ analyze
willKnowType := true
else if ← (!(← read).knowsType <||> (← read).inBottomUp) <&&> isStructureInstance (← getExpr) then
else if ← (pure !(← read).knowsType <||> pure (← read).inBottomUp) <&&> isStructureInstance (← getExpr) then
withType do
annotateBool `pp.structureInstanceTypes
withKnowing true false $ analyze
@ -515,7 +515,7 @@ mutual
hBinOpHeuristic := do
let { args, mvars, bInfos, ..} ← read
if ← (isHBinOp (← getExpr) <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then
if ← (pure (isHBinOp (← getExpr)) <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then
tryUnify mvars[0] mvars[1]
collectTrivialBottomUps := do
@ -536,7 +536,7 @@ mutual
| Expr.lam .., Expr.forallE n t b .. =>
let mut annotated := false
for i in [:argIdx] do
if ← bInfos[i] == BinderInfo.implicit <&&> valUnknown mvars[i] <&&> withNewMCtxDepth (checkpointDefEq t mvars[i]) then
if ← pure (bInfos[i] == BinderInfo.implicit) <&&> valUnknown mvars[i] <&&> withNewMCtxDepth (checkpointDefEq t mvars[i]) then
annotateBool `pp.funBinderTypes
tryUnify args[i] mvars[i]
-- Note: currently we always analyze the lambda binding domains in `analyzeLam`
@ -549,7 +549,7 @@ mutual
| _, _ => return false
for i in [:args.size] do
if ← bInfos[i] == BinderInfo.default then
if bInfos[i] == BinderInfo.default then
let b ← withNaryArg i (core i (← inferType mvars[i]))
if b then modify fun s => { s with funBinders := s.funBinders.set! i true }
@ -569,7 +569,7 @@ mutual
let argType ← inferType arg
let processNaturalImplicit : AnalyzeAppM Unit := do
if (← valUnknown mvars[i] <||> higherOrders[i]) && !forceRegularApp then
if (← valUnknown mvars[i] <||> pure higherOrders[i]) && !forceRegularApp then
annotateNamedArg (← mvarName mvars[i])
modify fun s => { s with provideds := s.provideds.set! i true }
else
@ -580,7 +580,7 @@ mutual
match bInfos[i] with
| BinderInfo.default =>
if ← getPPAnalyzeExplicitHoles (← getOptions) <&&> !(← valUnknown mvars[i]) <&&> !(← readThe Context).inBottomUp <&&> !(← isFunLike arg) <&&> !funBinders[i] <&&> checkpointDefEq mvars[i] arg then
if ← pure (getPPAnalyzeExplicitHoles (← getOptions)) <&&> pure !(← valUnknown mvars[i]) <&&> pure !(← readThe Context).inBottomUp <&&> pure !(← isFunLike arg) <&&> pure !funBinders[i] <&&> checkpointDefEq mvars[i] arg then
annotateBool `pp.analysis.hole
else
modify fun s => { s with provideds := s.provideds.set! i true }
@ -596,7 +596,7 @@ mutual
annotateBool `pp.analysis.skip
provided := false
else if getPPAnalyzeCheckInstances (← getOptions) then
let instResult ← try trySynthInstance argType catch _ => LOption.undef
let instResult ← try trySynthInstance argType catch _ => pure LOption.undef
match instResult with
| LOption.some inst =>
if ← checkpointDefEq inst arg then annotateBool `pp.analysis.skip; provided := false
@ -628,7 +628,7 @@ def topDownAnalyze (e : Expr) : MetaM OptionsPerPos := do
let s₀ ← get
traceCtx `pp.analyze do
withReader (fun ctx => { ctx with config := Elab.Term.setElabConfig ctx.config }) do
let ϕ : AnalyzeM OptionsPerPos := do withNewMCtxDepth analyze; (← get).annotations
let ϕ : AnalyzeM OptionsPerPos := do withNewMCtxDepth analyze; pure (← get).annotations
try
let knowsType := getPPAnalyzeKnowsType (← getOptions)
ϕ { knowsType := knowsType, knowsLevel := knowsType, subExpr := mkRoot e }

4
stage0/src/Lean/PrettyPrinter/Formatter.lean generated
View file

@ -297,9 +297,9 @@ def trailingNode.formatter (k : SyntaxNodeKind) (_ _ : Nat) (p : Formatter) : Fo
-- leading term, not actually produced by `p`
categoryParser.formatter `foo
def parseToken (s : String) : FormatterM ParserState := do
def parseToken (s : String) : FormatterM ParserState :=
-- include comment tokens, e.g. when formatting `- -0`
(Parser.andthenFn Parser.whitespace (Parser.tokenFn [])) {
return (Parser.andthenFn Parser.whitespace (Parser.tokenFn [])) {
input := s,
fileName := "",
fileMap := FileMap.ofString "",

8
stage0/src/Lean/ReducibilityAttrs.lean generated
View file

@ -40,12 +40,12 @@ def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := d
def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
match (← getReducibilityStatus declName) with
| ReducibilityStatus.reducible => true
| _ => false
| ReducibilityStatus.reducible => return true
| _ => return false
def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
match (← getReducibilityStatus declName) with
| ReducibilityStatus.irreducible => true
| _ => false
| ReducibilityStatus.irreducible => return true
| _ => return false
end Lean

8
stage0/src/Lean/Server/AsyncList.lean generated
View file

@ -51,7 +51,7 @@ partial def unfoldAsync (f : StateT σ (EIO ε) $ Option α) (init : σ)
return cons aNext $ asyncTail tNext
let tInit ← EIO.asTask (step init)
asyncTail tInit
return asyncTail tInit
/-- The computed, synchronous list. If an async tail was present, returns also
its terminating value. -/
@ -70,14 +70,14 @@ partial def waitAll (p : α → Bool := fun _ => true) : AsyncList ε α → Bas
| cons hd tl => do
if p hd then
let t ← tl.waitAll p
t.map fun ⟨l, e?⟩ => ⟨hd :: l, e?⟩
return t.map fun ⟨l, e?⟩ => ⟨hd :: l, e?⟩
else
return Task.pure ⟨[hd], none⟩
| nil => return Task.pure ⟨[], none⟩
| asyncTail tl => do
BaseIO.bindTask tl fun
| Except.ok tl => tl.waitAll p
| Except.error e => Task.pure ⟨[], some e⟩
| Except.error e => return Task.pure ⟨[], some e⟩
/-- Spawns a `Task` acting like `List.find?` but which will wait for tail evalution
when necessary to traverse the list. If the tail terminates before a matching element
@ -90,7 +90,7 @@ partial def waitFind? (p : α → Bool) : AsyncList ε α → BaseIO (Task $ Exc
| asyncTail tl => do
BaseIO.bindTask tl fun
| Except.ok tl => tl.waitFind? p
| Except.error e => Task.pure <| Except.error e
| Except.error e => return Task.pure <| Except.error e
/-- Extends the `finishedPrefix` as far as possible. If computation was ongoing
and has finished, also returns the terminating value. -/

16
stage0/src/Lean/Server/Completion.lean generated
View file

@ -26,11 +26,11 @@ def addToBlackList (env : Environment) (declName : Name) : Environment :=
private def isBlackListed (declName : Name) : MetaM Bool := do
let env ← getEnv
(declName.isInternal && !isPrivateName declName)
<||> isAuxRecursor env declName
<||> isNoConfusion env declName
(pure (declName.isInternal && !isPrivateName declName))
<||> (pure <| isAuxRecursor env declName)
<||> (pure <| isNoConfusion env declName)
<||> isRec declName
<||> completionBlackListExt.isTagged env declName
<||> (pure <| completionBlackListExt.isTagged env declName)
<||> isMatcher declName
private partial def consumeImplicitPrefix (e : Expr) (k : Expr → MetaM α) : MetaM α := do
@ -76,7 +76,7 @@ structure State where
abbrev M := OptionT $ StateRefT State MetaM
private def addCompletionItem (label : Name) (type : Expr) (expectedType? : Option Expr) (declName? : Option Name) (kind : CompletionItemKind) : M Unit := do
let docString? ← if let some declName := declName? then findDocString? (← getEnv) declName else none
let docString? ← if let some declName := declName? then findDocString? (← getEnv) declName else pure none
let item ← mkCompletionItem label type docString? kind
if (← isTypeApplicable type expectedType?) then
modify fun s => { s with itemsMain := s.itemsMain.push item }
@ -88,7 +88,7 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt
if constInfo.isCtor then
return CompletionItemKind.constructor
else if constInfo.isInductive then
if (← isClass env constInfo.name) then
if isClass env constInfo.name then
return CompletionItemKind.class
else if (← isEnumType constInfo.name) then
return CompletionItemKind.enum
@ -102,7 +102,7 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt
return CompletionItemKind.constant
private def addCompletionItemForDecl (label : Name) (declName : Name) (expectedType? : Option Expr) : M Unit := do
if let some c ← (← getEnv).find? declName then
if let some c := (← getEnv).find? declName then
addCompletionItem label c.type expectedType? (some declName) (← getCompletionKindForDecl c)
private def addKeywordCompletionItem (keyword : String) : M Unit := do
@ -160,7 +160,7 @@ private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName :
return some s₂
else
return none
| _, _ => none
| _, _ => return none
else
return none

20
stage0/src/Lean/Server/FileWorker.lean generated
View file

@ -134,7 +134,7 @@ section Elab
-- followup errors
publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
publishIleanInfoFinal m ctx.hOut #[headerSnap]
AsyncList.nil
pure AsyncList.nil
else
-- This will overwrite existing ilean info for the file since this has a
-- higher version number.
@ -199,7 +199,7 @@ section Initialization
let (headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx
let mut srcSearchPath ← initSrcSearchPath (← getBuildDir)
let lakePath ← match (← IO.getEnv "LAKE") with
| some path => System.FilePath.mk path
| some path => pure <| System.FilePath.mk path
| none =>
let lakePath :=
-- backward compatibility, kill when `leanpkg` is removed
@ -208,7 +208,7 @@ section Initialization
let lakePath ← match (← IO.getEnv "LEAN_SYSROOT") with
| some path => pure <| System.FilePath.mk path / "bin" / lakePath
| _ => pure <| (← appDir) / lakePath
lakePath.withExtension System.FilePath.exeExtension
pure <| lakePath.withExtension System.FilePath.exeExtension
let (headerEnv, msgLog) ← try
if let some path := m.uri.toPath? then
-- NOTE: we assume for now that `lakefile.lean` does not have any non-stdlib deps
@ -224,7 +224,7 @@ section Initialization
try
if let some path := m.uri.toPath? then
headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
catch _ => ()
catch _ => pure ()
let cmdState := Elab.Command.mkState headerEnv msgLog opts
let cmdState := { cmdState with infoState := {
enabled := true
@ -316,7 +316,7 @@ section Updates
else newHeaderSnap
let newLastStx ← parseNextCmd newMeta.text.source preLastSnap
if newLastStx != lastSnap.stx then
validSnaps ← validSnaps.dropLast
validSnaps := validSnaps.dropLast
let cancelTk ← CancelToken.new
let newSnaps ← unfoldCmdSnaps newMeta newHeaderSnap validSnaps.toArray cancelTk ctx
let newCmdSnaps := AsyncList.ofList validSnaps ++ newSnaps
@ -437,13 +437,13 @@ section MainLoop
let msg ← ctx.hIn.readLspMessage
let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
: IO PendingRequestMap := do
if (←hasFinished task) then
if (← hasFinished task) then
/- Handler tasks are constructed so that the only possible errors here
are failures of writing a response into the stream. -/
if let Except.error e := task.get then
throwServerError s!"Failed responding to request {id}: {e}"
acc.erase id
else acc
pure <| acc.erase id
else pure acc
let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
st := { st with pendingRequests }
@ -459,7 +459,7 @@ section MainLoop
handleRequest id method (toJson params)
mainLoop
| Message.notification "exit" none =>
let doc ← (←get).doc
let doc := (←get).doc
doc.cancelTk.set
return ()
| Message.notification method (some params) =>
@ -480,7 +480,7 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
so if we get the line number correct it shouldn't matter that there
is a CR there. -/
let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
let e ← e.withPrefix s!"[{param.textDocument.uri}] "
let e := e.withPrefix s!"[{param.textDocument.uri}] "
let _ ← IO.setStderr e
try
let (ctx, st) ← initializeWorker meta i o e initParams.param opts

10
stage0/src/Lean/Server/FileWorker/RequestHandling.lean generated
View file

@ -132,7 +132,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
let mut expr := ti.expr
if kind == type then
expr ← ci.runMetaM i.lctx do
Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
return Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
match expr with
| Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
| Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder snap.infoTree i id
@ -177,7 +177,7 @@ open Elab in
partial def handlePlainGoal (p : PlainGoalParams)
: RequestM (RequestTask (Option PlainGoal)) := do
let t ← getInteractiveGoals p
t.map <| Except.map <| Option.map <| fun ⟨goals⟩ =>
return t.map <| Except.map <| Option.map <| fun ⟨goals⟩ =>
if goals.isEmpty then
{ goals := #[], rendered := "no goals" }
else
@ -210,7 +210,7 @@ partial def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
def handlePlainTermGoal (p : PlainTermGoalParams)
: RequestM (RequestTask (Option PlainTermGoal)) := do
let t ← getInteractiveTermGoal p
t.map <| Except.map <| Option.map fun goal =>
return t.map <| Except.map <| Option.map fun goal =>
{ goal := toString goal.toInteractiveGoal.pretty
range := goal.range
}
@ -246,7 +246,7 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
withWaitFindSnap doc (fun s => s.endPos > pos)
(notFoundX := pure #[]) fun snap => do
let (snaps, _) ← doc.allSnaps.updateFinishedPrefix
if let some his ← highlightRefs? snaps.finishedPrefix.toArray p.position then
if let some his := highlightRefs? snaps.finishedPrefix.toArray p.position then
return his
if let some hi := highlightReturn? none snap.stx then
return #[hi]
@ -265,7 +265,7 @@ partial def handleDocumentSymbol (p : DocumentSymbolParams)
throw RequestError.fileChanged
| some (ElabTaskError.ioError e) =>
throw (e : RequestError)
| _ => ()
| _ => pure ()
let lastSnap := cmdSnaps.finishedPrefix.getLastD doc.headerSnap
stxs := stxs ++ (← parseAhead doc.meta.text.source lastSnap).toList

Some files were not shown because too many files have changed in this diff Show more