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 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
+ | ParamodulationFailure of
+ string * active_table * passive_table * Equality.equality_bag
+ | ParamodulationSuccess of
+ new_proof * active_table * passive_table * Equality.equality_bag
;;
-let list_of_passive (l,s) = l
-;;
+let list_of_passive (l,s) = l ;;
+let list_of_active (l,s) = l ;;
let make_passive eq_list =
let set =
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 bag, new_pos =
+ let bag, copy_of_current = Equality.fix_metas bag current in
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
+ let bag, res =
+ Indexing.superposition_right bag eq_uri 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
- | [] -> []
+ let rec infer_positive bag table = function
+ | [] -> bag, []
| equality::tl ->
- let maxm, res =
+ let bag, res =
Indexing.superposition_right bag
- ~subterms_only:true eq_uri !maxmeta env table equality
+ ~subterms_only:true eq_uri 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
+ let bag, pos = infer_positive bag table tl in
+ bag, 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 *)
+ let bag, pos = infer_positive bag curr_table ((*copy_of_current::*)active_list) in
if Utils.debug_metas then
ignore(List.map
(function current ->
Indexing.check_target bag c current "sup3") pos);
- res @ pos
+ bag, res @ pos
in
derived_clauses := !derived_clauses + (List.length new_pos);
match !maximal_retained_equality with
- | None -> new_pos
+ | None -> bag, new_pos
| Some eq ->
ignore(assert false);
(* if we have a maximal_retained_equality, we can discard all equalities
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
+ bag, List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
;;
let check_for_deep_subsumption env active_table eq =
(** 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
+ let demodulate bag table current =
+ let bag, newcurrent =
+ Indexing.demodulation_equality bag eq_uri env table current
in
- maxmeta := newmeta;
- if Equality.is_identity env newcurrent then None else Some newcurrent
+ bag, if Equality.is_identity env newcurrent then None else Some newcurrent
in
- let demod current =
+ let demod bag current =
if Utils.debug_metas then
ignore (Indexing.check_target bag context current "demod0");
- let res = demodulate active_table current in
+ let bag, res = demodulate bag active_table current in
if Utils.debug_metas then
ignore ((function None -> () | Some x ->
ignore (Indexing.check_target bag context x "demod1");()) res);
- res
+ bag, res
in
- let res = demod current in
+ let bag, res = demod bag current in
match res with
- | None -> None
+ | None -> bag, None
| Some c ->
if Indexing.in_index active_table c ||
check_for_deep_subsumption env active_table c
then
- None
+ bag, None
else
- res
+ bag, res
;;
(** simplifies new using active and passive *)
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
+ let demodulate bag table target =
+ let bag, newtarget =
+ Indexing.demodulation_equality bag eq_uri env table target
in
- maxmeta := newmeta;
- newtarget
+ bag, newtarget
in
(* we could also demodulate using passive. Currently we don't *)
- let new_pos = List.map (demodulate active_table) new_pos in
+ let bag, new_pos =
+ List.fold_right (fun x (bag,acc) ->
+ let bag, y = demodulate bag active_table x in
+ bag, y::acc)
+ new_pos (bag,[])
+ in
let new_pos_set =
List.fold_left
(fun s e ->
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)
+ bag, List.filter subs (List.filter is_duplicate new_pos)
;;
bag eq_uri env new_pos new_table min_weight active
=
let active_list, active_table = active in
- let active_list, newa, pruned =
+ let bag, active_list, newa, pruned =
List.fold_right
- (fun equality (res, newn,pruned) ->
+ (fun equality (bag, res, newn,pruned) ->
let ew, _, _, _,id = Equality.open_equality equality in
if ew < min_weight then
- equality::res, newn,pruned
+ bag, 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 ->
+ | bag, None -> bag, res, newn, id::pruned
+ | bag, Some e ->
if Equality.compare equality e = 0 then
- e::res, newn, pruned
+ bag, e::res, newn, pruned
else
- res, e::newn, pruned)
- active_list ([], [],[])
+ bag, res, e::newn, pruned)
+ active_list (bag, [], [],[])
in
let find eq1 where =
List.exists (Equality.meta_convertibility_eq eq1) where
newa []
in
match newa with
- | [] -> (active1,tbl), None, pruned
- | _ -> (active1,tbl), Some newa, pruned
+ | [] -> bag, (active1,tbl), None, pruned
+ | _ -> bag, (active1,tbl), Some newa, pruned
;;
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 f bag equality (resl, ress, newn) =
let ew, _, _, _ , _ = Equality.open_equality equality in
if ew < min_weight then
- equality::resl, ress, newn
+ bag, (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 ->
+ | bag, None ->
+ bag, (resl, EqualitySet.remove equality ress, newn)
+ | bag, Some e ->
if equality = e then
- equality::resl, ress, newn
+ bag, (equality::resl, ress, newn)
else
let ress = EqualitySet.remove equality ress in
- resl, ress, e::newn
+ bag, (resl, ress, e::newn)
in
- let pl, ps, newp = List.fold_right f pl ([], ps, []) in
+ let bag, (pl, ps, newp) =
+ List.fold_right (fun x (bag,acc) -> f bag x acc) pl (bag,([], 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)
+ | [] -> bag, ((pl, ps), passive_table), None
+ | _ -> bag, ((pl, ps), passive_table), Some (newp)
;;
let build_table 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 =
+ let bag, active, newa, pruned =
backward_simplify_active bag eq_uri env new_pos new_table min_weight active
in
- active, newa, pruned
+ bag, active, newa, pruned
;;
let close bag eq_uri env new' given =
([], 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
+ (fun (bag,p) c ->
+ let bag, pos = infer bag eq_uri env c (new_pos,new_table) in
+ bag, pos@p)
+ (bag,[]) given
;;
let is_commutative_law eq =
| [] -> 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 =
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)
+ let bag, res =
+ forward_simplify bag eq_uri env e (active, tbl)
in
match others with
| hd::tl -> (
)
| [] -> (
match res with
- | None -> others_simpl
- | Some e -> e::others_simpl
+ | None -> bag, others_simpl
+ | Some e -> bag, e::others_simpl
)
;;
(List.map Equality.string_of_equality equalities))));
Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
match equalities with
- | [] -> []
+ | [] -> bag, []
| hd::tl ->
- let res =
- List.rev (simpl bag eq_uri env hd tl [])
- in
+ let bag, res = simpl bag eq_uri env hd tl [] in
+ let res = List.rev res in
Utils.debug_print
(lazy
(Printf.sprintf "equalities AFTER:\n%s\n"
(String.concat "\n"
(List.map Equality.string_of_equality res))));
- res
+ bag, res
;;
let print_goals goals =
match ty with
| Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
when LibraryObjects.is_eq_URI uri ->
- (let goal_equation =
+ (let bag, goal_equation =
Equality.mk_equality bag
(0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv)
in
*)
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
- let p =
+ let bag, p =
if swapped then
Equality.symmetric bag eq_ty l id uri m
else
- p
+ bag, p
in
- Some (goalproof, p, id, subst, cicmenv)
- | None -> None)
- | _ -> None
+ bag, Some (goalproof, p, id, subst, cicmenv)
+ | None -> bag, None)
+ | _ -> bag, None
;;
-let find_all_subsumed bag maxm env table (goalproof,menv,ty) =
+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 =
+ let bag, 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 ) ->
+ List.fold_right
+ (fun (subst, equality, swapped) (bag,acc) ->
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
Indexing.check_for_duplicates cicmenv "from subsumption";
- let p =
+ let bag, p =
if swapped then
Equality.symmetric bag eq_ty l id uri m
else
- p
- in (goalproof, p, id, subst, cicmenv))
- (Indexing.subsumption_all env table goal_equation)
+ bag, p
+ in
+ bag, (goalproof, p, id, subst, cicmenv)::acc)
+ (Indexing.subsumption_all env table goal_equation) (bag,[])
(* (Indexing.unification_all env table goal_equation) *)
| _ -> assert false
;;
| _ -> None
;;
-let rec check goal = function
- | [] -> None
+let rec check b goal = function
+ | [] -> b, None
| f::tl ->
- match f goal with
- | None -> check goal tl
- | (Some p) as ok -> ok
+ match f b goal with
+ | b, None -> check b goal tl
+ | b, (Some _ as ok) -> b, ok
;;
let simplify_goal_set bag env goals active =
let check_if_goals_set_is_solved bag env active goals =
let active_goals, passive_goals = goals in
List.fold_left
- (fun proof goal ->
+ (fun (bag, proof) goal ->
match proof with
- | Some p -> proof
+ | Some p -> bag, proof
| None ->
- check goal [
- check_if_goal_is_identity env;
- check_if_goal_is_subsumed bag env (snd active)])
+ check bag goal [
+ (fun b x -> b, check_if_goal_is_identity env x);
+ (fun bag -> check_if_goal_is_subsumed bag env (snd active))])
(* provare active and passive?*)
- None active_goals
+ (bag,None) active_goals
;;
let infer_goal_set bag env active goals =
let active_goals, passive_goals = goals in
- let rec aux = function
- | [] -> active_goals, []
+ let rec aux bag = function
+ | [] -> bag, (active_goals, [])
| hd::tl ->
- let changed,selected = simplify_goal bag env hd active in
+ let changed, selected = simplify_goal bag env hd active in
let (_,_,t1) = selected in
- (*
- if changed && Utils.debug then
- prerr_endline ("goal semplificato: " ^ CicPp.ppterm t1); *)
let already_in =
List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
active_goals
in
if already_in then
- aux tl
+ aux bag tl
else
let passive_goals = tl in
- let new_passive_goals =
- if Utils.metas_of_term t1 = [] then passive_goals
+ let bag, new_passive_goals =
+ if Utils.metas_of_term t1 = [] then
+ bag, passive_goals
else
- let newmaxmeta,new' =
+ let bag, new' =
Indexing.superposition_left bag env (snd active) selected
- !maxmeta
in
- maxmeta := newmaxmeta;
- passive_goals @ new'
+ bag, passive_goals @ new'
in
- selected::active_goals, new_passive_goals
+ bag, (selected::active_goals, new_passive_goals)
in
- aux passive_goals
+ aux bag 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 bag, passive_goals =
+ List.fold_left
+ (fun (bag, acc) g ->
+ let bag, new' = Indexing.superposition_left bag env table g in
+ bag, acc @ new')
+ (bag, passive_goals) active_goals
+ in
+ bag, active_goals, passive_goals
;;
let ids_of_goal g =
(size_of_goal_set_a goals) (size_of_goal_set_p goals)))
;;
+let add_to_active_aux bag active passive env eq_uri current =
+ debug_print (lazy ("Adding to actives : " ^
+ Equality.string_of_equality ~env current));
+ match forward_simplify bag eq_uri env current active with
+ | bag, None -> None, active, passive, bag
+ | bag, Some current ->
+ let bag, new' = infer bag eq_uri env current active in
+ let active =
+ let al, tbl = active in
+ al @ [current], Indexing.index tbl current
+ in
+ let rec simplify bag new' active passive =
+ let bag, new' =
+ forward_simplify_new bag eq_uri env new' active
+ in
+ let bag, 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 -> bag, active, passive, new'
+ | Some p -> simplify bag (new' @ p) active passive
+ in
+ let bag, active, passive, new' =
+ simplify bag new' active passive
+ in
+ let passive = add_to_passive passive new' [] in
+ Some new', active, passive, bag
+;;
+
(** given-clause algorithm with full reduction strategy: NEW implementation *)
(* here goals is a set of goals in OR *)
let given_clause
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 =
+ let rec step bag 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))
+ (ParamodulationFailure ("No more iterations to spend",active,passive,bag))
else if Unix.gettimeofday () > max_time then
- (ParamodulationFailure ("No more time to spend",active,passive))
+ (ParamodulationFailure ("No more time to spend",active,passive,bag))
else
let _ =
print_status (max g_iterno s_iterno) goals active passive
passive
in
kept_clauses := (size_of_passive passive) + (size_of_active active);
- let goals =
+ let bag, goals =
if g_iterno < goal_steps then
infer_goal_set bag env active goals
else
- goals
+ bag, goals
in
match check_if_goals_set_is_solved bag env active goals with
- | Some p ->
+ | bag, Some p ->
debug_print (lazy
(Printf.sprintf "\nFound a proof in: %f\n"
(Unix.gettimeofday() -. initial_time)));
- ParamodulationSuccess (p,active,passive)
- | None ->
+ ParamodulationSuccess (p,active,passive,bag)
+ | bag, None ->
(* SELECTION *)
if passive_is_empty passive then
if no_more_passive_goals goals then
ParamodulationFailure
- ("No more passive equations/goals",active,passive)
+ ("No more passive equations/goals",active,passive,bag)
(*maybe this is a success! *)
else
- step goals passive active (g_iterno+1) (s_iterno+1)
+ step bag 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 bag =
+ if max g_iterno s_iterno mod 40 = 0 then
+ (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
+ Equality.collect bag active passive goal)
else
- None, passive
+ bag
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)
+ if s_iterno > saturation_steps then
+ ParamodulationFailure ("max saturation steps",active,passive,bag)
+ else
+ let current, passive = select env goals passive in
+ match add_to_active_aux bag active passive env eq_uri current with
+ | None, active, passive, bag ->
+ step bag goals passive active (g_iterno+1) (s_iterno+1)
+ | Some new', active, passive, bag ->
+ let bag, active_goals, passive_goals =
+ infer_goal_set_with_current bag env current goals active
+ in
+ let goals =
+ let a,b,_ = build_table new' in
+ let rc =
+ simplify_goal_set bag env (active_goals,passive_goals) (a,b)
+ in
+ rc
+ in
+ step bag goals passive active (g_iterno+1) (s_iterno+1)
end
in
- step goals passive active 1 1
+ step bag 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)
+ bag, active, passive
else
let current, passive = select env ([goal],[]) passive in
- let res = forward_simplify bag eq_uri env current active in
+ let bag, 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 bag, new' = infer bag eq_uri env current active in
let active =
if Equality.is_identity env current then active
else
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 =
+ let rec simplify bag new' active passive =
+ let bag, new' = forward_simplify_new bag eq_uri env new' active in
+ let bag, 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
+ | None -> bag, active, passive, new'
+ | Some p -> simplify bag (new' @ p) active passive
in
- let active, passive, new' = simplify new' active passive in
+ let bag, active, passive, new' = simplify bag new' active passive in
let _ =
Utils.debug_print
(lazy
and default_width = !maxwidth;;
let reset_refs () =
- maxmeta := 0;
symbols_counter := 0;
weight_age_counter := !weight_age_ratio;
processed_clauses := 0;
kept_clauses := 0;
;;
+let add_to_active bag active passive env ty term newmetas =
+ reset_refs ();
+ match LibraryObjects.eq_URI () with
+ | None -> active, passive, bag
+ | Some eq_uri ->
+ try
+ let bag, current = Equality.equality_of_term bag term ty newmetas in
+ let bag, current = Equality.fix_metas bag current in
+ match add_to_active_aux bag active passive env eq_uri current with
+ | _,a,p,b -> a,p,b
+ with
+ | Equality.TermIsNotAnEquality -> active, passive, bag
+;;
+
+
let eq_of_goal = function
| Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
uri
(* exported functions *)
-let pump_actives context bag maxm active passive saturation_steps max_time =
+let pump_actives context bag active passive saturation_steps max_time =
reset_refs();
- maxmeta := maxm;
(*
let max_l l =
List.fold_left
(* let ma = max_l active_l in *)
(* let mp = max_l passive_l in *)
match LibraryObjects.eq_URI () with
- | None -> active, passive, !maxmeta
+ | None -> active, passive, bag
| 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
+ | ParamodulationFailure (_,a,p,b) ->
+ a, p, b
| ParamodulationSuccess _ ->
assert false)
;;
-let all_subsumed bag maxm status active passive =
- maxmeta := maxm;
+let all_subsumed bag status active passive =
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 _,goal = simplify_goal bag env goal table in
let (_,_,ty) = goal in
debug_print (lazy ("in mezzo " ^ CicPp.ppterm ty));
- let subsumed = find_all_subsumed bag !maxmeta env (snd table) goal in
+ let bag, subsumed = find_all_subsumed bag env (snd table) goal in
debug_print (lazy ("dopo " ^ CicPp.ppterm ty));
let subsumed_or_id =
match (check_if_goal_is_identity env goal) with
let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
(subst, proof,gl)) subsumed_or_id
in
- res, !maxmeta
+ res
+;;
let given_clause
- bag maxm status active passive goal_steps saturation_steps max_time
+ bag 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
+ let metas_occurring_in_goal = CicUtil.metas_of_term cleaned_goal in
let canonical_menv,other_menv =
List.partition (fun (_,c,_) -> c = context) metasenv in
- (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *)
Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
let canonical_menv =
List.map
(fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv
in
- let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in
+ let metasenv' =
+ List.filter
+ (fun (i,_,_)-> i<>goalno && List.mem_assoc i metas_occurring_in_goal)
+ canonical_menv
+ in
let goal = [], metasenv', cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in
debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
given_clause bag eq_uri env goals passive active
goal_steps saturation_steps max_time
with
- | ParamodulationFailure (_,a,p) ->
- None, a, p, !maxmeta
+ | ParamodulationFailure (_,a,p,b) ->
+ None, a, p, b
| ParamodulationSuccess
- ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p) ->
+ ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p,b) ->
let subst, proof, gl =
- build_proof bag
+ build_proof b
status goalproof newproof subsumption_id subsumption_subst proof_menv
in
let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
- Some (subst, proof,gl),a,p, !maxmeta
+ Some (subst, proof,gl),a,p, b
;;
projects / helm.git / blobdiff