compile.ml 19.3 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

167 168
  type pmodule =
    decl list
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
  let mk_var id ty ghost = (id, ty, ghost)

186 187
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

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

191 192 193 194 195 196 197 198
  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]

199
end
Mário Pereira's avatar
Mário Pereira committed
200

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

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

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

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

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

Mário Pereira's avatar
Mário Pereira committed
288 289
  (** programs *)

290 291 292 293 294
  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

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

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

315 316 317 318
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
319 320 321 322 323 324 325 326 327 328 329 330 331 332
  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 =
333
      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
334 335 336 337 338 339 340 341 342
      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
343
  let app pvl =
Mário Pereira's avatar
Mário Pereira committed
344
    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
345
    filter_ghost_params pv_not_ghost def pvl
Mário Pereira's avatar
Mário Pereira committed
346

347 348 349 350 351 352 353 354 355 356
  (* function arguments *)
  let filter_params args =
    let args = List.map pvty args in
    let p (_, _, is_ghost) = not is_ghost in
    List.filter p args

  let params args =
    let args = filter_params args in
    if args = [] then [ML.mk_var_unit ()] else args

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

468

Mário Pereira's avatar
Mário Pereira committed
469 470
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
471

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

Mário Pereira's avatar
Mário Pereira committed
506 507 508 509 510
  let is_val e =
    match e.e_node with
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

Mário Pereira's avatar
Mário Pereira committed
511
  (* program declarations *)
512
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
513
    match pd.pd_node with
514
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mario Pereira's avatar
Mario Pereira committed
515 516
       []
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e ->
517
      (* FIXME: check that this symbol is defined in driver *)
Mário Pereira's avatar
Mário Pereira committed
518
      []
519 520
    | PDlet (LDsym ({rs_cty = {cty_args = []}} as rs, {c_node = Cfun e})) ->
      [ML.Dlet (ML.Lsym (rs, [], expr info e))]
521
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
522 523
      let args = params cty.cty_args in
      [ML.Dlet (ML.Lsym (rs, args, expr info e))]
524
    | PDlet (LDrec rl) ->
525
      let rec_def =
Mario Pereira's avatar
Mario Pereira committed
526
        List.map (fun {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} ->
527
          let e = match e.c_node with Cfun e -> e | _ -> assert false in
528
          let args = params rs1.rs_cty.cty_args in
Mario Pereira's avatar
Mario Pereira committed
529
          { ML.rec_sym = rs1; ML.rec_rsym = rs2;
530
            ML.rec_args = args; ML.rec_exp = expr info e }) rl
531
      in
Mário Pereira's avatar
Mário Pereira committed
532
      [ML.Dlet (ML.Lrec rec_def)]
533
    | PDlet (LDsym _)
Mário Pereira's avatar
Mário Pereira committed
534 535
    | PDpure
    | PDlet (LDvar (_, _)) ->
536
      []
537
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
538
      [ML.Dtype (List.map tdef itl)]
539
    | PDexn xs ->
540
       if ity_equal xs.xs_ity ity_unit then
541
         [ML.Dexn (xs, None)]
542
       else
543
         [ML.Dexn (xs, Some (ity xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
544 545

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

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

Mário Pereira's avatar
Mário Pereira committed
555 556
end

557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 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 608 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
(** Some transformations *)

module Transform = struct

  open ML

  type subst = expr Mpv.t

  let rec expr subst e =
    let mk n = { e with e_node = n } in
    match e.e_node with
    | Evar pv ->
      (try Mpv.find pv subst with Not_found -> e)
    | Elet (Lvar (pv, ({e_node = Econst _} as e1)), e2) ->
      expr (Mpv.add pv e1 subst) e2
    | Elet (ld, e) ->
      mk (Elet (let_def subst ld, expr subst e))
    | Eapp (rs, el) ->
      mk (Eapp (rs, List.map (expr subst) el))
    | Efun (vl, e) ->
      mk (Efun (vl, expr subst e))
    | Eif (e1, e2, e3) ->
      mk (Eif (expr subst e1, expr subst e2, expr subst e3))
    | Ecast (e, ty) ->
      mk (Ecast (expr subst e, ty))
    | Etuple el ->
      mk (Etuple (List.map (expr subst) el))
    | Ematch (e, bl) ->
      mk (Ematch (expr subst e, List.map (branch subst) bl))
    | Ebinop (e1, op, e2) ->
      mk (Ebinop (expr subst e1, op, expr subst e2))
    | Enot e ->
      mk (Enot (expr subst e))
    | Eblock el ->
      mk (Eblock (List.map (expr subst) el))
    | Ewhile (e1, e2) ->
      mk (Ewhile (expr subst e1, expr subst e2))
    | Efor (x, pv1, dir, pv2, e) ->
      let e = mk (Efor (x, pv1, dir, pv2, expr subst e)) in
      (* be careful when pv1 and pv2 are in subst *)
      mk_let subst pv1 (mk_let subst pv2 e)
    | Eraise (exn, eo) ->
      mk (Eraise (exn, Opt.map (expr subst) eo))
    | Etry (e, bl) ->
      mk (Etry (expr subst e, List.map (xbranch subst) bl))
    | Eassign al ->
      let assign e (_, _, pv) = mk_let subst pv e in
      List.fold_left assign e al
    | Econst _ | Eabsurd -> e

  and mk_let subst pv e =
    try
      let e1 = Mpv.find pv subst in
      { e with e_node = Elet (Lvar (pv, e1), e) }
    with Not_found -> e

  and branch subst (pat, e) = pat, expr subst e
  and xbranch subst (exn, pat, e) = exn, pat, expr subst e

  and let_def subst = function
    | Lvar (pv, e) ->
      assert (not (Mpv.mem pv subst)); (* no capture *)
      Lvar (pv, expr subst e)
    | Lsym (rs, args, e) ->
      Lsym (rs, args, expr subst e)
    | Lrec rl -> Lrec (List.map (rdef subst) rl)

  and rdef subst r =
    { r with rec_exp = expr subst r.rec_exp }

  let decl = function
    | Dtype _ | Dexn _ as d -> d
    | Dlet def -> Dlet (let_def Mpv.empty def)

  let module_ =
    List.map decl

end
Mário Pereira's avatar
Mário Pereira committed
635 636 637

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