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

Mário Pereira's avatar
Mário Pereira committed
76 77 78 79 80 81 82 83 84 85 86 87 88 89
let clean_name fname =
  (* TODO: replace with Filename.remove_extension
   * after migration to OCaml 4.04+ *)
  let remove_extension s =
    try Filename.chop_extension s with Invalid_argument _ -> s in
  let f = Filename.basename fname in (remove_extension f)

let module_name ?fname path t =
  let fname    = match fname, path with
    | None, "why3"::_ -> "why3"
    | None, _   -> String.concat "__" path
    | Some f, _ -> clean_name f in
  fname ^ "__" ^ t

90 91
module ML = struct

92 93
  open Expr

94
  type ty =
95
    | Tvar    of tvsymbol
96 97 98
    | Tapp    of ident * ty list
    | Ttuple  of ty list

99 100 101
  type is_ghost = bool

  type var = ident * ty * is_ghost
102

Mário Pereira's avatar
Mário Pereira committed
103 104
  type for_direction = To | DownTo

105 106 107
  type pat =
    | Pwild
    | Pident  of ident
Mário Pereira's avatar
Mário Pereira committed
108
    | Papp    of lsymbol * pat list
109 110 111 112 113 114 115 116
    | Ptuple  of pat list
    | Por     of pat * pat
    | Pas     of pat * ident

  type is_rec = bool

  type binop = Band | Bor | Beq

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

119
  type expr = {
Mário Pereira's avatar
Mário Pereira committed
120 121 122
    e_node   : expr_node;
    e_ity    : ity;
    e_effect : effect;
123
    (* TODO: add the set of free variables? *)
124 125 126 127
  }

  and expr_node =
    | Econst  of Number.integer_constant
128
    | Evar    of pvsymbol
129
    | Eapp    of rsymbol * expr list
130
    | Efun    of var list * expr
Mário Pereira's avatar
Mário Pereira committed
131
    | Elet    of let_def * expr
132
    | Eif     of expr * expr * expr
Mário Pereira's avatar
Mário Pereira committed
133
    (* | Ecast   of expr * ty *)
Mário Pereira's avatar
Mário Pereira committed
134
    | Eassign of (pvsymbol * rsymbol * pvsymbol) list
135 136 137
    | Ematch  of expr * (pat * expr) list
    | Eblock  of expr list
    | Ewhile  of expr * expr
Mário Pereira's avatar
Mário Pereira committed
138 139
    (* For loop for Why3's type int *)
    | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
Mário Pereira's avatar
Mário Pereira committed
140 141
    | Eraise  of xsymbol * expr option
    | Etry    of expr * (xsymbol * pvsymbol list * expr) list
142 143
    | Eabsurd

Mário Pereira's avatar
Mário Pereira committed
144 145
  and let_def =
    | Lvar of pvsymbol * expr
Mário Pereira's avatar
Mário Pereira committed
146
    | Lsym of rsymbol * ty * var list * expr
Mário Pereira's avatar
Mário Pereira committed
147 148 149 150 151 152 153
    | Lrec of rdef list

  and rdef = {
    rec_sym  : rsymbol; (* exported *)
    rec_rsym : rsymbol; (* internal *)
    rec_args : var list;
    rec_exp  : expr;
Mário Pereira's avatar
Mário Pereira committed
154
    rec_res  : ty;
Mário Pereira's avatar
Mário Pereira committed
155 156
  }

157 158 159 160 161 162 163
  type is_mutable = bool

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

164 165 166 167 168 169 170
  type its_defn = {
    its_name    : ident;
    its_args    : tvsymbol list;
    its_private : bool;
    its_def     : typedef option;
  }

171
  type decl = (* TODO add support for the extraction of ocaml modules *)
Mario Pereira's avatar
Mario Pereira committed
172
    | Dtype   of its_defn list
Mário Pereira's avatar
Mário Pereira committed
173
    | Dlet    of let_def
174
        (* TODO add return type? *)
Mario Pereira's avatar
Mario Pereira committed
175 176
    | Dexn    of xsymbol * ty option

177 178
  type pmodule =
    decl list
179

180
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
181 182
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

183
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
184
  let mk_let_var pv e1 e2 =
Mário Pereira's avatar
Mário Pereira committed
185
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
186 187

  let tunit = Ttuple []
188

Mário Pereira's avatar
Mário Pereira committed
189 190
  let ity_int  = I ity_int
  let ity_unit = I ity_unit
Mário Pereira's avatar
Mário Pereira committed
191

192 193 194 195 196
  let enope = Eblock []

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

197 198
  let mk_var id ty ghost = (id, ty, ghost)

199 200
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

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

204 205 206 207 208 209 210 211
  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]

212
end
Mário Pereira's avatar
Mário Pereira committed
213 214 215 216 217

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
218 219 220
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
221

Mário Pereira's avatar
Mário Pereira committed
222 223 224 225 226 227 228 229 230 231
  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
232 233 234
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

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

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

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

Mário Pereira's avatar
Mário Pereira committed
272 273 274 275 276 277
  let rec filter_ghost_rdef def = function
    | [] -> []
    | { rec_sym = rs; rec_rsym = rrs } :: l
      when rs_ghost rs || rs_ghost rrs -> filter_ghost_rdef def l
    | rdef :: l -> def rdef :: filter_ghost_rdef def l

278 279 280
  let rec pat p =
    match p.pat_node with
    | Pwild ->
281
      ML.Pwild
282
    | Pvar vs ->
283
      ML.Pident vs.vs_name
284
    | Por (p1, p2) ->
285
      ML.Por (pat p1, pat p2)
286
    | Pas (p, vs) ->
287
      ML.Pas (pat p, vs.vs_name)
288
    | Papp (ls, pl) when is_fs_tuple ls ->
289
      ML.Ptuple (List.map pat pl)
290
    | Papp (ls, pl) ->
291 292 293 294 295 296
      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
297
      ML.Papp (ls, List.rev pat_pl)
298

Mário Pereira's avatar
Mário Pereira committed
299 300
  (** programs *)

301 302 303 304 305
  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

306 307 308
  (* individual types *)
  let rec ity t =
    match t.ity_node with
309
    | Ityvar (tvs, _) ->
310
      ML.Tvar tvs
311
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
312
      ML.Ttuple (List.map ity itl)
313
    | Ityapp ({its_ts = ts}, itl, _) ->
314 315 316 317
      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
318

Mário Pereira's avatar
Mário Pereira committed
319
  let pvty pv =
320 321 322 323 324
    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
325

326 327 328 329
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
330 331 332 333 334 335 336 337
  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

Mário Pereira's avatar
Mário Pereira committed
338
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
339 340 341 342 343
    (* 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 =
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 346 347 348 349 350 351 352 353
      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
354
  let app pvl =
Mário Pereira's avatar
Mário Pereira committed
355
    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
356
    filter_ghost_params pv_not_ghost def pvl
Mário Pereira's avatar
Mário Pereira committed
357

358 359 360 361 362 363
  (* 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

Mário Pereira's avatar
Mário Pereira committed
364 365 366 367
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
      if args = [] then [ML.mk_var_unit ()] else args
368

Mário Pereira's avatar
Mário Pereira committed
369
  let mk_for op_b_rs op_a_rs i_pv from_pv to_pv body_expr eff =
Mário Pereira's avatar
Mário Pereira committed
370 371 372 373 374 375
    let i_expr, from_expr, to_expr =
      let int_ity = ML.ity_int in let eff_e = eff_empty in
      ML.mk_expr (ML.Evar i_pv)     int_ity eff_e,
      ML.mk_expr (ML.Evar from_pv)  int_ity eff_e,
      ML.mk_expr (ML.Evar to_pv)    int_ity eff_e in
    let for_rs    =
Mário Pereira's avatar
Mário Pereira committed
376
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
377
      let for_cty = create_cty [i_pv; to_pv] [] [] Mxs.empty
Mário Pereira's avatar
Mário Pereira committed
378
                               Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
379 380 381
      create_rsymbol for_id for_cty in
    let for_expr =
      let test = ML.mk_expr (ML.Eapp (op_b_rs, [i_expr; to_expr]))
Mário Pereira's avatar
Mário Pereira committed
382 383
                            (ML.I ity_bool) eff_empty in
      let next_expr =
Mário Pereira's avatar
Mário Pereira committed
384
        let one_const = Number.int_const_dec "1" in
Mário Pereira's avatar
Mário Pereira committed
385
        let one_expr  =
Mário Pereira's avatar
Mário Pereira committed
386
          ML.mk_expr (ML.Econst one_const) ML.ity_int eff_empty in
Mário Pereira's avatar
Mário Pereira committed
387 388
        let i_op_one = ML.Eapp (op_a_rs, [i_expr; one_expr]) in
        ML.mk_expr i_op_one ML.ity_int eff_empty in
Mário Pereira's avatar
Mário Pereira committed
389
       let rec_call  =
Mário Pereira's avatar
Mário Pereira committed
390
        ML.mk_expr (ML.Eapp (for_rs, [next_expr; to_expr]))
Mário Pereira's avatar
Mário Pereira committed
391
                    ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
392
      let seq_expr =
Mário Pereira's avatar
Mário Pereira committed
393
        ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
394 395
      ML.mk_expr (ML.Eif (test, seq_expr, ML.mk_unit)) ML.ity_unit eff in
    let ty_int = ity ity_int in
Mário Pereira's avatar
Mário Pereira committed
396
    let for_call_expr   =
Mário Pereira's avatar
Mário Pereira committed
397
      let for_call      = ML.Eapp (for_rs, [from_expr; to_expr]) in
Mário Pereira's avatar
Mário Pereira committed
398 399
      ML.mk_expr for_call ML.ity_unit eff in
    let pv_name pv = pv.pv_vs.vs_name in
Mário Pereira's avatar
Mário Pereira committed
400
    let args = [
Mário Pereira's avatar
Mário Pereira committed
401 402
      (pv_name  i_pv, ty_int, false);
      (pv_name to_pv, ty_int, false);
Mário Pereira's avatar
Mário Pereira committed
403
    ] in
Mário Pereira's avatar
Mário Pereira committed
404
    let for_rec_def = {
Mário Pereira's avatar
Mário Pereira committed
405 406
      ML.rec_sym  = for_rs; ML.rec_args = args;
      ML.rec_rsym = for_rs; ML.rec_exp  = for_expr;
Mário Pereira's avatar
Mário Pereira committed
407
      ML.rec_res  = ML.tunit;
Mário Pereira's avatar
Mário Pereira committed
408
    } in
Mário Pereira's avatar
Mário Pereira committed
409
    let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
410 411 412 413 414 415 416 417 418 419 420 421 422 423
    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
424 425
  exception ExtractionAny

Mário Pereira's avatar
Mário Pereira committed
426
  (* expressions *)
427
  let rec expr info ({e_effect = eff} as e) =
Mário Pereira's avatar
Mário Pereira committed
428
    assert (not eff.eff_ghost);
Mário Pereira's avatar
Mário Pereira committed
429
    match e.e_node with
430
    | Econst c ->
Mário Pereira's avatar
Mário Pereira committed
431 432
      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
433
    | Evar pvs ->
434
      ML.mk_expr (ML.Evar pvs) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
435
    | Elet (LDvar (pv, e1), e2) when e_ghost e1 || pv.pv_ghost ->
Mário Pereira's avatar
Mário Pereira committed
436
      expr info e2
Mário Pereira's avatar
Mário Pereira committed
437 438 439 440
    | Elet (LDvar (pv, e1), e2) when is_underscore pv && e_ghost e2 ->
      expr info e1
    | Elet (LDvar (pv, e1), e2) when is_underscore pv ->
      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
441
    | Elet (LDvar (pvs, e1), e2) ->
Mário Pereira's avatar
Mário Pereira committed
442
      let ml_let = ML.mk_let_var pvs (expr info e1) (expr info e2) in
443 444
      ML.mk_expr ml_let (ML.I e.e_ity) eff
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
445
      let args = params cty.cty_args in
446 447
      let ef = expr info ef in
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
448 449
      let res = ity cty.cty_result in
      let ml_letrec = ML.Elet (ML.Lsym (rs, res, args, ef), ein) in
450
      ML.mk_expr ml_letrec (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
451 452
    | Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein)
      when isconstructor info rs_app ->
Mário Pereira's avatar
Mário Pereira committed
453 454
      (* partial application of constructor *)
      let eta_app = mk_eta_expansion rs_app pvl cty in
Mário Pereira's avatar
Mário Pereira committed
455
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
456 457 458
      let mk_func pv f = ity_func pv.pv_ity f in
      let func = List.fold_right mk_func cty.cty_args cty.cty_result in
      let res = ity func in
Mário Pereira's avatar
Mário Pereira committed
459
      let ml_letrec = ML.Elet (ML.Lsym (rsf, res, [], eta_app), ein) in
Mário Pereira's avatar
Mário Pereira committed
460 461
      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) ->
462
      (* partial application *)
Mário Pereira's avatar
Mário Pereira committed
463
      let pvl = app pvl in
464
      let eapp =
Mário Pereira's avatar
Mário Pereira committed
465
        ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
Mário Pereira's avatar
Mário Pereira committed
466 467
      let ein  = expr info ein in
      let res  = ity cty.cty_result in
468 469
      let args =
        if filter_params cty.cty_args = [] then [ML.mk_var_unit ()] else [] in
Mário Pereira's avatar
Mário Pereira committed
470
      let ml_letrec = ML.Elet (ML.Lsym (rsf, res, args, eapp), ein) in
Mário Pereira's avatar
Mário Pereira committed
471 472 473 474
      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
475
        List.map (fun rdef -> match rdef with
Mário Pereira's avatar
Mário Pereira committed
476 477
          | {rec_sym = rs1; rec_rsym = rs2;
             rec_fun = {c_node = Cfun ef; c_cty = cty}} ->
Mário Pereira's avatar
Mário Pereira committed
478
            let res  = ity rs1.rs_cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
479 480
            let args = params cty.cty_args in let ef = expr info ef in
            { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
481
              ML.rec_args = args; ML.rec_exp  = ef ; ML.rec_res  = res }
Mário Pereira's avatar
Mário Pereira committed
482 483 484
          | _ -> assert false) rdefl
      in
      let ml_letrec = ML.Elet (ML.Lrec rdefl, ein) in
485
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
486 487 488 489
    | 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
490 491 492
    | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
      when isconstructor info rs ->
      mk_eta_expansion rs pvl cty
Mário Pereira's avatar
Mário Pereira committed
493
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
Mário Pereira's avatar
Mário Pereira committed
494
      let pvl = app pvl in
495
      ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff
496
    | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
497
      let args = params cty.cty_args in
498
      ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
499
    | Eexec ({c_node = Cany}, _) -> raise ExtractionAny
Mário Pereira's avatar
Mário Pereira committed
500
      (* ML.mk_unit *)
501
    | Eabsurd ->
502 503 504
      ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
    | Ecase (e1, _) when e_ghost e1 ->
      ML.mk_unit
505
    | Ecase (e1, pl) ->
Mário Pereira's avatar
Mário Pereira committed
506 507 508
      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
509
    | Eassert _ ->
Mário Pereira's avatar
Mário Pereira committed
510
      ML.mk_unit
511
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
512 513 514 515
      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
516 517 518 519
    | 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
520
    | Efor (pv1, (pv2, To, pv3), _, efor) ->
Mário Pereira's avatar
Mário Pereira committed
521
      let efor = expr info efor in
Mário Pereira's avatar
Mário Pereira committed
522 523 524 525
      mk_for_to info pv1 pv2 pv3 efor 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
526
    | Eghost _ -> assert false
527 528 529
    | Eassign al ->
      ML.mk_expr (ML.Eassign al) (ML.I e.e_ity) eff
    | Epure _ -> assert false (*TODO*)
Mário Pereira's avatar
Mário Pereira committed
530 531 532 533 534 535
    | Etry (etry, pvl_e_map) ->
      let etry = expr info etry in
      let bl   =
        let bl_map = Mxs.bindings pvl_e_map in
        List.map (fun (xs, (pvl, e)) -> xs, pvl, expr info e) bl_map in
      ML.mk_expr (ML.Etry (etry, bl)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
536 537 538
    | Eraise (xs, ex) ->
      let ex =
        match expr info ex with
Mário Pereira's avatar
Mário Pereira committed
539
        | {ML.e_node = ML.Eblock []} -> None
Mário Pereira's avatar
Mário Pereira committed
540 541
        | e -> Some e
      in
Mário Pereira's avatar
Mário Pereira committed
542
      ML.mk_expr (ML.Eraise (xs, ex)) (ML.I e.e_ity) eff
543 544 545 546 547
    | 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
548 549
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
550

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

Mário Pereira's avatar
Mário Pereira committed
585
  exception ExtractionVal of rsymbol
Mário Pereira's avatar
Mário Pereira committed
586

Mário Pereira's avatar
Mário Pereira committed
587
  (* program declarations *)
588
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
589
    match pd.pd_node with
590
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
591
      []
Mário Pereira's avatar
Mário Pereira committed
592 593 594
    | PDlet (LDsym (_rs, {c_node = Cany})) ->
      []
      (* raise (ExtractionVal _rs) *)
595
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
596
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
597 598
      let res = ity cty.cty_result in
      [ML.Dlet (ML.Lsym (rs, res, args, expr info e))]
599
    | PDlet (LDrec rl) ->
Mário Pereira's avatar
Mário Pereira committed
600
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
601
        let e    = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
602
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
603
        let res  = ity rs1.rs_cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
604
        { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
605 606
          ML.rec_args = args; ML.rec_exp  = expr info e;
          ML.rec_res  = res } in
Mário Pereira's avatar
Mário Pereira committed
607
      let rec_def = filter_ghost_rdef def rl in
Mário Pereira's avatar
Mário Pereira committed
608
      [ML.Dlet (ML.Lrec rec_def)]
Mário Pereira's avatar
Mário Pereira committed
609
    | PDlet (LDsym _) | PDpure | PDlet (LDvar (_, _)) ->
610
      []
611
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
612
      [ML.Dtype (List.map tdef itl)]
613
    | PDexn xs ->
Mário Pereira's avatar
Mário Pereira committed
614 615
      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
616 617

  (* unit module declarations *)
618
  let mdecl info = function
Mário Pereira's avatar
Mário Pereira committed
619
    | Udecl pd ->
620
       pdecl info pd
621
    |  _ -> (* TODO *) []
Mário Pereira's avatar
Mário Pereira committed
622 623

  (* modules *)
624 625
  let module_ info m =
    List.concat (List.map (mdecl info) m.mod_units)
Mário Pereira's avatar
Mário Pereira committed
626

Mário Pereira's avatar
Mário Pereira committed
627 628 629 630 631 632 633 634
  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
635 636
end

637 638 639 640 641 642 643 644
(** Some transformations *)

module Transform = struct

  open ML

  type subst = expr Mpv.t

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

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

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

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

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

end
Mário Pereira's avatar
Mário Pereira committed
716 717 718

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