From dcd3ec87a3bf26fab2856af720bbea5b0209cae5 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 28 Apr 2014 20:34:44 -0400 Subject: Refine check_is_subterm. Following Bruno's suggestion, we check if the tree expected for the recursive argument is included in the one which is inferred. This check is probably not necessary in the current state of affairs, but might become so after further extensions of the guard condition. --- lib/rtree.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'lib/rtree.ml') diff --git a/lib/rtree.ml b/lib/rtree.ml index efcb6aae1..504cc67a0 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -167,6 +167,10 @@ let rec inter cmp interlbl def n histo t t' = let inter cmp interlbl def t t' = inter cmp interlbl def 0 [] t t' +(** Inclusion of rtrees. We may want a more efficient implementation. *) +let incl cmp interlbl def t t' = + equal cmp t (inter cmp interlbl def t t') + (** 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. *) -- cgit v1.2.3