summaryrefslogtreecommitdiff
path: root/src/process_file.ml
diff options
context:
space:
mode:
authorKathy Gray2015-09-28 17:06:23 +0100
committerKathy Gray2015-09-28 17:06:36 +0100
commitd42ab302c2fbb2e5ffbd3ab88ab22c614a0905a4 (patch)
treee51cc7687d30163c38c61148b65c079cba503177 /src/process_file.ml
parent99815e730f4a0588ac886ad1bdf8ae0e1a5c9849 (diff)
basic untested ocaml boiler plate
Diffstat (limited to 'src/process_file.ml')
-rw-r--r--src/process_file.ml220
1 files changed, 14 insertions, 206 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index c36f9381..efa755b9 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -48,7 +48,7 @@ open Type_internal
type out_type =
| Lem_ast_out
- | Lem_out
+ | Ocaml_out of string option
(* let r = Ulib.Text.of_latin1 *)
@@ -108,6 +108,10 @@ let open_output_with_check file_name =
let o' = Format.formatter_of_out_channel o in
(o', (o, temp_file_name, file_name))
+let open_output_with_check_unformatted file_name =
+ let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
+ (o, temp_file_name, file_name)
+
let always_replace_files = ref true
let close_output_with_check (o, temp_file_name, file_name) =
@@ -120,43 +124,6 @@ let close_output_with_check (o, temp_file_name, file_name) =
let generated_line f =
Printf.sprintf "Generated by Sail from %s." f
-(*let tex_preamble =
- "\\documentclass{article}\n" ^
- "\\usepackage{amsmath,amssymb}\n" ^
- "\\usepackage{color}\n" ^
- "\\usepackage{geometry}\n" ^
- "\\usepackage{alltt}\n" ^
- "\\usepackage{lem}\n" ^
- "\\geometry{a4paper,dvips,twoside,left=22.5mm,right=22.5mm,top=20mm,bottom=30mm}\n" ^
- "\\begin{document}\n"^
- "\\tableofcontents\n\\newpage\n"
-
-let tex_postamble =
- "\\end{document}\n"
-
-(* TODO: make this not cppmem-specific *)
-let html_preamble =
-"\n" ^
-"<?xml version=\"1.0\" encoding=\"utf-8\"?>\n" ^
-"<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.1//EN\"\n" ^
-" \"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd\">\n" ^
-"<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^
-" <head>\n" ^
-" <meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\"/> \n" ^
-" <title>C/C++ memory model definitions</title>\n" ^
-" <link rel=\"stylesheet\" type=\"text/css\" title=\"cppmem style\" media=\"screen\" href=\"cppmem.css\"/>\n" ^
-" </head>\n" ^
-" <body>\n" ^
-" <h1 id=\"title\">C/C++ memory model definitions</h1>\n" ^
-"<pre>\n"
-
-let html_postamble =
-"\n" ^
-"</pre>\n" ^
-" </body>\n" ^
-"</html>\n"
-*)
-
let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum*) =
let f' = Filename.basename (Filename.chop_extension filename) in
match out_arg with
@@ -202,175 +169,16 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
Pretty_print.pp_lem_defs o defs;
close_output_with_check ext_o
end
- | Lem_out -> assert false
-(* | Some(Typed_ast.Target_html) ->
- begin
- let r = B.html_defs m.typed_ast in
- let (o, ext_o) = open_output_with_check (f' ^ ".html") in
- Printf.fprintf o "<!-- %s -->\n" (generated_line m.filename);
- Printf.fprintf o "%s" html_preamble;
- Printf.fprintf o "%s" (Ulib.Text.to_string r);
- Printf.fprintf o "%s" html_postamble;
- close_output_with_check ext_o
- end
- | Some(Typed_ast.Target_hol) ->
- begin
- let (r_main, r_extra_opt) = B.hol_defs m.typed_ast in
- let hol_header o = begin
- Printf.fprintf o "(*%s*)\n" (generated_line m.filename);
- Printf.fprintf o "open bossLib Theory Parse res_quanTheory\n";
- Printf.fprintf o "open fixedPointTheory finite_mapTheory listTheory pairTheory pred_setTheory\n";
- Printf.fprintf o "open integerTheory set_relationTheory sortingTheory stringTheory wordsTheory\n\n";
- Printf.fprintf o "val _ = numLib.prefer_num();\n\n";
- Printf.fprintf o "\n\n";
- begin
- if m.predecessor_modules <> [] then
- begin
- Printf.fprintf o "open";
- List.iter
- (fun f -> Printf.fprintf o " %s" f; Printf.fprintf o "Theory")
- m.predecessor_modules;
- Printf.fprintf o "\n\n"
- end
- else
- ()
- end
- end in
- let _ = begin
- let (o, ext_o) = open_output_with_check (m.module_name ^ "Script.sml") in
- hol_header o;
- Printf.fprintf o "val _ = new_theory \"%s\"\n\n" m.module_name;
- Printf.fprintf o "%s" (Ulib.Text.to_string r_main);
- Printf.fprintf o "val _ = export_theory()\n\n";
- close_output_with_check ext_o;
- end in
- let _ = match r_extra_opt with None -> () | Some r_extra ->
- begin
- let (o,ext_o) = open_output_with_check (m.module_name ^ "ExtraScript.sml") in
- hol_header o;
- Printf.fprintf o "open %sTheory\n\n" m.module_name;
- Printf.fprintf o "val _ = new_theory \"%sExtra\"\n\n" m.module_name;
- Printf.fprintf o "%s" (Ulib.Text.to_string r_extra);
- Printf.fprintf o "val _ = export_theory()\n\n";
- close_output_with_check ext_o
- end in ()
- end
- | Some(Typed_ast.Target_tex) ->
- begin
- let rr = B.tex_defs m.typed_ast in
- (* complete tex document, wrapped in tex_preamble and tex_postamble *)
- let (^^^^) = Ulib.Text.(^^^) in
- let r' = r"\\section{" ^^^^ Output.tex_escape (Ulib.Text.of_string f') ^^^^ r"}\n" ^^^^ rr in
- alldoc_accum := (!alldoc_accum) @ [r'];
- let (o, ext_o) = open_output_with_check (f' ^ ".tex") in
- Printf.fprintf o "%%%s\n" (generated_line m.filename);
- Printf.fprintf o "%s" tex_preamble;
- Printf.fprintf o "%s" (Ulib.Text.to_string rr);
- Printf.fprintf o "%s" tex_postamble;
- close_output_with_check ext_o;
- (* tex definitions to include in other documents *)
- let header = r"\n%%%% generated from " ^^^^ (Ulib.Text.of_string m.filename) ^^^^ r"\n" in
- let (r,r_usage) = B.tex_inc_defs m.typed_ast in
- let (r,r_usage) = (header ^^^^ r, header ^^^^ r_usage) in
- alldoc_inc_accum := (!alldoc_inc_accum) @ [r];
- alldoc_inc_usage_accum := (!alldoc_inc_usage_accum) @ [r_usage];
- let (o,ext_o) = open_output_with_check (f' ^ "-inc.tex") in
- Printf.fprintf o "%%%s\n" (generated_line m.filename);
- Printf.fprintf o "%s" (Ulib.Text.to_string r);
- close_output_with_check ext_o;
- let (o, ext_o) = open_output_with_check (f' ^ "-use_inc.tex") in
- Printf.fprintf o "%%%s\n" (generated_line m.filename);
- Printf.fprintf o "%s" (Ulib.Text.to_string r_usage);
- close_output_with_check ext_o
- end
- | Some(Typed_ast.Target_ocaml) ->
- begin
- let (r_main, r_extra_opt) = B.ocaml_defs m.typed_ast in
- let _ = begin
- let (o, ext_o) = open_output_with_check (f' ^ ".ml") in
- Printf.fprintf o "(*%s*)\n" (generated_line m.filename);
- Printf.fprintf o "open Nat_num\n\n";
- Printf.fprintf o "open Sum\n\n";
- Printf.fprintf o "type 'a set = 'a Pset.set\n\n";
- Printf.fprintf o "%s" (Ulib.Text.to_string r_main);
- close_output_with_check ext_o
- end in
- let _ = match r_extra_opt with None -> () | Some r_extra ->
- begin
- let (o, ext_o) = open_output_with_check (f' ^ "Extra.ml") in
- Printf.fprintf o "(*%s*)\n" (generated_line m.filename);
- Printf.fprintf o "open Nat_num\n";
- Printf.fprintf o "open %s\n\n" m.module_name;
- Printf.fprintf o "type 'a set = 'a Pset.set\n\n";
-
- Printf.fprintf o "%s" "let run_test n loc b =\n if b then (Format.printf \"%s : ok\\n\" n) else (Format.printf \"%s : FAILED\\n %s\\n\\n\" n loc);;\n\n";
-
- Printf.fprintf o "%s" (Ulib.Text.to_string r_extra);
- close_output_with_check ext_o
- end in ()
- end
- | Some(Typed_ast.Target_isa) ->
- begin
- try begin
- let (r_main, r_extra_opt) = B.isa_defs m.typed_ast in
- let r1 = B.isa_header_defs m.typed_ast in
- let _ =
- begin
- let (o, ext_o) = open_output_with_check (m.module_name ^ ".thy") in
- Printf.fprintf o "header{*%s*}\n\n" (generated_line m.filename);
- Printf.fprintf o "theory \"%s\" \n\n" m.module_name;
- Printf.fprintf o "imports \n \t Main\n";
- Printf.fprintf o "\t \"%s\"\n" isa_thy;
- (*
- Printf.fprintf o "imports \n \t \"%s/num_type\" \n" libpath;
- *)
- Printf.fprintf o "%s" (Ulib.Text.to_string r1);
-
- begin
- if m.predecessor_modules <> [] then
- begin
- List.iter (fun f -> Printf.fprintf o "\t \"%s\" \n" f) m.predecessor_modules;
- end
- else ()
- end;
-
- Printf.fprintf o "\nbegin \n\n";
- Printf.fprintf o "%s" (Ulib.Text.to_string r_main);
- Printf.fprintf o "end\n";
- close_output_with_check ext_o
- end in
-
- let _ = match r_extra_opt with None -> () | Some r_extra ->
- begin
- let (o, ext_o) = open_output_with_check (m.module_name ^ "Extra.thy") in
- Printf.fprintf o "header{*%s*}\n\n" (generated_line m.filename);
- Printf.fprintf o "theory \"%sExtra\" \n\n" m.module_name;
- Printf.fprintf o "imports \n \t Main \"~~/src/HOL/Library/Efficient_Nat\" \"%s\"\n" m.module_name;
- Printf.fprintf o "\nbegin \n\n";
- Printf.fprintf o "%s" (Ulib.Text.to_string r_extra);
- Printf.fprintf o "end\n";
- close_output_with_check ext_o
- end in ()
- end
- with | Trans.Trans_error(l,msg) ->
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_trans_header (l, msg)))
- end
+ | Ocaml_out None ->
+ let ((o,temp_file_name, filename) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
+ begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["sail_values"];
+ close_output_with_check ext_o
+ end
+ | Ocaml_out (Some lib) ->
+ let ((o,temp_file_name, filename) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
+ Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["sail_values"; lib];
+ close_output_with_check ext_o
- | Some(Typed_ast.Target_coq) ->
- begin
- let r = B.coq_defs m.typed_ast in
- let (o, ext_o) = open_output_with_check (f' ^ ".v") in
- Printf.fprintf o "(* %s *)\n\n" (generated_line m.filename);
- Printf.fprintf o "Require Import Arith.\n";
- Printf.fprintf o "Require Import Bool.\n";
- Printf.fprintf o "Require Import List.\n";
- Printf.fprintf o "Require Import String.\n";
- Printf.fprintf o "Require Import Program.Wf.\n\n";
- Printf.fprintf o "Open Scope nat_scope.\n";
- Printf.fprintf o "Open Scope string_scope.\n\n";
- Printf.fprintf o "%s" (Ulib.Text.to_string r);
- close_output_with_check ext_o
- end*)
let output libpath out_arg files (*alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum*) =
List.iter
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 14:48:50 +0000