some optimizations...

[helm.git] / helm / ocaml / paramodulation / inference.ml

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 00e543c2e6d182e3f0cf05b4baa12b783aef99d6..e79d78e846cac9677d6280cba0f78cf3a6e45b07 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1214,3 +1214,25 @@ let subsumption env target source =
     );
     res
 ;;
+
+
+let extract_differing_subterms t1 t2 =
+  let module C = Cic in
+  let rec aux t1 t2 =
+    match t1, t2 with
+    | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
+        [(t1, t2)]
+    | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
+        let res = List.concat (List.map2 aux tl1 tl2) in
+        if h1 <> h2 then
+          if res = [] then [(h1, h2)] else [(t1, t2)]
+        else
+          if List.length res > 1 then [(t1, t2)] else res
+    | t1, t2 ->
+        if t1 <> t2 then [(t1, t2)] else []
+  in
+  let res = aux t1 t2 in
+  match res with
+  | hd::[] -> Some hd
+  | _ -> None
+;;