X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=ff58512ea9d1f47c429d6f0f6b412fc5c96b4165;hb=f809c7537eda20a275b17bc1407f0ee446f70356;hp=d9472601c958c96b62526c9af50c11e1ac5a6f9b;hpb=cee1c02ad6a113b711b9d93176296cf16b9ec351;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index d9472601c..ff58512ea 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -1280,15 +1280,24 @@ let fix_proof metasenv context all_implicits p = let metasenv,s = aux metasenv n s in let metasenv,t = aux metasenv (n+1) t in metasenv,Cic.LetIn(name,s,t) + | Cic.Const(uri,ens) -> + let metasenv,ens = + List.fold_right + (fun (v,a) (metasenv,ens) -> + let metasenv,a' = aux metasenv n a in + metasenv,(v,a')::ens) + ens (metasenv,[]) + in + metasenv,Cic.Const(uri,ens) | t -> metasenv,t in 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 @@ -1310,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, 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 @@ -1334,28 +1343,37 @@ let build_proof 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 @@ -1522,16 +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 - assert (maxm > max ma mp); +*) +(* 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 -> @@ -1549,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, 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 @@ -1583,19 +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 - assert (maxm > max ma mp); +*) let proof, goalno = status in - let uri, metasenv, meta_proof, term_to_prove = proof in + let uri, metasenv, 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