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

4 files changed, 16 insertions, 9 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