move interpreter-specific types from Sail_impl_base to Interp_interface

1 files changed, 0 insertions, 102 deletions

diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 7ede9aa6..88e197d5 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -1,5 +1,4 @@
 open import Pervasives_extra
-open import Interp_ast (* this can go away *)
             
 (* maybe isn't a member of type Ord - this should be in the Lem standard library*)
 instance forall 'a. Ord 'a => (Ord (maybe 'a))
@@ -794,61 +793,6 @@ instance (Ord barrier_kind)
   let (>=) = barrier_kindGreaterEq
 end
 
-
-
-
-(*Type representint the constructor parameters in instruction, other is a type not representable externally*)
-type instr_parm_typ = 
-  | Bit (*A single bit, represented as a one element Bitvector as a value*)
-  | Bvector of maybe nat (* A bitvector type, with length when statically known *)
-  | Range of maybe nat (*Internally represented as a number, externally as a bitvector of length nat *)
-  | Enum of string * nat (*Internally represented as either a number or constructor, externally as a bitvector*)
-  | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
-
-let {coq} instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
-  | (Bit,Bit) -> true
-  | (Bvector i1,Bvector i2) -> i1 = i2
-  | (Range i1,Range i2) -> i1 = i2
-  | (Enum s1 i1,Enum s2 i2) -> s1 = s2 && i1 = i2
-  | (Other,Other) -> true
-  | _ -> false
-end
-let inline ~{coq} instr_parm_typEqual = unsafe_structural_equality
-
-let {coq} instr_parm_typInequal ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
-let inline ~{coq} instr_parm_typInequal = unsafe_structural_inequality
-
-instance (Eq instr_parm_typ) 
-  let (=) = instr_parm_typEqual
-  let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
-end 
-
-let instr_parm_typShow ip = match ip with
-  | Bit -> "Bit"
-  | Bvector i -> "Bvector " ^ show i
-  | Range i -> "Range " ^ show i
-  | Enum s i -> "Enum " ^ s ^ " " ^ show i
-  | Other -> "Other"
- end
-
-instance (Show instr_parm_typ)
-let show = instr_parm_typShow
-end
-
-(*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
-*)
-type instruction = (string * list (string * instr_parm_typ * instruction_field_value))
-
-let {coq} instructionEqual i1 i2 = match (i1,i2) with
-  | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2
-end
-let inline ~{coq} instructionEqual = unsafe_structural_equality
-
-let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2)
-let inline ~{coq} instructionInequal = unsafe_structural_inequality
-
 (** operations and coercions on basic values *)
 
 val word8_to_bitls : word8 -> list bit_lifted
@@ -1380,49 +1324,3 @@ end
 instance (Show dia)
   let show = stringFromDia
 end
-
-
-type v_kind = Bitv | Bytev
-
-type decode_error = 
-  | Unsupported_instruction_error of instruction
-  | Not_an_instruction_error of opcode
-  | Internal_error of string
-
-
-let decode_error_compare e1 e2 =
-  match (e1, e2) with
-  | (Unsupported_instruction_error i1, Unsupported_instruction_error i2)
-      -> defaultCompare i1 i2
-  | (Unsupported_instruction_error _, _) -> LT
-  | (_, Unsupported_instruction_error _) -> GT
-
-  | (Not_an_instruction_error o1, Not_an_instruction_error o2) -> defaultCompare o1 o2
-  | (Not_an_instruction_error _, _) -> LT
-  | (_, Not_an_instruction_error _) -> GT
-
-  | (Internal_error s1, Internal_error s2) -> compare s1 s2
-  (* | (Internal_error _, _) -> LT *)
-  (* | (_, Internal_error _) -> GT *)
-  end
-
-let decode_error_less e1 e2       = decode_error_compare e1 e2 =  LT
-let decode_error_less_eq e1 e2    = decode_error_compare e1 e2 <> GT
-let decode_error_greater e1 e2    = decode_error_compare e1 e2 =  GT
-let decode_error_greater_eq e1 e2 = decode_error_compare e1 e2 <> LT
-
-instance (Ord decode_error)
-  let compare = decode_error_compare
-  let (<)  = decode_error_less
-  let (<=) = decode_error_less_eq
-  let (>)  = decode_error_greater
-  let (>=) = decode_error_greater_eq
-end
-
-let decode_error_equal e1 e2 = (decode_error_compare e1 e2) = EQ
-let decode_error_inequal e1 e2 = not (decode_error_equal e1 e2)
-
-instance  (Eq decode_error)
-  let (=)  = decode_error_equal
-  let (<>) = decode_error_inequal
-end