diff --git a/library/init/lean/compiler/ir/emitc.lean b/library/init/lean/compiler/ir/emitc.lean index 4f288fdf66..4df6e12cb7 100644 --- a/library/init/lean/compiler/ir/emitc.lean +++ b/library/init/lean/compiler/ir/emitc.lean @@ -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 diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean index 9bea518207..8da6bf8930 100644 --- a/library/init/lean/compiler/ir/emitcpp.lean +++ b/library/init/lean/compiler/ir/emitcpp.lean @@ -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("; 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 diff --git a/src/runtime/object.h b/src/runtime/object.h index 85a81d6ffd..01fa9cb8b2 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -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(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 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(o, sizeof(constructor_object) + offset); +} +inline uint16 cnstr_get_uint16(b_obj_arg o, unsigned offset) { + return obj_data(o, sizeof(constructor_object) + offset); +} +inline uint32 cnstr_get_uint32(b_obj_arg o, unsigned offset) { + return obj_data(o, sizeof(constructor_object) + offset); +} +inline uint64 cnstr_get_uint64(b_obj_arg o, unsigned offset) { + return obj_data(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 inline T cnstr_get_scalar(b_obj_arg o, unsigned offset) { return obj_data(o, sizeof(constructor_object) + offset); } -template inline void cnstr_set_scalar(b_obj_arg o, unsigned i, T v) { - obj_set_data(o, sizeof(constructor_object) + i, v); +template 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); }