From 14e2489ae86ecb6467fe9a7ba3b742a8d53c47ea Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 9 Jun 2009 17:22:52 +0000 Subject: [PATCH] - Procedural: more support for the Debug inline option (does not work yet) - transcript: now we can process a given subset so the source files - termContentPres: bugfix in the syntax of letrec, a space was missing :( now nat/generic_iter_p.ma is fully reconstructed :) (thx Claudio) --- .../acic_procedural/acic2Procedural.ml | 5 +++++ .../acic_procedural/acic2Procedural.mli | 2 ++ .../components/binaries/transcript/engine.ml | 21 +++++++++++++------ .../components/binaries/transcript/engine.mli | 2 ++ .../components/binaries/transcript/options.ml | 2 ++ .../components/binaries/transcript/top.ml | 9 ++++++-- .../content_pres/termContentPres.ml | 2 +- .../components/syntax_extensions/.depend | 3 --- helm/software/matita/applyTransformation.ml | 13 +++++++----- .../contribs/procedural/Makefile.common | 6 ++++++ .../procedural/library/library.conf.xml | 1 + 11 files changed, 49 insertions(+), 17 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 68c88496b..9152d7a43 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -134,3 +134,8 @@ let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params in HLog.debug "Procedural: grafite rendering"; List.rev (T.render_steps [] steps) + +let rec is_debug n = function + | [] -> false + | G.IPDebug debug :: _ -> debug <= n + | _ :: tl -> is_debug n tl diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli index cca20ba5f..786f60073 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.mli +++ b/helm/software/components/acic_procedural/acic2Procedural.mli @@ -40,3 +40,5 @@ val procedural_of_acic_term: GrafiteAst.statement list val tex_formatter: Format.formatter option ref + +val is_debug: int -> GrafiteAst.inline_param list -> bool diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index a51d3f0c2..c55a1d19c 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -28,8 +28,8 @@ module X = HExtlib module HG = Http_getter module GA = GrafiteAst -module T = Types -module G = Grafite +module T = Types +module G = Grafite module O = Options type script = { @@ -66,8 +66,9 @@ let default_script = { let default_scripts = 2 +let suffix = ".conf.xml" + let load_registry registry = - let suffix = ".conf.xml" in let registry = if Filename.check_suffix registry suffix then registry else registry ^ suffix @@ -84,8 +85,10 @@ let set_files st = | None -> List.rev files | Some l -> let l = trim l in - if List.mem l st.excludes then aux files else aux (l :: files) - in + if List.mem l st.excludes then aux files else + if !O.sources = [] || List.mem l !O.sources then aux (l :: files) else + aux files + in let files = aux [] in let _ = Unix.close_process_in ich in {st with files = files} @@ -196,11 +199,17 @@ let make_script_name st script name = Filename.concat st.output_path (name ^ ext) let get_iparams st name = + let debug debug = GA.IPDebug debug in let map = function | "nodefaults" -> GA.IPNoDefaults | "coercions" -> GA.IPCoercions | "comments" -> GA.IPComments - | s -> failwith ("unknown inline parameter: " ^ s) + | s -> + try Scanf.sscanf s "debug-%u" debug with + | Scanf.Scan_failure _ + | Failure _ + | End_of_file -> + failwith ("unknown inline parameter: " ^ s) in List.map map (X.list_assoc_all name st.iparams) diff --git a/helm/software/components/binaries/transcript/engine.mli b/helm/software/components/binaries/transcript/engine.mli index 8016d71cf..fb80abbb0 100644 --- a/helm/software/components/binaries/transcript/engine.mli +++ b/helm/software/components/binaries/transcript/engine.mli @@ -25,6 +25,8 @@ type status +val suffix: string + val init: unit -> unit val make: string -> status diff --git a/helm/software/components/binaries/transcript/options.ml b/helm/software/components/binaries/transcript/options.ml index fa36624b2..eab659faf 100644 --- a/helm/software/components/binaries/transcript/options.ml +++ b/helm/software/components/binaries/transcript/options.ml @@ -34,3 +34,5 @@ let verbose_escape = ref false let comments = ref true let getter = ref false + +let sources = ref ([]: string list) diff --git a/helm/software/components/binaries/transcript/top.ml b/helm/software/components/binaries/transcript/top.ml index c92b71512..b66146b2e 100644 --- a/helm/software/components/binaries/transcript/top.ml +++ b/helm/software/components/binaries/transcript/top.ml @@ -32,7 +32,12 @@ let main = let help_p = " verbose parsing" in let help_x = " verbose character escaping" in let set_cwd dir = Options.cwd := dir; Engine.init () in - let process_package package = Engine.produce (Engine.make package) in + let process_file file = + if Sys.file_exists file || Sys.file_exists (file ^ Engine.suffix) then + begin Engine.produce (Engine.make file); Options.sources := [] end + else + Options.sources := file :: !Options.sources + in Arg.parse [ ("-C", Arg.String set_cwd, help_C); ("-g", Arg.Set Options.getter, help_g); @@ -40,4 +45,4 @@ let main = ("-m", Arg.Clear Options.comments, help_m); ("-p", Arg.Set Options.verbose_parser, help_p); ("-x", Arg.Set Options.verbose_escape, help_x); - ] process_package help + ] process_file help diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 00f6c9789..2544adb5d 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -239,7 +239,7 @@ let pp_ast0 t k = (fun (params, name, ty, body, rec_param) -> [ break; hvbox false true ([ - keyword "and"; + keyword "and"; space; name] @ params @ [space; keyword "on" ; space; rec_param ;space ] @ diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 4015293a4..f5f279e73 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -46,6 +46,7 @@ module LS = LibrarySync module Ds = CicDischarge module PO = ProceduralOptimizer module N = CicNotationPt +module A2P = Acic2Procedural let mpres_document pres_box = Xml.add_xml_declaration (CicNotationPres.print_box pres_box) @@ -213,10 +214,12 @@ let txt_of_cic_object failwith msg in if List.mem G.IPProcedural params then begin -(* - PO.debug := true; + + Procedural2.debug := A2P.is_debug 1 params; + PO.debug := A2P.is_debug 2 params; +(* PO.critical := false; - Acic2Procedural.tex_formatter := Some Format.std_formatter; + A2P.tex_formatter := Some Format.std_formatter; let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in *) let obj, info = PO.optimize_obj obj in @@ -259,7 +262,7 @@ let txt_of_cic_object str in let script = - Acic2Procedural.procedural_of_acic_object + A2P.procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ~info params aobj in String.concat "" (List.map aux script) ^ "\n\n" @@ -387,7 +390,7 @@ let procedural_txt_of_cic_term ~map_unicode_to_tex n params context term = let aux = GrafiteAstPp.pp_statement ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in let script = - Acic2Procedural.procedural_of_acic_term + A2P.procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params context annterm in String.concat "" (List.map aux script) diff --git a/helm/software/matita/contribs/procedural/Makefile.common b/helm/software/matita/contribs/procedural/Makefile.common index 92225d77d..a169ea049 100644 --- a/helm/software/matita/contribs/procedural/Makefile.common +++ b/helm/software/matita/contribs/procedural/Makefile.common @@ -53,3 +53,9 @@ endif mma: $(DEVEL).conf.xml clean.ma $(H)$(TRANSCRIPT) $(TRANSCRIPTOPTIONS) -C $(BIN) $(DEVEL) + +%.ts: $(DEVEL).conf.xml + $(H)$(BIN)matitaclean.opt $(MATITAOPTIONS) $*.ma + $(H)$(RM) $*.ma + $(H)$(TRANSCRIPT) $(TRANSCRIPTOPTIONS) -C $(BIN) $* $(DEVEL) + diff --git a/helm/software/matita/contribs/procedural/library/library.conf.xml b/helm/software/matita/contribs/procedural/library/library.conf.xml index 51e8b568b..e7d7717fc 100644 --- a/helm/software/matita/contribs/procedural/library/library.conf.xml +++ b/helm/software/matita/contribs/procedural/library/library.conf.xml @@ -11,6 +11,7 @@ procedural 14 + * debug-2 logic/equality/symmetric_eq nodefaults logic/equality/transitive_eq nodefaults logic/equality/eq_elim_r nodefaults -- 2.39.2