X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=7bbc4d43ca7fb7548a6397f08ffc16f473d9c648;hb=81ef66d9ad4cf863a770664190f96653e9777a57;hp=34c601b3558ee15ba9d1bbe90038e7d4d2b4879d;hpb=7fa3bd6487683920f34871688b357f08f67ebb3d;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 34c601b35..7bbc4d43c 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -151,11 +151,11 @@ let check_target bag context target msg = (* try ignore(CicTypeChecker.type_of_aux' - metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph) + metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph) with e -> prerr_endline msg; - prerr_endline (Inference.string_of_proof proof); - prerr_endline (CicPp.ppterm (Inference.build_proof_term proof)); + prerr_endline (Founif.string_of_proof proof); + prerr_endline (CicPp.ppterm (Founif.build_proof_term proof)); prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left)); prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); raise e @@ -246,7 +246,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = ) else let do_match c = let subst', metasenv', ugraph' = - Inference.matching + Founif.matching metasenv metas context term (S.lift lift_amount c) ugraph in Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate) @@ -259,7 +259,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = let res = try do_match c - with Inference.MatchingFailure -> + with Founif.MatchingFailure -> find_matches bag metasenv context ugraph lift_amount term termty tl in if Utils.debug_res then ignore (check_res res "find1"); @@ -267,7 +267,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = else let res = try do_match c - with Inference.MatchingFailure -> None + with Founif.MatchingFailure -> None in if Utils.debug_res then ignore (check_res res "find2"); match res with @@ -292,9 +292,9 @@ let find_matches metasenv context ugraph lift_amount term termty = (* as above, but finds all the matching equalities, and the matching condition - can be either Inference.matching or Inference.unification + can be either Founif.matching or Inference.unification *) -let rec find_all_matches ?(unif_fun=Inference.unification) +let rec find_all_matches ?(unif_fun=Founif.unification) metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in @@ -323,7 +323,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) res::(find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl) with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph @@ -343,7 +343,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph @@ -356,7 +356,7 @@ let find_all_matches find_all_matches ?unif_fun metasenv context ugraph lift_amount term termty l (*prerr_endline "CANDIDATES:"; - List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l; + List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l; prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int (List.length rc));*) ;; @@ -374,9 +374,9 @@ let subsumption_aux use_unification env table target = let metasenv = tmetas in let predicate, unif_fun = if use_unification then - Unification, Inference.unification + Unification, Founif.unification else - Matching, Inference.matching + Matching, Founif.matching in let leftr = match left with @@ -401,10 +401,10 @@ let subsumption_aux use_unification env table target = | None -> ok what leftorright tl | Some s -> Some (s, equation, leftorright <> pos )) with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ -> ok what leftorright tl in - match ok right Utils.Left leftr with + match ok right Utils.Left leftr with | Some _ as res -> res | None -> let rightr = @@ -426,6 +426,61 @@ let unification x y z = subsumption_aux true x y z ;; +let subsumption_aux_all use_unification env table target = + let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in + let _, context, ugraph = env in + let metasenv = tmetas in + let predicate, unif_fun = + if use_unification then + Unification, Founif.unification + else + Matching, Founif.matching + in + let leftr = + match left with + | Cic.Meta _ when not use_unification -> [] + | _ -> + let leftc = get_candidates predicate table left in + find_all_matches ~unif_fun + metasenv context ugraph 0 left ty leftc + in + let rightr = + match right with + | Cic.Meta _ when not use_unification -> [] + | _ -> + let rightc = get_candidates predicate table right in + find_all_matches ~unif_fun + metasenv context ugraph 0 right ty rightc + in + let rec ok_all what leftorright = function + | [] -> [] + | (_, subst, menv, ug, (pos,equation))::tl -> + let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in + try + let other = if pos = Utils.Left then r else l in + let what' = Subst.apply_subst subst what in + let other' = Subst.apply_subst subst other in + let subst', menv', ug' = + unif_fun metasenv m context what' other' ugraph + in + (match Subst.merge_subst_if_possible subst subst' with + | None -> ok_all what leftorright tl + | Some s -> + (s, equation, leftorright <> pos )::(ok_all what leftorright tl)) + with + | Founif.MatchingFailure + | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl) + in + (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr ) +;; + +let subsumption_all x y z = + subsumption_aux_all false x y z +;; + +let unification_all x y z = + subsumption_aux_all true x y z +;; let rec demodulation_aux bag ?from ?(typecheck=false) metasenv context ugraph table lift_amount term = (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*) @@ -601,8 +656,8 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = | Some t -> let newmeta, newtarget = build_newtarget true t in assert (not (Equality.meta_convertibility_eq target newtarget)); - if (Equality.is_weak_identity newtarget) || - (Equality.meta_convertibility_eq target newtarget) then + if (Equality.is_weak_identity newtarget) (* || *) + (*Equality.meta_convertibility_eq target newtarget*) then newmeta, newtarget else demodulation_equality bag ?from eq_uri newmeta env table newtarget @@ -824,7 +879,7 @@ let superposition_right bag if ordering = U.Gt then newgoal, apply_subst s right else apply_subst s left, newgoal in let neworder = !Utils.compare_terms left right in - let newmenv = (* Inference.filter s *) m in + let newmenv = (* Founif.filter s *) m in let stat = (eq_ty, left, right, neworder) in let eq' = let w = Utils.compute_equality_weight stat in @@ -953,7 +1008,7 @@ let build_newgoal bag context goal posu rule expansion = let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in bo, (newgoalproofstep::goalproof) in - let newmetasenv = (* Inference.filter subst *) menv in + let newmetasenv = (* Founif.filter subst *) menv in (newgoalproof, newmetasenv, newterm) ;;