cheri sail export progress

3 files changed, 19 insertions, 3 deletions

diff --git a/src/Makefile b/src/Makefile
index 3b12e7c3..fb71396d 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -81,6 +81,15 @@ _build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o cheri_notlb $(CHERI_NOTLB_SAILS)
 
+_build/cheri_embed_types.lem: $(CHERI_SAILS) ./sail.native
+	mkdir -p _build
+	cd _build ;\
+	../sail.native -lem_lib "Mips_extras_embed" -lem -o cheri $(CHERI_SAILS)
+
+_build/Cheri_embed_sequential.thy: _build/cheri_embed_types.lem
+	cd _build ;\
+	lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem ../../mips/mips_extras_embed_sequential.lem cheri_embed_sequential.lem
+
 _build/mips_all.sail: $(MIPS_SAILS)
 	cat $(MIPS_SAILS) > $@
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index f5680cb8..e7cf1e99 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -3105,7 +3105,7 @@ let doc_spec_lem regtypes (VS_aux (valspec,annot)) =
 (* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem regtypes typschm] ^/^ hardline *)
 
 
-let doc_def_lem regtypes def = match def with
+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)
@@ -3115,6 +3115,13 @@ let doc_def_lem regtypes def = match def with
   | DEF_val lbind -> (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_comm (DC_comm s) -> (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 doc_defs_lem regtypes (Defs defs) =
   let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in
diff --git a/src/process_file.ml b/src/process_file.ml
index a5423cc4..cda44e77 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -181,7 +181,7 @@ let output1 libpath out_arg filename defs  =
          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
+           open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in
 	 (Pretty_print.pp_defs_lem
             (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"])
             (o',["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values";
@@ -202,7 +202,7 @@ let output1 libpath out_arg filename defs  =
          let ((o'',_, _) as ext_o'') =
            open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in
 	 (Pretty_print.pp_defs_lem
-            (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";lib])
+            (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";