chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
39abe04e67
commit
61259697bd
2 changed files with 3 additions and 131 deletions
21
stage0/src/Lean/Modifiers.lean
generated
21
stage0/src/Lean/Modifiers.lean
generated
|
|
@ -17,34 +17,19 @@ def addProtected (env : Environment) (n : Name) : Environment :=
|
|||
def isProtected (env : Environment) (n : Name) : Bool :=
|
||||
protectedExt.isTagged env n
|
||||
|
||||
builtin_initialize privateExt : EnvExtension Nat ← registerEnvExtension (pure 1)
|
||||
|
||||
/- Private name support.
|
||||
|
||||
Suppose the user marks as declaration `n` as private. Then, we create
|
||||
the name: `_private.<module_name>.<index> ++ n`.
|
||||
We say `_private.<module_name>.<index>` is the "private prefix"
|
||||
where `<index>` comes from the environment extension `privateExt`.
|
||||
the name: `_private.<module_name>.0 ++ n`.
|
||||
We say `_private.<module_name>.0` is the "private prefix"
|
||||
|
||||
We assume that `n` is a valid user name and does not contain
|
||||
`Name.num` constructors. Thus, we can easily convert from
|
||||
private internal name to user given name.
|
||||
private internal name to the user given name.
|
||||
-/
|
||||
|
||||
def privateHeader : Name := `_private
|
||||
|
||||
@[export lean_mk_private_prefix]
|
||||
def mkUniquePrivatePrefix (env : Environment) : Environment × Name :=
|
||||
let idx := privateExt.getState env
|
||||
let p := Name.mkNum (privateHeader ++ env.mainModule) idx
|
||||
let env := privateExt.setState env (idx+1)
|
||||
(env, p)
|
||||
|
||||
@[export lean_mk_private_name]
|
||||
def mkUniquePrivateName (env : Environment) (n : Name) : Environment × Name :=
|
||||
let (env, p) := mkUniquePrivatePrefix env
|
||||
(env, p ++ n)
|
||||
|
||||
def mkPrivateName (env : Environment) (n : Name) : Name :=
|
||||
Name.mkNum (privateHeader ++ env.mainModule) 0 ++ n
|
||||
|
||||
|
|
|
|||
113
stage0/stdlib/Lean/Modifiers.c
generated
113
stage0/stdlib/Lean/Modifiers.c
generated
|
|
@ -18,10 +18,7 @@ lean_object* l_Lean_protectedExt___closed__1;
|
|||
lean_object* l_Lean_protectedExt___closed__3;
|
||||
lean_object* lean_name_mk_string(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_protectedExt___closed__5;
|
||||
lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1;
|
||||
lean_object* l_Lean_privateHeader;
|
||||
lean_object* lean_mk_private_name(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(lean_object*, lean_object*);
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_3____closed__1;
|
||||
|
|
@ -32,22 +29,16 @@ uint8_t lean_is_private_name(lean_object*);
|
|||
lean_object* l_Lean_isPrivateName___boxed(lean_object*);
|
||||
lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_3____closed__2;
|
||||
uint8_t l_Lean_isPrivateName(lean_object*);
|
||||
lean_object* lean_nat_add(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_3_(lean_object*);
|
||||
lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_30_(lean_object*);
|
||||
lean_object* l___private_Lean_Modifiers_0__Lean_privateToUserNameAux_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_protectedExt___elambda__3___boxed(lean_object*, lean_object*);
|
||||
lean_object* lean_add_protected(lean_object*, lean_object*);
|
||||
extern lean_object* l_IO_instInhabitedError___closed__1;
|
||||
lean_object* lean_mk_private_prefix(lean_object*);
|
||||
lean_object* l_Lean_protectedExt;
|
||||
lean_object* l_Lean_mkUniquePrivateName_match__1___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkUniquePrivateName_match__1(lean_object*);
|
||||
lean_object* l_Lean_isPrivateName_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_protectedExt___elambda__2(lean_object*);
|
||||
lean_object* lean_private_prefix(lean_object*);
|
||||
lean_object* l_Lean_EnvExtensionInterfaceUnsafe_setState___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Modifiers_0__Lean_privateToUserNameAux_match__1(lean_object*);
|
||||
lean_object* l_Lean_isPrivateName_match__1(lean_object*);
|
||||
lean_object* l_Lean_isPrivateNameExport___boxed(lean_object*);
|
||||
|
|
@ -59,7 +50,6 @@ extern lean_object* l_Lean_EnvExtensionInterfaceUnsafe_instInhabitedExt___closed
|
|||
lean_object* l___private_Lean_Modifiers_0__Lean_privatePrefixAux(lean_object*);
|
||||
lean_object* l_Lean_protectedExt___elambda__3(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_protectedExt___elambda__4___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_privateExt;
|
||||
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkTagDeclarationExtension(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_TagDeclarationExtension_isTagged(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -67,9 +57,7 @@ lean_object* l_Lean_protectedExt___elambda__4___rarg(lean_object*);
|
|||
lean_object* l_Lean_isProtected___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Modifiers_0__Lean_privatePrefixAux___boxed(lean_object*);
|
||||
lean_object* l_Lean_protectedExt___elambda__1(lean_object*);
|
||||
lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_privateHeader___closed__2;
|
||||
lean_object* l_Lean_EnvExtensionInterfaceUnsafe_getState___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_protectedExt___elambda__4(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_protectedExt___closed__4;
|
||||
lean_object* l_Lean_privateHeader___closed__1;
|
||||
|
|
@ -262,25 +250,6 @@ x_4 = lean_box(x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = lean_unsigned_to_nat(1u);
|
||||
x_2 = lean_alloc_closure((void*)(l_EStateM_pure___rarg), 2, 1);
|
||||
lean_closure_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_initFn____x40_Lean_Modifiers___hyg_30_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
x_2 = l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1;
|
||||
x_3 = l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(x_2, x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_privateHeader___closed__1() {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -307,81 +276,6 @@ x_1 = l_Lean_privateHeader___closed__2;
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* lean_mk_private_prefix(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
x_2 = l_Lean_privateExt;
|
||||
x_3 = l_Lean_EnvExtensionInterfaceUnsafe_getState___rarg(x_2, x_1);
|
||||
lean_inc(x_1);
|
||||
x_4 = lean_environment_main_module(x_1);
|
||||
x_5 = l_Lean_privateHeader;
|
||||
x_6 = l_Lean_Name_append(x_5, x_4);
|
||||
lean_inc(x_3);
|
||||
x_7 = lean_name_mk_numeral(x_6, x_3);
|
||||
x_8 = lean_unsigned_to_nat(1u);
|
||||
x_9 = lean_nat_add(x_3, x_8);
|
||||
lean_dec(x_3);
|
||||
x_10 = l_Lean_EnvExtensionInterfaceUnsafe_setState___rarg(x_2, x_1, x_9);
|
||||
x_11 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_11, 0, x_10);
|
||||
lean_ctor_set(x_11, 1, x_7);
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_mkUniquePrivateName_match__1___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_3);
|
||||
x_4 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_4);
|
||||
lean_dec(x_1);
|
||||
x_5 = lean_apply_2(x_2, x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_mkUniquePrivateName_match__1(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Lean_mkUniquePrivateName_match__1___rarg), 2, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* lean_mk_private_name(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; uint8_t x_4;
|
||||
x_3 = lean_mk_private_prefix(x_1);
|
||||
x_4 = !lean_is_exclusive(x_3);
|
||||
if (x_4 == 0)
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
x_5 = lean_ctor_get(x_3, 1);
|
||||
x_6 = l_Lean_Name_append(x_5, x_2);
|
||||
lean_dec(x_5);
|
||||
lean_ctor_set(x_3, 1, x_6);
|
||||
return x_3;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_7 = lean_ctor_get(x_3, 0);
|
||||
x_8 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_dec(x_3);
|
||||
x_9 = l_Lean_Name_append(x_8, x_2);
|
||||
lean_dec(x_8);
|
||||
x_10 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_10, 0, x_7);
|
||||
lean_ctor_set(x_10, 1, x_9);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_mkPrivateName(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -675,13 +569,6 @@ if (lean_io_result_is_error(res)) return res;
|
|||
l_Lean_protectedExt = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_protectedExt);
|
||||
lean_dec_ref(res);
|
||||
l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1 = _init_l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1();
|
||||
lean_mark_persistent(l_Lean_initFn____x40_Lean_Modifiers___hyg_30____closed__1);
|
||||
res = l_Lean_initFn____x40_Lean_Modifiers___hyg_30_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
l_Lean_privateExt = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_privateExt);
|
||||
lean_dec_ref(res);
|
||||
l_Lean_privateHeader___closed__1 = _init_l_Lean_privateHeader___closed__1();
|
||||
lean_mark_persistent(l_Lean_privateHeader___closed__1);
|
||||
l_Lean_privateHeader___closed__2 = _init_l_Lean_privateHeader___closed__2();
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue