context = [];
case = []
} in
+ H.print_times "LEVEL 2";
HLog.debug "Procedural: level 2 transformation";
let steps = proc_obj st ?flavour anobj in
+ H.print_times "RENDERING";
HLog.debug "Procedural: grafite rendering";
- List.rev (T.render_steps [] steps)
+ let r = List.rev (T.render_steps [] steps) in
+ H.print_times "DONE "; r
let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
prefix context annterm =
module PER = ProofEngineReduction
module Ut = CicUtil
+(* time stamping ************************************************************)
+
+let print_times =
+ let old = ref 0.0 in
+ fun msg ->
+ let times = Unix.times () in
+ let stamp = times.Unix.tms_utime +. times.Unix.tms_utime in
+ let lap = stamp -. !old in
+ Printf.eprintf "TIME STAMP: %s: %f\n" msg lap; flush stdout;
+ old := stamp
+
(* raw cic prettyprinter ****************************************************)
let xiter out so ss sc map l =
* http://cs.unibo.it/helm/.
*)
+val print_times:
+ string -> unit
val pp_term:
(string -> unit) -> Cic.metasenv -> Cic.context -> Cic.term -> unit
val mk_fresh_name:
Cic.context -> Cic.name -> Cic.name
val list_map_cps:
- ('a list -> 'b) -> (('a -> 'b) -> 'c -> 'b) -> 'c list -> 'b
+ ('a list -> 'b) -> (('a -> 'b) -> 'c -> 'b) -> 'c list -> 'b
val identity:
- 'a -> 'a
+ 'a -> 'a
val compose:
('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
val fst3:
module H = ProceduralHelpers
module Cl = ProceduralClassify
+(* debugging ****************************************************************)
+
+let debug = ref false
+
(* term preprocessing: optomization 1 ***************************************)
let defined_premise = "DEFINED"
| C.Lambda (_, _, t) when n > 0 ->
aux 0 (pred n) (S.lift (-1) t)
| t when n > 0 ->
- Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t);
+ Printf.eprintf "PO.clear_absts: %u %s\n" n (Pp.ppterm t);
assert false
| t -> t
in
| C.Constant (name, Some bo, ty, pars, attrs) ->
let bo, ty = H.cic_bc [] bo, H.cic_bc [] ty in
let g bo =
- Printf.eprintf "Optimized : %s\nPost Nodes: %u\n"
- (Pp.ppterm bo) (I.count_nodes 0 bo);
- prerr_string "H.pp_term : ";
- H.pp_term prerr_string [] [] bo; prerr_newline ();
+ if !debug then begin
+ Printf.eprintf "Optimized : %s\nPost Nodes: %u\n"
+ (Pp.ppterm bo) (I.count_nodes 0 bo);
+ prerr_string "H.pp_term : ";
+ H.pp_term prerr_string [] [] bo; prerr_newline ()
+ end;
let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in
+ H.print_times ("OPTIMIZED: " ^ name);
C.Constant (name, Some bo, ty, pars, attrs)
in
- Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n"
- name (I.count_nodes 0 bo);
+ H.print_times ("BEGIN : " ^ name);
+ if !debug then
+ Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n"
+ name (I.count_nodes 0 bo);
begin try opt1_term g (* (opt2_term g []) *) true [] bo with
| E.Object_not_found uri ->
let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in
*)
val optimize_obj: Cic.obj -> Cic.obj
+
+val debug: bool ref
let not_implemented =
"discharge of current proofs is not implemented yet"
+let debug = ref false
+
(* helper functions *********************************************************)
let list_pos found l =
let s = List.map (mk_arg s) args in
C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
| C.Var (u, s) ->
-(* FG: We do not discharge the nsubst here ?? *)
- let args = get_args st u in
- if args = [] then C.Rel (discharge st u) else
- let s = List.map (mk_arg s) args in
- (* C.Appl ( *) C.Rel (discharge st u) (* :: discharge_nsubst st s) *)
+(* We do not discharge the nsubst because variables are not closed *)
+(* thus only the identity nsubst should be allowed *)
+ if s <> [] then assert false else
+ C.Rel (discharge st u)
| C.Meta (i, s) ->
let s' = list_map_sh (discharge_usubst st) s in
if s' == s then t else C.Meta (i, s')
and discharge_uri dn du uri =
let obj, _ = E.get_obj Un.default_ugraph uri in
- prerr_endline ("Plain : " ^ CicPp.ppobj obj);
+ if !debug then prerr_endline ("Plain : " ^ CicPp.ppobj obj);
let obj' = discharge_object dn du obj in
- prerr_endline ("Discharged: " ^ CicPp.ppobj obj');
+ if !debug then prerr_endline ("Discharged: " ^ CicPp.ppobj obj');
obj', obj' == obj
and discharge_vars dn du vars =
val discharge_uri:
(string -> string) -> (UriManager.uri -> UriManager.uri) ->
UriManager.uri -> Cic.obj * bool
+
+(* if activated prints the received object before and after discharging *)
+val debug: bool ref
let fst4 = function (x,_,_,_) -> x;;
- let younger_s_t (_,cs, ct, _, _) a b =
+ let modified_before_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 modified_before_t_t (_,_,ct, _, _) a b =
let a =
try
match Hashtbl.find ct a with
| Some root -> not (F.is_readonly_buri_of opts f)
| None -> assert false
;;
-
+(* FG: Old sorting algorithm ************************************************)
+(*
let rec get_status opts what =
let _, _, _, cc, cd = opts in
let t, dependencies, root, tgt = what 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
+ if modified_before_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
| _ -> st
end
in
- let st = if younger_s_t opts t tgt then Done true else Ready true in
+ let st = if modified_before_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" *)
let rc =
match froot with
| Some froot when froot = root ->
- Hashtbl.remove ct tgt;
+ Hashtbl.remove ct tgt;
Hashtbl.add ct tgt None;
timestamp "building";
let r = F.build lo file in
end
else
ok
+*)
+(* FG: new sorting algorithm ************************************************)
+
+ let rec make_aux root opts ok deps =
+ List.fold_left (make_one root opts) ok deps
+
+ and make_one root opts ok what =
+ let lo, _, ct, cc, cd = opts in
+ let t, deps, froot, tgt = what in
+ let map (okd, okt) d =
+ let (_, _, _, tgtd) as whatd = (Hashtbl.find cd d) in
+ make_one root opts okd whatd, okt && modified_before_t_t opts tgtd tgt
+ in
+ try ok && Hashtbl.find cc t
+(* say "already built" *)
+ with Not_found ->
+ let okd, okt = List.fold_left map (true, modified_before_s_t opts t tgt) deps in
+ let res =
+ if okd then
+ if okt then true else
+ let str = F.string_of_source_object t in
+ match froot with
+ | Some froot when froot = root ->
+ if is_not_ro opts what then begin
+ Hashtbl.remove ct tgt;
+ Hashtbl.add ct tgt None;
+ timestamp "building";
+ let res = F.build lo t in
+ timestamp "done"; res
+ end else begin
+ HLog.warn("Read only baseuri for: "^ str); false
+ end
+ | Some froot -> make froot [t]
+ | None ->
+ HLog.error ("No root for: " ^ str); false
+ else false
+ in
+ Hashtbl.add cc t res; ok && res
+
+(****************************************************************************)
- and make root targets =
+ and make root targets =
timestamp "entering";
HLog.debug ("Entering directory '"^root^"'");
let old_root = Sys.getcwd () in
projects / helm.git / commitdiff