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
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
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
| 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 *)
;;
-(** 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 *)
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"
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));
+ 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
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
- (List.iter
- (fun x -> ignore
- (Indexing.check_target context x "simplify1"))
- n;
- List.iter
- (fun x -> ignore
- (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
(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
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 ();
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