compile.ml 23.1 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
  let mk_let_var pv e1 e2 =
Mário Pereira's avatar
Mário Pereira committed
175
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
176 177

  let tunit = Ttuple []
178

Mário Pereira's avatar
Mário Pereira committed
179 180 181
  let ity_int         = I ity_int
  let ity_unit        = I ity_unit

182 183 184 185 186
  let enope = Eblock []

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

187 188
  let mk_var id ty ghost = (id, ty, ghost)

189 190
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

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

194 195 196 197 198 199 200 201
  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]

202
end
Mário Pereira's avatar
Mário Pereira committed
203

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

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

246 247 248
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

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

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

Mário Pereira's avatar
Mário Pereira committed
291 292
  (** programs *)

293 294 295 296 297
  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

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

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

318 319 320 321
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

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

350 351 352 353 354 355 356 357 358 359
  (* 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
360 361
  exception ExtractionAny

Mário Pereira's avatar
Mário Pereira committed
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 418 419 420 421 422 423 424 425 426 427 428 429
  let mk_for op_b_rs op_a_rs i_pv from_pv to_pv body eff =
    let body_ity  = ity_func ity_int ity_unit in
    let body_pv   =
      let body_id = id_fresh "body" in create_pvsymbol body_id body_ity in
    let body_expr = ML.mk_expr (ML.Evar body_pv) (ML.I body_ity) eff in
    let i_expr, from_expr, to_expr =
      let ity_int = ML.ity_int in let eff_e = eff_empty in
      ML.mk_expr (ML.Evar i_pv)     ity_int eff_e,
      ML.mk_expr (ML.Evar from_pv)  ity_int eff_e,
      ML.mk_expr (ML.Evar to_pv)    ity_int eff_e in
    let for_rs =
      let for_id  = id_fresh "for_loop_to" in
      let for_cty = create_cty [i_pv; to_pv; body_pv] [] [] Mxs.empty
          Mpv.empty eff ity_unit in
      create_rsymbol for_id for_cty in
    let for_expr =
      let test = ML.mk_expr (ML.Eapp (op_b_rs, [i_expr; to_expr]))
          (ML.I ity_bool) eff_empty in
      let sc_expr = (* expression for "i + 1", to become "Z.add i 1" *)
        let one_const = Number.int_const_dec "1" in
        let one_expr =
          ML.mk_expr (ML.Econst one_const) ML.ity_int eff_empty in
        let i_plus_one = ML.Eapp (op_a_rs, [i_expr; one_expr]) in
        ML.mk_expr i_plus_one ML.ity_int eff_empty in
       let rec_call  =
        ML.mk_expr (ML.Eapp (for_rs, [sc_expr; to_expr; body_expr]))
          ML.ity_unit eff in
      let body_app =
        ML.mk_expr (ML.Eapp (rs_func_app, [body_expr; i_expr]))
          ML.ity_unit eff in
      let seq_expr =
        ML.mk_expr (ML.eseq body_app rec_call) ML.ity_unit eff in
      ML.mk_expr (ML.Eif (test, seq_expr, ML.mk_unit)) ML.ity_unit eff in
    let ty_int = ity ity_int in
    let for_call_expr =
      let body_fun = ML.Efun ([pv_name i_pv, ty_int, false], body) in
      let body_fun_expr = ML.mk_expr body_fun ML.ity_unit eff in
      let for_call = ML.Eapp (for_rs, [i_expr; to_expr; body_fun_expr]) in
      ML.mk_expr for_call ML.ity_unit eff in
    let let_i_for_call_expr =
      let let_i = ML.mk_let_var i_pv from_expr for_call_expr in
      ML.mk_expr let_i ML.ity_unit eff in
    let pv_name pv = pv.pv_vs.vs_name in
    let ty_int_to_unit = ity body_ity in
    let args = [(pv_name    i_pv, ty_int,         false);
                (pv_name   to_pv, ty_int,         false);
                 pv_name body_pv, ty_int_to_unit, false] in
    let for_rec_def = {
      ML.rec_sym = for_rs;
      ML.rec_rsym = for_rs;
      ML.rec_args = args;
      ML.rec_exp = for_expr
    } in
    let for_let = ML.Elet (ML.Lrec [for_rec_def], let_i_for_call_expr) in
    ML.mk_expr for_let ML.ity_unit eff

  let mk_for_downto info i_pv from_pv to_pv body eff =
    let ge_rs, minus_rs =
      let ns = (Opt.get info.info_current_mo).mod_export in
      ns_find_rs ns ["Int"; "infix >="], ns_find_rs ns ["Int"; "infix -"] in
    mk_for ge_rs minus_rs i_pv from_pv to_pv body eff

  let mk_for_to info i_pv from_pv to_pv body eff =
    let le_rs, plus_rs =
      let ns = (Opt.get info.info_current_mo).mod_export in
      ns_find_rs ns ["Int"; "infix <="], ns_find_rs ns ["Int"; "infix +"] in
    mk_for le_rs plus_rs i_pv from_pv to_pv body eff

Mário Pereira's avatar
Mário Pereira committed
430
  (* expressions *)
431
  let rec expr info ({e_effect = eff} as e) =
Mário Pereira's avatar
Mário Pereira committed
432
    assert (not eff.eff_ghost);
Mário Pereira's avatar
Mário Pereira committed
433
    match e.e_node with
434
    | Econst c ->
Mário Pereira's avatar
Mário Pereira committed
435 436
      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
437
    | Evar pvs ->
438
      ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
439 440
    | 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
441 442
    | 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
Mário Pereira's avatar
Mário Pereira committed
443 444
    | Elet (LDvar (_pvs, e1), e2) when e_ghost e1 ->
      expr info e2
Mário Pereira's avatar
Mário Pereira committed
445
    | Elet (LDvar (pvs, e1), e2) ->
Mário Pereira's avatar
Mário Pereira committed
446
      let ml_let = ML.mk_let_var pvs (expr info e1) (expr info e2) in
447 448
      ML.mk_expr ml_let (ML.I e.e_ity) eff
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
449
      let args = params cty.cty_args in
450 451
      let ef = expr info ef in
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
452
      let ml_letrec = ML.Elet (ML.Lsym (rs, args, ef), ein) in
453
      ML.mk_expr ml_letrec (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
454 455 456 457
    | 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
458
      let ml_letrec = ML.Elet (ML.Lsym (rsf, [], eta_app), ein) in
Mário Pereira's avatar
Mário Pereira committed
459 460
      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) ->
461
      (* partial application *)
Mário Pereira's avatar
Mário Pereira committed
462
      let pvl = app pvl in
463
      let eapp =
Mário Pereira's avatar
Mário Pereira committed
464
        ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
465
      let ein = expr info ein in
466 467 468
      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
469 470 471 472
      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 =
Mário Pereira's avatar
Mário Pereira committed
473
        List.map (fun rdef -> match rdef with
Mário Pereira's avatar
Mário Pereira committed
474 475
          | {rec_sym = rs1; rec_rsym = rs2;
             rec_fun = {c_node = Cfun ef; c_cty = cty}} ->
Mário Pereira's avatar
Mário Pereira committed
476 477 478
            let args = params 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 }
Mário Pereira's avatar
Mário Pereira committed
479 480 481
          | _ -> assert false) rdefl
      in
      let ml_letrec = ML.Elet (ML.Lrec rdefl, ein) in
482
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
483 484 485 486
    | 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
487
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
Mário Pereira's avatar
Mário Pereira committed
488
      let pvl = app pvl in
489
      ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
490
    | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
491
      let args = params cty.cty_args in
492
      ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
493
    | Eexec ({c_node = Cany}, _) ->
Mário Pereira's avatar
Mário Pereira committed
494
      raise ExtractionAny
495
    | Eabsurd ->
496 497 498
      ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
    | Ecase (e1, _) when e_ghost e1 ->
      ML.mk_unit
499
    | Ecase (e1, pl) ->
Mário Pereira's avatar
Mário Pereira committed
500 501 502
      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
503
    | Eassert _ ->
Mário Pereira's avatar
Mário Pereira committed
504
      ML.mk_unit
505
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
506 507 508 509
      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
510 511 512 513
    | 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
Mário Pereira's avatar
Mário Pereira committed
514
    | Efor (pv1, (pv2, To, pv3), _, efor) ->
Mário Pereira's avatar
Mário Pereira committed
515
      let efor = expr info efor in
Mário Pereira's avatar
Mário Pereira committed
516 517 518 519 520 521
      mk_for_to info pv1 pv2 pv3 efor eff
      (* let direction = for_direction direction in *)
      (* ML.mk_expr (ML.Efor (pv1, pv2, direction, pv3, efor)) (ML.I e.e_ity) eff *)
    | Efor (pv1, (pv2, DownTo, pv3), _, efor) ->
      let efor = expr info efor in
      mk_for_downto info pv1 pv2 pv3 efor eff
Mário Pereira's avatar
Mário Pereira committed
522
    | Eghost _ ->
Mario Pereira's avatar
Mario Pereira committed
523
      assert false
524 525 526 527
    | 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
528 529 530 531 532 533 534 535 536
    | 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
537 538 539 540 541
    | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _) ->
      assert false (*TODO*)
    | Eexec ({c_node=Cpur (_, _); _ }, _) ->
      assert false (*TODO*)

Mário Pereira's avatar
Mário Pereira committed
542 543
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
544

545 546 547 548
  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
549
  let tdef itd =
550
    let s = itd.itd_its in
551 552 553
    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
554
          let args = List.filter pv_not_ghost rsc.cty_args in
555 556
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
557 558 559 560
    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
561 562 563 564
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
565 566
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
567
        ML.mk_its_defn id args is_private None
568
      | None, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
569 570
        let cl = ddata_constructs cl in
        ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
571
      | None, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
572 573 574
        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))
575
      | Some t, _, _ ->
576
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
577
    end
Mário Pereira's avatar
Mário Pereira committed
578

Mário Pereira's avatar
Mário Pereira committed
579
  exception ExtractionVal of rsymbol
Mário Pereira's avatar
Mário Pereira committed
580

Mário Pereira's avatar
Mário Pereira committed
581
  (* program declarations *)
582
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
583
    match pd.pd_node with
584
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
585
      []
Mário Pereira's avatar
Mário Pereira committed
586 587
    | PDlet (LDsym (rs, {c_node = Cany}))->
      raise (ExtractionVal rs)
588 589
    | PDlet (LDsym ({rs_cty = {cty_args = []}} as rs, {c_node = Cfun e})) ->
      [ML.Dlet (ML.Lsym (rs, [], expr info e))]
590
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
591 592
      let args = params cty.cty_args in
      [ML.Dlet (ML.Lsym (rs, args, expr info e))]
593
    | PDlet (LDrec rl) ->
594
      let rec_def =
Mario Pereira's avatar
Mario Pereira committed
595
        List.map (fun {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} ->
596
          let e = match e.c_node with Cfun e -> e | _ -> assert false in
597
          let args = params rs1.rs_cty.cty_args in
Mario Pereira's avatar
Mario Pereira committed
598
          { ML.rec_sym = rs1; ML.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
599
            ML.rec_args = args; ML.rec_exp = expr info e }) rl in
Mário Pereira's avatar
Mário Pereira committed
600
      [ML.Dlet (ML.Lrec rec_def)]
Mário Pereira's avatar
Mário Pereira committed
601
    | PDlet (LDsym _) | PDpure | PDlet (LDvar (_, _)) ->
602
      []
603
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
604
      [ML.Dtype (List.map tdef itl)]
605
    | PDexn xs ->
Mário Pereira's avatar
Mário Pereira committed
606 607
      if ity_equal xs.xs_ity ity_unit then [ML.Dexn (xs, None)]
      else [ML.Dexn (xs, Some (ity xs.xs_ity))]
Mário Pereira's avatar
Mário Pereira committed
608 609

  (* unit module declarations *)
610
  let mdecl info = function
Mário Pereira's avatar
Mário Pereira committed
611
    | Udecl pd ->
612
       pdecl info pd
613
    |  _ -> (* TODO *) []
Mário Pereira's avatar
Mário Pereira committed
614 615

  (* modules *)
616 617
  let module_ info m =
    List.concat (List.map (mdecl info) m.mod_units)
Mário Pereira's avatar
Mário Pereira committed
618

Mário Pereira's avatar
Mário Pereira committed
619 620 621 622 623 624 625 626
  let () = Exn_printer.register (fun fmt e -> match e with
    | ExtractionAny ->
      Format.fprintf fmt "Cannot extract an undefined node"
    | ExtractionVal rs ->
      Format.fprintf fmt "Function %a cannot be extracted"
        print_rs rs
    | _ -> raise e)

Mário Pereira's avatar
Mário Pereira committed
627 628
end

629 630 631 632 633 634 635 636
(** Some transformations *)

module Transform = struct

  open ML

  type subst = expr Mpv.t

Mário Pereira's avatar
Mário Pereira committed
637
  let rec expr info subst e =
638
    let mk n = { e with e_node = n } in
Mário Pereira's avatar
Mário Pereira committed
639
    let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
640 641 642
    match e.e_node with
    | Evar pv ->
      (try Mpv.find pv subst with Not_found -> e)
Mário Pereira's avatar
Mário Pereira committed
643
    | Elet (Lvar (pv, ({e_node = Econst _ } as e1)), e2)
Mário Pereira's avatar
Mário Pereira committed
644
    | Elet (Lvar (pv, ({e_node = Eblock []} as e1)), e2) ->
Mário Pereira's avatar
Mário Pereira committed
645 646 647
      add_subst pv e1 e2
    | Elet (Lvar (pv, ({e_node = Eapp (rs, [])} as e1)), e2)
      when Translate.isconstructor info rs ->
Mário Pereira's avatar
Mário Pereira committed
648
      (* only optimize constructors with no argument *)
Mário Pereira's avatar
Mário Pereira committed
649
      (* because of Lvar we know the constructor is completely applied *)
Mário Pereira's avatar
Mário Pereira committed
650
      add_subst pv e1 e2
651
    | Elet (ld, e) ->
Mário Pereira's avatar
Mário Pereira committed
652
      mk (Elet (let_def info subst ld, expr info subst e))
653
    | Eapp (rs, el) ->
Mário Pereira's avatar
Mário Pereira committed
654
      mk (Eapp (rs, List.map (expr info subst) el))
655
    | Efun (vl, e) ->
Mário Pereira's avatar
Mário Pereira committed
656
      mk (Efun (vl, expr info subst e))
657
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
658
      mk (Eif (expr info subst e1, expr info subst e2, expr info subst e3))
659
    | Ecast (e, ty) ->
Mário Pereira's avatar
Mário Pereira committed
660
      mk (Ecast (expr info subst e, ty))
661
    | Etuple el ->
Mário Pereira's avatar
Mário Pereira committed
662
      mk (Etuple (List.map (expr info subst) el))
663
    | Ematch (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
664
      mk (Ematch (expr info subst e, List.map (branch info subst) bl))
665
    | Ebinop (e1, op, e2) ->
Mário Pereira's avatar
Mário Pereira committed
666
      mk (Ebinop (expr info subst e1, op, expr info subst e2))
667
    | Enot e ->
Mário Pereira's avatar
Mário Pereira committed
668
      mk (Enot (expr info subst e))
669
    | Eblock el ->
Mário Pereira's avatar
Mário Pereira committed
670
      mk (Eblock (List.map (expr info subst) el))
671
    | Ewhile (e1, e2) ->
Mário Pereira's avatar
Mário Pereira committed
672
      mk (Ewhile (expr info subst e1, expr info subst e2))
673
    | Efor (x, pv1, dir, pv2, e) ->
Mário Pereira's avatar
Mário Pereira committed
674
      let e = mk (Efor (x, pv1, dir, pv2, expr info subst e)) in
675 676 677
      (* be careful when pv1 and pv2 are in subst *)
      mk_let subst pv1 (mk_let subst pv2 e)
    | Eraise (exn, eo) ->
Mário Pereira's avatar
Mário Pereira committed
678
      mk (Eraise (exn, Opt.map (expr info subst) eo))
679
    | Etry (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
680
      mk (Etry (expr info subst e, List.map (xbranch info subst) bl))
681 682 683 684 685 686 687 688 689 690 691
    | 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

Mário Pereira's avatar
Mário Pereira committed
692 693
  and branch info subst (pat, e) = pat, expr info subst e
  and xbranch info subst (exn, pat, e) = exn, pat, expr info subst e
694

Mário Pereira's avatar
Mário Pereira committed
695
  and let_def info subst = function
696 697
    | Lvar (pv, e) ->
      assert (not (Mpv.mem pv subst)); (* no capture *)
Mário Pereira's avatar
Mário Pereira committed
698
      Lvar (pv, expr info subst e)
699
    | Lsym (rs, args, e) ->
Mário Pereira's avatar
Mário Pereira committed
700 701
      Lsym (rs, args, expr info subst e)
    | Lrec rl -> Lrec (List.map (rdef info subst) rl)
702

Mário Pereira's avatar
Mário Pereira committed
703 704
  and rdef info subst r =
    { r with rec_exp = expr info subst r.rec_exp }
705

Mário Pereira's avatar
Mário Pereira committed
706
  let decl info = function
707
    | Dtype _ | Dexn _ as d -> d
Mário Pereira's avatar
Mário Pereira committed
708
    | Dlet def -> Dlet (let_def info Mpv.empty def)
709

Mário Pereira's avatar
Mário Pereira committed
710 711
  let module_ info  =
    List.map (decl info)
712 713

end
Mário Pereira's avatar
Mário Pereira committed
714 715 716

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