summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
authorKathy Gray2015-06-09 16:46:15 +0100
committerKathy Gray2015-06-09 16:46:15 +0100
commit47899c51a2eb637a84585207c462d6512f628ba2 (patch)
tree7462cebada7bd1f30d28da2f66b3f06f9a0de85e /src/lem_interp
parentc2d25d8c763714023412b06caf3e986a46647694 (diff)
Too hasty removal; still used by trans_sail.gen
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp_inter_imp.lem4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 15a1653f..26a44539 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -111,6 +111,10 @@ let intern_ifield_value direction v =
let direction = intern_direction direction in
Interp.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits
+let num_to_bits size kind num =
+(* num_to_bits needed in src_power_get/trans_sail.gen - rather than reengineer the generation, we include a wrapper here *)
+ Interp_interface.bit_list_of_integer size num
+
let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
match d with
| D_increasing -> (i,j) (*This is the case the thread/concurrecny model expects, so no change needed*)