diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-28 20:34:44 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-07-22 18:05:00 -0400 |
| commit | dcd3ec87a3bf26fab2856af720bbea5b0209cae5 (patch) | |
| tree | c92cece474e78d76ab7b4f6e6c67cb190da9aadf /lib/rtree.ml | |
| parent | cc001c2b8d5ababee585cc43e07e0f9089b5d40e (diff) | |
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.
Diffstat (limited to 'lib/rtree.ml')
| -rw-r--r-- | lib/rtree.ml | 4 |
1 files changed, 4 insertions, 0 deletions
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. *) |