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

chore(library/init): delete dead files

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-09 10:35:38 -07:00
parent dfa9ca5dc5
commit b8cd88a827
10 changed files with 251 additions and 539 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/data/basic.lean
View file

@ -6,5 +6,5 @@ Authors: Leonardo de Moura
prelude
import init.data.nat.basic init.data.fin.basic init.data.list.basic init.data.char.basic
import init.data.string.basic init.data.option.basic
import init.data.uint init.data.ordering.basic init.data.repr
import init.data.uint init.data.repr
import init.data.tostring

2
library/init/data/default.lean
View file

@ -6,6 +6,6 @@ Authors: Leonardo de Moura
prelude
import init.data.basic init.data.nat init.data.char init.data.string
import init.data.list init.data.int init.data.array init.data.bytearray
import init.data.fin init.data.uint init.data.ordering
import init.data.fin init.data.uint
import init.data.rbtree init.data.rbmap init.data.option.basic init.data.option.instances
import init.data.hashmap init.data.random

59
library/init/data/ordering/basic.lean
View file

@ -1,59 +0,0 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.data.repr
universes u v
inductive Ordering
| lt | Eq | gt
instance : HasRepr Ordering :=
⟨(fun s => match s with | Ordering.lt => "lt" | Ordering.Eq => "Eq" | Ordering.gt => "gt")⟩
namespace Ordering
def swap : Ordering → Ordering
| lt => gt
| Eq => Eq
| gt => lt
@[inline] def orElse : Ordering → Ordering → Ordering
| lt, _ => lt
| Eq, o => o
| gt, _ => gt
theorem swapSwap : ∀ (o : Ordering), o.swap.swap = o
| lt => rfl
| Eq => rfl
| gt => rfl
end Ordering
@[inline] def cmpUsing {α : Type u} (lt : α → α → Prop) [DecidableRel lt] (a b : α) : Ordering :=
if lt a b then Ordering.lt
else if lt b a then Ordering.gt
else Ordering.Eq
def cmp {α : Type u} [HasLess α] [DecidableRel (HasLess.Less : α → α → Prop)] (a b : α) : Ordering :=
cmpUsing HasLess.Less a b
instance : DecidableEq Ordering :=
{decEq := fun a b =>
match a with
| Ordering.lt =>
match b with
| Ordering.lt => isTrue rfl
| Ordering.Eq => isFalse (fun h => Ordering.noConfusion h)
| Ordering.gt => isFalse (fun h => Ordering.noConfusion h)
| Ordering.Eq =>
match b with
| Ordering.lt => isFalse (fun h => Ordering.noConfusion h)
| Ordering.Eq => isTrue rfl
| Ordering.gt => isFalse (fun h => Ordering.noConfusion h)
| Ordering.gt =>
match b with
| Ordering.lt => isFalse (fun h => Ordering.noConfusion h)
| Ordering.Eq => isFalse (fun h => Ordering.noConfusion h)
| Ordering.gt => isTrue rfl}

7
library/init/data/ordering/default.lean
View file

@ -1,7 +0,0 @@
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import .basic

2
src/stage0/CMakeLists.txt
View file

@ -1 +1 @@
add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/binomialheap/basic.cpp ./init/data/binomialheap/default.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/persistenthashmap/basic.cpp ./init/data/persistenthashmap/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/fix.cpp ./init/lean/attributes.cpp ./init/lean/class.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/implementedbyattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inlineattrs.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/namemangling.cpp ./init/lean/compiler/specialize.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/elaborator/alias.cpp ./init/lean/elaborator/basic.cpp ./init/lean/elaborator/command.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/eqncompiler/default.cpp ./init/lean/eqncompiler/matchpattern.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/localcontext.cpp ./init/lean/message.cpp ./init/lean/metavarcontext.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/namegenerator.cpp ./init/lean/options.cpp ./init/lean/parser/command.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/term.cpp ./init/lean/parser/transform.cpp ./init/lean/parser/trie.cpp ./init/lean/path.cpp ./init/lean/position.cpp ./init/lean/projfns.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/scopes.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/system/default.cpp ./init/system/filepath.cpp ./init/system/io.cpp ./init/system/platform.cpp ./init/util.cpp ./init/wf.cpp)
add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/binomialheap/basic.cpp ./init/data/binomialheap/default.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/persistenthashmap/basic.cpp ./init/data/persistenthashmap/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/fix.cpp ./init/lean/attributes.cpp ./init/lean/class.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/implementedbyattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inlineattrs.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/namemangling.cpp ./init/lean/compiler/specialize.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/elaborator/alias.cpp ./init/lean/elaborator/basic.cpp ./init/lean/elaborator/command.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/eqncompiler/default.cpp ./init/lean/eqncompiler/matchpattern.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/localcontext.cpp ./init/lean/message.cpp ./init/lean/metavarcontext.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/namegenerator.cpp ./init/lean/options.cpp ./init/lean/parser/command.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/term.cpp ./init/lean/parser/transform.cpp ./init/lean/parser/trie.cpp ./init/lean/path.cpp ./init/lean/position.cpp ./init/lean/projfns.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/scopes.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/system/default.cpp ./init/system/filepath.cpp ./init/system/io.cpp ./init/system/platform.cpp ./init/util.cpp ./init/wf.cpp)

5
src/stage0/init/data/basic.cpp generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: init.data.basic
// Imports: init.data.nat.basic init.data.fin.basic init.data.list.basic init.data.char.basic init.data.string.basic init.data.option.basic init.data.uint init.data.ordering.basic init.data.repr init.data.tostring
// Imports: init.data.nat.basic init.data.fin.basic init.data.list.basic init.data.char.basic init.data.string.basic init.data.option.basic init.data.uint init.data.repr init.data.tostring
#include "runtime/object.h"
#include "runtime/apply.h"
typedef lean::object obj; typedef lean::usize usize;
@ -21,7 +21,6 @@ obj* initialize_init_data_char_basic(obj*);
obj* initialize_init_data_string_basic(obj*);
obj* initialize_init_data_option_basic(obj*);
obj* initialize_init_data_uint(obj*);
obj* initialize_init_data_ordering_basic(obj*);
obj* initialize_init_data_repr(obj*);
obj* initialize_init_data_tostring(obj*);
static bool _G_initialized = false;
@ -43,8 +42,6 @@ w = initialize_init_data_option_basic(w);
if (io_result_is_error(w)) return w;
w = initialize_init_data_uint(w);
if (io_result_is_error(w)) return w;
w = initialize_init_data_ordering_basic(w);
if (io_result_is_error(w)) return w;
w = initialize_init_data_repr(w);
if (io_result_is_error(w)) return w;
w = initialize_init_data_tostring(w);

5
src/stage0/init/data/default.cpp generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: init.data.default
// Imports: init.data.basic init.data.nat.default init.data.char.default init.data.string.default init.data.list.default init.data.int.default init.data.array.default init.data.bytearray.default init.data.fin.default init.data.uint init.data.ordering.default init.data.rbtree.default init.data.rbmap.default init.data.option.basic init.data.option.instances init.data.hashmap.default init.data.random
// Imports: init.data.basic init.data.nat.default init.data.char.default init.data.string.default init.data.list.default init.data.int.default init.data.array.default init.data.bytearray.default init.data.fin.default init.data.uint init.data.rbtree.default init.data.rbmap.default init.data.option.basic init.data.option.instances init.data.hashmap.default init.data.random
#include "runtime/object.h"
#include "runtime/apply.h"
typedef lean::object obj; typedef lean::usize usize;
@ -24,7 +24,6 @@ obj* initialize_init_data_array_default(obj*);
obj* initialize_init_data_bytearray_default(obj*);
obj* initialize_init_data_fin_default(obj*);
obj* initialize_init_data_uint(obj*);
obj* initialize_init_data_ordering_default(obj*);
obj* initialize_init_data_rbtree_default(obj*);
obj* initialize_init_data_rbmap_default(obj*);
obj* initialize_init_data_option_basic(obj*);
@ -56,8 +55,6 @@ w = initialize_init_data_fin_default(w);
if (io_result_is_error(w)) return w;
w = initialize_init_data_uint(w);
if (io_result_is_error(w)) return w;
w = initialize_init_data_ordering_default(w);
if (io_result_is_error(w)) return w;
w = initialize_init_data_rbtree_default(w);
if (io_result_is_error(w)) return w;
w = initialize_init_data_rbmap_default(w);

431
src/stage0/init/data/ordering/basic.cpp generated
View file

@ -1,431 +0,0 @@
// Lean compiler output
// Module: init.data.ordering.basic
// Imports: init.data.repr
#include "runtime/object.h"
#include "runtime/apply.h"
typedef lean::object obj; typedef lean::usize usize;
typedef lean::uint8 uint8; typedef lean::uint16 uint16;
typedef lean::uint32 uint32; typedef lean::uint64 uint64;
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
obj* l_cmp(obj*, obj*);
obj* l_Ordering_HasRepr___closed__1;
obj* l_cmp___rarg___boxed(obj*, obj*, obj*);
obj* l_cmpUsing(obj*, obj*);
obj* l_Ordering_orElse___boxed(obj*, obj*);
uint8 l_Ordering_orElse___main(uint8, uint8);
obj* l_Ordering_HasRepr(uint8);
obj* l_Ordering_orElse___main___boxed(obj*, obj*);
uint8 l_Ordering_swap___main(uint8);
obj* l_cmpUsing___rarg___boxed(obj*, obj*, obj*);
obj* l_Ordering_HasRepr___boxed(obj*);
obj* l_Ordering_HasRepr___closed__3;
obj* l_Ordering_swap___main___boxed(obj*);
uint8 l_cmpUsing___rarg(obj*, obj*, obj*);
uint8 l_Ordering_swap(uint8);
obj* l_Ordering_HasRepr___closed__2;
obj* l_Ordering_DecidableEq___boxed(obj*, obj*);
obj* l_cmpUsing___boxed(obj*, obj*);
uint8 l_Ordering_DecidableEq(uint8, uint8);
uint8 l_cmp___rarg(obj*, obj*, obj*);
uint8 l_Ordering_orElse(uint8, uint8);
obj* l_Ordering_swap___boxed(obj*);
obj* l_cmp___boxed(obj*, obj*);
obj* _init_l_Ordering_HasRepr___closed__1() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("lt");
return x_1;
}
}
obj* _init_l_Ordering_HasRepr___closed__2() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("Eq");
return x_1;
}
}
obj* _init_l_Ordering_HasRepr___closed__3() {
_start:
{
obj* x_1;
x_1 = lean::mk_string("gt");
return x_1;
}
}
obj* l_Ordering_HasRepr(uint8 x_1) {
_start:
{
switch (x_1) {
case 0:
{
obj* x_2;
x_2 = l_Ordering_HasRepr___closed__1;
return x_2;
}
case 1:
{
obj* x_3;
x_3 = l_Ordering_HasRepr___closed__2;
return x_3;
}
default:
{
obj* x_4;
x_4 = l_Ordering_HasRepr___closed__3;
return x_4;
}
}
}
}
obj* l_Ordering_HasRepr___boxed(obj* x_1) {
_start:
{
uint8 x_2; obj* x_3;
x_2 = lean::unbox(x_1);
lean::dec(x_1);
x_3 = l_Ordering_HasRepr(x_2);
return x_3;
}
}
uint8 l_Ordering_swap___main(uint8 x_1) {
_start:
{
switch (x_1) {
case 0:
{
uint8 x_2;
x_2 = 2;
return x_2;
}
case 1:
{
return x_1;
}
default:
{
uint8 x_3;
x_3 = 0;
return x_3;
}
}
}
}
obj* l_Ordering_swap___main___boxed(obj* x_1) {
_start:
{
uint8 x_2; uint8 x_3; obj* x_4;
x_2 = lean::unbox(x_1);
lean::dec(x_1);
x_3 = l_Ordering_swap___main(x_2);
x_4 = lean::box(x_3);
return x_4;
}
}
uint8 l_Ordering_swap(uint8 x_1) {
_start:
{
uint8 x_2;
x_2 = l_Ordering_swap___main(x_1);
return x_2;
}
}
obj* l_Ordering_swap___boxed(obj* x_1) {
_start:
{
uint8 x_2; uint8 x_3; obj* x_4;
x_2 = lean::unbox(x_1);
lean::dec(x_1);
x_3 = l_Ordering_swap(x_2);
x_4 = lean::box(x_3);
return x_4;
}
}
uint8 l_Ordering_orElse___main(uint8 x_1, uint8 x_2) {
_start:
{
obj* x_3;
x_3 = lean::box(x_1);
if (lean::obj_tag(x_3) == 1)
{
return x_2;
}
else
{
lean::dec(x_3);
return x_1;
}
}
}
obj* l_Ordering_orElse___main___boxed(obj* x_1, obj* x_2) {
_start:
{
uint8 x_3; uint8 x_4; uint8 x_5; obj* x_6;
x_3 = lean::unbox(x_1);
lean::dec(x_1);
x_4 = lean::unbox(x_2);
lean::dec(x_2);
x_5 = l_Ordering_orElse___main(x_3, x_4);
x_6 = lean::box(x_5);
return x_6;
}
}
uint8 l_Ordering_orElse(uint8 x_1, uint8 x_2) {
_start:
{
obj* x_3;
x_3 = lean::box(x_1);
if (lean::obj_tag(x_3) == 1)
{
return x_2;
}
else
{
lean::dec(x_3);
return x_1;
}
}
}
obj* l_Ordering_orElse___boxed(obj* x_1, obj* x_2) {
_start:
{
uint8 x_3; uint8 x_4; uint8 x_5; obj* x_6;
x_3 = lean::unbox(x_1);
lean::dec(x_1);
x_4 = lean::unbox(x_2);
lean::dec(x_2);
x_5 = l_Ordering_orElse(x_3, x_4);
x_6 = lean::box(x_5);
return x_6;
}
}
uint8 l_cmpUsing___rarg(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4; uint8 x_5;
lean::inc(x_1);
lean::inc(x_3);
lean::inc(x_2);
x_4 = lean::apply_2(x_1, x_2, x_3);
x_5 = lean::unbox(x_4);
lean::dec(x_4);
if (x_5 == 0)
{
obj* x_6; uint8 x_7;
x_6 = lean::apply_2(x_1, x_3, x_2);
x_7 = lean::unbox(x_6);
lean::dec(x_6);
if (x_7 == 0)
{
uint8 x_8;
x_8 = 1;
return x_8;
}
else
{
uint8 x_9;
x_9 = 2;
return x_9;
}
}
else
{
uint8 x_10;
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
x_10 = 0;
return x_10;
}
}
}
obj* l_cmpUsing(obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_cmpUsing___rarg___boxed), 3, 0);
return x_3;
}
}
obj* l_cmpUsing___rarg___boxed(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
uint8 x_4; obj* x_5;
x_4 = l_cmpUsing___rarg(x_1, x_2, x_3);
x_5 = lean::box(x_4);
return x_5;
}
}
obj* l_cmpUsing___boxed(obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = l_cmpUsing(x_1, x_2);
lean::dec(x_2);
return x_3;
}
}
uint8 l_cmp___rarg(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4; uint8 x_5;
lean::inc(x_1);
lean::inc(x_3);
lean::inc(x_2);
x_4 = lean::apply_2(x_1, x_2, x_3);
x_5 = lean::unbox(x_4);
lean::dec(x_4);
if (x_5 == 0)
{
obj* x_6; uint8 x_7;
x_6 = lean::apply_2(x_1, x_3, x_2);
x_7 = lean::unbox(x_6);
lean::dec(x_6);
if (x_7 == 0)
{
uint8 x_8;
x_8 = 1;
return x_8;
}
else
{
uint8 x_9;
x_9 = 2;
return x_9;
}
}
else
{
uint8 x_10;
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
x_10 = 0;
return x_10;
}
}
}
obj* l_cmp(obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_cmp___rarg___boxed), 3, 0);
return x_3;
}
}
obj* l_cmp___rarg___boxed(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
uint8 x_4; obj* x_5;
x_4 = l_cmp___rarg(x_1, x_2, x_3);
x_5 = lean::box(x_4);
return x_5;
}
}
obj* l_cmp___boxed(obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = l_cmp(x_1, x_2);
lean::dec(x_2);
return x_3;
}
}
uint8 l_Ordering_DecidableEq(uint8 x_1, uint8 x_2) {
_start:
{
switch (x_1) {
case 0:
{
obj* x_3;
x_3 = lean::box(x_2);
if (lean::obj_tag(x_3) == 0)
{
uint8 x_4;
x_4 = 1;
return x_4;
}
else
{
uint8 x_5;
lean::dec(x_3);
x_5 = 0;
return x_5;
}
}
case 1:
{
obj* x_6;
x_6 = lean::box(x_2);
if (lean::obj_tag(x_6) == 1)
{
uint8 x_7;
x_7 = 1;
return x_7;
}
else
{
uint8 x_8;
lean::dec(x_6);
x_8 = 0;
return x_8;
}
}
default:
{
obj* x_9;
x_9 = lean::box(x_2);
if (lean::obj_tag(x_9) == 2)
{
uint8 x_10;
x_10 = 1;
return x_10;
}
else
{
uint8 x_11;
lean::dec(x_9);
x_11 = 0;
return x_11;
}
}
}
}
}
obj* l_Ordering_DecidableEq___boxed(obj* x_1, obj* x_2) {
_start:
{
uint8 x_3; uint8 x_4; uint8 x_5; obj* x_6;
x_3 = lean::unbox(x_1);
lean::dec(x_1);
x_4 = lean::unbox(x_2);
lean::dec(x_2);
x_5 = l_Ordering_DecidableEq(x_3, x_4);
x_6 = lean::box(x_5);
return x_6;
}
}
obj* initialize_init_data_repr(obj*);
static bool _G_initialized = false;
obj* initialize_init_data_ordering_basic(obj* w) {
if (_G_initialized) return w;
_G_initialized = true;
if (io_result_is_error(w)) return w;
w = initialize_init_data_repr(w);
if (io_result_is_error(w)) return w;
l_Ordering_HasRepr___closed__1 = _init_l_Ordering_HasRepr___closed__1();
lean::mark_persistent(l_Ordering_HasRepr___closed__1);
l_Ordering_HasRepr___closed__2 = _init_l_Ordering_HasRepr___closed__2();
lean::mark_persistent(l_Ordering_HasRepr___closed__2);
l_Ordering_HasRepr___closed__3 = _init_l_Ordering_HasRepr___closed__3();
lean::mark_persistent(l_Ordering_HasRepr___closed__3);
return w;
}

26
src/stage0/init/data/ordering/default.cpp generated
View file

@ -1,26 +0,0 @@
// Lean compiler output
// Module: init.data.ordering.default
// Imports: init.data.ordering.basic
#include "runtime/object.h"
#include "runtime/apply.h"
typedef lean::object obj; typedef lean::usize usize;
typedef lean::uint8 uint8; typedef lean::uint16 uint16;
typedef lean::uint32 uint32; typedef lean::uint64 uint64;
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
obj* initialize_init_data_ordering_basic(obj*);
static bool _G_initialized = false;
obj* initialize_init_data_ordering_default(obj* w) {
if (_G_initialized) return w;
_G_initialized = true;
if (io_result_is_error(w)) return w;
w = initialize_init_data_ordering_basic(w);
if (io_result_is_error(w)) return w;
return w;
}

251
src/stage0/init/lean/syntax.cpp generated
View file

@ -36,6 +36,7 @@ obj* nat_sub(obj*, obj*);
obj* l_Lean_Syntax_ifNode(obj*, obj*);
obj* l_Lean_nullKind___closed__2;
obj* l_Lean_stxInh(obj*);
obj* l_Lean_Syntax_setArg(obj*);
extern obj* l_Lean_Format_paren___closed__2;
obj* l_Lean_unreachIsNodeOther(obj*, obj*, obj*, obj*);
obj* l___private_init_lean_syntax_4__reprintLeaf(obj*, obj*);
@ -78,6 +79,7 @@ obj* l___private_init_lean_syntax_7__decodeHexLitAux___main(obj*, obj*, obj*);
extern obj* l_Lean_Format_sbracket___closed__1;
obj* l___private_init_lean_syntax_2__updateLeadingAux___main___rarg(obj*, obj*);
obj* l_Lean_SyntaxNode_getNumArgs___rarg(obj*);
obj* l_Lean_Syntax_modifyArg___rarg(obj*, obj*, obj*);
obj* l_Lean_charLitKind___closed__2;
obj* l_Lean_Syntax_asNode___main___rarg___boxed(obj*);
obj* l_Lean_Syntax_setTailInfo(obj*);
@ -107,6 +109,7 @@ obj* l_Lean_Syntax_formatStx___main___rarg___closed__3;
obj* l_Lean_Syntax_formatStx___rarg(obj*);
extern obj* l_Lean_Format_sbracket___closed__2;
obj* l___private_init_lean_syntax_4__reprintLeaf___main___boxed(obj*, obj*);
obj* l_Lean_Syntax_setArg___rarg(obj*, obj*, obj*);
obj* l_Lean_Syntax_isStrLit___main(obj*);
obj* l_Lean_Syntax_isOfKind___main___rarg___boxed(obj*, obj*);
obj* l_Array_mfindRevAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___rarg___boxed(obj*, obj*, obj*);
@ -207,6 +210,7 @@ obj* l_Lean_strLitKind;
obj* l_Lean_Syntax_isOfKind___rarg___boxed(obj*, obj*);
obj* l_Lean_Syntax_asNode___main___rarg(obj*);
obj* l_List_map___main___at_Lean_Syntax_formatStx___main___spec__1___rarg(obj*);
obj* l_Lean_Syntax_setArgs(obj*);
obj* l_Lean_choiceKind___closed__2;
obj* l___private_init_lean_syntax_4__reprintLeaf___boxed(obj*, obj*);
obj* l_Lean_Syntax_reprint(obj*);
@ -215,6 +219,7 @@ obj* l_Lean_Syntax_getHeadInfo(obj*);
namespace lean {
uint32 string_utf8_get(obj*, obj*);
}
obj* l_Lean_Syntax_modifyArg(obj*);
obj* l_Lean_Syntax_mreplace___rarg(obj*, obj*, obj*);
obj* l_Lean_unreachIsNodeMissing(obj*, obj*, obj*);
obj* l_Array_ummapAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg(obj*, obj*, obj*, obj*);
@ -236,7 +241,6 @@ obj* l___private_init_lean_syntax_7__decodeHexLitAux(obj*, obj*, obj*);
obj* l_Lean_Syntax_isIdent(obj*);
obj* l_Array_mfindAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(obj*);
obj* l_Lean_Syntax_mrewriteBottomUp___main___at_Lean_Syntax_rewriteBottomUp___spec__1___rarg(obj*, obj*);
obj* l_Lean_SyntaxNode_updateArgs(obj*);
obj* l___private_init_lean_syntax_5__decodeBinLitAux(obj*, obj*, obj*);
obj* l_Lean_Syntax_reprint___rarg___boxed(obj*);
obj* l___private_init_lean_syntax_5__decodeBinLitAux___main___boxed(obj*, obj*, obj*);
@ -247,11 +251,14 @@ obj* l_Lean_SyntaxNode_getKind___rarg___boxed(obj*);
obj* l_Lean_Syntax_getId___main___rarg___boxed(obj*);
obj* l_Lean_Format_joinSep___main___at_Lean_Syntax_formatStx___main___spec__2___boxed(obj*, obj*);
obj* l_Lean_SyntaxNode_getArg___rarg___boxed(obj*, obj*);
obj* l_Lean_Syntax_setArgs___rarg(obj*, obj*);
obj* l___private_init_lean_syntax_1__updateInfo(obj*, obj*);
obj* l___private_init_lean_syntax_8__decodeDecimalLitAux___main___boxed(obj*, obj*, obj*);
uint8 l_Char_isDigit(uint32);
uint8 l_Lean_Syntax_isOfKind___main___rarg(obj*, obj*);
obj* l_Lean_Syntax_modifyArgs___rarg(obj*, obj*);
obj* l___private_init_lean_syntax_3__updateLast___main___at_Lean_Syntax_setTailInfoAux___main___spec__1___rarg(obj*, obj*, obj*);
obj* l_Lean_Syntax_modifyArgs(obj*);
obj* l_Array_ummapAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l___private_init_lean_syntax_3__updateLast___main___rarg(obj*, obj*, obj*, obj*);
obj* l_Lean_Syntax_getIdAt___rarg___boxed(obj*, obj*);
@ -297,7 +304,6 @@ obj* l_Array_ummapAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg(o
obj* l_Lean_Syntax_isMissing___main___rarg___boxed(obj*);
obj* l_Lean_Syntax_isNatLitAux___main___rarg___boxed(obj*, obj*);
obj* l_Lean_Syntax_getId___rarg___boxed(obj*);
obj* l_Lean_SyntaxNode_updateArgs___rarg(obj*, obj*);
obj* l_Lean_Syntax_formatStx___main___rarg___closed__5;
obj* l_Lean_unreachIsNodeAtom___boxed(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Syntax_isFieldIdx___rarg(obj*);
@ -315,6 +321,7 @@ obj* string_utf8_extract(obj*, obj*, obj*);
}
obj* l_Lean_Syntax_ifNodeKind___rarg___boxed(obj*, obj*, obj*, obj*);
obj* l_Array_mfindRevAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___rarg(obj*, obj*, obj*);
obj* l_Lean_SyntaxNode_modifyArgs___rarg(obj*, obj*);
obj* l_Lean_Syntax_getPos___rarg(obj*);
namespace lean {
obj* string_utf8_byte_size(obj*);
@ -331,6 +338,7 @@ obj* l_Array_set(obj*, obj*, obj*, obj*);
obj* l_Lean_Syntax_isStrLit___rarg___boxed(obj*);
obj* l_Lean_Syntax_HasToString___closed__1;
obj* l___private_init_lean_syntax_7__decodeHexLitAux___boxed(obj*, obj*, obj*);
obj* l_Lean_SyntaxNode_modifyArgs(obj*);
obj* l_Lean_strLitKind___closed__2;
obj* l_Lean_Syntax_formatStx___main___rarg___closed__7;
obj* l_String_quote(obj*);
@ -358,7 +366,9 @@ obj* nat_mul(obj*, obj*);
obj* l_Lean_Syntax_isIdOrAtom___main(obj*);
obj* l___private_init_lean_syntax_5__decodeBinLitAux___boxed(obj*, obj*, obj*);
obj* l_Lean_Syntax_mrewriteBottomUp___main___at_Lean_Syntax_rewriteBottomUp___spec__1(obj*);
obj* l_Lean_Syntax_modifyArg___rarg___boxed(obj*, obj*, obj*);
obj* l_Lean_Syntax_getTailInfo___rarg___boxed(obj*);
obj* l_Lean_Syntax_setArg___rarg___boxed(obj*, obj*, obj*);
obj* l_Lean_Syntax_formatStx___main___rarg___closed__4;
obj* l_Lean_charLitKind;
obj* l_Lean_Syntax_mrewriteBottomUp___main___boxed(obj*, obj*);
@ -1058,7 +1068,7 @@ lean::dec(x_1);
return x_2;
}
}
obj* l_Lean_SyntaxNode_updateArgs___rarg(obj* x_1, obj* x_2) {
obj* l_Lean_SyntaxNode_modifyArgs___rarg(obj* x_1, obj* x_2) {
_start:
{
uint8 x_3;
@ -1087,11 +1097,11 @@ return x_9;
}
}
}
obj* l_Lean_SyntaxNode_updateArgs(obj* x_1) {
obj* l_Lean_SyntaxNode_modifyArgs(obj* x_1) {
_start:
{
obj* x_2;
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_SyntaxNode_updateArgs___rarg), 2, 0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_SyntaxNode_modifyArgs___rarg), 2, 0);
return x_2;
}
}
@ -1582,6 +1592,237 @@ lean::dec(x_1);
return x_3;
}
}
obj* l_Lean_Syntax_setArgs___rarg(obj* x_1, obj* x_2) {
_start:
{
if (lean::obj_tag(x_1) == 1)
{
uint8 x_3;
x_3 = !lean::is_exclusive(x_1);
if (x_3 == 0)
{
obj* x_4;
x_4 = lean::cnstr_get(x_1, 1);
lean::dec(x_4);
lean::cnstr_set(x_1, 1, x_2);
return x_1;
}
else
{
obj* x_5; obj* x_6;
x_5 = lean::cnstr_get(x_1, 0);
lean::inc(x_5);
lean::dec(x_1);
x_6 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_6, 0, x_5);
lean::cnstr_set(x_6, 1, x_2);
return x_6;
}
}
else
{
lean::dec(x_2);
return x_1;
}
}
}
obj* l_Lean_Syntax_setArgs(obj* x_1) {
_start:
{
obj* x_2;
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Syntax_setArgs___rarg), 2, 0);
return x_2;
}
}
obj* l_Lean_Syntax_modifyArgs___rarg(obj* x_1, obj* x_2) {
_start:
{
if (lean::obj_tag(x_1) == 1)
{
uint8 x_3;
x_3 = !lean::is_exclusive(x_1);
if (x_3 == 0)
{
obj* x_4; obj* x_5;
x_4 = lean::cnstr_get(x_1, 1);
x_5 = lean::apply_1(x_2, x_4);
lean::cnstr_set(x_1, 1, x_5);
return x_1;
}
else
{
obj* x_6; obj* x_7; obj* x_8; obj* x_9;
x_6 = lean::cnstr_get(x_1, 0);
x_7 = lean::cnstr_get(x_1, 1);
lean::inc(x_7);
lean::inc(x_6);
lean::dec(x_1);
x_8 = lean::apply_1(x_2, x_7);
x_9 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_9, 0, x_6);
lean::cnstr_set(x_9, 1, x_8);
return x_9;
}
}
else
{
lean::dec(x_2);
return x_1;
}
}
}
obj* l_Lean_Syntax_modifyArgs(obj* x_1) {
_start:
{
obj* x_2;
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Syntax_modifyArgs___rarg), 2, 0);
return x_2;
}
}
obj* l_Lean_Syntax_setArg___rarg(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
if (lean::obj_tag(x_1) == 1)
{
uint8 x_4;
x_4 = !lean::is_exclusive(x_1);
if (x_4 == 0)
{
obj* x_5; obj* x_6;
x_5 = lean::cnstr_get(x_1, 1);
x_6 = lean::array_set(x_5, x_2, x_3);
lean::cnstr_set(x_1, 1, x_6);
return x_1;
}
else
{
obj* x_7; obj* x_8; obj* x_9; obj* x_10;
x_7 = lean::cnstr_get(x_1, 0);
x_8 = lean::cnstr_get(x_1, 1);
lean::inc(x_8);
lean::inc(x_7);
lean::dec(x_1);
x_9 = lean::array_set(x_8, x_2, x_3);
x_10 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_10, 0, x_7);
lean::cnstr_set(x_10, 1, x_9);
return x_10;
}
}
else
{
lean::dec(x_3);
return x_1;
}
}
}
obj* l_Lean_Syntax_setArg(obj* x_1) {
_start:
{
obj* x_2;
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Syntax_setArg___rarg___boxed), 3, 0);
return x_2;
}
}
obj* l_Lean_Syntax_setArg___rarg___boxed(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4;
x_4 = l_Lean_Syntax_setArg___rarg(x_1, x_2, x_3);
lean::dec(x_2);
return x_4;
}
}
obj* l_Lean_Syntax_modifyArg___rarg(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
if (lean::obj_tag(x_1) == 1)
{
uint8 x_4;
x_4 = !lean::is_exclusive(x_1);
if (x_4 == 0)
{
obj* x_5; obj* x_6; uint8 x_7;
x_5 = lean::cnstr_get(x_1, 1);
x_6 = lean::array_get_size(x_5);
x_7 = lean::nat_dec_lt(x_2, x_6);
lean::dec(x_6);
if (x_7 == 0)
{
lean::dec(x_3);
return x_1;
}
else
{
obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12;
x_8 = lean::array_fget(x_5, x_2);
x_9 = lean::box(0);
x_10 = lean::array_fset(x_5, x_2, x_9);
x_11 = lean::apply_1(x_3, x_8);
x_12 = lean::array_fset(x_10, x_2, x_11);
lean::cnstr_set(x_1, 1, x_12);
return x_1;
}
}
else
{
obj* x_13; obj* x_14; obj* x_15; uint8 x_16;
x_13 = lean::cnstr_get(x_1, 0);
x_14 = lean::cnstr_get(x_1, 1);
lean::inc(x_14);
lean::inc(x_13);
lean::dec(x_1);
x_15 = lean::array_get_size(x_14);
x_16 = lean::nat_dec_lt(x_2, x_15);
lean::dec(x_15);
if (x_16 == 0)
{
obj* x_17;
lean::dec(x_3);
x_17 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_17, 0, x_13);
lean::cnstr_set(x_17, 1, x_14);
return x_17;
}
else
{
obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23;
x_18 = lean::array_fget(x_14, x_2);
x_19 = lean::box(0);
x_20 = lean::array_fset(x_14, x_2, x_19);
x_21 = lean::apply_1(x_3, x_18);
x_22 = lean::array_fset(x_20, x_2, x_21);
x_23 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_23, 0, x_13);
lean::cnstr_set(x_23, 1, x_22);
return x_23;
}
}
}
else
{
lean::dec(x_3);
return x_1;
}
}
}
obj* l_Lean_Syntax_modifyArg(obj* x_1) {
_start:
{
obj* x_2;
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Syntax_modifyArg___rarg___boxed), 3, 0);
return x_2;
}
}
obj* l_Lean_Syntax_modifyArg___rarg___boxed(obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4;
x_4 = l_Lean_Syntax_modifyArg___rarg(x_1, x_2, x_3);
lean::dec(x_2);
return x_4;
}
}
obj* l_Lean_Syntax_getIdAt___rarg(obj* x_1, obj* x_2) {
_start:
{