From b1ec882fae6023000ff6076e0a45f9809a6210e4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 5 Apr 2006 08:06:55 +0000 Subject: [PATCH] subsumption fixed and called in given_clause_fullred. --- .../tactics/paramodulation/indexing.ml | 38 +- .../tactics/paramodulation/inference.ml | 1 + .../tactics/paramodulation/saturation.ml | 496 +++++++++--------- 3 files changed, 273 insertions(+), 262 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index f61202396..e6a2463c0 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -411,21 +411,24 @@ let subsumption env table target = let _, _, (ty, left, right, _), tmetas = target in let metasenv, context, ugraph = env in let metasenv = tmetas in - let samesubst subst subst' = - let tbl = Hashtbl.create (List.length subst) in - List.iter (fun (m, x) -> Hashtbl.add tbl m x) subst; - List.for_all - (fun (m, x) -> - try - let x' = Hashtbl.find tbl m in - x = x' - with Not_found -> - true) - subst' + let merge_if_possible s1 s2 = + let already_in = Hashtbl.create 13 in + let rec aux acc = function + | ((i,x) as s)::tl -> + (try + let x' = Hashtbl.find already_in i in + if x = x' then aux acc tl else None + with + | Not_found -> + Hashtbl.add already_in i x; + aux (s::acc) tl) + | [] -> Some acc + in + aux [] (s1@s2) in let leftr = match left with - | Cic.Meta _ -> [] + | Cic.Meta _ -> [] | _ -> let leftc = get_candidates Matching table left in find_all_matches ~unif_fun:Inference.matching @@ -440,7 +443,7 @@ let subsumption env table target = let t1 = Unix.gettimeofday () in try let r = - Inference.matching menv m context what other ugraph + Inference.matching metasenv menv context what other ugraph in let t2 = Unix.gettimeofday () in match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); @@ -450,10 +453,9 @@ let subsumption env table target = match_unif_time_no := !match_unif_time_no +. (t2 -. t1); raise e in - if samesubst subst subst' then - true, subst - else - ok what tl + (match merge_if_possible subst subst' with + | None -> ok what tl + | Some s -> true, s) with Inference.MatchingFailure -> ok what tl in @@ -464,7 +466,7 @@ let subsumption env table target = else let rightr = match right with - | Cic.Meta _ -> [] + | Cic.Meta _ -> [] | _ -> let rightc = get_candidates Matching table right in find_all_matches ~unif_fun:Inference.matching diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml index f74cd1797..547a23559 100644 --- a/helm/software/components/tactics/paramodulation/inference.ml +++ b/helm/software/components/tactics/paramodulation/inference.ml @@ -497,6 +497,7 @@ let locked menv i = ;; let unification_simple locked_menv metasenv context t1 t2 ugraph = + let debug_print x = prerr_endline (Lazy.force x) in let module C = Cic in let module M = CicMetaSubst in let module U = CicUnification in diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index b902dd86b..07c6c6012 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -121,7 +121,7 @@ module OrderedEquality = struct and w2, _, (ty', left', right', _), m2 = eq2 in match Pervasives.compare w1 w2 with | 0 -> - let res = (List.length m1) - (List.length m2) in + let res = (List.length m1) - (List.length m2) in if res <> 0 then res else Pervasives.compare eq1 eq2 | res -> res end @@ -133,30 +133,30 @@ module OrderedEquality = struct let minor eq = let w, _, (ty, left, right, o), _ = eq in match o with - | Lt -> Some left - | Le -> assert false - | Gt -> Some right - | Ge -> assert false - | Eq - | Incomparable -> None - + | Lt -> Some left + | Le -> assert false + | Gt -> Some right + | Ge -> assert false + | Eq + | Incomparable -> None + let compare eq1 eq2 = let w1, _, (ty, left, right, o1), m1 = eq1 and w2, _, (ty', left', right', o2), m2 = eq2 in match Pervasives.compare w1 w2 with | 0 -> - (match minor eq1, minor eq2 with - | Some t1, Some t2 -> - fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2) - | Some _, None -> -1 - | None, Some _ -> 1 - | _,_ -> - (List.length m2) - (List.length m1) ) - | res -> res + (match minor eq1, minor eq2 with + | Some t1, Some t2 -> + fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2) + | Some _, None -> -1 + | None, Some _ -> 1 + | _,_ -> + (List.length m2) - (List.length m1) ) + | res -> res let compare eq1 eq2 = match compare eq1 eq2 with - 0 -> Pervasives.compare eq1 eq2 + 0 -> Pervasives.compare eq1 eq2 | res -> res end *) @@ -187,15 +187,15 @@ let min_elt weight l = (match l with [] -> raise Empty_list | a::tl -> - let wa = float_of_int (weight a) in - let x = ref 0. in - List.fold_left - (fun (current,w) arg -> - x:=!x +. 1.; + let wa = float_of_int (weight a) in + let x = ref 0. in + List.fold_left + (fun (current,w) arg -> + x:=!x +. 1.; let w1 = weight arg in let wa = (float_of_int w1) +. !x *. age_factor in - if wa < w then (arg,wa) else (current,w)) - (a,wa) tl) + if wa < w then (arg,wa) else (current,w)) + (a,wa) tl) ;; (* @@ -233,7 +233,7 @@ let rec select env goals passive (active, _) = ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table) | [], (hd:EqualitySet.elt)::tl -> let passive_table = - Indexing.remove_index passive_table hd + Indexing.remove_index passive_table hd in (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table) | _, _ -> assert false @@ -454,18 +454,18 @@ let infer env sign current (active_list, active_table) = let maxm, res = Indexing.superposition_left !maxmeta env active_table current in if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup-1") res); + ignore(List.map + (function current -> + Indexing.check_target c current "sup-1") res); maxmeta := maxm; res, [] | Positive -> let maxm, res = Indexing.superposition_right !maxmeta env active_table current in if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup0") res); + ignore(List.map + (function current -> + Indexing.check_target c current "sup0") res); maxmeta := maxm; let rec infer_positive table = function | [] -> [], [] @@ -473,21 +473,21 @@ let infer env sign current (active_list, active_table) = let maxm, res = Indexing.superposition_left !maxmeta env table equality in maxmeta := maxm; - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "supl") res); + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "supl") res); let neg, pos = infer_positive table tl in res @ neg, pos | (Positive, equality)::tl -> let maxm, res = Indexing.superposition_right !maxmeta env table equality in maxmeta := maxm; - if Utils.debug_metas then - ignore - (List.map - (function current -> - Indexing.check_target c current "sup2") res); + if Utils.debug_metas then + ignore + (List.map + (function current -> + Indexing.check_target c current "sup2") res); let neg, pos = infer_positive table tl in neg, res @ pos in @@ -495,12 +495,12 @@ let infer env sign current (active_list, active_table) = maxmeta := maxm; let curr_table = Indexing.index Indexing.empty current in let neg, pos = - infer_positive curr_table ((sign,copy_of_current)::active_list) - in - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup3") pos); + infer_positive curr_table ((sign,copy_of_current)::active_list) + in + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "sup3") pos); neg, res @ pos in derived_clauses := !derived_clauses + (List.length new_neg) + @@ -508,12 +508,12 @@ let infer env sign current (active_list, active_table) = match !maximal_retained_equality with | None -> if Utils.debug_metas then - (ignore(List.map - (function current -> - Indexing.check_target c current "sup4") new_pos); - ignore(List.map - (function current -> - Indexing.check_target c current "sup5") new_neg)); + (ignore(List.map + (function current -> + Indexing.check_target c current "sup4") new_pos); + ignore(List.map + (function current -> + Indexing.check_target c current "sup5") new_neg)); new_neg, new_pos | Some eq -> ignore(assert false); @@ -560,7 +560,7 @@ let infer env sign current (active_list, active_table) = in List.filter filterfun new_pos in - new_neg, new_pos + new_neg, new_pos ;; @@ -599,17 +599,17 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) else ( -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *) -(* (string_of_equality current) *) -(* (string_of_equality newcurrent))); *) -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "active is: %s" *) -(* (String.concat "\n" *) -(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *) - None +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *) +(* (string_of_equality current) *) +(* (string_of_equality newcurrent))); *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "active is: %s" *) +(* (String.concat "\n" *) +(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *) + None ) else Some (sign, newcurrent) @@ -619,20 +619,20 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = ignore (Indexing.check_target context current "demod0"); let res = demodulate active_table current in if Utils.debug_metas then - ignore ((function None -> () | Some (_,x) -> - ignore (Indexing.check_target context x "demod1");()) res); + ignore ((function None -> () | Some (_,x) -> + ignore (Indexing.check_target context x "demod1");()) res); match res with | None -> None | Some (sign, newcurrent) -> match passive_table with | None -> res | Some passive_table -> - match demodulate passive_table newcurrent with - | None -> None + match demodulate passive_table newcurrent with + | None -> None | Some (sign,newnewcurrent) -> - if newcurrent <> newnewcurrent then - demod newnewcurrent - else Some (sign,newnewcurrent) + if newcurrent <> newnewcurrent then + demod newnewcurrent + else Some (sign,newnewcurrent) in let res = demod current in match res with @@ -650,17 +650,17 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = else match passive_table with | None -> - if fst (Indexing.subsumption env active_table c) then - None - else - res + if fst (Indexing.subsumption env active_table c) then + None + else + res | Some passive_table -> if Indexing.in_index passive_table c then None else - let r1, _ = Indexing.subsumption env active_table c in - if r1 then None else - let r2, _ = Indexing.subsumption env passive_table c in - if r2 then None else res + let r1, _ = Indexing.subsumption env active_table c in + if r1 then None else + let r2, _ = Indexing.subsumption env passive_table c in + if r2 then None else res ;; type fs_time_info_t = { @@ -677,11 +677,11 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = if Utils.debug_metas then begin let m,c,u = env in - ignore(List.map - (fun current -> - Indexing.check_target c current "forward new neg") new_neg); - ignore(List.map - (fun current -> Indexing.check_target c current "forward new pos") + ignore(List.map + (fun current -> + Indexing.check_target c current "forward new neg") new_neg); + ignore(List.map + (fun current -> Indexing.check_target c current "forward new pos") new_pos;) end; let t1 = Unix.gettimeofday () in @@ -923,16 +923,16 @@ let close env new' given = List.fold_left (fun (n,p) (s,c) -> let neg,pos = infer env s c (new_pos,new_table) in - neg@n,pos@p) + neg@n,pos@p) ([],[]) given ;; let is_commutative_law eq = let w, proof, (eq_ty, left, right, order), metas = snd eq in match left,right with - Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], - Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] -> - f1 = f2 && a1 = b2 && a2 = b1 + Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], + Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] -> + f1 = f2 && a1 = b2 && a2 = b1 | _ -> false ;; @@ -1099,8 +1099,8 @@ let apply_equality_to_goal env equality goal = | I.NoProof -> newproof | I.BasicProof _ -> newproof | I.SubProof (t, i, p) -> - prerr_endline "SUBPROOF!"; - I.SubProof (t, i, repl p) + prerr_endline "SUBPROOF!"; + I.SubProof (t, i, repl p) | _ -> assert false in repl gproof @@ -1197,7 +1197,7 @@ let apply_to_goal env theorems ?passive active goal = | ProofSymBlock (s, sp) -> ProofSymBlock (s, gp sp) | ProofBlock (s, u, nt, t, pe, sp) -> - prerr_endline "apply_to_goal!"; + prerr_endline "apply_to_goal!"; ProofBlock (s, u, nt, t, pe, gp sp) in gp proof in @@ -1650,7 +1650,7 @@ and given_clause_aux dbd env goals theorems passive active = let (sign, current), passive = select env (fst goals) passive active in let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in prerr_endline ("Selected = " ^ - (CicPp.pp (Inference.term_of_equality current) names)); + (CicPp.pp (Inference.term_of_equality current) names)); let time1 = Unix.gettimeofday () in let res = forward_simplify env (sign, current) ~passive active in let time2 = Unix.gettimeofday () in @@ -1774,12 +1774,12 @@ let rec given_clause_fullred dbd env goals theorems passive active = let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in match (fst goals) with | (_, [proof, m, Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_ - when left = right && iseq uri -> - let p = + when left = right && iseq uri -> + let p = Cic.Appl [Cic.MutConstruct (* reflexivity *) - (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left] - in - let newp = + (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left] + in + let newp = let rec repl = function | Inference.ProofGoalBlock (_, gp) -> Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp) @@ -1791,50 +1791,59 @@ let rec given_clause_fullred dbd env goals theorems passive active = in repl proof in true, Some newp - | _ -> false, None + | (_, [proof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_-> + (* here we check if the goal is subsumed by an active *) + let ok, subst = + (* the first m is unused *) + Indexing.subsumption (m,context,CicUniv.empty_ugraph) + (snd active) + (0,proof,(eq_ty,left,right,Eq),m) + in + if ok then + begin + prerr_endline "The goal is subsumed by an active"; + false, None + end + else + ok, None + | _ -> false, None in if ok then - (* let proof = - match (fst goals) with - | (_, [proof, m, _])::_ -> - prerr_endline (CicMetaSubst.ppmetasenv [] m); Some proof - | _ -> assert false - in *) ( prerr_endline "esco qui"; let active = - List.filter test (fst active) in - let s = Printf.sprintf "actives:\n%s\n" - (String.concat "\n" + List.filter test (fst active) in + let s = Printf.sprintf "actives:\n%s\n" + (String.concat "\n" ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ + (fun (s, e) -> (string_of_sign s) ^ " " ^ (string_of_equality ~env e)) - active))) - in prerr_endline s; + active))) + in prerr_endline s; let passive = - List.filter - (fun x -> test (1,x)) - (let x,y,_ = passive in (fst x)@(fst y)) in - let p = Printf.sprintf "passives:\n%s\n" - (String.concat "\n" + List.filter + (fun x -> test (1,x)) + (let x,y,_ = passive in (fst x)@(fst y)) in + let p = Printf.sprintf "passives:\n%s\n" + (String.concat "\n" ((List.map - (fun e -> + (fun e -> (string_of_equality ~env e)) - passive))) - in prerr_endline p; + passive))) + in prerr_endline p; (* - let s = Printf.sprintf "actives:\n%s\n" - (String.concat "\n" + let s = Printf.sprintf "actives:\n%s\n" + (String.concat "\n" ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ + (fun (s, e) -> (string_of_sign s) ^ " " ^ (string_of_equality ~env e)) - (fst active)))) in - let sp = Printf.sprintf "passives:\n%s\n" - (String.concat "\n" + (fst active)))) in + let sp = Printf.sprintf "passives:\n%s\n" + (String.concat "\n" (List.map - (string_of_equality ~env) - (let x,y,_ = passive in (fst x)@(fst y)))) in - prerr_endline s; - prerr_endline sp; *) + (string_of_equality ~env) + (let x,y,_ = passive in (fst x)@(fst y)))) in + prerr_endline s; + prerr_endline sp; *) ParamodulationSuccess (proof, env)) else given_clause_fullred_aux dbd env goals theorems passive active @@ -1857,9 +1866,9 @@ let rec given_clause_fullred dbd env goals theorems passive active = and given_clause_fullred_aux dbd env goals theorems passive active = prerr_endline (string_of_int !counter ^ - " MAXMETA: " ^ string_of_int !maxmeta ^ + " MAXMETA: " ^ string_of_int !maxmeta ^ " LOCALMAX: " ^ string_of_int !Indexing.local_max ^ - " #ACTIVES: " ^ string_of_int (size_of_active active) ^ + " #ACTIVES: " ^ string_of_int (size_of_active active) ^ " #PASSIVES: " ^ string_of_int (size_of_passive passive)); incr counter; (* if !counter mod 10 = 0 then @@ -1872,12 +1881,12 @@ and given_clause_fullred_aux dbd env goals theorems passive active = let sizel = HExtlib.estimate_size (l1,l2) in let sizes = HExtlib.estimate_size (s1,s2) in - prerr_endline ("SIZE: " ^ string_of_int size); - prerr_endline ("SIZE P: " ^ string_of_int sizep); - prerr_endline ("SIZE A: " ^ string_of_int sizea); + prerr_endline ("SIZE: " ^ string_of_int size); + prerr_endline ("SIZE P: " ^ string_of_int sizep); + prerr_endline ("SIZE A: " ^ string_of_int sizea); prerr_endline ("SIZE TBL: " ^ string_of_int sizetbl ^ - " SIZE L: " ^ string_of_int sizel ^ - " SIZE S:" ^ string_of_int sizes); + " SIZE L: " ^ string_of_int sizel ^ + " SIZE S:" ^ string_of_int sizes); end;*) (* if (size_of_active active) mod 50 = 0 then @@ -1925,19 +1934,19 @@ and given_clause_fullred_aux dbd env goals theorems passive active = | false -> let (sign, current), passive = select env (fst goals) passive active in prerr_endline - ("Selected = " ^ (string_of_sign sign) ^ " " ^ - string_of_equality ~env current); + ("Selected = " ^ (string_of_sign sign) ^ " " ^ + string_of_equality ~env current); (* ^ - (let w,p,(t,l,r,o),m = current in - " size w: " ^ string_of_int (HExtlib.estimate_size w)^ - " size p: " ^ string_of_int (HExtlib.estimate_size p)^ - " size t: " ^ string_of_int (HExtlib.estimate_size t)^ - " size l: " ^ string_of_int (HExtlib.estimate_size l)^ - " size r: " ^ string_of_int (HExtlib.estimate_size r)^ - " size o: " ^ string_of_int (HExtlib.estimate_size o)^ - " size m: " ^ string_of_int (HExtlib.estimate_size m)^ - " size m-c: " ^ string_of_int - (HExtlib.estimate_size (List.map (fun (x,_,_) -> x) m)))) *) + (let w,p,(t,l,r,o),m = current in + " size w: " ^ string_of_int (HExtlib.estimate_size w)^ + " size p: " ^ string_of_int (HExtlib.estimate_size p)^ + " size t: " ^ string_of_int (HExtlib.estimate_size t)^ + " size l: " ^ string_of_int (HExtlib.estimate_size l)^ + " size r: " ^ string_of_int (HExtlib.estimate_size r)^ + " size o: " ^ string_of_int (HExtlib.estimate_size o)^ + " size m: " ^ string_of_int (HExtlib.estimate_size m)^ + " size m-c: " ^ string_of_int + (HExtlib.estimate_size (List.map (fun (x,_,_) -> x) m)))) *) let time1 = Unix.gettimeofday () in let res = forward_simplify env (sign, current) ~passive active in let time2 = Unix.gettimeofday () in @@ -1948,17 +1957,17 @@ and given_clause_fullred_aux dbd env goals theorems passive active = given_clause_fullred dbd env goals theorems passive active | Some (sign, current) -> if test (sign, current) then - (prerr_endline - ("Simplified = " ^ (string_of_sign sign) ^ " " ^ - string_of_equality ~env current); - let active = fst active in - let s = Printf.sprintf "actives:\n%s\n" - (String.concat "\n" + (prerr_endline + ("Simplified = " ^ (string_of_sign sign) ^ " " ^ + string_of_equality ~env current); + let active = fst active in + let s = Printf.sprintf "actives:\n%s\n" + (String.concat "\n" ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ + (fun (s, e) -> (string_of_sign s) ^ " " ^ (string_of_equality ~env e)) - active))) - in prerr_endline s; + active))) + in prerr_endline s; assert false); if (sign = Negative) && (is_identity env current) then ( debug_print @@ -1975,7 +1984,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = let t1 = Unix.gettimeofday () in let new' = infer env sign current active in - let _ = + let _ = match new' with | neg, pos -> debug_print @@ -2017,15 +2026,15 @@ and given_clause_fullred_aux dbd env goals theorems passive active = | Some (n, p), None | None, Some (n, p) -> let nn, np = new' in - if Utils.debug_metas then - begin - List.iter - (fun x->Indexing.check_target context x "simplify1") - n; - List.iter - (fun x->Indexing.check_target context x "simplify2") - p - end; + if Utils.debug_metas then + begin + List.iter + (fun x->Indexing.check_target context x "simplify1") + n; + List.iter + (fun x->Indexing.check_target context x "simplify2") + p + end; simplify (nn @ n, np @ p) active passive | Some (n, p), Some (rn, rp) -> let nn, np = new' in @@ -2033,7 +2042,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = in let active, _, new' = simplify new' active passive in (* pessima prova - let new1 = prova env new' active in + let new1 = prova env new' active in let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in let _ = match new1 with @@ -2294,29 +2303,29 @@ let main dbd full term metasenv ugraph = | ParamodulationSuccess (None, env) -> Printf.printf "Success, but no proof?!?\n\n" in - if Utils.time then - begin - prerr_endline - ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ + if Utils.time then + begin + prerr_endline + ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ "forward_simpl_new_time: %.9f\n" ^^ "backward_simpl_time: %.9f\n") !infer_time !forward_simpl_time !forward_simpl_new_time !backward_simpl_time) ^ - (Printf.sprintf "beta_expand_time: %.9f\n" - !Indexing.beta_expand_time) ^ - (Printf.sprintf "passive_maintainance_time: %.9f\n" - !passive_maintainance_time) ^ - (Printf.sprintf " successful unification/matching time: %.9f\n" - !Indexing.match_unif_time_ok) ^ - (Printf.sprintf " failed unification/matching time: %.9f\n" - !Indexing.match_unif_time_no) ^ - (Printf.sprintf " indexing retrieval time: %.9f\n" - !Indexing.indexing_retrieval_time) ^ - (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n" - !Indexing.build_newtarget_time) ^ - (Printf.sprintf "derived %d clauses, kept %d clauses.\n" - !derived_clauses !kept_clauses)) - end + (Printf.sprintf "beta_expand_time: %.9f\n" + !Indexing.beta_expand_time) ^ + (Printf.sprintf "passive_maintainance_time: %.9f\n" + !passive_maintainance_time) ^ + (Printf.sprintf " successful unification/matching time: %.9f\n" + !Indexing.match_unif_time_ok) ^ + (Printf.sprintf " failed unification/matching time: %.9f\n" + !Indexing.match_unif_time_no) ^ + (Printf.sprintf " indexing retrieval time: %.9f\n" + !Indexing.indexing_retrieval_time) ^ + (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n" + !Indexing.build_newtarget_time) ^ + (Printf.sprintf "derived %d clauses, kept %d clauses.\n" + !derived_clauses !kept_clauses)) + end (* with exc -> print_endline ("EXCEPTION: " ^ (Printexc.to_string exc)); @@ -2434,7 +2443,6 @@ let saturate debug_print (lazy "OK, found a proof!"); let proof = Inference.build_proof_term proof in (* prerr_endline (CicPp.ppterm proof); *) - let metasenv = (2839,context,Cic.Rel 17)::(214882,context,Cic.Rel 17)::metasenv in let names = names_of_context context in let newmetasenv = let i1 = @@ -2487,24 +2495,24 @@ let saturate let tdemodulate = fs_time_info.demodulate in let tsubsumption = fs_time_info.subsumption in if Utils.time then - begin - prerr_endline ( - (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^ - (Printf.sprintf "\ntall: %.9f" tall) ^ - (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^ - (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^ - (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^ - (Printf.sprintf "\nbeta_expand_time: %.9f\n" - !Indexing.beta_expand_time) ^ - (Printf.sprintf "\nmetas_of_proof: %.9f\n" - !Inference.metas_of_proof_time) ^ - (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^ - (Printf.sprintf "\nforward_simpl_new_times: %.9f" - !forward_simpl_new_time) ^ - (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^ - (Printf.sprintf "\npassive_maintainance_time: %.9f" - !passive_maintainance_time)) - end; + begin + prerr_endline ( + (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^ + (Printf.sprintf "\ntall: %.9f" tall) ^ + (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^ + (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^ + (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^ + (Printf.sprintf "\nbeta_expand_time: %.9f\n" + !Indexing.beta_expand_time) ^ + (Printf.sprintf "\nmetas_of_proof: %.9f\n" + !Inference.metas_of_proof_time) ^ + (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^ + (Printf.sprintf "\nforward_simpl_new_times: %.9f" + !forward_simpl_new_time) ^ + (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^ + (Printf.sprintf "\npassive_maintainance_time: %.9f" + !passive_maintainance_time)) + end; newstatus | _ -> raise (ProofEngineTypes.Fail (lazy "NO proof found")) @@ -2547,14 +2555,14 @@ let retrieve_and_print dbd term metasenv ugraph = debug_print (lazy (Printf.sprintf "\n\nequalities:\n%s\n" - (String.concat "\n" + (String.concat "\n" (List.map - (fun (u, e) -> -(* Printf.sprintf "%s: %s" *) - (UriManager.string_of_uri u) -(* (string_of_equality e) *) - ) - equalities)))); + (fun (u, e) -> +(* Printf.sprintf "%s: %s" *) + (UriManager.string_of_uri u) +(* (string_of_equality e) *) + ) + equalities)))); debug_print (lazy "RETR: SIMPLYFYING EQUALITIES..."); let rec simpl e others others_simpl = let (u, e) = e in @@ -2568,36 +2576,36 @@ let retrieve_and_print dbd term metasenv ugraph = let res = forward_simplify env (Positive, e) (active, tbl) in match others with | hd::tl -> ( - match res with - | None -> simpl hd tl others_simpl - | Some e -> simpl hd tl ((u, (snd e))::others_simpl) - ) + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl ((u, (snd e))::others_simpl) + ) | [] -> ( - match res with - | None -> others_simpl - | Some e -> (u, (snd e))::others_simpl - ) + match res with + | None -> others_simpl + | Some e -> (u, (snd e))::others_simpl + ) in let _equalities = match equalities with | [] -> [] | hd::tl -> - let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) - let res = - List.rev (simpl (*(Positive,*) hd others []) - in - debug_print - (lazy - (Printf.sprintf "\nequalities AFTER:\n%s\n" - (String.concat "\n" - (List.map - (fun (u, e) -> - Printf.sprintf "%s: %s" - (UriManager.string_of_uri u) - (string_of_equality e) - ) - res)))); - res in + let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) + let res = + List.rev (simpl (*(Positive,*) hd others []) + in + debug_print + (lazy + (Printf.sprintf "\nequalities AFTER:\n%s\n" + (String.concat "\n" + (List.map + (fun (u, e) -> + Printf.sprintf "%s: %s" + (UriManager.string_of_uri u) + (string_of_equality e) + ) + res)))); + res in debug_print (lazy (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) @@ -2709,15 +2717,15 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = begin let opengoal = Cic.Meta(maxm,irl) in let proofterm = - Inference.build_proof_term ~noproof:opengoal newproof in + Inference.build_proof_term ~noproof:opengoal newproof in let extended_metasenv = (maxm,context,newty)::metasenv in - let extended_status = - (curi,extended_metasenv,pbo,pty),goal in - let (status,newgoals) = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) - extended_status in - (status,maxm::newgoals) + let extended_status = + (curi,extended_metasenv,pbo,pty),goal in + let (status,newgoals) = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) + extended_status in + (status,maxm::newgoals) end else if newty = ty then raise (ProofEngineTypes.Fail (lazy "no progress")) -- 2.39.2