fix bug #2447 in congruence

4 files changed, 245 insertions, 149 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 5a4a435a5..23e1af0e8 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -8,6 +8,7 @@
 
 (* 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
@@ -192,14 +193,16 @@ type patt_kind =
   | Creates_variables
 
 type quant_eq =
-    {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}
-
+  {
+    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
@@ -219,8 +222,7 @@ type representative=
      mutable fathers:Int.Set.t;
      mutable inductive_status: inductive_status;
      class_type : Term.types;
-     mutable functions: Int.Set.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
 
@@ -229,6 +231,7 @@ type vertex = Leaf| Node of (int*int)
 type node =
     {mutable clas:cl;
      mutable cpath: int;
+     mutable constructors: int PacMap.t;
      vertex:vertex;
      term:term}
 
@@ -275,32 +278,41 @@ type state =
      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.make init_size dummy_node;
-      epsilons=[];
-      axioms=Constrhash.create init_size;
-      syms=Termhash.create init_size};
-  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}
-
+  {
+    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
@@ -317,8 +329,18 @@ let get_representative uf i=
       Rep r -> r
     | _ -> 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
@@ -354,9 +376,9 @@ 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 =
@@ -394,8 +416,7 @@ let new_representative typ =
    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 *)
 
@@ -480,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 "]"
@@ -503,11 +524,13 @@ 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) ->
@@ -517,6 +540,7 @@ let rec add_term state t=
 		    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 ->
@@ -531,6 +555,7 @@ 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
@@ -616,7 +641,7 @@ 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
@@ -632,8 +657,8 @@ let join_path uf i j=
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (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;
@@ -649,7 +674,7 @@ let union state i1 i2 eq=
       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 -> Int.Set.iter
 	   (fun b -> Queue.add (b,Fmark paf) state.marks))
@@ -673,8 +698,8 @@ let union state i1 i2 eq=
 
 let merge eq state = (* merge and no-merge *)
   debug
-    (str "Merging " ++ pr_idx_term state eq.lhs ++
-       str " and " ++ pr_idx_term state eq.rhs ++ str ".");
+    (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
@@ -686,7 +711,7 @@ let merge eq state = (* merge and no-merge *)
 
 let update t state = (* update 1 and 2 *)
   debug
-    (str "Updating term " ++ pr_idx_term state t ++ str ".");
+    (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
@@ -699,7 +724,7 @@ let update t state = (* update 1 and 2 *)
     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;
@@ -714,7 +739,8 @@ let process_function_mark t rep paf state  =
   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 not (Int.equal pac.cnode opac.cnode) then (* Conflict *)
 	    raise (Discriminable (s,opac,t,pac))
@@ -732,14 +758,14 @@ let process_constructor_mark t i rep pac state =
 		      (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;
+(*	  add_pac state.uf.map.(i) pac t; *)
 	  state.terms<-Int.Set.union rep.lfathers state.terms
       | Unknown ->
 	  if Int.equal pac.arity 0 then
 	    rep.inductive_status <- Total (t,pac)
 	  else
 	    begin
-	      add_pac rep pac t;
+	     (* 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<- Int.Set.add i state.pa_classes
@@ -747,7 +773,7 @@ let process_constructor_mark t i rep pac state =
 
 let process_mark t m state =
   debug
-    (str "Processing mark for term " ++ pr_idx_term state t ++ str ".");
+    (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
@@ -768,8 +794,8 @@ let check_disequalities state =
           else (str "No", check_aux q)
         in
         let _ = debug
-        (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
-         pr_idx_term state dis.rhs ++ str " ... " ++ info) in
+        (str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
+         pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
         ans
     | [] -> None
   in
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 0c5d6ca1f..abee34203 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -10,6 +10,19 @@ open Util
 open Term
 open Names
 
+type pa_constructor =
+    { cnode : int;
+      arity : int;
+      args  : int list}
+
+type pa_fun=
+    {fsym:int;
+     fnargs:int}
+
+
+module PafMap : Map.S with type key = pa_fun
+module PacMap : Map.S with type key = pa_constructor
+
 type cinfo =
     {ci_constr: pconstructor; (* inductive type *)
      ci_arity: int;     (* # args *)
@@ -22,28 +35,14 @@ type term =
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
 
-val term_equal : term -> term -> bool
+module Constrhash : Hashtbl.S with type key = constr
+module Termhash : Hashtbl.S with type key = term
 
-type patt_kind =
-    Normal
-  | Trivial of types
-  | Creates_variables
 
 type ccpattern =
     PApp of term * ccpattern list
   | PVar of int
 
-type pa_constructor =
-    { cnode : int;
-      arity : int;
-      args  : int list}
-
-module PacMap : Map.S with type key = pa_constructor
-
-type forest
-
-type state
-
 type rule=
     Congruence
   | Axiom of constr * bool
@@ -61,13 +60,63 @@ type equality = rule eq
 
 type disequality = from eq
 
+type patt_kind =
+    Normal
+  | Trivial of types
+  | Creates_variables
+
+type quant_eq=
+    {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}
+
+type inductive_status =
+    Unknown
+  | Partial of pa_constructor
+  | Partial_applied
+  | Total of (int * pa_constructor)
+
+type representative=
+    {mutable weight:int;
+     mutable lfathers:Int.Set.t;
+     mutable fathers:Int.Set.t;
+     mutable inductive_status: inductive_status;
+     class_type : Term.types;
+     mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
+
+type cl = Rep of representative| Eqto of int*equality
+
+type vertex = Leaf| Node of (int*int)
+
+type node =
+    {mutable clas:cl;
+     mutable cpath: int;
+     mutable constructors: int PacMap.t;
+     vertex:vertex;
+     term:term}
+
+type forest=
+    {mutable max_size:int;
+     mutable size:int;
+     mutable map: node array;
+     axioms: (term*term) Constrhash.t;
+     mutable epsilons: pa_constructor list;
+     syms: int Termhash.t}
+
+type state
+
 type explanation =
     Discrimination of (int*pa_constructor*int*pa_constructor)
   | Contradiction of disequality
   | Incomplete
 
-module Constrhash : Hashtbl.S with type key = constr
-module Termhash : Hashtbl.S with type key = term
+type matching_problem
+
+val term_equal : term -> term -> bool
 
 val constr_of_term : term -> constr
 
@@ -96,6 +145,8 @@ val find : forest -> int -> int
 
 val find_pac : forest -> int -> pa_constructor -> int
 
+val find_oldest_pac : forest -> int -> pa_constructor -> int
+
 val term : forest -> int -> term
 
 val get_constructor_info : forest -> int -> cinfo
@@ -105,24 +156,6 @@ val subterms : forest -> int -> int * int
 val join_path : forest -> int -> int ->
   ((int * int) * equality) list * ((int * int) * equality) list
 
-type quant_eq=
-    {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}
-
-
-type pa_fun=
-    {fsym:int;
-     fnargs:int}
-
-type matching_problem
-
-module PafMap: Map.S with type key = pa_fun
-
 val make_fun_table : state -> Int.Set.t PafMap.t
 
 val do_match :  state ->
@@ -136,8 +169,9 @@ val find_instances : state -> (quant_eq * int array) list
 
 val execute : bool -> state -> explanation option
 
+val pr_idx_term : forest -> int -> Pp.std_ppcmds
 
-
+val empty_forest: unit -> forest
 
 
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 6177f22f3..7b1a02cbe 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -12,6 +12,7 @@
 open Errors
 open Term
 open Ccalgo
+open Pp
 
 type rule=
     Ax of constr
@@ -91,60 +92,65 @@ let pinject p c n a =
    p_rhs=nth_arg p.p_rhs (n-a);
    p_rule=Inject(p,c,n,a)}
 
-let build_proof uf=
+let rec equal_proof uf i j=
+  debug (str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  if i=j then prefl (term uf i) else
+    let (li,lj)=join_path uf i j in
+    ptrans (path_proof uf i li) (psym (path_proof uf j lj))
+      
+and edge_proof uf ((i,j),eq)=
+  debug (str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  let pi=equal_proof uf i eq.lhs in
+  let pj=psym (equal_proof uf j eq.rhs) in
+  let pij=
+    match eq.rule with
+      Axiom (s,reversed)->
+	if reversed then psymax (axioms uf) s
+	else pax (axioms uf) s
+    | Congruence ->congr_proof uf eq.lhs eq.rhs
+    | Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *) 
+      let p=ind_proof uf ti ipac tj jpac in
+      let cinfo= get_constructor_info uf ipac.cnode in
+      pinject p cinfo.ci_constr cinfo.ci_nhyps k in  
+  ptrans (ptrans pi pij) pj
+  
+and constr_proof uf i ipac=
+  debug (str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
+  let t=find_oldest_pac uf i ipac in
+  let eq_it=equal_proof uf i t in
+  if ipac.args=[] then
+    eq_it
+  else
+    let fipac=tail_pac ipac in
+    let (fi,arg)=subterms uf t in
+    let targ=term uf arg in
+    let p=constr_proof uf fi fipac in
+    ptrans eq_it (pcongr p (prefl targ))
+      
+and path_proof uf i l=
+  debug (str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
+	   (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
+  match l with
+  | [] -> prefl (term uf i)
+  | x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x)
+    
+and congr_proof uf i j=
+  debug (str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  let (i1,i2) = subterms uf i
+  and (j1,j2) = subterms uf j in
+  pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2)
+    
+and ind_proof uf i ipac j jpac=
+   debug (str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  let p=equal_proof uf i j
+  and p1=constr_proof uf i ipac
+  and p2=constr_proof uf j jpac in
+  ptrans (psym p1) (ptrans p p2)
 
-  let axioms = axioms uf in
-
-  let rec equal_proof i j=
-    if i=j then prefl (term uf i) else
-      let (li,lj)=join_path uf i j in
-	ptrans (path_proof i li) (psym (path_proof j lj))
-
-  and edge_proof ((i,j),eq)=
-    let pi=equal_proof i eq.lhs in
-    let pj=psym (equal_proof j eq.rhs) in
-    let pij=
-      match eq.rule with
-	  Axiom (s,reversed)->
-	    if reversed then psymax axioms s
-	    else pax axioms s
-	| Congruence ->congr_proof eq.lhs eq.rhs
-	| Injection (ti,ipac,tj,jpac,k) ->
-	    let p=ind_proof ti ipac tj jpac in
-	    let cinfo= get_constructor_info uf ipac.cnode in
-	      pinject p cinfo.ci_constr cinfo.ci_nhyps k
-    in  ptrans (ptrans pi pij) pj
-
-  and constr_proof i t ipac=
-    if ipac.args=[] then
-      equal_proof i t
-    else
-      let npac=tail_pac ipac in
-      let (j,arg)=subterms uf t in
-      let targ=term uf arg in
-      let rj=find uf j in
-      let u=find_pac uf rj npac in
-      let p=constr_proof j u npac in
-	ptrans (equal_proof i t) (pcongr p (prefl targ))
-
-  and path_proof i=function
-      [] -> prefl (term uf i)
-    | x::q->ptrans (path_proof (snd (fst x)) q) (edge_proof x)
-
-  and congr_proof i j=
-    let (i1,i2) = subterms uf i
-    and (j1,j2) = subterms uf j in
-      pcongr (equal_proof i1 j1) (equal_proof i2 j2)
-
-  and ind_proof i ipac j jpac=
-    let p=equal_proof i j
-    and p1=constr_proof i i ipac
-    and p2=constr_proof j j jpac in
-      ptrans (psym p1) (ptrans p p2)
-  in
-    function
-	`Prove (i,j) -> equal_proof i j
-      | `Discr (i,ci,j,cj)-> ind_proof i ci j cj
+let build_proof uf=
+  function
+  | `Prove (i,j) -> equal_proof uf i j
+  | `Discr (i,ci,j,cj)-> ind_proof uf i ci j cj
 
 
 
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 50e3624d0..ba95ebb59 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -20,10 +20,40 @@ type rule=
 and proof =
     private {p_lhs:term;p_rhs:term;p_rule:rule}
 
+(** Proof smart constructors *)
+
+val prefl:term -> proof
+
+val pcongr: proof -> proof -> proof
+
+val ptrans: proof -> proof -> proof
+
+val psym: proof -> proof
+
+val pax : (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t ->
+           Ccalgo.Constrhash.key -> proof
+
+val psymax :  (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t ->
+           Ccalgo.Constrhash.key -> proof
+
+val pinject :  proof -> pconstructor -> int -> int -> proof
+
+(** Proof building functions *)
+
+val equal_proof : forest -> int -> int -> proof
+
+val edge_proof : forest -> (int*int)*equality -> proof
+
+val path_proof : forest -> int -> ((int*int)*equality) list -> proof
+
+val congr_proof :  forest -> int -> int -> proof
+
+val ind_proof : forest -> int -> pa_constructor -> int -> pa_constructor -> proof
+
+(** Main proof building function *)
+
 val build_proof :
   forest ->
   [ `Discr of int * pa_constructor * int * pa_constructor
   | `Prove of int * int ] -> proof
 
-
-