X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=f8b0ff45fcc088dcc5c799c93e8831c9be2f3b2b;hb=e1f0bb910f75b8b21f2c5e394ebb4c5a63ef4945;hp=b2348f732a0b014fa26d515e28b8b9cb0401bd57;hpb=0de62d69d01f334e0300633d22b63c91edd8fc7f;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index b2348f732..f8b0ff45f 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -1294,10 +1294,10 @@ let fix_proof metasenv context all_implicits p = aux metasenv 0 p ;; -let fix_metasenv metasenv context = +let fix_metasenv metasenv = List.fold_left (fun m (i,c,t) -> - let m,t = fix_proof m context false t in + let m,t = fix_proof m c false t in let m = List.filter (fun (j,_,_) -> j<>i) m in (i,c,t)::m) metasenv metasenv @@ -1319,7 +1319,7 @@ let build_proof 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 uri, metasenv, _subst, meta_proof, term_to_prove, attrs = 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 @@ -1338,33 +1338,42 @@ let build_proof (ProofEngineHelpers.compare_metasenvs ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in let goal_proof, side_effects_t = - let initial = (* Equality.add_subst subsumption_subst*) newproof in + 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 +(* Equality.draw_proof bag names goalproof newproof subsumption_id; *) let goal_proof = Subst.apply_subst subsumption_subst goal_proof in - let real_menv = fix_metasenv (proof_menv@metasenv) context in + let real_menv = fix_metasenv (proof_menv@metasenv) 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 pp_error goal_proof names error exn = + prerr_endline "THE PROOF DOES NOT TYPECHECK! "; + prerr_endline (CicPp.pp goal_proof names); + prerr_endline "THE PROOF DOES NOT TYPECHECK!"; + prerr_endline error; + prerr_endline "THE PROOF DOES NOT TYPECHECK! "; + raise exn + in let goal_proof,goal_ty,real_menv,_ = (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *) try + prerr_endline (CicPp.ppterm goal_proof); CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph with - | CicUtil.Meta_not_found _ - | CicRefine.RefineFailure _ - | CicRefine.Uncertain _ - | CicRefine.AssertFailure _ + | CicRefine.RefineFailure s + | CicRefine.Uncertain s + | CicRefine.AssertFailure s as exn -> + pp_error goal_proof names (Lazy.force s) exn + | CicUtil.Meta_not_found i as exn -> + pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn | 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 + pp_error goal_proof names "Invalid_argument: list_fold_left2" exn in let subst_side_effects,real_menv,_ = try @@ -1385,7 +1394,7 @@ let build_proof *) let proof, real_metasenv = ProofEngineHelpers.subst_meta_and_metasenv_in_proof - proof goalno (CicMetaSubst.apply_subst final_subst) + proof goalno final_subst (List.filter (fun i,_,_ -> i<>goalno ) real_menv) in let open_goals = @@ -1531,15 +1540,17 @@ let build_proof let pump_actives context bag maxm active passive saturation_steps max_time = reset_refs(); maxmeta := maxm; +(* let max_l l = List.fold_left (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in List.fold_left (fun acc (i,_,_) -> max i acc) acc menv) 0 l in - let active_l = fst active in - let passive_l = fst passive in - let ma = max_l active_l in - let mp = max_l passive_l in +*) +(* let active_l = fst active in *) +(* let passive_l = fst passive in *) +(* let ma = max_l active_l in *) +(* let mp = max_l passive_l in *) match LibraryObjects.eq_URI () with | None -> active, passive, !maxmeta | Some eq_uri -> @@ -1557,7 +1568,7 @@ let pump_actives context bag maxm active passive saturation_steps max_time = let all_subsumed bag maxm status active passive = maxmeta := maxm; let proof, goalno = status in - let uri, metasenv, meta_proof, term_to_prove = proof in + let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let env = metasenv,context,CicUniv.empty_ugraph in let cleaned_goal = Utils.remove_local_context type_of_goal in @@ -1591,18 +1602,20 @@ let given_clause = reset_refs(); maxmeta := maxm; + let active_l = fst active in +(* let max_l l = List.fold_left (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in List.fold_left (fun acc (i,_,_) -> max i acc) acc menv) 0 l in - let active_l = fst active in let passive_l = fst passive in let ma = max_l active_l in let mp = max_l passive_l in +*) let proof, goalno = status in - let uri, metasenv, meta_proof, term_to_prove = proof in + let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in let cleaned_goal = Utils.remove_local_context type_of_goal in