diff options
Diffstat (limited to 'contrib/cc/ccproof.ml')
| -rw-r--r-- | contrib/cc/ccproof.ml | 146 |
1 files changed, 86 insertions, 60 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) |