From 0b7d9876999eb29ff4bbdcdde799d21707d521ab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Mar 2019 17:27:12 -0700 Subject: [PATCH] feat(frontends/lean, library/init/lean): opaque constants @kha I have added support for opaque constants to the old C++ frontend, and made sure the new frontend can still parse `library/init/core.lean`. The kernel should enforce that opaque constants are really opaque, and the following example should fail ``` constant x : nat := 0 theorem foo : x = 0 := rfl ``` If it doesn't, it is a bug. Here are some remaining issues: 1- `environment.mk_empty` is currently an axiom because we cannot create an inhabitant of an opaque type. A possible solution is to use `option environment` instead of `environment`. 2- There is no support for opaque constants in the new frontend. However, I modified it to handle axioms, and fixed the literal values with decl_cmd_kind. I tried to mark some of my changes with comments, but it is probably much easier for you to just check the commit change list. 3- I did not add any support for automatically constructing `e` at `constant x : t := e`. I think we can do this later after we replace the old frontend with the new one. BTW, it took only a few minutes to provide the inhabitants manually. --- lean4-mode/lean4-syntax.el | 6 +- library/init/core.lean | 6 +- library/init/data/char/basic.lean | 4 +- library/init/io.lean | 32 +- library/init/lean/elaborator.lean | 25 +- library/init/lean/expander.lean | 8 +- library/init/lean/parser/declaration.lean | 4 +- library/init/lean/util.lean | 2 +- src/boot/init/io.cpp | 80 +- src/boot/init/lean/elaborator.cpp | 17 +- src/boot/init/lean/expander.cpp | 40 +- src/boot/init/lean/frontend.cpp | 16 +- src/boot/init/lean/parser/declaration.cpp | 996 +++++++++------------- src/frontends/lean/decl_cmds.cpp | 48 +- src/frontends/lean/decl_cmds.h | 2 +- src/frontends/lean/decl_util.h | 2 +- src/frontends/lean/definition_cmds.cpp | 35 +- src/frontends/lean/token_table.cpp | 5 +- src/frontends/lean/vm_elaborator.cpp | 8 +- 19 files changed, 587 insertions(+), 749 deletions(-) diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el index 9cd531d9df..e1fb4dc5ca 100644 --- a/lean4-mode/lean4-syntax.el +++ b/lean4-mode/lean4-syntax.el @@ -9,9 +9,9 @@ (defconst lean4-keywords1 '("import" "prelude" "protected" "private" "noncomputable" "definition" "unsafe" "renaming" - "hiding" "exposing" "parameter" "parameters" "begin" "constant" "constants" + "hiding" "exposing" "parameter" "parameters" "begin" "constant" "lemma" "variable" "variables" "theorem" "example" "abbreviation" "abbrev" - "open" "export" "axiom" "axioms" "inductive" "coinductive" "with" "without" + "open" "export" "axiom" "inductive" "coinductive" "with" "without" "structure" "universe" "universes" "hide" "precedence" "reserve" "declare_trace" "add_key_equivalence" "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance" @@ -142,7 +142,7 @@ (1 'font-lock-function-name-face)) ;; declarations (,(rx word-start - (group (or "inductive" (group "class" (zero-or-more whitespace) "inductive") "instance" "structure" "class" "theorem" "axiom" "axioms" "lemma" "definition" "def" "constant")) + (group (or "inductive" (group "class" (zero-or-more whitespace) "inductive") "instance" "structure" "class" "theorem" "axiom" "lemma" "definition" "def" "constant")) word-end (zero-or-more whitespace) (group (zero-or-more "{" (zero-or-more (not (any "}"))) "}" (zero-or-more whitespace))) (zero-or-more whitespace) diff --git a/library/init/core.lean b/library/init/core.lean index cfc20cba93..80831246fc 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -337,7 +337,7 @@ inductive nat /- Auxiliary axiom used to implement `sorry`. TODO: add this theorem on-demand. That is, we should only add it if after the first error. -/ -constant sorry_ax (α : Sort u) (synthetic := tt) : α +unsafe axiom sorry_ax (α : Sort u) (synthetic := tt) : α /- Declare builtin and reserved notation -/ @@ -1724,7 +1724,7 @@ end setoid /- Propositional extensionality -/ -constant propext {a b : Prop} : (a ↔ b) → a = b +axiom propext {a b : Prop} : (a ↔ b) → a = b /- Additional congruence theorems. -/ @@ -1766,7 +1766,7 @@ theorem iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) eq.subst (propext h₁) h₂ namespace quot -constant sound : Π {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b +axiom sound : Π {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b attribute [elab_as_eliminator] lift ind diff --git a/library/init/data/char/basic.lean b/library/init/data/char/basic.lean index ef3840ddeb..5c01df53e3 100644 --- a/library/init/data/char/basic.lean +++ b/library/init/data/char/basic.lean @@ -42,8 +42,10 @@ uint32.dec_lt _ _ instance dec_le (a b : char) : decidable (a ≤ b) := uint32.dec_le _ _ +axiom is_valid_char_0 : is_valid_char 0 + @[noinline, pattern] def of_nat (n : nat) : char := -if h : is_valid_char (uint32.of_nat n) then {val := uint32.of_nat n, valid := h} else {val := 0, valid := sorry} +if h : is_valid_char (uint32.of_nat n) then {val := uint32.of_nat n, valid := h} else {val := 0, valid := is_valid_char_0} @[inline] def to_nat (c : char) : nat := c.val.to_nat diff --git a/library/init/io.lean b/library/init/io.lean index 8e39429601..1a0311057d 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -8,19 +8,20 @@ import init.control.state init.control.except init.data.string.basic init.fix /-- Like https://hackage.haskell.org/package/ghc-prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld. Makes sure we never reorder `io` operations. -/ -constant io.real_world : Type +constant io.real_world : Type := unit + -- TODO: make opaque @[irreducible, derive monad] def io : Type → Type := state io.real_world @[extern "lean_io_unsafe"] -constant unsafe_io {α : Type} [inhabited α] (fn : io α) : α +constant unsafe_io {α : Type} [inhabited α] (fn : io α) : α := default α @[extern 4 "lean_io_timeit"] -constant timeit {α : Type} (msg : @& string) (fn : io α) : io α +constant timeit {α : Type} (msg : @& string) (fn : io α) : io α := fn @[extern 4 "lean_io_allocprof"] -constant allocprof {α : Type} (msg : @& string) (fn : io α) : io α +constant allocprof {α : Type} (msg : @& string) (fn : io α) : io α := fn abbrev monad_io (m : Type → Type) := has_monad_lift_t io m @@ -56,7 +57,7 @@ end inductive fs.mode | read | write | read_write | append -constant fs.handle : Type +constant fs.handle : Type := unit namespace prim open fs @@ -85,23 +86,30 @@ iterate a $ λ r, do | except.ok (sum.inr r) := pure (sum.inr (except.ok r)) | except.error e := pure (sum.inr (except.error e)) + +section +local attribute [reducible] io +def eio_inh {α : Type} : eio α := +λ s, (except.error (default io.error), s) +end + @[extern 2 "lean_io_prim_put_str"] -constant put_str (s: @& string) : eio unit +constant put_str (s: @& string) : eio unit := eio_inh @[extern 1 "lean_io_prim_get_line"] -constant get_line : eio string +constant get_line : eio string := eio_inh @[extern 4 "lean_io_prim_handle_mk"] -constant handle.mk (s : @& string) (m : mode) (bin : bool := ff) : eio handle +constant handle.mk (s : @& string) (m : mode) (bin : bool := ff) : eio handle := eio_inh @[extern 2 "lean_io_prim_handle_is_eof"] -constant handle.is_eof (h : @& handle) : eio bool +constant handle.is_eof (h : @& handle) : eio bool := eio_inh @[extern 2 "lean_io_prim_handle_flush"] -constant handle.flush (h : @& handle) : eio unit +constant handle.flush (h : @& handle) : eio unit := eio_inh @[extern 2 "lean_io_prim_handle_close"] -constant handle.close (h : @& handle) : eio unit +constant handle.close (h : @& handle) : eio unit := eio_inh -- TODO: replace `string` with byte buffer -- constant handle.read : handle → nat → eio string -- constant handle.write : handle → string → eio unit @[extern 2 "lean_io_prim_handle_get_line"] -constant handle.get_line (h : @& handle) : eio string +constant handle.get_line (h : @& handle) : eio string := eio_inh @[inline] def lift_eio {m : Type → Type} {ε α : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m] (x : eio α) : m α := diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 20d382b3ee..5bf7c819af 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -13,14 +13,16 @@ import init.lean.options namespace lean -- TODO(Sebastian): should probably be meta together with the whole elaborator -constant environment : Type +constant environment : Type := unit + @[extern "lean_environment_mk_empty"] -constant environment.mk_empty : unit → environment +axiom environment.mk_empty : unit → environment + @[extern "lean_environment_contains"] -constant environment.contains : (@& environment) → (@& name) → bool +constant environment.contains (env : @& environment) (n : @& name) : bool := ff -- deprecated constructor @[extern "lean_expr_local"] -constant expr.local : name → name → expr → binder_info → expr +constant expr.local (n : name) (pp : name) (ty : expr) (bi : binder_info) : expr := default expr namespace elaborator -- TODO(Sebastian): move @@ -46,8 +48,7 @@ structure old_elaborator_state := (ns : name) @[extern "lean_elaborator_elaborate_command"] -constant elaborate_command (filename : @& string) : expr → (@& old_elaborator_state) → - option old_elaborator_state × message_log +constant elaborate_command (filename : @& string) (e : expr) (s : @& old_elaborator_state) : option old_elaborator_state × message_log := (none, ⟨[]⟩) open parser open parser.combinators @@ -460,8 +461,8 @@ def declaration.elaborate : elaborator := λ stx, locally $ do let decl := view «declaration» stx, match decl.inner with - | declaration.inner.view.constant c@{sig := {params := bracketed_binders.view.simple [], type := type}, ..} := do - let mdata := kvmap.set_name {} `command `constant, + | declaration.inner.view.«axiom» c@{sig := {params := bracketed_binders.view.simple [], type := type}, ..} := do + let mdata := kvmap.set_name {} `command `«axiom», -- CommentTo(Kha): It was `constant` here mods ← decl_modifiers_to_pexpr decl.modifiers, let id := ident_univ_params_to_pexpr c.name, type ← to_pexpr type.type, @@ -470,8 +471,8 @@ def declaration.elaborate : elaborator := let kind := match dl.kind with | def_like.kind.view.theorem _ := 0 | def_like.kind.view.def _ := 1 - | def_like.kind.view.abbreviation _ := 5 - | def_like.kind.view.«abbrev» _ := 5, + | def_like.kind.view.abbreviation _ := 6 + | def_like.kind.view.«abbrev» _ := 6, elab_def_like stx decl.modifiers dl kind -- these are almost macros for `def`, except the elaborator handles them specially at a few places @@ -481,13 +482,13 @@ def declaration.elaborate : elaborator := kind := def_like.kind.view.def, name := {id := name.anonymous}, sig := {..ex.sig}, - ..ex} 2 + ..ex} 3 | declaration.inner.view.instance i := elab_def_like stx decl.modifiers { kind := def_like.kind.view.def, name := i.name.get_or_else {id := name.anonymous}, sig := {..i.sig}, - ..i} 3 + ..i} 4 | declaration.inner.view.inductive ind@{«class» := none, sig := {params := bracketed_binders.view.simple bbs}, ..} := do let mdata := kvmap.set_name {} `command `inductives, diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index 1805aed037..7e8bdf229b 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -372,15 +372,15 @@ def let.transform : transformer := equations := [{item := {lhs := [llp], rhs := v.body}}]} -- move parameters into type -def constant.transform : transformer := +def axiom.transform : transformer := λ stx, do - let v := view «constant» stx, + let v := view «axiom» stx, match v with | {sig := {params := bracketed_binders.view.extended bindrs, type := type}, ..} := do let bindrs := binders.view.extended { leading_ids := [], remainder := binders_remainder.view.mixed $ bindrs.map mixed_binder.view.bracketed}, - pure $ review «constant» {v with sig := { + pure $ review «axiom» {v with sig := { params := bracketed_binders.view.simple [], type := {type := review pi {op := syntax.atom {val := "Π"}, binders := bindrs, range := type.type}}}} | _ := no_expansion @@ -482,7 +482,7 @@ def builtin_transformers : rbmap name transformer (<) := rbmap.from_list [ (assume.name, assume.transform), (if.name, if.transform), (let.name, let.transform), - (constant.name, constant.transform), + (axiom.name, axiom.transform), (declaration.name, declaration.transform), (intro_rule.name, intro_rule.transform), (variable.name, variable.transform), diff --git a/library/init/lean/parser/declaration.lean b/library/init/lean/parser/declaration.lean index 573b293946..d1e21c4a23 100644 --- a/library/init/lean/parser/declaration.lean +++ b/library/init/lean/parser/declaration.lean @@ -147,8 +147,8 @@ node! declaration [ name: ident_univ_params.parser, sig: opt_decl_sig.parser, val: decl_val.parser], «instance»: node! «instance» ["instance", name: ident_univ_params.parser?, sig: decl_sig.parser, val: decl_val.parser], «example»: node! «example» ["example", sig: decl_sig.parser, val: decl_val.parser], - «constant»: node! «constant» [ - kw: node_choice! constant_keyword {"constant", "axiom"}, + «axiom»: node! «axiom» [ -- CommentTo(Kha): -- replaced `constant with `axiom + kw: node_choice! constant_keyword {"axiom"}, name: ident_univ_params.parser, sig: decl_sig.parser], «inductive»: node! «inductive» [try [«class»: (symbol "class")?, "inductive"], diff --git a/library/init/lean/util.lean b/library/init/lean/util.lean index 9164b8ee0b..1b863ecfc5 100644 --- a/library/init/lean/util.lean +++ b/library/init/lean/util.lean @@ -10,7 +10,7 @@ namespace lean /-- Print and accumulate run time of `act` when option `profiler` is set to `true`. -/ @[extern 5 "lean_lean_profileit"] -constant profileit {α : Type} (category : @& string) (pos : @& position) (act : io α) : io α +constant profileit {α : Type} (category : @& string) (pos : @& position) (act : io α) : io α := act def profileit_pure {α : Type} (category : string) (pos : position) (fn : unit → α) : io α := profileit category pos $ io.lazy_pure fn diff --git a/src/boot/init/io.cpp b/src/boot/init/io.cpp index bd4e7a86fc..8d7db4a966 100644 --- a/src/boot/init/io.cpp +++ b/src/boot/init/io.cpp @@ -16,6 +16,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #endif obj* l_io_prim_iterate__aux___main___boxed(obj*, obj*); obj* l_io_prim_iterate___at_io_prim_iterate__eio___spec__1(obj*, obj*, obj*, obj*); +obj* l_io_prim_eio__inh___rarg___closed__1; obj* l_io_fs_handle_mk___rarg(obj*, obj*, obj*, obj*, obj*, uint8, uint8); obj* l_io_fs_handle_is__eof___at_io_fs_handle_read__to__end___spec__1(obj*, obj*); obj* l_io_println___at_io_println_x_27___spec__1(obj*, obj*); @@ -33,6 +34,7 @@ obj* l_io_prim_io__inhabited(obj*); obj* l_io_fs_handle_flush___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_io_has__eval___boxed(obj*); extern obj* l_string_iterator_extract___main___closed__1; +obj* l___private_init_io_1__put__str___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_io_prim_iterate___at_io_prim_iterate__eio___spec__1___boxed(obj*, obj*, obj*, obj*); obj* l_io_prim_handle_flush___boxed(obj*, obj*); obj* l_io_fs_handle_is__eof___rarg___lambda__1(obj*, obj*, obj*, obj*); @@ -51,11 +53,10 @@ obj* l_io_prim_handle_is__eof___boxed(obj*, obj*); obj* l_io_prim_iterate___at_io_prim_iterate__eio___spec__1___rarg(obj*, obj*, obj*); obj* l_io_prim_handle_mk___boxed(obj*, obj*, obj*, obj*); obj* l_io_fs_read__file___rarg(obj*, obj*, obj*, obj*, obj*, uint8); -obj* l___private_init_io_13__put__str___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_io_prim_lift__eio(obj*, obj*, obj*); obj* l_io_prim_io__inhabited___boxed(obj*); +obj* l_io_prim_eio__inh(obj*); obj* l_io_fs_handle_mk___boxed(obj*, obj*); -obj* l___private_init_io_13__put__str___boxed(obj*, obj*); obj* l_io_fs_handle_is__eof___at_io_fs_handle_read__to__end___spec__1___boxed(obj*, obj*); obj* l_io_println_x_27___boxed(obj*, obj*); obj* l_allocprof___boxed(obj*, obj*, obj*, obj*); @@ -69,9 +70,9 @@ namespace lean { obj* string_append(obj*, obj*); } obj* l_eio_has__eval(obj*, obj*); -obj* l___private_init_io_13__put__str___at_io_println_x_27___spec__3(obj*, obj*); obj* l_io_print___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_io_fs_read__file___boxed(obj*, obj*); +obj* l___private_init_io_1__put__str(obj*, obj*); obj* l_io_fs_handle_is__eof___boxed(obj*, obj*); obj* l_io_fs_read__file___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_io_fs_handle_read__to__end(obj*, obj*); @@ -83,6 +84,7 @@ obj* l_io_prim_io__inhabited___rarg(obj*); obj* l_io_fs_read__file___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*); extern "C" obj* lean_io_prim_handle_close(obj*, obj*); obj* l_io_lazy__pure___boxed(obj*); +obj* l___private_init_io_1__put__str___at_io_println_x_27___spec__3___boxed(obj*, obj*); obj* l_io_prim_inhabited(obj*, obj*); obj* l_io_println___boxed(obj*, obj*); obj* l_io_prim_iterate(obj*, obj*, obj*); @@ -92,7 +94,9 @@ obj* l_has__repr_has__eval(obj*); obj* l_io_println___rarg___closed__1; obj* l_io_print(obj*, obj*); obj* l_io_fs_handle_is__eof(obj*, obj*); +obj* l___private_init_io_1__put__str___boxed(obj*, obj*); obj* l_io_prim_iterate___at_io_prim_iterate__eio___spec__1___rarg___lambda__1(obj*, obj*, obj*); +obj* l_io_prim_eio__inh___boxed(obj*); obj* l_io_prim_inhabited___rarg(obj*); obj* l_io_fs_handle_close___rarg(obj*, obj*, obj*, obj*, obj*); extern "C" obj* lean_io_prim_handle_flush(obj*, obj*); @@ -113,7 +117,6 @@ obj* l_eio__unit_has__eval___rarg(obj*, obj*, obj*); obj* l_io_prim_iterate__aux(obj*, obj*); extern "C" obj* lean_io_unsafe(obj*, obj*, obj*); obj* l_io_fs_read__file(obj*, obj*); -obj* l___private_init_io_13__put__str___at_io_println_x_27___spec__3___boxed(obj*, obj*); obj* l_io_prim_lift__eio___boxed(obj*, obj*, obj*); obj* l_io_fs_handle_flush___boxed(obj*, obj*); obj* l_state__t_pure___at_io_prim_io__inhabited___spec__1(obj*); @@ -126,7 +129,6 @@ obj* l_io_println_x_27(obj*, obj*); obj* l_io_lazy__pure___rarg(obj*, obj*); obj* l_io_error_inhabited; obj* l_io_fs_handle_read__to__end___rarg(obj*, obj*, obj*, obj*, obj*); -obj* l___private_init_io_13__put__str(obj*, obj*); obj* l_io_prim_handle_close___boxed(obj*, obj*); obj* l_io_prim_iterate___at_io_fs_handle_read__to__end___spec__4(obj*, obj*, obj*); obj* l_id_bind___boxed(obj*, obj*); @@ -142,6 +144,7 @@ obj* l_io_prim_inhabited___boxed(obj*, obj*); obj* l_io_fs_handle_close(obj*, obj*); obj* l_io_println___at_io_println_x_27___spec__1___boxed(obj*, obj*); obj* l_io__unit_has__eval(obj*, obj*); +obj* l_io_prim_eio__inh___rarg(obj*); obj* l_state__t_pure___at_io_prim_io__inhabited___spec__1___boxed(obj*); extern "C" obj* lean_io_prim_handle_is_eof(obj*, obj*); obj* l_eio_has__eval___boxed(obj*, obj*); @@ -150,6 +153,7 @@ obj* l_id_monad___lambda__2___boxed(obj*, obj*, obj*, obj*); obj* l_string_has__lift(obj*); obj* l_io_fs_handle_get__line(obj*, obj*); obj* l_id_monad___lambda__3___boxed(obj*, obj*, obj*, obj*); +obj* l___private_init_io_1__put__str___at_io_println_x_27___spec__3(obj*, obj*); obj* l_io_prim_iterate__eio___at_io_fs_handle_read__to__end___spec__3(obj*, obj*, obj*); obj* l_io_prim_iterate__aux___main(obj*, obj*); obj* l_io_fs_read__file___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*); @@ -671,6 +675,44 @@ lean::dec(x_2); return x_3; } } +obj* _init_l_io_prim_eio__inh___rarg___closed__1() { +_start: +{ +obj* x_0; obj* x_1; +x_0 = lean::mk_string(""); +x_1 = lean::alloc_cnstr(0, 1, 0); +lean::cnstr_set(x_1, 0, x_0); +return x_1; +} +} +obj* l_io_prim_eio__inh___rarg(obj* x_0) { +_start: +{ +obj* x_1; obj* x_2; +x_1 = l_io_prim_eio__inh___rarg___closed__1; +x_2 = lean::alloc_cnstr(0, 2, 0); +lean::cnstr_set(x_2, 0, x_1); +lean::cnstr_set(x_2, 1, x_0); +return x_2; +} +} +obj* l_io_prim_eio__inh(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::alloc_closure(reinterpret_cast(l_io_prim_eio__inh___rarg), 1, 0); +return x_1; +} +} +obj* l_io_prim_eio__inh___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = l_io_prim_eio__inh(x_0); +lean::dec(x_0); +return x_1; +} +} obj* l_io_prim_put__str___boxed(obj* x_0, obj* x_1) { _start: { @@ -805,7 +847,7 @@ lean::dec(x_2); return x_3; } } -obj* l___private_init_io_13__put__str___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) { +obj* l___private_init_io_1__put__str___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) { _start: { obj* x_5; obj* x_6; obj* x_8; obj* x_9; obj* x_10; @@ -822,19 +864,19 @@ x_10 = lean::apply_4(x_6, lean::box(0), lean::box(0), x_8, x_9); return x_10; } } -obj* l___private_init_io_13__put__str(obj* x_0, obj* x_1) { +obj* l___private_init_io_1__put__str(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = lean::alloc_closure(reinterpret_cast(l___private_init_io_13__put__str___rarg), 5, 0); +x_2 = lean::alloc_closure(reinterpret_cast(l___private_init_io_1__put__str___rarg), 5, 0); return x_2; } } -obj* l___private_init_io_13__put__str___boxed(obj* x_0, obj* x_1) { +obj* l___private_init_io_1__put__str___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l___private_init_io_13__put__str(x_0, x_1); +x_2 = l___private_init_io_1__put__str(x_0, x_1); lean::dec(x_0); lean::dec(x_1); return x_2; @@ -845,7 +887,7 @@ _start: { obj* x_7; obj* x_8; x_7 = lean::apply_1(x_5, x_6); -x_8 = l___private_init_io_13__put__str___rarg(x_0, x_1, x_2, x_3, x_7); +x_8 = l___private_init_io_1__put__str___rarg(x_0, x_1, x_2, x_3, x_7); return x_8; } } @@ -899,7 +941,7 @@ lean::inc(x_1); lean::inc(x_0); x_16 = l_io_print___rarg(x_0, x_1, x_2, x_3, lean::box(0), x_5, x_6); x_17 = l_io_println___rarg___closed__1; -x_18 = l___private_init_io_13__put__str___rarg(x_0, x_1, x_2, x_3, x_17); +x_18 = l___private_init_io_1__put__str___rarg(x_0, x_1, x_2, x_3, x_17); x_19 = lean::apply_4(x_9, lean::box(0), lean::box(0), x_16, x_18); return x_19; } @@ -1752,7 +1794,7 @@ lean::cnstr_set(x_7, 1, x_3); return x_7; } } -obj* l___private_init_io_13__put__str___at_io_println_x_27___spec__3(obj* x_0, obj* x_1) { +obj* l___private_init_io_1__put__str___at_io_println_x_27___spec__3(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_3; @@ -1835,7 +1877,7 @@ obj* l_io_print___at_io_println_x_27___spec__2(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l___private_init_io_13__put__str___at_io_println_x_27___spec__3(x_0, x_1); +x_2 = l___private_init_io_1__put__str___at_io_println_x_27___spec__3(x_0, x_1); return x_2; } } @@ -1843,7 +1885,7 @@ obj* l_io_println___at_io_println_x_27___spec__1(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_3; -x_2 = l___private_init_io_13__put__str___at_io_println_x_27___spec__3(x_0, x_1); +x_2 = l___private_init_io_1__put__str___at_io_println_x_27___spec__3(x_0, x_1); x_3 = lean::cnstr_get(x_2, 0); lean::inc(x_3); if (lean::obj_tag(x_3) == 0) @@ -1889,7 +1931,7 @@ x_14 = lean::cnstr_get(x_2, 1); lean::inc(x_14); lean::dec(x_2); x_17 = l_io_println___rarg___closed__1; -x_18 = l___private_init_io_13__put__str___at_io_println_x_27___spec__3(x_17, x_14); +x_18 = l___private_init_io_1__put__str___at_io_println_x_27___spec__3(x_17, x_14); return x_18; } } @@ -1919,11 +1961,11 @@ lean::cnstr_set(x_7, 1, x_3); return x_7; } } -obj* l___private_init_io_13__put__str___at_io_println_x_27___spec__3___boxed(obj* x_0, obj* x_1) { +obj* l___private_init_io_1__put__str___at_io_println_x_27___spec__3___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l___private_init_io_13__put__str___at_io_println_x_27___spec__3(x_0, x_1); +x_2 = l___private_init_io_1__put__str___at_io_println_x_27___spec__3(x_0, x_1); lean::dec(x_0); return x_2; } @@ -2172,6 +2214,8 @@ lean::mark_persistent(l_io_monad); lean::mark_persistent(l_io_error_has__to__string); l_io_error_inhabited = _init_l_io_error_inhabited(); lean::mark_persistent(l_io_error_inhabited); + l_io_prim_eio__inh___rarg___closed__1 = _init_l_io_prim_eio__inh___rarg___closed__1(); +lean::mark_persistent(l_io_prim_eio__inh___rarg___closed__1); l_io_println___rarg___closed__1 = _init_l_io_println___rarg___closed__1(); lean::mark_persistent(l_io_println___rarg___closed__1); l_eio_has__eval___rarg___closed__1 = _init_l_eio_has__eval___rarg___closed__1(); diff --git a/src/boot/init/lean/elaborator.cpp b/src/boot/init/lean/elaborator.cpp index 1de579d37b..11571cd521 100644 --- a/src/boot/init/lean/elaborator.cpp +++ b/src/boot/init/lean/elaborator.cpp @@ -312,7 +312,6 @@ obj* l_reader__t_bind___at_lean_elaborator_declaration_elaborate___spec__1___rar obj* l_lean_elaborator_mk__notation__kind(obj*, obj*); obj* l_rbnode_ins___main___at_lean_elaborator_ordered__rbmap_insert___spec__4(obj*, obj*, obj*); extern "C" obj* level_mk_imax(obj*, obj*); -obj* l_lean_environment_mk__empty___boxed(obj*); obj* l_lean_elaborator_ordered__rbmap_empty___at_lean_elaborator_old__elab__command___spec__15___boxed(obj*); obj* l_rbnode_ins___main___at_lean_elaborator_old__elab__command___spec__13___boxed(obj*, obj*, obj*, obj*); obj* l_lean_elaborator_attribute_elaborate___closed__2; @@ -752,14 +751,6 @@ obj* l_lean_elaborator_init__quot_elaborate___closed__1; obj* l_lean_elaborator_postprocess__notation__spec___closed__1; obj* l_lean_elaborator_mk__state___closed__1; extern obj* l_lean_parser_command_set__option_has__view; -obj* l_lean_environment_mk__empty___boxed(obj* x_0) { -_start: -{ -obj* x_1; -x_1 = lean_environment_mk_empty(x_0); -return x_1; -} -} obj* l_lean_environment_contains___boxed(obj* x_0, obj* x_1) { _start: { @@ -22636,7 +22627,7 @@ x_0 = lean::box(0); x_1 = lean::box(0); x_2 = lean::mk_string("command"); x_3 = lean_name_mk_string(x_1, x_2); -x_4 = lean::mk_string("constant"); +x_4 = lean::mk_string("axiom"); x_5 = lean_name_mk_string(x_1, x_4); x_6 = l_lean_kvmap_set__name(x_0, x_3, x_5); return x_6; @@ -22731,7 +22722,7 @@ lean::dec(x_17); x_34 = lean::cnstr_get(x_11, 0); lean::inc(x_34); lean::dec(x_11); -x_37 = lean::mk_nat_obj(5u); +x_37 = lean::mk_nat_obj(6u); x_38 = lean::alloc_closure(reinterpret_cast(l_lean_elaborator_elab__def__like___boxed), 7, 4); lean::closure_set(x_38, 0, x_0); lean::closure_set(x_38, 1, x_34); @@ -22779,7 +22770,7 @@ lean::cnstr_set(x_65, 1, x_46); lean::cnstr_set(x_65, 2, x_50); lean::cnstr_set(x_65, 3, x_60); lean::cnstr_set(x_65, 4, x_61); -x_66 = lean::mk_nat_obj(3u); +x_66 = lean::mk_nat_obj(4u); x_67 = lean::alloc_closure(reinterpret_cast(l_lean_elaborator_elab__def__like___boxed), 7, 4); lean::closure_set(x_67, 0, x_0); lean::closure_set(x_67, 1, x_43); @@ -22821,7 +22812,7 @@ lean::cnstr_set(x_90, 1, x_75); lean::cnstr_set(x_90, 2, x_89); lean::cnstr_set(x_90, 3, x_84); lean::cnstr_set(x_90, 4, x_85); -x_91 = lean::mk_nat_obj(2u); +x_91 = lean::mk_nat_obj(3u); x_92 = lean::alloc_closure(reinterpret_cast(l_lean_elaborator_elab__def__like___boxed), 7, 4); lean::closure_set(x_92, 0, x_0); lean::closure_set(x_92, 1, x_72); diff --git a/src/boot/init/lean/expander.cpp b/src/boot/init/lean/expander.cpp index 1e08d0bc23..c1742f66e4 100644 --- a/src/boot/init/lean/expander.cpp +++ b/src/boot/init/lean/expander.cpp @@ -39,7 +39,6 @@ obj* l_lean_expander_pi_transform___lambda__1(obj*, obj*, obj*); extern obj* l_lean_parser_term_binder__ident_has__view; obj* l_lean_expander_if_transform___closed__1; obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__4(uint8, obj*, obj*); -extern obj* l_lean_parser_command_constant_has__view; obj* l_lean_expander_coe__simple__binder__binders(obj*); obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__19(obj*, obj*); obj* l_lean_expander_assume_transform___boxed(obj*, obj*); @@ -89,7 +88,6 @@ obj* l_lean_parser_syntax_flip__scopes___main(obj*, obj*); obj* l_rbnode_ins___main___at_lean_expander_builtin__transformers___spec__4(obj*, obj*, obj*, obj*); obj* l_lean_expander_mixfix__to__notation__spec___boxed(obj*, obj*, obj*); obj* l_lean_expander_error___rarg___lambda__1___closed__1; -obj* l_lean_expander_constant_transform___boxed(obj*, obj*); obj* l_list_map___main___at_lean_expander_coe__binders__ext___spec__2___boxed(obj*); obj* l_lean_expander_assume_transform___closed__1; obj* l_list_foldr___main___at_lean_expander_expand__binders___spec__7(obj*, obj*, obj*); @@ -111,6 +109,7 @@ uint8 l_lean_parser_syntax_is__of__kind___main(obj*, obj*); obj* l_list_foldr___main___at_lean_expander_expand__binders___spec__8___boxed(obj*, obj*, obj*); obj* l_lean_expander_transform__m_monad; obj* l_lean_expander_expand__bracketed__binder___main___closed__4; +extern obj* l_lean_parser_command_axiom_has__view; obj* l_lean_expander_error___at___private_init_lean_expander_1__pop__stx__arg___spec__1___rarg___boxed(obj*, obj*, obj*, obj*); extern obj* l_lean_parser_command_variable_has__view; obj* l_lean_expander_arrow_transform___closed__1; @@ -126,6 +125,7 @@ obj* l_lean_expander_if_transform___closed__3; obj* l_lean_expander_if_transform___boxed(obj*, obj*); obj* l_lean_expander_expander__config_has__lift___boxed(obj*); extern obj* l_lean_parser_term_pi_has__view; +obj* l_list_map___main___at_lean_expander_axiom_transform___spec__1(obj*); extern obj* l_lean_parser_command_universe_has__view; obj* l_lean_expander_error___at_lean_expander_mk__notation__transformer___spec__1(obj*); extern obj* l_lean_parser_ident__univs; @@ -200,6 +200,7 @@ extern obj* l_lean_parser_term__parser__m_lean_parser_monad__parsec; obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__2(uint8, obj*, obj*); obj* l_lean_expander_error___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_expander_binding__annotation__update; +obj* l_lean_expander_axiom_transform___closed__1; extern obj* l_lean_parser_term__parser__m_monad; extern obj* l_lean_parser_term_let_has__view; obj* l_lean_expander_transform__m_monad__reader; @@ -230,6 +231,7 @@ obj* l_rbnode_ins___main___at_lean_expander_builtin__transformers___spec__5___bo obj* l_lean_expander_no__expansion(obj*); obj* l_lean_expander_binding__annotation__update_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_syntax_mk__node(obj*, obj*); +obj* l_lean_expander_axiom_transform(obj*, obj*); obj* l_lean_expander_declaration_transform___closed__2; obj* l_rbnode_balance2___main___rarg(obj*, obj*); obj* l_lean_expander_get__opt__type___main(obj*); @@ -275,6 +277,7 @@ extern "C" uint8 lean_name_dec_eq(obj*, obj*); obj* l_lean_expander_error___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__18(obj*, obj*); obj* l_lean_expander_declaration_transform___closed__1; +obj* l_lean_expander_axiom_transform___boxed(obj*, obj*); obj* l_lean_expander_error___at_lean_expander_mk__notation__transformer___spec__1___boxed(obj*); uint8 l_lean_name_quick__lt(obj*, obj*); obj* l_lean_expander_coe__binders__ext__binders(obj*); @@ -291,6 +294,7 @@ obj* l_list_foldr___main___at_lean_expander_expand__binders___spec__4___boxed(ob obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__15(obj*, obj*); obj* l_lean_expander_binder__ident__to__ident___main___boxed(obj*); obj* l_lean_expander_transformer__config__coe__frontend__config(obj*); +extern obj* l_lean_parser_command_axiom; obj* l_lean_expander_expand__bracketed__binder___main(obj*, obj*); obj* l_lean_expander_binding__annotation__update_has__view_x_27___lambda__1(obj*); obj* l_string_trim(obj*); @@ -298,7 +302,6 @@ obj* l_lean_expander_variable_transform___closed__1; obj* l_list_map___main___at_lean_expander_mk__notation__transformer___spec__5(obj*); obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__13(obj*, obj*); obj* l_lean_expander_error___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*); -extern obj* l_lean_parser_command_constant; obj* l_lean_expander_paren_transform___closed__2; extern obj* l_lean_parser_term_if; extern obj* l_lean_parser_term_assume; @@ -314,7 +317,6 @@ obj* l___private_init_lean_expander_2__expand__core___main(obj*, obj*, obj*, obj obj* l_lean_expander_assume_transform(obj*, obj*); obj* l_lean_parser_syntax_mreplace___main___at_lean_parser_syntax_replace___spec__1(obj*, obj*); obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__17(obj*, obj*); -obj* l_list_map___main___at_lean_expander_constant_transform___spec__1(obj*); obj* l_lean_expander_mk__simple__binder___closed__1; extern obj* l_lean_parser_command_notation__spec_precedence_has__view; obj* l_lean_expander_variable_transform(obj*, obj*); @@ -349,7 +351,6 @@ obj* l_list_foldr___main___at_lean_expander_expand__binders___spec__5(obj*, obj* obj* l_dlist_singleton___rarg(obj*, obj*); obj* l_lean_expander_get__opt__type___main___closed__1; obj* l_list_mfoldr___main___at_lean_expander_expand__binders___spec__9___closed__3; -obj* l_lean_expander_constant_transform___closed__1; obj* l_lean_expander_mixfix__to__notation__spec___closed__4; obj* l_lean_parser_combinators_node___at_lean_parser_command_notation__spec_precedence__lit_parser___spec__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__1___boxed(obj*, obj*, obj*); @@ -373,7 +374,6 @@ obj* l_list_map___main___at___private_init_lean_expander_2__expand__core___main_ obj* l_list_mmap___main___at_lean_expander_variables_transform___spec__1(obj*, obj*); obj* l_id_monad___lambda__3___boxed(obj*, obj*, obj*, obj*); obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__4___boxed(obj*, obj*, obj*); -obj* l_lean_expander_constant_transform(obj*, obj*); obj* l_lean_expander_binder__ident__to__ident___boxed(obj*); obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__11(obj*, obj*); obj* l_rbnode_set__black___main___rarg(obj*); @@ -8886,7 +8886,7 @@ lean::dec(x_1); return x_2; } } -obj* l_list_map___main___at_lean_expander_constant_transform___spec__1(obj* x_0) { +obj* l_list_map___main___at_lean_expander_axiom_transform___spec__1(obj* x_0) { _start: { if (lean::obj_tag(x_0) == 0) @@ -8910,7 +8910,7 @@ if (lean::is_exclusive(x_0)) { } x_7 = lean::alloc_cnstr(0, 1, 0); lean::cnstr_set(x_7, 0, x_2); -x_8 = l_list_map___main___at_lean_expander_constant_transform___spec__1(x_4); +x_8 = l_list_map___main___at_lean_expander_axiom_transform___spec__1(x_4); if (lean::is_scalar(x_6)) { x_9 = lean::alloc_cnstr(1, 2, 0); } else { @@ -8922,7 +8922,7 @@ return x_9; } } } -obj* _init_l_lean_expander_constant_transform___closed__1() { +obj* _init_l_lean_expander_axiom_transform___closed__1() { _start: { obj* x_0; obj* x_1; @@ -8932,11 +8932,11 @@ lean::cnstr_set(x_1, 0, x_0); return x_1; } } -obj* l_lean_expander_constant_transform(obj* x_0, obj* x_1) { +obj* l_lean_expander_axiom_transform(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_3; obj* x_5; obj* x_6; obj* x_8; -x_2 = l_lean_parser_command_constant_has__view; +x_2 = l_lean_parser_command_axiom_has__view; x_3 = lean::cnstr_get(x_2, 0); lean::inc(x_3); x_5 = lean::apply_1(x_3, x_0); @@ -8960,7 +8960,7 @@ x_13 = lean::cnstr_get(x_8, 0); lean::inc(x_13); lean::dec(x_8); x_16 = lean::box(0); -x_17 = l_list_map___main___at_lean_expander_constant_transform___spec__1(x_13); +x_17 = l_list_map___main___at_lean_expander_axiom_transform___spec__1(x_13); x_18 = lean::alloc_cnstr(1, 1, 0); lean::cnstr_set(x_18, 0, x_17); x_19 = lean::alloc_cnstr(1, 1, 0); @@ -9003,7 +9003,7 @@ x_41 = l_lean_expander_mk__simple__binder___closed__1; x_42 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_42, 0, x_41); lean::cnstr_set(x_42, 1, x_40); -x_43 = l_lean_expander_constant_transform___closed__1; +x_43 = l_lean_expander_axiom_transform___closed__1; if (lean::is_scalar(x_12)) { x_44 = lean::alloc_cnstr(0, 2, 0); } else { @@ -9037,11 +9037,11 @@ return x_52; } } } -obj* l_lean_expander_constant_transform___boxed(obj* x_0, obj* x_1) { +obj* l_lean_expander_axiom_transform___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_lean_expander_constant_transform(x_0, x_1); +x_2 = l_lean_expander_axiom_transform(x_0, x_1); lean::dec(x_1); return x_2; } @@ -9535,7 +9535,7 @@ lean::cnstr_set(x_51, 0, x_50); lean::cnstr_set(x_51, 1, x_49); x_52 = lean::alloc_cnstr(1, 1, 0); lean::cnstr_set(x_52, 0, x_51); -x_53 = l_lean_expander_constant_transform___closed__1; +x_53 = l_lean_expander_axiom_transform___closed__1; if (lean::is_scalar(x_12)) { x_54 = lean::alloc_cnstr(0, 2, 0); } else { @@ -11041,8 +11041,8 @@ x_28 = lean::alloc_closure(reinterpret_cast(l_lean_expander_let_transform x_29 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_29, 0, x_27); lean::cnstr_set(x_29, 1, x_28); -x_30 = l_lean_parser_command_constant; -x_31 = lean::alloc_closure(reinterpret_cast(l_lean_expander_constant_transform___boxed), 2, 0); +x_30 = l_lean_parser_command_axiom; +x_31 = lean::alloc_closure(reinterpret_cast(l_lean_expander_axiom_transform___boxed), 2, 0); x_32 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_32, 0, x_30); lean::cnstr_set(x_32, 1, x_31); @@ -12134,8 +12134,8 @@ lean::mark_persistent(l_lean_expander_if_transform___closed__2); lean::mark_persistent(l_lean_expander_if_transform___closed__3); l_lean_expander_let_transform___closed__1 = _init_l_lean_expander_let_transform___closed__1(); lean::mark_persistent(l_lean_expander_let_transform___closed__1); - l_lean_expander_constant_transform___closed__1 = _init_l_lean_expander_constant_transform___closed__1(); -lean::mark_persistent(l_lean_expander_constant_transform___closed__1); + l_lean_expander_axiom_transform___closed__1 = _init_l_lean_expander_axiom_transform___closed__1(); +lean::mark_persistent(l_lean_expander_axiom_transform___closed__1); l_lean_expander_declaration_transform___closed__1 = _init_l_lean_expander_declaration_transform___closed__1(); lean::mark_persistent(l_lean_expander_declaration_transform___closed__1); l_lean_expander_declaration_transform___closed__2 = _init_l_lean_expander_declaration_transform___closed__2(); diff --git a/src/boot/init/lean/frontend.cpp b/src/boot/init/lean/frontend.cpp index 15030b52d8..5efe06851e 100644 --- a/src/boot/init/lean/frontend.cpp +++ b/src/boot/init/lean/frontend.cpp @@ -14,7 +14,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-label" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif -obj* l___private_init_io_13__put__str___at_lean_process__file___spec__3___boxed(obj*, obj*); +obj* l___private_init_io_1__put__str___at_lean_process__file___spec__3(obj*, obj*); obj* l_io_prim_iterate__aux___rarg(obj*, obj*, obj*, obj*); obj* l_list_mmap_x_27___main___at_lean_run__frontend___spec__2(obj*, obj*, obj*); obj* l_lean_run__frontend___boxed(obj*, obj*, obj*, obj*, obj*); @@ -56,7 +56,6 @@ obj* l_lean_parser_tokens___rarg(obj*); extern obj* l_lean_parser_module_eoi; obj* l_io_println___at_lean_process__file___spec__1___boxed(obj*, obj*); extern obj* l_lean_format_be___main___closed__1; -obj* l___private_init_io_13__put__str___at_lean_process__file___spec__3(obj*, obj*); obj* l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__1___boxed(obj*, obj*, obj*); obj* l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__4___closed__2; obj* l_io_print___at_lean_process__file___spec__2___boxed(obj*, obj*); @@ -70,6 +69,7 @@ obj* l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__2___boxed(obj obj* l_lean_message_to__string(obj*); obj* l_lean_process__file___lambda__1___closed__7; obj* l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__4___closed__3; +obj* l___private_init_io_1__put__str___at_lean_process__file___spec__3___boxed(obj*, obj*); obj* l_lean_file__map_from__string(obj*); extern obj* l_lean_parser_module_header_parser_lean_parser_has__tokens; obj* l_lean_process__file___boxed(obj*, obj*, obj*, obj*); @@ -1766,7 +1766,7 @@ x_6 = l_lean_run__frontend(x_0, x_1, x_2, x_5, x_4); return x_6; } } -obj* l___private_init_io_13__put__str___at_lean_process__file___spec__3(obj* x_0, obj* x_1) { +obj* l___private_init_io_1__put__str___at_lean_process__file___spec__3(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_3; @@ -1849,7 +1849,7 @@ obj* l_io_print___at_lean_process__file___spec__2(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l___private_init_io_13__put__str___at_lean_process__file___spec__3(x_0, x_1); +x_2 = l___private_init_io_1__put__str___at_lean_process__file___spec__3(x_0, x_1); return x_2; } } @@ -1857,7 +1857,7 @@ obj* l_io_println___at_lean_process__file___spec__1(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_3; -x_2 = l___private_init_io_13__put__str___at_lean_process__file___spec__3(x_0, x_1); +x_2 = l___private_init_io_1__put__str___at_lean_process__file___spec__3(x_0, x_1); x_3 = lean::cnstr_get(x_2, 0); lean::inc(x_3); if (lean::obj_tag(x_3) == 0) @@ -1903,7 +1903,7 @@ x_14 = lean::cnstr_get(x_2, 1); lean::inc(x_14); lean::dec(x_2); x_17 = l_lean_format_be___main___closed__1; -x_18 = l___private_init_io_13__put__str___at_lean_process__file___spec__3(x_17, x_14); +x_18 = l___private_init_io_1__put__str___at_lean_process__file___spec__3(x_17, x_14); return x_18; } } @@ -2243,11 +2243,11 @@ return x_58; } } } -obj* l___private_init_io_13__put__str___at_lean_process__file___spec__3___boxed(obj* x_0, obj* x_1) { +obj* l___private_init_io_1__put__str___at_lean_process__file___spec__3___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l___private_init_io_13__put__str___at_lean_process__file___spec__3(x_0, x_1); +x_2 = l___private_init_io_1__put__str___at_lean_process__file___spec__3(x_0, x_1); lean::dec(x_0); return x_2; } diff --git a/src/boot/init/lean/parser/declaration.cpp b/src/boot/init/lean/parser/declaration.cpp index 58bcab9038..9d264e7509 100644 --- a/src/boot/init/lean/parser/declaration.cpp +++ b/src/boot/init/lean/parser/declaration.cpp @@ -31,7 +31,6 @@ obj* l_list_map___main___rarg(obj*, obj*); obj* l_lean_parser_command_ident__univ__params_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_infer__modifier_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_decl__attributes_has__view_x_27; -obj* l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__4; obj* l_lean_parser_command_old__univ__params_parser___closed__1; obj* l_lean_parser_command_declaration_parser_lean_parser_has__view___lambda__1(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_struct__binder__content_has__view_x_27___lambda__1___closed__1; @@ -50,7 +49,6 @@ obj* l_reader__t_bind___at_lean_parser_command_doc__comment_parser_lean_parser_h obj* l_lean_parser_command_equation_has__view_x_27___lambda__1(obj*); obj* l_list_map___main___at_lean_parser_command_equation_has__view_x_27___spec__2(obj*); obj* l_lean_parser_monad__parsec_many1__aux_x_27___main___at_lean_parser_command_doc__comment_parser_lean_parser_has__view___spec__3___boxed(obj*, obj*, obj*, obj*, obj*, obj*); -obj* l_lean_parser_command_constant_has__view; obj* l___private_init_lean_parser_token_4__ident_x_27(obj*, obj*, obj*); obj* l_lean_parser_command_inductive_has__view_x_27___lambda__1___closed__3; extern obj* l_lean_parser_ident_parser___at_lean_parser_command_notation__spec_fold__action_parser_lean_parser_has__tokens___spec__4___rarg___closed__1; @@ -97,6 +95,7 @@ obj* l_lean_parser_command_struct__binder__content_has__view_x_27___lambda__1___ obj* l_lean_parser_command_infer__modifier_parser_lean_parser_has__tokens; obj* l_lean_parser_with__trailing___rarg___lambda__1(obj*, obj*); obj* l_lean_parser_command_structure__field__block; +obj* l_lean_parser_command_axiom_has__view_x_27; obj* l_lean_parser_combinators_sep__by1_tokens___rarg(obj*, obj*); obj* l_lean_parser_command_declaration_parser___closed__1; obj* l_lean_parser_command_decl__attributes_has__view_x_27___lambda__1___closed__1; @@ -163,6 +162,7 @@ obj* l_string_quote(obj*); obj* l_lean_parser_command_old__univ__params_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_simple__decl__val_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_decl__val_has__view_x_27___lambda__1(obj*); +obj* l_lean_parser_command_axiom_has__view; extern obj* l_lean_parser_monad__parsec_eoi__error___rarg___closed__1; obj* l_lean_parser_command_instance_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_command_example; @@ -206,7 +206,6 @@ extern obj* l_lean_parser_command_notation__like_parser_lean_parser_has__tokens; obj* l_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens; obj* l_lean_parser_command_intro__rule_has__view; obj* l_lean_parser_command_structure_has__view_x_27; -obj* l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__2; obj* l_lean_parser_command_structure_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_strict__implicit__binder_has__view_x_27; obj* l_lean_parser_monad__parsec_many_x_27___at_lean_parser_command_doc__comment_parser_lean_parser_has__tokens___spec__9(obj*, obj*, obj*, obj*, obj*); @@ -225,7 +224,6 @@ obj* l_lean_parser_command_attr__instance_has__view_x_27___lambda__1___closed__3 obj* l_lean_parser_monad__parsec_many1__aux_x_27___main___at_lean_parser_command_doc__comment_parser___spec__3(obj*, obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_combinators_3__sep__by_view__aux___main___at_lean_parser_command_decl__attributes_has__view_x_27___spec__1(obj*, obj*, obj*); obj* l_lean_parser_command_decl__val_has__view_x_27___lambda__2___closed__2; -obj* l_lean_parser_command_constant_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_parsec__t_lookahead___at_lean_parser_command_doc__comment_parser___spec__1___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_command_doc__comment_parser_lean_parser_has__tokens___spec__4___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_intro__rule_has__view_x_27___lambda__1___closed__2; @@ -239,7 +237,6 @@ obj* l_lean_parser_command_structure__ctor_has__view; extern obj* l_lean_parser_detail__ident__part_has__view_x_27___lambda__2___closed__1; obj* l_lean_parser_command_extends; obj* l_lean_parser_command_opt__decl__sig_has__view_x_27___lambda__2(obj*); -obj* l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; obj* l_lean_parser_command_attr__instance_parser_lean_parser_has__view; obj* l_lean_parser_command_instance_has__view_x_27___lambda__1(obj*); obj* l___private_init_lean_parser_parsec_1__str__aux___main(obj*, obj*, obj*); @@ -282,7 +279,7 @@ obj* l_lean_parser_command_intro__rule_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_opt__decl__sig_parser(obj*, obj*, obj*, obj*); obj* l_lean_parser_command_attr__instance_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_command_simple__decl__val_has__view; -obj* l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__1; +obj* l_lean_parser_command_axiom_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_relaxed__infer__modifier_has__view; obj* l_lean_parser_command_decl__sig_has__view; obj* l_lean_parser_command_decl__val_has__view; @@ -314,7 +311,6 @@ obj* l_lean_parser_command_decl__modifiers_parser_lean_parser_has__view; obj* l_lean_parser_command_opt__decl__sig_has__view; obj* l_lean_parser_command_extends_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_command_univ__params_has__view_x_27; -obj* l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_command_intro__rule_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_command_decl__val_parser___closed__1; obj* l_lean_parser_command_intro__rule_has__view_x_27; @@ -409,13 +405,13 @@ obj* l_lean_parser_command_decl__sig_has__view_x_27___lambda__1___closed__3; namespace lean { uint8 string_dec_eq(obj*, obj*); } -obj* l_lean_parser_command_constant_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_attr__instance_has__view; obj* l_lean_parser_command_intro__rule_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_decl__sig_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_structure_has__view_x_27___lambda__2___closed__1; obj* l_lean_parser_command_doc__comment_parser___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_list_map___main___at_lean_parser_command_struct__binder__content_has__view_x_27___spec__1(obj*); +obj* l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_equation_has__view_x_27; obj* l_lean_parser_command_decl__val; extern obj* l_lean_parser_combinators_choice__aux___main___rarg___closed__1; @@ -433,7 +429,6 @@ obj* l_lean_parser_command_struct__explicit__binder_has__view_x_27___lambda__1(o obj* l_list_map___main___at_lean_parser_command_attr__instance_has__view_x_27___spec__5(obj*); obj* l_string_mk__iterator(obj*); obj* l_lean_parser_command_decl__attributes_has__view_x_27___lambda__1___closed__3; -obj* l_lean_parser_command_constant_has__view_x_27; obj* l_lean_parser_command_strict__infer__modifier_has__view_x_27; obj* l_list_map___main___at_lean_parser_command_attr__instance_has__view_x_27___spec__2(obj*); obj* l_lean_parser_term__parser__command__parser__coe(obj*, obj*, obj*, obj*, obj*); @@ -442,6 +437,8 @@ obj* l_lean_parser_command_equation_parser(obj*, obj*, obj*, obj*); obj* l_lean_parser_command_inductive_has__view_x_27; obj* l_lean_parser_command_old__univ__params_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_decl__sig_parser_lean_parser_has__view; +obj* l_lean_parser_command_axiom_has__view_x_27___lambda__1(obj*); +obj* l_lean_parser_command_axiom; obj* l_lean_parser_command_old__univ__params_has__view_x_27; obj* l_lean_parser_command_inductive_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_command_visibility_has__view_x_27___lambda__1___closed__2; @@ -454,7 +451,6 @@ obj* l_lean_parser_command_structure__kw_has__view; obj* l_lean_parser_command_structure__field__block_parser___closed__1; obj* l_lean_parser_command_declaration_parser_lean_parser_has__tokens; obj* l_lean_parser_command_def__like_kind_has__view_x_27; -obj* l_lean_parser_command_constant; obj* l_lean_parser_command_strict__infer__modifier_has__view_x_27___lambda__2___closed__1; obj* l_list_map___main___at_lean_parser_command_attr__instance_has__view_x_27___spec__1(obj*); uint32 l_string_iterator_curr___main(obj*); @@ -491,6 +487,7 @@ obj* l_lean_parser_command_doc__comment_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_decl__sig_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_struct__explicit__binder_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_struct__implicit__binder_has__view_x_27___lambda__1(obj*); +obj* l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_command_inst__implicit__binder_has__view; obj* l_lean_parser_command_strict__infer__modifier_has__view; obj* l_lean_parser_command_def__like_kind; @@ -26715,32 +26712,12 @@ return x_8; obj* _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1() { _start: { -obj* x_0; obj* x_1; -x_0 = lean::box(0); -x_1 = lean::alloc_cnstr(1, 1, 0); -lean::cnstr_set(x_1, 0, x_0); -return x_1; -} -} -obj* _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__2() { -_start: -{ -obj* x_0; obj* x_1; -x_0 = lean::box(0); -x_1 = lean::alloc_cnstr(0, 1, 0); -lean::cnstr_set(x_1, 0, x_0); -return x_1; -} -} -obj* _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3() { -_start: -{ obj* x_0; -x_0 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__2; +x_0 = lean::box(0); return x_0; } } -obj* _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__4() { +obj* _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__2() { _start: { obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; @@ -26764,7 +26741,7 @@ x_1 = l_lean_parser_syntax_as__node___main(x_0); if (lean::obj_tag(x_1) == 0) { obj* x_2; -x_2 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; +x_2 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; return x_2; } else @@ -26778,14 +26755,14 @@ lean::inc(x_6); x_8 = lean::cnstr_get(x_3, 1); lean::inc(x_8); lean::dec(x_3); -x_11 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__4; +x_11 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__2; x_12 = lean_name_dec_eq(x_6, x_11); lean::dec(x_6); if (x_12 == 0) { obj* x_15; lean::dec(x_8); -x_15 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; +x_15 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; return x_15; } else @@ -26793,7 +26770,7 @@ else if (lean::obj_tag(x_8) == 0) { obj* x_16; -x_16 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; +x_16 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; return x_16; } else @@ -26811,7 +26788,7 @@ x_22 = l_lean_parser_syntax_as__node___main(x_19); if (lean::obj_tag(x_22) == 0) { obj* x_23; -x_23 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; +x_23 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; return x_23; } else @@ -26834,7 +26811,7 @@ case 0: obj* x_31; lean::dec(x_26); lean::dec(x_24); -x_31 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; +x_31 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; return x_31; } case 1: @@ -26843,138 +26820,89 @@ obj* x_35; lean::dec(x_26); lean::dec(x_27); lean::dec(x_24); -x_35 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; +x_35 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; return x_35; } default: { -obj* x_36; obj* x_39; obj* x_41; obj* x_44; uint8 x_45; +obj* x_36; obj* x_39; obj* x_42; uint8 x_43; x_36 = lean::cnstr_get(x_24, 1); lean::inc(x_36); lean::dec(x_24); x_39 = lean::cnstr_get(x_27, 0); lean::inc(x_39); -x_41 = lean::cnstr_get(x_27, 1); -lean::inc(x_41); lean::dec(x_27); -x_44 = lean::box(0); -x_45 = lean_name_dec_eq(x_39, x_44); +x_42 = lean::box(0); +x_43 = lean_name_dec_eq(x_39, x_42); lean::dec(x_39); -if (x_45 == 0) +if (x_43 == 0) { -obj* x_50; +obj* x_47; lean::dec(x_26); -lean::dec(x_41); lean::dec(x_36); -x_50 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; -return x_50; +x_47 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; +return x_47; } else { if (lean::obj_tag(x_36) == 0) { -obj* x_53; +obj* x_49; lean::dec(x_26); -lean::dec(x_41); -x_53 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; -return x_53; +x_49 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; +return x_49; } else { -obj* x_54; -x_54 = lean::cnstr_get(x_36, 1); -lean::inc(x_54); -if (lean::obj_tag(x_54) == 0) +obj* x_50; +x_50 = lean::cnstr_get(x_36, 1); +lean::inc(x_50); +if (lean::obj_tag(x_50) == 0) { -obj* x_56; obj* x_59; uint8 x_60; -x_56 = lean::cnstr_get(x_36, 0); -lean::inc(x_56); +obj* x_52; +x_52 = lean::cnstr_get(x_36, 0); +lean::inc(x_52); lean::dec(x_36); -x_59 = lean::mk_nat_obj(0u); -x_60 = lean::nat_dec_eq(x_41, x_59); -lean::dec(x_41); -if (x_60 == 0) -{ -switch (lean::obj_tag(x_56)) { +switch (lean::obj_tag(x_52)) { case 0: { -obj* x_62; obj* x_65; obj* x_66; -x_62 = lean::cnstr_get(x_56, 0); -lean::inc(x_62); -lean::dec(x_56); +obj* x_55; obj* x_58; +x_55 = lean::cnstr_get(x_52, 0); +lean::inc(x_55); +lean::dec(x_52); if (lean::is_scalar(x_26)) { - x_65 = lean::alloc_cnstr(1, 1, 0); + x_58 = lean::alloc_cnstr(1, 1, 0); } else { - x_65 = x_26; + x_58 = x_26; } -lean::cnstr_set(x_65, 0, x_62); -x_66 = lean::alloc_cnstr(1, 1, 0); -lean::cnstr_set(x_66, 0, x_65); -return x_66; +lean::cnstr_set(x_58, 0, x_55); +return x_58; } case 3: { -obj* x_68; +obj* x_60; lean::dec(x_26); -x_68 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; -return x_68; +x_60 = lean::box(0); +return x_60; } default: { -obj* x_71; -lean::dec(x_56); +obj* x_63; lean::dec(x_26); -x_71 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; -return x_71; +lean::dec(x_52); +x_63 = lean::box(0); +return x_63; } } } else { -switch (lean::obj_tag(x_56)) { -case 0: -{ -obj* x_72; obj* x_75; obj* x_76; -x_72 = lean::cnstr_get(x_56, 0); -lean::inc(x_72); -lean::dec(x_56); -if (lean::is_scalar(x_26)) { - x_75 = lean::alloc_cnstr(1, 1, 0); -} else { - x_75 = x_26; -} -lean::cnstr_set(x_75, 0, x_72); -x_76 = lean::alloc_cnstr(0, 1, 0); -lean::cnstr_set(x_76, 0, x_75); -return x_76; -} -case 3: -{ -obj* x_78; +obj* x_67; +lean::dec(x_50); lean::dec(x_26); -x_78 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__2; -return x_78; -} -default: -{ -obj* x_81; -lean::dec(x_56); -lean::dec(x_26); -x_81 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__2; -return x_81; -} -} -} -} -else -{ -obj* x_86; -lean::dec(x_26); -lean::dec(x_41); -lean::dec(x_54); lean::dec(x_36); -x_86 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; -return x_86; +x_67 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; +return x_67; } } } @@ -26984,11 +26912,11 @@ return x_86; } else { -obj* x_89; +obj* x_70; lean::dec(x_8); lean::dec(x_17); -x_89 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3; -return x_89; +x_70 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; +return x_70; } } } @@ -27018,127 +26946,49 @@ x_11 = l_lean_parser_syntax_mk__node(x_10, x_9); return x_11; } } -obj* _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__2() { -_start: -{ -obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; -x_0 = lean::box(0); -x_1 = lean::box(0); -x_2 = lean::mk_nat_obj(1u); -x_3 = lean_name_mk_numeral(x_1, x_2); -x_4 = lean::box(0); -x_5 = lean::box(3); -x_6 = l_option_get__or__else___main___rarg(x_4, x_5); -x_7 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_7, 0, x_6); -lean::cnstr_set(x_7, 1, x_0); -x_8 = l_lean_parser_syntax_mk__node(x_3, x_7); -x_9 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_9, 0, x_8); -lean::cnstr_set(x_9, 1, x_0); -x_10 = l_lean_parser_command_constant__keyword; -x_11 = l_lean_parser_syntax_mk__node(x_10, x_9); -return x_11; -} -} obj* l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2(obj* x_0) { _start: { -obj* x_1; -x_1 = lean::box(0); if (lean::obj_tag(x_0) == 0) { -obj* x_2; +obj* x_1; +x_1 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__1; +return x_1; +} +else +{ +obj* x_2; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; x_2 = lean::cnstr_get(x_0, 0); -lean::inc(x_2); -lean::dec(x_0); -if (lean::obj_tag(x_2) == 0) -{ -obj* x_5; -x_5 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__1; -return x_5; -} -else -{ -obj* x_6; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; -x_6 = lean::cnstr_get(x_2, 0); -if (lean::is_exclusive(x_2)) { - x_8 = x_2; +if (lean::is_exclusive(x_0)) { + x_4 = x_0; } else { - lean::inc(x_6); - lean::dec(x_2); - x_8 = lean::box(0); + lean::inc(x_2); + lean::dec(x_0); + x_4 = lean::box(0); } -x_9 = lean::alloc_cnstr(0, 1, 0); -lean::cnstr_set(x_9, 0, x_6); -if (lean::is_scalar(x_8)) { - x_10 = lean::alloc_cnstr(1, 1, 0); +x_5 = lean::box(0); +x_6 = lean::alloc_cnstr(0, 1, 0); +lean::cnstr_set(x_6, 0, x_2); +if (lean::is_scalar(x_4)) { + x_7 = lean::alloc_cnstr(1, 1, 0); } else { - x_10 = x_8; + x_7 = x_4; } -lean::cnstr_set(x_10, 0, x_9); -x_11 = lean::box(3); -x_12 = l_option_get__or__else___main___rarg(x_10, x_11); -lean::dec(x_10); +lean::cnstr_set(x_7, 0, x_6); +x_8 = lean::box(3); +x_9 = l_option_get__or__else___main___rarg(x_7, x_8); +lean::dec(x_7); +x_11 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_11, 0, x_9); +lean::cnstr_set(x_11, 1, x_5); +x_12 = l_lean_parser_detail__ident__part_has__view_x_27___lambda__2___closed__1; +x_13 = l_lean_parser_syntax_mk__node(x_12, x_11); x_14 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_14, 0, x_12); -lean::cnstr_set(x_14, 1, x_1); -x_15 = l_lean_parser_detail__ident__part_has__view_x_27___lambda__2___closed__1; +lean::cnstr_set(x_14, 0, x_13); +lean::cnstr_set(x_14, 1, x_5); +x_15 = l_lean_parser_command_constant__keyword; x_16 = l_lean_parser_syntax_mk__node(x_15, x_14); -x_17 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_17, 0, x_16); -lean::cnstr_set(x_17, 1, x_1); -x_18 = l_lean_parser_command_constant__keyword; -x_19 = l_lean_parser_syntax_mk__node(x_18, x_17); -return x_19; -} -} -else -{ -obj* x_20; -x_20 = lean::cnstr_get(x_0, 0); -lean::inc(x_20); -lean::dec(x_0); -if (lean::obj_tag(x_20) == 0) -{ -obj* x_23; -x_23 = l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__2; -return x_23; -} -else -{ -obj* x_24; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; -x_24 = lean::cnstr_get(x_20, 0); -if (lean::is_exclusive(x_20)) { - x_26 = x_20; -} else { - lean::inc(x_24); - lean::dec(x_20); - x_26 = lean::box(0); -} -x_27 = lean::alloc_cnstr(0, 1, 0); -lean::cnstr_set(x_27, 0, x_24); -if (lean::is_scalar(x_26)) { - x_28 = lean::alloc_cnstr(1, 1, 0); -} else { - x_28 = x_26; -} -lean::cnstr_set(x_28, 0, x_27); -x_29 = lean::box(3); -x_30 = l_option_get__or__else___main___rarg(x_28, x_29); -lean::dec(x_28); -x_32 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_32, 0, x_30); -lean::cnstr_set(x_32, 1, x_1); -x_33 = l_lean_parser_detail__ident__part_has__view_x_27___lambda__2___closed__3; -x_34 = l_lean_parser_syntax_mk__node(x_33, x_32); -x_35 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_35, 0, x_34); -lean::cnstr_set(x_35, 1, x_1); -x_36 = l_lean_parser_command_constant__keyword; -x_37 = l_lean_parser_syntax_mk__node(x_36, x_35); -return x_37; -} +return x_16; } } } @@ -27162,7 +27012,7 @@ x_0 = l_lean_parser_command_constant__keyword_has__view_x_27; return x_0; } } -obj* _init_l_lean_parser_command_constant() { +obj* _init_l_lean_parser_command_axiom() { _start: { obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; @@ -27173,12 +27023,12 @@ x_3 = lean::mk_string("parser"); x_4 = lean_name_mk_string(x_2, x_3); x_5 = lean::mk_string("command"); x_6 = lean_name_mk_string(x_4, x_5); -x_7 = lean::mk_string("constant"); +x_7 = lean::mk_string("axiom"); x_8 = lean_name_mk_string(x_6, x_7); return x_8; } } -obj* _init_l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__1() { +obj* _init_l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__1() { _start: { obj* x_0; obj* x_1; obj* x_4; obj* x_5; @@ -27191,7 +27041,7 @@ x_5 = lean::apply_1(x_1, x_4); return x_5; } } -obj* _init_l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__2() { +obj* _init_l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__2() { _start: { obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; @@ -27201,7 +27051,7 @@ lean::inc(x_1); lean::dec(x_0); x_4 = lean::box(3); x_5 = lean::apply_1(x_1, x_4); -x_6 = l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__1; +x_6 = l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__1; x_7 = l_lean_parser_command_instance_has__view_x_27___lambda__1___closed__1; x_8 = lean::alloc_cnstr(0, 3, 0); lean::cnstr_set(x_8, 0, x_5); @@ -27210,7 +27060,7 @@ lean::cnstr_set(x_8, 2, x_7); return x_8; } } -obj* l_lean_parser_command_constant_has__view_x_27___lambda__1(obj* x_0) { +obj* l_lean_parser_command_axiom_has__view_x_27___lambda__1(obj* x_0) { _start: { obj* x_1; obj* x_2; obj* x_4; @@ -27218,7 +27068,7 @@ x_4 = l_lean_parser_syntax_as__node___main(x_0); if (lean::obj_tag(x_4) == 0) { obj* x_5; -x_5 = l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__2; +x_5 = l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__2; return x_5; } else @@ -27264,7 +27114,7 @@ if (lean::obj_tag(x_1) == 0) if (lean::obj_tag(x_1) == 0) { obj* x_23; obj* x_24; obj* x_25; -x_23 = l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__1; +x_23 = l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__1; x_24 = l_lean_parser_command_instance_has__view_x_27___lambda__1___closed__1; x_25 = lean::alloc_cnstr(0, 3, 0); lean::cnstr_set(x_25, 0, x_22); @@ -27283,7 +27133,7 @@ x_30 = lean::cnstr_get(x_29, 0); lean::inc(x_30); lean::dec(x_29); x_33 = lean::apply_1(x_30, x_26); -x_34 = l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__1; +x_34 = l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__1; x_35 = lean::alloc_cnstr(0, 3, 0); lean::cnstr_set(x_35, 0, x_22); lean::cnstr_set(x_35, 1, x_34); @@ -27335,7 +27185,7 @@ return x_56; } } } -obj* l_lean_parser_command_constant_has__view_x_27___lambda__2(obj* x_0) { +obj* l_lean_parser_command_axiom_has__view_x_27___lambda__2(obj* x_0) { _start: { obj* x_1; obj* x_3; obj* x_5; obj* x_8; obj* x_9; obj* x_12; obj* x_13; obj* x_14; obj* x_17; obj* x_18; obj* x_19; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; @@ -27371,28 +27221,28 @@ lean::cnstr_set(x_25, 1, x_24); x_26 = lean::alloc_cnstr(1, 2, 0); lean::cnstr_set(x_26, 0, x_12); lean::cnstr_set(x_26, 1, x_25); -x_27 = l_lean_parser_command_constant; +x_27 = l_lean_parser_command_axiom; x_28 = l_lean_parser_syntax_mk__node(x_27, x_26); return x_28; } } -obj* _init_l_lean_parser_command_constant_has__view_x_27() { +obj* _init_l_lean_parser_command_axiom_has__view_x_27() { _start: { obj* x_0; obj* x_1; obj* x_2; -x_0 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_constant_has__view_x_27___lambda__1), 1, 0); -x_1 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_constant_has__view_x_27___lambda__2), 1, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_axiom_has__view_x_27___lambda__1), 1, 0); +x_1 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_axiom_has__view_x_27___lambda__2), 1, 0); x_2 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_2, 0, x_0); lean::cnstr_set(x_2, 1, x_1); return x_2; } } -obj* _init_l_lean_parser_command_constant_has__view() { +obj* _init_l_lean_parser_command_axiom_has__view() { _start: { obj* x_0; -x_0 = l_lean_parser_command_constant_has__view_x_27; +x_0 = l_lean_parser_command_axiom_has__view_x_27; return x_0; } } @@ -28920,7 +28770,7 @@ else { obj* x_79; obj* x_80; obj* x_83; obj* x_84; lean::dec(x_39); -x_79 = l_lean_parser_command_constant_has__view; +x_79 = l_lean_parser_command_axiom_has__view; x_80 = lean::cnstr_get(x_79, 0); lean::inc(x_80); lean::dec(x_79); @@ -29081,7 +28931,7 @@ obj* x_44; obj* x_47; obj* x_48; obj* x_51; obj* x_52; obj* x_53; obj* x_54; obj x_44 = lean::cnstr_get(x_0, 0); lean::inc(x_44); lean::dec(x_0); -x_47 = l_lean_parser_command_constant_has__view; +x_47 = l_lean_parser_command_axiom_has__view; x_48 = lean::cnstr_get(x_47, 1); lean::inc(x_48); lean::dec(x_47); @@ -29372,7 +29222,7 @@ return x_0; obj* _init_l_lean_parser_command_declaration_parser_lean_parser_has__tokens() { _start: { -obj* x_0; obj* x_1; obj* x_2; obj* x_4; obj* x_5; obj* x_7; obj* x_8; obj* x_10; obj* x_11; obj* x_13; obj* x_14; obj* x_16; obj* x_19; obj* x_22; obj* x_25; obj* x_27; obj* x_29; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_40; obj* x_42; obj* x_45; obj* x_47; obj* x_48; obj* x_50; obj* x_51; obj* x_52; obj* x_54; obj* x_56; obj* x_59; obj* x_61; obj* x_62; obj* x_64; obj* x_67; obj* x_69; obj* x_70; obj* x_72; obj* x_73; obj* x_75; obj* x_77; obj* x_80; obj* x_82; obj* x_84; obj* x_86; obj* x_87; obj* x_89; obj* x_92; obj* x_94; obj* x_95; obj* x_97; obj* x_99; obj* x_100; obj* x_102; obj* x_104; obj* x_107; obj* x_109; obj* x_111; obj* x_112; obj* x_113; obj* x_115; obj* x_116; obj* x_117; obj* x_119; obj* x_122; obj* x_124; obj* x_126; obj* x_129; obj* x_132; obj* x_134; obj* x_135; obj* x_136; obj* x_139; obj* x_142; obj* x_145; obj* x_148; obj* x_151; obj* x_153; obj* x_155; obj* x_157; obj* x_159; obj* x_160; obj* x_162; +obj* x_0; obj* x_1; obj* x_2; obj* x_4; obj* x_5; obj* x_7; obj* x_8; obj* x_10; obj* x_11; obj* x_13; obj* x_14; obj* x_16; obj* x_19; obj* x_22; obj* x_25; obj* x_27; obj* x_29; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_40; obj* x_42; obj* x_45; obj* x_47; obj* x_48; obj* x_50; obj* x_51; obj* x_52; obj* x_54; obj* x_56; obj* x_59; obj* x_61; obj* x_62; obj* x_64; obj* x_67; obj* x_69; obj* x_70; obj* x_72; obj* x_74; obj* x_76; obj* x_78; obj* x_80; obj* x_81; obj* x_83; obj* x_86; obj* x_88; obj* x_89; obj* x_91; obj* x_93; obj* x_94; obj* x_96; obj* x_98; obj* x_101; obj* x_103; obj* x_105; obj* x_106; obj* x_107; obj* x_109; obj* x_110; obj* x_111; obj* x_113; obj* x_116; obj* x_118; obj* x_120; obj* x_123; obj* x_126; obj* x_128; obj* x_129; obj* x_130; obj* x_133; obj* x_136; obj* x_139; obj* x_142; obj* x_145; obj* x_147; obj* x_149; obj* x_151; obj* x_153; obj* x_154; obj* x_156; x_0 = lean::mk_string("def"); x_1 = lean::mk_nat_obj(0u); x_2 = l_lean_parser_symbol_tokens___rarg(x_0, x_1); @@ -29442,102 +29292,96 @@ lean::dec(x_52); lean::dec(x_62); x_67 = l_lean_parser_tokens___rarg(x_64); lean::dec(x_64); -x_69 = lean::mk_string("constant"); +x_69 = lean::mk_string("axiom"); x_70 = l_lean_parser_symbol_tokens___rarg(x_69, x_1); lean::dec(x_69); -x_72 = lean::mk_string("axiom"); -x_73 = l_lean_parser_symbol_tokens___rarg(x_72, x_1); -lean::dec(x_72); -x_75 = l_lean_parser_list_cons_tokens___rarg(x_73, x_13); -lean::dec(x_73); -x_77 = l_lean_parser_list_cons_tokens___rarg(x_70, x_75); -lean::dec(x_75); +x_72 = l_lean_parser_list_cons_tokens___rarg(x_70, x_13); lean::dec(x_70); -x_80 = l_lean_parser_tokens___rarg(x_77); -lean::dec(x_77); -x_82 = l_lean_parser_list_cons_tokens___rarg(x_80, x_13); +x_74 = l_lean_parser_tokens___rarg(x_72); +lean::dec(x_72); +x_76 = l_lean_parser_list_cons_tokens___rarg(x_74, x_13); +lean::dec(x_74); +x_78 = l_lean_parser_tokens___rarg(x_76); +lean::dec(x_76); +x_80 = l_lean_parser_list_cons_tokens___rarg(x_51, x_13); +x_81 = l_lean_parser_list_cons_tokens___rarg(x_37, x_80); lean::dec(x_80); -x_84 = l_lean_parser_tokens___rarg(x_82); -lean::dec(x_82); -x_86 = l_lean_parser_list_cons_tokens___rarg(x_51, x_13); -x_87 = l_lean_parser_list_cons_tokens___rarg(x_37, x_86); -lean::dec(x_86); -x_89 = l_lean_parser_list_cons_tokens___rarg(x_84, x_87); -lean::dec(x_87); -lean::dec(x_84); -x_92 = l_lean_parser_tokens___rarg(x_89); +x_83 = l_lean_parser_list_cons_tokens___rarg(x_78, x_81); +lean::dec(x_81); +lean::dec(x_78); +x_86 = l_lean_parser_tokens___rarg(x_83); +lean::dec(x_83); +x_88 = lean::mk_string("class"); +x_89 = l_lean_parser_symbol_tokens___rarg(x_88, x_1); +lean::dec(x_88); +x_91 = l_lean_parser_tokens___rarg(x_89); lean::dec(x_89); -x_94 = lean::mk_string("class"); -x_95 = l_lean_parser_symbol_tokens___rarg(x_94, x_1); +x_93 = lean::mk_string("inductive"); +x_94 = l_lean_parser_symbol_tokens___rarg(x_93, x_1); +lean::dec(x_93); +x_96 = l_lean_parser_list_cons_tokens___rarg(x_94, x_13); lean::dec(x_94); -x_97 = l_lean_parser_tokens___rarg(x_95); -lean::dec(x_95); -x_99 = lean::mk_string("inductive"); -x_100 = l_lean_parser_symbol_tokens___rarg(x_99, x_1); -lean::dec(x_99); -x_102 = l_lean_parser_list_cons_tokens___rarg(x_100, x_13); -lean::dec(x_100); -x_104 = l_lean_parser_list_cons_tokens___rarg(x_97, x_102); -lean::dec(x_102); -lean::dec(x_97); -x_107 = l_lean_parser_tokens___rarg(x_104); -lean::dec(x_104); -x_109 = l_lean_parser_tokens___rarg(x_107); +x_98 = l_lean_parser_list_cons_tokens___rarg(x_91, x_96); +lean::dec(x_96); +lean::dec(x_91); +x_101 = l_lean_parser_tokens___rarg(x_98); +lean::dec(x_98); +x_103 = l_lean_parser_tokens___rarg(x_101); +lean::dec(x_101); +x_105 = l_lean_parser_command_notation__like_parser_lean_parser_has__tokens; +x_106 = l_lean_parser_tokens___rarg(x_105); +x_107 = l_lean_parser_tokens___rarg(x_106); +lean::dec(x_106); +x_109 = l_lean_parser_command_intro__rule_parser_lean_parser_has__tokens; +x_110 = l_lean_parser_tokens___rarg(x_109); +x_111 = l_lean_parser_list_cons_tokens___rarg(x_110, x_13); +lean::dec(x_110); +x_113 = l_lean_parser_list_cons_tokens___rarg(x_107, x_111); +lean::dec(x_111); lean::dec(x_107); -x_111 = l_lean_parser_command_notation__like_parser_lean_parser_has__tokens; -x_112 = l_lean_parser_tokens___rarg(x_111); -x_113 = l_lean_parser_tokens___rarg(x_112); -lean::dec(x_112); -x_115 = l_lean_parser_command_intro__rule_parser_lean_parser_has__tokens; -x_116 = l_lean_parser_tokens___rarg(x_115); -x_117 = l_lean_parser_list_cons_tokens___rarg(x_116, x_13); -lean::dec(x_116); -x_119 = l_lean_parser_list_cons_tokens___rarg(x_113, x_117); -lean::dec(x_117); +x_116 = l_lean_parser_list_cons_tokens___rarg(x_35, x_113); lean::dec(x_113); -x_122 = l_lean_parser_list_cons_tokens___rarg(x_35, x_119); -lean::dec(x_119); -x_124 = l_lean_parser_list_cons_tokens___rarg(x_37, x_122); -lean::dec(x_122); -x_126 = l_lean_parser_list_cons_tokens___rarg(x_32, x_124); -lean::dec(x_124); +x_118 = l_lean_parser_list_cons_tokens___rarg(x_37, x_116); +lean::dec(x_116); +x_120 = l_lean_parser_list_cons_tokens___rarg(x_32, x_118); +lean::dec(x_118); lean::dec(x_32); -x_129 = l_lean_parser_list_cons_tokens___rarg(x_109, x_126); -lean::dec(x_126); -lean::dec(x_109); -x_132 = l_lean_parser_tokens___rarg(x_129); +x_123 = l_lean_parser_list_cons_tokens___rarg(x_103, x_120); +lean::dec(x_120); +lean::dec(x_103); +x_126 = l_lean_parser_tokens___rarg(x_123); +lean::dec(x_123); +x_128 = l_lean_parser_command_structure_parser_lean_parser_has__tokens; +x_129 = l_lean_parser_list_cons_tokens___rarg(x_128, x_13); +x_130 = l_lean_parser_list_cons_tokens___rarg(x_126, x_129); lean::dec(x_129); -x_134 = l_lean_parser_command_structure_parser_lean_parser_has__tokens; -x_135 = l_lean_parser_list_cons_tokens___rarg(x_134, x_13); -x_136 = l_lean_parser_list_cons_tokens___rarg(x_132, x_135); -lean::dec(x_135); -lean::dec(x_132); -x_139 = l_lean_parser_list_cons_tokens___rarg(x_92, x_136); -lean::dec(x_136); -lean::dec(x_92); -x_142 = l_lean_parser_list_cons_tokens___rarg(x_67, x_139); -lean::dec(x_139); +lean::dec(x_126); +x_133 = l_lean_parser_list_cons_tokens___rarg(x_86, x_130); +lean::dec(x_130); +lean::dec(x_86); +x_136 = l_lean_parser_list_cons_tokens___rarg(x_67, x_133); +lean::dec(x_133); lean::dec(x_67); -x_145 = l_lean_parser_list_cons_tokens___rarg(x_59, x_142); -lean::dec(x_142); +x_139 = l_lean_parser_list_cons_tokens___rarg(x_59, x_136); +lean::dec(x_136); lean::dec(x_59); -x_148 = l_lean_parser_list_cons_tokens___rarg(x_45, x_145); -lean::dec(x_145); +x_142 = l_lean_parser_list_cons_tokens___rarg(x_45, x_139); +lean::dec(x_139); lean::dec(x_45); -x_151 = l_lean_parser_tokens___rarg(x_148); -lean::dec(x_148); -x_153 = l_lean_parser_list_cons_tokens___rarg(x_151, x_13); +x_145 = l_lean_parser_tokens___rarg(x_142); +lean::dec(x_142); +x_147 = l_lean_parser_list_cons_tokens___rarg(x_145, x_13); +lean::dec(x_145); +x_149 = l_lean_parser_tokens___rarg(x_147); +lean::dec(x_147); +x_151 = l_lean_parser_list_cons_tokens___rarg(x_149, x_13); +lean::dec(x_149); +x_153 = l_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens; +x_154 = l_lean_parser_list_cons_tokens___rarg(x_153, x_151); lean::dec(x_151); -x_155 = l_lean_parser_tokens___rarg(x_153); -lean::dec(x_153); -x_157 = l_lean_parser_list_cons_tokens___rarg(x_155, x_13); -lean::dec(x_155); -x_159 = l_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens; -x_160 = l_lean_parser_list_cons_tokens___rarg(x_159, x_157); -lean::dec(x_157); -x_162 = l_lean_parser_tokens___rarg(x_160); -lean::dec(x_160); -return x_162; +x_156 = l_lean_parser_tokens___rarg(x_154); +lean::dec(x_154); +return x_156; } } obj* l_lean_parser_command_declaration_parser_lean_parser_has__view___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) { @@ -29570,7 +29414,7 @@ return x_13; obj* _init_l_lean_parser_command_declaration_parser_lean_parser_has__view() { _start: { -obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_41; obj* x_42; obj* x_44; obj* x_46; obj* x_47; obj* x_48; obj* x_49; obj* x_50; obj* x_51; obj* x_54; obj* x_55; obj* x_57; obj* x_58; obj* x_60; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_70; obj* x_71; obj* x_72; obj* x_73; obj* x_74; obj* x_75; obj* x_76; obj* x_79; obj* x_80; obj* x_81; obj* x_82; obj* x_85; obj* x_86; obj* x_87; obj* x_88; obj* x_89; obj* x_90; obj* x_91; obj* x_92; obj* x_93; obj* x_95; obj* x_96; obj* x_97; obj* x_98; obj* x_99; obj* x_100; obj* x_103; obj* x_104; obj* x_105; obj* x_106; obj* x_107; obj* x_110; obj* x_111; obj* x_112; obj* x_113; obj* x_114; obj* x_115; obj* x_116; obj* x_117; obj* x_118; obj* x_119; obj* x_120; obj* x_121; obj* x_122; obj* x_123; obj* x_124; obj* x_125; obj* x_126; obj* x_127; obj* x_128; obj* x_129; obj* x_130; obj* x_131; obj* x_132; obj* x_133; obj* x_134; obj* x_135; obj* x_136; obj* x_137; obj* x_138; obj* x_139; obj* x_140; obj* x_141; obj* x_142; obj* x_143; obj* x_144; obj* x_145; obj* x_146; obj* x_147; obj* x_148; +obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_41; obj* x_42; obj* x_44; obj* x_46; obj* x_47; obj* x_48; obj* x_49; obj* x_50; obj* x_51; obj* x_54; obj* x_55; obj* x_57; obj* x_58; obj* x_60; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_70; obj* x_71; obj* x_72; obj* x_73; obj* x_74; obj* x_75; obj* x_76; obj* x_79; obj* x_80; obj* x_81; obj* x_82; obj* x_83; obj* x_84; obj* x_85; obj* x_86; obj* x_88; obj* x_89; obj* x_90; obj* x_91; obj* x_92; obj* x_93; obj* x_96; obj* x_97; obj* x_98; obj* x_99; obj* x_100; obj* x_103; obj* x_104; obj* x_105; obj* x_106; obj* x_107; obj* x_108; obj* x_109; obj* x_110; obj* x_111; obj* x_112; obj* x_113; obj* x_114; obj* x_115; obj* x_116; obj* x_117; obj* x_118; obj* x_119; obj* x_120; obj* x_121; obj* x_122; obj* x_123; obj* x_124; obj* x_125; obj* x_126; obj* x_127; obj* x_128; obj* x_129; obj* x_130; obj* x_131; obj* x_132; obj* x_133; obj* x_134; obj* x_135; obj* x_136; obj* x_137; obj* x_138; obj* x_139; obj* x_140; obj* x_141; x_0 = lean::mk_string("def"); x_1 = l_string_trim(x_0); lean::dec(x_0); @@ -29710,7 +29554,7 @@ x_73 = l_lean_parser_command_example; x_74 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); lean::closure_set(x_74, 0, x_73); lean::closure_set(x_74, 1, x_72); -x_75 = lean::mk_string("constant"); +x_75 = lean::mk_string("axiom"); x_76 = l_string_trim(x_75); lean::dec(x_75); lean::inc(x_76); @@ -29720,47 +29564,46 @@ x_80 = lean::alloc_closure(reinterpret_cast(l_lean_parser_symbol__core___ lean::closure_set(x_80, 0, x_76); lean::closure_set(x_80, 1, x_5); lean::closure_set(x_80, 2, x_79); -x_81 = lean::mk_string("axiom"); -x_82 = l_string_trim(x_81); -lean::dec(x_81); -lean::inc(x_82); -x_85 = lean::alloc_closure(reinterpret_cast(l_dlist_singleton___rarg), 2, 1); -lean::closure_set(x_85, 0, x_82); -x_86 = lean::alloc_closure(reinterpret_cast(l_lean_parser_symbol__core___at_lean_parser_command_doc__comment_parser_lean_parser_has__tokens___spec__1___boxed), 7, 3); -lean::closure_set(x_86, 0, x_82); -lean::closure_set(x_86, 1, x_5); -lean::closure_set(x_86, 2, x_85); -x_87 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_87, 0, x_86); -lean::cnstr_set(x_87, 1, x_25); -x_88 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_88, 0, x_80); -lean::cnstr_set(x_88, 1, x_87); -x_89 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_choice__aux___main___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__2), 6, 2); -lean::closure_set(x_89, 0, x_88); -lean::closure_set(x_89, 1, x_5); -x_90 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_90, 0, x_89); -lean::cnstr_set(x_90, 1, x_25); -x_91 = l_lean_parser_command_constant__keyword; -x_92 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); -lean::closure_set(x_92, 0, x_91); -lean::closure_set(x_92, 1, x_90); -x_93 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_93, 0, x_58); -lean::cnstr_set(x_93, 1, x_25); +x_81 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_81, 0, x_80); +lean::cnstr_set(x_81, 1, x_25); +x_82 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_choice__aux___main___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__2), 6, 2); +lean::closure_set(x_82, 0, x_81); +lean::closure_set(x_82, 1, x_5); +x_83 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_83, 0, x_82); +lean::cnstr_set(x_83, 1, x_25); +x_84 = l_lean_parser_command_constant__keyword; +x_85 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); +lean::closure_set(x_85, 0, x_84); +lean::closure_set(x_85, 1, x_83); +x_86 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_86, 0, x_58); +lean::cnstr_set(x_86, 1, x_25); lean::inc(x_42); -x_95 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_95, 0, x_42); -lean::cnstr_set(x_95, 1, x_93); -x_96 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_96, 0, x_92); -lean::cnstr_set(x_96, 1, x_95); -x_97 = l_lean_parser_command_constant; -x_98 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); +x_88 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_88, 0, x_42); +lean::cnstr_set(x_88, 1, x_86); +x_89 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_89, 0, x_85); +lean::cnstr_set(x_89, 1, x_88); +x_90 = l_lean_parser_command_axiom; +x_91 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); +lean::closure_set(x_91, 0, x_90); +lean::closure_set(x_91, 1, x_89); +x_92 = lean::mk_string("class"); +x_93 = l_string_trim(x_92); +lean::dec(x_92); +lean::inc(x_93); +x_96 = lean::alloc_closure(reinterpret_cast(l_dlist_singleton___rarg), 2, 1); +lean::closure_set(x_96, 0, x_93); +x_97 = lean::alloc_closure(reinterpret_cast(l_lean_parser_symbol__core___at_lean_parser_command_doc__comment_parser_lean_parser_has__tokens___spec__1___boxed), 7, 3); +lean::closure_set(x_97, 0, x_93); +lean::closure_set(x_97, 1, x_5); +lean::closure_set(x_97, 2, x_96); +x_98 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1); lean::closure_set(x_98, 0, x_97); -lean::closure_set(x_98, 1, x_96); -x_99 = lean::mk_string("class"); +x_99 = lean::mk_string("inductive"); x_100 = l_string_trim(x_99); lean::dec(x_99); lean::inc(x_100); @@ -29770,107 +29613,95 @@ x_104 = lean::alloc_closure(reinterpret_cast(l_lean_parser_symbol__core__ lean::closure_set(x_104, 0, x_100); lean::closure_set(x_104, 1, x_5); lean::closure_set(x_104, 2, x_103); -x_105 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1); -lean::closure_set(x_105, 0, x_104); -x_106 = lean::mk_string("inductive"); -x_107 = l_string_trim(x_106); -lean::dec(x_106); -lean::inc(x_107); -x_110 = lean::alloc_closure(reinterpret_cast(l_dlist_singleton___rarg), 2, 1); -lean::closure_set(x_110, 0, x_107); -x_111 = lean::alloc_closure(reinterpret_cast(l_lean_parser_symbol__core___at_lean_parser_command_doc__comment_parser_lean_parser_has__tokens___spec__1___boxed), 7, 3); -lean::closure_set(x_111, 0, x_107); -lean::closure_set(x_111, 1, x_5); -lean::closure_set(x_111, 2, x_110); -x_112 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_112, 0, x_111); -lean::cnstr_set(x_112, 1, x_25); +x_105 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_105, 0, x_104); +lean::cnstr_set(x_105, 1, x_25); +x_106 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_106, 0, x_98); +lean::cnstr_set(x_106, 1, x_105); +x_107 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_declaration_parser_lean_parser_has__view___lambda__1), 5, 1); +lean::closure_set(x_107, 0, x_106); +x_108 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_notation__like_parser), 5, 0); +x_109 = lean::alloc_closure(reinterpret_cast(l_lean_parser_term__parser_run), 5, 1); +lean::closure_set(x_109, 0, x_108); +x_110 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1); +lean::closure_set(x_110, 0, x_109); +x_111 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_intro__rule_parser), 4, 0); +x_112 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_many___at_lean_parser_command_attr__instance_parser_lean_parser_has__tokens___spec__2), 5, 1); +lean::closure_set(x_112, 0, x_111); x_113 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_113, 0, x_105); -lean::cnstr_set(x_113, 1, x_112); -x_114 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_declaration_parser_lean_parser_has__view___lambda__1), 5, 1); -lean::closure_set(x_114, 0, x_113); -x_115 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_notation__like_parser), 5, 0); -x_116 = lean::alloc_closure(reinterpret_cast(l_lean_parser_term__parser_run), 5, 1); -lean::closure_set(x_116, 0, x_115); -x_117 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1); -lean::closure_set(x_117, 0, x_116); -x_118 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_intro__rule_parser), 4, 0); -x_119 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_many___at_lean_parser_command_attr__instance_parser_lean_parser_has__tokens___spec__2), 5, 1); -lean::closure_set(x_119, 0, x_118); -x_120 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_120, 0, x_119); -lean::cnstr_set(x_120, 1, x_25); -x_121 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_121, 0, x_117); -lean::cnstr_set(x_121, 1, x_120); +lean::cnstr_set(x_113, 0, x_112); +lean::cnstr_set(x_113, 1, x_25); +x_114 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_114, 0, x_110); +lean::cnstr_set(x_114, 1, x_113); +x_115 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_115, 0, x_38); +lean::cnstr_set(x_115, 1, x_114); +x_116 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_116, 0, x_42); +lean::cnstr_set(x_116, 1, x_115); +x_117 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_117, 0, x_35); +lean::cnstr_set(x_117, 1, x_116); +x_118 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_118, 0, x_107); +lean::cnstr_set(x_118, 1, x_117); +x_119 = l_lean_parser_command_inductive; +x_120 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); +lean::closure_set(x_120, 0, x_119); +lean::closure_set(x_120, 1, x_118); +x_121 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_structure_parser), 4, 0); x_122 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_122, 0, x_38); -lean::cnstr_set(x_122, 1, x_121); +lean::cnstr_set(x_122, 0, x_121); +lean::cnstr_set(x_122, 1, x_25); x_123 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_123, 0, x_42); +lean::cnstr_set(x_123, 0, x_120); lean::cnstr_set(x_123, 1, x_122); x_124 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_124, 0, x_35); +lean::cnstr_set(x_124, 0, x_91); lean::cnstr_set(x_124, 1, x_123); x_125 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_125, 0, x_114); +lean::cnstr_set(x_125, 0, x_74); lean::cnstr_set(x_125, 1, x_124); -x_126 = l_lean_parser_command_inductive; -x_127 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); -lean::closure_set(x_127, 0, x_126); -lean::closure_set(x_127, 1, x_125); -x_128 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_structure_parser), 4, 0); +x_126 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_126, 0, x_65); +lean::cnstr_set(x_126, 1, x_125); +x_127 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_127, 0, x_49); +lean::cnstr_set(x_127, 1, x_126); +x_128 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_choice__aux___main___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__2), 6, 2); +lean::closure_set(x_128, 0, x_127); +lean::closure_set(x_128, 1, x_5); x_129 = lean::alloc_cnstr(1, 2, 0); lean::cnstr_set(x_129, 0, x_128); lean::cnstr_set(x_129, 1, x_25); -x_130 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_130, 0, x_127); -lean::cnstr_set(x_130, 1, x_129); -x_131 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_131, 0, x_98); -lean::cnstr_set(x_131, 1, x_130); +x_130 = l_lean_parser_command_declaration_inner; +x_131 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); +lean::closure_set(x_131, 0, x_130); +lean::closure_set(x_131, 1, x_129); x_132 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_132, 0, x_74); -lean::cnstr_set(x_132, 1, x_131); -x_133 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_133, 0, x_65); -lean::cnstr_set(x_133, 1, x_132); +lean::cnstr_set(x_132, 0, x_131); +lean::cnstr_set(x_132, 1, x_25); +x_133 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_decl__modifiers_parser), 4, 0); x_134 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_134, 0, x_49); -lean::cnstr_set(x_134, 1, x_133); -x_135 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_choice__aux___main___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__2), 6, 2); -lean::closure_set(x_135, 0, x_134); -lean::closure_set(x_135, 1, x_5); -x_136 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_136, 0, x_135); -lean::cnstr_set(x_136, 1, x_25); -x_137 = l_lean_parser_command_declaration_inner; -x_138 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); -lean::closure_set(x_138, 0, x_137); -lean::closure_set(x_138, 1, x_136); -x_139 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_139, 0, x_138); -lean::cnstr_set(x_139, 1, x_25); -x_140 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_decl__modifiers_parser), 4, 0); -x_141 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_141, 0, x_140); -lean::cnstr_set(x_141, 1, x_139); -x_142 = l_lean_parser_command__parser__m_monad___closed__1; -x_143 = l_lean_parser_command__parser__m_monad__except___closed__1; -x_144 = l_lean_parser_command__parser__m_lean_parser_monad__parsec___closed__1; -x_145 = l_lean_parser_command__parser__m_alternative___closed__1; -x_146 = l_lean_parser_command_declaration; -x_147 = l_lean_parser_command_declaration_has__view; -x_148 = l_lean_parser_combinators_node_view___rarg(x_142, x_143, x_144, x_145, x_146, x_141, x_147); -lean::dec(x_141); -return x_148; +lean::cnstr_set(x_134, 0, x_133); +lean::cnstr_set(x_134, 1, x_132); +x_135 = l_lean_parser_command__parser__m_monad___closed__1; +x_136 = l_lean_parser_command__parser__m_monad__except___closed__1; +x_137 = l_lean_parser_command__parser__m_lean_parser_monad__parsec___closed__1; +x_138 = l_lean_parser_command__parser__m_alternative___closed__1; +x_139 = l_lean_parser_command_declaration; +x_140 = l_lean_parser_command_declaration_has__view; +x_141 = l_lean_parser_combinators_node_view___rarg(x_135, x_136, x_137, x_138, x_139, x_134, x_140); +lean::dec(x_134); +return x_141; } } obj* _init_l_lean_parser_command_declaration_parser___closed__1() { _start: { -obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_41; obj* x_42; obj* x_44; obj* x_46; obj* x_47; obj* x_48; obj* x_49; obj* x_50; obj* x_51; obj* x_54; obj* x_55; obj* x_57; obj* x_58; obj* x_60; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_70; obj* x_71; obj* x_72; obj* x_73; obj* x_74; obj* x_75; obj* x_76; obj* x_79; obj* x_80; obj* x_81; obj* x_82; obj* x_85; obj* x_86; obj* x_87; obj* x_88; obj* x_89; obj* x_90; obj* x_91; obj* x_92; obj* x_93; obj* x_95; obj* x_96; obj* x_97; obj* x_98; obj* x_99; obj* x_100; obj* x_103; obj* x_104; obj* x_105; obj* x_106; obj* x_107; obj* x_110; obj* x_111; obj* x_112; obj* x_113; obj* x_114; obj* x_115; obj* x_116; obj* x_117; obj* x_118; obj* x_119; obj* x_120; obj* x_121; obj* x_122; obj* x_123; obj* x_124; obj* x_125; obj* x_126; obj* x_127; obj* x_128; obj* x_129; obj* x_130; obj* x_131; obj* x_132; obj* x_133; obj* x_134; obj* x_135; obj* x_136; obj* x_137; obj* x_138; obj* x_139; obj* x_140; obj* x_141; +obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_41; obj* x_42; obj* x_44; obj* x_46; obj* x_47; obj* x_48; obj* x_49; obj* x_50; obj* x_51; obj* x_54; obj* x_55; obj* x_57; obj* x_58; obj* x_60; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_70; obj* x_71; obj* x_72; obj* x_73; obj* x_74; obj* x_75; obj* x_76; obj* x_79; obj* x_80; obj* x_81; obj* x_82; obj* x_83; obj* x_84; obj* x_85; obj* x_86; obj* x_88; obj* x_89; obj* x_90; obj* x_91; obj* x_92; obj* x_93; obj* x_96; obj* x_97; obj* x_98; obj* x_99; obj* x_100; obj* x_103; obj* x_104; obj* x_105; obj* x_106; obj* x_107; obj* x_108; obj* x_109; obj* x_110; obj* x_111; obj* x_112; obj* x_113; obj* x_114; obj* x_115; obj* x_116; obj* x_117; obj* x_118; obj* x_119; obj* x_120; obj* x_121; obj* x_122; obj* x_123; obj* x_124; obj* x_125; obj* x_126; obj* x_127; obj* x_128; obj* x_129; obj* x_130; obj* x_131; obj* x_132; obj* x_133; obj* x_134; x_0 = lean::mk_string("def"); x_1 = l_string_trim(x_0); lean::dec(x_0); @@ -30010,7 +29841,7 @@ x_73 = l_lean_parser_command_example; x_74 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); lean::closure_set(x_74, 0, x_73); lean::closure_set(x_74, 1, x_72); -x_75 = lean::mk_string("constant"); +x_75 = lean::mk_string("axiom"); x_76 = l_string_trim(x_75); lean::dec(x_75); lean::inc(x_76); @@ -30020,47 +29851,46 @@ x_80 = lean::alloc_closure(reinterpret_cast(l_lean_parser_symbol__core___ lean::closure_set(x_80, 0, x_76); lean::closure_set(x_80, 1, x_5); lean::closure_set(x_80, 2, x_79); -x_81 = lean::mk_string("axiom"); -x_82 = l_string_trim(x_81); -lean::dec(x_81); -lean::inc(x_82); -x_85 = lean::alloc_closure(reinterpret_cast(l_dlist_singleton___rarg), 2, 1); -lean::closure_set(x_85, 0, x_82); -x_86 = lean::alloc_closure(reinterpret_cast(l_lean_parser_symbol__core___at_lean_parser_command_doc__comment_parser_lean_parser_has__tokens___spec__1___boxed), 7, 3); -lean::closure_set(x_86, 0, x_82); -lean::closure_set(x_86, 1, x_5); -lean::closure_set(x_86, 2, x_85); -x_87 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_87, 0, x_86); -lean::cnstr_set(x_87, 1, x_25); -x_88 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_88, 0, x_80); -lean::cnstr_set(x_88, 1, x_87); -x_89 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_choice__aux___main___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__2), 6, 2); -lean::closure_set(x_89, 0, x_88); -lean::closure_set(x_89, 1, x_5); -x_90 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_90, 0, x_89); -lean::cnstr_set(x_90, 1, x_25); -x_91 = l_lean_parser_command_constant__keyword; -x_92 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); -lean::closure_set(x_92, 0, x_91); -lean::closure_set(x_92, 1, x_90); -x_93 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_93, 0, x_58); -lean::cnstr_set(x_93, 1, x_25); +x_81 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_81, 0, x_80); +lean::cnstr_set(x_81, 1, x_25); +x_82 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_choice__aux___main___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__2), 6, 2); +lean::closure_set(x_82, 0, x_81); +lean::closure_set(x_82, 1, x_5); +x_83 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_83, 0, x_82); +lean::cnstr_set(x_83, 1, x_25); +x_84 = l_lean_parser_command_constant__keyword; +x_85 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); +lean::closure_set(x_85, 0, x_84); +lean::closure_set(x_85, 1, x_83); +x_86 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_86, 0, x_58); +lean::cnstr_set(x_86, 1, x_25); lean::inc(x_42); -x_95 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_95, 0, x_42); -lean::cnstr_set(x_95, 1, x_93); -x_96 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_96, 0, x_92); -lean::cnstr_set(x_96, 1, x_95); -x_97 = l_lean_parser_command_constant; -x_98 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); +x_88 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_88, 0, x_42); +lean::cnstr_set(x_88, 1, x_86); +x_89 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_89, 0, x_85); +lean::cnstr_set(x_89, 1, x_88); +x_90 = l_lean_parser_command_axiom; +x_91 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); +lean::closure_set(x_91, 0, x_90); +lean::closure_set(x_91, 1, x_89); +x_92 = lean::mk_string("class"); +x_93 = l_string_trim(x_92); +lean::dec(x_92); +lean::inc(x_93); +x_96 = lean::alloc_closure(reinterpret_cast(l_dlist_singleton___rarg), 2, 1); +lean::closure_set(x_96, 0, x_93); +x_97 = lean::alloc_closure(reinterpret_cast(l_lean_parser_symbol__core___at_lean_parser_command_doc__comment_parser_lean_parser_has__tokens___spec__1___boxed), 7, 3); +lean::closure_set(x_97, 0, x_93); +lean::closure_set(x_97, 1, x_5); +lean::closure_set(x_97, 2, x_96); +x_98 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1); lean::closure_set(x_98, 0, x_97); -lean::closure_set(x_98, 1, x_96); -x_99 = lean::mk_string("class"); +x_99 = lean::mk_string("inductive"); x_100 = l_string_trim(x_99); lean::dec(x_99); lean::inc(x_100); @@ -30070,93 +29900,81 @@ x_104 = lean::alloc_closure(reinterpret_cast(l_lean_parser_symbol__core__ lean::closure_set(x_104, 0, x_100); lean::closure_set(x_104, 1, x_5); lean::closure_set(x_104, 2, x_103); -x_105 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1); -lean::closure_set(x_105, 0, x_104); -x_106 = lean::mk_string("inductive"); -x_107 = l_string_trim(x_106); -lean::dec(x_106); -lean::inc(x_107); -x_110 = lean::alloc_closure(reinterpret_cast(l_dlist_singleton___rarg), 2, 1); -lean::closure_set(x_110, 0, x_107); -x_111 = lean::alloc_closure(reinterpret_cast(l_lean_parser_symbol__core___at_lean_parser_command_doc__comment_parser_lean_parser_has__tokens___spec__1___boxed), 7, 3); -lean::closure_set(x_111, 0, x_107); -lean::closure_set(x_111, 1, x_5); -lean::closure_set(x_111, 2, x_110); -x_112 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_112, 0, x_111); -lean::cnstr_set(x_112, 1, x_25); +x_105 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_105, 0, x_104); +lean::cnstr_set(x_105, 1, x_25); +x_106 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_106, 0, x_98); +lean::cnstr_set(x_106, 1, x_105); +x_107 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_declaration_parser_lean_parser_has__view___lambda__1), 5, 1); +lean::closure_set(x_107, 0, x_106); +x_108 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_notation__like_parser), 5, 0); +x_109 = lean::alloc_closure(reinterpret_cast(l_lean_parser_term__parser_run), 5, 1); +lean::closure_set(x_109, 0, x_108); +x_110 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1); +lean::closure_set(x_110, 0, x_109); +x_111 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_intro__rule_parser), 4, 0); +x_112 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_many___at_lean_parser_command_attr__instance_parser_lean_parser_has__tokens___spec__2), 5, 1); +lean::closure_set(x_112, 0, x_111); x_113 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_113, 0, x_105); -lean::cnstr_set(x_113, 1, x_112); -x_114 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_declaration_parser_lean_parser_has__view___lambda__1), 5, 1); -lean::closure_set(x_114, 0, x_113); -x_115 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_notation__like_parser), 5, 0); -x_116 = lean::alloc_closure(reinterpret_cast(l_lean_parser_term__parser_run), 5, 1); -lean::closure_set(x_116, 0, x_115); -x_117 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1); -lean::closure_set(x_117, 0, x_116); -x_118 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_intro__rule_parser), 4, 0); -x_119 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_many___at_lean_parser_command_attr__instance_parser_lean_parser_has__tokens___spec__2), 5, 1); -lean::closure_set(x_119, 0, x_118); -x_120 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_120, 0, x_119); -lean::cnstr_set(x_120, 1, x_25); -x_121 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_121, 0, x_117); -lean::cnstr_set(x_121, 1, x_120); +lean::cnstr_set(x_113, 0, x_112); +lean::cnstr_set(x_113, 1, x_25); +x_114 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_114, 0, x_110); +lean::cnstr_set(x_114, 1, x_113); +x_115 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_115, 0, x_38); +lean::cnstr_set(x_115, 1, x_114); +x_116 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_116, 0, x_42); +lean::cnstr_set(x_116, 1, x_115); +x_117 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_117, 0, x_35); +lean::cnstr_set(x_117, 1, x_116); +x_118 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_118, 0, x_107); +lean::cnstr_set(x_118, 1, x_117); +x_119 = l_lean_parser_command_inductive; +x_120 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); +lean::closure_set(x_120, 0, x_119); +lean::closure_set(x_120, 1, x_118); +x_121 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_structure_parser), 4, 0); x_122 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_122, 0, x_38); -lean::cnstr_set(x_122, 1, x_121); +lean::cnstr_set(x_122, 0, x_121); +lean::cnstr_set(x_122, 1, x_25); x_123 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_123, 0, x_42); +lean::cnstr_set(x_123, 0, x_120); lean::cnstr_set(x_123, 1, x_122); x_124 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_124, 0, x_35); +lean::cnstr_set(x_124, 0, x_91); lean::cnstr_set(x_124, 1, x_123); x_125 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_125, 0, x_114); +lean::cnstr_set(x_125, 0, x_74); lean::cnstr_set(x_125, 1, x_124); -x_126 = l_lean_parser_command_inductive; -x_127 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); -lean::closure_set(x_127, 0, x_126); -lean::closure_set(x_127, 1, x_125); -x_128 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_structure_parser), 4, 0); +x_126 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_126, 0, x_65); +lean::cnstr_set(x_126, 1, x_125); +x_127 = lean::alloc_cnstr(1, 2, 0); +lean::cnstr_set(x_127, 0, x_49); +lean::cnstr_set(x_127, 1, x_126); +x_128 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_choice__aux___main___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__2), 6, 2); +lean::closure_set(x_128, 0, x_127); +lean::closure_set(x_128, 1, x_5); x_129 = lean::alloc_cnstr(1, 2, 0); lean::cnstr_set(x_129, 0, x_128); lean::cnstr_set(x_129, 1, x_25); -x_130 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_130, 0, x_127); -lean::cnstr_set(x_130, 1, x_129); -x_131 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_131, 0, x_98); -lean::cnstr_set(x_131, 1, x_130); +x_130 = l_lean_parser_command_declaration_inner; +x_131 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); +lean::closure_set(x_131, 0, x_130); +lean::closure_set(x_131, 1, x_129); x_132 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_132, 0, x_74); -lean::cnstr_set(x_132, 1, x_131); -x_133 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_133, 0, x_65); -lean::cnstr_set(x_133, 1, x_132); +lean::cnstr_set(x_132, 0, x_131); +lean::cnstr_set(x_132, 1, x_25); +x_133 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_decl__modifiers_parser), 4, 0); x_134 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_134, 0, x_49); -lean::cnstr_set(x_134, 1, x_133); -x_135 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_choice__aux___main___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__2), 6, 2); -lean::closure_set(x_135, 0, x_134); -lean::closure_set(x_135, 1, x_5); -x_136 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_136, 0, x_135); -lean::cnstr_set(x_136, 1, x_25); -x_137 = l_lean_parser_command_declaration_inner; -x_138 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_node___at_lean_parser_command_doc__comment_parser___spec__4), 6, 2); -lean::closure_set(x_138, 0, x_137); -lean::closure_set(x_138, 1, x_136); -x_139 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_139, 0, x_138); -lean::cnstr_set(x_139, 1, x_25); -x_140 = lean::alloc_closure(reinterpret_cast(l_lean_parser_command_decl__modifiers_parser), 4, 0); -x_141 = lean::alloc_cnstr(1, 2, 0); -lean::cnstr_set(x_141, 0, x_140); -lean::cnstr_set(x_141, 1, x_139); -return x_141; +lean::cnstr_set(x_134, 0, x_133); +lean::cnstr_set(x_134, 1, x_132); +return x_134; } } obj* l_lean_parser_command_declaration_parser(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { @@ -30657,28 +30475,22 @@ lean::mark_persistent(l_lean_parser_command_constant__keyword); lean::mark_persistent(l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1); l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__2 = _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__2(); lean::mark_persistent(l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__2); - l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3 = _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3(); -lean::mark_persistent(l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__3); - l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__4 = _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__4(); -lean::mark_persistent(l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__4); l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__1 = _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__1(); lean::mark_persistent(l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__1); - l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__2 = _init_l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__2(); -lean::mark_persistent(l_lean_parser_command_constant__keyword_has__view_x_27___lambda__2___closed__2); l_lean_parser_command_constant__keyword_has__view_x_27 = _init_l_lean_parser_command_constant__keyword_has__view_x_27(); lean::mark_persistent(l_lean_parser_command_constant__keyword_has__view_x_27); l_lean_parser_command_constant__keyword_has__view = _init_l_lean_parser_command_constant__keyword_has__view(); lean::mark_persistent(l_lean_parser_command_constant__keyword_has__view); - l_lean_parser_command_constant = _init_l_lean_parser_command_constant(); -lean::mark_persistent(l_lean_parser_command_constant); - l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__1 = _init_l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__1(); -lean::mark_persistent(l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__1); - l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__2 = _init_l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__2(); -lean::mark_persistent(l_lean_parser_command_constant_has__view_x_27___lambda__1___closed__2); - l_lean_parser_command_constant_has__view_x_27 = _init_l_lean_parser_command_constant_has__view_x_27(); -lean::mark_persistent(l_lean_parser_command_constant_has__view_x_27); - l_lean_parser_command_constant_has__view = _init_l_lean_parser_command_constant_has__view(); -lean::mark_persistent(l_lean_parser_command_constant_has__view); + l_lean_parser_command_axiom = _init_l_lean_parser_command_axiom(); +lean::mark_persistent(l_lean_parser_command_axiom); + l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__1 = _init_l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__1(); +lean::mark_persistent(l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__1); + l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__2 = _init_l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__2(); +lean::mark_persistent(l_lean_parser_command_axiom_has__view_x_27___lambda__1___closed__2); + l_lean_parser_command_axiom_has__view_x_27 = _init_l_lean_parser_command_axiom_has__view_x_27(); +lean::mark_persistent(l_lean_parser_command_axiom_has__view_x_27); + l_lean_parser_command_axiom_has__view = _init_l_lean_parser_command_axiom_has__view(); +lean::mark_persistent(l_lean_parser_command_axiom_has__view); l_lean_parser_command_inductive = _init_l_lean_parser_command_inductive(); lean::mark_persistent(l_lean_parser_command_inductive); l_lean_parser_command_inductive_has__view_x_27___lambda__1___closed__1 = _init_l_lean_parser_command_inductive_has__view_x_27___lambda__1___closed__1(); diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 3f2ab3db07..efbabf5ed6 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -90,7 +90,6 @@ static environment declare_var(parser & p, environment env, p.add_variable(n, l); return env; } else { - lean_assert(k == variable_kind::Constant || k == variable_kind::Axiom); name const & ns = get_namespace(env); name full_n = ns + n; @@ -114,10 +113,6 @@ static environment declare_var(parser & p, environment env, env = ensure_decl_namespaces(env, full_n); /* Apply attributes last so that they may access any information on the new decl */ env = meta.m_attrs.apply(env, p.ios(), full_n); - if (k == variable_kind::Constant) { - /* We need to invoke the compiler and generate boxed version if needed. */ - env = compile(env, p.get_options(), names(full_n)); - } return env; } } @@ -137,8 +132,8 @@ optional parse_binder_info(parser & p, variable_kind k) { static void check_variable_kind(parser & p, variable_kind k) { if (in_section(p.env())) { - if (k == variable_kind::Axiom || k == variable_kind::Constant) - throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections", + if (k == variable_kind::Axiom) + throw parser_error("invalid declaration, 'axiom' cannot be used in sections", p.pos()); } } @@ -157,7 +152,7 @@ static bool curr_is_binder_annotation(parser & p) { p.curr_is_token(get_ldcurly_tk()) || p.curr_is_token(get_lbracket_tk()); } -/* Auxiliary class to setup naming scopes for a variable/constant/axiom command. +/* Auxiliary class to setup naming scopes for a variable/axiom command. We need the private_name_scope because the type may contain match-expressions. These match expressions produce private definitions, and we need to make sure @@ -250,8 +245,8 @@ static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const var_decl_scope var_scope(p, meta.m_modifiers); /* non instance implicit cases */ if (p.curr_is_token(get_lcurly_tk()) && (k == variable_kind::Variable)) - throw parser_error("invalid declaration, only constants/axioms can be universe polymorphic", p.pos()); - if (k == variable_kind::Constant || k == variable_kind::Axiom) + throw parser_error("invalid declaration, only axioms can be universe polymorphic", p.pos()); + if (k == variable_kind::Axiom) scope1.emplace(p); parse_univ_params(p, ls_buffer); n = p.check_decl_id_next("invalid declaration, identifier expected"); @@ -285,9 +280,6 @@ static environment variable_cmd(parser & p, cmd_meta const & meta) { static environment axiom_cmd(parser & p, cmd_meta const & meta) { return variable_cmd_core(p, variable_kind::Axiom, meta); } -static environment constant_cmd(parser & p, cmd_meta const & meta) { - return variable_cmd_core(p, variable_kind::Constant, meta); -} /* Remark: we currently do not support declarations such as: @@ -303,7 +295,7 @@ instead. */ static void ensure_no_match_in_variables_cmd(pos_info const & pos) { if (used_match_idx()) { - throw parser_error("match-expressions are not supported in `variables/constants` commands", pos); + throw parser_error("match-expressions are not supported in `variables` commands", pos); } } @@ -376,10 +368,10 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons else return p.env(); } else { - throw parser_error("invalid variables/constants/axioms declaration, ':' expected", pos); + throw parser_error("invalid variables declaration, ':' expected", pos); } } - if (k == variable_kind::Constant || k == variable_kind::Axiom) + if (k == variable_kind::Axiom) scope1.emplace(p); type = p.parse_expr(); ensure_no_match_in_variables_cmd(pos); @@ -401,34 +393,22 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons env = declare_var(p, env, id, new_ls, new_type, k, bi, pos, meta); } if (curr_is_binder_annotation(p)) { - if (k == variable_kind::Constant || k == variable_kind::Axiom) { - // Hack: temporarily update the parser environment. - // We must do that to be able to process - // constants (A : Type) (a : A) - parser::local_scope scope2(p, env); - return variables_cmd_core(p, k, meta); - } else { - return variables_cmd_core(p, k, meta); - } + return variables_cmd_core(p, k, meta); } return env; } static environment variables_cmd(parser & p, cmd_meta const & meta) { return variables_cmd_core(p, variable_kind::Variable, meta); } -static environment constants_cmd(parser & p, cmd_meta const & meta) { - return variables_cmd_core(p, variable_kind::Constant, meta); -} -static environment axioms_cmd(parser & p, cmd_meta const & meta) { - return variables_cmd_core(p, variable_kind::Axiom, meta); -} - static environment definition_cmd(parser & p, cmd_meta const & meta) { return definition_cmd_core(p, decl_cmd_kind::Definition, meta); } static environment theorem_cmd(parser & p, cmd_meta const & meta) { return definition_cmd_core(p, decl_cmd_kind::Theorem, meta); } +static environment constant_cmd(parser & p, cmd_meta const & meta) { + return definition_cmd_core(p, decl_cmd_kind::OpaqueConst, meta); +} static environment abbreviation_cmd(parser & p, cmd_meta const & meta) { return definition_cmd_core(p, decl_cmd_kind::Abbreviation, meta); } @@ -559,10 +539,8 @@ void register_decl_cmds(cmd_table & r) { add_cmd(r, cmd_info("universes", "declare universe levels", universes_cmd)); add_cmd(r, cmd_info("variable", "declare a new variable", variable_cmd)); add_cmd(r, cmd_info("constant", "declare a new constant (aka top-level variable)", constant_cmd)); - add_cmd(r, cmd_info("axiom", "declare a new axiom", axiom_cmd)); add_cmd(r, cmd_info("variables", "declare new variables", variables_cmd)); - add_cmd(r, cmd_info("constants", "declare new constants (aka top-level variables)", constants_cmd)); - add_cmd(r, cmd_info("axioms", "declare new axioms", axioms_cmd)); + add_cmd(r, cmd_info("axiom", "declare a new axiom", axiom_cmd)); add_cmd(r, cmd_info("unsafe", "add new unsafe declaration", modifiers_cmd, false)); add_cmd(r, cmd_info("mutual", "add new mutual declaration", modifiers_cmd, false)); add_cmd(r, cmd_info("noncomputable", "add new noncomputable definition", modifiers_cmd, false)); diff --git a/src/frontends/lean/decl_cmds.h b/src/frontends/lean/decl_cmds.h index 86f9df7a67..f36828f31c 100644 --- a/src/frontends/lean/decl_cmds.h +++ b/src/frontends/lean/decl_cmds.h @@ -22,7 +22,7 @@ bool parse_univ_params(parser & p, buffer & ps); Then sort \c ls_buffer (using the order in which the universe levels were declared). */ void update_univ_parameters(buffer & ls_buffer, name_set const & found_ls, parser const & p); -enum class variable_kind { Constant, Variable, Axiom }; +enum class variable_kind { Variable, Axiom }; environment elab_var(parser & p, variable_kind const & k, cmd_meta const & meta, pos_info const & pos, optional const & bi, name const & n, expr type, buffer & ls_buffer); diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h index 5523a80597..e0f0525874 100644 --- a/src/frontends/lean/decl_util.h +++ b/src/frontends/lean/decl_util.h @@ -14,7 +14,7 @@ struct parser; struct cmd_meta; class elaborator; -enum class decl_cmd_kind { Theorem, Definition, Example, Instance, Var, Abbreviation }; +enum class decl_cmd_kind { Theorem, Definition, OpaqueConst, Example, Instance, Var, Abbreviation }; struct decl_modifiers { bool m_is_private{false}; diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 93f9181648..5b3dd0e465 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -183,8 +183,7 @@ static environment compile_decl(parser & p, environment const & env, static pair declare_definition(environment const & env, decl_cmd_kind kind, buffer const & lp_names, - name const & c_name, name const & prv_name, expr type, optional val, cmd_meta const & meta, - bool is_abbrev) { + name const & c_name, name const & prv_name, expr type, optional val, cmd_meta const & meta) { name c_real_name; environment new_env = env; if (has_private_prefix(new_env, prv_name)) { @@ -201,12 +200,17 @@ declare_definition(environment const & env, decl_cmd_kind kind, buffer con std::tie(new_env, type) = abstract_nested_proofs(new_env, c_real_name, type); std::tie(new_env, *val) = abstract_nested_proofs(new_env, c_real_name, *val); } - bool is_meta = meta.m_modifiers.m_is_unsafe; - auto def = - (kind == decl_cmd_kind::Theorem ? - mk_theorem(c_real_name, names(lp_names), type, *val) : - (is_abbrev ? mk_definition(c_real_name, names(lp_names), type, *val, reducibility_hints::mk_abbreviation(), is_meta) : - mk_definition(new_env, c_real_name, names(lp_names), type, *val, is_meta))); + bool is_unsafe = meta.m_modifiers.m_is_unsafe; + declaration def; + switch (kind) { + case decl_cmd_kind::Theorem: def = mk_theorem(c_real_name, names(lp_names), type, *val); break; + case decl_cmd_kind::Abbreviation: def = mk_definition(c_real_name, names(lp_names), type, *val, reducibility_hints::mk_abbreviation(), is_unsafe); break; + case decl_cmd_kind::OpaqueConst: def = mk_opaque(c_real_name, names(lp_names), type, *val); break; + case decl_cmd_kind::Instance: + case decl_cmd_kind::Definition: def = mk_definition(new_env, c_real_name, names(lp_names), type, *val, is_unsafe); break; + default: + throw exception("unknown command declaration"); + } new_env = module::add(new_env, def); if (meta.m_modifiers.m_is_protected) @@ -254,9 +258,8 @@ static environment elab_defs_core(parser & p, decl_cmd_kind kind, cmd_meta const environment env = elab.env(); name c_name = local_name_p(fns[i]); name c_real_name; - bool is_abbrev = false; std::tie(env, c_real_name) = declare_definition(env, kind, lp_names, c_name, prv_names[i], - curr_type, some_expr(curr), meta, is_abbrev); + curr_type, some_expr(curr), meta); env = add_local_ref(p, env, c_name, c_real_name, lp_names, params); new_d_names.push_back(c_real_name); elab.set_env(env); @@ -300,7 +303,7 @@ static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cm Note that mlocal_pp_name_p(fn) and actual_name are different for scoped/private declarations. */ static std::tuple parse_definition(parser & p, buffer & lp_names, buffer & params, - bool is_example, bool is_instance, bool is_meta, bool is_abbrev) { + bool is_example, bool is_instance, bool is_unsafe, bool is_abbrev) { parser::local_scope scope1(p); auto header_pos = p.pos(); time_task _("parsing", p.mk_message(header_pos, INFORMATION)); @@ -309,7 +312,7 @@ static std::tuple parse_definition(parser & p, buffer & expr val; if (p.curr_is_token(get_assign_tk())) { p.next(); - if (is_meta) { + if (is_unsafe) { declaration_name_scope scope2("_main"); fn = mk_local(local_name_p(fn), local_pp_name_p(fn), local_type_p(fn), mk_rec_info()); p.add_local(fn); @@ -472,9 +475,9 @@ static void check_example(environment const & decl_env, options const & opts, buffer univ_params_buf; to_buffer(univ_params, univ_params_buf); finalize_definition(elab, params_buf, type, val, univ_params_buf); - bool is_meta = modifiers.m_is_unsafe; + bool is_unsafe = modifiers.m_is_unsafe; auto new_env = elab.env(); - declaration def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, is_meta); + declaration def = mk_definition(new_env, decl_name, names(univ_params_buf), type, val, is_unsafe); new_env = module::add(new_env, def); } catch (throwable & ex) { message_builder error_msg(tc, decl_env, get_global_ios(), @@ -534,7 +537,7 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m opt_val = elaborate_proof(decl_env, opts, header_pos, new_params_list, new_fn, val, thm_finfo, is_rfl, type, mctx, lctx, pos_provider, use_info_manager, file_name); - env_n = declare_definition(elab.env(), kind, lp_names, c_name, prv_name, type, opt_val, meta, is_abbrev); + env_n = declare_definition(elab.env(), kind, lp_names, c_name, prv_name, type, opt_val, meta); } else if (kind == decl_cmd_kind::Example) { auto env = p.env(); auto opts = p.get_options(); @@ -559,7 +562,7 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m val = get_equations_result(val, 0); } finalize_definition(elab, new_params, type, val, lp_names); - env_n = declare_definition(elab.env(), kind, lp_names, c_name, prv_name, type, some_expr(val), meta, is_abbrev); + env_n = declare_definition(elab.env(), kind, lp_names, c_name, prv_name, type, some_expr(val), meta); } time_task _("decl post-processing", p.mk_message(header_pos, INFORMATION), c_name); environment new_env = env_n.first; diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 604f421690..6e37bea18d 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -101,10 +101,9 @@ void init_token_table(token_table & t) { {"node_longest_choice!", g_max_prec}, {nullptr, 0}}; char const * commands[] = - {"theorem", "axiom", "axioms", "variable", "protected", "private", "hide", + {"theorem", "axiom", "variable", "protected", "private", "hide", "definition", "unsafe", "mutual", "example", "noncomputable", "abbreviation", "abbrev", - "variables", "constant", "constants", - "using_well_founded", "[whnf]", + "variables", "constant", "using_well_founded", "[whnf]", "end", "namespace", "section", "prelude", "import", "inductive", "coinductive", "structure", "class", "universe", "universes", "local", "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp index ae408ce606..a9cb57e93c 100644 --- a/src/frontends/lean/vm_elaborator.cpp +++ b/src/frontends/lean/vm_elaborator.cpp @@ -227,14 +227,14 @@ expr const & get_arg_names(expr const & e, buffer & ns) { return fn; } -void elab_constant_cmd(parser & p, expr const & cmd) { +void elab_axiom_cmd(parser & p, expr const & cmd) { buffer args; buffer ls; get_app_args(mdata_expr(cmd), args); auto fn = get_arg_names(args[1], ls); expr type = args[2]; type = resolve_names(p, type); - p.set_env(elab_var(p, variable_kind::Constant, to_cmd_meta(p.env(), args[0]), get_pos_info_provider()->get_pos_info_or_some(cmd), + p.set_env(elab_var(p, variable_kind::Axiom, to_cmd_meta(p.env(), args[0]), get_pos_info_provider()->get_pos_info_or_some(cmd), optional(), const_name(fn), type, ls)); } @@ -385,8 +385,8 @@ static void elaborate_command(parser & p, expr const & cmd) { } else if (*cmd_name == "#check") { elab_check_cmd(p, cmd); return; - } else if (*cmd_name == "constant") { - elab_constant_cmd(p, cmd); + } else if (*cmd_name == "axiom") { + elab_axiom_cmd(p, cmd); return; } else if (*cmd_name == "defs") { elab_defs_cmd(p, cmd);