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 : bool -> Interp.value -> value
val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name

let build_context defs = Interp.to_top_env defs

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 l with
  | [] -> []
  | (a::b::c::d::e::f::g::h::rest) ->
    (natFromInteger(integerFromBoolList (true,[a;b;c;d;e;f;g;h])))::(to_bytes rest)
end
		   
let intern_value v = match v with
  | Bitvector bs -> Interp.V_vector 0 true  (to_bits bs)
  | Bytevector bys -> Interp.V_vector 0 true (to_bits (List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys)))
  | Unknown -> Interp.V_unknown
end

let extern_value for_mem v = match v with
  | Interp.V_vector _ true bits ->
    if for_mem 
    then Bytevector (to_bytes (from_bits bits))
    else Bitvector (from_bits bits)
  | _ -> 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 initial_instruction_state top_level main arg = 
  let (e_arg,env) = Interp.to_exp <| Interp.eager_eval = true; Interp.track_values = false |> Interp.eenv (intern_value arg) in
  Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [e_arg]) (Interp_ast.Unknown, Nothing)) top_level Interp.eenv Interp.emem

(*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.value -> value))

(*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 =
  [ ("MEM", (Just(Interp.Read_plain), Just(Interp.Write_plain), (fun v -> extern_value true v)));
  ]

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 -> Interp.add_answer_to_stack next_state (intern_value v))
    | Interp.Write_reg reg_form slice value -> Write_reg (extern_reg reg_form slice) (extern_value false value) next_state
    | Interp.Read_mem (Id_aux (Id i) _) value slice ->
      match List.lookup i memory_functions with
      | (Just (Just read_k,_,f)) -> Read_mem read_k (f value) (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)) -> Write_mem write_k (f loc_val) (extern_value true write_val) (fun b -> next_state) 
      | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
      end 
    | Interp.Barrier (Id_aux (Id i) _) lval ->
      Barrier Interp.Plain 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  -> interp_to_outcome mode (fun _ -> Interp.resume mode next_state (Just (f value))) end
    | Interp.Step l _ _ -> Internal 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 i_state_fun ->
      (E_read_mem read_k loc)::(ie_loop mode (i_state_fun Unknown))
    | Write_mem write_k loc value i_state_fun ->
      (E_write_mem write_k loc value)::(ie_loop mode (i_state_fun true))
    | Internal next -> (ie_loop mode next)
     end ;;
  
let interp_exhaustive i_state = 
  let mode = <| Interp.eager_eval = true; Interp.track_values = false; |> in
  ie_loop mode i_state