From 128ea02422e0cc4254ea3f8e4b0c5248c7182479 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 12 Jul 2008 20:40:30 +0000 Subject: [PATCH] librarian: retrieval of buildable files speeded up a lot Procedural: some bug fixes termContentPres.ml: syntax of let-in construction fixed LAMBDA-TYPES: some improvements in the Makefile --- .../acic_procedural/acic2Procedural.ml | 57 ++--- .../acic_procedural/proceduralConversion.ml | 6 +- .../acic_procedural/proceduralConversion.mli | 2 + .../content_pres/termContentPres.ml | 2 +- helm/software/components/library/librarian.ml | 205 ++++++++++-------- .../matita/contribs/LAMBDA-TYPES/Makefile | 4 +- 6 files changed, 149 insertions(+), 127 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 4dd1bf192..8e99a9332 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -51,7 +51,6 @@ type status = { max_depth: int option; depth: int; context: C.context; - intros: string option list; clears: string list; clears_note: string; case: int list; @@ -88,12 +87,9 @@ let string_of_head = function | C.AMeta _ -> "meta" | C.AImplicit _ -> "implict" -let clear st = {st with intros = []} +let next st = {st with depth = succ st.depth} -let next st = {(clear st) with depth = succ st.depth} - -let add st entry intro = - {st with context = entry :: st.context; intros = intro :: st.intros} +let add st entry = {st with context = entry :: st.context} let push st = {st with case = 1 :: st.case} @@ -241,16 +237,11 @@ let get_intro = function | C.Anonymous -> None | C.Name s -> Some s -let mk_intros st what script = - let intros st script = - if st.intros = [] then script else - let count = List.length st.intros in - T.Intros (Some count, List.rev st.intros, "") :: script - in +let mk_preamble st what script = let clears st script = if true (* st.clears = [] *) then script else T.Clear (st.clears, st.clears_note) :: script in - intros st (clears st (convert st what @ script)) + clears st (convert st what @ script) let mk_arg st = function | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what @@ -264,6 +255,7 @@ let mk_fwd_rewrite st dtext name tl direction v t ity = assert (List.length tl = 6); let what, where, predicate = List.nth tl 5, List.nth tl 3, List.nth tl 2 in let e = Cn.mk_pattern 1 predicate in + if (Cn.does_not_occur e) then st, [] else match where with | C.ARel (_, _, i, premise) as w -> (* let _script = convert_elim st ~name:(premise, i) v w e in *) @@ -285,29 +277,29 @@ let mk_rewrite st dtext where qs tl direction t = assert (List.length tl = 5); let predicate = List.nth tl 2 in let e = Cn.mk_pattern 1 predicate in - let script = [] (* convert_elim st t t e *) in - script @ [T.Rewrite (direction, where, None, e, dtext); T.Branch (qs, "")] + let script = [T.Branch (qs, "")] in + if (Cn.does_not_occur e) then script else +(* let script = convert_elim st t t e in *) + T.Rewrite (direction, where, None, e, dtext) :: script let rec proc_lambda st what name v t = - let dno, ae = match get_inner_types st t with - | None -> false, true - | Some (sty, ety) -> + let dno = match get_inner_types st t with + | None -> false + | Some (sty, ety) -> let sty, ety = H.cic sty, H.cic ety in - DTI.does_not_occur 1 sty && DTI.does_not_occur 1 ety, - Ut.alpha_equivalence sty ety + DTI.does_not_occur 1 sty && DTI.does_not_occur 1 ety in let dno = dno && DTI.does_not_occur 1 (H.cic t) in let name = match dno, name with | true, _ -> C.Anonymous - | false, C.Anonymous -> H.mk_fresh_name st.context used_premise + | false, C.Anonymous -> H.mk_fresh_name st.context used_premise | false, name -> name in let entry = Some (name, C.Decl (H.cic v)) in let intro = get_intro name in - let st = (add st entry intro) in - if ae then proc_proof st t else - let script = proc_proof (clear st) t in - mk_intros st t script + let script = proc_proof (add st entry) t in + let script = T.Intros (Some 1, [intro], "") :: script in + mk_preamble st what script and proc_letin st what name v w t = let intro = get_intro name in @@ -330,28 +322,28 @@ and proc_letin st what name v w t = st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)] in let entry = Some (name, hyp) in - let qt = proc_proof (next (add st entry intro)) t in + let qt = proc_proof (next (add st entry)) t in List.rev_append rqv qt else [T.Apply (what, dtext)] in - mk_intros st what script + mk_preamble st what script and proc_rel st what = let _, dtext = test_depth st in let text = "assumption" in let script = [T.Apply (what, dtext ^ text)] in - mk_intros st what script + mk_preamble st what script and proc_mutconstruct st what = let _, dtext = test_depth st in let script = [T.Apply (what, dtext)] in - mk_intros st what script + mk_preamble st what script and proc_const st what = let _, dtext = test_depth st in let script = [T.Apply (what, dtext)] in - mk_intros st what script + mk_preamble st what script and proc_appl st what hd tl = let proceed, dtext = test_depth st in @@ -402,12 +394,12 @@ and proc_appl st what hd tl = else [T.Apply (what, dtext)] in - mk_intros st what script + mk_preamble st what script and proc_other st what = let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in let script = [T.Note text] in - mk_intros st what script + mk_preamble st what script and proc_proof st t = let f st = @@ -483,7 +475,6 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth max_depth = depth; depth = 0; context = []; - intros = []; clears = []; clears_note = ""; case = []; diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 30a52c32c..e42ad490e 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -72,7 +72,7 @@ let lift k n = | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl) | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t) | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t) - | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term k ty, lift_term (succ k) t) + | C.ALetIn (id, n, ty, s, t) -> C.ALetIn (id, n, lift_term k ty, lift_term k s, lift_term (succ k) t) | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl) | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl) in @@ -249,3 +249,7 @@ let elim_inferred_type context goal arg using cpattern = let ty = C.Appl (predicate :: actual_args) in let upto = List.length actual_args in Rd.head_beta_reduce ~delta:false ~upto ty + +let does_not_occur = function + | C.AImplicit (_, None) -> true + | _ -> false diff --git a/helm/software/components/acic_procedural/proceduralConversion.mli b/helm/software/components/acic_procedural/proceduralConversion.mli index ffc55d45e..bc49b9a22 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.mli +++ b/helm/software/components/acic_procedural/proceduralConversion.mli @@ -41,3 +41,5 @@ val clear: Cic.context -> string -> Cic.context val elim_inferred_type: Cic.context -> Cic.term -> Cic.term -> Cic.term -> Cic.term -> Cic.term + +val does_not_occur: Cic.annterm -> bool diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index a1f9268e4..fd326e5e9 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -196,7 +196,7 @@ let pp_ast0 t k = hvbox false true [ aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ]; - break; space; keyword "in" ]; + break; space; keyword "in"; space ]; break; k t ]) | Ast.LetRec (rec_kind, funs, where) -> diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index 919edb36c..e79fe6356 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -1,3 +1,33 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let timestamp msg = + let times = Unix.times () in + let msg = Printf.sprintf "UTIMESTAMP (%s): %f" msg times.Unix.tms_utime in + prerr_endline msg + let debug = false;; exception NoRootFor of string @@ -157,11 +187,16 @@ module type Format = module Make = functor (F:Format) -> struct + type status = Done of bool + | Ready of bool + let say s = if debug then prerr_endline ("make: "^s);; let unopt_or_call x f y = match x with Some _ -> x | None -> f y;; - let younger_s_t (_,cs,ct) a b = + let fst4 = function (x,_,_,_) -> x;; + + let younger_s_t (_,cs, ct, _, _) a b = let a = try Hashtbl.find cs a with Not_found -> assert false in let b = try @@ -180,7 +215,7 @@ module Make = functor (F:Format) -> struct | _ -> false ;; - let younger_t_t (_,_,ct) a b = + let younger_t_t (_,_,ct, _, _) a b = let a = try match Hashtbl.find ct a with @@ -210,72 +245,6 @@ module Make = functor (F:Format) -> struct | _ -> false ;; - let is_built opts t tgt = - younger_s_t opts t tgt - ;; - - let assoc4 l k = List.find (fun (k1,_,_,_) -> k1 = k) l;; - - let fst4 = function (x,_,_,_) -> x;; - - let rec needs_build opts deps compiled (t,dependencies,root,tgt) = - say ("Checking if "^F.string_of_source_object t^ " needs to be built"); - if List.mem t compiled then - (say "already compiled"; false) - else - if not (is_built opts t tgt) then - (say(F.string_of_source_object t^" is not built, thus needs to be built"); - true) - else - try - let unsat = - List.find - (needs_build opts deps compiled) - (List.map (assoc4 deps) dependencies) - in - say (F.string_of_source_object t^" depends on "^ - F.string_of_source_object (fst4 unsat)^ - " that needs to be built, thus needs to be built"); - true - with Not_found -> - try - let _,_,_,unsat = - List.find - (fun (_,_,_,tgt1) -> younger_t_t opts tgt tgt1) - (List.map (assoc4 deps) dependencies) - in - say - (F.string_of_source_object t^" depends on "^F.string_of_target_object - unsat^" and "^F.string_of_source_object t^".o is younger than "^ - F.string_of_target_object unsat^", thus needs to be built"); - true - with Not_found -> false - ;; - - let is_buildable opts compiled deps (t,dependencies,root,tgt as what) = - say ("Checking if "^F.string_of_source_object t^" is buildable"); - let b = needs_build opts deps compiled what in - if not b then - (say (F.string_of_source_object t^ - " does not need to be built, thus it not buildable"); - false) - else - try - let unsat,_,_,_ = - List.find (needs_build opts deps compiled) - (List.map (assoc4 deps) dependencies) - in - say (F.string_of_source_object t^" depends on "^ - F.string_of_source_object unsat^ - " that needs build, thus is not buildable"); - false - with Not_found -> - say - ("None of "^F.string_of_source_object t^ - " dependencies needs to be built, thus it is buildable"); - true - ;; - let rec purge_unwanted_roots wanted deps = let roots, rest = List.partition @@ -290,15 +259,62 @@ module Make = functor (F:Format) -> struct purge_unwanted_roots wanted (newroots @ rest) ;; - let is_not_ro (opts,_,_) (f,_,r,_) = + let is_not_ro (opts,_,_,_,_) (f,_,r,_) = match r with | Some root -> not (F.is_readonly_buri_of opts f) | None -> assert false ;; - let rec make_aux root (lo,_,ct as opts) compiled failed deps = - let todo = List.filter (is_buildable opts compiled deps) deps in - let todo = List.filter (fun (f,_,_,_)->not (List.mem f failed)) todo in + let rec get_status opts what = + let _, _, _, cc, cd = opts in + let t, dependencies, root, tgt = what in + try Done (Hashtbl.find cc t) +(* say "already built" *) + with Not_found -> + let map st d = match st with + | Done false -> st + | Ready false -> st + | _ -> + let whatd = Hashtbl.find cd d in + let _, _, _, tgtd = whatd in + begin match st, get_status opts whatd with + | _, Done false -> Hashtbl.add cc t false; Done false + | Done true, Done true -> + if younger_t_t opts tgt tgtd then Ready true else Done true +(* say (F.string_of_source_object t^" depends on "^F.string_of_target_object unsat^" and "^F.string_of_source_object t^".o is younger than "^ F.string_of_target_object unsat^", thus needs to be built") *) + | Done true, Ready _ -> Ready false + | Ready true, Ready _ -> Ready false +(* say (F.string_of_source_object t^" depends on "^ F.string_of_source_object (fst4 unsat)^ " that is not built, thus is not ready") *) + | Ready true, Done true -> Ready true + | _ -> st + end + in + let st = if younger_s_t opts t tgt then Done true else Ready true in + match List.fold_left map st dependencies with + | Done true -> Hashtbl.add cc t true; Done true +(* say(F.string_of_source_object t^" is built" *) + | st -> st + + let list_partition_filter_rev filter l = + let rec aux l1 l2 = function + | [] -> l1, l2 + | hd :: tl -> + begin match filter hd with + | None -> aux l1 l2 tl + | Some true -> aux (hd :: l1) l2 tl + | Some false -> aux l1 (hd :: l2) tl + end + in + aux [] [] l + + let rec make_aux root (lo,_,ct, cc, _ as opts) ok deps = + timestamp "filter get_status: begin"; + let map what = match get_status opts what with + | Done _ -> None + | Ready b -> Some b + in + let todo, deps = list_partition_filter_rev map deps in + timestamp "filter get_status: end"; let todo = let local, remote = List.partition (fun (_,_,froot,_) -> froot = Some root) todo @@ -310,36 +326,42 @@ module Make = functor (F:Format) -> struct skipped; remote @ local in - if todo <> [] then - let compiled, failed = - List.fold_left - (fun (c,f) (file,_,froot,tgt) -> + if todo <> [] then begin + let ok = List.fold_left + (fun ok (file,_,froot,tgt) -> let rc = match froot with | Some froot when froot = root -> Hashtbl.remove ct tgt; Hashtbl.add ct tgt None; - F.build lo file + timestamp "building"; + let r = F.build lo file in + timestamp "done"; r | Some froot -> make froot [file] | None -> HLog.error ("No root for: "^F.string_of_source_object file); false in - if rc then (file::c,f) - else (c,file::f)) - (compiled,failed) todo - in - make_aux root opts compiled failed deps + Hashtbl.add cc file rc; + ok && rc + ) + ok (List.rev todo) + in + make_aux root opts ok (List.rev deps) + end else - compiled, failed + ok and make root targets = + timestamp "entering"; HLog.debug ("Entering directory '"^root^"'"); let old_root = Sys.getcwd () in Sys.chdir root; let deps = F.load_deps_file (root^"/depends") in let local_options = load_root_file (root^"/root") in - let caches,cachet = Hashtbl.create 73, Hashtbl.create 73 in + let caches,cachet,cachec,cached = + Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73 + in (* deps are enriched with these informations to sped up things later *) let deps = List.map @@ -347,20 +369,23 @@ module Make = functor (F:Format) -> struct let r,tgt = F.root_and_target_of local_options file in Hashtbl.add caches file (F.mtime_of_source_object file); Hashtbl.add cachet tgt (F.mtime_of_target_object tgt); - file, d, r, tgt) + Hashtbl.add cached file (file, d, r, tgt); + (file, d, r, tgt) + ) deps in - let opts = local_options, caches, cachet in - let _compiled, failed = + let opts = local_options, caches, cachet, cachec, cached in + let ok = if targets = [] then - make_aux root opts [] [] deps + make_aux root opts true deps else - make_aux root opts [] [] + make_aux root opts true (purge_unwanted_roots targets deps) in HLog.debug ("Leaving directory '"^root^"'"); Sys.chdir old_root; - failed = [] + timestamp "leaving"; + ok ;; end diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile index e44fbb49a..194fc389e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile @@ -1,6 +1,7 @@ include ../Makefile.defs H=@ +S=-s MATITAOPTIONS=$(MATITAUSEROPTIONS) -onepass @@ -8,7 +9,7 @@ LOG = log.txt DIRS = Legacy-2 Base-2 LambdaDelta-2 -SILENTMAKE = $(H)$(MAKE) H=$(H) -s --no-print-directory +SILENTMAKE = $(H)$(MAKE) $(S) --no-print-directory H=$(H) S=$(S) MAS = $(shell find $(DIRS) -mindepth 2 -name "*.ma") @@ -44,7 +45,6 @@ clean.ma: $(H)$(BIN)matitaclean.opt $(MATITAOPTIONS) $(MAS) $(H)$(RM) $(MAS) depends - clean.mma: # $(H)for FILE in */*.mma ; do if [ -e ../LambdaDelta-1/$${FILE/.mma/.ma} ] ; then true ; else rm $$FILE ; fi done -- 2.39.2