(* set to false to disable paramodulation inside auto_tac *)
+let fst3 a,_,_ = a;;
+let last _,_,a = a;;
+
let connect_to_auto = true;;
+let debug_print = Utils.debug_print;;
(* profiling statistics... *)
let infer_time = ref 0.;;
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;;
module EqualitySet = Set.Make(OrderedEquality);;
-type passive_table = Equality.equality list * EqualitySet.t
+type passive_table = Equality.equality list * EqualitySet.t * Indexing.Index.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
+ | 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,_,_) = l ;;
+let list_of_active (l,_) = 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 *)
+ (* we have the invariant that the list and the set have the same
+ * cardinality *)
+ EqualitySet.elements set, set,
+ List.fold_left Indexing.index Indexing.empty eq_list
;;
+
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_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 *)
+ | [], s , _ when EqualitySet.is_empty s -> true
+ | [], s ,_ -> assert false (* the set and the list should be in sync *)
| _ -> false
;;
match (List.rev goals) with goal::_ -> goal | _ -> assert false
in
*)
- let pos_list, pos_set = passive in
+ let pos_list, pos_set, pos_table = passive in
let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in
if !weight_age_ratio > 0 then
weight_age_counter := !weight_age_counter - 1;
match !weight_age_counter with
| 0 -> (
weight_age_counter := !weight_age_ratio;
- let skip_giant pos_list pos_set =
+ let skip_giant pos_list pos_set pos_table =
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)
+ hd, (tl, EqualitySet.remove hd pos_set,
+ Indexing.remove_index pos_table hd)
else
(*
(prerr_endline
("+++ skipping giant of size "^string_of_int w^" +++");
*)
- select env g (tl@[hd],pos_set)
+ select env g (tl@[hd],pos_set,pos_table)
| _ -> assert false
in
- skip_giant pos_list pos_set)
+ skip_giant pos_list pos_set pos_table)
(*
let rec skip_giant pos_list pos_set =
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)
+ current,(remove current pos_list, EqualitySet.remove current pos_set,
+ Indexing.remove_index pos_table current)
;;
let filter_dependent bag passive id =
- let pos_list, pos_set = passive in
+ let pos_list, pos_set, pos_table = passive in
let passive,no_pruned =
List.fold_right
- (fun eq ((list,set),no) ->
+ (fun eq ((list,set,table),no) ->
if Equality.depend bag eq id then
- (list, EqualitySet.remove eq set), no + 1
+ (list, EqualitySet.remove eq set,Indexing.remove_index table eq),
+ no + 1
else
- (eq::list, set), no)
- pos_list (([],pos_set),0)
+ (eq::list,set,table), no)
+ pos_list (([],pos_set,pos_table),0)
in
(*
if no_pruned > 0 then
(* 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 pos_list, pos_set , pos_table = 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 =
(fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred)
pos
in
- pos_head @ pos_list @ pos_tail, add pos_set pos
+ pos_head @ pos_list @ pos_tail, add pos_set pos,
+ List.fold_left Indexing.index pos_table pos
;;
(* TODO *)
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
)
;;
(Printf.sprintf "equalities:\n%s\n"
(String.concat "\n"
(List.map Equality.string_of_equality equalities))));
- Utils.debug_print (lazy "SIMPLYFYING 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 =
let pp_goal_set msg goals names =
let active_goals, passive_goals = goals in
- prerr_endline ("////" ^ msg);
- prerr_endline ("ACTIVE G: " ^
+ debug_print (lazy ("////" ^ msg));
+ debug_print (lazy ("ACTIVE G: " ^
(String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
- active_goals)));
- prerr_endline ("PASSIVE G: " ^
+ active_goals))));
+ debug_print (lazy ("PASSIVE G: " ^
(String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
- passive_goals)))
+ passive_goals))))
;;
let check_if_goal_is_subsumed bag ((_,ctx,_) as 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
-(* match Indexing.subsumption env table goal_equation with*)
+ (* match Indexing.subsumption env table goal_equation with *)
match Indexing.unification env table goal_equation with
| Some (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 =
+ 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 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)
+ 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
- let p =
+ if Utils.debug_metas then
+ Indexing.check_for_duplicates cicmenv "from subsumption";
+ let bag, 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)
+ 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
;;
(let _,context,_ = env in
try
let s,m,_ =
- Founif.unification m m context left right CicUniv.empty_ugraph
+ Founif.unification [] 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)
+ with CicUnification.UnificationFailure _ -> None)
| _ -> 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 =
([],passive_goals) active_goals
;;
-let check_if_goals_set_is_solved bag env active goals =
+let check_if_goals_set_is_solved bag env active passive 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)])
-(* provare active and passive?*)
- None active_goals
+ 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));
+ (fun bag -> check_if_goal_is_subsumed bag env (last passive))
+ ])
+ (bag,None) (active_goals @ passive_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
-(*
- if changed then
- prerr_endline ("--------------- goal semplificato");
-*)
- let (_,_,t1) = selected in
+ let changed, selected = simplify_goal bag env hd active in
+ let (_,m1,t1) = selected in
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 =
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)))
+ debug_print (lazy
+ (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)))
+ debug_print (lazy
+ (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))))
(snd goals);
;;
let print_status iterno goals active passive =
- prerr_endline
+ 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))
+ (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 *)
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 ->
- prerr_endline
+ match check_if_goals_set_is_solved bag env active passive goals with
+ | bag, Some p ->
+ debug_print (lazy
(Printf.sprintf "\nFound a proof in: %f\n"
- (Unix.gettimeofday() -. initial_time));
- ParamodulationSuccess (p,active,passive)
- | None ->
+ (Unix.gettimeofday() -. initial_time)));
+ 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 passive = List.map Equality.id_of (fst3 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
+ 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
+ step bag goals passive active (g_iterno+1) (s_iterno+1)
+ (* 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 0 0
;;
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 w,_,_,_,_ = Equality.open_equality current in
+ if w > 100 then
+ (HLog.debug
+ ("skipping giant " ^ CicPp.ppterm term ^ " of weight " ^
+ string_of_int w); active, passive, bag)
+ else
+ 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
try
let _ = CicUtil.lookup_meta i metasenv in metasenv
with CicUtil.Meta_not_found _ ->
- prerr_endline ("not found: "^(string_of_int i));
+ 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
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) ->
+ | 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,t)
+ metasenv,Cic.LetIn(name,s,ty,t)
| Cic.Const(uri,ens) ->
let metasenv,ens =
List.fold_right
aux metasenv 0 p
;;
-let fix_metasenv metasenv =
+let fix_metasenv context metasenv =
List.fold_left
(fun m (i,c,t) ->
- let m,t = fix_proof m c false t in
+ let m,t = fix_proof m context false t in
let m = List.filter (fun (j,_,_) -> j<>i) m in
- (i,c,t)::m)
+ (i,context,t)::m)
metasenv metasenv
;;
+
(* status: input proof status
* goalproof: forward steps on goal
* newproof: backward steps
bag status
goalproof newproof subsumption_id subsumption_subst proof_menv
=
- if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
- else prerr_endline (CicMetaSubst.ppmetasenv [] 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, meta_proof, term_to_prove, attrs = proof 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
- prerr_endline "Proof:";
- prerr_endline
+ debug_print (lazy "Proof:");
+ debug_print (lazy
(Equality.pp_proof bag names goalproof newproof subsumption_subst
- subsumption_id type_of_goal);
+ subsumption_id type_of_goal));
(*
prerr_endline ("max weight: " ^
(string_of_int (Equality.max_weight goalproof newproof)));
(ProofEngineHelpers.compare_metasenvs
~newmetasenv:metasenv ~oldmetasenv:proof_menv) in
let goal_proof, side_effects_t =
- let initial = (* Equality.add_subst subsumption_subst*) newproof in
+ 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
+ (* assert (metasenv=[]); *)
+ let real_menv = fix_metasenv context (proof_menv@metasenv) in
let real_menv,goal_proof =
fix_proof real_menv context false goal_proof in
(*
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
- prerr_endline (CicPp.ppterm goal_proof);
- CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
+ 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.AssertFailure s -> assert false
(* fail "Maybe the local context of metas in the goal was not an IRL" s *)
in
- prerr_endline "+++++++++++++ FINE UNIF";
+ Utils.debug_print (lazy "+++++++++++++ FINE UNIF");
let final_subst =
(goalno,(context,goal_proof,type_of_goal))::subst_side_effects
in
*)
let proof, real_metasenv =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goalno (CicMetaSubst.apply_subst final_subst)
+ proof goalno final_subst
(List.filter (fun i,_,_ -> i<>goalno ) real_menv)
in
let open_goals =
(* 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
~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
(* 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, meta_proof, term_to_prove, attrs = proof 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 canonical_menv,other_menv =
+ List.partition (fun (_,c,_) -> c = context) metasenv in
+ (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *)
+ let metasenv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
- prerr_endline (string_of_int (List.length (fst active)));
+ 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 (_,_,ty) = goal in
+ debug_print (lazy ("prima " ^ CicPp.ppterm ty));
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
+ debug_print (lazy ("in mezzo " ^ CicPp.ppterm ty));
+ 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
None -> subsumed
| Some id -> id::subsumed in
+ debug_print (lazy "dopo subsumed");
let res =
List.map
(fun
(goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
+ let subst, proof, gl =
build_proof bag
- status goalproof newproof subsumption_id subsumption_subst proof_menv)
- subsumed_or_id in
- res, !maxmeta
+ status goalproof newproof subsumption_id subsumption_subst proof_menv
+ in
+ let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
+ let newmetasenv =
+ other_menv @
+ List.filter
+ (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
+ in
+ let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
+ (subst, proof,gl)) subsumed_or_id
+ in
+ 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, meta_proof, term_to_prove, attrs = proof 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
Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
- let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in
+ 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 && 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
- prerr_endline ">>>>>> ACTIVES >>>>>>>>";
- List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e))
+ debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
+ List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
active_l;
- prerr_endline ">>>>>>>>>>>>>>";
+ 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
+ | ParamodulationFailure (msg,a,p,b) ->
+ if Utils.debug then prerr_endline msg;
+ 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
- Some (subst, proof,gl),a,p, !maxmeta
+ 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, b
+;;
+
+let solve_narrowing bag status active passive goal_steps =
+ 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 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
+ 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 && 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
+ let goals =
+ let table = List.fold_left Indexing.index (last passive) (fst active) in
+ goal :: Indexing.demodulation_all_goal bag env table goal 4
+ in
+ let rec aux newactives newpassives bag = function
+ | [] -> bag, (newactives, newpassives)
+ | hd::tl ->
+ let selected = hd in
+ let (_,m1,t1) = selected in
+ let already_in =
+ List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
+ newactives
+ in
+ if already_in then
+ aux newactives newpassives bag tl
+ else
+ let bag, newpassives =
+ if Utils.metas_of_term t1 = [] then
+ bag, newpassives
+ else
+ let bag, new' =
+ Indexing.superposition_left bag env (snd active) selected
+ in
+ let new' =
+ List.map
+ (fun x -> let b, x = simplify_goal bag env x active in x)
+ new'
+ in
+ bag, newpassives @ new'
+ in
+ aux (selected::newactives) newpassives bag tl
+ in
+ let rec do_n bag ag pg = function
+ | 0 -> None, active, passive, bag
+ | n ->
+ let bag, (ag, pg) = aux [] [] bag (ag @ pg) in
+ match check_if_goals_set_is_solved bag env active passive (ag,pg) with
+ | bag, None -> do_n bag ag pg (n-1)
+ | bag, Some (gproof,newproof,subsumption_id,subsumption_subst,pmenv)->
+ let subst, proof, gl =
+ build_proof bag
+ status gproof newproof subsumption_id subsumption_subst pmenv
+ 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),active,passive, bag
+ in
+ do_n bag [] goals goal_steps
;;
+
let add_to_passive eql passives =
add_to_passive passives eql eql
;;
projects / helm.git / blobdiff