summaryrefslogtreecommitdiff
path: root/parsing/ppdecl_proof.ml
blob: c0eddcc59a7e8e196f6a7a5f5e553fa4d5fdb5fb (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: ppdecl_proof.ml 14641 2011-11-06 11:59:10Z herbelin $ *)

open Util
open Pp
open Decl_expr
open Names
open Nameops

let pr_constr = Printer.pr_constr_env
let pr_tac = Pptactic.pr_glob_tactic
let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr

let pr_label = function
    Anonymous -> mt ()
  | Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()

let pr_justification_items env = function
    Some [] -> mt ()
  | Some (_::_ as l) ->
      spc () ++ str "by" ++ spc () ++
	prlist_with_sep (fun () -> str ",") (pr_constr env) l
  | None -> spc () ++ str "by *"

let pr_justification_method env = function
    None -> mt ()
  | Some tac ->
      spc () ++ str "using" ++ spc () ++ pr_tac env tac

let pr_statement pr_it env st =
  pr_label st.st_label ++ pr_it env st.st_it

let pr_or_thesis pr_this env = function
    Thesis Plain -> str "thesis"
  | Thesis (For id) ->
      str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id
  | This c -> pr_this env c

let pr_cut pr_it env c =
  hov 1 (pr_it env c.cut_stat) ++
    pr_justification_items env c.cut_by ++
    pr_justification_method env c.cut_using

let type_or_thesis = function
    Thesis _ -> Term.mkProp
  | This c -> c

let _I x = x

let rec print_hyps pconstr gtyp env sep _be _have hyps =
  let pr_sep = if sep then str "and" ++ spc () else mt () in
    match hyps with
	(Hvar _ ::_) as rest ->
	  spc () ++ pr_sep ++ str _have ++
	    print_vars pconstr gtyp env false _be _have rest
      | Hprop st :: rest ->
	  begin
	    let nenv =
	      match st.st_label with
		  Anonymous -> env
		| Name id -> Environ.push_named (id,None,gtyp st.st_it) env in
	      spc() ++ pr_sep ++ pr_statement pconstr env st ++
		print_hyps pconstr gtyp nenv true _be _have rest
	  end
      | [] -> mt ()

and print_vars pconstr gtyp env sep _be _have vars =
  match vars with
    Hvar st :: rest ->
      begin
	let nenv =
	  match st.st_label with
	      Anonymous -> anomaly "anonymous variable"
	    | Name id -> Environ.push_named (id,None,st.st_it) env in
	let pr_sep = if sep then pr_comma () else mt () in
		spc() ++ pr_sep ++
		   pr_statement pr_constr env st ++
		  print_vars pconstr gtyp nenv true _be _have rest
      end
   | (Hprop _ :: _) as rest ->
      let _st =  if _be then
	str "be such that"
      else
	str "such that" in
	spc() ++ _st ++  print_hyps pconstr gtyp env false _be _have rest
  | [] -> mt ()

let pr_suffices_clause env (hyps,c) =
    print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++
       str "to show" ++ spc () ++ pr_or_thesis pr_constr env c

let pr_elim_type = function
    ET_Case_analysis -> str "cases"
  | ET_Induction -> str "induction"

let pr_casee env =function
    Real c -> str "on" ++ spc () ++ pr_constr env c
  | Virtual cut -> str "of" ++ spc () ++ pr_cut (pr_statement pr_constr) env cut

let pr_side = function
    Lhs -> str "=~"
  | Rhs -> str "~="

let rec pr_bare_proof_instr _then _thus env = function
  | Pescape -> str "escape"
  | Pthen i -> pr_bare_proof_instr true _thus env i
  | Pthus i -> pr_bare_proof_instr _then true env i
  | Phence i -> pr_bare_proof_instr true true env i
  | Pcut c ->
      begin
	match _then,_thus with
	    false,false -> str "have" ++ spc () ++
	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
	  | false,true  -> str "thus" ++ spc () ++
	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
	  | true,false  -> str "then" ++ spc () ++
	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
	  | true,true   -> str "hence" ++ spc () ++
	      pr_cut (pr_statement (pr_or_thesis pr_constr)) env c
      end
  | Psuffices c ->
      str "suffices" ++  pr_cut pr_suffices_clause env c
  | Prew (sid,c) ->
      (if _thus then str "thus" else str "    ") ++ spc () ++
	pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c
  | Passume hyps ->
      str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps
  | Plet hyps ->
      str "let" ++ print_vars pr_constr _I env false true "let" hyps
  | Pclaim st ->
      str "claim" ++ spc () ++ pr_statement pr_constr env st
  | Pfocus st ->
      str "focus on" ++ spc () ++ pr_statement pr_constr env st
  | Pconsider (id,hyps) ->
      str "consider" ++ print_vars pr_constr _I env false false "consider" hyps
      ++ spc () ++ str "from " ++ pr_constr env id
  | Pgiven hyps ->
      str "given" ++ print_vars pr_constr _I env false false "given" hyps
  | Ptake witl ->
      str "take" ++ spc () ++
	prlist_with_sep pr_comma (pr_constr env) witl
  | Pdefine (id,args,body) ->
      str "define" ++ spc () ++ pr_id id ++ spc () ++
	prlist_with_sep spc
	(fun st -> str "(" ++
	   pr_statement pr_constr env st ++ str ")") args ++ spc () ++
	str "as" ++ (pr_constr env body)
  | Pcast (id,typ) ->
      str "reconsider" ++ spc () ++
	pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++
	str "as" ++ spc () ++ (pr_constr env typ)
  | Psuppose hyps ->
      str "suppose" ++
	print_hyps pr_constr _I env false false "we have" hyps
  | Pcase (params,pat,hyps) ->
      str "suppose it is" ++ spc () ++ pr_pat pat ++
	(if params = [] then mt () else
	   (spc () ++ str "with" ++ spc () ++
	      prlist_with_sep spc
	      (fun st -> str "(" ++
		 pr_statement pr_constr env st ++ str ")") params ++ spc ()))
      ++
	(if hyps = [] then mt () else
	   (spc () ++ str "and" ++
	      print_hyps (pr_or_thesis pr_constr) type_or_thesis
	      env false false "we have" hyps))
  | Pper (et,c) ->
      str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
      pr_casee env c
  | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
  | _ -> anomaly "unprintable instruction"

let pr_emph = function
    0 -> str "    "
  | 1 -> str "*   "
  | 2 -> str "**  "
  | 3 -> str "*** "
  | _ -> anomaly "unknown emphasis"

let pr_proof_instr env instr =
  pr_emph instr.emph ++ spc () ++
    pr_bare_proof_instr false false env instr.instr