diff options
| author | Peter Sewell | 2014-11-05 00:16:35 +0000 |
|---|---|---|
| committer | Peter Sewell | 2014-11-05 00:16:35 +0000 |
| commit | 43df2c7fe73227c97dc933a2eda238167e4c74a4 (patch) | |
| tree | 3bbb9e6ffc392ebb69c449b54dba0451fcdc08d8 /src | |
| parent | 7b6880656c7e7f60abca0d31621cc8de34e72152 (diff) | |
fix(?) a Big_int/int type error wrt trans_sail
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 2 |
2 files changed, 2 insertions, 2 deletions
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 |