From 43df2c7fe73227c97dc933a2eda238167e4c74a4 Mon Sep 17 00:00:00 2001
From: Peter Sewell
Date: Wed, 5 Nov 2014 00:16:35 +0000
Subject: fix(?) a Big_int/int type error wrt trans_sail

---
 src/lem_interp/interp_inter_imp.lem | 2 +-
 src/lem_interp/interp_interface.lem | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 75dba6fc..5f89a1d8 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -257,7 +257,7 @@ end
 
 let migrate_typ = function
   | Instruction_extractor.IBit -> Bit
-  | Instruction_extractor.IBitvector len -> Bvector len
+  | Instruction_extractor.IBitvector len -> Bvector (match len with Nothing -> Nothing | Just i -> Just (intFromInteger i) end) 
   | Instruction_extractor.IOther -> Other
 end
 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index ca0ab9f3..7c675c75 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -109,7 +109,7 @@ val initial_instruction_state : context -> string -> list value -> instruction_s
 type instr_parm_typ = 
   | Bit (*A single bit, represented as a one element Bitvector as a value*)
   | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
-  | Bvector of maybe integer (* A bitvector type, with length when statically known *)
+  | Bvector of maybe int (* A bitvector type, with length when statically known *)
 
 (*A representation of the AST node for each instruction in the spec, with concrete values from this call, and the potential static effects from the funcl clause for this instruction 
 Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
-- 
cgit v1.2.3