MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

ocaml_printer.ml 21.4 KB
Newer Older
Mário Pereira's avatar
Mário Pereira committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

(** Printer for extracted OCaml code *)

open Compile
open Format
open Ident
open Pp
18
19
open Ity
open Term
20
21
open Expr
open Ty
22
23
24
open Theory
open Pmodule
open Stdlib
Mário Pereira's avatar
Mário Pereira committed
25
open Pdecl
Mario Pereira's avatar
Mario Pereira committed
26
open Printer
Mário Pereira's avatar
Mário Pereira committed
27

Mário Pereira's avatar
Mário Pereira committed
28
29
30
31
32
33
34
35
type info = {
  info_syn          : syntax_map;
  info_convert      : syntax_map;
  info_current_th   : Theory.theory;
  info_current_mo   : Pmodule.pmodule option;
  info_th_known_map : Decl.known_map;
  info_mo_known_map : Pdecl.known_map;
  info_fname        : string option;
36
  flat              : bool;
Mário Pereira's avatar
Mário Pereira committed
37
38
}

Mário Pereira's avatar
Mário Pereira committed
39
40
module Print = struct

41
42
  open Mltree
  open Compile.ML
Mário Pereira's avatar
Mário Pereira committed
43
44
45
46
47
48
49
50
51
52
53
54

  let ocaml_keywords =
    ["and"; "as"; "assert"; "asr"; "begin";
     "class"; "constraint"; "do"; "done"; "downto"; "else"; "end";
     "exception"; "external"; "false"; "for"; "fun"; "function";
     "functor"; "if"; "in"; "include"; "inherit"; "initializer";
     "land"; "lazy"; "let"; "lor"; "lsl"; "lsr"; "lxor"; "match";
     "method"; "mod"; "module"; "mutable"; "new"; "object"; "of";
     "open"; "or"; "private"; "rec"; "sig"; "struct"; "then"; "to";
     "true"; "try"; "type"; "val"; "virtual"; "when"; "while"; "with";
     "raise";]

55
56
57
58
59
  let is_ocaml_keyword =
    let h = Hstr.create 16 in
    List.iter (fun s -> Hstr.add h s ()) ocaml_keywords;
    Hstr.mem h

60
  (* FIXME? use different printers for record fields, types, etc. *)
Mário Pereira's avatar
Mário Pereira committed
61
  let iprinter, aprinter =
Mário Pereira's avatar
Mário Pereira committed
62
    let isanitize = sanitizer char_to_alpha char_to_alnumus in
Mário Pereira's avatar
Mário Pereira committed
63
64
65
    let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
    create_ident_printer ocaml_keywords ~sanitizer:isanitize,
    create_ident_printer ocaml_keywords ~sanitizer:lsanitize
Mário Pereira's avatar
Mário Pereira committed
66

Mário Pereira's avatar
Mário Pereira committed
67
  let forget_id id = forget_id iprinter id
Mário Pereira's avatar
Mário Pereira committed
68
  let _forget_ids = List.iter forget_id
Mário Pereira's avatar
Mário Pereira committed
69
70
71
  let forget_var (id, _, _) = forget_id id
  let forget_vars = List.iter forget_var

Mário Pereira's avatar
Mário Pereira committed
72
  let forget_let_defn = function
Mário Pereira's avatar
Mário Pereira committed
73
  | Lvar (v,_) -> forget_id v.pv_vs.vs_name
Mário Pereira's avatar
Mário Pereira committed
74
  | Lsym (s,_,_,_) -> forget_rs s
Mário Pereira's avatar
Mário Pereira committed
75
76
  | Lrec rdl -> List.iter (fun fd -> forget_rs fd.rec_sym) rdl

Mário Pereira's avatar
Mário Pereira committed
77
78
79
80
81
82
83
  let rec forget_pat = function
    | Pwild -> ()
    | Pident id -> forget_id id
    | Papp (_, pl) | Ptuple pl -> List.iter forget_pat pl
    | Por (p1, p2) -> forget_pat p1; forget_pat p2
    | Pas (p, _) -> forget_pat p

Mário Pereira's avatar
Mário Pereira committed
84
85
86
87
  let print_ident fmt id =
    let s = id_unique iprinter id in
    fprintf fmt "%s" s

88
89
  let is_local_id info id =
    Sid.mem id info.info_current_th.th_local ||
Mário Pereira's avatar
Mário Pereira committed
90
    Opt.fold (fun _ m -> Sid.mem id m.Pmodule.mod_local)
91
92
      false info.info_current_mo

93
  let print_qident ~sanitizer info fmt id =
Mário Pereira's avatar
Mário Pereira committed
94
    try
95
      if info.flat || is_local_id info id then raise Not_found;
Mário Pereira's avatar
Mário Pereira committed
96
      let lp, t, q =
97
98
99
100
101
        try Pmodule.restore_path id
        with Not_found -> Theory.restore_path id in
      let s = String.concat "__" q in
      let s = Ident.sanitizer char_to_alpha char_to_alnumus s in
      let s = sanitizer s in
102
      let s = if is_ocaml_keyword s then s ^ "_renamed" else s in (* FIXME *)
103
      let fname = if lp = [] then info.info_fname else None in
Mário Pereira's avatar
Mário Pereira committed
104
105
      let m = Strings.capitalize (module_name ?fname lp t) in
      fprintf fmt "%s.%s" m s
106
107
108
109
110
111
    with Not_found ->
      let s = id_unique ~sanitizer iprinter id in
      fprintf fmt "%s" s

  let print_lident = print_qident ~sanitizer:Strings.uncapitalize
  let print_uident = print_qident ~sanitizer:Strings.capitalize
Mário Pereira's avatar
Mário Pereira committed
112

Mário Pereira's avatar
Mário Pereira committed
113
114
  let print_tv fmt tv =
    fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
Mário Pereira's avatar
Mário Pereira committed
115

116
117
118
  let protect_on b s =
    if b then "(" ^^ s ^^ ")" else s

Mário Pereira's avatar
Mário Pereira committed
119
120
  let star fmt () = fprintf fmt " *@ "

Mário Pereira's avatar
Mário Pereira committed
121
122
  let rec print_list2 sep sep_m print1 print2 fmt (l1, l2) =
    match l1, l2 with
Mário Pereira's avatar
Mário Pereira committed
123
124
    | [x1], [x2] ->
      print1 fmt x1; sep_m fmt (); print2 fmt x2
Mário Pereira's avatar
Mário Pereira committed
125
126
127
128
129
    | x1 :: r1, x2 :: r2 ->
      print1 fmt x1; sep_m fmt (); print2 fmt x2; sep fmt ();
      print_list2 sep sep_m print1 print2 fmt (r1, r2)
    | _ -> ()

Mário Pereira's avatar
Mário Pereira committed
130
131
  let print_rs info fmt rs =
    fprintf fmt "%a" (print_lident info) rs.rs_name
Mário Pereira's avatar
Mário Pereira committed
132

133
134
  (** Types *)

Mario Pereira's avatar
Mario Pereira committed
135
  let rec print_ty ?(paren=false) info fmt = function
136
    | Tvar tv ->
Mário Pereira's avatar
Mário Pereira committed
137
      print_tv fmt tv
Mário Pereira's avatar
Mário Pereira committed
138
    | Ttuple [] ->
139
      fprintf fmt "unit"
Mário Pereira's avatar
Mário Pereira committed
140
    | Ttuple tl ->
141
      fprintf fmt (protect_on paren "@[%a@]")
142
        (print_list star (print_ty ~paren:true info)) tl
Mário Pereira's avatar
Mário Pereira committed
143
144
145
    | Tapp (ts, [t1; t2]) when id_equal ts ts_func.ts_name ->
      fprintf fmt (protect_on paren "@[%a ->@ %a@]")
        (print_ty ~paren:true info) t1 (print_ty info) t2
Mário Pereira's avatar
Mário Pereira committed
146
    | Tapp (ts, tl) ->
Mário Pereira's avatar
Mário Pereira committed
147
148
149
150
151
152
153
154
155
156
157
158
159
160
      match query_syntax info.info_syn ts with
      | Some s ->
        syntax_arguments s (print_ty ~paren:true info) fmt tl
      | None   ->
        match tl with
        | [] ->
          (print_lident info) fmt ts
        | [ty] ->
          fprintf fmt (protect_on paren "%a@ %a")
            (print_ty ~paren:true info) ty (print_lident info) ts
        | tl ->
          fprintf fmt (protect_on paren "(%a)@ %a")
            (print_list comma (print_ty ~paren:false info)) tl
            (print_lident info) ts
Mario Pereira's avatar
Mario Pereira committed
161

Mário Pereira's avatar
Mário Pereira committed
162
  let print_vsty_opt info fmt id ty =
163
    fprintf fmt "?%s:(%a:@ %a)" id.id_string (print_lident info) id
Mário Pereira's avatar
Mário Pereira committed
164
      (print_ty ~paren:false info) ty
Mário Pereira's avatar
Mário Pereira committed
165

Mário Pereira's avatar
Mário Pereira committed
166
  let print_vsty_named info fmt id ty =
167
    fprintf fmt "~%s:(%a:@ %a)" id.id_string (print_lident info) id
Mário Pereira's avatar
Mário Pereira committed
168
      (print_ty ~paren:false info) ty
Mário Pereira's avatar
Mário Pereira committed
169

Mário Pereira's avatar
Mário Pereira committed
170
171
172
173
174
  let print_vsty info fmt (id, ty, _) =
    let labels = id.id_label in
    if is_optional ~labels then print_vsty_opt info fmt id ty
    else if is_named ~labels then print_vsty_named info fmt id ty
    else fprintf fmt "(%a:@ %a)" (print_lident info) id
175
      (print_ty ~paren:false info) ty
176

Mário Pereira's avatar
Mário Pereira committed
177
178
  let print_tv_arg = print_tv
  let print_tv_args fmt = function
179
    | []   -> ()
Mário Pereira's avatar
Mário Pereira committed
180
181
    | [tv] -> fprintf fmt "%a@ " print_tv_arg tv
    | tvl  -> fprintf fmt "(%a)@ " (print_list comma print_tv_arg) tvl
Mário Pereira's avatar
Mário Pereira committed
182

Mario Pereira's avatar
Mario Pereira committed
183
  let print_vs_arg info fmt vs =
Mário Pereira's avatar
Mário Pereira committed
184
    fprintf fmt "@[%a@]" (print_vsty info) vs
Mário Pereira's avatar
Mário Pereira committed
185

Mário Pereira's avatar
Mário Pereira committed
186
187
188
189
190
191
192
193
194
195
196
197
198
  let print_path =
    print_list dot pp_print_string (* point-free *)

  let print_path_id fmt = function
    | [], id -> print_ident fmt id
    | p, id  -> fprintf fmt "%a.%a" print_path p print_ident id

  let print_theory_name fmt th =
    print_path_id fmt (th.th_path, th.th_name)

  let print_module_name fmt m =
    print_theory_name fmt m.mod_theory

Mário Pereira's avatar
Mário Pereira committed
199
200
201
  let get_record info rs =
    match Mid.find_opt rs.rs_name info.info_mo_known_map with
    | Some {pd_node = PDtype itdl} ->
202
203
      let eq_rs {itd_constructors=constr} = List.exists (rs_equal rs) constr in
      let itd = List.find eq_rs itdl in
Mário Pereira's avatar
Mário Pereira committed
204
205
206
207
      List.filter (fun e -> not (rs_ghost e)) itd.itd_fields
    | _ -> []

  let rec print_pat info fmt = function
208
209
210
    | Pwild ->
       fprintf fmt "_"
    | Pident id ->
Mário Pereira's avatar
Mário Pereira committed
211
       (print_lident info) fmt id
212
    | Pas (p, id) ->
Mário Pereira's avatar
Mário Pereira committed
213
       fprintf fmt "%a as %a" (print_pat info) p (print_lident info) id
214
    | Por (p1, p2) ->
Mário Pereira's avatar
Mário Pereira committed
215
       fprintf fmt "%a | %a" (print_pat info) p1 (print_pat info) p2
216
    | Ptuple pl ->
Mário Pereira's avatar
Mário Pereira committed
217
218
219
220
221
222
      fprintf fmt "(%a)" (print_list comma (print_pat info)) pl
    | Papp (ls, pl) ->
      match query_syntax info.info_syn ls.ls_name, pl with
      | Some s, _ ->
        syntax_arguments s (print_pat info) fmt pl
      | None, pl ->
Mário Pereira's avatar
Mário Pereira committed
223
224
225
226
        let pjl = let rs = restore_rs ls in get_record info rs in
        match pjl with
        | []  -> print_papp info ls fmt pl
        | pjl ->
Mário Pereira's avatar
Mário Pereira committed
227
          fprintf fmt "@[<hov 2>{ %a }@]"
Mário Pereira's avatar
Mário Pereira committed
228
            (print_list2 semi equal (print_rs info) (print_pat info)) (pjl, pl)
Mário Pereira's avatar
Mário Pereira committed
229
230
231
232
233
234
235

  and print_papp info ls fmt = function
    | []  -> fprintf fmt "%a"      (print_uident info) ls.ls_name
    | [p] -> fprintf fmt "%a %a"   (print_uident info) ls.ls_name
                                   (print_pat info) p
    | pl  -> fprintf fmt "%a (%a)" (print_uident info) ls.ls_name
                                   (print_list comma (print_pat info)) pl
236

237
238
  (** Expressions *)

239
240
  let pv_name pv = pv.pv_vs.vs_name

Mario Pereira's avatar
Mario Pereira committed
241
242
  let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)

243
244
245
246
247
248
249
250
  let is_true e = match e.e_node with
    | Eapp (s, []) -> rs_equal s rs_true
    | _ -> false

  let is_false e = match e.e_node with
    | Eapp (s, []) -> rs_equal s rs_false
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
251
  let rec print_apply_args info fmt = function
252
253
254
255
256
257
258
259
260
261
    | expr :: exprl, pv :: pvl ->
      if is_optional ~labels:(pv_name pv).id_label then
        fprintf fmt "?%s:%a" (pv_name pv).id_string
          (print_expr ~paren:true info) expr
      else if is_named ~labels:(pv_name pv).id_label then
        fprintf fmt "~%s:%a" (pv_name pv).id_string
          (print_expr ~paren:true info) expr
      else
        fprintf fmt "%a" (print_expr ~paren:true info) expr;
      if exprl <> [] then fprintf fmt "@ ";
Mário Pereira's avatar
Mário Pereira committed
262
      print_apply_args info fmt (exprl, pvl)
263
264
    | [], _ -> ()
    | _, [] -> assert false
Mário Pereira's avatar
Mário Pereira committed
265
266

  and print_apply ?(paren=false) info rs fmt pvl =
267
    let isfield =
268
      match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
269
      | None   -> false
270
271
272
273
274
275
276
      | Some _ -> true in
    let isconstructor () =
      match Mid.find_opt rs.rs_name info.info_mo_known_map with
      | Some {pd_node = PDtype its} ->
        let is_constructor its =
          List.exists (rs_equal rs) its.itd_constructors in
        List.exists is_constructor its
Mário Pereira's avatar
Mário Pereira committed
277
      | _ -> false in
Mário Pereira's avatar
Mário Pereira committed
278
279
    match query_syntax info.info_convert rs.rs_name,
          query_syntax info.info_syn rs.rs_name, pvl with
280
    | Some s, _, [{e_node = Econst _}] ->
Mário Pereira's avatar
Mário Pereira committed
281
282
      let print_constant fmt e = match e.e_node with
        | Econst c ->
283
284
285
          let s = BigInt.to_string (Number.compute_int_constant c) in
          if c.Number.ic_negative then fprintf fmt "(%s)" s
          else fprintf fmt "%s" s
286
        | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
287
      syntax_arguments s print_constant fmt pvl
Mário Pereira's avatar
Mário Pereira committed
288
    | _, Some s, _ ->
Mário Pereira's avatar
Mário Pereira committed
289
      syntax_arguments s (print_expr ~paren:true info) fmt pvl;
290
    | _, None, tl when is_rs_tuple rs ->
Mário Pereira's avatar
Mário Pereira committed
291
292
      fprintf fmt "@[(%a)@]"
        (print_list comma (print_expr info)) tl
293
    | _, None, [t1] when isfield ->
Mário Pereira's avatar
Mário Pereira committed
294
      fprintf fmt "%a.%a" (print_expr info) t1 (print_lident info) rs.rs_name
295
    | _, None, tl when isconstructor () ->
Mário Pereira's avatar
Mário Pereira committed
296
      let pjl = get_record info rs in
Mário Pereira's avatar
Mário Pereira committed
297
      begin match pjl, tl with
Mário Pereira's avatar
Mário Pereira committed
298
299
      | [], [] ->
        (print_uident info) fmt rs.rs_name
Mário Pereira's avatar
Mário Pereira committed
300
      | [], [t] ->
301
302
        fprintf fmt (protect_on paren "@[<hov 2>%a %a@]")
          (print_uident info) rs.rs_name (print_expr ~paren:true info) t
Mário Pereira's avatar
Mário Pereira committed
303
      | [], tl ->
304
305
        fprintf fmt (protect_on paren "@[<hov 2>%a (%a)@]") (print_uident info)
          rs.rs_name (print_list comma (print_expr info)) tl
Mário Pereira's avatar
Mário Pereira committed
306
      | pjl, tl ->
307
308
        let equal fmt () = fprintf fmt " = " in
        fprintf fmt "@[<hov 2>{ @[%a@] }@]"
Mário Pereira's avatar
Mário Pereira committed
309
          (print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl)
Mário Pereira's avatar
Mário Pereira committed
310
      end
311
    | _, None, [] ->
Mário Pereira's avatar
Mário Pereira committed
312
      (print_lident info) fmt rs.rs_name
313
    | _, None, tl ->
Mário Pereira's avatar
Mário Pereira committed
314
315
      fprintf fmt (protect_on paren "@[<hov 2>%a %a@]")
        (print_lident info) rs.rs_name
Mário Pereira's avatar
Mário Pereira committed
316
317
        (print_apply_args info) (tl, rs.rs_cty.cty_args)
        (* (print_list space (print_expr ~paren:true info)) tl *)
318

319
  and print_svar fmt s =
320
    Stv.iter (fun tv -> fprintf fmt "%a " print_tv tv) s
321
322

  and print_fun_type_args info fmt (args, s, res) =
323
324
    if Stv.is_empty s then
      fprintf fmt "@[%a@] :@ %a@ ="
325
326
327
328
329
        (print_list space (print_vs_arg info)) args
        (print_ty info) res
    else
      let ty_args = List.map (fun (_, ty, _) -> ty) args in
      let id_args = List.map (fun (id, _, _) -> id) args in
Mário Pereira's avatar
Mário Pereira committed
330
      fprintf fmt ": @[@[%a@]. @[%a ->@ %a@] =@ @[fun @[%a@]@ ->@]@]"
331
        print_svar s
332
333
        (print_list arrow (print_ty ~paren:true info)) ty_args
        (print_ty ~paren:true info) res
334
335
        (print_list space (print_lident info)) id_args

Mário Pereira's avatar
Mário Pereira committed
336
337
338
339
  and print_let_def info fmt = function
    | Lvar (pv, e) ->
      fprintf fmt "@[<hov 2>let %a =@ %a@]"
        (print_lident info) (pv_name pv) (print_expr info) e;
Mário Pereira's avatar
Mário Pereira committed
340
    | Lsym (rs, res, args, ef) ->
341
      fprintf fmt "@[<hov 2>let %a @[%a@] : %a@ =@ @[%a@]@]"
Mário Pereira's avatar
Mário Pereira committed
342
        (print_lident info) rs.rs_name
343
        (print_list space (print_vs_arg info)) args
Mário Pereira's avatar
Mário Pereira committed
344
        (print_ty info) res (print_expr info) ef;
Mário Pereira's avatar
Mário Pereira committed
345
      forget_vars args
346
    | Lrec rdef ->
Mário Pereira's avatar
Mário Pereira committed
347
      let print_one fst fmt = function
348
349
        | { rec_sym = rs1; rec_args = args; rec_exp = e;
            rec_res = res; rec_svar = s } ->
350
          fprintf fmt "@[<hov 2>%s %a @[%a@]@ %a@]"
Mário Pereira's avatar
Mário Pereira committed
351
352
            (if fst then "let rec" else "and")
            (print_lident info) rs1.rs_name
353
354
            (print_fun_type_args info) (args, s, res)
            (print_expr info) e;
355
          forget_vars args
Mário Pereira's avatar
Mário Pereira committed
356
357
358
359
360
      in
      List.iter (fun fd -> Hrs.replace ht_rs fd.rec_rsym fd.rec_sym) rdef;
      print_list_next newline print_one fmt rdef;
      List.iter (fun fd -> Hrs.remove ht_rs fd.rec_rsym) rdef

Mário Pereira's avatar
Mário Pereira committed
361
  and print_enode ?(paren=false) info fmt = function
362
    | Econst c ->
363
      let n = Number.compute_int_constant c in
Mário Pereira's avatar
Mário Pereira committed
364
      fprintf fmt "(Z.of_string \"%s\")" (BigInt.to_string n)
365
    | Evar pvs ->
Mário Pereira's avatar
Mário Pereira committed
366
      (print_lident info) fmt (pv_name pvs)
Mário Pereira's avatar
Mário Pereira committed
367
    | Elet (let_def, e) ->
Mário Pereira's avatar
Mário Pereira committed
368
      fprintf fmt (protect_on paren "@[%a@] in@ @[%a@]")
Mário Pereira's avatar
Mário Pereira committed
369
        (print_let_def info) let_def (print_expr info) e;
Mário Pereira's avatar
Mário Pereira committed
370
      forget_let_defn let_def
371
    | Eabsurd ->
Mário Pereira's avatar
Mário Pereira committed
372
      fprintf fmt (protect_on paren "assert false (* absurd *)")
Mário Pereira's avatar
Mário Pereira committed
373
    | Ehole -> ()
Mário Pereira's avatar
Mário Pereira committed
374
    | Eapp (rs, []) when rs_equal rs rs_true ->
Mário Pereira's avatar
Mário Pereira committed
375
      fprintf fmt "true"
Mário Pereira's avatar
Mário Pereira committed
376
    | Eapp (rs, []) when rs_equal rs rs_false ->
Mário Pereira's avatar
Mário Pereira committed
377
      fprintf fmt "false"
Mário Pereira's avatar
Mário Pereira committed
378
    | Eapp (rs, [e1; e2]) when rs_equal rs rs_func_app ->
379
      fprintf fmt (protect_on paren "@[<hov 1>%a %a@]")
Mário Pereira's avatar
Mário Pereira committed
380
        (print_expr info) e1 (print_expr ~paren:true info) e2
Mário Pereira's avatar
Mário Pereira committed
381
382
383
384
    | Eapp (rs, [])  ->
      (* avoids parenthesis around values *)
      fprintf fmt "%a" (print_apply info (Hrs.find_def ht_rs rs rs)) []
    | Eapp (rs, pvl) ->
Mário Pereira's avatar
Mário Pereira committed
385
386
387
388
      begin match query_syntax info.info_convert rs.rs_name, pvl with
        | Some s, [{e_node = Econst _}] ->
          let print_constant fmt e = begin match e.e_node with
            | Econst c ->
389
390
391
              let s = BigInt.to_string (Number.compute_int_constant c) in
              if c.Number.ic_negative then fprintf fmt "(%s)" s
              else fprintf fmt "%s" s
Mário Pereira's avatar
Mário Pereira committed
392
393
394
            | _ -> assert false end in
          syntax_arguments s print_constant fmt pvl
        | _ ->
Mário Pereira's avatar
Mário Pereira committed
395
396
      fprintf fmt (protect_on paren "%a")
        (print_apply info (Hrs.find_def ht_rs rs rs)) pvl end
397
    | Ematch (e, pl) ->
398
      fprintf fmt (protect_on paren "begin match @[%a@] with@\n@[%a@]@\nend")
399
        (print_expr info) e (print_list newline (print_branch info)) pl
400
401
    | Eassign al ->
      let assign fmt (rho, rs, pv) =
Mário Pereira's avatar
Mário Pereira committed
402
        fprintf fmt "@[<hov 2>%a.%a <-@ %a@]"
Mário Pereira's avatar
Mário Pereira committed
403
404
          (print_lident info) (pv_name rho) (print_lident info) rs.rs_name
          (print_lident info) (pv_name pv) in
405
406
407
      begin match al with
      | [] -> assert false | [a] -> assign fmt a
      | al -> fprintf fmt "@[begin %a end@]" (print_list semi assign) al end
Mário Pereira's avatar
Mário Pereira committed
408
    | Eif (e1, e2, {e_node = Eblock []}) ->
Mário Pereira's avatar
Mário Pereira committed
409
410
      fprintf fmt (protect_on paren
        "@[<hv>@[<hov 2>if@ %a@]@ then begin@;<1 2>@[%a@] end@]")
Mário Pereira's avatar
Mário Pereira committed
411
        (print_expr info) e1 (print_expr info) e2
Mário Pereira's avatar
Mário Pereira committed
412
413
    | Eif (e1, e2, e3) when is_false e2 && is_true e3 ->
      fprintf fmt (protect_on paren "not %a") (print_expr info ~paren:true) e1
414
    | Eif (e1, e2, e3) when is_true e2 ->
Mário Pereira's avatar
Mário Pereira committed
415
416
      fprintf fmt (protect_on paren "@[<hv>%a || %a@]")
        (print_expr info) e1 (print_expr info) e3
417
    | Eif (e1, e2, e3) when is_false e3 ->
Mário Pereira's avatar
Mário Pereira committed
418
419
      fprintf fmt (protect_on paren "@[<hv>%a && %a@]")
        (print_expr info) e1 (print_expr info) e2
420
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
421
      fprintf fmt (protect_on paren
Mário Pereira's avatar
Mário Pereira committed
422
        "@[<hv>@[<hov 2>if@ %a@ then@ @[%a@]@]@;<1 0>else@;<1 2>@[%a@]@]")
423
        (print_expr info) e1 (print_expr info) e2 (print_expr info) e3
424
    | Eblock [] ->
425
426
427
428
      fprintf fmt "()"
    | Eblock [e] ->
      print_expr info fmt e
    | Eblock el ->
429
430
431
      fprintf fmt "@[<hv>begin@;<1 2>@[%a@]@ end@]"
        (print_list semi (print_expr info)) el
    | Efun (varl, e) ->
Mário Pereira's avatar
Mário Pereira committed
432
      fprintf fmt (protect_on paren "@[<hov 2>fun %a ->@ %a@]")
Mario Pereira's avatar
Mario Pereira committed
433
        (print_list space (print_vs_arg info)) varl (print_expr info) e
Mário Pereira's avatar
Mário Pereira committed
434
    | Ewhile (e1, e2) ->
435
      fprintf fmt "@[<hov 2>while %a do@\n%a@ done@]"
Mário Pereira's avatar
Mário Pereira committed
436
        (print_expr info) e1 (print_expr info) e2
Mário Pereira's avatar
Mário Pereira committed
437
438
439
    | Eraise (xs, e_opt) ->
      print_raise ~paren info xs fmt e_opt
    (* | Etuple _ -> (\* TODO *\) assert false *)
Mário Pereira's avatar
Mário Pereira committed
440
441
442
443
444
445
    | Efor (pv1, pv2, direction, pv3, e) ->
      let print_for_direction fmt = function
        | To -> fprintf fmt "to"
        | DownTo -> fprintf fmt "downto"
      in
      fprintf fmt "@[<hov 2>for %a = %a %a %a do@ @[%a@]@ done@]"
Mário Pereira's avatar
Mário Pereira committed
446
        (print_lident info) (pv_name pv1) (print_lident info) (pv_name pv2)
Mário Pereira's avatar
Mário Pereira committed
447
448
        print_for_direction direction (print_lident info) (pv_name pv3)
        (print_expr info) e
Mário Pereira's avatar
Mário Pereira committed
449
450
451
452
    | Etry (e, bl) ->
      fprintf fmt
        "@[<hv>@[<hov 2>begin@ try@ %a@] with@]@\n@[<hov>%a@]@\nend"
        (print_expr info) e (print_list newline (print_xbranch info)) bl
453
454
455
456
457
458
459
    | Eexn (xs, None, e) ->
      fprintf fmt "@[<hv>let exception %a in@\n%a@]"
        (print_uident info) xs.xs_name (print_expr info) e
    | Eexn (xs, Some t, e) ->
      fprintf fmt "@[<hv>let exception %a of %a in@\n%a@]"
        (print_uident info) xs.xs_name (print_ty ~paren:true info) t
        (print_expr info) e
Mário Pereira's avatar
Mário Pereira committed
460
    | Eignore e -> fprintf fmt "ignore (%a)" (print_expr info) e
Mário Pereira's avatar
Mário Pereira committed
461
462
463
    (* | Enot _ -> (\* TODO *\) assert false *)
    (* | Ebinop _ -> (\* TODO *\) assert false *)
    (* | Ecast _ -> (\* TODO *\) assert false *)
Mário Pereira's avatar
Mário Pereira committed
464

465
  and print_branch info fmt (p, e) =
466
    fprintf fmt "@[<hov 2>| %a ->@ @[%a@]@]"
Mário Pereira's avatar
Mário Pereira committed
467
468
      (print_pat info) p (print_expr info) e;
    forget_pat p
469

Mário Pereira's avatar
Mário Pereira committed
470
471
472
473
474
475
476
477
478
479
480
481
482
483
  and print_raise ~paren info xs fmt e_opt =
    match query_syntax info.info_syn xs.xs_name, e_opt with
    | Some s, None ->
      fprintf fmt "raise %s" s
    | Some s, Some e ->
      fprintf fmt (protect_on paren "raise (%a)")
        (syntax_arguments s (print_expr info)) [e]
    | None, None ->
      fprintf fmt (protect_on paren "raise %a")
        (print_uident info) xs.xs_name
    | None, Some e ->
      fprintf fmt (protect_on paren "raise (%a %a)")
        (print_uident info) xs.xs_name (print_expr ~paren:true info) e

Mário Pereira's avatar
Mário Pereira committed
484
485
486
  and print_xbranch info fmt (xs, pvl, e) =
    let print_var fmt pv =
      print_lident info fmt (pv_name pv) in
Mário Pereira's avatar
Mário Pereira committed
487
488
489
490
491
492
493
    match query_syntax info.info_syn xs.xs_name with
    | Some s ->
      fprintf fmt "@[<hov 4>| %a ->@ %a@]"
        (syntax_arguments s print_var) pvl (print_expr info ~paren:true) e
    | None   ->
      fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" (print_uident info) (xs.xs_name)
        (print_list nothing print_var) pvl (print_expr info) e
Mário Pereira's avatar
Mário Pereira committed
494
495
496

  and print_expr ?(paren=false) info fmt e =
    print_enode ~paren info fmt e.e_node
Mário Pereira's avatar
Mário Pereira committed
497

Mário Pereira's avatar
Mário Pereira committed
498
  let print_type_decl info fst fmt its =
499
500
    let print_constr fmt (id, cs_args) =
      match cs_args with
Mário Pereira's avatar
Mário Pereira committed
501
502
503
      | [] -> fprintf fmt "@[<hov 4>| %a@]" (print_uident info) id
      | l -> fprintf fmt "@[<hov 4>| %a of %a@]" (print_uident info) id
               (print_list star (print_ty ~paren:false info)) l in
504
    let print_field fmt (is_mutable, id, ty) =
Mário Pereira's avatar
Mário Pereira committed
505
      fprintf fmt "%s%a: %a;" (if is_mutable then "mutable " else "")
Mário Pereira's avatar
Mário Pereira committed
506
        (print_lident info) id (print_ty ~paren:false info) ty in
507
    let print_def fmt = function
508
509
510
511
512
513
514
      | None ->
        ()
      | Some (Ddata csl) ->
        fprintf fmt " =@\n%a" (print_list newline print_constr) csl
      | Some (Drecord fl) ->
        fprintf fmt " = %s{@\n%a@\n}"
          (if its.its_private then "private " else "")
515
          (print_list newline print_field) fl
516
      | Some (Dalias ty) ->
Mario Pereira's avatar
Mario Pereira committed
517
        fprintf fmt " =@ %a" (print_ty ~paren:false info) ty
518
    in
519
    fprintf fmt "@[<hov 2>%s %a%a%a@]"
Mário Pereira's avatar
Mário Pereira committed
520
      (if fst then "type" else "and") print_tv_args its.its_args
Mário Pereira's avatar
Mário Pereira committed
521
      (print_lident info) its.its_name print_def its.its_def
522

523
  let print_decl info fmt = function
Mário Pereira's avatar
Mário Pereira committed
524
    | Dlet ldef ->
Mário Pereira's avatar
Mário Pereira committed
525
      print_let_def info fmt ldef;
Mário Pereira's avatar
Mário Pereira committed
526
      fprintf fmt "@\n"
527
    | Dtype dl ->
Mário Pereira's avatar
Mário Pereira committed
528
      print_list_next newline (print_type_decl info) fmt dl;
Mário Pereira's avatar
Mário Pereira committed
529
      fprintf fmt "@\n"
530
    | Dexn (xs, None) ->
Mário Pereira's avatar
Mário Pereira committed
531
       fprintf fmt "exception %a@\n" (print_uident info) xs.xs_name
Mário Pereira's avatar
Mário Pereira committed
532
    | Dexn (xs, Some t)->
Mário Pereira's avatar
Mário Pereira committed
533
      fprintf fmt "@[<hov 2>exception %a of %a@]@\n"
Mário Pereira's avatar
Mário Pereira committed
534
        (print_uident info) xs.xs_name (print_ty ~paren:true info) t
535
536
    | Dclone _ ->
      assert false (*TODO*)
Mário Pereira's avatar
Mário Pereira committed
537
538

  let print_decl info fmt decl =
539
540
    (* avoids printing the same decl for mutually recursive decls *)
    let memo = Hashtbl.create 64 in
Mário Pereira's avatar
Mário Pereira committed
541
542
    let decl_name = get_decl_name decl in
    let decide_print id =
543
544
545
      if query_syntax info.info_syn id = None &&
         not (Hashtbl.mem memo decl) then begin
        Hashtbl.add memo decl (); print_decl info fmt decl;
Mário Pereira's avatar
Mário Pereira committed
546
        fprintf fmt "@." end in
Mário Pereira's avatar
Mário Pereira committed
547
548
    List.iter decide_print decl_name

Mário Pereira's avatar
Mário Pereira committed
549
550
end

551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
let print_decl =
  let memo = Hashtbl.create 16 in
  fun pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d ->
    ignore (old);
    let info = {
      info_syn          = pargs.Pdriver.syntax;
      info_convert      = pargs.Pdriver.converter;
      info_current_th   = th;
      info_current_mo   = Some m;
      info_th_known_map = th.th_known;
      info_mo_known_map = m.mod_known;
      info_fname        = Opt.map Compile.clean_name fname;
      flat              = flat;
    } in
    if not (Hashtbl.mem memo d) then begin
      Hashtbl.add memo d (); Print.print_decl info fmt d end
567

568
let fg ?fname m =
Mário Pereira's avatar
Mário Pereira committed
569
570
571
  let mod_name = m.mod_theory.th_name.id_string in
  let path     = m.mod_theory.th_path in
  (module_name ?fname path mod_name) ^ ".ml"
572

573
let () = Pdriver.register_printer "ocaml"
Mário Pereira's avatar
Mário Pereira committed
574
  ~desc:"printer for OCaml code" fg print_decl