- some depend files fixed

- matitacLib: we peform a garbage collection after compiling every file instead of just .mma (let's see the times)
- transcript: support for "cr" inline param completed
- procedural: now record are supported

the records of logic/cprop_coonectives.ma are now reconstructed :)

logic higher_order_defs list nat Z Q are now fully reconstructed :))

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 2fec2dd1f9b2bb996c5a2e26a3bdd7552fbeed29..63b4d4972281d0c5f5822cf4555ee54b86ff56ee 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -57,6 +57,11 @@ let get_flavour sorts params context v attrs =
       | Some fl -> fl
       | None    -> aux attrs
 
+let rec is_record = function
+   | []                           -> None
+   | `Class (`Record fields) :: _ -> Some fields
+   | _ :: tl                      -> is_record tl
+
 let proc_obj ?(info="") proc_proof sorts params context = function
    | C.AConstant (_, _, s, Some v, t, [], attrs)         ->
       begin match get_flavour sorts params context v attrs with
@@ -79,7 +84,10 @@ let proc_obj ?(info="") proc_proof sorts params context = function
    | C.AConstant (_, _, s, None, t, [], attrs)           ->
       [T.Statement (`Axiom, Some s, t, None, "")]
    | C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
-      [T.Inductive (types, lpsno, "")] 
+      begin match is_record attrs with
+         | None    -> [T.Inductive (types, lpsno, "")]
+        | Some fs -> [T.Record (types, lpsno, fs, "")]
+      end
    | _                                          ->
       failwith "not a theorem, definition, axiom or inductive type"
 

diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml
index 402ef54fe7d2a03e0ee72c3ec6c74f8557ff7d74..5f4d8d150d0cff31f3e2dbe3018d6553412b186e 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTeX.ml
+++ b/helm/software/components/acic_procedural/proceduralTeX.ml
@@ -231,6 +231,7 @@ let rec xl frm = function
       F.fprintf frm "\\Elim{%a}{%a}{}{}{%a}" xat v xat t xl l
    | T.Cut (r, w, _) :: T.Branch ([l1; [T.Id _]], _) :: l2 ->
       F.fprintf frm "\\Cut{%a}{%a}{%a}{%a}" xx r xat w xl l1 xl l2
+   | T.Record _ :: _                                       -> assert false
    | T.Inductive _ :: _                                    -> assert false
    | T.Id _ :: _                                           -> assert false
    | T.Clear _ :: _                                        -> assert false

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 55516bf34aebd02241badb49501372493227f511..8cf705d0a1c098ca87375397799d1997a147b400 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -68,8 +68,10 @@ type pattern  = C.annterm
 type body     = C.annterm option
 type types    = C.anninductiveType list
 type lpsno    = int
+type fields   = (string * bool * int) list
 
 type step = Note of note 
+          | Record of types * lpsno * fields * note
           | Inductive of types * lpsno * note
          | Statement of flavour * name * what * body * note
           | Qed of note
@@ -134,7 +136,7 @@ let mk_notenote str a =
 let mk_thnote str a =
    if str = "" then a else mk_note "" :: mk_note str :: a
 
-let mk_inductive types lpsno =
+let mk_pre_inductive types lpsno =
    let map1 (lps1, cons) (name, arity) = 
       let lps2, arity = strip_lps lpsno arity in
       merge_lps lps1 lps2, (name, arity) :: cons
@@ -146,10 +148,29 @@ let mk_inductive types lpsno =
    in
    let map3 (name, xw) = arel_of_name name, xw in
    let rev_lps, rev_types = List.fold_left map2 ([], []) types in
-   let lpars, types = List.rev_map map3 rev_lps, List.rev rev_types in
+   List.rev_map map3 rev_lps, List.rev rev_types
+
+let mk_inductive types lpsno =
+   let lpars, types = mk_pre_inductive types lpsno in
    let obj = N.Inductive (lpars, types) in
    G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
 
+let mk_record types lpsno fields =
+   match mk_pre_inductive types lpsno with
+      | lpars, [name, _, ty, [_, cty]] -> 
+         let map (fields, cty) (name, coercion, arity) =
+           match cty with
+              | C.AProd (_, _, w, t) ->
+                 (name, w, coercion, arity) :: fields, t
+              | _                    ->
+                 assert false
+        in
+        let rev_fields, _ = List.fold_left map ([], cty) fields in 
+        let fields = List.rev rev_fields in
+        let obj = N.Record (lpars, name, ty, fields) in
+         G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
+      | _ -> assert false
+
 let mk_statement flavour name t v =
    let name = match name with Some name -> name | None -> assert false in
    let obj = N.Theorem (flavour, name, t, v) in
@@ -247,7 +268,8 @@ let mk_vb = G.Shift floc
 let rec render_step sep a = function
    | Note s                    -> mk_notenote s a
    | Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a 
-   | Inductive (lps, ts, s)    -> mk_inductive lps ts :: mk_thnote s a
+   | Inductive (ts, lps, s)    -> mk_inductive ts lps :: mk_thnote s a
+   | Record (ts, lps, fs, s)   -> mk_record ts lps fs :: mk_thnote s a
    | Qed s                     -> mk_qed :: mk_tacnote s a
    | Exact (t, s)              -> mk_exact t sep :: mk_tacnote s a   
    | Id s                      -> mk_id sep :: mk_tacnote s a
@@ -310,6 +332,7 @@ let count = I.count_nodes ~meta:false
 
 let rec count_node a = function
    | Note _
+   | Record _
    | Inductive _
    | Statement _
    | Qed _   
@@ -336,6 +359,7 @@ let rec note_of_step = function
    | Note s
    | Statement (_, _, _, _, s)
    | Inductive (_, _, s)
+   | Record (_, _, _, s)
    | Qed s
    | Exact (_, s)
    | Id s

diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli
index 34c7ba670216e332a02711e7b0c112d67a7991e2..a1d28e966c2c8428116fbd2be067bb808da101bc 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.mli
+++ b/helm/software/components/acic_procedural/proceduralTypes.mli
@@ -47,8 +47,10 @@ type pattern  = Cic.annterm
 type body     = Cic.annterm option
 type types    = Cic.anninductiveType list
 type lpsno    = int
+type fields   = (string * bool * int) list
 
 type step = Note of note 
+          | Record of types * lpsno * fields * note
           | Inductive of types * lpsno * note
           | Statement of flavour * name * what * body * note
           | Qed of note

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index 39086d53fa86a4b7f3e89152be122f384366bbd4..da07dd235489890fa39b5ec31d2aa3e47bcdb415 100644 (file)
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -201,9 +201,10 @@ let make_script_name st script name =
 let get_iparams st name =
    let debug debug = GA.IPDebug debug in
    let map = function
+      | "comments"   -> GA.IPComments
       | "nodefaults" -> GA.IPNoDefaults
       | "coercions"  -> GA.IPCoercions
-      | "comments"   -> GA.IPComments
+      | "cr"         -> GA.IPCR
       | s            -> 
         try Scanf.sscanf s "debug-%u" debug with
            | Scanf.Scan_failure _

diff --git a/helm/software/components/extlib/.depend.opt b/helm/software/components/extlib/.depend.opt
index 3f72e1d248c45af35b871360f1b6e5e47d6363b7..6d96e61e208bef26caadc6f9c5f7c049cf588648 100644 (file)
--- a/helm/software/components/extlib/.depend.opt
+++ b/helm/software/components/extlib/.depend.opt
@@ -1,12 +1,3 @@
-componentsConf.cmi: 
-hExtlib.cmi: 
-hMarshal.cmi: 
-patternMatcher.cmi: 
-hLog.cmi: 
-trie.cmi: 
-hTopoSort.cmi: 
-refCounter.cmi: 
-graphvizPp.cmi: 
 componentsConf.cmo: componentsConf.cmi 
 componentsConf.cmx: componentsConf.cmi 
 hExtlib.cmo: hExtlib.cmi 

diff --git a/helm/software/components/ng_cic_content/.depend b/helm/software/components/ng_cic_content/.depend
index 1316c8eab83e4c08ca7047ed72175492e98197a1..b4e17fa99bca931a5289d06541f5b69060d11594 100644 (file)
--- a/helm/software/components/ng_cic_content/.depend
+++ b/helm/software/components/ng_cic_content/.depend
@@ -1,5 +1,3 @@
-ncic2astMatcher.cmi: 
-nTermCicContent.cmi: 
 ncic2astMatcher.cmo: ncic2astMatcher.cmi 
 ncic2astMatcher.cmx: ncic2astMatcher.cmi 
 nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi 

diff --git a/helm/software/components/ng_cic_content/.depend.opt b/helm/software/components/ng_cic_content/.depend.opt
index 1316c8eab83e4c08ca7047ed72175492e98197a1..b4e17fa99bca931a5289d06541f5b69060d11594 100644 (file)
--- a/helm/software/components/ng_cic_content/.depend.opt
+++ b/helm/software/components/ng_cic_content/.depend.opt
@@ -1,5 +1,3 @@
-ncic2astMatcher.cmi: 
-nTermCicContent.cmi: 
 ncic2astMatcher.cmo: ncic2astMatcher.cmi 
 ncic2astMatcher.cmx: ncic2astMatcher.cmi 
 nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi 

diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend
index cf6dcda021130aa471c118cc2e6035425bc7239a..666cba23e955cea150f8f54ef68a9ad1f6941244 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend
+++ b/helm/software/components/ng_paramodulation/.depend
@@ -1,4 +1,3 @@
-terms.cmi: 
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
@@ -8,7 +7,6 @@ foUnif.cmi: terms.cmi
 superposition.cmi: terms.cmi index.cmi 
 nCicBlob.cmi: terms.cmi 
 cicBlob.cmi: terms.cmi 
-paramod.cmi: 
 terms.cmo: terms.cmi 
 terms.cmx: terms.cmi 
 pp.cmo: terms.cmi pp.cmi 
@@ -31,7 +29,7 @@ nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi
 nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi 
 cicBlob.cmo: terms.cmi cicBlob.cmi 
 cicBlob.cmx: terms.cmx cicBlob.cmi 
-paramod.cmo: superposition.cmi pp.cmi nCicBlob.cmi index.cmi foUtils.cmi \
-    foUnif.cmi paramod.cmi 
-paramod.cmx: superposition.cmx pp.cmx nCicBlob.cmx index.cmx foUtils.cmx \
-    foUnif.cmx paramod.cmi 
+paramod.cmo: terms.cmi superposition.cmi pp.cmi nCicBlob.cmi index.cmi \
+    foUtils.cmi foUnif.cmi paramod.cmi 
+paramod.cmx: terms.cmx superposition.cmx pp.cmx nCicBlob.cmx index.cmx \
+    foUtils.cmx foUnif.cmx paramod.cmi 

diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt
index cf6dcda021130aa471c118cc2e6035425bc7239a..666cba23e955cea150f8f54ef68a9ad1f6941244 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend.opt
+++ b/helm/software/components/ng_paramodulation/.depend.opt
@@ -1,4 +1,3 @@
-terms.cmi: 
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
@@ -8,7 +7,6 @@ foUnif.cmi: terms.cmi
 superposition.cmi: terms.cmi index.cmi 
 nCicBlob.cmi: terms.cmi 
 cicBlob.cmi: terms.cmi 
-paramod.cmi: 
 terms.cmo: terms.cmi 
 terms.cmx: terms.cmi 
 pp.cmo: terms.cmi pp.cmi 
@@ -31,7 +29,7 @@ nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi
 nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi 
 cicBlob.cmo: terms.cmi cicBlob.cmi 
 cicBlob.cmx: terms.cmx cicBlob.cmi 
-paramod.cmo: superposition.cmi pp.cmi nCicBlob.cmi index.cmi foUtils.cmi \
-    foUnif.cmi paramod.cmi 
-paramod.cmx: superposition.cmx pp.cmx nCicBlob.cmx index.cmx foUtils.cmx \
-    foUnif.cmx paramod.cmi 
+paramod.cmo: terms.cmi superposition.cmi pp.cmi nCicBlob.cmi index.cmi \
+    foUtils.cmi foUnif.cmi paramod.cmi 
+paramod.cmx: terms.cmx superposition.cmx pp.cmx nCicBlob.cmx index.cmx \
+    foUtils.cmx foUnif.cmx paramod.cmi 

diff --git a/helm/software/matita/.depend.opt b/helm/software/matita/.depend.opt
index 04e44bc25f20dba600367399370755c8f11ef372..e4454794f0d927126eb152f9ace60111645d47c0 100644 (file)
--- a/helm/software/matita/.depend.opt
+++ b/helm/software/matita/.depend.opt
@@ -10,10 +10,10 @@ matitaAutoGui.cmx: matitaGtkMisc.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
     applyTransformation.cmx matitaAutoGui.cmi 
 matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi 
 matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi 
-matitacLib.cmo: matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmx \
-    applyTransformation.cmi matitacLib.cmi 
-matitacLib.cmx: matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \
-    applyTransformation.cmx matitacLib.cmi 
+matitacLib.cmo: matitaMisc.cmi matitaExcPp.cmi matitaEngine.cmi \
+    buildTimeConf.cmx applyTransformation.cmi matitacLib.cmi 
+matitacLib.cmx: matitaMisc.cmx matitaExcPp.cmx matitaEngine.cmx \
+    buildTimeConf.cmx applyTransformation.cmx matitacLib.cmi 
 matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaWiki.cmx \
     matitaMisc.cmi matitaInit.cmi 
 matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaWiki.cmx \

diff --git a/helm/software/matita/contribs/procedural/library/library.conf.xml b/helm/software/matita/contribs/procedural/library/library.conf.xml
index e7d7717fc7b60c83d3716c7785894fb7048b4a5f..c22bca606f4d55a4ddb5592ddd343fec8310e9d5 100644 (file)
--- a/helm/software/matita/contribs/procedural/library/library.conf.xml
+++ b/helm/software/matita/contribs/procedural/library/library.conf.xml
@@ -11,12 +11,13 @@
     <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">* debug-6</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>
     <key name="inline">logic/equality/eq_f nodefaults</key>
     <key name="inline">logic/equality/eq_f' nodefaults</key>
-    <key name="inline">Z/plus/eq_plus_Zplus nocoercions</key>
+    <key name="inline">Z/plus/eq_plus_Zplus coercions</key>
+    <key name="inline">Z/times/Ztimes_Zplus_pos_neg_pos cr</key>
   </section>
 </helm_registry>

diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang
index ed1d5650b42cafe37ef6db42e88e0b7cd5cccd01..2f71b5f7e5ae91bc7d68adbcee21a12c50efbdec 100644 (file)
--- a/helm/software/matita/matita.lang
+++ b/helm/software/matita/matita.lang
@@ -189,6 +189,7 @@
     <keyword>coercions</keyword>
     <keyword>comments</keyword>
     <keyword>debug</keyword>
+    <keyword>cr</keyword>
   </keyword-list>
   
   <keyword-list _name = "Whelp Macro" style = "Others 3"

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 637bea9897270f274e388da7d2899d1024a01af8..1276300b10bd117d367ade15f9a95ab6c840cc44 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -397,7 +397,7 @@ module F =
             Printf.printf "rm %s\n" generated; flush stdout; r
          end
       else
-         compile ignore options fname
+         compact (compile ignore options fname)
     ;;
 
     let load_deps_file = Librarian.load_deps_file;;