let final_subst =
(goalno,(context,goal_proof,type_of_goal))::subst_side_effects
in
- let real_metasenv = List.filter (fun i,_,_ -> i<>goalno ) real_menv in
- let real_metasenv =
- CicMetaSubst.apply_subst_metasenv final_subst real_metasenv
- in
- let open_goals =
- (ProofEngineHelpers.compare_metasenvs
- ~oldmetasenv:metasenv ~newmetasenv:real_metasenv)
- in
- (* compaction of metas with the same type *)
- let open_goals, final_subst =
- let open_goals_menv_entry =
- List.map
- (fun i -> List.find (fun (j,_,_) -> j = i) real_metasenv)
- open_goals
- in
- let rec compact openg subst = function
- | [] -> openg, subst
- | (i,c,t)::tl ->
- let eq, tl =
- List.partition
- (fun (_,c1,t1) ->
- prerr_endline (CicPp.ppcontext c ^ " /// " ^
- CicPp.ppcontext c1);
- c1 = c && t1 = t) tl
- in
- prerr_endline (string_of_int i ^ " : " ^ CicPp.ppterm t);
- prerr_endline (string_of_int (List.length eq) ^ " .. " ^ string_of_int
- (List.length tl));
- let openg = i::openg in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable c in
- let subst =
- List.fold_left
- (fun subst (j,_,_) -> (j,(c,Cic.Meta(i,irl),t))::subst)
- subst eq
- in
- compact openg subst tl
- in
- compact [] final_subst open_goals_menv_entry
- in
- (* we redoo this to purge collapsed metas *)
- let real_metasenv =
- CicMetaSubst.apply_subst_metasenv final_subst real_metasenv
- 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 final_subst real_metasenv
+ proof goalno final_subst
+ (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
in
+ let open_goals =
+ (ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:real_metasenv) in
+(*
+ let open_goals =
+ List.map (fun i,_,_ -> i) real_metasenv in
+*)
final_subst, proof, open_goals
+
+
+(*
+
+ 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
+ if proof_menv = [] then prerr_endline "VUOTA";
+ CicMetaSubst.ppmetasenv [] proof_menv;
+ let what, with_what =
+ List.fold_left
+ (fun (acc1,acc2) i ->
+ (Cic.Meta(i,[]))::acc1, (Cic.Implicit None)::acc2)
+ ([],[])
+ metas_still_open_in_proof
+(*
+ (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 goal_proof_menv =
+ 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
+ * 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 goal_proof,goal_ty,real_menv,_ =
+ prerr_endline "parte la refine";
+ try
+ CicRefine.type_of_aux' metasenv context goal_proof
+ CicUniv.empty_ugraph
+ with
+ | CicUtil.Meta_not_found _
+ | CicRefine.RefineFailure _
+ | CicRefine.Uncertain _
+ | CicRefine.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
+ prerr_endline "+++++++++++++ METASENV";
+ prerr_endline
+ (CicMetaSubst.ppmetasenv [] real_menv);
+ let subst_side_effects,real_menv,_ =
+(*
+ 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 real_menv
+ goal_ty type_of_goal CicUniv.empty_ugraph
+ with
+ | CicUnification.UnificationFailure s
+ | CicUnification.Uncertain s
+ | CicUnification.AssertFailure s -> assert false
+(* 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
+(*
+ 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)
+ (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
+ in
+ let open_goals =
+ List.map (fun i,_,_ -> i) real_metasenv in
+
+(*
+ 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
;;
+*)
(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
projects / helm.git / commitdiff