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 2020-12-04 09:58:33 -08:00
parent 6f1facd07c
commit 540f9aa1ea
26 changed files with 11293 additions and 2783 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
stage0/src/Lean.lean generated
View file

@ -26,3 +26,4 @@ import Lean.PrettyPrinter
import Lean.CoreM
import Lean.InternalExceptionId
import Lean.Server
import Lean.ScopedEnvExtension

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

@ -17,3 +17,5 @@ import Lean.Data.Options
import Lean.Data.Position
import Lean.Data.SMap
import Lean.Data.Trie
import Lean.Data.PrefixTree
import Lean.Data.NameTrie

66
stage0/src/Lean/Data/NameTrie.lean generated Normal file
View file

@ -0,0 +1,66 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Data.PrefixTree
namespace Lean
inductive NamePart
| str (s : String)
| num (n : Nat)
instance : ToString NamePart where
toString
| NamePart.str s => s
| NamePart.num n => toString n
def NamePart.lt : NamePart → NamePart → Bool
| NamePart.str a, NamePart.str b => a < b
| NamePart.num a, NamePart.num b => a < b
| NamePart.num _, NamePart.str _ => true
| _, _ => false
def NameTrie (β : Type u) := PrefixTree NamePart β NamePart.lt
private def toKey (n : Name) : List NamePart :=
loop n []
where
loop
| Name.str p s _, parts => loop p (NamePart.str s :: parts)
| Name.num p n _, parts => loop p (NamePart.num n :: parts)
| Name.anonymous, parts => parts
def NameTrie.insert (t : NameTrie β) (n : Name) (b : β) : NameTrie β :=
PrefixTree.insert t (toKey n) b
def NameTrie.empty : NameTrie β :=
PrefixTree.empty
instance : Inhabited (NameTrie β) where
default := NameTrie.empty
instance : EmptyCollection (NameTrie β) where
emptyCollection := NameTrie.empty
def NameTrie.find? (t : NameTrie β) (k : Name) : Option β :=
PrefixTree.find? t (toKey k)
@[inline]
def NameTrie.foldMatchingM [Monad m] (t : NameTrie β) (k : Name) (init : σ) (f : β → σ → m σ) : m σ :=
PrefixTree.foldMatchingM t (toKey k) init f
@[inline]
def NameTrie.foldM [Monad m] (t : NameTrie β) (init : σ) (f : β → σ → m σ) : m σ :=
t.foldMatchingM Name.anonymous init f
@[inline]
def NameTrie.forMatchingM [Monad m] (t : NameTrie β) (k : Name) (f : β → m Unit) : m Unit :=
PrefixTree.forMatchingM t (toKey k) f
@[inline]
def NameTrie.forM [Monad m] (t : NameTrie β) (f : β → m Unit) : m Unit :=
t.forMatchingM Name.anonymous f
end Lean

111
stage0/src/Lean/Data/PrefixTree.lean generated Normal file
View file

@ -0,0 +1,111 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Std.Data.RBMap
namespace Lean
open Std
/- Similar to trie, but for arbitrary keys -/
inductive PrefixTreeNode (α : Type u) (β : Type v) where
| Node : Option β → RBNode α (fun _ => PrefixTreeNode α β) → PrefixTreeNode α β
instance : Inhabited (PrefixTreeNode α β) where
default := PrefixTreeNode.Node none RBNode.leaf
namespace PrefixTreeNode
def empty : PrefixTreeNode α β :=
PrefixTreeNode.Node none RBNode.leaf
@[specialize]
partial def insert (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : List α) (val : β) : PrefixTreeNode α β :=
let rec insertEmpty (k : List α) : PrefixTreeNode α β :=
match k with
| [] => PrefixTreeNode.Node (some val) RBNode.leaf
| k :: ks =>
let t := insertEmpty ks
PrefixTreeNode.Node none (RBNode.singleton k t)
let rec loop
| PrefixTreeNode.Node v m, [] =>
PrefixTreeNode.Node (some val) m -- overrides old value
| PrefixTreeNode.Node v m, k :: ks =>
let t := match RBNode.find lt m k with
| none => insertEmpty ks
| some t => loop t ks
PrefixTreeNode.Node v (RBNode.insert lt m k t)
loop t k
@[specialize]
partial def find? (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : List α) : Option β :=
let rec loop
| PrefixTreeNode.Node val m, [] => val
| PrefixTreeNode.Node val m, k :: ks =>
match RBNode.find lt m k with
| none => none
| some t => loop t ks
loop t k
@[specialize]
partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : List α) (init : σ) (f : β → σ → m σ) : m σ :=
let rec fold : PrefixTreeNode α β → σ → m σ
| PrefixTreeNode.Node b? n, d => do
let d ← match b? with
| none => pure d
| some b => f b d
n.foldM (init := d) fun d _ t => fold t d
let rec find : List α → PrefixTreeNode α β → σ → m σ
| [], t, d => fold t d
| k::ks, PrefixTreeNode.Node _ m, d =>
match RBNode.find lt m k with
| none => pure init
| some t => find ks t d
find k t init
inductive WellFormed (lt : α → α → Bool) : PrefixTreeNode α β → Prop where
| emptyWff : WellFormed lt empty
| insertWff {t : PrefixTreeNode α β} {k : List α} {val : β} : WellFormed lt t → WellFormed lt (insert t lt k val)
end PrefixTreeNode
def PrefixTree (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v) :=
{ t : PrefixTreeNode α β // t.WellFormed lt }
open PrefixTreeNode
def PrefixTree.empty : PrefixTree α β p :=
⟨PrefixTreeNode.empty, WellFormed.emptyWff⟩
instance : Inhabited (PrefixTree α β p) where
default := PrefixTree.empty
instance : EmptyCollection (PrefixTree α β p) where
emptyCollection := PrefixTree.empty
@[inline]
def PrefixTree.insert (t : PrefixTree α β p) (k : List α) (v : β) : PrefixTree α β p :=
⟨t.val.insert p k v, WellFormed.insertWff t.property⟩
@[inline]
def PrefixTree.find? (t : PrefixTree α β p) (k : List α) : Option β :=
t.val.find? p k
@[inline]
def PrefixTree.foldMatchingM [Monad m] (t : PrefixTree α β p) (k : List α) (init : σ) (f : β → σ → m σ) : m σ :=
t.val.foldMatchingM p k init f
@[inline]
def PrefixTree.foldM [Monad m] (t : PrefixTree α β p) (init : σ) (f : β → σ → m σ) : m σ :=
t.foldMatchingM [] init f
@[inline]
def PrefixTree.forMatchingM [Monad m] (t : PrefixTree α β p) (k : List α) (f : β → m Unit) : m Unit :=
t.val.foldMatchingM p k () (fun b _ => f b)
@[inline]
def PrefixTree.forM [Monad m] (t : PrefixTree α β p) (f : β → m Unit) : m Unit :=
t.forMatchingM [] f
end Lean

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

@ -3,13 +3,13 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
/-! Extensible parsing via attributes -/
import Lean.ScopedEnvExtension
import Lean.Parser.Basic
import Lean.Parser.StrInterpolation
import Lean.KeyedDeclsAttribute
/-! Extensible parsing via attributes -/
namespace Lean
namespace Parser
@ -47,29 +47,45 @@ private def addBuiltinParserCategory (catName : Name) (leadingIdentAsSymbol : Bo
let categories ← IO.ofExcept $ addParserCategoryCore categories catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol}
builtinParserCategoriesRef.set categories
inductive ParserExtensionOleanEntry where
| token (val : Token) : ParserExtensionOleanEntry
| kind (val : SyntaxNodeKind) : ParserExtensionOleanEntry
| category (catName : Name) (leadingIdentAsSymbol : Bool)
| parser (catName : Name) (declName : Name) (prio : Nat) : ParserExtensionOleanEntry
namespace ParserExtension
inductive ParserExtensionEntry where
| token (val : Token) : ParserExtensionEntry
| kind (val : SyntaxNodeKind) : ParserExtensionEntry
inductive OLeanEntry where
| token (val : Token) : OLeanEntry
| kind (val : SyntaxNodeKind) : OLeanEntry
| category (catName : Name) (leadingIdentAsSymbol : Bool)
| parser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : ParserExtensionEntry
| parser (catName : Name) (declName : Name) (prio : Nat) : OLeanEntry
structure ParserExtensionState where
inductive Entry where
| token (val : Token) : Entry
| kind (val : SyntaxNodeKind) : Entry
| category (catName : Name) (leadingIdentAsSymbol : Bool)
| parser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : Entry
instance : Inhabited OLeanEntry where
default := OLeanEntry.token arbitrary
instance : Inhabited Entry where
default := Entry.token arbitrary
def Entry.toOLeanEntry : Entry → OLeanEntry
| token v => OLeanEntry.token v
| kind v => OLeanEntry.kind v
| category c l => OLeanEntry.category c l
| parser c d _ _ prio => OLeanEntry.parser c d prio
structure State where
tokens : TokenTable := {}
kinds : SyntaxNodeKindSet := {}
categories : ParserCategories := {}
newEntries : List ParserExtensionOleanEntry := []
instance : Inhabited ParserExtensionState := ⟨{}⟩
instance : Inhabited State := ⟨{}⟩
abbrev ParserExtension := PersistentEnvExtension ParserExtensionOleanEntry ParserExtensionEntry ParserExtensionState
end ParserExtension
private def ParserExtension.mkInitial : IO ParserExtensionState := do
open ParserExtension in
abbrev ParserExtension := ScopedEnvExtension OLeanEntry Entry State
private def ParserExtension.mkInitial : IO ParserExtension.State := do
let tokens ← builtinTokenTable.get
let kinds ← builtinSyntaxNodeKindSetRef.get
let categories ← builtinParserCategoriesRef.get
@ -145,22 +161,21 @@ def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) (pri
def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
addBuiltinParser catName declName false p prio
private def ParserExtensionAddEntry (s : ParserExtensionState) (e : ParserExtensionEntry) : ParserExtensionState :=
def ParserExtension.addEntryImpl (s : State) (e : Entry) : State :=
match e with
| ParserExtensionEntry.token tk =>
| Entry.token tk =>
match addTokenConfig s.tokens tk with
| Except.ok tokens => { s with tokens := tokens, newEntries := ParserExtensionOleanEntry.token tk :: s.newEntries }
| Except.ok tokens => { s with tokens := tokens }
| _ => unreachable!
| ParserExtensionEntry.kind k =>
{ s with kinds := s.kinds.insert k, newEntries := ParserExtensionOleanEntry.kind k :: s.newEntries }
| ParserExtensionEntry.category catName leadingIdentAsSymbol =>
| Entry.kind k =>
{ s with kinds := s.kinds.insert k }
| Entry.category catName leadingIdentAsSymbol =>
if s.categories.contains catName then s
else { s with
categories := s.categories.insert catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol },
newEntries := ParserExtensionOleanEntry.category catName leadingIdentAsSymbol :: s.newEntries }
| ParserExtensionEntry.parser catName declName leading parser prio =>
categories := s.categories.insert catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol } }
| Entry.parser catName declName leading parser prio =>
match addParser s.categories catName declName leading parser prio with
| Except.ok categories => { s with categories := categories, newEntries := ParserExtensionOleanEntry.parser catName declName prio :: s.newEntries }
| Except.ok categories => { s with categories := categories }
| _ => unreachable!
unsafe def mkParserOfConstantUnsafe
@ -331,32 +346,22 @@ builtin_initialize
runParserAttributeHooks Name.anonymous decl (builtin := false)
}
private def ParserExtension.addImported (es : Array (Array ParserExtensionOleanEntry)) : ImportM ParserExtensionState := do
let s ← ParserExtension.mkInitial
es.foldlM (init := s) fun s entries =>
entries.foldlM (init := s) fun s entry =>
match entry with
| ParserExtensionOleanEntry.token tk => do
let tokens ← IO.ofExcept (addTokenConfig s.tokens tk)
pure { s with tokens := tokens }
| ParserExtensionOleanEntry.kind k =>
pure { s with kinds := s.kinds.insert k }
| ParserExtensionOleanEntry.category catName leadingIdentAsSymbol => do
let categories ← IO.ofExcept (addParserCategoryCore s.categories catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol})
pure { s with categories := categories }
| ParserExtensionOleanEntry.parser catName declName prio => do
let p ← mkParserOfConstant s.categories declName
let categories ← IO.ofExcept $ addParser s.categories catName declName p.1 p.2 prio
pure { s with categories := categories }
private def ParserExtension.OLeanEntry.toEntry (s : State) : OLeanEntry → ImportM Entry
| token tk => return Entry.token tk
| kind k => return Entry.kind k
| 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
builtin_initialize parserExtension : ParserExtension ←
registerPersistentEnvExtension {
name := `parserExt,
mkInitial := ParserExtension.mkInitial,
addImportedFn := ParserExtension.addImported,
addEntryFn := ParserExtensionAddEntry,
exportEntriesFn := fun s => s.newEntries.reverse.toArray,
statsFn := fun s => format "number of local entries: " ++ format s.newEntries.length
registerScopedEnvExtension {
name := `parserExt
mkInitial := ParserExtension.mkInitial
addEntry := ParserExtension.addEntryImpl
toOLeanEntry := ParserExtension.Entry.toOLeanEntry
ofOLeanEntry := ParserExtension.OLeanEntry.toEntry
eraseEntry := fun s _ => s
}
def isParserCategory (env : Environment) (catName : Name) : Bool :=
@ -366,7 +371,7 @@ def addParserCategory (env : Environment) (catName : Name) (leadingIdentAsSymbol
if isParserCategory env catName then
throwParserCategoryAlreadyDefined catName
else
pure $ parserExtension.addEntry env $ ParserExtensionEntry.category catName leadingIdentAsSymbol
return parserExtension.addEntry env <| ParserExtension.Entry.category catName leadingIdentAsSymbol
/-
Return true if in the given category leading identifiers in parsers may be treated as atoms/symbols.
@ -398,10 +403,10 @@ def addToken (env : Environment) (tk : Token) : Except String Environment := do
-- Recall that `ParserExtension.addEntry` is pure, and assumes `addTokenConfig` does not fail.
-- So, we must run it here to handle exception.
addTokenConfig (parserExtension.getState env).tokens tk
pure $ parserExtension.addEntry env $ ParserExtensionEntry.token tk
pure $ parserExtension.addEntry env <| ParserExtension.Entry.token tk
def addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment :=
parserExtension.addEntry env $ ParserExtensionEntry.kind k
parserExtension.addEntry env <| ParserExtension.Entry.kind k
def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool :=
let kinds := (parserExtension.getState env).kinds
@ -512,14 +517,14 @@ private def ParserAttribute.add (attrName : Name) (catName : Name) (declName : N
let kinds := parser.info.collectKinds {}
kinds.forM fun kind _ => modifyEnv fun env => addSyntaxNodeKind env kind
match addParser categories catName declName leading parser prio with
| Except.ok _ => modifyEnv fun env => parserExtension.addEntry env $ ParserExtensionEntry.parser catName declName leading parser prio
| Except.ok _ => modifyEnv fun env => parserExtension.addEntry env <| ParserExtension.Entry.parser catName declName leading parser prio
| Except.error ex => throwError ex
runParserAttributeHooks catName declName /- builtin -/ false
def mkParserAttributeImpl (attrName : Name) (catName : Name) : AttributeImpl := {
name := attrName,
descr := "parser",
add := fun declName args persistent => liftM $ ParserAttribute.add attrName catName declName args persistent,
name := attrName
descr := "parser"
add := fun declName args persistent => ParserAttribute.add attrName catName declName args persistent
applicationTime := AttributeApplicationTime.afterCompilation
}

170
stage0/src/Lean/ScopedEnvExtension.lean generated Normal file
View file

@ -0,0 +1,170 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Environment
import Lean.Data.NameTrie
namespace Lean
namespace ScopedEnvExtension
inductive Entry (α : Type) where
| global : α → Entry α
| «scoped» : Name → α → Entry α
structure State (σ : Type) where
state : σ
activeScopes : NameSet := {}
structure ScopedEntries (β : Type) where
map : SMap Name (Std.PArray β) := {}
structure StateStack (α : Type) (β : Type) (σ : Type) where
stateStack : List (State σ) := {}
scopedEntries : ScopedEntries β := {}
newEntries : List (Entry α) := []
instance : Inhabited (StateStack α β σ) where
default := {}
structure Descr (α : Type) (β : Type) (σ : Type) where
name : Name
mkInitial : IO σ
ofOLeanEntry : σ → α → ImportM β
toOLeanEntry : β → α
addEntry : σ → β → σ
eraseEntry : σ → β → σ
instance [Inhabited α] : Inhabited (Descr α β σ) where
default := {
name := arbitrary
mkInitial := arbitrary
ofOLeanEntry := arbitrary
toOLeanEntry := arbitrary
addEntry := fun s _ => s
eraseEntry := fun s _ => s
}
def mkInitial (descr : Descr α β σ) : IO (StateStack α β σ) :=
return { stateStack := [ { state := (← descr.mkInitial ) } ] }
def ScopedEntries.insert (scopedEntries : ScopedEntries β) (ns : Name) (b : β) : ScopedEntries β :=
match scopedEntries.map.find? ns with
| none => { map := scopedEntries.map.insert ns <| ({} : Std.PArray β).push b }
| some bs => { map := scopedEntries.map.insert ns <| bs.push b }
def addImportedFn (descr : Descr α β σ) (as : Array (Array (Entry α))) : ImportM (StateStack α β σ) := do
let mut s ← descr.mkInitial
let mut scopedEntries : ScopedEntries β := {}
for a in as do
for e in a do
match e with
| Entry.global a =>
let b ← descr.ofOLeanEntry s a
s := descr.addEntry s b
| Entry.scoped ns a =>
let b ← descr.ofOLeanEntry s a
scopedEntries := scopedEntries.insert ns b
return { stateStack := [ { state := s } ], scopedEntries := scopedEntries }
def addEntryFn (descr : Descr α β σ) (s : StateStack α β σ) (e : Entry β) : StateStack α β σ :=
match s with
| { stateStack := stateStack, scopedEntries := scopedEntries, newEntries := newEntries } =>
match e with
| Entry.global b => {
scopedEntries := scopedEntries
newEntries := (Entry.global (descr.toOLeanEntry b)) :: newEntries
stateStack := stateStack.map fun s => { s with state := descr.addEntry s.state b }
}
| Entry.«scoped» ns b => {
scopedEntries := scopedEntries.insert ns b
newEntries := (Entry.«scoped» ns (descr.toOLeanEntry b)) :: newEntries
stateStack := stateStack.map fun s =>
if s.activeScopes.contains ns then
{ s with state := descr.addEntry s.state b }
else
s
}
def exportEntriesFn (s : StateStack α β σ) : Array (Entry α) :=
s.newEntries.toArray.reverse
end ScopedEnvExtension
open ScopedEnvExtension
structure ScopedEnvExtension (α : Type) (β : Type) (σ : Type) where
descr : Descr α β σ
ext : PersistentEnvExtension (Entry α) (Entry β) (StateStack α β σ)
instance [Inhabited α] : Inhabited (ScopedEnvExtension α β σ) where
default := {
descr := arbitrary
ext := arbitrary
}
def registerScopedEnvExtension (descr : Descr α β σ) : IO (ScopedEnvExtension α β σ) := do
let ext ← registerPersistentEnvExtension {
name := descr.name
mkInitial := mkInitial descr
addImportedFn := addImportedFn descr
addEntryFn := addEntryFn descr
exportEntriesFn := exportEntriesFn
statsFn := fun s => format "number of local entries: " ++ format s.newEntries.length
}
return { descr := descr, ext := ext }
def ScopedEnvExtension.pushScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment :=
let s := ext.ext.getState env
match s.stateStack with
| [] => env
| state :: stack => ext.ext.setState env { s with stateStack := state :: state :: stack }
def ScopedEnvExtension.popScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment :=
let s := ext.ext.getState env
match s.stateStack with
| state₁ :: state₂ :: stack => ext.ext.setState env { s with stateStack := state₂ :: stack }
| _ => env
def ScopedEnvExtension.addEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (b : β) : Environment :=
ext.ext.addEntry env (Entry.global b)
def ScopedEnvExtension.addScopedEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (namespaceName : Name) (b : β) : Environment :=
ext.ext.addEntry env (Entry.«scoped» namespaceName b)
def ScopedEnvExtension.getState [Inhabited σ] (ext : ScopedEnvExtension α β σ) (env : Environment) : σ :=
match ext.ext.getState env |>.stateStack with
| top :: _ => top.state
| _ => unreachable!
def ScopedEnvExtension.eraseEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (b : β) : Environment :=
let s := ext.ext.getState env
match s.stateStack with
| top :: stack =>
let top := { top with state := ext.descr.eraseEntry top.state b }
ext.ext.setState env { s with stateStack := top :: stack }
| _ => env
def ScopedEnvExtension.activateScoped (ext : ScopedEnvExtension α β σ) (env : Environment) (namespaceName : Name) : Environment :=
let s := ext.ext.getState env
match s.stateStack with
| top :: stack =>
if top.activeScopes.contains namespaceName then
env
else
let activeScopes := top.activeScopes.insert namespaceName
let top :=
match s.scopedEntries.map.find? namespaceName with
| none =>
{ top with activeScopes := activeScopes }
| some bs => do
let mut state := top.state
for b in bs do
state := ext.descr.addEntry state b
{ state := state, activeScopes := activeScopes }
ext.ext.setState env { s with stateStack := top :: stack }
| _ => env
end Lean

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

1076
stage0/stdlib/Init/NotationExtra.c generated
View file

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean
// Imports: Init Lean.Data Lean.Compiler Lean.Environment Lean.Modifiers Lean.ProjFns Lean.Runtime Lean.ResolveName Lean.Attributes Lean.Parser Lean.ReducibilityAttrs Lean.Elab Lean.Class Lean.LocalContext Lean.MetavarContext Lean.AuxRecursor Lean.Meta Lean.Util Lean.Eval Lean.Structure Lean.PrettyPrinter Lean.CoreM Lean.InternalExceptionId Lean.Server
// Imports: Init Lean.Data Lean.Compiler Lean.Environment Lean.Modifiers Lean.ProjFns Lean.Runtime Lean.ResolveName Lean.Attributes Lean.Parser Lean.ReducibilityAttrs Lean.Elab Lean.Class Lean.LocalContext Lean.MetavarContext Lean.AuxRecursor Lean.Meta Lean.Util Lean.Eval Lean.Structure Lean.PrettyPrinter Lean.CoreM Lean.InternalExceptionId Lean.Server Lean.ScopedEnvExtension
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -37,6 +37,7 @@ lean_object* initialize_Lean_PrettyPrinter(lean_object*);
lean_object* initialize_Lean_CoreM(lean_object*);
lean_object* initialize_Lean_InternalExceptionId(lean_object*);
lean_object* initialize_Lean_Server(lean_object*);
lean_object* initialize_Lean_ScopedEnvExtension(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean(lean_object* w) {
lean_object * res;
@ -114,6 +115,9 @@ lean_dec_ref(res);
res = initialize_Lean_Server(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_ScopedEnvExtension(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

10
stage0/stdlib/Lean/Data.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Data
// Imports: Init Lean.Data.Format Lean.Data.Json Lean.Data.JsonRpc Lean.Data.KVMap Lean.Data.LBool Lean.Data.LOption Lean.Data.Lsp Lean.Data.Name Lean.Data.Occurrences Lean.Data.OpenDecl Lean.Data.Options Lean.Data.Position Lean.Data.SMap Lean.Data.Trie
// Imports: Init Lean.Data.Format Lean.Data.Json Lean.Data.JsonRpc Lean.Data.KVMap Lean.Data.LBool Lean.Data.LOption Lean.Data.Lsp Lean.Data.Name Lean.Data.Occurrences Lean.Data.OpenDecl Lean.Data.Options Lean.Data.Position Lean.Data.SMap Lean.Data.Trie Lean.Data.PrefixTree Lean.Data.NameTrie
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -28,6 +28,8 @@ lean_object* initialize_Lean_Data_Options(lean_object*);
lean_object* initialize_Lean_Data_Position(lean_object*);
lean_object* initialize_Lean_Data_SMap(lean_object*);
lean_object* initialize_Lean_Data_Trie(lean_object*);
lean_object* initialize_Lean_Data_PrefixTree(lean_object*);
lean_object* initialize_Lean_Data_NameTrie(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Data(lean_object* w) {
lean_object * res;
@ -78,6 +80,12 @@ lean_dec_ref(res);
res = initialize_Lean_Data_Trie(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Data_PrefixTree(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Data_NameTrie(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

820
stage0/stdlib/Lean/Data/NameTrie.c generated Normal file
View file

@ -0,0 +1,820 @@
// Lean compiler output
// Module: Lean.Data.NameTrie
// Imports: Init Lean.Data.PrefixTree
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldMatchingM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PrefixTree_empty___closed__1;
lean_object* l_Lean_instInhabitedNameTrie(lean_object*);
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey_loop_match__1(lean_object*);
lean_object* l_Lean_PrefixTreeNode_find_x3f_loop___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NamePart_lt_match__1(lean_object*);
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forM___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_find_x3f(lean_object*);
lean_object* l_Lean_NameTrie_forM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrefixTreeNode_insert_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_NamePart_lt(lean_object*, lean_object*);
lean_object* l_ReaderT_instMonadReaderT___rarg___lambda__7___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_foldMatchingM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_insert(lean_object*);
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldM___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forMatchingM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey_loop(lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_empty(lean_object*);
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey___boxed(lean_object*);
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey(lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* l_Lean_NameTrie_foldMatchingM(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_forMatchingM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_foldM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_forM(lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_foldM___rarg___closed__1;
lean_object* l_Lean_instEmptyCollectionNameTrie(lean_object*);
lean_object* l_Lean_NamePart_lt_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldMatchingM___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_foldM(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_forMatchingM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_foldMatchingM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_instToStringNamePart(lean_object*);
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_fold___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NamePart_lt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_instToStringNamePart_match__1(lean_object*);
lean_object* l_Lean_NameTrie_insert___rarg___closed__1;
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey_loop___boxed(lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_insert___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_find_x3f___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_find_x3f___rarg(lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_forMatchingM(lean_object*, lean_object*);
lean_object* l_Lean_NameTrie_insert___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey_loop_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forMatchingM___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_instToStringNamePart_match__1___rarg(lean_object*, lean_object*, lean_object*);
uint8_t lean_string_dec_lt(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_instToStringNamePart_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_4; lean_object* x_5;
lean_dec(x_3);
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_2);
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_1(x_3, x_6);
return x_7;
}
}
}
lean_object* l_Lean_instToStringNamePart_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_instToStringNamePart_match__1___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Lean_instToStringNamePart(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
lean_dec(x_1);
return x_2;
}
else
{
lean_object* x_3; lean_object* x_4;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l_Nat_repr(x_3);
return x_4;
}
}
}
lean_object* l_Lean_NamePart_lt_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_dec(x_5);
lean_dec(x_4);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_dec(x_6);
x_7 = lean_ctor_get(x_1, 0);
lean_inc(x_7);
lean_dec(x_1);
x_8 = lean_ctor_get(x_2, 0);
lean_inc(x_8);
lean_dec(x_2);
x_9 = lean_apply_2(x_3, x_7, x_8);
return x_9;
}
else
{
lean_object* x_10;
lean_dec(x_3);
x_10 = lean_apply_2(x_6, x_1, x_2);
return x_10;
}
}
else
{
lean_dec(x_6);
lean_dec(x_3);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_dec(x_4);
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
lean_dec(x_1);
x_12 = lean_ctor_get(x_2, 0);
lean_inc(x_12);
lean_dec(x_2);
x_13 = lean_apply_2(x_5, x_11, x_12);
return x_13;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16;
lean_dec(x_5);
x_14 = lean_ctor_get(x_1, 0);
lean_inc(x_14);
lean_dec(x_1);
x_15 = lean_ctor_get(x_2, 0);
lean_inc(x_15);
lean_dec(x_2);
x_16 = lean_apply_2(x_4, x_14, x_15);
return x_16;
}
}
}
}
lean_object* l_Lean_NamePart_lt_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_NamePart_lt_match__1___rarg), 6, 0);
return x_2;
}
}
uint8_t l_Lean_NamePart_lt(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_2, 0);
x_5 = lean_string_dec_lt(x_3, x_4);
return x_5;
}
else
{
uint8_t x_6;
x_6 = 0;
return x_6;
}
}
else
{
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_7;
x_7 = 1;
return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_8 = lean_ctor_get(x_1, 0);
x_9 = lean_ctor_get(x_2, 0);
x_10 = lean_nat_dec_lt(x_8, x_9);
return x_10;
}
}
}
}
lean_object* l_Lean_NamePart_lt___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_NamePart_lt(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey_loop_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 0:
{
lean_object* x_6;
lean_dec(x_4);
lean_dec(x_3);
x_6 = lean_apply_1(x_5, x_2);
return x_6;
}
case 1:
{
lean_object* x_7; lean_object* x_8; size_t x_9; lean_object* x_10; lean_object* x_11;
lean_dec(x_5);
lean_dec(x_4);
x_7 = lean_ctor_get(x_1, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_1, 1);
lean_inc(x_8);
x_9 = lean_ctor_get_usize(x_1, 2);
lean_dec(x_1);
x_10 = lean_box_usize(x_9);
x_11 = lean_apply_4(x_3, x_7, x_8, x_10, x_2);
return x_11;
}
default:
{
lean_object* x_12; lean_object* x_13; size_t x_14; lean_object* x_15; lean_object* x_16;
lean_dec(x_5);
lean_dec(x_3);
x_12 = lean_ctor_get(x_1, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_1, 1);
lean_inc(x_13);
x_14 = lean_ctor_get_usize(x_1, 2);
lean_dec(x_1);
x_15 = lean_box_usize(x_14);
x_16 = lean_apply_4(x_4, x_12, x_13, x_15, x_2);
return x_16;
}
}
}
}
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey_loop_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_NameTrie_0__Lean_toKey_loop_match__1___rarg), 5, 0);
return x_2;
}
}
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey_loop(lean_object* x_1, lean_object* x_2) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 0:
{
return x_2;
}
case 1:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
x_5 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_5, 0, x_4);
x_6 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_2);
x_1 = x_3;
x_2 = x_6;
goto _start;
}
default:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_8 = lean_ctor_get(x_1, 0);
x_9 = lean_ctor_get(x_1, 1);
lean_inc(x_9);
x_10 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_2);
x_1 = x_8;
x_2 = x_11;
goto _start;
}
}
}
}
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey_loop___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l___private_Lean_Data_NameTrie_0__Lean_toKey_loop(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_box(0);
x_3 = l___private_Lean_Data_NameTrie_0__Lean_toKey_loop(x_1, x_2);
return x_3;
}
}
lean_object* l___private_Lean_Data_NameTrie_0__Lean_toKey___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_NameTrie_0__Lean_toKey(x_1);
lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_NameTrie_insert___rarg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_NamePart_lt___boxed), 2, 0);
return x_1;
}
}
lean_object* l_Lean_NameTrie_insert___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = l___private_Lean_Data_NameTrie_0__Lean_toKey(x_2);
x_5 = l_Lean_NameTrie_insert___rarg___closed__1;
x_6 = l_Lean_PrefixTreeNode_insert_loop___rarg(x_5, x_3, x_1, x_4);
return x_6;
}
}
lean_object* l_Lean_NameTrie_insert(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_NameTrie_insert___rarg___boxed), 3, 0);
return x_2;
}
}
lean_object* l_Lean_NameTrie_insert___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_NameTrie_insert___rarg(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
}
lean_object* l_Lean_NameTrie_empty(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_PrefixTree_empty___closed__1;
return x_2;
}
}
lean_object* l_Lean_instInhabitedNameTrie(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_PrefixTree_empty___closed__1;
return x_2;
}
}
lean_object* l_Lean_instEmptyCollectionNameTrie(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_PrefixTree_empty___closed__1;
return x_2;
}
}
lean_object* l_Lean_NameTrie_find_x3f___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = l___private_Lean_Data_NameTrie_0__Lean_toKey(x_2);
x_4 = l_Lean_NameTrie_insert___rarg___closed__1;
x_5 = l_Lean_PrefixTreeNode_find_x3f_loop___rarg(x_4, x_1, x_3);
return x_5;
}
}
lean_object* l_Lean_NameTrie_find_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_NameTrie_find_x3f___rarg___boxed), 2, 0);
return x_2;
}
}
lean_object* l_Lean_NameTrie_find_x3f___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_NameTrie_find_x3f___rarg(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldMatchingM___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_8;
lean_dec(x_3);
lean_dec(x_2);
x_8 = l_Lean_PrefixTreeNode_foldMatchingM_fold___rarg(x_1, x_4, x_6, x_7);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_5, 1);
lean_inc(x_10);
lean_dec(x_5);
x_11 = lean_ctor_get(x_6, 1);
lean_inc(x_11);
lean_dec(x_6);
lean_inc(x_2);
x_12 = l_Std_RBNode_find___rarg(x_2, lean_box(0), x_11, x_9);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_10);
lean_dec(x_7);
lean_dec(x_4);
lean_dec(x_2);
x_13 = lean_ctor_get(x_1, 0);
lean_inc(x_13);
lean_dec(x_1);
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_apply_2(x_14, lean_box(0), x_3);
return x_15;
}
else
{
lean_object* x_16;
x_16 = lean_ctor_get(x_12, 0);
lean_inc(x_16);
lean_dec(x_12);
x_5 = x_10;
x_6 = x_16;
goto _start;
}
}
}
}
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldMatchingM___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldMatchingM___spec__1___rarg), 7, 0);
return x_4;
}
}
lean_object* l_Lean_NameTrie_foldMatchingM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l___private_Lean_Data_NameTrie_0__Lean_toKey(x_3);
x_7 = l_Lean_NameTrie_insert___rarg___closed__1;
lean_inc(x_4);
x_8 = l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldMatchingM___spec__1___rarg(x_1, x_7, x_4, x_5, x_6, x_2, x_4);
return x_8;
}
}
lean_object* l_Lean_NameTrie_foldMatchingM(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Lean_NameTrie_foldMatchingM___rarg___boxed), 5, 0);
return x_4;
}
}
lean_object* l_Lean_NameTrie_foldMatchingM___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l_Lean_NameTrie_foldMatchingM___rarg(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_3);
return x_6;
}
}
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldM___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_8;
lean_dec(x_3);
lean_dec(x_2);
x_8 = l_Lean_PrefixTreeNode_foldMatchingM_fold___rarg(x_1, x_4, x_6, x_7);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_5, 1);
lean_inc(x_10);
lean_dec(x_5);
x_11 = lean_ctor_get(x_6, 1);
lean_inc(x_11);
lean_dec(x_6);
lean_inc(x_2);
x_12 = l_Std_RBNode_find___rarg(x_2, lean_box(0), x_11, x_9);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_10);
lean_dec(x_7);
lean_dec(x_4);
lean_dec(x_2);
x_13 = lean_ctor_get(x_1, 0);
lean_inc(x_13);
lean_dec(x_1);
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_apply_2(x_14, lean_box(0), x_3);
return x_15;
}
else
{
lean_object* x_16;
x_16 = lean_ctor_get(x_12, 0);
lean_inc(x_16);
lean_dec(x_12);
x_5 = x_10;
x_6 = x_16;
goto _start;
}
}
}
}
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldM___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldM___spec__1___rarg), 7, 0);
return x_4;
}
}
static lean_object* _init_l_Lean_NameTrie_foldM___rarg___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = l___private_Lean_Data_NameTrie_0__Lean_toKey(x_1);
return x_2;
}
}
lean_object* l_Lean_NameTrie_foldM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = l_Lean_NameTrie_insert___rarg___closed__1;
x_6 = l_Lean_NameTrie_foldM___rarg___closed__1;
lean_inc(x_3);
x_7 = l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_foldM___spec__1___rarg(x_1, x_5, x_3, x_4, x_6, x_2, x_3);
return x_7;
}
}
lean_object* l_Lean_NameTrie_foldM(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Lean_NameTrie_foldM___rarg), 4, 0);
return x_4;
}
}
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forMatchingM___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_8;
lean_dec(x_3);
lean_dec(x_2);
x_8 = l_Lean_PrefixTreeNode_foldMatchingM_fold___rarg(x_1, x_4, x_6, x_7);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_5, 1);
lean_inc(x_10);
lean_dec(x_5);
x_11 = lean_ctor_get(x_6, 1);
lean_inc(x_11);
lean_dec(x_6);
lean_inc(x_2);
x_12 = l_Std_RBNode_find___rarg(x_2, lean_box(0), x_11, x_9);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_10);
lean_dec(x_7);
lean_dec(x_4);
lean_dec(x_2);
x_13 = lean_ctor_get(x_1, 0);
lean_inc(x_13);
lean_dec(x_1);
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_apply_2(x_14, lean_box(0), x_3);
return x_15;
}
else
{
lean_object* x_16;
x_16 = lean_ctor_get(x_12, 0);
lean_inc(x_16);
lean_dec(x_12);
x_5 = x_10;
x_6 = x_16;
goto _start;
}
}
}
}
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forMatchingM___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forMatchingM___spec__1___rarg), 7, 0);
return x_3;
}
}
lean_object* l_Lean_NameTrie_forMatchingM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_5 = l___private_Lean_Data_NameTrie_0__Lean_toKey(x_3);
x_6 = lean_alloc_closure((void*)(l_ReaderT_instMonadReaderT___rarg___lambda__7___boxed), 3, 1);
lean_closure_set(x_6, 0, x_4);
x_7 = l_Lean_NameTrie_insert___rarg___closed__1;
x_8 = lean_box(0);
x_9 = l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forMatchingM___spec__1___rarg(x_1, x_7, x_8, x_6, x_5, x_2, x_8);
return x_9;
}
}
lean_object* l_Lean_NameTrie_forMatchingM(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_NameTrie_forMatchingM___rarg___boxed), 4, 0);
return x_3;
}
}
lean_object* l_Lean_NameTrie_forMatchingM___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_NameTrie_forMatchingM___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forM___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_8;
lean_dec(x_3);
lean_dec(x_2);
x_8 = l_Lean_PrefixTreeNode_foldMatchingM_fold___rarg(x_1, x_4, x_6, x_7);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_5, 1);
lean_inc(x_10);
lean_dec(x_5);
x_11 = lean_ctor_get(x_6, 1);
lean_inc(x_11);
lean_dec(x_6);
lean_inc(x_2);
x_12 = l_Std_RBNode_find___rarg(x_2, lean_box(0), x_11, x_9);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_10);
lean_dec(x_7);
lean_dec(x_4);
lean_dec(x_2);
x_13 = lean_ctor_get(x_1, 0);
lean_inc(x_13);
lean_dec(x_1);
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_apply_2(x_14, lean_box(0), x_3);
return x_15;
}
else
{
lean_object* x_16;
x_16 = lean_ctor_get(x_12, 0);
lean_inc(x_16);
lean_dec(x_12);
x_5 = x_10;
x_6 = x_16;
goto _start;
}
}
}
}
lean_object* l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forM___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forM___spec__1___rarg), 7, 0);
return x_3;
}
}
lean_object* l_Lean_NameTrie_forM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_4 = lean_alloc_closure((void*)(l_ReaderT_instMonadReaderT___rarg___lambda__7___boxed), 3, 1);
lean_closure_set(x_4, 0, x_3);
x_5 = l_Lean_NameTrie_insert___rarg___closed__1;
x_6 = lean_box(0);
x_7 = l_Lean_NameTrie_foldM___rarg___closed__1;
x_8 = l_Lean_PrefixTreeNode_foldMatchingM_find___at_Lean_NameTrie_forM___spec__1___rarg(x_1, x_5, x_6, x_4, x_7, x_2, x_6);
return x_8;
}
}
lean_object* l_Lean_NameTrie_forM(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_NameTrie_forM___rarg), 3, 0);
return x_3;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Data_PrefixTree(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Data_NameTrie(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Data_PrefixTree(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_NameTrie_insert___rarg___closed__1 = _init_l_Lean_NameTrie_insert___rarg___closed__1();
lean_mark_persistent(l_Lean_NameTrie_insert___rarg___closed__1);
l_Lean_NameTrie_foldM___rarg___closed__1 = _init_l_Lean_NameTrie_foldM___rarg___closed__1();
lean_mark_persistent(l_Lean_NameTrie_foldM___rarg___closed__1);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

1174
stage0/stdlib/Lean/Data/PrefixTree.c generated Normal file
View file

File diff suppressed because it is too large Load diff

8
stage0/stdlib/Lean/Elab/Binders.c generated
View file

@ -60,6 +60,7 @@ lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___at_Lean_Elab_
lean_object* l_Lean_Syntax_mkSep(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_throwUnsupportedSyntax___rarg___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_elabLetStarDecl___closed__1;
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2865____closed__10;
lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__3(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_expandWhereDecls___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -112,7 +113,6 @@ lean_object* l_Lean_addDecl___at_Lean_Elab_Term_declareTacticSyntax___spec__1___
extern lean_object* l_myMacro____x40_Init_Notation___hyg_11163____closed__11;
lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__15;
extern lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__15;
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2853____closed__10;
lean_object* l_Lean_Meta_mkLambdaFVarsImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandFunBinders_loop_match__2___rarg(lean_object*, lean_object*, lean_object*);
@ -17590,7 +17590,7 @@ x_69 = l_Lean_nullKind___closed__2;
x_70 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_70, 0, x_69);
lean_ctor_set(x_70, 1, x_68);
x_71 = l_myMacro____x40_Init_NotationExtra___hyg_2853____closed__10;
x_71 = l_myMacro____x40_Init_NotationExtra___hyg_2865____closed__10;
x_72 = lean_array_push(x_71, x_70);
x_73 = l_Lean_Parser_Tactic_intro___closed__4;
x_74 = lean_alloc_ctor(1, 2, 0);
@ -17625,7 +17625,7 @@ x_87 = l_Lean_nullKind___closed__2;
x_88 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_88, 0, x_87);
lean_ctor_set(x_88, 1, x_86);
x_89 = l_myMacro____x40_Init_NotationExtra___hyg_2853____closed__10;
x_89 = l_myMacro____x40_Init_NotationExtra___hyg_2865____closed__10;
x_90 = lean_array_push(x_89, x_88);
x_91 = l_Lean_Parser_Tactic_intro___closed__4;
x_92 = lean_alloc_ctor(1, 2, 0);
@ -17758,7 +17758,7 @@ x_143 = l_Lean_nullKind___closed__2;
x_144 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_144, 0, x_143);
lean_ctor_set(x_144, 1, x_142);
x_145 = l_myMacro____x40_Init_NotationExtra___hyg_2853____closed__10;
x_145 = l_myMacro____x40_Init_NotationExtra___hyg_2865____closed__10;
x_146 = lean_array_push(x_145, x_144);
x_147 = l_Lean_Parser_Tactic_intro___closed__4;
x_148 = lean_alloc_ctor(1, 2, 0);

6
stage0/stdlib/Lean/Elab/Match.c generated
View file

@ -707,6 +707,7 @@ uint8_t l_Lean_Syntax_isNone(lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isAuxDiscrName___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_elabMatch_match__19___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__8;
lean_object* l_Lean_expandMacros(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__7___rarg(lean_object*);
lean_object* l_Lean_Expr_arrayLit_x3f(lean_object*);
@ -784,7 +785,6 @@ lean_object* l_Lean_Elab_Term_CollectPatternVars_processCtorApp___boxed(lean_obj
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabAtomicDiscr___closed__3;
extern lean_object* l_Lean_Meta_CheckAssignment_checkFVar___closed__2;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabPatterns_match__3(lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__8;
lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_withPatternVars_loop_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
uint8_t l_List_isEmpty___rarg(lean_object*);
@ -8796,7 +8796,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_instToExprName___closed__1;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__8;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -8806,7 +8806,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Init_Meta_0__Lean_quoteName___closed__2;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__8;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

16
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

@ -93,13 +93,13 @@ lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__14;
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l_Lean_Elab_Command_mkSimpleDelab_go___closed__3;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__28;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3887____closed__1;
lean_object* lean_io_error_to_string(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabDeclareSyntaxCat___closed__1;
lean_object* l_Lean_Elab_Term_toParserDescrAux___closed__12;
lean_object* l_Lean_Elab_Command_mkSimpleDelab_go___closed__15;
lean_object* l_Array_filterSepElemsM___at_Lean_Elab_Command_elabNoKindMacroRulesAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3879____closed__1;
lean_object* l_Lean_Elab_Term_toParserDescrAux___lambda__2___closed__4;
lean_object* l_Lean_Elab_Command_expandMixfix___closed__25;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__30;
@ -126,6 +126,7 @@ extern lean_object* l_Lean_Elab_Command_commandElabAttribute;
lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_getCatSuffix_match__1(lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l_Lean_Elab_Command_mkSimpleDelab_go___closed__14;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3879____closed__2;
lean_object* l_Lean_Elab_Command_mkSimpleDelab_go___closed__28;
lean_object* l___regBuiltin_Lean_Elab_Command_elabMacroRules(lean_object*);
lean_object* l_Lean_Elab_Command_expandElab___closed__32;
@ -271,7 +272,6 @@ lean_object* l_Lean_Elab_Command_expandMixfix___closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_54____closed__5;
lean_object* l_Lean_Elab_Command_expandElab___closed__3;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_expandMacro___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
lean_object* l_Lean_Elab_Term_expandOptPrecedence___boxed(lean_object*);
lean_object* l_Lean_Elab_Command_expandElab___closed__15;
lean_object* l___regBuiltin_Lean_Elab_Command_elabElab___closed__2;
@ -279,6 +279,7 @@ extern lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_
lean_object* l_Lean_Elab_Command_mkSimpleDelab_go___closed__16;
lean_object* l_Lean_Elab_Command_mkSimpleDelab_go___closed__29;
lean_object* l_Lean_Elab_Term_expandOptPrecedence___closed__1;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
lean_object* l___regBuiltin_Lean_Elab_Command_elabSyntaxAbbrev___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Command_expandNotation(lean_object*);
lean_object* l_Lean_Elab_Command_expandMixfix___closed__23;
@ -507,7 +508,6 @@ lean_object* l_Lean_Elab_Command_mkSimpleDelab_go___closed__8;
lean_object* l_Lean_Elab_Command_expandMixfix___closed__11;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Syntax_0__Lean_Elab_Command_antiquote___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_toParserDescrAux___closed__25;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3887____closed__2;
lean_object* l_Lean_Elab_Command_mkSimpleDelab_go___closed__17;
lean_object* l_Lean_Elab_Term_toParserDescrAux___closed__50;
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__11;
@ -9619,7 +9619,7 @@ static lean_object* _init_l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_decl
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3887____closed__1;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3879____closed__1;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
@ -9628,7 +9628,7 @@ static lean_object* _init_l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_decl
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3887____closed__1;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3879____closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__3;
x_4 = lean_alloc_ctor(0, 3, 0);
@ -10031,7 +10031,7 @@ lean_inc(x_16);
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec(x_15);
x_18 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3887____closed__2;
x_18 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3879____closed__2;
lean_inc(x_13);
lean_inc(x_16);
x_19 = l_Lean_addMacroScope(x_16, x_18, x_13);
@ -25958,7 +25958,7 @@ x_60 = lean_name_eq(x_22, x_59);
if (x_60 == 0)
{
lean_object* x_61; uint8_t x_62;
x_61 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_61 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_62 = lean_name_eq(x_22, x_61);
if (x_62 == 0)
{
@ -27109,7 +27109,7 @@ x_729 = lean_name_eq(x_22, x_728);
if (x_729 == 0)
{
lean_object* x_730; uint8_t x_731;
x_730 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_730 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_731 = lean_name_eq(x_22, x_730);
if (x_731 == 0)
{

6
stage0/stdlib/Lean/Elab/Tactic/Basic.c generated
View file

@ -64,6 +64,7 @@ extern lean_object* l_Lean_Elab_throwUnsupportedSyntax___rarg___closed__1;
lean_object* l_Lean_Elab_Tactic_evalSkip(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_getCurrMacroScope___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_focus___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2865____closed__10;
lean_object* l_Lean_Elab_Tactic_reportUnsolvedGoals(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalClear(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_logTrace___at_Lean_Elab_Tactic_evalTactic___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -120,7 +121,6 @@ lean_object* l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_getIntrosSiz
lean_object* l_Lean_Elab_Tactic_liftMetaTacticAux_match__2___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_ensureHasType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalIntro(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2853____closed__10;
lean_object* l_Lean_Elab_Tactic_evalCase___closed__3;
lean_object* l_Lean_Elab_Tactic_evalAssumption___rarg___lambda__1___closed__1;
lean_object* l_Lean_Meta_getMVars___at_Lean_Elab_Tactic_ensureHasNoMVars___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -10717,7 +10717,7 @@ x_34 = l_Lean_nullKind___closed__2;
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_34);
lean_ctor_set(x_35, 1, x_33);
x_36 = l_myMacro____x40_Init_NotationExtra___hyg_2853____closed__10;
x_36 = l_myMacro____x40_Init_NotationExtra___hyg_2865____closed__10;
x_37 = lean_array_push(x_36, x_35);
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_11);
@ -10907,7 +10907,7 @@ x_96 = lean_array_push(x_95, x_94);
x_97 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_97, 0, x_71);
lean_ctor_set(x_97, 1, x_96);
x_98 = l_myMacro____x40_Init_NotationExtra___hyg_2853____closed__10;
x_98 = l_myMacro____x40_Init_NotationExtra___hyg_2865____closed__10;
lean_inc(x_97);
x_99 = lean_array_push(x_98, x_97);
x_100 = lean_alloc_ctor(1, 2, 0);

4
stage0/stdlib/Lean/Meta/Tactic/Constructor.c generated
View file

@ -46,11 +46,11 @@ lean_object* l_Lean_Meta_existsIntro___lambda__1___boxed(lean_object*, lean_obje
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
lean_object* l_Lean_Meta_existsIntro___lambda__1___closed__1;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
extern lean_object* l___kind_term____x40_Init_NotationExtra___hyg_2209____closed__2;
lean_object* l_Lean_Meta_existsIntro___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_existsIntro_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_existsIntro___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_existsIntro___lambda__1___closed__2;
extern lean_object* l___kind_term____x40_Init_NotationExtra___hyg_2221____closed__2;
lean_object* l_Array_ofSubarray___rarg(lean_object*);
lean_object* l_Lean_Meta_existsIntro_match__2(lean_object*);
lean_object* l_Lean_Meta_existsIntro___lambda__1___closed__3;
@ -875,7 +875,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___kind_term____x40_Init_NotationExtra___hyg_2209____closed__2;
x_2 = l___kind_term____x40_Init_NotationExtra___hyg_2221____closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

62
stage0/stdlib/Lean/Parser/Command.c generated
View file

@ -695,7 +695,6 @@ lean_object* l_Lean_Parser_Command_structCtor___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_openHiding___closed__5;
lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_printAxioms_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__23;
lean_object* l_Lean_Parser_Command_partial_formatter___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Command_end_parenthesizer___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Command_variables_parenthesizer___closed__1;
@ -828,7 +827,6 @@ lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_declValSimple___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_axiom_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_mutual___elambda__1___closed__12;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
lean_object* l_Lean_Parser_Command_structure_formatter___closed__21;
lean_object* l_Lean_Parser_Command_structSimpleBinder_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Command_inferMod_parenthesizer___closed__2;
@ -863,6 +861,7 @@ lean_object* l_Lean_Parser_Command_universes___elambda__1___closed__10;
lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__7;
lean_object* l___regBuiltin_Lean_Parser_Command_synth_formatter(lean_object*);
extern lean_object* l_Lean_Parser_Term_binderDefault;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_visibility_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Command_in_parenthesizer(lean_object*);
@ -1100,6 +1099,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_sepBy1_parenthesizer(lean_object
lean_object* l_Lean_Parser_Command_classTk___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_variable___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Command_check_formatter___closed__1;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__23;
extern lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed___closed__5;
lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__18;
lean_object* l_Lean_Parser_Command_namespace___elambda__1(lean_object*, lean_object*);
@ -2698,7 +2698,7 @@ static lean_object* _init_l_Lean_Parser_Term_quot___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_categoryParser___elambda__1), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -2815,7 +2815,7 @@ static lean_object* _init_l_Lean_Parser_Term_quot___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_Parser_categoryParser(x_1, x_2);
return x_3;
@ -9606,7 +9606,7 @@ static lean_object* _init_l_Lean_Parser_Command_structFields___elambda__1___clos
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__23;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__23;
x_2 = l_Lean_Parser_Command_structFields___elambda__1___closed__7;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -11401,7 +11401,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_declaration(lean_object* x
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1161____closed__4;
x_4 = 1;
x_5 = l_Lean_Parser_Command_declaration;
@ -17897,7 +17897,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_section(lean_object* x_1)
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_section___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_section;
@ -18274,7 +18274,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_namespace(lean_object* x_1
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_namespace___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_namespace;
@ -18629,7 +18629,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_end(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_end;
@ -18968,7 +18968,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_variable(lean_object* x_1)
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_variable___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_variable;
@ -19329,7 +19329,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_variables(lean_object* x_1
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_variables___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_variables;
@ -19706,7 +19706,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_universe(lean_object* x_1)
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_universe___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_universe;
@ -20051,7 +20051,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_universes(lean_object* x_1
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_universes___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_universes;
@ -20408,7 +20408,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_check(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_check___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_check;
@ -20753,7 +20753,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_check__failure(lean_object
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_check__failure___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_check__failure;
@ -21098,7 +21098,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_eval(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_eval___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_eval;
@ -21443,7 +21443,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_synth(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_synth___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_synth;
@ -21764,7 +21764,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_exit(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_exit___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_exit;
@ -22121,7 +22121,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_print(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_print___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_print;
@ -22525,7 +22525,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_printAxioms(lean_object* x
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_printAxioms___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_printAxioms;
@ -22906,7 +22906,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_resolve__name(lean_object*
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_resolve__name___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_resolve__name;
@ -23219,7 +23219,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_init__quot(lean_object* x_
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_init__quot___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_init__quot;
@ -23676,7 +23676,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_set__option(lean_object* x
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_set__option;
@ -24304,7 +24304,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_attribute(lean_object* x_1
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_attribute___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_attribute;
@ -24843,7 +24843,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_export(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_export___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_export;
@ -26391,7 +26391,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_open(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_open___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_open;
@ -27638,7 +27638,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_mutual(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_mutual___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_mutual;
@ -28194,7 +28194,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_initialize(lean_object* x_
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_initialize___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_initialize;
@ -28661,7 +28661,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_builtin__initialize(lean_o
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_builtin__initialize___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_builtin__initialize;
@ -28868,7 +28868,7 @@ lean_inc(x_11);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_12 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_12 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_13 = lean_unsigned_to_nat(0u);
x_14 = l_Lean_Parser_categoryParser___elambda__1(x_12, x_13, x_1, x_10);
x_15 = l_Lean_Parser_Command_in___elambda__1___closed__2;
@ -28959,7 +28959,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_in(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_in___elambda__1___closed__2;
x_4 = 0;
x_5 = l_Lean_Parser_Command_in;

4
stage0/stdlib/Lean/Parser/Do.c generated
View file

@ -19,7 +19,6 @@ lean_object* l_Lean_Parser_Term_doIdDecl_parenthesizer___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Term_doBreak_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_doExpr___closed__1;
extern lean_object* l_Lean_Parser_Term_tupleTail_parenthesizer___closed__2;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__19;
lean_object* l_Lean_Parser_Term_termReturn___closed__1;
lean_object* l_Lean_Parser_Term_liftMethod_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doSeqBracketed_formatter___closed__2;
@ -255,6 +254,7 @@ lean_object* l_Lean_Parser_Term_termReturn___elambda__1___closed__5;
lean_object* l___regBuiltinParser_Lean_Parser_Term_do(lean_object*);
lean_object* l_Lean_Parser_Term_termUnless___closed__5;
lean_object* l_Lean_Parser_Term_doElem_quot___elambda__1___closed__4;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__19;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_withoutPosition_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_termUnless___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_doTry___closed__8;
@ -4997,7 +4997,7 @@ static lean_object* _init_l_Lean_Parser_Term_doPatDecl___elambda__1___closed__11
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__19;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__19;
x_2 = l_Lean_Parser_Term_doPatDecl___elambda__1___closed__10;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);

3285
stage0/stdlib/Lean/Parser/Extension.c generated
View file

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean/Parser/Extra.c generated
View file

@ -133,13 +133,13 @@ extern lean_object* l_Lean_Parser_Tactic_letrec___closed__4;
lean_object* l_Lean_Parser_registerAliasCore___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_587____closed__41;
lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_197____closed__36;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_587____closed__46;
lean_object* l_Lean_ppIndent_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_setExpected_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_termParser_formatter___boxed(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_587____closed__23;
lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_197____closed__19;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_587____closed__34;
lean_object* l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__2;
extern lean_object* l___kind_term____x40_Init_Notation___hyg_19____closed__1;
@ -474,7 +474,7 @@ lean_object* l_Lean_Parser_commandParser_formatter___rarg(lean_object* x_1, lean
_start:
{
lean_object* x_6; lean_object* x_7;
x_6 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_6 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_7 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter(x_6, x_1, x_2, x_3, x_4, x_5);
return x_7;
}
@ -500,7 +500,7 @@ lean_object* l_Lean_Parser_commandParser_parenthesizer(lean_object* x_1, lean_ob
_start:
{
lean_object* x_7; lean_object* x_8;
x_7 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_7 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_categoryParser_parenthesizer(x_7, x_1, x_2, x_3, x_4, x_5, x_6);
return x_8;
}

26
stage0/stdlib/Lean/Parser/Syntax.c generated
View file

@ -405,7 +405,6 @@ lean_object* l_Lean_Parser_Syntax_nonReserved_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_infix___closed__4;
lean_object* l_Lean_Parser_Syntax_paren_formatter___closed__1;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
lean_object* l_Lean_Parser_Command_elabTail___closed__8;
lean_object* l_Lean_Parser_Command_prefix___closed__4;
lean_object* l_Lean_Parser_Syntax_cat_formatter___closed__3;
@ -428,6 +427,7 @@ lean_object* l___regBuiltin_Lean_Parser_Term_stx_quot_formatter___closed__1;
lean_object* l_Lean_Parser_Command_macroTailCommand_formatter___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Command_syntax_formatter___closed__1;
lean_object* l_Lean_Parser_precedence_formatter___closed__2;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
lean_object* l___regBuiltin_Lean_Parser_Syntax_atom_formatter(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_withAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_elab___elambda__1___closed__3;
@ -1290,7 +1290,6 @@ lean_object* l_Lean_Parser_maxSymbol___closed__4;
lean_object* l_Lean_Parser_Command_elabTail___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Syntax_cat_formatter___closed__1;
lean_object* l_Lean_Parser_Command_mixfixKind___closed__5;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__4;
lean_object* l_Lean_Parser_Command_infix_formatter___closed__2;
lean_object* l_Lean_Parser_Syntax_atom___closed__5;
lean_object* l_Lean_Parser_Command_macro___closed__4;
@ -1336,6 +1335,7 @@ lean_object* l_Lean_Parser_precedence___closed__4;
lean_object* l_Lean_Parser_Syntax_cat_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_prefix_formatter___closed__2;
lean_object* l_Lean_Parser_Command_parserPrio___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__4;
lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_macroTailTactic___closed__7;
lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__2;
@ -3012,7 +3012,7 @@ static lean_object* _init_l_Lean_Parser_Syntax_unary___elambda__1___closed__3()
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__4;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__4;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_checkNoWsBefore___elambda__1___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -6143,7 +6143,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_mixfix(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_mixfix___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_mixfix;
@ -7752,7 +7752,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_notation(lean_object* x_1)
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_notation___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_notation;
@ -8433,7 +8433,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_macro__rules(lean_object*
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_macro__rules___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_macro__rules;
@ -9580,7 +9580,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_syntax(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_syntax___elambda__1___closed__1;
x_4 = 1;
x_5 = l_Lean_Parser_Command_syntax;
@ -10483,7 +10483,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_syntaxAbbrev(lean_object*
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_syntaxAbbrev___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_syntaxAbbrev;
@ -10878,7 +10878,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_syntaxCat(lean_object* x_1
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_syntaxCat;
@ -11527,7 +11527,7 @@ static lean_object* _init_l_Lean_Parser_Command_macroTailCommand___elambda__1___
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_identEqFn), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -12283,7 +12283,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_macro(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_macro___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_macro;
@ -13673,7 +13673,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_elab__rules(lean_object* x
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_elab__rules___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_elab__rules;
@ -14457,7 +14457,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Command_elab(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_3 = l_Lean_Parser_Command_elab___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_elab;

18
stage0/stdlib/Lean/Parser/Term.c generated
View file

@ -31,7 +31,6 @@ lean_object* l_Lean_Parser_Tactic_seq1___closed__3;
lean_object* l_Lean_Parser_Term_matchAlt___closed__5;
lean_object* l_Lean_Parser_Term_instBinder_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__5;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__19;
lean_object* l_Lean_Parser_Term_binderTactic_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_matchAlts_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Level_quot___closed__3;
@ -114,7 +113,6 @@ extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_587____c
lean_object* l_Lean_Parser_Term_fromTerm___closed__3;
lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_macroDollarArg___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__11;
lean_object* l___regBuiltin_Lean_Parser_Term_tparser_x21_formatter___closed__1;
lean_object* l_Lean_Parser_Term_decide___closed__1;
lean_object* l_Lean_Parser_Term_simpleBinder___closed__2;
@ -623,6 +621,7 @@ lean_object* l_Lean_Parser_Term_inaccessible_formatter___closed__3;
lean_object* l_Lean_Parser_Term_typeOf;
lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_letPatDecl___closed__4;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__19;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_withoutPosition_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_attributes_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_matchDiscr___elambda__1(lean_object*, lean_object*);
@ -715,6 +714,7 @@ lean_object* l_Lean_Parser_Term_cdot___elambda__1___closed__7;
extern lean_object* l_Lean_Parser_leadPrec___closed__1;
lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__8;
lean_object* lean_string_append(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__11;
lean_object* l_Lean_Parser_Term_dbgTrace___closed__6;
lean_object* l_Lean_Parser_Term_explicit___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_sorry___closed__2;
@ -2935,6 +2935,7 @@ lean_object* l_Lean_Parser_Term_hole;
lean_object* l___regBuiltinParser_Lean_Parser_Term_scientific(lean_object*);
lean_object* l_Lean_Parser_Term_app___closed__1;
lean_object* l_Lean_Parser_Term_emptyC___closed__5;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__8;
extern lean_object* l___kind_term____x40_Init_Notation___hyg_11713____closed__10;
lean_object* l___regBuiltin_Lean_Parser_Term_have_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_funSimpleBinder___closed__1;
@ -3311,7 +3312,6 @@ lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_matchAltsWhereDecls_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_num_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_unreachable___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__8;
lean_object* l___regBuiltin_Lean_Parser_Term_fun_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_dbgTrace___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_funSimpleBinder_parenthesizer___closed__2;
@ -3442,7 +3442,6 @@ lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
lean_object* l_Lean_Parser_Term_bracketedBinder_formatter(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_let_x21_formatter___closed__2;
lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__4;
lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_attrInstance___closed__10;
lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__7;
@ -3551,6 +3550,7 @@ lean_object* l_Lean_Parser_Term_binderTactic___closed__3;
lean_object* l_Lean_Parser_Term_structInst___closed__19;
lean_object* l_Lean_Parser_Term_depArrow_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_matchAlts_parenthesizer___closed__10;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__4;
lean_object* l_Lean_Parser_Term_sort___closed__7;
lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___closed__10;
lean_object* l_Lean_Parser_Term_pipeProj___closed__1;
@ -6665,7 +6665,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_myMacro____x40_Init_Notation___hyg_54____closed__6;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__8;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -6824,7 +6824,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_myMacro____x40_Init_Notation___hyg_54____closed__6;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__11;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__11;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -6959,7 +6959,7 @@ static lean_object* _init_l_Lean_Parser_Term_type___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__19;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__19;
x_2 = l_Lean_Parser_Level_max___elambda__1___closed__7;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -36754,7 +36754,7 @@ x_6 = lean_ctor_get(x_4, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__4;
x_8 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__4;
x_9 = l_Lean_Parser_checkNoWsBeforeFn(x_8, x_1, x_4);
x_10 = lean_ctor_get(x_9, 3);
lean_inc(x_10);
@ -37107,7 +37107,7 @@ x_6 = lean_ctor_get(x_4, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__4;
x_8 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__4;
x_9 = l_Lean_Parser_checkNoWsBeforeFn(x_8, x_1, x_4);
x_10 = lean_ctor_get(x_9, 3);
lean_inc(x_10);

24
stage0/stdlib/Lean/PrettyPrinter/Formatter.c generated
View file

@ -14,7 +14,6 @@
extern "C" {
#endif
lean_object* l_List_reverse___rarg(lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__51;
lean_object* l_Lean_PrettyPrinter_Formatter_State_stack___default;
extern lean_object* l_Lean_Parser_builtinTokenTable;
lean_object* l_Lean_ParserCompiler_CombinatorAttribute_runDeclFor___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -120,6 +119,7 @@ extern lean_object* l_rawNatLit___closed__8;
lean_object* l_Lean_PrettyPrinter_Formatter_pushLine(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_notFollowedByCategoryToken_formatter(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_instMonadTraverserFormatterM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__51;
lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__59;
lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__31;
lean_object* l_Lean_PrettyPrinter_Formatter_identNoAntiquot_formatter_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -194,12 +194,12 @@ lean_object* l_Lean_PrettyPrinter_Formatter_checkKind___closed__5;
lean_object* l_Lean_PrettyPrinter_Formatter_checkPrec_formatter___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_instMonadTraverserFormatterM___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_trailingNode_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
lean_object* l_Lean_PrettyPrinter_Formatter_getStackSize(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_checkColGe_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_formatterForKind(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_List_foldr___at_Lean_PrettyPrinter_Formatter_identNoAntiquot_formatter___spec__1(uint8_t, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_interpretParserDescr___elambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
lean_object* l_Lean_PrettyPrinter_Formatter_withAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Formatter_symbol_formatter___spec__1(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_unicodeSymbol_formatter___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -313,6 +313,7 @@ lean_object* l_Lean_PrettyPrinter_formatterAttribute;
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___lambda__1___closed__5;
lean_object* l_Lean_PrettyPrinter_Formatter_instMonadTraverserFormatterM___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__12;
lean_object* l_Lean_PrettyPrinter_Formatter_interpretParserDescr_match__1(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_rawIdent_formatter_match__1(lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_goUp___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -342,7 +343,6 @@ uint8_t lean_is_inaccessible_user_name(lean_object*);
lean_object* l_ReaderT_pure___at_Lean_PrettyPrinter_Formatter_interpolatedStr_formatter___spec__1(lean_object*);
lean_object* l_String_trimLeft(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_setExpected_formatter(lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__15;
lean_object* l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___lambda__2___closed__7;
lean_object* l_List_foldr___at_Lean_PrettyPrinter_Formatter_identNoAntiquot_formatter___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_instReprIterator___closed__2;
@ -360,6 +360,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_checkLineEq_formatter___boxed(lean_o
lean_object* l_Lean_PrettyPrinter_format(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_nameLitNoAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_withPosition_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__15;
lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__10;
lean_object* l_Lean_PrettyPrinter_Formatter_checkColGe_formatter(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_State_leadWord___default;
@ -406,7 +407,6 @@ lean_object* l_Lean_PrettyPrinter_Formatter_checkNoImmediateColon_formatter(lean
lean_object* l_Lean_Syntax_MonadTraverser_goUp___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__4___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__22;
extern lean_object* l_Lean_ParserCompiler_CombinatorAttribute_instInhabitedCombinatorAttribute___closed__1;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__12;
extern lean_object* l___kind_term____x40_Init_Notation___hyg_12477____closed__5;
extern lean_object* l_Lean_Format_getWidth___closed__1;
lean_object* l_Lean_PrettyPrinter_Formatter_checkNoWsBefore_formatter___boxed(lean_object*);
@ -448,7 +448,9 @@ lean_object* l_Lean_PrettyPrinter_Formatter_pushToken___lambda__1___boxed(lean_o
lean_object* l_Lean_PrettyPrinter_Formatter_pushNone_formatter___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_visitArgs___closed__1;
lean_object* l_Lean_PrettyPrinter_Formatter_throwBacktrack___rarg___closed__1;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__9;
lean_object* l_Lean_PrettyPrinter_format_match__1(lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__27;
lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__14;
lean_object* l_Lean_PrettyPrinter_Formatter_concat___closed__1;
lean_object* l_Lean_PrettyPrinter_Formatter_setStack(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -538,13 +540,11 @@ extern lean_object* l_Lean_Parser_Tactic_inductionAlts___closed__8;
lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__27;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_PrettyPrinter_Formatter_concat___spec__1(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_throwError___at_Lean_PrettyPrinter_Formatter_unicodeSymbol_formatter___spec__1(lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__9;
lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__4;
lean_object* l_Lean_PrettyPrinter_Formatter_symbol_formatter___closed__11;
extern lean_object* l_Lean_PrettyPrinter_backtrackExceptionId;
lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__64;
lean_object* l_Lean_PrettyPrinter_Formatter_suppressInsideQuot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__27;
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__2;
lean_object* l_Lean_Syntax_Traverser_left(lean_object*);
@ -10033,7 +10033,7 @@ lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
x_19 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__9;
x_19 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__9;
x_20 = l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__21;
x_21 = l_Lean_Parser_registerAliasCore___rarg(x_2, x_19, x_20, x_18);
if (lean_obj_tag(x_21) == 0)
@ -10042,7 +10042,7 @@ lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);
x_23 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__12;
x_23 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__12;
x_24 = l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__26;
x_25 = l_Lean_Parser_registerAliasCore___rarg(x_2, x_23, x_24, x_22);
if (lean_obj_tag(x_25) == 0)
@ -10051,7 +10051,7 @@ lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_26 = lean_ctor_get(x_25, 1);
lean_inc(x_26);
lean_dec(x_25);
x_27 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__15;
x_27 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__15;
x_28 = l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__31;
x_29 = l_Lean_Parser_registerAliasCore___rarg(x_2, x_27, x_28, x_26);
if (lean_obj_tag(x_29) == 0)
@ -10087,7 +10087,7 @@ lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_42 = lean_ctor_get(x_41, 1);
lean_inc(x_42);
lean_dec(x_41);
x_43 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__27;
x_43 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__27;
x_44 = l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2500____closed__42;
x_45 = l_Lean_Parser_registerAliasCore___rarg(x_2, x_43, x_44, x_42);
if (lean_obj_tag(x_45) == 0)
@ -10195,7 +10195,7 @@ lean_object* x_90; lean_object* x_91; lean_object* x_92;
x_90 = lean_ctor_get(x_89, 1);
lean_inc(x_90);
lean_dec(x_89);
x_91 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__51;
x_91 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__51;
x_92 = l_Lean_Parser_registerAliasCore___rarg(x_2, x_91, x_76, x_90);
if (lean_obj_tag(x_92) == 0)
{
@ -12227,7 +12227,7 @@ static lean_object* _init_l_Lean_PrettyPrinter_formatCommand___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_categoryParser_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;

24
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c generated
View file

@ -16,7 +16,6 @@ extern "C" {
lean_object* l_List_reverse___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__14;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__51;
lean_object* l_Lean_Syntax_MonadTraverser_goLeft___at_Lean_PrettyPrinter_Parenthesizer_visitToken___spec__1___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__46;
lean_object* l_Lean_ParserCompiler_CombinatorAttribute_runDeclFor___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -122,6 +121,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_withoutPosition_parenthesizer(le
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__7;
extern lean_object* l_rawNatLit___closed__8;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__20;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__51;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_throwBacktrack___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__34;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__15;
@ -219,7 +219,6 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkWsBefore_parenthesizer___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__2(lean_object*);
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1161____closed__33;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__4;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__59;
lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute;
@ -228,6 +227,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_setExpected_parenthesizer___rarg
lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__5;
lean_object* l_Lean_Syntax_Traverser_setCur(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__36;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
extern lean_object* l_Lean_Parser_Tactic_intro___closed__12;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__61;
@ -335,6 +335,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__5;
extern lean_object* l_Lean_Parser_Tactic_rwRuleSeq___closed__4;
extern lean_object* l_Lean_Unhygienic_instMonadQuotationUnhygienic___closed__4;
lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___closed__4;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__12;
lean_object* l_Lean_attrParamSyntaxToIdentifier(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
lean_object* l_Lean_Syntax_MonadTraverser_getCur___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__1___boxed(lean_object*);
@ -361,7 +362,6 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_eoi_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_getCur___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__1(lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__15;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_eoi_parenthesizer___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__20;
@ -390,6 +390,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_interpretParserDescr___elambda__
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__2;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_throwBacktrack___rarg___closed__1;
extern lean_object* l___kind_term____x40_Init_Notation___hyg_11713____closed__6;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__15;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoWsBefore_parenthesizer___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadTraverserParenthesizerM;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__51;
@ -437,7 +438,6 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2393_(lean_object*);
extern lean_object* l_Lean_ParserCompiler_CombinatorAttribute_instInhabitedCombinatorAttribute___closed__1;
lean_object* l_Lean_Syntax_MonadTraverser_goRight___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__12;
extern lean_object* l___kind_term____x40_Init_Notation___hyg_12477____closed__5;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_setExpected_parenthesizer(lean_object*);
uint8_t l_Lean_Parser_isParserCategory(lean_object*, lean_object*);
@ -490,7 +490,9 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadTraverserParenthesizerM
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize_match__5___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__27;
lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__9;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__27;
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__5;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadTraverserParenthesizerM___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_forM_loop___at_Lean_PrettyPrinter_Parenthesizer_parenthesizeCategoryCore___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -592,7 +594,6 @@ lean_object* l_Nat_min(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_many1_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__6;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__9;
extern lean_object* l_Lean_PrettyPrinter_backtrackExceptionId;
lean_object* l_Lean_PrettyPrinter_parenthesizeTerm___closed__1;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___closed__3;
@ -601,7 +602,6 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkColGt_parenthesizer___boxed
extern lean_object* l_myMacro____x40_Init_Notation___hyg_11163____closed__21;
lean_object* l_Lean_Syntax_MonadTraverser_getIdx___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__53;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__27;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__42;
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__55;
@ -11155,7 +11155,7 @@ lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
x_19 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__9;
x_19 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__9;
x_20 = l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__21;
x_21 = l_Lean_Parser_registerAliasCore___rarg(x_2, x_19, x_20, x_18);
if (lean_obj_tag(x_21) == 0)
@ -11164,7 +11164,7 @@ lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);
x_23 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__12;
x_23 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__12;
x_24 = l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__26;
x_25 = l_Lean_Parser_registerAliasCore___rarg(x_2, x_23, x_24, x_22);
if (lean_obj_tag(x_25) == 0)
@ -11173,7 +11173,7 @@ lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_26 = lean_ctor_get(x_25, 1);
lean_inc(x_26);
lean_dec(x_25);
x_27 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__15;
x_27 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__15;
x_28 = l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__31;
x_29 = l_Lean_Parser_registerAliasCore___rarg(x_2, x_27, x_28, x_26);
if (lean_obj_tag(x_29) == 0)
@ -11209,7 +11209,7 @@ lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_42 = lean_ctor_get(x_41, 1);
lean_inc(x_42);
lean_dec(x_41);
x_43 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__27;
x_43 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__27;
x_44 = l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2459____closed__42;
x_45 = l_Lean_Parser_registerAliasCore___rarg(x_2, x_43, x_44, x_42);
if (lean_obj_tag(x_45) == 0)
@ -11317,7 +11317,7 @@ lean_object* x_90; lean_object* x_91; lean_object* x_92;
x_90 = lean_ctor_get(x_89, 1);
lean_inc(x_90);
lean_dec(x_89);
x_91 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1890____closed__51;
x_91 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_1943____closed__51;
x_92 = l_Lean_Parser_registerAliasCore___rarg(x_2, x_91, x_76, x_90);
if (lean_obj_tag(x_92) == 0)
{
@ -13389,7 +13389,7 @@ static lean_object* _init_l_Lean_PrettyPrinter_parenthesizeCommand___closed__1()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3897____closed__3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3889____closed__3;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_categoryParser_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);

7028
stage0/stdlib/Lean/ScopedEnvExtension.c generated Normal file
View file

File diff suppressed because it is too large Load diff