Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 111 insertions, 57 deletions

diff --git a/lib/rtree.ml b/lib/rtree.ml
index ab689be1..4742a90d 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -6,11 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rtree.ml 8648 2006-03-18 15:37:14Z herbelin $ i*)
+(*i $Id: rtree.ml 10690 2008-03-18 13:30:04Z barras $ i*)
+
+open Util
 
 
 (* Type of regular trees:
    - Param denotes tree variables (like de Bruijn indices)
+     the first int is the depth of the occurrence, and the second int
+     is the index in the array of trees introduced at that depth
    - Node denotes the usual tree node, labelled with 'a
    - Rec(j,v1..vn) introduces infinite tree. It denotes
      v(j+1) with parameters 0..n-1 replaced by
@@ -19,55 +23,87 @@
      current Rec node (as usual in de Bruijn binding system)
  *)
 type 'a t =
-    Param of int 
+    Param of int * int
   | Node of 'a * 'a t array
   | Rec of int * 'a t array
 
 (* Building trees *)
-let mk_param i = Param i
+let mk_rec_calls i = Array.init i (fun j -> Param(0,j))
 let mk_node lab sons = Node (lab, sons)
 
-(* Given a vector of n bodies, builds the n mutual recursive trees.
-   Recursive calls are made with parameters 0 to n-1. We check
-   the bodies actually build something by checking it is not
-   directly one of the parameters 0 to n-1. *)
-let mk_rec defs =
-  Array.mapi
-    (fun i d ->
-      (match d with
-          Param k when k < Array.length defs -> failwith "invalid rec call"
-        | _ -> ());
-      Rec(i,defs))
-    defs
-
 (* The usual lift operation *)
 let rec lift_rtree_rec depth n = function
-    Param i -> if i < depth then Param i else Param (i+n)
+    Param (i,j) as t -> if i < depth then t else Param (i+n,j)
   | Node (l,sons) -> Node (l,Array.map (lift_rtree_rec depth n) sons)
   | Rec(j,defs) ->
-      Rec(j, Array.map (lift_rtree_rec (depth+Array.length defs) n) defs)
+      Rec(j, Array.map (lift_rtree_rec (depth+1) n) defs)
 
 let lift n t = if n=0 then t else lift_rtree_rec 0 n t
 
 (* The usual subst operation *)
 let rec subst_rtree_rec depth sub = function
-    Param i ->
-      if i < depth then Param i
-      else if i-depth < Array.length sub then lift depth sub.(i-depth)
-      else Param (i-Array.length sub)
+    Param (i,j) as t ->
+      if i < depth then t
+      else if i-depth < Array.length sub then
+        lift depth sub.(i-depth).(j)
+      else Param (i-Array.length sub,j)
   | Node (l,sons) -> Node (l,Array.map (subst_rtree_rec depth sub) sons)
   | Rec(j,defs) ->
-      Rec(j, Array.map (subst_rtree_rec (depth+Array.length defs) sub) defs)
+      Rec(j, Array.map (subst_rtree_rec (depth+1) sub) defs)
+
+let subst_rtree sub t = subst_rtree_rec 0 [|sub|] t
+
+(* To avoid looping, we must check that every body introduces a node 
+   or a parameter *)
+let rec expand = function
+  | Rec(j,defs) ->
+      let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in
+      expand (subst_rtree sub defs.(j))
+  | t -> t
+
+(* Given a vector of n bodies, builds the n mutual recursive trees.
+   Recursive calls are made with parameters (0,0) to (0,n-1). We check
+   the bodies actually build something by checking it is not
+   directly one of the parameters of depth 0. Some care is taken to
+   accept definitions like  rec X=Y and Y=f(X,Y) *)
+let mk_rec defs =
+  let rec check histo d =
+    match expand d with
+        Param(0,j) when List.mem j histo -> failwith "invalid rec call"
+      | Param(0,j) -> check (j::histo) defs.(j)
+      | _ -> () in
+  Array.mapi (fun i d -> check [i] d; Rec(i,defs)) defs
+(*
+let v(i,j) = lift i (mk_rec_calls(j+1)).(j);;
+let r = (mk_rec[|(mk_rec[|v(1,0)|]).(0)|]).(0);;
+let r = mk_rec[|v(0,1);v(1,0)|];;
+the last one should be accepted
+*)
+
+(* Tree destructors, expanding loops when necessary *)
+let dest_param t = 
+  match expand t with
+      Param (i,j) -> (i,j)
+    | _ -> failwith "Rtree.dest_param"
+
+let dest_node t = 
+  match expand t with
+      Node (l,sons) -> (l,sons)
+    | _ -> failwith "Rtree.dest_node"
+
+let is_node t = 
+  match expand t with
+      Node _ -> true
+    | _ -> false
 
-let subst_rtree sub t = subst_rtree_rec 0 sub t
 
 let rec map f t = match t with
-    Param i -> Param i
+    Param(i,j) -> Param(i,j)
   | Node (a,sons) -> Node (f a, Array.map (map f) sons)
   | Rec(j,defs) -> Rec (j, Array.map (map f) defs)
 
 let rec smartmap f t = match t with
-    Param i -> t
+    Param _ -> t
   | Node (a,sons) -> 
       let a'=f a and sons' = Util.array_smartmap (map f) sons in
 	if a'==a && sons'==sons then
@@ -81,43 +117,61 @@ let rec smartmap f t = match t with
 	else
 	  Rec(j,defs')
 
-(* To avoid looping, we must check that every body introduces a node 
-   or a parameter *)
-let rec expand_rtree = function
-  | Rec(j,defs) ->
-      let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in
-      expand_rtree (subst_rtree sub defs.(j))
-  | t -> t
-
-(* Tree destructors, expanding loops when necessary *)
-let dest_param t = 
-  match expand_rtree t with
-      Param i -> i
-    | _ -> failwith "dest_param"
-
-let dest_node t = 
-  match expand_rtree t with
-      Node (l,sons) -> (l,sons)
-    | _ -> failwith "dest_node"
-
-(* Tests if a given tree is infinite or not. It proceeds *)
-let rec is_infinite = function
-    Param i -> i = (-1)
-  | Node(_,sons) -> Util.array_exists is_infinite sons
-  | Rec(j,defs) ->
-      let newdefs =
-        Array.mapi (fun i def -> if i=j then Param (-1) else def) defs in
-      let sub =
-        Array.init (Array.length defs)
-          (fun i -> if i=j then Param (-1) else Rec(i,newdefs)) in
-      is_infinite (subst_rtree sub defs.(j))
+(* Fixpoint operator on trees:
+   f is the body of the fixpoint. Arguments passed to f are:
+   - a boolean telling if the subtree has already been seen
+   - the current subtree
+   - a function to make recursive calls on subtrees
+ *)
+let fold f t =
+  let rec fold histo t =
+    let seen = List.mem t histo in
+    let nhisto = if not seen then t::histo else histo in
+    f seen (expand t) (fold nhisto) in
+  fold [] t
+
+
+(* Tests if a given tree is infinite, i.e. has an branch of infinte length. *)
+let is_infinite t = fold
+  (fun seen t is_inf ->
+    seen ||
+    (match t with
+        Node(_,v) -> array_exists is_inf v
+      | Param _ -> false
+      | _ -> assert false))
+  t
+
+let fold2 f t x =
+  let rec fold histo t x =
+    let seen = List.mem (t,x) histo in
+    let nhisto = if not seen then (t,x)::histo else histo in
+    f seen (expand t) x (fold nhisto) in
+  fold [] t x
+
+let compare_rtree f = fold2
+  (fun seen t1 t2 cmp ->
+    seen ||
+    let b = f t1 t2 in
+    if b < 0 then false
+    else if b > 0 then true
+    else match expand t1, expand t2 with
+        Node(_,v1), Node(_,v2) when Array.length v1 = Array.length v2 ->
+          array_for_all2 cmp v1 v2
+      | _ -> false)
+
+let eq_rtree cmp t1 t2 =
+  t1 == t2 || t1=t2 ||
+  compare_rtree
+    (fun t1 t2 ->
+      if cmp (fst(dest_node t1)) (fst(dest_node t2)) then 0
+      else (-1)) t1 t2
 
 (* Pretty-print a tree (not so pretty) *)
 open Pp
 
 let rec pp_tree prl t =
   match t with
-      Param k -> str"#"++int k
+      Param (i,j) -> str"#"++int i++str","++int j
     | Node(lab,[||]) -> hov 2 (str"("++prl lab++str")")
     | Node(lab,v) ->
         hov 2 (str"("++prl lab++str","++brk(1,0)++