diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/deep_shallow_convert.lem | 116 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 2 | ||||
| -rw-r--r-- | src/pretty_print.mli | 2 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 191 | ||||
| -rw-r--r-- | src/process_file.ml | 13 |
5 files changed, 176 insertions, 148 deletions
diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem index 23c34222..4af6eb2f 100644 --- a/src/gen_lib/deep_shallow_convert.lem +++ b/src/gen_lib/deep_shallow_convert.lem @@ -6,20 +6,20 @@ open import Sail_values class (ToFromInterpValue 'a) - val toInterpValue : 'a -> Interp.value - val fromInterpValue : Interp.value -> 'a + val toInterpValue : 'a -> Interp_ast.value + val fromInterpValue : Interp_ast.value -> 'a end let toInterValueBool = function - | true -> Interp.V_lit (L_aux (L_one) Unknown) - | false -> Interp.V_lit (L_aux (L_zero) Unknown) + | true -> Interp_ast.V_lit (L_aux (L_one) Unknown) + | false -> Interp_ast.V_lit (L_aux (L_zero) Unknown) end let rec fromInterpValueBool v = match v with - | Interp.V_lit (L_aux (L_true) _) -> true - | Interp.V_lit (L_aux (L_false) _) -> false - | Interp.V_lit (L_aux (L_one) _) -> true - | Interp.V_lit (L_aux (L_zero) _) -> false - | Interp.V_tuple [v] -> fromInterpValueBool v + | Interp_ast.V_lit (L_aux (L_true) _) -> true + | Interp_ast.V_lit (L_aux (L_false) _) -> false + | Interp_ast.V_lit (L_aux (L_one) _) -> true + | Interp_ast.V_lit (L_aux (L_zero) _) -> false + | Interp_ast.V_tuple [v] -> fromInterpValueBool v | v -> failwith ("fromInterpValue bool: unexpected value. " ^ Interp.debug_print_value v) end @@ -29,10 +29,10 @@ instance (ToFromInterpValue bool) end -let toInterpValueUnit () = Interp.V_lit (L_aux (L_unit) Unknown) +let toInterpValueUnit () = Interp_ast.V_lit (L_aux (L_unit) Unknown) let rec fromInterpValueUnit v = match v with - | Interp.V_lit (L_aux (L_unit) _) -> () - | Interp.V_tuple [v] -> fromInterpValueUnit v + | Interp_ast.V_lit (L_aux (L_unit) _) -> () + | Interp_ast.V_tuple [v] -> fromInterpValueUnit v | v -> failwith ("fromInterpValue unit: unexpected value. " ^ Interp.debug_print_value v) end @@ -44,8 +44,8 @@ end let toInterpValueInteger i = V_lit (L_aux (L_num i) Unknown) let rec fromInterpValueInteger v = match v with - | Interp.V_lit (L_aux (L_num i) _) -> i - | Interp.V_tuple [v] -> fromInterpValueInteger v + | Interp_ast.V_lit (L_aux (L_num i) _) -> i + | Interp_ast.V_tuple [v] -> fromInterpValueInteger v | v -> failwith ("fromInterpValue integer: unexpected value. " ^ Interp.debug_print_value v) end @@ -57,8 +57,8 @@ end let toInterpValueString s = V_lit (L_aux (L_string s) Unknown) let rec fromInterpValueString v = match v with - | Interp.V_lit (L_aux (L_string s) _) -> s - | Interp.V_tuple [v] -> fromInterpValueString v + | Interp_ast.V_lit (L_aux (L_string s) _) -> s + | Interp_ast.V_tuple [v] -> fromInterpValueString v | v -> failwith ("fromInterpValue integer: unexpected value. " ^ Interp.debug_print_value v) end @@ -69,17 +69,17 @@ end let toInterpValueBitU = function - | I -> Interp.V_lit (L_aux (L_one) Unknown) - | O -> Interp.V_lit (L_aux (L_zero) Unknown) - | Undef -> Interp.V_lit (L_aux (L_undef) Unknown) + | I -> Interp_ast.V_lit (L_aux (L_one) Unknown) + | O -> Interp_ast.V_lit (L_aux (L_zero) Unknown) + | Undef -> Interp_ast.V_lit (L_aux (L_undef) Unknown) end let rec fromInterpValueBitU v = match v with - | Interp.V_lit (L_aux (L_one) _) -> I - | Interp.V_lit (L_aux (L_zero) _) -> O - | Interp.V_lit (L_aux (L_undef) _) -> Undef - | Interp.V_lit (L_aux (L_true) _) -> I - | Interp.V_lit (L_aux (L_false) _) -> O - | Interp.V_tuple [v] -> fromInterpValueBitU v + | Interp_ast.V_lit (L_aux (L_one) _) -> B1 + | Interp_ast.V_lit (L_aux (L_zero) _) -> B0 + | Interp_ast.V_lit (L_aux (L_undef) _) -> BU + | Interp_ast.V_lit (L_aux (L_true) _) -> B1 + | Interp_ast.V_lit (L_aux (L_false) _) -> B0 + | Interp_ast.V_tuple [v] -> fromInterpValueBitU v | v -> failwith ("fromInterpValue bitU: unexpected value. " ^ Interp.debug_print_value v) end @@ -383,29 +383,31 @@ instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a)) end -module SI = Interp -module SIA = Interp_ast - - let read_kindToInterpValue = function | Read_plain -> V_ctor (Id_aux (Id "Read_plain") Unknown) (T_id "read_kind") (C_Enum 0) (toInterpValue ()) - | Read_tag -> V_ctor (Id_aux (Id "Read_tag") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ()) - | Read_tag_reserve -> V_ctor (Id_aux (Id "Read_tag_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ()) | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ()) | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ()) | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ()) | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ()) | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_acquire") Unknown) (T_id "read_kind") (C_Enum 7) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 8) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved") Unknown) (T_id "read_kind") (C_Enum 9) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ()) end let rec read_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain - | V_ctor (Id_aux (Id "Read_tag") _) _ _ v -> Read_tag - | V_ctor (Id_aux (Id "Read_tag_reserve") _) _ _ v -> Read_tag_reserve | V_ctor (Id_aux (Id "Read_reserve") _) _ _ v -> Read_reserve | V_ctor (Id_aux (Id "Read_acquire") _) _ _ v -> Read_acquire | V_ctor (Id_aux (Id "Read_exclusive") _) _ _ v -> Read_exclusive | V_ctor (Id_aux (Id "Read_exclusive_acquire") _) _ _ v -> Read_exclusive_acquire | V_ctor (Id_aux (Id "Read_stream") _) _ _ v -> Read_stream + | V_ctor (Id_aux (Id "Read_RISCV_acquire") _) _ _ v -> Read_RISCV_acquire + | V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") _) _ _ v -> Read_RISCV_strong_acquire + | V_ctor (Id_aux (Id "Read_RISCV_reserved") _) _ _ v -> Read_RISCV_reserved + | V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") _) _ _ v -> Read_RISCV_reserved_acquire + | V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") _) _ _ v -> Read_RISCV_reserved_strong_acquire | V_tuple [v] -> read_kindFromInterpValue v | v -> failwith ("fromInterpValue read_kind: unexpected value. " ^ Interp.debug_print_value v) @@ -418,21 +420,27 @@ end let write_kindToInterpValue = function | Write_plain -> V_ctor (Id_aux (Id "Write_plain") Unknown) (T_id "write_kind") (C_Enum 0) (toInterpValue ()) - | Write_tag -> V_ctor (Id_aux (Id "Write_tag") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ()) - | Write_tag_conditional -> V_ctor (Id_aux (Id "Write_tag_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ()) | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ()) | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ()) | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ()) | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ()) + | Write_RISCV_release -> V_ctor (Id_aux (Id "Write_RISCV_release") Unknown) (T_id "write_kind") (C_Enum 6) (toInterpValue ()) + | Write_RISCV_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_strong_release") Unknown) (T_id "write_kind") (C_Enum 7) (toInterpValue ()) + | Write_RISCV_conditional -> V_ctor (Id_aux (Id "Write_RISCV_conditional") Unknown) (T_id "write_kind") (C_Enum 8) (toInterpValue ()) + | Write_RISCV_conditional_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_release") Unknown) (T_id "write_kind") (C_Enum 9) (toInterpValue ()) + | Write_RISCV_conditional_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") Unknown) (T_id "write_kind") (C_Enum 10) (toInterpValue ()) end let rec write_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Write_plain") _) _ _ v -> Write_plain - | V_ctor (Id_aux (Id "Write_tag") _) _ _ v -> Write_tag - | V_ctor (Id_aux (Id "Write_tag_conditional") _) _ _ v -> Write_tag_conditional | V_ctor (Id_aux (Id "Write_conditional") _) _ _ v -> Write_conditional | V_ctor (Id_aux (Id "Write_release") _) _ _ v -> Write_release | V_ctor (Id_aux (Id "Write_exclusive") _) _ _ v -> Write_exclusive | V_ctor (Id_aux (Id "Write_exclusive_release") _) _ _ v -> Write_exclusive_release + | V_ctor (Id_aux (Id "Write_RISCV_release") _) _ _ v -> Write_RISCV_release + | V_ctor (Id_aux (Id "Write_RISCV_strong_release") _) _ _ v -> Write_RISCV_strong_release + | V_ctor (Id_aux (Id "Write_RISCV_conditional") _) _ _ v -> Write_RISCV_conditional + | V_ctor (Id_aux (Id "Write_RISCV_conditional_release") _) _ _ v -> Write_RISCV_conditional_release + | V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") _) _ _ v -> Write_RISCV_conditional_strong_release | V_tuple [v] -> write_kindFromInterpValue v | v -> failwith ("fromInterpValue write_kind: unexpected value " ^ Interp.debug_print_value v) @@ -455,7 +463,14 @@ let barrier_kindToInterpValue = function | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ()) | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ()) | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ()) - | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ()) + | Barrier_TM_COMMIT -> V_ctor (Id_aux (Id "Barrier_TM_COMMIT") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ()) + | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ()) + | Barrier_RISCV_rw_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") Unknown) (T_id "barrier_kind") (C_Enum 13) (toInterpValue ()) + | Barrier_RISCV_r_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") Unknown) (T_id "barrier_kind") (C_Enum 14) (toInterpValue ()) + | Barrier_RISCV_rw_w -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") Unknown) (T_id "barrier_kind") (C_Enum 15) (toInterpValue ()) + | Barrier_RISCV_w_w -> V_ctor (Id_aux (Id "Barrier_RISCV_w_w") Unknown) (T_id "barrier_kind") (C_Enum 16) (toInterpValue ()) + | Barrier_RISCV_i -> V_ctor (Id_aux (Id "Barrier_RISCV_i") Unknown) (T_id "barrier_kind") (C_Enum 17) (toInterpValue ()) + | Barrier_x86_MFENCE -> V_ctor (Id_aux (Id "Barrier_x86_MFENCE") Unknown) (T_id "barrier_kind") (C_Enum 18) (toInterpValue ()) end let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync @@ -469,7 +484,14 @@ let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB + | V_ctor (Id_aux (Id "Barrier_TM_COMMIT") _) _ _ v -> Barrier_TM_COMMIT | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC + | V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") _) _ _ v -> Barrier_RISCV_rw_rw + | V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") _) _ _ v -> Barrier_RISCV_r_rw + | V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") _) _ _ v -> Barrier_RISCV_rw_w + | V_ctor (Id_aux (Id "Barrier_RISCV_w_w") _) _ _ v -> Barrier_RISCV_w_w + | V_ctor (Id_aux (Id "Barrier_RISCV_i") _) _ _ v -> Barrier_RISCV_i + | V_ctor (Id_aux (Id "Barrier_x86_MFENCE") _) _ _ v -> Barrier_x86_MFENCE | V_tuple [v] -> barrier_kindFromInterpValue v | v -> failwith ("fromInterpValue barrier_kind: unexpected value. " ^ Interp.debug_print_value v) @@ -503,18 +525,18 @@ instance (ToFromInterpValue instruction_kind) end let regfpToInterpValue = function - | RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) - | RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) - | RSliceBit v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) - | RField v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RField") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) + | RFull v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RFull") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v) + | RSlice v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSlice") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v) + | RSliceBit v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSliceBit") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v) + | RField v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RField") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v) end let rec regfpFromInterpValue v = match v with - | SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") _) _ _ v -> RFull (fromInterpValue v) - | SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v) - | SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v) - | SI.V_ctor (SIA.Id_aux (SIA.Id "RField") _) _ _ v -> RField (fromInterpValue v) - | SI.V_tuple [v] -> regfpFromInterpValue v + | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RFull") _) _ _ v -> RFull (fromInterpValue v) + | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v) + | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v) + | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RField") _) _ _ v -> RField (fromInterpValue v) + | Interp_ast.V_tuple [v] -> regfpFromInterpValue v | v -> failwith ("fromInterpValue regfp: unexpected value. " ^ Interp.debug_print_value v) end diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 48ddd10e..e6169762 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -428,6 +428,8 @@ end (* Data structures for building up instructions *) +(* careful: changes in the read/write/barrier kinds have to be + reflected in deep_shallow_convert *) type read_kind = (* common reads *) | Read_plain diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 9a002454..034db664 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -52,7 +52,7 @@ 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 * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit +val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit val pp_format_annot_ascii : tannot -> string diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 9758b2de..cf8fda59 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -50,7 +50,7 @@ open Pretty_print_common * PPrint-based sail-to-lem pprinter ****************************************************************************) -let print_to_from_interp_value = ref false +let print_to_from_interp_value = ref true let langlebar = string "<|" let ranglebar = string "|>" let anglebars = enclose langlebar ranglebar @@ -805,8 +805,8 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with | TD_abbrev(id,nm,typschm) -> - doc_op equals (concat [string "type"; space; doc_id_lem_type id]) - (doc_typschm_lem regtypes typschm) + (doc_op equals (concat [string "type"; space; doc_id_lem_type id]) + (doc_typschm_lem regtypes typschm),empty) | TD_record(id,nm,typq,fs,_) -> let f_pp (typ,fid) = let fname = if prefix_recordtype @@ -814,19 +814,19 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with else doc_id_lem_type fid in concat [fname;space;colon;space;doc_typ_lem regtypes typ; semi] in let fs_doc = group (separate_map (break 1) f_pp fs) in - doc_op equals + (doc_op equals (concat [string "type"; space; doc_id_lem_type id;]) - (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space))) + (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space))),empty) | TD_variant(id,nm,typq,ar,_) -> (match id with - | Id_aux ((Id "read_kind"),_) -> empty - | Id_aux ((Id "write_kind"),_) -> empty - | Id_aux ((Id "barrier_kind"),_) -> empty - | Id_aux ((Id "trans_kind"),_) -> empty - | Id_aux ((Id "instruction_kind"),_) -> empty - | Id_aux ((Id "regfp"),_) -> empty - | Id_aux ((Id "niafp"),_) -> empty - | Id_aux ((Id "diafp"),_) -> empty + | Id_aux ((Id "read_kind"),_) -> (empty,empty) + | Id_aux ((Id "write_kind"),_) -> (empty,empty) + | Id_aux ((Id "barrier_kind"),_) -> (empty,empty) + | Id_aux ((Id "trans_kind"),_) -> (empty,empty) + | Id_aux ((Id "instruction_kind"),_) -> (empty,empty) + | Id_aux ((Id "regfp"),_) -> (empty,empty) + | Id_aux ((Id "niafp"),_) -> (empty,empty) + | Id_aux ((Id "diafp"),_) -> (empty,empty) | _ -> let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in let typ_pp = @@ -835,9 +835,9 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with (concat [string "type"; space; doc_id_lem_type id;]) (doc_typquant_lem typq ar_doc) in let make_id pat id = - separate space [string "SIA.Id_aux"; - parens (string "SIA.Id " ^^ string_lit (doc_id id)); - if pat then underscore else string "SIA.Unknown"] in + separate space [string "Interp_ast.Id_aux"; + parens (string "Interp_ast.Id " ^^ string_lit (doc_id id)); + if pat then underscore else string "Interp_ast.Unknown"] in let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in let fromInterpValuePP = @@ -849,18 +849,18 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with match tu with | Tu_ty_id (ty,cid) -> (separate space) - [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; + [pipe;string "Interp_ast.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; arrow; doc_id_lem_ctor cid; parens (string "fromInterpValue v")] | Tu_id cid -> (separate space) - [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; + [pipe;string "Interp_ast.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; arrow; doc_id_lem_ctor cid]) ar) ^/^ - ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^ + ((separate space) [pipe;string "Interp_ast.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^ let failmessage = (string_lit @@ -879,43 +879,40 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with | Tu_ty_id (ty,cid) -> (separate space) [pipe;doc_id_lem_ctor cid;string "v";arrow; - string "SI.V_ctor"; + string "Interp_ast.V_ctor"; parens (make_id false cid); - parens (string "SIA.T_id " ^^ string_lit (doc_id id)); - string "SI.C_Union"; + parens (string "Interp_ast.T_id " ^^ string_lit (doc_id id)); + string "Interp_ast.C_Union"; parens (string "toInterpValue v")] | Tu_id cid -> (separate space) [pipe;doc_id_lem_ctor cid;arrow; - string "SI.V_ctor"; + string "Interp_ast.V_ctor"; parens (make_id false cid); - parens (string "SIA.T_id " ^^ string_lit (doc_id id)); - string "SI.C_Union"; + parens (string "Interp_ast.T_id " ^^ string_lit (doc_id id)); + string "Interp_ast.C_Union"; parens (string "toInterpValue ()")]) ar) ^/^ string "end") in let fromToInterpValuePP = + toInterpValuePP ^^ hardline ^^ hardline ^^ + fromInterpValuePP ^^ hardline ^^ hardline ^^ ((prefix 2 1) (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)]) (concat [string "let toInterpValue = ";toInterpValueF;hardline; string "let fromInterpValue = ";fromInterpValueF])) ^/^ string "end" in - typ_pp ^^ hardline ^^ hardline ^^ - if !print_to_from_interp_value then - toInterpValuePP ^^ hardline ^^ hardline ^^ - fromInterpValuePP ^^ hardline ^^ hardline ^^ - fromToInterpValuePP ^^ hardline - else empty) + (typ_pp ^^ hardline,fromToInterpValuePP ^^ hardline)) | TD_enum(id,nm,enums,_) -> (match id with - | Id_aux ((Id "read_kind"),_) -> empty - | Id_aux ((Id "write_kind"),_) -> empty - | Id_aux ((Id "barrier_kind"),_) -> empty - | Id_aux ((Id "trans_kind"),_) -> empty - | Id_aux ((Id "instruction_kind"),_) -> empty - | Id_aux ((Id "regfp"),_) -> empty - | Id_aux ((Id "niafp"),_) -> empty - | Id_aux ((Id "diafp"),_) -> empty + | Id_aux ((Id "read_kind"),_) -> (empty,empty) + | Id_aux ((Id "write_kind"),_) -> (empty,empty) + | Id_aux ((Id "barrier_kind"),_) -> (empty,empty) + | Id_aux ((Id "trans_kind"),_) -> (empty,empty) + | Id_aux ((Id "instruction_kind"),_) -> (empty,empty) + | Id_aux ((Id "regfp"),_) -> (empty,empty) + | Id_aux ((Id "niafp"),_) -> (empty,empty) + | Id_aux ((Id "diafp"),_) -> (empty,empty) | _ -> let rec range i j = if i > j then [] else i :: (range (i+1) j) in let nats = range 0 in @@ -926,9 +923,9 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in let make_id pat id = - separate space [string "SIA.Id_aux"; - parens (string "SIA.Id " ^^ string_lit (doc_id id)); - if pat then underscore else string "SIA.Unknown"] in + separate space [string "Interp_ast.Id_aux"; + parens (string "Interp_ast.Id " ^^ string_lit (doc_id id)); + if pat then underscore else string "Interp_ast.Unknown"] in let fromInterpValuePP = (prefix 2 1) (separate space [string "let rec";fromInterpValueF;string "v";equals;string "match v with"]) @@ -936,7 +933,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with ((separate_map (break 1)) (fun (cid) -> (separate space) - [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; + [pipe;string "Interp_ast.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; arrow;doc_id_lem_ctor cid] ) enums @@ -944,7 +941,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with ( (align ((prefix 3 1) - (separate space [pipe;string ("SI.V_lit (SIA.L_aux (SIA.L_num n) _)");arrow]) + (separate space [pipe;string ("Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _)");arrow]) (separate space [string "match";parens(string "natFromInteger n");string "with"] ^/^ ( ((separate_map (break 1)) @@ -960,7 +957,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with ) ) ^/^ - ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^ + ((separate space) [pipe;string "Interp_ast.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^ let failmessage = (string_lit @@ -978,25 +975,23 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with (fun (cid,number) -> (separate space) [pipe;doc_id_lem_ctor cid;arrow; - string "SI.V_ctor"; + string "Interp_ast.V_ctor"; parens (make_id false cid); - parens (string "SIA.T_id " ^^ string_lit (doc_id id)); - parens (string ("SI.C_Enum " ^ string_of_int number)); + parens (string "Interp_ast.T_id " ^^ string_lit (doc_id id)); + parens (string ("Interp_ast.C_Enum " ^ string_of_int number)); parens (string "toInterpValue ()")]) (List.combine enums (nats ((List.length enums) - 1)))) ^/^ string "end") in let fromToInterpValuePP = + toInterpValuePP ^^ hardline ^^ hardline ^^ + fromInterpValuePP ^^ hardline ^^ hardline ^^ ((prefix 2 1) (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)]) (concat [string "let toInterpValue = ";toInterpValueF;hardline; string "let fromInterpValue = ";fromInterpValueF])) ^/^ string "end" in - typ_pp ^^ hardline ^^ hardline ^^ - if !print_to_from_interp_value - then toInterpValuePP ^^ hardline ^^ hardline ^^ - fromInterpValuePP ^^ hardline ^^ hardline ^^ - fromToInterpValuePP ^^ hardline - else empty) + (typ_pp ^^ hardline, + fromToInterpValuePP ^^ hardline)) | TD_register(id,n1,n2,rs) -> match n1,n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> @@ -1010,11 +1005,11 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with let dir_b = i1 < i2 in let dir = string (if dir_b then "true" else "false") in let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in - (doc_op equals) + ((doc_op equals) (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"]) (string "Register" ^^ space ^^ align (separate space [string "regname"; doc_int size; doc_int i1; dir; - break 0 ^^ brackets (align doc_rids)])) + break 0 ^^ brackets (align doc_rids)])),empty) (*^^ hardline ^^ separate_map hardline doc_rfield rs *) @@ -1147,26 +1142,29 @@ let doc_spec_lem regtypes (VS_aux (valspec,annot)) = let rec doc_def_lem regtypes def = match def with - | DEF_spec v_spec -> (doc_spec_lem regtypes v_spec,empty) - | DEF_type t_def -> (group (doc_typdef_lem regtypes t_def) ^/^ hardline,empty) - | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty) + | DEF_spec v_spec -> ((doc_spec_lem regtypes v_spec,empty),empty) + | DEF_type t_def -> + let (typdefs,fromtodefs) = doc_typdef_lem regtypes t_def in + ((group typdefs ^/^ hardline,fromtodefs),empty) + | DEF_reg_dec dec -> ((group (doc_dec_lem dec),empty),empty) - | DEF_default df -> (empty,empty) - | DEF_fundef f_def -> (empty,group (doc_fundef_lem regtypes f_def) ^/^ hardline) - | DEF_val lbind -> (empty,group (doc_let_lem regtypes lbind) ^/^ hardline) + | DEF_default df -> ((empty,empty),empty) + | DEF_fundef f_def -> ((empty,empty),group (doc_fundef_lem regtypes f_def) ^/^ hardline) + | DEF_val lbind -> ((empty,empty),group (doc_let_lem regtypes lbind) ^/^ hardline) | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point" - | DEF_kind _ -> (empty,empty) + | DEF_kind _ -> ((empty,empty),empty) - | DEF_comm (DC_comm s) -> (empty,comment (string s)) + | DEF_comm (DC_comm s) -> ((empty,empty),comment (string s)) | DEF_comm (DC_comm_struct d) -> - let (typdefs,vdefs) = doc_def_lem regtypes d in - (empty,comment (typdefs ^^ hardline ^^ vdefs)) + let ((typdefs,tofromdefs),vdefs) = doc_def_lem regtypes d in + ((empty,empty),comment (typdefs ^^ hardline ^^ tofromdefs ^^ hardline ^^ vdefs)) let doc_defs_lem regtypes (Defs defs) = let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in - (separate empty typdefs,separate empty valdefs) + let (typdefs,tofromdefs) = List.split typdefs in + (separate empty typdefs,separate empty tofromdefs, separate empty valdefs) let find_regtypes (Defs defs) = List.fold_left @@ -1180,38 +1178,33 @@ let find_regtypes (Defs defs) = let typ_to_t env = Type_check.typ_to_t env false false -let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line = +let pp_defs_lem + (types_file,types_modules) + (prompt_file,prompt_modules) + (state_file,state_modules) + (tofrom_file,tofrom_modules) + d top_line = + let pp_aux file modules defs = + (print file) + (concat + [string "(*" ^^ (string top_line) ^^ string "*)";hardline; + (separate_map hardline) + (fun lib -> separate space [string "open import";string lib]) modules;hardline; + defs]); + in + + let regtypes = find_regtypes d in - let (typdefs,valdefs) = doc_defs_lem regtypes d in - (print types_file) - (concat - [string "(*" ^^ (string top_line) ^^ string "*)";hardline; - (separate_map hardline) - (fun lib -> separate space [string "open import";string lib]) types_modules;hardline; - if !print_to_from_interp_value - then - concat - [(separate_map hardline) - (fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"]; - string "open import Deep_shallow_convert"; - hardline; - hardline; - string "module SI = Interp"; hardline; - string "module SIA = Interp_ast"; hardline; - hardline] - else empty; - typdefs]); - (print prompt_file) - (concat - [string "(*" ^^ (string top_line) ^^ string "*)";hardline; - (separate_map hardline) - (fun lib -> separate space [string "open import";string lib]) prompt_modules;hardline; - hardline; - valdefs]); - (print state_file) + let (typdefs,tofromdefs,valdefs) = doc_defs_lem regtypes d in + + pp_aux types_file types_modules typdefs; + pp_aux prompt_file prompt_modules valdefs; + pp_aux state_file state_modules valdefs; + + (print tofrom_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; - (separate_map hardline) - (fun lib -> separate space [string "open import";string lib]) state_modules;hardline; - hardline; - valdefs]); + (separate_map hardline) (fun lib -> separate space [string "open import";string lib]) tofrom_modules;hardline; + (separate_map hardline) (fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"];hardline; + string "open import Deep_shallow_convert"; + hardline;tofromdefs]) diff --git a/src/process_file.ml b/src/process_file.ml index 273979cf..39a8bf58 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -172,18 +172,23 @@ let output1 libpath out_arg filename defs = | Lem_out None -> let generated_line = generated_line filename in let types_module = (f' ^ "_embed_types") in + let tofrom_module = (f' ^ "_toFromInterp") in let ((o,_, _) as ext_o) = open_output_with_check_unformatted (f' ^ "_embed_types.lem") in let ((o',_, _) as ext_o') = open_output_with_check_unformatted (f' ^ "_embed.lem") in let ((o'',_, _) as ext_o'') = open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in + let ((o''',_, _) as ext_o''') = + open_output_with_check_unformatted (f' ^ "_toFromInterp.lem") in (Pretty_print.pp_defs_lem (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) (o',["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values"; String.capitalize types_module]) (o'',["Pervasives_extra";"Sail_impl_base";"State";"Sail_values"; String.capitalize types_module]) + (o''',["Pervasives_extra";"Sail_impl_base";"Sail_values"; + String.capitalize types_module]) defs generated_line); close_output_with_check ext_o; close_output_with_check ext_o'; @@ -191,22 +196,28 @@ let output1 libpath out_arg filename defs = | Lem_out (Some lib) -> let generated_line = generated_line filename in let types_module = (f' ^ "_embed_types") in + let tofrom_module = (f' ^ "_toFromInterp") in let ((o,_, _) as ext_o) = open_output_with_check_unformatted (f' ^ "_embed_types.lem") in let ((o',_, _) as ext_o') = open_output_with_check_unformatted (f' ^ "_embed.lem") in let ((o'',_, _) as ext_o'') = open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in + let ((o''',_, _) as ext_o''') = + open_output_with_check_unformatted (f' ^ "_toFromInterp.lem") in (Pretty_print.pp_defs_lem (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) (o',["Pervasives_extra";"Sail_impl_base";"Prompt"; "Sail_values";String.capitalize types_module;lib]) (o'',["Pervasives_extra";"Sail_impl_base";"State"; "Sail_values";String.capitalize types_module;lib ^ "_sequential"]) + (o''',["Pervasives_extra";"Sail_impl_base"; + "Sail_values";String.capitalize types_module;lib]) defs generated_line); close_output_with_check ext_o; close_output_with_check ext_o'; - close_output_with_check ext_o'' + close_output_with_check ext_o''; + 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"]; |