From 8547814ac99a8f22875ecb3a3f42958e9a82f208 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 30 Jul 2014 23:20:24 -0400 Subject: Improve intersection of regular trees. For better efficiency, we try to preserve the shape of mutually recursive trees. --- lib/rtree.ml | 13 +++++++++---- 1 file 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 -- cgit v1.2.3