+let eq_of_goal = function
+ | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
+ uri
+ | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
+;;
+
+let eq_and_ty_of_goal = function
+ | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
+ uri,t
+ | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
+;;
+
+(* status: input proof status
+ * goalproof: forward steps on goal
+ * newproof: backward steps
+ * subsumption_id: the equation used if goal is closed by subsumption
+ * (0 if not closed by subsumption) (DEBUGGING: can be safely removed)
+ * subsumption_subst: subst to make newproof and goalproof match
+ * proof_menv: final metasenv
+ *)
+let build_proof
+ bag status
+ goalproof newproof subsumption_id subsumption_subst proof_menv
+=
+ let proof, goalno = status in
+ let uri, metasenv, meta_proof, term_to_prove = proof in
+ let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+ let eq_uri = eq_of_goal type_of_goal in
+ let names = Utils.names_of_context context in
+ prerr_endline "Proof:";
+ prerr_endline
+ (Equality.pp_proof bag names goalproof newproof subsumption_subst
+ subsumption_id type_of_goal);
+(* prerr_endline "ENDOFPROOFS"; *)
+(*
+ prerr_endline ("max weight: " ^
+ (string_of_int (Equality.max_weight goalproof newproof)));
+*)
+ (* generation of the CIC proof *)
+ let side_effects =
+ List.filter (fun i -> i <> goalno)
+ (ProofEngineHelpers.compare_metasenvs
+ ~newmetasenv:metasenv ~oldmetasenv:proof_menv)
+ in
+ let goal_proof, side_effects_t =
+ let initial = Equality.add_subst subsumption_subst newproof in
+ Equality.build_goal_proof bag
+ eq_uri goalproof initial type_of_goal side_effects
+ context proof_menv
+ 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 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
+ (* replacing fake mets with real ones *)
+ (* prerr_endline "replacing metas..."; *)
+ let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let goal_proof_menv, what, with_what,free_meta =
+ List.fold_left
+ (fun (acc1,acc2,acc3,uniq) (i,_,ty) ->
+ match uniq with
+ | Some m ->
+(* acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq *)
+ (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2,
+ (Cic.Meta(i,irl))::acc3, uniq
+ | None ->
+ [i,context,ty], (Cic.Meta(i,[]))::acc2,
+ (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl)))
+ ([],[],[],None)
+ (List.filter
+ (fun (i,_,_) ->
+ List.mem i metas_still_open_in_proof
+ (*&& not(List.mem i metas_still_open_in_goal)*))
+ proof_menv)
+ in
+ let replace where =
+ (* we need this fake equality since the metas of the hypothesis may be
+ * with a real local context *)
+ ProofEngineReduction.replace_lifting
+ ~equality:(fun x y ->
+ match x,y with Cic.Meta(i,_),Cic.Meta(j,_) -> i=j | _-> false)
+ ~what ~with_what ~where
+ in
+ let goal_proof = replace goal_proof in
+ (* ok per le meta libere... ma per quelle che c'erano e sono rimaste?
+ * what mi pare buono, sostituisce solo le meta farlocche *)
+ let side_effects_t = List.map replace side_effects_t in
+ let free_metas =
+ List.filter (fun i -> i <> goalno)
+ (ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
+ in
+ (* prerr_endline
+ * ("freemetas: " ^
+ * String.concat "," (List.map string_of_int free_metas) ); *)
+ (* check/refine/... build the new proof *)
+ let replaced_goal =
+ ProofEngineReduction.replace
+ ~what:side_effects ~with_what:side_effects_t
+ ~equality:(fun i t -> match t with Cic.Meta(j,_)->j=i|_->false)
+ ~where:type_of_goal
+ in
+ let subst_side_effects,real_menv,_ =
+ let fail t s = raise (ProofEngineTypes.Fail (lazy (t^Lazy.force s))) in
+ let free_metas_menv =
+ List.map (fun i -> CicUtil.lookup_meta i goal_proof_menv) free_metas
+ in
+(*
+ prerr_endline ("XX type_of_goal " ^ CicPp.ppterm type_of_goal);
+ prerr_endline ("XX replaced_goal " ^ CicPp.ppterm replaced_goal);
+ prerr_endline ("XX metasenv " ^
+ CicMetaSubst.ppmetasenv [] (metasenv @ free_metas_menv));
+*)
+ try
+ CicUnification.fo_unif_subst [] context (metasenv @ free_metas_menv)
+ replaced_goal type_of_goal CicUniv.empty_ugraph
+ with
+ | CicUnification.UnificationFailure s
+ | CicUnification.Uncertain s
+ | CicUnification.AssertFailure s ->
+ fail "Maybe the local context of metas in the goal was not an IRL" s
+ in
+ let final_subst =
+ (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
+ in
+(* prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); *)
+ let _ =
+ try
+ CicTypeChecker.type_of_aux' real_menv context goal_proof
+ CicUniv.empty_ugraph
+ with
+ | CicUtil.Meta_not_found _
+ | CicTypeChecker.TypeCheckerFailure _
+ | CicTypeChecker.AssertFailure _
+ | Invalid_argument "list_fold_left2" as exn ->
+ prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+ prerr_endline (CicPp.pp goal_proof names);
+ prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+ raise exn
+ in
+
+ let metas_of_proof = Utils.metas_of_term goal_proof in
+
+ let proof, real_metasenv =
+ ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+ proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
+ in
+ let open_goals =
+ HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof)
+ in
+(*
+ match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[]
+ in
+*)
+(*
+ Printf.eprintf
+ "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n"
+ (String.concat ", " (List.map string_of_int open_goals))
+ (CicMetaSubst.ppmetasenv [] metasenv)
+ (CicMetaSubst.ppmetasenv [] real_metasenv);
+*)
+ final_subst, proof, open_goals
+;;
+
+let find_equalities dbd status smart_flag auto cache =
+ let proof, goalno = status in
+ let _, metasenv,_,_ = proof in
+ let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+ let eq_uri = eq_of_goal type_of_goal in
+ let env = (metasenv, context, CicUniv.empty_ugraph) in
+ let bag = Equality.mk_equality_bag () in
+ let eq_indexes, equalities, maxm, cache =
+ Equality_retrieval.find_context_equalities 0 bag auto context proof cache
+ in
+ prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>";
+ List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
+ prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+ let lib_eq_uris, library_equalities, maxm, cache =
+ Equality_retrieval.find_library_equalities bag
+ auto smart_flag dbd context (proof, goalno) (maxm+2)
+ cache
+ in
+ prerr_endline (">>>>>>>>>> gained from the library >>>>>>>>>>>>" ^
+ string_of_int maxm);
+ List.iter
+ (fun (_,e) -> prerr_endline (Equality.string_of_equality e))
+ library_equalities;
+ prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+ let equalities = List.map snd library_equalities @ equalities in
+ let equalities =
+ simplify_equalities bag eq_uri env equalities
+ in
+ prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
+ List.iter
+ (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
+ prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
+ bag, equalities, cache, maxm
+;;
+
+let close_more bag active maxmeta status smart_flag auto cache =
+ let proof, goalno = status in
+ let _, metasenv,_,_ = proof in
+ let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+ let eq_uri = eq_of_goal type_of_goal in
+ let env = (metasenv, context, CicUniv.empty_ugraph) in
+ let eq_indexes, equalities, maxm, cache =
+ Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache
+ in
+ prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
+ string_of_int maxm);
+ List.iter
+ (fun e -> prerr_endline (Equality.string_of_equality ~env e))
+ equalities;
+ prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+ let equalities =
+ HExtlib.filter_map
+ (fun e -> forward_simplify bag eq_uri env e active)
+ equalities
+ in
+ prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
+ List.iter
+ (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities;
+ prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
+ bag, equalities, cache, maxm
+
+let saturate
+ smart_flag
+ dbd ?(full=false) ?(depth=default_depth) ?(width=default_width)
+ ?(timeout=600.) auto status =