congruence now knows about _ -> _

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

4 files changed, 81 insertions, 41 deletions

diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
index eab2db3086..2d7dd9d6c7 100644
--- a/contrib/cc/ccalgo.ml
+++ b/contrib/cc/ccalgo.ml
@@ -100,6 +100,7 @@ type cinfo=
 
 type term=
     Symb of constr
+  | Product of sorts_family * sorts_family
   | Eps of identifier
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
@@ -319,8 +320,17 @@ let new_representative typ =
     
 (* rebuild a constr from an applicative term *)
     
+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_))
+
 let rec constr_of_term = function
     Symb s->s
+  | Product(s1,s2) -> cc_product s1 s2
   | Eps id -> mkVar id
   | Constructor cinfo -> mkConstruct cinfo.ci_constr 
   | Appli (s1,s2)->
@@ -358,7 +368,7 @@ let rec add_term state t=
 	  let typ = pf_type_of state.gls (constr_of_term t) in
 	  let new_node=
 	    match t with
-		Symb s ->
+		Symb _ | Product (_,_) ->
 		  let paf =
 		    {fsym=b;
 		     fnargs=0} in
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
index 036abd9b31..3bd52b6e1d 100644
--- a/contrib/cc/ccalgo.mli
+++ b/contrib/cc/ccalgo.mli
@@ -19,6 +19,7 @@ type cinfo =
 
 type term =
     Symb of constr
+  | Product of sorts_family * sorts_family
   | Eps of identifier
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index d3c4f65c23..e90e7afaa2 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -24,6 +24,7 @@ open Termops
 open Tacmach
 open Tactics
 open Tacticals
+open Typing
 open Ccalgo
 open Tacinterp
 open Ccproof
@@ -49,6 +50,8 @@ let _False = constant ["Init";"Logic"] "False"
 
 (* decompose member of equality in an applicative format *)
 
+let sf_of env sigma c = family_of_sort (destSort (type_of env sigma c))
+
 let whd env=
   let infos=Closure.create_clos_infos Closure.betaiotazeta env in
     (fun t -> Closure.whd_val infos (Closure.inject t))
@@ -57,12 +60,19 @@ let whd_delta env=
    let infos=Closure.create_clos_infos Closure.betadeltaiota env in
     (fun t -> Closure.whd_val infos (Closure.inject t))
 
-let rec decompose_term env t=
+let rec decompose_term env sigma t=
     match kind_of_term (whd env t) with
       App (f,args)->
-	let tf=decompose_term env f in
-	let targs=Array.map (decompose_term env) args in
+	let tf=decompose_term env sigma f in
+	let targs=Array.map (decompose_term env sigma) args in
 	  Array.fold_left (fun s t->Appli (s,t)) tf targs
+    | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
+	let b = pop _b in
+	let sort_b = sf_of env sigma b in
+	let sort_a = sf_of env sigma a in
+	Appli(Appli(Product (sort_a,sort_b) ,
+		    decompose_term env sigma a),
+	      decompose_term env sigma b)
     | Construct c->
 	let (oib,_)=Global.lookup_inductive (fst c) in
 	let nargs=mis_constructor_nargs_env env c in
@@ -73,42 +83,50 @@ let rec decompose_term env t=
 	
 (* decompose equality in members and type *)
 	
-let atom_of_constr env term =
+let atom_of_constr env sigma term =
   let wh =  (whd_delta env term) in
   let kot = kind_of_term wh in 
     match kot with
       App (f,args)->
 	  if eq_constr f (Lazy.force _eq) && (Array.length args)=3 
 	  then `Eq (args.(0),
-		   decompose_term env args.(1), 
-		   decompose_term env args.(2)) 
-	  else `Other (decompose_term env term)
-    | _ -> `Other (decompose_term env term)
+		   decompose_term env sigma args.(1), 
+		   decompose_term env sigma args.(2)) 
+	  else `Other (decompose_term env sigma term)
+    | _ -> `Other (decompose_term env sigma term)
 
-let rec pattern_of_constr env c =
+let rec pattern_of_constr env sigma c =
   match kind_of_term (whd env c) with
       App (f,args)->
-	let pf = decompose_term env f in
+	let pf = decompose_term env sigma f in
 	let pargs,lrels = List.split 
-	  (array_map_to_list (pattern_of_constr env) args) in
+	  (array_map_to_list (pattern_of_constr env sigma) args) in
 	  PApp (pf,List.rev pargs),
-	List.fold_left Intset.union Intset.empty lrels 
+	List.fold_left Intset.union Intset.empty lrels
+    | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
+	let b =pop _b in
+	let pa,sa = pattern_of_constr env sigma a in
+	let pb,sb = pattern_of_constr env sigma (pop b) in
+	let sort_b = sf_of env sigma b in
+	let sort_a = sf_of env sigma a in
+	  PApp(Product (sort_a,sort_b),
+	       [pa;pb]),(Intset.union sa sb)
     | Rel i -> PVar i,Intset.singleton i
     | _ -> 
-	let pf = decompose_term env c in
+	let pf = decompose_term env sigma c in
 	  PApp (pf,[]),Intset.empty
 
 let non_trivial = function
     PVar _ -> false
   | _ -> true
 
-let patterns_of_constr env nrels term=
+let patterns_of_constr env sigma nrels term=
   let f,args= 
     try destApp (whd_delta env term) with _ -> raise Not_found in
 	if eq_constr f (Lazy.force _eq) && (Array.length args)=3 
 	then 
-	  let patt1,rels1 = pattern_of_constr env args.(1)
-	  and patt2,rels2 = pattern_of_constr env args.(2) in
+	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
+	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
 	  let valid1 = 
 	    if Intset.cardinal rels1 <> nrels then Creates_variables
 	    else if non_trivial patt1 then Normal
@@ -123,52 +141,53 @@ let patterns_of_constr env nrels term=
 	    else raise Not_found
 	else raise Not_found
 
-let rec quantified_atom_of_constr env nrels term =
+let rec quantified_atom_of_constr env sigma nrels term =
   match kind_of_term (whd_delta env term) with
       Prod (_,atom,ff) -> 
 	if eq_constr ff (Lazy.force _False) then
-	  let patts=patterns_of_constr env nrels atom in
+	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
-	  quantified_atom_of_constr env (succ nrels) ff
+	  quantified_atom_of_constr env sigma (succ nrels) ff
     | _ ->  
-	let patts=patterns_of_constr env nrels term in
+	let patts=patterns_of_constr env sigma nrels term in
 	    `Rule patts	  
 
-let litteral_of_constr env term=
+let litteral_of_constr env sigma term=
   match kind_of_term (whd_delta env term) with
     | Prod (_,atom,ff) -> 
 	if eq_constr ff (Lazy.force _False) then
-	  match (atom_of_constr env atom) with
+	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
 	    | `Other(p) -> `Nother(p)
 	else
 	  begin
 	    try 
-	      quantified_atom_of_constr env 1 ff  
+	      quantified_atom_of_constr env sigma 1 ff  
 	    with Not_found ->
-	      `Other (decompose_term env term)
+	      `Other (decompose_term env sigma term)
 	  end
     | _ -> 
-	atom_of_constr env term
+	atom_of_constr env sigma term
 	
 
 (* store all equalities from the context *)
 	
 let rec make_prb gls depth additionnal_terms =
   let env=pf_env gls in
+  let sigma=sig_sig gls in
   let state = empty depth gls in
   let pos_hyps = ref [] in
   let neg_hyps =ref [] in
     List.iter
       (fun c ->
-	 let t = decompose_term env c in
+	 let t = decompose_term env sigma c in
 	   ignore (add_term state t)) additionnal_terms; 
     List.iter 
       (fun (id,_,e) ->
 	 begin
 	   let cid=mkVar id in
-	   match litteral_of_constr env e with
+	   match litteral_of_constr env sigma e with
 	       `Eq (t,a,b) -> add_equality state cid a b
 	     | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
 	     | `Other ph ->
@@ -187,7 +206,7 @@ let rec make_prb gls depth additionnal_terms =
 	     | `Nrule patts -> add_quant state id false patts
 	 end) (Environ.named_context_of_val gls.it.evar_hyps);
     begin
-      match atom_of_constr env gls.it.evar_concl with
+      match atom_of_constr env sigma gls.it.evar_concl with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
 	|	`Other g ->  
 		  List.iter 
@@ -231,19 +250,19 @@ let rec proof_tac p gls =
     | SymAx c -> 
 	let l=constr_of_term p.p_lhs and 
 	    r=constr_of_term p.p_rhs in
-        let typ = pf_type_of gls l in 	  
+        let typ = refresh_universes (pf_type_of gls l) in 	  
 	  exact_check
 	    (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
     | Refl t ->
 	let lr = constr_of_term t in
-	let typ = pf_type_of gls lr in 
+	let typ = refresh_universes (pf_type_of gls lr) in 
 	exact_check
 	   (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
     | Trans (p1,p2)->
 	let t1 = constr_of_term p1.p_lhs and
 	    t2 = constr_of_term p1.p_rhs and
 	    t3 = constr_of_term p2.p_rhs in
-	let typ = pf_type_of gls t2 in 
+	let typ = refresh_universes (pf_type_of gls t2) in 
 	let prf = 
 	  mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
 	  tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
@@ -252,16 +271,17 @@ let rec proof_tac p gls =
 	and tx1=constr_of_term p2.p_lhs 
 	and tf2=constr_of_term p1.p_rhs 
 	and tx2=constr_of_term p2.p_rhs in
-	let typf = pf_type_of gls tf1 in
-	let typx = pf_type_of gls tx1 in
-	let typfx = pf_type_of gls (mkApp (tf1,[|tx1|])) in
+	let typf = refresh_universes (pf_type_of gls tf1) in
+	let typx = refresh_universes (pf_type_of gls tx1) in
+	let typfx = refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
 	let id = pf_get_new_id (id_of_string "f") gls in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
 	  mkApp(Lazy.force _f_equal,
 		[|typf;typfx;appx1;tf1;tf2;_M 1|]) in
 	let lemma2=
-	  mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
+	  mkApp(Lazy.force _f_equal,
+		[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
 	let prf = 
 	  mkApp(Lazy.force _trans_eq,
 		[|typfx;
@@ -281,8 +301,8 @@ let rec proof_tac p gls =
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
 	 let default=constr_of_term p.p_lhs in
-	 let intype=pf_type_of gls ti in
-	 let outtype=pf_type_of gls default in
+	 let intype=refresh_universes (pf_type_of gls ti) in
+	 let outtype=refresh_universes (pf_type_of gls default) in
 	 let special=mkRel (1+nargs-argind) in
 	 let proj=build_projection intype outtype cstr special default gls in
 	 let injt=
@@ -291,7 +311,7 @@ let rec proof_tac p gls =
 
 let refute_tac c t1 t2 p gls =      
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype=pf_type_of gls tt1 in
+  let intype=refresh_universes (pf_type_of gls tt1) in
   let neweq=
     mkApp(Lazy.force _eq,
 	  [|intype;tt1;tt2|]) in
@@ -302,7 +322,7 @@ let refute_tac c t1 t2 p gls =
 
 let convert_to_goal_tac c t1 t2 p gls =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let sort=pf_type_of gls tt2 in
+  let sort=refresh_universes (pf_type_of gls tt2) in
   let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in 
   let e=pf_get_new_id (id_of_string "e") gls in
   let x=pf_get_new_id (id_of_string "X") gls in
@@ -322,7 +342,7 @@ let convert_to_hyp_tac c1 t1 c2 t2 p gls =
   
 let discriminate_tac cstr p gls =
   let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
-  let intype=pf_type_of gls t1 in
+  let intype=refresh_universes (pf_type_of gls t1) 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
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index fecc897722..94d827fd5c 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -78,6 +78,14 @@ intros.
  congruence.
 Qed.
 
+(* example with implications *)
+
+Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D  -> 
+(A -> C) = (B -> D).
+congruence.
+Qed.
+
+
 Set Implicit Arguments.
 
 Parameter elt: Set.
@@ -94,5 +102,6 @@ Proof.
   auto.
 Qed.
             
+
             
             
\ No newline at end of file