cc update

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

4 files changed, 42 insertions, 17 deletions

diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
index 0343c96211..ee34b5e8f7 100644
--- a/contrib/cc/ccalgo.mli
+++ b/contrib/cc/ccalgo.mli
@@ -45,6 +45,7 @@ sig
   val empty : unit -> t
   val find : t -> int -> int
   val size : t -> int -> int
+  val get_constructor : t -> int -> Names.constructor
   val pac_arity : t -> int -> int * int -> int
   val mem_node_pac : t -> int -> int * int -> int 
   val add_pacs : t -> int -> pa_constructor PacMap.t -> 
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index 8d5d2642b9..fadd2d080c 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -150,6 +150,6 @@ let cc_proof (axioms,m)=
     with UF.Discriminable (i,ci,j,cj,uf) ->
       let prf=build_proof uf (Refute(i,ci,j,cj)) in 
       let (t1,t2)=type_proof axioms prf in 
-	Refute (t1,t2,prf,axioms) 
+	Refute (UF.get_constructor uf ci,t1,t2,prf,axioms) 
 
 
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
index 664ac31f81..7f21f9dc10 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -35,5 +35,6 @@ val type_proof :
 val cc_proof :
   (Names.identifier * (term * term)) list * (term * term) option ->
   (proof * (Names.identifier * (term * term)) list, 
-   term * term * proof * (Names.identifier * (term * term)) list ) mission
+   Names.constructor * term * term * proof * 
+   (Names.identifier * (term * term)) list ) mission
 
diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 61d04ef9a0..3d6463d1d9 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -20,6 +20,7 @@ open Nameops
 open Inductiveops
 open Declarations
 open Term
+open Termops
 open Tacmach
 open Tactics
 open Tacticals
@@ -38,6 +39,8 @@ let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
 
 let f_equal_theo = constant ["Init";"Logic"] "f_equal"
 
+let eq_rect_theo = constant ["Init";"Logic"] "eq_rect"
+
 (* decompose member of equality in an applicative format *)
 
 let rec decompose_term env t=
@@ -101,8 +104,10 @@ let make_prb gl=
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
 
-let build_projection (cstr:constructor) nargs argind ttype default atype gls=
-  let (h,argv) = destApplication ttype in
+let build_projection intype outtype (cstr:constructor) special default gls=
+  let (h,argv) = 
+    try destApplication intype with 
+	Invalid_argument _ -> (intype,[||])  in
   let ind=destInd h in 
   let (mib,mip) = Global.lookup_inductive ind in
   let n = mip.mind_nparams in
@@ -114,16 +119,16 @@ let build_projection (cstr:constructor) nargs argind ttype default atype gls=
     let ti=Term.prod_appvect types.(i) argv in
     let rc=fst (Sign.decompose_prod_assum ti) in
     let head=
-      if i=ci then mkRel (1+nargs-argind) else default in  
+      if i=ci then special else default in  
       Sign.it_mkLambda_or_LetIn head rc in
   let branches=Array.init lp branch in
   let casee=mkRel 1 in
-  let pred=mkLambda(Anonymous,ttype,atype) in
+  let pred=mkLambda(Anonymous,intype,outtype) in
   let env=pf_env gls in 
   let case_info=make_default_case_info (pf_env gls) RegularStyle ind in
   let body= mkCase(case_info, pred, casee, branches) in
   let id=pf_get_new_id (id_of_string "t") gls in     
-    mkLambda(Name id,ttype,body)
+    mkLambda(Name id,intype,body)
 
 (* generate an adhoc tactic following the proof tree  *)
 
@@ -165,11 +170,13 @@ let rec proof_tac axioms=function
 	 let cti=make_term ti in
 	 let ctj=make_term tj in
 	 let cai=make_term ai in
-	 let ttype=pf_type_of gls cti in
-	 let atype=pf_type_of gls cai in
-	 let proj=build_projection cstr nargs argind ttype cai atype gls in
+	 let intype=pf_type_of gls cti in
+	 let outtype=pf_type_of gls cai in
+	 let special=mkRel (1+nargs-argind) in
+	 let default=make_term ai in
+	 let proj=build_projection intype outtype cstr special default gls in
 	 let injt=
-	   mkApp (Lazy.force f_equal_theo,[|ttype;atype;proj;cti;ctj|]) in   
+	   mkApp (Lazy.force f_equal_theo,[|intype;outtype;proj;cti;ctj|]) in 
 	   tclTHEN (apply injt) (proof_tac axioms prf) gls)
 
 (* wrap everything *)
@@ -179,14 +186,30 @@ let cc_tactic gls=
   let prb=make_prb gls in
     match (cc_proof prb) with
         Prove (p,axioms)-> proof_tac axioms p gls
-      | Refute (t1,t2,p,axioms) ->
+      | Refute (cstr,t1,t2,p,axioms) ->
 	  let tt1=make_term t1 and tt2=make_term t2 in
-	  let typ=pf_type_of gls tt1 in
-	  let id=pf_get_new_id (id_of_string "Heq") gls in     
+	  let intype=pf_type_of gls tt1 in
+	  let concl=pf_concl gls in
+	  let outsort=mkType (new_univ ()) in
+	  let xid=pf_get_new_id (id_of_string "X") gls in
+	  let tid=pf_get_new_id (id_of_string "t") gls in
+	  let identity=
+	    mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
+	  let trivial=pf_type_of gls identity in
+	  let outtype=mkType (new_univ ()) in
+	  let pred=mkLambda(Name xid,outtype,mkRel 1) in
+	  let hid=pf_get_new_id (id_of_string "Heq") gls in     
+	  let proj=build_projection intype outtype cstr trivial concl gls in
+	  let injt=
+	    mkApp (Lazy.force f_equal_theo,
+		   [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in   
+	  let endt=
+	    mkApp (Lazy.force eq_rect_theo,
+		   [|outtype;trivial;pred;identity;concl;injt|]) in
 	  let neweq=
-	    mkApp(constr_of_reference Coqlib.glob_eq,[|typ;tt1;tt2|]) in
-	    tclTHENS (true_cut (Some id) neweq)
-	      [proof_tac axioms p;Equality.discr id] gls
+	    mkApp(constr_of_reference Coqlib.glob_eq,[|intype;tt1;tt2|]) in
+	    tclTHENS (true_cut (Some hid) neweq)
+	      [proof_tac axioms p;exact_check endt] gls
 
 (* Tactic registration *)