- 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)

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 68c88496ba91fbfe3e735a0264f2eb9be266b166..9152d7a436234d68eb7bb29776ed7e5b21268af0 100644 (file)
--- 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 cca20ba5f805e6837c52c960208b7a9fa71554d5..786f6007384b113f877cbc52f32f3bf193043321 100644 (file)
--- 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 a51d3f0c2bd9df07bd5d769a3b083dc18ea793a4..c55a1d19c70697c2528d487c6c05162e4c662d2a 100644 (file)
--- 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 8016d71cfa3c0f932206c442a9cd32b794d392e2..fb80abbb0fdef6d3eb926e299240104cd52f994a 100644 (file)
--- 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 fa36624b2b2adb2bc7cbb07b15cfd87b5d4a467a..eab659fafff729916a8240820d888e41372aea2d 100644 (file)
--- 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 c92b71512e05ffdb47432702cae54e31887011e2..b66146b2ea9e375ea9b729b3eee5c9c9d7658ff6 100644 (file)
--- 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 00f6c978982b5f7904f30a098c2eb699a401cd94..2544adb5d0deaec128f9d842a0768176f0a61e30 100644 (file)
--- 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 25e67131fca0487c4390d310d8307722b5058067..f3c6a8bd17a7351e99ce8e59905fda76a37cbf08 100644 (file)
--- 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 4015293a435907f7a24f29f20b5824fb14e05cc1..f5f279e73dd55d6c819083562cfc6d16c39bdc64 100644 (file)
--- 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 92225d77d00f07406c59c65995592e45d5d80e4b..a169ea049f0882ffc6208c34a952e773bb4a9884 100644 (file)
--- 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 51e8b568b0baa9fde7b9afb3cbbbc7e5d33d5ac9..e7d7717fc7b60c83d3716c7785894fb7048b4a5f 100644 (file)
--- a/helm/software/matita/contribs/procedural/library/library.conf.xml
+++ b/helm/software/matita/contribs/procedural/library/library.conf.xml
@@ -11,6 +11,7 @@
     <key name="output_type">procedural</key>    
     <key name="heading_lines">14</key>
     <key name="theory_file"></key>
+    <key name="inline">* debug-2</key>
     <key name="inline">logic/equality/symmetric_eq nodefaults</key>
     <key name="inline">logic/equality/transitive_eq nodefaults</key>
     <key name="inline">logic/equality/eq_elim_r nodefaults</key>