Pretty printer to Lem ast added; accessed by -lem_ast on the command line

1 files changed, 27 insertions, 47 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index e642baf5..a73eeac3 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -46,6 +46,10 @@
 
 open Type_internal
 
+type out_type =
+  | Lem_ast_out
+  | Lem_out
+
 (* let r = Ulib.Text.of_latin1 *)
 
 let get_lexbuf fn =
@@ -72,34 +76,10 @@ let parse_file (f : string) : Parse_ast.defs =
 let convert_ast (defs : Parse_ast.defs) : Type_internal.tannot Ast.defs =
   Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env Envmap.empty defs
 
-(* type instances = Types.instance list Types.Pfmap.t
-
-let check_ast (ts : Typed_ast.Targetset.t) (mod_path : Name.t list)
-      ((tdefs,env) : ((Types.type_defs * instances) * Typed_ast.env))
-      (ast, end_lex_skips)
-      : (Types.type_defs * instances * instances) * Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) =
-  try
-    let (defs,env,tast) =
-      Typecheck.check_defs ts mod_path tdefs env ast
-    in
-      (defs,env,(tast,end_lex_skips))
-  with
-    | Ident.No_type(l,m) ->
-        raise (Reporting_basic.Fatal_error (Reporting_basic.Err_type (l, m)))
-
-let check_ast_as_module (ts : Typed_ast.Targetset.t) (mod_path : Name.t list)
-      (e : ((Types.type_defs * instances) * Typed_ast.env))
-      (mod_name : Ulib.Text.t) (ast, end_lex_skips)
-      : (Types.type_defs * instances * instances) * Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) =
-  check_ast ts mod_path e
-    (Ast.Defs([(Ast.Def_l(Ast.Module(None, Ast.X_l((None,mod_name),Ast.Unknown), None, None, ast, None), Ast.Unknown),
-                None,
-                false)]), end_lex_skips)
-
-
 let open_output_with_check file_name =
   let (temp_file_name, o) = Filename.open_temp_file "lem_temp" "" in
-  (o, (o, temp_file_name, file_name))
+  let o' = Format.formatter_of_out_channel o in
+  (o', (o, temp_file_name, file_name))
 
 let always_replace_files = ref true
 
@@ -111,9 +91,9 @@ let close_output_with_check (o, temp_file_name, file_name) =
   ()
 
 let generated_line f =
-  Printf.sprintf "Generated by Lem from %s." f
+  Printf.sprintf "Generated by XX from %s." f
 
-let tex_preamble =
+(*let tex_preamble =
   "\\documentclass{article}\n" ^
   "\\usepackage{amsmath,amssymb}\n" ^
   "\\usepackage{color}\n" ^
@@ -148,20 +128,20 @@ let html_postamble =
 "</pre>\n" ^
 "  </body>\n" ^
 "</html>\n"
+*)
 
-let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
-  let module C = struct
-    let avoid = avoid
-  end
-  in
-  let module B = Backend.Make(C) in
-  let open Typed_ast in
-  let f' = Filename.basename (Filename.chop_extension m.filename) in
-    match targ with
-      | None ->
-          let r = B.ident_defs m.typed_ast in
-            Printf.printf "%s" (Ulib.Text.to_string r)
-      | Some(Typed_ast.Target_html) ->
+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
+      | Lem_ast_out ->
+	begin
+	  let (o, ext_o) = open_output_with_check (f' ^ ".lem") in
+	  Format.fprintf o "(* %s *)" (generated_line filename);
+	  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
@@ -328,16 +308,16 @@ let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum
               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
+          end*)
 
-let output libpath isa_thy targ consts type_info mods alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
+let output libpath out_arg files (*alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum*) =
   List.iter
-    (fun m ->
-       output1 libpath isa_thy targ consts type_info m alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum)
-    mods
+    (fun (f, defs) ->
+       output1 libpath out_arg f defs (*alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum*))
+    files
 
 
-let output_alldoc f' fs alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
+(*let output_alldoc f' fs alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
   let rs = !alldoc_accum in
   let (o, ext_o) = open_output_with_check (f' ^ ".tex") in
   Printf.fprintf o "%%%s\n" (generated_line fs);