feat(library/init/lean): unsafe support in the new frontend

library/init/lean/elaborator.lean

@@ -392,7 +392,7 @@ def decl_modifiers_to_pexpr (mods : decl_modifiers.view) : elaborator_m expr :=
     | some (visibility.view.protected _) := mdata.set_bool `protected tt
     | _ := mdata,
   let mdata := mdata.set_bool `noncomputable mods.noncomputable.is_some,
-  let mdata := mdata.set_bool `meta mods.meta.is_some,
+  let mdata := mdata.set_bool `unsafe mods.unsafe.is_some,
   expr.mdata mdata <$> attrs_to_pexpr (match mods.attrs with
     | some attrs := attrs.attrs
     | none       := [])

library/init/lean/parser/command.lean

@@ -117,7 +117,7 @@ def builtin_command_parsers : token_map command_parser := token_map.of_list [
   ("private", declaration.parser),
   ("protected", declaration.parser),
   ("noncomputable", declaration.parser),
-  ("meta", declaration.parser),
+  ("unsafe", declaration.parser),
   ("def", declaration.parser),
   ("abbreviation", declaration.parser),
   ("theorem", declaration.parser),

library/init/lean/parser/declaration.lean

@@ -46,7 +46,7 @@ node! decl_modifiers [
   attrs: decl_attributes.parser?,
   visibility: node_choice! visibility {"private", "protected"}?,
   «noncomputable»: (symbol "noncomputable")?,
-  «meta»: (symbol "meta")?,
+  «unsafe»: (symbol "unsafe")?,
 ]
 
 @[derive has_tokens has_view]

src/boot/init/io.cpp

@@ -111,14 +111,14 @@ obj* l_io_prim_iterate___at_io_fs_handle_read__to__end___spec__4___lambda__1(obj
 obj* l_io_fs_handle_get__line___rarg(obj*, obj*, obj*, obj*, obj*);
 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*);
+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*);
 extern "C" obj* lean_io_prim_handle_get_line(obj*, obj*);
-obj* l_unsafe__io___boxed(obj*, obj*);
+obj* l_unsafe__io___boxed(obj*, obj*, obj*);
 obj* l_io_lazy__pure(obj*);
 obj* l_io_fs_handle_mk(obj*, obj*);
 obj* l_io_fs_read__file___rarg___lambda__1___boxed(obj*, obj*, obj*);
@@ -181,12 +181,12 @@ x_10 = l_state__t_monad___rarg(x_9);
 return x_10;
 }
 }
-obj* l_unsafe__io___boxed(obj* x_0, obj* x_1) {
+obj* l_unsafe__io___boxed(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {
-obj* x_2; 
-x_2 = lean_io_unsafe(x_0, x_1);
-return x_2;
+obj* x_3; 
+x_3 = lean_io_unsafe(x_0, x_1, x_2);
+return x_3;
 }
 }
 obj* l_timeit___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {

src/boot/init/lean/elaborator.cpp

@@ -17715,7 +17715,7 @@ _start:
 {
 obj* x_0; obj* x_1; obj* x_2; 
 x_0 = lean::box(0);
-x_1 = lean::mk_string("meta");
+x_1 = lean::mk_string("unsafe");
 x_2 = lean_name_mk_string(x_0, x_1);
 return x_2;
 }

src/boot/init/lean/parser/command.cpp

@@ -13753,7 +13753,7 @@ lean::inc(x_3);
 x_21 = lean::alloc_cnstr(0, 2, 0);
 lean::cnstr_set(x_21, 0, x_19);
 lean::cnstr_set(x_21, 1, x_3);
-x_22 = lean::mk_string("meta");
+x_22 = lean::mk_string("unsafe");
 x_23 = lean_name_mk_string(x_0, x_22);
 lean::inc(x_3);
 x_25 = lean::alloc_cnstr(0, 2, 0);

src/boot/init/lean/parser/declaration.cpp

@@ -10421,7 +10421,7 @@ x_26 = l_lean_parser_symbol_tokens___rarg(x_25, x_5);
 lean::dec(x_25);
 x_28 = l_lean_parser_tokens___rarg(x_26);
 lean::dec(x_26);
-x_30 = lean::mk_string("meta");
+x_30 = lean::mk_string("unsafe");
 x_31 = l_lean_parser_symbol_tokens___rarg(x_30, x_5);
 lean::dec(x_30);
 x_33 = l_lean_parser_tokens___rarg(x_31);
@@ -10507,7 +10507,7 @@ lean::closure_set(x_30, 1, x_9);
 lean::closure_set(x_30, 2, x_29);
 x_31 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1);
 lean::closure_set(x_31, 0, x_30);
-x_32 = lean::mk_string("meta");
+x_32 = lean::mk_string("unsafe");
 x_33 = l_string_trim(x_32);
 lean::dec(x_32);
 lean::inc(x_33);
@@ -10607,7 +10607,7 @@ lean::closure_set(x_30, 1, x_9);
 lean::closure_set(x_30, 2, x_29);
 x_31 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1);
 lean::closure_set(x_31, 0, x_30);
-x_32 = lean::mk_string("meta");
+x_32 = lean::mk_string("unsafe");
 x_33 = l_string_trim(x_32);
 lean::dec(x_32);
 lean::inc(x_33);