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

chore(library/compiler/ir): remove box(13) hack

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-16 20:58:30 -07:00
parent ec0e74f5f8
commit 4429aac0b3
3 changed files with 966 additions and 980 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/lean/compiler/ir/basic.lean
View file

@ -125,7 +125,6 @@ instance : Inhabited Arg := ⟨irrelevant⟩
end Arg
@[export lean_ir_mk_var_arg] def mkVarArg (id : VarId) : Arg := Arg.var id
@[export lean_ir_mk_irrelevant_arg] def mkIrrelevantArg : Arg := Arg.irrelevant
inductive LitVal
| num (v : Nat)
@ -250,7 +249,7 @@ abbrev FnBody.nil := FnBody.unreachable
@[export lean_ir_mk_case] def mkCase (tid : Name) (x : VarId) (cs : Array (AltCore FnBody)) : FnBody := FnBody.case tid x cs
@[export lean_ir_mk_ret] def mkRet (x : Arg) : FnBody := FnBody.ret x
@[export lean_ir_mk_jmp] def mkJmp (j : JoinPointId) (ys : Array Arg) : FnBody := FnBody.jmp j ys
@[export lean_ir_mk_unreachable] def mkUnreachable : FnBody := FnBody.unreachable
@[export lean_ir_mk_unreachable] def mkUnreachable : Unit → FnBody := fun _ => FnBody.unreachable
abbrev Alt := AltCore FnBody
@[matchPattern] abbrev Alt.ctor := @AltCore.ctor FnBody

11
src/library/compiler/ir.cpp
View file

@ -15,9 +15,9 @@ Author: Leonardo de Moura
#include "library/compiler/extern_attribute.h"
namespace lean {
object * lean_ir_mk_irrelevant_arg; // HACK @[export] with extern "C" does not work for constants
object * lean_ir_mk_unreachable; // HACK @[export] with extern "C" does not work for constants
namespace ir {
object * irrelevant_arg;
extern "C" object * lean_ir_mk_unreachable(object *);
extern "C" object * lean_ir_mk_var_arg(object * id);
extern "C" object * lean_ir_mk_param(object * x, uint8 borrowed, uint8 ty);
extern "C" object * lean_ir_mk_ctor_expr(object * n, object * cidx, object * size, object * usize, object * ssize, object * ys);
@ -61,7 +61,7 @@ typedef object_ref alt;
typedef object_ref decl;
arg mk_var_arg(var_id const & id) { inc(id.raw()); return arg(lean_ir_mk_var_arg(id.raw())); }
arg mk_irrelevant_arg() { return arg(lean_ir_mk_irrelevant_arg); }
arg mk_irrelevant_arg() { return arg(irrelevant_arg); }
param mk_param(var_id const & x, type ty, bool borrowed = false) {
return param(lean_ir_mk_param(x.to_obj_arg(), borrowed, static_cast<uint8>(ty)));
}
@ -90,7 +90,7 @@ fn_body mk_sset(var_id const & x, unsigned i, unsigned o, var_id const & y, type
return fn_body(lean_ir_mk_sset(x.to_obj_arg(), mk_nat_obj(i), mk_nat_obj(o), y.to_obj_arg(), static_cast<uint8>(ty), b.to_obj_arg()));
}
fn_body mk_ret(arg const & x) { return fn_body(lean_ir_mk_ret(x.to_obj_arg())); }
fn_body mk_unreachable() { return fn_body(lean_ir_mk_unreachable); }
fn_body mk_unreachable() { return fn_body(lean_ir_mk_unreachable(box(0))); }
alt mk_alt(name const & n, unsigned cidx, unsigned size, unsigned usize, unsigned ssize, fn_body const & b) {
return alt(lean_ir_mk_alt(n.to_obj_arg(), mk_nat_obj(cidx), mk_nat_obj(size), mk_nat_obj(usize), mk_nat_obj(ssize), b.to_obj_arg()));
}
@ -566,8 +566,7 @@ string_ref emit_cpp(environment const & env, name const & mod_name) {
}
void initialize_ir() {
lean_ir_mk_irrelevant_arg = box(1);
lean_ir_mk_unreachable = box(13); // TOO HACKISH!!! It must be deleted in the future.
ir::irrelevant_arg = box(1);
}
void finalize_ir() {

1932
src/stage0/init/lean/compiler/ir/basic.cpp generated
View file

File diff suppressed because it is too large Load diff