ocaml_printer.ml 27 KB
Newer Older
Mário Pereira's avatar
Mário Pereira committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Mário Pereira's avatar
Mário Pereira committed
5 6 7 8 9 10 11 12 13 14 15 16 17
(*                                                                  *)
(*  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
open Theory
open Pmodule
24
open Wstdlib
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
type info = {
  info_syn          : syntax_map;
30
  info_literal      : syntax_map;
Mário Pereira's avatar
Mário Pereira committed
31 32 33 34 35
  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 37
  info_flat         : bool;
  info_current_ph   : string list; (* current path *)
Mário Pereira's avatar
Mário Pereira committed
38 39
}

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

42
  open Mltree
Mário Pereira's avatar
Mário Pereira committed
43

Andrei Paskevich's avatar
Andrei Paskevich committed
44 45 46 47
  (* extraction attributes *)
  let optional_arg = create_attribute "ocaml:optional"
  let named_arg = create_attribute "ocaml:named"
  let ocaml_remove = create_attribute "ocaml:remove"
48

Andrei Paskevich's avatar
Andrei Paskevich committed
49 50
  let is_optional ~attrs =
    Sattr.mem optional_arg attrs
51

Andrei Paskevich's avatar
Andrei Paskevich committed
52 53
  let is_named ~attrs =
    Sattr.mem named_arg attrs
54

Andrei Paskevich's avatar
Andrei Paskevich committed
55 56
  let is_ocaml_remove ~attrs =
    Ident.Sattr.mem ocaml_remove attrs
57

Mário Pereira's avatar
Mário Pereira committed
58 59 60 61 62 63 64 65 66 67 68
  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";]

Mário Pereira's avatar
Mário Pereira committed
69
  let _is_ocaml_keyword =
70 71 72 73
    let h = Hstr.create 16 in
    List.iter (fun s -> Hstr.add h s ()) ocaml_keywords;
    Hstr.mem h

74 75 76 77
  (* iprinter: local names
     aprinter: type variables
     tprinter: toplevel definitions *)
  let iprinter, aprinter, tprinter =
78 79
    let isanitize = sanitizer char_to_alnumus char_to_alnumus in
    let lsanitize = sanitizer char_to_lalnumus char_to_alnumus in
Mário Pereira's avatar
Mário Pereira committed
80
    create_ident_printer ocaml_keywords ~sanitizer:isanitize,
81
    create_ident_printer ocaml_keywords ~sanitizer:lsanitize,
Mário Pereira's avatar
Mário Pereira committed
82
    create_ident_printer ocaml_keywords ~sanitizer:lsanitize
Mário Pereira's avatar
Mário Pereira committed
83

Mário Pereira's avatar
Mário Pereira committed
84
  let forget_id id = forget_id iprinter id
Mário Pereira's avatar
Mário Pereira committed
85
  let _forget_ids = List.iter forget_id
Mário Pereira's avatar
Mário Pereira committed
86 87 88
  let forget_var (id, _, _) = forget_id id
  let forget_vars = List.iter forget_var

Mário Pereira's avatar
Mário Pereira committed
89
  let forget_let_defn = function
90 91 92
    | Lvar (v,_) -> forget_id v.pv_vs.vs_name
    | Lsym (s,_,_,_) | Lany (s,_,_) -> forget_rs s
    | Lrec rdl -> List.iter (fun fd -> forget_rs fd.rec_sym) rdl
Mário Pereira's avatar
Mário Pereira committed
93

Mário Pereira's avatar
Mário Pereira committed
94 95
  let rec forget_pat = function
    | Pwild -> ()
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
96
    | Pvar {vs_name=id} -> forget_id id
Mário Pereira's avatar
Mário Pereira committed
97 98 99 100
    | Papp (_, pl) | Ptuple pl -> List.iter forget_pat pl
    | Por (p1, p2) -> forget_pat p1; forget_pat p2
    | Pas (p, _) -> forget_pat p

101 102 103
  let print_global_ident ~sanitizer fmt id =
    let s = id_unique ~sanitizer tprinter id in
    Ident.forget_id tprinter id;
Mário Pereira's avatar
Mário Pereira committed
104 105
    fprintf fmt "%s" s

106 107 108 109 110
  let print_path ~sanitizer fmt (q, id) =
    assert (List.length q >= 1);
    match Lists.chop_last q with
    | [], _ -> print_global_ident ~sanitizer fmt id
    | q, _  ->
111 112
        fprintf fmt "%a.%a"
          (print_list dot string) q (print_global_ident ~sanitizer) id
113

114 115 116 117 118
  let rec remove_prefix acc current_path = match acc, current_path with
    | [], _ | _, [] -> acc
    | p1 :: _, p2 :: _ when p1 <> p2 -> acc
    | _ :: r1, _ :: r2 -> remove_prefix r1 r2

119 120
  let is_local_id info id =
    Sid.mem id info.info_current_th.th_local ||
Mário Pereira's avatar
Mário Pereira committed
121
    Opt.fold (fun _ m -> Sid.mem id m.Pmodule.mod_local)
122 123
      false info.info_current_mo

124 125
  exception Local

126
  let print_qident ~sanitizer info fmt id =
Mário Pereira's avatar
Mário Pereira committed
127
    try
128
      if info.info_flat then raise Not_found;
129
      if is_local_id info id then raise Local;
130 131
      let p, t, q =
        try Pmodule.restore_path id with Not_found -> Theory.restore_path id in
132 133
      let fname = if p = [] then info.info_fname else None in
      let m = Strings.capitalize (module_name ?fname p t) in
134
      fprintf fmt "%s.%a" m (print_path ~sanitizer) (q, id)
135
    with
136
    | Not_found ->
137 138
        let s = id_unique ~sanitizer iprinter id in
        fprintf fmt "%s" s
139
    | Local ->
140 141 142 143 144
        let _, _, q =
          try Pmodule.restore_path id with Not_found ->
            Theory.restore_path id in
        let q = remove_prefix q (List.rev info.info_current_ph) in
        print_path ~sanitizer fmt (q, id)
145 146 147

  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
148

Mário Pereira's avatar
Mário Pereira committed
149 150
  let print_tv fmt tv =
    fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
Mário Pereira's avatar
Mário Pereira committed
151

152 153 154
  let protect_on b s =
    if b then "(" ^^ s ^^ ")" else s

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

Mário Pereira's avatar
Mário Pereira committed
157 158
  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
159
    | [x1], [x2] ->
160
        print1 fmt x1; sep_m fmt (); print2 fmt x2
Mário Pereira's avatar
Mário Pereira committed
161
    | x1 :: r1, x2 :: r2 ->
162 163
        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
164 165
    | _ -> ()

Mário Pereira's avatar
Mário Pereira committed
166 167
  let print_rs info fmt rs =
    fprintf fmt "%a" (print_lident info) rs.rs_name
Mário Pereira's avatar
Mário Pereira committed
168

169 170
  (** Types *)

Mario Pereira's avatar
Mario Pereira committed
171
  let rec print_ty ?(paren=false) info fmt = function
172
    | Tvar tv ->
173
        print_tv fmt tv
Mário Pereira's avatar
Mário Pereira committed
174
    | Ttuple [] ->
175
        fprintf fmt "unit"
Mário Pereira's avatar
Mário Pereira committed
176
    | Ttuple [t] ->
177
        print_ty ~paren info fmt t
Mário Pereira's avatar
Mário Pereira committed
178
    | Ttuple tl ->
179 180
        fprintf fmt (protect_on paren "@[%a@]")
          (print_list star (print_ty ~paren:true info)) tl
Mário Pereira's avatar
Mário Pereira committed
181
    | Tapp (ts, tl) ->
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
        match query_syntax info.info_syn ts with
        | Some s ->
            fprintf fmt (protect_on paren "%a")
              (syntax_arguments s (print_ty ~paren:true info)) 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
197

Mário Pereira's avatar
Mário Pereira committed
198
  let print_vsty_opt info fmt id ty =
199
    fprintf fmt "?%s:(%a:@ %a)" id.id_string (print_lident info) id
Mário Pereira's avatar
Mário Pereira committed
200
      (print_ty ~paren:false info) ty
Mário Pereira's avatar
Mário Pereira committed
201

Mário Pereira's avatar
Mário Pereira committed
202
  let print_vsty_named info fmt id ty =
203
    fprintf fmt "~%s:(%a:@ %a)" id.id_string (print_lident info) id
Mário Pereira's avatar
Mário Pereira committed
204
      (print_ty ~paren:false info) ty
Mário Pereira's avatar
Mário Pereira committed
205

Mário Pereira's avatar
Mário Pereira committed
206
  let print_vsty info fmt (id, ty, _) =
Andrei Paskevich's avatar
Andrei Paskevich committed
207 208 209
    let attrs = id.id_attrs in
    if is_optional ~attrs then print_vsty_opt info fmt id ty
    else if is_named ~attrs then print_vsty_named info fmt id ty
Mário Pereira's avatar
Mário Pereira committed
210
    else fprintf fmt "(%a:@ %a)" (print_lident info) id
211
        (print_ty ~paren:false info) ty
212

Mário Pereira's avatar
Mário Pereira committed
213 214
  let print_tv_arg = print_tv
  let print_tv_args fmt = function
215
    | []   -> ()
Mário Pereira's avatar
Mário Pereira committed
216 217
    | [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
218

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

Mário Pereira's avatar
Mário Pereira committed
222 223 224
  let get_record info rs =
    match Mid.find_opt rs.rs_name info.info_mo_known_map with
    | Some {pd_node = PDtype itdl} ->
225 226 227 228
        let eq_rs {itd_constructors} =
          List.exists (rs_equal rs) itd_constructors in
        let itd = List.find eq_rs itdl in
        List.filter (fun e -> not (rs_ghost e)) itd.itd_fields
Mário Pereira's avatar
Mário Pereira committed
229 230
    | _ -> []

231
  let rec print_pat ?(paren=false) info fmt = function
232
    | Pwild ->
233
        fprintf fmt "_"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
234
    | Pvar {vs_name=id} ->
235
        (print_lident info) fmt id
236
    | Pas (p, {vs_name=id}) ->
237 238
        fprintf fmt (protect_on paren "%a as %a") (print_pat info) p
          (print_lident info) id
239
    | Por (p1, p2) ->
240 241
        fprintf fmt (protect_on paren "%a | %a") (print_pat info) p1
          (print_pat info) p2
242
    | Ptuple pl ->
243
        fprintf fmt "(%a)" (print_list comma (print_pat ~paren:true info)) pl
Mário Pereira's avatar
Mário Pereira committed
244
    | Papp (ls, pl) ->
245 246 247 248 249 250 251
        match query_syntax info.info_syn ls.ls_name, pl with
        | Some s, _ ->
            syntax_arguments s (print_pat info) fmt pl
        | None, pl ->
            let pjl = let rs = restore_rs ls in get_record info rs in
            match pjl with
            | []  -> print_papp info ls fmt pl
252 253 254 255
            | pjl ->
                fprintf fmt (protect_on paren "@[<hov 2>{ %a }@]")
                  (print_list2 semi equal (print_rs info)
                  (print_pat ~paren: true info)) (pjl, pl)
Mário Pereira's avatar
Mário Pereira committed
256 257 258 259

  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
260
               (print_pat info) p
Mário Pereira's avatar
Mário Pereira committed
261
    | pl  -> fprintf fmt "%a (%a)" (print_uident info) ls.ls_name
262
               (print_list comma (print_pat info)) pl
263

264 265
  (** Expressions *)

266
  let pv_name pv = pv.pv_vs.vs_name
267
  let print_pv info fmt pv = print_lident info fmt (pv_name pv)
268

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
269
  (* FIXME put these in Compile*)
270 271 272 273 274 275 276 277
  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

278 279
  let check_val_in_drv info ({rs_name = {id_loc = loc}} as rs) =
    (* here [rs] refers to a [val] declaration *)
280 281
    match query_syntax info.info_syn     rs.rs_name with
    | None (* when info.info_flat *) ->
282
        Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
283
    | _ -> ()
284

285 286
  let is_mapped_to_int info ity =
    match ity.ity_node with
287 288 289 290
    | Ityapp ({ its_ts = ts }, _, _) ->
        query_syntax info.info_syn ts.ts_name = Some "int"
    | _ -> false

291 292 293 294 295 296 297
  let print_constant fmt e = begin match e.e_node with
    | Econst c ->
        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
    | _ -> assert false end

298 299 300 301
  let print_for_direction fmt = function
    | To     -> fprintf fmt "to"
    | DownTo -> fprintf fmt "downto"

Mário Pereira's avatar
Mário Pereira committed
302
  let rec print_apply_args info fmt = function
303
    | expr :: exprl, pv :: pvl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
304
        if is_optional ~attrs:(pv_name pv).id_attrs then
305 306 307 308 309
          begin match expr.e_node with
            | Eapp (rs, _)
              when query_syntax info.info_syn rs.rs_name = Some "None" -> ()
            | _ -> fprintf fmt "?%s:%a" (pv_name pv).id_string
                     (print_expr ~paren:true info) expr end
Andrei Paskevich's avatar
Andrei Paskevich committed
310
        else if is_named ~attrs:(pv_name pv).id_attrs then
311 312
          fprintf fmt "~%s:%a" (pv_name pv).id_string
            (print_expr ~paren:true info) expr
313
        else fprintf fmt "%a" (print_expr ~paren:true info) expr;
314 315
        if exprl <> [] then fprintf fmt "@ ";
        print_apply_args info fmt (exprl, pvl)
316 317 318
    | expr :: exprl, [] ->
        fprintf fmt "%a" (print_expr ~paren:true info) expr;
        print_apply_args info fmt (exprl, [])
319
    | [], _ -> ()
Mário Pereira's avatar
Mário Pereira committed
320

321
  and print_apply info rs fmt pvl =
322
    let isfield =
323
      match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
324
      | None   -> false
325 326 327 328
      | Some _ -> true in
    let isconstructor () =
      match Mid.find_opt rs.rs_name info.info_mo_known_map with
      | Some {pd_node = PDtype its} ->
329 330 331
          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
332
      | _ -> false in
333 334
    match query_syntax info.info_syn rs.rs_name, pvl with
    | Some s, _ (* when is_local_id info rs.rs_name  *)->
335
        syntax_arguments s (print_expr ~paren:true info) fmt pvl;
336
    | None, [t] when is_rs_tuple rs ->
337
        fprintf fmt "@[%a@]" (print_expr info) t
338
    | None, tl when is_rs_tuple rs ->
339
        fprintf fmt "@[(%a)@]" (print_list comma (print_expr info)) tl
340
    | None, [t1] when isfield ->
341
        fprintf fmt "%a.%a" (print_expr info) t1 (print_lident info) rs.rs_name
342
    | None, tl when isconstructor () ->
343 344 345 346 347 348 349 350 351
        let pjl = get_record info rs in
        begin match pjl, tl with
          | [], [] ->
              (print_uident info) fmt rs.rs_name
          | [], [t] ->
              fprintf fmt "@[<hov 2>%a %a@]" (print_uident info) rs.rs_name
                (print_expr ~paren:true info) t
          | [], tl ->
              fprintf fmt "@[<hov 2>%a (%a)@]" (print_uident info) rs.rs_name
352 353 354 355 356
                (print_list comma (print_expr ~paren:true info)) tl
          | pjl, tl -> let equal fmt () = fprintf fmt " =@ " in
              fprintf fmt "@[<hov 2>{ %a }@]"
                (print_list2 semi equal (print_rs info)
                   (print_expr ~paren:true info)) (pjl, tl) end
357
    | None, [] ->
358
        (print_lident info) fmt rs.rs_name
359
    | _, tl ->
360 361 362
        fprintf fmt "@[<hov 2>%a %a@]"
          (print_lident info) rs.rs_name
          (print_apply_args info) (tl, rs.rs_cty.cty_args)
Mário Pereira's avatar
Mário Pereira committed
363
  (* (print_list space (print_expr ~paren:true info)) tl *)
364

365
  and print_svar fmt s =
366
    Stv.iter (fun tv -> fprintf fmt "%a " print_tv tv) s
367

368
  and print_fun_type_args info fmt (args, s, res, e) =
369
    if Stv.is_empty s then
370
      fprintf fmt "@[%a@] :@ %a@ =@ %a"
371 372
        (print_list space (print_vs_arg info)) args
        (print_ty info) res
373
        (print_expr info) e
374 375 376
    else
      let ty_args = List.map (fun (_, ty, _) -> ty) args in
      let id_args = List.map (fun (id, _, _) -> id) args in
377 378 379
      let arrow fmt () = fprintf fmt " ->@ " in
      fprintf fmt ":@ @[<h>@[%a@]. @[%a ->@ %a@]@] =@ \
                   @[<hov 2>fun @[%a@]@ ->@ %a@]"
380
        print_svar s
381 382
        (print_list arrow (print_ty ~paren:true info)) ty_args
        (print_ty ~paren:true info) res
383
        (print_list space (print_lident info)) id_args
384
        (print_expr info) e
385

386
  and print_let_def ?(functor_arg=false) info fmt = function
387 388
    | Lvar (pv, {e_node = Eany ty}) when functor_arg ->
        fprintf fmt "@[<hov 2>val %a : %a@]"
Mário Pereira's avatar
Mário Pereira committed
389
          (print_lident info) (pv_name pv) (print_ty info) ty;
Mário Pereira's avatar
Mário Pereira committed
390
    | Lvar (pv, e) ->
391
        fprintf fmt "@[<hov 2>let %a =@ %a@]"
Mário Pereira's avatar
Mário Pereira committed
392
          (print_lident info) (pv_name pv) (print_expr info) e
Mário Pereira's avatar
Mário Pereira committed
393
    | Lsym (rs, res, args, ef) ->
394 395 396 397 398
        fprintf fmt "@[<hov 2>let %a @[%a@] : %a@ =@ @[%a@]@]"
          (print_lident info) rs.rs_name
          (print_list space (print_vs_arg info)) args
          (print_ty info) res (print_expr info) ef;
        forget_vars args
399
    | Lrec rdef ->
400 401 402 403 404 405 406 407 408 409
        let print_one fst fmt = function
          | { rec_sym = rs1; rec_args = args; rec_exp = e;
              rec_res = res; rec_svar = s } ->
              fprintf fmt "@[<hov 2>%s %a %a@]"
                (if fst then "let rec" else "and")
                (print_lident info) rs1.rs_name
                (print_fun_type_args info) (args, s, res, e);
              forget_vars args
        in
        print_list_next newline print_one fmt rdef;
410 411 412 413
    | Lany (rs, res, []) when functor_arg ->
        fprintf fmt "@[<hov 2>val %a : %a@]"
          (print_lident info) rs.rs_name
          (print_ty info) res;
414
    | Lany (rs, res, args) when functor_arg ->
415 416 417 418 419 420 421
        let print_ty_arg info fmt (_, ty, _) =
          fprintf fmt "@[%a@]" (print_ty info) ty in
        fprintf fmt "@[<hov 2>val %a : @[%a@] ->@ %a@]"
          (print_lident info) rs.rs_name
          (print_list arrow (print_ty_arg info)) args
          (print_ty info) res;
        forget_vars args
422
    | Lany (rs, _, _) -> check_val_in_drv info rs
Mário Pereira's avatar
Mário Pereira committed
423

424 425
  and print_expr ?(paren=false) info fmt e =
    match e.e_node with
426
    | Econst c ->
427
        let n = Number.compute_int_constant c in
428 429 430 431 432 433
        let n = BigInt.to_string n in
        let id = match e.e_ity with
          | I { ity_node = Ityapp ({its_ts = ts},_,_) } -> ts.ts_name
          | _ -> assert false in
        (match query_syntax info.info_literal id with
         | Some s -> syntax_arguments s print_constant fmt [e]
434 435
         | None when n = "0" -> fprintf fmt "Z.zero"
         | None when n = "1" -> fprintf fmt "Z.one"
436
         | None   -> fprintf fmt (protect_on paren "Z.of_string \"%s\"") n)
437
    | Evar pvs ->
438
        (print_lident info) fmt (pv_name pvs)
Mário Pereira's avatar
Mário Pereira committed
439
    | Elet (let_def, e) ->
440 441 442
        fprintf fmt (protect_on paren "@[%a@] in@ @[%a@]")
          (print_let_def info) let_def (print_expr info) e;
        forget_let_defn let_def
443
    | Eabsurd ->
444
        fprintf fmt (protect_on paren "assert false (* absurd *)")
Mário Pereira's avatar
Mário Pereira committed
445
    | Ehole -> ()
446
    | Eany _ -> () (* FIXME *)
Mário Pereira's avatar
Mário Pereira committed
447
    | Eapp (rs, []) when rs_equal rs rs_true ->
448
        fprintf fmt "true"
Mário Pereira's avatar
Mário Pereira committed
449
    | Eapp (rs, []) when rs_equal rs rs_false ->
450
        fprintf fmt "false"
451
    | Eapp (rs, [])  -> (* avoids parenthesis around values *)
452
        fprintf fmt "%a" (print_apply info rs) []
Mário Pereira's avatar
Mário Pereira committed
453
    | Eapp (rs, pvl) ->
454 455
       fprintf fmt (protect_on paren "%a")
               (print_apply info rs) pvl
456
    | Ematch (e1, [p, e2], []) ->
457
        fprintf fmt (protect_on paren "let %a =@ %a in@ %a")
458
          (print_pat info) p (print_expr info) e1 (print_expr info) e2
459
    | Ematch (e, pl, []) ->
460 461 462
        fprintf fmt
          (protect_on paren "begin match @[%a@] with@\n@[<hov>%a@]@\nend")
          (print_expr info) e (print_list newline (print_branch info)) pl
463
    | Eassign al ->
464
        let assign fmt (rho, rs, e) =
465 466
          fprintf fmt "@[<hov 2>%a.%a <-@ %a@]"
            (print_lident info) (pv_name rho) (print_lident info) rs.rs_name
467
            (print_expr info) e in
468 469 470
        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
471
    | Eif (e1, e2, {e_node = Eblock []}) ->
472 473 474
        fprintf fmt
          (protect_on paren
             "@[<hv>@[<hov 2>if@ %a@]@ then begin@;<1 2>@[%a@] end@]")
475
          (print_expr info) e1 (print_expr info) e2
Mário Pereira's avatar
Mário Pereira committed
476
    | Eif (e1, e2, e3) when is_false e2 && is_true e3 ->
477
        fprintf fmt (protect_on paren "not %a") (print_expr info ~paren:true) e1
478
    | Eif (e1, e2, e3) when is_true e2 ->
479
        fprintf fmt (protect_on paren "@[<hv>%a || %a@]")
480
          (print_expr info ~paren:true) e1 (print_expr info ~paren:true) e3
481
    | Eif (e1, e2, e3) when is_false e3 ->
482
        fprintf fmt (protect_on paren "@[<hv>%a && %a@]")
483
          (print_expr info ~paren:true) e1 (print_expr info ~paren:true) e2
484
    | Eif (e1, e2, e3) ->
485 486 487 488
        fprintf fmt (protect_on paren
                       "@[<hv>@[<hov 2>if@ %a@ then@ begin@ @[%a@] end@]\
                        @;<1 0>else@ begin@;<1 2>@[%a@] end@]")
          (print_expr info) e1 (print_expr info) e2 (print_expr info) e3
489
    | Eblock [] ->
490
        fprintf fmt "()"
491
    | Eblock [e] ->
492
        print_expr info fmt e
493
    | Eblock el ->
494 495
        fprintf fmt "@[<hv>begin@;<1 2>@[%a@]@ end@]"
          (print_list semi (print_expr info)) el
496
    | Efun (varl, e) ->
497 498
        fprintf fmt (protect_on paren "@[<hov 2>fun %a ->@ %a@]")
          (print_list space (print_vs_arg info)) varl (print_expr info) e
Mário Pereira's avatar
Mário Pereira committed
499
    | Ewhile (e1, e2) ->
500 501
        fprintf fmt "@[<hov 2>while %a do@\n%a@ done@]"
          (print_expr info) e1 (print_expr info) e2
Mário Pereira's avatar
Mário Pereira committed
502
    | Eraise (xs, e_opt) ->
503
        print_raise ~paren info xs fmt e_opt
504
    | Efor (pv1, pv2, dir, pv3, e) ->
Mário Pereira's avatar
Mário Pereira committed
505
        if is_mapped_to_int info pv1.pv_ity then begin
506 507 508
          fprintf fmt "@[<hov 2>for %a = %a %a %a do@ @[%a@]@ done@]"
            (print_lident info) (pv_name pv1) (print_lident info) (pv_name pv2)
            print_for_direction dir (print_lident info) (pv_name pv3)
Mário Pereira's avatar
Mário Pereira committed
509 510
            (print_expr info) e;
          forget_pv pv1 end
511 512 513 514 515 516 517 518
        else
          let for_id  = id_register (id_fresh "for_loop_to") in
          let cmp, op = match dir with
            | To     -> "Z.leq", "Z.succ"
            | DownTo -> "Z.geq", "Z.pred" in
          fprintf fmt (protect_on paren
                         "@[<hov 2>let rec %a %a =@ if %s %a %a then \
                          begin@ %a; %a (%s %a) end@ in@ %a %a@]")
519 520 521 522 523
          (* let rec *) (print_lident info) for_id (print_pv info) pv1
          (* if      *)  cmp (print_pv info) pv1 (print_pv info) pv3
          (* then    *) (print_expr info) e (print_lident info) for_id
                        op (print_pv info) pv1
          (* in      *) (print_lident info) for_id (print_pv info) pv2
524 525 526 527
    | Ematch (e, [], xl) ->
        fprintf fmt "@[<hv>@[<hov 2>begin@ try@ %a@] with@]@\n@[<hov>%a@]@\nend"
          (print_expr info) e (print_list newline (print_xbranch info false)) xl
    | Ematch (e, bl, xl) ->
528
        fprintf fmt
529 530 531
          (protect_on paren "begin match @[%a@] with@\n@[<hov>%a@\n%a@]@\nend")
          (print_expr info) e (print_list newline (print_branch info)) bl
          (print_list newline (print_xbranch info true)) xl
532
    | Eexn (xs, None, e) ->
533 534
        fprintf fmt "@[<hv>let exception %a in@\n%a@]"
          (print_uident info) xs.xs_name (print_expr info) e
535
    | Eexn (xs, Some t, e) ->
536 537 538
        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
539
    | Eignore e -> fprintf fmt "ignore (%a)" (print_expr info) e
Mário Pereira's avatar
Mário Pereira committed
540

541
  and print_branch info fmt (p, e) =
542
    fprintf fmt "@[<hov 2>| %a ->@ @[%a@]@]"
Mário Pereira's avatar
Mário Pereira committed
543 544
      (print_pat info) p (print_expr info) e;
    forget_pat p
545

Mário Pereira's avatar
Mário Pereira committed
546 547 548
  and print_raise ~paren info xs fmt e_opt =
    match query_syntax info.info_syn xs.xs_name, e_opt with
    | Some s, None ->
549
        fprintf fmt "raise (%s)" s
Mário Pereira's avatar
Mário Pereira committed
550
    | Some s, Some e ->
551 552
        fprintf fmt (protect_on paren "raise (%a)")
          (syntax_arguments s (print_expr info)) [e]
Mário Pereira's avatar
Mário Pereira committed
553
    | None, None ->
554 555
        fprintf fmt (protect_on paren "raise %a")
          (print_uident info) xs.xs_name
Mário Pereira's avatar
Mário Pereira committed
556
    | None, Some e ->
557 558
        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
559

560 561 562 563
  and print_xbranch info case fmt (xs, pvl, e) =
    let print_exn fmt () =
      if case then fprintf fmt "exception " else fprintf fmt "" in
    let print_var fmt pv = print_lident info fmt (pv_name pv) in
564
    match query_syntax info.info_syn xs.xs_name, pvl with
565 566 567 568 569 570 571 572 573 574 575
    | Some s, _ -> fprintf fmt "@[<hov 4>| %a%a ->@ %a@]"
        print_exn () (syntax_arguments s print_var) pvl
        (print_expr info ~paren:true) e
    | None, [] -> fprintf fmt "@[<hov 4>| %a%a ->@ %a@]"
        print_exn () (print_uident info) xs.xs_name (print_expr info) e
    | None, [pv] -> fprintf fmt "@[<hov 4>| %a%a %a ->@ %a@]"
        print_exn () (print_uident info) xs.xs_name print_var pv
        (print_expr info) e
    | None, pvl -> fprintf fmt "@[<hov 4>| %a%a (%a) ->@ %a@]"
        print_exn () (print_uident info) xs.xs_name
        (print_list comma print_var) pvl (print_expr info) e
Mário Pereira's avatar
Mário Pereira committed
576

Mário Pereira's avatar
Mário Pereira committed
577
  let print_type_decl info fst fmt its =
578 579
    let print_constr fmt (id, cs_args) =
      match cs_args with
Mário Pereira's avatar
Mário Pereira committed
580 581 582
      | [] -> 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
583
    let print_field fmt (is_mutable, id, ty) =
584
      fprintf fmt "%s%a: @[%a@];" (if is_mutable then "mutable " else "")
Mário Pereira's avatar
Mário Pereira committed
585
        (print_lident info) id (print_ty ~paren:false info) ty in
586
    let print_def fmt = function
587
      | None ->
588
          ()
589
      | Some (Ddata csl) ->
590
          fprintf fmt " =@\n%a" (print_list newline print_constr) csl
591
      | Some (Drecord fl) ->
592 593 594
          fprintf fmt " = %s{@\n%a@\n}"
            (if its.its_private then "private " else "")
            (print_list newline print_field) fl
595
      | Some (Dalias ty) ->
596
          fprintf fmt " =@ %a" (print_ty ~paren:false info) ty
597 598 599 600
      | Some (Drange _) ->
          fprintf fmt " =@ Z.t"
      | Some (Dfloat _) ->
          assert false (*TODO*)
601
    in
Andrei Paskevich's avatar
Andrei Paskevich committed
602 603
    let attrs = its.its_name.id_attrs in
    if not (is_ocaml_remove ~attrs) then
Mário Pereira's avatar
Mário Pereira committed
604
      fprintf fmt "@[<hov 2>@[%s %a%a@]%a@]"
605 606
        (if fst then "type" else "and") print_tv_args its.its_args
        (print_lident info) its.its_name print_def its.its_def
607

608 609 610
  let rec is_signature_decl info = function
    | Dtype _ -> true
    | Dlet (Lany _) -> true
611
    | Dlet (Lvar (_, {e_node = Eany _})) -> true
612 613 614 615 616 617 618 619 620 621 622 623
    | Dlet _ -> false
    | Dexn _ -> true
    | Dmodule (_, dl) -> is_signature info dl

  and is_signature info dl =
    List.for_all (is_signature_decl info) dl

  let extract_functor_args info dl =
    let rec extract args = function
      (* FIXME remove empty args? *)
      (* | Dmodule (_, []) :: dl -> extract args dl *)
      | Dmodule (x, dlx) :: dl when is_signature info dlx ->
624
          extract ((x, dlx) :: args) dl
625 626 627
      | dl -> List.rev args, dl in
    extract [] dl

628
  let rec print_decl ?(functor_arg=false) info fmt = function
Mário Pereira's avatar
Mário Pereira committed
629
    | Dlet ldef ->
630
        print_let_def info ~functor_arg fmt ldef
631
    | Dtype dl ->
632
        print_list_next newline (print_type_decl info) fmt dl
633
    | Dexn (xs, None) ->
634
        fprintf fmt "exception %a" (print_uident info) xs.xs_name
Mário Pereira's avatar
Mário Pereira committed
635
    | Dexn (xs, Some t)->
636 637
        fprintf fmt "@[<hov 2>exception %a of %a@]"
          (print_uident info) xs.xs_name (print_ty ~paren:true info) t
638
    | Dmodule (s, dl) ->
639 640
        let args, dl = extract_functor_args info dl in
        let info = { info with info_current_ph = s :: info.info_current_ph } in
641
        fprintf fmt "@[@[<hov 2>module %s%a@ =@]@\n@[<hov 2>struct@ %a@]@ end" s
642 643
          (print_functor_args info) args
          (print_list newline2 (print_decl info)) dl
644 645 646 647

  and print_functor_args info fmt args =
    let print_sig info fmt dl =
      fprintf fmt "sig@ %a@ end"
648
        (print_list newline (print_decl info ~functor_arg:true)) dl in
649
    let print_pair fmt (s, dl) =
650
      let info = { info with info_current_ph = s :: info.info_current_ph } in
651
      fprintf fmt "(%s:@ %a)" s (print_sig info) dl in
652
    fprintf fmt "%a" (print_list space print_pair) args
Mário Pereira's avatar
Mário Pereira committed
653 654

  let print_decl info fmt decl =
655 656
    (* avoids printing the same decl for mutually recursive decls *)
    let memo = Hashtbl.create 64 in
Mário Pereira's avatar
Mário Pereira committed
657 658
    let decl_name = get_decl_name decl in
    let decide_print id =
659 660 661
      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
662
        fprintf fmt "@\n@." end in
Mário Pereira's avatar
Mário Pereira committed
663 664
    List.iter decide_print decl_name

Mário Pereira's avatar
Mário Pereira committed
665 666
end

667 668 669 670 671 672
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;
673
      info_literal      = pargs.Pdriver.literal;
674 675 676 677 678
      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;
679 680
      info_flat         = flat;
      info_current_ph   = [];
681
    } in
682 683
    if not (Hashtbl.mem memo d) then begin Hashtbl.add memo d ();
      Print.print_decl info fmt d end
684

685
let ng suffix ?fname m =
Mário Pereira's avatar
Mário Pereira committed
686 687
  let mod_name = m.mod_theory.th_name.id_string in
  let path     = m.mod_theory.th_path in
688
  (module_name ?fname path mod_name) ^ suffix
689

690 691 692 693 694 695 696 697 698 699 700 701 702 703
let file_gen = ng ".ml"
let mli_gen = ng ".mli"

open Pdriver

let ocaml_printer =
  { desc            = "printer for Ocaml code";
    file_gen        = file_gen;
    decl_printer    = print_decl;
    interf_gen      = Some mli_gen;
    interf_printer  = None;
    prelude_printer = print_empty_prelude }

let () = Pdriver.register_printer "ocaml" ocaml_printer