--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* let _profiler = <:profiler<_profiler>>;; *)
+
+(* $Id$ *)
+
+(* set to false to disable paramodulation inside auto_tac *)
+
+let connect_to_auto = true;;
+
+let debug_print = Utils.debug_print;;
+
+(* profiling statistics... *)
+let infer_time = ref 0.;;
+let forward_simpl_time = ref 0.;;
+let forward_simpl_new_time = ref 0.;;
+let backward_simpl_time = ref 0.;;
+let passive_maintainance_time = ref 0.;;
+
+(* limited-resource-strategy related globals *)
+let processed_clauses = ref 0;; (* number of equalities selected so far... *)
+let time_limit = ref 0.;; (* in seconds, settable by the user... *)
+let start_time = ref 0.;; (* time at which the execution started *)
+let elapsed_time = ref 0.;;
+(* let maximal_weight = ref None;; *)
+let maximal_retained_equality = ref None;;
+
+(* equality-selection related globals *)
+let use_fullred = ref true;;
+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;;
+
+(* non-recursive Knuth-Bendix term ordering by default *)
+(* Utils.compare_terms := Utils.rpo;; *)
+(* Utils.compare_terms := Utils.nonrec_kbo;; *)
+(* Utils.compare_terms := Utils.ao;; *)
+
+(* statistics... *)
+let derived_clauses = ref 0;;
+let kept_clauses = ref 0;;
+
+(* index of the greatest Cic.Meta created - TODO: find a better way! *)
+let maxmeta = ref 0;;
+
+(* varbiables controlling the search-space *)
+let maxdepth = ref 3;;
+let maxwidth = ref 3;;
+
+type theorem = Cic.term * Cic.term * Cic.metasenv;;
+
+let symbols_of_equality equality =
+ let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in
+ let m1 = Utils.symbols_of_term left in
+ let m =
+ Utils.TermMap.fold
+ (fun k v res ->
+ try
+ let c = Utils.TermMap.find k res in
+ Utils.TermMap.add k (c+v) res
+ with Not_found ->
+ Utils.TermMap.add k v res)
+ (Utils.symbols_of_term right) m1
+ in
+ m
+;;
+
+(* griggio *)
+module OrderedEquality = struct
+ type t = Equality.equality
+
+ let compare eq1 eq2 =
+ match Equality.meta_convertibility_eq eq1 eq2 with
+ | true -> 0
+ | 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
+ Equality.compare eq1 eq2
+ | res -> res
+end
+
+module EqualitySet = Set.Make(OrderedEquality);;
+
+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 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_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
+;;
+
+type goals = Equality.goal list * Equality.goal list
+
+let no_more_passive_goals g = match g with | _,[] -> true | _ -> false;;
+
+
+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 g passive =
+ processed_clauses := !processed_clauses + 1;
+(*
+ let goal =
+ 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;
+ 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 =
+ Utils.TermMap.fold (fun k v res -> res + v) map 0
+ in
+ let symbols =
+ let _, _, term = goal in
+ Utils.symbols_of_term term
+ in
+ let card = cardinality symbols in
+ let foldfun k v (r1, r2) =
+ 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
+ else
+ r1, r2 + v
+ in
+ let f equality (i, e) =
+ let common, others =
+ Utils.TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
+ in
+ let c = others + (abs (common - card)) in
+ if c < i then (c, equality)
+ else (i, e)
+ in
+ let e1 = EqualitySet.min_elt pos_set in
+ let initial =
+ let common, others =
+ 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
+ current,
+ (remove current pos_list, EqualitySet.remove current pos_set))
+*)
+ | _ ->
+ symbols_counter := !symbols_ratio;
+ 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)
+;;
+
+
+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
+(*
+ if no_pruned > 0 then
+ prerr_endline ("+++ pruning "^ string_of_int no_pruned ^" passives +++");
+*)
+ passive
+;;
+
+
+(* 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 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
+ 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 (pl, ps), tbl = passive in
+ let howmany = float_of_int howmany
+ and ratio = float_of_int !weight_age_ratio in
+ let round v =
+ let t = ceil v in
+ int_of_float (if t -. v < 0.5 then t else v)
+ in
+ let in_weight = round (howmany *. ratio /. (ratio +. 1.))
+ and in_age = round (howmany /. (ratio +. 1.)) in
+ Utils.debug_print
+ (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
+ let counter = ref !symbols_ratio in
+ let rec pickw w ps =
+ if w > 0 then
+ if !counter > 0 then
+ let _ =
+ counter := !counter - 1;
+ 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 ps' = pickw (w-1) (EqualitySet.remove e ps) in
+ EqualitySet.add e ps'
+ else
+ EqualitySet.empty
+ in
+ let ps = pickw in_weight ps in
+ let rec picka w s l =
+ if w > 0 then
+ match l with
+ | [] -> w, s, []
+ | hd::tl when not (EqualitySet.mem hd s) ->
+ let w, s, l = picka (w-1) s tl in
+ w, EqualitySet.add hd s, hd::l
+ | hd::tl ->
+ let w, s, l = picka w s tl in
+ w, s, hd::l
+ else
+ 0, s, l
+ 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);
+ let tbl =
+ EqualitySet.fold
+ (fun e tbl -> Indexing.index tbl e) ps Indexing.empty
+ in
+ (pl, ps), tbl
+;;
+
+
+(** inference of new equalities between current and some in active *)
+let infer bag eq_uri env current (active_list, active_table) =
+ let (_,c,_) = env in
+ if Utils.debug_metas then
+ (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;
+ let active_table = Indexing.index active_table copy_of_current in
+(* let _ = <:start<current contro active>> in *)
+ let maxm, res =
+ Indexing.superposition_right bag eq_uri !maxmeta env active_table current
+ in
+(* let _ = <:stop<current contro active>> 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 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 _ = <:start<active contro current>> in *)
+ let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in
+(* let _ = <:stop<active contro current>> 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_pos);
+ match !maximal_retained_equality with
+ | 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 *)
+ List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
+;;
+
+let check_for_deep_subsumption env active_table eq =
+ let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in
+ 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 bag eq_uri env current (active_list, active_table) =
+ let _, context, _ = env in
+ let demodulate table current =
+ let newmeta, newcurrent =
+ Indexing.demodulation_equality bag eq_uri !maxmeta env table current
+ in
+ maxmeta := newmeta;
+ if Equality.is_identity env newcurrent then None else Some newcurrent
+ in
+ let demod current =
+ if Utils.debug_metas then
+ 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 ->
+ ignore (Indexing.check_target bag context x "demod1");()) res);
+ res
+ in
+ let res = demod current in
+ match res with
+ | None -> None
+ | Some c ->
+ if Indexing.in_index active_table c ||
+ check_for_deep_subsumption env active_table c
+ then
+ None
+ else
+ res
+;;
+
+(** simplifies new using active and passive *)
+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 bag c current "forward new pos")
+ new_pos;)
+ end;
+ let active_list, active_table = active in
+ let demodulate table target =
+ let newmeta, newtarget =
+ Indexing.demodulation_equality bag eq_uri !maxmeta env table target
+ in
+ maxmeta := newmeta;
+ newtarget
+ in
+ (* 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 (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 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
+ bag eq_uri env new_pos new_table min_weight active
+=
+ let active_list, active_table = active in
+ let active_list, newa, pruned =
+ List.fold_right
+ (fun equality (res, newn,pruned) ->
+ let ew, _, _, _,id = Equality.open_equality equality in
+ if ew < min_weight then
+ equality::res, newn,pruned
+ else
+ 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, e::newn, pruned)
+ active_list ([], [],[])
+ in
+ let find eq1 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 ((active1,pruned),tbl), newa =
+ List.fold_right
+ (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
+ (eq::res,pruned), Indexing.index tbl eq)
+ active_list (([],pruned), Indexing.empty),
+ List.fold_right
+ (fun eq p ->
+ if (Equality.is_identity env eq) then p
+ else eq::p)
+ newa []
+ in
+ match newa with
+ | [] -> (active1,tbl), None, pruned
+ | _ -> (active1,tbl), Some newa, pruned
+;;
+
+
+(** simplifies passive using new *)
+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 bag eq_uri env equality (new_pos, new_table)
+ with
+ | None -> resl, EqualitySet.remove equality ress, newn
+ | Some e ->
+ if equality = e then
+ equality::resl, ress, newn
+ else
+ let ress = EqualitySet.remove equality ress in
+ resl, ress, e::newn
+ 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 newp with
+ | [] -> ((pl, ps), passive_table), None
+ | _ -> ((pl, ps), passive_table), Some (newp)
+;;
+
+let build_table equations =
+ List.fold_left
+ (fun (l, t, w) e ->
+ let ew, _, _, _ , _ = Equality.open_equality e in
+ e::l, Indexing.index t e, min ew w)
+ ([], Indexing.empty, 1000000) equations
+;;
+
+
+let backward_simplify 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 bag eq_uri env new' given =
+ let new_pos, new_table, min_weight =
+ List.fold_left
+ (fun (l, t, w) e ->
+ let ew, _, _, _ , _ = Equality.open_equality e in
+ e::l, Indexing.index t e, min ew w)
+ ([], Indexing.empty, 1000000) (snd new')
+ in
+ List.fold_left
+ (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 , _ =
+ 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
+ | _ -> false
+;;
+
+let prova bag eq_uri env new' active =
+ let given = List.filter is_commutative_law (fst active) in
+ let _ =
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "symmetric:\n%s\n"
+ (String.concat "\n"
+ (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
+ within the current time limit *)
+let get_selection_estimate () =
+ elapsed_time := (Unix.gettimeofday ()) -. !start_time;
+ (* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
+ int_of_float (
+ ceil ((float_of_int !processed_clauses) *.
+ ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
+;;
+
+
+(** initializes the set of goals *)
+let make_goals goal =
+ let active = []
+ and passive = [0, [goal]] in
+ active, passive
+;;
+
+let make_goal_set goal =
+ ([],[goal])
+;;
+
+(** initializes the set of theorems *)
+let make_theorems theorems =
+ theorems, []
+;;
+
+
+let activate_goal (active, passive) =
+ if active = [] then
+ match passive with
+ | goal_conj::tl -> true, (goal_conj::active, tl)
+ | [] -> false, (active, passive)
+ else
+ true, (active,passive)
+;;
+
+
+let activate_theorem (active, passive) =
+ match passive with
+ | theorem::tl -> true, (theorem::active, tl)
+ | [] -> false, (active, passive)
+;;
+
+
+
+let simplify_theorems bag env theorems ?passive (active_list, active_table) =
+ let pl, passive_table =
+ match passive with
+ | None -> [], None
+ | 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 bag !maxmeta env table theorem in
+ maxmeta := newmeta;
+ theorem != newthm, newthm
+ in
+ let foldfun table (a, p) theorem =
+ let changed, theorem = demodulate table theorem in
+ if changed then (a, theorem::p) else (theorem::a, p)
+ in
+ let mapfun table theorem = snd (demodulate table theorem) in
+ match passive_table with
+ | None ->
+ let p_theorems = List.map (mapfun active_table) p_theorems in
+ List.fold_left (foldfun active_table) ([], p_theorems) a_theorems
+ | Some passive_table ->
+ let p_theorems = List.map (mapfun active_table) p_theorems in
+ let p_theorems, a_theorems =
+ List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in
+ let p_theorems = List.map (mapfun passive_table) p_theorems in
+ List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
+;;
+
+
+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 ->
+ if Equality.is_identity env e then t else Indexing.index t e)
+ Indexing.empty active
+ in
+ let res =
+ forward_simplify bag eq_uri env e (active, tbl)
+ in
+ match others with
+ | hd::tl -> (
+ match res with
+ | 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
+ | None -> others_simpl
+ | Some e -> e::others_simpl
+ )
+;;
+
+let simplify_equalities bag eq_uri env equalities =
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "equalities:\n%s\n"
+ (String.concat "\n"
+ (List.map Equality.string_of_equality equalities))));
+ Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let res =
+ List.rev (simpl bag eq_uri env hd tl [])
+ in
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "equalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map Equality.string_of_equality res))));
+ res
+;;
+
+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 pp_goal_set msg goals names =
+ let active_goals, passive_goals = goals in
+ debug_print (lazy ("////" ^ msg));
+ debug_print (lazy ("ACTIVE G: " ^
+ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
+ active_goals))));
+ debug_print (lazy ("PASSIVE G: " ^
+ (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
+ passive_goals))))
+;;
+
+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
+(* 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
+ Some (goalproof, p, id, subst, cicmenv)
+ | None -> None)
+ | _ -> None
+;;
+
+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 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
+;;
+
+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
+ (* 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
+(*
+ if changed then
+ prerr_endline ("--------------- goal semplificato");
+*)
+ 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
+ selected::active_goals, new_passive_goals
+ in
+ aux passive_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 ids_of_goal g =
+ let p,_,_ = g in
+ let ids = List.map (fun _,_,i,_,_ -> i) p in
+ ids
+;;
+
+let ids_of_goal_set (ga,gp) =
+ List.flatten (List.map ids_of_goal ga) @
+ List.flatten (List.map ids_of_goal gp)
+;;
+
+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 ->
+ debug_print (lazy
+ (Printf.sprintf "Current goal: %s = %s\n" label (CicPp.pp g names))))
+ (fst goals);
+ List.iter
+ (fun _,_,g ->
+ debug_print (lazy
+ (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))))
+ (snd goals);
+;;
+
+let print_status iterno goals active passive =
+ debug_print (lazy
+ (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 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 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 ->
+ debug_print (lazy
+ (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 *)
+ debug_print (lazy
+ ("Selected : " ^
+ Equality.string_of_equality ~env current));
+ forward_simplify bag eq_uri env current active, passive
+ else
+ None, passive
+ in
+ 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
+ match newa with
+ | None -> active, passive, new'
+ | Some p -> simplify (new' @ p) active passive
+ in
+ let active, passive, new' =
+ simplify new' active passive
+ in
+
+(* prerr_endline "simpl goal with new"; *)
+ let goals =
+ let a,b,_ = build_table new' in
+(* let _ = <:start<simplify_goal_set new>> in *)
+ let rc = simplify_goal_set bag env goals (a,b) in
+(* let _ = <:stop<simplify_goal_set new>> in *)
+ rc
+ in
+ let passive = add_to_passive passive new' [] in
+ step goals passive active (g_iterno+1) (s_iterno+1)
+ end
+ in
+ step goals passive active 1 1
+;;
+
+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 current, passive = select env ([goal],[]) passive in
+ let res = forward_simplify bag eq_uri env current active in
+ match res with
+ | None ->
+ 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 Equality.is_identity env current then active
+ else
+ let al, tbl = active in
+ 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 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 _ =
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "active:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun e -> Equality.string_of_equality ~env e)
+ (fst active)))))
+ in
+ let _ =
+ 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' = 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 default_depth = !maxdepth
+and default_width = !maxwidth;;
+
+let reset_refs () =
+ maxmeta := 0;
+ symbols_counter := 0;
+ weight_age_counter := !weight_age_ratio;
+ processed_clauses := 0;
+ start_time := 0.;
+ elapsed_time := 0.;
+ maximal_retained_equality := None;
+ infer_time := 0.;
+ forward_simpl_time := 0.;
+ forward_simpl_new_time := 0.;
+ backward_simpl_time := 0.;
+ passive_maintainance_time := 0.;
+ derived_clauses := 0;
+ kept_clauses := 0;
+;;
+
+let 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 ")))
+;;
+
+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
+ 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 _ ->
+ debug_print (lazy ("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,ty,t) ->
+ let metasenv,s = aux metasenv n s in
+ let metasenv,ty = aux metasenv n ty in
+ let metasenv,t = aux metasenv (n+1) t in
+ metasenv,Cic.LetIn(name,s,ty,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 build_proof
+ bag status
+ goalproof newproof subsumption_id subsumption_subst proof_menv
+=
+ if proof_menv = [] then debug_print (lazy "+++++++++++++++VUOTA")
+ else debug_print (lazy (CicMetaSubst.ppmetasenv [] proof_menv));
+ let proof, goalno = status in
+ let uri, metasenv, _subst, 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
+ debug_print (lazy "Proof:");
+ debug_print (lazy
+ (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
+(* 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! <begin>";
+ prerr_endline (CicPp.pp goal_proof names);
+ prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+ prerr_endline error;
+ prerr_endline "THE PROOF DOES NOT TYPECHECK! <end>";
+ raise exn
+ in
+ let old_insert_coercions = !CicRefine.insert_coercions in
+ let goal_proof,goal_ty,real_menv,_ =
+ (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
+ try
+ debug_print (lazy (CicPp.ppterm goal_proof));
+ CicRefine.insert_coercions := false;
+ let res =
+ CicRefine.type_of_aux'
+ real_menv context goal_proof CicUniv.empty_ugraph
+ in
+ CicRefine.insert_coercions := old_insert_coercions;
+ res
+ with
+ | CicRefine.RefineFailure s
+ | CicRefine.Uncertain s
+ | CicRefine.AssertFailure s as exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
+ pp_error goal_proof names (Lazy.force s) exn
+ | CicUtil.Meta_not_found i as exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
+ pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn
+ | Invalid_argument "list_fold_left2" as exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
+ pp_error goal_proof names "Invalid_argument: list_fold_left2" exn
+ | exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
+ raise 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
+ Utils.debug_print (lazy "+++++++++++++ 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 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 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 all_subsumed bag maxm status active passive =
+ maxmeta := maxm;
+ let proof, goalno = status in
+ let uri, metasenv, _subst, 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
+ debug_print (lazy (string_of_int (List.length (fst active))));
+ (* we simplify using both actives passives *)
+ let table =
+ List.fold_left
+ (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
+ debug_print (lazy (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
+ 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, _subst, 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
+ debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
+ List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
+ active_l;
+ debug_print (lazy ">>>>>>>>>>>>>>");
+ 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 add_to_passive eql passives =
+ add_to_passive passives eql eql
+;;
+
+
projects / helm.git / blobdiff