Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

3 files changed, 181 insertions, 132 deletions

diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index 1ffa347a..d336f599 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ccproof.ml 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: ccproof.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
 
 (* This file uses the (non-compressed) union-find structure to generate *) 
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
@@ -16,58 +16,107 @@ open Names
 open Term
 open Ccalgo
   
-type proof=
+type rule=
     Ax of constr
   | SymAx of constr
   | Refl of term
   | Trans of proof*proof
   | Congr of proof*proof
   | Inject of proof*constructor*int*int 
-		  
-let pcongr=function
-    Refl t1, Refl t2 -> Refl (Appli (t1,t2))
-  | p1, p2 -> Congr (p1,p2)
-
-let rec ptrans=function
-    Refl _, p ->p
-  | p, Refl _ ->p
-  | Trans(p1,p2), p3 ->ptrans(p1,ptrans (p2,p3))
-  | Congr(p1,p2), Congr(p3,p4) ->pcongr(ptrans(p1,p3),ptrans(p2,p4))
-  | Congr(p1,p2), Trans(Congr(p3,p4),p5) ->
-      ptrans(pcongr(ptrans(p1,p3),ptrans(p2,p4)),p5)
-  | p1, p2 ->Trans (p1,p2)
-	
-let rec psym=function
-    Refl p->Refl p
-  | SymAx s->Ax s
-  | Ax s-> SymAx s
-  | Inject (p,c,n,a)-> Inject (psym p,c,n,a)
-  | Trans (p1,p2)-> ptrans (psym p2,psym p1)
-  | Congr (p1,p2)-> pcongr (psym p1,psym p2)
+and proof = 
+    {p_lhs:term;p_rhs:term;p_rule:rule}
+
+let prefl t = {p_lhs=t;p_rhs=t;p_rule=Refl t}
+
+let pcongr p1 p2 = 
+  match p1.p_rule,p2.p_rule with 
+    Refl t1, Refl t2 -> prefl (Appli (t1,t2))
+  | _, _ -> 
+      {p_lhs=Appli (p1.p_lhs,p2.p_lhs);
+       p_rhs=Appli (p1.p_rhs,p2.p_rhs);
+       p_rule=Congr (p1,p2)}
+
+let rec ptrans p1 p3=
+  match p1.p_rule,p3.p_rule with
+      Refl _, _ ->p3
+    | _, Refl _ ->p1
+    | Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3)
+    | Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4)
+    | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) ->
+	ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
+  | _, _ -> 
+      if p1.p_rhs = p3.p_lhs then 
+	{p_lhs=p1.p_lhs;
+	 p_rhs=p3.p_rhs;
+	 p_rule=Trans (p1,p3)}
+      else anomaly "invalid cc transitivity"
 	
-let pcongr=function
-    Refl t1, Refl t2 ->Refl (Appli (t1,t2))
-  | p1, p2 -> Congr (p1,p2)
+let rec psym p = 
+  match p.p_rule with 
+      Refl _ -> p 
+    | SymAx s ->
+	{p_lhs=p.p_rhs;
+	 p_rhs=p.p_lhs;
+	 p_rule=Ax s}
+    | Ax s->      
+	{p_lhs=p.p_rhs;
+	 p_rhs=p.p_lhs;
+	 p_rule=SymAx s}
+  | Inject (p0,c,n,a)-> 
+      {p_lhs=p.p_rhs;
+       p_rhs=p.p_lhs;
+       p_rule=Inject (psym p0,c,n,a)}
+  | Trans (p1,p2)-> ptrans (psym p2) (psym p1)
+  | Congr (p1,p2)-> pcongr (psym p1) (psym p2)
+
+let pax axioms s =
+  let l,r = Hashtbl.find axioms s in
+    {p_lhs=l;
+     p_rhs=r;
+     p_rule=Ax s}
+
+let psymax axioms s =
+  let l,r = Hashtbl.find axioms s in
+    {p_lhs=r;
+     p_rhs=l;
+     p_rule=SymAx s}
+
+let rec nth_arg t n=
+  match t with 
+      Appli (t1,t2)-> 
+	if n>0 then 
+	  nth_arg t1 (n-1)
+	else t2
+    | _ -> anomaly "nth_arg: not enough args"
+
+let pinject p c n a =
+  {p_lhs=nth_arg p.p_lhs (n-a);
+   p_rhs=nth_arg p.p_rhs (n-a);
+   p_rule=Inject(p,c,n,a)}
 
 let build_proof uf=
-  
+
+  let axioms = axioms uf in
+
   let rec equal_proof i j=
-    if i=j then Refl (term uf i) else 
+    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))
+	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 SymAx s else Ax s
+	  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
-	      Inject(p,cinfo.ci_constr,cinfo.ci_nhyps,k)	
-    in  ptrans(ptrans (pi,pij),pj)
+	      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
@@ -79,49 +128,26 @@ let build_proof uf=
       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,Refl targ))
+	ptrans (equal_proof i t) (pcongr p (prefl targ))
 
   and path_proof i=function
-      [] -> Refl (term uf i)
-    | x::q->ptrans (path_proof (snd (fst x)) q,edge_proof x)
+      [] -> 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)
+      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))
+      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 rec nth_arg t n=
-  match t with 
-      Appli (t1,t2)-> 
-	if n>0 then 
-	  nth_arg t1 (n-1)
-	else t2
-    | _ -> anomaly "nth_arg: not enough args"
 
-let rec type_proof axioms p=
-  match p with
-      Ax s->Hashtbl.find axioms s
-    | SymAx s-> let (t1,t2)=Hashtbl.find axioms s in (t2,t1)
-    | Refl t-> t,t
-    | Trans (p1,p2)->
-	let (s1,t1)=type_proof axioms p1 
-	and (t2,s2)=type_proof axioms p2 in
-	  if t1=t2 then (s1,s2) else anomaly "invalid cc transitivity"
-    | Congr (p1,p2)->
-	let (i1,j1)=type_proof axioms p1
-	and (i2,j2)=type_proof axioms p2 in
-	  Appli (i1,i2),Appli (j1,j2)
-    | Inject (p,c,n,a)->
-	let (ti,tj)=type_proof axioms p in
-	  nth_arg ti (n-a),nth_arg tj (n-a)
 
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
index abdd6fea..572b2c53 100644
--- a/contrib/cc/ccproof.mli
+++ b/contrib/cc/ccproof.mli
@@ -6,26 +6,26 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ccproof.mli 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: ccproof.mli 9856 2007-05-24 14:05:40Z corbinea $ *)
 
 open Ccalgo
 open Names
 open Term
 
-type proof =
+type rule=
     Ax of constr
   | SymAx of constr
   | Refl of term
-  | Trans of proof * proof
-  | Congr of proof * proof
-  | Inject of proof * constructor * int * int
+  | Trans of proof*proof
+  | Congr of proof*proof
+  | Inject of proof*constructor*int*int 
+and proof = 
+    private {p_lhs:term;p_rhs:term;p_rule:rule}
 
 val build_proof : 
   forest -> 
   [ `Discr of int * pa_constructor * int * pa_constructor
   | `Prove of int * int ] -> proof
 
-val type_proof :
-  (constr, (term * term)) Hashtbl.t -> proof -> term * term
 
 
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index ea8aceeb..86251254 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: cctac.ml 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: cctac.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
 
 (* This file is the interface between the c-c algorithm and Coq *)
 
@@ -37,6 +37,12 @@ let _f_equal = constant ["Init";"Logic"] "f_equal"
 
 let _eq_rect = constant ["Init";"Logic"] "eq_rect"
 
+let _refl_equal = constant ["Init";"Logic"] "refl_equal"
+
+let _sym_eq = constant ["Init";"Logic"] "sym_eq"
+
+let _trans_eq = constant ["Init";"Logic"] "trans_eq"
+
 let _eq = constant ["Init";"Logic"] "eq"
 
 let _False = constant ["Init";"Logic"] "False"
@@ -210,54 +216,73 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   
 (* generate an adhoc tactic following the proof tree  *)
 
-let rec proof_tac axioms=function
-    Ax c -> exact_check c
-  | SymAx c -> tclTHEN symmetry (exact_check c)
-  | Refl t -> reflexivity
-  | Trans (p1,p2)->let t=(constr_of_term (snd (type_proof axioms p1))) in
-      (tclTHENS (transitivity t) 
-	 [(proof_tac axioms p1);(proof_tac axioms p2)])
-  | Congr (p1,p2)->
-      fun gls->
-	let (f1,f2)=(type_proof axioms p1) 
-	and (x1,x2)=(type_proof axioms p2) in
-        let tf1=constr_of_term f1 and tx1=constr_of_term x1 
-	and tf2=constr_of_term f2 and tx2=constr_of_term x2 in
-	let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1
-	and typfx=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|])
-	and lemma2=
-	  mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2|]) in
-	  (tclTHENS (transitivity (mkApp(tf2,[|tx1|])))
-	     [tclTHEN (apply lemma1) (proof_tac axioms p1);
-  	      tclFIRST
-		[tclTHEN (apply lemma2) (proof_tac axioms p2);
-		 reflexivity;
-		 fun gls ->
-		   errorlabstrm  "Congruence" 
-		   (Pp.str 
-		      "I don't know how to handle dependent equality")]]
-	     gls)
-  | Inject (prf,cstr,nargs,argind)  as gprf->
-      (fun gls ->
-	 let ti,tj=type_proof axioms prf in
-	 let ai,aj=type_proof axioms gprf in
-	 let cti=constr_of_term ti in
-	 let ctj=constr_of_term tj in
-	 let cai=constr_of_term ai in
-	 let intype=pf_type_of gls cti in
-	 let outtype=pf_type_of gls cai in
+let _M =mkMeta
+
+let rec proof_tac p gls =
+  match p.p_rule with
+      Ax c -> exact_check c 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 	  
+	  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 
+	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 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
+    | Congr (p1,p2)->
+	let tf1=constr_of_term p1.p_lhs 
+	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 = prod_applist typf [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
+	let prf = 
+	  mkApp(Lazy.force _trans_eq,
+		[|typfx;
+		  mkApp(tf1,[|tx1|]);
+		  mkApp(tf2,[|tx1|]);
+		  mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in
+	  tclTHENS (refine prf)
+	    [tclTHEN (refine lemma1) (proof_tac p1);
+  	     tclFIRST
+	       [tclTHEN (refine lemma2) (proof_tac p2);
+		reflexivity;
+		fun gls ->
+		  errorlabstrm  "Congruence" 
+		    (Pp.str 
+		       "I don't know how to handle dependent equality")]] gls
+  | Inject (prf,cstr,nargs,argind) ->
+	 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 special=mkRel (1+nargs-argind) in
-	 let default=constr_of_term ai in
 	 let proj=build_projection intype outtype cstr special default gls in
 	 let injt=
-	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;cti;ctj|]) in 
-	   tclTHEN (apply injt) (proof_tac axioms prf) gls)
+	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in 
+	   tclTHEN (refine injt) (proof_tac prf) gls
 
-let refute_tac axioms c t1 t2 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 neweq=
@@ -266,9 +291,9 @@ let refute_tac axioms c t1 t2 p gls =
   let hid=pf_get_new_id (id_of_string "Heq") gls in
   let false_t=mkApp (c,[|mkVar hid|]) in
     tclTHENS (true_cut (Name hid) neweq)
-      [proof_tac axioms p; simplest_elim false_t] gls
+      [proof_tac p; simplest_elim false_t] gls
 
-let convert_to_goal_tac axioms 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 neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in 
@@ -278,20 +303,19 @@ let convert_to_goal_tac axioms c t1 t2 p gls =
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
     tclTHENS (true_cut (Name e) neweq) 
-      [proof_tac axioms p;exact_check endt] gls
+      [proof_tac p;exact_check endt] gls
 
-let convert_to_hyp_tac axioms c1 t1 c2 t2 p gls =
+let convert_to_hyp_tac c1 t1 c2 t2 p gls =
   let tt2=constr_of_term t2 in
   let h=pf_get_new_id (id_of_string "H") gls in
   let false_t=mkApp (c2,[|mkVar h|]) in
     tclTHENS (true_cut (Name h) tt2)
-      [convert_to_goal_tac axioms c1 t1 t2 p;
+      [convert_to_goal_tac c1 t1 t2 p;
        simplest_elim false_t] gls
   
-let discriminate_tac axioms cstr p gls =
-  let t1,t2=type_proof axioms p in 
-  let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype=pf_type_of gls tt1 in
+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 concl=pf_concl gls in
   let outsort=mkType (new_univ ()) in
   let xid=pf_get_new_id (id_of_string "X") gls in
@@ -303,12 +327,12 @@ let discriminate_tac axioms cstr p gls =
   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,
-		  [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in   
+		  [|intype;outtype;proj;t1;t2;mkVar hid|]) in   
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|outtype;trivial;pred;identity;concl;injt|]) in
-  let neweq=mkApp(Lazy.force _eq,[|intype;tt1;tt2|]) in
+  let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
     tclTHENS (true_cut (Name hid) neweq) 
-      [proof_tac axioms p;exact_check endt] gls
+      [proof_tac p;exact_check endt] gls
       
 (* wrap everything *)
 	
@@ -333,12 +357,12 @@ let cc_tactic depth additionnal_terms gls=
 	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
 	  match reason with
 	      Discrimination (i,ipac,j,jpac) ->
-		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in	  
+		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
 		let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
-		  discriminate_tac (axioms uf) cstr p gls
+		  discriminate_tac cstr p gls
 	    | Incomplete ->
 		let metacnt = ref 0 in
-		let newmeta _ = incr metacnt; mkMeta !metacnt in
+		let newmeta _ = incr metacnt; _M !metacnt in
 		let terms_to_complete = 
 		  List.map 
 		    (build_term_to_complete uf newmeta) 
@@ -363,14 +387,13 @@ let cc_tactic depth additionnal_terms gls=
 	    | Contradiction dis ->
 		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
 		let ta=term uf dis.lhs and tb=term uf dis.rhs in
-		let axioms = axioms uf in 
 		  match dis.rule with
-		      Goal -> proof_tac axioms p gls
-		    | Hyp id -> refute_tac axioms id ta tb p gls
+		      Goal -> proof_tac p gls
+		    | Hyp id -> refute_tac id ta tb p gls
 		    | HeqG id -> 
-			convert_to_goal_tac axioms id ta tb p gls
+			convert_to_goal_tac id ta tb p gls
 		    | HeqnH (ida,idb) -> 
-			convert_to_hyp_tac axioms ida ta idb tb p gls
+			convert_to_hyp_tac ida ta idb tb p gls
 		    
 
 let cc_fail gls =