X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=ff58512ea9d1f47c429d6f0f6b412fc5c96b4165;hb=f809c7537eda20a275b17bc1407f0ee446f70356;hp=bf9f8ba57dde43b7bcbbdf6b9fa0cb73a2940fc6;hpb=fd65a0a393bfb43d88ff936f40f045511e900e26;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index bf9f8ba57..ff58512ea 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -23,33 +23,12 @@ * http://cs.unibo.it/helm/. *) -(* $Id$ *) - -open Inference;; -open Utils;; +(* let _profiler = <:profiler<_profiler>>;; *) - -(* -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 -*) +(* $Id$ *) (* 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,174 +70,148 @@ let maxmeta = ref 0;; let maxdepth = ref 3;; let maxwidth = ref 3;; - -type result = - | ParamodulationFailure - | 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, _), _) = - let m1 = symbols_of_term left in +let symbols_of_equality equality = + let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in + let m1 = Utils.symbols_of_term left in let m = - TermMap.fold + Utils.TermMap.fold (fun k v res -> try - let c = TermMap.find k res in - TermMap.add k (c+v) res + let c = Utils.TermMap.find k res in + Utils.TermMap.add k (c+v) res with Not_found -> - TermMap.add k v res) - (symbols_of_term right) m1 + Utils.TermMap.add k v res) + (Utils.symbols_of_term right) m1 in m ;; (* 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 + | false -> + 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 - | _ -> false +type passive_table = Equality.equality list * EqualitySet.t +type active_table = Equality.equality list * Indexing.Index.t +type new_proof = + Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv +type result = + | ParamodulationFailure of string * active_table * passive_table + | ParamodulationSuccess of new_proof * active_table * passive_table ;; - -let size_of_passive ((_, ns), (_, ps), _) = - (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps) +let list_of_passive (l,s) = l ;; +let make_passive eq_list = + let set = + List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list + in + (*EqualitySet.elements set*) eq_list, set (* see applys.ma *) +;; +let make_empty_active () = [], Indexing.empty ;; +let make_active eq_list = + eq_list, List.fold_left Indexing.index Indexing.empty eq_list +;; -let size_of_active (active_list, _) = - List.length active_list +let size_of_passive (passive_list, _) = List.length passive_list;; +let size_of_active (active_list, _) = List.length active_list;; +let passive_is_empty = function + | [], s when EqualitySet.is_empty s -> true + | [], s -> assert false (* the set and the list should be in sync *) + | _ -> false ;; -let age_factor = 0.01;; +type goals = Equality.goal list * Equality.goal list -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 no_more_passive_goals g = match g with | _,[] -> true | _ -> false;; + -(* -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 -;; -*) +let age_factor = 0.01;; (** 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 g 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 + match (List.rev goals) with goal::_ -> goal | _ -> assert false in +*) + let pos_list, pos_set = 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 - 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) -> + let skip_giant pos_list pos_set = + match pos_list with + | (hd:EqualitySet.elt)::tl -> + let w,_,_,_,_ = Equality.open_equality hd in + if w < 30 then + hd, (tl, EqualitySet.remove hd pos_set) + else +(* + (prerr_endline + ("+++ skipping giant of size "^string_of_int w^" +++"); +*) + select env g (tl@[hd],pos_set) + | _ -> assert false + in + skip_giant pos_list pos_set) + +(* + let rec skip_giant pos_list pos_set = + match pos_list with + | (hd:EqualitySet.elt)::tl -> + let w,_,_,_,_ = Equality.open_equality hd in + let pos_set = EqualitySet.remove hd pos_set in + if w < 30 then + hd, (tl, pos_set) + else + (prerr_endline + ("+++ skipping giant of size "^string_of_int w^" +++"); + skip_giant tl pos_set) + | _ -> assert false + in + skip_giant pos_list pos_set) + +*) +(* + | _ when (!symbols_counter > 0) -> (symbols_counter := !symbols_counter - 1; let cardinality map = - TermMap.fold (fun k v res -> res + v) map 0 + Utils.TermMap.fold (fun k v res -> res + v) map 0 in let symbols = let _, _, term = goal in - symbols_of_term term + Utils.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 + if Utils.TermMap.mem k symbols then + let c = Utils.TermMap.find k symbols in let c1 = abs (c - v) in let c2 = v - c1 in r1 + c2, r2 + c1 @@ -267,7 +220,7 @@ let rec select env goals passive (active, _) = in let f equality (i, e) = let common, others = - TermMap.fold foldfun (symbols_of_equality equality) (0, 0) + Utils.TermMap.fold foldfun (symbols_of_equality equality) (0, 0) in let c = others + (abs (common - card)) in if c < i then (c, equality) @@ -276,84 +229,71 @@ let rec select env goals passive (active, _) = let e1 = EqualitySet.min_elt pos_set in let initial = let common, others = - TermMap.fold foldfun (symbols_of_equality e1) (0, 0) + Utils.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) - ) + current, + (remove current pos_list, EqualitySet.remove current pos_set)) +*) | _ -> 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 my_min e1 e2 = + let w1,_,_,_,_ = Equality.open_equality e1 in + let w2,_,_,_,_ = Equality.open_equality e2 in + if w1 < w2 then e1 else e2 + in + let rec my_min_elt min = function + | [] -> min + | hd::tl -> my_min_elt (my_min hd min) tl + in +(* let current = EqualitySet.min_elt pos_set in *) + let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in + current,(remove current pos_list, EqualitySet.remove current pos_set) ;; -(* 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 - in - let table = - List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos +let filter_dependent bag passive id = + let pos_list, pos_set = passive in + let passive,no_pruned = + List.fold_right + (fun eq ((list,set),no) -> + if Equality.depend bag eq id then + (list, EqualitySet.remove eq set), no + 1 + else + (eq::list, set), no) + pos_list (([],pos_set),0) in - (neg, set_of neg), - (pos, set_of pos), - table -;; - - -let make_active () = - [], Indexing.empty +(* + if no_pruned > 0 then + prerr_endline ("+++ pruning "^ string_of_int no_pruned ^" passives +++"); +*) + passive ;; -(* 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 preferred = + let pos_list, pos_set = 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 - in + let pos = List.filter (ok pos_set) new_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 + let pos_head, pos_tail = + List.partition + (fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred) + pos + in + pos_head @ pos_list @ pos_tail, add pos_set pos ;; - +(* 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 = @@ -362,69 +302,26 @@ let prune_passive howmany (active, _) passive = in let in_weight = round (howmany *. ratio /. (ratio +. 1.)) and in_age = round (howmany /. (ratio +. 1.)) in - debug_print + Utils.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 +335,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,453 +342,327 @@ 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 bag eq_uri 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); + (ignore(Indexing.check_target bag c current "infer1"); + ignore(List.map (function current -> Indexing.check_target bag c current "infer2") active_list)); + let new_pos = + let maxm, copy_of_current = Equality.fix_metas bag !maxmeta current in 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 + let active_table = Indexing.index active_table copy_of_current in +(* let _ = <:start> in *) + let maxm, res = + Indexing.superposition_right bag eq_uri !maxmeta env active_table current + in +(* let _ = <:stop> in *) + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target bag c current "sup0") res); + maxmeta := maxm; + let rec infer_positive table = function + | [] -> [] + | equality::tl -> + let maxm, res = + Indexing.superposition_right bag + ~subterms_only:true eq_uri !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 bag 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 _ = <:start> in *) + let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in +(* let _ = <:stop> in *) + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target bag 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 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_subsumption env active_table eq = + let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in + 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 _ -> 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') -> + let rc = check_subsumed b t1 t2 in + if rc then + true, true + else if h1 = h2 then + (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) + else + false, subsumption_used + | _ -> false, subsumption_used + in + fst (aux false (true,false) left right) ;; - (** simplifies current using active and passive *) -let forward_simplify env (sign, current) ?passive (active_list, active_table) = +let forward_simplify bag eq_uri env current (active_list, active_table) = let _, context, _ = env in - 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 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 + Indexing.demodulation_equality bag eq_uri !maxmeta env table 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 - ) - else - Some (sign, newcurrent) + if Equality.is_identity env newcurrent then None else Some newcurrent in - let res = + let demod current = if Utils.debug_metas then - ignore (Indexing.check_target context current "demod0"); + ignore (Indexing.check_target bag 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); - match res with - | None -> None - | Some (sign, newcurrent) -> - match passive_table with - | None -> res - | Some passive_table -> demodulate passive_table newcurrent - in + if Utils.debug_metas then + ignore ((function None -> () | Some x -> + ignore (Indexing.check_target bag context x "demod1");()) res); + res + 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) -> - if Indexing.in_index active_table c then + | Some c -> + if Indexing.in_index active_table c || + check_for_deep_subsumption env active_table c + then None - else - match passive_table with - | 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 - 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 + else + res ;; -type fs_time_info_t = { - mutable build_all: float; - mutable demodulate: float; - mutable subsumption: float; -};; - -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 bag eq_uri env new_pos 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 bag c current "forward new pos") new_pos;) end; - let t1 = Unix.gettimeofday () in - let active_list, active_table = active in - 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 t2 = Unix.gettimeofday () in - fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1); - - let demodulate sign table target = + let demodulate table target = let newmeta, newtarget = - Indexing.demodulation_equality !maxmeta env table sign target in + Indexing.demodulation_equality bag eq_uri !maxmeta env table target + in maxmeta := newmeta; 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 *) - in - - let t2 = Unix.gettimeofday () in - fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1); - + (* we could also demodulate using passive. Currently we don't *) + let new_pos = List.map (demodulate active_table) new_pos in let new_pos_set = List.fold_left (fun s e -> - if not (Inference.is_identity env e) then - if EqualitySet.mem e s then s - else EqualitySet.add e s + if not (Equality.is_identity env e) then + EqualitySet.add e s else s) EqualitySet.empty new_pos in let new_pos = EqualitySet.elements new_pos_set in - let subs = - match passive_table with - | None -> - (fun e -> not (fst (Indexing.subsumption env active_table e))) - | Some passive_table -> - (fun e -> not ((fst (Indexing.subsumption env active_table e)) || - (fst (Indexing.subsumption env passive_table e)))) - in -(* 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 -> - (fun e -> not (Indexing.in_index active_table e)) - | Some passive_table -> - (fun e -> - 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) + let subs e = Indexing.subsumption env active_table e = None in + let is_duplicate e = not (Indexing.in_index active_table e) in + List.filter subs (List.filter is_duplicate new_pos) +;; + + +(** simplifies a goal with equalities in active and passive *) +let rec simplify_goal bag env goal (active_list, active_table) = + let demodulate table goal = Indexing.demodulation_goal bag env table goal in + let changed, goal = demodulate active_table goal in + changed, + if not changed then + goal + else + snd (simplify_goal bag env goal (active_list, active_table)) +;; + + +let simplify_goals bag env goals active = + let a_goals, p_goals = goals in + let p_goals = List.map (fun g -> snd (simplify_goal bag env g active)) p_goals in + let a_goals = List.map (fun g -> snd (simplify_goal bag env g active)) a_goals in + a_goals, p_goals ;; (** simplifies active usign new *) -let backward_simplify_active env new_pos new_table min_weight active = +let backward_simplify_active + bag eq_uri 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 bag eq_uri env 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 id_of_eq eq = + let _, _, _, _,id = Equality.open_equality eq in id in - let active, newa = + let ((active1,pruned),tbl), newa = List.fold_right - (fun (s, eq) (res, tbl) -> - if List.mem (s, eq) res then - res, tbl - else if (is_identity env eq) || (find eq res) then ( - res, tbl + (fun eq ((res,pruned), tbl) -> + if List.mem eq res then + (res, (id_of_eq eq)::pruned),tbl + else if (Equality.is_identity env eq) || (find eq res) then ( + (res, (id_of_eq eq)::pruned),tbl ) else - (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) - active_list ([], Indexing.empty), + (eq::res,pruned), Indexing.index tbl eq) + active_list (([],pruned), 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, Some newa + | [] -> (active1,tbl), None, pruned + | _ -> (active1,tbl), Some newa, pruned ;; (** 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 +let backward_simplify_passive + bag eq_uri env new_pos new_table min_weight passive += + let (pl, ps), passive_table = passive in + let f equality (resl, ress, newn) = + 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 + match + forward_simplify bag eq_uri env 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 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 backward_simplify env new' ?passive active = - let new_pos, new_table, min_weight = +let build_table equations = 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') - 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 - | Some passive -> - active, passive, newa, None -(* prova - let passive, newp = - backward_simplify_passive env new_pos new_table min_weight passive in - active, passive, newa, newp *) + let ew, _, _, _ , _ = Equality.open_equality e in + e::l, Indexing.index t e, min ew w) + ([], Indexing.empty, 1000000) equations ;; + +let backward_simplify bag eq_uri env new' active = + let new_pos, new_table, min_weight = build_table new' in + let active, newa, pruned = + backward_simplify_active bag eq_uri env new_pos new_table min_weight active + in + active, newa, pruned +;; -let close env new' given = +let close bag eq_uri 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 bag eq_uri 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 ;; -let prova env new' active = +let prova bag eq_uri env new' active = let given = List.filter is_commutative_law (fst active) in let _ = - debug_print + Utils.debug_print (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 - close env new' given + (List.map + (fun e -> Equality.string_of_equality ~env e) + given)))) in + close bag eq_uri env new' given ;; (* returns an estimation of how many equalities in passive can be activated @@ -913,6 +683,9 @@ let make_goals goal = active, passive ;; +let make_goal_set goal = + ([],[goal]) +;; (** initializes the set of theorems *) let make_theorems theorems = @@ -921,9 +694,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,74 +710,17 @@ 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 simplify_theorems bag env theorems ?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 + | Some ((pn, _), (pp, _), pt) -> pn @ pp, Some pt in let a_theorems, p_theorems = theorems in let demodulate table theorem = let newmeta, newthm = - Indexing.demodulation_theorem !maxmeta env table theorem in + Indexing.demodulation_theorem bag !maxmeta env table theorem in maxmeta := newmeta; theorem != newthm, newthm in @@ -1023,19 +742,22 @@ let simplify_theorems env theorems ?passive (active_list, active_table) = ;; -let rec simpl env e others others_simpl = +let rec simpl bag eq_uri 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 -> + if Equality.is_identity env e then t else Indexing.index t e) Indexing.empty active in - let res = forward_simplify env e (active, tbl) in + let res = + forward_simplify bag eq_uri env e (active, tbl) + in match others with | hd::tl -> ( match res with - | None -> simpl env hd tl others_simpl - | Some e -> simpl env hd tl (e::others_simpl) + | None -> simpl bag eq_uri env hd tl others_simpl + | Some e -> simpl bag eq_uri env hd tl (e::others_simpl) ) | [] -> ( match res with @@ -1044,1188 +766,451 @@ let rec simpl env e others others_simpl = ) ;; -let simplify_equalities env equalities = - debug_print +let simplify_equalities bag eq_uri env equalities = + Utils.debug_print (lazy (Printf.sprintf "equalities:\n%s\n" (String.concat "\n" - (List.map string_of_equality equalities)))); - debug_print (lazy "SIMPLYFYING EQUALITIES..."); + (List.map Equality.string_of_equality equalities)))); + Utils.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 bag eq_uri env hd tl []) in - debug_print + Utils.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 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)) ;; - - - -let new_meta metasenv = - let m = CicMkImplicit.new_meta metasenv [] in - incr maxmeta; - while !maxmeta <= m do incr maxmeta done; - !maxmeta + +let pp_goal_set msg goals names = + let active_goals, passive_goals = goals in + prerr_endline ("////" ^ msg); + prerr_endline ("ACTIVE G: " ^ + (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names) + active_goals))); + prerr_endline ("PASSIVE G: " ^ + (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names) + passive_goals))) ;; - -(* 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 +let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = +(* let names = Utils.names_of_context ctx in *) + match ty with + | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] + when LibraryObjects.is_eq_URI uri -> + (let goal_equation = + Equality.mk_equality bag + (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) 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 +(* match Indexing.subsumption env table goal_equation with*) + match Indexing.unification env table goal_equation with + | Some (subst, equality, swapped ) -> +(* + prerr_endline + ("GOAL SUBSUMED IS: "^Equality.string_of_equality goal_equation ~env); + prerr_endline + ("GOAL IS SUBSUMED BY: "^Equality.string_of_equality equality ~env); + prerr_endline ("SUBST:"^Subst.ppsubst ~names subst); +*) + let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in + let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in + let p = + if swapped then + Equality.symmetric bag eq_ty l id uri m + else + p 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 + Some (goalproof, p, id, subst, cicmenv) + | None -> None) + | _ -> None ;; - -(* 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 find_all_subsumed bag env table (goalproof,menv,ty) = + match ty with + | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] + when LibraryObjects.is_eq_URI uri -> + let goal_equation = + Equality.mk_equality bag + (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) + in + List.map + (fun (subst, equality, swapped ) -> + let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in + let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in + let p = + if swapped then + Equality.symmetric bag eq_ty l id uri m + else + p + in (goalproof, p, id, subst, cicmenv)) + (Indexing.unification_all env table goal_equation) + | _ -> assert false ;; -let is_meta_closed goals = - List.for_all (fun (_, _, g) -> CicUtil.is_meta_closed g) goals +let check_if_goal_is_identity env = function + | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) + when left = right && LibraryObjects.is_eq_URI uri -> + let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in + Some (goalproof, reflproof, 0, Subst.empty_subst,m) + | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) + when LibraryObjects.is_eq_URI uri -> + (let _,context,_ = env in + try + let s,m,_ = + Founif.unification m m context left right CicUniv.empty_ugraph + in + let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in + let m = Subst.apply_subst_metasenv s m in + Some (goalproof, reflproof, 0, s,m) + with _ -> None) + | _ -> None +;; + +let rec check goal = function + | [] -> None + | f::tl -> + match f goal with + | None -> check goal tl + | (Some p) as ok -> ok ;; - - -(* 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]) - ) + +let simplify_goal_set bag env goals active = + let active_goals, passive_goals = goals in + let find (_,_,g) where = + List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where 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 + (* prova:tengo le passive semplificate + let passive_goals = + List.map (fun g -> snd (simplify_goal env g active)) passive_goals + in *) + List.fold_left + (fun (acc_a,acc_p) goal -> + match simplify_goal bag env goal active with + | changed, g -> + if changed then + if find g acc_p then acc_a,acc_p else acc_a,g::acc_p + else + if find g acc_a then acc_a,acc_p else g::acc_a,acc_p) + ([],passive_goals) active_goals ;; +let check_if_goals_set_is_solved bag env active goals = + let active_goals, passive_goals = goals in + List.fold_left + (fun proof goal -> + match proof with + | Some p -> proof + | None -> + check goal [ + check_if_goal_is_identity env; + check_if_goal_is_subsumed bag env (snd active)]) +(* provare active and passive?*) + None active_goals +;; +let infer_goal_set bag env active goals = + let active_goals, passive_goals = goals in + let rec aux = function + | [] -> active_goals, [] + | hd::tl -> + let changed,selected = simplify_goal bag env hd active in (* -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;; + if changed then + prerr_endline ("--------------- goal semplificato"); *) - - -(* -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))) + let (_,_,t1) = selected in + let already_in = + List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) + active_goals + in + if already_in then + aux tl + else + let passive_goals = tl in + let new_passive_goals = + if Utils.metas_of_term t1 = [] then passive_goals + else + let newmaxmeta,new' = + Indexing.superposition_left bag env (snd active) selected + !maxmeta + in + maxmeta := newmaxmeta; + passive_goals @ new' 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 + selected::active_goals, new_passive_goals + in + aux passive_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 infer_goal_set_with_current bag env current goals active = + let active_goals, passive_goals = simplify_goal_set bag env goals active in + let l,table,_ = build_table [current] in + active_goals, + List.fold_left + (fun acc g -> + let newmaxmeta, new' = Indexing.superposition_left bag env table g !maxmeta in + maxmeta := newmaxmeta; + acc @ new') + passive_goals active_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)) +let ids_of_goal g = + let p,_,_ = g in + let ids = List.map (fun _,_,i,_,_ -> i) p in + ids ;; - -(* 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 ids_of_goal_set (ga,gp) = + List.flatten (List.map ids_of_goal ga) @ + List.flatten (List.map ids_of_goal gp) ;; - -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) +let size_of_goal_set_a (l,_) = List.length l;; +let size_of_goal_set_p (_,l) = List.length l;; + +let pp_goals label goals context = + let names = Utils.names_of_context context in + List.iter + (fun _,_,g -> + prerr_endline + (Printf.sprintf "Current goal: %s = %s\n" label (CicPp.pp g names))) + (fst goals); + List.iter + (fun _,_,g -> + prerr_endline + (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))) + (snd goals); ;; +let print_status iterno goals active passive = + prerr_endline + (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)" + iterno (size_of_active active) (size_of_passive passive) + (size_of_goal_set_a goals) (size_of_goal_set_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 +(** given-clause algorithm with full reduction strategy: NEW implementation *) +(* here goals is a set of goals in OR *) +let given_clause + bag eq_uri ((_,context,_) as env) goals passive active + goal_steps saturation_steps max_time += + let initial_time = Unix.gettimeofday () in + let iterations_left iterno = + let now = Unix.gettimeofday () in + let time_left = max_time -. now in + let time_spent_until_now = now -. initial_time in + let iteration_medium_cost = + time_spent_until_now /. (float_of_int iterno) + in + let iterations_left = time_left /. iteration_medium_cost in + int_of_float iterations_left 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) + let rec step goals passive active g_iterno s_iterno = + if g_iterno > goal_steps && s_iterno > saturation_steps then + (ParamodulationFailure ("No more iterations to spend",active,passive)) + else if Unix.gettimeofday () > max_time then + (ParamodulationFailure ("No more time to spend",active,passive)) + else + let _ = + print_status (max g_iterno s_iterno) goals active passive +(* Printf.eprintf ".%!"; *) + in + (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) + let passive = + let selection_estimate = iterations_left (max g_iterno s_iterno) in + let kept = size_of_passive passive in + if kept > selection_estimate then + begin + (*Printf.eprintf "Too many passive equalities: pruning..."; + prune_passive selection_estimate active*) passive + end + else + passive + in + kept_clauses := (size_of_passive passive) + (size_of_active active); + let goals = + if g_iterno < goal_steps then + infer_goal_set bag env active goals + else + goals + in + match check_if_goals_set_is_solved bag env active goals with + | Some p -> + prerr_endline + (Printf.sprintf "\nFound a proof in: %f\n" + (Unix.gettimeofday() -. initial_time)); + ParamodulationSuccess (p,active,passive) + | None -> + (* SELECTION *) + if passive_is_empty passive then + if no_more_passive_goals goals then + ParamodulationFailure + ("No more passive equations/goals",active,passive) + (*maybe this is a success! *) + else + step goals passive active (g_iterno+1) (s_iterno+1) + else + begin + (* COLLECTION OF GARBAGED EQUALITIES *) + if max g_iterno s_iterno mod 40 = 0 then + begin + print_status (max g_iterno s_iterno) goals active passive; + let active = List.map Equality.id_of (fst active) in + let passive = List.map Equality.id_of (fst passive) in + let goal = ids_of_goal_set goals in + Equality.collect bag active passive goal + end; + let res, passive = + if s_iterno < saturation_steps then + let current, passive = select env goals passive in + (* SIMPLIFICATION OF CURRENT *) + prerr_endline + ("Selected : " ^ + Equality.string_of_equality ~env current); + forward_simplify bag eq_uri env current active, passive + else + None, passive in - let active = - match sign with - | Negative -> active - | Positive -> - let t1 = Unix.gettimeofday () in - let active, _, newa, _ = - backward_simplify env ([], [current]) active + match res with + | None -> step goals passive active (g_iterno+1) (s_iterno+1) + | Some current -> + (* GENERATION OF NEW EQUATIONS *) +(* prerr_endline "infer"; *) + let new' = infer bag eq_uri env current active in +(* prerr_endline "infer goal"; *) +(* + match check_if_goals_set_is_solved env active goals with + | Some p -> + prerr_endline + (Printf.sprintf "Found a proof in: %f\n" + (Unix.gettimeofday() -. initial_time)); + ParamodulationSuccess p + | None -> +*) + + let active = + let al, tbl = active in + al @ [current], Indexing.index tbl current + in + let goals = + infer_goal_set_with_current bag env current goals active + in + + (* FORWARD AND BACKWARD SIMPLIFICATION *) +(* prerr_endline "fwd/back simpl"; *) + let rec simplify new' active passive = + let new' = + forward_simplify_new bag eq_uri env new' active + in + let active, newa, pruned = + backward_simplify bag eq_uri env new' active + in + let passive = + List.fold_left (filter_dependent bag) passive pruned 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 + | None -> active, passive, new' + | Some p -> simplify (new' @ p) active passive 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 + let active, passive, new' = + simplify new' active passive in - ParamodulationSuccess (proof, env) - ) -;; - -(** 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 _,context,_ = env in - let ok, goals = activate_goal goals in -(* let theorems = simplify_theorems env theorems ~passive active in *) - if ok then - let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in - let _, _, t = List.hd (snd (List.hd (fst goals))) in - let _ = prerr_endline ("goal activated = " ^ (CicPp.pp t names)) in -(* 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 - ( prerr_endline "esco qui"; - (* - let s = Printf.sprintf "actives:\n%s\n" - (String.concat "\n" - ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) - (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)) - 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 = - prerr_endline ("MAXMETA: " ^ string_of_int !maxmeta ^ - " LOCALMAX: " ^ string_of_int !Indexing.local_max ^ - " #ACTIVES: " ^ string_of_int (size_of_active active) ^ - " #PASSIVES: " ^ string_of_int (size_of_passive passive)); -(* - if (size_of_active active) mod 50 = 0 then - (let s = Printf.sprintf "actives:\n%s\n" - (String.concat "\n" - ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) - (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); *) - let time1 = Unix.gettimeofday () in - let (_,context,_) = env 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 +(* prerr_endline "simpl goal with new"; *) + let goals = + let a,b,_ = build_table new' in +(* let _ = <:start> in *) + let rc = simplify_goal_set bag env goals (a,b) in +(* let _ = <:stop> in *) + rc + in + let passive = add_to_passive passive new' [] in + step goals passive active (g_iterno+1) (s_iterno+1) + end 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_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 time1 = Unix.gettimeofday () in - let res = forward_simplify env (sign, current) ~passive active in - let time2 = Unix.gettimeofday () in - forward_simpl_time := !forward_simpl_time +. (time2 -. time1); - match res with - | None -> - (* weight_age_counter := !weight_age_counter + 1; *) - given_clause_fullred dbd env goals theorems passive active - | Some (sign, current) -> - if (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 _ = - 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 - 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 - 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 - in - let active, passive, new' = simplify new' active passive in -(* pessima prova - let new1 = prova env new' active in - let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in - let _ = - match new1 with - | neg, pos -> - debug_print - (lazy - (Printf.sprintf "new1:\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 -end prova *) - 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 "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))))) - 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) - ) + step goals passive active 1 1 ;; - -let rec saturate_equations env goal accept_fun passive active = +let rec saturate_equations bag eq_uri 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 ([goal],[]) passive in + let res = forward_simplify bag eq_uri env current 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 + saturate_equations bag eq_uri env goal accept_fun passive active + | Some current -> + Utils.debug_print (lazy (Printf.sprintf "selected: %s" + (Equality.string_of_equality ~env current))); + let new' = infer bag eq_uri 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 + (* alla fine new' contiene anche le attive semplificate! + * quindi le aggiungo alle passive insieme alle new *) let rec simplify new' active passive = - let new' = forward_simplify_new env new' ~passive active in - let active, passive, newa, retained = - 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 + let new' = forward_simplify_new bag eq_uri env new' active in + let active, newa, pruned = + backward_simplify bag eq_uri env new' active in + let passive = + List.fold_left (filter_dependent bag) passive pruned in + match newa with + | None -> active, passive, new' + | Some p -> simplify (new' @ p) active passive in let active, passive, new' = simplify new' active passive in let _ = - debug_print + Utils.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)))))) + (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))))) + Utils.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 passive = add_to_passive passive new' in - saturate_equations env goal accept_fun passive active + let new' = List.filter accept_fun new' in + let passive = add_to_passive passive new' [] in + saturate_equations bag eq_uri env goal accept_fun passive active ;; - - - -let main dbd full 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 _, metasenv, meta_proof, _ = proof in - let _, context, goal = CicUtil.lookup_meta goal' metasenv in - let eq_indexes, equalities, maxm = find_equalities context proof 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 - 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 - 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 env = (metasenv, context, ugraph) 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 - (Printf.sprintf - "Theorems:\n-------------------------------------\n%s\n" - (String.concat "\n" - (List.map - (fun (t, ty, _) -> - Printf.sprintf - "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) - (fst theorems))))) - in - (*try*) - let goal = Inference.BasicProof new_meta_goal, [], goal in - let equalities = simplify_equalities env - (equalities@library_equalities) in - let active = make_active () in - let passive = make_passive [] equalities in - 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) - 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, 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 - apply the "apply" tactic to proof and status - *) - let names = names_of_context context in - print_endline (PP.pp proof names); - let newmetasenv = - List.fold_left - (fun m (_, _, _, menv) -> m @ menv) metasenv equalities - in - let _ = - (*try*) - let ty, ug = - CicTypeChecker.type_of_aux' newmetasenv context proof ugraph - in - print_endline (string_of_float (finish -. start)); - Printf.printf - "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" - (CicPp.pp type_of_goal names) (CicPp.pp ty names) - (string_of_bool - (fst (CicReduction.are_convertible - context type_of_goal ty ug))); - (*with e -> - Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e); - Printf.printf "MAXMETA USED: %d\n" !maxmeta; - print_endline (string_of_float (finish -. start));*) - in - () - - | ParamodulationSuccess (None, env) -> - Printf.printf "Success, but no proof?!?\n\n" - in - if Utils.time then - begin - prerr_endline - ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ - "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 -(* - 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,384 +1224,428 @@ let reset_refs () = passive_maintainance_time := 0.; derived_clauses := 0; kept_clauses := 0; - Indexing.beta_expand_time := 0.; - Inference.metas_of_proof_time := 0.; ;; -let saturate - dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = - let module C = Cic in - reset_refs (); - Indexing.init_index (); - maxdepth := depth; - maxwidth := width; - 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 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 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 = simplify_equalities env (equalities@library_equalities) 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, [] - 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 - let _ = - debug_print - (lazy - (Printf.sprintf - "Theorems:\n-------------------------------------\n%s\n" - (String.concat "\n" - (List.map - (fun (t, ty, _) -> - Printf.sprintf - "Term: %s, type: %s" - (CicPp.ppterm t) (CicPp.ppterm ty)) - (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 [] equalities in - let start = Unix.gettimeofday () 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, env) -> - debug_print (lazy "OK, found a proof!"); - let proof = Inference.build_proof_term proof in - let names = names_of_context context in - let newmetasenv = - let i1 = - match new_meta_goal with - | C.Meta (i, _) -> i | _ -> assert false - in - List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv - in - 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 - in - let real_proof = - ProofEngineReduction.replace - ~equality:equality_for_replace - ~what:[goal'] ~with_what:[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))); - ((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")) - 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 - | _ -> - raise (ProofEngineTypes.Fail (lazy "NO proof found")) +let eq_of_goal = function + | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri -> + uri + | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) ;; -(* dummy function called within matita to trigger linkage *) -let init () = ();; - - -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 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 = (* 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 "RETR: 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 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 - 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 []) +let eq_and_ty_of_goal = function + | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri -> + uri,t + | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) +;; + +(* fix proof takes in input a term and try to build a metasenv for it *) + +let fix_proof metasenv context all_implicits p = + let rec aux metasenv n p = + match p with + | Cic.Meta (i,_) -> + if all_implicits then + metasenv,Cic.Implicit None + else + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context 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))) + let meta = CicSubstitution.lift n (Cic.Meta (i,irl)) in + let metasenv = + try + let _ = CicUtil.lookup_meta i metasenv in metasenv + with CicUtil.Meta_not_found _ -> + prerr_endline ("not found: "^(string_of_int i)); + let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in + (i,context,Cic.Meta(j,irl))::metasenv + in + metasenv,meta + | Cic.Appl l -> + let metasenv,l= + List.fold_right + (fun a (metasenv,l) -> + let metasenv,a' = aux metasenv n a in + metasenv,a'::l) + l (metasenv,[]) + in metasenv,Cic.Appl l + | Cic.Lambda(name,s,t) -> + let metasenv,s = aux metasenv n s in + let metasenv,t = aux metasenv (n+1) t in + metasenv,Cic.Lambda(name,s,t) + | Cic.Prod(name,s,t) -> + let metasenv,s = aux metasenv n s in + let metasenv,t = aux metasenv (n+1) t in + metasenv,Cic.Prod(name,s,t) + | Cic.LetIn(name,s,t) -> + let metasenv,s = aux metasenv n s in + let metasenv,t = aux metasenv (n+1) t in + metasenv,Cic.LetIn(name,s,t) + | Cic.Const(uri,ens) -> + let metasenv,ens = + List.fold_right + (fun (v,a) (metasenv,ens) -> + let metasenv,a' = aux metasenv n a in + metasenv,(v,a')::ens) + ens (metasenv,[]) + in + metasenv,Cic.Const(uri,ens) + | t -> metasenv,t + in + aux metasenv 0 p ;; +let fix_metasenv metasenv = + List.fold_left + (fun m (i,c,t) -> + let m,t = fix_proof m c false t in + let m = List.filter (fun (j,_,_) -> j<>i) m in + (i,c,t)::m) + metasenv metasenv +;; + +(* status: input proof status + * goalproof: forward steps on goal + * newproof: backward steps + * subsumption_id: the equation used if goal is closed by subsumption + * (0 if not closed by subsumption) (DEBUGGING: can be safely removed) + * subsumption_subst: subst to make newproof and goalproof match + * proof_menv: final metasenv + *) -let main_demod_equalities 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 _, metasenv, meta_proof, _ = proof in - let _, context, goal = CicUtil.lookup_meta goal' metasenv in - let eq_indexes, equalities, maxm = find_equalities context proof in - let lib_eq_uris, library_equalities, maxm = - find_library_equalities dbd context (proof, goal') (maxm+2) +let build_proof + bag status + goalproof newproof subsumption_id subsumption_subst proof_menv += + if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA" + else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv); + let proof, goalno = status in + let uri, metasenv, meta_proof, term_to_prove, attrs = proof in + let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in + let eq_uri = eq_of_goal type_of_goal in + let names = Utils.names_of_context context in + prerr_endline "Proof:"; + prerr_endline + (Equality.pp_proof bag names goalproof newproof subsumption_subst + subsumption_id type_of_goal); +(* + prerr_endline ("max weight: " ^ + (string_of_int (Equality.max_weight goalproof newproof))); +*) + (* generation of the CIC proof *) + (* let metasenv' = List.filter (fun i,_,_ -> i<>goalno) metasenv in *) + let side_effects = + List.filter (fun i -> i <> goalno) + (ProofEngineHelpers.compare_metasenvs + ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in + let goal_proof, side_effects_t = + let initial = (* Equality.add_subst subsumption_subst*) newproof in + Equality.build_goal_proof bag + eq_uri goalproof initial type_of_goal side_effects + context proof_menv 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 - debug_print - (lazy - (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n" - (CicPp.ppterm ty))); - Cic.Meta (maxm+1, irl), - (maxm+1, context, ty)::metasenv, - ty +(* Equality.draw_proof bag names goalproof newproof subsumption_id; *) + let goal_proof = Subst.apply_subst subsumption_subst goal_proof in + let real_menv = fix_metasenv (proof_menv@metasenv) in + let real_menv,goal_proof = + fix_proof real_menv context false goal_proof in +(* + let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in + (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *) +*) + let pp_error goal_proof names error exn = + prerr_endline "THE PROOF DOES NOT TYPECHECK! "; + prerr_endline (CicPp.pp goal_proof names); + prerr_endline "THE PROOF DOES NOT TYPECHECK!"; + prerr_endline error; + prerr_endline "THE PROOF DOES NOT TYPECHECK! "; + raise exn in - let env = (metasenv, context, ugraph) in - (*try*) - let goal = Inference.BasicProof new_meta_goal, [], goal in - let equalities = simplify_equalities env (equalities@library_equalities) in - let active = make_active () in - let passive = make_passive [] equalities in - 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)); - print_endline "--------------------------------------------------"; - print_endline "GO!"; - start_time := Unix.gettimeofday (); - if !time_limit < 1. then time_limit := 60.; - let ra, rp = - saturate_equations env goal (fun e -> true) passive active - in + let goal_proof,goal_ty,real_menv,_ = + (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *) + try + prerr_endline (CicPp.ppterm goal_proof); + CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph + with + | CicRefine.RefineFailure s + | CicRefine.Uncertain s + | CicRefine.AssertFailure s as exn -> + pp_error goal_proof names (Lazy.force s) exn + | CicUtil.Meta_not_found i as exn -> + pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn + | Invalid_argument "list_fold_left2" as exn -> + pp_error goal_proof names "Invalid_argument: list_fold_left2" exn + in + let subst_side_effects,real_menv,_ = + try + CicUnification.fo_unif_subst [] context real_menv + goal_ty type_of_goal CicUniv.empty_ugraph + with + | CicUnification.UnificationFailure s + | CicUnification.Uncertain s + | CicUnification.AssertFailure s -> assert false + (* fail "Maybe the local context of metas in the goal was not an IRL" s *) + in + prerr_endline "+++++++++++++ FINE UNIF"; + let final_subst = + (goalno,(context,goal_proof,type_of_goal))::subst_side_effects + in +(* + let metas_of_proof = Utils.metas_of_term goal_proof in +*) + let proof, real_metasenv = + ProofEngineHelpers.subst_meta_and_metasenv_in_proof + proof goalno (CicMetaSubst.apply_subst final_subst) + (List.filter (fun i,_,_ -> i<>goalno ) real_menv) + in + let open_goals = + (ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:real_metasenv) in +(* + let open_goals = + List.map (fun i,_,_ -> i) real_metasenv in +*) + final_subst, proof, open_goals - let initial = - List.fold_left (fun s e -> EqualitySet.add e s) - EqualitySet.empty equalities - in - let addfun s e = - if not (EqualitySet.mem e initial) then EqualitySet.add e s else s - in - let passive = - match rp with - | (n, _), (p, _), _ -> - EqualitySet.elements (List.fold_left addfun EqualitySet.empty p) - in - let active = - let l = List.map snd (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 (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)); - print_newline (); (* - with e -> - debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e))) + + let metas_still_open_in_proof = Utils.metas_of_term goal_proof in + (* prerr_endline (CicPp.pp goal_proof names); *) + let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in + let side_effects_t = + List.map (Subst.apply_subst subsumption_subst) side_effects_t + in + (* replacing fake mets with real ones *) + (* prerr_endline "replacing metas..."; *) + let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in + if proof_menv = [] then prerr_endline "VUOTA"; + CicMetaSubst.ppmetasenv [] proof_menv; + let what, with_what = + List.fold_left + (fun (acc1,acc2) i -> + (Cic.Meta(i,[]))::acc1, (Cic.Implicit None)::acc2) + ([],[]) + metas_still_open_in_proof +(* + (List.filter + (fun (i,_,_) -> + List.mem i metas_still_open_in_proof + (*&& not(List.mem i metas_still_open_in_goal)*)) + proof_menv) +*) + in + let goal_proof_menv = + List.filter + (fun (i,_,_) -> List.mem i metas_still_open_in_proof) + proof_menv + in + let replace where = + (* we need this fake equality since the metas of the hypothesis may be + * with a real local context *) + ProofEngineReduction.replace_lifting + ~equality:(fun x y -> + match x,y with Cic.Meta(i,_),Cic.Meta(j,_) -> i=j | _-> false) + ~what ~with_what ~where + in + let goal_proof = replace goal_proof in + (* ok per le meta libere... ma per quelle che c'erano e sono rimaste? + * what mi pare buono, sostituisce solo le meta farlocche *) + let side_effects_t = List.map replace side_effects_t in + let free_metas = + List.filter (fun i -> i <> goalno) + (ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv) + in + (* prerr_endline + * ("freemetas: " ^ + * String.concat "," (List.map string_of_int free_metas) ); *) + (* check/refine/... build the new proof *) + let replaced_goal = + ProofEngineReduction.replace + ~what:side_effects ~with_what:side_effects_t + ~equality:(fun i t -> match t with Cic.Meta(j,_)->j=i|_->false) + ~where:type_of_goal + in + let goal_proof,goal_ty,real_menv,_ = + prerr_endline "parte la refine"; + try + CicRefine.type_of_aux' metasenv context goal_proof + CicUniv.empty_ugraph + with + | CicUtil.Meta_not_found _ + | CicRefine.RefineFailure _ + | CicRefine.Uncertain _ + | CicRefine.AssertFailure _ + | Invalid_argument "list_fold_left2" as exn -> + prerr_endline "THE PROOF DOES NOT TYPECHECK!"; + prerr_endline (CicPp.pp goal_proof names); + prerr_endline "THE PROOF DOES NOT TYPECHECK!"; + raise exn + in + prerr_endline "+++++++++++++ METASENV"; + prerr_endline + (CicMetaSubst.ppmetasenv [] real_menv); + let subst_side_effects,real_menv,_ = +(* + prerr_endline ("XX type_of_goal " ^ CicPp.ppterm type_of_goal); + prerr_endline ("XX replaced_goal " ^ CicPp.ppterm replaced_goal); + prerr_endline ("XX metasenv " ^ + CicMetaSubst.ppmetasenv [] (metasenv @ free_metas_menv)); +*) + try + CicUnification.fo_unif_subst [] context real_menv + goal_ty type_of_goal CicUniv.empty_ugraph + with + | CicUnification.UnificationFailure s + | CicUnification.Uncertain s + | CicUnification.AssertFailure s -> assert false +(* fail "Maybe the local context of metas in the goal was not an IRL" s *) + in + let final_subst = + (goalno,(context,goal_proof,type_of_goal))::subst_side_effects + in +(* + let metas_of_proof = Utils.metas_of_term goal_proof in +*) + let proof, real_metasenv = + ProofEngineHelpers.subst_meta_and_metasenv_in_proof + proof goalno (CicMetaSubst.apply_subst final_subst) + (List.filter (fun i,_,_ -> i<>goalno ) real_menv) + in + let open_goals = + List.map (fun i,_,_ -> i) real_metasenv in + +(* + HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof) + in *) +(* + match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] + in +*) +(* + Printf.eprintf + "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" + (String.concat ", " (List.map string_of_int open_goals)) + (CicMetaSubst.ppmetasenv [] metasenv) + (CicMetaSubst.ppmetasenv [] real_metasenv); +*) + final_subst, proof, open_goals +;; +*) + +(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *) + +(* exported functions *) + +let pump_actives context bag maxm active passive saturation_steps max_time = + reset_refs(); + maxmeta := maxm; +(* + let max_l l = + List.fold_left + (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in + List.fold_left (fun acc (i,_,_) -> max i acc) acc menv) + 0 l in *) +(* let active_l = fst active in *) +(* let passive_l = fst passive in *) +(* let ma = max_l active_l in *) +(* let mp = max_l passive_l in *) + match LibraryObjects.eq_URI () with + | None -> active, passive, !maxmeta + | Some eq_uri -> + let env = [],context,CicUniv.empty_ugraph in + (match + given_clause bag eq_uri env ([],[]) + passive active 0 saturation_steps max_time + with + | ParamodulationFailure (_,a,p) -> + a, p, !maxmeta + | ParamodulationSuccess _ -> + assert false) ;; -let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = - let module I = Inference in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let eq_indexes, equalities, maxm = I.find_equalities context proof in - let lib_eq_uris, library_equalities, maxm = - I.find_library_equalities dbd context (proof, goal) (maxm+2) in - if library_equalities = [] then prerr_endline "VUOTA!!!"; - 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 env = (metasenv, context, CicUniv.empty_ugraph) in - let equalities = simplify_equalities env (equalities@library_equalities) in +let all_subsumed bag maxm status active passive = + maxmeta := maxm; + let proof, goalno = status in + let uri, metasenv, meta_proof, term_to_prove, attrs = proof in + let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in + let env = metasenv,context,CicUniv.empty_ugraph in + let cleaned_goal = Utils.remove_local_context type_of_goal in + let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in + prerr_endline (string_of_int (List.length (fst active))); + (* we simplify using both actives passives *) let table = List.fold_left - (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 + (fun (l,tbl) eq -> eq::l,(Indexing.index tbl eq)) + active (list_of_passive passive) in + let _,goal = simplify_goal bag env goal table in + let (_,_,ty) = goal in + prerr_endline (CicPp.ppterm ty); + let subsumed = find_all_subsumed bag env (snd table) goal in + let subsumed_or_id = + match (check_if_goal_is_identity env goal) with + None -> subsumed + | Some id -> id::subsumed in + let res = + List.map + (fun + (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) -> + build_proof bag + status goalproof newproof subsumption_id subsumption_subst proof_menv) + subsumed_or_id in + res, !maxmeta + + +let given_clause + bag maxm status active passive goal_steps saturation_steps max_time += + reset_refs(); + maxmeta := maxm; + let active_l = fst active in +(* + let max_l l = + List.fold_left + (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in + List.fold_left (fun acc (i,_,_) -> max i acc) acc menv) + 0 l in - if newmeta != maxm then - begin - let opengoal = Cic.Meta(maxm,irl) in - let proofterm = - Inference.build_proof_term ~noproof:opengoal newproof in - let extended_metasenv = (maxm,context,newty)::metasenv in - let extended_status = - (curi,extended_metasenv,pbo,pty),goal in - let (status,newgoals) = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) - extended_status in - (status,maxm::newgoals) - end - else if newty = ty then - raise (ProofEngineTypes.Fail (lazy "no progress")) - else ProofEngineTypes.apply_tactic - (ReductionTactics.simpl_tac ~pattern) - initialstatus + let passive_l = fst passive in + let ma = max_l active_l in + let mp = max_l passive_l in +*) + let proof, goalno = status in + let uri, metasenv, meta_proof, term_to_prove, attrs = proof in + let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in + let eq_uri = eq_of_goal type_of_goal in + let cleaned_goal = Utils.remove_local_context type_of_goal in + Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *) + let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in + let goal = [], metasenv', cleaned_goal in + let env = metasenv,context,CicUniv.empty_ugraph in + prerr_endline ">>>>>> ACTIVES >>>>>>>>"; + List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e)) + active_l; + prerr_endline ">>>>>>>>>>>>>>"; + let goals = make_goal_set goal in + match +(* given_caluse non prende in input maxm ????? *) + given_clause bag eq_uri env goals passive active + goal_steps saturation_steps max_time + with + | ParamodulationFailure (_,a,p) -> + None, a, p, !maxmeta + | ParamodulationSuccess + ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p) -> + let subst, proof, gl = + build_proof bag + status goalproof newproof subsumption_id subsumption_subst proof_menv + in + Some (subst, proof,gl),a,p, !maxmeta ;; -let demodulate_tac ~dbd ~pattern = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern) +let add_to_passive eql passives = + add_to_passive passives eql eql ;; + +