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

chore(runtime/object): preparing for implementing object.h using lean.h

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-20 13:00:18 -07:00
parent 4405b30cc8
commit 25481d5cef
3 changed files with 56 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/compiler/ir/emitc.lean
View file

@ -349,7 +349,7 @@ else
emit offset
def emitUSet (x : VarId) (n : Nat) (y : VarId) : M Unit :=
do emit "lean_ctor_set_usize("; emit x; emit ", "; emitOffset n 0; emit ", "; emit y; emitLn ");"
do emit "lean_ctor_set_usize("; emit x; emit ", "; emit n; emit ", "; emit y; emitLn ");"
def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M Unit :=
do

28
library/init/lean/compiler/ir/emitcpp.lean
View file

@ -359,10 +359,18 @@ else
emit offset
def emitUSet (x : VarId) (n : Nat) (y : VarId) : M Unit :=
do emit "lean::cnstr_set_scalar("; emit x; emit ", "; emitOffset n 0; emit ", "; emit y; emitLn ");"
do emit "lean::cnstr_set_usize("; emit x; emit ", "; emit n; emit ", "; emit y; emitLn ");"
def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) : M Unit :=
do emit "lean::cnstr_set_scalar("; emit x; emit ", "; emitOffset n offset; emit ", "; emit y; emitLn ");"
def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M Unit :=
do
match t with
| IRType.float => throw "floats are not supported yet"
| IRType.uint8 => emit "lean::cnstr_set_uint8"
| IRType.uint16 => emit "lean::cnstr_set_uint16"
| IRType.uint32 => emit "lean::cnstr_set_uint32"
| IRType.uint64 => emit "lean::cnstr_set_uint64"
| _ => throw "invalid instruction";
emit "("; emit x; emit ", "; emitOffset n offset; emit ", "; emit y; emitLn ");"
def emitJmp (j : JoinPointId) (xs : Array Arg) : M Unit :=
do
@ -431,10 +439,18 @@ def emitProj (z : VarId) (i : Nat) (x : VarId) : M Unit :=
do emitLhs z; emit "lean::cnstr_get("; emit x; emit ", "; emit i; emitLn ");"
def emitUProj (z : VarId) (i : Nat) (x : VarId) : M Unit :=
do emitLhs z; emit "lean::cnstr_get_scalar<usize>("; emit x; emit ", sizeof(void*)*"; emit i; emitLn ");"
do emitLhs z; emit "lean::cnstr_get_usize("; emit x; emit ", "; emit i; emitLn ");"
def emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M Unit :=
do emitLhs z; emit "lean::cnstr_get_scalar<"; emit (toCppType t); emit ">("; emit x; emit ", "; emitOffset n offset; emitLn ");"
do emitLhs z;
match t with
| IRType.float => throw "floats are not supported yet"
| IRType.uint8 => emit "lean::cnstr_get_uint8"
| IRType.uint16 => emit "lean::cnstr_get_uint16"
| IRType.uint32 => emit "lean::cnstr_get_uint32"
| IRType.uint64 => emit "lean::cnstr_get_uint64"
| _ => throw "invalid instruction";
emit "("; emit x; emit ", "; emitOffset n offset; emitLn ");"
def toStringArgs (ys : Array Arg) : List String :=
ys.toList.map argToCppString
@ -619,7 +635,7 @@ partial def emitBlock (emitBody : FnBody → M Unit) : FnBody → M Unit
| FnBody.setTag x i b => emitSetTag x i *> emitBlock b
| FnBody.set x i y b => emitSet x i y *> emitBlock b
| FnBody.uset x i y b => emitUSet x i y *> emitBlock b
| FnBody.sset x i o y _ b => emitSSet x i o y *> emitBlock b
| FnBody.sset x i o y t b => emitSSet x i o y t *> emitBlock b
| FnBody.mdata _ b => emitBlock b
| FnBody.ret x => emit "return " *> emitArg x *> emitLn ";"
| FnBody.case _ x alts => emitCase emitBody x alts

36
src/runtime/object.h
View file

@ -581,12 +581,42 @@ inline void cnstr_release(u_obj_arg o, unsigned i) {
dec(*field_ptr);
*field_ptr = box(0);
}
inline usize cnstr_get_usize(b_obj_arg o, unsigned i) {
return obj_data<usize>(o, sizeof(constructor_object) + i*sizeof(void*));
}
inline void cnstr_set_usize(b_obj_arg o, unsigned i, usize v) {
obj_set_data(o, sizeof(constructor_object) + i*sizeof(void*), v);
}
/* Access scalar data at the given offset. */
template<typename T> inline T cnstr_get_scalar(b_obj_arg o, size_t offset) {
inline uint8 cnstr_get_uint8(b_obj_arg o, unsigned offset) {
return obj_data<uint8>(o, sizeof(constructor_object) + offset);
}
inline uint16 cnstr_get_uint16(b_obj_arg o, unsigned offset) {
return obj_data<uint16>(o, sizeof(constructor_object) + offset);
}
inline uint32 cnstr_get_uint32(b_obj_arg o, unsigned offset) {
return obj_data<uint32>(o, sizeof(constructor_object) + offset);
}
inline uint64 cnstr_get_uint64(b_obj_arg o, unsigned offset) {
return obj_data<uint32>(o, sizeof(constructor_object) + offset);
}
inline void cnstr_set_uint8(b_obj_arg o, unsigned offset, uint8 v) {
obj_set_data(o, sizeof(constructor_object) + offset, v);
}
inline void cnstr_set_uint16(b_obj_arg o, unsigned offset, uint16 v) {
obj_set_data(o, sizeof(constructor_object) + offset, v);
}
inline void cnstr_set_uint32(b_obj_arg o, unsigned offset, uint32 v) {
obj_set_data(o, sizeof(constructor_object) + offset, v);
}
inline void cnstr_set_uint64(b_obj_arg o, unsigned offset, uint64 v) {
obj_set_data(o, sizeof(constructor_object) + offset, v);
}
template<typename T> inline T cnstr_get_scalar(b_obj_arg o, unsigned offset) {
return obj_data<T>(o, sizeof(constructor_object) + offset);
}
template<typename T> inline void cnstr_set_scalar(b_obj_arg o, unsigned i, T v) {
obj_set_data(o, sizeof(constructor_object) + i, v);
template<typename T> inline void cnstr_set_scalar(b_obj_arg o, unsigned offset, T v) {
obj_set_data(o, sizeof(constructor_object) + offset, v);
}
inline unsigned obj_tag(b_obj_arg o) { if (is_scalar(o)) return unbox(o); else return cnstr_tag(o); }