pmodule.ml 46.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

12
open Wstdlib
13 14
open Ident
open Ty
15
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
16
open Decl
17 18 19
open Theory
open Ity
open Expr
20
open Pdecl
21 22 23 24 25 26

(** *)

type prog_symbol =
  | PV of pvsymbol
  | RS of rsymbol
27
  | OO of Srs.t
28 29 30 31

type namespace = {
  ns_ts : itysymbol   Mstr.t;  (* type symbols *)
  ns_ps : prog_symbol Mstr.t;  (* program symbols *)
32
  ns_xs : xsymbol     Mstr.t;  (* exception symbols *)
33 34 35 36 37 38
  ns_ns : namespace   Mstr.t;  (* inner namespaces *)
}

let empty_ns = {
  ns_ts = Mstr.empty;
  ns_ps = Mstr.empty;
39
  ns_xs = Mstr.empty;
40 41 42 43 44
  ns_ns = Mstr.empty;
}

let ns_replace eq chk x vo vn =
  if not chk then vn else
45
  if eq vo vn then vo else
46 47
  raise (ClashSymbol x)

48 49
let merge_ts = ns_replace its_equal
let merge_xs = ns_replace xs_equal
50

51
type overload =
52 53 54
  | FixedRes of ity (* t -> t -> ... -> T *)
  | SameType        (* t -> t -> ... -> t *)
  | NoOver          (* neither *)
55 56 57 58

let overload_of_rs {rs_cty = cty} =
  if cty.cty_effect.eff_ghost then NoOver else
  if cty.cty_mask <> MaskVisible then NoOver else
59
  let same_type ity a = not a.pv_ghost && ity_equal a.pv_ity ity in
60
  match cty.cty_args with
61 62 63
  | a::al when not a.pv_ghost && List.for_all (same_type a.pv_ity) al ->
      let res = cty.cty_result in
      if ity_equal res a.pv_ity then SameType else
64
      if ity_closed res && res.ity_pure then FixedRes res else NoOver
65 66
  | _ -> NoOver

67 68 69 70 71 72 73
let same_overload r1 r2 =
  List.length r1.rs_cty.cty_args = List.length r2.rs_cty.cty_args &&
  match overload_of_rs r1, overload_of_rs r2 with
  | SameType, SameType -> true
  | FixedRes t1, FixedRes t2 -> ity_equal t1 t2
  | _ -> false (* two NoOver's are not the same *)

74 75
exception IncompatibleNotation of string

Andrei Paskevich's avatar
Andrei Paskevich committed
76 77 78 79 80 81 82 83 84 85 86 87 88
let merge_ps chk x vo vn =
  let fsty rs = (List.hd rs.rs_cty.cty_args).pv_ity in
  if chk then match vo, vn with (* export namespace *)
    (* currently, we have no way to export notation *)
    | _, OO _ | OO _, _ -> assert false
    | PV v1, PV v2 when pv_equal v1 v2 -> vo
    | RS r1, RS r2 when rs_equal r1 r2 -> vo
    | _ -> raise (ClashSymbol x)
  else match vo, vn with (* import namespace *)
    (* once again, no way to export notation *)
    | _, OO _ -> assert false
    (* but we can merge two compatible symbols *)
    | RS r1, RS r2 when not (rs_equal r1 r2) ->
89 90
        if not (same_overload r1 r2) then vn else
        if ity_equal (fsty r1) (fsty r2) then vn else
Andrei Paskevich's avatar
Andrei Paskevich committed
91 92 93
        OO (Srs.add r2 (Srs.singleton r1))
    (* or add a compatible symbol to notation *)
    | OO s1, RS r2 ->
94 95 96
        let r1 = Srs.choose s1 and ty = fsty r2 in
        if not (same_overload r1 r2) then vn else
        let confl r = not (ity_equal (fsty r) ty) in
Andrei Paskevich's avatar
Andrei Paskevich committed
97 98 99 100
        let s1 = Srs.filter confl s1 in
        if Srs.is_empty s1 then vn else
        OO (Srs.add r2 s1)
    | _ -> vn
101

102 103 104 105 106 107 108 109 110
let rec merge_ns chk _ no nn =
  if no == nn then no else
  let union merge o n =
    let merge x vo vn = Some (merge chk x vo vn) in
    if o == n then o else Mstr.union merge o n in
  { ns_ts = union merge_ts no.ns_ts nn.ns_ts;
    ns_ps = union merge_ps no.ns_ps nn.ns_ps;
    ns_xs = union merge_xs no.ns_xs nn.ns_xs;
    ns_ns = union merge_ns no.ns_ns nn.ns_ns }
111

112 113
let ns_add merge chk x vn m = Mstr.change (function
  | Some vo -> Some (merge chk x vo vn)
114 115
  | None    -> Some vn) x m

116 117 118 119 120 121
let add_ts chk x ts ns = { ns with ns_ts = ns_add merge_ts chk x ts ns.ns_ts }
let add_ps chk x ps ns = { ns with ns_ps = ns_add merge_ps chk x ps ns.ns_ps }
let add_xs chk x xs ns = { ns with ns_xs = ns_add merge_xs chk x xs ns.ns_xs }
let add_ns chk x nn ns = { ns with ns_ns = ns_add merge_ns chk x nn ns.ns_ns }

let merge_ns chk nn no = merge_ns chk "" no nn (* swap arguments *)
122 123 124 125 126 127

let rec ns_find get_map ns = function
  | []   -> assert false
  | [a]  -> Mstr.find a (get_map ns)
  | a::l -> ns_find get_map (Mstr.find a ns.ns_ns) l

128 129 130 131 132 133 134 135 136 137 138 139
let ns_find_its = ns_find (fun ns -> ns.ns_ts)
let ns_find_xs  = ns_find (fun ns -> ns.ns_xs)
let ns_find_ns  = ns_find (fun ns -> ns.ns_ns)

let ns_find_prog_symbol ns s =
  let ps = ns_find (fun ns -> ns.ns_ps) ns s in
  match ps with
  | RS _ | PV _ -> ps
  | OO ss ->
      let rs1 = Expr.Srs.min_elt ss in
      let rs2 = Expr.Srs.max_elt ss in
      if Expr.rs_equal rs1 rs2 then RS rs1 else ps
140 141 142 143 144 145 146 147 148

let ns_find_pv ns s = match ns_find_prog_symbol ns s with
  | PV pv -> pv | _ -> raise Not_found

let ns_find_rs ns s = match ns_find_prog_symbol ns s with
  | RS rs -> rs | _ -> raise Not_found

(** {2 Module} *)

149
type pmodule = {
Andrei Paskevich's avatar
Andrei Paskevich committed
150 151 152 153 154 155 156 157 158 159 160
  mod_theory : theory;        (* pure theory *)
  mod_units  : mod_unit list; (* module declarations *)
  mod_export : namespace;     (* exported namespace *)
  mod_known  : known_map;     (* known identifiers *)
  mod_local  : Sid.t;         (* locally declared idents *)
  mod_used   : Sid.t;         (* used modules *)
}

and mod_unit =
  | Udecl  of pdecl
  | Uuse   of pmodule
Andrei Paskevich's avatar
Andrei Paskevich committed
161
  | Uclone of mod_inst
Andrei Paskevich's avatar
Andrei Paskevich committed
162
  | Umeta  of meta * meta_arg list
163
  | Uscope of string * mod_unit list
Andrei Paskevich's avatar
Andrei Paskevich committed
164

Andrei Paskevich's avatar
Andrei Paskevich committed
165
and mod_inst = {
Andrei Paskevich's avatar
Andrei Paskevich committed
166
  mi_mod : pmodule;
167 168
  mi_ty  : ity Mts.t;
  mi_ts  : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
169 170
  mi_ls  : lsymbol Mls.t;
  mi_pr  : prsymbol Mpr.t;
171
  mi_pk  : prop_kind Mpr.t;
172
  mi_pv  : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
173
  mi_rs  : rsymbol Mrs.t;
174
  mi_xs  : xsymbol Mxs.t;
175
  mi_df  : prop_kind;
176 177
}

178 179 180 181 182 183 184 185 186
let empty_mod_inst m = {
  mi_mod = m;
  mi_ty  = Mts.empty;
  mi_ts  = Mts.empty;
  mi_ls  = Mls.empty;
  mi_pr  = Mpr.empty;
  mi_pk  = Mpr.empty;
  mi_pv  = Mvs.empty;
  mi_rs  = Mrs.empty;
187
  mi_xs  = Mxs.empty;
188
  mi_df  = Plemma;
189 190
}

191 192
(** {2 Module under construction} *)

193
type pmodule_uc = {
194
  muc_theory : theory_uc;
Andrei Paskevich's avatar
Andrei Paskevich committed
195
  muc_units  : mod_unit list;
196 197 198 199 200
  muc_import : namespace list;
  muc_export : namespace list;
  muc_known  : known_map;
  muc_local  : Sid.t;
  muc_used   : Sid.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
201
  muc_env    : Env.env;
202 203 204 205
}

let empty_module env n p = {
  muc_theory = create_theory ~path:p n;
Andrei Paskevich's avatar
Andrei Paskevich committed
206
  muc_units  = [];
207 208 209 210 211 212 213 214 215 216 217 218 219
  muc_import = [empty_ns];
  muc_export = [empty_ns];
  muc_known  = Mid.empty;
  muc_local  = Sid.empty;
  muc_used   = Sid.empty;
  muc_env    = env;
}

let close_module, restore_module =
  let h = Hid.create 17 in
  (fun uc ->
     let th = close_theory uc.muc_theory in (* catches errors *)
     let m = { mod_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
220
               mod_units  = List.rev uc.muc_units;
221 222 223 224 225 226 227 228
               mod_export = List.hd uc.muc_export;
               mod_known  = uc.muc_known;
               mod_local  = uc.muc_local;
               mod_used   = uc.muc_used; } in
     Hid.add h th.th_name m;
     m),
  (fun th -> Hid.find h th.th_name)

229
let open_scope uc s = match uc.muc_import with
230
  | ns :: _ -> { uc with
231
      muc_theory = Theory.open_scope uc.muc_theory s;
232
      muc_units  = [Uscope (s, uc.muc_units)];
233 234 235 236
      muc_import =       ns :: uc.muc_import;
      muc_export = empty_ns :: uc.muc_export; }
  | [] -> assert false

237 238
let close_scope uc ~import =
  let th = Theory.close_scope uc.muc_theory ~import in
Andrei Paskevich's avatar
Andrei Paskevich committed
239
  match List.rev uc.muc_units, uc.muc_import, uc.muc_export with
240
  | [Uscope (_,ul1)], _ :: sti, _ :: ste -> (* empty scope *)
Andrei Paskevich's avatar
Andrei Paskevich committed
241 242
      { uc with muc_theory = th;  muc_units  = ul1;
                muc_import = sti; muc_export = ste; }
243
  | Uscope (s,ul1) :: ul0, _ :: i1 :: sti, e0 :: e1 :: ste ->
244 245 246 247
      let i1 = if import then merge_ns false e0 i1 else i1 in
      let i1 = add_ns false s e0 i1 in
      let e1 = add_ns true  s e0 e1 in
      { uc with
248
          muc_theory = th;
249
          muc_units  = Uscope (s,ul0) :: ul1;
250 251
          muc_import = i1 :: sti;
          muc_export = e1 :: ste; }
Andrei Paskevich's avatar
Andrei Paskevich committed
252
  | _ -> assert false
253

254 255 256 257 258 259 260
let import_scope uc ql = match uc.muc_import with
  | i1 :: sti ->
      let th = Theory.import_scope uc.muc_theory ql in
      let i1 = merge_ns false (ns_find_ns i1 ql) i1 in
      { uc with muc_theory = th; muc_import = i1::sti }
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
261 262 263 264 265 266
let use_export uc ({mod_theory = mth} as m) =
  let th = Theory.use_export uc.muc_theory mth in
  let uc = if Sid.mem mth.th_name uc.muc_used then uc
    else { uc with
      muc_known = merge_known uc.muc_known m.mod_known;
      muc_used  = Sid.add mth.th_name uc.muc_used } in
267 268 269
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
270 271 272
      muc_units  = Uuse m :: uc.muc_units;
      muc_import = merge_ns false m.mod_export i0 :: sti;
      muc_export = merge_ns true  m.mod_export e0 :: ste; }
273 274
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
275 276 277
let add_meta uc m al = { uc with
  muc_theory = Theory.add_meta uc.muc_theory m al;
  muc_units  = Umeta (m,al) :: uc.muc_units; }
278

279 280
let store_path, store_module, restore_path =
  let id_to_path = Wid.create 17 in
Andrei Paskevich's avatar
Andrei Paskevich committed
281
  let store_path {muc_theory = uc} path id =
282 283
    (* this symbol already belongs to some theory *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
284 285 286
    let prefix = List.rev (id.id_string :: path @ uc.uc_prefix) in
    Wid.set id_to_path id (uc.uc_path, uc.uc_name.id_string, prefix) in
  let store_module {mod_theory = {th_name = id} as th} =
287 288
    (* this symbol is already a module *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
289
    Wid.set id_to_path id (th.th_path, id.id_string, []) in
290 291 292 293 294 295 296 297
  let restore_path id = Wid.find id_to_path id in
  store_path, store_module, restore_path

let close_module uc =
  let m = close_module uc in
  store_module m;
  m

298
(*
299 300 301 302
let count_regions {muc_known = kn} {pv_ity = ity} mr =
  let add_reg r mr = Mreg.change (fun n -> Some (n <> None)) r mr in
  let meet mr1 mr2 = Mreg.union (fun _ x y -> Some (x || y)) mr1 mr2 in
  let join mr1 mr2 = Mreg.union (fun _ _ _ -> Some true) mr1 mr2 in
303
  let rec down mr ity = if ity.ity_imm then mr else
304 305 306
    match ity.ity_node with
    | Ityreg r -> fields (add_reg r mr) r.reg_its r.reg_args r.reg_regs
    | Ityapp (s,tl,rl) -> fields mr s tl rl
307
    | Ityvar _ -> assert false
308 309 310
  and fields mr s tl rl =
    if s.its_private && rl = [] then mr else
    let isb = its_match_regs s tl rl in
311 312 313 314 315 316 317 318 319 320 321
    let add_ity mr ity = down mr (ity_full_inst isb ity) in
    let add_proj mr f = add_ity mr f.rs_cty.cty_result in
    let add_field mr v = add_ity mr v.pv_ity in
    let d = find_its_defn kn s in
    if d.itd_constructors = [] then
      List.fold_left add_proj mr d.itd_fields
    else
      join mr (List.fold_left (fun mr c ->
        meet mr (List.fold_left add_field Mreg.empty c.rs_cty.cty_args))
        Mreg.empty d.itd_constructors) in
  down mr ity
322
*)
323

324 325 326 327 328 329 330 331
let add_symbol add id v uc =
  store_path uc [] id;
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_import = add false id.id_string v i0 :: sti;
      muc_export = add true  id.id_string v e0 :: ste }
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
332
let add_pdecl_no_logic uc d =
333
  let uc = { uc with
Andrei Paskevich's avatar
Andrei Paskevich committed
334
    muc_units = Udecl d :: uc.muc_units;
335
    muc_known = known_add_decl uc.muc_known d;
336
    muc_local = Sid.union uc.muc_local d.pd_news } in
337
  let add_rs uc s = add_symbol add_ps s.rs_name (RS s) uc in
338
  let add_rd uc d = add_rs uc d.rec_sym in
339 340 341 342 343 344 345 346
  match d.pd_node with
  | PDtype tdl ->
      let add uc d =
        let uc = List.fold_left add_rs uc d.itd_fields in
        let uc = List.fold_left add_rs uc d.itd_constructors in
        add_symbol add_ts d.itd_its.its_ts.ts_name d.itd_its uc in
      List.fold_left add uc tdl
  | PDlet (LDvar (v,_)) -> add_symbol add_ps v.pv_vs.vs_name (PV v) uc
347
  | PDlet (LDsym (s,_)) -> add_rs uc s
348
  | PDlet (LDrec l) -> List.fold_left add_rd uc l
349
  | PDexn xs -> add_symbol add_xs xs.xs_name xs uc
350
  | PDpure -> uc
351

352
let add_pdecl_raw ?(warn=true) uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
353
  let uc = add_pdecl_no_logic uc d in
354
  let th = List.fold_left (add_decl ~warn) uc.muc_theory d.pd_pure in
355 356
  let add_meta th (m,l) = Theory.add_meta th m l in
  let th = List.fold_left add_meta th d.pd_meta in
Andrei Paskevich's avatar
Andrei Paskevich committed
357 358
  { uc with muc_theory = th }

359 360
(** {2 Builtin symbols} *)

Andrei Paskevich's avatar
Andrei Paskevich committed
361 362
let dummy_env = Env.create_env []

363
let builtin_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
364 365 366 367
  let uc = empty_module dummy_env (id_fresh "BuiltIn") ["why3";"BuiltIn"] in
  let uc = add_pdecl_no_logic uc pd_int in
  let uc = add_pdecl_no_logic uc pd_real in
  let uc = add_pdecl_no_logic uc pd_equ in
368 369
  let m = close_module uc in
  { m with mod_theory = builtin_theory }
370 371

let bool_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
372 373
  let uc = empty_module dummy_env (id_fresh "Bool") ["why3";"Bool"] in
  let uc = add_pdecl_no_logic uc pd_bool in
374 375
  let m = close_module uc in
  { m with mod_theory = bool_theory }
376 377

let highord_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
378 379 380
  let uc = empty_module dummy_env (id_fresh "HighOrd") ["why3";"HighOrd"] in
  let uc = add_pdecl_no_logic uc pd_func in
  let uc = add_pdecl_no_logic uc pd_func_app in
381 382
  let m = close_module uc in
  { m with mod_theory = highord_theory }
383

384 385
let tuple_module = Hint.memo 17 (fun n ->
  let nm = "Tuple" ^ string_of_int n in
Andrei Paskevich's avatar
Andrei Paskevich committed
386 387
  let uc = empty_module dummy_env (id_fresh nm) ["why3";nm] in
  let uc = add_pdecl_no_logic uc (pd_tuple n) in
388 389
  let m = close_module uc in
  { m with mod_theory = tuple_theory n })
390 391

let unit_module =
Andrei Paskevich's avatar
Andrei Paskevich committed
392
  let uc = empty_module dummy_env (id_fresh "Unit") ["why3";"Unit"] in
393
  let uc = use_export uc (tuple_module 0) in
394
  let add uc d = add_pdecl_raw ~warn:false uc d in
395
  let td = create_alias_decl (id_fresh "unit") [] ity_unit in
396
  close_module (List.fold_left add uc (create_type_decl [td]))
397 398

let create_module env ?(path=[]) n =
Andrei Paskevich's avatar
Andrei Paskevich committed
399
  let m = empty_module env n path in
400 401 402 403 404
  let m = use_export m builtin_module in
  let m = use_export m bool_module in
  let m = use_export m unit_module in
  m

Andrei Paskevich's avatar
Andrei Paskevich committed
405 406 407 408 409 410 411
let add_use uc d = Sid.fold (fun id uc ->
  if id_equal id ts_func.ts_name then
    use_export uc highord_module
  else match is_ts_tuple_id id with
  | Some n -> use_export uc (tuple_module n)
  | None -> uc) (Mid.set_diff d.pd_syms uc.muc_known) uc

412 413
let mk_vc uc d = Vc.vc uc.muc_env uc.muc_known uc.muc_theory d

414
let add_pdecl ?(warn=true) ~vc uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
415
  let uc = add_use uc d in
416
  let dl = if vc then mk_vc uc d else [] in
417 418 419 420
  (* verification conditions must not add additional dependencies
     on built-in theories like TupleN or HighOrd. Also, we expect
     int.Int or any other library theory to be in the context:
     importing them automatically seems to be too invasive. *)
421
  add_pdecl_raw ~warn (List.fold_left (add_pdecl_raw ~warn) uc dl) d
422

Andrei Paskevich's avatar
Andrei Paskevich committed
423 424 425 426
(** {2 Cloning} *)

type clones = {
  cl_local : Sid.t;
427 428
  mutable ty_table : ity Mts.t;
  mutable ts_table : itysymbol Mts.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
429 430 431
  mutable ls_table : lsymbol Mls.t;
  mutable pr_table : prsymbol Mpr.t;
  mutable rn_table : region Mreg.t;
432
  mutable fd_table : pvsymbol Mpv.t;
433
  mutable pv_table : pvsymbol Mvs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
434
  mutable rs_table : rsymbol Mrs.t;
435
  mutable xs_table : xsymbol Mxs.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
436 437
}

438 439
let empty_clones m = {
  cl_local = m.mod_local;
440
  ty_table = Mts.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
441 442 443 444
  ts_table = Mts.empty;
  ls_table = Mls.empty;
  pr_table = Mpr.empty;
  rn_table = Mreg.empty;
445
  fd_table = Mpv.empty;
446
  pv_table = Mvs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
447
  rs_table = Mrs.empty;
448
  xs_table = Mxs.empty;
Andrei Paskevich's avatar
Andrei Paskevich committed
449 450 451 452
}

(* populate the clone structure *)

453
let rec sm_trans_ty tym tsm ty = match ty.ty_node with
454
  | Tyapp (s, tl) ->
455
      let tl = List.map (sm_trans_ty tym tsm) tl in
456
      begin match Mts.find_opt s tsm with
457 458
      | Some its -> ty_app its.its_ts tl
      | None -> begin match Mts.find_opt s tym with
459 460
      | Some ity -> ty_inst (ts_match_args s tl) (ty_of_ity ity)
      | None -> ty_app s tl
461
      end end
462 463
  | Tyvar _ -> ty

Andrei Paskevich's avatar
Andrei Paskevich committed
464
let clone_ty cl ty = sm_trans_ty cl.ty_table cl.ts_table ty
465

466 467 468
let cl_find_its cl its =
  if not (Sid.mem its.its_ts.ts_name cl.cl_local) then its
  else Mts.find its.its_ts cl.ts_table
469

470 471 472
let cl_find_ts cl ts =
  if not (Sid.mem ts.ts_name cl.cl_local) then ts
  else (Mts.find ts cl.ts_table).its_ts
473

Andrei Paskevich's avatar
Andrei Paskevich committed
474
let rec clone_ity cl ity = match ity.ity_node with
475
  | Ityreg r ->
Andrei Paskevich's avatar
Andrei Paskevich committed
476
      ity_reg (clone_reg cl r)
477
  | Ityapp (s, tl, rl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
478
      let tl = List.map (clone_ity cl) tl in
479
      let rl = List.map (clone_ity cl) rl in
480
      begin match Mts.find_opt s.its_ts cl.ts_table with
481 482 483
      | Some its -> ity_app_pure its tl rl
      | None -> (* creative indentation *)
      begin match Mts.find_opt s.its_ts cl.ty_table with
484
      | Some ity -> ity_full_inst (its_match_regs s tl rl) ity
485
      | None -> ity_app_pure s tl rl
486
      end end
Andrei Paskevich's avatar
Andrei Paskevich committed
487 488
  | Ityvar _ -> ity

Andrei Paskevich's avatar
Andrei Paskevich committed
489
and clone_reg cl reg =
490 491 492 493
  (* FIXME: what about top-level non-instantiated regions?
     We cannot check in cl.cl_local to see if they are there.
     Instead, we should prefill cl.pv_table and cl.rn_table
     with all top-level pvsymbols (local or external) before
494 495 496
     descending into a let_defn.
     TODO: add to module/uc a list of locally-defined toplevel
     variables, as well as a set of imported toplevel variables. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
497
  try Mreg.find reg cl.rn_table with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
498
  let tl = List.map (clone_ity cl) reg.reg_args in
499
  let rl = List.map (clone_ity cl) reg.reg_regs in
500
  let r = match Mts.find_opt reg.reg_its.its_ts cl.ts_table with
501 502
    | Some its ->
        create_region (id_clone reg.reg_name) its tl rl
503 504
    | None -> (* creative indentation *)
    begin match Mts.find_opt reg.reg_its.its_ts cl.ty_table with
505 506 507
    | Some {ity_node = Ityreg r} ->
        let sbs = its_match_regs reg.reg_its tl rl in
        let tl = List.map (ity_full_inst sbs) r.reg_args in
508
        let rl = List.map (ity_full_inst sbs) r.reg_regs in
509
        create_region (id_clone reg.reg_name) r.reg_its tl rl
510
    | Some _ -> assert false
511 512
    | None ->
        create_region (id_clone reg.reg_name) reg.reg_its tl rl
513
    end in
514 515
  cl.rn_table <- Mreg.add reg r cl.rn_table;
  r
Andrei Paskevich's avatar
Andrei Paskevich committed
516 517 518

let cl_find_ls cl ls =
  if not (Sid.mem ls.ls_name cl.cl_local) then ls
519
  else Mls.find ls cl.ls_table
Andrei Paskevich's avatar
Andrei Paskevich committed
520

Andrei Paskevich's avatar
Andrei Paskevich committed
521
let clone_term cl mv t = t_gen_map (clone_ty cl) (cl_find_ls cl) mv t
522

Andrei Paskevich's avatar
Andrei Paskevich committed
523
let clone_fmla cl f = clone_term cl Mvs.empty f (* for closed terms *)
Andrei Paskevich's avatar
Andrei Paskevich committed
524

Andrei Paskevich's avatar
Andrei Paskevich committed
525
let cl_find_pr cl pr =
Andrei Paskevich's avatar
Andrei Paskevich committed
526
  if not (Sid.mem pr.pr_name cl.cl_local) then pr
527
  else Mpr.find pr cl.pr_table
Andrei Paskevich's avatar
Andrei Paskevich committed
528

Andrei Paskevich's avatar
Andrei Paskevich committed
529
let cl_find_pv cl pv =
Andrei Paskevich's avatar
Andrei Paskevich committed
530
  if not (Sid.mem pv.pv_vs.vs_name cl.cl_local) then pv
531
  else Mvs.find pv.pv_vs cl.pv_table
Andrei Paskevich's avatar
Andrei Paskevich committed
532

Andrei Paskevich's avatar
Andrei Paskevich committed
533
let cl_find_rs cl rs =
Andrei Paskevich's avatar
Andrei Paskevich committed
534 535 536
  if not (Sid.mem rs.rs_name cl.cl_local) then rs
  else Mrs.find rs cl.rs_table

Andrei Paskevich's avatar
Andrei Paskevich committed
537
let cl_find_xs cl xs =
Andrei Paskevich's avatar
Andrei Paskevich committed
538
  if not (Sid.mem xs.xs_name cl.cl_local) then xs
539
  else Mxs.find xs cl.xs_table
Andrei Paskevich's avatar
Andrei Paskevich committed
540

541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571
let cl_init m inst =
  let cl = empty_clones m in
  let non_local id =
    if not (Sid.mem id cl.cl_local) then raise (NonLocal id) in
  Mts.iter (fun ts _ -> non_local ts.ts_name) inst.mi_ts;
  Mts.iter (fun ts _ -> non_local ts.ts_name) inst.mi_ty;
  let check_ls ls _ =
    non_local ls.ls_name;
    try  ignore (restore_rs ls); raise (BadInstance ls.ls_name)
    with Not_found -> () in
  Mls.iter check_ls inst.mi_ls;
  let check_rs rs _ =
    non_local rs.rs_name;
    match (Mid.find rs.rs_name m.mod_known).pd_node with
    | PDtype _ -> raise (BadInstance rs.rs_name)
    | PDlet  _ | PDexn  _ | PDpure -> () in
  Mrs.iter check_rs inst.mi_rs;
  Mvs.iter (fun vs _ -> non_local vs.vs_name) inst.mi_pv;
  Mxs.iter (fun xs _ -> non_local xs.xs_name) inst.mi_xs;
  let check_pk pr _ =
    non_local pr.pr_name;
    match (Mid.find pr.pr_name m.mod_known).pd_node with
    | PDtype _ | PDlet  _ | PDexn  _ -> raise (BadInstance pr.pr_name)
    | PDpure -> () in
  Mpr.iter check_pk inst.mi_pk;
  Mpr.iter (fun pr _ -> raise (BadInstance pr.pr_name)) inst.mi_pr;
  cl

(* clone declarations *)

let clone_ls cl ls =
Andrei Paskevich's avatar
Andrei Paskevich committed
572
  let constr = ls.ls_constr in
573
  let id = id_clone ls.ls_name in
Andrei Paskevich's avatar
Andrei Paskevich committed
574 575
  let at = List.map (clone_ty cl) ls.ls_args in
  let vt = Opt.map (clone_ty cl) ls.ls_value in
Andrei Paskevich's avatar
Andrei Paskevich committed
576 577 578 579 580
  let ls' = create_lsymbol ~constr id at vt in
  cl.ls_table <- Mls.add ls ls' cl.ls_table;
  ls'

let clone_decl inst cl uc d = match d.d_node with
581
  | Dtype _ | Ddata _ -> assert false (* impossible *)
582 583 584 585 586 587 588 589 590 591 592 593
  | Dparam ({ls_name = id} as ls) when Mls.mem ls inst.mi_ls ->
      let ls' = Mls.find ls inst.mi_ls in
      let mtch sb ty ty' = try ty_match sb ty' (clone_ty cl ty)
        with TypeMismatch _ -> raise (BadInstance id) in
      let sbs = match ls.ls_value,ls'.ls_value with
        | Some ty, Some ty' -> mtch Mtv.empty ty ty'
        | None, None -> Mtv.empty
        | _ -> raise (BadInstance id) in
      ignore (try List.fold_left2 mtch sbs ls.ls_args ls'.ls_args
        with Invalid_argument _ -> raise (BadInstance id));
      cl.ls_table <- Mls.add ls ls' cl.ls_table;
      uc
Andrei Paskevich's avatar
Andrei Paskevich committed
594
  | Dparam ls ->
595
      let d = create_param_decl (clone_ls cl ls) in
596
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
597
  | Dlogic ldl ->
598 599 600
      List.iter (fun (ls,_) ->
        if Mls.mem ls inst.mi_ls then raise (CannotInstantiate ls.ls_name);
        ignore (clone_ls cl ls)) ldl;
Andrei Paskevich's avatar
Andrei Paskevich committed
601
      let get_logic (_,ld) =
Andrei Paskevich's avatar
Andrei Paskevich committed
602
        Opt.get (ls_defn_of_axiom (clone_fmla cl (ls_defn_axiom ld))) in
Andrei Paskevich's avatar
Andrei Paskevich committed
603
      let d = create_logic_decl (List.map get_logic ldl) in
604
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
605
  | Dind (s, idl) ->
606 607 608
      let lls = List.map (fun (ls,_) ->
        if Mls.mem ls inst.mi_ls then raise (CannotInstantiate ls.ls_name);
        clone_ls cl ls) idl in
Andrei Paskevich's avatar
Andrei Paskevich committed
609
      let get_case (pr,f) =
610
        if Mpr.mem pr inst.mi_pk then raise (CannotInstantiate pr.pr_name);
Andrei Paskevich's avatar
Andrei Paskevich committed
611 612
        let pr' = create_prsymbol (id_clone pr.pr_name) in
        cl.pr_table <- Mpr.add pr pr' cl.pr_table;
Andrei Paskevich's avatar
Andrei Paskevich committed
613
        pr', clone_fmla cl f in
Andrei Paskevich's avatar
Andrei Paskevich committed
614 615
      let get_ind ls (_,la) = ls, List.map get_case la in
      let d = create_ind_decl s (List.map2 get_ind lls idl) in
616
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
617
  | Dprop (k,pr,f) ->
618
      let skip, k' = match k, Mpr.find_opt pr inst.mi_pk with
619 620 621 622
        | Pgoal, _ -> true, Pgoal
        | Plemma, Some Pgoal -> true, Pgoal
        | Plemma, _ -> false, Plemma
        | Paxiom, Some k -> false, k
623
        | Paxiom, None -> false, inst.mi_df in
Andrei Paskevich's avatar
Andrei Paskevich committed
624
      if skip then uc else
Andrei Paskevich's avatar
Andrei Paskevich committed
625 626
      let pr' = create_prsymbol (id_clone pr.pr_name) in
      cl.pr_table <- Mpr.add pr pr' cl.pr_table;
Andrei Paskevich's avatar
Andrei Paskevich committed
627
      let d = create_prop_decl k' pr' (clone_fmla cl f) in
628
      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
629

630 631 632
let cl_save_ls cl s s' =
  cl.ls_table <- Mls.add_new (CannotInstantiate s.ls_name) s s' cl.ls_table

633 634 635
let cl_save_rs cl s s' =
  cl.rs_table <- Mrs.add s s' cl.rs_table;
  begin match s.rs_field, s'.rs_field with
636 637 638
  | Some v, Some v' -> cl.fd_table <- Mpv.add v v' cl.fd_table
  | None, _ -> () (* can instantiate a non-field with a field *)
  | _ -> assert false (* but not vice versa *)
639 640
  end;
  match s.rs_logic, s'.rs_logic with
641
  | RLls s, RLls s' -> cl_save_ls cl s s'
642 643 644 645
  | RLlemma, RLlemma -> () (* TODO: update cl.pr_table? *)
  | RLnone, RLnone -> ()
  | _ -> assert false

Mário Pereira's avatar
Mário Pereira committed
646 647 648
type smap = {
  sm_vs : vsymbol Mvs.t;
  sm_pv : pvsymbol Mvs.t;
649
  sm_xs : xsymbol Mxs.t;
Mário Pereira's avatar
Mário Pereira committed
650 651 652 653 654 655
  sm_rs : rsymbol Mrs.t;
}

let sm_of_cl cl = {
  sm_vs = Mvs.map (fun v -> v.pv_vs) cl.pv_table;
  sm_pv = cl.pv_table;
656
  sm_xs = cl.xs_table;
Mário Pereira's avatar
Mário Pereira committed
657 658 659 660 661
  sm_rs = cl.rs_table }

let sm_save_vs sm v v' = {
  sm_vs = Mvs.add v v'.pv_vs sm.sm_vs;
  sm_pv = Mvs.add v v' sm.sm_pv;
662
  sm_xs = sm.sm_xs;
Mário Pereira's avatar
Mário Pereira committed
663 664 665 666 667
  sm_rs = sm.sm_rs }

let sm_save_pv sm v v' = {
  sm_vs = Mvs.add v.pv_vs v'.pv_vs sm.sm_vs;
  sm_pv = Mvs.add v.pv_vs v' sm.sm_pv;
668
  sm_xs = sm.sm_xs;
Mário Pereira's avatar
Mário Pereira committed
669 670
  sm_rs = sm.sm_rs }

671 672 673
let sm_save_xs sm s s' =
  { sm with sm_xs = Mxs.add s s' sm.sm_xs }

Mário Pereira's avatar
Mário Pereira committed
674 675 676 677 678 679 680 681 682 683
let sm_save_rs cl sm s s' =
  let sm = { sm with sm_rs = Mrs.add s s' sm.sm_rs } in
  match s.rs_logic, s'.rs_logic with
  | RLls s, RLls s' -> cl_save_ls cl s s'; sm
  | RLpv v, RLpv v' -> sm_save_pv sm v v'
  | _ -> sm

let sm_find_pv sm v = Mvs.find_def v v.pv_vs sm.sm_pv
  (* non-instantiated global variables are not in sm *)

684 685 686 687
let sm_find_xs sm xs = Mxs.find_def xs xs sm.sm_xs

let sm_find_rs sm rs = Mrs.find_def rs rs sm.sm_rs

Mário Pereira's avatar
Mário Pereira committed
688 689 690 691 692 693
let clone_pv cl {pv_vs = vs; pv_ity = ity; pv_ghost = ghost} =
  create_pvsymbol (id_clone vs.vs_name) ~ghost (clone_ity cl ity)

let clone_invl cl sm invl =
  List.map (fun t -> clone_term cl sm.sm_vs t) invl

694
let clone_varl cl sm varl = List.map (fun (t,r) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
695
  clone_term cl sm.sm_vs t, Opt.map (cl_find_ls cl) r) varl
696

697
let clone_cty cl sm ?(drop_decr=false) cty =
698
  let res = clone_ity cl cty.cty_result in
699
  let args = List.map (clone_pv cl) cty.cty_args in
700
  let sm_args = List.fold_left2 sm_save_pv sm cty.cty_args args in
701
  let add_old o n (sm, olds) = let o' = clone_pv cl o in
702
    sm_save_pv sm o o', Mpv.add o' (sm_find_pv sm_args n) olds in
703
  let sm_olds, olds = Mpv.fold add_old cty.cty_oldies (sm_args, Mpv.empty) in
704 705
  let pre = if drop_decr then List.tl cty.cty_pre else cty.cty_pre in
  let pre = clone_invl cl sm_args pre in
706
  let post = clone_invl cl sm_olds cty.cty_post in
707
  let xpost = Mxs.fold (fun xs fl q ->
708
    let xs = sm_find_xs sm xs in
709
    let fl = clone_invl cl sm_olds fl in
710
    Mxs.add xs fl q) cty.cty_xpost Mxs.empty in
711
  let add_read v s = Spv.add (sm_find_pv sm_args v) s in
712 713 714
  let reads = Spv.fold add_read (cty_reads cty) Spv.empty in
  let reads = List.fold_right add_read cty.cty_args reads in
  let reads = Spv.union reads (Mpv.domain olds) in
Mário Pereira's avatar
Mário Pereira committed
715
  let add_write reg fs m = (* add new mutable fields to functions effect *)
716
    let add_fd fd s = Spv.add (Mpv.find_def fd fd cl.fd_table) s in
717
    let reg' = clone_reg cl reg in
Mário Pereira's avatar
Mário Pereira committed
718 719
    let smf_reg' = Spv.of_list reg'.reg_its.its_mfields in
    let smf_reg = Spv.of_list reg.reg_its.its_mfields in
720 721
    let smf_ref = Spv.fold add_fd smf_reg Spv.empty in
    let smf_new = Spv.diff smf_reg' smf_ref in
Mário Pereira's avatar
Mário Pereira committed
722
    let fs = Spv.fold add_fd fs Spv.empty in
723
    Mreg.add reg' (Spv.union fs smf_new) m in
724
  let writes = Mreg.fold add_write cty.cty_effect.eff_writes Mreg.empty in
Andrei Paskevich's avatar
Andrei Paskevich committed
725
  let add_reset reg s = Sreg.add (clone_reg cl reg) s in
726 727
  let resets = Sreg.fold add_reset cty.cty_effect.eff_resets Sreg.empty in
  let eff = eff_reset (eff_write reads writes) resets in
728
  let add_raise xs eff = eff_raise eff (sm_find_xs sm xs) in
729
  let eff = Sxs.fold add_raise cty.cty_effect.eff_raises eff in
730
  let eff = if cty.cty_effect.eff_oneway then eff_diverge eff else eff in
731 732
  let cty = create_cty ~mask:cty.cty_mask args pre post xpost olds eff res in
  cty_ghostify (cty_ghost cty) cty
733 734 735 736 737

let sm_save_args sm c c' =
  List.fold_left2 sm_save_pv sm c.cty_args c'.cty_args

let sm_save_olds sm c c' =
738 739
  let revs = Mpv.fold (fun o n m -> Mpv.add n o m) c'.cty_oldies Mpv.empty in
  let add_old o n sm = sm_save_pv sm o (Mpv.find (sm_find_pv sm n) revs) in
740 741
  Mpv.fold add_old c.cty_oldies sm

742
let clone_ppat cl sm pp mask =
743 744
  let rec conv_pat p = match p.pat_node with
    | Term.Pwild -> PPwild
745 746 747
    | Term.Pvar v -> PPvar (id_clone v.vs_name, (restore_pv v).pv_ghost)
    | Term.Pas (p,v) ->
        PPas (conv_pat p, id_clone v.vs_name, (restore_pv v).pv_ghost)
748 749 750 751
    | Term.Por (p1,p2) -> PPor (conv_pat p1, conv_pat p2)
    | Term.Papp (s,pl) ->
        PPapp (restore_rs (cl_find_ls cl s), List.map conv_pat pl) in
  let pre = conv_pat pp.pp_pat in
752
  let vm, pp' = create_prog_pattern pre (clone_ity cl pp.pp_ity) mask in
753 754 755
  let save v sm = sm_save_vs sm v (Mstr.find v.vs_name.id_string vm) in
  Svs.fold save pp.pp_pat.pat_vars sm, pp'

Andrei Paskevich's avatar
Andrei Paskevich committed
756
let rec clone_expr cl sm e = e_attr_copy e (match e.e_node with
757
  | Evar v -> e_var (sm_find_pv sm v)
758
  | Econst c -> e_const c e.e_ity
759
  | Eexec (c,_) -> e_exec (clone_cexp cl sm c)
760 761 762 763
  | Eassign asl ->
      let conv (r,f,v) =
        e_var (sm_find_pv sm r), cl_find_rs cl f, e_var (sm_find_pv sm v) in
      e_assign (List.map conv asl)
764 765 766 767 768
  | Elet (ld, e) ->
      let sm, ld = clone_let_defn cl sm ld in
      e_let ld (clone_expr cl sm e)
  | Eif (e1, e2, e3) ->
      e_if (clone_expr cl sm e1) (clone_expr cl sm e2) (clone_expr cl sm e3)
769
  | Ematch (d, bl, xl) ->
770
      let d = clone_expr cl sm d in
771
      let conv_rbr (pp, e) =
772
        let sm, pp = clone_ppat cl sm pp d.e_mask in
773
        pp, clone_expr cl sm e in
774 775 776 777
      let conv_xbr xs (vl, e) m =
        let vl' = List.map (clone_pv cl) vl in
        let sm = List.fold_left2 sm_save_pv sm vl vl' in
        Mxs.add (sm_find_xs sm xs) (vl', clone_expr cl sm e) m in
778
      e_match d (List.map conv_rbr bl) (Mxs.fold conv_xbr xl Mxs.empty)
779 780 781
  | Ewhile (c,invl,varl,e) ->
      e_while (clone_expr cl sm c) (clone_invl cl sm invl)
              (clone_varl cl sm varl) (clone_expr cl sm e)
782 783 784 785 786 787
  | Efor (v, (f,dir,t), i, invl, e) ->
      let v' = clone_pv cl v in
      let ism = sm_save_pv sm v v' in
      let i' = if pv_equal v i then v' else clone_pv cl i in
      let ism = if pv_equal v i then ism else sm_save_pv ism i i' in
      e_for v'
788
        (e_var (sm_find_pv sm f)) dir (e_var (sm_find_pv sm t))
789
        i' (clone_invl cl ism invl) (clone_expr cl ism e)
790
  | Eraise (xs, e) ->
791 792 793 794
      e_raise (sm_find_xs sm xs) (clone_expr cl sm e) (clone_ity cl e.e_ity)
  | Eexn ({xs_name = id; xs_mask = mask; xs_ity = ity} as xs, e) ->
      let xs' = create_xsymbol (id_clone id) ~mask (clone_ity cl ity) in
      e_exn xs' (clone_expr cl (sm_save_xs sm xs xs') e)
795
  | Eassert (k, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
796
      e_assert k (clone_term cl sm.sm_vs f)
797 798
  | Eghost e ->
      e_ghostify true (clone_expr cl sm e)
799
  | Epure t ->
Andrei Paskevich's avatar
Andrei Paskevich committed
800
      e_pure (clone_term cl sm.sm_vs t)
801
  | Eabsurd -> e_absurd (clone_ity cl e.e_ity))
802

803
and clone_cexp cl sm c = match c.c_node with
804
  | Capp (s,vl) ->
805
      let vl = List.map (fun v -> sm_find_pv sm v) vl in
Andrei Paskevich's avatar
Andrei Paskevich committed
806 807
      let al = List.map (fun v -> clone_ity cl v.pv_ity) c.c_cty.cty_args in
      let res = clone_ity cl c.c_cty.cty_result in
808
      c_app (sm_find_rs sm s) vl al res
809 810 811 812 813
  | Cpur (s,vl) ->
      let vl = List.map (fun v -> sm_find_pv sm v) vl in
      let al = List.map (fun v -> clone_ity cl v.pv_ity) c.c_cty.cty_args in
      let res = clone_ity cl c.c_cty.cty_result in
      c_pur (cl_find_ls cl s) vl al res
814 815 816 817
  | Cfun e ->
      let cty = clone_cty cl sm c.c_cty in
      let sm = sm_save_args sm c.c_cty cty in
      let sm = sm_save_olds sm c.c_cty cty in
818 819
      c_fun ~mask:cty.cty_mask cty.cty_args cty.cty_pre
        cty.cty_post cty.cty_xpost cty.cty_oldies (clone_expr cl sm e)
820
  | Cany ->
821
      c_any (clone_cty cl sm c.c_cty)
822 823 824 825

and clone_let_defn cl sm ld = match ld with
  | LDvar (v,e) ->
      let e' = clone_expr cl sm e in
826 827
      let id = id_clone v.pv_vs.vs_name in
      let ld, v' = let_var id ~ghost:v.pv_ghost e' in
828 829 830 831 832 833 834
      sm_save_pv sm v v', ld
  | LDsym (s,c) ->
      let c' = clone_cexp cl sm c in
      let ld, s' = let_sym (id_clone s.rs_name)
        ~ghost:(rs_ghost s) ~kind:(rs_kind s) c' in
      sm_save_rs cl sm s s', ld
  | LDrec rdl ->
835 836
      let conv_rs mrs {rec_rsym = {rs_name = id} as rs} =
        let cty = clone_cty cl sm ~drop_decr:true rs.rs_cty in
837
        let rs' = create_rsymbol (id_clone id) ~ghost:(rs_ghost rs) cty in
838 839 840 841 842 843 844 845 846 847
        Mrs.add rs rs' mrs, rs' in
      let mrs, rsyml = Lists.map_fold_left conv_rs sm.sm_rs rdl in
      let rsm = { sm with sm_rs = mrs } in
      let conv_rd ({rec_fun = c} as rd) ({rs_cty = cty} as rs) =
        let rsm = sm_save_args rsm c.c_cty cty in
        let varl = clone_varl cl rsm rd.rec_varl in
        let rsm = sm_save_olds rsm c.c_cty cty in
        let e = match c.c_node with
          | Cfun e -> clone_expr cl rsm e
          | _ -> assert false (* can't be *) in
848
        let c = c_fun ~mask:c.c_cty