← Back to branch summary

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

« back to all changes in this revision

Viewing changes to parsing/ppdecl_proof.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:
parsing/ppdecl_proof.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: ppdecl_proof.ml 10739 2008-04-01 14:45:20Z herbelin $ *)
 
10
 
 
11
open Util 
 
12
open Pp
 
13
open Decl_expr
 
14
open Names 
 
15
open Nameops
 
16
 
 
17
let pr_constr = Printer.pr_constr_env
 
18
let pr_tac = Pptactic.pr_glob_tactic
 
19
let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr 
 
20
 
 
21
let pr_label = function
 
22
    Anonymous -> mt ()
 
23
  | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () 
 
24
 
 
25
let pr_justification_items env = function
 
26
    Some [] -> mt ()
 
27
  | Some (_::_ as l) -> 
 
28
      spc () ++ str "by" ++ spc () ++  
 
29
        prlist_with_sep (fun () -> str ",") (pr_constr env) l
 
30
  | None -> spc () ++ str "by *"
 
31
 
 
32
let pr_justification_method env = function
 
33
    None -> mt ()
 
34
  | Some tac -> 
 
35
      spc () ++ str "using" ++ spc () ++ pr_tac env tac
 
36
 
 
37
let pr_statement pr_it env st = 
 
38
  pr_label st.st_label ++ pr_it env st.st_it
 
39
 
 
40
let pr_or_thesis pr_this env = function
 
41
    Thesis Plain -> str "thesis"
 
42
  | Thesis (For id) -> 
 
43
      str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id 
 
44
  | This c -> pr_this env c
 
45
 
 
46
let pr_cut pr_it env c = 
 
47
  hov 1 (pr_it env c.cut_stat) ++ 
 
48
    pr_justification_items env c.cut_by ++
 
49
    pr_justification_method env c.cut_using
 
50
 
 
51
let type_or_thesis = function
 
52
    Thesis _ -> Term.mkProp
 
53
  | This c -> c
 
54
 
 
55
let _I x = x
 
56
 
 
57
let rec print_hyps pconstr gtyp env sep _be _have hyps = 
 
58
  let pr_sep = if sep then str "and" ++ spc () else mt () in
 
59
    match hyps with 
 
60
        (Hvar _ ::_) as rest -> 
 
61
          spc () ++ pr_sep ++ str _have ++ 
 
62
            print_vars pconstr gtyp env false _be _have rest
 
63
      | Hprop st :: rest -> 
 
64
          begin
 
65
            let nenv =
 
66
              match st.st_label with
 
67
                  Anonymous -> env
 
68
                | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
 
69
              spc() ++ pr_sep ++ pr_statement pconstr env st ++ 
 
70
                print_hyps pconstr gtyp nenv true _be _have rest
 
71
          end
 
72
      | [] -> mt ()
 
73
 
 
74
and print_vars pconstr gtyp env sep _be _have vars =
 
75
  match vars with
 
76
    Hvar st :: rest -> 
 
77
      begin
 
78
        let nenv = 
 
79
          match st.st_label with
 
80
              Anonymous -> anomaly "anonymous variable"
 
81
            | Name id -> Environ.push_named (id,None,st.st_it) env in
 
82
        let pr_sep = if sep then pr_coma () else mt () in
 
83
                spc() ++ pr_sep ++
 
84
                   pr_statement pr_constr env st ++
 
85
                  print_vars pconstr gtyp nenv true _be _have rest
 
86
      end
 
87
   | (Hprop _ :: _) as rest ->
 
88
      let _st =  if _be then 
 
89
        str "be such that" 
 
90
      else 
 
91
        str "such that" in
 
92
        spc() ++ _st ++  print_hyps pconstr gtyp env false _be _have rest
 
93
  | [] -> mt ()
 
94
 
 
95
let pr_suffices_clause env (hyps,c) = 
 
96
    print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++
 
97
       str "to show" ++ spc () ++ pr_or_thesis pr_constr env c
 
98
 
 
99
let pr_elim_type = function
 
100
    ET_Case_analysis -> str "cases"
 
101
  | ET_Induction -> str "induction"
 
102
 
 
103
let pr_casee env =function
 
104
    Real c -> str "on" ++ spc () ++ pr_constr env c
 
105
  | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut
 
106
 
 
107
let pr_side = function
 
108
    Lhs -> str "=~"
 
109
  | Rhs -> str "~="
 
110
 
 
111
let rec pr_bare_proof_instr _then _thus env = function
 
112
  | Pescape -> str "escape"
 
113
  | Pthen i -> pr_bare_proof_instr true _thus env i 
 
114
  | Pthus i -> pr_bare_proof_instr _then true env i 
 
115
  | Phence i -> pr_bare_proof_instr true true env i
 
116
  | Pcut c -> 
 
117
      begin
 
118
        match _then,_thus with
 
119
            false,false -> str "have" ++ spc () ++ 
 
120
              pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
 
121
          | false,true  -> str "thus" ++ spc () ++ 
 
122
              pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
 
123
          | true,false  -> str "then" ++ spc () ++
 
124
              pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
 
125
          | true,true   -> str "hence" ++ spc () ++ 
 
126
              pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
 
127
      end
 
128
  | Psuffices c ->
 
129
      str "suffices" ++  pr_cut pr_suffices_clause env c 
 
130
  | Prew (sid,c) ->
 
131
      (if _thus then str "thus" else str "    ") ++ spc () ++
 
132
        pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c
 
133
  | Passume hyps -> 
 
134
      str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps
 
135
  | Plet hyps -> 
 
136
      str "let" ++ print_vars pr_constr _I env false true "let" hyps
 
137
  | Pclaim st ->
 
138
      str "claim" ++ spc () ++ pr_statement pr_constr env st
 
139
  | Pfocus st ->
 
140
      str "focus on" ++ spc () ++ pr_statement pr_constr env st
 
141
  | Pconsider (id,hyps) ->
 
142
      str "consider" ++ print_vars pr_constr _I env false false "consider" hyps 
 
143
      ++ spc () ++ str "from " ++ pr_constr env id 
 
144
  | Pgiven hyps ->
 
145
      str "given" ++ print_vars pr_constr _I env false false "given" hyps
 
146
  | Ptake witl -> 
 
147
      str "take" ++ spc () ++ 
 
148
        prlist_with_sep pr_coma (pr_constr env) witl
 
149
  | Pdefine (id,args,body) ->
 
150
      str "define" ++ spc () ++ pr_id id ++ spc () ++ 
 
151
        prlist_with_sep spc 
 
152
        (fun st -> str "(" ++ 
 
153
           pr_statement pr_constr env st ++ str ")") args ++ spc () ++ 
 
154
        str "as" ++ (pr_constr env body) 
 
155
  | Pcast (id,typ) -> 
 
156
      str "reconsider" ++ spc () ++ 
 
157
        pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ 
 
158
        str "as" ++ spc () ++ (pr_constr env typ)  
 
159
  | Psuppose hyps -> 
 
160
      str "suppose" ++ 
 
161
        print_hyps pr_constr _I env false false "we have" hyps
 
162
  | Pcase (params,pat,hyps) ->
 
163
      str "suppose it is" ++ spc () ++ pr_pat pat ++
 
164
        (if params = [] then mt () else 
 
165
           (spc () ++ str "with" ++ spc () ++ 
 
166
              prlist_with_sep spc 
 
167
              (fun st -> str "(" ++ 
 
168
                 pr_statement pr_constr env st ++ str ")") params ++ spc ())) 
 
169
      ++
 
170
        (if hyps = [] then mt () else 
 
171
           (spc () ++ str "and" ++ 
 
172
              print_hyps (pr_or_thesis pr_constr) type_or_thesis
 
173
              env false false "we have" hyps))
 
174
  | Pper (et,c) -> 
 
175
      str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
 
176
      pr_casee env c
 
177
  | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
 
178
  | _ -> anomaly "unprintable instruction"
 
179
 
 
180
let pr_emph = function
 
181
    0 -> str "    "
 
182
  | 1 -> str "*   "
 
183
  | 2 -> str "**  "
 
184
  | 3 -> str "*** "
 
185
  | _ -> anomaly "unknown emphasis"
 
186
 
 
187
let pr_proof_instr env instr = 
 
188
  pr_emph instr.emph ++ spc () ++ 
 
189
    pr_bare_proof_instr false false env instr.instr
 
190