diff options
Diffstat (limited to 'contrib/cc/ccproof.ml')
| -rw-r--r-- | contrib/cc/ccproof.ml | 153 |
1 files changed, 0 insertions, 153 deletions
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml deleted file mode 100644 index a459b18f..00000000 --- a/contrib/cc/ccproof.ml +++ /dev/null @@ -1,153 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: ccproof.ml 9857 2007-05-24 14:21:08Z corbinea $ *) - -(* 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 Term -open Ccalgo - -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 -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 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 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 - - - |