coq.ml 36.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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

MARCHE Claude's avatar
MARCHE Claude committed
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
let fresh_printer () =
MARCHE Claude's avatar
MARCHE Claude committed
39
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
40
  create_ident_printer black_list ~sanitizer:isanitize
41

42
43
let iprinter = fresh_printer ()

44
let forget_all () = forget_all iprinter
MARCHE Claude's avatar
MARCHE Claude committed
45
46
47

let tv_set = ref Sid.empty

48
49
50
51
52
53
54
55
56
(* 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
57
(* type variables *)
MARCHE Claude's avatar
MARCHE Claude committed
58

59
let print_tv info ~whytypes fmt tv =
MARCHE Claude's avatar
MARCHE Claude committed
60
  let n = id_unique iprinter tv.tv_name in
61
  fprintf fmt "%s" n;
62
  if whytypes && not info.ssreflect then fprintf fmt " %s_WT" n
MARCHE Claude's avatar
MARCHE Claude committed
63

64
let print_tv_binder info ~whytypes ~implicit fmt tv =
MARCHE Claude's avatar
MARCHE Claude committed
65
66
  tv_set := Sid.add tv.tv_name !tv_set;
  let n = id_unique iprinter tv.tv_name in
67
68
69
70
71
72
  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
73

74
75
let print_tv_binders info ~whytypes ~implicit fmt stv =
  Stv.iter (fprintf fmt "@ %a" (print_tv_binder info ~whytypes ~implicit)) stv
76

77
78
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
79

80
let print_params info ~whytypes fmt stv =
MARCHE Claude's avatar
MARCHE Claude committed
81
  if Stv.is_empty stv then () else
82
83
    fprintf fmt "forall%a,@ "
      (print_tv_binders info ~whytypes ~implicit:true) stv
84

85
let print_params_list info ~whytypes fmt ltv =
MARCHE Claude's avatar
MARCHE Claude committed
86
  match ltv with
87
  | [] -> ()
88
89
90
  | _ ->
    fprintf fmt "forall%a,@ "
      (print_tv_binders_list info ~whytypes ~implicit:false) ltv
MARCHE Claude's avatar
MARCHE Claude committed
91

MARCHE Claude's avatar
MARCHE Claude committed
92
93
94
95
96
97
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
98
  let n = id_unique iprinter vs.vs_name in
MARCHE Claude's avatar
MARCHE Claude committed
99
100
101
102
103
  fprintf fmt "%s" n

let forget_var vs = forget_id iprinter vs.vs_name

let print_ts fmt ts =
104
  fprintf fmt "%s" (id_unique iprinter ts.ts_name)
MARCHE Claude's avatar
MARCHE Claude committed
105
106

let print_ls fmt ls =
107
  fprintf fmt "%s" (id_unique iprinter ls.ls_name)
MARCHE Claude's avatar
MARCHE Claude committed
108
109

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

112
113
114
115
116
117
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)


118
(* unused printing function
119
let print_path = print_list (constant_string ".") string
120
*)
121
122
123

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

124
let print_id_real info fmt id =
125
126
127
128
  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
129

130
let print_ls_real info fmt ls =
131
  print_id_real info fmt ls.ls_name
132

133
let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name
134
(* unused printing function
135
let print_pr_real info fmt pr = print_id_real info fmt pr.pr_name
136
*)
137

MARCHE Claude's avatar
MARCHE Claude committed
138
139
(** Types *)

140
let print_ts_tv info fmt ts =
141
142
143
  match ts.ts_args with
  | [] -> fprintf fmt "%a" print_ts ts
  | _ -> fprintf fmt "(%a %a)" print_ts ts
144
    (print_list space (print_tv info ~whytypes:false)) ts.ts_args
145

146
let rec print_ty info fmt ty =
MARCHE Claude's avatar
MARCHE Claude committed
147
  begin match ty.ty_node with
148
  | Tyvar v -> print_tv info ~whytypes:false fmt v
MARCHE Claude's avatar
MARCHE Claude committed
149
  | Tyapp (ts, tl) when is_ts_tuple ts ->
150
      begin
MARCHE Claude's avatar
MARCHE Claude committed
151
152
153
        match tl with
          | []  -> fprintf fmt "unit"
          | [ty] -> print_ty info fmt ty
MARCHE Claude's avatar
MARCHE Claude committed
154
          | _   -> fprintf fmt "(%a)%%type" (print_list star (print_ty info)) tl
155
      end
156
157
  | Tyapp (ts, [l;r]) when ts_equal ts ts_func ->
      fprintf fmt "(%a ->@ %a)" (print_ty info) l (print_ty info) r
158
  | Tyapp (ts, tl) ->
MARCHE Claude's avatar
MARCHE Claude committed
159
160
161
162
163
164
    begin match query_syntax info.info_syn ts.ts_name with
      | Some s -> syntax_arguments s (print_ty info) fmt tl
      | None ->
        begin
          match tl with
            | []  -> (print_ts_real info) fmt ts
165
166
            | l   -> fprintf fmt "(%a@ %a)" (print_ts_real info) ts
              (print_list space (print_ty info)) l
MARCHE Claude's avatar
MARCHE Claude committed
167
168
        end
    end
169
  end
MARCHE Claude's avatar
MARCHE Claude committed
170
171
172
173

(* 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
174
    | Tyvar u when tv_equal u v -> true
MARCHE Claude's avatar
MARCHE Claude committed
175
176
177
178
179
180
181
    | _ -> 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
182
  inspect (Opt.get fs.ls_value)
MARCHE Claude's avatar
MARCHE Claude committed
183
184
185

(** Patterns, terms, and formulas *)

186
(* unused
MARCHE Claude's avatar
MARCHE Claude committed
187
let lparen_l fmt () = fprintf fmt "@ ("
188
*)
MARCHE Claude's avatar
MARCHE Claude committed
189
let lparen_r fmt () = fprintf fmt "(@,"
190
(* unused
191
192
let print_paren_l fmt x =
  print_list_delim ~start:lparen_l ~stop:rparen ~sep:comma fmt x
193
*)
194
195
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
196

197
let arrow fmt () = fprintf fmt " ->@ "
198
let print_arrow_list fmt x = print_list_suf arrow fmt x
MARCHE Claude's avatar
MARCHE Claude committed
199

200
let rec print_pat info fmt p = match p.pat_node with
MARCHE Claude's avatar
MARCHE Claude committed
201
202
  | Pwild -> fprintf fmt "_"
  | Pvar v -> print_vs fmt v
Andrei Paskevich's avatar
Andrei Paskevich committed
203
204
205
206
  | 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
207
  | Papp (cs,pl) when is_fs_tuple cs ->
MARCHE Claude's avatar
MARCHE Claude committed
208
      fprintf fmt "%a" (print_paren_r (print_pat info)) pl
209
  | Papp (cs,pl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
210
211
      begin match query_syntax info.info_syn cs.ls_name with
        | Some s -> syntax_arguments s (print_pat info) fmt pl
212
        | _ when pl = [] -> (print_ls_real info) fmt cs
213
        | _ -> fprintf fmt "(%a %a)"
214
          (print_ls_real info) cs (print_list space (print_pat info)) pl
Andrei Paskevich's avatar
Andrei Paskevich committed
215
      end
MARCHE Claude's avatar
MARCHE Claude committed
216

217
218
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
219

220
221
let print_vsty info fmt v =
  fprintf fmt "(%a)" (print_vsty_nopar info) v
MARCHE Claude's avatar
MARCHE Claude committed
222
223

let print_binop fmt = function
224
225
226
227
  | Tand -> fprintf fmt "/\\"
  | Tor -> fprintf fmt "\\/"
  | Timplies -> fprintf fmt "->"
  | Tiff -> fprintf fmt "<->"
MARCHE Claude's avatar
MARCHE Claude committed
228

229
(* unused
MARCHE Claude's avatar
MARCHE Claude committed
230
let print_label fmt (l,_) = fprintf fmt "(*%s*)" l
231
*)
MARCHE Claude's avatar
MARCHE Claude committed
232
233
234

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

235
236
237
238
239
240
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
241

242
and print_lrterm opl opr info fmt t = match t.t_label with
243
244
  | _ -> print_tnode opl opr info fmt t
(*
245
  | [] -> print_tnode opl opr info fmt t
MARCHE Claude's avatar
MARCHE Claude committed
246
  | ll -> fprintf fmt "(%a %a)"
247
      (print_list space print_label) ll (print_tnode false false info) t
248
*)
MARCHE Claude's avatar
MARCHE Claude committed
249

250
and print_lrfmla opl opr info fmt f = match f.t_label with
251
252
  | _ -> print_fnode opl opr info fmt f
(*
253
  | [] -> print_fnode opl opr info fmt f
MARCHE Claude's avatar
MARCHE Claude committed
254
  | ll -> fprintf fmt "(%a %a)"
255
      (print_list space print_label) ll (print_fnode false false info) f
256
*)
MARCHE Claude's avatar
MARCHE Claude committed
257

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
258
and print_tnode _opl opr info fmt t = match t.t_node with
MARCHE Claude's avatar
MARCHE Claude committed
259
260
  | Tvar v ->
      print_vs fmt v
261
262
  | Tconst c ->
      let number_format = {
263
          Number.long_int_support = true;
264
          Number.extra_leading_zeros_support = true;
265
          Number.negative_int_support = Number.Number_custom "(-%a)%%Z";
266
267
268
          Number.dec_int_support =
            if info.ssreflect then Number.Number_custom "%s%%:Z"
            else Number.Number_custom "%s%%Z";
269
270
271
272
          Number.hex_int_support = Number.Number_unsupported;
          Number.oct_int_support = Number.Number_unsupported;
          Number.bin_int_support = Number.Number_unsupported;
          Number.def_int_support = Number.Number_unsupported;
273
          Number.negative_real_support = Number.Number_custom "(-%a)%%R";
274
275
276
277
278
          Number.dec_real_support = Number.Number_unsupported;
          Number.hex_real_support = Number.Number_unsupported;
          Number.frac_real_support = Number.Number_custom
            (Number.PrintFracReal ("%s%%R", "(%s * %s)%%R", "(%s / %s)%%R"));
          Number.def_real_support = Number.Number_unsupported;
279
        } in
280
      Number.print number_format fmt c
281
282
  | Tif (f,t1,t2) ->
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
283
        (print_fmla info) f (print_term info) t1 (print_opl_term info) t2
MARCHE Claude's avatar
MARCHE Claude committed
284
285
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
MARCHE Claude's avatar
MARCHE Claude committed
286
      fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
287
        print_vs v (print_term info) t1 (print_opl_term info) t2;
MARCHE Claude's avatar
MARCHE Claude committed
288
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
289
  | Tcase (t,bl) ->
MARCHE Claude's avatar
MARCHE Claude committed
290
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
291
        (print_term info) t
292
        (print_list newline (print_tbranch info)) bl
MARCHE Claude's avatar
MARCHE Claude committed
293
  | Teps fb ->
294
295
296
297
298
299
300
301
302
303
304
305
306
307
      let vl,_,t0 = t_open_lambda t in
      if vl = [] then begin
        let v,f = t_open_bound fb in
        fprintf fmt (protect_on opr "epsilon %a.@ %a")
          (print_vsty info) v (print_opl_fmla info) f;
        forget_var v
      end else begin
        if t0.t_ty = None then unsupportedTerm t
          "Coq: Prop-typed lambdas are not supported";
        fprintf fmt (protect_on opr "fun %a =>@ %a")
          (print_list space (print_vsty info)) vl
          (print_opl_term info) t0;
        List.iter forget_var vl
      end
MARCHE Claude's avatar
MARCHE Claude committed
308
  | Tapp (fs,[]) when is_fs_tuple fs ->
309
      fprintf fmt "tt"
310
  | Tapp (fs,pl) when is_fs_tuple fs ->
MARCHE Claude's avatar
MARCHE Claude committed
311
      fprintf fmt "%a" (print_paren_r (print_term info)) pl
312
313
  | Tapp (fs,[l;r]) when ls_equal fs fs_func_app ->
      fprintf fmt "(%a@ %a)" (print_opr_term info) l (print_opr_term info) r
MARCHE Claude's avatar
MARCHE Claude committed
314
  | Tapp (fs, tl) ->
315
    begin match query_syntax info.info_syn fs.ls_name with
316
      | Some s ->
317
          syntax_arguments s (print_opr_term info) fmt tl
MARCHE Claude's avatar
MARCHE Claude committed
318
      | _ -> if unambig_fs fs
319
          then
320
321
            if tl = [] then fprintf fmt "%a" (print_ls_real info) fs
            else fprintf fmt "(%a %a)" (print_ls_real info) fs
322
              (print_list space (print_opr_term info)) tl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
323
          else fprintf fmt "(%a %a: %a)"
324
325
            (print_ls_real info) fs (print_list space (print_opr_term info)) tl
            (print_ty info) (t_type t)
MARCHE Claude's avatar
MARCHE Claude committed
326
    end
327
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
MARCHE Claude's avatar
MARCHE Claude committed
328

329
and print_fnode opl opr info fmt f = match f.t_node with
330
331
  | Tquant (Tforall,fq) ->
      let vl,_tl,f = t_open_quant fq in
332
      fprintf fmt (protect_on opr "forall %a,@ %a")
333
        (print_list space (print_vsty info)) vl
334
335
        (* (print_tl info) tl *) (print_fmla info) f;
      List.iter forget_var vl
336
337
  | Tquant (Texists,fq) ->
      let vl,_tl,f = t_open_quant fq in
MARCHE Claude's avatar
MARCHE Claude committed
338
      let rec aux fmt vl =
339
340
341
        match vl with
          | [] -> print_fmla info fmt f
          | v::vr ->
342
              fprintf fmt (protect_on opr "exists %a,@ %a")
MARCHE Claude's avatar
MARCHE Claude committed
343
344
                (print_vsty_nopar info) v
                aux vr
345
      in
MARCHE Claude's avatar
MARCHE Claude committed
346
      aux fmt vl;
MARCHE Claude's avatar
MARCHE Claude committed
347
      List.iter forget_var vl
348
  | Ttrue ->
MARCHE Claude's avatar
MARCHE Claude committed
349
      fprintf fmt "True"
350
  | Tfalse ->
MARCHE Claude's avatar
MARCHE Claude committed
351
      fprintf fmt "False"
352
  | Tbinop (b,f1,f2) ->
MARCHE Claude's avatar
MARCHE Claude committed
353
      fprintf fmt (protect_on (opl || opr) "%a %a@ %a")
354
        (print_opr_fmla info) f1 print_binop b (print_opl_fmla info) f2
355
  | Tnot f ->
356
      fprintf fmt (protect_on opr "~ %a") (print_opl_fmla info) f
357
  | Tlet (t,f) ->
358
      let v,f = t_open_bound f in
MARCHE Claude's avatar
MARCHE Claude committed
359
      fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
360
        print_vs v (print_term info) t (print_opl_fmla info) f;
MARCHE Claude's avatar
MARCHE Claude committed
361
      forget_var v
362
  | Tcase (t,bl) ->
MARCHE Claude's avatar
MARCHE Claude committed
363
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
364
        (print_term info) t
365
        (print_list newline (print_fbranch info)) bl
366
  | Tif (f1,f2,f3) ->
MARCHE Claude's avatar
MARCHE Claude committed
367
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
368
        (print_fmla info) f1 (print_fmla info) f2 (print_opl_fmla info) f3
369
  | Tapp (ps, tl) ->
370
    begin match query_syntax info.info_syn ps.ls_name with
371
      | Some s -> syntax_arguments s (print_opr_term info) fmt tl
372
      | _ -> fprintf fmt "(%a%a)" (print_ls_real info) ps
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
373
          (print_list_pre space (print_opr_term info)) tl
MARCHE Claude's avatar
MARCHE Claude committed
374
    end
375
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
MARCHE Claude's avatar
MARCHE Claude committed
376

377
and print_tbranch info fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
378
  let p,t = t_open_branch br in
MARCHE Claude's avatar
MARCHE Claude committed
379
  fprintf fmt "@[<hov 4>| %a =>@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
380
381
    (print_pat info) p (print_term info) t;
  Svs.iter forget_var p.pat_vars
MARCHE Claude's avatar
MARCHE Claude committed
382

383
and print_fbranch info fmt br =
384
  let p,f = t_open_branch br in
MARCHE Claude's avatar
MARCHE Claude committed
385
  fprintf fmt "@[<hov 4>| %a =>@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
386
387
    (print_pat info) p (print_fmla info) f;
  Svs.iter forget_var p.pat_vars
MARCHE Claude's avatar
MARCHE Claude committed
388

389
390
let print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
MARCHE Claude's avatar
MARCHE Claude committed
391
392
393

(** Declarations *)

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

400
401
402
403
404
405
(*

  copy of old user scripts

*)

406
type content_type =
407
  Notation | (*Gallina |*) Vernacular
MARCHE Claude's avatar
MARCHE Claude committed
408

409
type statement =
410
  | Info  of string  (* name *)
411
412
413
  | Axiom of string (* name *)
  | Query of string * content_type * string (* name and content *)
  | Other of string (* content *)
MARCHE Claude's avatar
MARCHE Claude committed
414

415
416
417
exception StringValue of string

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

429
430
431
432
433
434
(** no nested comment *)
let read_comment =
  let start_comment = Str.regexp "(\\*[ ]+\\([^ :]+\\)" in
  let end_comment = Str.regexp ".*\\*)" in
  fun ch ->
    let line = ref "" in
435
    (* look for "( * name" *)
436
437
438
439
440
441
442
443
444
445
446
    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
447
    (* look for end of comment *)
448
449
450
451
452
    while not (Str.string_match end_comment (!line) 0) do
      line := input_line ch
    done;
    name

453
454
455
456
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

Julien Thierry's avatar
Julien Thierry committed
457
458
459
460
461
462
let read_until_or_eof re s i ch =
  try
    read_until re s i ch
  with
  | End_of_file -> ()

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

500
(* Load old-style proofs where users were confined to a few sections. *)
501
let read_deprecated_script ch in_context =
502
  let sc = ref [] in
503
  let context = ref in_context in
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
  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

521
522
let read_old_script =
  let axm = Str.regexp "\\(Axiom\\|Parameter\\)[ ]+\\([^ :(.]+\\)" in
523
  let prelude = Str.regexp "(\\* This file is generated by Why3.*\\*)" in
524
  fun ch ->
525
  let skip_to_empty = ref false in
526
  let last_empty_line = ref 0 in
527
  let sc = ref [] in
528
529
530
  try
    while true do
      let s = input_line ch in
531
      if s = "" then last_empty_line := pos_in ch;
532
      if !skip_to_empty then (if s = "" then skip_to_empty := false) else
533
534
535
      if s = "(* Why3 comment *)" then
        (let name = read_comment ch in sc := Info name :: !sc;
         skip_to_empty := true) else
536
537
538
539
540
541
      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
542
543
      if s = "(* Why3 goal *)" then
        (sc := read_old_proof ch :: !sc; skip_to_empty := true) else
544
545
546
      if Str.string_match prelude s 0 then
        (sc := Info "Why3 prelude" :: !sc;
         skip_to_empty := true) else
547
      if s = "(* YOU MAY EDIT THE CONTEXT BELOW *)" then
548
549
550
551
552
        (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
553
554
555
      sc := Other s :: !sc
    done;
    assert false
556
  with
557
558
559
560
561
562
563
564
565
566
567
568
  | 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
569
570
571
572
573
      | h :: l when h == i ->
        let l = match l with
          | Other "" :: l -> l
          | _ -> l in
        script := List.rev_append acc l
574
575
576
577
578
      | 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
579
    | Info n as o :: _ when n = name -> print o; Some o
580
581
582
583
584
585
    | 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

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

592
593
594
let rec intros_hyp n fmt f =
  match f.t_node with
    | Tbinop(Tand,f1,f2) ->
595
      fprintf fmt "(";
596
      let (m,vsl1) = intros_hyp n fmt f1 in
597
      fprintf fmt ",";
598
      let (k,vsl2) = intros_hyp m fmt f2 in
599
      fprintf fmt ")";
600
      (k,vsl1@vsl2)
601
602
603
604
605
606
607
608
609
610
611
    | 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
612
      aux n vsl
613
    | _ ->
614
      fprintf fmt "h%d" n;
615
      (n+1,[])
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630

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) ->
631
      fprintf fmt "@ ";
632
633
634
      let m,vsl = intros_hyp n fmt f1 in
      do_intros m fmt f2;
      List.iter forget_var vsl
635
636
    | _ -> ()

637
638
639
640
let intros_params fmt params =
  Stv.iter
    (fun tv ->
      let n = id_unique iprinter tv.tv_name in
641
      fprintf fmt "@ %s %s_WT" n n)
642
643
    params

644
645
646
647
648
649
650
651
let need_intros params fmla =
  not (Stv.is_empty params) ||
  match fmla.t_node with
  | Tlet _
  | Tquant(Tforall,_)
  | Tbinop(Timplies, _, _) -> true
  | _ -> false

652
let intros fmt params fmla =
653
  fprintf fmt "@[intros%a%a.@]" intros_params params (do_intros 1) fmla
654

655
let print_empty_proof fmt def =
656
  match def with
657
    | Some (params,fmla) ->
658
      if need_intros params fmla then intros fmt params fmla;
659
      fprintf fmt "@\n@\n";
660
661
662
663
      fprintf fmt "Qed.@\n"
    | None ->
      fprintf fmt "@\n";
      fprintf fmt "Defined.@\n"
664

665
let print_previous_proof def info fmt previous =
666
  match previous with
667
  | None ->
668
669
    print_empty_proof fmt def
  | Some (Query (_,Vernacular,c)) ->
670
    begin match def with
671
672
    | Some (p, f) when not info.realization && need_intros p f ->
        fprintf fmt "@[(* Why3 %a *)@]@\n" (fun fmt f -> intros fmt p f) f
673
674
    | _ -> ()
    end;
675
    fprintf fmt "%s" c
676
  | Some (Query (_,Notation,_))
677
  | Some (Axiom _) | Some (Other _) | Some (Info _) ->
678
    assert false
MARCHE Claude's avatar
MARCHE Claude committed
679

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

716
let print_type_decl ~prev info fmt ts =
717
  if not (Mid.mem ts.ts_name info.info_syn) then
718
    (print_type_decl ~prev info fmt ts; forget_tvs ())
719

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

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

748
749
750
751
752
753
754
755
756
757
758
759
760
761
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";
762
      List.iter (print_data_whytype_and_implicits info fmt) d
763
    end
MARCHE Claude's avatar
MARCHE Claude committed
764

765
let print_ls_type info fmt = function
MARCHE Claude's avatar
MARCHE Claude committed
766
  | None -> fprintf fmt "Prop"
767
  | Some ty -> print_ty info fmt ty
MARCHE Claude's avatar
MARCHE Claude committed
768

769
let print_param_decl ~prev info fmt ls =
770
  let _, _, all_ty_params = ls_ty_vars ls in
771
  if info.realization then
772
    match prev with
773
774
775
776
    | Some (Query (_,Notation,c)) ->
      fprintf fmt "(* Why3 goal *)@\n%s@\n" c
    | Some (Axiom _) ->
      fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Variable %a: %a%a%a.@]@\n@\n"
777
        print_ls ls (print_params info ~whytypes:true) all_ty_params
778
        (print_arrow_list (print_ty info)) ls.ls_args
779
        (print_ls_type info) ls.ls_value
780
781
782
783
784
785
786
787
788
789
    | (* 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
        (print_expr info) e;
      List.iter forget_var vl
790
791
    | _ ->
      fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Definition %a: %a%a%a.@]@\n%a@\n"
792
        print_ls ls (print_params info ~whytypes:true) all_ty_params
793
        (print_arrow_list (print_ty info)) ls.ls_args
794
        (print_ls_type info) ls.ls_value
795
        (print_previous_proof None info) prev
796
797
  else
    fprintf fmt "@[<hov 2>Parameter %a: %a%a%a.@]@\n@\n"
798
      print_ls ls (print_params info ~whytypes:true) all_ty_params
799
      (print_arrow_list (print_ty info)) ls.ls_args
800
      (print_ls_type info) ls.ls_value
801

802
let print_param_decl ~prev info fmt ls =
803
  if info.realization || not (Mid.mem ls.ls_name info.info_syn) then
804
    (print_param_decl ~prev info fmt ls; forget_tvs ())
805
806

let print_logic_decl info fmt (ls,ld) =
807
  let _, _, all_ty_params = ls_ty_vars ls in
808
809
810
  let vl,e = open_ls_defn ld in
  fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Definition %a%a%a: %a :=@ %a.@]@\n"
    print_ls ls
811
    (print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
812
    (print_list_pre space (print_vsty info)) vl
813
814
815
816
817
    (print_ls_type info) ls.ls_value
    (print_expr info) e;
  List.iter forget_var vl;
  fprintf fmt "@\n"

818
819
820
821
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
822
    "(* Why3 goal *)@\n@[<hov 2>Lemma %s :@ %a%a.@]@\n"
823
    name
824
    (print_params info ~whytypes:true) all_ty_params
825
826
    (print_expr info) def_formula;
  fprintf fmt "%a@\n"
827
    (print_previous_proof (Some (all_ty_params,def_formula)) info) prev
828
829
830
831
832
833
834
835
836

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 =
837
838
839
  (* During realization the definition of a "builtin" symbol is
     printed and an equivalence lemma with associated coq function is
     requested *)
840
  if not (Mid.mem (fst d).ls_name info.info_syn) then
841
    (print_logic_decl info fmt d; forget_tvs ())
842
843
  else if info.realization then
    print_equivalence_lemma ~old info fmt d
MARCHE Claude's avatar
MARCHE Claude committed
844

845
let print_recursive_decl info fmt (ls,ld) =
846
  let _, _, all_ty_params = ls_ty_vars ls in
847
848
  let i = match Decl.ls_defn_decrease ld with
    | [i] -> i | _ -> assert false in
849
850
851
  let vl,e = open_ls_defn ld in
  fprintf fmt "%a%a%a {struct %a}: %a :=@ %a@]"
    print_ls ls
Jean-Christophe Filliâtre's avatar