compile.ml 18 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
  type pat =
    | Pwild
    | Pident  of ident
Mário Pereira's avatar
Mário Pereira committed
94
    | Papp    of lsymbol * pat list
95 96 97 98 99 100 101 102 103
    | Ptuple  of 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
104
    | Xident of ident
105

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

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

  and expr_node =
    | Econst  of Number.integer_constant
117
    | Evar    of pvsymbol
118
    | Eapp    of rsymbol * expr list
119
    | Efun    of var list * expr
Mário Pereira's avatar
Mário Pereira committed
120
    | Elet    of let_def * expr
121 122
    | Eif     of expr * expr * expr
    | Ecast   of expr * ty
Mário Pereira's avatar
Mário Pereira committed
123
    | Eassign of (pvsymbol * rsymbol * pvsymbol) list
124 125 126 127 128 129
    | 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
130
    | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
131
    | Eraise  of exn * expr option
132
    | Etry    of expr * (exn * pvsymbol option * expr) list
133 134
    | Eabsurd

Mário Pereira's avatar
Mário Pereira committed
135 136 137 138 139 140 141 142 143 144 145 146
  and let_def =
    | Lvar of pvsymbol * expr
    | Lsym of rsymbol * var list * expr
    | Lrec of rdef list

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

147 148 149 150 151 152 153
  type is_mutable = bool

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

154 155 156 157 158 159 160
  type its_defn = {
    its_name    : ident;
    its_args    : tvsymbol list;
    its_private : bool;
    its_def     : typedef option;
  }

161
  type decl = (* TODO add support for the extraction of ocaml modules *)
Mario Pereira's avatar
Mario Pereira committed
162
    | Dtype   of its_defn list
Mário Pereira's avatar
Mário Pereira committed
163
    | Dlet    of let_def
164
        (* TODO add return type? *)
Mario Pereira's avatar
Mario Pereira committed
165 166
    | Dexn    of xsymbol * ty option

Mário Pereira's avatar
Mário Pereira committed
167 168
  (* type pmodule = { *)
  (* } *)
169

170
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
171 172
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

173
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
174 175
  let ml_let_var pv e1 e2 =
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
176 177

  let tunit = Ttuple []
178

179 180 181 182 183
  let enope = Eblock []

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

184 185 186 187 188
  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; }

189 190 191 192 193 194 195 196
  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]

197
end
Mário Pereira's avatar
Mário Pereira committed
198

199 200 201 202 203 204 205 206 207 208
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
209 210 211 212 213 214 215
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
216 217 218 219 220 221 222 223 224
(** 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
225 226 227
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
228 229 230 231
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
232
       ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
233 234 235 236 237 238 239 240
    | 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

241 242 243
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

Mário Pereira's avatar
Mário Pereira committed
244
  let filter_ghost_params p def l =
245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264
    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)

265 266 267
  let rec pat p =
    match p.pat_node with
    | Pwild ->
268
      ML.Pwild
269
    | Pvar vs ->
270
      ML.Pident vs.vs_name
271
    | Por (p1, p2) ->
272
      ML.Por (pat p1, pat p2)
273
    | Pas (p, vs) ->
274
      ML.Pas (pat p, vs.vs_name)
275
    | Papp (ls, pl) when is_fs_tuple ls ->
276
      ML.Ptuple (List.map pat pl)
277
    | Papp (ls, pl) ->
278 279 280 281 282 283
      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
Mário Pereira's avatar
Mário Pereira committed
284
      ML.Papp (ls, List.rev pat_pl)
285

Mário Pereira's avatar
Mário Pereira committed
286 287
  (** programs *)

288 289 290 291 292
  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

293 294 295
  (* individual types *)
  let rec ity t =
    match t.ity_node with
296
    | Ityvar (tvs, _) ->
297
      ML.Tvar tvs
298
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
299
      ML.Ttuple (List.map ity itl)
300
    | Ityapp ({its_ts = ts}, itl, _) ->
301 302 303 304
      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
305

Mário Pereira's avatar
Mário Pereira committed
306
  let pvty pv =
307 308 309 310 311
    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
312

313 314 315 316
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
317 318 319 320
  (* function arguments *)
  let args = (* point-free *)
    List.map pvty

Mário Pereira's avatar
Mário Pereira committed
321 322 323 324 325 326 327 328 329 330 331 332 333 334
  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 =
335
      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
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

Mário Pereira's avatar
Mário Pereira committed
345
  let app pvl =
Mário Pereira's avatar
Mário Pereira committed
346
    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
347
    filter_ghost_params pv_not_ghost def pvl
Mário Pereira's avatar
Mário Pereira committed
348

Mário Pereira's avatar
Mário Pereira committed
349
  (* expressions *)
350
  let rec expr info ({e_effect = eff} as e) =
Mário Pereira's avatar
Mário Pereira committed
351
    assert (not eff.eff_ghost);
Mário Pereira's avatar
Mário Pereira committed
352
    match e.e_node with
353
    | Econst c ->
Mário Pereira's avatar
Mário Pereira committed
354 355
      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
356
    | Evar pvs ->
357
      ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
358 359
    | 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
360 361 362
    | 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 ->
Mário Pereira's avatar
Mário Pereira committed
363 364
      let ml_let = ML.ml_let_var 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
365
    | Elet (LDvar (pvs, e1), e2) ->
Mário Pereira's avatar
Mário Pereira committed
366
      let ml_let = ML.ml_let_var pvs (expr info e1) (expr info e2) in
367 368 369 370
      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
371
      let args = filter2_ghost_params pv_not_ghost def al cty.cty_args in
372 373
      let ef = expr info ef in
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
374
      let ml_letrec = ML.Elet (ML.Lsym (rs, args, ef), ein) in
375
      ML.mk_expr ml_letrec (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
376 377 378 379 380
    | 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
Mário Pereira's avatar
Mário Pereira committed
381
      let ml_letrec = ML.Elet (ML.Lsym (rsf, [], eta_app), ein) in
Mário Pereira's avatar
Mário Pereira committed
382 383
      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) ->
Mário Pereira's avatar
Mário Pereira committed
384
      let pvl = app pvl in
385
      let eapp =
Mário Pereira's avatar
Mário Pereira committed
386
        ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
387
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406
      let ml_letrec = ML.Elet (ML.Lsym (rsf, [], eapp), ein) in
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
    | Elet (LDrec rdefl, 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
      let ein = expr info ein in
      let rdefl =
        List.map (fun rdef ->
          match rdef with
          | {rec_sym = rs1; rec_rsym = rs2;
             rec_fun = {c_node = Cfun ef; c_cty = cty}} ->
            let args =
              filter2_ghost_params pv_not_ghost def al cty.cty_args in
            let ef = expr info ef in
            { ML.rec_sym = rs1; ML.rec_rsym = rs2;
              ML.rec_args = args; ML.rec_exp = ef }
          | _ -> assert false) rdefl
      in
      let ml_letrec = ML.Elet (ML.Lrec rdefl, ein) in
407
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
408 409 410 411
    | 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
412
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
Mário Pereira's avatar
Mário Pereira committed
413
      let pvl = app pvl in
414
      ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
415 416 417
    | 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
418
      let args = filter2_ghost_params pv_not_ghost def al cty.cty_args in
419
      ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
420 421
    | Eexec ({c_node = Cany}, _) ->
      (* Error message here *) assert false
422
    | Eabsurd ->
423 424 425
      ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
    | Ecase (e1, _) when e_ghost e1 ->
      ML.mk_unit
426
    | Ecase (e1, pl) ->
Mário Pereira's avatar
Mário Pereira committed
427 428 429
      let e1 = expr info e1 in
      let pl = List.map (ebranch info) pl in
      ML.mk_expr (ML.Ematch (e1, pl)) (ML.I e.e_ity) eff
430
    | Eassert _ ->
Mário Pereira's avatar
Mário Pereira committed
431
      ML.mk_unit
432
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
433 434 435 436
      let e1 = expr info e1 in
      let e2 = expr info e2 in
      let e3 = expr info e3 in
      ML.mk_expr (ML.Eif (e1, e2, e3)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
437 438 439 440 441
    | 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
442
      let efor = expr info efor in
Mário Pereira's avatar
Mário Pereira committed
443
      let direction = for_direction direction in
Mário Pereira's avatar
Mário Pereira committed
444 445
      ML.mk_expr (ML.Efor (pv1, pv2, direction, pv3, efor)) (ML.I e.e_ity) eff
    | Eghost _ ->
Mario Pereira's avatar
Mario Pereira committed
446
      assert false
Mário Pereira's avatar
Mário Pereira committed
447 448
    | Eassign [(rho, rs, pv)] ->
      ML.mk_expr (ML.Eassign [(rho, rs, pv)]) (ML.I e.e_ity) eff
449 450
    | Epure _ -> assert false
    | Etry _ -> assert false
Mário Pereira's avatar
Mário Pereira committed
451 452 453 454 455 456 457 458 459
    | 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
460 461
    | _ -> (* TODO *) assert false

Mário Pereira's avatar
Mário Pereira committed
462 463
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
464

465 466 467 468
  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
469
  let tdef itd =
470
    let s = itd.itd_its in
471 472 473
    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
474
          let args = List.filter pv_not_ghost rsc.cty_args in
475 476
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
477 478 479 480
    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
481 482 483 484
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
485 486
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
487
        ML.mk_its_defn id args is_private None
488
      | None, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
489 490
        let cl = ddata_constructs cl in
        ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
491
      | None, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
492 493 494
        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))
495
      | Some t, _, _ ->
496
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
497
    end
Mário Pereira's avatar
Mário Pereira committed
498

Mário Pereira's avatar
Mário Pereira committed
499 500 501 502 503
  let is_val e =
    match e.e_node with
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
504
  (* program declarations *)
505
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
506
    match pd.pd_node with
507
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mario Pereira's avatar
Mario Pereira committed
508 509
       []
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e ->
Mário Pereira's avatar
Mário Pereira committed
510
      []
511
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
512 513 514 515 516
      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
Mário Pereira's avatar
Mário Pereira committed
517
      [ML.Dlet (ML.Lsym (rs, args_filter, expr info e))]
518
    | PDlet (LDrec rl) ->
519
      let rec_def =
Mario Pereira's avatar
Mario Pereira committed
520
        List.map (fun {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} ->
521 522 523 524 525
          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
526 527 528
            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
529
      in
Mário Pereira's avatar
Mário Pereira committed
530
      [ML.Dlet (ML.Lrec rec_def)]
531
    | PDlet (LDsym _)
Mário Pereira's avatar
Mário Pereira committed
532 533
    | PDpure
    | PDlet (LDvar (_, _)) ->
534
      []
535
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
536
      [ML.Dtype (List.map tdef itl)]
537
    | PDexn xs ->
538
       if ity_equal xs.xs_ity ity_unit then
539
         [ML.Dexn (xs, None)]
540
       else
541
         [ML.Dexn (xs, Some (ity xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
542 543

  (* unit module declarations *)
544
  let mdecl info = function
Mário Pereira's avatar
Mário Pereira committed
545
    | Udecl pd ->
546
       pdecl info pd
547
    |  _ -> (* TODO *) []
Mário Pereira's avatar
Mário Pereira committed
548 549

  (* modules *)
550 551
  let module_ info m =
    List.concat (List.map (mdecl info) m.mod_units)
Mário Pereira's avatar
Mário Pereira committed
552

Mário Pereira's avatar
Mário Pereira committed
553 554
end

Mário Pereira's avatar
Mário Pereira committed
555
(** Optimistion operations *)
Mário Pereira's avatar
Mário Pereira committed
556

Mário Pereira's avatar
Mário Pereira committed
557
(* module Erasure = struct *)
Mário Pereira's avatar
Mário Pereira committed
558

Mário Pereira's avatar
Mário Pereira committed
559
(*   open ML *)
Mário Pereira's avatar
Mário Pereira committed
560

Mário Pereira's avatar
Mário Pereira committed
561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579
(*   let rec remove_superf_let subs e = *)
(*     match e.e_node with *)
(*     | Evar pv -> try let Hpv.find pv  *)
(*     | Eapp    of rsymbol * expr list *)
(*     | Efun    of var list * expr *)
(*     | Elet    of let_def * expr *)
(*     | Eif     of expr * expr * expr *)
(*     | Ecast   of expr * ty *)
(*     | Eassign of (pvsymbol * rsymbol * pvsymbol) list *)
(*     | 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 *)
(*     | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr *)
(*     | Eraise  of exn * expr option *)
(*     | Etry    of expr * (exn * pvsymbol option * expr) list *)
(*     | _ -> e.e_node *)
Mário Pereira's avatar
Mário Pereira committed
580

Mário Pereira's avatar
Mário Pereira committed
581
(* end *)
Mário Pereira's avatar
Mário Pereira committed
582 583 584

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