From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 plugins/cc/ccproof.ml | 123 ++++++++++++++++++++++++++------------------------
 1 file changed, 64 insertions(+), 59 deletions(-)

(limited to 'plugins/cc/ccproof.ml')

diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 037e9f66..42c03234 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.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        *)
@@ -9,10 +9,10 @@
 (* This file uses the (non-compressed) union-find structure to generate *)
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
-open Util
-open Names
+open Errors
 open Term
 open Ccalgo
+open Pp
 
 type rule=
     Ax of constr
@@ -20,7 +20,7 @@ type rule=
   | Refl of term
   | Trans of proof*proof
   | Congr of proof*proof
-  | Inject of proof*constructor*int*int
+  | Inject of proof*pconstructor*int*int
 and proof =
     {p_lhs:term;p_rhs:term;p_rule:rule}
 
@@ -47,7 +47,7 @@ let rec ptrans p1 p3=
 	{p_lhs=p1.p_lhs;
 	 p_rhs=p3.p_rhs;
 	 p_rule=Trans (p1,p3)}
-      else anomaly "invalid cc transitivity"
+      else anomaly (Pp.str "invalid cc transitivity")
 
 let rec psym p =
   match p.p_rule with
@@ -85,67 +85,72 @@ let rec nth_arg t n=
 	if n>0 then
 	  nth_arg t1 (n-1)
 	else t2
-    | _ -> anomaly "nth_arg: not enough args"
+    | _ -> anomaly ~label:"nth_arg" (Pp.str "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 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
 
 
 
-- 
cgit v1.2.3