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
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 =
| _ -> 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";
| _ -> 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
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
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
type inline_kind = Con | Ind | Var
-type input_kind = Gallina8 | Grafite
+type input_kind = Gallina8 | Grafite of string
type output_kind = Declarative | Procedural
<key name="input_type">grafite</key>
<key name="output_type">procedural</key>
<key name="heading_lines">14</key>
+ <key name="theory_file"></key>
</section>
</helm_registry>
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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".
-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
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
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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".
-
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
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
"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 <name>", Arg.String set_theory_file,
+ "generate a theory file <name>.ma (it includes all other files)"
];
MatitaInit.parse_cmdline_and_configuration_file ();
MatitaInit.initialize_environment ();
projects / helm.git / commitdiff