active, passive, newa, newp *)
;;
-
let close env new' given =
let new_pos, new_table, min_weight =
List.fold_left
*)
match ty with
| Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
- when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
+ when UriManager.eq uri (Utils.eq_URI ()) ->
(let goal_equation =
Equality.mk_equality
(0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv)
(* 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
+ let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
match fst goals with
| (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])::_
when left = right && iseq uri ->
(given_clause_fullred dbd env goals theorems passive) active
*)
-let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ());;
+let iseq uri = UriManager.eq uri (Utils.eq_URI ());;
let check_if_goal_is_identity env = function
| (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])
when left = right && iseq uri ->
let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
Some (goalproof, reflproof, 0, Subst.empty_subst,m)
+ | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])
+ when iseq uri ->
+ (let _,context,_ = env in
+ try
+ let s,m,_ =
+ Inference.unification m m context left right CicUniv.empty_ugraph
+ in
+ let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
+ let m = Subst.apply_subst_metasenv s m in
+ Some (goalproof, reflproof, 0, s,m)
+ with _ -> None)
| _ -> None
;;
(fun acc goal ->
match simplify_goal env goal ~passive active with
| _, g -> if find g acc then acc else g::acc)
+ (* active_goals active_goals *)
[] active_goals
in
if List.length active_goals <> List.length simplified then
let infer_goal_set_with_current env current goals =
let active_goals, passive_goals = goals in
let _,table,_ = build_table [current] in
+ let _,_,_,_,id = Equality.open_equality current in
active_goals,
List.fold_left
(fun acc g ->
let new' = Indexing.superposition_left env table g in
+ if id = 2 then
+ begin
+ prerr_endline "XXXXXXX";
+ List.iter (fun _,_,e -> prerr_endline (CicPp.ppterm e)) new' ;
+ end;
acc @ new')
passive_goals active_goals
;;
let given_clause
((_,context,_) as env) goals theorems passive active max_iterations max_time
=
+ let names = names_of_context context in
let initial_time = Unix.gettimeofday () in
let iterations_left iterno =
let now = Unix.gettimeofday () in
(ParamodulationFailure "No more time to spend")
else
let _ = prerr_endline "simpl goal with active" in
+ let _ = <:start<simplify goal set active>> in
let goals = simplify_goal_set env goals passive active in
+ let _ = <:stop<simplify goal set active>> in
match check_if_goals_set_is_solved env active goals with
| Some p ->
prerr_endline
ParamodulationFailure "No more passive"(*maybe this is a success! *)
else
begin
+ let goals = infer_goal_set env active goals in
+ let goals = infer_goal_set env active goals in
let goals = infer_goal_set env active goals in
let current, passive = select env goals passive in
+ let _,_,goaltype = List.hd (fst goals) in
+ prerr_endline (Printf.sprintf "Current goal = %s\n"
+ (CicPp.pp goaltype names));
prerr_endline (Printf.sprintf "Selected = %s\n"
(Equality.string_of_equality ~env current));
(* SIMPLIFICATION OF CURRENT *)
let res =
- forward_simplify env (Positive, current) ~passive active
+ forward_simplify env (Positive, current) (*~passive*) active
in
match res with
| None -> step goals theorems passive active (iterno+1)
| Some p, Some rp -> simplify (new' @ p @ rp) active passive
in
let active, passive, new' = simplify new' active passive in
+ if iterno = 36 || iterno = 654 then
+ begin
+ prerr_endline "...................";
+ List.iter
+ (fun x -> prerr_endline (Equality.string_of_equality
+~env:env x)) new';
+ prerr_endline "FINE...................";
+ end;
prerr_endline "simpl goal with new";
let goals =
let a,b,_ = build_table new' in
+ let _ = <:start<simplify_goal_set new>> in
+ <:stop<simplify_goal_set new
simplify_goal_set env goals passive (a,b)
+ >>
in
let passive = add_to_passive passive new' in
step goals theorems passive active (iterno+1)
context_hyp @ thms, []
else
let refl_equal =
- let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+ let us = UriManager.string_of_uri (Utils.eq_URI ()) in
UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
in
let t = CicUtil.term_of_uri refl_equal in
~newmetasenv:metasenv ~oldmetasenv:proof_menv)
in
let goal_proof, side_effects_t =
- let initial = newproof in
+ let initial = Equality.add_subst subsumption_subst newproof in
Equality.build_goal_proof goalproof initial type_of_goal side_effects
in
-(*prerr_endline (CicPp.pp goal_proof names);*)
let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+ let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
+(*prerr_endline (CicPp.pp goal_proof names);*)
+ (* ?? *)
+ let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
let side_effects_t =
List.map (Subst.apply_subst subsumption_subst) side_effects_t
in
| None ->
[i,context,ty], (Cic.Meta(i,[]))::acc2,
(Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl)))
- ([],[],[],None) proof_menv
+ ([],[],[],None)
+ (List.filter
+ (fun (i,_,_) -> List.mem i metas_still_open_in_proof)
+ proof_menv)
in
let replace where =
(* we need this fake equality since the metas of the hypothesis may be
projects / helm.git / blobdiff