;;
let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-(*
let names = names_of_context ctx in
+(*
Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
*)
match ty with
match Indexing.unification env table goal_equation with
| Some (subst, equality, swapped ) ->
prerr_endline
- ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
- prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
+ ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env);
+ prerr_endline
+ ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env);
+ prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst);
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 new_passive_goals =
if Utils.metas_of_term t1 = [] then passive_goals
else
- let new' =
- Indexing.superposition_left env (snd active) selected in
+ let newmaxmeta,new' =
+ Indexing.superposition_left env (snd active) selected
+ !maxmeta
+ in
+ maxmeta := newmaxmeta;
passive_goals @ new'
in
selected::active_goals, new_passive_goals
active_goals,
List.fold_left
(fun acc g ->
- let new' = Indexing.superposition_left env table g in
+ let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in
+ maxmeta := newmaxmeta;
acc @ new')
passive_goals active_goals
;;
prerr_endline
(Equality.pp_proof names goalproof newproof subsumption_subst
subsumption_id type_of_goal);
- prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
prerr_endline "ENDOFPROOFS";
(* generation of the CIC proof *)
let side_effects =
Equality.build_goal_proof
eq_uri goalproof initial type_of_goal side_effects
in
+ prerr_endline ("PROOF: " ^ 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 t = Equality.term_of_equality eq_uri e in
prerr_endline (CicPp.pp t names))
eql;
+ prerr_endline ("\n result proofs: ");
+ List.iter (fun e ->
+ prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
+ let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
+ Subst.ppsubst s ^ "\n" ^
+ CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql;
if demod_table <> "" then
begin
let demod =