ocaml_printer.ml 27.2 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
Guillaume Melquiond's avatar
Guillaume Melquiond committed
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 30
type info = {
  info_syn          : syntax_map;
  info_convert      : syntax_map;
31
  info_literal      : syntax_map;
Mário Pereira's avatar
Mário Pereira committed
32 33 34 35 36
  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;
37 38
  info_flat         : bool;
  info_current_ph   : string list; (* current path *)
Mário Pereira's avatar
Mário Pereira committed
39 40
}

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

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

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

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

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

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

Mário Pereira's avatar
Mário Pereira committed
59 60 61 62 63 64 65 66 67 68 69
  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
70
  let _is_ocaml_keyword =
71 72 73 74
    let h = Hstr.create 16 in
    List.iter (fun s -> Hstr.add h s ()) ocaml_keywords;
    Hstr.mem h

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

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

Mário Pereira's avatar
Mário Pereira committed
90
  let forget_let_defn = function
91 92 93
    | 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
94

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

102 103 104
  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
105 106
    fprintf fmt "%s" s

107 108 109 110 111
  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, _  ->
112 113
        fprintf fmt "%a.%a"
          (print_list dot string) q (print_global_ident ~sanitizer) id
114

115 116 117 118 119
  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

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

125 126
  exception Local

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

  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
149

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

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

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

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

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

170 171
  (** Types *)

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

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

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

Mário Pereira's avatar
Mário Pereira committed
207
  let print_vsty info fmt (id, ty, _) =
Andrei Paskevich's avatar
Andrei Paskevich committed
208 209 210
    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
211
    else fprintf fmt "(%a:@ %a)" (print_lident info) id
212
        (print_ty ~paren:false info) ty
213

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

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

Mário Pereira's avatar
Mário Pereira committed
223 224 225
  let get_record info rs =
    match Mid.find_opt rs.rs_name info.info_mo_known_map with
    | Some {pd_node = PDtype itdl} ->
226 227 228 229
        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
230 231 232
    | _ -> []

  let rec print_pat info fmt = function
233
    | Pwild ->
234
        fprintf fmt "_"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
235
    | Pvar {vs_name=id} ->
236
        (print_lident info) fmt id
237
    | Pas (p, {vs_name=id}) ->
238
        fprintf fmt "%a as %a" (print_pat info) p (print_lident info) id
239
    | Por (p1, p2) ->
240
        fprintf fmt "%a | %a" (print_pat info) p1 (print_pat info) p2
241
    | Ptuple pl ->
242
        fprintf fmt "(%a)" (print_list comma (print_pat info)) pl
Mário Pereira's avatar
Mário Pereira committed
243
    | Papp (ls, pl) ->
244 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
            | pjl -> fprintf fmt "@[<hov 2>{ %a }@]"
252 253
                (print_list2 semi equal (print_rs info) (print_pat info))
                (pjl, pl)
Mário Pereira's avatar
Mário Pereira committed
254 255 256 257

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

262 263
  (** Expressions *)

264
  let pv_name pv = pv.pv_vs.vs_name
265
  let print_pv info fmt pv = print_lident info fmt (pv_name pv)
266

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

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_convert rs.rs_name,
          query_syntax info.info_syn     rs.rs_name with
282
    | None, None (* when info.info_flat *) ->
283
        Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
284
    | _ -> ()
285

Mário Pereira's avatar
Mário Pereira committed
286 287
  let is_mapped_to_int info ity =
    match ity.ity_node with
288 289 290 291
    | Ityapp ({ its_ts = ts }, _, _) ->
        query_syntax info.info_syn ts.ts_name = Some "int"
    | _ -> false

292 293 294 295 296 297 298
  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

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

Mário Pereira's avatar
Mário Pereira committed
303
  let rec print_apply_args info fmt = function
304
    | expr :: exprl, pv :: pvl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
305
        if is_optional ~attrs:(pv_name pv).id_attrs then
306 307 308 309 310
          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
311
        else if is_named ~attrs:(pv_name pv).id_attrs then
312 313
          fprintf fmt "~%s:%a" (pv_name pv).id_string
            (print_expr ~paren:true info) expr
314
        else fprintf fmt "%a" (print_expr ~paren:true info) expr;
315 316
        if exprl <> [] then fprintf fmt "@ ";
        print_apply_args info fmt (exprl, pvl)
317 318 319
    | expr :: exprl, [] ->
        fprintf fmt "%a" (print_expr ~paren:true info) expr;
        print_apply_args info fmt (exprl, [])
320
    | [], _ -> ()
Mário Pereira's avatar
Mário Pereira committed
321

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

368
  and print_svar fmt s =
369
    Stv.iter (fun tv -> fprintf fmt "%a " print_tv tv) s
370

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

389
  and print_let_def ?(functor_arg=false) info fmt = function
390 391 392 393
    | Lvar (pv, {e_node = Eany ty}) when functor_arg ->
        fprintf fmt "@[<hov 2>val %a : %a@]"
          (print_lident info) (pv_name pv)
          (print_ty info) ty;
Mário Pereira's avatar
Mário Pereira committed
394
    | Lvar (pv, e) ->
395 396 397
        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
398
    | Lsym (rs, res, args, ef) ->
399 400 401 402 403
        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
404
    | Lrec rdef ->
405 406 407 408 409 410 411 412 413 414 415 416
        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
        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
417 418 419 420
    | Lany (rs, res, []) when functor_arg ->
        fprintf fmt "@[<hov 2>val %a : %a@]"
          (print_lident info) rs.rs_name
          (print_ty info) res;
Mário Pereira's avatar
Mário Pereira committed
421
    | Lany (rs, res, args) when functor_arg ->
422 423 424 425 426 427 428
        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
429
    | Lany (rs, _, _) -> check_val_in_drv info rs
Mário Pereira's avatar
Mário Pereira committed
430

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

551
  and print_branch info fmt (p, e) =
552
    fprintf fmt "@[<hov 2>| %a ->@ @[%a@]@]"
Mário Pereira's avatar
Mário Pereira committed
553 554
      (print_pat info) p (print_expr info) e;
    forget_pat p
555

Mário Pereira's avatar
Mário Pereira committed
556 557 558
  and print_raise ~paren info xs fmt e_opt =
    match query_syntax info.info_syn xs.xs_name, e_opt with
    | Some s, None ->
559
        fprintf fmt "raise (%s)" s
Mário Pereira's avatar
Mário Pereira committed
560
    | Some s, Some e ->
561 562
        fprintf fmt (protect_on paren "raise (%a)")
          (syntax_arguments s (print_expr info)) [e]
Mário Pereira's avatar
Mário Pereira committed
563
    | None, None ->
564 565
        fprintf fmt (protect_on paren "raise %a")
          (print_uident info) xs.xs_name
Mário Pereira's avatar
Mário Pereira committed
566
    | None, Some e ->
567 568
        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
569

570 571 572 573
  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
574
    match query_syntax info.info_syn xs.xs_name, pvl with
575 576 577 578 579 580 581 582 583 584 585
    | 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
586

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

618 619 620
  let rec is_signature_decl info = function
    | Dtype _ -> true
    | Dlet (Lany _) -> true
621
    | Dlet (Lvar (_, {e_node = Eany _})) -> true
622 623 624 625 626 627 628 629 630 631 632 633
    | 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 ->
634
          extract ((x, dlx) :: args) dl
635 636 637
      | dl -> List.rev args, dl in
    extract [] dl

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

  and print_functor_args info fmt args =
    let print_sig info fmt dl =
      fprintf fmt "sig@ %a@ end"
658
        (print_list newline (print_decl info ~functor_arg:true)) dl in
Mário Pereira's avatar
Mário Pereira committed
659
    let print_pair fmt (s, dl) =
660
      let info = { info with info_current_ph = s :: info.info_current_ph } in
Mário Pereira's avatar
Mário Pereira committed
661
      fprintf fmt "(%s:@ %a)" s (print_sig info) dl in
662
    fprintf fmt "%a" (print_list space print_pair) args
Mário Pereira's avatar
Mário Pereira committed
663 664

  let print_decl info fmt decl =
665 666
    (* avoids printing the same decl for mutually recursive decls *)
    let memo = Hashtbl.create 64 in
Mário Pereira's avatar
Mário Pereira committed
667 668
    let decl_name = get_decl_name decl in
    let decide_print id =
669 670 671
      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
672
        fprintf fmt "@\n@." end in
Mário Pereira's avatar
Mário Pereira committed
673 674
    List.iter decide_print decl_name

Mário Pereira's avatar
Mário Pereira committed
675 676
end

677 678 679 680 681 682 683
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;
684
      info_literal      = pargs.Pdriver.literal;
685 686 687 688 689
      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;
690 691
      info_flat         = flat;
      info_current_ph   = [];
692
    } in
693 694
    if not (Hashtbl.mem memo d) then begin Hashtbl.add memo d ();
      Print.print_decl info fmt d end
695

696
let fg ?fname m =
Mário Pereira's avatar
Mário Pereira committed
697 698 699
  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"
700

701
let () = Pdriver.register_printer "ocaml"
702
    ~desc:"printer for OCaml code" fg print_decl