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, args = 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
type theorem = Cic.term * Cic.term * Cic.metasenv;;
-let symbols_of_equality (_, _, (_, left, right, _), _, _) =
+let symbols_of_equality (_, _, (_, left, right, _), _) =
let m1 = symbols_of_term left in
let m =
TermMap.fold
m
;;
-module OrderedEquality = struct
+(* griggio *)
+module OrderedEquality = struct
type t = Inference.equality
let compare eq1 eq2 =
match meta_convertibility_eq eq1 eq2 with
| true -> 0
| false ->
- let w1, _, (ty, left, right, _), _, a = eq1
- and w2, _, (ty', left', right', _), _, a' = eq2 in
+ let w1, _, (ty, left, right, _), m1 = eq1
+ and w2, _, (ty', left', right', _), m2 = eq2 in
match Pervasives.compare w1 w2 with
+ | 0 ->
+ let res = (List.length m1) - (List.length m2) in
+ if res <> 0 then res else Pervasives.compare eq1 eq2
+ | res -> res
+end
+
+(*
+module OrderedEquality = struct
+ type t = Inference.equality
+
+ let minor eq =
+ let w, _, (ty, left, right, o), _ = eq in
+ match o with
+ | Lt -> Some left
+ | Le -> assert false
+ | Gt -> Some right
+ | Ge -> assert false
+ | Eq
+ | Incomparable -> None
+
+ let compare eq1 eq2 =
+ let w1, _, (ty, left, right, o1), m1 = eq1
+ and w2, _, (ty', left', right', o2), m2 = eq2 in
+ match Pervasives.compare w1 w2 with
| 0 ->
- let res = (List.length a) - (List.length a') in
- if res <> 0 then res else (
- try
- let res = Pervasives.compare (List.hd a) (List.hd a') in
- if res <> 0 then res else Pervasives.compare eq1 eq2
- with Failure "hd" -> Pervasives.compare eq1 eq2
- )
- | 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
+ | res -> res
end
+*)
module EqualitySet = Set.Make(OrderedEquality);;
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
| [], (hd:EqualitySet.elt)::tl ->
- let w,_,_,_,_ = hd in
let passive_table =
Indexing.remove_index passive_table hd
in (Positive, hd),
| _ ->
symbols_counter := !symbols_ratio;
let set_selection set = EqualitySet.min_elt set in
- (* let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in *)
+ (* let set_selection l = min_elt (fun (w,_,_,_) -> w) l in *)
if EqualitySet.is_empty neg_set then
let current = set_selection pos_set in
let passive =
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 neg, pos = infer_positive table tl in
neg, res @ pos
in
+ let maxm, copy_of_current = Inference.fix_metas !maxmeta current in
+ maxmeta := maxm;
let curr_table = Indexing.index Indexing.empty current in
- let neg, pos = infer_positive curr_table active_list 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 ->
try
let found =
List.find
- (fun (w, proof, (ty, left, right, ordering), m, a) ->
+ (fun (w, proof, (ty, left, right, ordering), m) ->
fst (CicReduction.are_convertible context left right ugraph))
negative
in
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 (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) ->
;;
+(** 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
let active_list, newa =
List.fold_right
(fun (s, equality) (res, newn) ->
- let ew, _, _, _, _ = equality in
+ let ew, _, _, _ = equality in
if ew < min_weight then
(s, equality)::res, newn
else
let backward_simplify_passive env new_pos new_table min_weight passive =
let (nl, ns), (pl, ps), passive_table = passive in
let f sign equality (resl, ress, newn) =
- let ew, _, _, _, _ = equality in
+ let ew, _, _, _ = equality in
if ew < min_weight then
equality::resl, ress, newn
else
let new_pos, new_table, min_weight =
List.fold_left
(fun (l, t, w) e ->
- let ew, _, _, _, _ = e in
+ let ew, _, _, _ = e in
(Positive, e)::l, Indexing.index t e, min ew w)
([], Indexing.empty, 1000000) (snd new')
in
let new_pos, new_table, min_weight =
List.fold_left
(fun (l, t, w) e ->
- let ew, _, _, _, _ = e in
+ let ew, _, _, _ = e in
(Positive, e)::l, Indexing.index t e, min ew w)
([], Indexing.empty, 1000000) (snd new')
in
;;
let is_commutative_law eq =
- let w, proof, (eq_ty, left, right, order), metas, args = snd eq in
+ 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] ->
;;
-(** 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
let module HL = HelmLibraryObjects in
let module I = Inference in
let metasenv, context, ugraph = env in
- let _, proof, (ty, left, right, _), metas, args = equality in
+ let _, proof, (ty, left, right, _), metas = equality in
let eqterm =
C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
let gproof, gmetas, gterm = goal in
(* (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 *)
debug_print
(lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
(string_of_equality ~env current)));
- let _, proof, _, _, _ = current in
+ let _, proof, _, _ = current in
ParamodulationSuccess (Some proof, env)
) else (
debug_print
if res then
let proof =
match goal' with
- | Some goal -> let _, proof, _, _, _ = goal in Some proof
+ | Some goal -> let _, proof, _, _ = goal in Some proof
| None -> None
in
ParamodulationSuccess (proof, env)
let proof =
match goal with
| Some goal ->
- let _, proof, _, _, _ = goal in Some proof
+ let _, proof, _, _ = goal in Some proof
| None -> None
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
+ | _ -> false, None
+ in
if ok then
- let proof =
+ (* let proof =
match (fst goals) with
- | (_, [proof, _, _])::_ -> Some proof
+ | (_, [proof, m, _])::_ ->
+ prerr_endline (CicMetaSubst.ppmetasenv [] m); Some proof
| _ -> assert false
- in
+ 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"
((List.map
(string_of_equality ~env)
(let x,y,_ = passive in (fst x)@(fst y)))) in
prerr_endline s;
- prerr_endline sp;
+ 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) ^
" #PASSIVES: " ^ string_of_int (size_of_passive passive));
- if (size_of_active active) mod 54 = 0 then
+ 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"
(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);
+ prerr_endline sp); *)
let time1 = Unix.gettimeofday () in
let (_,context,_) = env in
let selection_estimate = get_selection_estimate () in
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
forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
match res with
| None ->
+ (* weight_age_counter := !weight_age_counter + 1; *)
given_clause_fullred dbd env goals theorems passive active
| Some (sign, current) ->
+ if 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
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
| 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
+ 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 new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in
| true, goal ->
let proof =
match goal with
- | Some goal -> let _, proof, _, _, _ = goal in Some proof
+ | Some goal -> let _, proof, _, _ = goal in Some proof
| None -> None
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
print_endline (PP.pp proof names);
let newmetasenv =
List.fold_left
- (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
+ (fun m (_, _, _, menv) -> m @ menv) metasenv equalities
in
let _ =
(*try*)
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 metasenv = (2839,context,Cic.Rel 17)::(214882,context,Cic.Rel 17)::metasenv in
let names = names_of_context context in
let newmetasenv =
let i1 =
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 =
projects / helm.git / blobdiff