X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=8e67bc7a05cee8147a2f0a774f56f0fe7073d12e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=4cf14ae18a4baf579c13e8f54db8d8f68d57b962;hpb=d2b3f3c816a651cbed998976a343f83cad1be69c;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 4cf14ae18..8e67bc7a0 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -1,3 +1,28 @@ +(* 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://cs.unibo.it/helm/. + *) + open Inference;; open Utils;; @@ -48,12 +73,10 @@ type result = | ParamodulationSuccess of Inference.proof option * environment ;; +type goal = proof * Cic.metasenv * Cic.term;; + +type theorem = Cic.term * Cic.term * Cic.metasenv;; -(* -let symbols_of_equality (_, (_, left, right), _, _) = - TermSet.union (symbols_of_term left) (symbols_of_term right) -;; -*) let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) = let m1 = symbols_of_term left in @@ -67,10 +90,6 @@ let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) = TermMap.add k v res) (symbols_of_term right) m1 in -(* Printf.printf "symbols_of_equality %s:\n" *) -(* (string_of_equality equality); *) -(* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *) -(* print_newline (); *) m ;; @@ -84,9 +103,6 @@ module OrderedEquality = struct | false -> let w1, _, (ty, left, right, _), _, a = eq1 and w2, _, (ty', left', right', _), _, a' = eq2 in -(* let weight_of t = fst (weight_of_term ~consider_metas:false t) in *) -(* let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *) -(* and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *) match Pervasives.compare w1 w2 with | 0 -> let res = (List.length a) - (List.length a') in @@ -95,11 +111,6 @@ module OrderedEquality = struct 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 -(* match a, a' with *) -(* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *) -(* let res = Pervasives.compare i j in *) -(* if res <> 0 then res else Pervasives.compare eq1 eq2 *) -(* | _, _ -> Pervasives.compare eq1 eq2 *) ) | res -> res end @@ -107,13 +118,15 @@ end module EqualitySet = Set.Make(OrderedEquality);; +(** + selects one equality from passive. The selection strategy is a combination + of weight, age and goal-similarity +*) let select env goals passive (active, _) = processed_clauses := !processed_clauses + 1; - let goal = match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false in - let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in let remove eq l = List.filter (fun e -> e <> eq) l @@ -131,8 +144,6 @@ let select env goals passive (active, _) = | [], hd::tl -> let passive_table = Indexing.remove_index passive_table hd -(* if !use_fullred then Indexing.remove_index passive_table hd *) -(* else passive_table *) in (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table) @@ -143,67 +154,43 @@ let select env goals passive (active, _) = let cardinality map = TermMap.fold (fun k v res -> res + v) map 0 in -(* match active with *) -(* | (Negative, e)::_ -> *) -(* let symbols = symbols_of_equality e in *) let symbols = let _, _, term = goal in symbols_of_term term in - let card = cardinality symbols in - let foldfun k v (r1, r2) = - if TermMap.mem k symbols then - let c = TermMap.find k symbols in - let c1 = abs (c - v) in - let c2 = v - c1 in - r1 + c2, r2 + c1 - else - r1, r2 + v - in - let f equality (i, e) = - let common, others = - TermMap.fold foldfun (symbols_of_equality equality) (0, 0) - in - let c = others + (abs (common - card)) in - if c < i then (c, equality) -(* else if c = i then *) -(* match OrderedEquality.compare equality e with *) -(* | -1 -> (c, equality) *) -(* | res -> (i, e) *) - else (i, e) - in - let e1 = EqualitySet.min_elt pos_set in - let initial = - let common, others = - TermMap.fold foldfun (symbols_of_equality e1) (0, 0) - in - (others + (abs (common - card))), e1 - in - let _, current = EqualitySet.fold f pos_set initial in -(* Printf.printf "\nsymbols-based selection: %s\n\n" *) -(* (string_of_equality ~env current); *) - let passive_table = - Indexing.remove_index passive_table current -(* if !use_fullred then Indexing.remove_index passive_table current *) -(* else passive_table *) - in - (Positive, current), - (([], neg_set), - (remove current pos_list, EqualitySet.remove current pos_set), - passive_table) -(* | _ -> *) -(* let current = EqualitySet.min_elt pos_set in *) -(* let passive_table = *) -(* Indexing.remove_index passive_table current *) -(* (\* if !use_fullred then Indexing.remove_index passive_table current *\) *) -(* (\* else passive_table *\) *) -(* in *) -(* let passive = *) -(* (neg_list, neg_set), *) -(* (remove current pos_list, EqualitySet.remove current pos_set), *) -(* passive_table *) -(* in *) -(* (Positive, current), passive *) + let card = cardinality symbols in + let foldfun k v (r1, r2) = + if TermMap.mem k symbols then + let c = TermMap.find k symbols in + let c1 = abs (c - v) in + let c2 = v - c1 in + r1 + c2, r2 + c1 + else + r1, r2 + v + in + let f equality (i, e) = + let common, others = + TermMap.fold foldfun (symbols_of_equality equality) (0, 0) + in + let c = others + (abs (common - card)) in + if c < i then (c, equality) + else (i, e) + in + let e1 = EqualitySet.min_elt pos_set in + let initial = + let common, others = + TermMap.fold foldfun (symbols_of_equality e1) (0, 0) + in + (others + (abs (common - card))), e1 + in + let _, current = EqualitySet.fold f pos_set initial in + let passive_table = + Indexing.remove_index passive_table current + in + (Positive, current), + (([], neg_set), + (remove current pos_list, EqualitySet.remove current pos_set), + passive_table) ) | _ -> symbols_counter := !symbols_ratio; @@ -214,8 +201,6 @@ let select env goals passive (active, _) = (neg_list, neg_set), (remove current pos_list, EqualitySet.remove current pos_set), Indexing.remove_index passive_table current -(* if !use_fullred then Indexing.remove_index passive_table current *) -(* else passive_table *) in (Positive, current), passive else @@ -229,6 +214,7 @@ let select env goals passive (active, _) = ;; +(* initializes the passive set of equalities *) let make_passive neg pos = let set_of equalities = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities @@ -236,11 +222,6 @@ let make_passive neg pos = let table = List.fold_left (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pos -(* if !use_fullred then *) -(* List.fold_left (fun tbl e -> Indexing.index tbl e) *) -(* (Indexing.empty_table ()) pos *) -(* else *) -(* Indexing.empty_table () *) in (neg, set_of neg), (pos, set_of pos), @@ -253,17 +234,15 @@ let make_active () = ;; +(* adds to passive a list of equalities: new_neg is a list of negative + equalities, new_pos a list of positive equalities *) let add_to_passive passive (new_neg, new_pos) = let (neg_list, neg_set), (pos_list, pos_set), table = passive in 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 -(* if !use_fullred then *) -(* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *) -(* else *) -(* 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 @@ -290,6 +269,8 @@ let size_of_active (active_list, _) = ;; +(* removes from passive equalities that are estimated impossible to activate + within the current time limit *) let prune_passive howmany (active, _) passive = let (nl, ns), (pl, ps), tbl = passive in let howmany = float_of_int howmany @@ -362,8 +343,6 @@ let prune_passive howmany (active, _) passive = else EqualitySet.empty, EqualitySet.empty in -(* let in_weight, ns = pickw in_weight ns in *) -(* let _, ps = pickw in_weight ps in *) let ns, ps = pickw in_weight ns ps in let rec picka w s l = if w > 0 then @@ -381,21 +360,16 @@ let prune_passive howmany (active, _) passive = let in_age, ns, nl = picka in_age ns nl in let _, ps, pl = picka in_age ps pl in if not (EqualitySet.is_empty ps) then -(* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *) maximal_retained_equality := Some (EqualitySet.max_elt ps); let tbl = EqualitySet.fold (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) -(* if !use_fullred then *) -(* EqualitySet.fold *) -(* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *) -(* else *) -(* tbl *) in (nl, ns), (pl, ps), tbl ;; +(** inference of new equalities between current and some in active *) let infer env sign current (active_list, active_table) = let new_neg, new_pos = match sign with @@ -494,6 +468,7 @@ let contains_empty env (negative, positive) = ;; +(** simplifies current using active and passive *) let forward_simplify env (sign, current) ?passive (active_list, active_table) = let pl, passive_table = match passive with @@ -504,24 +479,6 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = pn @ pp, Some pt in let all = if pl = [] then active_list else active_list @ pl in - - (* let rec find_duplicate sign current = function *) -(* | [] -> false *) -(* | (s, eq)::tl when s = sign -> *) -(* if meta_convertibility_eq current eq then true *) -(* else find_duplicate sign current tl *) -(* | _::tl -> find_duplicate sign current tl *) -(* in *) - -(* let res = *) -(* if sign = Positive then *) -(* Indexing.subsumption env active_table current *) -(* else *) -(* false *) -(* in *) -(* if res then *) -(* None *) -(* else *) let demodulate table current = let newmeta, newcurrent = @@ -529,7 +486,19 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = maxmeta := newmeta; if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) - else None + 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 + ) else Some (sign, newcurrent) in @@ -556,34 +525,18 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = None else match passive_table with - | None -> res + | None -> + 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 res - -(* | Some (s, c) -> if find_duplicate s c all then None else res *) - -(* if s = Utils.Negative then *) -(* res *) -(* else *) -(* if Indexing.subsumption env active_table c then *) -(* None *) -(* else ( *) -(* match passive_table with *) -(* | None -> res *) -(* | Some passive_table -> *) -(* if Indexing.subsumption env passive_table c then *) -(* None *) -(* else *) -(* res *) -(* ) *) - -(* let pred (sign, eq) = *) -(* if sign <> s then false *) -(* else subsumption env c eq *) -(* in *) -(* if List.exists pred all then None *) -(* else res *) + 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 ;; type fs_time_info_t = { @@ -595,6 +548,7 @@ type fs_time_info_t = { let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };; +(** simplifies new using active and passive *) let forward_simplify_new env (new_neg, new_pos) ?passive active = let t1 = Unix.gettimeofday () in @@ -618,11 +572,6 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = maxmeta := newmeta; newtarget in -(* let f sign' target (sign, eq) = *) -(* if sign <> sign' then false *) -(* else subsumption env target eq *) -(* in *) - let t1 = Unix.gettimeofday () in let new_neg, new_pos = @@ -657,22 +606,9 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = (fun e -> not ((fst (Indexing.subsumption env active_table e)) || (fst (Indexing.subsumption env passive_table e)))) in - - let t1 = Unix.gettimeofday () in - -(* let new_neg, new_pos = *) -(* List.filter subs new_neg, *) -(* List.filter subs new_pos *) -(* in *) - -(* let new_neg, new_pos = *) -(* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *) -(* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *) -(* in *) - - let t2 = Unix.gettimeofday () in - fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); - +(* let t1 = Unix.gettimeofday () in *) +(* let t2 = Unix.gettimeofday () in *) +(* fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); *) let is_duplicate = match passive_table with | None -> @@ -682,18 +618,11 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = not ((Indexing.in_index active_table e) || (Indexing.in_index passive_table e))) in - new_neg, List.filter is_duplicate new_pos - -(* new_neg, new_pos *) - -(* let res = *) -(* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *) -(* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *) -(* in *) -(* res *) + new_neg, List.filter subs (List.filter is_duplicate new_pos) ;; +(** 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 = @@ -722,8 +651,7 @@ let backward_simplify_active env new_pos new_table min_weight active = res, tbl else if (is_identity env eq) || (find eq res) then ( res, tbl - ) (* else if (find eq res) then *) -(* res, tbl *) + ) else (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) active_list ([], Indexing.empty_table ()), @@ -742,12 +670,12 @@ let backward_simplify_active env new_pos new_table min_weight active = ;; +(** simplifies passive using new *) 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 if ew < min_weight then -(* let _ = debug_print (lazy (Printf.sprintf "OK: %d %d" ew min_weight)) in *) equality::resl, ress, newn else match forward_simplify env (sign, equality) (new_pos, new_table) with @@ -791,15 +719,46 @@ let backward_simplify env new' ?passive active = ;; +(* returns an estimation of how many equalities in passive can be activated + within the current time limit *) let get_selection_estimate () = elapsed_time := (Unix.gettimeofday ()) -. !start_time; -(* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *) + (* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *) int_of_float ( ceil ((float_of_int !processed_clauses) *. ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.))) ;; - + +(** initializes the set of goals *) +let make_goals goal = + let active = [] + and passive = [0, [goal]] in + active, passive +;; + + +(** initializes the set of theorems *) +let make_theorems theorems = + theorems, [] +;; + + +let activate_goal (active, passive) = + match passive with + | goal_conj::tl -> true, (goal_conj::active, tl) + | [] -> false, (active, passive) +;; + + +let activate_theorem (active, passive) = + match passive with + | theorem::tl -> true, (theorem::active, tl) + | [] -> false, (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 @@ -815,32 +774,43 @@ let simplify_goal env goal ?passive (active_list, active_table) = let newmeta, newgoal = Indexing.demodulation_goal !maxmeta env table goal in maxmeta := newmeta; - newgoal + goal != newgoal, newgoal in - let goal = + let changed, goal = match passive_table with | None -> demodulate active_table goal | Some passive_table -> - let goal = demodulate active_table goal in - demodulate passive_table goal + let changed, goal = demodulate active_table goal in + let changed', goal = demodulate passive_table goal in + (changed || changed'), goal in - let _ = - let p, _, t = goal in - debug_print - (lazy - (Printf.sprintf "Goal after demodulation: %s, %s" - (string_of_proof p) (CicPp.ppterm t))) - in - goal + changed, goal ;; let simplify_goals env goals ?passive active = - List.map - (fun (d, gl) -> - let gl = List.map (fun g -> simplify_goal env g ?passive active) gl in - d, gl) - goals + 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 ;; @@ -854,21 +824,32 @@ let simplify_theorems env theorems ?passive (active_list, active_table) = pn @ pp, Some pt in let all = if pl = [] then active_list else active_list @ pl in - + let a_theorems, p_theorems = theorems in let demodulate table theorem = let newmeta, newthm = Indexing.demodulation_theorem !maxmeta env table theorem in maxmeta := newmeta; - newthm + theorem != newthm, newthm + in + let foldfun table (a, p) theorem = + let changed, theorem = demodulate table theorem in + if changed then (a, theorem::p) else (theorem::a, p) in + let mapfun table theorem = snd (demodulate table theorem) in match passive_table with - | None -> List.map (demodulate active_table) theorems + | None -> + let p_theorems = List.map (mapfun active_table) p_theorems in + List.fold_left (foldfun active_table) ([], p_theorems) a_theorems | Some passive_table -> - let theorems = List.map (demodulate active_table) theorems in - List.map (demodulate passive_table) theorems + let p_theorems = List.map (mapfun active_table) p_theorems in + let p_theorems, a_theorems = + List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in + let p_theorems = List.map (mapfun passive_table) p_theorems in + List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems ;; +(* 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 @@ -878,6 +859,10 @@ let apply_equality_to_goal env equality goal = let eqterm = C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in let gproof, gmetas, gterm = goal in +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s" *) +(* (string_of_equality equality) (CicPp.ppterm gterm))); *) try let subst, metasenv', _ = let menv = metasenv @ metas @ gmetas in @@ -906,123 +891,49 @@ let apply_equality_to_goal env equality goal = ;; -(* -let apply_to_goal env theorems active (depth, goals) = - let _ = - debug_print ("apply_to_goal: " ^ (string_of_int (List.length goals))) - in - let metasenv, context, ugraph = env in - let goal = List.hd goals in - let proof, metas, term = goal in -(* debug_print *) -(* (Printf.sprintf "apply_to_goal with goal: %s" (CicPp.ppterm term)); *) - let newmeta = CicMkImplicit.new_meta metasenv [] in - let metasenv = (newmeta, context, term)::metasenv @ metas in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let status = - ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta) - in - let rec aux = function - | [] -> false, [] (* goals *) (* None *) - | (theorem, thmty, _)::tl -> - try - let subst_in, (newproof, newgoals) = - PrimitiveTactics.apply_tac_verbose ~term:theorem status - in - if newgoals = [] then - let _, _, p, _ = newproof 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, [[newp, metas, term]] (* Some newp *) - else if List.length newgoals = 1 then - let _, menv, p, _ = newproof in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let goals = - List.map - (fun i -> - let _, _, ty = CicUtil.lookup_meta i menv in - let proof = - Inference.SubProof - (p, i, Inference.BasicProof (Cic.Meta (i, irl))) - in (proof, menv, ty)) - newgoals - in - let res, others = aux tl in - if res then (true, others) else (false, goals::others) - else - aux tl - with ProofEngineTypes.Fail msg -> - (* debug_print ("FAIL!!:" ^ msg); *) - aux tl - in - let r, l = - if Inference.term_is_equality term then - let rec appleq = function - | [] -> false, [] - | (Positive, equality)::tl -> - let ok, _, newproof = apply_equality_to_goal env equality goal in - if ok then true, [(depth, [newproof, metas, term])] else appleq tl - | _::tl -> appleq tl - in - let al, _ = active in - appleq al - else - false, [] - in - if r = true then r, l else - let r, l = aux theorems in - if r = true then - r, List.map (fun l -> (depth+1, l)) l - else - r, (depth, goals)::(List.map (fun l -> (depth+1, l)) l) -;; -*) - -let new_meta () = - incr maxmeta; !maxmeta +let new_meta metasenv = + let m = CicMkImplicit.new_meta metasenv [] in + incr maxmeta; + while !maxmeta <= m do incr maxmeta done; + !maxmeta ;; -let apply_to_goal env theorems active goal = +(* applies a theorem or an equality to goal, returning a list of subgoals or + an indication of failure *) +let apply_to_goal env theorems ?passive active goal = let metasenv, context, ugraph = env in let proof, metas, term = goal in - debug_print - (lazy - (Printf.sprintf "apply_to_goal with goal: %s, %s" - (string_of_proof proof) (CicPp.ppterm term))); + (* debug_print *) + (* (lazy *) + (* (Printf.sprintf "apply_to_goal with goal: %s" *) + (* (\* (string_of_proof proof) *\)(CicPp.ppterm term))); *) let status = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let proof', newmeta = let rec get_meta = function - | SubProof (t, i, _) -> t, i + | SubProof (t, i, p) -> + let t', i' = get_meta p in + if i' = -1 then t, i else t', i' | ProofGoalBlock (_, p) -> get_meta p - | _ -> - let n = new_meta () in (* CicMkImplicit.new_meta metasenv [] in *) - Cic.Meta (n, irl), n + | _ -> Cic.Implicit None, -1 in - get_meta proof + let p, m = get_meta proof in + if m = -1 then + let n = new_meta (metasenv @ metas) in + Cic.Meta (n, irl), n + else + p, m in -(* let newmeta = CicMkImplicit.new_meta metasenv [] in *) let metasenv = (newmeta, context, term)::metasenv @ metas in - ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta) -(* ((None, metasenv, proof', term), newmeta) *) + let bit = new_meta metasenv, context, term in + let metasenv' = bit::metasenv in + ((None, metasenv', Cic.Meta (newmeta, irl), term), newmeta) in let rec aux = function - | [] -> `No (* , [], [] *) + | [] -> `No | (theorem, thmty, _)::tl -> try let subst, (newproof, newgoals) = @@ -1044,10 +955,6 @@ let apply_to_goal env theorems active goal = in let _, m = status in let subst = List.filter (fun (i, _) -> i = m) subst in -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "m = %d\nsubst = %s\n" *) -(* m (print_subst subst))); *) `Ok (subst, [newp, metas, term]) else let _, menv, p, _ = newproof in @@ -1063,9 +970,7 @@ let apply_to_goal env theorems active goal = | SubProof (t, i, p) -> SubProof (t, i, gp p) | ProofGoalBlock (sp1, sp2) -> -(* SubProof (p, i, sp) *) ProofGoalBlock (sp1, gp sp2) -(* gp sp *) | BasicProof _ | NoProof -> SubProof (p, i, BasicProof (Cic.Meta (i, irl))) @@ -1073,41 +978,49 @@ let apply_to_goal env theorems active goal = ProofSymBlock (s, gp sp) | ProofBlock (s, u, nt, t, pe, sp) -> ProofBlock (s, u, nt, t, pe, gp sp) -(* | _ -> assert false *) in gp proof in - debug_print - (lazy - (Printf.sprintf "new sub goal: %s, %s" - (string_of_proof p') (CicPp.ppterm ty))); (p', menv, ty)) newgoals in -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "\nGoOn with subst: %s" (print_subst subst))); *) + let goals = + let weight t = + let w, m = weight_of_term t in + w + 2 * (List.length m) + in + List.sort + (fun (_, _, t1) (_, _, t2) -> + Pervasives.compare (weight t1) (weight t2)) + goals + in let best = aux tl in match best with | `Ok (_, _) -> best | `No -> `GoOn ([subst, goals]) - | `GoOn sl(* , subst', goals' *) -> -(* if (List.length goals') < (List.length goals) then best *) -(* else `GoOn, subst, goals *) - `GoOn ((subst, goals)::sl) + | `GoOn sl -> `GoOn ((subst, goals)::sl) with ProofEngineTypes.Fail msg -> aux tl in let r, s, l = if Inference.term_is_equality term then - let rec appleq = function + let rec appleq_a = function | [] -> false, [], [] | (Positive, equality)::tl -> let ok, s, newproof = apply_equality_to_goal env equality goal in - if ok then true, s, [newproof, metas, term] else appleq tl - | _::tl -> appleq tl + if ok then true, s, [newproof, metas, term] else appleq_a tl + | _::tl -> appleq_a tl + in + let rec appleq_p = function + | [] -> false, [], [] + | equality::tl -> + let ok, s, newproof = apply_equality_to_goal env equality goal in + if ok then true, s, [newproof, metas, term] else appleq_p tl in let al, _ = active in - appleq al + match passive with + | None -> appleq_a al + | Some (_, (pl, _), _) -> + let r, s, l = appleq_a al in if r then r, s, l else appleq_p pl else false, [], [] in @@ -1115,117 +1028,147 @@ let apply_to_goal env theorems active goal = ;; -let apply_to_goal_conj env theorems active (depth, goals) = - let rec aux = function - | goal::tl -> - let propagate_subst subst (proof, metas, term) = - debug_print - (lazy - (Printf.sprintf "\npropagate_subst:\n%s\n%s, %s\n" - (print_subst subst) (string_of_proof proof) - (CicPp.ppterm term))); - let rec repl = function - | NoProof -> NoProof - | BasicProof t -> - BasicProof (CicMetaSubst.apply_subst subst t) - | ProofGoalBlock (p, pb) -> - debug_print (lazy "HERE"); - let pb' = repl pb in - ProofGoalBlock (p, pb') - | SubProof (t, i, p) -> - let t' = CicMetaSubst.apply_subst subst t in - debug_print - (lazy - (Printf.sprintf - "SubProof %d\nt = %s\nsubst = %s\nt' = %s\n" - i (CicPp.ppterm t) (print_subst subst) - (CicPp.ppterm t'))); - let p = repl p in - SubProof (t', i, p) - | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p) - | ProofBlock (s, u, nty, t, pe, p) -> - ProofBlock (subst @ s, u, nty, t, pe, p) - in (repl proof, metas, term) - in - let r = apply_to_goal env theorems active goal in ( - match r with - | `No -> `No (depth, goals) - | `GoOn sl (* (subst, gl) *) -> -(* let tl = List.map (propagate_subst subst) tl in *) - debug_print (lazy "GO ON!!!"); - let l = - List.map - (fun (s, gl) -> - (depth+1, gl @ (List.map (propagate_subst s) tl))) sl +(* sorts a conjunction of goals in order to detect earlier if it is + unsatisfiable. Non-predicate goals are placed at the end of the list *) +let sort_goal_conj (metasenv, context, ugraph) (depth, gl) = + let gl = + List.stable_sort + (fun (_, e1, g1) (_, e2, g2) -> + let ty1, _ = + CicTypeChecker.type_of_aux' (e1 @ metasenv) context g1 ugraph + and ty2, _ = + CicTypeChecker.type_of_aux' (e2 @ metasenv) context g2 ugraph + in + let prop1 = + let b, _ = + CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty1 ugraph + in + if b then 0 else 1 + and prop2 = + let b, _ = + CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty2 ugraph + in + if b then 0 else 1 + in + if prop1 = 0 && prop2 = 0 then + let e1 = if Inference.term_is_equality g1 then 0 else 1 + and e2 = if Inference.term_is_equality g2 then 0 else 1 in + e1 - e2 + else + prop1 - prop2) + gl + in + (depth, gl) +;; + + +let is_meta_closed goals = + List.for_all (fun (_, _, g) -> CicUtil.is_meta_closed g) goals +;; + + +(* applies a series of theorems/equalities to a conjunction of goals *) +let rec apply_to_goal_conj env theorems ?passive active (depth, goals) = + let aux (goal, r) tl = + let propagate_subst subst (proof, metas, term) = + let rec repl = function + | NoProof -> NoProof + | BasicProof t -> + BasicProof (CicMetaSubst.apply_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 p = repl p in + SubProof (t', i, p) + | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p) + | ProofBlock (s, u, nty, t, pe, p) -> + ProofBlock (subst @ s, u, nty, t, pe, p) + in (repl proof, metas, term) + in + (* let r = apply_to_goal env theorems ?passive active goal in *) ( + match r with + | `No -> `No (depth, goals) + | `GoOn sl -> + let l = + List.map + (fun (s, gl) -> + let tl = List.map (propagate_subst s) tl in + sort_goal_conj env (depth+1, gl @ tl)) sl + in + `GoOn l + | `Ok (subst, gl) -> + if tl = [] then + `Ok (depth, gl) + else + let p, _, _ = List.hd gl in + let subproof = + let rec repl = function + | SubProof (_, _, p) -> repl p + | ProofGoalBlock (p1, p2) -> + ProofGoalBlock (repl p1, repl p2) + | p -> p in - debug_print - (lazy - (Printf.sprintf "%s\n" - (String.concat "; " - (List.map - (fun (s, gl) -> - (Printf.sprintf "[%s]" - (String.concat "; " - (List.map - (fun (p, _, g) -> - (Printf.sprintf "<%s, %s>" - (string_of_proof p) - (CicPp.ppterm g))) gl)))) l)))); - `GoOn l (* (depth+1, gl @ tl) *) - | `Ok (subst, gl) -> - if tl = [] then -(* let _ = *) -(* let p, _, t = List.hd gl in *) -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "OK: %s, %s\n" *) -(* (string_of_proof p) (CicPp.ppterm t))) *) -(* in *) - `Ok (depth, gl) - else - let p, _, _ = List.hd gl in - let subproof = - let rec repl = function - | SubProof (_, _, p) -> repl p - | ProofGoalBlock (p1, p2) -> - ProofGoalBlock (repl p1, repl p2) - | p -> p - in - build_proof_term (repl p) - in - let i = - let rec get_meta = function - | SubProof (_, i, p) -> max i (get_meta p) - | ProofGoalBlock (_, p) -> get_meta p - | _ -> -1 (* assert false *) - in - get_meta p - in - let subst = - let _, (context, _, _) = List.hd subst in - [i, (context, subproof, Cic.Implicit None)] - in - let tl = List.map (propagate_subst subst) tl in - `GoOn ([depth+1, tl]) - ) - | _ -> assert false + build_proof_term (repl p) + in + let i = + let rec get_meta = function + | SubProof (_, i, p) -> + let i' = get_meta p in + if i' = -1 then i else i' +(* max i (get_meta p) *) + | ProofGoalBlock (_, p) -> get_meta p + | _ -> -1 + in + get_meta p + in + let subst = + let _, (context, _, _) = List.hd subst in + [i, (context, subproof, Cic.Implicit None)] + in + let tl = List.map (propagate_subst subst) tl in + let conj = sort_goal_conj env (depth(* +1 *), tl) in + `GoOn ([conj]) + ) in - debug_print - (lazy - (Printf.sprintf "apply_to_goal_conj (%d, [%s])" - depth - (String.concat "; " - (List.map (fun (_, _, t) -> CicPp.ppterm t) goals)))); - if depth > !maxdepth || (List.length goals) > !maxwidth then ( - debug_print - (lazy (Printf.sprintf "Pruning because depth = %d, width = %d" - depth (List.length goals))); + if depth > !maxdepth || (List.length goals) > !maxwidth then `No (depth, goals) - ) else - aux goals + else + let rec search_best res = function + | [] -> res + | goal::tl -> + let r = apply_to_goal env theorems ?passive active goal in + match r with + | `Ok _ -> (goal, r) + | `No -> search_best res tl + | `GoOn l -> + let newres = + match res with + | _, `Ok _ -> assert false + | _, `No -> goal, r + | _, `GoOn l2 -> + if (List.length l) < (List.length l2) then goal, r else res + in + search_best newres tl + in + let hd = List.hd goals in + let res = hd, (apply_to_goal env theorems ?passive active hd) in + let best = + match res with + | _, `Ok _ -> res + | _, _ -> search_best res (List.tl goals) + in + let res = aux best (List.filter (fun g -> g != (fst best)) goals) in + match res with + | `GoOn ([conj]) when is_meta_closed (snd conj) && + (List.length (snd conj)) < (List.length goals)-> + apply_to_goal_conj env theorems ?passive active conj + | _ -> res ;; +(* module OrderedGoals = struct type t = int * (Inference.proof * Cic.metasenv * Cic.term) list @@ -1248,26 +1191,16 @@ module OrderedGoals = struct ) else false) l1 l2 in !res -(* let res = Pervasives.compare g1 g2 in *) -(* let _ = *) -(* let print_goals (d, gl) = *) -(* let gl' = List.map (fun (_, _, t) -> CicPp.ppterm t) gl in *) -(* Printf.sprintf "%d, [%s]" d (String.concat "; " gl') *) -(* in *) -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "comparing g1:%s and g2:%s, res: %d\n" *) -(* (print_goals g1) (print_goals g2) res)) *) -(* in *) -(* res *) end module GoalsSet = Set.Make(OrderedGoals);; exception SearchSpaceOver;; +*) +(* let apply_to_goals env is_passive_empty theorems active goals = debug_print (lazy "\n\n\tapply_to_goals\n\n"); let add_to set goals = @@ -1294,38 +1227,11 @@ let apply_to_goals env is_passive_empty theorems active goals = in true, GoalsSet.singleton newgoals | `GoOn newgoals -> - let print_set set msg = - debug_print - (lazy - (Printf.sprintf "%s:\n%s" msg - (String.concat "\n" - (GoalsSet.fold - (fun (d, gl) l -> - let gl' = - List.map (fun (_, _, t) -> CicPp.ppterm t) gl - in - let s = - Printf.sprintf "%d, [%s]" d - (String.concat "; " gl') - in - s::l) set [])))) - in - let set = add_to set (goals::tl) in -(* print_set set "SET BEFORE"; *) - let n = GoalsSet.cardinal set in - let set = add_to set newgoals in -(* print_set set "SET AFTER"; *) - let m = GoalsSet.cardinal set in -(* if n < m then *) - false, set -(* else *) -(* let _ = print_set set "SET didn't change" in *) -(* aux set tl *) + let set' = add_to set (goals::tl) in + let set' = add_to set' newgoals in + false, set' | `No newgoals -> aux set tl -(* let set = add_to set (newgoals::goals::tl) in *) -(* let res, set = aux set tl in *) -(* res, set *) in let n = List.length goals in let res, goals = aux (add_to GoalsSet.empty goals) goals in @@ -1337,9 +1243,160 @@ let apply_to_goals env is_passive_empty theorems active goals = else res, goals ;; +*) + +(* sorts the list of passive goals to minimize the search for a proof (doesn't + work that well yet...) *) +let sort_passive_goals goals = + List.stable_sort + (fun (d1, l1) (d2, l2) -> + let r1 = d2 - d1 + and r2 = (List.length l1) - (List.length l2) in + let foldfun ht (_, _, t) = + let _ = List.map (fun i -> Hashtbl.replace ht i 1) (metas_of_term t) + in ht + in + let m1 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l1) + and m2 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l2) + in let r3 = m1 - m2 in + if r3 <> 0 then r3 + else if r2 <> 0 then r2 + else r1) + (* let _, _, g1 = List.hd l1 *) +(* and _, _, g2 = List.hd l2 in *) +(* let e1 = if Inference.term_is_equality g1 then 0 else 1 *) +(* and e2 = if Inference.term_is_equality g2 then 0 else 1 *) +(* in let r4 = e1 - e2 in *) +(* if r4 <> 0 then r3 else r1) *) + goals +;; + + +let print_goals goals = + (String.concat "\n" + (List.map + (fun (d, gl) -> + let gl' = + List.map + (fun (p, _, t) -> + (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl + in + Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals)) +;; + + +(* tries to prove the first conjunction in goals with applications of + theorems/equalities, returning new sub-goals or an indication of success *) +let apply_goal_to_theorems dbd env theorems ?passive active goals = + let theorems, _ = theorems in + let a_goals, p_goals = goals in + let goal = List.hd a_goals in + let not_in_active gl = + not + (List.exists + (fun (_, gl') -> + if (List.length gl) = (List.length gl') then + List.for_all2 (fun (_, _, g1) (_, _, g2) -> g1 = g2) gl gl' + else + false) + a_goals) + in + let aux theorems = + let res = apply_to_goal_conj env theorems ?passive active goal in + match res with + | `Ok newgoals -> + true, ([newgoals], []) + | `No _ -> + false, (a_goals, p_goals) + | `GoOn newgoals -> + let newgoals = + List.filter + (fun (d, gl) -> + (d <= !maxdepth) && (List.length gl) <= !maxwidth && + not_in_active gl) + newgoals in + let p_goals = newgoals @ p_goals in + let p_goals = sort_passive_goals p_goals in + false, (a_goals, p_goals) + in + aux theorems +;; + + +let apply_theorem_to_goals env theorems active goals = + let a_goals, p_goals = goals in + let theorem = List.hd (fst theorems) in + let theorems = [theorem] in + let rec aux p = function + | [] -> false, ([], p) + | goal::tl -> + let res = apply_to_goal_conj env theorems active goal in + match res with + | `Ok newgoals -> true, ([newgoals], []) + | `No _ -> aux p tl + | `GoOn newgoals -> aux (newgoals @ p) tl + in + let ok, (a, p) = aux p_goals a_goals in + if ok then + ok, (a, p) + else + let p_goals = + List.stable_sort + (fun (d1, l1) (d2, l2) -> + let r = d2 - d1 in + if r <> 0 then r + else let r = (List.length l1) - (List.length l2) in + if r <> 0 then r + else + let res = ref 0 in + let _ = + List.exists2 + (fun (_, _, t1) (_, _, t2) -> + let r = Pervasives.compare t1 t2 in + if r <> 0 then (res := r; true) else false) l1 l2 + in !res) + p + in + ok, (a_goals, p_goals) +;; + + +(* given-clause algorithm with lazy reduction strategy *) +let rec given_clause dbd env goals theorems passive active = + let goals = simplify_goals env goals active in + let ok, goals = activate_goal goals in + (* let theorems = simplify_theorems env theorems active in *) + if ok then + let ok, goals = apply_goal_to_theorems dbd env theorems active goals in + if ok then + let proof = + match (fst goals) with + | (_, [proof, _, _])::_ -> Some proof + | _ -> assert false + in + ParamodulationSuccess (proof, env) + else + given_clause_aux dbd env goals theorems passive active + else +(* let ok', theorems = activate_theorem theorems in *) + let ok', theorems = false, theorems in + if ok' then + let ok, goals = apply_theorem_to_goals env theorems active goals in + if ok then + let proof = + match (fst goals) with + | (_, [proof, _, _])::_ -> Some proof + | _ -> assert false + in + ParamodulationSuccess (proof, env) + else + given_clause_aux dbd env goals theorems passive active + else + if (passive_is_empty passive) then ParamodulationFailure + else given_clause_aux dbd env goals theorems passive active -let rec given_clause env goals theorems passive active = +and given_clause_aux dbd env goals theorems passive active = let time1 = Unix.gettimeofday () in let selection_estimate = get_selection_estimate () in @@ -1365,153 +1422,150 @@ let rec given_clause env goals theorems passive active = passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1); kept_clauses := (size_of_passive passive) + (size_of_active active); - -(* let refl_equal = *) -(* CicUtil.term_of_uri *) -(* (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *) -(* in *) - let goals = simplify_goals env goals active in - let theorems = simplify_theorems env theorems active in - let is_passive_empty = passive_is_empty passive in - try - let ok, goals = apply_to_goals env is_passive_empty theorems active goals in - if ok then - let proof = - match goals with - | (_, [proof, _, _])::_ -> Some proof - | _ -> assert false - in - ParamodulationSuccess (proof, env) - else - match is_passive_empty (* passive_is_empty passive *) with - | true -> (* ParamodulationFailure *) - given_clause env goals theorems passive active - | false -> - let (sign, current), passive = select env goals passive active in - 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 -> - given_clause env goals theorems passive active - | Some (sign, current) -> - 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 - ParamodulationSuccess (Some proof (* current *), env) - ) else ( - debug_print - (lazy "\n================================================"); - debug_print (lazy (Printf.sprintf "selected: %s %s" - (string_of_sign sign) - (string_of_equality ~env current))); - - let t1 = Unix.gettimeofday () in - let new' = infer env sign current active in - let t2 = Unix.gettimeofday () in - infer_time := !infer_time +. (t2 -. t1); - - let res, goal' = contains_empty env new' in - if res then - let proof = - match goal' with - | Some goal -> let _, proof, _, _, _ = goal in Some proof - | None -> None - in - ParamodulationSuccess (proof (* goal *), env) - else - let t1 = Unix.gettimeofday () in - let new' = forward_simplify_new env new' active in - let t2 = Unix.gettimeofday () in - let _ = - forward_simpl_new_time := - !forward_simpl_new_time +. (t2 -. t1) - in + match passive_is_empty passive with + | true -> (* ParamodulationFailure *) + given_clause dbd env goals theorems passive active + | false -> + let (sign, current), passive = select env (fst goals) passive active in + 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 -> + given_clause dbd env goals theorems passive active + | Some (sign, current) -> + 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 + ParamodulationSuccess (Some proof, env) + ) else ( + debug_print + (lazy "\n================================================"); + debug_print (lazy (Printf.sprintf "selected: %s %s" + (string_of_sign sign) + (string_of_equality ~env current))); + + let t1 = Unix.gettimeofday () in + let new' = infer env sign current active in + let t2 = Unix.gettimeofday () in + infer_time := !infer_time +. (t2 -. t1); + + let res, goal' = contains_empty env new' in + if res then + let proof = + match goal' with + | Some goal -> let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof, env) + else + let t1 = Unix.gettimeofday () in + let new' = forward_simplify_new env new' active in + let t2 = Unix.gettimeofday () in + let _ = + forward_simpl_new_time := + !forward_simpl_new_time +. (t2 -. t1) + in + let active = + match sign with + | Negative -> active + | Positive -> + let t1 = Unix.gettimeofday () in + let active, _, newa, _ = + backward_simplify env ([], [current]) active + in + let t2 = Unix.gettimeofday () in + backward_simpl_time := + !backward_simpl_time +. (t2 -. t1); + match newa with + | None -> active + | Some (n, p) -> + let al, tbl = active in + let nn = List.map (fun e -> Negative, e) n in + let pp, tbl = + List.fold_right + (fun e (l, t) -> + (Positive, e)::l, + Indexing.index tbl e) + p ([], tbl) + in + nn @ al @ pp, tbl + in + match contains_empty env new' with + | false, _ -> let active = + let al, tbl = active in match sign with - | Negative -> active + | Negative -> (sign, current)::al, tbl | Positive -> - let t1 = Unix.gettimeofday () in - let active, _, newa, _ = - backward_simplify env ([], [current]) active - in - let t2 = Unix.gettimeofday () in - backward_simpl_time := - !backward_simpl_time +. (t2 -. t1); - match newa with - | None -> active - | Some (n, p) -> - let al, tbl = active in - let nn = List.map (fun e -> Negative, e) n in - let pp, tbl = - List.fold_right - (fun e (l, t) -> - (Positive, e)::l, - Indexing.index tbl e) - p ([], tbl) - in - nn @ al @ pp, tbl + al @ [(sign, current)], Indexing.index tbl current in -(* let _ = *) -(* Printf.printf "active:\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map *) -(* (fun (s, e) -> (string_of_sign s) ^ " " ^ *) -(* (string_of_equality ~env e)) (fst active)))); *) -(* print_newline (); *) -(* in *) -(* let _ = *) -(* match new' with *) -(* | neg, pos -> *) -(* Printf.printf "new':\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map *) -(* (fun e -> "Negative " ^ *) -(* (string_of_equality ~env e)) neg) @ *) -(* (List.map *) -(* (fun e -> "Positive " ^ *) -(* (string_of_equality ~env e)) pos))); *) -(* print_newline (); *) -(* in *) - match contains_empty env new' with - | false, _ -> - let active = - let al, tbl = active in - match sign with - | Negative -> (sign, current)::al, tbl - | Positive -> - al @ [(sign, current)], Indexing.index tbl current - in - let passive = add_to_passive passive new' in - let (_, ns), (_, ps), _ = passive in -(* Printf.printf "passive:\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map (fun e -> "Negative " ^ *) -(* (string_of_equality ~env e)) *) -(* (EqualitySet.elements ns)) @ *) -(* (List.map (fun e -> "Positive " ^ *) -(* (string_of_equality ~env e)) *) -(* (EqualitySet.elements ps)))); *) -(* print_newline (); *) - given_clause env goals theorems passive active - | true, goal -> - let proof = - match goal with - | Some goal -> - let _, proof, _, _, _ = goal in Some proof - | None -> None - in - ParamodulationSuccess (proof (* goal *), env) - ) - with SearchSpaceOver -> - ParamodulationFailure + let passive = add_to_passive passive new' in + let (_, ns), (_, ps), _ = passive in + given_clause dbd env goals theorems passive active + | true, goal -> + let proof = + match goal with + | Some goal -> + let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof, env) + ) ;; -let rec given_clause_fullred env goals theorems passive active = +(** given-clause algorithm with full reduction strategy *) +let rec given_clause_fullred dbd env goals theorems passive active = + let goals = simplify_goals env goals ~passive active in + let ok, goals = activate_goal goals in +(* let theorems = simplify_theorems env theorems ~passive active in *) + if ok then +(* let _ = *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" *) +(* (print_goals (fst goals)) (print_goals (snd goals)))); *) +(* let current = List.hd (fst goals) in *) +(* let p, _, t = List.hd (snd current) in *) +(* debug_print *) +(* (lazy *) +(* (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 + if ok then + let proof = + match (fst goals) with + | (_, [proof, _, _])::_ -> Some proof + | _ -> assert false + in + ParamodulationSuccess (proof, env) + else + given_clause_fullred_aux dbd env goals theorems passive active + else +(* let ok', theorems = activate_theorem theorems in *) +(* if ok' then *) +(* let ok, goals = apply_theorem_to_goals env theorems active goals in *) +(* if ok then *) +(* let proof = *) +(* match (fst goals) with *) +(* | (_, [proof, _, _])::_ -> Some proof *) +(* | _ -> assert false *) +(* in *) +(* ParamodulationSuccess (proof, env) *) +(* else *) +(* given_clause_fullred_aux env goals theorems passive active *) +(* else *) + if (passive_is_empty passive) then ParamodulationFailure + else given_clause_fullred_aux dbd env goals theorems passive active + +and given_clause_fullred_aux dbd env goals theorems passive active = let time1 = Unix.gettimeofday () in let selection_estimate = get_selection_estimate () in @@ -1535,163 +1589,116 @@ let rec given_clause_fullred env goals theorems passive active = let time2 = Unix.gettimeofday () in passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1); - + kept_clauses := (size_of_passive passive) + (size_of_active active); + match passive_is_empty passive with + | true -> (* ParamodulationFailure *) + given_clause_fullred dbd env goals theorems passive active + | false -> + let (sign, current), passive = select env (fst goals) passive active in + 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 -> + given_clause_fullred dbd env goals theorems passive active + | Some (sign, current) -> + 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 + ParamodulationSuccess (Some proof, env) + ) else ( + debug_print + (lazy "\n================================================"); + debug_print (lazy (Printf.sprintf "selected: %s %s" + (string_of_sign sign) + (string_of_equality ~env current))); + + let t1 = Unix.gettimeofday () in + let new' = infer env sign current active in + let t2 = Unix.gettimeofday () in + infer_time := !infer_time +. (t2 -. t1); + + let active = + if is_identity env current then active + else + let al, tbl = active in + match sign with + | Negative -> (sign, current)::al, tbl + | Positive -> + al @ [(sign, current)], Indexing.index tbl current + in + let rec simplify new' active passive = + let t1 = Unix.gettimeofday () 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 + let t2 = Unix.gettimeofday () in + backward_simpl_time := !backward_simpl_time +. (t2 -. t1); + match newa, retained with + | None, None -> active, passive, new' + | Some (n, p), None + | None, Some (n, p) -> + let nn, np = new' in + 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 refl_equal = *) -(* CicUtil.term_of_uri *) -(* (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *) -(* in *) - let goals = simplify_goals env goals ~passive active in - let theorems = simplify_theorems env theorems ~passive active in - let is_passive_empty = passive_is_empty passive in - try - let ok, goals = apply_to_goals env is_passive_empty theorems active goals in - if ok then - let proof = - match goals with - | (_, [proof, _, _])::_ -> Some proof - | _ -> assert false - in - ParamodulationSuccess (proof, env) - else - let _ = - debug_print - (lazy ("new_goals: " ^ (string_of_int (List.length goals)))); - debug_print - (lazy - (String.concat "\n" - (List.map - (fun (d, gl) -> - let gl' = - List.map - (fun (p, _, t) -> - (string_of_proof p) ^ ", " ^ (CicPp.ppterm t)) gl - in - Printf.sprintf "%d: %s" d (String.concat "; " gl')) - goals))); - in - match is_passive_empty (* passive_is_empty passive *) with - | true -> (* ParamodulationFailure *) - given_clause_fullred env goals theorems passive active - | false -> - let (sign, current), passive = select env goals passive active in - 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 -> - given_clause_fullred env goals theorems passive active - | Some (sign, current) -> - 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 - ParamodulationSuccess (Some proof (* current *), env) - ) else ( - debug_print - (lazy "\n================================================"); - debug_print (lazy (Printf.sprintf "selected: %s %s" - (string_of_sign sign) - (string_of_equality ~env current))); - - let t1 = Unix.gettimeofday () in - let new' = infer env sign current active in - let t2 = Unix.gettimeofday () in - infer_time := !infer_time +. (t2 -. t1); - - let active = - if is_identity env current then active - else - let al, tbl = active in - match sign with - | Negative -> (sign, current)::al, tbl - | Positive -> - al @ [(sign, current)], Indexing.index tbl current - in - let rec simplify new' active passive = - let t1 = Unix.gettimeofday () 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 - let t2 = Unix.gettimeofday () in - backward_simpl_time := !backward_simpl_time +. (t2 -. t1); - match newa, retained with - | None, None -> active, passive, new' - | Some (n, p), None - | None, Some (n, p) -> - let nn, np = new' in - 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 k = size_of_passive passive in - if k < (kept - 1) then - processed_clauses := !processed_clauses + (kept - 1 - k); - - let _ = + let k = size_of_passive passive in + if k < (kept - 1) then + processed_clauses := !processed_clauses + (kept - 1 - k); + + let _ = + debug_print + (lazy + (Printf.sprintf "active:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) + (fst active)))))) + in + let _ = + match new' with + | neg, pos -> debug_print (lazy - (Printf.sprintf "active:\n%s\n" + (Printf.sprintf "new':\n%s\n" (String.concat "\n" ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) - (fst active)))))) - in - let _ = - match new' with - | neg, pos -> - debug_print - (lazy - (Printf.sprintf "new':\n%s\n" - (String.concat "\n" - ((List.map - (fun e -> "Negative " ^ - (string_of_equality ~env e)) neg) @ - (List.map - (fun e -> "Positive " ^ - (string_of_equality ~env e)) pos))))) + (fun e -> "Negative " ^ + (string_of_equality ~env e)) neg) @ + (List.map + (fun e -> "Positive " ^ + (string_of_equality ~env e)) pos))))) + in + match contains_empty env new' with + | false, _ -> + let passive = add_to_passive passive new' in + given_clause_fullred dbd env goals theorems passive active + | true, goal -> + let proof = + match goal with + | Some goal -> let _, proof, _, _, _ = goal in Some proof + | None -> None in - match contains_empty env new' with - | false, _ -> - let passive = add_to_passive passive new' in -(* let (_, ns), (_, ps), _ = passive in *) -(* Printf.printf "passive:\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map (fun e -> "Negative " ^ *) -(* (string_of_equality ~env e)) *) -(* (EqualitySet.elements ns)) @ *) -(* (List.map (fun e -> "Positive " ^ *) -(* (string_of_equality ~env e)) *) -(* (EqualitySet.elements ps)))); *) -(* print_newline (); *) - given_clause_fullred env goals theorems passive active - | true, goal -> - let proof = - match goal with - | Some goal -> let _, proof, _, _, _ = goal in Some proof - | None -> None - in - ParamodulationSuccess (proof (* goal *), env) - ) - with SearchSpaceOver -> - ParamodulationFailure + ParamodulationSuccess (proof, env) + ) ;; -(* let given_clause_ref = ref given_clause;; *) -let main dbd term metasenv ugraph = +let main dbd full term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in let module PET = ProofEngineTypes in @@ -1706,21 +1713,38 @@ let main dbd term metasenv ugraph = let lib_eq_uris, library_equalities, maxm = find_library_equalities dbd context (proof, goal') (maxm+2) in + let library_equalities = List.map snd library_equalities in maxmeta := maxm+2; (* TODO ugly!! *) let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let new_meta_goal, metasenv, type_of_goal = let _, context, ty = CicUtil.lookup_meta goal' metasenv in - Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty); - print_newline (); + debug_print + (lazy + (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n\n" (CicPp.ppterm ty))); Cic.Meta (maxm+1, irl), (maxm+1, context, ty)::metasenv, ty in -(* let new_meta_goal = Cic.Meta (goal', irl) in *) let env = (metasenv, context, ugraph) in - let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in - let context_hyp = find_context_hypotheses env eq_indexes in - let theorems = context_hyp @ theorems in + let t1 = Unix.gettimeofday () in + let theorems = + if full then + let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in + let context_hyp = find_context_hypotheses env eq_indexes in + context_hyp @ theorems, [] + else + let refl_equal = + let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + UriManager.uri_of_string (us ^ "#xpointer(1/1/1)") + in + let t = CicUtil.term_of_uri refl_equal in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + [(t, ty, [])], [] + in + let t2 = Unix.gettimeofday () in + debug_print + (lazy + (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); let _ = debug_print (lazy @@ -1731,94 +1755,78 @@ let main dbd term metasenv ugraph = (fun (t, ty, _) -> Printf.sprintf "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) - theorems)))) + (fst theorems))))) in try let goal = Inference.BasicProof new_meta_goal, [], goal in -(* let term_equality = equality_of_term new_meta_goal goal in *) -(* let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *) -(* if is_identity env term_equality then *) -(* let proof = *) -(* Cic.Appl [Cic.MutConstruct (\* reflexivity *\) *) -(* (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); *) -(* eq_ty; left] *) -(* in *) -(* let _ = *) -(* Printf.printf "OK, found a proof!\n"; *) -(* let names = names_of_context context in *) -(* print_endline (PP.pp proof names) *) -(* in *) -(* () *) -(* else *) - let equalities = - let equalities = equalities @ library_equalities in - debug_print - (lazy - (Printf.sprintf "equalities:\n%s\n" - (String.concat "\n" - (List.map string_of_equality equalities)))); - debug_print (lazy "SIMPLYFYING EQUALITIES..."); - let rec simpl e others others_simpl = - let active = others @ others_simpl in - let tbl = - List.fold_left - (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active - in - let res = forward_simplify env e (active, tbl) in - match others with - | hd::tl -> ( - match res with - | None -> simpl hd tl others_simpl - | Some e -> simpl hd tl (e::others_simpl) - ) - | [] -> ( - match res with - | None -> others_simpl - | Some e -> e::others_simpl - ) + let equalities = + let equalities = equalities @ library_equalities in + debug_print + (lazy + (Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities)))); + debug_print (lazy "SIMPLYFYING EQUALITIES..."); + let rec simpl e others others_simpl = + let active = others @ others_simpl in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + (Indexing.empty_table ()) active in - match equalities with - | [] -> [] - | hd::tl -> - let others = List.map (fun e -> (Positive, e)) tl in - let res = - List.rev (List.map snd (simpl (Positive, hd) others [])) - in - debug_print - (lazy - (Printf.sprintf "equalities AFTER:\n%s\n" - (String.concat "\n" - (List.map string_of_equality res)))); - res + let res = forward_simplify env e (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl (e::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> e::others_simpl + ) in - let active = make_active () in - let passive = make_passive [] (* [term_equality] *) equalities in - Printf.printf "\ncurrent goal: %s\n" - (let _, _, g = goal in CicPp.ppterm g); -(* (string_of_equality ~env term_equality); *) - Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); - Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); - Printf.printf "\nequalities:\n%s\n" - (String.concat "\n" - (List.map - (string_of_equality ~env) - (equalities @ library_equalities))); + match equalities with + | [] -> [] + | hd::tl -> + let others = List.map (fun e -> (Positive, e)) tl in + let res = + List.rev (List.map snd (simpl (Positive, hd) others [])) + in + debug_print + (lazy + (Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res)))); + res + in + let active = make_active () in + let passive = make_passive [] equalities in + Printf.printf "\ncurrent goal: %s\n" + (let _, _, g = goal in CicPp.ppterm g); + Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); + Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); + Printf.printf "\nequalities:\n%s\n" + (String.concat "\n" + (List.map + (string_of_equality ~env) equalities)); +(* (equalities @ library_equalities))); *) print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in print_endline "GO!"; start_time := Unix.gettimeofday (); let res = + let goals = make_goals goal in (if !use_fullred then given_clause_fullred else given_clause) - env [0, [goal]] theorems passive active + dbd env goals theorems passive active in let finish = Unix.gettimeofday () in let _ = match res with | ParamodulationFailure -> Printf.printf "NO proof found! :-(\n\n" - | ParamodulationSuccess (Some proof (* goal *), env) -> -(* let proof = Inference.build_proof_term goal in *) + | ParamodulationSuccess (Some proof, env) -> let proof = Inference.build_proof_term proof in Printf.printf "OK, found a proof!\n"; (* REMEMBER: we have to instantiate meta_proof, we should use @@ -1831,24 +1839,10 @@ let main dbd term metasenv ugraph = (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities in let _ = - Printf.printf "OK, found a proof!\n"; - (* REMEMBER: we have to instantiate meta_proof, we should use - apply the "apply" tactic to proof and status - *) - let names = names_of_context context in - print_endline (PP.pp proof names); try let ty, ug = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in -(* Printf.printf "OK, found a proof!\n"; *) -(* (\* REMEMBER: we have to instantiate meta_proof, we should use *) -(* apply the "apply" tactic to proof and status *) -(* *\) *) -(* let names = names_of_context context in *) -(* print_endline (PP.pp proof names); *) - (* print_endline (PP.ppterm proof); *) - print_endline (string_of_float (finish -. start)); Printf.printf "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" @@ -1892,10 +1886,28 @@ let main dbd term metasenv ugraph = let default_depth = !maxdepth and default_width = !maxwidth;; +let reset_refs () = + maxmeta := 0; + symbols_counter := 0; + weight_age_counter := !weight_age_ratio; + processed_clauses := 0; + start_time := 0.; + elapsed_time := 0.; + maximal_retained_equality := None; + infer_time := 0.; + forward_simpl_time := 0.; + forward_simpl_new_time := 0.; + backward_simpl_time := 0.; + passive_maintainance_time := 0.; + derived_clauses := 0; + kept_clauses := 0; +;; + let saturate dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in - maxmeta := 0; + reset_refs (); + Indexing.init_index (); maxdepth := depth; maxwidth := width; let proof, goal = status in @@ -1916,10 +1928,13 @@ let saturate let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in let goal = Inference.BasicProof new_meta_goal, [], goal in - let res, time = + let res, time = + let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = find_library_equalities dbd context (proof, goal') (maxm+2) in + let library_equalities = List.map snd library_equalities in + let t2 = Unix.gettimeofday () in maxmeta := maxm+2; let equalities = let equalities = equalities @ library_equalities in @@ -1963,11 +1978,15 @@ let saturate (List.map string_of_equality res)))); res in + debug_print + (lazy + (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))); + let t1 = Unix.gettimeofday () in let theorems = if full then let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in let context_hyp = find_context_hypotheses env eq_indexes in - context_hyp @ thms + context_hyp @ thms, [] else let refl_equal = let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in @@ -1975,8 +1994,9 @@ let saturate in let t = CicUtil.term_of_uri refl_equal in let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - [(t, ty, [])] + [(t, ty, [])], [] in + let t2 = Unix.gettimeofday () in let _ = debug_print (lazy @@ -1988,19 +2008,24 @@ let saturate Printf.sprintf "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) - theorems)))) + (fst theorems))))); + debug_print + (lazy + (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); in let active = make_active () in - let passive = make_passive [(* term_equality *)] equalities in + let passive = make_passive [] equalities in let start = Unix.gettimeofday () in - let res = given_clause_fullred env [0, [goal]] theorems passive active in + let res = + let goals = make_goals goal in + given_clause_fullred dbd env goals theorems passive active + in let finish = Unix.gettimeofday () in (res, finish -. start) in match res with - | ParamodulationSuccess (Some proof (* goal *), env) -> + | ParamodulationSuccess (Some proof, env) -> debug_print (lazy "OK, found a proof!"); -(* let proof = Inference.build_proof_term goal in *) let proof = Inference.build_proof_term proof in let names = names_of_context context in let newmetasenv = @@ -2048,12 +2073,12 @@ let saturate debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!"); debug_print (lazy (CicPp.pp proof names)); raise (ProofEngineTypes.Fail - "Found a proof, but it doesn't typecheck") + (lazy "Found a proof, but it doesn't typecheck")) in debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time)); newstatus | _ -> - raise (ProofEngineTypes.Fail "NO proof found") + raise (ProofEngineTypes.Fail (lazy "NO proof found")) ;; (* dummy function called within matita to trigger linkage *) @@ -2066,3 +2091,95 @@ if connect_to_auto then ( AutoTactic.term_is_equality := Inference.term_is_equality; );; + +let retrieve_and_print dbd term metasenv ugraph = + let module C = Cic in + let module T = CicTypeChecker in + let module PET = ProofEngineTypes in + let module PP = CicPp in + let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in + let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in + let proof, goals = status in + let goal' = List.nth goals 0 in + let uri, metasenv, meta_proof, term_to_prove = proof in + let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let eq_indexes, equalities, maxm = find_equalities context proof in + let new_meta_goal, metasenv, type_of_goal = + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let _, context, ty = CicUtil.lookup_meta goal' metasenv in + debug_print + (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty))); + Cic.Meta (maxm+1, irl), + (maxm+1, context, ty)::metasenv, + ty + in + let ugraph = CicUniv.empty_ugraph in + let env = (metasenv, context, ugraph) in + let goal = Inference.BasicProof new_meta_goal, [], goal in + let t1 = Unix.gettimeofday () in + let lib_eq_uris, library_equalities, maxm = + find_library_equalities dbd context (proof, goal') (maxm+2) + in + let t2 = Unix.gettimeofday () in + maxmeta := maxm+2; + let equalities = + let equalities = (* equalities @ *) library_equalities in + debug_print + (lazy + (Printf.sprintf "\n\nequalities:\n%s\n" + (String.concat "\n" + (List.map + (fun (u, e) -> +(* Printf.sprintf "%s: %s" *) + (UriManager.string_of_uri u) +(* (string_of_equality e) *) + ) + equalities)))); + debug_print (lazy "SIMPLYFYING EQUALITIES..."); + let rec simpl e others others_simpl = + let (u, e) = e in + let active = List.map (fun (u, e) -> (Positive, e)) + (others @ others_simpl) in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + (Indexing.empty_table ()) active + in + 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 -> others_simpl + | Some e -> (u, (snd e))::others_simpl + ) + in + 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 + debug_print + (lazy + (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) +;;