From: Enrico Tassi <enrico.tassi@inria.fr>
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