import Interp
import Interp_lib
import Instruction_extractor
open import Interp_ast
open import Interp_interface
open import Pervasives
open import Assert_extra


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 l with
  | [] -> []
  | (a::b::c::d::e::f::g::h::rest) ->
    (natFromInteger(integerFromBoolList (false,(List.reverse([a;b;c;d;e;f;g;h])))))::(to_bytes rest)
end
		   
let intern_value v = match v with
  | Bitvector [true] _ _ -> Interp.V_lit (L_aux L_one Interp_ast.Unknown)
  | Bitvector [false] _ _ -> Interp.V_lit (L_aux L_zero Interp_ast.Unknown)
  | Bitvector bs inc fst   -> Interp.V_vector fst inc  (to_bits bs)
  | Bytevector bys -> Interp.V_vector 0 true 
    (List.concat (List.map (fun by -> 
      match Interp_lib.to_vec_inc (Interp.V_tuple([Interp.V_lit(L_aux (L_num 8) Interp_ast.Unknown);
						   Interp.V_lit(L_aux (L_num (integerFromNat by)) Interp_ast.Unknown)]))
      with
	| Interp.V_vector _ _ bits -> bits 
	| _ -> [] end) bys))
  | Unknown -> Interp.V_unknown
  | _ -> Interp.V_unknown
end

let num_to_bits size kind num =
  match kind with
    | Bitv -> Bitvector (match (Interp_lib.to_vec_inc (Interp.V_tuple([Interp.V_lit(L_aux (L_num size) Interp_ast.Unknown);
								       Interp.V_lit(L_aux (L_num (integerFromNat num))
										          Interp_ast.Unknown)]))) with
	| Interp.V_vector _ _ bits -> from_bits bits end) true 0
    | Bytev -> 
      Bytevector (match (Interp_lib.to_vec_inc (Interp.V_tuple([Interp.V_lit(L_aux (L_num size) Interp_ast.Unknown);
								Interp.V_lit(L_aux (L_num (integerFromNat num))
									       Interp_ast.Unknown)]))) with
	| Interp.V_vector _ _ bits -> (to_bytes (from_bits bits)) end)
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 y x (i,i)
end

let rec extern_value mode for_mem v = match v with
  | Interp.V_track v regs -> 
    let (external_v,_) = extern_value mode for_mem v in
    (external_v,
     if (for_mem && mode.Interp.track_values)
     then (Just (List.map (fun r -> extern_reg r Nothing) regs))
     else Nothing)
  | Interp.V_vector fst inc bits ->
    if for_mem 
    then (Bytevector (to_bytes (from_bits bits)), Nothing)
    else (Bitvector (from_bits bits) inc fst, Nothing)
  | Interp.V_lit (L_aux L_zero _) -> 
    if for_mem
    then (Bytevector [0],Nothing)
    else (Bitvector [false] true 0, Nothing)
  | Interp.V_lit (L_aux L_false _) ->
    if for_mem
    then (Bytevector [0],Nothing)
    else (Bitvector [false] true 0, Nothing)
  | Interp.V_lit (L_aux L_one _) -> 
    if for_mem
    then (Bytevector [1],Nothing)
    else (Bitvector [true] true 0, Nothing)
  | Interp.V_lit (L_aux L_true _) ->
    if for_mem
    then (Bytevector [1],Nothing)
    else (Bitvector [true] true 0, Nothing)
  | _ -> (Unknown,Nothing)
end 

let rec slice_value bits start stop = 
  match bits with
    | Bitvector bools inc fst -> 
      Bitvector (Interp.from_n_to_n (if inc then (start - fst) else (fst - start))
                                    (if inc then (stop - fst) else (fst - stop)) bools)
                 inc
                 (if inc then start else ((stop - start) + 1))                
    | Bytevector bytes -> 
      Bytevector (Interp.from_n_to_n start stop bytes)
    | Unknown -> Unknown
end

let append_value left right =
  match (left,right) with
    | (Bitvector bools1 inc fst, Bitvector bools2 _ _) -> Bitvector (bools1++bools2) inc fst
    | (Bytevector bytes1, Bytevector bytes2) -> Bytevector (bytes1++bytes2)
    | ((Bitvector _ _ _ as bit),(Bytevector _ as byte)) ->
      (match (intern_value bit,intern_value byte) with
	| (Interp.V_vector a b bits1,Interp.V_vector _ _ bits2) -> 
	  (fst (extern_value (make_mode true false) false (Interp.V_vector a b (bits1++bits2))))
	| _ -> Unknown end)
    | ((Bytevector _ as byte),(Bitvector _ _ _ as bit)) ->
      (match (intern_value byte,intern_value bit) with
	| (Interp.V_vector a b bits1,Interp.V_vector _ _ bits2) -> 
	  (fst (extern_value (make_mode true false) true (Interp.V_vector a b (bits1++bits2))))
	| _ -> Unknown end)
    | _ -> Unknown 
end

let add_to_address value num =
  match value with
    | Unknown -> Unknown
    | Bitvector _ _ _ -> 
      fst(extern_value (make_mode true false) false 
	             (Interp_lib.arith_op_vec_range (+) 1 
			(Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
    | Bytevector _ ->
      fst(extern_value (make_mode true false) true 
	             (Interp_lib.arith_op_vec_range (+) 1 
			(Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
end


let coerce_Bytevector_of_Bitvector (v: value) : value =
  match v with
  | Bitvector bs b i -> Bytevector (to_bytes bs)
  | _ -> Assert_extra.failwith "coerce_Bytevector_of_Bitvector given non-Bitvector"
  end

let coerce_Bitvector_of_Bytevector (v: value) : value =
  match v with
  | Bytevector ws -> Bitvector 
        (List.concatMap 
           (fun w -> 
             List.reverse 
               (boolListFrombitSeq 8 (bitSeqFromNat w)))
            ws)
        true
        0
  | _ -> Assert_extra.failwith "coerce_Bitvector_of_Bitvector given non-Bytevector"
  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) 
		   | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
		     let (v,loc_regs) = extern_value mode true location in
		     match loc_regs with
		       | Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
		       | Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
	      end end end)));
    ("MEMr_reserve", (Just(Read_reserve),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) 
			    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
			      let (v,loc_regs) = extern_value mode true location in
			      match loc_regs with
				| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
				| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
		       end 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)
		    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
		      let (v,loc_regs) = extern_value mode true location in
		      match loc_regs with
			| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
			| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
	       end end end)));
    ("MEMw_conditional", (Nothing, Just(Write_conditional), 
	      (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)
		    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
		      let (v,loc_regs) = extern_value mode true location in
		      match loc_regs with
			| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
			| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
	      end end end)));
  ]

let rec interp_to_value_helper arg instr thunk = 
  match thunk() with
    | Interp.Value value -> (Just value,Nothing)
    | Interp.Error l msg -> (Nothing, Just (Internal_error msg))
    | Interp.Action (Interp.Call_extern i value) stack ->
      match List.lookup i external_functions with
	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
	| Just f  -> 
          interp_to_value_helper arg instr (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
      end 
    | Interp.Action (Interp.Exit (E_aux e _)) _ ->
      match e with
	| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error instr))
	| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just (Not_an_instruction_error arg))
      end 
    | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
end

let rec find_instruction i = function
  | [] -> Nothing
  | Instruction_extractor.Skipped::instrs -> find_instruction i instrs
  | ((Instruction_extractor.Instr_form name parms effects) as instr)::instrs ->
      if i = name
      then Just instr
      else find_instruction i instrs
end

let migrate_typ = function
  | Instruction_extractor.IBit -> Bit
  | Instruction_extractor.IBitvector len -> Bvector (match len with Nothing -> Nothing | Just i -> Just (intFromInteger i) end) 
  | Instruction_extractor.IOther -> Other
end

let decode_to_istate top_level value = 
  let mode = make_mode true false in
  let (arg,_) = Interp.to_exp mode Interp.eenv (intern_value value) in
  let (Interp.Env _ instructions _ _ _ _ _) = top_level in
  let (instr_decoded,error) = interp_to_value_helper value ("",[],[])
    (fun _ -> Interp.resume 
      (make_mode true false) 
      (Interp.Thunk_frame 
	 (E_aux (E_app (Id_aux (Id "decode") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) 
	 top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
  match (instr_decoded,error) with
    | (Just instr, _) -> 
      let instr_external = match instr with
	| Interp.V_ctor (Id_aux (Id i) _) _ parm ->
	  match (find_instruction i instructions) with
	    | Just(Instruction_extractor.Instr_form name parms effects) -> 
	      match (parm,parms) with
		| (Interp.V_lit (L_aux L_unit _),[]) -> (name, [], effects)
		| (value,[(p_name,ie_typ)]) -> (name, [(p_name,(migrate_typ ie_typ),fst(extern_value mode false value))], effects)
		| (Interp.V_tuple vals,parms) -> 
		  (name, (Interp.map2 (fun value (p_name,ie_typ) -> (p_name,(migrate_typ ie_typ),fst(extern_value mode false value))) vals parms), effects)
          end end end in 
      let (arg,_) = Interp.to_exp mode Interp.eenv instr in
      let (instr_decoded,error) = interp_to_value_helper value instr_external
	(fun _ -> Interp.resume 
	 (make_mode true false) 
	 (Interp.Thunk_frame 
	 (E_aux (E_app (Id_aux (Id "supported_instructions") Interp_ast.Unknown) [arg]) 
	    (Interp_ast.Unknown, Nothing)) 
	 top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
      match (instr_decoded,error) with
	| (Just instr,_) ->
	  let (arg,_) = Interp.to_exp mode Interp.eenv instr in
	  Instr instr_external
	    (Interp.Thunk_frame
		   (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
		   top_level Interp.eenv Interp.emem Interp.Top)
	| (Nothing, Just err) -> Decode_error err
      end 
    | (Nothing, Just err) -> Decode_error err
end


let decode_to_instruction top_level value = 
  match decode_to_istate top_level value with
  | Instr inst is -> IDE_instr inst
  | Decode_error de -> IDE_decode_error de
  end


let instruction_to_istate top_level ((name, parms, _) as instr) = 
  let mode = make_mode true false in
  let get_value (name,typ,v) = let (e,_) = Interp.to_exp mode Interp.eenv (intern_value v) in e in
(*  (Instr instr*)
    (Interp.Thunk_frame
       (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) 
		 [(E_aux (E_app (Id_aux (Id name) Interp_ast.Unknown) (List.map get_value parms))
		        (Interp_ast.Unknown,Interp.ctor_annot (T_id "ast")) (*This type shouldn't be hard-coded*))])
	      (Interp_ast.Unknown,Nothing))
       top_level Interp.eenv Interp.emem Interp.Top) (*)*)

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, v_tracking) = (extern_value mode true write_val) in
        Write_mem write_k location length tracking value v_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.string_of_value new_v)))
                      (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)

(*TODO: Only find exact matches, need to look for field/slice sub pieces*)
let rec find_reg_name reg = function
  | [] -> Nothing
  | (reg_name,v)::registers ->
    match (reg,reg_name) with
      | (Reg i, Reg n) -> if i = n then (Just v) else find_reg_name reg registers
      | (Reg_slice  i (p1,p2), Reg_slice n (p3,p4)) ->
	if i=n && p1=p3 && p2 = p4 then (Just v) else find_reg_name reg registers
      | (Reg_field i f _,Reg_field n fn _) ->
	if i=n && f = fn then (Just v) else find_reg_name reg registers
      | (Reg_f_slice i f _ (p1,p2), Reg_f_slice n fn _ (p3,p4)) ->
	if i=n && f=fn && p1=p3 && p2=p3 then (Just v) else find_reg_name reg registers
      | _ -> find_reg_name reg registers
end end

let rec ie_loop mode register_values i_state = 
  match (interp mode i_state) with
    | Done -> []
    | Error msg -> [E_error msg]
    | Read_reg reg i_state_fun -> 
      let v =  match register_values with
	| Nothing -> Unknown
	| Just(registers) -> match find_reg_name reg registers with
	    | Nothing -> Unknown
	    | Just v -> v end end in
      (E_read_reg reg)::(ie_loop mode register_values (i_state_fun v))
    | Write_reg reg value i_state->
      (E_write_reg reg value)::(ie_loop mode register_values i_state)
    | Read_mem read_k loc length tracking i_state_fun ->
      (E_read_mem read_k loc length tracking)::(ie_loop mode register_values (i_state_fun Unknown))
    | Write_mem write_k loc length tracking value v_tracking i_state_fun ->
      (E_write_mem write_k loc length tracking value v_tracking)::(ie_loop mode register_values (i_state_fun true))
    | Internal _ _ next -> (ie_loop mode register_values next)
     end ;;
  
let interp_exhaustive register_values i_state = 
  let mode = make_mode true true in
  ie_loop mode register_values 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 tracking value v_tracking i_state_fun ->
      let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
      (((E_write_mem write_k loc length tracking value v_tracking)::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)