From: Enrico Tassi Date: Mon, 8 Jun 2009 17:27:16 +0000 (+0000) Subject: a skeleton of supright X-Git-Tag: make_still_working~3906 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a631b7a0a43b178eb7f68efb4345302441067dcd;p=helm.git a skeleton of supright --- diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 67185a88a..6d10c86d8 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -14,6 +14,8 @@ module Superposition (B : Terms.Blob) = struct module IDX = Index.Index(B) + module Unif = FoUnif.Founif(B) + module Subst = FoSubst.Subst(B) let all_positions t f = let rec aux pos ctx = function @@ -34,20 +36,41 @@ module Superposition (B : Terms.Blob) = aux [] (fun x -> x) t ;; - let superposition_right table subterm pos context = - let _cands = IDX.DT.retrieve_unifiables table subterm in - assert false;; -(* - for every cand in cands - let subst = FoUnif.unify l_can t - (apply_subst subst (c r_cand)), pos, id_cand, subst -*) + let superposition_right table varlist subterm pos context = + let cands = IDX.DT.retrieve_unifiables table subterm in + HExtlib.filter_map + (fun (dir, (id,lit,vl,_)) -> + match lit with + | Terms.Predicate _ -> assert false + | Terms.Equation (l,r,_,o) -> + let side, newside = if dir=Terms.Left2Right then l,r else r,l in + try + let subst, varlist = + Unif.unification (varlist@vl) [] subterm side + in + Some (context newside, subst, varlist, id, pos, dir) + with FoUnif.UnificationFailure _ -> None) + (IDX.ClauseSet.elements cands) + ;; - let superposition_right_step bag (_,selected,_,_) table = + let superposition_right_step bag (id,selected,vl,_) table = match selected with | Terms.Predicate _ -> assert false - | Terms.Equation (l,r,_,Terms.Lt) -> - let _r's = all_positions r (superposition_right table) in + | Terms.Equation (l,r,ty,Terms.Lt) -> + let res = all_positions r (superposition_right table vl) in + let _new_clauses = + List.map + (fun (r,subst,vl,id2,pos,dir) -> + let proof = + Terms.Step(Terms.SuperpositionRight,id,id2, dir, pos, subst) + in + let r = Subst.apply_subst subst r in + let l = Subst.apply_subst subst l in + let ty = Subst.apply_subst subst ty in + (0, Terms.Equation (l,r,ty,Terms.Incomparable), vl, proof)) + res + in + (* fresh ID and metas and compute orientataion of new_clauses *) assert false | Terms.Equation (l,r,_,Terms.Gt) -> assert false | _ -> assert false