open Inference;;
open Utils;;
+let check_table t l =
+ List.fold_left
+ (fun b (_,eq) -> b && (Indexing.in_index t eq)) true l
-(*
-for debugging
-let check_equation env equation msg =
- let w, proof, (eq_ty, left, right, order), metas = equation in
- let metasenv, context, ugraph = env in
- let metasenv' = metasenv @ metas in
- try
- CicTypeChecker.type_of_aux' metasenv' context left ugraph;
- CicTypeChecker.type_of_aux' metasenv' context right ugraph;
- ()
- with
- CicUtil.Meta_not_found _ as exn ->
- begin
- prerr_endline msg;
- prerr_endline (CicPp.ppterm left);
- prerr_endline (CicPp.ppterm right);
- raise exn
- end
-*)
(* set to false to disable paramodulation inside auto_tac *)
let connect_to_auto = true;;
let maxdepth = ref 3;;
let maxwidth = ref 3;;
+let test eq = false
+(*
+ let (_,(_,_,(ty,left,right,_),m1)) = eq in
+ let actual =
+ (Inference.metas_of_term left)@(Inference.metas_of_term right)
+ in
+ let m = List.filter (fun (i, _, _) -> List.mem i actual) m1 in
+ m <> m1
+;; *)
type result =
| ParamodulationFailure
and w2, _, (ty', left', right', _), m2 = eq2 in
match Pervasives.compare w1 w2 with
| 0 ->
- let res = (List.length m1) - (List.length m2) in
+ let res = (List.length m1) - (List.length m2) in
if res <> 0 then res else Pervasives.compare eq1 eq2
| res -> res
end
let minor eq =
let w, _, (ty, left, right, o), _ = eq in
match o with
- | Lt -> Some left
- | Le -> assert false
- | Gt -> Some right
- | Ge -> assert false
- | Eq
- | Incomparable -> None
-
+ | Lt -> Some left
+ | Le -> assert false
+ | Gt -> Some right
+ | Ge -> assert false
+ | Eq
+ | Incomparable -> None
+
let compare eq1 eq2 =
let w1, _, (ty, left, right, o1), m1 = eq1
and w2, _, (ty', left', right', o2), m2 = eq2 in
match Pervasives.compare w1 w2 with
| 0 ->
- (match minor eq1, minor eq2 with
- | Some t1, Some t2 ->
- fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2)
- | Some _, None -> -1
- | None, Some _ -> 1
- | _,_ ->
- (List.length m2) - (List.length m1) )
- | res -> res
+ (match minor eq1, minor eq2 with
+ | Some t1, Some t2 ->
+ fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2)
+ | Some _, None -> -1
+ | None, Some _ -> 1
+ | _,_ ->
+ (List.length m2) - (List.length m1) )
+ | res -> res
let compare eq1 eq2 =
match compare eq1 eq2 with
- 0 -> Pervasives.compare eq1 eq2
+ 0 -> Pervasives.compare eq1 eq2
| res -> res
end
*)
(match l with
[] -> raise Empty_list
| a::tl ->
- let wa = float_of_int (weight a) in
- let x = ref 0. in
- List.fold_left
- (fun (current,w) arg ->
- x:=!x +. 1.;
+ let wa = float_of_int (weight a) in
+ let x = ref 0. in
+ List.fold_left
+ (fun (current,w) arg ->
+ x:=!x +. 1.;
let w1 = weight arg in
let wa = (float_of_int w1) +. !x *. age_factor in
- if wa < w then (arg,wa) else (current,w))
- (a,wa) tl)
+ if wa < w then (arg,wa) else (current,w))
+ (a,wa) tl)
;;
(*
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
| [], (hd:EqualitySet.elt)::tl ->
- let w,_,_,_ = hd in
let passive_table =
- Indexing.remove_index passive_table hd
+ Indexing.remove_index passive_table hd
in (Positive, hd),
(([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
| _, _ -> assert false
let ok set equality = not (EqualitySet.mem equality set) in
let neg = List.filter (ok neg_set) new_neg
and pos = List.filter (ok pos_set) new_pos in
- let table =
- List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+ let table =
+ List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
in
let add set equalities =
List.fold_left (fun s e -> EqualitySet.add e s) set equalities
let maxm, res =
Indexing.superposition_left !maxmeta env active_table current in
if Utils.debug_metas then
- ignore(List.map
- (function current ->
- Indexing.check_target c current "sup-1") res);
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup-1") res);
maxmeta := maxm;
res, []
| Positive ->
let maxm, res =
Indexing.superposition_right !maxmeta env active_table current in
if Utils.debug_metas then
- ignore(List.map
- (function current ->
- Indexing.check_target c current "sup0") res);
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup0") res);
maxmeta := maxm;
let rec infer_positive table = function
| [] -> [], []
let maxm, res =
Indexing.superposition_left !maxmeta env table equality in
maxmeta := maxm;
- if Utils.debug_metas then
- ignore(List.map
- (function current ->
- Indexing.check_target c current "supl") res);
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "supl") res);
let neg, pos = infer_positive table tl in
res @ neg, pos
| (Positive, equality)::tl ->
let maxm, res =
Indexing.superposition_right !maxmeta env table equality in
maxmeta := maxm;
- if Utils.debug_metas then
- ignore
- (List.map
- (function current ->
- Indexing.check_target c current "sup2") res);
+ if Utils.debug_metas then
+ ignore
+ (List.map
+ (function current ->
+ Indexing.check_target c current "sup2") res);
let neg, pos = infer_positive table tl in
neg, res @ pos
in
maxmeta := maxm;
let curr_table = Indexing.index Indexing.empty current in
let neg, pos =
- infer_positive curr_table ((sign,copy_of_current)::active_list)
- in
- if Utils.debug_metas then
- ignore(List.map
- (function current ->
- Indexing.check_target c current "sup3") pos);
+ infer_positive curr_table ((sign,copy_of_current)::active_list)
+ in
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup3") pos);
neg, res @ pos
in
derived_clauses := !derived_clauses + (List.length new_neg) +
match !maximal_retained_equality with
| None ->
if Utils.debug_metas then
- (ignore(List.map
- (function current ->
- Indexing.check_target c current "sup4") new_pos);
- ignore(List.map
- (function current ->
- Indexing.check_target c current "sup5") new_neg));
+ (ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup4") new_pos);
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup5") new_neg));
new_neg, new_pos
| Some eq ->
ignore(assert false);
in
List.filter filterfun new_pos
in
- new_neg, new_pos
+ new_neg, new_pos
;;
if is_identity env newcurrent then
if sign = Negative then Some (sign, newcurrent)
else (
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
-(* (string_of_equality current) *)
-(* (string_of_equality newcurrent))); *)
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "active is: %s" *)
-(* (String.concat "\n" *)
-(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *)
- None
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
+(* (string_of_equality current) *)
+(* (string_of_equality newcurrent))); *)
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "active is: %s" *)
+(* (String.concat "\n" *)
+(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *)
+ None
)
else
Some (sign, newcurrent)
in
- let res =
+ let rec demod current =
if Utils.debug_metas then
ignore (Indexing.check_target context current "demod0");
let res = demodulate active_table current in
if Utils.debug_metas then
- ignore ((function None -> () | Some (_,x) ->
- Indexing.check_target context x "demod1";()) res);
+ ignore ((function None -> () | Some (_,x) ->
+ ignore (Indexing.check_target context x "demod1");()) res);
match res with
| None -> None
| Some (sign, newcurrent) ->
match passive_table with
| None -> res
- | Some passive_table -> demodulate passive_table newcurrent
- in
+ | Some passive_table ->
+ match demodulate passive_table newcurrent with
+ | None -> None
+ | Some (sign,newnewcurrent) ->
+ if newcurrent <> newnewcurrent then
+ demod newnewcurrent
+ else Some (sign,newnewcurrent)
+ in
+ let res = demod current in
match res with
| None -> None
| Some (Negative, c) ->
else
match passive_table with
| None ->
- if fst (Indexing.subsumption env active_table c) then
- None
- else
- res
+ if fst (Indexing.subsumption env active_table c) then
+ None
+ else
+ res
| Some passive_table ->
if Indexing.in_index passive_table c then None
else
- let r1, _ = Indexing.subsumption env active_table c in
- if r1 then None else
- let r2, _ = Indexing.subsumption env passive_table c in
- if r2 then None else res
+ let r1, _ = Indexing.subsumption env active_table c in
+ if r1 then None else
+ let r2, _ = Indexing.subsumption env passive_table c in
+ if r2 then None else res
;;
type fs_time_info_t = {
if Utils.debug_metas then
begin
let m,c,u = env in
- ignore(List.map
- (fun current ->
- Indexing.check_target c current "forward new neg") new_neg);
- ignore(List.map
- (fun current -> Indexing.check_target c current "forward new pos")
+ ignore(List.map
+ (fun current ->
+ Indexing.check_target c current "forward new neg") new_neg);
+ ignore(List.map
+ (fun current -> Indexing.check_target c current "forward new pos")
new_pos;)
end;
let t1 = Unix.gettimeofday () in
;;
+(** simplifies a goal with equalities in active and passive *)
+let rec simplify_goal env goal ?passive (active_list, active_table) =
+ let pl, passive_table =
+ match passive with
+ | None -> [], None
+ | Some ((pn, _), (pp, _), pt) ->
+ let pn = List.map (fun e -> (Negative, e)) pn
+ and pp = List.map (fun e -> (Positive, e)) pp in
+ pn @ pp, Some pt
+ in
+
+ let demodulate table goal =
+ let newmeta, newgoal =
+ Indexing.demodulation_goal !maxmeta env table goal in
+ maxmeta := newmeta;
+ goal <> newgoal, newgoal
+ in
+ let changed, goal =
+ match passive_table with
+ | None -> demodulate active_table goal
+ | Some passive_table ->
+ let changed, goal = demodulate active_table goal in
+ let changed', goal = demodulate passive_table goal in
+ (changed || changed'), goal
+ in
+ changed, if not changed then goal
+ else snd (simplify_goal env goal ?passive (active_list, active_table))
+;;
+
+
+let simplify_goals env goals ?passive active =
+ let a_goals, p_goals = goals in
+ let p_goals =
+ List.map
+ (fun (d, gl) ->
+ let gl =
+ List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in
+ d, gl)
+ p_goals
+ in
+ let goals =
+ List.fold_left
+ (fun (a, p) (d, gl) ->
+ let changed = ref false in
+ let gl =
+ List.map
+ (fun g ->
+ let c, g = simplify_goal env g ?passive active in
+ changed := !changed || c; g) gl in
+ if !changed then (a, (d, gl)::p) else ((d, gl)::a, p))
+ ([], p_goals) a_goals
+ in
+ goals
+;;
+
+
(** simplifies active usign new *)
let backward_simplify_active env new_pos new_table min_weight active =
let active_list, active_table = active in
List.fold_left
(fun (n,p) (s,c) ->
let neg,pos = infer env s c (new_pos,new_table) in
- neg@n,pos@p)
+ neg@n,pos@p)
([],[]) given
;;
let is_commutative_law eq =
let w, proof, (eq_ty, left, right, order), metas = snd eq in
match left,right with
- Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1],
- Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
- f1 = f2 && a1 = b2 && a2 = b1
+ Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1],
+ Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
+ f1 = f2 && a1 = b2 && a2 = b1
| _ -> false
;;
;;
-(** simplifies a goal with equalities in active and passive *)
-let simplify_goal env goal ?passive (active_list, active_table) =
- let pl, passive_table =
- match passive with
- | None -> [], None
- | Some ((pn, _), (pp, _), pt) ->
- let pn = List.map (fun e -> (Negative, e)) pn
- and pp = List.map (fun e -> (Positive, e)) pp in
- pn @ pp, Some pt
- in
-
- let demodulate table goal =
- let newmeta, newgoal =
- Indexing.demodulation_goal !maxmeta env table goal in
- maxmeta := newmeta;
- goal != newgoal, newgoal
- in
- let changed, goal =
- match passive_table with
- | None -> demodulate active_table goal
- | Some passive_table ->
- let changed, goal = demodulate active_table goal in
- let changed', goal = demodulate passive_table goal in
- (changed || changed'), goal
- in
- changed, goal
-;;
-
-
-let simplify_goals env goals ?passive active =
- let a_goals, p_goals = goals in
- let p_goals =
- List.map
- (fun (d, gl) ->
- let gl =
- List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in
- d, gl)
- p_goals
- in
- let goals =
- List.fold_left
- (fun (a, p) (d, gl) ->
- let changed = ref false in
- let gl =
- List.map
- (fun g ->
- let c, g = simplify_goal env g ?passive active in
- changed := !changed || c; g) gl in
- if !changed then (a, (d, gl)::p) else ((d, gl)::a, p))
- ([], p_goals) a_goals
- in
- goals
-;;
-
let simplify_theorems env theorems ?passive (active_list, active_table) =
let pl, passive_table =
res
;;
+(*
(* applies equality to goal to see if the goal can be closed *)
let apply_equality_to_goal env equality goal =
let module C = Cic in
(* (string_of_equality equality) (CicPp.ppterm gterm))); *)
try
let subst, metasenv', _ =
- let menv = metasenv @ metas @ gmetas in
Inference.unification metas gmetas context eqterm gterm ugraph
in
let newproof =
match proof with
- | I.BasicProof t -> I.BasicProof (CicMetaSubst.apply_subst subst t)
+ | I.BasicProof (subst',t) -> I.BasicProof (subst@subst',t)
| I.ProofBlock (s, uri, nt, t, pe, p) ->
I.ProofBlock (subst @ s, uri, nt, t, pe, p)
| _ -> assert false
let rec repl = function
| I.ProofGoalBlock (_, gp) -> I.ProofGoalBlock (newproof, gp)
| I.NoProof -> newproof
- | I.BasicProof p -> newproof
- | I.SubProof (t, i, p) -> I.SubProof (t, i, repl p)
+ | I.BasicProof _ -> newproof
+ | I.SubProof (t, i, p) ->
+ prerr_endline "SUBPROOF!";
+ I.SubProof (t, i, repl p)
| _ -> assert false
in
repl gproof
in
- true, subst, newgproof
+ true, (subst:Inference.substitution), newgproof
with CicUnification.UnificationFailure _ ->
false, [], I.NoProof
;;
let newp =
let rec repl = function
| Inference.ProofGoalBlock (_, gp) ->
- Inference.ProofGoalBlock (Inference.BasicProof p, gp)
- | Inference.NoProof -> Inference.BasicProof p
- | Inference.BasicProof _ -> Inference.BasicProof p
+ Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
+ | Inference.NoProof -> Inference.BasicProof ([],p)
+ | Inference.BasicProof _ -> Inference.BasicProof ([],p)
| Inference.SubProof (t, i, p2) ->
Inference.SubProof (t, i, repl p2)
| _ -> assert false
ProofGoalBlock (sp1, gp sp2)
| BasicProof _
| NoProof ->
- SubProof (p, i, BasicProof (Cic.Meta (i, irl)))
+ SubProof (p, i, BasicProof ([],Cic.Meta (i, irl)))
| ProofSymBlock (s, sp) ->
ProofSymBlock (s, gp sp)
| ProofBlock (s, u, nt, t, pe, sp) ->
+ prerr_endline "apply_to_goal!";
ProofBlock (s, u, nt, t, pe, gp sp)
in gp proof
in
else
false, [], []
in
- if r = true then `Ok (s, l) else aux theorems
+ if r = true then `Ok ((s:Cic.substitution),l) else aux theorems
;;
let propagate_subst subst (proof, metas, term) =
let rec repl = function
| NoProof -> NoProof
- | BasicProof t ->
- BasicProof (CicMetaSubst.apply_subst subst t)
+ | BasicProof (subst',t) ->
+ BasicProof (subst@subst',t)
| ProofGoalBlock (p, pb) ->
let pb' = repl pb in
ProofGoalBlock (p, pb')
| SubProof (t, i, p) ->
- let t' = CicMetaSubst.apply_subst subst t in
+ let t' = Inference.apply_subst subst t in
let p = repl p in
SubProof (t', i, p)
| ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p)
ok, (a_goals, p_goals)
;;
-
(* given-clause algorithm with lazy reduction strategy *)
let rec given_clause dbd env goals theorems passive active =
- let _,context,_ = env in
let goals = simplify_goals env goals active in
let ok, goals = activate_goal goals in
(* let theorems = simplify_theorems env theorems active in *)
let (sign, current), passive = select env (fst goals) passive active in
let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
prerr_endline ("Selected = " ^
- (CicPp.pp (Inference.term_of_equality current) names));
+ (CicPp.pp (Inference.term_of_equality current) names));
let time1 = Unix.gettimeofday () in
let res = forward_simplify env (sign, current) ~passive active in
let time2 = Unix.gettimeofday () in
ParamodulationSuccess (proof, env)
)
;;
+*)
+let counter = ref 0
(** given-clause algorithm with full reduction strategy *)
let rec given_clause_fullred dbd env goals theorems passive active =
+(*
+ let table,list = active in
+ assert (check_table list table);
+*)
let goals = simplify_goals env goals ~passive active in
let _,context,_ = env in
let ok, goals = activate_goal goals in
(* (Printf.sprintf "goal activated:\n%s\n%s\n" *)
(* (CicPp.ppterm t) (string_of_proof p))); *)
(* in *)
- let ok, goals =
- apply_goal_to_theorems dbd env theorems ~passive active goals
- in
+ let ok, proof =
+ (* apply_goal_to_theorems dbd env theorems ~passive active goals in *)
+ let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+ match (fst goals) with
+ | (_, [proof, m, Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_
+ when left = right && iseq uri ->
+ let p =
+ Cic.Appl [Cic.MutConstruct (* reflexivity *)
+ (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left]
+ in
+ let newp =
+ let rec repl = function
+ | Inference.ProofGoalBlock (_, gp) ->
+ Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
+ | Inference.NoProof -> Inference.BasicProof ([],p)
+ | Inference.BasicProof _ -> Inference.BasicProof ([],p)
+ | Inference.SubProof (t, i, p2) ->
+ Inference.SubProof (t, i, repl p2)
+ | _ -> assert false
+ in
+ repl proof
+ in true, Some newp
+ | (_, [proof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_->
+ (* here we check if the goal is subsumed by an active *)
+ let ok, subst =
+ (* the first m is unused *)
+ Indexing.subsumption (m,context,CicUniv.empty_ugraph)
+ (snd active)
+ (0,proof,(eq_ty,left,right,Eq),m)
+ in
+ if ok then
+ begin
+ prerr_endline "The goal is subsumed by an active";
+ false, None
+ end
+ else
+ ok, None
+ | _ -> false, None
+ in
if ok then
- let proof =
- match (fst goals) with
- | (_, [proof, _, _])::_ -> Some proof
- | _ -> assert false
- in
( prerr_endline "esco qui";
+ let active =
+ List.filter test (fst active) in
+ let s = Printf.sprintf "actives:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ active)))
+ in prerr_endline s;
+ let passive =
+ List.filter
+ (fun x -> test (1,x))
+ (let x,y,_ = passive in (fst x)@(fst y)) in
+ let p = Printf.sprintf "passives:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun e ->
+ (string_of_equality ~env e))
+ passive)))
+ in prerr_endline p;
(*
- let s = Printf.sprintf "actives:\n%s\n"
- (String.concat "\n"
+ let s = Printf.sprintf "actives:\n%s\n"
+ (String.concat "\n"
((List.map
- (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
(string_of_equality ~env e))
- (fst active)))) in
- let sp = Printf.sprintf "passives:\n%s\n"
- (String.concat "\n"
+ (fst active)))) in
+ let sp = Printf.sprintf "passives:\n%s\n"
+ (String.concat "\n"
(List.map
- (string_of_equality ~env)
- (let x,y,_ = passive in (fst x)@(fst y)))) in
- prerr_endline s;
- prerr_endline sp; *)
+ (string_of_equality ~env)
+ (let x,y,_ = passive in (fst x)@(fst y)))) in
+ prerr_endline s;
+ prerr_endline sp; *)
ParamodulationSuccess (proof, env))
else
given_clause_fullred_aux dbd env goals theorems passive active
else given_clause_fullred_aux dbd env goals theorems passive active
and given_clause_fullred_aux dbd env goals theorems passive active =
- prerr_endline ("MAXMETA: " ^ string_of_int !maxmeta ^
+ prerr_endline (string_of_int !counter ^
+ " MAXMETA: " ^ string_of_int !maxmeta ^
" LOCALMAX: " ^ string_of_int !Indexing.local_max ^
- " #ACTIVES: " ^ string_of_int (size_of_active active) ^
+ " #ACTIVES: " ^ string_of_int (size_of_active active) ^
" #PASSIVES: " ^ string_of_int (size_of_passive passive));
+ incr counter;
+(* if !counter mod 10 = 0 then
+ begin
+ let size = HExtlib.estimate_size (passive,active) in
+ let sizep = HExtlib.estimate_size (passive) in
+ let sizea = HExtlib.estimate_size (active) in
+ let (l1,s1),(l2,s2), t = passive in
+ let sizetbl = HExtlib.estimate_size t in
+ let sizel = HExtlib.estimate_size (l1,l2) in
+ let sizes = HExtlib.estimate_size (s1,s2) in
+
+ prerr_endline ("SIZE: " ^ string_of_int size);
+ prerr_endline ("SIZE P: " ^ string_of_int sizep);
+ prerr_endline ("SIZE A: " ^ string_of_int sizea);
+ prerr_endline ("SIZE TBL: " ^ string_of_int sizetbl ^
+ " SIZE L: " ^ string_of_int sizel ^
+ " SIZE S:" ^ string_of_int sizes);
+ end;*)
(*
if (size_of_active active) mod 50 = 0 then
(let s = Printf.sprintf "actives:\n%s\n"
given_clause_fullred dbd env goals theorems passive active
| false ->
let (sign, current), passive = select env (fst goals) passive active in
- let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
- prerr_endline ("Selected = " ^ (string_of_sign sign) ^ " " ^
- string_of_equality ~env current);
- (* (CicPp.pp (Inference.term_of_equality current) names));*)
+ prerr_endline
+ ("Selected = " ^ (string_of_sign sign) ^ " " ^
+ string_of_equality ~env current);
+(* ^
+ (let w,p,(t,l,r,o),m = current in
+ " size w: " ^ string_of_int (HExtlib.estimate_size w)^
+ " size p: " ^ string_of_int (HExtlib.estimate_size p)^
+ " size t: " ^ string_of_int (HExtlib.estimate_size t)^
+ " size l: " ^ string_of_int (HExtlib.estimate_size l)^
+ " size r: " ^ string_of_int (HExtlib.estimate_size r)^
+ " size o: " ^ string_of_int (HExtlib.estimate_size o)^
+ " size m: " ^ string_of_int (HExtlib.estimate_size m)^
+ " size m-c: " ^ string_of_int
+ (HExtlib.estimate_size (List.map (fun (x,_,_) -> x) m)))) *)
let time1 = Unix.gettimeofday () in
let res = forward_simplify env (sign, current) ~passive active in
let time2 = Unix.gettimeofday () in
(* weight_age_counter := !weight_age_counter + 1; *)
given_clause_fullred dbd env goals theorems passive active
| Some (sign, current) ->
+ if test (sign, current) then
+ (prerr_endline
+ ("Simplified = " ^ (string_of_sign sign) ^ " " ^
+ string_of_equality ~env current);
+ let active = fst active in
+ let s = Printf.sprintf "actives:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ active)))
+ in prerr_endline s;
+ assert false);
if (sign = Negative) && (is_identity env current) then (
debug_print
(lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current)));
- let _, proof, _, _ = current in
+ let _, proof, _, m = current in
ParamodulationSuccess (Some proof, env)
) else (
debug_print
let t1 = Unix.gettimeofday () in
let new' = infer env sign current active in
- let _ =
+ let _ =
match new' with
| neg, pos ->
debug_print
in
let rec simplify new' active passive =
let t1 = Unix.gettimeofday () in
- let new' = forward_simplify_new env new' ~passive active in
+ let new' = forward_simplify_new env new'~passive active in
let t2 = Unix.gettimeofday () in
forward_simpl_new_time :=
!forward_simpl_new_time +. (t2 -. t1);
let t1 = Unix.gettimeofday () in
let active, passive, newa, retained =
- backward_simplify env new' ~passive active in
+ backward_simplify env new' ~passive active in
+
let t2 = Unix.gettimeofday () in
backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
match newa, retained with
| Some (n, p), None
| None, Some (n, p) ->
let nn, np = new' in
- if Utils.debug_metas then
- ignore (
- List.map (fun x -> Indexing.check_target context x "simplify1")n;
- List.map (fun x -> Indexing.check_target context x "simplify2")p);
- simplify (nn @ n, np @ p) active passive
+ if Utils.debug_metas then
+ begin
+ List.iter
+ (fun x->Indexing.check_target context x "simplify1")
+ n;
+ List.iter
+ (fun x->Indexing.check_target context x "simplify2")
+ p
+ end;
+ simplify (nn @ n, np @ p) active passive
| Some (n, p), Some (rn, rp) ->
let nn, np = new' in
simplify (nn @ n @ rn, np @ p @ rp) active passive
in
- let active, passive, new' = simplify new' active passive in
+ let active, _, new' = simplify new' active passive in
(* pessima prova
- let new1 = prova env new' active in
+ let new1 = prova env new' active in
let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in
let _ =
match new1 with
in
ParamodulationSuccess (proof, env)
)
+
;;
+let profiler0 = HExtlib.profile "P/Saturation.given_clause_fullred"
+
+let given_clause_fullred dbd env goals theorems passive active =
+ profiler0.HExtlib.profile
+ (given_clause_fullred dbd env goals theorems passive) active
+
let rec saturate_equations env goal accept_fun passive active =
elapsed_time := Unix.gettimeofday () -. !start_time;
(fst theorems)))))
in
(*try*)
- let goal = Inference.BasicProof new_meta_goal, [], goal in
+ let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
let equalities = simplify_equalities env
(equalities@library_equalities) in
let active = make_active () in
start_time := Unix.gettimeofday ();
let res =
let goals = make_goals goal in
- (if !use_fullred then given_clause_fullred else given_clause)
+ (if !use_fullred then given_clause_fullred else given_clause_fullred)
dbd env goals theorems passive active
in
let finish = Unix.gettimeofday () in
| ParamodulationSuccess (None, env) ->
Printf.printf "Success, but no proof?!?\n\n"
in
- if Utils.time then
- begin
- prerr_endline
- ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+ if Utils.time then
+ begin
+ prerr_endline
+ ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
"forward_simpl_new_time: %.9f\n" ^^
"backward_simpl_time: %.9f\n")
!infer_time !forward_simpl_time !forward_simpl_new_time
!backward_simpl_time) ^
- (Printf.sprintf "beta_expand_time: %.9f\n"
- !Indexing.beta_expand_time) ^
- (Printf.sprintf "passive_maintainance_time: %.9f\n"
- !passive_maintainance_time) ^
- (Printf.sprintf " successful unification/matching time: %.9f\n"
- !Indexing.match_unif_time_ok) ^
- (Printf.sprintf " failed unification/matching time: %.9f\n"
- !Indexing.match_unif_time_no) ^
- (Printf.sprintf " indexing retrieval time: %.9f\n"
- !Indexing.indexing_retrieval_time) ^
- (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n"
- !Indexing.build_newtarget_time) ^
- (Printf.sprintf "derived %d clauses, kept %d clauses.\n"
- !derived_clauses !kept_clauses))
- end
+ (Printf.sprintf "beta_expand_time: %.9f\n"
+ !Indexing.beta_expand_time) ^
+ (Printf.sprintf "passive_maintainance_time: %.9f\n"
+ !passive_maintainance_time) ^
+ (Printf.sprintf " successful unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_ok) ^
+ (Printf.sprintf " failed unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_no) ^
+ (Printf.sprintf " indexing retrieval time: %.9f\n"
+ !Indexing.indexing_retrieval_time) ^
+ (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n"
+ !Indexing.build_newtarget_time) ^
+ (Printf.sprintf "derived %d clauses, kept %d clauses.\n"
+ !derived_clauses !kept_clauses))
+ end
(*
with exc ->
print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
Inference.metas_of_proof_time := 0.;
;;
-let saturate
+let saturate
dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status =
let module C = Cic in
reset_refs ();
Indexing.init_index ();
maxdepth := depth;
maxwidth := width;
+(* CicUnification.unif_ty := false;*)
let proof, goal = status in
let goal' = goal in
let uri, metasenv, meta_proof, term_to_prove = proof in
let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+ prerr_endline ("CTX: " ^ string_of_int (HExtlib.estimate_size context));
let eq_indexes, equalities, maxm = find_equalities context proof in
let new_meta_goal, metasenv, type_of_goal =
let irl =
ty
in
let ugraph = CicUniv.empty_ugraph in
- let env = (metasenv, context, ugraph) in
- let goal = Inference.BasicProof new_meta_goal, [], goal in
+ let env = (metasenv, context, ugraph) in
+ let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
let res, time =
let t1 = Unix.gettimeofday () in
let lib_eq_uris, library_equalities, maxm =
(res, finish -. start)
in
match res with
- | ParamodulationSuccess (Some proof, env) ->
+ | ParamodulationSuccess (Some proof, _) ->
debug_print (lazy "OK, found a proof!");
let proof = Inference.build_proof_term proof in
+ (* prerr_endline (CicPp.ppterm proof); *)
let names = names_of_context context in
let newmetasenv =
let i1 =
let tdemodulate = fs_time_info.demodulate in
let tsubsumption = fs_time_info.subsumption in
if Utils.time then
- begin
- prerr_endline (
- (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^
- (Printf.sprintf "\ntall: %.9f" tall) ^
- (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
- (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
- (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
- (Printf.sprintf "\nbeta_expand_time: %.9f\n"
- !Indexing.beta_expand_time) ^
- (Printf.sprintf "\nmetas_of_proof: %.9f\n"
- !Inference.metas_of_proof_time) ^
- (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
- (Printf.sprintf "\nforward_simpl_new_times: %.9f"
- !forward_simpl_new_time) ^
- (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^
- (Printf.sprintf "\npassive_maintainance_time: %.9f"
- !passive_maintainance_time))
- end;
+ begin
+ prerr_endline (
+ (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^
+ (Printf.sprintf "\ntall: %.9f" tall) ^
+ (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
+ (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
+ (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
+ (Printf.sprintf "\nbeta_expand_time: %.9f\n"
+ !Indexing.beta_expand_time) ^
+ (Printf.sprintf "\nmetas_of_proof: %.9f\n"
+ !Inference.metas_of_proof_time) ^
+ (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
+ (Printf.sprintf "\nforward_simpl_new_times: %.9f"
+ !forward_simpl_new_time) ^
+ (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^
+ (Printf.sprintf "\npassive_maintainance_time: %.9f"
+ !passive_maintainance_time))
+ end;
newstatus
| _ ->
raise (ProofEngineTypes.Fail (lazy "NO proof found"))
debug_print
(lazy
(Printf.sprintf "\n\nequalities:\n%s\n"
- (String.concat "\n"
+ (String.concat "\n"
(List.map
- (fun (u, e) ->
-(* Printf.sprintf "%s: %s" *)
- (UriManager.string_of_uri u)
-(* (string_of_equality e) *)
- )
- equalities))));
+ (fun (u, e) ->
+(* Printf.sprintf "%s: %s" *)
+ (UriManager.string_of_uri u)
+(* (string_of_equality e) *)
+ )
+ equalities))));
debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
let rec simpl e others others_simpl =
let (u, e) = e in
let res = forward_simplify env (Positive, e) (active, tbl) in
match others with
| hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
- )
+ match res with
+ | None -> simpl hd tl others_simpl
+ | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
+ )
| [] -> (
- match res with
- | None -> others_simpl
- | Some e -> (u, (snd e))::others_simpl
- )
+ match res with
+ | None -> others_simpl
+ | Some e -> (u, (snd e))::others_simpl
+ )
in
let _equalities =
match equalities with
| [] -> []
| hd::tl ->
- let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
- let res =
- List.rev (simpl (*(Positive,*) hd others [])
- in
- debug_print
- (lazy
- (Printf.sprintf "\nequalities AFTER:\n%s\n"
- (String.concat "\n"
- (List.map
- (fun (u, e) ->
- Printf.sprintf "%s: %s"
- (UriManager.string_of_uri u)
- (string_of_equality e)
- )
- res))));
- res in
+ let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
+ let res =
+ List.rev (simpl (*(Positive,*) hd others [])
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "\nequalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+ Printf.sprintf "%s: %s"
+ (UriManager.string_of_uri u)
+ (string_of_equality e)
+ )
+ res))));
+ res in
debug_print
(lazy
(Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
in
let env = (metasenv, context, ugraph) in
(*try*)
- let goal = Inference.BasicProof new_meta_goal, [], goal in
+ let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
let equalities = simplify_equalities env (equalities@library_equalities) in
let active = make_active () in
let passive = make_passive [] equalities in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let library_equalities = List.map snd library_equalities in
let goalterm = Cic.Meta (metano,irl) in
- let initgoal = Inference.BasicProof goalterm, [], ty in
+ let initgoal = Inference.BasicProof ([],goalterm), [], ty in
let env = (metasenv, context, CicUniv.empty_ugraph) in
let equalities = simplify_equalities env (equalities@library_equalities) in
let table =
begin
let opengoal = Cic.Meta(maxm,irl) in
let proofterm =
- Inference.build_proof_term ~noproof:opengoal newproof in
+ Inference.build_proof_term ~noproof:opengoal newproof in
let extended_metasenv = (maxm,context,newty)::metasenv in
- let extended_status =
- (curi,extended_metasenv,pbo,pty),goal in
- let (status,newgoals) =
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm)
- extended_status in
- (status,maxm::newgoals)
+ let extended_status =
+ (curi,extended_metasenv,pbo,pty),goal in
+ let (status,newgoals) =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm)
+ extended_status in
+ (status,maxm::newgoals)
end
else if newty = ty then
raise (ProofEngineTypes.Fail (lazy "no progress"))
projects / helm.git / blobdiff