coq.ml 27.3 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 fresh_printer () =
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 40
let iprinter = fresh_printer ()

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

let tv_set = ref Sid.empty

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

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

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

56 57 58 59 60
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
61 62 63 64 65 66 67 68 69 70 71 72 73 74
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

75 76 77
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
78 79
let print_params_list fmt ltv =
  match ltv with
80
    | [] -> ()
MARCHE Claude's avatar
MARCHE Claude committed
81 82
    | _ -> fprintf fmt "forall%a,@ " print_ne_params_list ltv

MARCHE Claude's avatar
MARCHE Claude committed
83 84 85 86 87 88
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
89
  let n = id_unique iprinter vs.vs_name in
MARCHE Claude's avatar
MARCHE Claude committed
90 91 92 93 94
  fprintf fmt "%s" n

let forget_var vs = forget_id iprinter vs.vs_name

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

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

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

103 104 105
(* info *)

type info = {
106
  info_syn : syntax_map;
107
  symbol_printers : (string * ident_printer) Mid.t;
108
  realization : bool;
109 110
}

111 112 113 114
let print_path = print_list (constant_string ".") string

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

115
let print_id_real info fmt id =
116 117 118 119
  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
120 121 122 123 124

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
    | _ -> 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 "(@,"
165 166 167 168
let print_paren_l fmt x =
  print_list_delim ~start:lparen_l ~stop:rparen ~sep:comma fmt x
let print_paren_r fmt x =
  print_list_delim ~start:lparen_r ~stop:rparen ~sep:comma fmt x
MARCHE Claude's avatar
MARCHE Claude committed
169

MARCHE Claude's avatar
MARCHE Claude committed
170 171 172 173
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

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

191 192
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
193

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

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

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

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

207 208 209 210 211 212
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
213

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

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

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

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

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

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

343 344
let print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
MARCHE Claude's avatar
MARCHE Claude committed
345 346 347

(** Declarations *)

348
let print_constr info ts fmt (cs,_) =
349 350 351 352 353 354 355 356
  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
357

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

372 373 374 375 376 377
(*

  copy of old user scripts

*)

378
type content_type =
379
  Notation | (*Gallina |*) Vernacular
MARCHE Claude's avatar
MARCHE Claude committed
380

381 382 383 384
type statement =
  | Axiom of string (* name *)
  | Query of string * content_type * string (* name and content *)
  | Other of string (* content *)
MARCHE Claude's avatar
MARCHE Claude committed
385

386 387 388 389 390
exception StringValue of string

let read_generated_name =
  let def = Str.regexp "\\(Definition\\|Fixpoint\\|Inductive\\)[ ]+\\([^ :(.]+\\)" in
  fun ch ->
MARCHE Claude's avatar
MARCHE Claude committed
391 392 393
  try
    while true do
      let s = input_line ch in
394 395 396 397 398 399 400
      if Str.string_match def s 0 then
        raise (StringValue (Str.matched_group 2 s))
    done;
    assert false
  with StringValue name -> name

let read_old_proof =
401
  let def = Str.regexp "\\(Definition\\|Notation\\|Lemma\\|Theorem\\)[ ]+\\([^ :(.]+\\)" in
402 403 404 405
  let def_end = Str.regexp ".*[.]$" in
  let qed = Str.regexp "\\(Qed\\|Defined\\|Save\\|Admitted\\)[.]" in
  fun ch ->
  try
406
    let start = ref (pos_in ch) in
407 408
    let s = input_line ch in
    if not (Str.string_match def s 0) then raise (StringValue s);
409
    let kind = Str.matched_group 1 s in
410 411 412
    let name = Str.matched_group 2 s in
    if not (Str.string_match def_end s (Str.match_end ())) then
      while not (Str.string_match def_end (input_line ch) 0) do () done;
413 414 415 416 417 418 419 420
    let k =
      if kind = "Notation" then Notation
      else begin
        start := pos_in ch;
        while not (Str.string_match qed (input_line ch) 0) do () done;
        Vernacular
      end in
    let len = pos_in ch - !start in
421
    let s = String.create len in
422
    seek_in ch !start;
423
    really_input ch s 0 len;
424
    Query (name, k, s)
425 426
  with StringValue s -> Other s

427
(* Load old-style proofs where users were confined to a few sections. *)
428
let read_deprecated_script ch in_context =
429
  let sc = ref [] in
430
  let context = ref in_context in
431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447
  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

448 449 450 451
let read_old_script =
  let axm = Str.regexp "\\(Axiom\\|Parameter\\)[ ]+\\([^ :(.]+\\)" in
  fun ch ->
  let skip_to_empty = ref true in
452
  let last_empty_line = ref 0 in
453
  let sc = ref [] in
454 455 456
  try
    while true do
      let s = input_line ch in
457
      if s = "" then last_empty_line := pos_in ch;
458 459 460 461 462 463 464 465
      if !skip_to_empty then (if s = "" then skip_to_empty := false) else
      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
      if s = "(* Why3 goal *)" then sc := read_old_proof ch :: !sc else
466
      if s = "(* YOU MAY EDIT THE CONTEXT BELOW *)" then
467 468 469 470 471
        (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
472 473 474
      sc := Other s :: !sc
    done;
    assert false
475
  with
476 477 478 479 480 481 482 483 484 485 486 487
  | 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
488 489 490 491 492
      | h :: l when h == i ->
        let l = match l with
          | Other "" :: l -> l
          | _ -> l in
        script := List.rev_append acc l
493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521
      | 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
    | 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

let rec output_remaining fmt ?(in_other=false) script =
  match script with
  | Axiom _ :: t -> output_remaining fmt t
  | Query (n,_,c) :: t ->
    if in_other then fprintf fmt "*)@\n";
    fprintf fmt "(* Unused content named %s@\n%s *)@\n" n c;
    output_remaining fmt t
  | Other c :: t ->
    if not in_other then fprintf fmt "(* ";
    fprintf fmt "%s@\n" c;
    output_remaining fmt ~in_other:true t
  | [] ->
    if in_other then fprintf fmt "*)@\n"

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

523 524 525 526 527 528
let print_previous_proof def fmt previous =
  match previous with
  | None | Some (Axiom _) ->
    print_empty_proof fmt def
  | Some (Query (_,Vernacular,c)) ->
    fprintf fmt "%s" c
529
  | Some (Query (_,Notation,_))
530 531
  | Some (Other _) ->
    assert false
MARCHE Claude's avatar
MARCHE Claude committed
532

533
let print_type_decl ~old info fmt (ts,def) =
MARCHE Claude's avatar
MARCHE Claude committed
534
  if is_ts_tuple ts then () else
535 536
  let name = id_unique iprinter ts.ts_name in
  let prev = output_till_statement fmt old name in
MARCHE Claude's avatar
MARCHE Claude committed
537
  match def with
538 539 540 541
  | Tabstract ->
    begin match ts.ts_def with
    | None ->
      if info.realization then
542 543 544 545
        match prev with
        | Some (Query (_,Notation,c)) ->
          fprintf fmt "(* Why3 goal *)@\n%s@\n" c
        | _ ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
546
          fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Definition %s : %aType.@]@\n%a@\n"
547 548
            name print_params_list ts.ts_args
            (print_previous_proof true) prev
549 550 551 552 553 554 555 556 557 558 559 560 561
      else
        fprintf fmt "@[<hov 2>Parameter %s : %aType.@]@\n@\n"
          name print_params_list ts.ts_args
    | Some ty ->
      fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Definition %s %a :=@ %a.@]@\n@\n"
        name (print_list space print_tv_binder) ts.ts_args
        (print_ty info) ty
    end
  | Talgebraic csl ->
    fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Inductive %s %a :=@\n@[<hov>%a@].@]@\n"
      name (print_list space print_tv_binder) ts.ts_args
      (print_list newline (print_constr info ts)) csl;
    List.iter
562
      (fun (cs,_) ->
563 564 565 566
        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
567

568
let print_type_decl ~old info fmt d =
569
  if not (Mid.mem (fst d).ts_name info.info_syn) then
570
    (print_type_decl ~old info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
571

572
let print_ls_type ?(arrow=false) info fmt ls =
MARCHE Claude's avatar
MARCHE Claude committed
573 574
  if arrow then fprintf fmt " ->@ ";
  match ls with
MARCHE Claude's avatar
MARCHE Claude committed
575
  | None -> fprintf fmt "Prop"
576
  | Some ty -> print_ty info fmt ty
MARCHE Claude's avatar
MARCHE Claude committed
577

578
let print_logic_decl ~old info fmt (ls,ld) =
MARCHE Claude's avatar
MARCHE Claude committed
579
  let ty_vars_args, ty_vars_value, all_ty_params = ls_ty_vars ls in
580 581 582
  let name = id_unique iprinter ls.ls_name in
  let prev = output_till_statement fmt old name in
  begin match ld with
MARCHE Claude's avatar
MARCHE Claude committed
583 584
      | Some ld ->
          let vl,e = open_ls_defn ld in
585
          fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Definition %a%a%a: %a :=@ %a.@]@\n"
586
            print_ls ls
MARCHE Claude's avatar
MARCHE Claude committed
587
            print_ne_params all_ty_params
MARCHE Claude's avatar
MARCHE Claude committed
588 589 590 591
            (print_space_list (print_vsty info)) vl
            (print_ls_type info) ls.ls_value
            (print_expr info) e;
          List.iter forget_var vl
592 593
  | None ->
    if info.realization then
594 595 596 597 598 599 600 601 602
      match prev with
      | Some (Query (_,Notation,c)) ->
        fprintf fmt "(* Why3 goal *)@\n%s" c
      | _ ->
        fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Definition %s: %a%a%a.@]@\n%a"
          name print_params all_ty_params
          (print_arrow_list (print_ty info)) ls.ls_args
          (print_ls_type ~arrow:(ls.ls_args <> []) info) ls.ls_value
          (print_previous_proof true) prev
603 604 605 606 607
    else
      fprintf fmt "@[<hov 2>Parameter %s: %a%a%a.@]@\n"
        name print_params all_ty_params
        (print_arrow_list (print_ty info)) ls.ls_args
        (print_ls_type ~arrow:(ls.ls_args <> []) info) ls.ls_value
MARCHE Claude's avatar
MARCHE Claude committed
608
  end;
MARCHE Claude's avatar
MARCHE Claude committed
609
  print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params;
MARCHE Claude's avatar
MARCHE Claude committed
610
  fprintf fmt "@\n"
611

612
let print_logic_decl ~old info fmt d =
613
  if not (Mid.mem (fst d).ls_name info.info_syn) then
614
    (print_logic_decl ~old info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
615

616 617 618 619 620 621 622
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
623
        fprintf fmt "%a%a%a {struct %a}: %a :=@ %a@]"
624 625 626 627 628 629 630 631 632 633 634 635 636
          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
637
  fprintf fmt "(* Why3 assumption *)@\nSet Implicit Arguments.@\n";
638 639 640 641 642 643
  print_list_delim
    ~start:(fun fmt () -> fprintf fmt "@[<hov 2>Fixpoint ")
    ~stop:(fun fmt () -> fprintf fmt ".@\n")
    ~sep:(fun fmt () -> fprintf fmt "@\n@[<hov 2>with ")
    (fun fmt d -> print_recursive_decl info tm fmt d; forget_tvs ())
    fmt dl;
644 645
  fprintf fmt "Unset Implicit Arguments.@\n@\n"

646 647
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
648

649
let print_ind_decl info fmt (ps,bl) =
650
  let ty_vars_args, ty_vars_value, all_ty_params = ls_ty_vars ps in
651
  fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Inductive %a%a : %a -> Prop :=@ @[<hov>%a@].@]@\n"
652 653 654 655 656
     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
657

658
let print_ind_decl info fmt d =
659
  if not (Mid.mem (fst d).ls_name info.info_syn) then
660
    (print_ind_decl info fmt d; forget_tvs ())
MARCHE Claude's avatar
MARCHE Claude committed
661

662 663 664 665 666 667 668 669 670 671 672
let print_prop_decl ~old info fmt (k,pr,f) =
  let params = t_ty_freevars Stv.empty f in
  let name = id_unique iprinter pr.pr_name in
  let prev = output_till_statement fmt old name in
  let stt = match k with
    | Paxiom when info.realization -> "Lemma"
    | Paxiom -> ""
    | Plemma -> "Lemma"
    | Pgoal -> "Theorem"
    | Pskip -> assert false (* impossible *) in
  if stt <> "" then
673
    fprintf fmt "(* Why3 goal *)@\n@[<hov 2>%s %s : %a%a.@]@\n%a@\n"
674 675 676 677 678 679 680 681
      stt name print_params params
      (print_fmla info) f
      (print_previous_proof false) prev
  else
    fprintf fmt "@[<hov 2>Axiom %s : %a%a.@]@\n@\n"
      name print_params params
      (print_fmla info) f;
  forget_tvs ()
682

683
let print_decl ~old info fmt d = match d.d_node with
684 685 686 687 688 689 690 691
  | 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
692
  | Dprop (_,pr,_) when Mid.mem pr.pr_name info.info_syn ->
693
      ()
694 695
  | Dprop pr ->
      print_prop_decl ~old info fmt pr
MARCHE Claude's avatar
MARCHE Claude committed
696

697
let print_decls ~old info fmt dl =
698
  fprintf fmt "@\n@[<hov>%a@\n@]" (print_list nothing (print_decl ~old info)) dl
MARCHE Claude's avatar
MARCHE Claude committed
699

700
let print_task env pr thpr realize ?old fmt task =
701
  forget_all ();
702 703
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738
  (* find theories that are both used and realized from metas *)
  let realized_theories =
    Task.on_meta meta_realized (fun mid args ->
      match args with
      | [Theory.MAstr s1; Theory.MAstr s2] ->
        (* TODO: do not split string; in fact, do not even use a string argument *)
        let f,id = let l = split_string_rev s1 '.' in List.rev (List.tl l),List.hd l in
        let th = Env.find_theory env f id in
        Mid.add th.Theory.th_name (th, if s2 = "" then s1 else s2) mid
      | _ -> assert false
    ) Mid.empty task in
  (* 2 cases: goal is clone T with [] or goal is a real goal *)
  let realized_theories =
    match task with
    | None -> assert false
    | Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
      Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
      Mid.remove th.Theory.th_name realized_theories
    | _ -> realized_theories in
  let realized_theories' =
    Mid.map (fun (th,s) -> fprintf fmt "Require %s.@\n" s; th) realized_theories in
  let realized_symbols = Task.used_symbols realized_theories' in
  let local_decls = Task.local_decls task realized_symbols in
  (* 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
Andrei Paskevich's avatar
Andrei Paskevich committed
739 740
  let info = {
    info_syn = get_syntax_map task;
741 742
    symbol_printers = symbol_printers;
    realization = realize;
743 744
  }
  in
745 746 747 748 749
  let old = ref (match old with
    | None -> []
    | Some ch -> read_old_script ch) in
  print_decls ~old info fmt local_decls;
  output_remaining fmt !old
MARCHE Claude's avatar
MARCHE Claude committed
750

751 752
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
753

754 755
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
756

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

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

open Theory

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
795
*)
MARCHE Claude's avatar
MARCHE Claude committed
796

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