diff options
Diffstat (limited to 'plugins/cc/ccproof.ml')
| -rw-r--r-- | plugins/cc/ccproof.ml | 123 |
1 files changed, 64 insertions, 59 deletions
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 |