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;
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
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";
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 = [];
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;
$(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)
(* *)
(**************************************************************************)
-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".
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).
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.
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.
+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".
+
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"
(** 2>/dev/null, HLog = (fun _ -> ()) *)
val shutup: unit -> unit
+
+ (** outputs the preamble of a generated .ma file *)
+val out_preamble: out_channel -> unit
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
~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
(* $Id$ *)
+module S = Set.Make (String)
+
module GA = GrafiteAst
module U = UriManager
module HR = Helm_registry
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
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
["-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 ();
[] 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
projects / helm.git / commitdiff