compile.ml 16.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

(*
  - option to extract into a single file

  - no more why3extract.cma
    use driver preludes instead

  - 2 drivers for nums and zarith

  - no delcaration at all for a module -> no file produced
    (e.g. ref.Ref)

  - suggest a command line to compile the extracted code
    (for instance in a comment)

  - drivers for val now may use %1, %2, etc. (though not mandatory)
    Capp f x y
      "..." -> "..." x y
      "...%1..." -> "...x..." y
      "..(*%1*)..." -> "...(*x*)..." y
      "..%1..%3.." -> (fun z -> "..x..z..")  (y ignored)

  - extract file f.mlw into OCaml file f.ml, with sub-modules

  - "use (im|ex)port" -> "open"
    but OCaml's open is not transitive, so requires some extra work
    to figure out all the opens

  - if a WhyML module M is extracted to something that is a signature,
    then extract "module type B_sig = ..." (as well as "module B = ...")

  - use a black list in printer to avoid clash with Pervasives symbols
    (e.g. ref, (!), etc.)

*)

47 48 49 50 51
(*
  Questions pour Jean-Christophe et Andreï :
    - est-ce qu'il y a des utilisations particulières du champ
      [itd_fields], vis-à-vis du champ [itd_constructors] ?

52 53 54
    - comme l'AST [expr] est déjà en forme normale-A, est-ce que ça
      fait du sense pour vous d'utiliser des applications de la forme
      [Eapp of ident * ident list] ?
55 56 57 58

    - faire un module Erasure, pour y concentrer tout ce qui
      appartient à l'éffacement du code fantôme ?

59 60
    - comment est-ce qu'il marche la [mask] d'un [prog_pattern] ?

61
 *)
62

63 64
(*
  TODO: réfléchir sur l'affectation parallèle
65 66 67
*)


68 69 70 71
(** Abstract syntax of ML *)

open Ident
open Ity
Mário Pereira's avatar
Mário Pereira committed
72
open Ty
Mário Pereira's avatar
Mário Pereira committed
73
open Term
74
open Printer
75 76 77

module ML = struct

78 79
  open Expr

80
  type ty =
81
    | Tvar    of tvsymbol
82 83 84
    | Tapp    of ident * ty list
    | Ttuple  of ty list

85 86 87
  type is_ghost = bool

  type var = ident * ty * is_ghost
88

Mário Pereira's avatar
Mário Pereira committed
89 90
  type for_direction = To | DownTo

91 92 93 94 95 96 97 98 99 100 101 102 103 104
  type pat =
    | Pwild
    | Pident  of ident
    | Papp    of ident * pat list
    | Ptuple  of pat list
    | Precord of (ident * pat) list
    | Por     of pat * pat
    | Pas     of pat * ident

  type is_rec = bool

  type binop = Band | Bor | Beq

  type exn =
Mário Pereira's avatar
Mário Pereira committed
105
    | Xident of ident
106

107
  type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *)
108

109
  type expr = {
Mário Pereira's avatar
Mário Pereira committed
110 111 112
    e_node   : expr_node;
    e_ity    : ity;
    e_effect : effect;
113
    (* TODO: add the set of free variables? *)
114 115 116 117
  }

  and expr_node =
    | Econst  of Number.integer_constant
118
    | Evar    of pvsymbol
119
    | Eapp    of rsymbol * expr list
120
    | Efun    of var list * expr
121 122
    | Elet    of pvsymbol * expr * expr
    | Eletrec of is_rec * (rsymbol * var list * expr) list * expr
123 124
    | Eif     of expr * expr * expr
    | Ecast   of expr * ty
Mário Pereira's avatar
Mário Pereira committed
125
    | Eassign of (pvsymbol * rsymbol * pvsymbol) list
126 127 128 129 130 131
    | Etuple  of expr list (* at least 2 expressions *)
    | Ematch  of expr * (pat * expr) list
    | Ebinop  of expr * binop * expr
    | Enot    of expr
    | Eblock  of expr list
    | Ewhile  of expr * expr
132
    | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
133
    | Eraise  of exn * expr option
134
    | Etry    of expr * (exn * pvsymbol option * expr) list
135 136 137 138 139 140 141 142 143
    | Eabsurd

  type is_mutable = bool

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

144 145 146 147 148 149 150
  type its_defn = {
    its_name    : ident;
    its_args    : tvsymbol list;
    its_private : bool;
    its_def     : typedef option;
  }

151
  type decl = (* TODO add support for the extraction of ocaml modules *)
Mario Pereira's avatar
Mario Pereira committed
152 153 154
    | Dtype   of its_defn list
    | Dlet    of rsymbol * var list * expr
    | Dletrec of rdef list
155
        (* TODO add return type? *)
Mario Pereira's avatar
Mario Pereira committed
156 157 158 159 160 161 162 163
    | Dexn    of xsymbol * ty option

  and rdef = {
    rec_sym  : rsymbol; (* exported *)
    rec_rsym : rsymbol; (* internal *)
    rec_args : var list;
    rec_exp  : expr;
  }
164

165
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
166 167
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

168
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
169 170 171 172
  let ml_let id e1 e2 =
    Elet (id, e1, e2)

  let tunit = Ttuple []
173

174 175 176 177 178
  let enope = Eblock []

  let mk_unit =
    mk_expr enope (I Ity.ity_unit) Ity.eff_empty

179 180 181 182 183
  let mk_var id ty ghost = (id, ty, ghost)

  let mk_its_defn id args private_ def =
    { its_name = id; its_args = args; its_private = private_; its_def = def; }

184 185 186 187 188 189 190 191
  let eseq e1 e2 =
    match e1.e_node, e2.e_node with
    | Eblock [], e | e, Eblock [] -> e
    | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
    | _, Eblock e2 -> Eblock (e1 :: e2)
    | Eblock e1, _ -> Eblock (e1 @ [e2])
    | _ -> Eblock [e1; e2]

192
end
Mário Pereira's avatar
Mário Pereira committed
193

194 195 196 197 198 199 200 201 202 203
type info = {
  info_syn          : syntax_map;
  info_convert      : syntax_map;
  info_current_th   : Theory.theory;
  info_current_mo   : Pmodule.pmodule option;
  info_th_known_map : Decl.known_map;
  info_mo_known_map : Pdecl.known_map;
  info_fname        : string option;
}

Mário Pereira's avatar
Mário Pereira committed
204 205 206 207 208 209 210
let has_syntax cxt id =
  (* Mid.iter *)
  (*   (fun id' _ -> Format.printf "id': %s@\n" id'.id_string) *)
  (*   cxt.info_syn; *)
  query_syntax cxt.info_syn id <> None ||
  query_syntax cxt.info_convert id <> None

Mário Pereira's avatar
Mário Pereira committed
211 212 213 214 215 216 217 218 219
(** Translation from Mlw to ML *)

module Translate = struct

  open Expr    (* Mlw expressions *)

  open Pmodule (* for the type of modules *)
  open Pdecl   (* for the type of program declarations *)

Mário Pereira's avatar
Mário Pereira committed
220 221 222
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
223 224 225 226
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
227
       ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
228 229 230 231 232 233 234 235
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
       ML.Ttuple (List.map type_ tyl)
    | Tyapp (ts, tyl) ->
       ML.Tapp (ts.ts_name, List.map type_ tyl)

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

236 237 238
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

Mário Pereira's avatar
Mário Pereira committed
239
  let filter_ghost_params p def l =
240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259
    let rec filter_ghost_params_cps l k =
      match l with
      | [] -> k []
      | e :: r ->
        filter_ghost_params_cps r
          (fun fr -> k (if p e then (def e) :: fr else fr))
    in
    filter_ghost_params_cps l (fun x -> x)

  let filter2_ghost_params p def al l =
    let rec filter2_ghost_params_cps l k =
      match l with
      | []  -> k []
      | [e] -> k (if p e then [def e] else [al e])
      | e :: r ->
        filter2_ghost_params_cps r
          (fun fr -> k (if p e then (def e) :: fr else fr))
    in
    filter2_ghost_params_cps l (fun x -> x)

260 261 262
  let rec pat p =
    match p.pat_node with
    | Pwild ->
263
      ML.Pwild
264
    | Pvar vs ->
265
      ML.Pident vs.vs_name
266
    | Por (p1, p2) ->
267
      ML.Por (pat p1, pat p2)
268
    | Pas (p, vs) ->
269
      ML.Pas (pat p, vs.vs_name)
270
    | Papp (ls, pl) when is_fs_tuple ls ->
271
      ML.Ptuple (List.map pat pl)
272
    | Papp (ls, pl) ->
273 274 275 276 277 278 279
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
      let pat_pl = List.fold_left2
          (fun acc pv pp -> if not pv.pv_ghost then (pat pp) :: acc else acc)
          [] args pl
      in
      ML.Papp (ls.ls_name, List.rev pat_pl)
280

Mário Pereira's avatar
Mário Pereira committed
281 282
  (** programs *)

283 284 285 286 287
  let pv_name pv = pv.pv_vs.vs_name

  let is_underscore pv =
    (pv_name pv).id_string = "_" && ity_equal pv.pv_ity ity_unit

288 289 290
  (* individual types *)
  let rec ity t =
    match t.ity_node with
291
    | Ityvar (tvs, _) ->
292
      ML.Tvar tvs
293
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
294
      ML.Ttuple (List.map ity itl)
295
    | Ityapp ({its_ts = ts}, itl, _) ->
296 297 298 299
      ML.Tapp (ts.ts_name, List.map ity itl)
    | Ityreg {reg_its = its; reg_args = args} ->
      let args = List.map ity args in
      ML.Tapp (its.its_ts.ts_name, args)
Mário Pereira's avatar
Mário Pereira committed
300

Mário Pereira's avatar
Mário Pereira committed
301
  let pvty pv =
302 303 304 305 306
    if pv.pv_ghost then
      ML.mk_var (pv_name pv) ML.tunit true
    else
      let (vs, vs_ty) = vsty pv.pv_vs in
      ML.mk_var vs vs_ty false
Mário Pereira's avatar
Mário Pereira committed
307

308 309 310 311
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
312 313 314 315
  (* function arguments *)
  let args = (* point-free *)
    List.map pvty

Mário Pereira's avatar
Mário Pereira committed
316 317 318 319 320 321 322 323 324 325 326 327 328 329
  let isconstructor info rs =
    match Mid.find_opt rs.rs_name info.info_mo_known_map with
    | Some {pd_node = PDtype its} ->
      let is_constructor its =
        List.exists (rs_equal rs) its.itd_constructors in
      List.exists is_constructor its
    | _ -> false

  let make_eta_expansion rsc pvl cty_app =
    (* FIXME : effects and types of the expression in this situation *)
    let args_f =
      let def pv = pv_name pv, ity pv.pv_ity, pv.pv_ghost in
      filter_ghost_params pv_not_ghost def cty_app.cty_args in
    let args =
330
      let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
Mário Pereira's avatar
Mário Pereira committed
331 332 333 334 335 336 337 338 339 340 341 342 343 344
      let args = filter_ghost_params pv_not_ghost def pvl in
      let extra_args =
        (* FIXME : ghost status in this extra arguments *)
        List.map def cty_app.cty_args in
      args @ extra_args in
    let eapp =
      ML.mk_expr (ML.Eapp (rsc, args)) (ML.C cty_app) cty_app.cty_effect in
    ML.mk_expr (ML.Efun (args_f, eapp)) (ML.C cty_app) cty_app.cty_effect

  let app info rs pvl =
    let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
    if isconstructor info rs then
      filter_ghost_params pv_not_ghost def pvl
    else
345
      let al _ = ML.mk_unit in
Mário Pereira's avatar
Mário Pereira committed
346
      filter2_ghost_params pv_not_ghost def al pvl
347

Mário Pereira's avatar
Mário Pereira committed
348
  (* expressions *)
349
  let rec expr info ({e_effect = eff} as e) =
Mário Pereira's avatar
Mário Pereira committed
350
    assert (not eff.eff_ghost);
Mário Pereira's avatar
Mário Pereira committed
351
    match e.e_node with
352 353 354
    | Econst c ->
       let c = match c with Number.ConstInt c -> c | _ -> assert false in
       ML.mk_expr (ML.Econst c) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
355
    | Evar pvs ->
356
      ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
357 358
    | Elet (LDvar (pvs, e1), e2) when is_underscore pvs && e_ghost e2 ->
      ML.mk_expr (ML.eseq (expr info e1) ML.mk_unit) (ML.I e.e_ity) eff
359 360 361 362 363
    | Elet (LDvar (pvs, e1), e2) when is_underscore pvs ->
      ML.mk_expr (ML.eseq (expr info e1) (expr info e2)) (ML.I e.e_ity) eff
    | Elet (LDvar (pvs, e1), e2) when e_ghost e1 ->
      let ml_let = ML.ml_let pvs ML.mk_unit (expr info e2) in
       ML.mk_expr ml_let (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
364
    | Elet (LDvar (pvs, e1), e2) ->
365 366 367 368 369
      let ml_let = ML.ml_let pvs (expr info e1) (expr info e2) in
      ML.mk_expr ml_let (ML.I e.e_ity) eff
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
      let def pv = pv_name pv, ity pv.pv_ity, pv.pv_ghost in
      let al pv = pv_name pv, ML.tunit, false in
Mário Pereira's avatar
Mário Pereira committed
370
      let args = filter2_ghost_params pv_not_ghost def al cty.cty_args in
371 372 373 374
      let ef = expr info ef in
      let ein = expr info ein in
      let ml_letrec = ML.Eletrec (false, [rs, args, ef], ein) in
      ML.mk_expr ml_letrec (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
375 376 377 378 379 380 381 382 383
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein)
      when isconstructor info rs_app ->

      let eta_app = make_eta_expansion rs_app pvl cty in
      let ein = expr info ein in
      let ml_letrec = ML.Eletrec (false, [rsf, [], eta_app], ein) in
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
      let pvl = app info rs_app pvl in
384
      let eapp =
Mário Pereira's avatar
Mário Pereira committed
385
        ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
386 387 388
      let ein = expr info ein in
      let ml_letrec = ML.Eletrec (false, [rsf, [], eapp], ein) in
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
389 390 391 392
    | Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs ->
      ML.mk_unit
    | Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
      ML.mk_unit
Mário Pereira's avatar
Mário Pereira committed
393
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
394 395
      let pvl = app info rs pvl in
      ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
396 397 398
    | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
      let def pv = pv_name pv, ity pv.pv_ity, pv.pv_ghost in
      let al pv = pv_name pv, ML.tunit, false in
Mário Pereira's avatar
Mário Pereira committed
399
      let args = filter2_ghost_params pv_not_ghost def al cty.cty_args in
400
      ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
401
    | Eexec ({c_node = Cany}, _) -> assert false
402
    | Eabsurd ->
403 404 405
      ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
    | Ecase (e1, _) when e_ghost e1 ->
      ML.mk_unit
406
    | Ecase (e1, pl) ->
407 408
       let e1 = expr info e1 in
       let pl = List.map (ebranch info) pl in
409 410 411
       ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) eff
    | Eassert _ ->
       ML.mk_unit
412
    | Eif (e1, e2, e3) ->
413 414 415
       let e1 = expr info e1 in
       let e2 = expr info e2 in
       let e3 = expr info e3 in
416
       ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
417 418 419 420 421
    | Ewhile (e1, _, _, e2) ->
      let e1 = expr info e1 in
      let e2 = expr info e2 in
      ML.mk_expr (ML.Ewhile (e1, e2)) (ML.I e.e_ity) eff
    | Efor (pv1, (pv2, direction, pv3), _, efor) ->
Mário Pereira's avatar
Mário Pereira committed
422
      let efor = expr info efor in
Mário Pereira's avatar
Mário Pereira committed
423
      let direction = for_direction direction in
Mário Pereira's avatar
Mário Pereira committed
424 425
      ML.mk_expr (ML.Efor (pv1, pv2, direction, pv3, efor)) (ML.I e.e_ity) eff
    | Eghost _ ->
Mario Pereira's avatar
Mario Pereira committed
426
      assert false
Mário Pereira's avatar
Mário Pereira committed
427 428
    | Eassign [(rho, rs, pv)] ->
      ML.mk_expr (ML.Eassign [(rho, rs, pv)]) (ML.I e.e_ity) eff
429 430
    | Epure _ -> assert false
    | Etry _ -> assert false
Mário Pereira's avatar
Mário Pereira committed
431 432 433 434 435 436 437 438 439
    | Eraise (xs, ex) ->
      let ex =
        let open ML in
        match expr info ex with
        | {e_node = Eblock []} -> None
        | e -> Some e
      in
      let exn = ML.Xident xs.xs_name in
      ML.mk_expr (ML.Eraise (exn, ex)) (ML.I e.e_ity) eff
440 441
    | _ -> (* TODO *) assert false

Mário Pereira's avatar
Mário Pereira committed
442 443
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
444

445 446 447 448
  let its_args ts = ts.its_ts.ts_args
  let itd_name td = td.itd_its.its_ts.ts_name

  (* type declarations/definitions *)
Mário Pereira's avatar
Mário Pereira committed
449
  let tdef info itd =
450
    let s = itd.itd_its in
451 452 453
    let ddata_constructs = (* point-free *)
      List.map (fun ({rs_cty = rsc} as rs) ->
          rs.rs_name,
Mário Pereira's avatar
Mário Pereira committed
454
          let args = List.filter pv_not_ghost rsc.cty_args in
455 456
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
457 458 459 460
    let drecord_fields ({rs_cty = rsc} as rs) = (* point-free *)
      (List.exists (pv_equal (Opt.get rs.rs_field)) s.its_mfields),
      rs.rs_name,
      ity rsc.cty_result
461 462 463 464
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
465 466
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
467
        ML.mk_its_defn id args is_private None
468
      | None, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
469 470
        let cl = ddata_constructs cl in
        ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
471
      | None, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
472 473 474
        let p e = not (rs_ghost e) in
        let pjl = filter_ghost_params p drecord_fields pjl in
        ML.mk_its_defn id args is_private (Some (ML.Drecord pjl))
475
      | Some t, _, _ ->
476
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
477
    end
Mário Pereira's avatar
Mário Pereira committed
478

Mário Pereira's avatar
Mário Pereira committed
479 480 481 482 483
  let is_val e =
    match e.e_node with
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
484
  (* program declarations *)
485
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
486
    match pd.pd_node with
487
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mario Pereira's avatar
Mario Pereira committed
488 489
       []
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e ->
Mário Pereira's avatar
Mário Pereira committed
490
      []
491
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
492 493 494 495 496
      let args_filter =
        let p (_, _, is_ghost) = not is_ghost in
        let def = fun x -> x in
        let al = fun x -> x in
        filter2_ghost_params p def al (args cty.cty_args) in
Mario Pereira's avatar
Mario Pereira committed
497
      [ML.Dlet (rs, args_filter, expr info e)]
498
    | PDlet (LDrec rl) ->
499
      let rec_def =
Mario Pereira's avatar
Mario Pereira committed
500
        List.map (fun {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} ->
501 502 503 504 505
          let e = match e.c_node with Cfun e -> e | _ -> assert false in
          let args_filter =
            let p (_, _, is_ghost) = not is_ghost in
            let def = fun x -> x in
            let al = fun x -> x in
Mario Pereira's avatar
Mario Pereira committed
506 507 508
            filter2_ghost_params p def al (args rs1.rs_cty.cty_args) in
          { ML.rec_sym = rs1; ML.rec_rsym = rs2;
            ML.rec_args = args_filter; ML.rec_exp = expr info e }) rl
509
      in
Mario Pereira's avatar
Mario Pereira committed
510
      [ML.Dletrec rec_def]
511
    | PDlet (LDsym _)
Mário Pereira's avatar
Mário Pereira committed
512 513
    | PDpure
    | PDlet (LDvar (_, _)) ->
514
      []
515
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
516
      [ML.Dtype (List.map (tdef info) itl)]
517
    | PDexn xs ->
518
       if ity_equal xs.xs_ity ity_unit then
519
         [ML.Dexn (xs, None)]
520
       else
521
         [ML.Dexn (xs, Some (ity xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
522 523

  (* unit module declarations *)
524
  let mdecl info = function
Mário Pereira's avatar
Mário Pereira committed
525
    | Udecl pd ->
526
       pdecl info pd
527
    |  _ -> (* TODO *) []
Mário Pereira's avatar
Mário Pereira committed
528 529

  (* modules *)
530 531
  let module_ info m =
    List.concat (List.map (mdecl info) m.mod_units)
Mário Pereira's avatar
Mário Pereira committed
532

Mário Pereira's avatar
Mário Pereira committed
533 534 535 536
end

(** Erasure operations related to ghost code *)

Mário Pereira's avatar
Mário Pereira committed
537
(* module Erasure = struct *)
Mário Pereira's avatar
Mário Pereira committed
538

Mário Pereira's avatar
Mário Pereira committed
539
(*   open ML *)
Mário Pereira's avatar
Mário Pereira committed
540 541 542



Mário Pereira's avatar
Mário Pereira committed
543
(* end *)
Mário Pereira's avatar
Mário Pereira committed
544 545 546

(*
 * Local Variables:
547
 * compile-command: "make -C ../.. -j3 bin/why3extract.opt"
Mário Pereira's avatar
Mário Pereira committed
548 549
 * End:
 *)