mlw_ocaml.ml 39.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

12 13 14 15 16
(* TODO

  - no more parentheses in drivers (the printer will add them with protect_on)

  - driver uses %1, %2, etc. and translation eta-expanses if necessary
17
      introduce a let when %1 appears several times?
18 19 20 21 22 23

  - simplications
      let x = y in ...
      let x = 17 in ... (converter)
      let x = () in ...
      let f (us: unit) = ... (when variable us is not used)
24
      some beta-reductions, at least (fun _ -> e) ()
25 26 27 28

  - singleton types
    record/constructor fields of type unit

29 30
  - ghost code
    remove it as much as possible (in types and function arguments)
31

32 33
*)

34 35
open Format
open Pp
36
open Stdlib
37 38 39 40
open Ident
open Ty
open Term
open Theory
41
open Printer
42

43
let debug =
Andrei Paskevich's avatar
Andrei Paskevich committed
44 45
  Debug.register_info_flag "extraction"
    ~desc:"Print@ details@ of@ program@ extraction."
46

47 48 49 50
let clean_fname fname =
  let fname = Filename.basename fname in
  (try Filename.chop_extension fname with _ -> fname)

51 52
let modulename ?fname path t =
  let fname = match fname, path with
53
    | Some fname, _ -> clean_fname fname
54 55
    | None, [] -> "why3"
    | None, _ -> String.concat "__" path
56
  in
57
  fname ^ "__" ^ t
58

59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
(** Abstract syntax of ML *)

module ML = struct

  type ty =
    | Tvar    of ident
    | Tapp    of ident * ty list
    | Ttuple  of ty list
    | Tsyntax of string * ty list

  type var = ident * ty

  type pat =
    | Pwild
    | Pident  of ident
    | Papp    of ident * pat list
    | Ptuple  of pat list
    | Precord of (ident * pat) list
    | Psyntax of string * pat list
    | Por     of pat * pat
    | Pas     of pat * ident

  type is_rec = bool

  type binop = Band | Bor | Beq

  type for_direction = To | DownTo

  type exn =
    | Xident  of ident
    | Xsyntax of string
    | Xexit             (* Pervasives.Exit *)

  type expr =
    | Econst  of Number.integer_constant
    | Ebool   of bool
    | Eident  of ident
    | Esyntax of string * expr list
    | Eapp    of expr * expr list
    | Efun    of var list * expr
    | Elet    of ident * expr * expr
    | Eletrec of is_rec * (ident * var list * expr) list * expr
    | Eif     of expr * expr * expr
    | Ecast   of expr * ty
    | Etuple  of expr list (* at least 2 expressions *)
    | Econstr of ident * expr list
    | Ematch  of expr * (pat * expr) list
    | Ebinop  of expr * binop * expr
    | Enot    of expr
    | Eblock  of expr list
    | Ewhile  of expr * expr
    | Efor    of ident * ident * for_direction * ident * expr
    | Eraise  of exn * expr option
    | Etry    of expr * (exn * ident option * expr) list
    | Eabsurd
    (* records *)
    | Erecord   of (ident * expr) list
    | Egetfield of expr * ident
    | Esetfield of expr * ident * expr

  type is_mutable = bool

  type typedef =
    | Dabstract
    | Ddata     of (ident * ty list) list
    | Drecord   of (is_mutable * ident * ty) list
    | Dalias    of ty

  type decl =
    | Dtype of (ident * ident list * typedef) list
    | Dlet  of is_rec * (ident * var list * expr) list
        (* TODO add return type? *)
    | Dexn  of ident * ty option

  (** smart constructors *)

  let tunit = Ttuple []

  let enop = Eblock []

  let etuple = function
    | []  -> enop
    | [e] -> e
    | l   -> Etuple l

  let eseq e1 e2 = match e1, e2 with
    | Eblock [], e | e, Eblock [] -> e
    | Eblock l1, Eblock l2 -> Eblock (l1 @ l2)
    | _, Eblock l2 -> Eblock (e1 :: l2)
    | Eblock l1, _ -> Eblock (l1 @ [e2])
    | _ -> Eblock [e1; e2]

end

(** Translation from WhyML to ML *)
154 155

type info = {
156
  exec: Mlw_exec.t;
157
  info_syn: syntax_map;
158
  converters: syntax_map;
159
  current_theory: Theory.theory;
160
  current_module: Mlw_module.modul option;
161 162
  th_known_map: Decl.known_map;
  mo_known_map: Mlw_decl.known_map;
163
  fname: string option;
164
  unsafe_int: bool;
165 166
}

167 168 169
module Translate = struct

  open Decl
170

171 172
  let type_unit = ML.Ttuple []

173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190
  let rec type_ info ty = match ty.ty_node with
    | Tyvar v ->
        ML.Tvar v.tv_name
    | Tyapp (ts, tl) when is_ts_tuple ts ->
        ML.Ttuple (List.map (type_ info) tl)
    | Tyapp (ts, tl) ->
        begin match query_syntax info.info_syn ts.ts_name with
        | Some s -> ML.Tsyntax (s, List.map (type_ info) tl)
        | None -> ML.Tapp (ts.ts_name, List.map (type_ info) tl)
        end

  let vsty info vs = vs.vs_name, type_ info vs.vs_ty

  let has_syntax info id = Mid.mem id info.info_syn

  let get_record info ls =
    match Mid.find_opt ls.ls_name info.th_known_map with
      | Some { d_node = Ddata dl } ->
191
        let rec lookup = function
192 193 194 195
          | [] -> []
          | (_, [cs, pjl]) :: _ when ls_equal cs ls ->
            (try List.map Opt.get pjl with _ -> [])
          | _ :: dl -> lookup dl
196 197
        in
        lookup dl
198
      | Some _ | None ->
199
        []
200

201
  let type_decl info ts = match ts.ts_def with
Clément Fumex's avatar
Clément Fumex committed
202 203
    | NoDef | Range _ | Float _ ->
        (* FIXME: how should we extract Range and Float? *)
204
        ML.Dabstract
Clément Fumex's avatar
Clément Fumex committed
205
    | Alias ty ->
206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249
        ML.Dalias (type_ info ty)

  let type_args = List.map (fun tv -> tv.tv_name)

  let type_decl info ts =
    if has_syntax info ts.ts_name then [] else
    [ML.Dtype [ts.ts_name, type_args ts.ts_args, type_decl info ts]]

  let data_decl info (ts, csl) =
    let default () =
      let constr (cs, _) = cs.ls_name, List.map (type_ info) cs.ls_args in
      ML.Ddata (List.map constr csl) in
    let field ls = false, ls.ls_name, type_ info (Opt.get ls.ls_value) in
    let defn = function
      | [cs, _] ->
          let pjl = get_record info cs in
          if pjl = [] then default () else ML.Drecord (List.map field pjl)
      | _ ->
          default ()
    in
    ts.ts_name, type_args ts.ts_args, defn csl

  let data_decl info (ts, _ as d) =
    if has_syntax info ts.ts_name then [] else [data_decl info d]

  let projections _info (ts, csl) =
    let pjl = List.filter ((<>) None) (snd (List.hd csl)) in
    let pjl = List.map Opt.get pjl in
    let x = id_register (id_fresh "x") in
    let projection ls =
      let branch (cs, pjl) =
        let arg = function
          | Some ls' when ls_equal ls' ls -> ML.Pident x
          | _ -> ML.Pwild in
        ML.Papp (cs.ls_name, List.map arg pjl), ML.Eident x
      in
      let id = id_register (id_fresh "x") in
      let ty =
        ML.Tapp (ts.ts_name,
                 List.map (fun tv -> ML.Tvar tv.tv_name) ts.ts_args) in
      let def = ML.Ematch (ML.Eident id, List.map branch csl) in
      ML.Dlet (false, [ls.ls_name, [id, ty], def])
    in
    List.map projection pjl
250

251 252 253
  let is_record = function
    | _, [_, pjl] -> List.for_all ((<>) None) pjl
    | _ -> false
254

255 256 257 258
  let projections info (ts, _ as d) =
    if has_syntax info ts.ts_name || is_record d then []
    else projections info d

259
  let filter_ghost_fields ls def al =
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279
    let flt fd arg = if fd.Mlw_expr.fd_ghost then def else arg in
    try List.map2 flt (Mlw_expr.restore_pl ls).Mlw_expr.pl_args al
    with Not_found -> al

  let rec pat info p = match p.pat_node with
    | Pwild ->
        ML.Pwild
    | Pvar v ->
        ML.Pident v.vs_name
    | Pas (p, v) ->
        ML.Pas (pat info p, v.vs_name)
    | Por (p, q) ->
        ML.Por (pat info p, pat info q)
    | Papp (cs, pl) when is_fs_tuple cs ->
        ML.Ptuple (List.map (pat info) pl)
    | Papp (cs, pl) ->
        begin match query_syntax info.info_syn cs.ls_name with
        | Some s -> ML.Psyntax (s, List.map (pat info) pl)
        | None ->
          let pat_void = Term.pat_app Mlw_expr.fs_void [] Mlw_ty.ty_unit in
280
          let pl = filter_ghost_fields cs pat_void pl in
281 282 283 284 285 286 287
          let pjl = get_record info cs in
          if pjl = [] then
            ML.Papp (cs.ls_name, List.map (pat info) pl)
          else
            let field ls p = ls.ls_name, pat info p in
            ML.Precord (List.map2 field pjl pl)
        end
288

289 290 291 292 293 294 295
  let is_constructor info ls =
  (* eprintf "is_constructor: ls=%s@." ls.ls_name.id_string; *)
    match Mid.find_opt ls.ls_name info.th_known_map with
      | Some { d_node = Ddata dl } ->
        let constr (_,csl) = List.exists (fun (cs,_) -> ls_equal cs ls) csl in
        List.exists constr dl
      | _ -> false
296

297 298 299 300 301 302 303 304 305 306 307 308
  (* can the type of a value be derived from the type of the arguments? *)
  let unambig_fs fs =
    let rec lookup v ty = match ty.ty_node with
      | Tyvar u when tv_equal u v -> true
      | _ -> ty_any (lookup v) ty
    in
    let lookup v = List.exists (lookup v) fs.ls_args in
    let rec inspect ty = match ty.ty_node with
      | Tyvar u when not (lookup u) -> false
      | _ -> ty_all inspect ty
    in
    Opt.fold (fun _ -> inspect) true fs.ls_value
309

310
  let oty_int = Some ty_int
311

312 313 314 315 316 317 318 319 320 321 322 323 324 325
  let rec app ls info tl =
    let isconstr = is_constructor info ls in
    let is_field (_, csl) = match csl with
      | [_, pjl] ->
        let is_ls = function None -> false | Some ls' -> ls_equal ls ls' in
        List.for_all ((<>) None) pjl && List.exists is_ls pjl
      | _ -> false in
    let isfield = match Mid.find_opt ls.ls_name info.th_known_map with
      | Some { d_node = Ddata dl } -> not isconstr && List.exists is_field dl
      | _ -> false
    in
    let id = ls.ls_name in
    match tl with
      | tl when isconstr ->
326
          let tl = filter_ghost_fields ls Mlw_expr.t_void tl in
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352
          let pjl = get_record info ls in
          if pjl = [] then
            ML.Econstr (id, List.map (term info) tl)
          else
            let field ls t = ls.ls_name, term info t in
            ML.Erecord (List.map2 field pjl tl)
      | [t1] when isfield ->
          ML.Egetfield (term info t1, id)
      | tl ->
          ML.Eapp (ML.Eident id, List.map (term info) tl)

  and term info t = match t.t_node with
    | Tvar v ->
        let gh = try (Mlw_ty.restore_pv v).Mlw_ty.pv_ghost
          with Not_found -> false in
        if gh then ML.enop else ML.Eident v.vs_name
    | Ttrue ->
        ML.Ebool true
    | Tfalse ->
        ML.Ebool false
    | Tconst (Number.ConstInt c) ->
        ML.Econst c
    | Tconst (Number.ConstReal _) ->
        assert false
    | Tapp (fs, tl) when is_fs_tuple fs ->
        ML.etuple (List.map (term info) tl)
353 354
    | Tapp (fs, [t1; t2]) when not info.unsafe_int
        && ls_equal fs ps_equ && oty_equal t1.t_ty oty_int ->
355 356
        ML.Esyntax ("(Why3extract.Why3__BigInt.eq %1 %2)",
                    [term info t1; term info t2])
357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417
    | Tapp (fs, tl) ->
        begin match query_syntax info.info_syn fs.ls_name with
        | Some s -> ML.Esyntax (s, List.map (term info) tl)
        | None when unambig_fs fs -> app fs info tl
        | None -> ML.Ecast (app fs info tl, type_ info (t_type t))
        end
    | Tif (t1, t2, t3) ->
        ML.Eif (term info t1, term info t2, term info t3)
    | Tlet (t1, tb) ->
        let v, t2 = t_open_bound tb in
        ML.Elet (v.vs_name, term info t1, term info t2)
    | Tcase (t1, bl) ->
        ML.Ematch (term info t1, List.map (tbranch info) bl)
    | Teps _ when t_is_lambda t ->
        let vl, _, t1 = t_open_lambda t in
        ML.Efun (List.map (vsty info) vl, term info t1)
    | Teps _ | Tquant _ ->
        Format.eprintf "t = %a@." Pretty.print_term t;
        assert false
    | Tbinop (op, t1, t2) ->
        let t1 = term info t1 in
        let t2 = term info t2 in
        begin match op with
          | Tand -> ML.Ebinop (t1, ML.Band, t2)
          | Tor -> ML.Ebinop (t1, ML.Bor, t2)
          | Tiff -> ML.Ebinop (t1, ML.Beq, t2)
          | Timplies -> ML.Ebinop (ML.Enot t1, ML.Bor, t2) end
    | Tnot t1 ->
        ML.Enot (term info t1)

  and tbranch info br =
    let p, t = t_open_branch br in
    pat info p, term info t

  let logic_defn info (ls, ld) =
    let vl, t = open_ls_defn ld in
    (ls.ls_name, List.map (vsty info) vl, term info t)

  let logic_defn info (ls, _ as d) =
    if has_syntax info ls.ls_name then [] else [logic_defn info d]

  let logic_decl info d = match d.d_node with
    | Dtype ts ->
        type_decl info ts
    | Ddata tl ->
        begin match List.flatten (List.map (data_decl info) tl) with
          | [] -> []
          | dl -> [ML.Dtype dl] end @
        List.flatten (List.map (projections info) tl)
    | Dlogic [ls, _ as ld] ->
        if has_syntax info ls.ls_name then [] else
        let isrec = Sid.mem ls.ls_name d.d_syms in
        [ML.Dlet (isrec, logic_defn info ld)]
    | Dlogic ll ->
        begin match List.flatten (List.map (logic_defn info) ll) with
          | [] -> []
          | dl -> [ML.Dlet (true, dl)] end
    | Decl.Dparam _
    | Dind _
    | Dprop _ ->
        []
418

419 420
  let logic_decl info d =
    if Mlw_exec.is_exec_decl info.exec d then logic_decl info d else []
421

422 423 424 425 426 427 428
  let logic_decl info td = match td.td_node with
    | Decl d ->
        let union = Sid.union d.d_syms d.d_news in
        let inter = Mid.set_inter union info.mo_known_map in
        if Sid.is_empty inter then logic_decl info d else []
    | Use _ | Clone _ | Meta _ ->
        []
429

430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
  let theory info th =
    List.flatten (List.map (logic_decl info) th.th_decls)

  (** programs *)

  open Mlw_ty
  open Mlw_ty.T
  open Mlw_expr
  open Mlw_decl
  open Mlw_module

  let rec ity info t = match t.ity_node with
    | Ityvar v ->
        ML.Tvar v.tv_name
    | Itypur (ts, tl) when is_ts_tuple ts ->
        ML.Ttuple (List.map (ity info) tl)
    | Itypur (ts, tl)
    | Ityapp ({its_ts=ts}, tl, _) ->
        begin match query_syntax info.info_syn ts.ts_name with
        | Some s -> ML.Tsyntax (s, List.map (ity info) tl)
        | None -> ML.Tapp (ts.ts_name, List.map (ity info) tl)
        end
452

453 454 455 456 457 458 459 460 461 462 463
  let is_underscore pv =
    pv.pv_vs.vs_name.id_string = "_" && ity_equal pv.pv_ity ity_unit

  let is_int_constant e = match e.e_node with
    | Elogic { t_node = Tconst (Number.ConstInt _) } -> true
    | _ -> false
  let get_int_constant e = match e.e_node with
    | Elogic { t_node = Tconst (Number.ConstInt n) } -> n
    | _ -> assert false

  let pv_name pv = pv.pv_vs.vs_name
464 465 466 467

  let pvty info pv =
    if pv.pv_ghost then (pv.pv_vs.vs_name, type_unit)
    else vsty info pv.pv_vs
468 469 470 471 472 473 474 475 476 477 478 479 480

  let lv_name = function
    | LetV pv -> pv_name pv
    | LetA ps -> ps.ps_name

  let for_direction = function
    | To     -> ML.To
    | DownTo -> ML.DownTo

  let is_letrec = function
    | [fd] -> fd.fun_lambda.l_spec.c_letrec <> 0
    | _ -> true

481
  let filter_ghost_params =
482
(* removal of ghost does not work
483 484 485 486 487
    let dummy = create_pvsymbol (Ident.id_fresh "") ity_unit in
    fun args ->
    match List.filter (fun v -> not v.Mlw_ty.pv_ghost) args with
    | [] -> [dummy]
    | l -> l
488 489 490 491 492 493 494 495
*)
    fun args -> args (* filtering ghost happens in pvty *)
(*
    List.map
      (fun v -> if v.Mlw_ty.pv_ghost then
                  create_pvsymbol (Ident.id_fresh "") ity_unit
                else v)
 *)
496 497 498 499 500
  let rec expr info e =
    assert (not e.e_ghost);
    match e.e_node with
      | Elogic t ->
          term info t
501 502
      | Evalue pv when pv.pv_ghost ->
         ML.enop
503 504 505 506 507 508 509 510 511 512 513
      | Evalue pv ->
           ML.Eident (pv_name pv)
      | Earrow a ->
          begin match query_syntax info.info_syn a.ps_name with
          | Some s -> ML.Esyntax (s, [])
          | None   -> ML.Eident a.ps_name end
      (* converter *)
      | Elet ({ let_sym = LetV pv; let_expr = e1 },
              { e_node = Eapp ({ e_node = Earrow a }, pv', _) })
        when pv_equal pv' pv
             && Mid.mem a.ps_name info.converters && is_int_constant e1 ->
514
          let s = fst (Mid.find a.ps_name info.converters) in
515 516 517
          let n = Number.compute_int (get_int_constant e1) in
          let e1 = ML.Esyntax (BigInt.to_string n, []) in
          ML.Esyntax (s, [e1])
518
      | Eapp (e, v, _) when v.pv_ghost ->
519 520
         (* ghost parameters are unit *)
         ML.Eapp (expr info e, [ML.enop])
521 522
      | Eapp (e, v, _) ->
          ML.Eapp (expr info e, [ML.Eident (pv_name v)])
MARCHE Claude's avatar
MARCHE Claude committed
523
      | Elet ({ let_sym = _lv; let_expr = e1 }, e2) when e1.e_ghost ->
524
         (* TODO: remove superflous let *)
525
         (* ML.Elet (lv_name lv, ML.enop, *) expr info e2 (* ) *)
526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546
      | Elet ({ let_sym = LetV pv }, e2) when ity_equal pv.pv_ity ity_mark ->
          expr info e2
      | Elet ({ let_sym = LetV pv; let_expr = e1 }, e2) when is_underscore pv ->
          ML.eseq (expr info e1) (expr info e2)
      | Elet ({ let_sym = lv ; let_expr = e1 }, e2) ->
          ML.Elet (lv_name lv, expr info e1, expr info e2)
      | Eif (e0, e1, e2) ->
          ML.Eif (expr info e0, expr info e1, expr info e2)
      | Eassign (pl, e1, _, pv) ->
          ML.Esetfield (expr info e1, pl.pl_ls.ls_name,
                        ML.Eident (pv_name pv))
      | Eloop (_, _, e1) ->
          ML.Ewhile (ML.Ebool true, expr info e1)
      | Efor (pv, (pvfrom, dir, pvto), _, e1) ->
          ML.Efor (pv_name pv,
                   pv_name pvfrom, for_direction dir, pv_name pvto,
                   expr info e1)
      | Eraise (xs,_) when xs_equal xs xs_exit ->
          ML.Eraise (ML.Xexit, None)
      | Eraise (xs, e1) ->
          begin match query_syntax info.info_syn xs.xs_name with
547 548
          | Some s ->
              ML.Eraise (ML.Xsyntax s, Some (expr info e1))
549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577
          | None when ity_equal xs.xs_ity ity_unit ->
              ML.Eraise (ML.Xident xs.xs_name, None)
          | None ->
              ML.Eraise (ML.Xident xs.xs_name, Some (expr info e1))
          end
      | Etry (e1, bl) ->
          ML.Etry (expr info e1, List.map (xbranch info) bl)
      | Eabstr (e1, _) ->
          expr info e1
      | Eabsurd ->
          ML.Eabsurd
      | Eassert _ ->
          ML.enop
      | Eghost _
      | Eany _ ->
          assert false
      | Ecase (e1, [_,e2]) when e1.e_ghost ->
          expr info e2
      | Ecase (e1, bl) ->
          ML.Ematch (expr info e1, List.map (ebranch info) bl)
      | Erec (fdl, e1) ->
          (* FIXME what about ghosts? *)
          let cmp {fun_ps=ps1} {fun_ps=ps2} =
            Pervasives.compare ps1.ps_ghost ps2.ps_ghost in
          let fdl = List.sort cmp fdl in
          ML.Eletrec (is_letrec fdl, List.map (recdef info) fdl, expr info e1)

  and recdef info { fun_ps = ps; fun_lambda = lam } =
    assert (not ps.ps_ghost);
578 579
    let args = filter_ghost_params lam.l_args in
    ps.ps_name, List.map (pvty info) args, expr info lam.l_expr
580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607

  and ebranch info ({ppat_pattern=p}, e) =
    pat info p, expr info e

  and xbranch info (xs, pv, e) =
    match query_syntax info.info_syn xs.xs_name with
      | Some s ->
          ML.Xsyntax s, Some (pv_name pv), expr info e
      | None when xs_equal xs xs_exit ->
          ML.Xexit, None, expr info e
      | None when ity_equal xs.xs_ity ity_unit ->
          ML.Xident xs.xs_name, None, expr info e
      | None ->
          ML.Xident xs.xs_name, Some (pv_name pv), expr info e

  let pdata_decl info (its, csl, _) =
    let field fd = if fd.fd_ghost then ML.tunit else ity info fd.fd_ity in
    let default () =
      let constr (cs, _) = cs.pl_ls.ls_name, List.map field cs.pl_args in
      ML.Ddata (List.map constr csl) in
    let field (ls, fd) = fd.fd_mut <> None, ls.ls_name, field fd in
    let defn = function
      | [cs, _] ->
        let pjl = get_record info cs.pl_ls in
        if pjl = [] then default ()
        else ML.Drecord (List.map field (List.combine pjl cs.pl_args))
      | _ ->
        default ()
608
    in
609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
    let ts = its.its_ts in
    ts.ts_name, type_args ts.ts_args, defn csl

  let pdata_decl info (its, _, _ as d) =
    if has_syntax info its.its_ts.ts_name then [] else [pdata_decl info d]

  let pprojections _info ({its_ts=ts}, csl, _) =
    let pjl = List.filter ((<>) None) (snd (List.hd csl)) in
    let pjl = List.map Opt.get pjl in
    let x = id_register (id_fresh "x") in
    let projection ls =
      let branch (cs, pjl) =
        let arg = function
          | Some ls' when pl_equal ls' ls -> ML.Pident x
          | _ -> ML.Pwild in
        ML.Papp (cs.pl_ls.ls_name, List.map arg pjl), ML.Eident x
      in
      let id = id_register (id_fresh "x") in
      let ty =
        ML.Tapp (ts.ts_name,
                 List.map (fun tv -> ML.Tvar tv.tv_name) ts.ts_args) in
      let def = ML.Ematch (ML.Eident id, List.map branch csl) in
      ML.Dlet (false, [ls.pl_ls.ls_name, [id, ty], def])
    in
    List.map projection pjl

  let is_record = function
    | _, [_, pjl], _ -> List.for_all ((<>) None) pjl
    | _ -> false

  let pprojections info (ts, _, _ as d) =
    if has_syntax info ts.its_ts.ts_name || is_record d then []
    else pprojections info d

643 644
  let pdecl info pd =
    match pd.pd_node with
645
    | PDval (LetV pv) when pv_equal pv Mlw_decl.pv_old ->
646 647 648 649 650 651 652 653 654 655 656 657
        []
    | PDval _ ->
        []
    | PDtype ({ its_ts = ts } as its) ->
        let id = ts.ts_name in
        begin match its.its_def with
          | None ->
              [ML.Dtype [id, type_args ts.ts_args, ML.Dabstract]]
          | Some ty ->
              [ML.Dtype [id, type_args ts.ts_args, ML.Dalias (ity info ty)]]
        end
    | PDlet { let_sym = lv ; let_expr = e } ->
658 659 660
       Debug.dprintf debug "extract 'let' declaration %s@."
                     (lv_name lv).id_string;
       [ML.Dlet (false, [lv_name lv, [], expr info e])]
661 662 663 664 665 666 667 668 669 670 671 672
    | PDdata tl ->
        begin match List.flatten (List.map (pdata_decl info) tl) with
          | [] -> []
          | dl -> [ML.Dtype dl] end @
        List.flatten (List.map (pprojections info) tl)
    | PDrec fdl ->
        (* print defined, non-ghost first *)
        let cmp {fun_ps=ps1} {fun_ps=ps2} =
          Pervasives.compare
            (ps1.ps_ghost || has_syntax info ps1.ps_name)
            (ps2.ps_ghost || has_syntax info ps2.ps_name) in
        let fdl = List.sort cmp fdl in
673 674 675 676
        List.iter
          (fun {fun_ps=ps} ->
           Debug.dprintf debug "extract 'let rec' declaration %s@."
                         ps.ps_name.id_string) fdl;
677 678 679 680 681 682 683 684
        [ML.Dlet (is_letrec fdl, List.map (recdef info) fdl)]
    | PDexn xs ->
        let id = xs.xs_name in
        if ity_equal xs.xs_ity ity_unit then
          [ML.Dexn (id, None)]
        else
          [ML.Dexn (id, Some (ity info xs.xs_ity))]

685 686 687 688 689 690
  let warn_non_ghost_non_exec ps =
    if not ps.ps_ghost then
      Warning.emit ?loc:ps.ps_name.id_loc
        "Cannot extract code from non-ghost function %s: body is not executable"
        ps.ps_name.id_string

691
  let pdecl info d =
692 693 694
    if Mlw_exec.is_exec_pdecl info.exec d then pdecl info d else
      begin
        begin match d.pd_node with
695
        | PDlet { let_sym = LetA ps } -> warn_non_ghost_non_exec ps
696 697
        | PDrec fdl ->
           List.iter
698
             (fun {fun_ps=ps} -> warn_non_ghost_non_exec ps) fdl
699 700 701 702
        | _ -> ()
        end;
        []
      end
703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778

  let module_ info m =
    List.flatten (List.map (pdecl info) m.mod_decls)

end

(** OCaml printers *)

module Print = struct

  open ML

  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";]

  let is_ocaml_keyword =
    let h = Hstr.create 17 in
    List.iter (fun s -> Hstr.add h s ()) ocaml_keywords;
    Hstr.mem h

  let iprinter,aprinter,_tprinter,_pprinter =
    let isanitize = sanitizer char_to_alpha char_to_alnumus in
    let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
    create_ident_printer ocaml_keywords ~sanitizer:isanitize,
    create_ident_printer ocaml_keywords ~sanitizer:lsanitize,
    create_ident_printer ocaml_keywords ~sanitizer:lsanitize,
    create_ident_printer ocaml_keywords ~sanitizer:isanitize

  let forget_tvs () =
    forget_all aprinter

  (* type variables always start with a quote *)
  let print_tv fmt tv =
    fprintf fmt "'%s" (id_unique aprinter tv)

  let forget_id vs = forget_id iprinter vs
  let _forget_ids = List.iter forget_id
  let forget_var (vs, _) = forget_id vs
  let forget_vars = List.iter forget_var

  let rec forget_pat = function
    | Pwild -> ()
    | Pident id -> forget_id id
    | Papp (_, pl) | Ptuple pl | Psyntax (_, pl) -> List.iter forget_pat pl
    | Precord fl -> List.iter (fun (_, p) -> forget_pat p) fl
    | Por (p1, p2) -> forget_pat p1; forget_pat p2
    | Pas (p, _) -> forget_pat p

  let print_ident fmt id =
    let s = id_unique iprinter id in
    fprintf fmt "%s" s

  let print_path = print_list dot pp_print_string

  let print_qident ~sanitizer info fmt id =
    try
      let lp, t, p =
        try Mlw_module.restore_path id
        with Not_found -> Theory.restore_path id in
      let s = String.concat "__" p in
      let s = Ident.sanitizer char_to_alpha char_to_alnumus s in
      let s = sanitizer s in
      let s = if is_ocaml_keyword s then s ^ "_renamed" else s in
      if Sid.mem id info.current_theory.th_local ||
        Opt.fold (fun _ m -> Sid.mem id m.Mlw_module.mod_local)
        false info.current_module
      then
        fprintf fmt "%s" s
779
      else
780
        let fname = if lp = [] then info.fname else None in
781
        let m = Strings.capitalize (modulename ?fname lp t) in
782 783 784 785 786
        fprintf fmt "%s.%s" m s
    with Not_found ->
      let s = id_unique ~sanitizer iprinter id in
      fprintf fmt "%s" s

787 788
  let print_lident = print_qident ~sanitizer:Strings.uncapitalize
  let print_uident = print_qident ~sanitizer:Strings.capitalize
789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813

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

  let print_theory_name fmt th = print_path_id fmt (th.th_path, th.th_name)
  let print_module_name fmt m  = print_theory_name fmt m.Mlw_module.mod_theory

  (** Types *)

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

  let star fmt () = fprintf fmt " *@ "

  let rec print_ty ?(paren=false) info fmt = function
    | Tvar v ->
        print_tv fmt v
    | Ttuple [] ->
        fprintf fmt "unit"
    | Ttuple tl ->
        fprintf fmt (protect_on paren "%a") (print_list star (print_ty info)) tl
    | Tapp (ts, []) ->
        print_lident info fmt ts
    | Tapp (ts, [ty]) ->
        fprintf fmt (protect_on paren "%a@ %a")
814
          (print_ty ~paren:true info) ty (print_lident info) ts
815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831
    | Tapp (ts, tl) ->
        fprintf fmt (protect_on paren "(%a)@ %a")
          (print_list comma (print_ty info)) tl
          (print_lident info) ts
    | Tsyntax (s, tl) ->
        syntax_arguments s (print_ty info) fmt tl

  let print_vsty info fmt (v, ty) =
    fprintf fmt "%a:@ %a" (print_lident info) v (print_ty info) ty

  let print_tv_arg = print_tv
  let print_tv_args fmt = function
    | [] -> ()
    | [tv] -> fprintf fmt "%a@ " print_tv_arg tv
    | tvl -> fprintf fmt "(%a)@ " (print_list comma print_tv_arg) tvl

  let print_ty_arg info fmt ty = fprintf fmt "%a" (print_ty ~paren:true info) ty
832
  let print_vs_arg info fmt vs = fprintf fmt "@[(%a)@]" (print_vsty info) vs
833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902

  let print_type_decl info fst fmt (ts, args, def) =
    let print_constr fmt (cs, args) = match args with
      | [] ->
          fprintf fmt "@[<hov 4>| %a@]" (print_uident info) cs
      | tl ->
          fprintf fmt "@[<hov 4>| %a of %a@]" (print_uident info) cs
            (print_list star (print_ty_arg info)) tl in
    let print_field fmt (mut, ls, ty) =
      fprintf fmt "%s%a: %a;"
        (if mut then "mutable " else "")
        (print_lident info) ls (print_ty info) ty in
    let print_defn fmt = function
      | Dabstract ->
          ()
      | Ddata csl ->
          fprintf fmt " =@\n%a" (print_list newline print_constr) csl
      | Drecord fl ->
          fprintf fmt " = {@\n%a@\n}" (print_list newline print_field) fl
      | Dalias ty ->
          fprintf fmt " =@ %a" (print_ty info) ty
    in
    fprintf fmt "@[<hov 2>%s %a%a%a@]"
      (if fst then "type" else "and")
      print_tv_args args (print_lident info) ts print_defn def

  let print_list_next sep print fmt = function
    | [] ->
        ()
    | [x] ->
        print true fmt x
    | x :: r ->
        print true fmt x; sep fmt ();
        print_list sep (print false) fmt r

  let rec print_pat ?(paren=false) info fmt = function
    | Pwild ->
        fprintf fmt "_"
    | Pident v ->
        print_lident info fmt v
    | Pas (p, v) ->
        fprintf fmt (protect_on paren "%a as %a")
          (print_pat ~paren:true info) p (print_lident info) v
    | Por (p, q) ->
        fprintf fmt (protect_on paren "%a | %a")
          (print_pat info) p (print_pat info) q
    | Ptuple pl ->
        fprintf fmt "(%a)"
          (print_list comma (print_pat info)) pl
    | Psyntax (s, pl) ->
        syntax_arguments s (print_pat ~paren:true info) fmt pl
    | Papp (cs, []) ->
        print_uident info fmt cs
    | Papp (cs, [p]) ->
        fprintf fmt (protect_on paren "%a@ %a")
          (print_uident info) cs (print_pat ~paren:true info) p
    | Papp (cs, pl) ->
        fprintf fmt (protect_on paren "%a@ (%a)")
          (print_uident info) cs (print_list comma (print_pat info)) pl
    | Precord fl ->
        let print_field fmt (ls, p) = fprintf fmt "%a = %a"
          (print_lident info) ls (print_pat info) p in
        fprintf fmt "{ %a }" (print_list semi print_field) fl

  let min_int31 = BigInt.of_int (- 0x40000000)
  let max_int31 = BigInt.of_int    0x3FFFFFFF

  let print_const ~paren fmt c =
    let n = Number.compute_int c in
    if BigInt.eq n BigInt.zero then
903
      fprintf fmt "Why3extract.Why3__BigInt.zero"
904
    else if BigInt.eq n BigInt.one then
905
      fprintf fmt "Why3extract.Why3__BigInt.one"
906 907
    else if BigInt.le min_int31 n && BigInt.le n max_int31 then
      let m = BigInt.to_int n in
908
      fprintf fmt (protect_on paren "Why3extract.Why3__BigInt.of_int %d") m
909 910
    else
      let s = BigInt.to_string n in
911 912
      fprintf fmt
        (protect_on paren "Why3extract.Why3__BigInt.of_string \"%s\"") s
913 914 915 916 917 918 919 920

  let print_binop fmt = function
    | Band -> fprintf fmt "&&"
    | Bor -> fprintf fmt "||"
    | Beq -> fprintf fmt "="

  let is_unit = function
    | Eblock [] -> true
921
    | _ -> false
922 923 924 925 926 927

  let rec print_expr ?(paren=false) info fmt = function
    | Eident v ->
        print_lident info fmt v
    | Ebool b ->
        fprintf fmt "%b" b
928 929
    | Econst c when info.unsafe_int ->
        fprintf fmt "%s" (BigInt.to_string (Number.compute_int c))
930 931 932 933 934 935 936 937 938 939 940 941 942 943
    | Econst c ->
        print_const ~paren fmt c
    | Etuple el ->
        fprintf fmt "(%a)" (print_list comma (print_expr info)) el
    | Esyntax (s, tl) ->
        syntax_arguments s (print_expr_p info) fmt tl
    | Ecast (e, ty) ->
        fprintf fmt "@[<hov 2>(%a:@ %a)@]"
          (print_expr info) e (print_ty info) ty
    | Eif (e1, e2, e3) when is_unit e3 ->
        fprintf fmt
          (protect_on paren "@[<hv>@[<hov 2>if@ %a@]@ then@;<1 2>@[%a@]@]")
          (print_expr info) e1 (print_expr ~paren:true info) e2
    | Eif (e1, e2, e3) ->
944 945
        fprintf fmt (protect_on paren
        "@[<hv>@[<hov 2>if@ %a@]@ then@;<1 2>@[%a@]@;<1 0>else@;<1 2>@[%a@]@]")
946 947
          (print_expr info) e1 (print_expr info) e2 (print_expr info) e3
    | Elet (v, e1, e2) ->
948
        fprintf fmt (protect_on paren "@[<hov 2>let @[%a@] =@ @[%a@]@] in@ %a")
949 950
          (print_lident info) v (print_expr info) e1 (print_expr info) e2;
        forget_id v
951 952 953
    | Ematch (e1, [p, b1]) ->
        fprintf fmt (protect_on paren "@[<hov 2>let @[%a@] =@ @[%a@]@] in@ %a")
          (print_pat info) p (print_expr info) e1 (print_expr info) b1
954 955 956 957 958 959 960 961 962 963 964 965
    | Ematch (e1, bl) ->
        fprintf fmt "@[begin match @[%a@] with@\n@[<hov>%a@] end@]"
          (print_expr info) e1 (print_list newline (print_branch info)) bl
    | Ebinop (e1, op, e2) ->
        fprintf fmt (protect_on paren "@[<hov 1>%a %a@ %a@]")
          (print_expr_p info) e1 print_binop op (print_expr_p info) e2
    | Enot e1 ->
        fprintf fmt (protect_on paren "not %a") (print_expr_p info) e1
    | Eapp (e, el) ->
        fprintf fmt (protect_on paren "@[<hov 2>%a@ %a@]")
          (print_expr info) e (print_list space (print_expr_p info)) el
    | Efun (vl, e1) ->
966
        fprintf fmt (protect_on paren "@[<hov 2>(fun %a ->@ %a)@]")
967 968 969 970 971 972 973 974
          (print_list space (print_vs_arg info)) vl (print_expr info) e1;
        forget_vars vl
    | Econstr (c, []) ->
        print_uident info fmt c
    | Econstr (c, [e1]) ->
        fprintf fmt (protect_on paren "%a %a")
          (print_uident info) c (print_expr_p info) e1
    | Econstr (c, el) ->
975
        fprintf fmt (protect_on paren "@[<hov 1>%a@ (%a)@]")
976 977 978 979 980 981 982 983 984
          (print_uident info) c (print_list comma (print_expr info)) el
    | Erecord fl ->
        let print_field fmt (f, e) =
          fprintf fmt "%a = %a" (print_lident info) f (print_expr info) e in
        fprintf fmt "@[<hov 1>{ %a }@]" (print_list semi print_field) fl
    | Egetfield (e, f) ->
        fprintf fmt "%a.%a" (print_expr_p info) e (print_lident info) f
    | Esetfield (e1, f, e2) ->
        fprintf fmt (protect_on paren "%a.%a <- %a")
985
        (print_expr_p info) e1 (print_lident info) f (print_expr info) e2
986 987 988 989 990 991 992 993 994 995
    | Eblock [] ->
        fprintf fmt "()"
    | Eblock [e] ->
        print_expr ~paren info fmt e
    | Eblock bl ->
        fprintf fmt "@[<hv>begin@;<1 2>@[%a@]@ end@]"
          (print_list semi (print_expr info)) bl
    | Ewhile (e1, e2) ->
        fprintf fmt "@[<hv>while %a do@;<1 2>@[%a@]@ done@]"
          (print_expr info) e1 (print_expr info) e2
996 997 998 999 1000 1001
    | Efor (x, vfrom, dir, vto, e1) when info.unsafe_int ->
        fprintf fmt
          "@[<hov 2>for %a = %a %s %a do@\n%a@\ndone@]"
          (print_lident info) x  (print_lident info) vfrom
          (if dir = To then "to" else "downto") (print_lident info) vto
          (print_expr info) e1
1002 1003
    | Efor (x, vfrom, dir, vto, e1) ->
        fprintf fmt
1004
      "@[<hov 2>(Why3extract.Why3__IntAux.for_loop_%s %a %a@ (fun %a ->@ %a))@]"
1005 1006 1007 1008 1009 1010 1011
          (if dir = To then "to" else "downto")
          (print_lident info) vfrom (print_lident info) vto
          (print_lident info) x (print_expr info) e1
    | Eraise (Xexit, a) ->
        assert (a = None);
        fprintf fmt (protect_on paren "raise Pervasives.Exit")
    | Eraise (Xsyntax s, None) ->
1012 1013
        fprintf fmt (protect_on paren "raise %a")
          (syntax_arguments s (print_expr info)) []
1014
    | Eraise (Xsyntax s, Some e1) ->
1015 1016
        fprintf fmt (protect_on paren "raise %a")
          (syntax_arguments s (print_expr info)) [e1]
1017 1018 1019 1020
    | Eraise (Xident id, None) ->
        fprintf fmt (protect_on paren "raise %a") (print_uident info) id
    | Eraise (Xident id, Some e1) ->
        fprintf fmt (protect_on paren "raise (%a %a)")
1021
              (print_uident info) id (print_expr ~paren:true info) e1
1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066
    | Etry (e1, bl) ->
        fprintf fmt
          "@[<v>@[<hv>@[<hov 2>begin@ try@ %a@]@ with@]@\n@[<hov>%a@]@\nend@]"
          (print_expr info) e1 (print_list newline (print_xbranch info)) bl
    | Eabsurd ->
        fprintf fmt (protect_on paren "assert false (* absurd *)")
    | Eletrec (is_rec, fdl, e1) ->
        fprintf fmt (protect_on paren "@[<v>%a@\nin@\n%a@]")
          (print_list_next newline (print_rec is_rec info)) fdl
          (print_expr info) e1

  and print_rec lr info fst fmt (id, args, e) =
    let print_arg fmt v = fprintf fmt "@[%a@]" (print_vs_arg info) v in
    fprintf fmt "@[<hov 2>%s %a %a =@\n@[%a@]@]"
      (if fst then if lr then "let rec" else "let" else "and")
      (print_lident info) id (print_list space print_arg) args
      (print_expr info) e;
    forget_vars args

  and print_expr_p info fmt t = print_expr ~paren:true info fmt t

  and print_branch info fmt (p, e) =
    fprintf fmt "@[<hov 4>| %a ->@ %a@]" (print_pat info) p (print_expr info) e;
    forget_pat p

  and print_xbranch info fmt (xs, v, e) =
    begin match xs, v with
    | Xsyntax s, _ ->
        let v = match v with None -> [] | Some v -> [v] in
        fprintf fmt "@[<hov 4>| %a ->@ %a@]"
          (syntax_arguments s (print_lident info)) v
          (print_expr info) e
    | Xexit, _ ->
        fprintf fmt "@[<hov 4>| Pervasives.Exit ->@ %a@]" (print_expr info) e
    | Xident xs, None ->
        fprintf fmt "@[<hov 4>| %a ->@ %a@]"
          (print_uident info) xs (print_expr info) e
    | Xident xs, Some v ->
        fprintf fmt "@[<hov 4>| %a %a ->@ %a@]"
          (print_uident info) xs (print_lident info) v (print_expr info) e
    end;
    Opt.iter forget_id v

  let print_decl info fmt = function
    | Dtype dl ->
1067 1068
       print_list_next newline (print_type_decl info) fmt dl;
       fprintf fmt "@\n@\n"
1069
    | Dlet (isrec, dl) ->
1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080
       let print_one fst fmt (ls, vl, e) =
         fprintf fmt "@[<hov 2>%s %a@ %a@ =@ %a@]"
                 (if fst then if isrec then "let rec" else "let" else "and")
                 (print_lident info) ls
                 (print_list space (print_vs_arg info)) vl
                 (print_expr info) e;
         forget_vars vl;
         forget_tvs ()
       in
       print_list_next newline print_one fmt dl;
       fprintf fmt "@\n@\n"
1081
    | Dexn (xs, None) ->
1082
       fprintf fmt "exception %a@\n@\n" (print_uident info) xs
1083
    | Dexn (xs, Some ty) ->
1084
       fprintf fmt "@[<hov 2>exception %a of %a@]@\n@\n"
1085
               (print_uident info) xs (print_ty ~paren:true info) ty
1086 1087 1088 1089 1090 1091 1092

end

(** Exported functions *)

let extract_filename ?fname th =
  (modulename ?fname th.th_path th.th_name.Ident.id_string) ^ ".ml"
1093

1094 1095
let unsafe_int drv =
  drv.Mlw_driver.drv_printer = Some "ocaml-unsafe-int"
1096

1097 1098 1099 1100 1101 1102 1103 1104
let print_preludes used fmt pm =
  (* we do not print the same prelude twice *)
  let ht = Hstr.create 5 in
  let add l s = if Hstr.mem ht s then l else (Hstr.add ht s (); s :: l) in
  let l = Sid.fold
    (fun id l -> List.fold_left add l (Mid.find_def [] id pm)) used [] in
  print_prelude fmt l

1105
let extract_theory drv ?old ?fname fmt th =
1106
  ignore (old); ignore (fname);
1107
  let info = {
1108
    exec = Mlw_exec.create drv th.th_known Mid.empty;
1109 1110
    info_syn = drv.Mlw_driver.drv_syntax;
    converters = drv.Mlw_driver.drv_converter;
1111
    current_theory = th;
1112
    current_module = None;
1113 1114
    th_known_map = th.th_known;
    mo_known_map = Mid.empty;
1115 1116
    fname = Opt.map clean_fname fname;
    unsafe_int = unsafe_int drv; } in
1117
  let decls = Translate.theory info th in
1118 1119
  fprintf fmt
    "(* This file has been generated from Why3 theory %a *)@\n@\n"
1120
    Print.print_theory_name th;
1121 1122 1123
  print_prelude fmt drv.Mlw_driver.drv_prelude;
  print_preludes th.th_used fmt drv.Mlw_driver.drv_thprelude;
  fprintf fmt "@\n";
1124
  print_list nothing (Print.print_decl info) fmt decls;
1125
  fprintf fmt "@."
1126

1127 1128
open Mlw_module

1129
let extract_module drv ?old ?fname fmt m =
1130
  ignore (old); ignore (fname);
1131 1132
  let th = m.mod_theory in
  let info = {
1133
    exec = Mlw_exec.create drv th.th_known m.mod_known;
1134 1135
    info_syn = drv.Mlw_driver.drv_syntax;
    converters = drv.Mlw_driver.drv_converter;
1136
    current_theory = th;
1137
    current_module = Some m;
1138 1139
    th_known_map = th.th_known;
    mo_known_map = m.mod_known;
1140 1141
    fname = Opt.map clean_fname fname;
    unsafe_int = unsafe_int drv; } in
1142 1143
  let decls = Translate.theory info th in
  let mdecls = Translate.module_ info m in
1144 1145
  fprintf fmt
    "(* This file has been generated from Why3 module %a *)@\n@\n"
1146
    Print.print_module_name m;
1147 1148 1149 1150
  print_prelude fmt drv.Mlw_driver.drv_prelude;
  let used = Sid.union m.mod_used m.mod_theory.th_used in
  print_preludes used fmt drv.Mlw_driver.drv_thprelude;
  fprintf fmt "@\n";
1151 1152
  print_list nothing (Print.print_decl info) fmt decls;
  print_list nothing (Print.print_decl info) fmt mdecls;
1153 1154 1155 1156
  fprintf fmt "@."

(*
Local Variables:
1157
compile-command: "unset LANG; make -C ../.."
1158 1159
End:
*)