coq.ml 25.9 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
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

MARCHE Claude's avatar
MARCHE Claude committed
31 32 33
let black_list =
  [ "at"; "cofix"; "exists2"; "fix"; "IF"; "left"; "mod"; "Prop";
    "return"; "right"; "Set"; "Type"; "using"; "where"; ]
34

35
let iprinter =
MARCHE Claude's avatar
MARCHE Claude committed
36
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
37
  create_ident_printer black_list ~sanitizer:isanitize
38 39

let forget_all () = forget_all iprinter
MARCHE Claude's avatar
MARCHE Claude committed
40 41 42 43

let tv_set = ref Sid.empty

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

MARCHE Claude's avatar
MARCHE Claude committed
45
let print_tv fmt tv =
MARCHE Claude's avatar
MARCHE Claude committed
46
  let n = id_unique iprinter tv.tv_name in
MARCHE Claude's avatar
MARCHE Claude committed
47 48
  fprintf fmt "%s" n

MARCHE Claude's avatar
MARCHE Claude committed
49 50 51 52 53
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

54 55 56 57 58
let print_implicit_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

MARCHE Claude's avatar
MARCHE Claude committed
59 60 61 62 63 64 65 66 67 68 69 70 71 72
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

73 74 75
let print_implicit_params fmt stv =
  Stv.iter (fun tv -> fprintf fmt "%a@ " print_implicit_tv_binder tv) stv

MARCHE Claude's avatar
MARCHE Claude committed
76 77
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
  fprintf fmt "%s" n

let forget_var vs = forget_id iprinter vs.vs_name

let print_ts fmt ts =
93
  fprintf fmt "%s" (id_unique iprinter ts.ts_name)
MARCHE Claude's avatar
MARCHE Claude committed
94 95

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

let print_pr fmt pr =
99
  fprintf fmt "%s" (id_unique iprinter pr.pr_name)
MARCHE Claude's avatar
MARCHE Claude committed
100

101 102 103
(* info *)

type info = {
104
  info_syn : syntax_map;
105 106
  symbol_printers : (Theory.theory * ident_printer) Mid.t;
  realization : bool;
107 108
}

109 110 111 112
let print_path = print_list (constant_string ".") string

let print_id fmt id = string fmt (id_unique iprinter id)

113 114
let print_id_real info fmt id =
        try let th,ipr = Mid.find id info.symbol_printers in
115 116 117 118 119 120 121 122 123 124
        fprintf fmt "%a.%s.%s"
          print_path th.Theory.th_path
          th.Theory.th_name.id_string
          (id_unique ipr id)
        with Not_found -> print_id fmt id

let print_ls_real info fmt ls = print_id_real info fmt ls.ls_name
let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name
let print_pr_real info fmt pr = print_id_real info fmt pr.pr_name

MARCHE Claude's avatar
MARCHE Claude committed
125 126
(** Types *)

127
let rec print_ty info fmt ty = match ty.ty_node with
MARCHE Claude's avatar
MARCHE Claude committed
128
  | Tyvar v -> print_tv fmt v
MARCHE Claude's avatar
MARCHE Claude committed
129
  | Tyapp (ts, tl) when is_ts_tuple ts ->
130
      begin
MARCHE Claude's avatar
MARCHE Claude committed
131 132 133
        match tl with
          | []  -> fprintf fmt "unit"
          | [ty] -> print_ty info fmt ty
MARCHE Claude's avatar
MARCHE Claude committed
134
          | _   -> fprintf fmt "(%a)%%type" (print_list star (print_ty info)) tl
135 136
      end
  | Tyapp (ts, tl) ->
MARCHE Claude's avatar
MARCHE Claude committed
137 138
      begin match query_syntax info.info_syn ts.ts_name with
        | Some s -> syntax_arguments s (print_ty info) fmt tl
139 140
        | None ->
            begin
MARCHE Claude's avatar
MARCHE Claude committed
141
              match tl with
142 143
                | []  -> (print_ts_real info) fmt ts
                | l   -> fprintf fmt "(%a@ %a)" (print_ts_real info) ts
MARCHE Claude's avatar
MARCHE Claude committed
144 145 146
                    (print_list space (print_ty info)) l
            end
      end
MARCHE Claude's avatar
MARCHE Claude committed
147 148 149 150

(* 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
151
    | Tyvar u when tv_equal u v -> true
MARCHE Claude's avatar
MARCHE Claude committed
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
    | _ -> 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
168 169 170 171
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

172
let rec print_pat info fmt p = match p.pat_node with
MARCHE Claude's avatar
MARCHE Claude committed
173 174
  | Pwild -> fprintf fmt "_"
  | Pvar v -> print_vs fmt v
Andrei Paskevich's avatar
Andrei Paskevich committed
175 176 177 178
  | 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
179
  | Papp (cs,pl) when is_fs_tuple cs ->
MARCHE Claude's avatar
MARCHE Claude committed
180
      fprintf fmt "%a" (print_paren_r (print_pat info)) pl
181
  | Papp (cs,pl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
182 183
      begin match query_syntax info.info_syn cs.ls_name with
        | Some s -> syntax_arguments s (print_pat info) fmt pl
184
        | _ when pl = [] -> (print_ls_real info) fmt cs
185
        | _ -> fprintf fmt "(%a %a)"
186
          (print_ls_real info) cs (print_list space (print_pat info)) pl
Andrei Paskevich's avatar
Andrei Paskevich committed
187
      end
MARCHE Claude's avatar
MARCHE Claude committed
188

189 190
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
191

192 193
let print_vsty info fmt v =
  fprintf fmt "(%a)" (print_vsty_nopar info) v
MARCHE Claude's avatar
MARCHE Claude committed
194 195

let print_binop fmt = function
196 197 198 199
  | Tand -> fprintf fmt "/\\"
  | Tor -> fprintf fmt "\\/"
  | Timplies -> fprintf fmt "->"
  | Tiff -> fprintf fmt "<->"
MARCHE Claude's avatar
MARCHE Claude committed
200

MARCHE Claude's avatar
MARCHE Claude committed
201
let print_label fmt (l,_) = fprintf fmt "(*%s*)" l
MARCHE Claude's avatar
MARCHE Claude committed
202 203 204

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

205 206 207 208 209 210
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
211

212
and print_lrterm opl opr info fmt t = match t.t_label with
213 214
  | _ -> print_tnode opl opr info fmt t
(*
215
  | [] -> print_tnode opl opr info fmt t
MARCHE Claude's avatar
MARCHE Claude committed
216
  | ll -> fprintf fmt "(%a %a)"
217
      (print_list space print_label) ll (print_tnode false false info) t
218
*)
MARCHE Claude's avatar
MARCHE Claude committed
219

220
and print_lrfmla opl opr info fmt f = match f.t_label with
221 222
  | _ -> print_fnode opl opr info fmt f
(*
223
  | [] -> print_fnode opl opr info fmt f
MARCHE Claude's avatar
MARCHE Claude committed
224
  | ll -> fprintf fmt "(%a %a)"
225
      (print_list space print_label) ll (print_fnode false false info) f
226
*)
MARCHE Claude's avatar
MARCHE Claude committed
227

228
and print_tnode opl opr info fmt t = match t.t_node with
MARCHE Claude's avatar
MARCHE Claude committed
229 230
  | Tvar v ->
      print_vs fmt v
231 232 233 234 235 236 237 238 239 240 241
  | Tconst c ->
      let number_format = {
          Print_number.long_int_support = true;
          Print_number.dec_int_support = Print_number.Number_custom "%s%%Z";
          Print_number.hex_int_support = Print_number.Number_unsupported;
          Print_number.oct_int_support = Print_number.Number_unsupported;
          Print_number.bin_int_support = Print_number.Number_unsupported;
          Print_number.def_int_support = Print_number.Number_unsupported;
          Print_number.dec_real_support = Print_number.Number_unsupported;
          Print_number.hex_real_support = Print_number.Number_unsupported;
          Print_number.frac_real_support = Print_number.Number_custom
242
            (Print_number.PrintFracReal ("%s%%R", "(%s * %s)%%R", "(%s / %s)%%R"));
243 244 245
          Print_number.def_real_support = Print_number.Number_unsupported;
        } in
      Print_number.print number_format fmt c
246 247
  | Tif (f,t1,t2) ->
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
248
        (print_fmla info) f (print_term info) t1 (print_opl_term info) t2
MARCHE Claude's avatar
MARCHE Claude committed
249 250
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
MARCHE Claude's avatar
MARCHE Claude committed
251
      fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
252
        print_vs v (print_opl_term info) t1 (print_opl_term info) t2;
MARCHE Claude's avatar
MARCHE Claude committed
253
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
254
  | Tcase (t,bl) ->
MARCHE Claude's avatar
MARCHE Claude committed
255
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
256
        (print_term info) t
257
        (print_list newline (print_tbranch info)) bl
MARCHE Claude's avatar
MARCHE Claude committed
258
  | Teps fb ->
259
      let v,f = t_open_bound fb in
MARCHE Claude's avatar
MARCHE Claude committed
260
      fprintf fmt (protect_on opr "epsilon %a.@ %a")
261
        (print_vsty info) v (print_opl_fmla info) f;
MARCHE Claude's avatar
MARCHE Claude committed
262
      forget_var v
263
  | Tapp (fs,pl) when is_fs_tuple fs ->
MARCHE Claude's avatar
MARCHE Claude committed
264
      fprintf fmt "%a" (print_paren_r (print_term info)) pl
MARCHE Claude's avatar
MARCHE Claude committed
265
  | Tapp (fs, tl) ->
266
    begin match query_syntax info.info_syn fs.ls_name with
267
      | Some s ->
268
          syntax_arguments s (print_term info) fmt tl
MARCHE Claude's avatar
MARCHE Claude committed
269
      | _ -> if unambig_fs fs
270
          then
271 272
            if tl = [] then fprintf fmt "%a" (print_ls_real info) fs
            else fprintf fmt "(%a %a)" (print_ls_real info) fs
273
              (print_space_list (print_term info)) tl
274
          else fprintf fmt (protect_on opl "(%a%a:%a)") (print_ls_real info) fs
275
            (print_paren_r (print_term info)) tl (print_ty info) (t_type t)
MARCHE Claude's avatar
MARCHE Claude committed
276
    end
277
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
MARCHE Claude's avatar
MARCHE Claude committed
278

279
and print_fnode opl opr info fmt f = match f.t_node with
280 281
  | Tquant (Tforall,fq) ->
      let vl,_tl,f = t_open_quant fq in
282
      fprintf fmt (protect_on opr "forall %a,@ %a")
283
        (print_space_list (print_vsty info)) vl
284 285
        (* (print_tl info) tl *) (print_fmla info) f;
      List.iter forget_var vl
286 287
  | Tquant (Texists,fq) ->
      let vl,_tl,f = t_open_quant fq in
MARCHE Claude's avatar
MARCHE Claude committed
288
      let rec aux fmt vl =
289 290 291
        match vl with
          | [] -> print_fmla info fmt f
          | v::vr ->
292
              fprintf fmt (protect_on opr "exists %a,@ %a")
MARCHE Claude's avatar
MARCHE Claude committed
293 294
                (print_vsty_nopar info) v
                aux vr
295
      in
MARCHE Claude's avatar
MARCHE Claude committed
296
      aux fmt vl;
MARCHE Claude's avatar
MARCHE Claude committed
297
      List.iter forget_var vl
298
  | Ttrue ->
MARCHE Claude's avatar
MARCHE Claude committed
299
      fprintf fmt "True"
300
  | Tfalse ->
MARCHE Claude's avatar
MARCHE Claude committed
301
      fprintf fmt "False"
302
  | Tbinop (b,f1,f2) ->
MARCHE Claude's avatar
MARCHE Claude committed
303
      fprintf fmt (protect_on (opl || opr) "%a %a@ %a")
304
        (print_opr_fmla info) f1 print_binop b (print_opl_fmla info) f2
305
  | Tnot f ->
306
      fprintf fmt (protect_on opr "~ %a") (print_opl_fmla info) f
307
  | Tlet (t,f) ->
308
      let v,f = t_open_bound f in
MARCHE Claude's avatar
MARCHE Claude committed
309
      fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
310
        print_vs v (print_opl_term info) t (print_opl_fmla info) f;
MARCHE Claude's avatar
MARCHE Claude committed
311
      forget_var v
312
  | Tcase (t,bl) ->
MARCHE Claude's avatar
MARCHE Claude committed
313
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
314
        (print_term info) t
315
        (print_list newline (print_fbranch info)) bl
316
  | Tif (f1,f2,f3) ->
MARCHE Claude's avatar
MARCHE Claude committed
317
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
318
        (print_fmla info) f1 (print_fmla info) f2 (print_opl_fmla info) f3
319
  | Tapp (ps, tl) ->
320
    begin match query_syntax info.info_syn ps.ls_name with
321
      | Some s -> syntax_arguments s (print_term info) fmt tl
322
      | _ -> fprintf fmt "(%a %a)" (print_ls_real info) ps
323
          (print_space_list (print_term info)) tl
MARCHE Claude's avatar
MARCHE Claude committed
324
    end
325
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
MARCHE Claude's avatar
MARCHE Claude committed
326

327
and print_tbranch info fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
328
  let p,t = t_open_branch br in
MARCHE Claude's avatar
MARCHE Claude committed
329
  fprintf fmt "@[<hov 4>| %a =>@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
330 331
    (print_pat info) p (print_term info) t;
  Svs.iter forget_var p.pat_vars
MARCHE Claude's avatar
MARCHE Claude committed
332

333
and print_fbranch info fmt br =
334
  let p,f = t_open_branch br in
MARCHE Claude's avatar
MARCHE Claude committed
335
  fprintf fmt "@[<hov 4>| %a =>@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
336 337
    (print_pat info) p (print_fmla info) f;
  Svs.iter forget_var p.pat_vars
MARCHE Claude's avatar
MARCHE Claude committed
338

339 340
let print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
MARCHE Claude's avatar
MARCHE Claude committed
341 342 343

(** Declarations *)

344
let print_constr info ts fmt cs =
345 346 347 348 349 350 351 352
  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
353

MARCHE Claude's avatar
MARCHE Claude committed
354 355 356 357 358 359
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 =
360
  if not (Stv.is_empty all_ty_params) then
MARCHE Claude's avatar
MARCHE Claude committed
361
    begin
362
      let need_context = not (Stv.subset ty_vars_value ty_vars_args) in
MARCHE Claude's avatar
MARCHE Claude committed
363 364 365 366 367
      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

MARCHE Claude's avatar
MARCHE Claude committed
368
let definition fmt info =
369
  fprintf fmt "%s" (if info.realization then "Definition" else "Parameter")
MARCHE Claude's avatar
MARCHE Claude committed
370

371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388
(*

  copy of old user scripts

*)

let copy_user_script begin_string end_string ch fmt =
  fprintf fmt "%s@\n" begin_string;
  try
    while true do
      let s = input_line ch in
      fprintf fmt "%s@\n" s;
      if s = end_string then raise Exit
    done
  with
    | Exit -> fprintf fmt "@\n"
    | End_of_file -> fprintf fmt "%s@\n@\n" end_string

MARCHE Claude's avatar
MARCHE Claude committed
389 390
let proof_begin = "(* YOU MAY EDIT THE PROOF BELOW *)"
let proof_end = "(* DO NOT EDIT BELOW *)"
391 392 393 394 395 396
let context_begin = "(* YOU MAY EDIT THE CONTEXT BELOW *)"
let context_end = "(* DO NOT EDIT BELOW *)"

(* current kind of script in an old file *)
type old_file_state = InContext | InProof | NoWhere

397
let copy_proof s ch fmt =
398 399 400
  copy_user_script proof_begin proof_end ch fmt;
  s := NoWhere

401
let copy_context s ch fmt =
402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421
  copy_user_script context_begin context_end ch fmt;
  s := NoWhere

let lookup_context_or_proof old_state old_channel =
  match !old_state with
    | InProof | InContext -> ()
    | NoWhere ->
        let rec loop () =
          let s = input_line old_channel in
          if s = proof_begin then old_state := InProof else
            if s = context_begin then old_state := InContext else
              loop ()
        in
        try loop ()
        with End_of_file -> ()

let print_empty_context fmt =
  fprintf fmt "%s@\n" context_begin;
  fprintf fmt "@\n";
  fprintf fmt "%s@\n@\n" context_end
MARCHE Claude's avatar
MARCHE Claude committed
422 423 424 425 426 427 428 429

let print_empty_proof ?(def=false) fmt =
  fprintf fmt "%s@\n" proof_begin;
  if not def then fprintf fmt "intuition.@\n";
  fprintf fmt "@\n";
  fprintf fmt "%s.@\n" (if def then "Defined" else "Qed");
  fprintf fmt "%s@\n@\n" proof_end

430
(*
MARCHE Claude's avatar
MARCHE Claude committed
431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447
let print_next_proof ?def 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 ?def fmt
    | Exit -> fprintf fmt "@\n"
448
*)
MARCHE Claude's avatar
MARCHE Claude committed
449

450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481
let print_context ~old fmt =
  match old with
    | None -> print_empty_context fmt
    | Some(s,ch) ->
        lookup_context_or_proof s ch;
        match !s with
          | InProof | NoWhere -> print_empty_context fmt
          | InContext -> copy_context s ch fmt

let print_proof ~old ?def fmt =
  match old with
    | None -> print_empty_proof ?def fmt
    | Some(s,ch) ->
        lookup_context_or_proof s ch;
        match !s with
          | InContext | NoWhere -> print_empty_proof ?def fmt
          | InProof -> copy_proof s ch fmt

let produce_remaining_contexts_and_proofs ~old fmt =
  match old with
    | None -> ()
    | Some(s,ch) ->
        let rec loop () =
          lookup_context_or_proof s ch;
          match !s with
            | NoWhere -> ()
            | InContext -> copy_context s ch fmt; loop ()
            | InProof -> copy_proof s ch fmt; loop ()
        in
        loop ()

(*
482 483 484 485 486 487 488 489 490 491 492 493
let produce_remaining_proofs ~old fmt =
  match old with
    | None -> ()
    | Some ch ->
  try
    while true do
      let s = input_line ch in
      if s = proof_begin then
        begin
          fprintf fmt "(* OBSOLETE PROOF *)@\n";
          try while true do
            let s = input_line ch in
494
            if s = proof_end then
495 496 497 498
              begin
                fprintf fmt "(* END OF OBSOLETE PROOF *)@\n@\n";
                raise Exit
              end;
499 500
            fprintf fmt "%s@\n" s;
          done
501
          with Exit -> ()
502 503 504 505
        end
    done
  with
    | End_of_file -> fprintf fmt "@\n"
506
*)
507 508 509

let realization ~old ?def fmt produce_realization =
  if produce_realization then
510 511
    print_proof ~old ?def fmt
(*
MARCHE Claude's avatar
MARCHE Claude committed
512
    begin match old with
513
      | None -> print_empty_proof ?def fmt
MARCHE Claude's avatar
MARCHE Claude committed
514 515
      | Some ch -> print_next_proof ?def ch fmt
    end
516
*)
MARCHE Claude's avatar
MARCHE Claude committed
517 518 519
  else
    fprintf fmt "@\n"

520
let print_type_decl ~old info fmt (ts,def) =
MARCHE Claude's avatar
MARCHE Claude committed
521 522 523 524
  if is_ts_tuple ts then () else
  match def with
    | Tabstract -> begin match ts.ts_def with
        | None ->
MARCHE Claude's avatar
MARCHE Claude committed
525
            fprintf fmt "@[<hov 2>%a %a : %aType.@]@\n%a"
526
              definition info
MARCHE Claude's avatar
MARCHE Claude committed
527
              print_ts ts print_params_list ts.ts_args
528
              (realization ~old ~def:true) info.realization
MARCHE Claude's avatar
MARCHE Claude committed
529 530
        | Some ty ->
            fprintf fmt "@[<hov 2>Definition %a %a :=@ %a.@]@\n@\n"
MARCHE Claude's avatar
MARCHE Claude committed
531
              print_ts ts (print_list space print_tv_binder) ts.ts_args
532
              (print_ty info) ty
MARCHE Claude's avatar
MARCHE Claude committed
533
      end
MARCHE Claude's avatar
MARCHE Claude committed
534
    | Talgebraic csl ->
MARCHE Claude's avatar
MARCHE Claude committed
535
        fprintf fmt "@[<hov 2>Inductive %a %a :=@\n@[<hov>%a@].@]@\n"
536
          print_ts ts (print_list space print_tv_binder) ts.ts_args
MARCHE Claude's avatar
MARCHE Claude committed
537 538 539 540 541 542 543
          (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
544

545
let print_type_decl ~old info fmt d =
546
  if not (Mid.mem (fst d).ts_name info.info_syn) then
547
    (print_type_decl ~old info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
548

549
let print_ls_type ?(arrow=false) info fmt ls =
MARCHE Claude's avatar
MARCHE Claude committed
550 551
  if arrow then fprintf fmt " ->@ ";
  match ls with
MARCHE Claude's avatar
MARCHE Claude committed
552
  | None -> fprintf fmt "Prop"
553
  | Some ty -> print_ty info fmt ty
MARCHE Claude's avatar
MARCHE Claude committed
554

555
let print_logic_decl ~old info fmt (ls,ld) =
MARCHE Claude's avatar
MARCHE Claude committed
556
  let ty_vars_args, ty_vars_value, all_ty_params = ls_ty_vars ls in
MARCHE Claude's avatar
MARCHE Claude committed
557 558 559 560 561
  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"
562
            print_ls ls
MARCHE Claude's avatar
MARCHE Claude committed
563
            print_ne_params all_ty_params
MARCHE Claude's avatar
MARCHE Claude committed
564 565 566 567 568
            (print_space_list (print_vsty info)) vl
            (print_ls_type info) ls.ls_value
            (print_expr info) e;
          List.iter forget_var vl
      | None ->
569
          fprintf fmt "@[<hov 2>%a %a: %a%a%a.@]@\n%a"
570
            definition info
571
            print_ls ls
MARCHE Claude's avatar
MARCHE Claude committed
572
            print_params all_ty_params
MARCHE Claude's avatar
MARCHE Claude committed
573 574
            (print_arrow_list (print_ty info)) ls.ls_args
            (print_ls_type ~arrow:(ls.ls_args <> []) info) ls.ls_value
575
            (realization ~old ~def:true) info.realization
MARCHE Claude's avatar
MARCHE Claude committed
576
  end;
MARCHE Claude's avatar
MARCHE Claude committed
577
  print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params;
MARCHE Claude's avatar
MARCHE Claude committed
578
  fprintf fmt "@\n"
579

580
let print_logic_decl ~old info fmt d =
581
  if not (Mid.mem (fst d).ls_name info.info_syn) then
582
    (print_logic_decl ~old info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
583

584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615
let print_recursive_decl info tm fmt (ls,ld) =
  let _, _, all_ty_params = ls_ty_vars ls in
  let il = try Mls.find ls tm with Not_found -> assert false in
  let i = match il with [i] -> i | _ -> assert false in
  begin match ld with
    | Some ld ->
        let vl,e = open_ls_defn ld in
        fprintf fmt "%a%a%a {struct %a}: %a :=@ %a.@]@\n"
          print_ls ls
          print_ne_params all_ty_params
          (print_space_list (print_vsty info)) vl
          print_vs (List.nth vl i)
          (print_ls_type info) ls.ls_value
          (print_expr info) e;
        List.iter forget_var vl
    | None ->
        assert false
  end

let print_recursive_decl info fmt dl =
  let tm = check_termination dl in
  let d, dl = match dl with d :: dl -> d, dl | [] -> assert false in
  fprintf fmt "Set Implicit Arguments.@\n";
  fprintf fmt "@[<hov 2>Fixpoint ";
  print_recursive_decl info tm fmt d; forget_tvs ();
  List.iter
    (fun d ->
       fprintf fmt "@[<hov 2>with ";
       print_recursive_decl info tm fmt d; forget_tvs ())
    dl;
  fprintf fmt "Unset Implicit Arguments.@\n@\n"

616 617
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
618

619
let print_ind_decl info fmt (ps,bl) =
620 621 622 623 624 625 626
  let ty_vars_args, ty_vars_value, all_ty_params = ls_ty_vars ps in
  fprintf fmt "@[<hov 2>Inductive %a%a : %a -> Prop :=@ @[<hov>%a@].@]@\n"
     print_ls ps print_implicit_params all_ty_params
    (print_arrow_list (print_ty info)) ps.ls_args
     (print_list newline (print_ind info)) bl;
  print_implicits fmt ps ty_vars_args ty_vars_value all_ty_params;
  fprintf fmt "@\n"
MARCHE Claude's avatar
MARCHE Claude committed
627

628
let print_ind_decl info fmt d =
629
  if not (Mid.mem (fst d).ls_name info.info_syn) then
630
    (print_ind_decl info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
631

MARCHE Claude's avatar
MARCHE Claude committed
632
let print_pkind info fmt = function
633
  | Paxiom ->
634
      if info.realization then
635
        fprintf fmt "Lemma"
MARCHE Claude's avatar
MARCHE Claude committed
636
      else
637
        fprintf fmt "Axiom"
MARCHE Claude's avatar
MARCHE Claude committed
638 639
  | Plemma -> fprintf fmt "Lemma"
  | Pgoal  -> fprintf fmt "Theorem"
640
  | Pskip  -> assert false (* impossible *)
MARCHE Claude's avatar
MARCHE Claude committed
641

642
let print_proof ~old info fmt = function
643
  | Plemma | Pgoal ->
644
      realization ~old fmt true
MARCHE Claude's avatar
MARCHE Claude committed
645
  | Paxiom ->
646
      realization ~old fmt info.realization
MARCHE Claude's avatar
MARCHE Claude committed
647
  | Pskip -> ()
MARCHE Claude's avatar
MARCHE Claude committed
648

649 650 651 652
let print_proof_context ~old info fmt = function
  | Plemma | Pgoal ->
      print_context ~old fmt
  | Paxiom ->
653
      if info.realization then print_context ~old fmt
654 655
  | Pskip -> ()

656
let print_decl ~old info fmt d = match d.d_node with
657 658 659 660 661 662 663 664
  | Dtype tl  ->
      print_list nothing (print_type_decl ~old info) fmt tl
  | Dlogic [s,_ as ld] when not (Sid.mem s.ls_name d.d_syms) ->
      print_logic_decl ~old info fmt ld
  | Dlogic ll ->
      print_recursive_decl info fmt ll
  | Dind il   ->
      print_list nothing (print_ind_decl info) fmt il
665
  | Dprop (_,pr,_) when Mid.mem pr.pr_name info.info_syn ->
666
      ()
MARCHE Claude's avatar
MARCHE Claude committed
667
  | Dprop (k,pr,f) ->
668
      print_proof_context ~old info fmt k;
669
      let params = t_ty_freevars Stv.empty f in
MARCHE Claude's avatar
MARCHE Claude committed
670 671
      fprintf fmt "@[<hov 2>%a %a : %a%a.@]@\n%a"
        (print_pkind info) k
672
        print_pr pr
MARCHE Claude's avatar
MARCHE Claude committed
673
        print_params params
674
        (print_fmla info) f (print_proof ~old info) k;
675
      forget_tvs ()
MARCHE Claude's avatar
MARCHE Claude committed
676

677 678
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
679

680 681 682 683 684 685
let init_printer th =
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let pr = create_ident_printer black_list ~sanitizer:isanitize in
  Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
  pr

686 687 688 689 690 691 692 693 694 695 696 697 698
(* TODO: change into a less intrusive coding, e.g. a driver meta, and
   make the lookup a bit more efficient along the way *)
let realized_theories = [
  ["int"; "Abs"];
  ["int"; "ComputerDivision"];
  ["int"; "EuclideanDivision"];
  ["int"; "Int"];
  ["int"; "MinMax"];
  ["real"; "Abs"];
  ["real"; "FromInt"];
  ["real"; "MinMax"];
  ["real"; "Real"];
  ["real"; "Square"];
699 700 701
  ["floating_point"; "Rounding"];
  ["floating_point"; "Single"];
  ["floating_point"; "Double"];
702 703 704
]

let print_task _env pr thpr realize ?old fmt task =
705
  forget_all ();
706 707
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
708
  let symbol_printers,decls =
709
      let used = Task.used_theories task in
710
      let used = Mid.filter (fun _ th -> List.mem (th.Theory.th_path@[th.Theory.th_name.id_string]) realized_theories) used in
711 712 713 714
      (* 2 cases: goal is clone T with [] or goal is a real goal *)
      let used = match task with
        | None -> assert false
        | Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
715 716 717
            Sid.iter
              (fun id -> ignore (id_unique iprinter id))
              th.Theory.th_local;
718
            Mid.remove th.Theory.th_name used
719 720
        | _ -> used
      in
721
      (*
722
      (* output the Require commands *)
723 724 725
      List.iter
        (fprintf fmt "Add Rec LoadPath \"%s\".@\n")
        (Env.get_loadpath env);
726
      *)
727
      Mid.iter
728 729
        (fun id th -> fprintf fmt "Require %a.%s.@\n"
          print_path th.Theory.th_path id.id_string)
730
        used;
731 732 733 734 735 736 737 738
      let symbols = Task.used_symbols used in
      (* build the printers for each theories *)
      let printers = Mid.map init_printer used in
      let decls = Task.local_decls task symbols in
      let symbols =
        Mid.map (fun th -> (th,Mid.find th.Theory.th_name printers))
          symbols
      in
739
      symbols, decls
740
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
741 742
  let info = {
    info_syn = get_syntax_map task;
743 744
    symbol_printers = symbol_printers;
    realization = realize;
745 746
  }
  in
747 748 749 750
  let old = match old with
    | None -> None
    | Some ch -> Some(ref NoWhere,ch)
  in
751
  print_decls ~old info fmt decls
MARCHE Claude's avatar
MARCHE Claude committed
752

753 754
let print_task_full env pr thpr ?old fmt task =
  print_task env pr thpr false ?old fmt task
MARCHE Claude's avatar
MARCHE Claude committed
755

756 757
let print_task_real env pr thpr ?old fmt task =
  print_task env pr thpr true  ?old fmt task
MARCHE Claude's avatar
MARCHE Claude committed
758

759 760
let () = register_printer "coq" print_task_full
let () = register_printer "coq-realize" print_task_real
MARCHE Claude's avatar
MARCHE Claude committed
761

MARCHE Claude's avatar
MARCHE Claude committed
762
(* specific printer for realization of theories *)
MARCHE Claude's avatar
MARCHE Claude committed
763
(* OBSOLETE
MARCHE Claude's avatar
MARCHE Claude committed
764 765 766

open Theory

767
let print_tdecl ~old info fmt d = match d.td_node with
768 769 770 771 772
  | Decl d ->
      print_decl ~old info fmt d
  | Use t ->
      fprintf fmt "Require %s.@\n@\n"
        (id_unique iprinter t.th_name)
773 774
  | Meta _ -> assert false (* TODO ? *)
  | Clone _ -> assert false (* TODO *)
MARCHE Claude's avatar
MARCHE Claude committed
775

776
let print_tdecls ~old info fmt dl =
777 778
  fprintf fmt "@[<hov>%a@\n@]"
    (print_list nothing (print_tdecl ~old info)) dl
MARCHE Claude's avatar
MARCHE Claude committed
779

780
let print_theory _env pr thpr ?old fmt th =
MARCHE Claude's avatar
MARCHE Claude committed
781 782 783 784
  forget_all ();
  print_prelude fmt pr;
  print_prelude_for_theory th fmt thpr;
  let info = {
785 786
    info_syn = (Mid.empty : string Ident.Mid.t)
      (* get_syntax_map_of_theory th*);
MARCHE Claude's avatar
MARCHE Claude committed
787
    realization = true;
788
  }
MARCHE Claude's avatar
MARCHE Claude committed
789
  in
790 791 792 793
  let old = match old with
    | None -> None
    | Some ch -> Some(ref NoWhere,ch)
  in
794
  print_tdecls ~old info fmt th.th_decls;
795
  produce_remaining_contexts_and_proofs ~old fmt
MARCHE Claude's avatar
MARCHE Claude committed
796

MARCHE Claude's avatar
MARCHE Claude committed
797
*)
MARCHE Claude's avatar
MARCHE Claude committed
798

MARCHE Claude's avatar
MARCHE Claude committed
799
(*
800
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
801
compile-command: "unset LANG; make -C ../.. "
802
End:
MARCHE Claude's avatar
MARCHE Claude committed
803
*)