Refining match subterm and commutative cut rules. The parameters that are

instantiated in the return predicate are now taken into account. The resulting
recargs tree is the intersection between the one of the branches and the
appearing in the return predicate. Both the domain and co-domain are filtered.

2 files changed, 20 insertions, 2 deletions

diff --git a/lib/rtree.ml b/lib/rtree.ml
index 5806ebd000..3c900d0b4d 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -145,8 +145,24 @@ let equal cmp t t' =
 (** Deprecated alias *)
 let eq_rtree = equal
 
-(** Tests if a given tree is infinite, i.e. has an branch of infinite length.
-   This correspond to a cycle when visiting the expanded tree.
+(* Intersection of rtrees of same arity *)
+let rec inter interlbl def t t' =
+  match t, t' with
+  | Param (i,j), Param (i',j') ->
+      assert (Int.equal i i' && Int.equal j j'); t
+  | Node (x, a), Node (x', a') ->
+      (match interlbl x x' with
+      | None -> mk_node def [||]
+      | Some x'' -> Node (x'', Array.map2 (inter interlbl def) a a'))
+  | Rec (i, a), Rec (i', a') ->
+      if Int.equal i i' then Rec(i, Array.map2 (inter interlbl def) a a')
+      else mk_node def [||]
+  | Rec _, _ -> inter interlbl def (expand t) t'
+  | _ , Rec _ -> inter interlbl def t (expand t')
+  | _ -> assert false
+
+(** Tests if a given tree is infinite, i.e. has a branch of infinite length.
+   This corresponds to a cycle when visiting the expanded tree.
    We use a specific comparison to detect already seen trees. *)
 
 let is_infinite cmp t =
diff --git a/lib/rtree.mli b/lib/rtree.mli
index c3ec3a0c51..b1cfc35bcc 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -66,6 +66,8 @@ val equiv :
     then by logical equivalence [Rtree.equiv eq eq] *)
 val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
 
+val inter : ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -> 'a t
+
 (** Iterators *)
 
 val map : ('a -> 'b) -> 'a t -> 'b t