]> matita.cs.unibo.it Git - helm.git/commitdiff
added option -dump to matitac for persistent macro expansion
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 9 Feb 2007 17:27:31 +0000 (17:27 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 9 Feb 2007 17:27:31 +0000 (17:27 +0000)
helm/software/components/acic_procedural/acic2Procedural.ml
helm/software/components/acic_procedural/proceduralTypes.ml
helm/software/components/cic/cicParser.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_parser/test_parser.ml
helm/software/matita/applyTransformation.ml
helm/software/matita/matitac.ml
helm/software/matita/matitacLib.ml

index adfe4b05cdf8d647f26e68359332737e4c0097fc..e26dd68a2ac23004f0e0de013d6cef8aa91ca8fd 100644 (file)
@@ -342,7 +342,7 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj =
       intros    = [];
       ety       = None
    } in
-   prerr_endline "Level 2 transformation";
+   HLog.debug "Level 2 transformation";
    let steps = mk_obj st aobj in
-   prerr_endline "grafite rendering";
+   HLog.debug "grafite rendering";
    List.rev (T.render_steps [] steps)
index 95fdc6e562d6c8e281c937509dd8b57d57431ab9..53605271d5627154a1227afd782b2aa577eb9e36 100644 (file)
@@ -164,7 +164,7 @@ let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None))
 let rec render_step sep a = function
    | Note s               -> mk_note s :: a
    | Theorem (n, t, s)    -> mk_note s :: mk_theorem n t :: a 
-   | Qed s                -> mk_note s :: mk_qed :: a
+   | Qed s                -> (* mk_note s :: *) mk_qed :: a
    | Id s                 -> mk_note s :: cont sep (mk_id :: a)
    | Intros (c, ns, s)    -> mk_note s :: cont sep (mk_intros c ns :: a)
    | Cut (n, t, s)        -> mk_note s :: cont sep (mk_cut n t :: a)
index 49a5a1ab7cc5d3c48e6a9b9a15a04aca4d0f122f..8334ccfb62e65aac3e4162731b23d2b3078b5597 100644 (file)
@@ -772,7 +772,7 @@ let parse uri filename =
   | Getter_failure _ as exn ->
       raise exn
   | exn ->
-      raise (Parser_failure ("uncaught exception: " ^ Printexc.to_string exn))
+      raise (Parser_failure ("CicParser: uncaught exception: " ^ Printexc.to_string exn))
 
 (** {2 API implementation} *)
 
index 183fc5ec464ca725ccd4b6b54b591ad326478d70..d5fbf80343c42a413c718b27fa3bbc93baf1dfaf 100644 (file)
@@ -301,7 +301,7 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
       pp_tactical ~lazy_term_pp ~term_pp tac
       ^ pp_tactical ~lazy_term_pp ~term_pp punct
   | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac
-  | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
+  | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ ".\n"
                       
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
   function
index 2deef1bd53a24fc78bef7b0e5eb7ccf6bcd22b37..7e316879bc3415b56d5d74a056ad231ec48f877d 100644 (file)
@@ -118,7 +118,7 @@ let process_stream istream =
               (!char_count + x) (!char_count + y) msg)
         | exn ->
             prerr_endline
-              (sprintf "Uncaught exception: %s" (Printexc.to_string exn))
+              (sprintf "TestParser: Uncaught exception: %s" (Printexc.to_string exn))
        done
     with End_of_file -> ()
 
index 499c1705be978b97c7f9634ead475190e817e208..f1c1f496d200f41a15ea38171e25747e2e08042e 100644 (file)
@@ -159,7 +159,7 @@ let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
   let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = 
      try Cic2acic.acic_object_of_cic_object obj
      with e -> 
-        let msg = "Cic2ACic: " ^ Printexc.to_string e in
+        let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
        failwith msg
   in
   match style with
@@ -178,7 +178,7 @@ let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
         let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in
         let script = Acic2Procedural.acic2procedural 
           ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in
-       "\n\n" ^ String.concat "" (List.map aux script)
+       "\n" ^ String.concat "" (List.map aux script)
 
 let txt_of_inline_macro style suri prefix =
    let dbd = LibraryDb.instance () in   
@@ -191,4 +191,4 @@ let txt_of_inline_macro style suri prefix =
            Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
            (UriManager.string_of_uri uri) (Printexc.to_string e)
    in
-   String.concat "\n\n" (List.map map sorted_uris)
+   String.concat "" (List.map map sorted_uris)
index 2249998e9c09d06c8b1534aaeb0524a27ba5db04..be6546e8d237437e803f29558289be92929e1c8c 100644 (file)
 
 (* $Id$ *)
 
+module G = GrafiteAst
+
+(* from transcript *)
+
+let out_comment och s =
+   let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in 
+   Printf.fprintf och "%s%s%s\n\n" "(*" s "*)"
+
+let out_line_comment och s =
+   let l = 70 - String.length s in
+   let s = Printf.sprintf " %s %s" s (String.make l '*') in
+   out_comment och s
+
+let out_preamble och (path, lines) =
+   let ich = open_in path in
+   let rec print i =
+      if i > 0 then 
+         let s = input_line ich in
+         begin Printf.fprintf och "%s\n" s; print (pred i) end
+   in 
+   print lines;
+   out_line_comment och "This file was automatically generated: do not edit"
+
+(* from matitacLib *)
+
+let pp_ast_statement =
+  GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+    ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term)
+
+(**)
+
+let dump f =
+   let och = open_out f in
+   let atexit () = close_out och in
+   let rt_base_dir = Filename.dirname Sys.argv.(0) in
+   let path = Filename.concat rt_base_dir "matita.ma.templ" in
+   let lines = 14 in
+   out_preamble och (path, lines);
+   let grafite_parser_cb ast =
+      output_string och (LexiconAstPp.pp_command ast)
+   in
+   let matita_engine_cb = function
+      | G.Executable (_, G.Macro (_, G.Inline _)) -> ()
+      | ast                                                 ->
+         output_string och (pp_ast_statement ast)
+   in
+   let matitac_lib_cb = output_string och in
+(*   GrafiteParser.set_callback grafite_parser_cb; *)
+   MatitaEngine.set_callback matita_engine_cb;
+   MatitacLib.set_callback matitac_lib_cb;
+   at_exit atexit
+   
 let main () =
  match Filename.basename Sys.argv.(0) with
  |"gragrep"    |"gragrep.opt"    |"gragrep.opt.static"    ->Gragrep.main()
@@ -38,6 +90,8 @@ let main () =
 (*
       let _ = Paramodulation.Saturation.init () in  *)
 (* ALB to link paramodulation *)
+      let dump_msg = "<filename> Dump source with expanded macros to <filename>" in
+      MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg];
       let _ = MatitacLib.main `COMPILER in
       ()
 
index 52ad776e71d3a2fe91a07c5107b28dea21baa3ff..17cb2952c08a879c874566c2aea693fc5a191dc2 100644 (file)
@@ -78,7 +78,8 @@ let run_script is eval_function  =
   with
   | GrafiteEngine.Drop  
   | End_of_file
-  | CicNotationParser.Parse_error _ as exn -> raise exn
+  | CicNotationParser.Parse_error _ 
+  | GrafiteEngine.Macro _ as exn -> raise exn
   | exn -> 
       if not matita_debug then
        HLog.error (snd (MatitaExcPp.to_string exn)) ;
@@ -120,7 +121,15 @@ let clean_exit n =
       with GrafiteTypes.Option_error("baseuri", "not found") ->
        (* no baseuri ==> nothing to clean yet *)
        opt_exit n
-  
+
+let get_macro_context = function
+   | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
+   | Some status                ->
+      let stack = GrafiteTypes.get_stack status in
+      let goal = Continuationals.Stack.find_goal stack in
+      GrafiteTypes.get_proof_context status goal
+   | None                       -> assert false
+   
 let rec interactive_loop () = 
   let str = Ulexing.from_utf8_channel stdin in
   try
@@ -131,16 +140,16 @@ let rec interactive_loop () =
   with 
   | GrafiteEngine.Drop -> pp_ocaml_mode ()
   | GrafiteEngine.Macro (floc, f) ->
-      begin match snd (f []) with 
-       | GrafiteAst.Inline (_, style, suri, prefix) ->
+      begin match f (get_macro_context !grafite_status) with 
+       | _, GrafiteAst.Inline (_, style, suri, prefix) ->
          let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
-         !out str
-       | _ -> ()
-      end;
-      let x, y = HExtlib.loc_of_floc floc in
-      HLog.error
-       (sprintf "A macro has been found in a script at %d-%d" x y);
-      interactive_loop ()
+         !out str;
+        interactive_loop ()
+       | _ ->
+         let x, y = HExtlib.loc_of_floc floc in
+         HLog.error (sprintf "A macro has been found in a script at %d-%d" x y);
+         interactive_loop ()
+      end
   | Sys.Break -> HLog.error "user break!"; interactive_loop ()
   | GrafiteTypes.Command_error _ -> interactive_loop ()
   | End_of_file ->
@@ -215,6 +224,71 @@ let pp_times fname bench_mode rc big_bang =
     end
 ;;
 
+let rec compiler_loop fname big_bang mode buf =
+ let include_paths =
+  Helm_registry.get_list Helm_registry.string "matita.includes" in
+ let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in    
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
+ let bench_mode =  Helm_registry.get_bool "matita.bench" in
+ try
+  run_script buf 
+   (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
+    ~clean_baseuri)
+ with 
+  | End_of_file -> ()
+  | Sys.Break as exn ->
+     if matita_debug then raise exn;
+      HLog.error "user break!";
+      pp_times fname bench_mode false big_bang;
+      if mode = `COMPILER then
+        clean_exit (Some ~-1)
+      else
+        pp_ocaml_mode ()
+  | GrafiteEngine.Drop ->
+      if mode = `COMPILER then 
+        begin
+          pp_times fname bench_mode false big_bang;
+          clean_exit (Some 1)
+        end
+      else 
+        pp_ocaml_mode ()
+  | GrafiteEngine.Macro (floc, f) ->
+      begin match f (get_macro_context !grafite_status) with 
+       | _, GrafiteAst.Inline (_, style, suri, prefix) ->
+         let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+         !out str;
+         compiler_loop fname big_bang mode buf
+       | _ ->
+         let x, y = HExtlib.loc_of_floc floc in
+         HLog.error (sprintf "A macro has been found in a script at %d-%d" x y);
+         if mode = `COMPILER then
+           begin 
+              pp_times fname bench_mode false big_bang;
+              clean_exit (Some 1)
+            end 
+        else 
+            pp_ocaml_mode ()
+      end
+  | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+     let (x, y) = HExtlib.loc_of_floc floc in
+     HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
+     if mode = `COMPILER then
+       begin
+         pp_times fname bench_mode false big_bang;
+         clean_exit (Some 1)
+       end
+     else
+       pp_ocaml_mode ()
+  | exn ->
+      if matita_debug then raise exn;
+      if mode = `COMPILER then 
+        begin
+          pp_times fname bench_mode false big_bang;
+          clean_exit (Some 3)
+        end
+      else 
+        pp_ocaml_mode ()
+
 let main ~mode = 
   let big_bang = Unix.gettimeofday () in
   MatitaInit.initialize_all ();
@@ -241,25 +315,17 @@ let main ~mode =
   if Helm_registry.get_int "matita.verbosity" < 1 then
     HLog.set_log_callback newcb;
   if bench_mode then MatitaMisc.shutup ();
-  let matita_debug = Helm_registry.get_bool "matita.debug" in
-  try
     let time = Unix.time () in
     if Helm_registry.get_int "matita.verbosity" < 1 && not bench_mode then
       origcb `Message ("compiling " ^ Filename.basename fname ^ "...")
     else
       HLog.message (sprintf "execution of %s started:" fname);
-    let is =
-      Ulexing.from_utf8_channel
-        (match fname with
-        | "stdin" -> stdin
-        | fname -> open_in fname) in
-    let include_paths =
-     Helm_registry.get_list Helm_registry.string "matita.includes" in
-    (try
-      run_script is 
-       (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
-         ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")))
-     with End_of_file -> ());
+    let ich = match fname with
+     | "stdin" -> stdin
+     | fname -> open_in fname
+    in
+    let buf = Ulexing.from_utf8_channel ich in
+    compiler_loop fname big_bang mode buf;
     let elapsed = Unix.time () -. time in
     let tm = Unix.gmtime elapsed in
     let sec = string_of_int tm.Unix.tm_sec ^ "''" in
@@ -307,51 +373,3 @@ let main ~mode =
        pp_times fname bench_mode true big_bang;
        exit 0
      end
-  with 
-  | Sys.Break as exn ->
-     if matita_debug then raise exn;
-      HLog.error "user break!";
-      pp_times fname bench_mode false big_bang;
-      if mode = `COMPILER then
-        clean_exit (Some ~-1)
-      else
-        pp_ocaml_mode ()
-  | GrafiteEngine.Drop ->
-      if mode = `COMPILER then 
-        begin
-          pp_times fname bench_mode false big_bang;
-          clean_exit (Some 1)
-        end
-      else 
-        pp_ocaml_mode ()
-  | GrafiteEngine.Macro (floc,_) ->
-     let x, y = HExtlib.loc_of_floc floc in
-      HLog.error
-       (sprintf "A macro has been found in a script at %d-%d" x y);
-      if mode = `COMPILER then 
-        begin
-          pp_times fname bench_mode false big_bang;
-          clean_exit (Some 1)
-        end
-      else 
-        pp_ocaml_mode ()
-  | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
-     let (x, y) = HExtlib.loc_of_floc floc in
-     HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
-     if mode = `COMPILER then
-       begin
-         pp_times fname bench_mode false big_bang;
-         clean_exit (Some 1)
-       end
-     else
-       pp_ocaml_mode ()
-  | exn ->
-      if matita_debug then raise exn;
-      if mode = `COMPILER then 
-        begin
-          pp_times fname bench_mode false big_bang;
-          clean_exit (Some 3)
-        end
-      else 
-        pp_ocaml_mode ()
-