From: Ferruccio Guidi Date: Wed, 22 Apr 2009 20:47:20 +0000 (+0000) Subject: - transcript: we have now two styles of mma's from grafite: X-Git-Tag: make_still_working~4060 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0137a346eaaf9ae7a0b23c7a3b4c6628073b7dfb;p=helm.git - transcript: we have now two styles of mma's from grafite: 1) each includes its source (minimum choice) 2) each includes the theory file of the source devel (maximim choice) - matitadep: creation of the theory file is now optional and defaults to no - procedural/library: we use style 1) above so library/theory is not needed --- diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index f17459162..efadc681e 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,11 +1,6 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 2e81186ea..916338368 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -104,10 +104,11 @@ let init () = let make registry = let id x = x in let get_pairs = R.get_list (R.pair id id) in - let get_input_type key = - match R.get_string key with - | "gallina8" -> T.Gallina8, ".v" - | "grafite" -> T.Grafite, ".ma" + let get_input_type key1 key2 = + match R.get_string key1, R.get_string key2 with + | "gallina8", _ -> T.Gallina8, ".v", [] + | "grafite", "" -> T.Grafite "", ".ma", [] + | "grafite", s -> T.Grafite s, ".ma", [s] | _ -> failwith "unknown input type" in let get_output_type key = @@ -117,11 +118,9 @@ let make registry = | _ -> failwith "unknown output type" 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 input_type, input_ext, excludes = + get_input_type "package.input_type" "package.theory_file" + in let st = { heading_path = R.get_string "transcript.heading_path"; heading_lines = R.get_int "transcript.heading_lines"; @@ -213,8 +212,8 @@ let produce st = | _ -> true in let get_items = match st.input_type with - | T.Gallina8 -> Gallina8Parser.items Gallina8Lexer.token - | T.Grafite -> GrafiteParser.items GrafiteLexer.token + | T.Gallina8 -> Gallina8Parser.items Gallina8Lexer.token + | T.Grafite _ -> GrafiteParser.items GrafiteLexer.token in let produce st name = let in_base_uri = Filename.concat st.input_base_uri name in @@ -253,9 +252,9 @@ let produce st = let rec remove_lines ich n = if n > 0 then let _ = input_line ich in remove_lines ich (pred n) in - Printf.eprintf "processing file name: %s ...\n" name; flush stderr; - let file = Filename.concat st.input_path (name ^ st.input_ext) in - let ich = open_in file in + Printf.eprintf "processing file name: %s ...\n" name; flush stderr; + let file = Filename.concat st.input_path name in + let ich = open_in (file ^ st.input_ext) in begin try remove_lines ich st.remove_lines with End_of_file -> () end; let lexbuf = Lexing.from_channel ich in try @@ -266,12 +265,25 @@ let produce st = let comment = T.Line (Printf.sprintf "From %s" name) in if global_items <> [] then set_items st st.input_package (comment :: global_items); - init name; require st name st.input_package; set_includes st name; - set_items st name local_items; commit st name + init name; + begin match st.input_type with + | T.Grafite "" -> require st name file + | _ -> require st name st.input_package + end; + set_includes st name; set_items st name local_items; commit st name with e -> prerr_endline (Printexc.to_string e); close_in ich in is_ma st st.input_package; init st.input_package; require st st.input_package "preamble"; - List.iter (produce st) st.files; - commit st st.input_package + match st.input_type with + | T.Grafite "" -> + List.iter (produce st) st.files + | T.Grafite s -> + let theory = Filename.concat st.input_path s in + require st st.input_package theory; + List.iter (produce st) st.files; + commit st st.input_package + | _ -> + List.iter (produce st) st.files; + commit st st.input_package diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml index 7b17db7b2..3b774f832 100644 --- a/helm/software/components/binaries/transcript/types.ml +++ b/helm/software/components/binaries/transcript/types.ml @@ -27,7 +27,7 @@ type local = bool type inline_kind = Con | Ind | Var -type input_kind = Gallina8 | Grafite +type input_kind = Gallina8 | Grafite of string type output_kind = Declarative | Procedural diff --git a/helm/software/matita/contribs/procedural/library/library.conf.xml b/helm/software/matita/contribs/procedural/library/library.conf.xml index 355234785..967ca4cdc 100644 --- a/helm/software/matita/contribs/procedural/library/library.conf.xml +++ b/helm/software/matita/contribs/procedural/library/library.conf.xml @@ -10,5 +10,6 @@ grafite procedural 14 + diff --git a/helm/software/matita/contribs/procedural/library/preamble.ma b/helm/software/matita/contribs/procedural/library/preamble.ma deleted file mode 100644 index df40a272f..000000000 --- a/helm/software/matita/contribs/procedural/library/preamble.ma +++ /dev/null @@ -1,15 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -include "../../../library/theory.ma". diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 1afd0516c..4e5374dc7 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,4 +1,3 @@ -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 @@ -19,7 +18,6 @@ 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 deleted file mode 100644 index 866a24b5c..000000000 --- a/helm/software/matita/library/theory.ma +++ /dev/null @@ -1,78 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/matitadep.ml b/helm/software/matita/matitadep.ml index 514147bd1..af811b140 100644 --- a/helm/software/matita/matitadep.ml +++ b/helm/software/matita/matitadep.ml @@ -49,6 +49,7 @@ let exclude excluded_files files = List.filter map files let generate_theory theory_file deps = + if theory_file = "" then deps else 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 @@ -59,16 +60,18 @@ let generate_theory theory_file deps = 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 + begin + MatitaMisc.out_preamble och; + S.iter (out_include och) top_depset; + close_out och; + (theory_file, S.elements top_depset) :: deps + end 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 + let theory_file = ref "" in (* all are maps from "file" to "something" *) let include_deps = Hashtbl.create 13 in let baseuri_of = Hashtbl.create 13 in @@ -112,8 +115,8 @@ let main () = "Save dependency graph in dot format and generate a png"; "-stdout", Arg.Set use_stdout, "Print dependences on stdout"; - "-theory", Arg.String set_theory_file, - "Set the name of the theory file (it includes all other files)" + "-theory ", Arg.String set_theory_file, + "generate a theory file .ma (it includes all other files)" ]; MatitaInit.parse_cmdline_and_configuration_file (); MatitaInit.initialize_environment ();