a skeleton of supright

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 67185a88a41dc404a0f683f47c33958de99b2fb7..6d10c86d8ad01842fe807925f930b898b2ad3acc 100644 (file)
--- 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