import Interp
import Interp_lib
open import Interp_ast
open import Interp_interface
open import Pervasives

val intern_value : value -> Interp.value
val extern_value : interp_mode -> bool -> Interp.value -> (value * maybe (list reg_name))
val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name

let build_context defs = match Interp.to_top_env defs with (_,context) -> context end

let make_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values |>;;
let tracking_dependencies mode = mode.Interp.track_values

let to_bits l = (List.map (fun b -> match b with
                               | false -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) 
			       | true ->  (Interp.V_lit (L_aux L_one Interp_ast.Unknown)) end) l)
let from_bits l = (List.map (fun b -> match b with
                                 | Interp.V_lit (L_aux L_zero _) -> false
				 | _ -> true end) l) 
let rec to_bytes l = match (List.reverse l) with
  | [] -> []
  | (a::b::c::d::e::f::g::h::rest) ->
    (natFromInteger(integerFromBoolList (false,[a;b;c;d;e;f;g;h])))::(to_bytes rest)
end
		   
let intern_value v = match v with
  | Bitvector bs inc fst   -> Interp.V_vector fst inc  (to_bits bs)
  | Bytevector bys inc fst -> Interp.V_vector fst inc 
    (to_bits (List.reverse
		(List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys))))
  | Unknown -> Interp.V_unknown
  | _ -> Interp.V_unknown
end

let extern_reg r slice = match (r,slice) with
  | (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x
  | (Interp.Reg (Id_aux (Id x) _) _,Just(i1,i2)) -> Reg_slice x (i1,i2)
  | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field x y (i,i)
end

let extern_value mode for_mem v = match v with
  | Interp.V_vector fst inc bits ->
    if for_mem 
    then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, Nothing)
    else (Bitvector (from_bits bits) inc fst, Nothing)
  | Interp.V_track (Interp.V_vector fst inc bits) regs -> 
    if for_mem
    then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, 
          if (mode.Interp.track_values) 
          then (Just (List.map (fun r -> extern_reg r Nothing) regs))
          else Nothing)
    else (Bitvector (from_bits bits) inc fst, Nothing)
  | _ -> (Unknown,Nothing)
end

let initial_instruction_state top_level main args = 
  let e_args = match args with
    | [] -> [E_aux (E_lit (L_aux L_unit Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)]
    | [arg] -> let (e,_) = Interp.to_exp (make_mode true false) Interp.eenv (intern_value arg) in [e]
    | args -> List.map fst (List.map (Interp.to_exp (make_mode true false) Interp.eenv)
			      (List.map intern_value args)) end in
  Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing)) 
    top_level Interp.eenv Interp.emem Interp.Top

(*For now, append to this list to add more external functions; should add to the mode record for more perhaps *)
let external_functions = 
  Interp_lib.function_map

type mem_function = (string * 
                     (maybe read_kind * maybe write_kind * (interp_mode -> Interp.value -> (value * (maybe (list reg_name))))))

(*List of memory functions; needs to be expanded with all of the memory functions needed for PPCMem.
  Should probably be expanded into a parameter to mode as with above
*)
let memory_functions =
  [ ("MEMr", (Just(Read_plain), Nothing, 
	     (fun mode v -> match v with
	       | Interp.V_tuple [location;length] ->
		 match length with
		   | Interp.V_lit (L_aux (L_num len) _) ->
		     let (v,regs) = extern_value mode true location in
		     (v,len,regs) end end)));
    ("MEMw", (Nothing, Just(Write_plain), 
	      (fun mode v -> match v with
		| Interp.V_tuple [location;length] ->
		  match length with
		    | Interp.V_lit (L_aux (L_num len) _) ->
		      let (v,regs) = extern_value mode true location in
		      (v,len,regs) end end)));
  ]

let rec interp_to_outcome mode thunk = 
  match thunk () with
  | Interp.Value _ -> Done
  | Interp.Error l msg -> Error msg (*Todo, add the l information the string format*)
  | Interp.Action a next_state ->
    match a with
    | Interp.Read_reg reg_form slice -> 
      Read_reg (extern_reg reg_form slice) 
               (fun v -> 
                 let v = (intern_value v) in
                 let v = if mode.Interp.track_values then (Interp.V_track v [reg_form]) else v in 
                 Interp.add_answer_to_stack next_state v)
    | Interp.Write_reg reg_form slice value -> 
      let (v,_) = extern_value mode false value in Write_reg (extern_reg reg_form slice) v next_state
    | Interp.Read_mem (Id_aux (Id i) _) value slice ->
      match List.lookup i memory_functions with
      | (Just (Just read_k,_,f)) -> 
        let (location, length, tracking) = (f mode value) in
        Read_mem read_k location length tracking (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
      | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
      end
    | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
      match List.lookup i memory_functions with
      | (Just (_,Just write_k,f)) -> 
        let (location, length, tracking) = (f mode loc_val) in
        let (value, val_tracking) = (extern_value mode true write_val) in
        Write_mem write_k location length tracking value val_tracking (fun b -> next_state) 
      | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
      end 
    | Interp.Barrier (Id_aux (Id i) _) lval ->
      Barrier Sync next_state (* TODO set up some barrier functions and see if the value would be anything needed *)
    | Interp.Nondet exps -> 
      let nondet_states = List.map (Interp.set_in_context next_state) exps in
      Nondet_choice nondet_states next_state      
    | Interp.Call_extern i value -> 
      match List.lookup i external_functions with
      | Nothing -> Error ("External function not available " ^ i)
      | Just f  -> 
        if (mode.Interp.eager_eval)
        then interp_to_outcome mode (fun _ -> Interp.resume mode next_state (Just (f value))) 
        else let new_v = f value in
             Internal (Just i) 
                      (Just (fun _ -> Interp.string_of_value value))
                      (Interp.add_answer_to_stack next_state new_v)
      end
    | Interp.Step l Nothing Nothing -> Internal Nothing Nothing next_state 
    | Interp.Step l (Just name) Nothing -> Internal (Just name) Nothing next_state
    | Interp.Step l (Just name) (Just value) ->
      Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) next_state
    end 
  end 

let interp mode i_state = interp_to_outcome mode (fun _ -> Interp.resume mode i_state Nothing)

let rec ie_loop mode i_state = 
  match (interp mode i_state) with
    | Done -> []
    | Error msg -> [E_error msg]
    | Read_reg reg i_state_fun -> 
      (E_read_reg reg)::(ie_loop mode (i_state_fun Unknown))
    | Write_reg reg value i_state->
      (E_write_reg reg value)::(ie_loop mode i_state)
    | Read_mem read_k loc length tracking i_state_fun ->
      (E_read_mem read_k loc length tracking)::(ie_loop mode (i_state_fun Unknown))
    | Write_mem write_k loc length l_track value v_track i_state_fun ->
      (E_write_mem write_k loc length l_track value v_track)::(ie_loop mode (i_state_fun true))
    | Internal _ _ next -> (ie_loop mode next)
     end ;;
  
let interp_exhaustive i_state = 
  let mode = make_mode true false in
  ie_loop mode i_state

let rec rr_ie_loop mode i_state = 
  match (interp mode i_state) with
    | Done -> ([],Done)
    | Error msg -> ([E_error msg], Error msg)
    | Read_reg reg i_state_fun -> ([], Read_reg reg i_state_fun)
    | Write_reg reg value i_state->
      let (events,outcome) = (rr_ie_loop mode i_state) in
      (((E_write_reg reg value)::events), outcome)
    | Read_mem read_k loc length tracking i_state_fun ->
      let (events,outcome) = (rr_ie_loop mode (i_state_fun Unknown)) in 
      (((E_read_mem read_k loc length tracking)::events),outcome)
    | Write_mem write_k loc length l_track value v_track i_state_fun ->
      let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
      (((E_write_mem write_k loc length l_track value v_track)::events),outcome)
    | Internal _ _ next -> (rr_ie_loop mode next)
     end ;;

let rr_interp_exhaustive mode i_state events = 
  let (events',outcome) = rr_ie_loop mode i_state in ((events ++ events'),outcome)