git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 162 insertions, 69 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 691992dec..c299ff553 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -386,7 +386,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
     push_rel (Anonymous,None,
               hnf_prod_applist env (type_of_inductive env specif) lpar) env in
   let ra_env' = 
-    (Imbr mi,Rtree.mk_param 0) ::
+    (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
   (* New index of the inductive types *)
   let newidx = n + auxntyp in
@@ -510,8 +510,8 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
 
 let check_positivity env_ar params inds =
   let ntypes = Array.length inds in
-  let lra_ind =
-    List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in
+  let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in
+  let lra_ind = List.rev (Array.to_list rc) in
   let lparams = rel_context_length params in
   let nmr = rel_context_nhyps params in
   let check_one i (_,lcnames,lc,(sign,_)) =
diff --git a/lib/rtree.ml b/lib/rtree.ml
index bc6555e75..4832fe58d 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -8,9 +8,13 @@
 
 (*i $Id$ 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)++
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 554af8163..db5475b79 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -9,32 +9,71 @@
 (*i $Id$ i*)
 
 (* Type of regular tree with nodes labelled by values of type 'a *)
-
+(* The implementation uses de Bruijn indices, so binding capture
+   is avoided by the lift operator (see example below) *)
 type 'a t 
 
 (* Building trees *)
-(* build a recursive call *) 
-val mk_param : int -> 'a t
+
 (* build a node given a label and the vector of sons *)
 val mk_node  : 'a -> 'a t array -> 'a t
-(* build mutually dependent trees *)
+
+(* Build mutually recursive trees:
+    X_1 = f_1(X_1,..,X_n) ... X_n = f_n(X_1,..,X_n)
+   is obtained by the following pseudo-code
+   let vx = mk_rec_calls n in
+   let [|x_1;..;x_n|] =
+      mk_rec[|f_1(vx.(0),..,vx.(n-1);..;f_n(vx.(0),..,vx.(n-1))|]
+
+  First example: build  rec X = a(X,Y) and Y = b(X,Y,Y)
+  let [|vx;vy|] = mk_rec_calls 2 in
+  let [|x;y|] = mk_rec [|mk_node a [|vx;vy|]; mk_node b [|vx;vy;vy|]|]
+
+  Another example: nested recursive trees rec Y = b(rec X = a(X,Y),Y,Y)
+  let [|vy|] = mk_rec_calls 1 in
+  let [|vx|] = mk_rec_calls 1 in
+  let [|x|] = mk_rec[|mk_node a [|vx;lift 1 vy|]
+  let [|y|] = mk_rec[|mk_node b [|x;vy;vy|]|]
+  (note the lift to avoid
+ *)
+val mk_rec_calls : int -> 'a t array
 val mk_rec   : 'a t array -> 'a t array
 
 (* [lift k t] increases of [k] the free parameters of [t]. Needed
    to avoid captures when a tree appears under [mk_rec] *) 
 val lift : int -> 'a t -> 'a t
 
-val map : ('a -> 'b) -> 'a t -> 'b t
-
-(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
-val smartmap : ('a -> 'a) -> 'a t -> 'a t
-
+val is_node : 'a t -> bool
 (* Destructors (recursive calls are expanded) *)
-val dest_param : 'a t -> int
 val dest_node  : 'a t -> 'a * 'a t array
+(* dest_param is not needed for closed trees (i.e. with no free variable) *)
+val dest_param : 'a t -> int * int
 
 (* Tells if a tree has an infinite branch *)
 val is_infinite : 'a t -> bool
 
+(* [compare_rtree f t1 t2] compares t1 t2 (top-down).
+   f is called on each node: if the result is negative then the
+   traversal ends on false, it is is positive then deeper nodes are
+   not examined, and the traversal continues on respective siblings,
+   and if it is 0, then the traversal continues on sons, pairwise.
+   In this latter case, if the nodes do not have the same number of
+   sons, then the traversal ends on false.
+   In case of loop, the traversal is successful and it resumes on
+   siblings.
+ *)
+val compare_rtree : ('a t -> 'b t -> int) -> 'a t -> 'b t -> bool
+
+val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+
+(* Iterators *)
+
+val map : ('a -> 'b) -> 'a t -> 'b t
+(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
+val smartmap : ('a -> 'a) -> 'a t -> 'a t
+val fold : (bool -> 'a t -> ('a t -> 'b) -> 'b) -> 'a t -> 'b
+val fold2 :
+  (bool -> 'a t -> 'b -> ('a t -> 'b -> 'c) -> 'c) -> 'a t -> 'b -> 'c
+
 (* A rather simple minded pretty-printer *)
 val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds