summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/pretty_print_lem.ml')
-rw-r--r--src/pretty_print_lem.ml191
1 files changed, 92 insertions, 99 deletions
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])
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-12 00:34:07 +0000