X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=6b1b65e276eef42a34c2426490a62da745cbace4;hb=1a65db059b643422fc8eded4f4e03b512071515b;hp=bf9f8ba57dde43b7bcbbdf6b9fa0cb73a2940fc6;hpb=102b6ad309695168ae95c2d4a9c3daa96599de21;p=helm.git diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index bf9f8ba57..6b1b65e27 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -28,27 +28,6 @@ open Inference;; open Utils;; - -(* -for debugging -let check_equation env equation msg = - let w, proof, (eq_ty, left, right, order), metas = 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;; @@ -70,7 +49,7 @@ let maximal_retained_equality = ref None;; (* equality-selection related globals *) let use_fullred = ref true;; -let weight_age_ratio = ref 4 (* 5 *);; (* settable by the user *) +let weight_age_ratio = ref 6 (* 5 *);; (* settable by the user *) let weight_age_counter = ref !weight_age_ratio ;; let symbols_ratio = ref 0 (* 3 *);; let symbols_counter = ref 0;; @@ -91,17 +70,20 @@ let maxmeta = ref 0;; let maxdepth = ref 3;; let maxwidth = ref 3;; - +type new_proof = + Equality.goal_proof * Equality.new_proof * Equality.substitution * Cic.metasenv +type old_proof = Equality.old_proof * Cic.metasenv type result = | ParamodulationFailure - | ParamodulationSuccess of Inference.proof option * environment + | ParamodulationSuccess of (new_proof * old_proof) option ;; -type goal = proof * Cic.metasenv * Cic.term;; +type goal = (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Cic.term;; type theorem = Cic.term * Cic.term * Cic.metasenv;; -let symbols_of_equality (_, _, (_, left, right, _), _) = +let symbols_of_equality equality = + let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in let m1 = symbols_of_term left in let m = TermMap.fold @@ -118,135 +100,66 @@ let symbols_of_equality (_, _, (_, left, right, _), _) = (* griggio *) module OrderedEquality = struct - type t = Inference.equality + type t = Equality.equality let compare eq1 eq2 = - match meta_convertibility_eq eq1 eq2 with + match Equality.meta_convertibility_eq eq1 eq2 with | true -> 0 | false -> - let w1, _, (ty, left, right, _), m1 = eq1 - and w2, _, (ty', left', right', _), m2 = eq2 in + let w1, _, (ty,left, right, _), m1,_ = Equality.open_equality eq1 in + let w2, _, (ty',left', right', _), m2,_ = Equality.open_equality 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 + let res = (List.length m1) - (List.length m2) in + if res <> 0 then res else + Equality.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 -> - (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);; exception Empty_list;; let passive_is_empty = function - | ([], _), ([], _), _ -> true + | ([], _), _ -> true | _ -> false ;; -let size_of_passive ((_, ns), (_, ps), _) = - (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps) +let size_of_passive ((passive_list, ps), _) = List.length passive_list +(* EqualitySet.cardinal ps *) ;; -let size_of_active (active_list, _) = - List.length active_list +let size_of_active (active_list, _) = List.length active_list ;; let age_factor = 0.01;; -let min_elt weight l = - fst - (match l with - [] -> raise Empty_list - | a::tl -> - let wa = float_of_int (weight a) in - let x = ref 0. in - List.fold_left - (fun (current,w) arg -> - x:=!x +. 1.; - let w1 = weight arg in - let wa = (float_of_int w1) +. !x *. age_factor in - if wa < w then (arg,wa) else (current,w)) - (a,wa) tl) -;; - -(* -let compare eq1 eq2 = - let w1, _, (ty, left, right, _), m1, _ = eq1 in - let w2, _, (ty', left', right', _), m2, _ = eq2 in - match Pervasives.compare w1 w2 with - | 0 -> (List.length m1) - (List.length m2) - | res -> res -;; -*) - (** selects one equality from passive. The selection strategy is a combination of weight, age and goal-similarity *) -let rec select env goals passive (active, _) = + +let rec select env goals passive = 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 - in + let (pos_list, pos_set), passive_table = passive in + let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in if !weight_age_ratio > 0 then weight_age_counter := !weight_age_counter - 1; match !weight_age_counter with | 0 -> ( weight_age_counter := !weight_age_ratio; - match neg_list, pos_list with - | hd::tl, pos -> - (* Negatives aren't indexed, no need to remove them... *) - (Negative, hd), - ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table) - | [], (hd:EqualitySet.elt)::tl -> - let w,_,_,_ = hd in + match pos_list with + | (hd:EqualitySet.elt)::tl -> let passive_table = - Indexing.remove_index passive_table hd - in (Positive, hd), - (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table) - | _, _ -> assert false - ) - | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> + Indexing.remove_index passive_table hd + in hd, ((tl, EqualitySet.remove hd pos_set), passive_table) + | _ -> assert false) + | _ when (!symbols_counter > 0) -> (symbols_counter := !symbols_counter - 1; let cardinality map = TermMap.fold (fun k v res -> res + v) map 0 @@ -284,43 +197,29 @@ let rec select env goals passive (active, _) = 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) - ) + current, + ((remove current pos_list, EqualitySet.remove current pos_set), + passive_table)) | _ -> symbols_counter := !symbols_ratio; - let set_selection set = EqualitySet.min_elt set 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 = - (neg_list, neg_set), - (remove current pos_list, EqualitySet.remove current pos_set), - Indexing.remove_index passive_table current - in - (Positive, current), passive - else - let current = set_selection neg_set in - let passive = - (remove current neg_list, EqualitySet.remove current neg_set), - (pos_list, pos_set), - passive_table - in - (Negative, current), passive + let current = EqualitySet.min_elt pos_set in + let passive_table = + Indexing.remove_index passive_table current + in + current, + ((remove current pos_list, EqualitySet.remove current pos_set), + passive_table) ;; (* initializes the passive set of equalities *) -let make_passive neg pos = +let make_passive pos = let set_of equalities = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities in let table = List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos in - (neg, set_of neg), (pos, set_of pos), table ;; @@ -331,29 +230,26 @@ 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 +(* adds to passive a list of equalities new_pos *) +let add_to_passive passive new_pos = + let (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 + let pos = List.filter (ok pos_set) new_pos in + 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 in - (neg @ neg_list, add neg_set neg), (pos_list @ pos, add pos_set pos), table ;; - +(* TODO *) (* 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 (pl, ps), tbl = passive in let howmany = float_of_int howmany and ratio = float_of_int !weight_age_ratio in let round v = @@ -364,67 +260,24 @@ let prune_passive howmany (active, _) passive = and in_age = round (howmany /. (ratio +. 1.)) in debug_print (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age)); - let symbols, card = - match active with - | (Negative, e)::_ -> - let symbols = symbols_of_equality e in - let card = TermMap.fold (fun k v res -> res + v) symbols 0 in - Some symbols, card - | _ -> None, 0 - in let counter = ref !symbols_ratio in - let rec pickw w ns ps = + let rec pickw w ps = if w > 0 then - if not (EqualitySet.is_empty ns) then - let e = EqualitySet.min_elt ns in - let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in - EqualitySet.add e ns', ps - else if !counter > 0 then + if !counter > 0 then let _ = counter := !counter - 1; - if !counter = 0 then counter := !symbols_ratio - in - match symbols with - | None -> - let e = EqualitySet.min_elt ps in - let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in - ns, EqualitySet.add e ps' - | Some symbols -> - 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 ps in - let initial = - let common, others = - TermMap.fold foldfun (symbols_of_equality e1) (0, 0) - in - (others + (abs (common - card))), e1 - in - let _, e = EqualitySet.fold f ps initial in - let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in - ns, EqualitySet.add e ps' + if !counter = 0 then counter := !symbols_ratio in + let e = EqualitySet.min_elt ps in + let ps' = pickw (w-1) (EqualitySet.remove e ps) in + EqualitySet.add e ps' else let e = EqualitySet.min_elt ps in - let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in - ns, EqualitySet.add e ps' + let ps' = pickw (w-1) (EqualitySet.remove e ps) in + EqualitySet.add e ps' else - EqualitySet.empty, EqualitySet.empty + EqualitySet.empty in - let ns, ps = pickw in_weight ns ps in + let ps = pickw in_weight ps in let rec picka w s l = if w > 0 then match l with @@ -438,7 +291,6 @@ let prune_passive howmany (active, _) passive = else 0, s, l in - 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_retained_equality := Some (EqualitySet.max_elt ps); @@ -446,222 +298,194 @@ let prune_passive howmany (active, _) passive = EqualitySet.fold (fun e tbl -> Indexing.index tbl e) ps Indexing.empty in - (nl, ns), (pl, ps), tbl + (pl, ps), tbl ;; (** inference of new equalities between current and some in active *) -let infer env sign current (active_list, active_table) = +let infer env current (active_list, active_table) = let (_,c,_) = env in if Utils.debug_metas then (ignore(Indexing.check_target c current "infer1"); - ignore(List.map (function (_,current) -> Indexing.check_target c current "infer2") active_list)); - let new_neg, new_pos = - match sign with - | Negative -> - let maxm, res = - Indexing.superposition_left !maxmeta env active_table current in - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup-1") res); - maxmeta := maxm; - res, [] - | Positive -> - let maxm, res = - Indexing.superposition_right !maxmeta env active_table current in - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup0") res); - maxmeta := maxm; - let rec infer_positive table = function - | [] -> [], [] - | (Negative, equality)::tl -> - let maxm, res = - Indexing.superposition_left !maxmeta env table equality in - maxmeta := maxm; - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "supl") res); - let neg, pos = infer_positive table tl in - res @ neg, pos - | (Positive, equality)::tl -> - let maxm, res = - Indexing.superposition_right !maxmeta env table equality in + ignore(List.map (function current -> Indexing.check_target c current "infer2") active_list)); + let new_pos = + let maxm, res = + Indexing.superposition_right !maxmeta env active_table current in + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "sup0") res); + maxmeta := maxm; + let rec infer_positive table = function + | [] -> [] + | equality::tl -> + let maxm, res = + Indexing.superposition_right !maxmeta env table equality in maxmeta := maxm; - if Utils.debug_metas then - ignore - (List.map - (function current -> - Indexing.check_target c current "sup2") res); - let neg, pos = infer_positive table tl in - neg, res @ pos - in - let maxm, copy_of_current = Inference.fix_metas !maxmeta current in + if Utils.debug_metas then + ignore + (List.map + (function current -> + Indexing.check_target c current "sup2") res); + let pos = infer_positive table tl in + res @ pos + in + let maxm, copy_of_current = Equality.fix_metas !maxmeta current in maxmeta := maxm; - let curr_table = Indexing.index Indexing.empty current in - let neg, pos = - infer_positive curr_table ((sign,copy_of_current)::active_list) - in - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup3") pos); - neg, res @ pos + let curr_table = Indexing.index Indexing.empty current in + let pos = infer_positive curr_table (copy_of_current::active_list) + in + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "sup3") pos); + res @ pos in - derived_clauses := !derived_clauses + (List.length new_neg) + - (List.length new_pos); + derived_clauses := !derived_clauses + (List.length new_pos); match !maximal_retained_equality with - | None -> - if Utils.debug_metas then - (ignore(List.map - (function current -> - Indexing.check_target c current "sup4") new_pos); - ignore(List.map - (function current -> - Indexing.check_target c current "sup5") new_neg)); - new_neg, new_pos - | Some eq -> + | None -> new_pos + | Some eq -> ignore(assert false); (* if we have a maximal_retained_equality, we can discard all equalities "greater" than it, as they will never be reached... An equality is greater than maximal_retained_equality if it is bigger wrt. OrderedEquality.compare and it is less similar than maximal_retained_equality to the current goal *) - let symbols, card = - match active_list with - | (Negative, e)::_ -> - let symbols = symbols_of_equality e in - let card = TermMap.fold (fun k v res -> res + v) symbols 0 in - Some symbols, card - | _ -> None, 0 - in - let new_pos = - match symbols with - | None -> - List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos - | Some symbols -> - let filterfun e = - if OrderedEquality.compare e eq <= 0 then - true - else - 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 initial = - let common, others = - TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in - others + (abs (common - card)) - in - let common, others = - TermMap.fold foldfun (symbols_of_equality e) (0, 0) in - let c = others + (abs (common - card)) in - if c < initial then true else false - in - List.filter filterfun new_pos - in - new_neg, new_pos + List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos ;; +let check_for_deep_subsumption env active_table eq = + let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in + if id = 14242 then assert false; + + let check_subsumed deep l r = + let eqtmp = + Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in + match Indexing.subsumption env active_table eqtmp with + | None -> false + | Some (s,eq') -> + prerr_endline + ("\n\n " ^ Equality.string_of_equality ~env eq ^ + "\nis"^(if deep then " CONTEXTUALLY " else " ")^"subsumed by \n " ^ + Equality.string_of_equality ~env eq' ^ "\n\n"); + true + in + let rec aux b (ok_so_far, subsumption_used) t1 t2 = + match t1,t2 with + | t1, t2 when not ok_so_far -> ok_so_far, subsumption_used + | t1, t2 when subsumption_used -> t1 = t2, subsumption_used + | Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 -> + let rc = check_subsumed b t1 t1 in + if rc then + true, true + else + (try + List.fold_left2 + (fun (ok_so_far, subsumption_used) t t' -> + aux true (ok_so_far, subsumption_used) t t') + (ok_so_far, subsumption_used) l l' + with Invalid_argument _ -> false,subsumption_used) + | _ -> false, subsumption_used + in + fst (aux false (true,false) left right) +;; -let contains_empty env (negative, positive) = - let metasenv, context, ugraph = env in - try - let found = - List.find - (fun (w, proof, (ty, left, right, ordering), m) -> - fst (CicReduction.are_convertible context left right ugraph)) - negative - in - true, Some found - with Not_found -> - false, None +(* +let check_for_deep env active_table eq = + match Indexing.subsumption env active_table eq with + | None -> false + | Some _ -> true +;; +*) + +let profiler = HExtlib.profile "check_for_deep";; + +let check_for_deep_subsumption env active_table eq = + profiler.HExtlib.profile (check_for_deep_subsumption env active_table) eq ;; +(* buttare via sign *) (** simplifies current using active and passive *) -let forward_simplify env (sign, current) ?passive (active_list, active_table) = +let forward_simplify env (sign,current) ?passive (active_list, active_table) = let _, context, _ = env in - let pl, passive_table = + let 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 + | None -> None + | Some ((_, _), pt) -> Some pt in - let all = if pl = [] then active_list else active_list @ pl in - let demodulate table current = let newmeta, newcurrent = Indexing.demodulation_equality !maxmeta env table sign current in maxmeta := newmeta; - if is_identity env newcurrent then - if sign = Negative then Some (sign, newcurrent) - else ( -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *) -(* (string_of_equality current) *) -(* (string_of_equality newcurrent))); *) -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "active is: %s" *) -(* (String.concat "\n" *) -(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *) - None - ) + if Equality.is_identity env newcurrent then +(* 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) + Some 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 ((function None -> () | Some x -> + ignore (Indexing.check_target context x "demod1");()) res); match res with | None -> None - | Some (sign, newcurrent) -> + | Some 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 newnewcurrent -> + if Equality.compare newcurrent newnewcurrent <> 0 then + demod newnewcurrent + else Some newnewcurrent + in + let res = demod current in match res with | None -> None - | Some (Negative, c) -> - let ok = not ( - List.exists - (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c) - all) - in - if ok then res else None - | Some (Positive, c) -> + | Some c -> if Indexing.in_index active_table c then None else match passive_table with | None -> - if fst (Indexing.subsumption env active_table c) then - None - else - res + if check_for_deep_subsumption env active_table c then + None + else + res +(* + if Indexing.subsumption env active_table c = None then + res + else + None +*) | Some passive_table -> if Indexing.in_index passive_table c then None else - let r1, _ = Indexing.subsumption env active_table c in - if r1 then None else - let r2, _ = Indexing.subsumption env passive_table c in - if r2 then None else res + if check_for_deep_subsumption env active_table c then + None + else +(* if Indexing.subsumption env active_table c = None then*) + (match Indexing.subsumption env passive_table c with + | None -> res + | Some (_,c') -> None (*Some c'*)) +(* + else + None +*) ;; type fs_time_info_t = { @@ -674,29 +498,22 @@ 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 forward_simplify_new env new_pos ?passive active = if Utils.debug_metas then begin let m,c,u = env in - ignore(List.map - (fun current -> - Indexing.check_target c current "forward new neg") new_neg); - ignore(List.map - (fun current -> Indexing.check_target c current "forward new pos") + ignore(List.map + (fun current -> Indexing.check_target c current "forward new pos") new_pos;) end; let t1 = Unix.gettimeofday () in let active_list, active_table = active in - let pl, passive_table = + let 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 + | None -> None + | Some ((_, _), pt) -> Some pt in - let t2 = Unix.gettimeofday () in fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1); @@ -707,26 +524,17 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = newtarget in let t1 = Unix.gettimeofday () in - - let new_neg, new_pos = - let new_neg = List.map (demodulate Negative active_table) new_neg - and new_pos = List.map (demodulate Positive active_table) new_pos in - new_neg,new_pos -(* PROVA - match passive_table with - | None -> new_neg, new_pos - | Some passive_table -> - List.map (demodulate Negative passive_table) new_neg, - List.map (demodulate Positive passive_table) new_pos *) + (* we could also demodulate using passive. Currently we don't *) + let new_pos = + List.map (demodulate Positive active_table) new_pos in - let t2 = Unix.gettimeofday () in fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1); let new_pos_set = List.fold_left (fun s e -> - if not (Inference.is_identity env e) then + if not (Equality.is_identity env e) then if EqualitySet.mem e s then s else EqualitySet.add e s else s) @@ -737,10 +545,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let subs = match passive_table with | None -> - (fun e -> not (fst (Indexing.subsumption env active_table e))) + (fun e -> (Indexing.subsumption env active_table e = None)) | Some passive_table -> - (fun e -> not ((fst (Indexing.subsumption env active_table e)) || - (fst (Indexing.subsumption env passive_table e)))) + (fun e -> ((Indexing.subsumption env active_table e = None) && + (Indexing.subsumption env passive_table e = None))) in (* let t1 = Unix.gettimeofday () in *) (* let t2 = Unix.gettimeofday () in *) @@ -754,100 +562,161 @@ 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 subs (List.filter is_duplicate new_pos) + List.filter subs (List.filter is_duplicate new_pos) +;; + + +(** simplifies a goal with equalities in active and passive *) +let rec simplify_goal env goal ?passive (active_list, active_table) = + let passive_table = + match passive with + | None -> None + | Some ((_, _), pt) -> Some pt + in + let demodulate table goal = + let changed, newmeta, newgoal = + Indexing.demodulation_goal !maxmeta env table goal in + maxmeta := newmeta; + changed, 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 = + let active_list, newa, pruned = List.fold_right - (fun (s, equality) (res, newn) -> - let ew, _, _, _ = equality in + (fun equality (res, newn,pruned) -> + let ew, _, _, _,id = Equality.open_equality equality in if ew < min_weight then - (s, equality)::res, newn + equality::res, newn,pruned else - match forward_simplify env (s, equality) (new_pos, new_table) with - | None -> res, newn - | Some (s, e) -> - if equality = e then - (s, e)::res, newn + match forward_simplify env (Utils.Positive, equality) (new_pos, new_table) with + | None -> res, newn, id::pruned + | Some e -> + if Equality.compare equality e = 0 then + e::res, newn, pruned else - res, (s, e)::newn) - active_list ([], []) + res, e::newn, pruned) + active_list ([], [],[]) in let find eq1 where = - List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where + List.exists (Equality.meta_convertibility_eq eq1) where in let active, newa = List.fold_right - (fun (s, eq) (res, tbl) -> - if List.mem (s, eq) res then + (fun eq (res, tbl) -> + if List.mem eq res then res, tbl - else if (is_identity env eq) || (find eq res) then ( + else if (Equality.is_identity env eq) || (find eq res) then ( res, tbl ) else - (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) + eq::res, Indexing.index tbl eq) active_list ([], Indexing.empty), List.fold_right - (fun (s, eq) (n, p) -> - if (s <> Negative) && (is_identity env eq) then ( - (n, p) - ) else - if s = Negative then eq::n, p - else n, eq::p) - newa ([], []) + (fun eq p -> + if (Equality.is_identity env eq) then p + else eq::p) + newa [] in match newa with - | [], [] -> active, None + | [] -> active, None | _ -> active, Some newa ;; (** 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 (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = - let ew, _, _, _ = equality in + let ew, _, _, _ , _ = Equality.open_equality equality in if ew < min_weight then equality::resl, ress, newn else match forward_simplify env (sign, equality) (new_pos, new_table) with | None -> resl, EqualitySet.remove equality ress, newn - | Some (s, e) -> + | Some e -> if equality = e then equality::resl, ress, newn else let ress = EqualitySet.remove equality ress in - resl, ress, e::newn + resl, ress, e::newn in - let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, []) - and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in + let pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in let passive_table = List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pl in - match newn, newp with - | [], [] -> ((nl, ns), (pl, ps), passive_table), None - | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp) + match newp with + | [] -> ((pl, ps), passive_table), None + | _ -> ((pl, ps), passive_table), Some (newp) ;; +let build_table equations = + List.fold_left + (fun (l, t, w) e -> + let ew, _, _, _ , _ = Equality.open_equality e in + e::l, Indexing.index t e, min ew w) + ([], Indexing.empty, 1000000) equations +;; + let backward_simplify env new' ?passive active = - let new_pos, new_table, min_weight = + let new_pos, new_table, min_weight = build_table new' in +(* List.fold_left (fun (l, t, w) e -> - let ew, _, _, _ = e in - (Positive, e)::l, Indexing.index t e, min ew w) - ([], Indexing.empty, 1000000) (snd new') + let ew, _, _, _ , _ = Equality.open_equality e in + e::l, Indexing.index t e, min ew w) + ([], Indexing.empty, 1000000) new' in +*) let active, newa = backward_simplify_active env new_pos new_table min_weight active in match passive with | None -> - active, (make_passive [] []), newa, None + active, (make_passive []), newa, None | Some passive -> active, passive, newa, None (* prova @@ -861,23 +730,25 @@ let close env new' given = let new_pos, new_table, min_weight = List.fold_left (fun (l, t, w) e -> - let ew, _, _, _ = e in - (Positive, e)::l, Indexing.index t e, min ew w) + let ew, _, _, _ , _ = Equality.open_equality e in + e::l, Indexing.index t e, min ew w) ([], Indexing.empty, 1000000) (snd new') in List.fold_left - (fun (n,p) (s,c) -> - let neg,pos = infer env s c (new_pos,new_table) in - neg@n,pos@p) - ([],[]) given + (fun p c -> + let pos = infer env c (new_pos,new_table) in + pos@p) + [] given ;; let is_commutative_law eq = - let w, proof, (eq_ty, left, right, order), metas = snd eq in + let w, proof, (eq_ty, left, right, order), metas , _ = + Equality.open_equality eq + in match left,right with - Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], - Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] -> - f1 = f2 && a1 = b2 && a2 = b1 + Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], + Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] -> + f1 = f2 && a1 = b2 && a2 = b1 | _ -> false ;; @@ -888,10 +759,9 @@ let prova env new' active = (lazy (Printf.sprintf "symmetric:\n%s\n" (String.concat "\n" - ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) - (given)))))) in + (List.map + (fun e -> Equality.string_of_equality ~env e) + given)))) in close env new' given ;; @@ -921,9 +791,12 @@ let make_theorems theorems = let activate_goal (active, passive) = - match passive with - | goal_conj::tl -> true, (goal_conj::active, tl) - | [] -> false, (active, passive) + if active = [] then + match passive with + | goal_conj::tl -> true, (goal_conj::active, tl) + | [] -> false, (active, passive) + else + true, (active,passive) ;; @@ -934,60 +807,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 = @@ -1027,10 +846,10 @@ let rec simpl env e others others_simpl = let active = others @ others_simpl in let tbl = List.fold_left - (fun t (_, e) -> Indexing.index t e) + (fun t e -> Indexing.index t e) Indexing.empty active in - let res = forward_simplify env e (active, tbl) in + let res = forward_simplify env (Positive,e) (active, tbl) in match others with | hd::tl -> ( match res with @@ -1049,447 +868,22 @@ let simplify_equalities env equalities = (lazy (Printf.sprintf "equalities:\n%s\n" (String.concat "\n" - (List.map string_of_equality equalities)))); + (List.map Equality.string_of_equality equalities)))); debug_print (lazy "SIMPLYFYING EQUALITIES..."); match equalities with | [] -> [] | hd::tl -> - let others = List.map (fun e -> (Positive, e)) tl in let res = - List.rev (List.map snd (simpl env (Positive, hd) others [])) + List.rev (simpl env hd tl []) in debug_print (lazy (Printf.sprintf "equalities AFTER:\n%s\n" (String.concat "\n" - (List.map string_of_equality res)))); + (List.map Equality.string_of_equality res)))); 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 = equality in - 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 - 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.ProofBlock (s, uri, nt, t, pe, p) -> - I.ProofBlock (subst @ s, uri, nt, t, pe, p) - | _ -> assert false - in - let newgproof = - 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) - | _ -> assert false - in - repl gproof - in - true, subst, newgproof - with CicUnification.UnificationFailure _ -> - false, [], I.NoProof -;; - - - -let new_meta metasenv = - let m = CicMkImplicit.new_meta metasenv [] in - incr maxmeta; - while !maxmeta <= m do incr maxmeta done; - !maxmeta -;; - - -(* 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" *) - (* (\* (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, p) -> - let t', i' = get_meta p in - if i' = -1 then t, i else t', i' - | ProofGoalBlock (_, p) -> get_meta p - | _ -> Cic.Implicit None, -1 - in - 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 metasenv = (newmeta, context, term)::metasenv @ metas in - 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 - | (theorem, thmty, _)::tl -> - try - let subst, (newproof, newgoals) = - PrimitiveTactics.apply_tac_verbose_with_subst ~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 - let _, m = status in - let subst = List.filter (fun (i, _) -> i = m) subst in - `Ok (subst, [newp, metas, term]) - else - 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 p' = - let rec gp = function - | SubProof (t, i, p) -> - SubProof (t, i, gp p) - | ProofGoalBlock (sp1, sp2) -> - ProofGoalBlock (sp1, gp sp2) - | BasicProof _ - | NoProof -> - SubProof (p, i, BasicProof (Cic.Meta (i, irl))) - | ProofSymBlock (s, sp) -> - ProofSymBlock (s, gp sp) - | ProofBlock (s, u, nt, t, pe, sp) -> - ProofBlock (s, u, nt, t, pe, gp sp) - in gp proof - in - (p', menv, ty)) - newgoals - in - 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 -> `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_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_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 - 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 - if r = true then `Ok (s, l) else aux theorems -;; - - -(* 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 - 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 - if depth > !maxdepth || (List.length goals) > !maxwidth then - `No (depth, 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 - - let compare g1 g2 = - let d1, l1 = g1 - and d2, l2 = g2 in - 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 -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 = - List.fold_left (fun s g -> GoalsSet.add g s) set goals - in - let rec aux set = function - | [] -> - debug_print (lazy "HERE!!!"); - if is_passive_empty then raise SearchSpaceOver else false, set - | goals::tl -> - let res = apply_to_goal_conj env theorems active goals in - match res with - | `Ok newgoals -> - let _ = - let d, p, t = - match newgoals with - | (d, (p, _, t)::_) -> d, p, t - | _ -> assert false - in - debug_print - (lazy - (Printf.sprintf "\nOK!!!!\ndepth: %d\nProof: %s\ngoal: %s\n" - d (string_of_proof p) (CicPp.ppterm t))) - in - true, GoalsSet.singleton newgoals - | `GoOn newgoals -> - let set' = add_to set (goals::tl) in - let set' = add_to set' newgoals in - false, set' - | `No newgoals -> - aux set tl - in - let n = List.length goals in - let res, goals = aux (add_to GoalsSet.empty goals) goals in - let goals = GoalsSet.elements goals in - debug_print (lazy "\n\tapply_to_goals end\n"); - let m = List.length goals in - if m = n && is_passive_empty then - raise SearchSpaceOver - 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 @@ -1502,245 +896,55 @@ let print_goals goals = 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 _,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 *) - 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 - -and given_clause_aux dbd env goals theorems passive active = - let _,context,_ = env in - let time1 = Unix.gettimeofday () in - - let selection_estimate = get_selection_estimate () in - let kept = size_of_passive passive in - let passive = - if !time_limit = 0. || !processed_clauses = 0 then - passive - else if !elapsed_time > !time_limit then ( - debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time)); - make_passive [] [] - ) else if kept > selection_estimate then ( - debug_print - (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ - "(kept: %d, selection_estimate: %d)\n") - kept selection_estimate)); - prune_passive selection_estimate active passive - ) else - passive - in - - 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 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 = " ^ - (CicPp.pp (Inference.term_of_equality current) names)); - let time1 = Unix.gettimeofday () in - let res = forward_simplify env (sign, current) ~passive active in - let time2 = Unix.gettimeofday () in - 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 -> (sign, current)::al, tbl - | Positive -> - al @ [(sign, current)], Indexing.index tbl current - in - let passive = add_to_passive passive new' 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 check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table = + prerr_endline "check_goal_subsumed"; + match ty with + | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] + when UriManager.eq uri (LibraryObjects.eq_URI ()) -> + (let goal_equation = + Equality.mk_equality + (0,(Equality.Exact (Cic.Rel (-1)),proof),(eq_ty,left,right,Eq),menv) + in + match Indexing.subsumption env table goal_equation with + | Some (subst, equality ) -> + let (_,(np,p),(ty,l,r,_),m,id) = + Equality.open_equality equality in + prerr_endline "1"; + let p = Equality.apply_subst subst + (Equality.build_proof_term_old p) in + prerr_endline "2"; + let newp = + let rec repl = function + | Equality.ProofGoalBlock (_, gp) -> + Equality.ProofGoalBlock + (Equality.BasicProof (Equality.empty_subst,p), gp) + | Equality.NoProof -> + Equality.BasicProof (Equality.empty_subst,p) + | Equality.BasicProof _ -> + Equality.BasicProof (Equality.empty_subst,p) + | Equality.SubProof (t, i, p2) -> + Equality.SubProof (t, i, repl p2) + | _ -> assert false + in + repl proof + in + prerr_endline "3"; + let newcicp,np,subst,cicmenv = + cicproof,np, subst, + Equality.apply_subst_metasenv subst (m @ menv) + in + prerr_endline "."; + Some + ((newcicp,np,subst,cicmenv), + (newp, Equality.apply_subst_metasenv subst m @ menv )) + | None -> None) + | _ -> None ;; +let counter = ref 0 (** given-clause algorithm with full reduction strategy *) -let rec given_clause_fullred dbd env goals theorems passive active = +let rec given_clause_fullred dbd env goals theorems ~passive active = let goals = simplify_goals env goals ~passive active in let _,context,_ = env in let ok, goals = activate_goal goals in @@ -1761,31 +965,62 @@ 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 + | Equality.ProofGoalBlock (_, gp) -> + Equality.ProofGoalBlock + (Equality.BasicProof (Equality.empty_subst,p), gp) + | Equality.NoProof -> + + Equality.BasicProof (Equality.empty_subst,p) + | Equality.BasicProof _ -> + Equality.BasicProof (Equality.empty_subst,p) + | Equality.SubProof (t, i, p2) -> + Equality.SubProof (t, i, repl p2) + | _ -> assert false + in + repl (snd proof) + in + let reflproof = Equality.refl_proof eq_ty left in + true, + Some ((fst proof,Equality.Exact reflproof, + Equality.empty_subst,m), + (newp,m)) + | (_, [proof,m,ty])::_ -> + (match check_if_goal_is_subsumed env (proof,m,ty) (snd active) with + | None -> false,None + | Some p -> + prerr_endline "Proof found by subsumption!"; + true, Some p) + | _ -> false, None + in if ok then - let proof = - match (fst goals) with - | (_, [proof, _, _])::_ -> Some proof - | _ -> assert false - in ( prerr_endline "esco qui"; (* - let s = Printf.sprintf "actives:\n%s\n" - (String.concat "\n" + let s = Printf.sprintf "actives:\n%s\n" + (String.concat "\n" ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ + (fun (s, e) -> (string_of_sign s) ^ " " ^ (string_of_equality ~env e)) - (fst active)))) in - let sp = Printf.sprintf "passives:\n%s\n" - (String.concat "\n" + (fst active)))) in + let sp = Printf.sprintf "passives:\n%s\n" + (String.concat "\n" (List.map - (string_of_equality ~env) - (let x,y,_ = passive in (fst x)@(fst y)))) in - prerr_endline s; - prerr_endline sp; *) - ParamodulationSuccess (proof, env)) + (string_of_equality ~env) + (let x,y,_ = passive in (fst x)@(fst y)))) in + prerr_endline s; + prerr_endline sp; *) + ParamodulationSuccess (proof)) else given_clause_fullred_aux dbd env goals theorems passive active else @@ -1806,10 +1041,29 @@ 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 ^ - " LOCALMAX: " ^ string_of_int !Indexing.local_max ^ - " #ACTIVES: " ^ string_of_int (size_of_active active) ^ + prerr_endline (string_of_int !counter ^ + " MAXMETA: " ^ string_of_int !maxmeta ^ + " #ACTIVES: " ^ string_of_int (size_of_active active) ^ " #PASSIVES: " ^ string_of_int (size_of_passive passive)); + 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" @@ -1835,7 +1089,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = else if !elapsed_time > !time_limit then ( debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" !time_limit !elapsed_time)); - make_passive [] [] + make_passive [] ) else if kept > selection_estimate then ( debug_print (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ @@ -1851,91 +1105,86 @@ and given_clause_fullred_aux dbd env goals theorems passive active = 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 + | true -> ParamodulationFailure + (* 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));*) + let current, passive = select env (fst goals) passive in + prerr_endline + ("Selected = " ^ Equality.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 res = forward_simplify env (Positive, 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 (sign = Negative) && (is_identity env current) then ( + | Some current -> +(* prerr_endline (Printf.sprintf "selected simpl: %s" + (Equality.string_of_equality ~env current));*) + let t1 = Unix.gettimeofday () in + let new' = infer env current active in + let _ = 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 _ = - match new' with - | neg, pos -> - debug_print - (lazy - (Printf.sprintf "new' (senza semplificare):\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))))) - in - let t2 = Unix.gettimeofday () in + (lazy + (Printf.sprintf "new' (senza semplificare):\n%s\n" + (String.concat "\n" + (List.map + (fun e -> "Positive " ^ + (Equality.string_of_equality ~env e)) new')))) + in + let t2 = Unix.gettimeofday () in infer_time := !infer_time +. (t2 -. t1); let active = - if is_identity env current then active + if Equality.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 + al @ [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 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 | None, None -> active, passive, new' - | Some (n, p), None - | 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 - | Some (n, p), Some (rn, rp) -> - let nn, np = new' in - simplify (nn @ n @ rn, np @ p @ rp) active passive + | Some p, None + | None, Some p -> + if Utils.debug_metas then + begin + List.iter + (fun x->Indexing.check_target context x "simplify1") + p; + end; + simplify (new' @ p) active passive + | Some p, Some rp -> + simplify (new' @ p @ rp) active passive + in + let active, _, new' = simplify new' active passive in + let goals = + let a,b,_ = build_table new' in + simplify_goals env goals ~passive (a,b) in - let active, passive, new' = simplify new' active passive in + (* pessima prova - let new1 = prova env new' active in + let new1 = prova env new' active in let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in let _ = match new1 with @@ -1962,62 +1211,50 @@ end prova *) (Printf.sprintf "active:\n%s\n" (String.concat "\n" ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) + (fun e -> (Equality.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))))) + debug_print + (lazy + (Printf.sprintf "new':\n%s\n" + (String.concat "\n" + ((List.map + (fun e -> "Negative " ^ + (Equality.string_of_equality ~env e)) new'))))) 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 - ParamodulationSuccess (proof, env) - ) + let passive = add_to_passive passive new' in + given_clause_fullred dbd env goals theorems passive active ;; +(* +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; if !elapsed_time > !time_limit then (active, passive) else - let (sign, current), passive = select env [1, [goal]] passive active in - let res = forward_simplify env (sign, current) ~passive active in + let current, passive = select env [1, [goal]] passive in + let res = forward_simplify env (Positive, current) ~passive active in match res with | None -> saturate_equations env goal accept_fun passive active - | Some (sign, current) -> - assert (sign = Positive); - debug_print - (lazy "\n================================================"); - debug_print (lazy (Printf.sprintf "selected: %s %s" - (string_of_sign sign) - (string_of_equality ~env current))); - let new' = infer env sign current active in + | Some current -> + debug_print (lazy (Printf.sprintf "selected: %s" + (Equality.string_of_equality ~env current))); + let new' = infer env current active in let active = - if is_identity env current then active + if Equality.is_identity env current then active else let al, tbl = active in - al @ [(sign, current)], Indexing.index tbl current + al @ [current], Indexing.index tbl current in let rec simplify new' active passive = let new' = forward_simplify_new env new' ~passive active in @@ -2025,13 +1262,9 @@ let rec saturate_equations env goal accept_fun passive active = backward_simplify env new' ~passive active in 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 + | Some p, None + | None, Some p -> simplify (new' @ p) active passive + | Some p, Some rp -> simplify (new' @ p @ rp) active passive in let active, passive, new' = simplify new' active passive in let _ = @@ -2039,33 +1272,26 @@ let rec saturate_equations env goal accept_fun passive active = (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)))))) + (List.map + (fun e -> Equality.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))))) + debug_print + (lazy + (Printf.sprintf "new':\n%s\n" + (String.concat "\n" + (List.map + (fun e -> "Negative " ^ + (Equality.string_of_equality ~env e)) new')))) in - let new' = match new' with _, pos -> [], List.filter accept_fun pos in + let new' = List.filter accept_fun new' in let passive = add_to_passive passive new' in saturate_equations env goal accept_fun passive active ;; - - - +let main dbd full term metasenv ugraph = () +(* let main dbd full term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in @@ -2127,11 +1353,13 @@ let main dbd full term metasenv ugraph = (fst theorems))))) in (*try*) - let goal = Inference.BasicProof new_meta_goal, [], goal in + let goal = + ([],Equality.BasicProof (Equality.empty_subst ,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 + 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); @@ -2139,7 +1367,7 @@ let main dbd full term metasenv ugraph = Printf.printf "\nequalities:\n%s\n" (String.concat "\n" (List.map - (string_of_equality ~env) equalities)); + (Equality.string_of_equality ~env) equalities)); (* (equalities @ library_equalities))); *) print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in @@ -2147,7 +1375,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 @@ -2155,17 +1383,27 @@ let main dbd full term metasenv ugraph = match res with | ParamodulationFailure -> Printf.printf "NO proof found! :-(\n\n" - | ParamodulationSuccess (Some proof, env) -> - let proof = Inference.build_proof_term proof in + | ParamodulationSuccess (Some ((cicproof,cicmenv),(proof, env))) -> Printf.printf "OK, found a proof!\n"; + let oldproof = Equation.build_proof_term proof in + let newproof,_,newenv,_ = + CicRefine.type_of_aux' + cicmenv context cicproof CicUniv.empty_ugraph + in (* 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 + prerr_endline "OLD PROOF"; print_endline (PP.pp proof names); + prerr_endline "NEW PROOF"; + print_endline (PP.pp newproof names); let newmetasenv = List.fold_left - (fun m (_, _, _, menv) -> m @ menv) metasenv equalities + (fun m eq -> + let (_, _, _, menv,_) = Equality.open_equality eq in + m @ menv) + metasenv equalities in let _ = (*try*) @@ -2186,46 +1424,43 @@ let main dbd full term metasenv ugraph = in () - | ParamodulationSuccess (None, env) -> + | ParamodulationSuccess None -> Printf.printf "Success, but no proof?!?\n\n" in - if Utils.time then - begin - prerr_endline - ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ + if Utils.time then + begin + prerr_endline + ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ "forward_simpl_new_time: %.9f\n" ^^ "backward_simpl_time: %.9f\n") !infer_time !forward_simpl_time !forward_simpl_new_time !backward_simpl_time) ^ - (Printf.sprintf "beta_expand_time: %.9f\n" - !Indexing.beta_expand_time) ^ - (Printf.sprintf "passive_maintainance_time: %.9f\n" - !passive_maintainance_time) ^ - (Printf.sprintf " successful unification/matching time: %.9f\n" - !Indexing.match_unif_time_ok) ^ - (Printf.sprintf " failed unification/matching time: %.9f\n" - !Indexing.match_unif_time_no) ^ - (Printf.sprintf " indexing retrieval time: %.9f\n" - !Indexing.indexing_retrieval_time) ^ - (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n" - !Indexing.build_newtarget_time) ^ - (Printf.sprintf "derived %d clauses, kept %d clauses.\n" - !derived_clauses !kept_clauses)) - end + (Printf.sprintf "passive_maintainance_time: %.9f\n" + !passive_maintainance_time) ^ + (Printf.sprintf " successful unification/matching time: %.9f\n" + !Indexing.match_unif_time_ok) ^ + (Printf.sprintf " failed unification/matching time: %.9f\n" + !Indexing.match_unif_time_no) ^ + (Printf.sprintf " indexing retrieval time: %.9f\n" + !Indexing.indexing_retrieval_time) ^ + (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n" + !Indexing.build_newtarget_time) ^ + (Printf.sprintf "derived %d clauses, kept %d clauses.\n" + !derived_clauses !kept_clauses)) + end (* with exc -> print_endline ("EXCEPTION: " ^ (Printexc.to_string exc)); raise exc *) ;; - +*) let default_depth = !maxdepth and default_width = !maxwidth;; let reset_refs () = maxmeta := 0; - Indexing.local_max := 100; symbols_counter := 0; weight_age_counter := !weight_age_ratio; processed_clauses := 0; @@ -2239,21 +1474,23 @@ let reset_refs () = passive_maintainance_time := 0.; derived_clauses := 0; kept_clauses := 0; - Indexing.beta_expand_time := 0.; - Inference.metas_of_proof_time := 0.; + Equality.reset (); ;; -let saturate +let saturate dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in reset_refs (); Indexing.init_index (); + counter := 0; 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 + let names = names_of_context context in let eq_indexes, equalities, maxm = find_equalities context proof in let new_meta_goal, metasenv, type_of_goal = let irl = @@ -2266,8 +1503,10 @@ 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 = + ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal + in let res, time = let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = @@ -2313,7 +1552,7 @@ let saturate (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); in let active = make_active () in - let passive = make_passive [] equalities in + let passive = make_passive equalities in let start = Unix.gettimeofday () in let res = let goals = make_goals goal in @@ -2323,10 +1562,77 @@ let saturate (res, finish -. start) in match res with - | ParamodulationSuccess (Some proof, env) -> - debug_print (lazy "OK, found a proof!"); - let proof = Inference.build_proof_term proof in - let names = names_of_context context in + | ParamodulationSuccess + (Some + ((goalproof,newproof,subsumption_subst, newproof_menv), (* NEW *) + (proof, proof_menv))) (* OLD *) + -> + prerr_endline "OK, found a proof!"; + + prerr_endline "NEWPROOF"; + (* prerr_endline (Equality.string_of_proof_new ~names newproof + * goalproof);*) + prerr_endline (Equality.pp_proof names goalproof newproof); + + (* generation of the old proof *) + let cic_proof = Equality.build_proof_term_old proof in + + (* generation of the new proof *) + let cic_proof_new = + Equality.build_goal_proof + goalproof (Equality.build_proof_term_new newproof) + in + let cic_proof_new = + Equality.apply_subst subsumption_subst cic_proof_new + in + + (* replacing fake mets with real ones *) + let equality_for_replace i t1 = + match t1 with + | C.Meta (n, _) -> n = i + | _ -> false + in + let mkirl = CicMkImplicit.identity_relocation_list_for_metavariable in + prerr_endline "replacing metas (old)"; + let proof_menv, what, with_what = + let irl = mkirl context in + List.fold_left + (fun (acc1,acc2,acc3) (i,_,ty) -> + (i,context,ty)::acc1, + (Cic.Meta(i,[]))::acc2, + (Cic.Meta(i,irl)) ::acc3) + ([],[],[]) proof_menv + in + let cic_proof = ProofEngineReduction.replace_lifting + ~equality:(=) + ~what ~with_what + ~where:cic_proof + in + prerr_endline "replacing metas (new)"; + let newproof_menv, what, with_what = + let irl = mkirl context in + List.fold_left + (fun (acc1,acc2,acc3) (i,_,ty) -> + (i,context,ty)::acc1, + (Cic.Meta(i,[]))::acc2, + (Cic.Meta(i,irl)) ::acc3) + ([],[],[]) newproof_menv + in + let cic_proof_new = ProofEngineReduction.replace_lifting + ~equality:(=) + ~what ~with_what + ~where:cic_proof_new + in + + (* pp new/old proof *) +(* prerr_endline "OLDPROOF";*) +(* prerr_endline (Equality.string_of_proof_old proof);*) +(* prerr_endline "OLDPROOFCIC";*) +(* prerr_endline (CicPp.pp cic_proof names); *) +(* prerr_endline "NEWPROOFCIC";*) +(* prerr_endline (CicPp.pp cic_proof_new names); *) + + (* generation of proof metasenv *) let newmetasenv = let i1 = match new_meta_goal with @@ -2334,70 +1640,108 @@ let saturate in List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv in + let newmetasenv_new = newmetasenv@newproof_menv in + let newmetasenv = newmetasenv@proof_menv in + (* check/refine/... build the new proof *) let newstatus = - try - let ty, ug = - CicTypeChecker.type_of_aux' newmetasenv context proof ugraph - in - debug_print (lazy (CicPp.pp proof [](* names *))); - debug_print - (lazy - (Printf.sprintf - "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n" - (CicPp.pp type_of_goal names) (CicPp.pp ty names) - (string_of_bool - (fst (CicReduction.are_convertible - context type_of_goal ty ug))))); - let equality_for_replace i t1 = - match t1 with - | C.Meta (n, _) -> n = i - | _ -> false + let cic_proof,newmetasenv,proof_menv,ty, ug = + prerr_endline "type checking ... (old) "; + let _old_ty, _oldug = + try + CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph + with + CicTypeChecker.TypeCheckerFailure s -> + prerr_endline "THE *OLD* PROOF DOESN'T TYPECHECK!!!"; + prerr_endline (Lazy.force s); + Cic.Implicit None, CicUniv.empty_ugraph in - let real_proof = - ProofEngineReduction.replace - ~equality:equality_for_replace - ~what:[goal'] ~with_what:[proof] - ~where:meta_proof + let cic_proof_new,new_ty,newmetasenv_new,newug = + try + (* + prerr_endline "refining ... (new) "; + CicRefine.type_of_aux' + newmetasenv_new context cic_proof_new ugraph + *) + let ty,ug = + prerr_endline "typechecking ... (new) "; + CicTypeChecker.type_of_aux' + newmetasenv_new context cic_proof_new ugraph + in + cic_proof_new, ty, newmetasenv_new, ug + with + | CicTypeChecker.TypeCheckerFailure s -> + prerr_endline "THE PROOF DOESN'T TYPECHECK!!!"; + prerr_endline (Lazy.force s); + assert false + | CicRefine.RefineFailure s + | CicRefine.Uncertain s + | CicRefine.AssertFailure s -> + prerr_endline "FAILURE IN REFINE"; + prerr_endline (Lazy.force s); + assert false in - debug_print - (lazy - (Printf.sprintf "status:\n%s\n%s\n%s\n%s\n" - (match uri with Some uri -> UriManager.string_of_uri uri - | None -> "") - (print_metasenv newmetasenv) - (CicPp.pp real_proof [](* names *)) - (CicPp.pp term_to_prove names))); - ((uri, newmetasenv, real_proof, term_to_prove), []) - with CicTypeChecker.TypeCheckerFailure _ -> - debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!"); - debug_print (lazy (CicPp.pp proof names)); - raise (ProofEngineTypes.Fail - (lazy "Found a proof, but it doesn't typecheck")) + if List.length newmetasenv_new <> 0 then + prerr_endline + ("Some METAS are still open: "(* ^ CicMetaSubst.ppmetasenv + [] newmetasenv_new*)); + cic_proof_new, newmetasenv_new, newmetasenv_new,new_ty, newug + (* THE OLD PROOF: cic_proof,newmetasenv,proof_menv,oldty,oldug *) + in +(* prerr_endline "FINAL PROOF";*) +(* prerr_endline (CicPp.pp cic_proof names);*) + prerr_endline "ENDOFPROOFS"; + (* + debug_print + (lazy + (Printf.sprintf + "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n" + (CicPp.pp type_of_goal names) (CicPp.pp ty names) + (string_of_bool + (fst (CicReduction.are_convertible + context type_of_goal ty ug))))); + *) + let real_proof = + ProofEngineReduction.replace + ~equality:equality_for_replace + ~what:[goal'] ~with_what:[cic_proof] + ~where:meta_proof + in + (* + debug_print + (lazy + (Printf.sprintf "status:\n%s\n%s\n%s\n%s\n" + (match uri with Some uri -> UriManager.string_of_uri uri + | None -> "") + (print_metasenv newmetasenv) + (CicPp.pp real_proof [](* names *)) + (CicPp.pp term_to_prove names))); + *) + let open_goals = List.map (fun (i,_,_) -> i) proof_menv in + (uri, newmetasenv, real_proof, term_to_prove), open_goals in - let tall = fs_time_info.build_all in - let tdemodulate = fs_time_info.demodulate in - let tsubsumption = fs_time_info.subsumption in if Utils.time then - begin - prerr_endline ( - (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^ - (Printf.sprintf "\ntall: %.9f" tall) ^ - (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^ - (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^ - (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^ - (Printf.sprintf "\nbeta_expand_time: %.9f\n" - !Indexing.beta_expand_time) ^ - (Printf.sprintf "\nmetas_of_proof: %.9f\n" - !Inference.metas_of_proof_time) ^ - (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^ - (Printf.sprintf "\nforward_simpl_new_times: %.9f" - !forward_simpl_new_time) ^ - (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^ - (Printf.sprintf "\npassive_maintainance_time: %.9f" - !passive_maintainance_time)) - end; - newstatus - | _ -> + begin + let tall = fs_time_info.build_all in + let tdemodulate = fs_time_info.demodulate in + let tsubsumption = fs_time_info.subsumption in + prerr_endline ( + (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^ + (Printf.sprintf "\ntall: %.9f" tall) ^ + (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^ + (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^ + (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^ + (Printf.sprintf "\nforward_simpl_times: %.9f" + !forward_simpl_time) ^ + (Printf.sprintf "\nforward_simpl_new_times: %.9f" + !forward_simpl_new_time) ^ + (Printf.sprintf "\nbackward_simpl_times: %.9f" + !backward_simpl_time) ^ + (Printf.sprintf "\npassive_maintainance_time: %.9f" + !passive_maintainance_time)) + end; + newstatus + | ParamodulationSuccess None -> assert false + | ParamodulationFailure -> raise (ProofEngineTypes.Fail (lazy "NO proof found")) ;; @@ -2438,14 +1782,14 @@ let retrieve_and_print dbd term metasenv ugraph = debug_print (lazy (Printf.sprintf "\n\nequalities:\n%s\n" - (String.concat "\n" + (String.concat "\n" (List.map - (fun (u, e) -> -(* Printf.sprintf "%s: %s" *) - (UriManager.string_of_uri u) -(* (string_of_equality e) *) - ) - equalities)))); + (fun (u, e) -> +(* Printf.sprintf "%s: %s" *) + (UriManager.string_of_uri u) +(* (string_of_equality e) *) + ) + equalities)))); debug_print (lazy "RETR: SIMPLYFYING EQUALITIES..."); let rec simpl e others others_simpl = let (u, e) = e in @@ -2459,36 +1803,36 @@ let retrieve_and_print dbd term metasenv ugraph = let res = forward_simplify env (Positive, e) (active, tbl) in match others with | hd::tl -> ( - match res with - | None -> simpl hd tl others_simpl - | Some e -> simpl hd tl ((u, (snd e))::others_simpl) - ) + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl ((u, e)::others_simpl) + ) | [] -> ( - match res with - | None -> others_simpl - | Some e -> (u, (snd e))::others_simpl - ) + match res with + | None -> others_simpl + | Some e -> (u, e)::others_simpl + ) in let _equalities = match equalities with | [] -> [] | hd::tl -> - let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) - let res = - List.rev (simpl (*(Positive,*) hd others []) - in - debug_print - (lazy - (Printf.sprintf "\nequalities AFTER:\n%s\n" - (String.concat "\n" - (List.map - (fun (u, e) -> - Printf.sprintf "%s: %s" - (UriManager.string_of_uri u) - (string_of_equality e) - ) - res)))); - res in + let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) + let res = + List.rev (simpl (*(Positive,*) hd others []) + in + debug_print + (lazy + (Printf.sprintf "\nequalities AFTER:\n%s\n" + (String.concat "\n" + (List.map + (fun (u, e) -> + Printf.sprintf "%s: %s" + (UriManager.string_of_uri u) + (Equality.string_of_equality e) + ) + res)))); + res in debug_print (lazy (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) @@ -2525,16 +1869,18 @@ 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 = + ([],Equality.BasicProof (Equality.empty_subst,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 + let passive = make_passive equalities in 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)); + (Equality.string_of_equality ~env) equalities)); print_endline "--------------------------------------------------"; print_endline "GO!"; start_time := Unix.gettimeofday (); @@ -2553,20 +1899,20 @@ let main_demod_equalities dbd term metasenv ugraph = let passive = match rp with - | (n, _), (p, _), _ -> + | (p, _), _ -> EqualitySet.elements (List.fold_left addfun EqualitySet.empty p) in let active = - let l = List.map snd (fst ra) in + let l = fst ra in EqualitySet.elements (List.fold_left addfun EqualitySet.empty l) in Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n" - (String.concat "\n" (List.map (string_of_equality ~env) active)) + (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) (* (String.concat "\n" (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *) (* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *) (String.concat "\n" - (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive)); + (List.map (fun e -> CicPp.ppterm (Equality.term_of_equality e)) passive)); print_newline (); (* with e -> @@ -2585,7 +1931,9 @@ 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 = + ([],Equality.BasicProof (Equality.empty_subst,goalterm)), [], ty + in let env = (metasenv, context, CicUniv.empty_ugraph) in let equalities = simplify_equalities env (equalities@library_equalities) in let table = @@ -2593,22 +1941,23 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = (fun tbl eq -> Indexing.index tbl eq) Indexing.empty equalities in - let newmeta,(newproof,newmetasenv, newty) = Indexing.demodulation_goal - maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal + let _, newmeta,(newproof,newmetasenv, newty) = + Indexing.demodulation_goal + maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal in if newmeta != maxm then begin let opengoal = Cic.Meta(maxm,irl) in let proofterm = - Inference.build_proof_term ~noproof:opengoal newproof in + Equality.build_proof_term_old ~noproof:opengoal (snd newproof) in let extended_metasenv = (maxm,context,newty)::metasenv in - let extended_status = - (curi,extended_metasenv,pbo,pty),goal in - let (status,newgoals) = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) - extended_status in - (status,maxm::newgoals) + let extended_status = + (curi,extended_metasenv,pbo,pty),goal in + let (status,newgoals) = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) + extended_status in + (status,maxm::newgoals) end else if newty = ty then raise (ProofEngineTypes.Fail (lazy "no progress"))