From 951e8fda6fbef9b4149e37e4d406b2f82fd64a98 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 11 Jun 2009 12:59:35 +0000 Subject: [PATCH] - 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 :)) --- .../acic_procedural/acic2Procedural.ml | 10 ++++++- .../acic_procedural/proceduralTeX.ml | 1 + .../acic_procedural/proceduralTypes.ml | 30 +++++++++++++++++-- .../acic_procedural/proceduralTypes.mli | 2 ++ .../components/binaries/transcript/engine.ml | 3 +- helm/software/components/extlib/.depend.opt | 9 ------ .../components/ng_cic_content/.depend | 2 -- .../components/ng_cic_content/.depend.opt | 2 -- .../components/ng_paramodulation/.depend | 10 +++---- .../components/ng_paramodulation/.depend.opt | 10 +++---- helm/software/matita/.depend.opt | 8 ++--- .../procedural/library/library.conf.xml | 5 ++-- helm/software/matita/matita.lang | 1 + helm/software/matita/matitacLib.ml | 2 +- 14 files changed, 58 insertions(+), 37 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 2fec2dd1f..63b4d4972 100644 --- 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 402ef54fe..5f4d8d150 100644 --- 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 55516bf34..8cf705d0a 100644 --- 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 34c7ba670..a1d28e966 100644 --- 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 39086d53f..da07dd235 100644 --- 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 3f72e1d24..6d96e61e2 100644 --- 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 1316c8eab..b4e17fa99 100644 --- 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 1316c8eab..b4e17fa99 100644 --- 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 cf6dcda02..666cba23e 100644 --- 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 cf6dcda02..666cba23e 100644 --- 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 04e44bc25..e4454794f 100644 --- 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 e7d7717fc..c22bca606 100644 --- a/helm/software/matita/contribs/procedural/library/library.conf.xml +++ b/helm/software/matita/contribs/procedural/library/library.conf.xml @@ -11,12 +11,13 @@ procedural 14 - * debug-2 + * debug-6 logic/equality/symmetric_eq nodefaults logic/equality/transitive_eq nodefaults logic/equality/eq_elim_r nodefaults logic/equality/eq_f nodefaults logic/equality/eq_f' nodefaults - Z/plus/eq_plus_Zplus nocoercions + Z/plus/eq_plus_Zplus coercions + Z/times/Ztimes_Zplus_pos_neg_pos cr diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index ed1d5650b..2f71b5f7e 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -189,6 +189,7 @@ coercions comments debug + cr