From 86cced899859b1730a4789d3ba0db71d21a37604 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 9 Feb 2007 17:27:31 +0000 Subject: [PATCH] added option -dump to matitac for persistent macro expansion --- .../acic_procedural/acic2Procedural.ml | 4 +- .../acic_procedural/proceduralTypes.ml | 2 +- helm/software/components/cic/cicParser.ml | 2 +- .../components/grafite/grafiteAstPp.ml | 2 +- .../components/grafite_parser/test_parser.ml | 2 +- helm/software/matita/applyTransformation.ml | 6 +- helm/software/matita/matitac.ml | 54 ++++++ helm/software/matita/matitacLib.ml | 164 ++++++++++-------- 8 files changed, 154 insertions(+), 82 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index adfe4b05c..e26dd68a2 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -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) diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index 95fdc6e56..53605271d 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -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) diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml index 49a5a1ab7..8334ccfb6 100644 --- a/helm/software/components/cic/cicParser.ml +++ b/helm/software/components/cic/cicParser.ml @@ -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} *) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 183fc5ec4..d5fbf8034 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -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 diff --git a/helm/software/components/grafite_parser/test_parser.ml b/helm/software/components/grafite_parser/test_parser.ml index 2deef1bd5..7e316879b 100644 --- a/helm/software/components/grafite_parser/test_parser.ml +++ b/helm/software/components/grafite_parser/test_parser.ml @@ -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 -> () diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 499c1705b..f1c1f496d 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -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) diff --git a/helm/software/matita/matitac.ml b/helm/software/matita/matitac.ml index 2249998e9..be6546e8d 100644 --- a/helm/software/matita/matitac.ml +++ b/helm/software/matita/matitac.ml @@ -25,6 +25,58 @@ (* $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 = " Dump source with expanded macros to " in + MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg]; let _ = MatitacLib.main `COMPILER in () diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 52ad776e7..17cb2952c 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -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 () - -- 2.39.2