(* PS NOTES FOR KATHY:

pls also change:  

  decode_to_istate
  decode_to_instruction 

to take an opcode as defined above, instead of a value 

and change 

*)


open import Sail_impl_base
import Interp
open import Interp_ast
open import Pervasives
open import Num

open import Assert_extra

type interpreter_state = Interp.stack (*Deem abstract*)
(* Will come from a .lem file generated by Sail, bound to a 'defs' identifier *)
type specification = Interp_ast.defs Interp.tannot (*Deem abstract*)
type interpreter_mode = Interp.interp_mode (*Deem abstract*)
type interp_mode = <| internal_mode: interpreter_mode; endian: end_flag |>
val make_mode : (*eager*) bool -> (*tracking*) bool -> end_flag -> interp_mode
val tracking_dependencies : interp_mode -> bool



(*Map between external functions as preceived from a Sail spec and the actual implementation of the function *)
type external_functions = list (string * (Interp.value -> Interp.value))

(*Maps between the memory functions as preceived from a Sail spec and the values needed for actions in the memory model*)
type barriers = list (string * barrier_kind)
type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name))
type optional_memory_transformer = interp_mode -> Interp.value -> maybe memory_value
type memory_read = MR of read_kind * memory_parameter_transformer
type memory_reads  = list (string * memory_read)
type memory_write_ea = MEA of write_kind * memory_parameter_transformer
type memory_write_eas = list (string * memory_write_ea)
type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state))
and memory_writes = list (string * memory_write)
and memory_write_val = MV of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state))
and memory_write_vals = list (string * memory_write_val)

(* Definition information needed to run an instruction *)
and context =
    Context of Interp.top_level * direction * 
	memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * external_functions

(* An instruction in flight *)
and instruction_state = IState of interpreter_state * context


type outcome =
(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values,
   integer is size to read, followed by registers that were used in computing that size *)
| Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) *  (memory_value -> instruction_state)
(* Request to write memory, first value and dependent registers is location, second is the value to write *)
| Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state)
(* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *)
| Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * instruction_state
(* Request to write memory at last signaled address. Memory value should be 8* the size given in ea signal *)
| Write_memv of maybe address_lifted * memory_value * maybe (list reg_name) * (bool -> instruction_state)
(* Request a memory barrier *)
| Barrier of barrier_kind * instruction_state
(* Tell the system to dynamically recalculate dependency footprint *)
| Footprint of instruction_state
(* Request to read register, will track dependency when mode.track_values *)
| Read_reg of reg_name * (register_value -> instruction_state) 
(* Request to write register *)
| Write_reg of reg_name * register_value * instruction_state
(* List of instruciton states to be run in parrallel, any order permitted *)
| Nondet_choice of list instruction_state * instruction_state
(* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler 
   The non-optional instruction_state is what we would be doing if we're not escaping. This is for exhaustive interp *)
| Escape of maybe instruction_state * instruction_state
(*Result of a failed assert with possible error message to report*)
| Fail of maybe string
(* Stop for incremental stepping, function can be used to display function call data *)
| Internal of maybe string * maybe (unit -> string) * instruction_state
(* Analysis can lead to non_deterministic evaluation, represented with this outcome *)
(*Note: this should not be externally visible *)
| Analysis_non_det of list instruction_state * instruction_state
(*Completed interpreter*)
| Done
(*Interpreter error*)
| Error of string

type event = 
| E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
| E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
| E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name)
| E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name)
| E_barrier of barrier_kind
| E_footprint 
| E_read_reg of reg_name
| E_write_reg of reg_name * register_value
| E_escape
| E_error of string 


let ~{ocaml} eventCompare e1 e2 = 
  match (e1,e2) with
  | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) ->
     compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
  | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> 
    compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
  | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) ->
    compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2))
  | (E_write_memv _ mv1 tr1, E_write_memv _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
  | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2
  | (E_read_reg r1, E_read_reg r2) -> compare r1 r2
  | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2)
  | (E_error s1, E_error s2) -> compare s1 s2
  | (E_escape,E_escape) -> EQ
  | (E_read_mem _ _ _ _, _) -> LT
  | (E_write_mem _ _ _ _ _ _, _) -> LT
  | (E_write_ea _ _ _ _, _) -> LT
  | (E_write_memv _ _ _, _) -> LT
  | (E_barrier _, _) -> LT
  | (E_read_reg _, _) -> LT
  | (E_write_reg _ _, _) -> LT
  | _ -> GT
  end
let inline {ocaml} eventCompare = defaultCompare

let ~{ocaml} eventLess b1 b2      = eventCompare b1 b2 =  LT
let ~{ocaml} eventLessEq b1 b2    = eventCompare b1 b2 <> GT
let ~{ocaml} eventGreater b1 b2   = eventCompare b1 b2 =  GT
let ~{ocaml} eventGreaterEq b1 b2 = eventCompare b1 b2 <> LT

let inline {ocaml} eventLess      = defaultLess
let inline {ocaml} eventLessEq    = defaultLessEq
let inline {ocaml} eventGreater   = defaultGreater
let inline {ocaml} eventGreaterEq = defaultGreaterEq

instance (Ord event)
  let compare = eventCompare
  let (<)  = eventLess
  let (<=) = eventLessEq
  let (>)  = eventGreater
  let (>=) = eventGreaterEq
end

instance (SetType event)
  let setElemCompare = compare
end


(* Functions to build up the initial state for interpretation *)
val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context 
val initial_instruction_state : context -> string -> list register_value -> instruction_state 
  (* string is a function name, list of value are the parameters to that function *)

type instruction_or_decode_error =
  | IDE_instr of instruction * Interp.value
  | IDE_decode_error of decode_error

(** propose to remove the following type and use the above instead *)
type i_state_or_error =
  | Instr of instruction * instruction_state
  | Decode_error of decode_error


(** PS:I agree. propose to remove this: Function to decode an instruction and build the state to run it*)
val decode_to_istate : context -> maybe (list (reg_name * register_value)) -> opcode -> i_state_or_error

(** propose to add this, and then use instruction_to_istate on the result: Function to decode an instruction and build the state to run it*)
(** PS made a placeholder in interp_inter_imp.lem, but it just uses decode_to_istate and throws away the istate; surely it's easy to just do what's necessary to get the instruction.   This sort-of works, but it crashes on ioid 10 after 167 steps - maybe instruction_to_istate (which I wasn't using directly before) isn't quite right? *)
val decode_to_instruction : context -> maybe (list (reg_name * register_value))-> opcode -> instruction_or_decode_error

(*Function to generate the state to run from an instruction form; is always an Instr*)
val instruction_to_istate : context -> instruction -> instruction_state (*i_state_or_error*)

(* Slice a register value into a smaller vector, starting at first number (wrt the indices of the register value, not raw positions in its list of bits) and going to second (inclusive) according to order. *)
val slice_reg_value : register_value -> nat -> nat -> register_value
(*Create a new register value where the contents of nat to nat are replaced by the second register_value *)  
val update_reg_value_slice : reg_name -> register_value -> nat -> nat -> register_value -> register_value


(* Big step of the interpreter, to the next request for an external action *)
(* When interp_mode has eager_eval false, interpreter is (close to) small step *)
val interp : interp_mode -> instruction_state -> outcome

(* Run the interpreter without external interaction, feeding in Unknown on all reads except for those register values provided *)
val interp_exhaustive : maybe (list (reg_name * register_value)) -> instruction_state -> list event

(* As above, but will request register reads: outcome will only be rreg, done, or error *)
val rr_interp_exhaustive : interp_mode -> instruction_state -> list event -> (outcome * (list event)) 

val translate_address :
  context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address
  -> maybe address * maybe (list event)

                      
val instruction_analysis :
  context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat)))
  -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind)


val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit