diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2014-07-30 23:20:24 -0400 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2014-07-31 01:08:33 -0400 |
commit | 8547814ac99a8f22875ecb3a3f42958e9a82f208 (patch) | |
tree | 580d6a353604295661036854d843c23a3e5361de | |
parent | 72d3f73a4a4596558e06535cbc27ec4a871cc1f8 (diff) |
Improve intersection of regular trees.
For better efficiency, we try to preserve the shape of mutually recursive
trees.
-rw-r--r-- | lib/rtree.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/lib/rtree.ml b/lib/rtree.ml index 504cc67a0..228cf0fd5 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -157,10 +157,15 @@ let rec inter cmp interlbl def n histo t t' = (match interlbl x x' with | None -> mk_node def [||] | Some x'' -> Node (x'', Array.map2 (inter cmp interlbl def n histo) a a')) - (* Mutually recursive trees are transformed into nested trees *) - | Rec _, Rec _ -> - let histo = ((t,t'),(n,0))::histo in - Rec(0, [|inter cmp interlbl def (n+1) histo (expand t) (expand t')|]) + | Rec (i,v), Rec (i',v') -> + (* If possible, we preserve the shape of input trees *) + if Int.equal i i' && Int.equal (Array.length v) (Array.length v') then + let histo = ((t,t'),(n,i))::histo in + Rec(i, Array.map2 (inter cmp interlbl def (n+1) histo) v v') + else + (* Otherwise, mutually recursive trees are transformed into nested trees *) + let histo = ((t,t'),(n,0))::histo in + Rec(0, [|inter cmp interlbl def (n+1) histo (expand t) (expand t')|]) | Rec _, _ -> inter cmp interlbl def n histo (expand t) t' | _ , Rec _ -> inter cmp interlbl def n histo t (expand t') | _ -> assert false |