From 93cc2a2254a2620000377dfc99a7aaedf2b8ec63 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 21 Apr 2009 19:49:59 +0000 Subject: [PATCH] - MatitaMisc: we factorized here the function out_preamble used in matitadep and MatitacLib - ApplyTransformation: we moved some "\n" hoping in a better rendering :) - matitadep: we now generate a "theory" file (dfault name "theory.ma" but can - MatitaMisc: we factorized here the function out_preamble used in matitadep and MatitacLib - ApplyTransformation: we moved some "\n" hoping in a better rendering :) - matitadep: we now generate a "theory" file (dfault name "theory.ma" but can be changed via the -theory cmdline option) that includes all the files of the devel so the devel itself can be included just including the theory file. To speed up the inclusion process, only the "top level" files are included (inclusion seems slow anyway) - procedural/Makefile.common: new entries for single file compilation - procedural/library: better preamble including library/theory.ma. Now the devel should be reconstructed with the correct notation - power_derivative.ma: we definitely do not want 'x' as a keyword in a serious file. All files including it (for intance its reconstructed version) can not use 'x' as an identifier. For now we replaced 'x' with 'X' - transcript: bug fix in obtaining the list of files to be processed --- .../components/binaries/transcript/engine.ml | 17 ++-- helm/software/matita/applyTransformation.ml | 4 +- .../contribs/procedural/Makefile.common | 11 +++ .../contribs/procedural/library/preamble.ma | 19 +---- .../matita/library/demo/power_derivative.ma | 64 ++++++++------- helm/software/matita/library/depends | 2 + helm/software/matita/library/theory.ma | 78 +++++++++++++++++++ helm/software/matita/matitaMisc.ml | 25 +++++- helm/software/matita/matitaMisc.mli | 3 + helm/software/matita/matitacLib.ml | 26 +------ helm/software/matita/matitadep.ml | 35 ++++++++- 11 files changed, 200 insertions(+), 84 deletions(-) create mode 100644 helm/software/matita/library/theory.ma diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 027b03575..2e81186ea 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -50,6 +50,7 @@ type status = { output_type: T.output_kind; input_ext: string; remove_lines: int; + excludes: string list; includes: (string * string) list; coercions: (string * string) list; files: string list; @@ -75,12 +76,13 @@ let load_registry registry = let set_files st = let eof ich = try Some (input_line ich) with End_of_file -> None in let trim l = Filename.chop_extension (Str.string_after l 2) in - let cmd = Printf.sprintf "cd %s && find -name *%s" st.input_path st.input_ext in + let cmd = Printf.sprintf "cd %s && find -name '*%s'" st.input_path st.input_ext in let ich = Unix.open_process_in cmd in - let rec aux files = - match eof ich with - | None -> List.rev files - | Some l -> aux (trim l :: files) + let rec aux files = match eof ich with + | 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 let files = aux [] in let _ = Unix.close_process_in ich in @@ -116,6 +118,10 @@ let make registry = in load_registry registry; let input_type, input_ext = get_input_type "package.input_type" in + let excludes = match input_type with + | T.Grafite -> ["theory"] + | T.Gallina8 -> [] + in let st = { heading_path = R.get_string "transcript.heading_path"; heading_lines = R.get_int "transcript.heading_lines"; @@ -129,6 +135,7 @@ let make registry = output_type = get_output_type "package.output_type"; input_ext = input_ext; remove_lines = R.get_int "package.heading_lines"; + excludes = excludes; includes = get_pairs "package.include"; coercions = get_pairs "package.coercion"; files = []; diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index c504996e0..21b841f41 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -205,11 +205,11 @@ let txt_of_cic_object Content2pres.content2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj in - remove_closed_substs ("\n\n" ^ + remove_closed_substs ( BoxPp.render_to_string ~map_unicode_to_tex (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) - ) + ^ "\n\n" ) | G.Procedural depth -> (* PO.critical := false; diff --git a/helm/software/matita/contribs/procedural/Makefile.common b/helm/software/matita/contribs/procedural/Makefile.common index 7fdf63830..9d322ddc0 100644 --- a/helm/software/matita/contribs/procedural/Makefile.common +++ b/helm/software/matita/contribs/procedural/Makefile.common @@ -17,6 +17,17 @@ $(DIR) all: $(DIR).opt opt all.opt: $(H)$(RM) $(LOG) $(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2>> $(LOG) + +%.ma %.mma: + $(H)$(RM) $(LOG) + $(H)$(BIN)matitac $(MATITAOPTIONS) $@ 2>> $(LOG) +%.ma.opt: + $(H)$(RM) $(LOG) + $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.ma 2>> $(LOG) +%.mma.opt: + $(H)$(RM) $(LOG) + $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.mma 2>> $(LOG) + clean: $(H)$(BIN)matitaclean $(MATITAOPTIONS) $(H)$(RM) $(MAS) diff --git a/helm/software/matita/contribs/procedural/library/preamble.ma b/helm/software/matita/contribs/procedural/library/preamble.ma index 5bad82685..df40a272f 100644 --- a/helm/software/matita/contribs/procedural/library/preamble.ma +++ b/helm/software/matita/contribs/procedural/library/preamble.ma @@ -12,21 +12,4 @@ (* *) (**************************************************************************) -default "true" cic:/matita/logic/connectives/True.ind. - -default "false" cic:/matita/logic/connectives/False.ind. - -default "absurd" cic:/matita/logic/connectives/absurd.con. - -default "equality" - cic:/matita/logic/equality/eq.ind - cic:/matita/logic/equality/sym_eq.con - cic:/matita/logic/equality/transitive_eq.con - cic:/matita/logic/equality/eq_ind.con - cic:/matita/logic/equality/eq_elim_r.con - cic:/matita/logic/equality/eq_rec.con - cic:/matita/logic/equality/eq_elim_r'.con - cic:/matita/logic/equality/eq_rect.con - cic:/matita/logic/equality/eq_elim_r''.con - cic:/matita/logic/equality/eq_f.con - cic:/matita/logic/equality/eq_OF_eq.con. +include "../../../library/theory.ma". diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index 10cb21835..bca5bbf01 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -209,40 +209,44 @@ for @{ 'derivative $f }. interpretation "Rderivative" 'derivative f = (derivative f). -notation "hvbox('x' \sup n)" +(* FG: we definitely do not want 'x' as a keyward! + * Any file that includes this one can not use 'x' as an identifier + *) +notation "hvbox('X' \sup n)" non associative with precedence 60 for @{ 'monomio $n }. -notation "hvbox('x')" +notation "hvbox('X')" non associative with precedence 60 for @{ 'monomio 1 }. interpretation "Rmonomio" 'monomio n = (monomio n). -axiom derivative_x0: D[x \sup 0] = 0. -axiom derivative_x1: D[x] = 1. +axiom derivative_x0: D[X \sup 0] = 0. +axiom derivative_x1: D[X] = 1. + axiom derivative_mult: ∀f,g:R→R. D[f·g] = D[f]·g + f·D[g]. alias symbol "middot" = "Fmult". -theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n). +theorem derivative_power: ∀n:nat. D[X \sup n] = n·X \sup (pred n). assume n:nat. (*we proceed by induction on n to prove - (D[x \sup n] = n · x \sup (pred n)).*) + (D[X \sup n] = n · X \sup (pred n)).*) elim n 0. case O. - the thesis becomes (D[x \sup 0] = 0·x \sup (pred 0)). + the thesis becomes (D[X \sup 0] = 0·X \sup (pred 0)). done. case S (m:nat). by induction hypothesis we know - (D[x \sup m] = m·x \sup (pred m)) (H). + (D[X \sup m] = m·X \sup (pred m)) (H). the thesis becomes - (D[x \sup (1+m)] = (1+m) · x \sup m). + (D[X \sup (1+m)] = (1+m) · X \sup m). we need to prove - (m · (x \sup (1+ pred m)) = m · x \sup m) (Ppred). + (m · (X \sup (1+ pred m)) = m · X \sup m) (Ppred). we proved (0 < m ∨ 0=m) (cases). we proceed by induction on cases - to prove (m · (x \sup (1+ pred m)) = m · x \sup m). + to prove (m · (X \sup (1+ pred m)) = m · X \sup m). case left. suppose (0 < m) (m_pos). using (S_pred ? m_pos) we proved (m = 1 + pred m) (H1). @@ -251,13 +255,13 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n). suppose (0=m) (m_zero). by m_zero, Fmult_zero_f done. conclude - (D[x \sup (1+m)]) - = (D[x · x \sup m]). - = (D[x] · x \sup m + x · D[x \sup m]). - = (x \sup m + x · (m · x \sup (pred m))) timeout=30. - = (x \sup m + m · (x \sup (1 + pred m))). - = (x \sup m + m · x \sup m). - = ((1+m) · x \sup m) timeout=30 by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum + (D[X \sup (1+m)]) + = (D[X · X \sup m]). + = (D[X] · X \sup m + X · D[X \sup m]). + = (X \sup m + X · (m · X \sup (pred m))) timeout=30. + = (X \sup m + m · (X \sup (1 + pred m))). + = (X \sup m + m · X \sup m). + = ((1+m) · X \sup m) timeout=30 by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum done. qed. @@ -271,30 +275,30 @@ for @{ 'derivative ${default interpretation "Rderivative" 'derivative \eta.f = (derivative f). *) -notation "hvbox(\frac 'd' ('d' 'x') break p)" with precedence 90 +notation "hvbox(\frac 'd' ('d' 'X') break p)" with precedence 90 for @{ 'derivative $p}. interpretation "Rderivative" 'derivative f = (derivative f). -theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n. +theorem derivative_power': ∀n:nat. D[X \sup (1+n)] = (1+n) · X \sup n. assume n:nat. (*we proceed by induction on n to prove - (D[x \sup (1+n)] = (1+n) · x \sup n).*) elim n 0. + (D[X \sup (1+n)] = (1+n) · X \sup n).*) elim n 0. case O. - the thesis becomes (D[x \sup 1] = 1 · x \sup 0). + the thesis becomes (D[X \sup 1] = 1 · X \sup 0). done. case S (m:nat). by induction hypothesis we know - (D[x \sup (1+m)] = (1+m) · x \sup m) (H). + (D[X \sup (1+m)] = (1+m) · X \sup m) (H). the thesis becomes - (D[x \sup (2+m)] = (2+m) · x \sup (1+m)). + (D[X \sup (2+m)] = (2+m) · X \sup (1+m)). conclude - (D[x \sup (2+m)]) - = (D[x · x \sup (1+m)]). - = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]). - = (x \sup (1+m) + x · (costante (1+m) · x \sup m)). - = (x \sup (1+m) + costante (1+m) · x \sup (1+m)). - = ((2+m) · x \sup (1+m)) timeout=30 by Fmult_one_f, Fmult_commutative, + (D[X \sup (2+m)]) + = (D[X · X \sup (1+m)]). + = (D[X] · X \sup (1+m) + X · D[X \sup (1+m)]). + = (X \sup (1+m) + X · (costante (1+m) · X \sup m)). + = (X \sup (1+m) + costante (1+m) · X \sup (1+m)). + = ((2+m) · X \sup (1+m)) timeout=30 by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, assoc_plus, plus_n_SO, costante_sum done. qed. diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 4e5374dc7..1afd0516c 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,3 +1,4 @@ +theory.ma Q/Qaxioms.ma Q/frac.ma Q/inv.ma Q/q/qplus.ma Q/q/qtimes.ma R/Rlog.ma Z/inversion.ma algebra/finite_groups.ma dama/models/nat_lebesgue.ma datatypes/subsets.ma decidable_kit/fgraph.ma demo/cantor.ma demo/natural_deduction.ma demo/power_derivative.ma demo/propositional_sequent_calculus.ma demo/realisability.ma demo/toolbox.ma didactic/exercises/duality.ma didactic/exercises/natural_deduction.ma didactic/exercises/natural_deduction1.ma didactic/exercises/natural_deduction_fst_order.ma didactic/exercises/natural_deduction_theories.ma didactic/exercises/shannon.ma didactic/exercises/substitution.ma nat/bertrand.ma nat/chebyshev_thm.ma nat/euler_theorem.ma nat/factorization2.ma nat/fermat_little_theorem.ma nat/totient1.ma technicalities/setoids.ma dama/sandwich.ma dama/ordered_uniform.ma demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma @@ -18,6 +19,7 @@ algebra/groups.ma algebra/monoids.ma datatypes/bool.ma nat/compare.ma nat/le_ari nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma +theory.ma Q/Qaxioms.ma Q/frac.ma Q/inv.ma Q/q/qplus.ma Q/q/qtimes.ma R/Rlog.ma Z/inversion.ma algebra/finite_groups.ma dama/models/nat_lebesgue.ma datatypes/subsets.ma decidable_kit/fgraph.ma demo/cantor.ma demo/natural_deduction.ma demo/power_derivative.ma demo/propositional_sequent_calculus.ma demo/realisability.ma demo/toolbox.ma didactic/exercises/duality.ma didactic/exercises/natural_deduction.ma didactic/exercises/natural_deduction1.ma didactic/exercises/natural_deduction_fst_order.ma didactic/exercises/natural_deduction_theories.ma didactic/exercises/shannon.ma didactic/exercises/substitution.ma nat/bertrand.ma nat/chebyshev_thm.ma nat/euler_theorem.ma nat/factorization2.ma nat/fermat_little_theorem.ma nat/totient1.ma technicalities/setoids.ma dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_set.ma list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma datatypes/compare.ma diff --git a/helm/software/matita/library/theory.ma b/helm/software/matita/library/theory.ma new file mode 100644 index 000000000..866a24b5c --- /dev/null +++ b/helm/software/matita/library/theory.ma @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "Q/Qaxioms.ma". + +include "Q/frac.ma". + +include "Q/inv.ma". + +include "Q/q/qplus.ma". + +include "Q/q/qtimes.ma". + +include "R/Rlog.ma". + +include "Z/inversion.ma". + +include "algebra/finite_groups.ma". + +include "dama/models/nat_lebesgue.ma". + +include "datatypes/subsets.ma". + +include "decidable_kit/fgraph.ma". + +include "demo/cantor.ma". + +include "demo/natural_deduction.ma". + +include "demo/power_derivative.ma". + +include "demo/propositional_sequent_calculus.ma". + +include "demo/realisability.ma". + +include "demo/toolbox.ma". + +include "didactic/exercises/duality.ma". + +include "didactic/exercises/natural_deduction.ma". + +include "didactic/exercises/natural_deduction1.ma". + +include "didactic/exercises/natural_deduction_fst_order.ma". + +include "didactic/exercises/natural_deduction_theories.ma". + +include "didactic/exercises/shannon.ma". + +include "didactic/exercises/substitution.ma". + +include "nat/bertrand.ma". + +include "nat/chebyshev_thm.ma". + +include "nat/euler_theorem.ma". + +include "nat/factorization2.ma". + +include "nat/fermat_little_theorem.ma". + +include "nat/totient1.ma". + +include "technicalities/setoids.ma". + diff --git a/helm/software/matita/matitaMisc.ml b/helm/software/matita/matitaMisc.ml index 211295261..687cb94f0 100644 --- a/helm/software/matita/matitaMisc.ml +++ b/helm/software/matita/matitaMisc.ml @@ -155,9 +155,32 @@ let list_tl_at ?(equality=(==)) e l = aux l let shutup () = - HLog.set_log_callback (fun _ _ -> ()); + HLog.set_log_callback (fun _ _ -> ()) (* let out = open_out "/dev/null" in Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr) *) +(* FG: out_preamble *********************************************************) + +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 = + 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 + 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" diff --git a/helm/software/matita/matitaMisc.mli b/helm/software/matita/matitaMisc.mli index b91275618..eec60932d 100644 --- a/helm/software/matita/matitaMisc.mli +++ b/helm/software/matita/matitaMisc.mli @@ -76,3 +76,6 @@ val image_path: string -> string (** 2>/dev/null, HLog = (fun _ -> ()) *) val shutup: unit -> unit + + (** outputs the preamble of a generated .ma file *) +val out_preamble: out_channel -> unit diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index e793a725b..aff789517 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -63,26 +63,6 @@ let dump f = Helm_registry.set_bool "matita.moo" false; let floc = H.dummy_floc in let nl_ast = G.Comment (floc, G.Note (floc, "")) in - let och = open_out f in - 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 "*)" - in - 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 - in - 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" - in let pp_ast_statement st = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term ~map_unicode_to_tex:(Helm_registry.get_bool @@ -90,11 +70,9 @@ let dump f = ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st in + let och = open_out f in let nl () = output_string och (pp_ast_statement nl_ast) 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); + MatitaMisc.out_preamble och; let grafite_parser_cb fname = let ast = G.Executable (floc, G.Command (floc, G.Include (floc, fname))) in diff --git a/helm/software/matita/matitadep.ml b/helm/software/matita/matitadep.ml index 050fa220e..514147bd1 100644 --- a/helm/software/matita/matitadep.ml +++ b/helm/software/matita/matitadep.ml @@ -25,6 +25,8 @@ (* $Id$ *) +module S = Set.Make (String) + module GA = GrafiteAst module U = UriManager module HR = Helm_registry @@ -46,10 +48,27 @@ let exclude excluded_files files = let map file = not (List.mem (fix_name file) excluded_files) in List.filter map files +let generate_theory theory_file deps = + let map (files, deps) (t, d) = + if t = theory_file then files, deps else + S.add t files, List.fold_left (fun deps dep -> S.add dep deps) deps d + in + let out_include och dep = + Printf.fprintf och "include \"%s\".\n\n" dep + in + let fileset, depset = List.fold_left map (S.empty, S.empty) deps in + let top_depset = S.diff fileset depset in + let och = open_out theory_file in + MatitaMisc.out_preamble och; + S.iter (out_include och) top_depset; + close_out och; + (theory_file, S.elements top_depset) :: deps + let main () = (* let _ = print_times "inizio" in *) let include_paths = ref [] in let use_stdout = ref false in + let theory_file = ref "theory.ma" in (* all are maps from "file" to "something" *) let include_deps = Hashtbl.create 13 in let baseuri_of = Hashtbl.create 13 in @@ -57,6 +76,7 @@ let main () = let dot_name = "depends" in let dot_file = ref "" in let set_dot_file () = dot_file := dot_name^".dot" in + let set_theory_file s = theory_file := s ^ ".ma" in (* helpers *) let rec baseuri_of_script s = try Hashtbl.find baseuri_of s @@ -91,7 +111,9 @@ let main () = ["-dot", Arg.Unit set_dot_file, "Save dependency graph in dot format and generate a png"; "-stdout", Arg.Set use_stdout, - "Print dependences on stdout" + "Print dependences on stdout"; + "-theory", Arg.String set_theory_file, + "Set the name of the theory file (it includes all other files)" ]; MatitaInit.parse_cmdline_and_configuration_file (); MatitaInit.initialize_environment (); @@ -195,9 +217,14 @@ let main () = [] deps in let where = if !use_stdout then None else Some (Sys.getcwd()) in - Librarian.write_deps_file where - (deps@HExtlib.list_uniq (List.sort Pervasives.compare (List.map (fun x -> - x,[]) extern))); + let all_deps = + deps @ + HExtlib.list_uniq (List.sort Pervasives.compare (List.map (fun x -> x,[]) extern)) + in + (* theory generation *) + let all_deps_and_theory = generate_theory !theory_file all_deps in + (* matita depend file generation *) + Librarian.write_deps_file where all_deps_and_theory; (* dot generation *) if !dot_file <> "" then begin -- 2.39.2