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

Mário Pereira's avatar
Mário Pereira committed
75 76 77 78 79 80 81 82
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 =
Mário Pereira's avatar
Mário Pereira committed
83
  let fname = match fname, path with
Mário Pereira's avatar
Mário Pereira committed
84 85 86 87 88
    | None, "why3"::_ -> "why3"
    | None, _   -> String.concat "__" path
    | Some f, _ -> clean_name f in
  fname ^ "__" ^ t

89 90
module ML = struct

91 92
  open Expr

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

98 99 100
  type is_ghost = bool

  type var = ident * ty * is_ghost
101

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

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

  type is_rec = bool

  type binop = Band | Bor | Beq

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

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

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

Mário Pereira's avatar
Mário Pereira committed
143 144
  and let_def =
    | Lvar of pvsymbol * expr
Mário Pereira's avatar
Mário Pereira committed
145
    | Lsym of rsymbol * ty * var list * expr
Mário Pereira's avatar
Mário Pereira committed
146 147 148 149 150 151 152
    | 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
153
    rec_res  : ty;
Mário Pereira's avatar
Mário Pereira committed
154 155
  }

156 157 158 159 160 161 162
  type is_mutable = bool

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

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

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

Mário Pereira's avatar
Mário Pereira committed
176 177 178 179 180 181 182 183 184 185
  type known_map = decl Mid.t

  type pmodule = {
    mod_decl  : decl list;
    mod_known : known_map;
  }

  let add_known_decl id decl k_map =
    Mid.add id decl k_map

Mário Pereira's avatar
Mário Pereira committed
186 187
  let rec iter_deps_ty f = function
    | Tvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
188
    | Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
Mário Pereira's avatar
Mário Pereira committed
189 190 191
    | Ttuple ty_l -> List.iter (iter_deps_ty f) ty_l

  let iter_deps_typedef f = function
Mário Pereira's avatar
Mário Pereira committed
192 193 194
    | Ddata constrl ->
      List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
    | Drecord _pjl -> assert false (*TODO*)
Mário Pereira's avatar
Mário Pereira committed
195 196 197 198 199 200
    | Dalias ty -> iter_deps_ty f ty

  let iter_deps_its_defn f its_d =
    Opt.iter (iter_deps_typedef f) its_d.its_def

  let iter_deps f = function
Mário Pereira's avatar
Mário Pereira committed
201 202
    | Dtype its_dl ->
      List.iter (iter_deps_its_defn f) its_dl
Mário Pereira's avatar
Mário Pereira committed
203
    | _ -> assert false (*TODO*)
204

205
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
206 207
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

208
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
209
  let mk_let_var pv e1 e2 =
Mário Pereira's avatar
Mário Pereira committed
210
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
211 212

  let tunit = Ttuple []
213

Mário Pereira's avatar
Mário Pereira committed
214 215
  let ity_int  = I ity_int
  let ity_unit = I ity_unit
Mário Pereira's avatar
Mário Pereira committed
216

217 218 219 220 221
  let enope = Eblock []

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

222 223
  let mk_var id ty ghost = (id, ty, ghost)

224 225
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

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

229 230 231 232 233 234 235 236
  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]

237
end
Mário Pereira's avatar
Mário Pereira committed
238 239 240 241 242

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
243 244 245
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
246

Mário Pereira's avatar
Mário Pereira committed
247 248 249 250 251
  type info = {
    info_current_mo   : Pmodule.pmodule option;
    info_mo_known_map : Pdecl.known_map;
  }

Mário Pereira's avatar
Mário Pereira committed
252 253 254
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
255 256 257 258
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
259
       ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
260 261 262 263 264 265 266 267
    | 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

268 269 270
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

Mário Pereira's avatar
Mário Pereira committed
271
  let filter_ghost_params p def l =
272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291
    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
292 293 294 295 296 297
  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

298 299 300
  let rec pat p =
    match p.pat_node with
    | Pwild ->
301
      ML.Pwild
302
    | Pvar vs ->
303
      ML.Pident vs.vs_name
304
    | Por (p1, p2) ->
305
      ML.Por (pat p1, pat p2)
306
    | Pas (p, vs) ->
307
      ML.Pas (pat p, vs.vs_name)
308
    | Papp (ls, pl) when is_fs_tuple ls ->
309
      ML.Ptuple (List.map pat pl)
310
    | Papp (ls, pl) ->
311 312 313 314 315 316
      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
317
      ML.Papp (ls, List.rev pat_pl)
318

Mário Pereira's avatar
Mário Pereira committed
319 320
  (** programs *)

321 322 323 324 325
  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

326 327 328
  (* individual types *)
  let rec ity t =
    match t.ity_node with
329
    | Ityvar (tvs, _) ->
330
      ML.Tvar tvs
331
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
332
      ML.Ttuple (List.map ity itl)
333
    | Ityapp ({its_ts = ts}, itl, _) ->
334 335 336 337
      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
338

Mário Pereira's avatar
Mário Pereira committed
339
  let pvty pv =
340 341 342 343 344
    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
345

346 347 348 349
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
350 351 352 353 354 355 356 357
  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
358
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
359 360 361 362 363
    (* 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 =
364
      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
365 366 367 368 369 370 371 372 373
      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
374
  let app pvl =
Mário Pereira's avatar
Mário Pereira committed
375
    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
376
    filter_ghost_params pv_not_ghost def pvl
Mário Pereira's avatar
Mário Pereira committed
377

378 379 380 381 382 383
  (* 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
384 385 386 387
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
      if args = [] then [ML.mk_var_unit ()] else args
388

Mário Pereira's avatar
Mário Pereira committed
389
  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
390 391 392 393 394 395
    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
396
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
397
      let for_cty = create_cty [i_pv; to_pv] [] [] Mxs.empty
Mário Pereira's avatar
Mário Pereira committed
398
                               Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
399 400 401
      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
402 403
                            (ML.I ity_bool) eff_empty in
      let next_expr =
Mário Pereira's avatar
Mário Pereira committed
404
        let one_const = Number.int_const_dec "1" in
Mário Pereira's avatar
Mário Pereira committed
405
        let one_expr  =
Mário Pereira's avatar
Mário Pereira committed
406
          ML.mk_expr (ML.Econst one_const) ML.ity_int eff_empty in
Mário Pereira's avatar
Mário Pereira committed
407 408
        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
409
       let rec_call  =
Mário Pereira's avatar
Mário Pereira committed
410
        ML.mk_expr (ML.Eapp (for_rs, [next_expr; to_expr]))
Mário Pereira's avatar
Mário Pereira committed
411
                    ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
412
      let seq_expr =
Mário Pereira's avatar
Mário Pereira committed
413
        ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
414 415
      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
416
    let for_call_expr   =
Mário Pereira's avatar
Mário Pereira committed
417
      let for_call      = ML.Eapp (for_rs, [from_expr; to_expr]) in
Mário Pereira's avatar
Mário Pereira committed
418 419
      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
420
    let args = [
Mário Pereira's avatar
Mário Pereira committed
421 422
      (pv_name  i_pv, ty_int, false);
      (pv_name to_pv, ty_int, false);
Mário Pereira's avatar
Mário Pereira committed
423
    ] in
Mário Pereira's avatar
Mário Pereira committed
424
    let for_rec_def = {
Mário Pereira's avatar
Mário Pereira committed
425 426
      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
427
      ML.rec_res  = ML.tunit;
Mário Pereira's avatar
Mário Pereira committed
428
    } in
Mário Pereira's avatar
Mário Pereira committed
429
    let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
430 431 432 433 434 435 436 437 438 439 440 441 442 443
    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
444 445
  exception ExtractionAny

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

572 573 574 575
  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
576
  let tdef itd =
577
    let s = itd.itd_its in
578 579 580
    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
581
          let args = List.filter pv_not_ghost rsc.cty_args in
582 583
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
584 585 586 587
    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
588 589 590 591
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
592 593
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
594
        ML.mk_its_defn id args is_private None
595
      | None, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
596 597
        let cl = ddata_constructs cl in
        ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
598
      | None, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
599 600 601
        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))
602
      | Some t, _, _ ->
603
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
604
    end
Mário Pereira's avatar
Mário Pereira committed
605

Mário Pereira's avatar
Mário Pereira committed
606
  exception ExtractionVal of rsymbol
Mário Pereira's avatar
Mário Pereira committed
607

Mário Pereira's avatar
Mário Pereira committed
608
  (* program declarations *)
609
  let pdecl info pd =
Mário Pereira's avatar
Mário Pereira committed
610
    match pd.pd_node with
611
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
612
      []
Mário Pereira's avatar
Mário Pereira committed
613 614 615
    | PDlet (LDsym (_rs, {c_node = Cany})) ->
      []
      (* raise (ExtractionVal _rs) *)
616
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
617
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
618 619 620 621
      let res  = ity cty.cty_result in
      let decl = ML.Dlet (ML.Lsym (rs, res, args, expr info e)) in
      let add_known = Mid.singleton rs.rs_name decl in
      [decl, add_known]
622
    | PDlet (LDrec rl) ->
Mário Pereira's avatar
Mário Pereira committed
623
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
624
        let e    = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
625
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
626
        let res  = ity rs1.rs_cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
627
        { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
628 629
          ML.rec_args = args; ML.rec_exp  = expr info e;
          ML.rec_res  = res } in
Mário Pereira's avatar
Mário Pereira committed
630
      let rec_def = filter_ghost_rdef def rl in
Mário Pereira's avatar
Mário Pereira committed
631 632 633 634 635
      let decl    = ML.Dlet (ML.Lrec rec_def) in
      let mk_add_km m {ML.rec_sym = rs} =
        ML.add_known_decl rs.rs_name decl m in
      let add_known = List.fold_left mk_add_km Mid.empty rec_def in
      [decl, add_known]
Mário Pereira's avatar
Mário Pereira committed
636
    | PDlet (LDsym _) | PDpure | PDlet (LDvar (_, _)) ->
637
      []
638
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
639 640 641 642 643
      let itsd = List.map tdef itl in
      let decl = ML.Dtype itsd in
      let mk_add_mk m {ML.its_name = id} = ML.add_known_decl id decl m in
      let add_known = List.fold_left mk_add_mk Mid.empty itsd in
      [decl, add_known]
644
    | PDexn xs ->
Mário Pereira's avatar
Mário Pereira committed
645 646 647 648
      let decl = if ity_equal xs.xs_ity ity_unit then ML.Dexn (xs, None)
        else ML.Dexn (xs, Some (ity xs.xs_ity)) in
      let add_known = Mid.singleton xs.xs_name decl in
      [decl, add_known]
Mário Pereira's avatar
Mário Pereira committed
649

Mário Pereira's avatar
Mário Pereira committed
650 651 652 653 654 655
  let pdecl_m m pd =
    let info = {
      info_current_mo   = Some m;
      info_mo_known_map = m.mod_known; } in
    pdecl info pd

Mário Pereira's avatar
Mário Pereira committed
656
  (* unit module declarations *)
657
  let mdecl info = function
Mário Pereira's avatar
Mário Pereira committed
658
    | Udecl pd ->
659
       pdecl info pd
660
    |  _ -> (* TODO *) []
Mário Pereira's avatar
Mário Pereira committed
661 662

  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
663 664 665 666
  let module_ m =
    let info = {
      info_current_mo   = Some m;
      info_mo_known_map = m.mod_known; } in
Mário Pereira's avatar
Mário Pereira committed
667 668 669 670 671 672 673
    let known_m = ref Mid.empty in
    let mk_decl_and_km (decl, known_m_new) =
      known_m := Mid.set_union !known_m known_m_new;
      decl in
    let comp munit =
      let m = mdecl info munit in List.map mk_decl_and_km m in
    let decl = List.map comp m.mod_units in
Mário Pereira's avatar
Mário Pereira committed
674
    { ML.mod_decl = List.concat decl; ML.mod_known = !known_m }, info
Mário Pereira's avatar
Mário Pereira committed
675

Mário Pereira's avatar
Mário Pereira committed
676 677 678 679 680 681 682 683
  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
684 685
end

686 687 688 689 690 691 692 693
(** Some transformations *)

module Transform = struct

  open ML

  type subst = expr Mpv.t

Mário Pereira's avatar
Mário Pereira committed
694
  let rec expr info subst e =
695
    let mk n = { e with e_node = n } in
Mário Pereira's avatar
Mário Pereira committed
696
    let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
697 698 699
    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
700
    | Elet (Lvar (pv, ({e_node = Econst _ } as e1)), e2)
Mário Pereira's avatar
Mário Pereira committed
701
    | Elet (Lvar (pv, ({e_node = Eblock []} as e1)), e2) ->
Mário Pereira's avatar
Mário Pereira committed
702 703 704
      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
705
      (* only optimize constructors with no argument *)
Mário Pereira's avatar
Mário Pereira committed
706
      (* because of Lvar we know the constructor is completely applied *)
Mário Pereira's avatar
Mário Pereira committed
707
      add_subst pv e1 e2
708
    | Elet (ld, e) ->
Mário Pereira's avatar
Mário Pereira committed
709
      mk (Elet (let_def info subst ld, expr info subst e))
710
    | Eapp (rs, el) ->
Mário Pereira's avatar
Mário Pereira committed
711
      mk (Eapp (rs, List.map (expr info subst) el))
712
    | Efun (vl, e) ->
Mário Pereira's avatar
Mário Pereira committed
713
      mk (Efun (vl, expr info subst e))
714
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
715
      mk (Eif (expr info subst e1, expr info subst e2, expr info subst e3))
Mário Pereira's avatar
Mário Pereira committed
716 717
    (* | Ecast (e, ty) -> *)
    (*   mk (Ecast (expr info subst e, ty)) *)
718
    | Ematch (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
719
      mk (Ematch (expr info subst e, List.map (branch info subst) bl))
720
    | Eblock el ->
Mário Pereira's avatar
Mário Pereira committed
721
      mk (Eblock (List.map (expr info subst) el))
722
    | Ewhile (e1, e2) ->
Mário Pereira's avatar
Mário Pereira committed
723
      mk (Ewhile (expr info subst e1, expr info subst e2))
724
    | Efor (x, pv1, dir, pv2, e) ->
Mário Pereira's avatar
Mário Pereira committed
725
      let e = mk (Efor (x, pv1, dir, pv2, expr info subst e)) in
726 727 728
      (* 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
729
      mk (Eraise (exn, Opt.map (expr info subst) eo))
730
    | Etry (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
731
      mk (Etry (expr info subst e, List.map (xbranch info subst) bl))
732 733 734 735 736 737 738 739 740 741 742
    | 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
743 744
  and branch info subst (pat, e) = pat, expr info subst e
  and xbranch info subst (exn, pat, e) = exn, pat, expr info subst e
745

Mário Pereira's avatar
Mário Pereira committed
746
  and let_def info subst = function
747 748
    | Lvar (pv, e) ->
      assert (not (Mpv.mem pv subst)); (* no capture *)
Mário Pereira's avatar
Mário Pereira committed
749
      Lvar (pv, expr info subst e)
Mário Pereira's avatar
Mário Pereira committed
750 751
    | Lsym (rs, res, args, e) ->
      Lsym (rs, res, args, expr info subst e)
Mário Pereira's avatar
Mário Pereira committed
752
    | Lrec rl -> Lrec (List.map (rdef info subst) rl)
753

Mário Pereira's avatar
Mário Pereira committed
754 755
  and rdef info subst r =
    { r with rec_exp = expr info subst r.rec_exp }
756

Mário Pereira's avatar
Mário Pereira committed
757
  let pdecl info = function
758
    | Dtype _ | Dexn _ as d -> d
Mário Pereira's avatar
Mário Pereira committed
759
    | Dlet def -> Dlet (let_def info Mpv.empty def)
760

Mário Pereira's avatar
Mário Pereira committed
761 762
  let module_ info m =
    { m with mod_decl = List.map (pdecl info) m.mod_decl }
763 764

end
Mário Pereira's avatar
Mário Pereira committed
765 766 767

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