move armv8_extras and power_extras to idl/power and idlarm, fixes

5 files changed, 71 insertions, 137 deletions

diff --git a/src/gen_lib/armv8_extras.lem b/src/gen_lib/armv8_extras.lem
deleted file mode 100644
index abab2163..00000000
--- a/src/gen_lib/armv8_extras.lem
+++ /dev/null
@@ -1,53 +0,0 @@
-open import Pervasives
-open import Sail_impl_base
-open import Vector
-open import Sail_values
-open import Prompt
-
-val rMem_NORMAL         : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
-val rMem_STREAM         : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
-val rMem_ORDERED        : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
-val rMem_ATOMICL        : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
-val rMem_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
-
-let rMem_NORMAL (addr,size)         = read_memory Read_plain addr size
-let rMem_STREAM (addr,size)         = read_memory Read_stream addr size
-let rMem_ORDERED (addr,size)        = read_memory Read_acquire addr size
-let rMem_ATOMIC (addr,size)         = read_memory Read_exclusive addr size
-let rMem_ATOMIC_ORDERED (addr,size) = read_memory Read_exclusive_acquire addr size
-
-val wMem_Addr_NORMAL         : forall 'e. (vector bitU * integer) -> M 'e unit
-val wMem_Addr_ORDERED        : forall 'e. (vector bitU * integer) -> M 'e unit
-val wMem_Addr_ATOMIC         : forall 'e. (vector bitU * integer) -> M 'e unit
-val wMem_Addr_ATOMIC_ORDERED : forall 'e. (vector bitU * integer) -> M 'e unit
-
-let wMem_Addr_NORMAL (addr,size)         = write_memory_ea Write_plain addr size
-let wMem_Addr_ORDERED (addr,size)        = write_memory_ea Write_release addr size
-let wMem_Addr_ATOMIC (addr,size)         = write_memory_ea Write_exclusive addr size
-let wMem_Addr_ATOMIC_ORDERED (addr,size) = write_memory_ea Write_exclusive_release addr size
-
-
-val wMem_Val_NORMAL : forall 'e. (integer * vector bitU) -> M 'e unit
-val wMem_Val_ATOMIC : forall 'e. (integer * vector bitU) -> M 'e bitU
-
-let wMem_Val_NORMAL (_,v) = write_memory_val v >>= fun _ -> return ()
-(* in ARM the status returned is inversed *)
-let wMem_Val_ATOMIC (_,v) = write_memory_val v >>= fun b -> return (if b then O else I)
-
-
-val DataMemoryBarrier_Reads            : forall 'e. unit -> M 'e unit
-val DataMemoryBarrier_Writes           : forall 'e. unit -> M 'e unit
-val DataMemoryBarrier_All              : forall 'e. unit -> M 'e unit
-val DataSynchronizationBarrier_Reads   : forall 'e. unit -> M 'e unit
-val DataSynchronizationBarrier_Writes  : forall 'e. unit -> M 'e unit
-val DataSynchronizationBarrier_All     : forall 'e. unit -> M 'e unit
-val InstructionSynchronizationBarrier  : forall 'e. unit -> M 'e unit
-
-let DataMemoryBarrier_Reads ()           = barrier DMB_LD
-let DataMemoryBarrier_Writes ()          = barrier DMB_ST
-let DataMemoryBarrier_All ()             = barrier DMB
-let DataSynchronizationBarrier_Reads ()  = barrier DSB_LD
-let DataSynchronizationBarrier_Writes () = barrier DSB_ST
-let DataSynchronizationBarrier_All ()    = barrier DSB
-let InstructionSynchronizationBarrier () = barrier Isync
-
diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
deleted file mode 100644
index c16b197f..00000000
--- a/src/gen_lib/power_extras.lem
+++ /dev/null
@@ -1,47 +0,0 @@
-open import Pervasives
-open import Sail_impl_base
-open import Vector
-open import Sail_values
-open import Prompt
-
-val MEMr         : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
-val MEMr_reserve : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
-
-let MEMr (addr,size) = read_memory Read_plain addr size
-let MEMr_reserve (addr,size) = read_memory Read_reserve addr size
-
-
-val MEMw_EA      : forall 'e. (vector bitU * integer) -> M 'e unit
-val MEMr_EA_cond : forall 'e. (vector bitU * integer) -> M 'e unit
-                                                           
-let MEMw_EA (addr,size) = write_memory_ea Write_plain addr size
-let MEMw_EA_cond (addr,size) = write_memory_ea Write_conditional addr size
-
-
-val MEMw             : forall 'e. (vector bitU * integer * vector bitU) -> M 'e unit
-val MEMw_conditional : forall 'e. (vector bitU * integer * vector bitU) -> M 'e bitU
-
-let MEMw (_,_,value) = write_memory_val value >>= fun _ -> return ()
-let MEMw_conditional (_,_,value) = write_memory_val value >>= fun b -> return (bool_to_bit b)
-
-
-val I_Sync     : forall 'e. unit -> M 'e unit
-val H_Sync     : forall 'e. unit -> M 'e unit
-val LW_Sync    : forall 'e. unit -> M 'e unit
-val EIEIO_Sync : forall 'e. unit -> M 'e unit
-
-let I_Sync ()     = barrier Isync
-let H_Sync ()     = barrier Sync
-let LW_Sync ()    = barrier LwSync
-let EIEIO_Sync () = barrier Eieio
-
-let recalculate_dependency () = footprint
-
-let trap () = exit "error"
-(* this needs to change, but for that we'd have to make the type checker know about trap 
- * as an effect *)
-
-val countLeadingZeroes : vector bitU * integer -> integer
-let countLeadingZeroes (Vector bits _ _ ,n)  = 
-  let (_,bits) = List.splitAt (natFromInteger n) bits in
-  integerFromNat (List.length (takeWhile ((=) O) bits))
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 7d495969..0cc9e679 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2035,23 +2035,63 @@ let anglebars = enclose langlebar ranglebar
 module M = Map.Make(String)
 
 let keywords =
-  (List.fold_left (fun m (x,y) -> M.add x y m) (M.empty))
+  (List.fold_left (fun m x -> M.add x (x ^ "_") m) (M.empty))
     [
-      ("assert","assert_");
-      ("lsl","lsl_");
-      ("lsr","lsr_");
-      ("asr","asr_");
-      ("type","type_");
-      ("fun","fun_");
-      ("function","function_");
-      ("raise","raise_");
-      ("try","try_");
-      ("match","match_");
-      ("with","with_");
-      ("field","fields_");
-      ("LT","LT_");
-      ("GT","GT_");
-      ("EQ","EQ_");
+      "assert";
+      "lsl";
+      "lsr";
+      "asr";
+      "type";
+      "fun";
+      "function";
+      "raise";
+      "try";
+      "match";
+      "with";
+      "field";
+      "LT";
+      "GT";
+      "EQ";
+
+(*      "nia";
+      "NIA_successor";
+      "NIA_concrete_address";
+      "NIA_LR";
+      "NIA_CTR";
+      "NIA_register";
+      "read_kind";
+      "Read_plain";
+      "Read_tag";
+      "Read_reserve";
+      "Read_acquire";
+      "Read_exclusive";
+      "Read_exclusive_acquire";
+      "Read_stream";
+      "write_kind";
+      "Write_plain";
+      "Write_tag";
+      "Write_conditional";
+      "Write_release";
+      "Write_exclusive";
+      "Write_exclusive_release";
+      "barrier_kind";
+      "Barrier_Sync";
+      "Barrier_LwSync";
+      "Barrier_Eieio";
+      "Barrier_Isync";
+      "Barrier_DMB";
+      "Barrier_DMB_ST";
+      "Barrier_DMB_LD";
+      "Barrier_DSB";
+      "Barrier_DSB_ST";
+      "Barrier_DSB_LD";
+      "Barrier_ISB";
+      "instruction_kind";
+      "IK_barrier";
+      "IK_mem_read";
+      "IK_mem_write";
+      "IK_cond_branch";
+      "IK_simple"; *)
     ] 
 
 let fix_id i = if M.mem i keywords then M.find i keywords else i
@@ -2880,12 +2920,12 @@ let find_regtypes (Defs defs) =
     ) [] defs
 
 
-let pp_defs_lem f_arch f d top_line opens =
+let pp_defs_lem f d top_line opens =
   let regtypes = find_regtypes d in
   let defs = doc_defs_lem regtypes d in
-  print f
-        (string "(*" ^^ (string top_line) ^^ string "*)" ^/^
-           ((separate_map hardline)
-              (fun lib -> separate space [string "open import";string lib]) opens) ^/^
-             hardline ^^ defs);
+  (print f)
+    (string "(*" ^^ (string top_line) ^^ string "*)" ^/^
+       ((separate_map hardline)
+          (fun lib -> separate space [string "open import";string lib]) opens) ^/^
+         hardline ^^ defs);
 
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 43680643..4b51db8a 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -10,4 +10,4 @@ val pat_to_string : tannot pat -> string
 val pp_lem_defs : Format.formatter -> tannot defs -> unit
 
 val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit
-val pp_defs_lem : out_channel -> out_channel -> tannot defs -> string -> string list -> unit
+val pp_defs_lem : out_channel -> tannot defs -> string -> string list -> unit
diff --git a/src/process_file.ml b/src/process_file.ml
index bf696fc2..2da44daa 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -174,23 +174,17 @@ let output1 libpath out_arg filename defs  =
 	  close_output_with_check ext_o
 	end
       | Lem_out None ->
-         let ((o1,_, _) as ext_o1) =
-           open_output_with_check_unformatted ("arch.lem") in
-         let ((o2,_, _) as ext_o2) =
-           open_output_with_check_unformatted (f' ^ "embed.lem") in
-         (Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename))
+         let ((o,_, _) as ext_o) =
+           open_output_with_check_unformatted (f' ^ "_embedded.lem") in
+         (Pretty_print.pp_defs_lem o defs (generated_line filename))
            ["Pervasives_extra";"Sail_impl_base";"Vector";"Prompt";"Sail_values"];
-         close_output_with_check ext_o1;
-         close_output_with_check ext_o2
+         close_output_with_check ext_o
       | Lem_out (Some lib) ->
-         let ((o1,_, _) as ext_o1) =
-           open_output_with_check_unformatted ("arch.lem") in
-         let ((o2,_, _) as ext_o2) =
-           open_output_with_check_unformatted (f' ^ "embed.lem") in
-	 (Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename))
+         let ((o,_, _) as ext_o) =
+           open_output_with_check_unformatted (f' ^ "_embedded.lem") in
+	 (Pretty_print.pp_defs_lem o defs (generated_line filename))
            ["Pervasives_extra";"Sail_impl_base";"Vector";"Prompt";"Sail_values"; lib];
-         close_output_with_check ext_o1;
-         close_output_with_check ext_o2
+         close_output_with_check ext_o;
       | Ocaml_out None ->
         let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
 	begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"];