X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=b902dd86be7e1c98b8b0f6866228faa0092ea25c;hb=dbdd5bb6ea9a29c0a06bf29c6ff5db684c8ca0e9;hp=b3fa5f3fcd955d283fede4fef9ef6eea912a1edf;hpb=984df0f8feff95dcfdbdcebe6e23ace0b5529fa5;p=helm.git diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index b3fa5f3fc..b902dd86b 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -28,26 +28,10 @@ open Inference;; open Utils;; +let check_table t l = + List.fold_left + (fun b (_,eq) -> b && (Indexing.in_index t eq)) true l -(* -for debugging -let check_equation env equation msg = - let w, proof, (eq_ty, left, right, order), metas, args = equation in - let metasenv, context, ugraph = env in - let metasenv' = metasenv @ metas in - try - CicTypeChecker.type_of_aux' metasenv' context left ugraph; - CicTypeChecker.type_of_aux' metasenv' context right ugraph; - () - with - CicUtil.Meta_not_found _ as exn -> - begin - prerr_endline msg; - prerr_endline (CicPp.ppterm left); - prerr_endline (CicPp.ppterm right); - raise exn - end -*) (* set to false to disable paramodulation inside auto_tac *) let connect_to_auto = true;; @@ -91,6 +75,15 @@ let maxmeta = ref 0;; let maxdepth = ref 3;; let maxwidth = ref 3;; +let test eq = false +(* + let (_,(_,_,(ty,left,right,_),m1)) = eq in + let actual = + (Inference.metas_of_term left)@(Inference.metas_of_term right) + in + let m = List.filter (fun (i, _, _) -> List.mem i actual) m1 in + m <> m1 +;; *) type result = | ParamodulationFailure @@ -101,7 +94,7 @@ type goal = proof * Cic.metasenv * Cic.term;; type theorem = Cic.term * Cic.term * Cic.metasenv;; -let symbols_of_equality (_, _, (_, left, right, _), _, _) = +let symbols_of_equality (_, _, (_, left, right, _), _) = let m1 = symbols_of_term left in let m = TermMap.fold @@ -116,26 +109,57 @@ let symbols_of_equality (_, _, (_, left, right, _), _, _) = m ;; -module OrderedEquality = struct +(* griggio *) +module OrderedEquality = struct type t = Inference.equality let compare eq1 eq2 = match meta_convertibility_eq eq1 eq2 with | true -> 0 | false -> - let w1, _, (ty, left, right, _), _, a = eq1 - and w2, _, (ty', left', right', _), _, a' = eq2 in + let w1, _, (ty, left, right, _), m1 = eq1 + and w2, _, (ty', left', right', _), m2 = eq2 in match Pervasives.compare w1 w2 with + | 0 -> + let res = (List.length m1) - (List.length m2) in + if res <> 0 then res else Pervasives.compare eq1 eq2 + | res -> res +end + +(* +module OrderedEquality = struct + type t = Inference.equality + + 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 + + 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 -> - let res = (List.length a) - (List.length a') in - if res <> 0 then res else ( - try - let res = Pervasives.compare (List.hd a) (List.hd a') in - if res <> 0 then res else Pervasives.compare eq1 eq2 - with Failure "hd" -> Pervasives.compare eq1 eq2 - ) - | 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 + | res -> res end +*) module EqualitySet = Set.Make(OrderedEquality);; @@ -208,7 +232,6 @@ let rec select env goals passive (active, _) = (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table) | [], (hd:EqualitySet.elt)::tl -> - let w,_,_,_,_ = hd in let passive_table = Indexing.remove_index passive_table hd in (Positive, hd), @@ -261,7 +284,7 @@ let rec select env goals passive (active, _) = | _ -> symbols_counter := !symbols_ratio; let set_selection set = EqualitySet.min_elt set in - (* let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in *) + (* let set_selection l = min_elt (fun (w,_,_,_) -> w) l in *) if EqualitySet.is_empty neg_set then let current = set_selection pos_set in let passive = @@ -307,8 +330,8 @@ let add_to_passive passive (new_neg, new_pos) = let ok set equality = not (EqualitySet.mem equality set) in let neg = List.filter (ok neg_set) new_neg and pos = List.filter (ok pos_set) new_pos in - let table = - List.fold_left (fun tbl e -> Indexing.index tbl e) table pos + let table = + List.fold_left (fun tbl e -> Indexing.index tbl e) table pos in let add set equalities = List.fold_left (fun s e -> EqualitySet.add e s) set equalities @@ -468,8 +491,12 @@ let infer env sign current (active_list, active_table) = let neg, pos = infer_positive table tl in neg, res @ pos in + let maxm, copy_of_current = Inference.fix_metas !maxmeta current in + maxmeta := maxm; let curr_table = Indexing.index Indexing.empty current in - let neg, pos = infer_positive curr_table active_list 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 -> @@ -542,7 +569,7 @@ let contains_empty env (negative, positive) = try let found = List.find - (fun (w, proof, (ty, left, right, ordering), m, a) -> + (fun (w, proof, (ty, left, right, ordering), m) -> fst (CicReduction.are_convertible context left right ugraph)) negative in @@ -587,20 +614,27 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = else Some (sign, newcurrent) in - let res = + let rec demod current = if Utils.debug_metas then ignore (Indexing.check_target context current "demod0"); let res = demodulate active_table current in if Utils.debug_metas then ignore ((function None -> () | Some (_,x) -> - Indexing.check_target context x "demod1";()) res); + 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 -> demodulate passive_table newcurrent - in + | Some passive_table -> + match demodulate passive_table newcurrent with + | None -> None + | Some (sign,newnewcurrent) -> + if newcurrent <> newnewcurrent then + demod newnewcurrent + else Some (sign,newnewcurrent) + in + let res = demod current in match res with | None -> None | Some (Negative, c) -> @@ -723,13 +757,69 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = ;; +(** simplifies a goal with equalities in active and passive *) +let rec simplify_goal env goal ?passive (active_list, active_table) = + let pl, passive_table = + match passive with + | None -> [], None + | Some ((pn, _), (pp, _), pt) -> + let pn = List.map (fun e -> (Negative, e)) pn + and pp = List.map (fun e -> (Positive, e)) pp in + pn @ pp, Some pt + in + + let demodulate table goal = + let newmeta, newgoal = + Indexing.demodulation_goal !maxmeta env table goal in + maxmeta := newmeta; + goal <> newgoal, newgoal + in + let changed, goal = + match passive_table with + | None -> demodulate active_table goal + | Some passive_table -> + let changed, goal = demodulate active_table goal in + let changed', goal = demodulate passive_table goal in + (changed || changed'), goal + in + changed, if not changed then goal + else snd (simplify_goal env goal ?passive (active_list, active_table)) +;; + + +let simplify_goals env goals ?passive active = + let a_goals, p_goals = goals in + let p_goals = + List.map + (fun (d, gl) -> + let gl = + List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in + d, gl) + p_goals + in + let goals = + List.fold_left + (fun (a, p) (d, gl) -> + let changed = ref false in + let gl = + List.map + (fun g -> + let c, g = simplify_goal env g ?passive active in + changed := !changed || c; g) gl in + if !changed then (a, (d, gl)::p) else ((d, gl)::a, p)) + ([], p_goals) a_goals + in + goals +;; + + (** simplifies active usign new *) let backward_simplify_active env new_pos new_table min_weight active = let active_list, active_table = active in let active_list, newa = List.fold_right (fun (s, equality) (res, newn) -> - let ew, _, _, _, _ = equality in + let ew, _, _, _ = equality in if ew < min_weight then (s, equality)::res, newn else @@ -775,7 +865,7 @@ let backward_simplify_active env new_pos new_table min_weight active = let backward_simplify_passive env new_pos new_table min_weight passive = let (nl, ns), (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = - let ew, _, _, _, _ = equality in + let ew, _, _, _ = equality in if ew < min_weight then equality::resl, ress, newn else @@ -804,7 +894,7 @@ let backward_simplify env new' ?passive active = let new_pos, new_table, min_weight = List.fold_left (fun (l, t, w) e -> - let ew, _, _, _, _ = e in + let ew, _, _, _ = e in (Positive, e)::l, Indexing.index t e, min ew w) ([], Indexing.empty, 1000000) (snd new') in @@ -826,7 +916,7 @@ let close env new' given = let new_pos, new_table, min_weight = List.fold_left (fun (l, t, w) e -> - let ew, _, _, _, _ = e in + let ew, _, _, _ = e in (Positive, e)::l, Indexing.index t e, min ew w) ([], Indexing.empty, 1000000) (snd new') in @@ -838,7 +928,7 @@ let close env new' given = ;; let is_commutative_law eq = - let w, proof, (eq_ty, left, right, order), metas, args = snd eq in + 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] -> @@ -899,60 +989,6 @@ let activate_theorem (active, passive) = ;; -(** simplifies a goal with equalities in active and passive *) -let simplify_goal env goal ?passive (active_list, active_table) = - let pl, passive_table = - match passive with - | None -> [], None - | Some ((pn, _), (pp, _), pt) -> - let pn = List.map (fun e -> (Negative, e)) pn - and pp = List.map (fun e -> (Positive, e)) pp in - pn @ pp, Some pt - in - - let demodulate table goal = - let newmeta, newgoal = - Indexing.demodulation_goal !maxmeta env table goal in - maxmeta := newmeta; - goal != newgoal, newgoal - in - let changed, goal = - match passive_table with - | None -> demodulate active_table goal - | Some passive_table -> - let changed, goal = demodulate active_table goal in - let changed', goal = demodulate passive_table goal in - (changed || changed'), goal - in - changed, goal -;; - - -let simplify_goals env goals ?passive active = - let a_goals, p_goals = goals in - let p_goals = - List.map - (fun (d, gl) -> - let gl = - List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in - d, gl) - p_goals - in - let goals = - List.fold_left - (fun (a, p) (d, gl) -> - let changed = ref false in - let gl = - List.map - (fun g -> - let c, g = simplify_goal env g ?passive active in - changed := !changed || c; g) gl in - if !changed then (a, (d, gl)::p) else ((d, gl)::a, p)) - ([], p_goals) a_goals - in - goals -;; - let simplify_theorems env theorems ?passive (active_list, active_table) = let pl, passive_table = @@ -1031,13 +1067,14 @@ let simplify_equalities env equalities = res ;; +(* (* applies equality to goal to see if the goal can be closed *) let apply_equality_to_goal env equality goal = let module C = Cic in let module HL = HelmLibraryObjects in let module I = Inference in let metasenv, context, ugraph = env in - let _, proof, (ty, left, right, _), metas, args = equality in + let _, proof, (ty, left, right, _), metas = equality in let eqterm = C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in let gproof, gmetas, gterm = goal in @@ -1047,12 +1084,11 @@ let apply_equality_to_goal env equality goal = (* (string_of_equality equality) (CicPp.ppterm gterm))); *) try let subst, metasenv', _ = - let menv = metasenv @ metas @ gmetas in Inference.unification metas gmetas context eqterm gterm ugraph in let newproof = match proof with - | I.BasicProof t -> I.BasicProof (CicMetaSubst.apply_subst subst t) + | I.BasicProof (subst',t) -> I.BasicProof (subst@subst',t) | I.ProofBlock (s, uri, nt, t, pe, p) -> I.ProofBlock (subst @ s, uri, nt, t, pe, p) | _ -> assert false @@ -1061,13 +1097,15 @@ let apply_equality_to_goal env equality goal = let rec repl = function | I.ProofGoalBlock (_, gp) -> I.ProofGoalBlock (newproof, gp) | I.NoProof -> newproof - | I.BasicProof p -> newproof - | I.SubProof (t, i, p) -> I.SubProof (t, i, repl p) + | I.BasicProof _ -> newproof + | I.SubProof (t, i, p) -> + prerr_endline "SUBPROOF!"; + I.SubProof (t, i, repl p) | _ -> assert false in repl gproof in - true, subst, newgproof + true, (subst:Inference.substitution), newgproof with CicUnification.UnificationFailure _ -> false, [], I.NoProof ;; @@ -1126,9 +1164,9 @@ let apply_to_goal env theorems ?passive active goal = let newp = let rec repl = function | Inference.ProofGoalBlock (_, gp) -> - Inference.ProofGoalBlock (Inference.BasicProof p, gp) - | Inference.NoProof -> Inference.BasicProof p - | Inference.BasicProof _ -> Inference.BasicProof p + Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp) + | Inference.NoProof -> Inference.BasicProof ([],p) + | Inference.BasicProof _ -> Inference.BasicProof ([],p) | Inference.SubProof (t, i, p2) -> Inference.SubProof (t, i, repl p2) | _ -> assert false @@ -1155,10 +1193,11 @@ let apply_to_goal env theorems ?passive active goal = ProofGoalBlock (sp1, gp sp2) | BasicProof _ | NoProof -> - SubProof (p, i, BasicProof (Cic.Meta (i, irl))) + SubProof (p, i, BasicProof ([],Cic.Meta (i, irl))) | ProofSymBlock (s, sp) -> ProofSymBlock (s, gp sp) | ProofBlock (s, u, nt, t, pe, sp) -> + prerr_endline "apply_to_goal!"; ProofBlock (s, u, nt, t, pe, gp sp) in gp proof in @@ -1206,7 +1245,7 @@ let apply_to_goal env theorems ?passive active goal = else false, [], [] in - if r = true then `Ok (s, l) else aux theorems + if r = true then `Ok ((s:Cic.substitution),l) else aux theorems ;; @@ -1255,13 +1294,13 @@ let rec apply_to_goal_conj env theorems ?passive active (depth, goals) = let propagate_subst subst (proof, metas, term) = let rec repl = function | NoProof -> NoProof - | BasicProof t -> - BasicProof (CicMetaSubst.apply_subst subst t) + | BasicProof (subst',t) -> + BasicProof (subst@subst',t) | ProofGoalBlock (p, pb) -> let pb' = repl pb in ProofGoalBlock (p, pb') | SubProof (t, i, p) -> - let t' = CicMetaSubst.apply_subst subst t in + let t' = Inference.apply_subst subst t in let p = repl p in SubProof (t', i, p) | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p) @@ -1543,10 +1582,8 @@ let apply_theorem_to_goals env theorems active goals = ok, (a_goals, p_goals) ;; - (* given-clause algorithm with lazy reduction strategy *) let rec given_clause dbd env goals theorems passive active = - let _,context,_ = env in let goals = simplify_goals env goals active in let ok, goals = activate_goal goals in (* let theorems = simplify_theorems env theorems active in *) @@ -1626,7 +1663,7 @@ and given_clause_aux dbd env goals theorems passive active = debug_print (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current))); - let _, proof, _, _, _ = current in + let _, proof, _, _ = current in ParamodulationSuccess (Some proof, env) ) else ( debug_print @@ -1644,7 +1681,7 @@ and given_clause_aux dbd env goals theorems passive active = if res then let proof = match goal' with - | Some goal -> let _, proof, _, _, _ = goal in Some proof + | Some goal -> let _, proof, _, _ = goal in Some proof | None -> None in ParamodulationSuccess (proof, env) @@ -1696,16 +1733,22 @@ and given_clause_aux dbd env goals theorems passive active = let proof = match goal with | Some goal -> - let _, proof, _, _, _ = goal in Some proof + let _, proof, _, _ = goal in Some proof | None -> None in ParamodulationSuccess (proof, env) ) ;; +*) +let counter = ref 0 (** given-clause algorithm with full reduction strategy *) let rec given_clause_fullred dbd env goals theorems passive active = +(* + let table,list = active in + assert (check_table list table); +*) let goals = simplify_goals env goals ~passive active in let _,context,_ = env in let ok, goals = activate_goal goals in @@ -1726,16 +1769,59 @@ let rec given_clause_fullred dbd env goals theorems passive active = (* (Printf.sprintf "goal activated:\n%s\n%s\n" *) (* (CicPp.ppterm t) (string_of_proof p))); *) (* in *) - let ok, goals = - apply_goal_to_theorems dbd env theorems ~passive active goals - in + let ok, proof = + (* apply_goal_to_theorems dbd env theorems ~passive active goals in *) + 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 = + Cic.Appl [Cic.MutConstruct (* reflexivity *) + (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left] + in + let newp = + let rec repl = function + | Inference.ProofGoalBlock (_, gp) -> + Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp) + | Inference.NoProof -> Inference.BasicProof ([],p) + | Inference.BasicProof _ -> Inference.BasicProof ([],p) + | Inference.SubProof (t, i, p2) -> + Inference.SubProof (t, i, repl p2) + | _ -> assert false + in + repl proof + in true, Some newp + | _ -> false, None + in if ok then - let proof = + (* let proof = match (fst goals) with - | (_, [proof, _, _])::_ -> Some proof + | (_, [proof, m, _])::_ -> + prerr_endline (CicMetaSubst.ppmetasenv [] m); Some proof | _ -> assert false - in + 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.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) + 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.map + (fun e -> + (string_of_equality ~env e)) + passive))) + in prerr_endline p; + (* let s = Printf.sprintf "actives:\n%s\n" (String.concat "\n" ((List.map @@ -1748,7 +1834,7 @@ let rec given_clause_fullred dbd env goals theorems passive active = (string_of_equality ~env) (let x,y,_ = passive in (fst x)@(fst y)))) in prerr_endline s; - prerr_endline sp; + prerr_endline sp; *) ParamodulationSuccess (proof, env)) else given_clause_fullred_aux dbd env goals theorems passive active @@ -1770,11 +1856,31 @@ let rec given_clause_fullred dbd env goals theorems passive active = else given_clause_fullred_aux dbd env goals theorems passive active and given_clause_fullred_aux dbd env goals theorems passive active = - prerr_endline ("MAXMETA: " ^ string_of_int !maxmeta ^ + prerr_endline (string_of_int !counter ^ + " MAXMETA: " ^ string_of_int !maxmeta ^ " LOCALMAX: " ^ string_of_int !Indexing.local_max ^ " #ACTIVES: " ^ string_of_int (size_of_active active) ^ " #PASSIVES: " ^ string_of_int (size_of_passive passive)); - if (size_of_active active) mod 54 = 0 then + incr counter; +(* if !counter mod 10 = 0 then + begin + let size = HExtlib.estimate_size (passive,active) in + let sizep = HExtlib.estimate_size (passive) in + let sizea = HExtlib.estimate_size (active) in + let (l1,s1),(l2,s2), t = passive in + let sizetbl = HExtlib.estimate_size t in + 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 TBL: " ^ string_of_int sizetbl ^ + " SIZE L: " ^ string_of_int sizel ^ + " SIZE S:" ^ string_of_int sizes); + end;*) +(* + if (size_of_active active) mod 50 = 0 then (let s = Printf.sprintf "actives:\n%s\n" (String.concat "\n" ((List.map @@ -1787,7 +1893,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = (string_of_equality ~env) (let x,y,_ = passive in (fst x)@(fst y)))) in prerr_endline s; - prerr_endline sp); + prerr_endline sp); *) let time1 = Unix.gettimeofday () in let (_,context,_) = env in let selection_estimate = get_selection_estimate () in @@ -1818,23 +1924,47 @@ and given_clause_fullred_aux dbd env goals theorems passive active = given_clause_fullred dbd env goals theorems passive active | false -> 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 = " ^ (string_of_sign sign) ^ " " ^ - string_of_equality ~env current); - (* (CicPp.pp (Inference.term_of_equality current) names));*) + prerr_endline + ("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 time1 = Unix.gettimeofday () in let res = forward_simplify env (sign, current) ~passive active in let time2 = Unix.gettimeofday () in forward_simpl_time := !forward_simpl_time +. (time2 -. time1); match res with | None -> + (* weight_age_counter := !weight_age_counter + 1; *) 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" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) + active))) + in prerr_endline s; + assert false); if (sign = Negative) && (is_identity env current) then ( debug_print (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current))); - let _, proof, _, _, _ = current in + let _, proof, _, m = current in ParamodulationSuccess (Some proof, env) ) else ( debug_print @@ -1872,13 +2002,14 @@ and given_clause_fullred_aux dbd env goals theorems passive active = in let rec simplify new' active passive = let t1 = Unix.gettimeofday () in - let new' = forward_simplify_new env new' ~passive active in + let new' = forward_simplify_new env new'~passive active in let t2 = Unix.gettimeofday () in forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1); let t1 = Unix.gettimeofday () in let active, passive, newa, retained = - backward_simplify env new' ~passive active in + backward_simplify env new' ~passive active in + let t2 = Unix.gettimeofday () in backward_simpl_time := !backward_simpl_time +. (t2 -. t1); match newa, retained with @@ -1887,15 +2018,20 @@ and given_clause_fullred_aux dbd env goals theorems passive active = | None, Some (n, p) -> let nn, np = new' in if Utils.debug_metas then - ignore ( - List.map (fun x -> Indexing.check_target context x "simplify1")n; - List.map (fun x -> Indexing.check_target context x "simplify2")p); - simplify (nn @ n, np @ p) active passive + 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 simplify (nn @ n @ rn, np @ p @ rp) active passive in - let active, passive, new' = simplify new' active passive in + let active, _, new' = simplify new' active passive in (* pessima prova let new1 = prova env new' active in let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in @@ -1949,13 +2085,20 @@ end prova *) | true, goal -> let proof = match goal with - | Some goal -> let _, proof, _, _, _ = goal in Some proof + | Some goal -> let _, proof, _, _ = goal in Some proof | None -> None in ParamodulationSuccess (proof, env) ) + ;; +let profiler0 = HExtlib.profile "P/Saturation.given_clause_fullred" + +let given_clause_fullred dbd env goals theorems passive active = + profiler0.HExtlib.profile + (given_clause_fullred dbd env goals theorems passive) active + let rec saturate_equations env goal accept_fun passive active = elapsed_time := Unix.gettimeofday () -. !start_time; @@ -2089,7 +2232,7 @@ let main dbd full term metasenv ugraph = (fst theorems))))) in (*try*) - let goal = Inference.BasicProof new_meta_goal, [], goal in + let goal = Inference.BasicProof ([],new_meta_goal), [], goal in let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in @@ -2109,7 +2252,7 @@ let main dbd full term metasenv ugraph = start_time := Unix.gettimeofday (); let res = let goals = make_goals goal in - (if !use_fullred then given_clause_fullred else given_clause) + (if !use_fullred then given_clause_fullred else given_clause_fullred) dbd env goals theorems passive active in let finish = Unix.gettimeofday () in @@ -2127,7 +2270,7 @@ let main dbd full term metasenv ugraph = print_endline (PP.pp proof names); let newmetasenv = List.fold_left - (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities + (fun m (_, _, _, menv) -> m @ menv) metasenv equalities in let _ = (*try*) @@ -2205,17 +2348,19 @@ let reset_refs () = Inference.metas_of_proof_time := 0.; ;; -let saturate +let saturate dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in reset_refs (); Indexing.init_index (); maxdepth := depth; maxwidth := width; +(* CicUnification.unif_ty := false;*) let proof, goal = status in let goal' = goal in let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in + prerr_endline ("CTX: " ^ string_of_int (HExtlib.estimate_size context)); let eq_indexes, equalities, maxm = find_equalities context proof in let new_meta_goal, metasenv, type_of_goal = let irl = @@ -2228,8 +2373,8 @@ let saturate ty in let ugraph = CicUniv.empty_ugraph in - let env = (metasenv, context, ugraph) in - let goal = Inference.BasicProof new_meta_goal, [], goal in + let env = (metasenv, context, ugraph) in + let goal = Inference.BasicProof ([],new_meta_goal), [], goal in let res, time = let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = @@ -2285,9 +2430,11 @@ let saturate (res, finish -. start) in match res with - | ParamodulationSuccess (Some proof, env) -> + | ParamodulationSuccess (Some proof, _) -> 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,7 +2634,7 @@ let main_demod_equalities dbd term metasenv ugraph = in let env = (metasenv, context, ugraph) in (*try*) - let goal = Inference.BasicProof new_meta_goal, [], goal in + let goal = Inference.BasicProof ([],new_meta_goal), [], goal in let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in let passive = make_passive [] equalities in @@ -2547,7 +2694,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let library_equalities = List.map snd library_equalities in let goalterm = Cic.Meta (metano,irl) in - let initgoal = Inference.BasicProof goalterm, [], ty in + let initgoal = Inference.BasicProof ([],goalterm), [], ty in let env = (metasenv, context, CicUniv.empty_ugraph) in let equalities = simplify_equalities env (equalities@library_equalities) in let table =