Rtree : cleanup of the comparing code

 * Using generic fold functions was unecessarily obscure
 * No more List.mem and hence indirect use of ocaml generic comparison
 * Rtree.equiv (former Rtree.compare_rtree) has now a less cryptic
   semantic...

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

8 files changed, 102 insertions, 102 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index dfa7d401e4..97958c2b75 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -469,6 +469,14 @@ let dest_subterms p =
 
 let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
 
+let eq_recarg r1 r2 = match r1, r2 with
+  | Norec, Norec -> true
+  | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
+  | Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
+  | _ -> false
+
+let eq_wf_paths = Rtree.equal eq_recarg
+
 (**********************************************************************)
 (* Representation of mutual inductive types in the kernel             *)
 (*
diff --git a/checker/declarations.mli b/checker/declarations.mli
index ab74114d55..a5785b52a3 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -18,6 +18,8 @@ val mk_norec : wf_paths
 val mk_paths : recarg -> wf_paths list array -> wf_paths
 val dest_recarg : wf_paths -> recarg
 val dest_subterms : wf_paths -> wf_paths list array
+val eq_recarg : recarg -> recarg -> bool
+val eq_wf_paths : wf_paths -> wf_paths -> bool
 
 (* Modules *)
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index c26349207c..539a36331f 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -498,13 +498,10 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
       indlc
   in mk_paths (Mrec ind) irecargs
 
-let check_subtree (t1:'a) (t2:'a) =
-  if not (Rtree.compare_rtree (fun t1 t2 ->
-    let l1 = fst(Rtree.dest_node t1) in
-    let l2 = fst(Rtree.dest_node t2) in
-    if l1 = Norec || l1 = l2 then 0 else -1)
-    t1 t2) then
-    failwith "bad recursive trees"
+let check_subtree t1 t2 =
+  let cmp_labels l1 l2 = l1 == Norec || eq_recarg l1 l2 in
+  if not (Rtree.equiv eq_recarg cmp_labels t1 t2)
+  then failwith "bad recursive trees"
 (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*)
 
 let check_positivity env_ar mind params nrecp inds =
diff --git a/checker/inductive.ml b/checker/inductive.ml
index e2c7f30ab8..4dcf3d3f19 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -401,7 +401,7 @@ type subterm_spec =
   | Not_subterm
 
 let spec_of_tree t = lazy
-  (if Rtree.eq_rtree (=) (Lazy.force t) mk_norec
+  (if eq_wf_paths (Lazy.force t) mk_norec
    then Not_subterm
    else Subterm(Strict,Lazy.force t))
 
@@ -413,7 +413,7 @@ let subterm_spec_glb =
       | Not_subterm, _ -> Not_subterm
       | _, Not_subterm -> Not_subterm
       | Subterm (a1,t1), Subterm (a2,t2) ->
-          if Rtree.eq_rtree (=) t1 t2 then Subterm (size_glb a1 a2, t1)
+          if eq_wf_paths t1 t2 then Subterm (size_glb a1 a2, t1)
           (* branches do not return objects with same spec *)
           else Not_subterm in
   Array.fold_left glb2 Dead_code
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e564feb692..e3e636e4aa 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -419,7 +419,7 @@ type subterm_spec =
   | Dead_code
   | Not_subterm
 
-let eq_wf_paths = Rtree.eq_rtree Declareops.eq_recarg
+let eq_wf_paths = Rtree.equal Declareops.eq_recarg
 
 let spec_of_tree t = lazy
   (if eq_wf_paths (Lazy.force t) mk_norec
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 16789cd3d7..c016bf0c30 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -103,75 +103,61 @@ let rec map f t = match t with
 let smartmap f t = match t with
     Param _ -> t
   | Node (a,sons) ->
-      let a'=f a and sons' = Util.Array.smartmap (map f) sons in
-	if a'==a && sons'==sons then
-	  t
-	else
-	  Node (a',sons')
+      let a'=f a and sons' = Array.smartmap (map f) sons in
+      if a'==a && sons'==sons then t
+      else Node (a',sons')
   | Rec(j,defs) ->
-      let defs' = Util.Array.smartmap (map f) defs in
-	if defs'==defs then
-	  t
-	else
-	  Rec(j,defs')
-
-(* 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 Int.equal (Array.length v1) (Array.length v2) ->
-          Array.for_all2 cmp v1 v2
-      | _ -> false)
-
-let rec raw_eq cmp t1 t2 = match t1, t2 with
-| Param (i1, j1), Param (i2, j2) ->
-  Int.equal i1 i2 && Int.equal j1 j2
-| Node (x1, a1), Node (x2, a2) ->
-  cmp x1 x2 && Array.equal (raw_eq cmp) a1 a2
-| Rec (i1, a1), Rec (i2, a2) ->
-  Int.equal i1 i2 && Array.equal (raw_eq cmp) a1 a2
-| _ -> false
-
-let eq_rtree cmp t1 t2 =
-  t1 == t2 || raw_eq cmp t1 t2 ||
-  compare_rtree
-    (fun t1 t2 ->
-      if cmp (fst(dest_node t1)) (fst(dest_node t2)) then 0
-      else (-1)) t1 t2
+      let defs' = Array.smartmap (map f) defs in
+      if defs'==defs then t
+      else Rec(j,defs')
+
+(** Structural equality test, parametrized by an equality on elements *)
+
+let rec raw_eq cmp t t' = match t, t' with
+  | Param (i,j), Param (i',j') -> Int.equal i i' && Int.equal j j'
+  | Node (x, a), Node (x', a') -> cmp x x' && Array.equal (raw_eq cmp) a a'
+  | Rec (i, a), Rec (i', a') -> Int.equal i i' && Array.equal (raw_eq cmp) a a'
+  | _ -> false
+
+let raw_eq2 cmp (t,u) (t',u') = raw_eq cmp t t' && raw_eq cmp u u'
+
+(** Equivalence test on expanded trees. It is parametrized by two
+    equalities on elements:
+    - [cmp] is used when checking for already seen trees
+    - [cmp'] is used when comparing node labels. *)
+
+let equiv cmp cmp' =
+  let rec compare histo t t' =
+    List.mem_f (raw_eq2 cmp) (t,t') histo ||
+    match expand t, expand t' with
+    | Node(x,v), Node(x',v') ->
+        cmp' x x' &&
+        Int.equal (Array.length v) (Array.length v') &&
+        Array.for_all2 (compare ((t,t')::histo)) v v'
+    | _ -> false
+  in compare []
+
+(** The main comparison on rtree tries first physical equality, then
+    the structural one, then the logical equivalence *)
+
+let equal cmp t t' =
+  t == t' || raw_eq cmp t t' || equiv cmp cmp t t'
+
+(** Deprecated alias *)
+let eq_rtree = equal
+
+(** Tests if a given tree is infinite, i.e. has an branch of infinite length.
+   This correspond to a cycle when visiting the expanded tree.
+   We use a specific comparison to detect already seen trees. *)
+
+let is_infinite cmp t =
+  let rec is_inf histo t =
+    List.mem_f (raw_eq cmp) t histo ||
+    match expand t with
+    | Node (_,v) -> Array.exists (is_inf (t::histo)) v
+    | _ -> false
+  in
+  is_inf [] t
 
 (* Pretty-print a tree (not so pretty) *)
 open Pp
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 7bfac2d4df..c3ec3a0c51 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Type of regular tree with nodes labelled by values of type 'a 
+(** 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
@@ -49,22 +49,22 @@ 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
+(** Tells if a tree has an infinite branch. The first arg is a comparison
+    used to detect already seen elements, hence loops *)
+val is_infinite : ('a -> 'a -> bool) -> 'a t -> bool
 
-val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+(** [Rtree.equiv eq eqlab t1 t2] compares t1 t2 (top-down).
+   If t1 and t2 are both nodes, [eqlab] is called on their labels,
+   in case of success deeper nodes are examined.
+   In case of loop (detected via structural equality parametrized
+   by [eq]), then the comparison is successful. *)
+val equiv :
+  ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+
+(** [Rtree.equal eq t1 t2] compares t1 and t2, first via physical
+    equality, then by structural equality (using [eq] on elements),
+    then by logical equivalence [Rtree.equiv eq eq] *)
+val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
 
 (** Iterators *)
 
@@ -72,9 +72,9 @@ 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
+
+val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+(** @deprecated Same as [Rtree.equal] *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b6a8fdc1a3..4f7a61fbf2 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -918,7 +918,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	| _ -> assert false
     in
     let ids = res::hres::graph_principle_id::ids in
-    (* we also compute fresh names for each hyptohesis of each branche of the principle *)
+    (* we also compute fresh names for each hyptohesis of each branch
+       of the principle *)
     let branches = List.rev princ_infos.branches in
     let intro_pats =
       List.map
@@ -935,8 +936,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     *)
     let rewrite_tac j ids : tactic =
       let graph_def = graphs.(j) in
-      let infos =  try find_Function_infos (destConst funcs.(j)) with Not_found ->  error "No graph found" in
-      if infos.is_general ||  Rtree.is_infinite graph_def.mind_recargs
+      let infos =
+        try find_Function_infos (destConst funcs.(j))
+        with Not_found ->  error "No graph found"
+      in
+      if infos.is_general
+        || Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs
       then
 	let eq_lemma =
 	  try Option.get (infos).equation_lemma
@@ -945,7 +950,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	tclTHENSEQ[
 	  tclMAP h_intro ids;
 	  Equality.rewriteLR (mkConst eq_lemma);
-	  (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *)
+	  (* Don't forget to $\zeta$ normlize the term since the principles
+             have been $\zeta$-normalized *)
 	  h_reduce
 	    (Genredexpr.Cbv
 	       {Redops.all_flags
@@ -956,7 +962,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  h_generalize (List.map mkVar ids);
 	  thin ids
 	]
-      else unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (destConst f))]
+      else
+        unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (destConst f))]
     in
     (* The proof of each branche itself *)
     let ind_number = ref 0 in