From 5d8c5f14f8794501ebe2453d2fc97d51f16d2273 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Wed, 21 May 2014 17:33:48 +0100
Subject: correct accidental capitalization of Interp in file name

---
 src/lem_interp/Interp_interface.lem | 53 -------------------------------------
 src/lem_interp/interp_interface.lem | 53 +++++++++++++++++++++++++++++++++++++
 2 files changed, 53 insertions(+), 53 deletions(-)
 delete mode 100644 src/lem_interp/Interp_interface.lem
 create mode 100644 src/lem_interp/interp_interface.lem

(limited to 'src')

diff --git a/src/lem_interp/Interp_interface.lem b/src/lem_interp/Interp_interface.lem
deleted file mode 100644
index 00c22bbe..00000000
--- a/src/lem_interp/Interp_interface.lem
+++ /dev/null
@@ -1,53 +0,0 @@
-import Interp
-open import Num
-
-type read_kind = Interp.read_kind
-type write_kind = Interp.write_kind
-type barrier_kind = Interp.barrier_kind
-
-type word8 = nat (* bounded at a byte, for when lem supports it*)
-
-type value = 
-| Bitvector of list bool (* For register accesses *)
-| Bytevector of list word8 (* For memory accesses *)
-| Unknown
-
-type instruction_state = Interp.stack
-type context = Interp.top_level
-
-type slice = (integer * integer)
-
-type reg_name = 
-| Reg of string (*Name of the register, accessing the entire register*)
-| Reg_slice of string * slice (*Name of the register, accessing from the first to second integer of the slice*)
-| Reg_field of string * string * slice (*Name of the register, name of the field of the register accessed, the slice of the field*)
-| Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *)
-
-type outcome =
-| Read_mem of read_kind * value * (value -> instruction_state)
-| Write_mem of write_kind * value * value * (bool -> instruction_state)
-| Barrier of barrier_kind * instruction_state
-| Read_reg of reg_name * (value -> instruction_state) 
-| Write_reg of reg_name * value * instruction_state
-| Nondet_choice of list instruction_state
-| Internal of instruction_state
-| Done
-| Error of string
-
-type event = 
-| E_read_mem of read_kind * value
-| E_write_mem of write_kind * value
-| E_barrier of barrier_kind
-| E_read_reg of reg_name
-| E_write_reg of reg_name
-(*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
-
-
-val build_context : Interp_ast.defs Interp.tannot -> context
-val initial_instruction_state : context -> string -> value -> instruction_state
-
-type interp_mode = <| eager_eval : bool |>
-val interp : interp_mode -> instruction_state -> outcome
-
-val interp_exhaustive : instruction_state -> list event
-
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
new file mode 100644
index 00000000..00c22bbe
--- /dev/null
+++ b/src/lem_interp/interp_interface.lem
@@ -0,0 +1,53 @@
+import Interp
+open import Num
+
+type read_kind = Interp.read_kind
+type write_kind = Interp.write_kind
+type barrier_kind = Interp.barrier_kind
+
+type word8 = nat (* bounded at a byte, for when lem supports it*)
+
+type value = 
+| Bitvector of list bool (* For register accesses *)
+| Bytevector of list word8 (* For memory accesses *)
+| Unknown
+
+type instruction_state = Interp.stack
+type context = Interp.top_level
+
+type slice = (integer * integer)
+
+type reg_name = 
+| Reg of string (*Name of the register, accessing the entire register*)
+| Reg_slice of string * slice (*Name of the register, accessing from the first to second integer of the slice*)
+| Reg_field of string * string * slice (*Name of the register, name of the field of the register accessed, the slice of the field*)
+| Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *)
+
+type outcome =
+| Read_mem of read_kind * value * (value -> instruction_state)
+| Write_mem of write_kind * value * value * (bool -> instruction_state)
+| Barrier of barrier_kind * instruction_state
+| Read_reg of reg_name * (value -> instruction_state) 
+| Write_reg of reg_name * value * instruction_state
+| Nondet_choice of list instruction_state
+| Internal of instruction_state
+| Done
+| Error of string
+
+type event = 
+| E_read_mem of read_kind * value
+| E_write_mem of write_kind * value
+| E_barrier of barrier_kind
+| E_read_reg of reg_name
+| E_write_reg of reg_name
+(*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
+
+
+val build_context : Interp_ast.defs Interp.tannot -> context
+val initial_instruction_state : context -> string -> value -> instruction_state
+
+type interp_mode = <| eager_eval : bool |>
+val interp : interp_mode -> instruction_state -> outcome
+
+val interp_exhaustive : instruction_state -> list event
+
-- 
cgit v1.2.3