chore(init/lean/ir): remove old IR

library/init/lean/ir/elim_phi.lean

@@ -1,82 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.lean.ir.instances init.control.state init.lean.disjoint_set
-
-namespace lean
-namespace ir
-/-
-We need to eliminate Phi nodes before we translate the IR to C/C++.
-
-The procedure is the following. First, for each instruction `x : ty := phi y_1 ... y_n`,
-we put `x`, `y_1`, ... `y_n` in the same equivalence class.
-Then, we select a representative from each equivalence class and replace each
-variable with its representative.
--/
-@[reducible] def elim_phi_m (α : Type) := state_t (disjoint_set var) id α
-
-def elim_phi_m.run {α} (a : elim_phi_m α) : α :=
-run a (mk_disjoint_set var)
-
-def merge (x y : var) : elim_phi_m unit :=
-modify $ λ s, s.merge x y
-
-def find (x : var) : elim_phi_m var :=
-do s ← get, pure $ s.find x
-
-def group_vars : decl → elim_phi_m unit
-| (decl.defn _ bs) := bs.mfor $ λ b, b.phis.mfor $ λ p, p.ys.mfor (merge p.x)
-| _                := pure ()
-
-def instr.replace_vars : instr → elim_phi_m instr
-| (instr.assign x ty y)            := instr.assign <$> find x <*> pure ty <*> find y
-| (instr.assign_lit x ty lit)      := instr.assign_lit <$> find x <*> pure ty <*> pure lit
-| (instr.assign_unop x ty op y)    := instr.assign_unop <$> find x <*> pure ty <*> pure op <*> find y
-| (instr.assign_binop x ty op y z) := instr.assign_binop <$> find x <*> pure ty <*> pure op <*> find y <*> find z
-| (instr.unop op x)                := instr.unop op <$> find x
-| (instr.call x f ys)              := instr.call <$> find x <*> pure f <*> ys.mmap find
-| (instr.cnstr o tag n s)          := instr.cnstr <$> find o <*> pure tag <*> pure n <*> pure s
-| (instr.set o i x)                := instr.set <$> find o <*> pure i <*> find x
-| (instr.get x o i)                := instr.get <$> find x <*> find o <*> pure i
-| (instr.sset o i x)               := instr.sset <$> find o <*> pure i <*> find x
-| (instr.sget x ty o i)            := instr.sget <$> find x <*> pure ty <*> find o <*> pure i
-| (instr.closure x f ys)           := instr.closure <$> find x <*> pure f <*> ys.mmap find
-| (instr.apply x ys)               := instr.apply <$> find x <*> ys.mmap find
-| (instr.array a sz c)             := instr.array <$> find a <*> find sz <*> find c
-| (instr.array_write a i v)        := instr.array_write <$> find a <*> find i <*> find v
-| (instr.sarray a ty sz c)         := instr.sarray <$> find a <*> pure ty <*> find sz <*> find c
-
-def terminator.replace_vars : terminator → elim_phi_m terminator
-| (terminator.ret x)    := terminator.ret <$> find x
-| (terminator.case x bs) := terminator.case <$> find x <*> pure bs
-| j@(terminator.jmp _)   := pure j
-
-def arg.replace_vars (a : arg) : elim_phi_m arg :=
-do x ← find a.n, pure { n := x, ..a }
-
-def header.replace_vars (h : header) : elim_phi_m header :=
-do as ← h.args.mmap arg.replace_vars, pure { args := as, ..h }
-
-def block.replace_vars (b : block) : elim_phi_m block :=
-do instrs' ← b.instrs.mmap instr.replace_vars,
-   term'   ← b.term.replace_vars,
-   pure
-     { phis   := [],
-       instrs := instrs',
-       term   := term', ..b}
-
-def decl.replace_vars : decl → elim_phi_m decl
-| (decl.defn h bs) := decl.defn <$> (header.replace_vars h) <*> bs.mmap block.replace_vars
-| other            := pure other
-
-def elim_phi_aux (d : decl) : elim_phi_m decl :=
-group_vars d *> d.replace_vars
-
-def elim_phi (d : decl) : decl :=
-(elim_phi_aux d).run
-
-end ir
-end lean

library/init/lean/ir/extract_cpp.lean

@@ -1,451 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.lean.name_mangling init.lean.config
-import init.lean.ir.type_check
-
-namespace lean
-namespace ir
-/--
-C++ code extraction configuration object.
-
-- `unit_name`: compilation unit name. The name is used to generate initialization/finalization procedures.
-- `unit_deps`: list of compilation units the given unit depends on. This information is also used to generate
-   initialization and finalization procedures.
-- `runtime_dir` : location of the Lean C++ runtime include files.
-- `env`: mapping from declaration name to declaration.
-- `external_names`: a mapping s.t. entry `(fid, n)` is in the mapping when we need to use name `n` for
-   declaration `fid` when emitting C++ code.
-- `main_proc`: name of the main procedure. Initialization and finalization code is inserted for it.
--/
-structure extract_cpp_config :=
-(unit_name : string := "main")
-(unit_deps : list string := [])
-(runtime_dir : string := "runtime")
-(env : environment := λ _, none)
-(external_names : fnid → option string := λ _, none)
-(main_proc : option fnid := none)
-
-namespace cpp
-def initialize_prefix := "_lean_initialize_"
-def finalize_prefix   := "_lean_finalize_"
-
-def file_header (runtime_dir : string) :=
-   "#include <" ++ runtime_dir ++ "/object.h>\n"
-++ "#include <" ++ runtime_dir ++ "/apply.h>\n"
-++ "typedef lean::object obj;"
-
-structure extract_env :=
-(cfg : extract_cpp_config)
-(ctx : context := mk_context)
-
-@[derive monad monad_except monad_state monad_reader monad_run]
-def extract_m := reader_t extract_env (except_t format (state_t string id))
-
-def emit {α} [has_to_string α] (a : α) : extract_m unit :=
-modify (++ (to_string a))
-
-def emit_line : extract_m unit :=
-emit "\n"
-
-@[inline] def paren {α} (a : extract_m α) : extract_m α :=
-emit "(" *> a <* emit ")"
-
-@[inline] def comma (a b : extract_m unit) : extract_m unit :=
-a *> emit ", " *> b
-
-local infix ` <+> `:65 := comma
-
-def emit_var (x : var) : extract_m unit :=
-emit $ name.mangle x "_x"
-
-def emit_blockid (b : blockid) : extract_m unit :=
-emit $ name.mangle b "_lbl"
-
-def fid2cpp (fid : fnid) : extract_m string :=
-do env ← read,
-   match env.cfg.external_names fid with
-   | some s := pure s
-   | none   := pure (name.mangle fid)
-
-def emit_fnid (fid : fnid) : extract_m unit :=
-fid2cpp fid >>= emit
-
-def is_const (fid : fnid) : extract_m bool :=
-do env ← read,
-   match env.cfg.env fid with
-   | some d := pure d.header.is_const
-   | none   := pure ff
-
-def global2cpp (fid : fnid) : extract_m string :=
-do s ← fid2cpp fid, pure $ "_g" ++ s
-
-def emit_global (fid : fnid) : extract_m unit :=
-global2cpp fid >>= emit
-
-def type2cpp : type → string
-| type.bool   := "unsigned char"  | type.byte   := "unsigned char"
-| type.uint16 := "unsigned short" | type.uint32 := "unsigned"      | type.uint64 := "unsigned long long"  | type.usize  := "size_t"
-| type.int16  := "short"          | type.int32  := "int"           | type.int64  := "long long"
-| type.float  := "float"          | type.double := "double"
-| type.object := "obj*"
-
-def emit_type (ty : type) : extract_m unit :=
-emit (type2cpp ty)
-
-def emit_sep_aux {α} (f : α → extract_m unit) (sep : string) : list α → extract_m unit
-| []      := pure ()
-| [a]     := f a
-| (a::as) := f a *> emit sep *> emit " " *> emit_sep_aux as
-
-def emit_sep {α} (l : list α) (f : α → extract_m unit) (sep := ",") : extract_m unit :=
-emit_sep_aux f sep l
-
-def emit_var_list (xs : list var) : extract_m unit :=
-emit_sep xs emit_var
-
-def emit_template_params (ts : list type) : extract_m unit :=
-emit "<" *> emit_sep ts emit_type *> emit ">"
-
-def emit_template_param (t : type) : extract_m unit :=
-emit_template_params [t]
-
-def emit_arg_list (args : list arg) : extract_m unit :=
-emit_sep args $ λ a, emit_type a.ty *> emit " " *> emit_var a.n
-
-/-- Emit end-of-statement -/
-def emit_eos : extract_m unit :=
-emit ";" *> emit_line
-
-def emit_cases : list blockid → nat → extract_m unit
-| []      n := throw "ill-formed case terminator"
-| [b]     n := emit "default: goto " *> emit_blockid b *> emit_eos
-| (b::bs) n := emit "case " *> emit n *> emit ": goto " *> emit_blockid b *> emit_eos *> emit_cases bs (n+1)
-
-def emit_case : var → list blockid → extract_m unit
-| x [b]     := emit "goto " *> emit_blockid b *> emit_eos
-| x [b₁,b₂] := do
-     env ← read,
-     (match env.ctx.find x with
-      | some type.bool   := emit "if (" *> emit_var x *> emit ") goto " *> emit_blockid b₂ *> emit "; else goto " *> emit_blockid b₁
-      | some type.uint32 := emit "if (" *> emit_var x *> emit " == 0) goto " *> emit_blockid b₁ *> emit "; else goto " *> emit_blockid b₂
-      | _                := throw "ill-formed case"),
-     emit_eos
-| x bs      :=  do
-    env ← read,
-    emit "switch ",
-    paren (emit_var x),
-    emit " {" *> emit_line *> emit_cases bs 0 *> emit "}" *> emit_line
-
-def emit_terminator (term : terminator) : extract_m unit :=
-term.decorate_error $
-match term with
-| (terminator.jmp b)     := emit "goto " *> emit_blockid b *> emit_eos
-| (terminator.ret x)     := emit "return " *> emit_var x *> emit_eos
-| (terminator.case x bs) := emit_case x bs
-
-def emit_type_size (ty : type) : extract_m unit :=
-emit "sizeof" *> paren(emit_type ty)
-
-/-- Emit `op(x)` -/
-def emit_op_x (op : string) (x : var) : extract_m unit :=
-emit op *> paren (emit_var x)
-
-/-- Emit `x := y op z` -/
-def emit_infix (x y z : var) (op : string) : extract_m unit :=
-emit_var x *> emit " = " *> emit_var y *> emit " " *> emit op *> emit " " *> emit_var z
-
-/- Emit `x := big_op(y, z)` -/
-def emit_big_binop (x y z : var) (big_op : string) : extract_m unit :=
-emit_var x *> emit " = " *> emit big_op *> paren (emit_var y <+> emit_var z)
-
-def emit_arith (t : type) (x y z : var) (op : string) (big_op : string) : extract_m unit :=
-match t with
-| type.object := emit_big_binop x y z big_op
-| _           := emit_infix x y z op
-
-def emit_logical_arith (t : type) (x y z : var) (bool_op : string) (op : string) (big_op : string) : extract_m unit :=
-match t with
-| type.bool   := emit_infix x y z bool_op
-| type.object := emit_big_binop x y z big_op
-| _           := emit_infix x y z op
-
-def emit_assign_binop (x : var) (t : type) (op : assign_binop) (y z : var) : extract_m unit :=
-match op with
-| assign_binop.add  := emit_arith t x y z "+" "lean::nat_add"
-| assign_binop.sub  := emit_arith t x y z "-" "lean::nat_sub"
-| assign_binop.mul  := emit_arith t x y z "*" "lean::nat_mul"
-| assign_binop.div  := emit_arith t x y z "/" "lean::nat_div"
-| assign_binop.mod  := emit_arith t x y z "%" "lean::nat_mod"
-| assign_binop.iadd := emit_big_binop x y z "lean::int_add"
-| assign_binop.isub := emit_big_binop x y z "lean::int_sub"
-| assign_binop.imul := emit_big_binop x y z "lean::int_mul"
-| assign_binop.idiv := emit_big_binop x y z "lean::int_div"
-| assign_binop.imod := emit_big_binop x y z "lean::int_mod"
-| assign_binop.shl  := emit_infix x y z "<<"
-| assign_binop.shr  := emit_infix x y z ">>"
-| assign_binop.and  := emit_logical_arith t x y z "&&" "&" "lean::nat_land"
-| assign_binop.or   := emit_logical_arith t x y z "||" "|" "lean::nat_lor"
-| assign_binop.xor  := emit_logical_arith t x y z "!=" "^" "lean::nat_lxor"
-| assign_binop.le   := emit_arith t x y z "<=" "lean::nat_le"
-| assign_binop.lt   := emit_arith t x y z "<"  "lean::nat_lt"
-| assign_binop.eq   := emit_arith t x y z "==" "lean::nat_eq"
-| assign_binop.ne   := emit_arith t x y z "!=" "lean::nat_ne"
-| assign_binop.ile  := emit_big_binop x y z "lean::int_le"
-| assign_binop.ilt  := emit_big_binop x y z "lean::int_lt"
-| assign_binop.ieq  := emit_big_binop x y z "lean::int_eq"
-| assign_binop.ine  := emit_big_binop x y z "lean::int_ne"
-| assign_binop.array_read :=
-  (match t with
-   | type.object := emit_var x *> emit " = lean::array_obj" *> paren (emit_var y <+> emit_var z)
-   | _           := emit_var x *> emit " = lean::sarray_data" *> emit_template_param t *> paren (emit_var y <+> emit_var z))
-| assign_binop.array_push :=
-  do env ← read, emit_var x, emit " = ",
-     if env.ctx.find z = some type.object then emit "lean::array_push" else emit "lean::sarray_push",
-     paren(emit_var y <+> emit_var z)
-| assign_binop.string_push   := emit_var x *> emit " = lean::string_push" *> paren (emit_var y <+> emit_var z)
-| assign_binop.string_append := emit_var x *> emit " = lean::string_append" *> paren (emit_var y <+> emit_var z)
-
-/-- Emit `x := op(y)` -/
-def emit_x_op_y (x : var) (op : string) (y : var) : extract_m unit :=
-emit_var x *> emit " = " *> emit op *> paren(emit_var y)
-
-def assign_unop2cpp (t : type) : assign_unop → string
-| assign_unop.not          := if t = type.bool then "!" else "~"
-| assign_unop.neg          := "-"
-| assign_unop.ineg         := "lean::int_neg"
-| assign_unop.nat2int      := "lean::nat2int"
-| assign_unop.is_scalar    := "lean::is_scalar"
-| assign_unop.is_shared    := "lean::is_shared"
-| assign_unop.is_null      := "lean::is_null"
-| assign_unop.box          := "lean::box"
-| assign_unop.unbox        := "lean::unbox"
-| assign_unop.cast         := "static_cast<" ++ type2cpp t ++ ">"
-| assign_unop.array_copy   := "lean::array_copy"
-| assign_unop.sarray_copy  := "lean::sarray_copy"
-| assign_unop.array_size   := "lean::array_size"
-| assign_unop.sarray_size  := "lean::sarray_size"
-| assign_unop.string_len   := "lean::string_len"
-| assign_unop.succ         := "lean::nat_succ"
-| assign_unop.tag_ref      := "lean::cnstr_tag"
-| assign_unop.tag          := "lean::obj_tag"
-
-def emit_assign_unop (x : var) (t : type) (op : assign_unop) (y : var) : extract_m unit :=
-emit_var x *> emit " = " *> emit (assign_unop2cpp t op) *> paren(emit_var y)
-
-def emit_num_suffix : type → extract_m unit
-| type.uint32 := emit "u"
-| type.uint64 := emit "ull"
-| type.int64  := emit "ll"
-| _           := pure ()
-
-def emit_assign_lit (x : var) (t : type) (l : literal) : extract_m unit :=
-match l with
-| literal.bool tt := emit_var x *> emit " = true"
-| literal.bool ff := emit_var x *> emit " = false"
-| literal.str s   := emit_var x *> emit " = lean::mk_string" *> paren(emit (repr s))
-| literal.float v := emit_var x *> emit " = " *> emit v
-| literal.num v   :=
-  match t with
-  | type.object :=
-    emit_var x *> emit " = " *>
-    if v < uint32_sz then emit "lean::mk_nat_obj" *> paren(emit v *> emit "u")
-    else emit "lean::mk_mpz_core(lean::mpz(\"" *> emit v *> emit "\"))"
-  | _           := emit_var x *> emit " = " *> emit v *> emit_num_suffix t
-
-def unop2cpp : unop → string
-| unop.inc_ref        := "lean::inc_ref"
-| unop.dec_ref        := "lean::dec_ref"
-| unop.dec_sref       := "lean::dec_shared_ref"
-| unop.inc            := "lean::inc"
-| unop.dec            := "lean::dec"
-| unop.free           := "free"
-| unop.dealloc        := "lean::dealloc"
-| unop.array_pop      := "lean::array_pop"
-| unop.sarray_pop     := "lean::sarray_pop"
-
-def emit_unop (op : unop) (x : var) : extract_m unit :=
-emit (unop2cpp op) *> paren(emit_var x)
-
-def emit_apply (x : var) (ys : list var) : extract_m unit :=
-match ys with
-| (f::as) :=
-  let n := as.length in
-  if n > closure_max_args
-  then emit "{ obj * as[" *> emit n *> emit "] = {" *> emit_var_list as *> emit "}; "
-       *> emit_var x *> emit " = apply_m" *> paren(emit_var f <+> emit n <+> emit "as") *> emit "; }"
-  else emit_var x *> emit " = apply_" *> emit n *> paren(emit_var_list ys)
-| _       := throw "ill-formed apply"
-
-def emit_closure (x : var) (f : fnid) (ys : list var) : extract_m unit :=
-do env ← read,
-   match env.cfg.env f with
-   | some d := do
-     emit_var x, emit " = lean::alloc_closure(",
-     let arity := d.header.args.length,
-     fname ← fid2cpp f,
-     let fname := if arity > closure_max_args then "uncurry" ++ fname else fname,
-     emit "reinterpret_cast<lean::lean_cfun>(" *> emit fname *> emit ")" <+> emit arity <+> emit ys.length,
-     emit ")",
-     ys.mfoldl (λ i y, emit ";\nlean::closure_set_arg" *> paren (emit_var x <+> emit i <+> emit_var y) *> pure (i+1)) 0,
-     pure ()
-   | none   := throw "invalid closure"
-
-def emit_instr (ins : instr) : extract_m unit :=
-ins.decorate_error $
-(match ins with
- | (instr.assign x t y)             := emit_var x *> emit " = " *> emit_var y
- | (instr.assign_lit x t l)         := emit_assign_lit x t l
- | (instr.assign_unop x t op y)     := emit_assign_unop x t op y
- | (instr.assign_binop x t op y z)  := emit_assign_binop x t op y z
- | (instr.unop op x)                := emit_unop op x
- | (instr.call x f ys)      := do
-   emit_var x *> emit " = ",
-   c ← is_const f,
-   if c then emit_global f
-   else (emit_fnid f *> paren(emit_var_list ys))
- | (instr.cnstr o t n sz)    := emit_var o *> emit " = lean::alloc_cnstr" *> paren(emit t <+> emit n <+> emit sz)
- | (instr.set o i x)         := emit "lean::cnstr_set_obj" *> paren (emit_var o <+> emit i <+> emit_var x)
- | (instr.get x o i)         := emit_var x *> emit " = lean::cnstr_obj" *> paren(emit_var o <+> emit i)
- | (instr.sset o d x)        := emit "lean::cnstr_set_scalar" *> paren(emit_var o <+> emit d <+> emit_var x)
- | (instr.sget x t o d)      := emit_var x *> emit " = lean::cnstr_scalar" *> emit_template_param t *> paren(emit_var o <+> emit d)
- | (instr.closure x f ys)    := emit_closure x f ys
- | (instr.apply x ys)        := emit_apply x ys
- | (instr.array a sz c)      := emit_var a *> emit " = lean::alloc_array" *> paren(emit_var sz <+> emit_var c)
- | (instr.sarray a t sz c)   := emit_var a *> emit " = lean::alloc_sarray" *> paren(emit_type_size t <+> emit_var sz <+> emit_var c)
- | (instr.array_write a i v) :=
-   do env ← read,
-      if env.ctx.find v = some type.object
-      then emit "lean::array_set_obj" *> paren(emit_var a <+> emit_var i <+> emit_var v)
-      else emit "lean::sarray_set_data" *> paren(emit_var a <+> emit_var i <+> emit_var v))
-*> emit_eos
-
-def emit_block (b : block) : extract_m unit :=
-   unless b.phis.empty (throw "failed to extract C++ code, definition contains phi nodes")
-*> emit_blockid b.id *> emit ":" *> emit_line
-*> b.instrs.mfor emit_instr
-*> emit_terminator b.term
-
-def emit_header (h : header) : extract_m unit :=
-emit_type h.return.ty *> emit " " *> emit_fnid h.name *> paren(emit_arg_list h.args)
-
-def decl_local (x : var) (ty : type) : extract_m unit :=
-emit_type ty *> emit " " *> emit_var x *> emit_eos
-
-def decl_locals (args : list arg) : extract_m unit :=
-do env ← read,
-   env.ctx.mfor $ λ x ty,
-     unless (args.any (λ a, a.n = x)) (decl_local x ty)
-
-def need_uncurry (d : decl) : bool :=
-d.header.args.length > lean.closure_max_args &&
-d.header.return.ty = type.object &&
-d.header.args.all (λ a, a.ty = type.object)
-
-def emit_uncurry_header (d : decl) : extract_m unit :=
-emit "obj* uncurry" *> emit_fnid d.header.name *> emit "(obj** as)"
-
-def emit_uncurry (d : decl) : extract_m unit :=
-let nargs := d.header.args.length in
-   emit_uncurry_header d *> emit " {\n"
-*> emit "return " *> emit_fnid d.header.name *> paren (emit "as[0]" *> (nargs-1).mrepeat (λ i, emit ", " *> emit "as[" *> emit (i+1) *> emit "]")) *> emit_eos
-*> emit "}\n"
-
-def emit_def_core (d : decl) : extract_m unit :=
-d.decorate_error $
-match d with
-| (decl.defn h bs)  :=
-  emit_header h *> emit " {" *> emit_line
-  *> decl_locals h.args *> bs.mfor emit_block
-  *> emit "}" *> emit_line *>
-  when (need_uncurry d) (emit_uncurry d)
-| _ := pure ()
-
-section
-local attribute [reducible] extract_m
-def emit_def (d : decl) : extract_m unit :=
-do env ← read,
-   ctx ← monad_lift $ infer_types d env.cfg.env,
-   adapt_reader (λ env : extract_env, {ctx := ctx, ..env}) $
-     emit_def_core d
-end
-
-def collect_used (d : list decl) : fnid_set :=
-d.foldl (λ s d, match d with
-  | decl.defn _ bs := bs.foldl (λ s b, b.instrs.foldl (λ s ins, match ins with
-    | instr.call _ fid _    := s.insert fid
-    | instr.closure _ fid _ := s.insert fid
-    | _                     := s) s) s
-  | _                := s) mk_fnid_set
-
-def emit_used_headers (ds : list decl) : extract_m unit :=
-let used := collect_used ds in
-do env ← read,
-used.mfor (λ fid, match env.cfg.env fid with
- | some d := do
-   unless (env.cfg.external_names fid = none) (emit "extern \"C\" "),
-   emit_header d.header *> emit ";\n" *> when (need_uncurry d) (emit_uncurry_header d *> emit ";\n")
- | _      := pure ())
-
-def emit_global_var_decls (ds : list decl) : extract_m unit :=
-ds.mfor $ λ d, when d.header.is_const $
-  emit_type d.header.return.ty *> emit " " *> emit_global d.header.name *> emit ";\n"
-
-def emit_initialize_proc (ds : list decl) : extract_m unit :=
-do env ← read,
-   emit "void ", emit initialize_prefix, emit env.cfg.unit_name, emit "() {\n",
-   emit "if (_G_initialized) return;\n",
-   emit "_G_initialized = true;\n",
-   env.cfg.unit_deps.mfor $ λ dep, emit initialize_prefix *> emit dep *> emit "();\n",
-   ds.mfor $ λ d, when d.header.is_const $
-     emit_global d.header.name *> emit " = " *> emit_fnid d.header.name *> emit "();\n",
-   emit "}\n"
-
-def emit_finalize_proc (ds : list decl) : extract_m unit :=
-do env ← read,
-   emit "void ", emit finalize_prefix, emit env.cfg.unit_name, emit "() {\n",
-   emit "if (_G_finalized) return;\n",
-   emit "_G_finalized = true;\n",
-   env.cfg.unit_deps.mfor $ λ dep, emit finalize_prefix *> emit dep *> emit "();\n",
-   ds.mfor $ λ d, when (d.header.is_const && d.header.return.ty = type.object) $
-     emit "if (!is_scalar(" *> emit_global d.header.name *> emit ")) lean::dec_ref(" *> emit_global d.header.name *> emit ");\n",
-   emit "}\n"
-
-def emit_main_proc : extract_m unit :=
-do env ← read,
-   match env.cfg.main_proc with
-   | some fid :=
-     (match env.cfg.env fid with
-      | some d :=
-        unless (d.header.args.length = 0) (throw $ "invalid main function '" ++ to_string fid ++ "', it must not take any arguments")
-        *> unless (d.header.return.ty = type.int32) (throw $ "invalid main function '" ++ to_string fid ++ "', return type must be int32")
-        *> emit "int main() {\n"
-        *> emit initialize_prefix *> emit env.cfg.unit_name *> emit "();\n"
-        *> emit "int r = " *> emit_fnid fid *> emit "();\n"
-        *> emit finalize_prefix *> emit env.cfg.unit_name *> emit "();\n"
-        *> emit "return r;\n}\n"
-      | none := throw ("unknown main function '" ++ to_string fid ++ "'"))
-   | none := pure ()
-
-end cpp
-
-open cpp
-
-def extract_cpp (ds : list decl) (cfg : extract_cpp_config := {}) : except format string :=
-let out := file_header cfg.runtime_dir ++ "\n" in
-run (emit_used_headers ds
-     *> emit "static bool _G_initialized = false;\n"
-     *> emit "static bool _G_finalized = false;\n"
-     *> emit_global_var_decls ds
-     *> emit_initialize_proc ds
-     *> emit_finalize_proc ds
-     *> ds.mfor emit_def
-     *> emit_main_proc
-     *> get)
-{cfg := cfg} out
-
-end ir
-end lean

library/init/lean/ir/format.lean

@@ -1,188 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.lean.format init.lean.parser.identifier
-import init.lean.ir.reserved init.lean.ir.ir
-
-namespace lean
-namespace ir
-open lean.format
-
-def should_escape_aux : nat → bool → string.iterator → bool
-| 0     _ _   := ff
-| (n+1) tt it := !is_id_first it.curr || should_escape_aux n ff it.next
-| (n+1) ff it := !is_id_rest it.curr  || should_escape_aux n ff it.next
-
-def should_escape (s : string) : bool :=
-should_escape_aux s.length tt s.mk_iterator
-
-def escape_string (s : string) : string :=
-to_string id_begin_escape ++ s ++ to_string id_end_escape
-
-def id_part.to_string (s : string) : string :=
-if should_escape s then escape_string s else s
-
-def id.to_string : name → string
-| name.anonymous                     := escape_string ""
-| (name.mk_string name.anonymous s)  := if is_reserved s then escape_string s else id_part.to_string s
-| (name.mk_numeral name.anonymous v) := escape_string (to_string v)
-| (name.mk_string n s)               := id.to_string n ++ "." ++ id_part.to_string s
-| (name.mk_numeral n v)              := id.to_string n ++ "." ++ escape_string (to_string v)
-
-instance var.has_to_format : has_to_format var         := ⟨λ v, id.to_string v⟩
-instance blockid.has_to_format : has_to_format blockid := ⟨λ b, id.to_string b⟩
-instance fnid.has_to_format : has_to_format fnid       := ⟨λ f, id.to_string f⟩
-instance fnid.has_to_string : has_to_string fnid       := ⟨λ f, id.to_string f⟩
-instance tag.has_to_format : has_to_format tag         := infer_instance_as (has_to_format uint16)
-instance tag.has_to_string : has_to_string tag         := infer_instance_as (has_to_string uint16)
-
-def type.to_format : type → format
-| type.bool   := "bool"   | type.byte   := "byte"
-| type.uint16 := "uint16" | type.uint32 := "uint32" | type.uint64 := "uint64" | type.usize := "usize"
-| type.int16  := "int16"  | type.int32  := "int32"   | type.int64  := "int64"
-| type.float  := "float"  | type.double := "double"  | type.object := "object"
-
-instance type.has_to_format : has_to_format type := ⟨type.to_format⟩
-instance type.has_to_string : has_to_string type := ⟨pretty ∘ to_fmt⟩
-
-def assign_unop.to_format : assign_unop → format
-| assign_unop.not           := "not"        | assign_unop.neg          := "neg"       | assign_unop.ineg    := "ineg"
-| assign_unop.nat2int       := "nat2int"
-| assign_unop.is_scalar     := "is_scalar"  | assign_unop.is_shared    := "is_shared" | assign_unop.is_null := "is_null"
-| assign_unop.box           := "box"        | assign_unop.unbox        := "unbox"
-| assign_unop.cast          := "cast"
-| assign_unop.array_copy    := "array_copy" | assign_unop.sarray_copy  := "sarray_copy"
-| assign_unop.array_size    := "array_size" | assign_unop.sarray_size  := "sarray_size"
-| assign_unop.string_len    := "string_len" | assign_unop.succ         := "succ"
-| assign_unop.tag           := "tag"        | assign_unop.tag_ref      := "tag_ref"
-
-instance assign_unop.has_to_format : has_to_format assign_unop := ⟨assign_unop.to_format⟩
-instance assign_unop.has_to_string : has_to_string assign_unop := ⟨pretty ∘ to_fmt⟩
-
-def assign_binop.to_format : assign_binop → format
-| assign_binop.add  := "add"  | assign_binop.sub  := "sub"  | assign_binop.mul  := "mul"   | assign_binop.div   := "div"  | assign_binop.mod  := "mod"
-| assign_binop.iadd := "iadd" | assign_binop.isub := "isub" | assign_binop.imul := "imul"  | assign_binop.idiv  := "idiv" | assign_binop.imod := "imod"
-| assign_binop.shl  := "shl"  | assign_binop.shr  := "shr"
-| assign_binop.and  := "and"  | assign_binop.or   := "or"   | assign_binop.xor  := "xor"
-| assign_binop.le   := "le"   | assign_binop.lt   := "lt"   | assign_binop.eq   := "eq"  | assign_binop.ne   := "ne"
-| assign_binop.ile  := "ile"  | assign_binop.ilt  := "ilt"  | assign_binop.ieq  := "ieq" | assign_binop.ine  := "ine"
-| assign_binop.array_read    := "array_read"
-| assign_binop.array_push    := "array_push"
-| assign_binop.string_push   := "string_push"
-| assign_binop.string_append := "string_append"
-
-instance assign_binop.has_to_format : has_to_format assign_binop := ⟨assign_binop.to_format⟩
-instance assign_binop.has_to_string : has_to_string assign_binop := ⟨pretty ∘ to_fmt⟩
-
-def unop.to_format : unop → format
-| unop.inc_ref   := "inc_ref"   | unop.dec_ref := "dec_ref"  | unop.dec_sref := "dec_sref"
-| unop.inc       := "inc"       | unop.dec     := "dec"
-| unop.free      := "free"      | unop.dealloc := "dealloc"
-| unop.array_pop := "array_pop" | unop.sarray_pop := "sarray_pop"
-
-instance unop.has_to_format : has_to_format unop := ⟨unop.to_format⟩
-instance unop.has_to_string : has_to_string unop := ⟨pretty ∘ to_fmt⟩
-
-def literal.to_format : literal → format
-| (literal.bool b)  := to_fmt b
-| (literal.str s)   := repr s
-| (literal.num n)   := to_fmt n
-| (literal.float n) := to_fmt n
-
-instance literal.has_to_format : has_to_format literal := ⟨literal.to_format⟩
-instance literal.has_to_string : has_to_string literal := ⟨pretty ∘ to_fmt⟩
-
-def sizet_entry.to_format : nat × type → format
-| (1, ty) := to_fmt ty
-| (n, ty) := to_fmt n ++ ":" ++ to_fmt ty
-
-def instr.to_format : instr → format
-| (instr.assign x ty y)             := to_fmt x ++ " : " ++ to_fmt ty ++ " := " ++ to_fmt y
-| (instr.assign_lit x ty lit)       := to_fmt x ++ " : " ++ to_fmt ty ++ " := " ++ to_fmt lit
-| (instr.assign_unop x ty op y)     := to_fmt x ++ " : " ++ to_fmt ty ++ " := " ++ to_fmt op ++ " " ++ to_fmt y
-| (instr.assign_binop x ty op y z)  := to_fmt x ++ " : " ++ to_fmt ty ++ " := " ++ to_fmt op ++ " " ++ to_fmt y ++ " " ++ to_fmt z
-| (instr.unop op x)                 := to_fmt op ++ " " ++ to_fmt x
-| (instr.call x fn ys)              := to_fmt x ++ " := call " ++ to_fmt fn ++ prefix_join " " ys
-| (instr.cnstr o t n sz)            := to_fmt o ++ " := cnstr " ++ to_fmt t ++ " " ++ to_fmt n ++ " " ++ to_fmt sz
-| (instr.set o i x)                 := to_fmt "set " ++ to_fmt o ++ " " ++ to_fmt i ++ " " ++ to_fmt x
-| (instr.get x o i)                 := to_fmt x ++ " := get " ++ to_fmt o ++ " " ++ to_fmt i
-| (instr.sset o d v)                := to_fmt "sset " ++ to_fmt o ++ " " ++ to_fmt d ++ " " ++ to_fmt v
-| (instr.sget x ty o d)             := to_fmt x ++ " : " ++ to_fmt ty ++ " := sget " ++ to_fmt o ++ " " ++ to_fmt d
-| (instr.closure x f ys)            := to_fmt x ++ " := closure " ++ to_fmt f ++ prefix_join " " ys
-| (instr.apply x ys)                := to_fmt x ++ " := apply " ++ join_sep ys " "
-| (instr.array a sz c)              := to_fmt a ++ " := array " ++ to_fmt sz ++ " " ++ to_fmt c
-| (instr.sarray a ty sz c)          := to_fmt a ++ " := sarray " ++ to_fmt ty ++ " " ++ to_fmt sz ++ " " ++ to_fmt c
-| (instr.array_write a i v)         := "array_write " ++ to_fmt a ++ " " ++ to_fmt i ++ " " ++ to_fmt v
-
-instance instr.has_to_format : has_to_format instr := ⟨instr.to_format⟩
-instance instr.has_to_string : has_to_string instr := ⟨pretty ∘ to_fmt⟩
-
-def phi.to_format : phi → format
-| {x := x, ty := ty, ys := ys} := to_fmt x ++ " : " ++ to_fmt ty ++  " := phi " ++ join_sep ys " "
-
-instance phi.has_to_format : has_to_format phi := ⟨phi.to_format⟩
-instance phi.has_to_string : has_to_string phi := ⟨pretty ∘ to_fmt⟩
-
-def terminator.to_format : terminator → format
-| (terminator.ret y)     := "ret " ++ to_fmt y
-| (terminator.case x bs) := "case " ++ to_fmt x ++ " " ++ to_fmt bs
-| (terminator.jmp b)     := "jmp " ++ to_fmt b
-
-instance terminator.has_to_format : has_to_format terminator := ⟨terminator.to_format⟩
-instance terminator.has_to_string : has_to_string terminator := ⟨pretty ∘ to_fmt⟩
-
-def block.to_format : block → format
-| {id := id, phis := ps, instrs := is, term := t} :=
-  to_fmt id ++ ":" ++ nest 2 (line ++ join_suffix ps (";" ++ line) ++ join_suffix is (";" ++ line) ++ to_fmt t ++ ";")
-
-instance block.has_to_format : has_to_format block := ⟨block.to_format⟩
-instance block.has_to_string : has_to_string block := ⟨pretty ∘ to_fmt⟩
-
-def arg.to_format : arg → format
-| {n := n, ty := ty} := "(" ++ to_fmt n ++ " : " ++ to_fmt ty ++ ")"
-
-instance arg.has_to_format : has_to_format arg := ⟨arg.to_format⟩
-instance arg.has_to_string : has_to_string arg := ⟨pretty ∘ to_fmt⟩
-
-def result.to_format : result → format
-| {ty := ty, ..} := to_fmt ty
-
-instance result.has_to_format : has_to_format result := ⟨result.to_format⟩
-instance result.has_to_string : has_to_string result := ⟨pretty ∘ to_fmt⟩
-
-def header.to_format (h : header) : format :=
-to_fmt h.name ++ " " ++ join_sep h.args " " ++ " : " ++ to_fmt h.return
-
-instance header.has_to_format : has_to_format header := ⟨header.to_format⟩
-instance header.has_to_string : has_to_string header := ⟨pretty ∘ to_fmt⟩
-
-def decl.to_format : decl → format
-| (decl.defn h bs)  := "def " ++ to_fmt h ++ " := " ++ line ++ join_sep bs line ++ line
-| (decl.external h) := "external " ++ to_fmt h
-
-instance decl.has_to_format : has_to_format decl := ⟨decl.to_format⟩
-instance decl.has_to_string : has_to_string decl := ⟨pretty ∘ to_fmt⟩
-
-@[inline] def phi.decorate_error {α m} [monad_except format m] (p : phi) (a : m α) : m α :=
-catch a (λ e, throw ("at phi '" ++ to_fmt p ++ "'" ++ line ++ e))
-
-@[inline] def instr.decorate_error {α m} [monad_except format m] (ins : instr) (a : m α) : m α :=
-catch a (λ e, throw ("at instruction '" ++ to_fmt ins ++ "'" ++ line ++ e))
-
-@[inline] def terminator.decorate_error {α m} [monad_except format m] (t : terminator) (a : m α) : m α :=
-catch a (λ e, throw ("at terminator '" ++ to_fmt t ++ "'" ++ line ++ e))
-
-@[inline] def block.decorate_error {α m} [monad_except format m] (b : block) (a : m α) : m α :=
-catch a (λ e, throw ("at block '" ++ to_fmt b.id ++ "'" ++ line ++ e))
-
-@[inline] def header.decorate_error {α m} [monad_except format m] (h : header) (a : m α) : m α :=
-catch a (λ e, throw ("error at declaration '" ++ to_fmt h.name ++ "'" ++ line ++ e))
-
-@[inline] def decl.decorate_error {α m} [monad_except format m] (d : decl) (a : m α) : m α :=
-d.header.decorate_error a
-
-end ir
-end lean

library/init/lean/ir/instances.lean

@@ -1,64 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.lean.ir.ir
-
-namespace lean
-namespace ir
-/- TEMPORARY HACK for defining (decidable_eq type) until we bootstrap new compiler -/
-def type2id : type → nat
-| type.bool   := 0  | type.byte   := 1
-| type.uint16 := 2  | type.uint32 := 3  | type.uint64 := 4 | type.usize := 5
-| type.int16  := 6  | type.int32  := 7  | type.int64  := 8
-| type.float  := 9  | type.double := 10 | type.object := 11
-
-def id2type : nat → type
-| 0 := type.bool   | 1 := type.byte
-| 2 := type.uint16 | 3 := type.uint32  | 4 := type.uint64 | 5 := type.usize
-| 6 := type.int16  | 7 := type.int32   | 8 := type.int64
-| 9 := type.float  | 10 := type.double | _       := type.object
-
-theorem id2type_type2id_eq : ∀ (ty : type), id2type (type2id ty) = ty
-| type.bool   := rfl  | type.byte   := rfl
-| type.uint16 := rfl  | type.uint32 := rfl  | type.uint64 := rfl | type.usize := rfl
-| type.int16  := rfl  | type.int32  := rfl  | type.int64  := rfl
-| type.float  := rfl  | type.double := rfl  | type.object := rfl
-
-instance type_has_dec_eq : decidable_eq type :=
-{dec_eq := λ t₁ t₂,
- if h : type2id t₁ = type2id t₂
- then is_true (id2type_type2id_eq t₁ ▸ id2type_type2id_eq t₂ ▸ h ▸ rfl)
- else is_false (λ h', absurd rfl (@eq.subst _ (λ t, ¬ type2id t = type2id t₂) _ _ h' h))}
-/- END of TEMPORARY HACK for (decidable_eq type) -/
-
-instance : has_coe string fnid :=
-⟨mk_simple_name⟩
-
--- TODO: move collection declarations to another file
-instance var_has_lt : has_lt var := (name.has_lt_quick : has_lt name)
-instance blockid_has_lt : has_lt blockid := (name.has_lt_quick : has_lt name)
-instance fnid_has_lt : has_lt fnid := (name.has_lt_quick : has_lt name)
-
-attribute [derive decidable_eq hashable] var blockid fnid
-
-def var_set        := rbtree var (<)
-def blockid_set    := rbtree blockid (<)
-def context        := rbmap var type (<)
-def var2blockid    := rbmap var blockid (<)
-def fnid2string    := rbmap fnid string (<)
-def fnid_set       := rbtree fnid (<)
-def mk_var_set     : var_set     := mk_rbtree var (<)
-def mk_blockid_set : blockid_set := mk_rbtree blockid (<)
-def mk_var2blockid : var2blockid := mk_rbmap var blockid (<)
-def mk_context     : context     := mk_rbmap var type (<)
-def mk_fnid2string : fnid2string := mk_rbmap fnid string (<)
-def mk_fnid_set    : fnid_set    := mk_rbtree fnid (<)
-
-instance : inhabited result :=
-⟨⟨type.bool⟩⟩
-
-end ir
-end lean

library/init/lean/ir/ir.lean

@@ -1,274 +0,0 @@
-/-
-Copyright (c) 2018 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.rbmap init.data.int init.control.state init.control.except init.control.combinators
-import init.lean.name
-
-/-
-Missing
-- float/double literals are strings since we did not define them in Lean
-- borrowed annotations
--/
-
-namespace lean
-namespace ir
-/-
-The type `object` is a pointer to constructor/composite objects, arrays of objects, scalar arrays (`string` is a scalar array),
-closures, big numbers (implemented using GMP), external objects or a tagged pointer.
-Tagged pointers are used to represent small scalar values in polymorphic code.
-
-The other types `bool/byte/uint16/uint32/uint64/usize/int16/int32/int64/float/double` are the usual unboxed scalar data.
-We box values of type `bool/byte/uint16/uint32/int16/int32/float` are boxed (in 64-bit machines) as tagged pointers.
-`usize/uint64/int64/double` are boxed by creating a composite object with a single field. -/
-inductive type | bool | byte | uint16 | uint32 |
-uint64 | usize | int16 | int32 | int64 | float | double | object
-
-/-- Operators for instructions of the form `x : t := op y`
-
-- `x : t := not y`, if `t = bool`, then it is the logical negation.
-Otherwise, it is bitwise negation if `t` is `uint32/uint64/usize`.
-
-- `x : t := neg y`, arithmetical `-`. `t` is `int16/int32/int64/float/double`.
-
-- `x : object := ineg y`, integer `-`.
-
-- `x : object := nat2int y`, convert a natural (big) number into an integer (big) number.
-
-- `x : bool := is_scalar y`, set `x` to `tt` iff `y : object` is a tagged
-pointer.
-
-- `x : bool := is_shared y`, set `x` to `tt` iff `y : object` `RC(y)` is greater than 1.
-The behavior is unspecified if `y` is a tagged pointer.
-
-- `x : bool := is_null y`, set `x` to `tt` iff `y : object` is null.
-
-- `x : t := cast y` is a scalar type casting operation. `t` and `typeof(y)` must not be
-`object`.
-
-- `x : object := box y` convert `y : t` where `t` is `int32/uint32` into a tagged
-pointer. `y` must fit in 31bits (in 32-bit machines).
-
-- `x : t := unbox y` convert `y : object` back into a scalar value. `t` is `int32/uint32`.
-The behavior is unspecified if `y` is not a tagged pointer.
-
-- `x : object := array_copy y` creates a copy of the array `y : object`.
-The behavior is unspecified if `y` is not an array of objects.
-
-- `x : object := sarray_copy y` creates a copy of the scalar array `y : object`.
-The behavior is unspecified if `y` is not an array of scalar values.
-Remark: `sarray_copy` can be used to copy strings.
-
-- `x : usize := array_size y` stores the size of the array `y : object` into `x`.
-The behavior is unspecified if `y` is not an array of objects.
-
-- `x : usize := sarray_size y` stores the size of the scalar array `y : object` into `x`.
-The behavior is unspecified if `y` is not an array of scalar values.
-
-- `x : usize := string_len y` stores the length of the string `y : object` into `x`.
-The length is the number of unicode scalar values.
-The behavior is unspecified if `y` is not a string.
-
-- `x : object := succ y` natural number successor.
-
-- `x : uint32 := tag_ref y` return the tag of the (constructor) object `y`. `y` must not be
-  a tagged pointer.
-
-- `x : uint32 := tag y` return the tag of the (constructor) object `y` OR tagged pointer.
--/
-inductive assign_unop
-| not | neg | ineg | nat2int | is_scalar | is_shared | is_null | cast | box | unbox
-| array_copy | sarray_copy | array_size | sarray_size | string_len
-| succ | tag | tag_ref
-
-/-- Operators for instructions of the form `x : t := op y z`
-
-- `x : t := add y z`: addition. Remark: `t ≠ bool`.
-When `t = object`, i.e., `t` is big number or tagged pointer, a new big number may be allocated
-if the result does not fit in a tagged pointer.
-
-- `x : t := sub y z`: subtraction. Remark: `t ≠ bool`. See `add` for big number case.
-
-- `x : t := mul y z`: multiplication. Remark: `t ≠ bool`. See `add` for big number case.
-
-- `x : t := div y z`: division. Remark: `t ≠ bool`. See `add` for big number case.
-
-- `x : t := mod y z`: modulo. Remark: `t ≠ bool`, `t ≠ float` and `t ≠ double`. See `add` for big number case.
-
-- `x : object := iadd y z`: (big) integer addition.
-
-- `x : object := isub y z`: (big) integer subtraction.
-
-- `x : object := imul y z`: (big) integer multiplication.
-
-- `x : object := idiv y z`: (big) integer division.
-
-- `x : object := imod y z`: (big) integer modulo.
-
-- `x : t := shl y z`: bit shift left. Remark: `t ≠ bool`, `t ≠ float`, `t ≠ double` and `t ≠ object`.
-
-- `x : t := shr y z`: bit shift right. Remark: `t ≠ bool`, `t ≠ float`, `t ≠ double` and `t ≠ object`.
-If `t` is `int16`, `int32` or `int64`, it is an arithmetical bit shift.
-
-- `x : t := and y z`: if `t = bool`, then it is the logical and. Otherwise, it is the bitwise and.
-Remark: `t ≠ bool`, `t ≠ float`, `t ≠ double` and `t ≠ object`.
-
-- `x : t := or y z`: if `t = bool`, then it is the logical or. Otherwise, it is the bitwise or.
-Remark: `t ≠ bool`, `t ≠ float`, `t ≠ double` and `t ≠ object`.
-
-- `x : t := xor y z`: if `t = bool`, then it is the logical xor. Otherwise, it is the bitwise xor.
-Remark: `t ≠ bool`, `t ≠ float`, `t ≠ double` and `t ≠ object`.
-
-- `x : bool := le y z`: less than or equal to. Remark: `t ≠ bool`.
-If `y` and `z` are `object`, then they must be big numbers.
-
-- `x : bool := lt y z`: less than. Remark: `t ≠ bool`.
-If `y` and `z` are `object`, then they must be big numbers.
-
-- `x : bool := eq y z`: equality test. If `y` and `z` are `object`, then they must be big numbers.
-
-- `x : bool := ne y z`: disequality test. If `y` and `z` are `object`, then they must be big numbers.
-
-- `x : bool := ile y z`: (big) integer less than or equal to. `y` and `z` have type `object`.
-
-- `x : bool := ilt y z`: (big) integer less than. `y` and `z` have type `object`.
-
-- `x : bool := ieq y z`: (big) integer equality. `y` and `z` have type `object`.
-
-- `x : bool := ine y z`: (big) integer disequality. `y` and `z` have type `object`.
-
-- `x : t := array_read a i`: Read position `i` of the array `a`. `a` must be an (array) `object`.
-If `a` is a scalar array, then `t ≠ object`. If `a` is an (non-scalar) array, then `t = object`.
-
-- `r : object := array_push a x`: push element `x` in the end of array `a`. `x` must have type `object`, `RC(x) = 1`, and it must
-be an array. If `x` has a scalar type, then `a` is an array of scalar. Otherwise, it is an array of objects.
-Remark: if `a` has space for the new element, then `r` is set to `a`. Otherwise, a new array object is allocated, set to `r`,
-and `a` is deleted.
-
-- `r : object := string_push s c`: push character `c` in the end of string `s`. `s` must have type `object`, and `RC(s) = 1`.
-be a string.
-Remark: if `s` has space for the new element, then `r` is set to `s`. Otherwise, a new string is allocated, set to `r`,
-and `s` is deleted.
-
-- `r : object : string_append s₁ s₂`: append string `s₂` in the end of string `s₁`. `s₁` must have type `object`, and `RC(s₁) = 1`.
-Remark: if `s₁` has space for all `s₂` characters, then `r` is set to `s₁`. Otherwise, a new string is allocated, set to `r`,
-and `s₁` is deleted.
-
-Remark: in the future we may add instructions for performing updates destructively on big numbers. Example:
-`add_acc x y` would be `x += y`, and require `RC(x) = 1`. -/
-inductive assign_binop
-| add  | sub  | mul  | div  | mod
-| iadd | isub | imul | idiv | imod
-| shl  | shr  | and  | or   | xor
-| le   | lt   | eq   | ne
-| ile  | ilt  | ieq  | ine
-| array_read | array_push | string_push | string_append
-
-/-- Operators for instructions of the form `op x`
-
-- `inc_ref x`: increment `RC(x)`, `x` must have type `object`, and it must not be a tagged pointer.
-
-- `dec_ref x`: decrement `RC(x)`, `x` must have type `object`, and it must not be a tagged pointer.
-If `RC(x)` becomes zero, then `x` is deleted.
-
-- `dec_sref x`: decrement `RC(x)`, `x` must have type `object`, `RC(x) > 1`, and it must not be a tagged pointer.
-That is, `x` must be a shared object.
-
-- `inc x`: increment `RC(x)` IF `x` is not a tagged pointer. `x` must have type `object`.
-
-- `dec x`: decrement `RC(x)` IF `x` is not a tagged pointer.  `x` must have type `object`.
-
-- `free x`: free `x`'s memory. `x` must have type `object`, it must not be a tagged pointer,
-and it must not be an external or big number.
-
-- `dealloc x`: finalize `x` and free `x`'s memory. `x` must have type `object`, and it must not be a tagged pointer.
-
-- `array_pop x`: remove the last element of array `x`. `x` must have type `object`, `RC(x) = 1`, and it must
-be an array of objects.
-
-- `sarray_pop x`: remove the last element of array `x`. `x` must have type `object`, `RC(x) = 1`, and it must
-be an array of scalar values. -/
-inductive unop
-| inc_ref | dec_ref | dec_sref | inc | dec
-| free | dealloc
-| array_pop | sarray_pop
-
-inductive literal
-| bool    : bool   → literal
-| str     : string → literal
-| num     : int    → literal  -- for uint32/uint64/int32/int64/byte/object literals
-| float   : string → literal  -- for float/double literals
-
-def tag     := uint16
-def var     := name
-def fnid    := name
-def blockid := name
-
-/- IR Instructions -/
-inductive instr
-| assign       (x : var) (ty : type) (y : var)                       -- x : ty := y
-| assign_lit   (x : var) (ty : type) (lit : literal)                 -- x : ty := lit
-| assign_unop  (x : var) (ty : type) (op : assign_unop) (y : var)    -- x : ty := op y
-| assign_binop (x : var) (ty : type) (op : assign_binop) (y z : var) -- x : ty := op y z
-| unop         (op : unop) (x : var)                                 -- op x
-| call         (x : var) (f : fnid) (ys : list var)                  -- Function call:  x := f ys
-/- Constructor objects -/
-| cnstr   (o : var) (tag : tag) (nobjs : uint16) (ssz : usize)       -- Create constructor object
-| set     (o : var) (i : uint16) (x : var)                           -- Set object field:          set o i x
-| get     (x : var) (o : var) (i : uint16)                           -- Get object field:          x := get o i
-| sset    (o : var) (d : usize) (v : var)                            -- Set scalar field:          sset o d v
-| sget    (x : var) (ty : type) (o : var) (d : usize)                -- Get scalar field:          x : ty := sget o d
-/- Closures -/
-| closure (x : var) (f : fnid) (ys : list var)                       -- Create closure:            x := closure f ys
-| apply   (x : var) (ys : list var)                                  -- Apply closure:             x := apply ys
-/- Arrays -/
-| array   (a sz c : var)                                             -- Create array of objects with size `sz` and capacity `c`
-| sarray  (a : var) (ty : type) (sz c : var)                         -- Create scalar array
-| array_write (a i v : var)                                          -- (scalar) Array write      write a i v
-
-structure phi :=
-(x : var) (ty : type) (ys : list var)
-
-inductive terminator
-| ret  (y : var)
-| case (x : var) (bs : list blockid)
-| jmp  (b : blockid)
-
-structure block :=
-(id : blockid) (phis : list phi) (instrs : list instr) (term : terminator)
-
-structure arg :=
-(n : var) (ty : type)
-
-structure result :=
-(ty : type)
-
-/--
-Header of function declarations.
-If `is_const` is `tt` than it is a constant declaration.
-The result of this kind of function (when `args = []`) is precomputed
-during compilation unit initialization. -/
-structure header :=
-(name : fnid) (args : list arg) (return : result) (is_const : bool)
-
-inductive decl
-| external (h : header)
-| defn     (h : header) (bs : list block)
-
-def decl.is_definition : decl → bool
-| (decl.defn _ _) := tt
-| _               := ff
-
-def decl.header : decl → header
-| (decl.external h) := h
-| (decl.defn h _)   := h
-
-def decl.name (d : decl) : name :=
-d.header.name
-
-def environment := fnid → option decl
-
-end ir
-end lean

library/init/lean/ir/lirc.lean

@@ -1,57 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.lean.ir.parser init.lean.ir.type_check init.lean.ir.ssa_check
-import init.lean.ir.extract_cpp init.lean.ir.format init.lean.ir.elim_phi
-
-/-
-Frontend for compiling a file containing IR declarations into C++.
-We use it for testing.
--/
-
-namespace lean
-namespace ir
-open lean.parser
-open lean.parser.monad_parsec
-
-def parse_input_aux : nat → list decl → fnid2string → parsec' (list decl × fnid2string)
-| 0     ds m := pure (ds.reverse, m)
-| (n+1) ds m :=
-  (eoi *> pure (ds.reverse, m))
-  <|>
-  (do cid ← (do symbol "[", n ← lexeme $ c_identifier, symbol "]", pure (some n)) <|> pure none,
-      d ← parse_decl,
-      match cid with
-      | some cid := parse_input_aux n (d::ds) (m.insert d.name cid)
-      | none     := parse_input_aux n (d::ds) m)
-
-def parse_input (s : string) : except format (list decl × fnid2string) :=
-match parsec.parse (whitespace *> parse_input_aux s.length [] mk_fnid2string) s with
-| except.ok r    := pure r
-| except.error m := throw m.to_string
-
-def check (env : environment) (ssa : bool) (d : decl) : except format unit :=
-when ssa (d.valid_ssa *> pure ()) *> check_blockids d *> type_check d env *> pure ()
-
-local attribute [instance] name.has_lt_quick
-
-def update_env (ds : list decl) (env : environment) : environment :=
-let m := ds.foldl (λ m d, rbmap.insert m d.name d) (mk_rbmap name decl (<)) in
-λ n, m.find n <|> env n
-
-def update_external_names (m : fnid2string) (external_names : fnid → option string) : fnid → option string :=
-λ n, m.find n <|> external_names n
-
-def lirc (s : string) (cfg : extract_cpp_config := {}) (ssa := ff) : except format string :=
-do (ds, m) ← parse_input s,
-   let env := update_env ds cfg.env,
-   let ext := update_external_names m cfg.external_names,
-   ds.mfor (check env ssa),
-   let ds := if ssa then ds.map elim_phi else ds,
-   extract_cpp ds { env := env, external_names := ext, ..cfg }
-
-end ir
-end lean

library/init/lean/ir/parser.lean

@@ -1,172 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.lean.ir.ir init.lean.parser.parsec
-import init.lean.parser.identifier init.lean.parser.string_literal
-import init.lean.ir.reserved
-
-namespace lean
-namespace ir
-open lean.parser
-open lean.parser.monad_parsec
-
-def symbol (s : string) : parsec' unit :=
-(str s *> whitespace) <?> ("'" ++ s ++ "'")
-
-def keyword (s : string) : parsec' unit :=
-(try $ str s *> not_followed_by_sat is_id_rest *> whitespace) <?> ("'" ++ s ++ "'")
-
-def parse_key2val {α : Type} (msg : string) : list (string × α) → parsec' α
-| []              := error msg
-| ((s, v) :: kvs) := (keyword s *> pure v) <|> parse_key2val kvs
-
-def str2type : list (string × type) :=
-[ ("object", type.object), ("bool", type.bool), ("byte", type.byte),
-  ("uint16", type.uint16), ("uint32", type.uint32), ("uint64", type.uint64), ("usize", type.usize),
-  ("int16", type.int16), ("int32", type.int32), ("int64", type.int64),
-  ("float", type.float), ("double", type.double) ]
-
-def parse_type : parsec' type :=
-parse_key2val "type" str2type
-
-def str2aunop : list (string × assign_unop) :=
-[ ("not", assign_unop.not), ("neg", assign_unop.neg), ("ineg", assign_unop.ineg), ("nat2int", assign_unop.nat2int),
-  ("is_scalar", assign_unop.is_scalar), ("is_shared", assign_unop.is_shared), ("is_null", assign_unop.is_null),
-  ("array_copy", assign_unop.array_copy), ("sarray_copy", assign_unop.sarray_copy), ("box", assign_unop.box),
-  ("unbox", assign_unop.unbox), ("cast", assign_unop.cast), ("array_size", assign_unop.array_size),
-  ("sarray_size", assign_unop.sarray_size), ("string_len", assign_unop.string_len), ("succ", assign_unop.succ),
-  ("tag", assign_unop.tag), ("tag_ref", assign_unop.tag_ref) ]
-
-def parse_assign_unop : parsec' assign_unop :=
-parse_key2val "unary operator" str2aunop
-
-def str2abinop : list (string × assign_binop) :=
-[ ("add", assign_binop.add), ("sub", assign_binop.sub), ("mul", assign_binop.mul), ("div", assign_binop.div), ("mod", assign_binop.mod),
-  ("iadd", assign_binop.iadd), ("isub", assign_binop.isub), ("imul", assign_binop.imul), ("idiv", assign_binop.idiv), ("imod", assign_binop.imod),
-  ("shl", assign_binop.shl), ("shr", assign_binop.shr), ("and", assign_binop.and), ("or", assign_binop.or), ("xor", assign_binop.xor), ("le", assign_binop.le),
-  ("lt", assign_binop.lt), ("eq", assign_binop.eq), ("ne", assign_binop.ne), ("ile", assign_binop.ile), ("ilt", assign_binop.ilt), ("ieq", assign_binop.ieq),
-  ("ine", assign_binop.ine), ("array_read", assign_binop.array_read), ("array_push", assign_binop.array_push), ("string_push", assign_binop.string_push),
-  ("string_append", assign_binop.string_append) ]
-
-def parse_assign_binop : parsec' assign_binop :=
-parse_key2val "binary operator" str2abinop
-
-def str2unop : list (string × unop) :=
-[ ("inc_ref", unop.inc_ref), ("dec_ref", unop.dec_ref), ("inc", unop.inc), ("dec", unop.dec),
-  ("dec_sref", unop.dec_sref), ("free", unop.free), ("dealloc", unop.dealloc), ("array_pop", unop.array_pop),
-  ("sarray_pop", unop.sarray_pop) ]
-
-def parse_unop : parsec' unop :=
-parse_key2val "unary operator" str2unop
-
-def parse_literal : parsec' literal :=
-    (keyword "tt" *> pure (literal.bool tt))
-<|> (keyword "ff" *> pure (literal.bool ff))
-<|> (do n ← lexeme num <?> "numeral", pure (literal.num n))
-<|> (do n ← (ch '-' *> lexeme num), pure (literal.num (- n)))
-<|> literal.str <$> parse_string_literal
-
-def parse_uint16 : parsec' uint16 :=
-try (do it ← left_over,
-        n ← lexeme num,
-        when (n ≥ uint16_sz) $ unexpected_at "big numeral, it does not fit in an uint16" it,
-        pure $ uint16.of_nat n)
-<?> "uint16"
-
-def parse_usize : parsec' usize :=
-try (do it ← left_over,
-        n ← lexeme num,
-        when (n ≥ usize_sz) $ unexpected_at "big numeral, it does not fit in an usize" it,
-        pure $ usize.of_nat n)
-<?> "usize"
-
-def identifier : parsec' name :=
-try (do it ← left_over,
-        n ← lean.parser.identifier,
-        when (is_reserved_name n) $ unexpected_at "keyword" it,
-        pure n)
-<?> "identifier"
-
-def parse_var : parsec' var :=
-lexeme identifier <?> "variable"
-
-def parse_fnid : parsec' fnid :=
-lexeme identifier <?> "function name"
-
-def parse_blockid : parsec' blockid :=
-lexeme identifier <?> "label"
-
-def parse_typed_assignment (x : var) : parsec' instr :=
-do  symbol ":",
-    ty ← parse_type,
-    symbol ":=",
-    (keyword "sget" *> instr.sget x ty <$> parse_var <*> parse_usize)
-<|> (instr.assign x ty <$> parse_var)
-<|> (instr.assign_unop x ty <$> parse_assign_unop <*> parse_var)
-<|> (instr.assign_binop x ty <$> parse_assign_binop <*> parse_var <*> parse_var)
-<|> (instr.assign_lit x ty <$> parse_literal)
-
-def parse_untyped_assignment (x : var) : parsec' instr :=
-do  symbol ":=",
-    (keyword "closure" *> instr.closure x <$> parse_fnid <*> many parse_var)
-<|> (keyword "apply"   *> instr.apply x <$> many1 parse_var)
-<|> (keyword "get"     *> instr.get x <$> parse_var <*> parse_uint16)
-<|> (keyword "call"    *> instr.call x <$> parse_fnid <*> many parse_var)
-<|> (keyword "cnstr"   *> instr.cnstr x <$> parse_uint16 <*> parse_uint16 <*> parse_usize)
-<|> (keyword "array"   *> instr.array x <$> parse_var <*> parse_var)
-<|> (keyword "sarray"  *> instr.sarray x <$> parse_type <*> parse_var <*> parse_var)
-
-def parse_assignment : parsec' instr :=
-do x ← parse_var,
-   (parse_untyped_assignment x <|> parse_typed_assignment x)
-
-def parse_instr : parsec' instr :=
-    (keyword "array_write" *> instr.array_write <$> parse_var <*> parse_var <*> parse_var)
-<|> (keyword "set" *> instr.set <$> parse_var <*> parse_uint16 <*> parse_var)
-<|> (keyword "sset" *> instr.sset <$> parse_var <*> parse_usize <*> parse_var)
-<|> (instr.unop <$> parse_unop <*> parse_var)
-<|> parse_assignment
-
-def parse_phi : parsec' phi :=
-do (x, ty) ← try $ do { x ← parse_var, symbol ":", ty ← parse_type, symbol ":=", keyword "phi", pure (x, ty) },
-   ys ← many1 parse_var,
-   pure {x := x, ty := ty, ys := ys}
-
-def parse_terminator : parsec' terminator :=
-    (keyword "jmp" *> terminator.jmp <$> parse_blockid)
-<|> (keyword "ret" *> terminator.ret <$> parse_var)
-<|> (keyword "case" *> terminator.case <$> parse_var <*> (symbol "[" *> sep_by1 parse_blockid (symbol ",") <* symbol "]"))
-
-def parse_block : parsec' block :=
-do id ← try (parse_blockid <* symbol ":"),
-   ps ← many (parse_phi <* symbol ";"),
-   is ← many (parse_instr <* symbol ";"),
-   t  ← parse_terminator <* symbol ";",
-   pure { id := id, phis := ps, instrs := is, term := t }
-
-def parse_arg : parsec' arg :=
-do symbol "(", x ← parse_var, symbol ":", ty ← parse_type, symbol ")", pure {n := x, ty := ty}
-
-def parse_header (is_const : bool) : parsec' header :=
-do n ← parse_fnid,
-   as ← if is_const then pure [] else many parse_arg,
-   r ← symbol ":" *> result.mk <$> parse_type,
-   pure { name := n, args := as, return := r, is_const := is_const }
-
-def parse_def : parsec' decl :=
-keyword "def" *> decl.defn <$> parse_header ff <*> (symbol ":=" *> many parse_block)
-
-def parse_defconst : parsec' decl :=
-keyword "defconst" *> decl.defn <$> parse_header tt <*> (symbol ":=" *> many parse_block)
-
-def parse_external : parsec' decl :=
-keyword "external" *> decl.external <$> parse_header ff
-
-def parse_decl : parsec' decl :=
-parse_def <|> parse_defconst <|> parse_external
-
-end ir
-end lean

library/init/lean/ir/reserved.lean

@@ -1,42 +0,0 @@
-/-
-Copyright (c) 2018 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.rbtree.basic init.lean.name
-
-namespace lean
-namespace ir
-
-def reserved := [ "bool", "byte", "uint16", "uint32", "uint64", "usize",
- "int16", "int32", "int64", "float", "double", "object",
- "not", "neg", "ineg", "nat2int",
- "is_scalar", "is_shared", "is_null", "unbox", "box", "cast",
- "array_copy", "sarray_copy", "array_size", "sarray_size", "string_len",
- "succ", "tag", "tag_ref",
- "add", "sub", "mul", "div", "mod",
- "iadd", "isub", "imul", "idiv", "imod",
- "shl", "shr", "and",
- "or", "xor",
- "le", "lt", "eq", "ne",
- "ile", "ilt", "ieq", "ine",
- "array_read", "array_push",
- "string_push", "string_append", "inc_ref", "dec_ref", "dec_sref",
- "inc", "dec", "free", "dealloc", "array_pop", "sarray_pop",
- "call", "cnstr", "set", "get", "sset", "sget", "closure", "apply",
- "array", "sarray", "array_write", "phi", "ret", "case", "jmp",
- "def", "external"]
-
-def reserved_set : rbtree string (<) :=
-reserved.foldl rbtree.insert (mk_rbtree string (<))
-
-def is_reserved (s : string) : bool :=
-reserved_set.contains s
-
-def is_reserved_name : name → bool
-| (name.mk_string p s) := is_reserved s
-| _                    := ff
-
-end ir
-end lean

library/init/lean/ir/ssa_check.lean

@@ -1,189 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.lean.ir.instances init.lean.ir.format
-
-namespace lean
-namespace ir
-@[reducible] def ssa_pre_m := except_t format (state_t var2blockid id)
-
-def var.declare (x : var) : reader_t blockid ssa_pre_m unit :=
-do m ← get,
-   if m.contains x then throw ("already defined " ++ to_fmt x)
-   else do b ← read, put (m.insert x b)
-
-def instr.declare_vars : instr → reader_t blockid ssa_pre_m unit
-| (instr.assign x _ _)           := x.declare
-| (instr.assign_lit x _ _)       := x.declare
-| (instr.assign_unop x _ _ _)    := x.declare
-| (instr.assign_binop x _ _ _ _) := x.declare
-| (instr.call x _ _)             := x.declare
-| (instr.cnstr o _ _ _)          := o.declare
-| (instr.get x _ _)              := x.declare
-| (instr.sget x _ _ _)           := x.declare
-| (instr.closure x _ _)          := x.declare
-| (instr.apply x _)              := x.declare
-| (instr.array a _ _)            := a.declare
-| (instr.sarray x _ _ _)         := x.declare
-| _                              := pure ()
-
-def phi.declare  (p : phi) : reader_t blockid ssa_pre_m unit :=
-p.decorate_error p.x.declare
-
-def block.declare_vars (b : block) : ssa_pre_m unit :=
-b.decorate_error $ (b.phis.mfor phi.declare *> b.instrs.mfor instr.declare_vars).run b.id
-
-def arg.declare (a : arg) : reader_t blockid ssa_pre_m unit :=
-a.n.declare
-
-/- Collect where each variable is declared, and
-   check whether each variable was declared at most once. -/
-def decl.declare_vars : decl → ssa_pre_m unit
-| (decl.defn h (b::bs)) :=
-  /- We assume that arguments are declared in the first basic block. -/
-  h.decorate_error $ (h.args.mfor arg.declare).run b.id *> b.declare_vars *> bs.mfor block.declare_vars
-| (decl.defn _  []) := throw "declaration must have at least one basic block"
-| _                 := pure ()
-
-/- Generate the mapping from variable to blockid for the given declaration.
-   This function assumes `d` is in SSA. -/
-def decl.var2blockid (d : decl) : except format var2blockid :=
-run (d.declare_vars *> get) mk_var2blockid
-
-@[reducible] def ssa_valid_m := except_t format (reader_t var2blockid (state_t var_set id))
-
-def ssa_valid_m.run {α} (a : ssa_valid_m α) (m : var2blockid) : except format α :=
-run a m mk_var_set
-
-/- Mark `x` as a variable defined in the current basic block. -/
-def var.define (x : var) : ssa_valid_m unit :=
-modify $ λ s, s.insert x
-
-def arg.define (a : arg) : ssa_valid_m unit :=
-a.n.define
-
-/- Check whether `x` has been already defined in the current basic block or not. -/
-def var.defined (x : var) : ssa_valid_m unit :=
-do s ← get,
-   if s.contains x then pure ()
-   else throw ("undefined '" ++ to_fmt x ++ "'")
-
-/- Given, x := phi ys,
-   check whether every ys is declared at the var2blockid mapping,
-   and update the set of already defined variables in the basic block with `x`. -/
-def phi.valid_ssa (p : phi) : ssa_valid_m unit :=
-p.decorate_error $
-do m ← read,
-   p.ys.mfor $ λ y, unless (m.contains y) $ throw ("undefined '" ++ to_fmt y ++ "'"),
-   p.x.define
-
-def instr.valid_ssa (ins : instr) : ssa_valid_m unit :=
-ins.decorate_error $
-match ins with
-| (instr.assign x _ y)           := x.define *> y.defined
-| (instr.assign_lit x _ _)       := x.define
-| (instr.assign_unop x _ _ y)    := x.define *> y.defined
-| (instr.assign_binop x _ _ y z) := x.define *> y.defined *> z.defined
-| (instr.unop _ x)               := x.defined
-| (instr.call x _ ys)            := x.define *> ys.mfor var.defined
-| (instr.cnstr o _ _ _)          := o.define
-| (instr.set o _ x)              := o.defined *> x.defined
-| (instr.get x y _)              := x.define *> y.defined
-| (instr.sset o _ x)             := o.defined *> x.defined
-| (instr.sget x _ y _)           := x.define *> y.defined
-| (instr.closure x _ ys)         := x.define *> ys.mfor var.defined
-| (instr.apply x ys)             := x.define *> ys.mfor var.defined
-| (instr.array a sz c)           := a.define *> sz.defined *> c.defined
-| (instr.sarray x _ sz c)        := x.define *> sz.defined *> c.defined
-| (instr.array_write a i v)      := a.defined *> i.defined *> v.defined
-
-def terminator.valid_ssa (term : terminator) : ssa_valid_m unit :=
-term.decorate_error $
-match term with
-| (terminator.ret y)      := y.defined
-| (terminator.case x _)   := x.defined
-| (terminator.jmp _)      := pure ()
-
-def phi.predecessors (p : phi) : ssa_valid_m blockid_set :=
-p.ys.mfoldl (λ s y,
-  do m ← read,
-     match m.find y with
-     | some bid := if s.contains bid
-                   then throw ("multiple predecessors at '" ++ to_fmt p ++ "'")
-                   else pure $ s.insert bid
-     | none   := throw ("undefined '" ++ to_fmt y ++ "' at '" ++ to_fmt p ++ "'"))
-  mk_blockid_set
-
-def phis.check_predecessors (ps : list phi) : ssa_valid_m unit :=
-do ps.mfoldl (λ (os : option blockid_set) (p : phi),
-     p.decorate_error $
-     do s' ← p.predecessors,
-        match os with
-        | (some s) := if s.seteq s' then pure os
-                      else throw ("missing predecessor '" ++ to_fmt p.x ++ "' at '" ++ to_fmt p ++ "'")
-        | none      := pure (some s'))
-     none,
-   pure ()
-
-def block.valid_ssa_core (b : block) : ssa_valid_m unit :=
-b.decorate_error $
-do phis.check_predecessors b.phis,
-   b.phis.mfor phi.valid_ssa,
-   b.instrs.mfor instr.valid_ssa,
-   b.term.valid_ssa
-
-/-
-We first check whether every variable `x` was declared only once
-and store the blockid where `x` is defined (action: `decl.declare_vars`).
-Then, we check whether every used variable in basic block has been
-defined before being used.
--/
-def decl.valid_ssa (d : decl) : except format var2blockid :=
-d.decorate_error $
-do m ← d.var2blockid,
-   match d with
-   | decl.defn {args:=args, ..} (b::bs) :=
-       (args.mfor arg.define *> block.valid_ssa_core b).run m
-    *> (bs.mfor block.valid_ssa_core).run m
-    *> pure m
-   | _                   := pure m
-
-/- Check blockids -/
-@[reducible] def blockid_check_m :=
-except_t format (state blockid_set)
-
-def blockid_check_m.run {α} (a : blockid_check_m α) : except format α :=
-run a mk_blockid_set
-
-def block.declare (b : block) : blockid_check_m unit :=
-do s ← get,
-   if s.contains b.id then throw $ "block label '" ++ to_fmt b.id ++ "' has been used more than once"
-   else put (s.insert b.id)
-
-def blockid.defined (bid : blockid) : blockid_check_m unit :=
-do s ← get,
-   if s.contains bid then pure ()
-   else throw $ "unknown basic block '" ++ to_fmt bid ++ "'"
-
-def terminator.check_blockids (term : terminator) : blockid_check_m unit :=
-term.decorate_error $
-match term with
-| (terminator.ret ys)      := pure ()
-| (terminator.case _ bids) := bids.mfor blockid.defined
-| (terminator.jmp bid)     := bid.defined
-
-def block.check_blockids (b : block) : blockid_check_m unit :=
-b.term.check_blockids
-
-def decl.check_blockids : decl → blockid_check_m unit
-| (decl.defn h bs) := h.decorate_error $ bs.mfor block.declare *> bs.mfor block.check_blockids
-| _                := pure ()
-
-def check_blockids (d : decl) : except format blockid_set :=
-(d.check_blockids *> get).run
-
-end ir
-end lean

library/init/lean/ir/type_check.lean

@@ -1,237 +0,0 @@
-/-
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.lean.ir.instances init.lean.ir.format init.control.combinators
-
-namespace lean
-namespace ir
-/-- Return `tt` iff `ty` is a type that may occur in signed arithmetical operations. -/
-def is_signed_arith_ty (ty : type) : bool :=
-match ty with
-| type.int16  := tt | type.int32 := tt  | type.int64 := tt
-| type.float  := tt | type.double := tt
-| _ := ff
-
-/-- Return `tt` iff `ty` is a type that may occur in arithmetical operations. -/
-def is_arith_ty (ty : type) : bool :=
-ty ≠ type.bool -- Recall that type.object may be encoding a big num.
-
-/-- Return `tt` iff `ty` is a type that may occur in non floating point arithmetical operations. -/
-def is_nonfloat_arith_ty (ty : type) : bool :=
-is_arith_ty ty && ty ≠ type.float && ty ≠ type.double
-
-/-- Return `tt` iff `ty` is a type that may occur in bitwise/logical operations. -/
-def is_bitwise_ty (ty : type) : bool :=
-match ty with
-| type.bool   := tt | type.byte := tt
-| type.uint16 := tt | type.uint32 := tt | type.uint64 := tt | type.usize := tt
-| type.object := tt
-| _ := ff
-
-/-- Return `tt` iff `ty` is a type that may occur in bitshift operations. -/
-def is_bitshift_ty (ty : type) : bool :=
-match ty with
-| type.byte   := tt
-| type.int16  := tt | type.int32 := tt  | type.int64  := tt
-| type.uint16 := tt | type.uint32 := tt | type.uint64 := tt | type.usize := tt
-| _ := ff
-
-/-- Return `tt` iff the instruction `x : r := op y` is type correct where `y : t` -/
-def valid_assign_unop_types (op : assign_unop) (r : type) (t : type) : bool :=
-match op with
-| assign_unop.not           := t = r && is_bitwise_ty t
-| assign_unop.neg           := t = r && is_signed_arith_ty t
-| assign_unop.ineg          := t = r && t = type.object
-| assign_unop.nat2int       := t = r && t = type.object
-| assign_unop.is_scalar     := t = type.object && r = type.bool
-| assign_unop.is_shared     := t = type.object && r = type.bool
-| assign_unop.is_null       := t = type.object && r = type.bool
-| assign_unop.array_copy    := t = type.object && r = type.object
-| assign_unop.sarray_copy   := t = type.object && r = type.object
-| assign_unop.unbox         := t = type.object && (r = type.uint32 || r = type.int32)
-| assign_unop.box           := r = type.object && (t = type.uint32 || t = type.int32)
-| assign_unop.cast          := r ≠ type.object && r ≠ type.object
-| assign_unop.array_size    := r = type.usize && t = type.object
-| assign_unop.sarray_size   := r = type.usize && t = type.object
-| assign_unop.string_len    := r = type.usize && t = type.object
-| assign_unop.succ          := r = type.object && t = type.object
-| assign_unop.tag           := r = type.uint32 && t = type.object
-| assign_unop.tag_ref       := r = type.uint32 && t = type.object
-
-/-- Return `tt` iff the instruction `x : r := op y z` is type correct where `y z : t` -/
-def valid_assign_binop_types (op : assign_binop) (r : type) (t₁ t₂ : type) : bool :=
-match op with
-| assign_binop.add  := r = t₁ && r = t₂ && is_arith_ty r
-| assign_binop.sub  := r = t₁ && r = t₂ && is_arith_ty r
-| assign_binop.mul  := r = t₁ && r = t₂ && is_arith_ty r
-| assign_binop.div  := r = t₁ && r = t₂ && is_arith_ty r
-| assign_binop.mod  := r = t₁ && r = t₂ && is_nonfloat_arith_ty r
-| assign_binop.iadd := r = t₁ && r = t₂ && r = type.object
-| assign_binop.isub := r = t₁ && r = t₂ && r = type.object
-| assign_binop.imul := r = t₁ && r = t₂ && r = type.object
-| assign_binop.idiv := r = t₁ && r = t₂ && r = type.object
-| assign_binop.imod := r = t₁ && r = t₂ && r = type.object
-| assign_binop.shl  := r = t₁ && r = t₂ && is_bitshift_ty r
-| assign_binop.shr  := r = t₁ && r = t₂ && is_bitshift_ty r
-| assign_binop.and  := r = t₁ && r = t₂ && is_bitwise_ty r
-| assign_binop.or   := r = t₁ && r = t₂ && is_bitwise_ty r
-| assign_binop.xor  := r = t₁ && r = t₂ && is_bitwise_ty r
-| assign_binop.le   := r = type.bool && t₁ = t₂ && is_arith_ty t₁
-| assign_binop.lt   := r = type.bool && t₁ = t₂ && is_arith_ty t₁
-| assign_binop.eq   := r = type.bool && t₁ = t₂
-| assign_binop.ne   := r = type.bool && t₁ = t₂
-| assign_binop.ile  := r = type.bool && t₁ = t₂ && t₁ = type.object
-| assign_binop.ilt  := r = type.bool && t₁ = t₂ && t₁ = type.object
-| assign_binop.ieq  := r = type.bool && t₁ = t₂ && t₁ = type.object
-| assign_binop.ine  := r = type.bool && t₁ = t₂ && t₁ = type.object
-| assign_binop.array_read    := t₁ = type.object && t₂ = type.usize
-| assign_binop.array_push    := r = type.object && t₁ = type.object
-| assign_binop.string_push   := r = type.object && t₁ = type.object && t₂ = type.uint32
-| assign_binop.string_append := r = type.object && t₁ = type.object && t₂ = type.object
-
-@[reducible] def type_checker_m := except_t format (reader_t (environment × result) (state_t context id))
-
-def type_checker_m.run {α} (a : type_checker_m α) (env : environment) (r : result) : except format α :=
-run a (env, r) mk_context
-
-def match_type (x : var) (t expected : type) : type_checker_m unit :=
-unless (t = expected) $
-  throw ("type mismatch, variable `" ++ to_fmt x ++ "` has type `" ++ to_fmt t ++ "`" ++
-         ", but is expected to have type `" ++ to_fmt expected ++ "`")
-
-def get_type (x : var) : type_checker_m type :=
-do m ← get,
-   match m.find x with
-   | some t := pure t
-   | none   := throw ("undefined variable `" ++ to_fmt x ++ "`")
-
-def set_type (x : var) (t : type) : type_checker_m unit :=
-do m ← get,
-   match m.find x with
-   | some t' := match_type x t' t
-   | none    := put (m.insert x t)
-
-def check_type (x : var) (t : type) : type_checker_m unit :=
-do m ← get,
-   match m.find x with
-   | some t' := match_type x t' t
-   | none    := throw ("type for variable `" ++ to_fmt x ++ "` is not available")
-
-def check_ne_type (x : var) (t : type) : type_checker_m unit :=
-do m ← get,
-   match m.find x with
-   | some t' := unless (t' ≠ t) $ throw ("variable `" ++ to_fmt x ++ "` must not have type `" ++ to_fmt t ++ "`")
-   | none    := throw ("type for variable `" ++ to_fmt x ++ "` is not available")
-
-def invalid_literal : type_checker_m unit :=
-throw "invalid literal"
-
-def literal.check (l : literal) (t : type) : type_checker_m unit :=
-match l with
-| literal.bool _  := unless (t = type.bool) invalid_literal
-| literal.str  _  := unless (t = type.object) invalid_literal
-| literal.num  v  := unless (is_nonfloat_arith_ty t) invalid_literal *>
-                     when (v < 0) (unless (is_signed_arith_ty t) invalid_literal)
-| literal.float _ := unless (t = type.float || t = type.double) invalid_literal
-
-def get_decl (f : fnid) : type_checker_m decl :=
-do (env, _) ← read,
-   match env f with
-   | some d := pure d
-   | none   := throw ("unknown function `" ++ to_fmt f ++ "`")
-
-def set_result_types : var → result → type_checker_m unit
-| x ⟨t⟩ := set_type x t
-
-def instr.infer_types (ins : instr) : type_checker_m unit :=
-ins.decorate_error $
-match ins with
-| (instr.assign x t y)            := set_type x t
-| (instr.assign_lit x t l)        := set_type x t
-| (instr.assign_unop x t op y)    := set_type x t
-| (instr.assign_binop x t op y z) := set_type x t
-| (instr.call x f ys)      := do d ← get_decl f, set_result_types x d.header.return
-| (instr.cnstr o _ _ _)    := set_type o type.object
-| (instr.get x o _)        := set_type x type.object
-| (instr.sget x t o _)     := set_type x t
-| (instr.closure x f ys)   := set_type x type.object
-| (instr.apply x ys)       := set_type x type.object
-| (instr.array a sz c)     := set_type a type.object
-| (instr.sarray a t sz c)  := set_type a type.object
-| other                    := pure ()
-
-def phi.infer_types (p : phi) : type_checker_m unit :=
-p.decorate_error $ set_type p.x p.ty
-
-def arg.infer_types (a : arg) : type_checker_m unit :=
-set_type a.n a.ty
-
-def block.infer_types (b : block) : type_checker_m unit :=
-b.decorate_error $ b.phis.mfor phi.infer_types *> b.instrs.mfor instr.infer_types
-
-def decl.infer_types : decl → type_checker_m context
-| (decl.defn h bs) := h.decorate_error $ h.args.mfor arg.infer_types *> bs.mfor block.infer_types *> get
-| _                := get
-
-/-- Return context with the type of variables used in the given declaration.
-    It does not check whether instructions are being used correctly. -/
-def infer_types (d : decl) (env : environment) : except format context :=
-d.infer_types.run env d.header.return
-
-def check_arg_types : list var → list arg → type_checker_m unit
-| []      []      := pure ()
-| (x::xs) (t::ts) := check_type x t.ty *> check_arg_types xs ts
-| _       _       := throw "unexpected number of arguments"
-
-/-- Check whether the given instruction is type correct or not. It assumes the context already contains
-    the type of all variables. -/
-def instr.check (ins : instr) : type_checker_m unit :=
-ins.decorate_error $
-match ins with
-| (instr.assign x t y)             := do t₁ ← get_type y, unless (t = t₁) (throw "invalid assignment")
-| (instr.assign_lit x t l)         := l.check t
-| (instr.assign_unop x t op y)     := do t₁ ← get_type y, unless (valid_assign_unop_types op t t₁) $ throw "invalid unary operation"
-| (instr.assign_binop x t op y z)  := do t₁ ← get_type y, t₂ ← get_type z, unless (valid_assign_binop_types op t t₁ t₂) $ throw "invalid binary operation"
-| (instr.unop _ x)          := check_type x type.object
-| (instr.call xs f ys)      := do d ← get_decl f, check_arg_types ys d.header.args
-| (instr.cnstr o _ _ _)     := pure ()
-| (instr.set o _ x)         := check_type o type.object *> check_type x type.object
-| (instr.get x o _)         := check_type o type.object
-| (instr.sset o _ x)        := check_type o type.object *> check_ne_type x type.object
-| (instr.sget x t o _)      := check_type o type.object *> check_ne_type x type.object
-| (instr.closure x f ys)    := do ys.mfor (flip check_type type.object), d ← get_decl f,
-                                 unless (d.header.args.length ≥ ys.length) $ throw "too many arguments",
-                                 d.header.args.mfor (λ a, unless (a.ty = type.object) $ throw "invalid closure, arguments must have type object")
-| (instr.apply x ys)        := ys.mfor (flip check_type type.object)
-| (instr.array a sz c)      := check_type sz type.usize *> check_type c type.usize
-| (instr.sarray a t sz c)   := check_type sz type.usize *> check_type c type.usize *> unless (t ≠ type.object) (throw "invalid scalar array")
-| (instr.array_write a i _) := check_type a type.object *> check_type i type.usize
-
-def phi.check (p : phi) : type_checker_m unit :=
-p.decorate_error $ p.ys.mfor (flip check_type p.ty)
-
-def check_result_type : var → result → type_checker_m unit
-| x ⟨t⟩ := check_type x t
-
-def terminator.check (term : terminator) : type_checker_m unit :=
-term.decorate_error $
-match term with
-| (terminator.ret y)    := do (_, r) ← read, check_result_type y r
-| (terminator.case x _) := do t ← get_type x, unless (t = type.bool || t = type.uint32) $ throw "variable must be an uint32 or bool"
-| (terminator.jmp _)    := pure ()
-
-def block.check (b : block) : type_checker_m unit :=
-b.decorate_error $ b.phis.mfor phi.check *> b.instrs.mfor instr.check *> b.term.check
-
-def decl.check : decl → type_checker_m unit
-| (decl.defn h bs) := bs.mfor block.check
-| _                := pure ()
-
-def type_check (d : decl) (env : environment := λ _, none) : except format context :=
-(d.infer_types *> d.check *> get).run env d.header.return
-
-end ir
-end lean

src/boot/CMakeLists.txt

@@ -1 +1 @@
-add_library (boot OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/coroutine.cpp ./init/control/default.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monad_fail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/basic.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/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/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/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/to_string.cpp ./init/data/uint.cpp ./init/data/usize.cpp ./init/default.cpp ./init/env_ext.cpp ./init/function.cpp ./init/io.cpp ./init/lean/compiler/const_folding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/ir.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/ir/elim_phi.cpp ./init/lean/ir/extract_cpp.cpp ./init/lean/ir/format.cpp ./init/lean/ir/instances.cpp ./init/lean/ir/ir.cpp ./init/lean/ir/lirc.cpp ./init/lean/ir/parser.cpp ./init/lean/ir/reserved.cpp ./init/lean/ir/ssa_check.cpp ./init/lean/ir/type_check.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/string_literal.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
+add_library (boot OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/coroutine.cpp ./init/control/default.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monad_fail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/default.cpp ./init/data/basic.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/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/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/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/to_string.cpp ./init/data/uint.cpp ./init/data/usize.cpp ./init/default.cpp ./init/env_ext.cpp ./init/function.cpp ./init/io.cpp ./init/lean/compiler/const_folding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/ir.cpp ./init/lean/compiler/util.cpp ./init/lean/config.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator.cpp ./init/lean/expander.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/frontend.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/basic.cpp ./init/lean/parser/combinators.cpp ./init/lean/parser/command.cpp ./init/lean/parser/declaration.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/module.cpp ./init/lean/parser/notation.cpp ./init/lean/parser/parsec.cpp ./init/lean/parser/pratt.cpp ./init/lean/parser/rec.cpp ./init/lean/parser/string_literal.cpp ./init/lean/parser/syntax.cpp ./init/lean/parser/term.cpp ./init/lean/parser/token.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)

src/boot/init/lean/ir/instances.cpp

@@ -1,610 +0,0 @@
-// Lean compiler output
-// Module: init.lean.ir.instances
-// Imports: init.lean.ir.ir
-#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_lean_ir_blockid_decidable__eq;
-obj* l_lean_ir_mk__var__set;
-obj* l_lean_ir_var_hashable;
-obj* l_lean_ir_blockid_hashable;
-extern obj* l_lean_name_decidable__eq;
-obj* l_lean_ir_fnid__set;
-uint8 l_lean_ir_id2type(obj*);
-uint8 l_lean_ir_type__has__dec__eq(uint8, uint8);
-obj* l_lean_ir_fnid2string;
-obj* l_lean_ir_type2id___main(uint8);
-obj* l_lean_ir_type2id___main___boxed(obj*);
-obj* l_lean_ir_mk__fnid__set;
-obj* l_lean_ir_blockid__set;
-obj* l_lean_ir_mk__fnid2string;
-extern obj* l_lean_name_hashable;
-namespace lean {
-uint8 nat_dec_eq(obj*, obj*);
-}
-obj* l_lean_ir_type2id___boxed(obj*);
-obj* l_lean_ir_mk__var2blockid;
-obj* l_lean_ir_inhabited___boxed;
-obj* l_lean_ir_var__has__lt;
-obj* l_lean_ir_context;
-obj* l_lean_mk__simple__name(obj*);
-obj* l_lean_ir_mk__blockid__set;
-obj* l_lean_ir_fnid_decidable__eq;
-obj* l_lean_ir_id2type___main___boxed(obj*);
-obj* l_lean_ir_var__set;
-obj* l_lean_ir_fnid_hashable;
-obj* l_lean_ir_has__coe;
-uint8 l_lean_ir_inhabited;
-obj* l_lean_ir_mk__context;
-uint8 l_lean_ir_id2type___main(obj*);
-obj* l_lean_ir_var_decidable__eq;
-obj* l_lean_ir_var2blockid;
-obj* l_lean_ir_fnid__has__lt;
-obj* l_lean_ir_id2type___boxed(obj*);
-obj* l_lean_ir_type__has__dec__eq___boxed(obj*, obj*);
-obj* l_lean_ir_blockid__has__lt;
-obj* l_lean_ir_type2id(uint8);
-obj* l_lean_ir_type2id___main(uint8 x_0) {
-_start:
-{
-switch (x_0) {
-case 0:
-{
-obj* x_1; 
-x_1 = lean::mk_nat_obj(0u);
-return x_1;
-}
-case 1:
-{
-obj* x_2; 
-x_2 = lean::mk_nat_obj(1u);
-return x_2;
-}
-case 2:
-{
-obj* x_3; 
-x_3 = lean::mk_nat_obj(2u);
-return x_3;
-}
-case 3:
-{
-obj* x_4; 
-x_4 = lean::mk_nat_obj(3u);
-return x_4;
-}
-case 4:
-{
-obj* x_5; 
-x_5 = lean::mk_nat_obj(4u);
-return x_5;
-}
-case 5:
-{
-obj* x_6; 
-x_6 = lean::mk_nat_obj(5u);
-return x_6;
-}
-case 6:
-{
-obj* x_7; 
-x_7 = lean::mk_nat_obj(6u);
-return x_7;
-}
-case 7:
-{
-obj* x_8; 
-x_8 = lean::mk_nat_obj(7u);
-return x_8;
-}
-case 8:
-{
-obj* x_9; 
-x_9 = lean::mk_nat_obj(8u);
-return x_9;
-}
-case 9:
-{
-obj* x_10; 
-x_10 = lean::mk_nat_obj(9u);
-return x_10;
-}
-case 10:
-{
-obj* x_11; 
-x_11 = lean::mk_nat_obj(10u);
-return x_11;
-}
-default:
-{
-obj* x_12; 
-x_12 = lean::mk_nat_obj(11u);
-return x_12;
-}
-}
-}
-}
-obj* l_lean_ir_type2id___main___boxed(obj* x_0) {
-_start:
-{
-uint8 x_1; obj* x_2; 
-x_1 = lean::unbox(x_0);
-x_2 = l_lean_ir_type2id___main(x_1);
-return x_2;
-}
-}
-obj* l_lean_ir_type2id(uint8 x_0) {
-_start:
-{
-obj* x_1; 
-x_1 = l_lean_ir_type2id___main(x_0);
-return x_1;
-}
-}
-obj* l_lean_ir_type2id___boxed(obj* x_0) {
-_start:
-{
-uint8 x_1; obj* x_2; 
-x_1 = lean::unbox(x_0);
-x_2 = l_lean_ir_type2id(x_1);
-return x_2;
-}
-}
-uint8 l_lean_ir_id2type___main(obj* x_0) {
-_start:
-{
-obj* x_1; uint8 x_2; 
-x_1 = lean::mk_nat_obj(0u);
-x_2 = lean::nat_dec_eq(x_0, x_1);
-if (x_2 == 0)
-{
-obj* x_3; uint8 x_4; 
-x_3 = lean::mk_nat_obj(1u);
-x_4 = lean::nat_dec_eq(x_0, x_3);
-if (x_4 == 0)
-{
-obj* x_5; uint8 x_6; 
-x_5 = lean::mk_nat_obj(2u);
-x_6 = lean::nat_dec_eq(x_0, x_5);
-if (x_6 == 0)
-{
-obj* x_7; uint8 x_8; 
-x_7 = lean::mk_nat_obj(3u);
-x_8 = lean::nat_dec_eq(x_0, x_7);
-if (x_8 == 0)
-{
-obj* x_9; uint8 x_10; 
-x_9 = lean::mk_nat_obj(4u);
-x_10 = lean::nat_dec_eq(x_0, x_9);
-if (x_10 == 0)
-{
-obj* x_11; uint8 x_12; 
-x_11 = lean::mk_nat_obj(5u);
-x_12 = lean::nat_dec_eq(x_0, x_11);
-if (x_12 == 0)
-{
-obj* x_13; uint8 x_14; 
-x_13 = lean::mk_nat_obj(6u);
-x_14 = lean::nat_dec_eq(x_0, x_13);
-if (x_14 == 0)
-{
-obj* x_15; uint8 x_16; 
-x_15 = lean::mk_nat_obj(7u);
-x_16 = lean::nat_dec_eq(x_0, x_15);
-if (x_16 == 0)
-{
-obj* x_17; uint8 x_18; 
-x_17 = lean::mk_nat_obj(8u);
-x_18 = lean::nat_dec_eq(x_0, x_17);
-if (x_18 == 0)
-{
-obj* x_19; uint8 x_20; 
-x_19 = lean::mk_nat_obj(9u);
-x_20 = lean::nat_dec_eq(x_0, x_19);
-if (x_20 == 0)
-{
-obj* x_21; uint8 x_22; 
-x_21 = lean::mk_nat_obj(10u);
-x_22 = lean::nat_dec_eq(x_0, x_21);
-if (x_22 == 0)
-{
-uint8 x_23; 
-x_23 = 11;
-return x_23;
-}
-else
-{
-uint8 x_24; 
-x_24 = 10;
-return x_24;
-}
-}
-else
-{
-uint8 x_25; 
-x_25 = 9;
-return x_25;
-}
-}
-else
-{
-uint8 x_26; 
-x_26 = 8;
-return x_26;
-}
-}
-else
-{
-uint8 x_27; 
-x_27 = 7;
-return x_27;
-}
-}
-else
-{
-uint8 x_28; 
-x_28 = 6;
-return x_28;
-}
-}
-else
-{
-uint8 x_29; 
-x_29 = 5;
-return x_29;
-}
-}
-else
-{
-uint8 x_30; 
-x_30 = 4;
-return x_30;
-}
-}
-else
-{
-uint8 x_31; 
-x_31 = 3;
-return x_31;
-}
-}
-else
-{
-uint8 x_32; 
-x_32 = 2;
-return x_32;
-}
-}
-else
-{
-uint8 x_33; 
-x_33 = 1;
-return x_33;
-}
-}
-else
-{
-uint8 x_34; 
-x_34 = 0;
-return x_34;
-}
-}
-}
-obj* l_lean_ir_id2type___main___boxed(obj* x_0) {
-_start:
-{
-uint8 x_1; obj* x_2; 
-x_1 = l_lean_ir_id2type___main(x_0);
-x_2 = lean::box(x_1);
-lean::dec(x_0);
-return x_2;
-}
-}
-uint8 l_lean_ir_id2type(obj* x_0) {
-_start:
-{
-uint8 x_1; 
-x_1 = l_lean_ir_id2type___main(x_0);
-return x_1;
-}
-}
-obj* l_lean_ir_id2type___boxed(obj* x_0) {
-_start:
-{
-uint8 x_1; obj* x_2; 
-x_1 = l_lean_ir_id2type(x_0);
-x_2 = lean::box(x_1);
-lean::dec(x_0);
-return x_2;
-}
-}
-uint8 l_lean_ir_type__has__dec__eq(uint8 x_0, uint8 x_1) {
-_start:
-{
-obj* x_2; obj* x_3; uint8 x_4; 
-x_2 = l_lean_ir_type2id___main(x_0);
-x_3 = l_lean_ir_type2id___main(x_1);
-x_4 = lean::nat_dec_eq(x_2, x_3);
-lean::dec(x_3);
-lean::dec(x_2);
-if (x_4 == 0)
-{
-uint8 x_7; 
-x_7 = 0;
-return x_7;
-}
-else
-{
-uint8 x_8; 
-x_8 = 1;
-return x_8;
-}
-}
-}
-obj* l_lean_ir_type__has__dec__eq___boxed(obj* x_0, obj* x_1) {
-_start:
-{
-uint8 x_2; uint8 x_3; uint8 x_4; obj* x_5; 
-x_2 = lean::unbox(x_0);
-x_3 = lean::unbox(x_1);
-x_4 = l_lean_ir_type__has__dec__eq(x_2, x_3);
-x_5 = lean::box(x_4);
-return x_5;
-}
-}
-obj* _init_l_lean_ir_has__coe() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_mk__simple__name), 1, 0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_var__has__lt() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_blockid__has__lt() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_fnid__has__lt() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_var_decidable__eq() {
-_start:
-{
-obj* x_0; 
-x_0 = l_lean_name_decidable__eq;
-return x_0;
-}
-}
-obj* _init_l_lean_ir_var_hashable() {
-_start:
-{
-obj* x_0; 
-x_0 = l_lean_name_hashable;
-return x_0;
-}
-}
-obj* _init_l_lean_ir_blockid_decidable__eq() {
-_start:
-{
-obj* x_0; 
-x_0 = l_lean_name_decidable__eq;
-return x_0;
-}
-}
-obj* _init_l_lean_ir_blockid_hashable() {
-_start:
-{
-obj* x_0; 
-x_0 = l_lean_name_hashable;
-return x_0;
-}
-}
-obj* _init_l_lean_ir_fnid_decidable__eq() {
-_start:
-{
-obj* x_0; 
-x_0 = l_lean_name_decidable__eq;
-return x_0;
-}
-}
-obj* _init_l_lean_ir_fnid_hashable() {
-_start:
-{
-obj* x_0; 
-x_0 = l_lean_name_hashable;
-return x_0;
-}
-}
-obj* _init_l_lean_ir_var__set() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_blockid__set() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_context() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_var2blockid() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_fnid2string() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_fnid__set() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_mk__var__set() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_mk__blockid__set() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_mk__var2blockid() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_mk__context() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_mk__fnid2string() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_mk__fnid__set() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-uint8 _init_l_lean_ir_inhabited() {
-_start:
-{
-uint8 x_0; 
-x_0 = 0;
-return x_0;
-}
-}
-obj* _init_l_lean_ir_inhabited___boxed() {
-_start:
-{
-uint8 x_0; obj* x_1; 
-x_0 = l_lean_ir_inhabited;
-x_1 = lean::box(x_0);
-return x_1;
-}
-}
-void initialize_init_lean_ir_ir();
-static bool _G_initialized = false;
-void initialize_init_lean_ir_instances() {
- if (_G_initialized) return;
- _G_initialized = true;
- initialize_init_lean_ir_ir();
- l_lean_ir_has__coe = _init_l_lean_ir_has__coe();
-lean::mark_persistent(l_lean_ir_has__coe);
- l_lean_ir_var__has__lt = _init_l_lean_ir_var__has__lt();
-lean::mark_persistent(l_lean_ir_var__has__lt);
- l_lean_ir_blockid__has__lt = _init_l_lean_ir_blockid__has__lt();
-lean::mark_persistent(l_lean_ir_blockid__has__lt);
- l_lean_ir_fnid__has__lt = _init_l_lean_ir_fnid__has__lt();
-lean::mark_persistent(l_lean_ir_fnid__has__lt);
- l_lean_ir_var_decidable__eq = _init_l_lean_ir_var_decidable__eq();
-lean::mark_persistent(l_lean_ir_var_decidable__eq);
- l_lean_ir_var_hashable = _init_l_lean_ir_var_hashable();
-lean::mark_persistent(l_lean_ir_var_hashable);
- l_lean_ir_blockid_decidable__eq = _init_l_lean_ir_blockid_decidable__eq();
-lean::mark_persistent(l_lean_ir_blockid_decidable__eq);
- l_lean_ir_blockid_hashable = _init_l_lean_ir_blockid_hashable();
-lean::mark_persistent(l_lean_ir_blockid_hashable);
- l_lean_ir_fnid_decidable__eq = _init_l_lean_ir_fnid_decidable__eq();
-lean::mark_persistent(l_lean_ir_fnid_decidable__eq);
- l_lean_ir_fnid_hashable = _init_l_lean_ir_fnid_hashable();
-lean::mark_persistent(l_lean_ir_fnid_hashable);
- l_lean_ir_var__set = _init_l_lean_ir_var__set();
-lean::mark_persistent(l_lean_ir_var__set);
- l_lean_ir_blockid__set = _init_l_lean_ir_blockid__set();
-lean::mark_persistent(l_lean_ir_blockid__set);
- l_lean_ir_context = _init_l_lean_ir_context();
-lean::mark_persistent(l_lean_ir_context);
- l_lean_ir_var2blockid = _init_l_lean_ir_var2blockid();
-lean::mark_persistent(l_lean_ir_var2blockid);
- l_lean_ir_fnid2string = _init_l_lean_ir_fnid2string();
-lean::mark_persistent(l_lean_ir_fnid2string);
- l_lean_ir_fnid__set = _init_l_lean_ir_fnid__set();
-lean::mark_persistent(l_lean_ir_fnid__set);
- l_lean_ir_mk__var__set = _init_l_lean_ir_mk__var__set();
-lean::mark_persistent(l_lean_ir_mk__var__set);
- l_lean_ir_mk__blockid__set = _init_l_lean_ir_mk__blockid__set();
-lean::mark_persistent(l_lean_ir_mk__blockid__set);
- l_lean_ir_mk__var2blockid = _init_l_lean_ir_mk__var2blockid();
-lean::mark_persistent(l_lean_ir_mk__var2blockid);
- l_lean_ir_mk__context = _init_l_lean_ir_mk__context();
-lean::mark_persistent(l_lean_ir_mk__context);
- l_lean_ir_mk__fnid2string = _init_l_lean_ir_mk__fnid2string();
-lean::mark_persistent(l_lean_ir_mk__fnid2string);
- l_lean_ir_mk__fnid__set = _init_l_lean_ir_mk__fnid__set();
-lean::mark_persistent(l_lean_ir_mk__fnid__set);
- l_lean_ir_inhabited = _init_l_lean_ir_inhabited();
- l_lean_ir_inhabited___boxed = _init_l_lean_ir_inhabited___boxed();
-lean::mark_persistent(l_lean_ir_inhabited___boxed);
-}

src/boot/init/lean/ir/ir.cpp

@@ -1,198 +0,0 @@
-// Lean compiler output
-// Module: init.lean.ir.ir
-// Imports: init.data.rbmap.default init.data.int.default init.control.state init.control.except init.control.combinators init.lean.name
-#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_lean_ir_decl_is__definition___boxed(obj*);
-obj* l_lean_ir_decl_header___main___boxed(obj*);
-obj* l_lean_ir_decl_name___boxed(obj*);
-obj* l_lean_ir_var;
-uint8 l_lean_ir_decl_is__definition___main(obj*);
-obj* l_lean_ir_decl_is__definition___main___boxed(obj*);
-obj* l_lean_ir_environment;
-obj* l_lean_ir_decl_header___main(obj*);
-obj* l_lean_ir_decl_header___boxed(obj*);
-obj* l_lean_ir_decl_header(obj*);
-obj* l_lean_ir_blockid;
-obj* l_lean_ir_tag;
-uint8 l_lean_ir_decl_is__definition(obj*);
-obj* l_lean_ir_decl_name(obj*);
-obj* l_lean_ir_fnid;
-obj* _init_l_lean_ir_tag() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_var() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_fnid() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-obj* _init_l_lean_ir_blockid() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-uint8 l_lean_ir_decl_is__definition___main(obj* x_0) {
-_start:
-{
-if (lean::obj_tag(x_0) == 0)
-{
-uint8 x_1; 
-x_1 = 0;
-return x_1;
-}
-else
-{
-uint8 x_2; 
-x_2 = 1;
-return x_2;
-}
-}
-}
-obj* l_lean_ir_decl_is__definition___main___boxed(obj* x_0) {
-_start:
-{
-uint8 x_1; obj* x_2; 
-x_1 = l_lean_ir_decl_is__definition___main(x_0);
-x_2 = lean::box(x_1);
-lean::dec(x_0);
-return x_2;
-}
-}
-uint8 l_lean_ir_decl_is__definition(obj* x_0) {
-_start:
-{
-uint8 x_1; 
-x_1 = l_lean_ir_decl_is__definition___main(x_0);
-return x_1;
-}
-}
-obj* l_lean_ir_decl_is__definition___boxed(obj* x_0) {
-_start:
-{
-uint8 x_1; obj* x_2; 
-x_1 = l_lean_ir_decl_is__definition(x_0);
-x_2 = lean::box(x_1);
-lean::dec(x_0);
-return x_2;
-}
-}
-obj* l_lean_ir_decl_header___main(obj* x_0) {
-_start:
-{
-obj* x_1; 
-x_1 = lean::cnstr_get(x_0, 0);
-lean::inc(x_1);
-return x_1;
-}
-}
-obj* l_lean_ir_decl_header___main___boxed(obj* x_0) {
-_start:
-{
-obj* x_1; 
-x_1 = l_lean_ir_decl_header___main(x_0);
-lean::dec(x_0);
-return x_1;
-}
-}
-obj* l_lean_ir_decl_header(obj* x_0) {
-_start:
-{
-obj* x_1; 
-x_1 = l_lean_ir_decl_header___main(x_0);
-return x_1;
-}
-}
-obj* l_lean_ir_decl_header___boxed(obj* x_0) {
-_start:
-{
-obj* x_1; 
-x_1 = l_lean_ir_decl_header(x_0);
-lean::dec(x_0);
-return x_1;
-}
-}
-obj* l_lean_ir_decl_name(obj* x_0) {
-_start:
-{
-obj* x_1; obj* x_2; 
-x_1 = l_lean_ir_decl_header___main(x_0);
-x_2 = lean::cnstr_get(x_1, 0);
-lean::inc(x_2);
-lean::dec(x_1);
-return x_2;
-}
-}
-obj* l_lean_ir_decl_name___boxed(obj* x_0) {
-_start:
-{
-obj* x_1; 
-x_1 = l_lean_ir_decl_name(x_0);
-lean::dec(x_0);
-return x_1;
-}
-}
-obj* _init_l_lean_ir_environment() {
-_start:
-{
-obj* x_0; 
-x_0 = lean::box(0);
-return x_0;
-}
-}
-void initialize_init_data_rbmap_default();
-void initialize_init_data_int_default();
-void initialize_init_control_state();
-void initialize_init_control_except();
-void initialize_init_control_combinators();
-void initialize_init_lean_name();
-static bool _G_initialized = false;
-void initialize_init_lean_ir_ir() {
- if (_G_initialized) return;
- _G_initialized = true;
- initialize_init_data_rbmap_default();
- initialize_init_data_int_default();
- initialize_init_control_state();
- initialize_init_control_except();
- initialize_init_control_combinators();
- initialize_init_lean_name();
- l_lean_ir_tag = _init_l_lean_ir_tag();
-lean::mark_persistent(l_lean_ir_tag);
- l_lean_ir_var = _init_l_lean_ir_var();
-lean::mark_persistent(l_lean_ir_var);
- l_lean_ir_fnid = _init_l_lean_ir_fnid();
-lean::mark_persistent(l_lean_ir_fnid);
- l_lean_ir_blockid = _init_l_lean_ir_blockid();
-lean::mark_persistent(l_lean_ir_blockid);
- l_lean_ir_environment = _init_l_lean_ir_environment();
-lean::mark_persistent(l_lean_ir_environment);
-}

src/boot/init/lean/ir/reserved.cpp

@@ -1,893 +0,0 @@
-// Lean compiler output
-// Module: init.lean.ir.reserved
-// Imports: init.data.rbtree.basic init.lean.name
-#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_lean_ir_reserved__set;
-obj* l_rbtree_find___at_lean_ir_is__reserved___spec__1(obj*, obj*);
-obj* l_rbnode_ins___main___at_lean_ir_reserved__set___spec__4(obj*, obj*, obj*);
-obj* l_list_foldl___main___at_lean_ir_reserved__set___spec__5(obj*, obj*);
-obj* l_rbtree_find___at_lean_ir_is__reserved___spec__1___boxed(obj*, obj*);
-obj* l_rbmap_insert___main___at_lean_ir_reserved__set___spec__2(obj*, obj*, obj*);
-obj* l_rbnode_insert___at_lean_ir_reserved__set___spec__3(obj*, obj*, obj*);
-obj* l_rbnode_find__core___main___at_lean_ir_is__reserved___spec__3(obj*, obj*);
-uint8 l_lean_ir_is__reserved(obj*);
-obj* l_lean_ir_is__reserved__name___boxed(obj*);
-uint8 l_option_is__some___main___rarg(obj*);
-namespace lean {
-uint8 string_dec_lt(obj*, obj*);
-}
-obj* l_rbnode_balance2___main___rarg(obj*, obj*);
-uint8 l_lean_ir_is__reserved__name(obj*);
-obj* l_rbtree_insert___at_lean_ir_reserved__set___spec__1(obj*, obj*);
-obj* l_rbmap_find__core___main___at_lean_ir_is__reserved___spec__2___boxed(obj*, obj*);
-obj* l_lean_ir_reserved;
-obj* l_lean_ir_is__reserved__name___main___boxed(obj*);
-obj* l_rbnode_find__core___main___at_lean_ir_is__reserved___spec__3___boxed(obj*, obj*);
-uint8 l_lean_ir_is__reserved__name___main(obj*);
-obj* l_rbnode_balance1___main___rarg(obj*, obj*);
-obj* l_lean_ir_is__reserved___boxed(obj*);
-obj* l_rbmap_find__core___main___at_lean_ir_is__reserved___spec__2(obj*, obj*);
-uint8 l_rbnode_is__red___main___rarg(obj*);
-obj* l_rbnode_set__black___main___rarg(obj*);
-obj* _init_l_lean_ir_reserved() {
-_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; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; 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_39; obj* x_40; obj* x_41; obj* x_42; obj* x_43; obj* x_44; obj* x_45; obj* x_46; obj* x_47; obj* x_48; obj* x_49; obj* x_50; obj* x_51; obj* x_52; obj* x_53; obj* x_54; obj* x_55; obj* x_56; obj* x_57; obj* x_58; obj* x_59; obj* x_60; obj* x_61; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_68; obj* x_69; obj* x_70; obj* x_71; obj* x_72; obj* x_73; obj* x_74; obj* x_75; obj* x_76; obj* x_77; obj* x_78; 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_87; obj* x_88; obj* x_89; obj* x_90; obj* x_91; obj* x_92; obj* x_93; obj* x_94; obj* x_95; obj* x_96; obj* x_97; obj* x_98; obj* x_99; obj* x_100; obj* x_101; obj* x_102; 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; obj* x_142; obj* x_143; obj* x_144; obj* x_145; obj* x_146; obj* x_147; obj* x_148; obj* x_149; obj* x_150; obj* x_151; obj* x_152; obj* x_153; obj* x_154; obj* x_155; obj* x_156; obj* x_157; obj* x_158; obj* x_159; obj* x_160; obj* x_161; obj* x_162; obj* x_163; obj* x_164; obj* x_165; obj* x_166; 
-x_0 = lean::box(0);
-x_1 = lean::mk_string("external");
-x_2 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_2, 0, x_1);
-lean::cnstr_set(x_2, 1, x_0);
-x_3 = lean::mk_string("def");
-x_4 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_4, 0, x_3);
-lean::cnstr_set(x_4, 1, x_2);
-x_5 = lean::mk_string("jmp");
-x_6 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_6, 0, x_5);
-lean::cnstr_set(x_6, 1, x_4);
-x_7 = lean::mk_string("case");
-x_8 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_8, 0, x_7);
-lean::cnstr_set(x_8, 1, x_6);
-x_9 = lean::mk_string("ret");
-x_10 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_10, 0, x_9);
-lean::cnstr_set(x_10, 1, x_8);
-x_11 = lean::mk_string("phi");
-x_12 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_12, 0, x_11);
-lean::cnstr_set(x_12, 1, x_10);
-x_13 = lean::mk_string("array_write");
-x_14 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_14, 0, x_13);
-lean::cnstr_set(x_14, 1, x_12);
-x_15 = lean::mk_string("sarray");
-x_16 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_16, 0, x_15);
-lean::cnstr_set(x_16, 1, x_14);
-x_17 = lean::mk_string("array");
-x_18 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_18, 0, x_17);
-lean::cnstr_set(x_18, 1, x_16);
-x_19 = lean::mk_string("apply");
-x_20 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_20, 0, x_19);
-lean::cnstr_set(x_20, 1, x_18);
-x_21 = lean::mk_string("closure");
-x_22 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_22, 0, x_21);
-lean::cnstr_set(x_22, 1, x_20);
-x_23 = lean::mk_string("sget");
-x_24 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_24, 0, x_23);
-lean::cnstr_set(x_24, 1, x_22);
-x_25 = lean::mk_string("sset");
-x_26 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_26, 0, x_25);
-lean::cnstr_set(x_26, 1, x_24);
-x_27 = lean::mk_string("get");
-x_28 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_28, 0, x_27);
-lean::cnstr_set(x_28, 1, x_26);
-x_29 = lean::mk_string("set");
-x_30 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_30, 0, x_29);
-lean::cnstr_set(x_30, 1, x_28);
-x_31 = lean::mk_string("cnstr");
-x_32 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_32, 0, x_31);
-lean::cnstr_set(x_32, 1, x_30);
-x_33 = lean::mk_string("call");
-x_34 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_34, 0, x_33);
-lean::cnstr_set(x_34, 1, x_32);
-x_35 = lean::mk_string("sarray_pop");
-x_36 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_36, 0, x_35);
-lean::cnstr_set(x_36, 1, x_34);
-x_37 = lean::mk_string("array_pop");
-x_38 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_38, 0, x_37);
-lean::cnstr_set(x_38, 1, x_36);
-x_39 = lean::mk_string("dealloc");
-x_40 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_40, 0, x_39);
-lean::cnstr_set(x_40, 1, x_38);
-x_41 = lean::mk_string("free");
-x_42 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_42, 0, x_41);
-lean::cnstr_set(x_42, 1, x_40);
-x_43 = lean::mk_string("dec");
-x_44 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_44, 0, x_43);
-lean::cnstr_set(x_44, 1, x_42);
-x_45 = lean::mk_string("inc");
-x_46 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_46, 0, x_45);
-lean::cnstr_set(x_46, 1, x_44);
-x_47 = lean::mk_string("dec_sref");
-x_48 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_48, 0, x_47);
-lean::cnstr_set(x_48, 1, x_46);
-x_49 = lean::mk_string("dec_ref");
-x_50 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_50, 0, x_49);
-lean::cnstr_set(x_50, 1, x_48);
-x_51 = lean::mk_string("inc_ref");
-x_52 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_52, 0, x_51);
-lean::cnstr_set(x_52, 1, x_50);
-x_53 = lean::mk_string("string_append");
-x_54 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_54, 0, x_53);
-lean::cnstr_set(x_54, 1, x_52);
-x_55 = lean::mk_string("string_push");
-x_56 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_56, 0, x_55);
-lean::cnstr_set(x_56, 1, x_54);
-x_57 = lean::mk_string("array_push");
-x_58 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_58, 0, x_57);
-lean::cnstr_set(x_58, 1, x_56);
-x_59 = lean::mk_string("array_read");
-x_60 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_60, 0, x_59);
-lean::cnstr_set(x_60, 1, x_58);
-x_61 = lean::mk_string("ine");
-x_62 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_62, 0, x_61);
-lean::cnstr_set(x_62, 1, x_60);
-x_63 = lean::mk_string("ieq");
-x_64 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_64, 0, x_63);
-lean::cnstr_set(x_64, 1, x_62);
-x_65 = lean::mk_string("ilt");
-x_66 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_66, 0, x_65);
-lean::cnstr_set(x_66, 1, x_64);
-x_67 = lean::mk_string("ile");
-x_68 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_68, 0, x_67);
-lean::cnstr_set(x_68, 1, x_66);
-x_69 = lean::mk_string("ne");
-x_70 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_70, 0, x_69);
-lean::cnstr_set(x_70, 1, x_68);
-x_71 = lean::mk_string("eq");
-x_72 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_72, 0, x_71);
-lean::cnstr_set(x_72, 1, x_70);
-x_73 = lean::mk_string("lt");
-x_74 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_74, 0, x_73);
-lean::cnstr_set(x_74, 1, x_72);
-x_75 = lean::mk_string("le");
-x_76 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_76, 0, x_75);
-lean::cnstr_set(x_76, 1, x_74);
-x_77 = lean::mk_string("xor");
-x_78 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_78, 0, x_77);
-lean::cnstr_set(x_78, 1, x_76);
-x_79 = lean::mk_string("or");
-x_80 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_80, 0, x_79);
-lean::cnstr_set(x_80, 1, x_78);
-x_81 = lean::mk_string("and");
-x_82 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_82, 0, x_81);
-lean::cnstr_set(x_82, 1, x_80);
-x_83 = lean::mk_string("shr");
-x_84 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_84, 0, x_83);
-lean::cnstr_set(x_84, 1, x_82);
-x_85 = lean::mk_string("shl");
-x_86 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_86, 0, x_85);
-lean::cnstr_set(x_86, 1, x_84);
-x_87 = lean::mk_string("imod");
-x_88 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_88, 0, x_87);
-lean::cnstr_set(x_88, 1, x_86);
-x_89 = lean::mk_string("idiv");
-x_90 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_90, 0, x_89);
-lean::cnstr_set(x_90, 1, x_88);
-x_91 = lean::mk_string("imul");
-x_92 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_92, 0, x_91);
-lean::cnstr_set(x_92, 1, x_90);
-x_93 = lean::mk_string("isub");
-x_94 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_94, 0, x_93);
-lean::cnstr_set(x_94, 1, x_92);
-x_95 = lean::mk_string("iadd");
-x_96 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_96, 0, x_95);
-lean::cnstr_set(x_96, 1, x_94);
-x_97 = lean::mk_string("mod");
-x_98 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_98, 0, x_97);
-lean::cnstr_set(x_98, 1, x_96);
-x_99 = lean::mk_string("div");
-x_100 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_100, 0, x_99);
-lean::cnstr_set(x_100, 1, x_98);
-x_101 = lean::mk_string("mul");
-x_102 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_102, 0, x_101);
-lean::cnstr_set(x_102, 1, x_100);
-x_103 = lean::mk_string("sub");
-x_104 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_104, 0, x_103);
-lean::cnstr_set(x_104, 1, x_102);
-x_105 = lean::mk_string("add");
-x_106 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_106, 0, x_105);
-lean::cnstr_set(x_106, 1, x_104);
-x_107 = lean::mk_string("tag_ref");
-x_108 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_108, 0, x_107);
-lean::cnstr_set(x_108, 1, x_106);
-x_109 = lean::mk_string("tag");
-x_110 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_110, 0, x_109);
-lean::cnstr_set(x_110, 1, x_108);
-x_111 = lean::mk_string("succ");
-x_112 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_112, 0, x_111);
-lean::cnstr_set(x_112, 1, x_110);
-x_113 = lean::mk_string("string_len");
-x_114 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_114, 0, x_113);
-lean::cnstr_set(x_114, 1, x_112);
-x_115 = lean::mk_string("sarray_size");
-x_116 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_116, 0, x_115);
-lean::cnstr_set(x_116, 1, x_114);
-x_117 = lean::mk_string("array_size");
-x_118 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_118, 0, x_117);
-lean::cnstr_set(x_118, 1, x_116);
-x_119 = lean::mk_string("sarray_copy");
-x_120 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_120, 0, x_119);
-lean::cnstr_set(x_120, 1, x_118);
-x_121 = lean::mk_string("array_copy");
-x_122 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_122, 0, x_121);
-lean::cnstr_set(x_122, 1, x_120);
-x_123 = lean::mk_string("cast");
-x_124 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_124, 0, x_123);
-lean::cnstr_set(x_124, 1, x_122);
-x_125 = lean::mk_string("box");
-x_126 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_126, 0, x_125);
-lean::cnstr_set(x_126, 1, x_124);
-x_127 = lean::mk_string("unbox");
-x_128 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_128, 0, x_127);
-lean::cnstr_set(x_128, 1, x_126);
-x_129 = lean::mk_string("is_null");
-x_130 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_130, 0, x_129);
-lean::cnstr_set(x_130, 1, x_128);
-x_131 = lean::mk_string("is_shared");
-x_132 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_132, 0, x_131);
-lean::cnstr_set(x_132, 1, x_130);
-x_133 = lean::mk_string("is_scalar");
-x_134 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_134, 0, x_133);
-lean::cnstr_set(x_134, 1, x_132);
-x_135 = lean::mk_string("nat2int");
-x_136 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_136, 0, x_135);
-lean::cnstr_set(x_136, 1, x_134);
-x_137 = lean::mk_string("ineg");
-x_138 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_138, 0, x_137);
-lean::cnstr_set(x_138, 1, x_136);
-x_139 = lean::mk_string("neg");
-x_140 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_140, 0, x_139);
-lean::cnstr_set(x_140, 1, x_138);
-x_141 = lean::mk_string("not");
-x_142 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_142, 0, x_141);
-lean::cnstr_set(x_142, 1, x_140);
-x_143 = lean::mk_string("object");
-x_144 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_144, 0, x_143);
-lean::cnstr_set(x_144, 1, x_142);
-x_145 = lean::mk_string("double");
-x_146 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_146, 0, x_145);
-lean::cnstr_set(x_146, 1, x_144);
-x_147 = lean::mk_string("float");
-x_148 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_148, 0, x_147);
-lean::cnstr_set(x_148, 1, x_146);
-x_149 = lean::mk_string("int64");
-x_150 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_150, 0, x_149);
-lean::cnstr_set(x_150, 1, x_148);
-x_151 = lean::mk_string("int32");
-x_152 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_152, 0, x_151);
-lean::cnstr_set(x_152, 1, x_150);
-x_153 = lean::mk_string("int16");
-x_154 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_154, 0, x_153);
-lean::cnstr_set(x_154, 1, x_152);
-x_155 = lean::mk_string("usize");
-x_156 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_156, 0, x_155);
-lean::cnstr_set(x_156, 1, x_154);
-x_157 = lean::mk_string("uint64");
-x_158 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_158, 0, x_157);
-lean::cnstr_set(x_158, 1, x_156);
-x_159 = lean::mk_string("uint32");
-x_160 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_160, 0, x_159);
-lean::cnstr_set(x_160, 1, x_158);
-x_161 = lean::mk_string("uint16");
-x_162 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_162, 0, x_161);
-lean::cnstr_set(x_162, 1, x_160);
-x_163 = lean::mk_string("byte");
-x_164 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_164, 0, x_163);
-lean::cnstr_set(x_164, 1, x_162);
-x_165 = lean::mk_string("bool");
-x_166 = lean::alloc_cnstr(1, 2, 0);
-lean::cnstr_set(x_166, 0, x_165);
-lean::cnstr_set(x_166, 1, x_164);
-return x_166;
-}
-}
-obj* l_rbnode_ins___main___at_lean_ir_reserved__set___spec__4(obj* x_0, obj* x_1, obj* x_2) {
-_start:
-{
-if (lean::obj_tag(x_0) == 0)
-{
-uint8 x_3; obj* x_4; obj* x_5; 
-x_3 = 0;
-x_4 = lean::alloc_cnstr(1, 4, 1);
-lean::cnstr_set(x_4, 0, x_0);
-lean::cnstr_set(x_4, 1, x_1);
-lean::cnstr_set(x_4, 2, x_2);
-lean::cnstr_set(x_4, 3, x_0);
-lean::cnstr_set_scalar(x_4, sizeof(void*)*4, x_3);
-x_5 = x_4;
-return x_5;
-}
-else
-{
-uint8 x_6; 
-x_6 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*4);
-if (x_6 == 0)
-{
-obj* x_7; obj* x_9; obj* x_11; obj* x_13; obj* x_15; uint8 x_16; 
-x_7 = lean::cnstr_get(x_0, 0);
-x_9 = lean::cnstr_get(x_0, 1);
-x_11 = lean::cnstr_get(x_0, 2);
-x_13 = lean::cnstr_get(x_0, 3);
-if (lean::is_exclusive(x_0)) {
- lean::cnstr_set(x_0, 0, lean::box(0));
- lean::cnstr_set(x_0, 1, lean::box(0));
- lean::cnstr_set(x_0, 2, lean::box(0));
- lean::cnstr_set(x_0, 3, lean::box(0));
- x_15 = x_0;
-} else {
- lean::inc(x_7);
- lean::inc(x_9);
- lean::inc(x_11);
- lean::inc(x_13);
- lean::dec(x_0);
- x_15 = lean::box(0);
-}
-x_16 = lean::string_dec_lt(x_1, x_9);
-if (x_16 == 0)
-{
-uint8 x_17; 
-x_17 = lean::string_dec_lt(x_9, x_1);
-if (x_17 == 0)
-{
-obj* x_20; obj* x_21; 
-lean::dec(x_9);
-lean::dec(x_11);
-if (lean::is_scalar(x_15)) {
- x_20 = lean::alloc_cnstr(1, 4, 1);
-} else {
- x_20 = x_15;
-}
-lean::cnstr_set(x_20, 0, x_7);
-lean::cnstr_set(x_20, 1, x_1);
-lean::cnstr_set(x_20, 2, x_2);
-lean::cnstr_set(x_20, 3, x_13);
-lean::cnstr_set_scalar(x_20, sizeof(void*)*4, x_6);
-x_21 = x_20;
-return x_21;
-}
-else
-{
-obj* x_22; obj* x_23; obj* x_24; 
-x_22 = l_rbnode_ins___main___at_lean_ir_reserved__set___spec__4(x_13, x_1, x_2);
-if (lean::is_scalar(x_15)) {
- x_23 = lean::alloc_cnstr(1, 4, 1);
-} else {
- x_23 = x_15;
-}
-lean::cnstr_set(x_23, 0, x_7);
-lean::cnstr_set(x_23, 1, x_9);
-lean::cnstr_set(x_23, 2, x_11);
-lean::cnstr_set(x_23, 3, x_22);
-lean::cnstr_set_scalar(x_23, sizeof(void*)*4, x_6);
-x_24 = x_23;
-return x_24;
-}
-}
-else
-{
-obj* x_25; obj* x_26; obj* x_27; 
-x_25 = l_rbnode_ins___main___at_lean_ir_reserved__set___spec__4(x_7, x_1, x_2);
-if (lean::is_scalar(x_15)) {
- x_26 = lean::alloc_cnstr(1, 4, 1);
-} else {
- x_26 = x_15;
-}
-lean::cnstr_set(x_26, 0, x_25);
-lean::cnstr_set(x_26, 1, x_9);
-lean::cnstr_set(x_26, 2, x_11);
-lean::cnstr_set(x_26, 3, x_13);
-lean::cnstr_set_scalar(x_26, sizeof(void*)*4, x_6);
-x_27 = x_26;
-return x_27;
-}
-}
-else
-{
-obj* x_28; obj* x_30; obj* x_32; obj* x_34; obj* x_36; uint8 x_37; 
-x_28 = lean::cnstr_get(x_0, 0);
-x_30 = lean::cnstr_get(x_0, 1);
-x_32 = lean::cnstr_get(x_0, 2);
-x_34 = lean::cnstr_get(x_0, 3);
-if (lean::is_exclusive(x_0)) {
- lean::cnstr_set(x_0, 0, lean::box(0));
- lean::cnstr_set(x_0, 1, lean::box(0));
- lean::cnstr_set(x_0, 2, lean::box(0));
- lean::cnstr_set(x_0, 3, lean::box(0));
- x_36 = x_0;
-} else {
- lean::inc(x_28);
- lean::inc(x_30);
- lean::inc(x_32);
- lean::inc(x_34);
- lean::dec(x_0);
- x_36 = lean::box(0);
-}
-x_37 = lean::string_dec_lt(x_1, x_30);
-if (x_37 == 0)
-{
-uint8 x_38; 
-x_38 = lean::string_dec_lt(x_30, x_1);
-if (x_38 == 0)
-{
-obj* x_41; obj* x_42; 
-lean::dec(x_30);
-lean::dec(x_32);
-if (lean::is_scalar(x_36)) {
- x_41 = lean::alloc_cnstr(1, 4, 1);
-} else {
- x_41 = x_36;
-}
-lean::cnstr_set(x_41, 0, x_28);
-lean::cnstr_set(x_41, 1, x_1);
-lean::cnstr_set(x_41, 2, x_2);
-lean::cnstr_set(x_41, 3, x_34);
-lean::cnstr_set_scalar(x_41, sizeof(void*)*4, x_6);
-x_42 = x_41;
-return x_42;
-}
-else
-{
-uint8 x_43; 
-x_43 = l_rbnode_is__red___main___rarg(x_34);
-if (x_43 == 0)
-{
-obj* x_44; obj* x_45; obj* x_46; 
-x_44 = l_rbnode_ins___main___at_lean_ir_reserved__set___spec__4(x_34, x_1, x_2);
-if (lean::is_scalar(x_36)) {
- x_45 = lean::alloc_cnstr(1, 4, 1);
-} else {
- x_45 = x_36;
-}
-lean::cnstr_set(x_45, 0, x_28);
-lean::cnstr_set(x_45, 1, x_30);
-lean::cnstr_set(x_45, 2, x_32);
-lean::cnstr_set(x_45, 3, x_44);
-lean::cnstr_set_scalar(x_45, sizeof(void*)*4, x_6);
-x_46 = x_45;
-return x_46;
-}
-else
-{
-obj* x_47; obj* x_48; obj* x_49; obj* x_50; obj* x_51; 
-x_47 = lean::box(0);
-if (lean::is_scalar(x_36)) {
- x_48 = lean::alloc_cnstr(1, 4, 1);
-} else {
- x_48 = x_36;
-}
-lean::cnstr_set(x_48, 0, x_28);
-lean::cnstr_set(x_48, 1, x_30);
-lean::cnstr_set(x_48, 2, x_32);
-lean::cnstr_set(x_48, 3, x_47);
-lean::cnstr_set_scalar(x_48, sizeof(void*)*4, x_6);
-x_49 = x_48;
-x_50 = l_rbnode_ins___main___at_lean_ir_reserved__set___spec__4(x_34, x_1, x_2);
-x_51 = l_rbnode_balance2___main___rarg(x_49, x_50);
-return x_51;
-}
-}
-}
-else
-{
-uint8 x_52; 
-x_52 = l_rbnode_is__red___main___rarg(x_28);
-if (x_52 == 0)
-{
-obj* x_53; obj* x_54; obj* x_55; 
-x_53 = l_rbnode_ins___main___at_lean_ir_reserved__set___spec__4(x_28, x_1, x_2);
-if (lean::is_scalar(x_36)) {
- x_54 = lean::alloc_cnstr(1, 4, 1);
-} else {
- x_54 = x_36;
-}
-lean::cnstr_set(x_54, 0, x_53);
-lean::cnstr_set(x_54, 1, x_30);
-lean::cnstr_set(x_54, 2, x_32);
-lean::cnstr_set(x_54, 3, x_34);
-lean::cnstr_set_scalar(x_54, sizeof(void*)*4, x_6);
-x_55 = x_54;
-return x_55;
-}
-else
-{
-obj* x_56; obj* x_57; obj* x_58; obj* x_59; obj* x_60; 
-x_56 = lean::box(0);
-if (lean::is_scalar(x_36)) {
- x_57 = lean::alloc_cnstr(1, 4, 1);
-} else {
- x_57 = x_36;
-}
-lean::cnstr_set(x_57, 0, x_56);
-lean::cnstr_set(x_57, 1, x_30);
-lean::cnstr_set(x_57, 2, x_32);
-lean::cnstr_set(x_57, 3, x_34);
-lean::cnstr_set_scalar(x_57, sizeof(void*)*4, x_6);
-x_58 = x_57;
-x_59 = l_rbnode_ins___main___at_lean_ir_reserved__set___spec__4(x_28, x_1, x_2);
-x_60 = l_rbnode_balance1___main___rarg(x_58, x_59);
-return x_60;
-}
-}
-}
-}
-}
-}
-obj* l_rbnode_insert___at_lean_ir_reserved__set___spec__3(obj* x_0, obj* x_1, obj* x_2) {
-_start:
-{
-uint8 x_3; 
-x_3 = l_rbnode_is__red___main___rarg(x_0);
-if (x_3 == 0)
-{
-obj* x_4; 
-x_4 = l_rbnode_ins___main___at_lean_ir_reserved__set___spec__4(x_0, x_1, x_2);
-return x_4;
-}
-else
-{
-obj* x_5; obj* x_6; 
-x_5 = l_rbnode_ins___main___at_lean_ir_reserved__set___spec__4(x_0, x_1, x_2);
-x_6 = l_rbnode_set__black___main___rarg(x_5);
-return x_6;
-}
-}
-}
-obj* l_rbmap_insert___main___at_lean_ir_reserved__set___spec__2(obj* x_0, obj* x_1, obj* x_2) {
-_start:
-{
-obj* x_3; 
-x_3 = l_rbnode_insert___at_lean_ir_reserved__set___spec__3(x_0, x_1, x_2);
-return x_3;
-}
-}
-obj* l_rbtree_insert___at_lean_ir_reserved__set___spec__1(obj* x_0, obj* x_1) {
-_start:
-{
-obj* x_2; obj* x_3; 
-x_2 = lean::box(0);
-x_3 = l_rbnode_insert___at_lean_ir_reserved__set___spec__3(x_0, x_1, x_2);
-return x_3;
-}
-}
-obj* l_list_foldl___main___at_lean_ir_reserved__set___spec__5(obj* x_0, obj* x_1) {
-_start:
-{
-if (lean::obj_tag(x_1) == 0)
-{
-return x_0;
-}
-else
-{
-obj* x_2; obj* x_4; obj* x_7; obj* x_8; 
-x_2 = lean::cnstr_get(x_1, 0);
-lean::inc(x_2);
-x_4 = lean::cnstr_get(x_1, 1);
-lean::inc(x_4);
-lean::dec(x_1);
-x_7 = lean::box(0);
-x_8 = l_rbnode_insert___at_lean_ir_reserved__set___spec__3(x_0, x_2, x_7);
-x_0 = x_8;
-x_1 = x_4;
-goto _start;
-}
-}
-}
-obj* _init_l_lean_ir_reserved__set() {
-_start:
-{
-obj* x_0; obj* x_1; obj* x_2; 
-x_0 = lean::box(0);
-x_1 = l_lean_ir_reserved;
-x_2 = l_list_foldl___main___at_lean_ir_reserved__set___spec__5(x_0, x_1);
-return x_2;
-}
-}
-obj* l_rbnode_find__core___main___at_lean_ir_is__reserved___spec__3(obj* x_0, obj* x_1) {
-_start:
-{
-if (lean::obj_tag(x_0) == 0)
-{
-obj* x_2; 
-x_2 = lean::box(0);
-return x_2;
-}
-else
-{
-obj* x_3; obj* x_5; obj* x_7; obj* x_9; uint8 x_12; 
-x_3 = lean::cnstr_get(x_0, 0);
-lean::inc(x_3);
-x_5 = lean::cnstr_get(x_0, 1);
-lean::inc(x_5);
-x_7 = lean::cnstr_get(x_0, 2);
-lean::inc(x_7);
-x_9 = lean::cnstr_get(x_0, 3);
-lean::inc(x_9);
-lean::dec(x_0);
-x_12 = lean::string_dec_lt(x_1, x_5);
-if (x_12 == 0)
-{
-uint8 x_14; 
-lean::dec(x_3);
-x_14 = lean::string_dec_lt(x_5, x_1);
-if (x_14 == 0)
-{
-obj* x_16; obj* x_17; 
-lean::dec(x_9);
-x_16 = lean::alloc_cnstr(0, 2, 0);
-lean::cnstr_set(x_16, 0, x_5);
-lean::cnstr_set(x_16, 1, x_7);
-x_17 = lean::alloc_cnstr(1, 1, 0);
-lean::cnstr_set(x_17, 0, x_16);
-return x_17;
-}
-else
-{
-lean::dec(x_7);
-lean::dec(x_5);
-x_0 = x_9;
-goto _start;
-}
-}
-else
-{
-lean::dec(x_7);
-lean::dec(x_9);
-lean::dec(x_5);
-x_0 = x_3;
-goto _start;
-}
-}
-}
-}
-obj* l_rbmap_find__core___main___at_lean_ir_is__reserved___spec__2(obj* x_0, obj* x_1) {
-_start:
-{
-obj* x_2; 
-x_2 = l_rbnode_find__core___main___at_lean_ir_is__reserved___spec__3(x_0, x_1);
-return x_2;
-}
-}
-obj* l_rbtree_find___at_lean_ir_is__reserved___spec__1(obj* x_0, obj* x_1) {
-_start:
-{
-obj* x_2; 
-x_2 = l_rbnode_find__core___main___at_lean_ir_is__reserved___spec__3(x_0, x_1);
-if (lean::obj_tag(x_2) == 0)
-{
-obj* x_3; 
-x_3 = lean::box(0);
-return x_3;
-}
-else
-{
-obj* x_4; obj* x_6; obj* x_7; obj* x_10; 
-x_4 = lean::cnstr_get(x_2, 0);
-if (lean::is_exclusive(x_2)) {
- x_6 = x_2;
-} else {
- lean::inc(x_4);
- lean::dec(x_2);
- x_6 = lean::box(0);
-}
-x_7 = lean::cnstr_get(x_4, 0);
-lean::inc(x_7);
-lean::dec(x_4);
-if (lean::is_scalar(x_6)) {
- x_10 = lean::alloc_cnstr(1, 1, 0);
-} else {
- x_10 = x_6;
-}
-lean::cnstr_set(x_10, 0, x_7);
-return x_10;
-}
-}
-}
-uint8 l_lean_ir_is__reserved(obj* x_0) {
-_start:
-{
-obj* x_1; obj* x_2; uint8 x_3; 
-x_1 = l_lean_ir_reserved__set;
-x_2 = l_rbtree_find___at_lean_ir_is__reserved___spec__1(x_1, x_0);
-x_3 = l_option_is__some___main___rarg(x_2);
-lean::dec(x_2);
-return x_3;
-}
-}
-obj* l_rbnode_find__core___main___at_lean_ir_is__reserved___spec__3___boxed(obj* x_0, obj* x_1) {
-_start:
-{
-obj* x_2; 
-x_2 = l_rbnode_find__core___main___at_lean_ir_is__reserved___spec__3(x_0, x_1);
-lean::dec(x_1);
-return x_2;
-}
-}
-obj* l_rbmap_find__core___main___at_lean_ir_is__reserved___spec__2___boxed(obj* x_0, obj* x_1) {
-_start:
-{
-obj* x_2; 
-x_2 = l_rbmap_find__core___main___at_lean_ir_is__reserved___spec__2(x_0, x_1);
-lean::dec(x_1);
-return x_2;
-}
-}
-obj* l_rbtree_find___at_lean_ir_is__reserved___spec__1___boxed(obj* x_0, obj* x_1) {
-_start:
-{
-obj* x_2; 
-x_2 = l_rbtree_find___at_lean_ir_is__reserved___spec__1(x_0, x_1);
-lean::dec(x_1);
-return x_2;
-}
-}
-obj* l_lean_ir_is__reserved___boxed(obj* x_0) {
-_start:
-{
-uint8 x_1; obj* x_2; 
-x_1 = l_lean_ir_is__reserved(x_0);
-x_2 = lean::box(x_1);
-lean::dec(x_0);
-return x_2;
-}
-}
-uint8 l_lean_ir_is__reserved__name___main(obj* x_0) {
-_start:
-{
-switch (lean::obj_tag(x_0)) {
-case 1:
-{
-obj* x_1; uint8 x_2; 
-x_1 = lean::cnstr_get(x_0, 1);
-x_2 = l_lean_ir_is__reserved(x_1);
-return x_2;
-}
-default:
-{
-uint8 x_3; 
-x_3 = 0;
-return x_3;
-}
-}
-}
-}
-obj* l_lean_ir_is__reserved__name___main___boxed(obj* x_0) {
-_start:
-{
-uint8 x_1; obj* x_2; 
-x_1 = l_lean_ir_is__reserved__name___main(x_0);
-x_2 = lean::box(x_1);
-lean::dec(x_0);
-return x_2;
-}
-}
-uint8 l_lean_ir_is__reserved__name(obj* x_0) {
-_start:
-{
-uint8 x_1; 
-x_1 = l_lean_ir_is__reserved__name___main(x_0);
-return x_1;
-}
-}
-obj* l_lean_ir_is__reserved__name___boxed(obj* x_0) {
-_start:
-{
-uint8 x_1; obj* x_2; 
-x_1 = l_lean_ir_is__reserved__name(x_0);
-x_2 = lean::box(x_1);
-lean::dec(x_0);
-return x_2;
-}
-}
-void initialize_init_data_rbtree_basic();
-void initialize_init_lean_name();
-static bool _G_initialized = false;
-void initialize_init_lean_ir_reserved() {
- if (_G_initialized) return;
- _G_initialized = true;
- initialize_init_data_rbtree_basic();
- initialize_init_lean_name();
- l_lean_ir_reserved = _init_l_lean_ir_reserved();
-lean::mark_persistent(l_lean_ir_reserved);
- l_lean_ir_reserved__set = _init_l_lean_ir_reserved__set();
-lean::mark_persistent(l_lean_ir_reserved__set);
-}