coq.ml 16.4 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4
5
6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
MARCHE Claude's avatar
MARCHE Claude committed
7
8
9
10
11
12
13
14
15
16
17
18
19
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

Francois Bobot's avatar
Francois Bobot committed
20
21
(** Coq printer *)

MARCHE Claude's avatar
MARCHE Claude committed
22
23
24
25
26
27
28
open Format
open Pp
open Util
open Ident
open Ty
open Term
open Decl
29
open Printer
MARCHE Claude's avatar
MARCHE Claude committed
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51

let iprinter,tprinter,lprinter,pprinter =
  let bl = [ "at"; "cofix"; "exists2"; "fix"; "IF"; "mod"; "Prop";
	     "return"; "Set"; "Type"; "using"; "where"]
  in
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
  let usanitize = sanitizer char_to_ualpha char_to_alnumus in
  create_ident_printer bl ~sanitizer:isanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
  create_ident_printer bl ~sanitizer:usanitize

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
  forget_all lprinter;
  forget_all pprinter

let tv_set = ref Sid.empty

(* type variables *)
MARCHE Claude's avatar
MARCHE Claude committed
52

MARCHE Claude's avatar
MARCHE Claude committed
53
let print_tv fmt tv =
MARCHE Claude's avatar
MARCHE Claude committed
54
  let n = id_unique iprinter tv.tv_name in
MARCHE Claude's avatar
MARCHE Claude committed
55
56
  fprintf fmt "%s" n

MARCHE Claude's avatar
MARCHE Claude committed
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
let print_tv_binder fmt tv =
  tv_set := Sid.add tv.tv_name !tv_set;
  let n = id_unique iprinter tv.tv_name in
  fprintf fmt "(%s:Type)" n

let print_ne_params fmt stv =
  Stv.iter
    (fun tv -> fprintf fmt "@ %a" print_tv_binder tv)
    stv

let print_ne_params_list fmt ltv =
  List.iter
    (fun tv -> fprintf fmt "@ %a" print_tv_binder tv)
    ltv

let print_params fmt stv =
  if Stv.is_empty stv then () else
    fprintf fmt "forall%a,@ " print_ne_params stv

let print_params_list fmt ltv =
  match ltv with
78
    | [] -> ()
MARCHE Claude's avatar
MARCHE Claude committed
79
80
    | _ -> fprintf fmt "forall%a,@ " print_ne_params_list ltv

MARCHE Claude's avatar
MARCHE Claude committed
81
82
83
84
85
86
let forget_tvs () =
  Sid.iter (forget_id iprinter) !tv_set;
  tv_set := Sid.empty

(* logic variables *)
let print_vs fmt vs =
MARCHE Claude's avatar
MARCHE Claude committed
87
  let n = id_unique iprinter vs.vs_name in
MARCHE Claude's avatar
MARCHE Claude committed
88
89
90
91
92
93
94
95
  fprintf fmt "%s" n

let forget_var vs = forget_id iprinter vs.vs_name

let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)

let print_ls fmt ls =
MARCHE Claude's avatar
MARCHE Claude committed
96
  fprintf fmt "%s" (id_unique lprinter ls.ls_name)
MARCHE Claude's avatar
MARCHE Claude committed
97
98
99
100

let print_pr fmt pr =
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)

101
102
103
(* info *)

type info = {
Andrei Paskevich's avatar
Andrei Paskevich committed
104
  info_syn : string Mid.t;
105
106
107
  info_rem : Sid.t;
}

MARCHE Claude's avatar
MARCHE Claude committed
108
109
(** Types *)

110
let rec print_ty info fmt ty = match ty.ty_node with
MARCHE Claude's avatar
MARCHE Claude committed
111
  | Tyvar v -> print_tv fmt v
MARCHE Claude's avatar
MARCHE Claude committed
112
  | Tyapp (ts, tl) when is_ts_tuple ts ->
113
      begin
MARCHE Claude's avatar
MARCHE Claude committed
114
115
116
        match tl with
          | []  -> fprintf fmt "unit"
          | [ty] -> print_ty info fmt ty
MARCHE Claude's avatar
MARCHE Claude committed
117
          | _   -> fprintf fmt "(%a)%%type" (print_list star (print_ty info)) tl
118
119
      end
  | Tyapp (ts, tl) ->
MARCHE Claude's avatar
MARCHE Claude committed
120
121
      begin match query_syntax info.info_syn ts.ts_name with
        | Some s -> syntax_arguments s (print_ty info) fmt tl
122
123
        | None ->
            begin
MARCHE Claude's avatar
MARCHE Claude committed
124
125
126
127
128
129
              match tl with
                | []  -> print_ts fmt ts
                | l   -> fprintf fmt "(%a@ %a)" print_ts ts
                    (print_list space (print_ty info)) l
            end
      end
MARCHE Claude's avatar
MARCHE Claude committed
130
131
132
133

(* can the type of a value be derived from the type of the arguments? *)
let unambig_fs fs =
  let rec lookup v ty = match ty.ty_node with
134
    | Tyvar u when tv_equal u v -> true
MARCHE Claude's avatar
MARCHE Claude committed
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
    | _ -> ty_any (lookup v) ty
  in
  let lookup v = List.exists (lookup v) fs.ls_args in
  let rec inspect ty = match ty.ty_node with
    | Tyvar u when not (lookup u) -> false
    | _ -> ty_all inspect ty
  in
  inspect (of_option fs.ls_value)

(** Patterns, terms, and formulas *)

let lparen_l fmt () = fprintf fmt "@ ("
let lparen_r fmt () = fprintf fmt "(@,"
let print_paren_l fmt x = print_list_delim lparen_l rparen comma fmt x
let print_paren_r fmt x = print_list_delim lparen_r rparen comma fmt x

MARCHE Claude's avatar
MARCHE Claude committed
151
152
153
154
let arrow fmt () = fprintf fmt "@ -> "
let print_arrow_list fmt x = print_list arrow fmt x
let print_space_list fmt x = print_list space fmt x

155
let rec print_pat info fmt p = match p.pat_node with
MARCHE Claude's avatar
MARCHE Claude committed
156
157
  | Pwild -> fprintf fmt "_"
  | Pvar v -> print_vs fmt v
Andrei Paskevich's avatar
Andrei Paskevich committed
158
159
160
161
  | Pas (p,v) ->
      fprintf fmt "(%a as %a)" (print_pat info) p print_vs v
  | Por (p,q) ->
      fprintf fmt "(%a|%a)" (print_pat info) p (print_pat info) q
162
  | Papp (cs,pl) when is_fs_tuple cs ->
MARCHE Claude's avatar
MARCHE Claude committed
163
      fprintf fmt "%a" (print_paren_r (print_pat info)) pl
164
  | Papp (cs,pl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
165
166
      begin match query_syntax info.info_syn cs.ls_name with
        | Some s -> syntax_arguments s (print_pat info) fmt pl
167
168
        | _ -> fprintf fmt "%a %a"
            print_ls cs (print_list space (print_pat info)) pl
Andrei Paskevich's avatar
Andrei Paskevich committed
169
      end
MARCHE Claude's avatar
MARCHE Claude committed
170

171
172
let print_vsty_nopar info fmt v =
  fprintf fmt "%a:%a" print_vs v (print_ty info) v.vs_ty
MARCHE Claude's avatar
MARCHE Claude committed
173

174
175
let print_vsty info fmt v =
  fprintf fmt "(%a)" (print_vsty_nopar info) v
MARCHE Claude's avatar
MARCHE Claude committed
176
177
178
179
180
181
182

let print_binop fmt = function
  | Fand -> fprintf fmt "/\\"
  | For -> fprintf fmt "\\/"
  | Fimplies -> fprintf fmt "->"
  | Fiff -> fprintf fmt "<->"

MARCHE Claude's avatar
MARCHE Claude committed
183
let print_label fmt (l,_) = fprintf fmt "(*%s*)" l
MARCHE Claude's avatar
MARCHE Claude committed
184
185
186

let protect_on x s = if x then "(" ^^ s ^^ ")" else s

187
188
189
190
191
192
let rec print_term info fmt t = print_lrterm false false info fmt t
and     print_fmla info fmt f = print_lrfmla false false info fmt f
and print_opl_term info fmt t = print_lrterm true  false info fmt t
and print_opl_fmla info fmt f = print_lrfmla true  false info fmt f
and print_opr_term info fmt t = print_lrterm false true  info fmt t
and print_opr_fmla info fmt f = print_lrfmla false true  info fmt f
MARCHE Claude's avatar
MARCHE Claude committed
193

194
and print_lrterm opl opr info fmt t = match t.t_label with
195
196
  | _ -> print_tnode opl opr info fmt t
(*
197
  | [] -> print_tnode opl opr info fmt t
MARCHE Claude's avatar
MARCHE Claude committed
198
  | ll -> fprintf fmt "(%a %a)"
199
      (print_list space print_label) ll (print_tnode false false info) t
200
*)
MARCHE Claude's avatar
MARCHE Claude committed
201

202
and print_lrfmla opl opr info fmt f = match f.f_label with
203
204
  | _ -> print_fnode opl opr info fmt f
(*
205
  | [] -> print_fnode opl opr info fmt f
MARCHE Claude's avatar
MARCHE Claude committed
206
  | ll -> fprintf fmt "(%a %a)"
207
      (print_list space print_label) ll (print_fnode false false info) f
208
*)
MARCHE Claude's avatar
MARCHE Claude committed
209

210
and print_tnode opl opr info fmt t = match t.t_node with
MARCHE Claude's avatar
MARCHE Claude committed
211
212
  | Tvar v ->
      print_vs fmt v
MARCHE Claude's avatar
MARCHE Claude committed
213
  | Tconst (ConstInt n) -> fprintf fmt "%s%%Z" n
214
  | Tconst (ConstReal c) ->
MARCHE Claude's avatar
MARCHE Claude committed
215
216
      Print_real.print_with_integers
	"(%s)%%R" "(%s * %s)%%R" "(%s / %s)%%R" fmt c
217
218
  | Tif (f,t1,t2) ->
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
219
        (print_fmla info) f (print_term info) t1 (print_opl_term info) t2
MARCHE Claude's avatar
MARCHE Claude committed
220
221
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
MARCHE Claude's avatar
MARCHE Claude committed
222
      fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
223
        print_vs v (print_opl_term info) t1 (print_opl_term info) t2;
MARCHE Claude's avatar
MARCHE Claude committed
224
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
225
  | Tcase (t,bl) ->
MARCHE Claude's avatar
MARCHE Claude committed
226
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
227
        (print_term info) t
228
        (print_list newline (print_tbranch info)) bl
MARCHE Claude's avatar
MARCHE Claude committed
229
230
231
  | Teps fb ->
      let v,f = f_open_bound fb in
      fprintf fmt (protect_on opr "epsilon %a.@ %a")
232
        (print_vsty info) v (print_opl_fmla info) f;
MARCHE Claude's avatar
MARCHE Claude committed
233
      forget_var v
234
  | Tapp (fs,pl) when is_fs_tuple fs ->
MARCHE Claude's avatar
MARCHE Claude committed
235
      fprintf fmt "%a" (print_paren_r (print_term info)) pl
MARCHE Claude's avatar
MARCHE Claude committed
236
  | Tapp (fs, tl) ->
237
    begin match query_syntax info.info_syn fs.ls_name with
238
      | Some s ->
239
          syntax_arguments s (print_term info) fmt tl
MARCHE Claude's avatar
MARCHE Claude committed
240
      | _ -> if unambig_fs fs
MARCHE Claude's avatar
MARCHE Claude committed
241
          then fprintf fmt "(%a %a)" print_ls fs
242
            (print_space_list (print_term info)) tl
243
          else fprintf fmt (protect_on opl "(%a%a:%a)") print_ls fs
244
            (print_paren_r (print_term info)) tl (print_ty info) t.t_ty
MARCHE Claude's avatar
MARCHE Claude committed
245
246
    end

247
and print_fnode opl opr info fmt f = match f.f_node with
248
249
  | Fquant (Fforall,fq) ->
      let vl,_tl,f = f_open_quant fq in
250
      fprintf fmt (protect_on opr "forall %a,@ %a")
251
        (print_space_list (print_vsty info)) vl
252
253
254
255
        (* (print_tl info) tl *) (print_fmla info) f;
      List.iter forget_var vl
  | Fquant (Fexists,fq) ->
      let vl,_tl,f = f_open_quant fq in
MARCHE Claude's avatar
MARCHE Claude committed
256
      let rec aux fmt vl =
257
258
259
        match vl with
          | [] -> print_fmla info fmt f
          | v::vr ->
260
              fprintf fmt (protect_on opr "exists %a,@ %a")
MARCHE Claude's avatar
MARCHE Claude committed
261
262
                (print_vsty_nopar info) v
                aux vr
263
      in
MARCHE Claude's avatar
MARCHE Claude committed
264
      aux fmt vl;
MARCHE Claude's avatar
MARCHE Claude committed
265
266
267
268
269
270
271
      List.iter forget_var vl
  | Ftrue ->
      fprintf fmt "True"
  | Ffalse ->
      fprintf fmt "False"
  | Fbinop (b,f1,f2) ->
      fprintf fmt (protect_on (opl || opr) "%a %a@ %a")
272
        (print_opr_fmla info) f1 print_binop b (print_opl_fmla info) f2
MARCHE Claude's avatar
MARCHE Claude committed
273
  | Fnot f ->
274
      fprintf fmt (protect_on opr "~ %a") (print_opl_fmla info) f
MARCHE Claude's avatar
MARCHE Claude committed
275
276
  | Flet (t,f) ->
      let v,f = f_open_bound f in
MARCHE Claude's avatar
MARCHE Claude committed
277
      fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
278
        print_vs v (print_opl_term info) t (print_opl_fmla info) f;
MARCHE Claude's avatar
MARCHE Claude committed
279
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
280
  | Fcase (t,bl) ->
MARCHE Claude's avatar
MARCHE Claude committed
281
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
282
        (print_term info) t
283
        (print_list newline (print_fbranch info)) bl
MARCHE Claude's avatar
MARCHE Claude committed
284
285
  | Fif (f1,f2,f3) ->
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
286
        (print_fmla info) f1 (print_fmla info) f2 (print_opl_fmla info) f3
MARCHE Claude's avatar
MARCHE Claude committed
287
  | Fapp (ps, tl) ->
288
    begin match query_syntax info.info_syn ps.ls_name with
289
      | Some s -> syntax_arguments s (print_term info) fmt tl
MARCHE Claude's avatar
MARCHE Claude committed
290
      | _ -> fprintf fmt "(%a %a)" print_ls ps
291
          (print_space_list (print_term info)) tl
MARCHE Claude's avatar
MARCHE Claude committed
292
293
    end

294
and print_tbranch info fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
295
  let p,t = t_open_branch br in
MARCHE Claude's avatar
MARCHE Claude committed
296
  fprintf fmt "@[<hov 4>| %a =>@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
297
298
    (print_pat info) p (print_term info) t;
  Svs.iter forget_var p.pat_vars
MARCHE Claude's avatar
MARCHE Claude committed
299

300
and print_fbranch info fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
301
  let p,f = f_open_branch br in
MARCHE Claude's avatar
MARCHE Claude committed
302
  fprintf fmt "@[<hov 4>| %a =>@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
303
304
    (print_pat info) p (print_fmla info) f;
  Svs.iter forget_var p.pat_vars
MARCHE Claude's avatar
MARCHE Claude committed
305

306
and print_tl info fmt tl =
MARCHE Claude's avatar
MARCHE Claude committed
307
  if tl = [] then () else fprintf fmt "@ [%a]"
308
    (print_list alt (print_list comma (print_expr info))) tl
MARCHE Claude's avatar
MARCHE Claude committed
309

310
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
MARCHE Claude's avatar
MARCHE Claude committed
311
312
313

(** Declarations *)

314
let print_constr info ts fmt cs =
315
316
317
318
319
320
321
322
  match cs.ls_args with
    | [] ->
        fprintf fmt "@[<hov 4>| %a : %a %a@]" print_ls cs
          print_ts ts (print_list space print_tv) ts.ts_args
    | l ->
        fprintf fmt "@[<hov 4>| %a : %a -> %a %a@]" print_ls cs
          (print_arrow_list (print_ty info)) l
          print_ts ts (print_list space print_tv) ts.ts_args
MARCHE Claude's avatar
MARCHE Claude committed
323

MARCHE Claude's avatar
MARCHE Claude committed
324
325
326
327
328
329
let ls_ty_vars ls =
  let ty_vars_args = List.fold_left Ty.ty_freevars Stv.empty ls.ls_args in
  let ty_vars_value = option_fold Ty.ty_freevars Stv.empty ls.ls_value in
  (ty_vars_args, ty_vars_value, Stv.union ty_vars_args ty_vars_value)

let print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params =
330
  if not (Stv.is_empty all_ty_params) then
MARCHE Claude's avatar
MARCHE Claude committed
331
    begin
332
      let need_context = not (Stv.subset ty_vars_value ty_vars_args) in
MARCHE Claude's avatar
MARCHE Claude committed
333
334
335
336
337
      if need_context then fprintf fmt "Set Contextual Implicit.@\n";
      fprintf fmt "Implicit Arguments %a.@\n" print_ls ls;
      if need_context then fprintf fmt "Unset Contextual Implicit.@\n"
    end

338
let print_type_decl info fmt (ts,def) =
MARCHE Claude's avatar
MARCHE Claude committed
339
340
341
342
343
344
345
346
347
348
  if is_ts_tuple ts then () else
  match def with
    | Tabstract -> begin match ts.ts_def with
        | None ->
            fprintf fmt "@[<hov 2>Parameter %a : %aType.@]@\n@\n"
              print_ts ts print_params_list ts.ts_args
        | Some ty ->
            fprintf fmt "@[<hov 2>Definition %a %a :=@ %a.@]@\n@\n"
              print_ts ts (print_arrow_list print_tv) ts.ts_args
	      (print_ty info) ty
MARCHE Claude's avatar
MARCHE Claude committed
349
      end
MARCHE Claude's avatar
MARCHE Claude committed
350
    | Talgebraic csl ->
MARCHE Claude's avatar
MARCHE Claude committed
351
        fprintf fmt "@[<hov 2>Inductive %a %a :=@\n@[<hov>%a@].@]@\n"
352
          print_ts ts (print_list space print_tv) ts.ts_args
MARCHE Claude's avatar
MARCHE Claude committed
353
354
355
356
357
358
359
          (print_list newline (print_constr info ts)) csl;
        List.iter
          (fun cs ->
             let ty_vars_args, ty_vars_value, all_ty_params = ls_ty_vars cs in
             print_implicits fmt cs ty_vars_args ty_vars_value all_ty_params)
          csl;
        fprintf fmt "@\n"
MARCHE Claude's avatar
MARCHE Claude committed
360

361
362
363
let print_type_decl info fmt d =
  if not (Sid.mem (fst d).ts_name info.info_rem) then
    (print_type_decl info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
364

365
let print_ls_type ?(arrow=false) info fmt ls =
MARCHE Claude's avatar
MARCHE Claude committed
366
367
  if arrow then fprintf fmt " ->@ ";
  match ls with
MARCHE Claude's avatar
MARCHE Claude committed
368
  | None -> fprintf fmt "Prop"
369
  | Some ty -> print_ty info fmt ty
MARCHE Claude's avatar
MARCHE Claude committed
370

371
let print_logic_decl info fmt (ls,ld) =
MARCHE Claude's avatar
MARCHE Claude committed
372
  let ty_vars_args, ty_vars_value, all_ty_params = ls_ty_vars ls in
MARCHE Claude's avatar
MARCHE Claude committed
373
374
375
376
377
  begin
    match ld with
      | Some ld ->
          let vl,e = open_ls_defn ld in
          fprintf fmt "@[<hov 2>Definition %a%a%a: %a :=@ %a.@]@\n"
378
            print_ls ls
MARCHE Claude's avatar
MARCHE Claude committed
379
            print_ne_params all_ty_params
MARCHE Claude's avatar
MARCHE Claude committed
380
381
382
383
384
385
            (print_space_list (print_vsty info)) vl
            (print_ls_type info) ls.ls_value
            (print_expr info) e;
          List.iter forget_var vl
      | None ->
          fprintf fmt "@[<hov 2>Parameter %a: %a%a@ %a.@]@\n"
386
            print_ls ls
MARCHE Claude's avatar
MARCHE Claude committed
387
            print_params all_ty_params
MARCHE Claude's avatar
MARCHE Claude committed
388
389
390
            (print_arrow_list (print_ty info)) ls.ls_args
            (print_ls_type ~arrow:(ls.ls_args <> []) info) ls.ls_value
  end;
MARCHE Claude's avatar
MARCHE Claude committed
391
  print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params;
MARCHE Claude's avatar
MARCHE Claude committed
392
  fprintf fmt "@\n"
393

MARCHE Claude's avatar
MARCHE Claude committed
394

395
let print_logic_decl info fmt d =
396
  if not (Sid.mem (fst d).ls_name info.info_rem) then
397
    (print_logic_decl info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
398

399
400
let print_ind info fmt (pr,f) =
  fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr (print_fmla info) f
MARCHE Claude's avatar
MARCHE Claude committed
401

402
(* TODO: fix syntax with type parameters *)
403
let print_ind_decl info fmt (ps,bl) =
404
405
  fprintf fmt "@[<hov 2>Inductive %a : %a -> Prop :=@ @[<hov>%a@].@]@\n@\n"
     print_ls ps (print_arrow_list (print_ty info)) ps.ls_args
406
     (print_list newline (print_ind info)) bl
MARCHE Claude's avatar
MARCHE Claude committed
407

408
let print_ind_decl info fmt d =
409
  if not (Sid.mem (fst d).ls_name info.info_rem) then
410
    (print_ind_decl info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
411
412
413
414
415

let print_pkind fmt = function
  | Paxiom -> fprintf fmt "Axiom"
  | Plemma -> fprintf fmt "Lemma"
  | Pgoal  -> fprintf fmt "Theorem"
416
  | Pskip  -> assert false (* impossible *)
MARCHE Claude's avatar
MARCHE Claude committed
417

418
419
420
421
422
let proof_begin = "(* YOU MAY EDIT THE PROOF BELOW *)"
let proof_end = "(* DO NOT EDIT BELOW *)"

let print_empty_proof fmt =
  fprintf fmt "%s@\n" proof_begin;
MARCHE Claude's avatar
MARCHE Claude committed
423
  fprintf fmt "intuition.@\n";
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
  fprintf fmt "@\n";
  fprintf fmt "Qed.@\n";
  fprintf fmt "%s@\n" proof_end

let print_next_proof ch fmt =
  try
    while true do
      let s = input_line ch in
      if s = proof_begin then
        begin
          fprintf fmt "%s@\n" proof_begin;
          while true do
            let s = input_line ch in
            fprintf fmt "%s@\n" s;
            if s = proof_end then raise Exit
          done
        end
    done
  with
    | End_of_file -> print_empty_proof fmt
    | Exit -> ()

let print_proof ?old fmt = function
447
  | Paxiom | Pskip -> ()
448
449
450
451
  | Plemma | Pgoal ->
      match old with
        | None -> print_empty_proof fmt
        | Some ch -> print_next_proof ch fmt
MARCHE Claude's avatar
MARCHE Claude committed
452

453
let print_decl ?old info fmt d = match d.d_node with
454
455
456
457
  | Dtype tl  -> print_list nothing (print_type_decl info) fmt tl
  | Dlogic ll -> print_list nothing (print_logic_decl info) fmt ll
  | Dind il   -> print_list nothing (print_ind_decl info) fmt il
  | Dprop (_,pr,_) when Sid.mem pr.pr_name info.info_rem -> ()
MARCHE Claude's avatar
MARCHE Claude committed
458
  | Dprop (k,pr,f) ->
459
460
461
462
 (*
     fprintf fmt "@\n@\n(* YOU MAY EDIT BELOW *)@\n@\n@\n";
      fprintf fmt "(* DO NOT EDIT BELOW *)@\n@\@\n";
 *)
MARCHE Claude's avatar
MARCHE Claude committed
463
      let params = f_ty_freevars Stv.empty f in
464
      fprintf fmt "@[<hov 2>%a %a : %a%a.@]@\n%a@\n"
MARCHE Claude's avatar
MARCHE Claude committed
465
        print_pkind k
466
        print_pr pr
MARCHE Claude's avatar
MARCHE Claude committed
467
468
        print_params params
        (print_fmla info) f (print_proof ?old) k;
469
      forget_tvs ()
MARCHE Claude's avatar
MARCHE Claude committed
470

471
472
let print_decls ?old info fmt dl =
  fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl ?old info)) dl
MARCHE Claude's avatar
MARCHE Claude committed
473

MARCHE Claude's avatar
MARCHE Claude committed
474
let print_task _env pr thpr ?old fmt task =
475
  forget_all ();
476
477
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
Andrei Paskevich's avatar
Andrei Paskevich committed
478
479
480
  let info = {
    info_syn = get_syntax_map task;
    info_rem = get_remove_set task } in
481
  print_decls ?old info fmt (Task.task_decls task)
MARCHE Claude's avatar
MARCHE Claude committed
482

483
let () = register_printer "coq" print_task
MARCHE Claude's avatar
MARCHE Claude committed
484

MARCHE Claude's avatar
MARCHE Claude committed
485
486
487
488



(*
489
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
490
compile-command: "unset LANG; make -C ../.. "
491
End:
MARCHE Claude's avatar
MARCHE Claude committed
492
*)