max_depth: int option;
depth: int;
context: C.context;
- intros: string option list;
clears: string list;
clears_note: string;
case: int list;
| 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}
| 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
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 *)
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
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
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 =
max_depth = depth;
depth = 0;
context = [];
- intros = [];
clears = [];
clears_note = "";
case = [];
+(* 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
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
| _ -> false
;;
- let younger_t_t (_,_,ct) a b =
+ let younger_t_t (_,_,ct, _, _) a b =
let a =
try
match Hashtbl.find ct a with
| _ -> 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
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
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
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
projects / helm.git / commitdiff