1 files changed, 305 insertions, 212 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 056ae3a9..29bca862 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,22 +8,24 @@
 
 (* This file implements the basic congruence-closure algorithm by *)
 (* Downey,Sethi and Tarjan. *)
+(* Plus some e-matching and constructor handling by P. Corbineau *)
 
+open Errors
 open Util
 open Pp
 open Goptions
 open Names
 open Term
+open Vars
 open Tacmach
 open Evd
-open Proof_type
 
 let init_size=5
 
 let cc_verbose=ref false
 
-let debug f x =
-  if !cc_verbose then f x
+let debug x =
+  if !cc_verbose then msg_debug x
 
 let _=
   let gdopt=
@@ -42,32 +44,39 @@ module ST=struct
 
   (* l: sign -> term r: term -> sign *)
 
-  type t = {toterm:(int*int,int) Hashtbl.t;
-	    tosign:(int,int*int) Hashtbl.t}
+  module IntTable = Hashtbl.Make(Int)
+  module IntPair =
+  struct
+    type t = int * int
+    let equal (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2
+    let hash (i, j) = Hashset.Combine.combine (Int.hash i) (Int.hash j)
+  end
+  module IntPairTable = Hashtbl.Make(IntPair)
+
+  type t = {toterm: int IntPairTable.t;
+	    tosign: (int * int) IntTable.t}
 
   let empty ()=
-    {toterm=Hashtbl.create init_size;
-     tosign=Hashtbl.create init_size}
+    {toterm=IntPairTable.create init_size;
+     tosign=IntTable.create init_size}
 
   let enter t sign st=
-    if Hashtbl.mem st.toterm sign then
-	anomaly "enter: signature already entered"
+    if IntPairTable.mem st.toterm sign then
+	anomaly ~label:"enter" (Pp.str "signature already entered")
     else
-	Hashtbl.replace st.toterm sign t;
-	Hashtbl.replace st.tosign t sign
-
-  let query sign st=Hashtbl.find st.toterm sign
+	IntPairTable.replace st.toterm sign t;
+	IntTable.replace st.tosign t sign
 
-  let rev_query term st=Hashtbl.find st.tosign term
+  let query sign st=IntPairTable.find st.toterm sign
 
   let delete st t=
-    try let sign=Hashtbl.find st.tosign t in
-	Hashtbl.remove st.toterm sign;
-	Hashtbl.remove st.tosign t
+    try let sign=IntTable.find st.tosign t in
+	IntPairTable.remove st.toterm sign;
+	IntTable.remove st.tosign t
     with
 	Not_found -> ()
 
-  let rec delete_set st s = Intset.iter (delete st) s
+  let delete_set st s = Int.Set.iter (delete st) s
 
 end
 
@@ -84,45 +93,78 @@ type pa_mark=
     Fmark of pa_fun
   | Cmark of pa_constructor
 
-module PacMap=Map.Make(struct
-			 type t=pa_constructor
-			 let compare=Pervasives.compare end)
+module PacOrd =
+struct
+  type t = pa_constructor
+  let compare { cnode = cnode0; arity = arity0; args = args0 }
+              { cnode = cnode1; arity = arity1; args = args1 } =
+    let cmp = Int.compare cnode0 cnode1 in
+    if cmp = 0 then
+      let cmp' = Int.compare arity0 arity1 in
+      if cmp' = 0 then
+        List.compare Int.compare args0 args1
+      else
+        cmp'
+    else
+      cmp
+end
+
+module PafOrd =
+struct
+  type t = pa_fun
+  let compare { fsym = fsym0; fnargs = fnargs0 } { fsym = fsym1; fnargs = fnargs1 } =
+    let cmp = Int.compare fsym0 fsym1 in
+    if cmp = 0 then
+      Int.compare fnargs0 fnargs1
+    else
+      cmp
+end
 
-module PafMap=Map.Make(struct
-			 type t=pa_fun
-			 let compare=Pervasives.compare end)
+module PacMap=Map.Make(PacOrd)
+module PafMap=Map.Make(PafOrd)
 
 type cinfo=
-    {ci_constr: constructor; (* inductive type *)
+    {ci_constr: pconstructor; (* inductive type *)
      ci_arity: int;     (* # args *)
      ci_nhyps: int}     (* # projectable args *)
 
+let family_eq f1 f2 = match f1, f2 with
+| InProp, InProp
+| InSet, InSet
+| InType, InType -> true
+| _ -> false
+
 type term=
     Symb of constr
   | Product of sorts_family * sorts_family
-  | Eps of identifier
+  | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
 
 let rec term_equal t1 t2 =
   match t1, t2 with
-    | Symb c1, Symb c2 -> eq_constr c1 c2
-    | Product (s1, t1), Product (s2, t2) -> s1 = s2 && t1 = t2
-    | Eps i1, Eps i2 -> id_ord i1 i2 = 0
+    | Symb c1, Symb c2 -> eq_constr_nounivs c1 c2
+    | Product (s1, t1), Product (s2, t2) -> family_eq s1 s2 && family_eq t1 t2
+    | Eps i1, Eps i2 -> Id.equal i1 i2
     | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2
-    | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1},
-      Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} ->
-      i1 = i2 && j1 = j2 && eq_constructor c1 c2
-    | _ -> t1 = t2
+    | Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1},
+      Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} ->
+      Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 (* FIXME check eq? *)
+    | _ -> false
+
+open Hashset.Combine
 
-open Hashtbl_alt.Combine
+let hash_sorts_family = function
+| InProp -> 0
+| InSet -> 1
+| InType -> 2
 
 let rec hash_term = function
   | Symb c -> combine 1 (hash_constr c)
-  | Product (s1, s2) -> combine3 2 (Hashtbl.hash s1) (Hashtbl.hash s2)
-  | Eps i -> combine 3 (Hashtbl.hash i)
+  | Product (s1, s2) -> combine3 2 (hash_sorts_family s1) (hash_sorts_family s2)
+  | Eps i -> combine 3 (Id.hash i)
   | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
-  | Constructor {ci_constr=c; ci_arity=i; ci_nhyps=j} -> combine4 5 (Hashtbl.hash c) i j
+  | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j
 
 type ccpattern =
     PApp of term * ccpattern list (* arguments are reversed *)
@@ -151,14 +193,16 @@ type patt_kind =
   | Creates_variables
 
 type quant_eq =
-    {qe_hyp_id: identifier;
-     qe_pol: bool;
-     qe_nvars:int;
-     qe_lhs: ccpattern;
-     qe_lhs_valid:patt_kind;
-     qe_rhs: ccpattern;
-     qe_rhs_valid:patt_kind}
-
+  {
+    qe_hyp_id: Id.t;
+    qe_pol: bool;
+    qe_nvars:int;
+    qe_lhs: ccpattern;
+    qe_lhs_valid:patt_kind;
+    qe_rhs: ccpattern;
+    qe_rhs_valid:patt_kind
+  }
+    
 let swap eq : equality =
   let swap_rule=match eq.rule with
       Congruence -> Congruence
@@ -174,12 +218,11 @@ type inductive_status =
 
 type representative=
     {mutable weight:int;
-     mutable lfathers:Intset.t;
-     mutable fathers:Intset.t;
+     mutable lfathers:Int.Set.t;
+     mutable fathers:Int.Set.t;
      mutable inductive_status: inductive_status;
      class_type : Term.types;
-     mutable functions: Intset.t PafMap.t;
-     mutable constructors: int PacMap.t} (*pac -> term = app(constr,t) *)
+     mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
 
 type cl = Rep of representative| Eqto of int*equality
 
@@ -188,12 +231,13 @@ type vertex = Leaf| Node of (int*int)
 type node =
     {mutable clas:cl;
      mutable cpath: int;
+     mutable constructors: int PacMap.t;
      vertex:vertex;
      term:term}
 
 module Constrhash = Hashtbl.Make
   (struct type t = constr
-	  let equal = eq_constr
+	  let equal = eq_constr_nounivs
 	  let hash = hash_constr
    end)
 module Typehash = Constrhash
@@ -205,9 +249,9 @@ module Termhash = Hashtbl.Make
    end)
 
 module Identhash = Hashtbl.Make
-  (struct type t = identifier
-	  let equal = Pervasives.(=)
-	  let hash = Hashtbl.hash
+  (struct type t = Id.t
+	  let equal = Id.equal
+	  let hash = Id.hash
    end)
 
 type forest=
@@ -221,45 +265,54 @@ type forest=
 type state =
     {uf: forest;
      sigtable:ST.t;
-     mutable terms: Intset.t;
+     mutable terms: Int.Set.t;
      combine: equality Queue.t;
      marks: (int * pa_mark) Queue.t;
      mutable diseq: disequality list;
      mutable quant: quant_eq list;
-     mutable pa_classes: Intset.t;
+     mutable pa_classes: Int.Set.t;
      q_history: (int array) Identhash.t;
      mutable rew_depth:int;
      mutable changed:bool;
-     by_type: Intset.t Typehash.t;
+     by_type: Int.Set.t Typehash.t;
      mutable gls:Proof_type.goal Tacmach.sigma}
 
 let dummy_node =
-  {clas=Eqto(min_int,{lhs=min_int;rhs=min_int;rule=Congruence});
-   cpath=min_int;
-   vertex=Leaf;
-   term=Symb (mkRel min_int)}
-
+  {
+    clas=Eqto (min_int,{lhs=min_int;rhs=min_int;rule=Congruence});
+    cpath=min_int;
+    constructors=PacMap.empty;
+    vertex=Leaf;
+    term=Symb (mkRel min_int)
+  }
+
+let empty_forest() =
+  {
+    max_size=init_size;
+    size=0;
+    map=Array.make init_size dummy_node;
+    epsilons=[];
+    axioms=Constrhash.create init_size;
+    syms=Termhash.create init_size
+  }
+    
 let empty depth gls:state =
-  {uf=
-     {max_size=init_size;
-      size=0;
-      map=Array.create init_size dummy_node;
-      epsilons=[];
-      axioms=Constrhash.create init_size;
-      syms=Termhash.create init_size};
-  terms=Intset.empty;
-  combine=Queue.create ();
-  marks=Queue.create ();
-  sigtable=ST.empty ();
-  diseq=[];
-  quant=[];
-  pa_classes=Intset.empty;
-  q_history=Identhash.create init_size;
-  rew_depth=depth;
-  by_type=Constrhash.create init_size;
-  changed=false;
-  gls=gls}
-
+  {
+    uf= empty_forest ();
+    terms=Int.Set.empty;
+    combine=Queue.create ();
+    marks=Queue.create ();
+    sigtable=ST.empty ();
+    diseq=[];
+    quant=[];
+    pa_classes=Int.Set.empty;
+    q_history=Identhash.create init_size;
+    rew_depth=depth;
+    by_type=Constrhash.create init_size;
+    changed=false;
+    gls=gls
+  }
+    
 let forest state = state.uf
 
 let compress_path uf i j = uf.map.(j).cpath<-i
@@ -274,15 +327,25 @@ let find uf i= find_aux uf [] i
 let get_representative uf i=
   match uf.map.(i).clas with
       Rep r -> r
-    | _ -> anomaly "get_representative: not a representative"
+    | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative")
+
+let get_constructors uf i= uf.map.(i).constructors
 
 let find_pac uf i pac =
-  PacMap.find pac (get_representative uf i).constructors
+  PacMap.find pac (get_constructors uf i)
+
+let rec find_oldest_pac uf i pac=
+  try PacMap.find pac (get_constructors uf i) with
+    Not_found -> 
+      match uf.map.(i).clas with 
+	Eqto (j,_) -> find_oldest_pac uf j pac
+      | Rep _ -> raise Not_found
+     
 
 let get_constructor_info uf i=
   match uf.map.(i).term with
       Constructor cinfo->cinfo
-    | _ -> anomaly "get_constructor: not a constructor"
+    | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor")
 
 let size uf i=
   (get_representative uf i).weight
@@ -294,13 +357,13 @@ let epsilons uf = uf.epsilons
 let add_lfather uf i t=
   let r=get_representative uf i in
     r.weight<-r.weight+1;
-    r.lfathers<-Intset.add t r.lfathers;
-    r.fathers <-Intset.add t r.fathers
+    r.lfathers<-Int.Set.add t r.lfathers;
+    r.fathers <-Int.Set.add t r.fathers
 
 let add_rfather uf i t=
   let r=get_representative uf i in
     r.weight<-r.weight+1;
-    r.fathers <-Intset.add t r.fathers
+    r.fathers <-Int.Set.add t r.fathers
 
 exception Discriminable of int * pa_constructor * int * pa_constructor
 
@@ -313,21 +376,21 @@ let tail_pac p=
 let fsucc paf =
   {paf with fnargs=succ paf.fnargs}
 
-let add_pac rep pac t =
-  if not (PacMap.mem pac rep.constructors) then
-    rep.constructors<-PacMap.add pac t rep.constructors
+let add_pac node pac t =
+  if not (PacMap.mem pac node.constructors) then
+    node.constructors<-PacMap.add pac t node.constructors
 
 let add_paf rep paf t =
   let already =
-    try PafMap.find paf rep.functions with Not_found -> Intset.empty in
-    rep.functions<- PafMap.add paf (Intset.add t already) rep.functions
+    try PafMap.find paf rep.functions with Not_found -> Int.Set.empty in
+    rep.functions<- PafMap.add paf (Int.Set.add t already) rep.functions
 
 let term uf i=uf.map.(i).term
 
 let subterms uf i=
   match uf.map.(i).vertex with
       Node(j,k) -> (j,k)
-    | _ -> anomaly "subterms: not a node"
+    | _ -> anomaly ~label:"subterms" (Pp.str "not a node")
 
 let signature uf i=
   let j,k=subterms uf i in (find uf j,find uf k)
@@ -335,9 +398,9 @@ let signature uf i=
 let next uf=
   let size=uf.size in
   let nsize= succ size in
-    if nsize=uf.max_size then
+    if Int.equal nsize uf.max_size then
       let newmax=uf.max_size * 3 / 2 + 1 in
-      let newmap=Array.create newmax dummy_node in
+      let newmap=Array.make newmax dummy_node in
 	begin
 	  uf.max_size<-newmax;
 	  Array.blit uf.map 0 newmap 0 size;
@@ -349,46 +412,63 @@ let next uf=
 
 let new_representative typ =
   {weight=0;
-   lfathers=Intset.empty;
-   fathers=Intset.empty;
+   lfathers=Int.Set.empty;
+   fathers=Int.Set.empty;
    inductive_status=Unknown;
    class_type=typ;
-   functions=PafMap.empty;
-   constructors=PacMap.empty}
+   functions=PafMap.empty}
 
 (* rebuild a constr from an applicative term *)
 
-let _A_ = Name (id_of_string "A")
-let _B_ = Name (id_of_string "A")
+let _A_ = Name (Id.of_string "A")
+let _B_ = Name (Id.of_string "A")
 let _body_ =  mkProd(Anonymous,mkRel 2,mkRel 2)
 
 let cc_product s1 s2 =
-  mkLambda(_A_,mkSort(Termops.new_sort_in_family s1),
-	   mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_))
+  mkLambda(_A_,mkSort(Universes.new_sort_in_family s1),
+	   mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_))
 
 let rec constr_of_term = function
-    Symb s->s
+    Symb s-> applist_projection s []
   | Product(s1,s2) -> cc_product s1 s2
   | Eps id -> mkVar id
-  | Constructor cinfo -> mkConstruct cinfo.ci_constr
+  | Constructor cinfo -> mkConstructU cinfo.ci_constr
   | Appli (s1,s2)->
       make_app [(constr_of_term s2)] s1
 and make_app l=function
     Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
-  | other -> applistc (constr_of_term other) l
+  | other -> 
+    applist_proj other l
+and applist_proj c l =
+  match c with
+  | Symb s -> applist_projection s l
+  | _ -> applistc (constr_of_term c) l
+and applist_projection c l =
+  match kind_of_term c with
+  | Const c when Environ.is_projection (fst c) (Global.env()) ->
+    let p = Projection.make (fst c) false in
+    (match l with 
+    | [] -> (* Expand the projection *)
+      let ty,_ = Typeops.type_of_constant (Global.env ()) c in
+      let pb = Environ.lookup_projection p (Global.env()) in
+      let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
+	it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
+    | hd :: tl ->
+      applistc (mkProj (p, hd)) tl)
+  | _ -> applistc c l
 
 let rec canonize_name c =
   let func =  canonize_name in
     match kind_of_term c with
-      | Const kn ->
+      | Const (kn,u) ->
 	  let canon_const = constant_of_kn (canonical_con kn) in 
-	    (mkConst canon_const)
-      | Ind (kn,i) ->
+	    (mkConstU (canon_const,u))
+      | Ind ((kn,i),u) ->
 	  let canon_mind = mind_of_kn (canonical_mind kn) in
-	    (mkInd (canon_mind,i))
-      | Construct ((kn,i),j) ->
+	    (mkIndU ((canon_mind,i),u))
+      | Construct (((kn,i),j),u) ->
 	  let canon_mind = mind_of_kn (canonical_mind kn) in
-	    mkConstruct ((canon_mind,i),j) 
+	    mkConstructU (((canon_mind,i),j),u)
       | Prod (na,t,ct) ->
 	  mkProd (na,func t, func ct)
       | Lambda (na,t,ct) ->
@@ -396,16 +476,22 @@ let rec canonize_name c =
       | LetIn (na,b,t,ct) ->
 	  mkLetIn (na, func b,func t,func ct)
       | App (ct,l) ->
-	  mkApp (func ct,array_smartmap func l)
+	  mkApp (func ct,Array.smartmap func l)
+      | Proj(p,c) ->
+	let p' = Projection.map (fun kn ->
+          constant_of_kn (canonical_con kn)) p in 
+	  (mkProj (p', func c))
       | _ -> c
 
 (* rebuild a term from a pattern and a substitution *)
 
 let build_subst uf subst =
-  Array.map (fun i ->
-	       try term uf i
-	       with e when Errors.noncritical e ->
-                 anomaly "incomplete matching") subst
+  Array.map
+    (fun i ->
+      try term uf i
+      with e when Errors.noncritical e ->
+        anomaly (Pp.str "incomplete matching"))
+    subst
 
 let rec inst_pattern subst = function
     PVar i ->
@@ -415,8 +501,8 @@ let rec inst_pattern subst = function
 	(fun spat f -> Appli (f,inst_pattern subst spat))
 	   args t
 
-let pr_idx_term state i = str "[" ++ int i ++ str ":=" ++
-  Termops.print_constr (constr_of_term (term state.uf i)) ++ str "]"
+let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
+  Termops.print_constr (constr_of_term (term uf i)) ++ str "]"
 
 let pr_term t = str "[" ++
   Termops.print_constr (constr_of_term t) ++ str "]"
@@ -426,7 +512,8 @@ let rec add_term state t=
     try Termhash.find uf.syms t with
 	Not_found ->
 	  let b=next uf in
-	  let typ = pf_type_of state.gls (constr_of_term t) in
+          let trm = constr_of_term t in
+	  let typ = pf_type_of state.gls trm in
 	  let typ = canonize_name typ in
 	  let new_node=
 	    match t with
@@ -437,20 +524,23 @@ let rec add_term state t=
 		    Queue.add (b,Fmark paf) state.marks;
 		    {clas= Rep (new_representative typ);
 		     cpath= -1;
+		     constructors=PacMap.empty;
 		     vertex= Leaf;
 		     term= t}
 	      | Eps id ->
 		  {clas= Rep (new_representative typ);
 		   cpath= -1;
+		   constructors=PacMap.empty;
 		   vertex= Leaf;
 		   term= t}
 	      | Appli (t1,t2) ->
 		  let i1=add_term state t1 and i2=add_term state t2 in
 		    add_lfather uf (find uf i1) b;
 		    add_rfather uf (find uf i2) b;
-		    state.terms<-Intset.add b state.terms;
+		    state.terms<-Int.Set.add b state.terms;
 		    {clas= Rep (new_representative typ);
 		     cpath= -1;
+		     constructors=PacMap.empty;
 		     vertex= Node(i1,i2);
 		     term= t}
 	      | Constructor cinfo ->
@@ -465,15 +555,16 @@ let rec add_term state t=
 		    Queue.add (b,Cmark pac) state.marks;
 		    {clas=Rep (new_representative typ);
 		     cpath= -1;
+		     constructors=PacMap.empty;
 		     vertex=Leaf;
 		     term=t}
 	  in
 	    uf.map.(b)<-new_node;
 	    Termhash.add uf.syms t b;
 	    Typehash.replace state.by_type typ
-	      (Intset.add b
+	      (Int.Set.add b
 		 (try Typehash.find state.by_type typ with
-		      Not_found -> Intset.empty));
+		      Not_found -> Int.Set.empty));
 	    b
 
 let add_equality state c s t=
@@ -503,23 +594,23 @@ let is_redundant state id args =
     let prev_args = Identhash.find_all state.q_history id in
     List.exists
       (fun old_args ->
-	 Util.array_for_all2 (fun i j -> i = find state.uf j)
+	 Util.Array.for_all2 (fun i j -> Int.equal i (find state.uf j))
          norm_args old_args)
       prev_args
     with Not_found -> false
 
 let add_inst state (inst,int_subst) =
-  check_for_interrupt ();
+  Control.check_for_interrupt ();
   if state.rew_depth > 0 then
   if is_redundant state inst.qe_hyp_id int_subst then
-    debug msgnl (str "discarding redundant (dis)equality")
+    debug (str "discarding redundant (dis)equality")
   else
     begin
       Identhash.add state.q_history inst.qe_hyp_id int_subst;
       let subst = build_subst (forest state) int_subst in
       let prfhead= mkVar inst.qe_hyp_id in
       let args = Array.map constr_of_term subst in
-      let _ = array_rev args in (* highest deBruijn index first *)
+      let _ = Array.rev args in (* highest deBruijn index first *)
       let prf= mkApp(prfhead,args) in
 	  let s = inst_pattern subst inst.qe_lhs
 	  and t = inst_pattern subst inst.qe_rhs in
@@ -527,20 +618,18 @@ let add_inst state (inst,int_subst) =
 	    state.rew_depth<-pred state.rew_depth;
 	    if inst.qe_pol then
 	      begin
-		debug (fun () ->
-		  msgnl
-		   (str "Adding new equality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++
-			   pr_term s ++ str " == " ++ pr_term t ++ str "]")) ();
+		debug (
+		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
+	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
 		add_equality state prf s t
 	      end
 	    else
 	      begin
-		debug (fun () ->
-		  msgnl
-		   (str "Adding new disequality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++
-			   pr_term s ++ str " <> " ++ pr_term t ++ str "]")) ();
+		debug (
+		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
+	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
   end
@@ -552,75 +641,77 @@ let link uf i j eq = (* links i -> j *)
 
 let rec down_path uf i l=
   match uf.map.(i).clas with
-      Eqto(j,t)->down_path uf j (((i,j),t)::l)
+      Eqto (j,eq) ->down_path uf j (((i,j),eq)::l)
     | Rep _ ->l
 
+let eq_pair (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2
+
 let rec min_path=function
     ([],l2)->([],l2)
   | (l1,[])->(l1,[])
-  | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2)
+  | (((c1,t1)::q1),((c2,t2)::q2)) when eq_pair c1 c2 -> min_path (q1,q2)
   | cpl -> cpl
 
 let join_path uf i j=
-  assert (find uf i=find uf j);
+  assert (Int.equal (find uf i) (find uf j));
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++
-		 str " and " ++ pr_idx_term state i2 ++ str ".")) ();
+  debug (str "Linking " ++ pr_idx_term state.uf i1 ++
+		 str " and " ++ pr_idx_term state.uf i2 ++ str ".");
   let r1= get_representative state.uf i1
   and r2= get_representative state.uf i2 in
     link state.uf i1 i2 eq;
     Constrhash.replace state.by_type r1.class_type
-      (Intset.remove i1
+      (Int.Set.remove i1
 	 (try Constrhash.find state.by_type r1.class_type with
-	      Not_found -> Intset.empty));
-    let f= Intset.union r1.fathers r2.fathers in
-      r2.weight<-Intset.cardinal f;
+	      Not_found -> Int.Set.empty));
+    let f= Int.Set.union r1.fathers r2.fathers in
+      r2.weight<-Int.Set.cardinal f;
       r2.fathers<-f;
-      r2.lfathers<-Intset.union r1.lfathers r2.lfathers;
+      r2.lfathers<-Int.Set.union r1.lfathers r2.lfathers;
       ST.delete_set state.sigtable r1.fathers;
-      state.terms<-Intset.union state.terms r1.fathers;
+      state.terms<-Int.Set.union state.terms r1.fathers;
       PacMap.iter
 	(fun pac b -> Queue.add (b,Cmark pac) state.marks)
-	r1.constructors;
+	state.uf.map.(i1).constructors;
       PafMap.iter
-	(fun paf -> Intset.iter
+	(fun paf -> Int.Set.iter
 	   (fun b -> Queue.add (b,Fmark paf) state.marks))
 	r1.functions;
       match r1.inductive_status,r2.inductive_status with
 	  Unknown,_ -> ()
 	| Partial pac,Unknown ->
 	    r2.inductive_status<-Partial pac;
-	    state.pa_classes<-Intset.remove i1 state.pa_classes;
-	    state.pa_classes<-Intset.add i2 state.pa_classes
+	    state.pa_classes<-Int.Set.remove i1 state.pa_classes;
+	    state.pa_classes<-Int.Set.add i2 state.pa_classes
 	| Partial _ ,(Partial _ |Partial_applied) ->
-	    state.pa_classes<-Intset.remove i1 state.pa_classes
+	    state.pa_classes<-Int.Set.remove i1 state.pa_classes
 	| Partial_applied,Unknown ->
 	    r2.inductive_status<-Partial_applied
 	| Partial_applied,Partial _ ->
-	    state.pa_classes<-Intset.remove i2 state.pa_classes;
+	    state.pa_classes<-Int.Set.remove i2 state.pa_classes;
 	    r2.inductive_status<-Partial_applied
 	| Total cpl,Unknown -> r2.inductive_status<-Total cpl;
 	| Total (i,pac),Total _ -> Queue.add (i,Cmark pac) state.marks
 	| _,_ -> ()
 
 let merge eq state = (* merge and no-merge *)
-  debug (fun () -> msgnl
-    (str "Merging " ++ pr_idx_term state eq.lhs ++
-       str " and " ++ pr_idx_term state eq.rhs ++ str ".")) ();
+  debug
+    (str "Merging " ++ pr_idx_term state.uf eq.lhs ++
+       str " and " ++ pr_idx_term state.uf eq.rhs ++ str ".");
   let uf=state.uf in
   let i=find uf eq.lhs
   and j=find uf eq.rhs in
-    if i<>j then
+    if not (Int.equal i j) then
       if (size uf i)<(size uf j) then
 	union state i j eq
       else
 	union state j i (swap eq)
 
 let update t state = (* update 1 and 2 *)
-  debug (fun () -> msgnl
-    (str "Updating term " ++ pr_idx_term state t ++ str ".")) ();
+  debug
+    (str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
   let (i,j) as sign = signature state.uf t in
   let (u,v) = subterms state.uf t in
   let rep = get_representative state.uf i in
@@ -628,12 +719,12 @@ let update t state = (* update 1 and 2 *)
       match rep.inductive_status with
 	  Partial _ ->
 	    rep.inductive_status <- Partial_applied;
-	    state.pa_classes <- Intset.remove i state.pa_classes
+	    state.pa_classes <- Int.Set.remove i state.pa_classes
 	| _ -> ()
     end;
     PacMap.iter
       (fun pac _ -> Queue.add (t,Cmark (append_pac v pac)) state.marks)
-      rep.constructors;
+      (get_constructors state.uf i);
     PafMap.iter
       (fun paf _ -> Queue.add (t,Fmark (fsucc paf)) state.marks)
       rep.functions;
@@ -645,12 +736,13 @@ let update t state = (* update 1 and 2 *)
 
 let process_function_mark t rep paf state  =
   add_paf rep paf t;
-  state.terms<-Intset.union rep.lfathers state.terms
+  state.terms<-Int.Set.union rep.lfathers state.terms
 
 let process_constructor_mark t i rep pac state =
-    match rep.inductive_status with
+     add_pac state.uf.map.(i) pac t;
+     match rep.inductive_status with
 	Total (s,opac) ->
-	  if pac.cnode <> opac.cnode then (* Conflict *)
+	  if not (Int.equal pac.cnode opac.cnode) then (* Conflict *)
 	    raise (Discriminable (s,opac,t,pac))
 	  else (* Match *)
 	    let cinfo = get_constructor_info state.uf pac.cnode in
@@ -662,26 +754,26 @@ let process_constructor_mark t i rep pac state =
 			{lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)}
 			state.combine;
 		      f (n-1) q1 q2
-		  | _-> anomaly
-		      "add_pacs : weird error in injection subterms merge"
+		  | _-> anomaly ~label:"add_pacs"
+		      (Pp.str "weird error in injection subterms merge")
 	    in f cinfo.ci_nhyps opac.args pac.args
       | Partial_applied | Partial _ ->
-	  add_pac rep pac t;
-	  state.terms<-Intset.union rep.lfathers state.terms
+(*	  add_pac state.uf.map.(i) pac t; *)
+	  state.terms<-Int.Set.union rep.lfathers state.terms
       | Unknown ->
-	  if pac.arity = 0 then
+	  if Int.equal pac.arity 0 then
 	    rep.inductive_status <- Total (t,pac)
 	  else
 	    begin
-	      add_pac rep pac t;
-	      state.terms<-Intset.union rep.lfathers state.terms;
+	     (* add_pac state.uf.map.(i) pac t; *)
+	      state.terms<-Int.Set.union rep.lfathers state.terms;
 	      rep.inductive_status <- Partial pac;
-	      state.pa_classes<- Intset.add i state.pa_classes
+	      state.pa_classes<- Int.Set.add i state.pa_classes
 	    end
 
 let process_mark t m state =
-  debug (fun () -> msgnl
-    (str "Processing mark for term " ++ pr_idx_term state t ++ str ".")) ();
+  debug
+    (str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
   let i=find state.uf t in
   let rep=get_representative state.uf i in
     match m with
@@ -696,14 +788,15 @@ type explanation =
 let check_disequalities state =
   let uf=state.uf in
   let rec check_aux = function
-      dis::q ->
-	debug (fun () -> msg
-	(str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
-	 pr_idx_term state dis.rhs ++ str " ... ")) ();
-	if find uf dis.lhs=find uf dis.rhs then
-	  begin debug msgnl (str "Yes");Some dis end
-	else
-	  begin debug msgnl (str "No");check_aux q end
+    | dis::q ->
+        let (info, ans) =
+          if Int.equal (find uf dis.lhs) (find uf dis.rhs) then (str "Yes", Some dis)
+          else (str "No", check_aux q)
+        in
+        let _ = debug
+        (str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
+         pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
+        ans
     | [] -> None
   in
     check_aux state.diseq
@@ -720,13 +813,13 @@ let one_step state =
 	  true
       with Queue.Empty ->
 	try
-	  let t = Intset.choose state.terms in
-	    state.terms<-Intset.remove t state.terms;
+	  let t = Int.Set.choose state.terms in
+	    state.terms<-Int.Set.remove t state.terms;
 	    update t state;
 	    true
 	with Not_found -> false
 
-let __eps__ = id_of_string "_eps_"
+let __eps__ = Id.of_string "_eps_"
 
 let new_state_var typ state =
   let id = pf_get_new_id __eps__ state.gls in
@@ -752,10 +845,10 @@ let complete_one_class state i=
 	let ct = app (term state.uf i) typ pac.arity in
 	  state.uf.epsilons <- pac :: state.uf.epsilons;
 	  ignore (add_term state ct)
-    | _ -> anomaly "wrong incomplete class"
+    | _ -> anomaly (Pp.str "wrong incomplete class")
 
 let complete state =
-  Intset.iter (complete_one_class state) state.pa_classes
+  Int.Set.iter (complete_one_class state) state.pa_classes
 
 type matching_problem =
 {mp_subst : int array;
@@ -773,14 +866,14 @@ let make_fun_table state =
 	       (fun paf _ ->
 		  let elem =
 		    try PafMap.find paf !funtab
-		    with Not_found -> Intset.empty in
-		    funtab:= PafMap.add paf (Intset.add i elem) !funtab)
+		    with Not_found -> Int.Set.empty in
+		    funtab:= PafMap.add paf (Int.Set.add i elem) !funtab)
 	       rep.functions
 	 | _ -> ()) state.uf.map;
     !funtab
 
 
-let rec do_match state res pb_stack =
+let do_match state res pb_stack =
   let mp=Stack.pop pb_stack in
     match mp.mp_stack with
 	[] ->
@@ -795,13 +888,13 @@ let rec do_match state res pb_stack =
 		      Stack.push {mp with mp_stack=remains} pb_stack
 		    end
 		  else
-		    if mp.mp_subst.(pred i) = cl then
+		    if Int.equal mp.mp_subst.(pred i) cl then
 		      Stack.push {mp with mp_stack=remains} pb_stack
 		    else (* mismatch for non-linear variable in pattern *) ()
 	      | PApp (f,[]) ->
 		  begin
 		    try let j=Termhash.find uf.syms f in
-		      if find uf j =cl then
+		      if Int.equal (find uf j) cl then
 			Stack.push {mp with mp_stack=remains} pb_stack
 		    with Not_found -> ()
 		  end
@@ -819,7 +912,7 @@ let rec do_match state res pb_stack =
 			     mp_stack=
 			      (PApp(f,rem_args),s) ::
 				(last_arg,t) :: remains} pb_stack in
-		      Intset.iter aux good_terms
+		      Int.Set.iter aux good_terms
 		  with Not_found -> ()
 
 let paf_of_patt syms = function
@@ -836,21 +929,21 @@ let init_pb_stack state =
     begin
       let good_classes =
 	match inst.qe_lhs_valid with
-	  Creates_variables -> Intset.empty
+	  Creates_variables -> Int.Set.empty
 	| Normal ->
 	    begin
 	      try
 		let paf= paf_of_patt syms inst.qe_lhs in
 		  PafMap.find paf funtab
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end
 	| Trivial typ ->
 	    begin
 	      try
 		Typehash.find state.by_type typ
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end in
-	Intset.iter (fun i ->
+	Int.Set.iter (fun i ->
 		       Stack.push
 			 {mp_subst = Array.make inst.qe_nvars (-1);
 			  mp_inst=inst;
@@ -859,21 +952,21 @@ let init_pb_stack state =
     begin
       let good_classes =
 	match inst.qe_rhs_valid with
-	  Creates_variables -> Intset.empty
+	  Creates_variables -> Int.Set.empty
 	| Normal ->
 	    begin
 	      try
 		let paf= paf_of_patt syms inst.qe_rhs in
 		  PafMap.find paf funtab
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end
 	| Trivial typ ->
 	    begin
 	      try
 		Typehash.find state.by_type typ
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end in
-	Intset.iter (fun i ->
+	Int.Set.iter (fun i ->
 		       Stack.push
 			 {mp_subst = Array.make inst.qe_nvars (-1);
 			  mp_inst=inst;
@@ -886,28 +979,28 @@ let find_instances state =
   let pb_stack= init_pb_stack state in
   let res =ref [] in
   let _ =
-    debug msgnl (str "Running E-matching algorithm ... ");
+    debug (str "Running E-matching algorithm ... ");
     try
       while true do
-	check_for_interrupt ();
+	Control.check_for_interrupt ();
 	do_match state res pb_stack
       done;
-      anomaly "get out of here !"
+      anomaly (Pp.str "get out of here !")
     with Stack.Empty -> () in
     !res
 
 let rec execute first_run state =
-  debug msgnl (str "Executing ... ");
+  debug (str "Executing ... ");
   try
     while
-      check_for_interrupt ();
+      Control.check_for_interrupt ();
       one_step state do ()
     done;
     match check_disequalities state with
 	None ->
-	  if not(Intset.is_empty state.pa_classes) then
+	  if not(Int.Set.is_empty state.pa_classes) then
 	    begin
-	      debug msgnl (str "First run was incomplete, completing ... ");
+	      debug (str "First run was incomplete, completing ... ");
 	      complete state;
 	      execute false state
 	    end
@@ -922,12 +1015,12 @@ let rec execute first_run state =
 		  end
 		else
 	      begin
-		debug msgnl (str "Out of instances ... ");
+		debug (str "Out of instances ... ");
 		None
 	      end
 	    else
 	      begin
-		debug msgnl (str "Out of depth ... ");
+		debug (str "Out of depth ... ");
 		None
 	      end
       | Some dis -> Some