ocaml_printer.ml 31.4 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-2019   --   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
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
  info_flat         : bool;
37
  info_prec         : int list Mid.t;
38
  info_current_ph   : string list; (* current path *)
Mário Pereira's avatar
Mário Pereira committed
39
}
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59

(* operator precedence, from http://caml.inria.fr/pub/docs/manual-ocaml/expr.html
   ! ? ~ ...   | 1
   . .( .[ .~  | 2
   #...        | 3
   fun/cstr app| 4 left
   -_ -._      | 5
   ** lsl lsr  | 6 right
   * / %       | 7 left
   + -         | 8 left
   ::          | 9 right
   @ ^         | 10 right
   = < > !=    | 11 left
   & &&        | 12 right
   or ||       | 13 right
   ,           | 14
   <- :=       | 15 right
   if          | 16
   ;           | 17 right
   let fun try | 18 *)
Mário Pereira's avatar
Mário Pereira committed
60

Mário Pereira's avatar
Mário Pereira committed
61 62
module Print = struct

63
  open Mltree
Mário Pereira's avatar
Mário Pereira committed
64

Andrei Paskevich's avatar
Andrei Paskevich committed
65 66 67 68
  (* extraction attributes *)
  let optional_arg = create_attribute "ocaml:optional"
  let named_arg = create_attribute "ocaml:named"
  let ocaml_remove = create_attribute "ocaml:remove"
69

Andrei Paskevich's avatar
Andrei Paskevich committed
70 71
  let is_optional ~attrs =
    Sattr.mem optional_arg attrs
72

Andrei Paskevich's avatar
Andrei Paskevich committed
73 74
  let is_named ~attrs =
    Sattr.mem named_arg attrs
75

Andrei Paskevich's avatar
Andrei Paskevich committed
76 77
  let is_ocaml_remove ~attrs =
    Ident.Sattr.mem ocaml_remove attrs
78

Mário Pereira's avatar
Mário Pereira committed
79 80 81 82 83 84 85 86 87 88 89
  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
90
  let _is_ocaml_keyword =
91 92 93 94
    let h = Hstr.create 16 in
    List.iter (fun s -> Hstr.add h s ()) ocaml_keywords;
    Hstr.mem h

95 96 97
  let char_to_alnumusquote c =
    match c with '\'' -> "\'" | _ -> char_to_alnumus c

98 99 100 101
  (* iprinter: local names
     aprinter: type variables
     tprinter: toplevel definitions *)
  let iprinter, aprinter, tprinter =
102 103
    let isanitize = sanitizer char_to_alnumus char_to_alnumusquote in
    let lsanitize = sanitizer char_to_lalnumus char_to_alnumusquote in
Mário Pereira's avatar
Mário Pereira committed
104
    create_ident_printer ocaml_keywords ~sanitizer:isanitize,
105
    create_ident_printer ocaml_keywords ~sanitizer:lsanitize,
Mário Pereira's avatar
Mário Pereira committed
106
    create_ident_printer ocaml_keywords ~sanitizer:lsanitize
Mário Pereira's avatar
Mário Pereira committed
107

Mário Pereira's avatar
Mário Pereira committed
108
  let forget_id id = forget_id iprinter id
Mário Pereira's avatar
Mário Pereira committed
109
  let _forget_ids = List.iter forget_id
Mário Pereira's avatar
Mário Pereira committed
110 111 112
  let forget_var (id, _, _) = forget_id id
  let forget_vars = List.iter forget_var

Mário Pereira's avatar
Mário Pereira committed
113
  let forget_let_defn = function
114
    | Lvar (v,_) -> forget_id v.pv_vs.vs_name
MARCHE Claude's avatar
MARCHE Claude committed
115
    | Lsym (s,_,_,_,_) | Lany (s,_,_,_) -> forget_rs s
116
    | Lrec rdl -> List.iter (fun fd -> forget_rs fd.rec_sym) rdl
Mário Pereira's avatar
Mário Pereira committed
117

Mário Pereira's avatar
Mário Pereira committed
118 119
  let rec forget_pat = function
    | Pwild -> ()
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
120
    | Pvar {vs_name=id} -> forget_id id
Mário Pereira's avatar
Mário Pereira committed
121 122 123 124
    | Papp (_, pl) | Ptuple pl -> List.iter forget_pat pl
    | Por (p1, p2) -> forget_pat p1; forget_pat p2
    | Pas (p, _) -> forget_pat p

125 126 127
  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
128 129
    fprintf fmt "%s" s

130 131 132 133 134
  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, _  ->
135 136
        fprintf fmt "%a.%a"
          (print_list dot string) q (print_global_ident ~sanitizer) id
137

138 139 140 141 142
  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

143 144
  let is_local_id info id =
    Sid.mem id info.info_current_th.th_local ||
Mário Pereira's avatar
Mário Pereira committed
145
    Opt.fold (fun _ m -> Sid.mem id m.Pmodule.mod_local)
146 147
      false info.info_current_mo

148 149
  exception Local

150
  let print_qident ~sanitizer info fmt id =
Mário Pereira's avatar
Mário Pereira committed
151
    try
152
      if info.info_flat then raise Not_found;
153
      if is_local_id info id then raise Local;
154 155
      let p, t, q =
        try Pmodule.restore_path id with Not_found -> Theory.restore_path id in
156 157
      let fname = if p = [] then info.info_fname else None in
      let m = Strings.capitalize (module_name ?fname p t) in
158
      fprintf fmt "%s.%a" m (print_path ~sanitizer) (q, id)
159
    with
160
    | Not_found ->
161 162
        let s = id_unique ~sanitizer iprinter id in
        fprintf fmt "%s" s
163
    | Local ->
164 165 166 167 168
        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)
169 170 171

  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
172

MARCHE Claude's avatar
MARCHE Claude committed
173
  let print_tv ~use_quote fmt tv =
Mário Pereira's avatar
Mário Pereira committed
174 175
    fprintf fmt (if use_quote then "'%s" else "%s")
      (id_unique aprinter tv.tv_name)
Mário Pereira's avatar
Mário Pereira committed
176

177
  let protect_on ?(boxed=false) ?(be=false) b s =
178 179 180
    if b
    then if be
         then "begin@;<1 2>@["^^ s ^^ "@] end"
181 182
         else "@[<1>(" ^^ s ^^ ")@]"
    else if not boxed then "@[<hv>" ^^ s ^^ "@]"
183
    else s
184

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

Mário Pereira's avatar
Mário Pereira committed
187 188
  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
189
    | [x1], [x2] ->
190
        print1 fmt x1; sep_m fmt (); print2 fmt x2
Mário Pereira's avatar
Mário Pereira committed
191
    | x1 :: r1, x2 :: r2 ->
192 193
        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
194 195
    | _ -> ()

Mário Pereira's avatar
Mário Pereira committed
196 197
  let print_rs info fmt rs =
    fprintf fmt "%a" (print_lident info) rs.rs_name
Mário Pereira's avatar
Mário Pereira committed
198

199 200
  let complex_syntax s =
    String.contains s '%' || String.contains s ' ' || String.contains s '('
Mário Pereira's avatar
Mário Pereira committed
201

202 203
  (** Types *)

MARCHE Claude's avatar
MARCHE Claude committed
204
  let rec print_ty ~use_quote ?(paren=false) info fmt = function
205
    | Tvar tv ->
MARCHE Claude's avatar
MARCHE Claude committed
206
        print_tv ~use_quote fmt tv
Mário Pereira's avatar
Mário Pereira committed
207
    | Ttuple [] ->
208
        fprintf fmt "unit"
Mário Pereira's avatar
Mário Pereira committed
209
    | Ttuple [t] ->
MARCHE Claude's avatar
MARCHE Claude committed
210
        print_ty  ~use_quote ~paren info fmt t
Mário Pereira's avatar
Mário Pereira committed
211
    | Ttuple tl ->
212
        fprintf fmt (protect_on paren "@[%a@]")
MARCHE Claude's avatar
MARCHE Claude committed
213
          (print_list star (print_ty ~use_quote ~paren:true info)) tl
Mário Pereira's avatar
Mário Pereira committed
214
    | Tapp (ts, tl) ->
215
        match query_syntax info.info_syn ts with
216
        | Some s when complex_syntax s ->
217
            fprintf fmt (protect_on paren "%a")
MARCHE Claude's avatar
MARCHE Claude committed
218
              (syntax_arguments s (print_ty ~use_quote ~paren:true info)) tl
219 220 221 222
        | Some s ->
           fprintf fmt (protect_on paren "%a%s")
             (print_list_suf space (print_ty ~use_quote ~paren:true info)) tl
             s
223 224 225 226 227 228
        | None   ->
            match tl with
            | [] ->
                (print_lident info) fmt ts
            | [ty] ->
                fprintf fmt (protect_on paren "%a@ %a")
Mário Pereira's avatar
Mário Pereira committed
229 230
                  (print_ty ~use_quote ~paren:true info) ty (print_lident info)
                  ts
231 232
            | tl ->
                fprintf fmt (protect_on paren "(%a)@ %a")
MARCHE Claude's avatar
MARCHE Claude committed
233
                  (print_list comma (print_ty ~use_quote ~paren:false info)) tl
234
                  (print_lident info) ts
Mario Pereira's avatar
Mario Pereira committed
235

Mário Pereira's avatar
Mário Pereira committed
236
  let print_vsty_opt info fmt id ty =
237
    fprintf fmt "?%s:(%a:@ %a)" id.id_string (print_lident info) id
MARCHE Claude's avatar
MARCHE Claude committed
238
      (print_ty ~use_quote:false ~paren:false info) ty
Mário Pereira's avatar
Mário Pereira committed
239

Mário Pereira's avatar
Mário Pereira committed
240 241 242
  let print_vs_opt info fmt id =
    fprintf fmt "?%s:%a" id.id_string (print_lident info) id

Mário Pereira's avatar
Mário Pereira committed
243
  let print_vsty_named info fmt id ty =
244
    fprintf fmt "~%s:(%a:@ %a)" id.id_string (print_lident info) id
MARCHE Claude's avatar
MARCHE Claude committed
245
      (print_ty ~use_quote:false ~paren:false info) ty
Mário Pereira's avatar
Mário Pereira committed
246

Mário Pereira's avatar
Mário Pereira committed
247 248 249
  let print_vs_named info fmt id =
    fprintf fmt "~%s:%a" id.id_string (print_lident info) id

Mário Pereira's avatar
Mário Pereira committed
250
  let print_vsty info fmt (id, ty, _) =
Andrei Paskevich's avatar
Andrei Paskevich committed
251 252 253
    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
254
    else fprintf fmt "(%a:@ %a)" (print_lident info) id
Mário Pereira's avatar
Mário Pereira committed
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278
      (print_ty ~use_quote:false ~paren:false info) ty

  let print_vsty_opt_fun info fmt id = function
    | Tapp (id_ty, [arg]) ->
        assert (query_syntax info.info_syn id_ty = Some "%1 option");
        fprintf fmt "?%s:%a" id.id_string
          (print_ty ~use_quote:false ~paren:false info) arg
    | _ -> invalid_arg "print_vsty_opt_fun" (*FIXME : better error message *)

  let print_vsty_named_fun info fmt id ty =
    fprintf fmt "%s:%a" id.id_string
      (print_ty ~use_quote:false ~paren:false info) ty

  let print_vsty_fun info fmt (id, ty, _) =
    let attrs = id.id_attrs in
    if is_optional ~attrs then print_vsty_opt_fun info fmt id ty
    else if is_named ~attrs then print_vsty_named_fun info fmt id ty
    else fprintf fmt "%a" (print_ty ~use_quote:false ~paren:true info) ty

  let print_vs_fun info fmt id =
    let attrs = id.id_attrs in
    if is_optional ~attrs then print_vs_opt info fmt id
    else if is_named ~attrs then print_vs_named info fmt id
    else print_lident info fmt id
279

Mário Pereira's avatar
Mário Pereira committed
280
  let print_tv_arg = print_tv
MARCHE Claude's avatar
MARCHE Claude committed
281
  let print_tv_args ~use_quote fmt = function
282
    | []   -> ()
MARCHE Claude's avatar
MARCHE Claude committed
283
    | [tv] -> fprintf fmt "%a@ " (print_tv_arg ~use_quote) tv
Mário Pereira's avatar
Mário Pereira committed
284 285
    | tvl  ->
        fprintf fmt "(%a)@ " (print_list comma (print_tv_arg ~use_quote)) tvl
Mário Pereira's avatar
Mário Pereira committed
286

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

Mário Pereira's avatar
Mário Pereira committed
290 291 292
  let get_record info rs =
    match Mid.find_opt rs.rs_name info.info_mo_known_map with
    | Some {pd_node = PDtype itdl} ->
293 294 295 296
        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
297 298
    | _ -> []

299
  let rec print_pat ?(paren=false) info fmt = function
300
    | Pwild ->
301
        fprintf fmt "_"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
302
    | Pvar {vs_name=id} ->
303
        (print_lident info) fmt id
304
    | Pas (p, {vs_name=id}) ->
305 306
        fprintf fmt (protect_on paren "%a as %a") (print_pat info) p
          (print_lident info) id
307
    | Por (p1, p2) ->
308 309
        fprintf fmt (protect_on paren "%a | %a") (print_pat info) p1
          (print_pat info) p2
310
    | Ptuple pl ->
311
        fprintf fmt "(%a)" (print_list comma (print_pat ~paren:true info)) pl
Mário Pereira's avatar
Mário Pereira committed
312
    | Papp (ls, pl) ->
313 314 315 316 317 318 319
        match query_syntax info.info_syn ls.ls_name with
        | Some s when complex_syntax s || pl = [] ->
           syntax_arguments s (print_pat info) fmt pl
        | Some s ->
           fprintf fmt (protect_on paren "%s (%a)")
             s (print_list comma (print_pat ~paren:true info)) pl
        | None ->
320 321 322
            let pjl = let rs = restore_rs ls in get_record info rs in
            match pjl with
            | []  -> print_papp info ls fmt pl
323 324 325 326
            | 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
327 328 329 330

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

335 336
  (** Expressions *)

337
  let pv_name pv = pv.pv_vs.vs_name
338
  let print_pv info fmt pv = print_lident info fmt (pv_name pv)
339

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
340
  (* FIXME put these in Compile*)
341 342 343 344 345 346 347 348
  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

349
  let check_val_in_drv info loc id =
350
    (* here [rs] refers to a [val] declaration *)
351
    match query_syntax info.info_syn id with
352
    | None (* when info.info_flat *) ->
353
        Loc.errorm ?loc "Symbol %a cannot be extracted" (print_lident info) id
354
    | _ -> ()
355

Mário Pereira's avatar
Mário Pereira committed
356 357
  let is_mapped_to_int info ity =
    match ity.ity_node with
358 359 360 361
    | Ityapp ({ its_ts = ts }, _, _) ->
        query_syntax info.info_syn ts.ts_name = Some "int"
    | _ -> false

362 363
  let print_constant fmt e = begin match e.e_node with
    | Econst c ->
364 365 366
        let v = c.Number.il_int in
        let s = BigInt.to_string v in
        if BigInt.lt v BigInt.zero then fprintf fmt "(%s)" s
367 368 369
        else fprintf fmt "%s" s
    | _ -> assert false end

370 371 372 373
  let print_for_direction fmt = function
    | To     -> fprintf fmt "to"
    | DownTo -> fprintf fmt "downto"

Mário Pereira's avatar
Mário Pereira committed
374
  let rec print_apply_args info fmt = function
375
    | expr :: exprl, pv :: pvl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
376
        if is_optional ~attrs:(pv_name pv).id_attrs then
377 378 379 380
          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
381
                     (print_expr info 1) expr end
Andrei Paskevich's avatar
Andrei Paskevich committed
382
        else if is_named ~attrs:(pv_name pv).id_attrs then
383
          fprintf fmt "~%s:%a" (pv_name pv).id_string
384 385
            (print_expr info 1) expr
        else fprintf fmt "%a" (print_expr info 3) expr;
386 387
        if exprl <> [] then fprintf fmt "@ ";
        print_apply_args info fmt (exprl, pvl)
388
    | expr :: exprl, [] ->
389
        fprintf fmt "%a" (print_expr info 3) expr;
390
        print_apply_args info fmt (exprl, [])
391
    | [], _ -> ()
Mário Pereira's avatar
Mário Pereira committed
392

393
  and print_apply info rs fmt pvl =
394
    let isfield =
395
      match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
396
      | None   -> false
397 398 399 400
      | Some _ -> true in
    let isconstructor () =
      match Mid.find_opt rs.rs_name info.info_mo_known_map with
      | Some {pd_node = PDtype its} ->
401 402 403
          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
404
      | _ -> false in
405
    match query_syntax info.info_syn rs.rs_name, pvl with
406
    | Some s, _ when complex_syntax s || pvl = [] ->
407 408
       let p = Mid.find rs.rs_name info.info_prec in
       syntax_arguments_prec s (print_expr info) p fmt pvl
409 410 411 412
    | Some s, _ ->
       fprintf fmt "@[<hov 2>%s %a@]"
         s
         (print_apply_args info) (pvl, rs.rs_cty.cty_args)
413
    | None, [t] when is_rs_tuple rs ->
414
        fprintf fmt "@[%a@]" (print_expr info 1) t
415
    | None, tl when is_rs_tuple rs ->
416
        fprintf fmt "@[(%a)@]" (print_list comma (print_expr info 14)) tl
417
    | None, [t1] when isfield ->
Mário Pereira's avatar
Mário Pereira committed
418 419
        fprintf fmt "%a.%a" (print_expr info 2) t1 (print_lident info)
          rs.rs_name
420
    | None, tl when isconstructor () ->
421 422 423 424 425 426
        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
427
                (print_expr info 2) t
428 429
          | [], tl ->
              fprintf fmt "@[<hov 2>%a (%a)@]" (print_uident info) rs.rs_name
430
                (print_list comma (print_expr info 14)) tl
431 432 433
          | pjl, tl -> let equal fmt () = fprintf fmt " =@ " in
              fprintf fmt "@[<hov 2>{ %a }@]"
                (print_list2 semi equal (print_rs info)
434
                   (print_expr info 17)) (pjl, tl) end
435
    | None, [] ->
436
        (print_lident info) fmt rs.rs_name
437
    | _, tl ->
438 439 440
        fprintf fmt "@[<hov 2>%a %a@]"
          (print_lident info) rs.rs_name
          (print_apply_args info) (tl, rs.rs_cty.cty_args)
441

442
  and print_svar fmt s =
443
    print_list space (print_tv ~use_quote:false) fmt (Stv.elements s)
444

445
  and print_fun_type_args info fmt (args, s, res, e) =
446
    if Stv.is_empty s then
447
      fprintf fmt "@[%a@]:@ %a@ =@ @[<hv>%a@]"
448
        (print_list_suf space (print_vs_arg info)) args
MARCHE Claude's avatar
MARCHE Claude committed
449
        (print_ty ~use_quote:false info) res
450
        (print_expr ~opr:false info 18) e
451 452
    else
      let id_args = List.map (fun (id, _, _) -> id) args in
453
      let arrow fmt () = fprintf fmt " ->@ " in
MARCHE Claude's avatar
MARCHE Claude committed
454 455
      let start fmt () = fprintf fmt "fun@ " in
      fprintf fmt ":@ @[<h>type @[%a@]. @[%a@ %a@]@] =@ \
456
                   @[<hv 2>@[%a@]%a@]"
457
        print_svar s
Mário Pereira's avatar
Mário Pereira committed
458
        (print_list_suf arrow (print_vsty_fun info)) args
MARCHE Claude's avatar
MARCHE Claude committed
459
        (print_ty ~use_quote:false ~paren:true info) res
Mário Pereira's avatar
Mário Pereira committed
460 461
        (print_list_delim ~start ~stop:arrow ~sep:space (print_vs_fun info))
          id_args
462
        (print_expr ~opr:false info 18) e
463

464
  and print_let_def ?(functor_arg=false) info fmt = function
Mário Pereira's avatar
Mário Pereira committed
465
    | Lvar (pv, e) ->
466
        fprintf fmt "@[<hov 2>let %a =@ %a@]"
467
          (print_lident info) (pv_name pv) (print_expr ~opr:false info 18) e
MARCHE Claude's avatar
MARCHE Claude committed
468 469
    | Lsym (rs, svar, res, args, ef) ->
        fprintf fmt "@[<hov 2>let %a %a@]"
470
          (print_lident info) rs.rs_name
MARCHE Claude's avatar
MARCHE Claude committed
471 472
          (print_fun_type_args info) (args,svar,res,ef);
       forget_vars args
473
    | Lrec rdef ->
474 475 476 477 478 479 480
        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);
481
              forget_vars args in
482
        print_list_next newline print_one fmt rdef;
MARCHE Claude's avatar
MARCHE Claude committed
483
    | Lany (rs, _svar, res, []) when functor_arg ->
484 485
        fprintf fmt "@[<hov 2>val %a : %a@]"
          (print_lident info) rs.rs_name
MARCHE Claude's avatar
MARCHE Claude committed
486 487
          (print_ty ~use_quote:true info) res;
    | Lany (rs, _svar, res, args) when functor_arg ->
488
        let print_ty_arg info fmt (_, ty, _) =
MARCHE Claude's avatar
MARCHE Claude committed
489
          fprintf fmt "@[%a@]" (print_ty ~use_quote:true info) ty in
490 491 492
        fprintf fmt "@[<hov 2>val %a : @[%a@] ->@ %a@]"
          (print_lident info) rs.rs_name
          (print_list arrow (print_ty_arg info)) args
MARCHE Claude's avatar
MARCHE Claude committed
493
          (print_ty ~use_quote:true info) res;
494
        forget_vars args
MARCHE Claude's avatar
MARCHE Claude committed
495
    | Lany ({rs_name}, _, _, _) -> check_val_in_drv info rs_name.id_loc rs_name
Mário Pereira's avatar
Mário Pereira committed
496

497 498 499
  and print_expr ?(boxed=false) ?(opr=true) ?(be=false) info prec fmt e =
    let protect_on_be ?(boxed=false) b s = protect_on ~boxed ~be:true b s in
    let protect_on ?(boxed=false) b s = protect_on ~boxed ~be b s in
500
    match e.e_node with
501
    | Econst c ->
502
        let n = c.Number.il_int in
503 504 505 506 507 508
        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]
509 510
         | None when n = "0" -> fprintf fmt "Z.zero"
         | None when n = "1" -> fprintf fmt "Z.one"
511
         | None   -> fprintf fmt (protect_on (prec < 4) "Z.of_string \"%s\"") n)
512
    | Evar pvs ->
513
        (print_lident info) fmt (pv_name pvs)
Mário Pereira's avatar
Mário Pereira committed
514
    | Elet (let_def, e) ->
515 516
        fprintf fmt (protect_on ~boxed (opr && prec < 18) "@[%a in@]@;%a")
          (print_let_def info) let_def (print_expr ~boxed:true ~opr info 18) e;
517
        forget_let_defn let_def
518
    | Eabsurd ->
519
        fprintf fmt (protect_on (opr && prec < 4) "assert false (* absurd *)")
Mário Pereira's avatar
Mário Pereira committed
520
    | Eapp (rs, []) when rs_equal rs rs_true ->
521
        fprintf fmt "true"
Mário Pereira's avatar
Mário Pereira committed
522
    | Eapp (rs, []) when rs_equal rs rs_false ->
523
        fprintf fmt "false"
524
    | Eapp (rs, [])  -> (* avoids parenthesis around values *)
525
        fprintf fmt "%a" (print_apply info rs) []
Mário Pereira's avatar
Mário Pereira committed
526
    | Eapp (rs, pvl) ->
527
       fprintf fmt (protect_on (prec < 4) "%a") (print_apply info rs) pvl
528
    | Ematch (e1, [p, e2], []) ->
529 530 531
        fprintf fmt (protect_on (opr && prec < 18) "let %a =@ %a in@ %a")
          (print_pat info) p (print_expr ~opr:false info 18) e1
          (print_expr ~opr info 18) e2
532
    | Ematch (e, pl, []) ->
533
        fprintf fmt
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
534 535 536
          (if prec < 18 && opr
           then "@[<hv>@[<hv 2>begin@ match@ %a@]@ with@]@\n@[<hv>%a@]@\nend"
           else "@[<hv>@[<hv 2>match@ %a@]@ with@]@\n@[<hv>%a@]")
537 538
          (print_expr info 18) e
          (print_list newline (print_branch info)) pl
539
    | Eassign al ->
540
        let assign fmt (rho, rs, e) =
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
541
          fprintf fmt "@[<hv 2>%a.%a <-@ %a@]"
542
            (print_lident info) (pv_name rho) (print_lident info) rs.rs_name
543
            (print_expr info 15) e in
544 545 546
        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
547
    | Eif (e1, e2, {e_node = Eblock []}) ->
548
        fprintf fmt
549
          (protect_on (opr && prec < 16)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
550
             "@[<hv>@[<hv 2>if@ %a@]@ then %a@]")
551
          (print_expr ~opr:false info 15) e1 (print_expr ~be:true info 15) e2
Mário Pereira's avatar
Mário Pereira committed
552
    | Eif (e1, e2, e3) when is_false e2 && is_true e3 ->
553
        fprintf fmt (protect_on (prec < 4) "not %a")
554
          (print_expr info 3) e1
555
    | Eif (e1, e2, e3) when is_true e2 ->
556
        fprintf fmt (protect_on (prec < 13) "@[<hv>%a || %a@]")
557
          (print_expr info 12) e1 (print_expr info 13) e3
558
    | Eif (e1, e2, e3) when is_false e3 ->
559
        fprintf fmt (protect_on (prec < 12) "@[<hv>%a && %a@]")
560
          (print_expr info 11) e1 (print_expr info 12) e2
561
    | Eif (e1, e2, e3) ->
562
        fprintf fmt (protect_on (opr && prec < 16)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
563 564 565
                       "@[<hv>@[<hv>if %a@]\
                        @;<1 0>@[<hv 2>then@;%a@]\
                        @;<1 0>@[<hv 2>else@;%a@]@]")
566 567 568
          (print_expr ~opr:false info 15) e1
          (print_expr ~opr:false ~be:true info 15) e2
          (print_expr ~be:true info 15) e3
569
    | Eblock [] ->
570
        fprintf fmt "()"
571
    | Eblock [e] ->
572
        print_expr ~be info prec fmt e
573
    | Eblock el ->
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
574
        let semibreak fmt () = fprintf fmt ";@ " in
575 576 577
        let rec aux fmt = function
          | [] -> assert false
          | [e] -> print_expr ~opr:false info 18 fmt e
578 579 580
          | h::t -> print_expr info 17 fmt h; semibreak fmt (); aux fmt t in
        fprintf fmt
          (if prec < 17
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
581 582
           then "@[<hv>begin@;<1 2>@[<hv>%a@]@ end@]"
           else "@[<hv>@[<hv>%a@]@]") aux el
583
    | Efun (varl, e) ->
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
584
        fprintf fmt (protect_on (opr && prec < 18) "@[<hv 2>fun %a ->@ %a@]")
585
          (print_list space (print_vs_arg info)) varl (print_expr info 17) e
Mário Pereira's avatar
Mário Pereira committed
586
    | Ewhile (e1, e2) ->
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
587
        fprintf fmt "@[<hv 2>while %a do@\n%a@;<1 -2>done@]"
588
          (print_expr info 18) e1 (print_expr ~opr:false info 18) e2
Mário Pereira's avatar
Mário Pereira committed
589
    | Eraise (xs, e_opt) ->
590
        print_raise ~paren:(prec < 4) info xs fmt e_opt
591
    | Efor (pv1, pv2, dir, pv3, e) ->
Mário Pereira's avatar
Mário Pereira committed
592
        if is_mapped_to_int info pv1.pv_ity then begin
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
593
          fprintf fmt "@[<hv 2>for %a = %a %a %a do@ @[%a@]@ done@]"
594 595
            (print_lident info) (pv_name pv1) (print_lident info) (pv_name pv2)
            print_for_direction dir (print_lident info) (pv_name pv3)
596
            (print_expr ~opr:false info 18) e;
Mário Pereira's avatar
Mário Pereira committed
597
          forget_pv pv1 end
598 599 600 601 602
        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
603
          fprintf fmt (protect_on_be (opr && prec < 18)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
604 605 606
                         "@[<hv 2>let rec %a %a =@ \
                          @[<hv 2>if %s %a %a@]@;<1 0>\
                          @[<hv 2>then begin@ %a;@ %a (%s %a)@;<1 -2>end@]@;<1 -2>in %a %a@]")
607 608
          (* let rec *) (print_lident info) for_id (print_pv info) pv1
          (* if      *)  cmp (print_pv info) pv1 (print_pv info) pv3
609
          (* then    *) (print_expr info 16) e (print_lident info) for_id
610 611
                        op (print_pv info) pv1
          (* in      *) (print_lident info) for_id (print_pv info) pv2
612
    | Ematch (e, [], xl) ->
613 614
        fprintf fmt
          (if prec < 18 && opr
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
615 616
           then "@[<hv>@[<hv 2>begin@ try@ %a@]@ with@]@\n@[<hv>%a@]@\nend"
           else "@[<hv>@[<hv 2>try@ %a@]@ with@]@\n@[<hv>%a@]")
617 618
          (print_expr ~be:true ~opr:false info 17) e
          (print_list newline (print_xbranch info false)) xl
619
    | Ematch (e, bl, xl) ->
620
        fprintf fmt
621
          (if (prec < 18 && opr)
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
622 623
           then "@[begin match @[%a@]@ with@]@\n@[<hv>%a@\n%a@]@\nend"
           else "@[<hv>match @[%a@]@ with@]@\n@[<hv>%a@\n%a@]")
624 625
          (print_expr ~be:true ~opr:false info 17) e
          (print_list newline (print_branch info)) bl
626
          (print_list newline (print_xbranch info true)) xl
627
    | Eexn (xs, None, e) ->
628
        fprintf fmt "@[<hv>let exception %a in@\n%a@]"
629
          (print_uident info) xs.xs_name (print_expr info 18) e
630
    | Eexn (xs, Some t, e) ->
631
        fprintf fmt "@[<hv>let exception %a of %a in@\n%a@]"
MARCHE Claude's avatar
MARCHE Claude committed
632
          (print_uident info) xs.xs_name (print_ty ~use_quote:false ~paren:true info) t
633
          (print_expr info 18) e
634 635 636
    | Eignore e ->
        fprintf fmt (protect_on (prec < 4)"ignore %a")
          (print_expr info 4) e
Mário Pereira's avatar
Mário Pereira committed
637

638
  and print_branch info fmt (p, e) =
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
639
    fprintf fmt "@[<hv 2>| %a ->@ @[%a@]@]"
640
      (print_pat info) p (print_expr info 17) e;
Mário Pereira's avatar
Mário Pereira committed
641
    forget_pat p
642

Mário Pereira's avatar
Mário Pereira committed
643 644 645
  and print_raise ~paren info xs fmt e_opt =
    match query_syntax info.info_syn xs.xs_name, e_opt with
    | Some s, None ->
646
        fprintf fmt "raise (%s)" s
647
    | Some s, Some e when complex_syntax s ->
648
        fprintf fmt (protect_on paren "raise %a")
649 650 651 652
          (syntax_arguments_prec s (print_expr info) []) [e]
    | Some s, Some e ->
        fprintf fmt (protect_on paren "raise (%s %a)")
          s (print_expr info 3) e
Mário Pereira's avatar
Mário Pereira committed
653
    | None, None ->
654 655
        fprintf fmt (protect_on paren "raise %a")
          (print_uident info) xs.xs_name
Mário Pereira's avatar
Mário Pereira committed
656
    | None, Some e ->
657
        fprintf fmt (protect_on paren "raise (%a %a)")
658
          (print_uident info) xs.xs_name (print_expr info 3) e
Mário Pereira's avatar
Mário Pereira committed
659

660 661 662 663
  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
664
    match query_syntax info.info_syn xs.xs_name, pvl with
665 666 667 668 669 670 671
    | Some s, _ when complex_syntax s || pvl = [] ->
        fprintf fmt "@[<hov 4>| %a%a ->@ %a@]"
          print_exn () (syntax_arguments s print_var) pvl
          (print_expr info 17) e
    | Some s, _ -> fprintf fmt "@[<hov 4>| %a%s (%a) ->@ %a@]"
        print_exn () s
        (print_list comma print_var) pvl (print_expr info 17) e
672
    | None, [] -> fprintf fmt "@[<hov 4>| %a%a ->@ %a@]"
673
        print_exn () (print_uident info) xs.xs_name (print_expr info 17) e
674 675
    | None, [pv] -> fprintf fmt "@[<hov 4>| %a%a %a ->@ %a@]"
        print_exn () (print_uident info) xs.xs_name print_var pv
676
        (print_expr info 17) e
677 678
    | None, pvl -> fprintf fmt "@[<hov 4>| %a%a (%a) ->@ %a@]"
        print_exn () (print_uident info) xs.xs_name
679
        (print_list comma print_var) pvl (print_expr info 17) e
Mário Pereira's avatar
Mário Pereira committed
680

Mário Pereira's avatar
Mário Pereira committed
681
  let print_type_decl info fst fmt its =
682 683
    let print_constr fmt (id, cs_args) =
      match cs_args with
Mário Pereira's avatar
Mário Pereira committed
684 685
      | [] -> fprintf fmt "@[<hov 4>| %a@]" (print_uident info) id
      | l -> fprintf fmt "@[<hov 4>| %a of %a@]" (print_uident info) id
MARCHE Claude's avatar
MARCHE Claude committed
686
               (print_list star (print_ty ~use_quote:true ~paren:false info)) l in
687
    let print_field fmt (is_mutable, id, ty) =
688
      fprintf fmt "%s%a: @[%a@];" (if is_mutable then "mutable " else "")
MARCHE Claude's avatar
MARCHE Claude committed
689
        (print_lident info) id (print_ty ~use_quote:true ~paren:false info) ty in
690
    let print_def fmt = function
691
      | None ->
692
          ()
693
      | Some (Ddata csl) ->
694
          fprintf fmt " =@\n%a" (print_list newline print_constr) csl
695
      | Some (Drecord fl) ->
696 697 698
          fprintf fmt " = %s{@\n%a@\n}"
            (if its.its_private then "private " else "")
            (print_list newline print_field) fl
699
      | Some (Dalias ty) ->
MARCHE Claude's avatar
MARCHE Claude committed
700
          fprintf fmt " =@ %a" (print_ty ~use_quote:true ~paren:false info) ty
701 702 703 704
      | Some (Drange _) ->
          fprintf fmt " =@ Z.t"
      | Some (Dfloat _) ->
          assert false (*TODO*)
705
    in
Andrei Paskevich's avatar
Andrei Paskevich committed
706 707
    let attrs = its.its_name.id_attrs in
    if not (is_ocaml_remove ~attrs) then
Mário Pereira's avatar
Mário Pereira committed
708
      fprintf fmt "@[<hov 2>@[%s %a%a@]%a@]"
MARCHE Claude's avatar
MARCHE Claude committed
709
        (if fst then "type" else "and") (print_tv_args ~use_quote:true) its.its_args
710
        (print_lident info) its.its_name print_def its.its_def
711

712 713 714
  let rec is_signature_decl info = function
    | Dtype _ -> true
    | Dlet (Lany _) -> true
715
    | Dval _ -> true
716 717 718 719 720 721 722 723 724
    | 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
725
      | Dmodule (_, []) :: dl -> extract args dl
726
      | Dmodule (x, dlx) :: dl when is_signature info dlx ->
727
          extract ((x, dlx) :: args) dl
728 729 730
      | dl -> List.rev args, dl in
    extract [] dl

731 732 733
  let print_top_val ?(functor_arg=false) info fmt ({pv_vs}, ty) =
    if functor_arg then
      fprintf fmt "@[<hov 2>val %a : %a@]"
MARCHE Claude's avatar
MARCHE Claude committed
734
        (print_lident info) pv_vs.vs_name (print_ty ~use_quote:true info) ty
735 736 737
    else
      check_val_in_drv info pv_vs.vs_name.id_loc pv_vs.vs_name

Mário Pereira's avatar
Mário Pereira committed
738
  let rec print_decl ?(functor_arg=false) info fmt = function
Mário Pereira's avatar
Mário Pereira committed
739
    | Dlet ldef ->
740
        print_let_def info ~functor_arg fmt ldef
741 742
    | Dval (pv, ty) ->
        print_top_val info ~functor_arg fmt (pv, ty)
743
    | Dtype dl ->
744
        print_list_next newline (print_type_decl info) fmt dl
745
    | Dexn (xs, None) ->
746
        fprintf fmt "exception %a" (print_uident info) xs.xs_name
Mário Pereira's avatar
Mário Pereira committed
747
    | Dexn (xs, Some t)->
748
        fprintf fmt "@[<hov 2>exception %a of %a@]"
MARCHE Claude's avatar
MARCHE Claude committed