open import Pervasives
open import Interp_ast
open import Interp_interface
open import Sail_impl_base
open import Interp_inter_imp
import Set_extra

let memory_parameter_transformer mode v =
  match v with
  | Interp_ast.V_tuple [location;length] ->
    let (v,loc_regs) = extern_with_track mode extern_vector_value location in

    match length with
    | Interp_ast.V_lit (L_aux (L_num len) _) ->
      (v,(natFromInteger len),loc_regs)
    | Interp_ast.V_track (Interp_ast.V_lit (L_aux (L_num len) _)) size_regs ->
      match loc_regs with
      | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
      | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
      end
    | _ -> Assert_extra.failwith "expected 'V_lit (L_aux (L_num _) _)' or 'V_track (V_lit (L_aux (L_num len) _)) _'"
    end
  | _ -> Assert_extra.failwith ("memory_parameter_transformer: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v))
  end

let memory_parameter_transformer_option_address _mode v =
  match v with
  | Interp_ast.V_tuple [location;_] ->
     Just (extern_vector_value location)
  | _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v))
  end


let riscv_read_memory_functions : memory_reads =
  [ ("MEMr",                  (MR Read_plain                  memory_parameter_transformer));
    ("MEMr_acquire",          (MR Read_RISCV_acquire          memory_parameter_transformer));
    ("MEMr_strong_acquire",   (MR Read_RISCV_strong_acquire   memory_parameter_transformer));
    ("MEMr_reserved",         (MR Read_RISCV_reserved         memory_parameter_transformer));
    ("MEMr_reserved_acquire", (MR Read_RISCV_reserved_acquire memory_parameter_transformer));
    ("MEMr_reserved_strong_acquire",
                              (MR Read_RISCV_reserved_acquire memory_parameter_transformer));
  ]

let riscv_memory_writes : memory_writes =
  []

let riscv_memory_eas : memory_write_eas =
  [ ("MEMea",                     (MEA Write_plain                     memory_parameter_transformer));
    ("MEMea_release",             (MEA Write_RISCV_release             memory_parameter_transformer));
    ("MEMea_strong_release",      (MEA Write_RISCV_strong_release      memory_parameter_transformer));
    ("MEMea_conditional",         (MEA Write_RISCV_conditional         memory_parameter_transformer));
    ("MEMea_conditional_release", (MEA Write_RISCV_conditional_release memory_parameter_transformer));
    ("MEMea_conditional_strong_release",
                                  (MEA Write_RISCV_conditional_strong_release
                                                                       memory_parameter_transformer));
  ]

let riscv_memory_vals : memory_write_vals =
  [ ("MEMval",                    (MV memory_parameter_transformer_option_address Nothing));
    ("MEMval_release",            (MV memory_parameter_transformer_option_address Nothing));
    ("MEMval_strong_release",     (MV memory_parameter_transformer_option_address Nothing));
    ("MEMval_conditional",        (MV memory_parameter_transformer_option_address Nothing));
    ("MEMval_conditional_release",(MV memory_parameter_transformer_option_address Nothing));
    ("MEMval_conditional_strong_release",
                                  (MV memory_parameter_transformer_option_address Nothing));

  ]

let riscv_speculate_conditional_success : excl_res =
  let f = fun (IState interp context) b ->
    let bool_res = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in
    IState (Interp.add_answer_to_stack interp bool_res) context
  in
  Just ("speculate_conditional_success", (ER (Just f)))

let riscv_barrier_functions =
  [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw);
    ("MEM_fence_r_rw",  Barrier_RISCV_r_rw);
    ("MEM_fence_r_r",   Barrier_RISCV_r_r);
    ("MEM_fence_rw_w",  Barrier_RISCV_rw_w);
    ("MEM_fence_w_w",   Barrier_RISCV_w_w);
    ("MEM_fence_i",     Barrier_RISCV_i);
  ]