← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/cc/ccproof.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/cc/ccproof.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: ccproof.ml 9857 2007-05-24 14:21:08Z corbinea $ *)
 
10
 
 
11
(* This file uses the (non-compressed) union-find structure to generate *) 
 
12
(* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
13
 
 
14
open Util
 
15
open Names
 
16
open Term
 
17
open Ccalgo
 
18
  
 
19
type rule=
 
20
    Ax of constr
 
21
  | SymAx of constr
 
22
  | Refl of term
 
23
  | Trans of proof*proof
 
24
  | Congr of proof*proof
 
25
  | Inject of proof*constructor*int*int 
 
26
and proof = 
 
27
    {p_lhs:term;p_rhs:term;p_rule:rule}
 
28
 
 
29
let prefl t = {p_lhs=t;p_rhs=t;p_rule=Refl t}
 
30
 
 
31
let pcongr p1 p2 = 
 
32
  match p1.p_rule,p2.p_rule with 
 
33
    Refl t1, Refl t2 -> prefl (Appli (t1,t2))
 
34
  | _, _ -> 
 
35
      {p_lhs=Appli (p1.p_lhs,p2.p_lhs);
 
36
       p_rhs=Appli (p1.p_rhs,p2.p_rhs);
 
37
       p_rule=Congr (p1,p2)}
 
38
 
 
39
let rec ptrans p1 p3=
 
40
  match p1.p_rule,p3.p_rule with
 
41
      Refl _, _ ->p3
 
42
    | _, Refl _ ->p1
 
43
    | Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3)
 
44
    | Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4)
 
45
    | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) ->
 
46
        ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
 
47
  | _, _ -> 
 
48
      if p1.p_rhs = p3.p_lhs then 
 
49
        {p_lhs=p1.p_lhs;
 
50
         p_rhs=p3.p_rhs;
 
51
         p_rule=Trans (p1,p3)}
 
52
      else anomaly "invalid cc transitivity"
 
53
        
 
54
let rec psym p = 
 
55
  match p.p_rule with 
 
56
      Refl _ -> p 
 
57
    | SymAx s ->
 
58
        {p_lhs=p.p_rhs;
 
59
         p_rhs=p.p_lhs;
 
60
         p_rule=Ax s}
 
61
    | Ax s->      
 
62
        {p_lhs=p.p_rhs;
 
63
         p_rhs=p.p_lhs;
 
64
         p_rule=SymAx s}
 
65
  | Inject (p0,c,n,a)-> 
 
66
      {p_lhs=p.p_rhs;
 
67
       p_rhs=p.p_lhs;
 
68
       p_rule=Inject (psym p0,c,n,a)}
 
69
  | Trans (p1,p2)-> ptrans (psym p2) (psym p1)
 
70
  | Congr (p1,p2)-> pcongr (psym p1) (psym p2)
 
71
 
 
72
let pax axioms s =
 
73
  let l,r = Hashtbl.find axioms s in
 
74
    {p_lhs=l;
 
75
     p_rhs=r;
 
76
     p_rule=Ax s}
 
77
 
 
78
let psymax axioms s =
 
79
  let l,r = Hashtbl.find axioms s in
 
80
    {p_lhs=r;
 
81
     p_rhs=l;
 
82
     p_rule=SymAx s}
 
83
 
 
84
let rec nth_arg t n=
 
85
  match t with 
 
86
      Appli (t1,t2)-> 
 
87
        if n>0 then 
 
88
          nth_arg t1 (n-1)
 
89
        else t2
 
90
    | _ -> anomaly "nth_arg: not enough args"
 
91
 
 
92
let pinject p c n a =
 
93
  {p_lhs=nth_arg p.p_lhs (n-a);
 
94
   p_rhs=nth_arg p.p_rhs (n-a);
 
95
   p_rule=Inject(p,c,n,a)}
 
96
 
 
97
let build_proof uf=
 
98
 
 
99
  let axioms = axioms uf in
 
100
 
 
101
  let rec equal_proof i j=
 
102
    if i=j then prefl (term uf i) else 
 
103
      let (li,lj)=join_path uf i j in
 
104
        ptrans (path_proof i li) (psym (path_proof j lj))
 
105
  
 
106
  and edge_proof ((i,j),eq)=
 
107
    let pi=equal_proof i eq.lhs in
 
108
    let pj=psym (equal_proof j eq.rhs) in
 
109
    let pij=
 
110
      match eq.rule with 
 
111
          Axiom (s,reversed)->
 
112
            if reversed then psymax axioms s 
 
113
            else pax axioms s
 
114
        | Congruence ->congr_proof eq.lhs eq.rhs
 
115
        | Injection (ti,ipac,tj,jpac,k) ->
 
116
            let p=ind_proof ti ipac tj jpac in
 
117
            let cinfo= get_constructor_info uf ipac.cnode in
 
118
              pinject p cinfo.ci_constr cinfo.ci_nhyps k        
 
119
    in  ptrans (ptrans pi pij) pj
 
120
 
 
121
  and constr_proof i t ipac=
 
122
    if ipac.args=[] then
 
123
      equal_proof i t
 
124
    else
 
125
      let npac=tail_pac ipac in
 
126
      let (j,arg)=subterms uf t in
 
127
      let targ=term uf arg in
 
128
      let rj=find uf j in
 
129
      let u=find_pac uf rj npac in
 
130
      let p=constr_proof j u npac in
 
131
        ptrans (equal_proof i t) (pcongr p (prefl targ))
 
132
 
 
133
  and path_proof i=function
 
134
      [] -> prefl (term uf i)
 
135
    | x::q->ptrans (path_proof (snd (fst x)) q) (edge_proof x)
 
136
  
 
137
  and congr_proof i j=
 
138
    let (i1,i2) = subterms uf i
 
139
    and (j1,j2) = subterms uf j in   
 
140
      pcongr (equal_proof i1 j1) (equal_proof i2 j2)
 
141
        
 
142
  and ind_proof i ipac j jpac=
 
143
    let p=equal_proof i j 
 
144
    and p1=constr_proof i i ipac 
 
145
    and p2=constr_proof j j jpac in
 
146
      ptrans (psym p1) (ptrans p p2)
 
147
  in
 
148
    function
 
149
        `Prove (i,j) -> equal_proof i j
 
150
      | `Discr (i,ci,j,cj)-> ind_proof i ci j cj
 
151
 
 
152
 
 
153