| _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
;;
+(* fix proof takes in input a term and try to build a metasenv for it *)
+
+let fix_proof metasenv context all_implicits p =
+ let rec aux metasenv n p =
+ match p with
+ | Cic.Meta (i,_) ->
+ if all_implicits then
+ metasenv,Cic.Implicit None
+ else
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ let meta = CicSubstitution.lift n (Cic.Meta (i,irl)) in
+ let metasenv =
+ try
+ let _ = CicUtil.lookup_meta i metasenv in metasenv
+ with CicUtil.Meta_not_found _ ->
+ prerr_endline ("not found: "^(string_of_int i));
+ let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in
+ (i,context,Cic.Meta(j,irl))::metasenv
+ in
+ metasenv,meta
+ | Cic.Appl l ->
+ let metasenv,l=
+ List.fold_right
+ (fun a (metasenv,l) ->
+ let metasenv,a' = aux metasenv n a in
+ metasenv,a'::l)
+ l (metasenv,[])
+ in metasenv,Cic.Appl l
+ | Cic.Lambda(name,s,t) ->
+ let metasenv,s = aux metasenv n s in
+ let metasenv,t = aux metasenv (n+1) t in
+ metasenv,Cic.Lambda(name,s,t)
+ | Cic.Prod(name,s,t) ->
+ let metasenv,s = aux metasenv n s in
+ let metasenv,t = aux metasenv (n+1) t in
+ metasenv,Cic.Prod(name,s,t)
+ | Cic.LetIn(name,s,t) ->
+ let metasenv,s = aux metasenv n s in
+ let metasenv,t = aux metasenv (n+1) t in
+ metasenv,Cic.LetIn(name,s,t)
+ | t -> metasenv,t
+ in
+ aux metasenv 0 p
+;;
+
+let fix_metasenv metasenv context =
+ List.fold_left
+ (fun m (i,c,t) ->
+ let m,t = fix_proof m context false t in
+ let m = List.filter (fun (j,_,_) -> j<>i) m in
+ (i,c,t)::m)
+ metasenv metasenv
+;;
+
(* status: input proof status
* goalproof: forward steps on goal
* newproof: backward steps
* 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
=
+ if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
+ else prerr_endline (CicMetaSubst.ppmetasenv [] 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"; *)
+ 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 ("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
+ (* generation of the CIC proof *)
+ (* let metasenv' = List.filter (fun i,_,_ -> i<>goalno) metasenv in *)
+ 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
+ let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+ let real_menv = fix_metasenv (proof_menv@metasenv) context in
+ let real_menv,goal_proof =
+ fix_proof real_menv context false goal_proof in
+(*
+ let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in
+ (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
+*)
+ let goal_proof,goal_ty,real_menv,_ =
+ (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
+ try
+ CicRefine.type_of_aux' real_menv 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
+ let subst_side_effects,real_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
+ prerr_endline "+++++++++++++ FINE UNIF";
+ 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 =
+ (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
(* 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 =
+ if proof_menv = [] then prerr_endline "VUOTA";
+ CicMetaSubst.ppmetasenv [] proof_menv;
+ let what, with_what =
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)
+ (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
~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,_ =
- 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
+ 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 ->
- fail "Maybe the local context of metas in the goal was not an IRL" 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
-(* 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
+ proof goalno (CicMetaSubst.apply_subst final_subst)
+ (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
in
- let open_goals =
+ let open_goals =
+ List.map (fun i,_,_ -> i) real_metasenv in
+
+(*
HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof)
- in
+ in *)
(*
match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[]
in
*)
final_subst, proof, open_goals
;;
-
+*)
(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
let passive_l = fst passive in
let ma = max_l active_l in
let mp = max_l passive_l in
- assert (maxm > max ma mp);
- let eq_uri =
- match LibraryObjects.eq_URI () with
- | None -> assert false
- | Some uri -> uri
- in
- let env = [],context,CicUniv.empty_ugraph in
- match
- given_clause bag eq_uri env ([],[]) passive active 0 saturation_steps max_time
- with
- | ParamodulationFailure (_,a,p) ->
- a, p, !maxmeta
- | ParamodulationSuccess _ ->
- assert false
+ assert (maxm > max ma mp);
+ match LibraryObjects.eq_URI () with
+ | None -> active, passive, !maxmeta
+ | Some eq_uri ->
+ let env = [],context,CicUniv.empty_ugraph in
+ (match
+ given_clause bag eq_uri env ([],[])
+ passive active 0 saturation_steps max_time
+ with
+ | ParamodulationFailure (_,a,p) ->
+ a, p, !maxmeta
+ | ParamodulationSuccess _ ->
+ assert false)
;;
let all_subsumed bag maxm status active passive =
let eq_uri = eq_of_goal type_of_goal in
let cleaned_goal = Utils.remove_local_context type_of_goal in
Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
- let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
+ let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in
+ let goal = [], metasenv', cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in
prerr_endline ">>>>>> ACTIVES >>>>>>>>";
List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e))
projects / helm.git / blobdiff