diff options
| author | Peter Sewell | 2014-11-23 13:53:08 +0000 |
|---|---|---|
| committer | Peter Sewell | 2014-11-23 13:53:08 +0000 |
| commit | 022bea5d40c80b006f4784a85c7351eb2b28545a (patch) | |
| tree | e41ae449795ba8908e782304a377047f51452f8f /src | |
| parent | 344003fe4c5eb283e1ac8e09e6f9c8d478dc89dc (diff) | |
wib
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 21 | ||||
| -rw-r--r-- | src/lem_interp/printing_functions.ml | 3 |
2 files changed, 22 insertions, 2 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 02e7d2e2..3519a690 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -186,7 +186,7 @@ type register_value = <| rv_bits: list bit_lifted; rv_dir: direction; rv_start: type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *) -type instruction_field_value = (*SHOULD BE JUST*) list bit (*register_value *) +type instruction_field_value = list bit type byte = Byte of list bit (* of length 8 *) @@ -203,6 +203,25 @@ type address = Address of list byte (* of length 8 *) type opcode = Opcode of list byte (* of length 4 *) (** typeclass instantiations *) +(* +let bitCompare (b1:bit) (b2:bit) = + match (b1,b2) with + | (Bitc_zero, Bitc_zero) -> EQ + | (Bitc_one, Bitc_one) -> EQ + | (Bitc_zero, _) -> LT + | (_,_) -> GT + end + +let bit_liftedCompare (bl1:bit) (bl2:bit) = + match (bl1,bl2) with + | (Bitl_zero, Bitl_zero) -> EQ + | (Bitl_one, Bitl_one) -> EQ +... + end +*) + +let addressCompare = defaultCompare + instance (Ord register_value) let compare = defaultCompare diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index 73feb8ac..22aea37e 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -306,7 +306,8 @@ let rec instr_parms_to_string ps = let pad n s = if String.length s < n then s ^ String.make (n-String.length s) ' ' else s let instruction_to_string (name, parms, base_effects) = - (pad 5 (String.lowercase name)) ^ " " ^ instr_parms_to_string parms + raise (Failure "TODO instruction_to_string") +(* (pad 5 (String.lowercase name)) ^ " " ^ instr_parms_to_string parms *) let print_backtrace_compact printer stack = List.iter (fun (e,(env,mem)) -> print_exp printer env e) (compact_stack stack) let print_continuation printer stack = let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env e |