coq.ml 36.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11

Francois Bobot's avatar
Francois Bobot committed
12 13
(** Coq printer *)

MARCHE Claude's avatar
MARCHE Claude committed
14 15 16 17 18 19
open Format
open Pp
open Ident
open Ty
open Term
open Decl
20
open Printer
MARCHE Claude's avatar
MARCHE Claude committed
21

22 23 24
let black_list =
  [ "at"; "cofix"; "exists2"; "fix"; "IF"; "left"; "mod"; "Prop";
    "return"; "right"; "Set"; "Type"; "using"; "where"; ]
25

26
(* wrong: ' not allowed as first character in Coq identifiers
27 28 29 30
let char_to_alpha c =
  match c with
    | '\'' -> String.make 1 c
    | _ -> Ident.char_to_alpha c
31
*)
32 33 34 35 36 37

let char_to_alnumus c =
  match c with
    | '\'' -> String.make 1 c
    | _ -> Ident.char_to_alnumus c

38 39 40
let complex_syntax s =
  String.contains s '%' || String.contains s ' ' || String.contains s '('

41 42
let syntax_arguments s f fmt l =
  let sl = Strings.split ' ' s in
43
  pp_open_box fmt 1;
44 45 46
  print_list space (fun fmt s -> syntax_arguments s f fmt l) fmt sl;
  pp_close_box fmt ()

47
let fresh_printer () =
MARCHE Claude's avatar
MARCHE Claude committed
48
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
49
  create_ident_printer black_list ~sanitizer:isanitize
50

51 52
let iprinter = fresh_printer ()

53
let forget_all () = forget_all iprinter
MARCHE Claude's avatar
MARCHE Claude committed
54 55 56

let tv_set = ref Sid.empty

57 58 59 60 61 62 63 64 65
(* info *)

type info = {
  info_syn : syntax_map;
  symbol_printers : (string * ident_printer) Mid.t;
  realization : bool;
  ssreflect: bool;
}

MARCHE Claude's avatar
MARCHE Claude committed
66
(* type variables *)
MARCHE Claude's avatar
MARCHE Claude committed
67

68
let print_tv info ~whytypes fmt tv =
MARCHE Claude's avatar
MARCHE Claude committed
69
  let n = id_unique iprinter tv.tv_name in
70
  fprintf fmt "%s" n;
71
  if whytypes && not info.ssreflect then fprintf fmt " %s_WT" n
MARCHE Claude's avatar
MARCHE Claude committed
72

73
let print_tv_binder info ~whytypes ~implicit fmt tv =
MARCHE Claude's avatar
MARCHE Claude committed
74 75
  tv_set := Sid.add tv.tv_name !tv_set;
  let n = id_unique iprinter tv.tv_name in
76 77 78 79 80 81
  if info.ssreflect then
    fprintf fmt "{%s: why3Type}" n
  else begin
    if implicit then fprintf fmt "{%s:Type}" n else fprintf fmt "(%s:Type)" n;
    if whytypes then fprintf fmt " {%s_WT:WhyType %s}" n n
  end
MARCHE Claude's avatar
MARCHE Claude committed
82

83 84
let print_tv_binders info ~whytypes ~implicit fmt stv =
  Stv.iter (fprintf fmt "@ %a" (print_tv_binder info ~whytypes ~implicit)) stv
85

86 87
let print_tv_binders_list info ~whytypes ~implicit fmt ltv =
  List.iter (fprintf fmt "@ %a" (print_tv_binder info ~whytypes ~implicit)) ltv
MARCHE Claude's avatar
MARCHE Claude committed
88

89
let print_params info ~whytypes fmt stv =
MARCHE Claude's avatar
MARCHE Claude committed
90
  if Stv.is_empty stv then () else
91
    fprintf fmt "@[<2>forall%a,@]@ "
92
      (print_tv_binders info ~whytypes ~implicit:true) stv
93

94
let print_params_list info ~whytypes fmt ltv =
MARCHE Claude's avatar
MARCHE Claude committed
95
  match ltv with
96
  | [] -> ()
97 98 99
  | _ ->
    fprintf fmt "forall%a,@ "
      (print_tv_binders_list info ~whytypes ~implicit:false) ltv
MARCHE Claude's avatar
MARCHE Claude committed
100

MARCHE Claude's avatar
MARCHE Claude committed
101 102 103 104 105 106
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
107
  let n = id_unique iprinter vs.vs_name in
MARCHE Claude's avatar
MARCHE Claude committed
108 109 110 111 112
  fprintf fmt "%s" n

let forget_var vs = forget_id iprinter vs.vs_name

let print_ts fmt ts =
113
  fprintf fmt "%s" (id_unique iprinter ts.ts_name)
MARCHE Claude's avatar
MARCHE Claude committed
114 115

let print_ls fmt ls =
116
  fprintf fmt "%s" (id_unique iprinter ls.ls_name)
MARCHE Claude's avatar
MARCHE Claude committed
117 118

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

121 122 123 124 125 126
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 = Opt.fold Ty.ty_freevars Stv.empty ls.ls_value in
  (ty_vars_args, ty_vars_value, Stv.union ty_vars_args ty_vars_value)


127
(* unused printing function
128
let print_path = print_list (constant_string ".") string
129
*)
130 131 132

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

133
let print_id_real info fmt id =
134 135 136 137
  try
    let path,ipr = Mid.find id info.symbol_printers in
    fprintf fmt "%s.%s" path (id_unique ipr id)
  with Not_found -> print_id fmt id
138

139
let print_ls_real info fmt ls =
140
  print_id_real info fmt ls.ls_name
141

142
let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name
143
(* unused printing function
144
let print_pr_real info fmt pr = print_id_real info fmt pr.pr_name
145
*)
146

MARCHE Claude's avatar
MARCHE Claude committed
147 148
(** Types *)

149
let print_ts_tv info fmt ts =
150 151 152
  match ts.ts_args with
  | [] -> fprintf fmt "%a" print_ts ts
  | _ -> fprintf fmt "(%a %a)" print_ts ts
153
    (print_list space (print_tv info ~whytypes:false)) ts.ts_args
154

155
let protect_on ?(boxed=false) x s =
156 157
  if x then "@[<1>(" ^^ s ^^ ")@]"
  else if not boxed then "@[" ^^ s ^^ "@]"
158
  else s
159

160 161
let rec print_type ?(opr=true) info ~prec fmt ty =
  match ty.ty_node with
162
  | Tyvar v -> print_tv info ~whytypes:false fmt v
MARCHE Claude's avatar
MARCHE Claude committed
163
  | Tyapp (ts, tl) when is_ts_tuple ts ->
164 165 166 167
      begin match tl with
      | [] -> fprintf fmt "Init.Datatypes.unit"
      | [ty] -> print_type ~opr info ~prec fmt ty
      | _ -> fprintf fmt "(%a)%%type" (print_list star (print_type info ~prec:40)) tl
168
      end
169
  | Tyapp (ts, [l;r]) when ts_equal ts ts_func ->
170 171 172
      fprintf fmt (protect_on (opr && prec < 99) "%a ->@ %a")
        (print_type info ~prec:98) l
        (print_type ~opr info ~prec:99) r
173
  | Tyapp (ts, tl) ->
174 175 176 177 178 179 180 181 182 183
      begin match query_syntax info.info_syn ts.ts_name with
      | Some s when complex_syntax s ->
          syntax_arguments s (print_type info ~prec:1) fmt tl
      | Some s ->
          begin match tl with
          | [] -> pp_print_string fmt s
          | l ->
              fprintf fmt (protect_on (prec < 10) "%s%a") s
                (print_list_pre space (print_type info ~prec:9)) l
          end
MARCHE Claude's avatar
MARCHE Claude committed
184
      | None ->
185 186 187 188 189 190 191 192
          begin match tl with
          | [] -> print_ts_real info fmt ts
          | l ->
              fprintf fmt (protect_on (prec < 10) "%a%a")
                (print_ts_real info) ts
                (print_list_pre space (print_type info ~prec:9)) l
          end
      end
MARCHE Claude's avatar
MARCHE Claude committed
193 194 195 196

(* 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
197
    | Tyvar u when tv_equal u v -> true
MARCHE Claude's avatar
MARCHE Claude committed
198 199 200 201 202 203 204
    | _ -> 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
205 206 207
  match fs.ls_value with
  | None -> true
  | Some v -> inspect v
MARCHE Claude's avatar
MARCHE Claude committed
208 209 210

(** Patterns, terms, and formulas *)

211
let lparen_r fmt () = fprintf fmt "@[<1>("
212
let rparen_r fmt () = fprintf fmt ")@]"
213 214
let print_paren_r f =
  print_list_delim ~start:lparen_r ~stop:rparen_r ~sep:comma f
MARCHE Claude's avatar
MARCHE Claude committed
215

216
let arrow fmt () = fprintf fmt " ->@ "
217
let print_arrow_list fmt x = print_list_suf arrow fmt x
218

219 220
let rec print_pattern info fmt p = print_pat false info fmt p
and print_pat op info fmt p = match p.pat_node with
MARCHE Claude's avatar
MARCHE Claude committed
221 222
  | Pwild -> fprintf fmt "_"
  | Pvar v -> print_vs fmt v
Andrei Paskevich's avatar
Andrei Paskevich committed
223
  | Pas (p,v) ->
224
      fprintf fmt (protect_on op "%a as %a") (print_pat true info) p print_vs v
Andrei Paskevich's avatar
Andrei Paskevich committed
225
  | Por (p,q) ->
226
      fprintf fmt (protect_on op "%a|%a") (print_pat true info) p (print_pat true info) q
227
  | Papp (cs,pl) when is_fs_tuple cs ->
228
      print_paren_r (print_pat false info) fmt pl
229
  | Papp (cs,pl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
230
      begin match query_syntax info.info_syn cs.ls_name with
231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247
      | Some s when complex_syntax s ->
          syntax_arguments s (print_pat true info) fmt pl
      | Some s ->
          begin match pl with
          | [] -> pp_print_string fmt s
          | _ ->
              fprintf fmt (protect_on op "%s%a") s
                (print_list_pre space (print_pat true info)) pl
          end
      | None ->
          begin match pl with
          | [] -> print_ls_real info fmt cs
          | _ ->
              fprintf fmt (protect_on op "%a%a")
                (print_ls_real info) cs
                (print_list_pre space (print_pat true info)) pl
          end
Andrei Paskevich's avatar
Andrei Paskevich committed
248
      end
MARCHE Claude's avatar
MARCHE Claude committed
249

250
let print_vsty info fmt v =
251 252 253
  fprintf fmt "@[<1>(%a:@,%a)@]"
    print_vs v
    (print_type ~opr:false info ~prec:100) v.vs_ty
MARCHE Claude's avatar
MARCHE Claude committed
254

255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
let number_format info = {
    Number.long_int_support = `Default;
    Number.negative_int_support = `Custom (fun fmt f -> fprintf fmt "(-%t)%%Z" f);
    Number.dec_int_support =
      `Custom (fun fmt i ->
          fprintf fmt (if info.ssreflect then "%s%%:Z" else "%s%%Z") (BigInt.to_string i));
    Number.hex_int_support = `Unsupported;
    Number.oct_int_support = `Unsupported;
    Number.bin_int_support = `Unsupported;
    Number.negative_real_support = `Custom (fun fmt f -> fprintf fmt "(-%t)%%R" f);
    Number.dec_real_support = `Unsupported;
    Number.hex_real_support = `Unsupported;
    Number.frac_real_support =
      `Custom
        ((fun fmt i -> fprintf fmt "%s%%R" i),
         (fun fmt i n -> fprintf fmt "(%s * %s)%%R" i n),
         (fun fmt i n -> fprintf fmt "(%s / %s)%%R" i n));
  }


275 276 277
(* [opr] means that there is no expected delimiter on the right of the term,
   so parentheses should be put around the term if it does not end with a
   delimiter, to avoid any ambiguity *)
278

279 280
let rec print_term ?(boxed=false) ?(opr=true) info ~prec fmt t =
  match t.t_node with
MARCHE Claude's avatar
MARCHE Claude committed
281 282
  | Tvar v ->
      print_vs fmt v
283
  | Tconst c ->
284
      Number.print (number_format info) fmt c
MARCHE Claude's avatar
MARCHE Claude committed
285 286
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
287 288 289 290
      fprintf fmt (protect_on (opr && prec < 200) "let %a :=@ %a in@ %a")
        print_vs v
        (print_term info ~prec:200) t1
        (print_term ~opr info ~prec:200) t2;
MARCHE Claude's avatar
MARCHE Claude committed
291
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
292
  | Tcase (t,bl) ->
293
      fprintf fmt "@[<v>match %a with@,%a@,end@]"
294
        (print_term info ~prec:200) t
295
        (print_list pp_print_cut (print_tbranch info)) bl
296
  | Teps _ ->
297
      let vl,_,t0 = t_open_lambda t in
298 299
      if vl = [] then unsupportedTerm t "???"
      else begin
300 301
        if t0.t_ty = None then unsupportedTerm t
          "Coq: Prop-typed lambdas are not supported";
302
        fprintf fmt (protect_on (prec < 200) "fun %a =>@ %a")
303
          (print_list space (print_vsty info)) vl
304
          (print_term info ~prec:200) t0;
305 306
        List.iter forget_var vl
      end
MARCHE Claude's avatar
MARCHE Claude committed
307
  | Tapp (fs,[]) when is_fs_tuple fs ->
308
      fprintf fmt "Init.Datatypes.tt"
309
  | Tapp (fs,pl) when is_fs_tuple fs ->
310
      fprintf fmt "%a" (print_paren_r (print_term ~prec:250 info)) pl
311
  | Tapp (fs,[l;r]) when ls_equal fs fs_func_app ->
312 313
      fprintf fmt (protect_on (prec < 10) "%a@ %a")
        (print_term info ~prec:10) l (print_term info ~prec:9) r
MARCHE Claude's avatar
MARCHE Claude committed
314
  | Tapp (fs, tl) ->
315 316
      begin match query_syntax info.info_syn fs.ls_name with
      | Some s when complex_syntax s ->
317
          syntax_arguments s (print_term info ~prec:1) fmt tl
318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338
      | Some s ->
          begin match tl with
          | [] -> pp_print_string fmt s
          | _ ->
              fprintf fmt (protect_on (prec < 10) "%s%a") s
                (print_list_pre space (print_term info ~prec:9)) tl
          end
      | None ->
        if unambig_fs fs then
          match tl with
          | [] -> print_ls_real info fmt fs
          | _ ->
              fprintf fmt (protect_on (prec < 10) "%a%a")
                (print_ls_real info) fs
                (print_list_pre space (print_term info ~prec:9)) tl
        else
          fprintf fmt (protect_on (prec < 100) "@[%a%a@] :@ %a")
            (print_ls_real info) fs
            (print_list_pre space (print_term ~prec:9 info)) tl
            (print_type ~opr info ~prec:100) (t_type t)
      end
339 340
  | Tquant (Tforall,fq) ->
      let vl,_tl,f = t_open_quant fq in
341
      fprintf fmt (protect_on ~boxed (opr && prec < 200) "@[<2>forall %a@],@ %a")
342
        (print_list space (print_vsty info)) vl
343
        (print_term ~boxed:true ~opr info ~prec:200) f;
344
      List.iter forget_var vl
345 346
  | Tquant (Texists,fq) ->
      let vl,_tl,f = t_open_quant fq in
MARCHE Claude's avatar
MARCHE Claude committed
347
      let rec aux fmt vl =
348
        match vl with
349
        | [] -> print_term ~opr info ~prec:200 fmt f
350
        | v::vr ->
351 352 353 354
            fprintf fmt "exists %a:@,%a,@ %a"
              print_vs v
              (print_type ~opr:false info ~prec:100) v.vs_ty
              aux vr in
355
      fprintf fmt (protect_on (opr && prec < 200) "%a") aux vl;
MARCHE Claude's avatar
MARCHE Claude committed
356
      List.iter forget_var vl
357
  | Ttrue ->
MARCHE Claude's avatar
MARCHE Claude committed
358
      fprintf fmt "True"
359
  | Tfalse ->
MARCHE Claude's avatar
MARCHE Claude committed
360
      fprintf fmt "False"
361
  | Tbinop (b,f1,f2) ->
362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379
      begin match b with
      | Tand ->
          fprintf fmt (protect_on (prec < 80) "%a /\\@ %a")
            (print_term info ~prec:79) f1
            (print_term info ~prec:80) f2
      | Tor ->
          fprintf fmt (protect_on (prec < 85) "%a \\/@ %a")
            (print_term info ~prec:84) f1
            (print_term info ~prec:85) f2
      | Timplies ->
          fprintf fmt (protect_on ~boxed (prec < 99) "%a ->@ %a")
            (print_term info ~prec:98) f1
            (print_term ~boxed:true ~opr info ~prec:99) f2
      | Tiff ->
          fprintf fmt (protect_on (prec < 95) "%a <->@ %a")
            (print_term info ~prec:94) f1
            (print_term info ~prec:94) f2
      end
380
  | Tnot f ->
381
      fprintf fmt "~ %a" (print_term info ~prec:75) f
382
  | Tif (f1,f2,f3) ->
383
      fprintf fmt (protect_on opr
384
        "if %a then@ %a@ else@ %a")
385 386 387
        (print_term info ~prec:200) f1
        (print_term info ~prec:200) f2
        (print_term info ~prec:200) f3
MARCHE Claude's avatar
MARCHE Claude committed
388

389
and print_tbranch info fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
390
  let p,t = t_open_branch br in
391
  fprintf fmt "@[<4>| %a =>@ %a@]"
392
    (print_pattern info) p (print_term info ~prec:200) t;
Andrei Paskevich's avatar
Andrei Paskevich committed
393
  Svs.iter forget_var p.pat_vars
MARCHE Claude's avatar
MARCHE Claude committed
394 395 396

(** Declarations *)

397
let print_constr info ts fmt (cs,_) =
398
  fprintf fmt "@[<4>| %a : %a%a%a@]" print_ls cs
399
    (print_arrow_list (print_type info ~prec:98)) cs.ls_args
400 401
    print_ts ts
      (print_list_pre space (print_tv info ~whytypes:false)) ts.ts_args
MARCHE Claude's avatar
MARCHE Claude committed
402

403 404 405 406 407 408
(*

  copy of old user scripts

*)

409
type content_type =
410
  Notation | (*Gallina |*) Vernacular
411

412
type statement =
413
  | Info  of string  (* name *)
414 415 416
  | Axiom of string (* name *)
  | Query of string * content_type * string (* name and content *)
  | Other of string (* content *)
417

418 419 420
exception StringValue of string

let read_generated_name =
421
  let def = Str.regexp "\\(Definition\\|Fixpoint\\|Inductive\\|CoInductive\\)[ ]+\\([^ :(.]+\\)" in
422
  fun ch ->
423 424 425
  try
    while true do
      let s = input_line ch in
426 427 428 429 430 431
      if Str.string_match def s 0 then
        raise (StringValue (Str.matched_group 2 s))
    done;
    assert false
  with StringValue name -> name

432 433 434 435 436 437
(** no nested comment *)
let read_comment =
  let start_comment = Str.regexp "(\\*[ ]+\\([^ :]+\\)" in
  let end_comment = Str.regexp ".*\\*)" in
  fun ch ->
    let line = ref "" in
438
    (* look for "( * name" *)
439 440 441 442 443 444 445 446 447 448 449
    let name =
      try
        while true do
          let s = input_line ch in
          if Str.string_match start_comment s 0 then begin
            line := s;
            raise (StringValue (Str.matched_group 1 s))
          end
        done;
        assert false
      with StringValue name -> name in
450
    (* look for end of comment *)
451 452 453 454 455
    while not (Str.string_match end_comment (!line) 0) do
      line := input_line ch
    done;
    name

456 457 458 459
let read_until re s i ch =
  if not (Str.string_match re s i) then
    while not (Str.string_match re (input_line ch) 0) do () done

460 461 462 463 464 465
let read_until_or_eof re s i ch =
  try
    read_until re s i ch
  with
  | End_of_file -> ()

466
let read_old_proof =
467
  let def = Str.regexp "\\(Definition\\|Notation\\|Lemma\\|Theorem\\|Variable\\|Hypothesis\\)[ ]+\\([^ :({.]+\\)" in
468
  let def_end = Str.regexp ".*[.]$" in
469 470
  let old_intros = Str.regexp "^ *([*] Why3 intros " in
  let old_end = Str.regexp ".*[*])" in
471 472 473
  let qed = Str.regexp "\\(Qed\\|Defined\\|Save\\|Admitted\\)[.]" in
  fun ch ->
  try
474
    let start = ref (pos_in ch) in
475 476
    let s = input_line ch in
    if not (Str.string_match def s 0) then raise (StringValue s);
477
    let kind = Str.matched_group 1 s in
478
    let name = Str.matched_group 2 s in
479
    read_until def_end s (Str.match_end ()) ch;
480 481 482 483 484 485 486
    match kind with
    | "Variable" | "Hypothesis" -> Axiom name
    | _  ->
      let k =
        if kind = "Notation" then Notation
        else begin
          start := pos_in ch;
487 488 489 490
          let s = input_line ch in
          if Str.string_match old_intros s 0 then begin
            read_until old_end s (Str.match_end ()) ch;
            start := pos_in ch;
491
            read_until_or_eof qed (input_line ch) 0 ch
492
          end else
493
            read_until_or_eof qed s 0 ch;
494 495 496
          Vernacular
        end in
      let len = pos_in ch - !start in
497
      let s = Bytes.create len in
498 499
      seek_in ch !start;
      really_input ch s 0 len;
500
      Query (name, k, Bytes.unsafe_to_string s)
501 502
  with StringValue s -> Other s

503
(* Load old-style proofs where users were confined to a few sections. *)
504
let read_deprecated_script ch in_context =
505
  let sc = ref [] in
506
  let context = ref in_context in
507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523
  try
    while true do
      let pos = pos_in ch in
      let s = input_line ch in
      if !context then
        if s = "(* DO NOT EDIT BELOW *)" then context := false else
        sc := Other s :: !sc
      else if s <> "" then begin
        seek_in ch pos;
        sc := read_old_proof ch :: Other "" :: !sc;
        raise End_of_file
      end
    done;
    assert false
  with
  | End_of_file -> !sc

524 525
let read_old_script =
  let axm = Str.regexp "\\(Axiom\\|Parameter\\)[ ]+\\([^ :(.]+\\)" in
526
  let prelude = Str.regexp "(\\* This file is generated by Why3.*\\*)" in
527
  fun ch ->
528
  let skip_to_empty = ref false in
529
  let last_empty_line = ref 0 in
530
  let sc = ref [] in
531 532 533
  try
    while true do
      let s = input_line ch in
534
      if s = "" then last_empty_line := pos_in ch;
535
      if !skip_to_empty then (if s = "" then skip_to_empty := false) else
536 537 538
      if s = "(* Why3 comment *)" then
        (let name = read_comment ch in sc := Info name :: !sc;
         skip_to_empty := true) else
539 540 541 542 543 544
      if s = "(* Why3 assumption *)" then
        (let name = read_generated_name ch in sc := Axiom name :: !sc;
        skip_to_empty := true) else
      if Str.string_match axm s 0 then
        (let name = Str.matched_group 2 s in sc := Axiom name :: !sc;
        skip_to_empty := true) else
545 546
      if s = "(* Why3 goal *)" then
        (sc := read_old_proof ch :: !sc; skip_to_empty := true) else
547 548 549
      if Str.string_match prelude s 0 then
        (sc := Info "Why3 prelude" :: !sc;
         skip_to_empty := true) else
550
      if s = "(* YOU MAY EDIT THE CONTEXT BELOW *)" then
551 552 553 554 555
        (sc := read_deprecated_script ch true; raise End_of_file) else
      if s = "(* YOU MAY EDIT THE PROOF BELOW *)" then
        (seek_in ch !last_empty_line;
        sc := read_deprecated_script ch false;
        raise End_of_file) else
556 557 558
      sc := Other s :: !sc
    done;
    assert false
559
  with
560 561 562 563 564 565 566 567 568 569 570 571
  | End_of_file ->
    let rec rmv = function
      | Other "" :: t -> rmv t
      | l -> l in
    List.rev (rmv !sc)

(* Output all the Other entries of the script that occur before the
   location of name. Modify the script by removing the name entry and all
   these outputs. Return the user content. *)
let output_till_statement fmt script name =
  let print i =
    let rec aux acc = function
572 573 574 575 576
      | h :: l when h == i ->
        let l = match l with
          | Other "" :: l -> l
          | _ -> l in
        script := List.rev_append acc l
577 578 579 580 581
      | Other o :: l -> fprintf fmt "%s@\n" o; aux acc l
      | h :: l -> aux (h :: acc) l
      | [] -> assert false in
    aux [] !script in
  let rec find = function
582
    | Info n as o :: _ when n = name -> print o; Some o
583 584 585 586 587 588
    | Axiom n as o :: _ when n = name -> print o; Some o
    | Query (n,_,_) as o :: _ when n = name -> print o; Some o
    | [] -> None
    | _ :: t -> find t in
  find !script

589 590
let output_remaining fmt script =
  List.iter (function
591
    | Info _ | Axiom _ -> ()
592 593
    | Query (n,_,c) -> fprintf fmt "(* Unused content named %s@\n%s *)@\n" n c
    | Other c -> fprintf fmt "%s@\n" c) script
594

595 596 597
let rec intros_hyp n fmt f =
  match f.t_node with
    | Tbinop(Tand,f1,f2) ->
598
      fprintf fmt "(";
599
      let (m,vsl1) = intros_hyp n fmt f1 in
600
      fprintf fmt ",";
601
      let (k,vsl2) = intros_hyp m fmt f2 in
602
      fprintf fmt ")";
603
      (k,vsl1@vsl2)
604 605 606 607 608 609 610 611 612 613 614
    | Tquant(Texists,fq) ->
      let vsl,_trl,f = t_open_quant fq in
      let rec aux n vsl =
        match vsl with
          | [] -> intros_hyp n fmt f
          | v::l ->
            fprintf fmt "(%a," print_vs v;
            let m = aux n l in
            fprintf fmt ")";
            m
      in
615
      aux n vsl
616
    | _ ->
617
      fprintf fmt "h%d" n;
618
      (n+1,[])
619 620 621 622 623 624 625 626 627 628 629 630 631 632 633

let rec do_intros n fmt fmla =
  match fmla.t_node with
    | Tlet(_,fb) ->
      let vs,f = t_open_bound fb in
      fprintf fmt "@ %a" print_vs vs;
      do_intros n fmt f;
      forget_var vs
    | Tquant(Tforall,fq) ->
      let vsl,_trl,f = t_open_quant fq in
      List.iter
        (fun v -> fprintf fmt "@ %a" print_vs v) vsl;
      do_intros n fmt f;
      List.iter forget_var vsl
    | Tbinop(Timplies, f1, f2) ->
634
      fprintf fmt "@ ";
635 636 637
      let m,vsl = intros_hyp n fmt f1 in
      do_intros m fmt f2;
      List.iter forget_var vsl
638 639
    | _ -> ()

640
let need_intros fmla =
641 642 643 644 645 646
  match fmla.t_node with
  | Tlet _
  | Tquant(Tforall,_)
  | Tbinop(Timplies, _, _) -> true
  | _ -> false

647 648
let intros fmt fmla =
  fprintf fmt "@[intros%a.@]" (do_intros 1) fmla
649

650
let print_empty_proof fmt def =
651
  match def with
652
    | Some (_params,fmla) ->
653
      fprintf fmt "Proof.@\n";
654
      if need_intros fmla then intros fmt fmla;
655
      fprintf fmt "@\n@\nQed.@\n"
656
    | None ->
657
      fprintf fmt "Proof.@\n@\nDefined.@\n"
658

659
let print_previous_proof def info fmt previous =
660
  match previous with
661
  | None ->
662 663
    print_empty_proof fmt def
  | Some (Query (_,Vernacular,c)) ->
664
    begin match def with
665 666
    | Some (_p, f) when not info.realization && need_intros f ->
        fprintf fmt "@[(* Why3 %a *)@]@\n" (fun fmt f -> intros fmt f) f
667 668
    | _ -> ()
    end;
669
    fprintf fmt "%s" c
670
  | Some (Query (_,Notation,_))
671
  | Some (Axiom _) | Some (Other _) | Some (Info _) ->
672
    assert false
673

674
let print_type_decl ~prev info fmt ts =
MARCHE Claude's avatar
MARCHE Claude committed
675
  if is_ts_tuple ts then () else
676
  match ts.ts_def with
Clément Fumex's avatar
Clément Fumex committed
677
    | NoDef | Range _ | Float _ ->
678
      if info.realization then
679 680 681
        match prev with
        | Some (Query (_,Notation,c)) ->
          fprintf fmt "(* Why3 goal *)@\n%s@\n" c
682
        | Some (Axiom _) ->
683
          fprintf fmt "(* Why3 goal *)@\n@[<hv 2>Variable %a :@ @[%aType.@]@]@\n@[<hv 2>Hypothesis %a_WhyType :@ @[%aWhyType %a.@]@]@\nExisting Instance %a_WhyType.@\n@\n"
684 685 686
            print_ts ts (print_params_list info ~whytypes:false) ts.ts_args
            print_ts ts (print_params_list info ~whytypes:true)
              ts.ts_args (print_ts_tv info) ts print_ts ts
687
        | _ ->
688
          fprintf fmt "(* Why3 goal *)@\n@[<hv 2>Definition %a :@ @[%aType.@]@]@\n%a@\n"
689
            print_ts ts (print_params_list info ~whytypes:false) ts.ts_args
690
            (print_previous_proof None info) prev
691
      else begin
692
        fprintf fmt "@[<hv 2>Axiom %a :@ @[%aType.@]@]@\n"
693 694
          print_ts ts (print_params_list info ~whytypes:false) ts.ts_args;
        if not info.ssreflect then begin
695
          fprintf fmt "@[<hv 2>Parameter %a_WhyType :@ @[%aWhyType %a.@]@]@\n"
696 697 698 699 700 701 702
            print_ts ts (print_params_list info ~whytypes:true) ts.ts_args
            (print_ts_tv info) ts;
          fprintf fmt "Existing Instance %a_WhyType.@\n"
            print_ts ts
        end;
        fprintf fmt "@\n"
      end
Clément Fumex's avatar
Clément Fumex committed
703
    | Alias ty ->
704
      fprintf fmt "(* Why3 assumption *)@\n@[<2>Definition %a%a :=@ %a.@]@\n@\n"
705 706
        print_ts ts
          (print_list_pre space
707
             (print_tv_binder info ~whytypes:false ~implicit:false)) ts.ts_args
708
        (print_type ~opr:false info ~prec:200) ty
709

710
let print_type_decl ~prev info fmt ts =
711
  if not (Mid.mem ts.ts_name info.info_syn) then
712
    (print_type_decl ~prev info fmt ts; forget_tvs ())
713

714
let print_data_decl ~first info fmt ts csl =
715
  let name = id_unique iprinter ts.ts_name in
716
  if first then
717
    fprintf fmt "(* Why3 assumption *)@\n@[<2>Inductive"
718
  else fprintf fmt "@\nwith";
719
  fprintf fmt " %s%a :=@\n@[%a@]"
720
    name (print_list_pre space
721
            (print_tv_binder info ~whytypes:false ~implicit:false)) ts.ts_args
722
    (print_list newline (print_constr info ts)) csl;
723 724
  name

725 726
let print_data_whytype_and_implicits info fmt (name,ts,csl) =
  if not info.ssreflect then
727
    fprintf fmt "@[<2>Axiom %s_WhyType : %aWhyType %a.@]@\nExisting Instance %s_WhyType.@\n"
728 729
      name (print_params_list info ~whytypes:true) ts.ts_args
      (print_ts_tv info) ts name;
730 731
  List.iter
    (fun (cs,_) ->
732 733
      let _, _, all_ty_params = ls_ty_vars cs in
      if not (Stv.is_empty all_ty_params) then
734
        let print fmt tv =
735 736
          fprintf fmt "{%a}" (print_tv info ~whytypes:false) tv in
        fprintf fmt "@[<2>Arguments %a@ %a.@]@\n"
737 738
          print_ls cs
          (print_list space print) ts.ts_args)
739 740 741
    csl;
  fprintf fmt "@\n"

742 743 744 745 746 747 748 749 750 751 752 753 754 755
let print_data_decls info fmt tl =
  let none,d =
    List.fold_left
      (fun ((first,l) as acc) (ts,csl) ->
        if is_ts_tuple ts || Mid.mem ts.ts_name info.info_syn
        then acc else
        let name = print_data_decl info ~first fmt ts csl in
        forget_tvs ();
        (false,(name,ts,csl)::l))
      (true,[]) tl
  in
  if none then () else
    begin
      fprintf fmt ".@]@\n";
756
      List.iter (print_data_whytype_and_implicits info fmt) d
757
    end
MARCHE Claude's avatar
MARCHE Claude committed
758

759
let print_ls_type info fmt = function
760
  | None -> fprintf fmt "Prop"
761
  | Some ty -> print_type ~opr:false info ~prec:100 fmt ty
MARCHE Claude's avatar
MARCHE Claude committed
762

763
let print_param_decl ~prev info fmt ls =
764
  let _, _, all_ty_params = ls_ty_vars ls in
765
  if info.realization then
766
    match prev with
767 768 769
    | Some (Query (_,Notation,c)) ->
      fprintf fmt "(* Why3 goal *)@\n%s@\n" c
    | Some (Axiom _) ->
770
      fprintf fmt "(* Why3 goal *)@\n@[<2>Variable %a: %a%a%a.@]@\n@\n"
771
        print_ls ls (print_params info ~whytypes:true) all_ty_params
772
        (print_arrow_list (print_type info ~prec:98)) ls.ls_args
773
        (print_ls_type info) ls.ls_value
774 775 776 777 778 779 780 781
    | (* Some Info *) _ when Mid.mem ls.ls_name info.info_syn ->
      let vl =
        List.map (fun ty -> create_vsymbol (id_fresh "x") ty) ls.ls_args in
      let e = Term.t_app ls (List.map Term.t_var vl) ls.ls_value in
      fprintf fmt
        "(* Why3 comment *)@\n\
         (* %a is replaced with %a by the coq driver *)@\n@\n"
        print_ls ls
782
        (print_term info ~prec:1) e;
783
      List.iter forget_var vl
784
    | _ ->
785 786 787
      fprintf fmt "(* Why3 goal *)@\n@[<hv 2>Definition @[<h>%a%a@] :@ @[%a%a.@]@]@\n%a@\n"
        print_ls ls
        (print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
788
        (print_arrow_list (print_type info ~prec:98)) ls.ls_args
789
        (print_ls_type info) ls.ls_value
790
        (print_previous_proof None info) prev
791
  else
792
    fprintf fmt "@[<hv 2>Parameter %a:@ @[%a%a%a.@]@]@\n@\n"
793
      print_ls ls (print_params info ~whytypes:true) all_ty_params
794
      (print_arrow_list (print_type info ~prec:98)) ls.ls_args
795
      (print_ls_type info) ls.ls_value
796

797
let print_param_decl ~prev info fmt ls =
798
  if info.realization || not (Mid.mem ls.ls_name info.info_syn) then
799
    (print_param_decl ~prev info fmt ls; forget_tvs ())
800 801

let print_logic_decl info fmt (ls,ld) =
802
  let _, _, all_ty_params = ls_ty_vars ls in
803
  let vl,e = open_ls_defn ld in
804
  fprintf fmt "(* Why3 assumption *)@\n@[<hv 2>@[<4>Definition %a%a%a :@ %a@] :=@ @[%a.@]@]@\n"
805
    print_ls ls
806
    (print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
807
    (print_list_pre space (print_vsty info)) vl
808
    (print_ls_type info) ls.ls_value
809
    (print_term ~opr:false info ~prec:200) e;
810 811 812
  List.iter forget_var vl;
  fprintf fmt "@\n"

813 814 815 816
let print_equivalence_lemma ~prev info fmt name (ls,ld) =
  let _, _, all_ty_params = ls_ty_vars ls in
  let def_formula = ls_defn_axiom ld in
  fprintf fmt
817
    "(* Why3 goal *)@\n@[<hv 2>Lemma @[<h>%s%a@] :@ @[%a.@]@]@\n%a@\n"
818
    name
819
    (print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
820
    (print_term ~opr:false info ~prec:200) def_formula
821
    (print_previous_proof (Some (all_ty_params,def_formula)) info) prev
822 823 824 825 826 827 828 829 830

let print_equivalence_lemma ~old info fmt ((ls,_) as d) =
  if info.realization && (Mid.mem ls.ls_name info.info_syn) then
    let name = Ident.string_unique iprinter
      ((id_unique iprinter ls.ls_name)^"_def") in
    let prev = output_till_statement fmt old name in
    (print_equivalence_lemma ~prev info fmt name d; forget_tvs ())

let print_logic_decl ~old info fmt d =
831 832 833
  (* During realization the definition of a "builtin" symbol is
     printed and an equivalence lemma with associated coq function is
     requested *)
834
  if not (Mid.mem (fst d).ls_name info.info_syn) then
835
    (print_logic_decl info fmt d; forget_tvs ())
836 837
  else if info.realization then
    print_equivalence_lemma ~old info fmt d
MARCHE Claude's avatar
MARCHE Claude committed
838

839
let print_recursive_decl info fmt (ls,ld) =
840
  let _, _, all_ty_params = ls_ty_vars ls in
841 842
  let i = match Decl.ls_defn_decrease ld with
    | [i] -> i | _ -> assert false in
843 844 845
  let vl,e = open_ls_defn ld in
  fprintf fmt "%a%a%a {struct %a}: %a :=@ %a@]"
    print_ls ls
846
    (print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
847
    (print_list_pre space (print_vsty info)) vl
848 849
    print_vs (List.nth vl i)
    (print_ls_type info) ls.ls_value
850
    (print_term ~opr:false info ~prec:200) e;
851
  List.iter forget_var vl
852

853 854 855 856 857 858 859
let print_recursive_decl ~old info fmt dl =
  let dl_syn, dl_no_syn =
    List.partition (fun (ls,_) ->
      info.realization && (Mid.mem ls.ls_name info.info_syn)) dl in
  if dl_no_syn <> [] then begin
    fprintf fmt "(* Why3 assumption *)@\n";
    print_list_delim
860
      ~start:(fun fmt () -> fprintf fmt "@[<2>Fixpoint ")
861
      ~stop:(fun fmt () -> fprintf fmt ".@]@\n")
862
      ~sep:(fun fmt () -> fprintf fmt "@]@\n@[<2>with ")
863 864 865 866 867 868
      (fun fmt d -> print_recursive_decl info fmt d; forget_tvs ())
      fmt dl_no_syn;
    fprintf fmt "@\n";
  end;
  List.iter (print_equivalence_lemma ~old info fmt) dl_syn

869
let print_ind info fmt (pr,f) =
870 871 872
  fprintf fmt "@[<hv 4>| %a :@ @[%a@]@]"
    print_pr pr
    (print_term ~opr:false info ~prec:200) f
MARCHE Claude's avatar
MARCHE Claude committed
873

874
let print_ind_decl info fmt ps bl =
875
  let _, _, all_ty_params = ls_ty_vars ps in
876
  fprintf fmt " %a%a: %aProp :=@ @[%a@]"
877 878
    print_ls ps
    (print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
879
    (print_arrow_list (print_type info ~prec:98)) ps.ls_args
880
    (print_list newline (print_ind info)) bl
MARCHE Claude's avatar
MARCHE Claude committed
881

882 883 884 885 886 887
let print_ind_decls info s fmt tl =
  let none =
    List.fold_left (fun first (ps,bl) ->
      if Mid.mem ps.ls_name info.info_syn then first
      else begin
        if first then
888
          fprintf fmt "(* Why3 assumption *)@\n@[<2>%s"
889 890 891 892 893 894 895
            (match s with Ind -> "Inductive" | Coind -> "CoInductive")
          else fprintf fmt "@\nwith";
        print_ind_decl info fmt ps bl;
        forget_tvs ();
        false
      end) true tl in
  if not none then fprintf fmt ".@]@\n@\n"
MARCHE Claude's avatar
MARCHE Claude committed
896

897
let print_prop_decl ~prev info fmt (k,pr,f) =
Jean-Christophe's avatar
Jean-Christophe committed
898
  ignore prev;
899 900 901 902 903 904
  let params = t_ty_freevars Stv.empty f in
  let stt = match k with
    | Paxiom when info.realization -> "Lemma"
    | Paxiom -> ""
    | Plemma -> "Lemma"
    | Pgoal -> "Theorem"
905
  in
906
  if stt <> "" then
907 908
    match prev with
    | Some (Axiom _) when stt = "Lemma" ->
909
      fprintf fmt "(* Why3 goal *)@\n@[<hv 2>Hypothesis %a :@ @[%a%a.@]@]@\n@\n"
910
        print_pr pr (print_params info ~whytypes:true) params
911
        (print_term ~opr:false info ~prec:200) f
912
    | _ ->
913 914 915
      fprintf fmt "(* Why3 goal *)@\n@[<hv 2>%s @[<h>%a%a@] :@ @[%a.@]@]@\n%a@\n"
        stt print_pr pr
        (print_tv_binders info ~whytypes:true ~implicit:true) params
916
        (print_term ~opr:false info ~prec:200) f
917
        (print_previous_proof (Some (params,f)) info) prev
918
  else
919
    fprintf fmt "@[<hv 2>Axiom %a :@ @[%a%a.@]@]@\n@\n"
920
      print_pr pr (print_params info ~whytypes:true) params
921
      (print_term ~opr:false info ~prec:200) f;
922
  forget_tvs ()
923

924 925 926 927 928 929 930
let print_decl ~old info fmt d =
  let name =
    match d.d_node with
    | Dtype ts
    | Ddata ((ts, _)::_) -> id_unique iprinter ts.ts_name
    | Dparam ls
    | Dlogic ((ls,_)::_)
931
    | Dind (_, (ls,_)::_) -> id_unique iprinter ls.ls_name
932 933 934
    | Dprop (_,pr,_) -> id_unique iprinter pr.pr_name
    | Ddata []
    | Dlogic []
935
    | Dind (_, []) -> assert false in
936 937
  let prev = output_till_statement fmt old name in
  match d.d_node with
938
  | Dtype ts ->
939
      print_type_decl ~prev info fmt ts
940
  | Ddata tl -> print_data_decls info fmt tl
941
  | Dparam ls ->
942
      print_param_decl ~prev info fmt ls
943
  | Dlogic [s,_ as ld] when not (Sid.mem s.ls_name d.d_syms) ->
944
      print_logic_decl ~old info fmt ld
945
  | Dlogic ll ->
946
      print_recursive_decl ~old info fmt ll
947
  | Dind (s, il) ->
948
      print_ind_decls info s fmt il
949
  | Dprop (_,pr,_) when not info.realization && Mid.mem pr.pr_name info.info_syn ->
950
      ()
951
  | Dprop pr ->
952
      print_prop_decl ~prev info fmt pr
MARCHE Claude's avatar
MARCHE Claude committed
953

954
let print_decls ~old info fmt dl =
955
  fprintf fmt "@\n@[%a@]" (print_list nothing (print_decl ~old info)) dl
MARCHE Claude's avatar
MARCHE Claude committed
956

957
let print_task printer_args ~realize ~ssreflect ?old fmt task =
958
  (* eprintf "Task:%a@.@." Pretty.print_task task; *)
959
  forget_all ();
960 961
  (* find theories that are both used and realized from metas *)
  let realized_theories =
Andrei Paskevich's avatar
Andrei Paskevich committed
962
    Task.on_meta meta_realized_theory (fun mid args ->
963 964 965
      match args with
      | [Theory.MAstr s1; Theory.MAstr s2] ->
        (* TODO: do not split string; in fact, do not even use a string argument *)
966
        let f,id =
967
          let l = Strings.rev_split '.' s1 in
968
          List.rev (List.tl l), List.hd l in
969
        let th = Env.read_theory printer_args.env f id in
970 971 972
        Mid.add th.Theory.th_name (th, if s2 = "" then s1 else s2) mid
      | _ -> assert false
    ) Mid.empty task in
973
  (* 2 cases: goal is use T or goal is a real goal *)
974 975 976 977
  let rec upd_realized_theories = function
    | Some { Task.task_decl = { Theory.td_node =
               Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, _) }}} ->
        realized_theories
978
    | Some { Task.task_decl = { Theory.td_node = Theory.Use th }} ->
979 980 981 982 983 984 985
        Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
        Mid.remove th.Theory.th_name realized_theories
    | Some { Task.task_decl = { Theory.td_node = Theory.Meta _ };
             Task.task_prev = task } ->
        upd_realized_theories task
    | _ -> assert false in
  let realized_theories = upd_realized_theories task in
986
  let realized_theories' = Mid.map fst realized_theories in
987 988
  let realized_symbols = Task.used_symbols realized_theories' in
  let local_decls = Task.local_decls task realized_symbols in
989
  (* eprintf "local_decls:%i@." (List.length local_decls); *)
990 991 992 993 994 995 996 997 998 999 1000 1001
  (* associate a special printer to each symbol in a realized theory *)
  let symbol_printers =
    let printers =
      Mid.map (fun th ->
        let pr = fresh_printer () in
        Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
        pr
      ) realized_theories' in
    Mid.map (fun th ->
      (snd (Mid.find th.Theory.th_name realized_theories),
       Mid.find th.Theory.th_name printers)
    ) realized_symbols in
1002 1003
  let info = {
    info_syn = get_syntax_map task;
1004 1005
    symbol_printers = symbol_printers;
    realization = realize;
1006
    ssreflect = ssreflect;
1007 1008
  }
  in
1009 1010 1011
  let old = ref (match old with
    | None -> []
    | Some ch -> read_old_script ch) in
1012 1013 1014 1015
  ignore (output_till_statement fmt old "Why3 prelude");
  print_prelude fmt printer_args.prelude;
  print_th_prelude task fmt printer_args.th_prelude;
  Mid.iter (fun _ (_, s) -> fprintf fmt "Require %s.@\n" s) realized_theories;
1016 1017
  print_decls ~old info fmt local_decls;
  output_remaining fmt !old
MARCHE Claude's avatar
MARCHE Claude committed
1018

1019
let print_task_full args ?old fmt task =
1020
  print_task args ~realize:false ~ssreflect:false ?old fmt task
MARCHE Claude's avatar
MARCHE Claude committed
1021

1022
let print_task_real args ?old fmt task =
1023
  print_task args ~realize:true  ~ssreflect:false ?old fmt task
MARCHE Claude's avatar
MARCHE Claude committed
1024

1025
let () = register_printer "coq" print_task_full
1026 1027
  ~desc:"Printer@ for@ the@ Coq@ proof@ assistant@ \
         (without@ realization@ capabilities)."
1028
let () = register_printer "coq-realize" print_task_real
1029 1030
  ~desc:"Printer@ for@ the@ Coq@ proof@ assistant@ \
         (with@ realization@ capabilities)."
MARCHE Claude's avatar
MARCHE Claude committed
1031

1032 1033 1034 1035 1036 1037 1038
let print_task_full_ssr args ?old fmt task =
  print_task args ~realize:false ~ssreflect:true ?old fmt task
let () = register_printer "coq-ssr" print_task_full_ssr
  ~desc:"Printer@ for@ the@ Coq@ proof@ assistant,@ ssreflect@ extension\
         (without@ realization@ capabilities)."


1039
(* specific printer for realization of theories *)
1040
(* OBSOLETE
1041 1042 1043

open Theory

1044
let print_tdecl ~old info fmt d = match d.td_node with
1045 1046 1047 1048 1049
  | Decl d ->
      print_decl ~old info fmt d
  | Use t ->
      fprintf fmt "Require %s.@\n@\n"
        (id_unique iprinter t.th_name)
1050 1051
  | Meta _ -> assert false (* TODO ? *)
  | Clone _ -> assert false (* TODO *)
1052

1053
let print_tdecls ~old info fmt dl =
1054 1055
  fprintf fmt "@[<hov>%a@\n@]"
    (print_list nothing (print_tdecl ~old info)) dl
1056

1057
let print_theory _env pr thpr ?old fmt th =
1058 1059 1060 1061
  forget_all ();
  print_prelude fmt pr;
  print_prelude_for_theory th fmt thpr;
  let info = {
1062 1063
    info_syn = (Mid.empty : string Ident.Mid.t)
      (* get_syntax_map_of_theory th*);
1064
    rea