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


(*MIPS specific external functions*)
let mips_externs = [
]

let read_memory_functions : memory_reads =
  [ ("MEMr", (MR Read_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_mem_value mode location in
                       (v,(natFromInteger len),regs) 
                     | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
                       let (v,loc_regs) = extern_mem_value mode location in
                       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 end end)));
    ("MEMr_reserve", (MR Read_reserve (*TODO Likely this isn't really best to be the same as Power*)
                        (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_mem_value mode location in
                               (v,(natFromInteger len),regs) 
                             | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
                               let (v,loc_regs) = extern_mem_value mode location in
                               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 end end)));                
]
let memory_writes : memory_writes = [
  ("MEMw", (MW 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_mem_value mode location in
                     (v,(natFromInteger len),regs)
                   | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
                     let (v,loc_regs) = extern_mem_value mode location in
                     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 end end) Nothing));
  (* As above, probably not best to be the same write kind as power *)
  ("MEMw_conditional", (MW 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_mem_value mode location in
                                 (v,(natFromInteger len),regs)
                               | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
                                 let (v,loc_regs) = extern_mem_value mode location in
                                 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 end end) 
                            (Just (fun (IState interp_state c) success ->
                              let v = Interp.V_lit (L_aux (if success then L_one else L_zero) Unknown) in
                              IState (Interp.add_answer_to_stack interp_state v) c))
     ));
  ]

let barrier_functions = [
  (*Need to know what barrier kind to install*)
  ("MEM_Sync", Isync);
]