compile.ml 33.6 KB
Newer Older
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Mário Pereira's avatar
Mário Pereira committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
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
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

(*
  - suggest a command line to compile the extracted code
    (for instance in a comment)

  - 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 = ...")
*)

(** Abstract syntax of ML *)

open Ident
open Ity
Mário Pereira's avatar
Mário Pereira committed
30
open Ty
Mário Pereira's avatar
Mário Pereira committed
31
open Term
32

Mário Pereira's avatar
Mário Pereira committed
33
34
35
36
37
38
39
40
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
41
  let fname = match fname, path with
Mário Pereira's avatar
Mário Pereira committed
42
43
44
45
46
    | None, "why3"::_ -> "why3"
    | None, _   -> String.concat "__" path
    | Some f, _ -> clean_name f in
  fname ^ "__" ^ t

47
48
module ML = struct

49
50
  open Expr

51
  type ty =
52
    | Tvar    of tvsymbol
53
54
55
    | Tapp    of ident * ty list
    | Ttuple  of ty list

56
57
58
  type is_ghost = bool

  type var = ident * ty * is_ghost
59

Mário Pereira's avatar
Mário Pereira committed
60
61
  type for_direction = To | DownTo

62
63
64
  type pat =
    | Pwild
    | Pident  of ident
Mário Pereira's avatar
Mário Pereira committed
65
    | Papp    of lsymbol * pat list
66
67
68
69
70
71
72
73
    | Ptuple  of pat list
    | Por     of pat * pat
    | Pas     of pat * ident

  type is_rec = bool

  type binop = Band | Bor | Beq

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

76
  type expr = {
Mário Pereira's avatar
Mário Pereira committed
77
78
79
    e_node   : expr_node;
    e_ity    : ity;
    e_effect : effect;
80
81
82
83
  }

  and expr_node =
    | Econst  of Number.integer_constant
84
    | Evar    of pvsymbol
85
    | Eapp    of rsymbol * expr list
86
    | Efun    of var list * expr
Mário Pereira's avatar
Mário Pereira committed
87
    | Elet    of let_def * expr
88
    | Eif     of expr * expr * expr
Mário Pereira's avatar
Mário Pereira committed
89
    | Eassign of (pvsymbol * rsymbol * pvsymbol) list
90
91
92
    | Ematch  of expr * (pat * expr) list
    | Eblock  of expr list
    | Ewhile  of expr * expr
Mário Pereira's avatar
Mário Pereira committed
93
94
    (* For loop for Why3's type int *)
    | Efor    of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
Mário Pereira's avatar
Mário Pereira committed
95
96
    | Eraise  of xsymbol * expr option
    | Etry    of expr * (xsymbol * pvsymbol list * expr) list
Mário Pereira's avatar
Mário Pereira committed
97
    | Eignore of expr
98
    | Eabsurd
Mário Pereira's avatar
Mário Pereira committed
99
    | Ehole
100

Mário Pereira's avatar
Mário Pereira committed
101
102
  and let_def =
    | Lvar of pvsymbol * expr
Mário Pereira's avatar
Mário Pereira committed
103
    | Lsym of rsymbol * ty * var list * expr
Mário Pereira's avatar
Mário Pereira committed
104
105
106
107
108
109
110
    | 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
111
    rec_res  : ty;
112
    rec_svar : Stv.t;
Mário Pereira's avatar
Mário Pereira committed
113
114
  }

115
116
117
118
119
120
121
  type is_mutable = bool

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

122
123
124
125
126
127
128
  type its_defn = {
    its_name    : ident;
    its_args    : tvsymbol list;
    its_private : bool;
    its_def     : typedef option;
  }

129
  type decl =
Mario Pereira's avatar
Mario Pereira committed
130
    | Dtype   of its_defn list
Mário Pereira's avatar
Mário Pereira committed
131
    | Dlet    of let_def
Mario Pereira's avatar
Mario Pereira committed
132
    | Dexn    of xsymbol * ty option
133
134
135
136
    | Dclone  of ident * decl list
(*
    | Dfunctor of ident * (ident * decl list) list * decl list
*)
Mario Pereira's avatar
Mario Pereira committed
137

Mário Pereira's avatar
Mário Pereira committed
138
139
  type known_map = decl Mid.t

140
141
142
143
144
  type from_module = {
    from_mod: Pmodule.pmodule option;
    from_km : Pdecl.known_map;
  }

Mário Pereira's avatar
Mário Pereira committed
145
  type pmodule = {
146
    mod_from  : from_module;
Mário Pereira's avatar
Mário Pereira committed
147
148
149
150
    mod_decl  : decl list;
    mod_known : known_map;
  }

Mário Pereira's avatar
Mário Pereira committed
151
152
153
  let get_decl_name = function
    | Dtype itdefl -> List.map (fun {its_name = id} -> id) itdefl
    | Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
154
155
156
    | Dlet (Lvar ({pv_vs={vs_name=id}}, _))
    | Dlet (Lsym ({rs_name=id}, _, _, _))
    | Dexn ({xs_name=id}, _) -> [id]
157
    | Dclone _ -> [] (* FIXME? *)
Mário Pereira's avatar
Mário Pereira committed
158
159

  let add_known_decl decl k_map id =
Mário Pereira's avatar
Mário Pereira committed
160
161
    Mid.add id decl k_map

Mário Pereira's avatar
Mário Pereira committed
162
163
  let rec iter_deps_ty f = function
    | Tvar _ -> ()
Mário Pereira's avatar
Mário Pereira committed
164
    | Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
Mário Pereira's avatar
Mário Pereira committed
165
166
167
    | 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
168
169
    | Ddata constrl ->
      List.iter (fun (_, tyl) -> List.iter (iter_deps_ty f) tyl) constrl
Mário Pereira's avatar
Mário Pereira committed
170
    | Drecord pjl -> List.iter (fun (_, _, ty) -> iter_deps_ty f ty) pjl
Mário Pereira's avatar
Mário Pereira committed
171
172
173
174
175
    | 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

Mário Pereira's avatar
Mário Pereira committed
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
  let iter_deps_args f =
    List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg)

  let rec iter_deps_xbranch f (xs, _, e) =
    f xs.xs_name;
    iter_deps_expr f e

  and iter_deps_pat_list f patl =
    List.iter (iter_deps_pat f) patl

  and iter_deps_pat f = function
    | Pwild | Pident _ -> ()
    | Papp (ls, patl) ->
      f ls.ls_name;
      iter_deps_pat_list f patl
    | Ptuple patl -> iter_deps_pat_list f patl
    | Por (p1, p2) ->
      iter_deps_pat f p1;
      iter_deps_pat f p2
    | Pas (p, _) -> iter_deps_pat f p

  and iter_deps_expr f e = match e.e_node with
Mário Pereira's avatar
Mário Pereira committed
198
    | Econst _ | Evar _ | Eabsurd | Ehole -> ()
Mário Pereira's avatar
Mário Pereira committed
199
200
    | Eapp (rs, exprl) ->
      f rs.rs_name; List.iter (iter_deps_expr f) exprl
Mário Pereira's avatar
Mário Pereira committed
201
202
203
    | Efun (args, e) ->
      List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
      iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
    | Elet (Lvar (_, e1), e2) ->
      iter_deps_expr f e1;
      iter_deps_expr f e2
    | Elet (Lsym (_, ty_result, args, e1), e2) ->
      iter_deps_ty f ty_result;
      List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
      iter_deps_expr f e1;
      iter_deps_expr f e2
    | Elet ((Lrec rdef), e) ->
      List.iter
        (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
           f rs.rs_name; iter_deps_args f args;
           iter_deps_expr f e; iter_deps_ty f res) rdef;
      iter_deps_expr f e
    | Ematch (e, branchl) ->
      iter_deps_expr f e;
      List.iter (fun (p, e) -> iter_deps_pat f p; iter_deps_expr f e) branchl
    | Eif (e1, e2, e3) ->
      iter_deps_expr f e1;
      iter_deps_expr f e2;
      iter_deps_expr f e3
    | Eblock exprl ->
      List.iter (iter_deps_expr f) exprl
    | Ewhile (e1, e2) ->
      iter_deps_expr f e1;
      iter_deps_expr f e2
    | Efor (_, _, _, _, e) ->
      iter_deps_expr f e
    | Eraise (xs, None) ->
      f xs.xs_name
    | Eraise (xs, Some e) ->
      f xs.xs_name;
      iter_deps_expr f e
    | Etry (e, xbranchl) ->
      iter_deps_expr f e;
      List.iter (iter_deps_xbranch f) xbranchl
    | Eassign assingl ->
      List.iter (fun (_, rs, _) -> f rs.rs_name) assingl
Mário Pereira's avatar
Mário Pereira committed
242
    | Eignore e -> iter_deps_expr f e
Mário Pereira's avatar
Mário Pereira committed
243

244
  let rec iter_deps f = function
Mário Pereira's avatar
Mário Pereira committed
245
246
    | Dtype its_dl ->
      List.iter (iter_deps_its_defn f) its_dl
Mário Pereira's avatar
Mário Pereira committed
247
248
249
250
251
252
253
254
255
    | Dlet (Lsym (_rs, ty_result, args, e)) ->
      iter_deps_ty f ty_result;
      iter_deps_args f args;
      iter_deps_expr f e
    | Dlet (Lrec rdef) ->
      List.iter
        (fun {rec_sym = rs; rec_args = args; rec_exp = e; rec_res = res} ->
           f rs.rs_name; iter_deps_args f args;
           iter_deps_expr f e; iter_deps_ty f res) rdef
Mário Pereira's avatar
Mário Pereira committed
256
257
258
    | Dlet (Lvar (_, e)) -> iter_deps_expr f e
    | Dexn (_, None) -> ()
    | Dexn (_, Some ty) -> iter_deps_ty f ty
259
    | Dclone (_, dl) -> List.iter (iter_deps f) dl
260

261
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
262
263
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

264
  (* smart constructors *)
Mário Pereira's avatar
Mário Pereira committed
265
  let mk_let_var pv e1 e2 =
Mário Pereira's avatar
Mário Pereira committed
266
    Elet (Lvar (pv, e1), e2)
Mário Pereira's avatar
Mário Pereira committed
267
268

  let tunit = Ttuple []
269

Mário Pereira's avatar
Mário Pereira committed
270
271
272
273
274
275
  let ity_int  = I Ity.ity_int
  let ity_unit = I Ity.ity_unit

  let is_unit = function
    | I i -> ity_equal i Ity.ity_unit
    | _ -> false
Mário Pereira's avatar
Mário Pereira committed
276

277
278
279
280
281
  let enope = Eblock []

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

Mário Pereira's avatar
Mário Pereira committed
282
283
284
  let mk_hole =
    mk_expr Ehole (I Ity.ity_unit) Ity.eff_empty

285
286
  let mk_var id ty ghost = (id, ty, ghost)

287
288
  let mk_var_unit () = id_register (id_fresh "_"), tunit, true

289
  let mk_its_defn id args private_ def =
Mário Pereira's avatar
Mário Pereira committed
290
291
    { its_name    = id      ; its_args = args;
      its_private = private_; its_def  = def; }
292

Mário Pereira's avatar
Mário Pereira committed
293
294
295
296
  let mk_ignore e =
    if is_unit e.e_ity then e
    else { e_node = Eignore e; e_effect = e.e_effect; e_ity = ity_unit }

297
298
  let eseq e1 e2 =
    match e1.e_node, e2.e_node with
Mário Pereira's avatar
Mário Pereira committed
299
    | (Eblock [] | Ehole), e | e, (Eblock [] | Ehole) -> e
300
301
302
303
304
    | Eblock e1, Eblock e2 -> Eblock (e1 @ e2)
    | _, Eblock e2 -> Eblock (e1 :: e2)
    | Eblock e1, _ -> Eblock (e1 @ [e2])
    | _ -> Eblock [e1; e2]

305
end
Mário Pereira's avatar
Mário Pereira committed
306
307
308
309
310

(** Translation from Mlw to ML *)

module Translate = struct

Mário Pereira's avatar
Mário Pereira committed
311
312
313
  open Expr
  open Pmodule
  open Pdecl
Mário Pereira's avatar
Mário Pereira committed
314

Mário Pereira's avatar
Mário Pereira committed
315
316
317
  (* useful predicates and transformations *)
  let pv_not_ghost e = not e.pv_ghost

Mário Pereira's avatar
Mário Pereira committed
318
319
320
321
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
322
       ML.Tvar tvs
Mário Pereira's avatar
Mário Pereira committed
323
324
325
326
327
328
329
330
    | 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

331
332
333
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

Mário Pereira's avatar
Mário Pereira committed
334
335
336
337
338
  let rec filter_ghost_params p def = function
    | [] -> []
    | pv :: l ->
      if p pv then def pv :: (filter_ghost_params p def l)
      else filter_ghost_params p def l
339
340
341
342
343
344
345
346
347
348
349
350

  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)

351
  let rec filter_out_ghost_rdef = function
Mário Pereira's avatar
Mário Pereira committed
352
353
    | [] -> []
    | { rec_sym = rs; rec_rsym = rrs } :: l
354
355
      when rs_ghost rs || rs_ghost rrs -> filter_out_ghost_rdef l
    | rdef :: l -> rdef :: filter_out_ghost_rdef l
Mário Pereira's avatar
Mário Pereira committed
356

357
358
359
  let rec pat p =
    match p.pat_node with
    | Pwild ->
360
      ML.Pwild
361
362
    | Pvar vs when (restore_pv vs).pv_ghost ->
      ML.Pwild
363
    | Pvar vs ->
364
      ML.Pident vs.vs_name
365
    | Por (p1, p2) ->
366
      ML.Por (pat p1, pat p2)
367
368
    | Pas (p, vs) when (restore_pv vs).pv_ghost ->
      pat p
369
    | Pas (p, vs) ->
370
      ML.Pas (pat p, vs.vs_name)
371
    | Papp (ls, pl) when is_fs_tuple ls ->
372
      ML.Ptuple (List.map pat pl)
373
    | Papp (ls, pl) ->
374
375
      let rs = restore_rs ls in
      let args = rs.rs_cty.cty_args in
376
377
      let mk acc pv pp = if not pv.pv_ghost then pat pp :: acc else acc in
      let pat_pl = List.fold_left2 mk [] args pl in
Mário Pereira's avatar
Mário Pereira committed
378
      ML.Papp (ls, List.rev pat_pl)
379

Mário Pereira's avatar
Mário Pereira committed
380
381
  (** programs *)

382
383
  let pv_name pv = pv.pv_vs.vs_name

384
385
386
  (* individual types *)
  let rec ity t =
    match t.ity_node with
387
    | Ityvar (tvs, _) ->
388
      ML.Tvar tvs
389
    | Ityapp ({its_ts = ts}, itl, _) when is_ts_tuple ts ->
390
      ML.Ttuple (List.map ity itl)
391
    | Ityapp ({its_ts = ts}, itl, _) ->
392
393
394
395
      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
396

Mário Pereira's avatar
Mário Pereira committed
397
  let pvty pv =
Mário Pereira's avatar
Mário Pereira committed
398
399
    if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true
    else let (vs, vs_ty) = vsty pv.pv_vs in
400
      ML.mk_var vs vs_ty false
Mário Pereira's avatar
Mário Pereira committed
401

402
403
404
405
  let for_direction = function
    | To -> ML.To
    | DownTo -> ML.DownTo

Mário Pereira's avatar
Mário Pereira committed
406
  let isconstructor info rs =
407
    match Mid.find_opt rs.rs_name info.ML.from_km with
Mário Pereira's avatar
Mário Pereira committed
408
409
410
411
412
413
    | 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
414
415
416
417
  let is_singleton_imutable itd =
    let not_g e = not (rs_ghost e) in
    let pjl = itd.itd_fields in
    let mfields = itd.itd_its.its_mfields in
418
    let pv_equal_field rs = pv_equal (fd_of_rs rs) in
Mário Pereira's avatar
Mário Pereira committed
419
420
421
422
    let get_mutable rs = List.exists (pv_equal_field rs) mfields in
    match filter_ghost_params not_g get_mutable pjl with
    | [is_mutable] -> not is_mutable
    | _ -> false
Mário Pereira's avatar
Mário Pereira committed
423

424
  let get_record_itd info rs =
425
    match Mid.find_opt rs.rs_name info.ML.from_km with
Mário Pereira's avatar
Mário Pereira committed
426
427
    | Some {pd_node = PDtype itdl} ->
      let f pjl_constr = List.exists (rs_equal rs) pjl_constr in
428
      let itd = match rs.rs_field with
Mário Pereira's avatar
Mário Pereira committed
429
        | Some _ -> List.find (fun itd -> f itd.itd_fields) itdl
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
        | None -> List.find (fun itd -> f itd.itd_constructors) itdl in
      if itd.itd_fields = [] then None else Some itd
    | _ -> None

  let is_optimizable_record_itd itd =
    not itd.itd_its.its_private && is_singleton_imutable itd

  let is_optimizable_record_rs info rs =
    Opt.fold (fun _ -> is_optimizable_record_itd) false (get_record_itd info rs)

  let is_empty_record_itd itd =
    let is_ghost rs = rs_ghost rs in
    List.for_all is_ghost itd.itd_fields

  let is_empty_record info rs =
    Opt.fold (fun _ -> is_empty_record_itd) false (get_record_itd info rs)
Mário Pereira's avatar
Mário Pereira committed
446

Mário Pereira's avatar
Mário Pereira committed
447
  let mk_eta_expansion rsc pvl cty_app =
Mário Pereira's avatar
Mário Pereira committed
448
449
450
451
452
    (* 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 =
453
      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
454
455
456
457
458
459
460
461
462
      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

463
464
465
466
467
468
  (* 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
469
470
471
472
  let params = function
    | []   -> []
    | args -> let args = filter_params args in
      if args = [] then [ML.mk_var_unit ()] else args
473

Mário Pereira's avatar
Mário Pereira committed
474
475
  let filter_params_cty p def pvl cty_args =
    let rec loop = function
Mário Pereira's avatar
Mário Pereira committed
476
      | [], _ -> []
Mário Pereira's avatar
Mário Pereira committed
477
478
479
480
481
482
483
484
485
486
      | pv :: l1, arg :: l2 ->
        if p pv && p arg then def pv :: loop (l1, l2)
        else loop (l1, l2)
      | _ -> assert false
    in loop (pvl, cty_args)

  let app pvl cty_args =
    let def pv = ML.mk_expr (ML.Evar pv) (ML.I pv.pv_ity) eff_empty in
    filter_params_cty pv_not_ghost def pvl cty_args

Mário Pereira's avatar
Mário Pereira committed
487
  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
488
489
490
491
492
493
    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
494
      let for_id  = id_fresh "for_loop_to" in
Mário Pereira's avatar
Mário Pereira committed
495
      let for_cty = create_cty [i_pv] [] [] Mxs.empty
Mário Pereira's avatar
Mário Pereira committed
496
                               Mpv.empty eff ity_unit in
Mário Pereira's avatar
Mário Pereira committed
497
498
499
      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
500
501
                            (ML.I ity_bool) eff_empty in
      let next_expr =
Mário Pereira's avatar
Mário Pereira committed
502
        let one_const = Number.int_const_dec "1" in
Mário Pereira's avatar
Mário Pereira committed
503
        let one_expr  =
Mário Pereira's avatar
Mário Pereira committed
504
          ML.mk_expr (ML.Econst one_const) ML.ity_int eff_empty in
Mário Pereira's avatar
Mário Pereira committed
505
506
        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
507
       let rec_call  =
Mário Pereira's avatar
Mário Pereira committed
508
        ML.mk_expr (ML.Eapp (for_rs, [next_expr]))
Mário Pereira's avatar
Mário Pereira committed
509
                    ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
510
      let seq_expr =
Mário Pereira's avatar
Mário Pereira committed
511
        ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff in
Mário Pereira's avatar
Mário Pereira committed
512
513
      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
514
    let for_call_expr   =
Mário Pereira's avatar
Mário Pereira committed
515
      let for_call      = ML.Eapp (for_rs, [from_expr]) in
Mário Pereira's avatar
Mário Pereira committed
516
517
      ML.mk_expr for_call ML.ity_unit eff in
    let pv_name pv = pv.pv_vs.vs_name in
518
    let args = [ pv_name i_pv, ty_int, false ] in
Mário Pereira's avatar
Mário Pereira committed
519
    let for_rec_def = {
520
521
      ML.rec_sym  = for_rs;   ML.rec_args = args;
      ML.rec_rsym = for_rs;   ML.rec_exp  = for_expr;
522
      ML.rec_res  = ML.tunit; ML.rec_svar = Stv.empty;
Mário Pereira's avatar
Mário Pereira committed
523
    } in
Mário Pereira's avatar
Mário Pereira committed
524
    let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in
Mário Pereira's avatar
Mário Pereira committed
525
526
527
528
    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 =
529
      let ns = (Opt.get info.ML.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
530
531
532
533
534
      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 =
535
      let ns = (Opt.get info.ML.from_mod).mod_export in
Mário Pereira's avatar
Mário Pereira committed
536
537
538
      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
539
540
  exception ExtractionAny

541
542
  (* build the set of type variables from functions arguments *)
  let rec add_tvar acc = function
543
    | ML.Tvar tv -> Stv.add tv acc
544
545
546
    | ML.Tapp (_, tyl) | ML.Ttuple tyl ->
      List.fold_left add_tvar acc tyl

Mário Pereira's avatar
Mário Pereira committed
547
  (* expressions *)
548
  let rec expr info ({e_effect = eff} as e) =
Mário Pereira's avatar
Mário Pereira committed
549
    assert (not eff.eff_ghost);
Mário Pereira's avatar
Mário Pereira committed
550
    match e.e_node with
551
    | Econst c ->
Mário Pereira's avatar
Mário Pereira committed
552
553
      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
554
555
    | Evar pv ->
      ML.mk_expr (ML.Evar pv) (ML.I e.e_ity) eff
556
    | Elet (LDvar (_, e1), e2) when e_ghost e1 ->
Mário Pereira's avatar
Mário Pereira committed
557
      expr info e2
558
559
    | Elet (LDvar (_, e1), e2) when e_ghost e2 ->
      ML.mk_expr (ML.eseq (expr info e1) ML.mk_unit) ML.ity_unit eff
Mário Pereira's avatar
Mário Pereira committed
560
561
562
563
564
    | Elet (LDvar (pv, e1), e2)
      when pv.pv_ghost || not (Mpv.mem pv e2.e_effect.eff_reads) ->
      if eff_pure e1.e_effect then expr info e2
      else let e1 = ML.mk_ignore (expr info e1) in
        ML.mk_expr (ML.eseq e1 (expr info e2)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
565
566
    | Elet (LDvar (pv, e1), e2) ->
      let ml_let = ML.mk_let_var pv (expr info e1) (expr info e2) in
567
      ML.mk_expr ml_let (ML.I e.e_ity) eff
568
569
    | Elet (LDsym (rs, _), ein) when rs_ghost rs ->
      expr info ein
570
    | Elet (LDsym (rs, {c_node = Cfun ef; c_cty = cty}), ein) ->
571
      let args = params cty.cty_args in
572
573
      let ef = expr info ef in
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
574
575
      let res = ity cty.cty_result in
      let ml_letrec = ML.Elet (ML.Lsym (rs, res, args, ef), ein) in
576
      ML.mk_expr ml_letrec (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
577
578
    | 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
579
580
      (* partial application of constructor *)
      let eta_app = mk_eta_expansion rs_app pvl cty in
Mário Pereira's avatar
Mário Pereira committed
581
      let ein = expr info ein in
Mário Pereira's avatar
Mário Pereira committed
582
583
584
      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
585
      let ml_letrec = ML.Elet (ML.Lsym (rsf, res, [], eta_app), ein) in
Mário Pereira's avatar
Mário Pereira committed
586
587
      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) ->
588
      (* partial application *)
Mário Pereira's avatar
Mário Pereira committed
589
      let pvl = app pvl rs_app.rs_cty.cty_args in
590
      let eapp =
Mário Pereira's avatar
Mário Pereira committed
591
        ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
Mário Pereira's avatar
Mário Pereira committed
592
593
      let ein  = expr info ein in
      let res  = ity cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
594
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
595
      let ml_letrec = ML.Elet (ML.Lsym (rsf, res, args, eapp), ein) in
Mário Pereira's avatar
Mário Pereira committed
596
597
      ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
    | Elet (LDrec rdefl, ein) ->
598
599
600
601
      let rdefl = filter_out_ghost_rdef rdefl in
      let def = function
        | {rec_sym = rs1; rec_rsym = rs2;
           rec_fun = {c_node = Cfun ef; c_cty = cty}} ->
602
603
604
605
          let res  = ity rs1.rs_cty.cty_result in
          let args = params cty.cty_args in
          let svar =
            let args' = List.map (fun (_, ty, _) -> ty) args in
606
            let svar  = List.fold_left add_tvar Stv.empty args' in
607
608
609
610
611
            add_tvar svar res in
          let ef = expr info ef in
          { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
            ML.rec_args = args; ML.rec_exp  = ef ;
            ML.rec_res  = res;  ML.rec_svar = svar; }
612
613
        | _ -> assert false in
      let rdefl = List.map def rdefl in
614
615
616
617
      if rdefl <> [] then
        let ml_letrec = ML.Elet (ML.Lrec rdefl, expr info ein) in
        ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
      else expr info ein
618
619
    | Eexec ({c_node = Capp (rs, [])}, _) when is_rs_tuple rs ->
      ML.mk_unit
620
621
    | Eexec ({c_node = Capp (rs, _)}, _) when is_empty_record info rs ->
      ML.mk_unit
622
623
    | Eexec ({c_node = Capp (rs, _)}, _) when rs_ghost rs ->
      ML.mk_unit
Mário Pereira's avatar
Mário Pereira committed
624
    | Eexec ({c_node = Capp (rs, pvl); c_cty = cty}, _)
Mário Pereira's avatar
Mário Pereira committed
625
626
      when isconstructor info rs && cty.cty_args <> [] ->
      (* partial application of constructors *)
Mário Pereira's avatar
Mário Pereira committed
627
      mk_eta_expansion rs pvl cty
Mário Pereira's avatar
Mário Pereira committed
628
    | Eexec ({c_node = Capp (rs, pvl); _}, _) ->
Mário Pereira's avatar
Mário Pereira committed
629
      let pvl = app pvl rs.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
630
      begin match pvl with
631
      | [pv_expr] when is_optimizable_record_rs info rs -> pv_expr
Mário Pereira's avatar
Mário Pereira committed
632
633
634
635
      | _ -> ML.mk_expr (ML.Eapp (rs, pvl)) (ML.I e.e_ity) eff end
    | Eexec ({c_node = Cfun e; c_cty = {cty_args = []}}, _) ->
      (* abstract block *)
      expr info e
636
    | Eexec ({c_node = Cfun e; c_cty = cty}, _) ->
637
      let args = params cty.cty_args in
638
      ML.mk_expr (ML.Efun (args, expr info e)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
639
    | Eexec ({c_node = Cany}, _) -> (* raise ExtractionAny *)
Mário Pereira's avatar
Mário Pereira committed
640
      ML.mk_hole
641
    | Eabsurd ->
642
643
644
      ML.mk_expr ML.Eabsurd (ML.I e.e_ity) eff
    | Ecase (e1, _) when e_ghost e1 ->
      ML.mk_unit
645
    | Ecase (e1, pl) ->
Mário Pereira's avatar
Mário Pereira committed
646
647
648
      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
Mário Pereira's avatar
Mário Pereira committed
649
    | Eassert _ -> ML.mk_unit
Mário Pereira's avatar
Mário Pereira committed
650
651
652
653
654
655
656
657
    | Eif (e1, e2, e3) when e_ghost e3 ->
      let e1 = expr info e1 in
      let e2 = expr info e2 in
      ML.mk_expr (ML.Eif (e1, e2, ML.mk_unit)) (ML.I e.e_ity) eff
    | Eif (e1, e2, e3) when e_ghost e2 ->
      let e1 = expr info e1 in
      let e3 = expr info e3 in
      ML.mk_expr (ML.Eif (e1, ML.mk_unit, e3)) (ML.I e.e_ity) eff
658
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
659
660
661
662
      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
663
664
665
666
    | 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
667
    | Efor (pv1, (pv2, To, pv3), _, efor) ->
Mário Pereira's avatar
Mário Pereira committed
668
      let efor = expr info efor in
Mário Pereira's avatar
Mário Pereira committed
669
670
671
672
      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
673
    | Eghost _ -> assert false
674
675
    | Eassign al ->
      ML.mk_expr (ML.Eassign al) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
676
    | Epure _ -> (* assert false (\*TODO*\) *) ML.mk_hole
Mário Pereira's avatar
Mário Pereira committed
677
678
679
680
681
682
    | 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
683
684
685
    | Eraise (xs, ex) ->
      let ex =
        match expr info ex with
Mário Pereira's avatar
Mário Pereira committed
686
        | {ML.e_node = ML.Eblock []} -> None
Mário Pereira's avatar
Mário Pereira committed
687
688
        | e -> Some e
      in
Mário Pereira's avatar
Mário Pereira committed
689
      ML.mk_expr (ML.Eraise (xs, ex)) (ML.I e.e_ity) eff
Mário Pereira's avatar
Mário Pereira committed
690
691
692
693
    | Elet (LDsym (_, {c_node=(Cany|Cpur (_, _)); _ }), _)
    (*   assert false (\*TODO*\) *)
    | Eexec ({c_node=Cpur (_, _); _ }, _) -> ML.mk_hole
    (*   assert false (\*TODO*\) *)
694

Mário Pereira's avatar
Mário Pereira committed
695
696
  and ebranch info ({pp_pat = p}, e) =
    (pat p, expr info e)
697

698
699
700
701
  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
702
  let tdef itd =
703
    let s = itd.itd_its in
704
705
706
    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
707
          let args = List.filter pv_not_ghost rsc.cty_args in
708
709
          List.map (fun {pv_vs = vs} -> type_ vs.vs_ty) args)
    in
Mário Pereira's avatar
Mário Pereira committed
710
    let drecord_fields ({rs_cty = rsc} as rs) =
711
      (List.exists (pv_equal (fd_of_rs rs)) s.its_mfields),
Mário Pereira's avatar
Mário Pereira committed
712
713
      rs.rs_name,
      ity rsc.cty_result
714
715
716
717
    in
    let id = s.its_ts.ts_name in
    let is_private = s.its_private in
    let args = s.its_ts.ts_args in
718
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
719
      | NoDef, [], [] ->
Mário Pereira's avatar
Mário Pereira committed
720
        ML.mk_its_defn id args is_private None
721
      | NoDef, cl, [] ->
Mário Pereira's avatar
Mário Pereira committed
722
723
        let cl = ddata_constructs cl in
        ML.mk_its_defn id args is_private (Some (ML.Ddata cl))
724
      | NoDef, _, pjl ->
Mário Pereira's avatar
Mário Pereira committed
725
726
        let p e = not (rs_ghost e) in
        let pjl = filter_ghost_params p drecord_fields pjl in
Mário Pereira's avatar
Mário Pereira committed
727
        begin match pjl with
728
729
          | [] -> ML.mk_its_defn id args is_private (Some (ML.Dalias ML.tunit))
          | [_, _, ty_pj] when is_optimizable_record_itd itd ->
Mário Pereira's avatar
Mário Pereira committed
730
731
732
            ML.mk_its_defn id args is_private (Some (ML.Dalias ty_pj))
          | pjl -> ML.mk_its_defn id args is_private (Some (ML.Drecord pjl))
        end
733
      | Alias t, _, _ ->
734
         ML.mk_its_defn id args is_private (Some (ML.Dalias (ity t)))
735
736
      | Range _, _, _ -> assert false (* TODO *)
      | Float _, _, _ -> assert false (* TODO *)
737
    end
Mário Pereira's avatar
Mário Pereira committed
738

Mário Pereira's avatar
Mário Pereira committed
739
  exception ExtractionVal of rsymbol
Mário Pereira's avatar
Mário Pereira committed
740

Mário Pereira's avatar
Mário Pereira committed
741
742
743
744
  let is_val = function
    | Eexec ({c_node = Cany}, _) -> true
    | _ -> false

745
746
  (* pids: identifiers from cloned modules without definitions *)
  let pdecl _pids info pd =
Mário Pereira's avatar
Mário Pereira committed
747
    match pd.pd_node with
748
    | PDlet (LDsym (rs, _)) when rs_ghost rs ->
Mário Pereira's avatar
Mário Pereira committed
749
      []
Mário Pereira's avatar
Mário Pereira committed
750
751
752
    | PDlet (LDsym (_rs, {c_node = Cany})) ->
      []
      (* raise (ExtractionVal _rs) *)
Mário Pereira's avatar
Mário Pereira committed
753
754
    | PDlet (LDsym (_, {c_node = Cfun e})) when is_val e.e_node ->
      []
755
    | PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
756
      let args = params cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
757
      let res  = ity cty.cty_result in
Mário Pereira's avatar
Mário Pereira committed
758
      [ML.Dlet (ML.Lsym (rs, res, args, expr info e))]
759
    | PDlet (LDrec rl) ->
760
      let rl = filter_out_ghost_rdef rl in
Mário Pereira's avatar
Mário Pereira committed
761
      let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
Mário Pereira's avatar
Mário Pereira committed
762
        let e = match e.c_node with Cfun e -> e | _ -> assert false in
Mário Pereira's avatar
Mário Pereira committed
763
        let args = params rs1.rs_cty.cty_args in
Mário Pereira's avatar
Mário Pereira committed
764
        let res  = ity rs1.rs_cty.cty_result in
765
766
        let svar =
          let args' = List.map (fun (_, ty, _) -> ty) args in
767
          let svar  = List.fold_left add_tvar Stv.empty args' in
768
          add_tvar svar res in
Mário Pereira's avatar
Mário Pereira committed
769
        { ML.rec_sym  = rs1;  ML.rec_rsym = rs2;
Mário Pereira's avatar
Mário Pereira committed
770
          ML.rec_args = args; ML.rec_exp  = expr info e;
771
          ML.rec_res  = res;  ML.rec_svar = svar; } in
772
      if rl = [] then [] else [ML.Dlet (ML.Lrec (List.map def rl))]
Mário Pereira's avatar
Mário Pereira committed
773
    | PDlet (LDsym _) | PDpure | PDlet (LDvar _) ->
774
      []
775
    | PDtype itl ->
Mário Pereira's avatar
Mário Pereira committed
776
      let itsd = List.map tdef itl in
Mário Pereira's avatar
Mário Pereira committed
777
      [ML.Dtype itsd]
778
    | PDexn xs ->
Mário Pereira's avatar
Mário Pereira committed
779
780
      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
781

Mário Pereira's avatar
Mário Pereira committed
782
  let pdecl_m m pd =
783
784
    let info = { ML.from_mod = Some m; ML.from_km  = m.mod_known; } in
    pdecl Sid.empty info pd
Mário Pereira's avatar
Mário Pereira committed
785

Mário Pereira's avatar
Mário Pereira committed
786
  (* unit module declarations *)
787
788
789
  let rec mdecl pids info = function
    | Udecl pd -> pdecl pids info pd
    | Uscope (_, _, l) -> List.concat (List.map (mdecl pids info) l)
790
    | Uuse _ | Uclone _ | Umeta _ -> []
Mário Pereira's avatar
Mário Pereira committed
791

792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
  let abstract_or_alias_type itd =
    itd.itd_fields = [] && itd.itd_constructors = []

  let empty_pdecl pd  = match pd.pd_node with
    | PDlet (LDsym (_, {c_node = Cfun _})) | PDlet (LDrec _) -> false
    | PDexn _ -> false (* FIXME? *)
    | PDtype itl -> List.for_all abstract_or_alias_type itl
    | _ -> true
  let rec empty_munit = function
    | Udecl pd -> empty_pdecl pd
    | Uclone mi -> List.for_all empty_munit mi.mi_mod.mod_units
    | Uscope (_, _, l) -> List.for_all empty_munit l
    | Uuse _ | Umeta _ -> true

  let is_empty_clone mi =
    Mts.is_empty mi.mi_ty &&
    Mts.is_empty mi.mi_ts &&
    Mls.is_empty mi.mi_ls &&
    Decl.Mpr.is_empty mi.mi_pr &&
    Decl.Mpr.is_empty mi.mi_pk &&
    Mvs.is_empty mi.mi_pv &&
    Mrs.is_empty mi.mi_rs &&
    Mxs.is_empty mi.mi_xs &&
    List.for_all empty_munit mi.mi_mod.mod_units

  let find_params dl =
    let add params = function
      | Uclone mi when is_empty_clone mi -> mi :: params
      | _ -> params in
    List.fold_left add [] dl

  let make_param from mi =
    let id = mi.mi_mod.mod_theory.Theory.th_name in
    Format.printf "param %s@." id.id_string;
    let dl =
      List.concat (List.map (mdecl Sid.empty from) mi.mi_mod.mod_units) in
    ML.Dclone (id, dl)

  let ids_of_params pids mi =
    Mid.fold (fun id _ pids -> Sid.add id pids) mi.mi_mod.mod_known pids

Mário Pereira's avatar
Mário Pereira committed
833
  (* modules *)
Mário Pereira's avatar
Mário Pereira committed
834
  let module_ m =
835
836
837
838
839
    let from = { ML.from_mod = Some m; ML.from_km = m.mod_known; } in
    let params = find_params m.mod_units in
    let pids = List.fold_left ids_of_params Sid.empty params in
    let mod_decl = List.concat (List.map (mdecl pids from) m.mod_units) in
    let mod_decl = List.map (make_param from) params @ mod_decl in
Mário Pereira's avatar
Mário Pereira committed
840
841
842
843
    let add known_map decl =
      let idl = ML.get_decl_name decl in
      List.fold_left (ML.add_known_decl decl) known_map idl in
    let mod_known = List.fold_left add Mid.empty mod_decl in
844
    { ML.mod_from = from; ML.mod_decl = mod_decl; ML.mod_known = mod_known }
Mário Pereira's avatar
Mário Pereira committed
845

Mário Pereira's avatar
Mário Pereira committed
846
847
848
849
850
851
852
853
  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
854
855
end

856
857
858
859
860
861
(** Some transformations *)

module Transform = struct

  open ML

Mário Pereira's avatar
Mário Pereira committed
862
  let no_reads_writes_conflict spv spv_mreg =
863
    let is_not_write {pv_ity = ity} = match ity.ity_node with
Mário Pereira's avatar
Mário Pereira committed
864
865
        | Ityreg rho -> not (Mreg.mem rho spv_mreg)
        | _ -> true in
866
    Spv.for_all is_not_write spv
Mário Pereira's avatar
Mário Pereira committed
867

868
869
  type subst = expr Mpv.t

Mário Pereira's avatar
Mário Pereira committed
870
871
872
873
874
  let mk_list_eb ebl f =
    let mk_acc e (e_acc, s_acc) =
      let e, s = f e in e::e_acc, Spv.union s s_acc in
    List.fold_right mk_acc ebl ([], Spv.empty)

Mário Pereira's avatar
Mário Pereira committed
875
  let rec expr info subst e =
Mário Pereira's avatar
Mário Pereira committed
876
    let mk e_node = { e with e_node = e_node } in
Mário Pereira's avatar
Mário Pereira committed
877
    let add_subst pv e1 e2 = expr info (Mpv.add pv e1 subst) e2 in
878
    match e.e_node with
Mário Pereira's avatar
Mário Pereira committed
879
880
    | Evar pv -> begin try Mpv.find pv subst, Spv.singleton pv
        with Not_found -> e, Spv.empty end
Mário Pereira's avatar
Mário Pereira committed
881
    | Elet (Lvar (pv, ({e_effect = eff1} as e1)), ({e_effect = eff2} as e2))
Mário Pereira's avatar
Mário Pereira committed
882
      when Slab.mem Expr.proxy_label pv.pv_vs.vs_name.id_label &&
Mário Pereira's avatar
Mário Pereira committed
883
           eff_pure eff1 &&
Mário Pereira's avatar
Mário Pereira committed
884
           no_reads_writes_conflict eff1.eff_reads eff2.eff_writes ->
Mário Pereira's avatar
Mário Pereira committed
885
886
887
888
889
890
      let e1, s1 = expr info subst e1 in
      let e2, s2 = add_subst pv e1 e2 in
      let s_union = Spv.union s1 s2 in
      if Spv.mem pv s2 then e2, s_union (* [pv] was substituted in [e2] *)
      else (* [pv] was not substituted in [e2], e.g [e2] is an [Efun] *)
        mk (Elet (Lvar (pv, e1), e2)), s_union
891
    | Elet (ld, e) ->
Mário Pereira's avatar
Mário Pereira committed
892
893
894
      let e, spv = expr info subst e in
      let e_let, spv_let = let_def info subst ld in
      mk (Elet (e_let, e)), Spv.union spv spv_let
895
    | Eapp (rs, el) ->
Mário Pereira's avatar
Mário Pereira committed
896
897
      let e_app, spv = mk_list_eb el (expr info subst) in
      mk (Eapp (rs, e_app)), spv
898
    | Efun (vl, e) ->
Mário Pereira's avatar
Mário Pereira committed
899
900
901
902
903
904
905
906
      (* For now, we accept to inline constants and constructors
         with zero arguments inside a [Efun]. *)
      let p _k e = match e.e_node with
        | Econst _ -> true
        | Eapp (rs, []) when Translate.isconstructor info rs -> true
        | _ -> false in
      let restrict_subst = Mpv.filter p subst in
      (* We begin the inlining of proxy variables in an [Efun] with a
907
         restricted substitution. This keeps some proxy lets, preventing
Mário Pereira's avatar
Mário Pereira committed
908
909
         undiserable captures inside the [Efun] expression. *)
      let e, spv = expr info restrict_subst e in
Mário Pereira's avatar
Mário Pereira committed
910
      mk (Efun (vl, e)), spv
911
    | Eif (e1, e2, e3) ->
Mário Pereira's avatar
Mário Pereira committed
912
913
914
915
      let e1, s1 = expr info subst e1 in
      let e2, s2 = expr info subst e2 in
      let e3, s3 = expr info subst e3 in
      mk (Eif (e1, e2, e3)), Spv.union (Spv.union s1 s2) s3
916
    | Ematch (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
917
918
919
      let e, spv = expr info subst e in
      let e_bl, spv_bl = mk_list_eb bl (branch info subst) in
      mk (Ematch (e, e_bl)), Spv.union spv spv_bl
920
    | Eblock el ->
Mário Pereira's avatar
Mário Pereira committed
921
922
      let e_app, spv = mk_list_eb el (expr info subst) in
      mk (Eblock e_app), spv
923
    | Ewhile (e1, e2) ->
Mário Pereira's avatar
Mário Pereira committed
924
925
926
      let e1, s1 = expr info subst e1 in
      let e2, s2 = expr info subst e2 in
      mk (Ewhile (e1, e2)), Spv.union s1 s2
927
    | Efor (x, pv1, dir, pv2, e) ->
Mário Pereira's avatar
Mário Pereira committed
928
929
      let e, spv = expr info subst e in
      let e = mk (Efor (x, pv1, dir, pv2, e)) in
930
      (* be careful when pv1 and pv2 are in subst *)
Mário Pereira's avatar
Mário Pereira committed
931
932
933
934
935
      mk_let subst pv1 (mk_let subst pv2 e), spv
    | Eraise (exn, None) -> mk (Eraise (exn, None)), Spv.empty
    | Eraise (exn, Some e) ->
      let e, spv = expr info subst e in
      mk (Eraise (exn, Some e)), spv
936
    | Etry (e, bl) ->
Mário Pereira's avatar
Mário Pereira committed
937
938
939
      let e, spv = expr info subst e in
      let e_bl, spv_bl = mk_list_eb bl (xbranch info subst) in
      mk (Etry (e, e_bl)), Spv.union spv spv_bl
Mário Pereira's avatar
Mário Pereira committed
940
    | Eassign al -> (* FIXME : produced superfolous let *)