pmodule.ml 25.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2015   --   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.                           *)
(*                                                                  *)
(********************************************************************)

open Stdlib
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 27 28 29 30

(** *)

type prog_symbol =
  | PV of pvsymbol
  | RS of rsymbol

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

let empty_ns = {
  ns_ts = Mstr.empty;
  ns_ps = Mstr.empty;
38
  ns_xs = Mstr.empty;
39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
  ns_ns = Mstr.empty;
}

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

let psym_equal p1 p2 = match p1,p2 with
  | PV p1, PV p2 -> pv_equal p1 p2
  | RS p1, RS p2 -> rs_equal p1 p2
  | _, _ -> false

let rec merge_ns chk ns1 ns2 =
  if ns1 == ns2 then ns1 else
  let join eq x n o = Some (ns_replace eq chk x o n) in
  let ns_union eq m1 m2 =
    if m1 == m2 then m1 else Mstr.union (join eq) m1 m2 in
  let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
  { ns_ts = ns_union its_equal ns1.ns_ts ns2.ns_ts;
    ns_ps = ns_union psym_equal ns1.ns_ps ns2.ns_ps;
60
    ns_xs = ns_union xs_equal ns1.ns_xs ns2.ns_xs;
61 62 63 64 65 66 67 68 69 70
    ns_ns = Mstr.union fusion ns1.ns_ns ns2.ns_ns; }

let add_ns chk x ns m = Mstr.change (function
  | Some os -> Some (merge_ns chk ns os)
  | None    -> Some ns) x m

let ns_add eq chk x vn m = Mstr.change (function
  | Some vo -> Some (ns_replace eq chk x vo vn)
  | None    -> Some vn) x m

71
let add_xs chk x xs ns = { ns with ns_xs = ns_add xs_equal   chk x xs ns.ns_xs }
72
let add_ts chk x ts ns = { ns with ns_ts = ns_add its_equal  chk x ts ns.ns_ts }
73
let add_ps chk x ps ns = { ns with ns_ps = ns_add psym_equal chk x ps ns.ns_ps }
74 75 76 77 78 79 80 81 82
let add_ns chk x nn ns = { ns with ns_ns = add_ns            chk x nn ns.ns_ns }

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

let ns_find_prog_symbol = ns_find (fun ns -> ns.ns_ps)
let ns_find_ns          = ns_find (fun ns -> ns.ns_ns)
83
let ns_find_xs          = ns_find (fun ns -> ns.ns_xs)
84 85 86 87 88 89 90 91 92 93
let ns_find_its         = ns_find (fun ns -> ns.ns_ts)

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} *)

94
type pmodule = {
Andrei Paskevich's avatar
Andrei Paskevich committed
95 96 97 98 99 100 101 102 103 104 105
  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
106
  | Uclone of mod_inst
Andrei Paskevich's avatar
Andrei Paskevich committed
107 108 109
  | Umeta  of meta * meta_arg list
  | Uscope of string * bool * mod_unit list

Andrei Paskevich's avatar
Andrei Paskevich committed
110
and mod_inst = {
Andrei Paskevich's avatar
Andrei Paskevich committed
111 112 113 114 115 116 117
  mi_mod : pmodule;
  mi_ts  : itysymbol Mts.t;
  mi_ls  : lsymbol Mls.t;
  mi_pr  : prsymbol Mpr.t;
  mi_pv  : pvsymbol Mpv.t;
  mi_rs  : rsymbol Mrs.t;
  mi_xs  : xsymbol Mexn.t;
118 119 120 121
}

(** {2 Module under construction} *)

122
type pmodule_uc = {
123
  muc_theory : theory_uc;
Andrei Paskevich's avatar
Andrei Paskevich committed
124
  muc_units  : mod_unit list;
125 126 127 128 129 130 131 132 133 134
  muc_import : namespace list;
  muc_export : namespace list;
  muc_known  : known_map;
  muc_local  : Sid.t;
  muc_used   : Sid.t;
  muc_env    : Env.env option;
}

let empty_module env n p = {
  muc_theory = create_theory ~path:p n;
Andrei Paskevich's avatar
Andrei Paskevich committed
135
  muc_units  = [];
136 137 138 139 140 141 142 143 144 145 146 147 148
  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
149
               mod_units  = List.rev uc.muc_units;
150 151 152 153 154 155 156 157
               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)

158
let open_scope uc s = match uc.muc_import with
159
  | ns :: _ -> { uc with
160
      muc_theory = Theory.open_scope uc.muc_theory s;
Andrei Paskevich's avatar
Andrei Paskevich committed
161
      muc_units  = [Uscope (s, false, uc.muc_units)];
162 163 164 165
      muc_import =       ns :: uc.muc_import;
      muc_export = empty_ns :: uc.muc_export; }
  | [] -> assert false

166 167
let close_scope uc ~import =
  let th = Theory.close_scope uc.muc_theory ~import in
Andrei Paskevich's avatar
Andrei Paskevich committed
168
  match List.rev uc.muc_units, uc.muc_import, uc.muc_export with
Andrei Paskevich's avatar
Andrei Paskevich committed
169 170 171
  | [Uscope (_,_,ul1)], _ :: sti, _ :: ste -> (* empty scope *)
      { uc with muc_theory = th;  muc_units  = ul1;
                muc_import = sti; muc_export = ste; }
Andrei Paskevich's avatar
Andrei Paskevich committed
172
  | Uscope (s,_,ul1) :: ul0, _ :: i1 :: sti, e0 :: e1 :: ste ->
173 174 175 176 177
      let i1 = if import then merge_ns false e0 i1 else i1 in
      let _  = if import then merge_ns true  e0 e1 else e1 in
      let i1 = add_ns false s e0 i1 in
      let e1 = add_ns true  s e0 e1 in
      { uc with
178
          muc_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
179
          muc_units  = Uscope (s, import, ul0) :: ul1;
180 181
          muc_import = i1 :: sti;
          muc_export = e1 :: ste; }
Andrei Paskevich's avatar
Andrei Paskevich committed
182
  | _ -> assert false
183

Andrei Paskevich's avatar
Andrei Paskevich committed
184 185 186 187 188 189
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
190 191 192
  match uc.muc_import, uc.muc_export with
  | i0 :: sti, e0 :: ste -> { uc with
      muc_theory = th;
Andrei Paskevich's avatar
Andrei Paskevich committed
193 194 195
      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; }
196 197
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
198 199 200
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; }
201

202 203
let store_path, store_module, restore_path =
  let id_to_path = Wid.create 17 in
Andrei Paskevich's avatar
Andrei Paskevich committed
204
  let store_path {muc_theory = uc} path id =
205 206
    (* this symbol already belongs to some theory *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
207 208 209
    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} =
210 211
    (* this symbol is already a module *)
    if Wid.mem id_to_path id then () else
Andrei Paskevich's avatar
Andrei Paskevich committed
212
    Wid.set id_to_path id (th.th_path, id.id_string, []) in
213 214 215 216 217 218 219 220
  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

221 222 223 224 225 226 227 228 229
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
  let rec down mr ity = if ity.ity_pure then mr else
    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
    | Itypur (s,tl) -> fields mr s tl []
230
    | Ityvar _ -> assert false
231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
  and fields mr s tl rl = if s.its_privmut then mr else
    let add_arg isb v ity = ity_match isb (ity_var v) ity in
    let isb = List.fold_left2 add_arg isb_empty s.its_ts.ts_args tl in
    let isb = List.fold_left2 reg_match isb s.its_regions rl in
    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

247 248 249 250 251 252 253 254
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

255
let add_pdecl uc d =
256
  let uc = { uc with
Andrei Paskevich's avatar
Andrei Paskevich committed
257
    muc_units = Udecl d :: uc.muc_units;
258
    muc_known = known_add_decl uc.muc_known d;
259
    muc_local = Sid.union uc.muc_local d.pd_news } in
260
  let add_rs uc s = add_symbol add_ps s.rs_name (RS s) uc in
261 262 263 264 265 266 267 268 269 270
  let add_rs_noalias uc s = match s.rs_logic with
    | RLls _ | RLlemma ->
        let sv = s.rs_cty.cty_effect.eff_reads in
        let mr = Spv.fold (count_regions uc) sv Mreg.empty in
        Mreg.iter (fun _ n ->
          if n then Loc.errorm ?loc:s.rs_name.id_loc
            "The type of this function contains an alias") mr;
        add_rs uc s
    | _ -> add_rs uc s in
  let add_rd uc d = add_rs_noalias uc d.rec_sym in
271 272 273 274 275 276 277 278
  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
279 280
  | PDlet (LDsym (s,_)) -> add_rs_noalias uc s
  | PDlet (LDrec l) -> List.fold_left add_rd uc l
281
  | PDexn xs -> add_symbol add_xs xs.xs_name xs uc
282
  | PDpure -> uc
283 284 285 286

(** {2 Builtin symbols} *)

let builtin_module =
287 288 289 290 291 292
  let uc = empty_module None (id_fresh "BuiltIn") ["why3";"BuiltIn"] in
  let uc = add_pdecl uc pd_int in
  let uc = add_pdecl uc pd_real in
  let uc = add_pdecl uc pd_equ in
  let m = close_module uc in
  { m with mod_theory = builtin_theory }
293 294 295

let bool_module =
  let uc = empty_module None (id_fresh "Bool") ["why3";"Bool"] in
296 297 298
  let uc = add_pdecl uc pd_bool in
  let m = close_module uc in
  { m with mod_theory = bool_theory }
299 300 301 302

let highord_module =
  let uc = empty_module None (id_fresh "HighOrd") ["why3";"HighOrd"] in
  let uc = use_export uc bool_module in
303 304 305 306 307
  let uc = add_pdecl uc pd_func in
  let uc = add_pdecl uc pd_pred in
  let uc = add_pdecl uc pd_func_app in
  let m = close_module uc in
  { m with mod_theory = highord_theory }
308

309 310 311 312 313 314
let tuple_module = Hint.memo 17 (fun n ->
  let nm = "Tuple" ^ string_of_int n in
  let uc = empty_module None (id_fresh nm) ["why3";nm] in
  let uc = add_pdecl uc (pd_tuple n) in
  let m = close_module uc in
  { m with mod_theory = tuple_theory n })
315 316 317 318

let unit_module =
  let uc = empty_module None (id_fresh "Unit") ["why3";"Unit"] in
  let uc = use_export uc (tuple_module 0) in
319 320 321
  let td = create_alias_decl (id_fresh "unit") [] ity_unit in
  let uc = add_pdecl uc (create_type_decl [td]) in
  close_module uc
322 323 324 325 326 327 328 329

let create_module env ?(path=[]) n =
  let m = empty_module (Some env) n path in
  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

330
let add_pdecl ~vc uc d =
331 332 333 334 335 336 337
  let ids = Mid.set_diff d.pd_syms uc.muc_known in
  let uc = 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) ids uc in
338
  ignore vc; (* TODO *)
339
  let uc = add_pdecl uc d in
Andrei Paskevich's avatar
Andrei Paskevich committed
340
  let th = List.fold_left add_decl uc.muc_theory d.pd_pure in
341 342
  { uc with muc_theory = th }

Andrei Paskevich's avatar
Andrei Paskevich committed
343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373
(** {2 Cloning} *)

type clones = {
  cl_local : Sid.t;
  mutable ts_table : itysymbol Mts.t;
  mutable ls_table : lsymbol Mls.t;
  mutable pr_table : prsymbol Mpr.t;
  mutable rn_table : region Mreg.t;
  mutable pv_table : pvsymbol Mpv.t;
  mutable rs_table : rsymbol Mrs.t;
  mutable xs_table : xsymbol Mexn.t;
}

let empty_clones s = {
  cl_local = s;
  ts_table = Mts.empty;
  ls_table = Mls.empty;
  pr_table = Mpr.empty;
  rn_table = Mreg.empty;
  pv_table = Mpv.empty;
  rs_table = Mrs.empty;
  xs_table = Mexn.empty;
}

(* populate the clone structure *)

let rec cl_find_its cl its =
  if not (Sid.mem its.its_ts.ts_name cl.cl_local) then
    match its.its_def with
    | Some _ -> cl_make_its_alias cl its
    | None -> its
Andrei Paskevich's avatar
Andrei Paskevich committed
374 375
  else (*try*) Mts.find its.its_ts cl.ts_table
(*  with Not_found -> cl_make_its_pure cl its*)
Andrei Paskevich's avatar
Andrei Paskevich committed
376 377 378 379 380 381

and cl_find_ts cl ts =
  if not (Sid.mem ts.ts_name cl.cl_local) then
    match ts.ts_def with
    | Some _ -> (cl_make_its_alias cl (restore_its ts)).its_ts
    | None -> ts
Andrei Paskevich's avatar
Andrei Paskevich committed
382 383
  else (*try*) (Mts.find ts cl.ts_table).its_ts
(*  with Not_found -> (cl_make_its_pure cl (restore_its ts)).its_ts*)
Andrei Paskevich's avatar
Andrei Paskevich committed
384

Andrei Paskevich's avatar
Andrei Paskevich committed
385
(*
Andrei Paskevich's avatar
Andrei Paskevich committed
386 387 388 389 390 391 392
and cl_make_its_pure cl ({its_ts = ts} as its) =
  let id = id_clone ts.ts_name in
  let nts = match its.its_def with
    | Some def -> create_itysymbol_alias id ts.ts_args (cl_trans_ity cl def)
    | None -> create_itysymbol_pure id ts.ts_args in
  cl.ts_table <- Mts.add its.its_ts nts cl.ts_table;
  nts
Andrei Paskevich's avatar
Andrei Paskevich committed
393
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434

and cl_make_its_alias cl its =
  let odf = Opt.get its.its_def in
  let ndf = cl_trans_ity cl odf in
  if ity_equal odf ndf then its else
  create_itysymbol_alias (id_clone its.its_ts.ts_name) its.its_ts.ts_args ndf

and cl_trans_ity cl ity = match ity.ity_node with
  | Ityreg r -> ity_reg (cl_trans_reg cl r)
  | Ityapp (s,tl,rl) ->
      ity_app (cl_find_its cl s) (List.map (cl_trans_ity cl) tl)
                                 (List.map (cl_trans_reg cl) rl)
  | Itypur (s,tl) ->
      ity_pur (cl_find_its cl s) (List.map (cl_trans_ity cl) tl)
  | Ityvar _ -> ity

and cl_trans_reg cl reg =
  (* FIXME: what about global non-instantiated regions? *)
  try Mreg.find reg cl.rn_table with Not_found ->
    let r = create_region (id_clone reg.reg_name)
      (cl_find_its cl reg.reg_its) (List.map (cl_trans_ity cl) reg.reg_args)
                                   (List.map (cl_trans_reg cl) reg.reg_regs) in
    cl.rn_table <- Mreg.add reg r cl.rn_table;
    r

and cl_trans_ty cl ty = ty_s_map (cl_find_ts cl) ty

let cl_find_ls cl ls =
  if not (Sid.mem ls.ls_name cl.cl_local) then ls
  else (*try*) Mls.find ls cl.ls_table
(*
  with Not_found ->
    let constr = ls.ls_constr in
    let id  = id_clone ls.ls_name in
    let ta' = List.map (cl_trans_ty cl) ls.ls_args in
    let vt' = Opt.map (cl_trans_ty cl) ls.ls_value in
    let ls' = create_lsymbol ~constr id ta' vt' in
    cl.ls_table <- Mls.add ls ls' cl.ls_table;
    ls'
*)

Andrei Paskevich's avatar
Andrei Paskevich committed
435
let cl_trans_fmla cl f = t_s_map (cl_trans_ty cl) (cl_find_ls cl) f
Andrei Paskevich's avatar
Andrei Paskevich committed
436

Andrei Paskevich's avatar
Andrei Paskevich committed
437
let cl_find_pr cl pr =
Andrei Paskevich's avatar
Andrei Paskevich committed
438 439 440 441 442 443 444 445 446
  if not (Sid.mem pr.pr_name cl.cl_local) then pr
  else (*try*) Mpr.find pr cl.pr_table
(*
  with Not_found ->
    let pr' = create_prsymbol (id_clone pr.pr_name) in
    cl.pr_table <- Mpr.add pr pr' cl.pr_table;
    pr'
*)

Andrei Paskevich's avatar
Andrei Paskevich committed
447
let cl_find_pv cl pv =
Andrei Paskevich's avatar
Andrei Paskevich committed
448 449 450
  if not (Sid.mem pv.pv_vs.vs_name cl.cl_local) then pv
  else Mpv.find pv cl.pv_table

Andrei Paskevich's avatar
Andrei Paskevich committed
451
let cl_find_rs cl rs =
Andrei Paskevich's avatar
Andrei Paskevich committed
452 453 454
  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
455
let cl_find_xs cl xs =
Andrei Paskevich's avatar
Andrei Paskevich committed
456 457 458
  if not (Sid.mem xs.xs_name cl.cl_local) then xs
  else Mexn.find xs cl.xs_table

Andrei Paskevich's avatar
Andrei Paskevich committed
459
(*
Andrei Paskevich's avatar
Andrei Paskevich committed
460 461 462 463 464 465 466 467 468
(* initialize the clone structure *)

let cl_init_ts cl ({ts_name = id} as ts) ts' =
  if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
(* TODO: check later
  if List.length ts.ts_args <> List.length ts'.ts_args
    then raise (BadInstance (id, ts'.ts_name));
*)
  cl.ts_table <- Mts.add ts (restore_its ts') cl.ts_table
Andrei Paskevich's avatar
Andrei Paskevich committed
469
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
470

Andrei Paskevich's avatar
Andrei Paskevich committed
471 472 473 474 475 476 477 478 479 480 481 482 483 484
let cl_clone_ls inst cl ls =
  if Mls.mem ls inst.inst_ls then raise (CannotInstantiate ls.ls_name);
  let constr = ls.ls_constr in
  let id  = id_clone ls.ls_name in
  let at = List.map (cl_trans_ty cl) ls.ls_args in
  let vt = Opt.map (cl_trans_ty cl) ls.ls_value in
  let ls' = create_lsymbol ~constr id at vt in
  cl.ls_table <- Mls.add ls ls' cl.ls_table;
  ls'

let cl_add_ls cl ({ls_name = id} as ls) ({ls_name = id'} as ls') =
  let mtch sb ty ty' = try ty_match sb ty' (cl_trans_ty cl ty)
    with TypeMismatch _ -> raise (BadInstance (id, id')) in
  let sbs = match ls.ls_value,ls'.ls_value with
Andrei Paskevich's avatar
Andrei Paskevich committed
485 486
    | Some ty, Some ty' -> mtch Mtv.empty ty ty'
    | None, None -> Mtv.empty
Andrei Paskevich's avatar
Andrei Paskevich committed
487 488 489
    | _ -> raise (BadInstance (id, id')) in
  ignore (try List.fold_left2 mtch sbs ls.ls_args ls'.ls_args
    with Invalid_argument _ -> raise (BadInstance (id, id')));
Andrei Paskevich's avatar
Andrei Paskevich committed
490 491
  cl.ls_table <- Mls.add ls ls' cl.ls_table

Andrei Paskevich's avatar
Andrei Paskevich committed
492 493 494 495 496 497 498 499 500 501
let cl_found_ls inst cl uc ls =
  let nls = match Mls.find_opt ls inst.inst_ls with
    | None ->
        let ns = Theory.get_namespace uc.muc_theory in
        (try Some (ns_find_ls ns [ls.ls_name.id_string])
        with Not_found -> None)
    | nls -> nls in
  match nls with
  | Some ls' -> cl_add_ls cl ls ls'; true
  | None -> false
Andrei Paskevich's avatar
Andrei Paskevich committed
502 503 504

(* clone declarations *)

Andrei Paskevich's avatar
Andrei Paskevich committed
505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 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 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599
let clone_decl inst cl uc d = match d.d_node with
  | Dtype _ | Ddata _ -> assert false
  | Dparam ls ->
      if cl_found_ls inst cl uc ls then uc else
      let d = create_param_decl (cl_clone_ls inst cl ls) in
      add_pdecl ~vc:false uc (create_pure_decl d)
  | Dlogic ldl ->
      let get_ls (ls,_) = ignore (cl_clone_ls inst cl ls) in
      let get_logic (_,ld) =
        Opt.get (ls_defn_of_axiom (cl_trans_fmla cl (ls_defn_axiom ld))) in
      List.iter get_ls ldl;
      let d = create_logic_decl (List.map get_logic ldl) in
      add_pdecl ~vc:false uc (create_pure_decl d)
  | Dind (s, idl) ->
      let get_ls (ls,_) = cl_clone_ls inst cl ls in
      let get_case (pr,f) =
        if Spr.mem pr inst.inst_lemma || Spr.mem pr inst.inst_goal
          then raise (CannotInstantiate pr.pr_name);
        let pr' = create_prsymbol (id_clone pr.pr_name) in
        cl.pr_table <- Mpr.add pr pr' cl.pr_table;
        pr', cl_trans_fmla cl f in
      let get_ind ls (_,la) = ls, List.map get_case la in
      let lls = List.map get_ls idl in
      let d = create_ind_decl s (List.map2 get_ind lls idl) in
      add_pdecl ~vc:false uc (create_pure_decl d)
  | Dprop (k,pr,f) ->
      let k' = match k with
        | Pskip | Pgoal -> Pskip
        | Plemma when Spr.mem pr inst.inst_goal -> Pskip
        | Paxiom when Spr.mem pr inst.inst_goal -> Pgoal
        | Paxiom when Spr.mem pr inst.inst_lemma -> Plemma
        | Paxiom -> Paxiom (* TODO: Plemma *)
        | Plemma -> Paxiom in
      let pr' = create_prsymbol (id_clone pr.pr_name) in
      cl.pr_table <- Mpr.add pr pr' cl.pr_table;
      let d = create_prop_decl k' pr' (cl_trans_fmla cl f) in
      add_pdecl ~vc:false uc (create_pure_decl d)

let clone_pdecl inst cl uc d = match d.pd_node with
  | PDtype _tdl -> assert false (* TODO *)
  | PDlet _ld -> assert false (* TODO *)
  | PDexn xs ->
      let ity = cl_trans_ity cl xs.xs_ity in
      let xs' = create_xsymbol (id_clone xs.xs_name) ity in
      cl.xs_table <- Mexn.add xs xs' cl.xs_table;
      add_pdecl ~vc:false uc (create_exn_decl xs')
  | PDpure ->
      List.fold_left (clone_decl inst cl) uc d.pd_pure

let add_clone uc mi =
  (* TODO: add TDclone to the muc_theory *)
  { uc with muc_units = Uclone mi :: uc.muc_units }

let clone_export uc m inst =
  let check_local id =
    if not (Sid.mem id m.mod_local) then raise (NonLocal id) in
  Mts.iter (fun ts _ -> check_local ts.ts_name) inst.inst_ts;
  Mls.iter (fun ls _ -> check_local ls.ls_name) inst.inst_ls;
  Spr.iter (fun pr -> check_local pr.pr_name) inst.inst_goal;
  Spr.iter (fun pr -> check_local pr.pr_name) inst.inst_lemma;
  let cl = empty_clones m.mod_local in
  let rec add_unit uc u = match u with
    | Udecl d -> clone_pdecl inst cl uc d
    | Uuse m -> use_export uc m
    | Uclone mi ->
        add_clone uc { mi_mod = mi.mi_mod;
          mi_ts = Mts.map (cl_find_its cl) mi.mi_ts;
          mi_ls = Mls.map (cl_find_ls cl) mi.mi_ls;
          mi_pr = Mpr.map (cl_find_pr cl) mi.mi_pr;
          mi_pv = Mpv.map (cl_find_pv cl) mi.mi_pv;
          mi_rs = Mrs.map (cl_find_rs cl) mi.mi_rs;
          mi_xs = Mexn.map (cl_find_xs cl) mi.mi_xs}
    | Umeta (m,al) ->
        let cl_marg = function
          | MAty ty -> MAty (cl_trans_ty cl ty)
          | MAts ts -> MAts (cl_find_ts cl ts)
          | MAls ls -> MAls (cl_find_ls cl ls)
          | MApr pr -> MApr (cl_find_pr cl pr)
          | a -> a in
        add_meta uc m (List.map cl_marg al)
    | Uscope (n,import,ul) ->
        let uc = open_scope uc n in
        let uc = List.fold_left add_unit uc ul in
        close_scope ~import uc in
  let uc = List.fold_left add_unit uc m.mod_units in
  let mi = {
    mi_mod = m;
    mi_ts  = cl.ts_table;
    mi_ls  = cl.ls_table;
    mi_pr  = cl.pr_table;
    mi_pv  = cl.pv_table;
    mi_rs  = cl.rs_table;
    mi_xs  = cl.xs_table} in
  add_clone uc mi

Andrei Paskevich's avatar
Andrei Paskevich committed
600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680
(*
let cl_type cl inst ts =
  if Mts.mem ts inst.inst_ts then
    if ts.ts_def = None then raise EmptyDecl
    else raise (CannotInstantiate ts.ts_name);
  create_ty_decl (cl_find_ts cl ts)

let cl_data cl inst tdl =
  let add_ls ls =
    if Mls.mem ls inst.inst_ls then
      raise (CannotInstantiate ls.ls_name);
    cl_find_ls cl ls
  in
  let add_constr (ls,pl) =
    add_ls ls, List.map (Opt.map add_ls) pl
  in
  let add_type (ts,csl) =
    if Mts.mem ts inst.inst_ts then
      raise (CannotInstantiate ts.ts_name);
    let ts' = cl_find_ts cl ts in
    let td' = List.map add_constr csl in
    (ts',td')
  in
  create_data_decl (List.map add_type tdl)

let extract_ls_defn f =
  let vl,_,f = match f.t_node with
    | Tquant (Tforall,b) -> t_open_quant b
    | _ -> [],[],f in
  match f.t_node with
    | Tapp (_, [{t_node = Tapp (ls,_)}; f])
    | Tbinop (_, {t_node = Tapp (ls,_)}, f) -> make_ls_defn ls vl f
    | _ -> assert false

let cl_param cl inst ls =
  if Mls.mem ls inst.inst_ls then raise EmptyDecl;
  create_param_decl (cl_find_ls cl ls)

let cl_logic cl inst ldl =
  let add_logic (ls,ld) =
    if Mls.mem ls inst.inst_ls then
      raise (CannotInstantiate ls.ls_name);
    let f = ls_defn_axiom ld in
    extract_ls_defn (cl_trans_fmla cl f)
  in
  create_logic_decl (List.map add_logic ldl)

let cl_ind cl inst (s, idl) =
  let add_case (pr,f) =
    if Spr.mem pr inst.inst_lemma || Spr.mem pr inst.inst_goal
      then raise (CannotInstantiate pr.pr_name)
      else cl_find_pr cl pr, cl_trans_fmla cl f
  in
  let add_ind (ps,la) =
    if Mls.mem ps inst.inst_ls
      then raise (CannotInstantiate ps.ls_name)
      else cl_find_ls cl ps, List.map add_case la
  in
  create_ind_decl s (List.map add_ind idl)

let cl_prop cl inst (k,pr,f) =
  let k' = match k with
    | Pskip | Pgoal -> Pskip
    | Plemma when Spr.mem pr inst.inst_goal -> Pskip
    | Paxiom when Spr.mem pr inst.inst_goal -> Pgoal
    | Paxiom when Spr.mem pr inst.inst_lemma -> Plemma
    | Paxiom | Plemma -> Paxiom
  in
  let pr' = cl_find_pr cl pr in
  let f' = cl_trans_fmla cl f in
  create_prop_decl k' pr' f'

let cl_decl cl inst d = match d.d_node with
  | Dtype ts -> cl_type cl inst ts
  | Ddata tdl -> cl_data cl inst tdl
  | Dparam ls -> cl_param cl inst ls
  | Dlogic ldl -> cl_logic cl inst ldl
  | Dind idl -> cl_ind cl inst idl
  | Dprop p -> cl_prop cl inst p
*)

681 682
(** {2 WhyML language} *)

683
type mlw_file = pmodule Mstr.t
684

685 686 687 688 689 690 691 692
let convert mm =
  let convert m = m.mod_theory in
  if Mstr.is_empty mm then Mstr.empty else
  match (snd (Mstr.choose mm)).mod_theory.th_path with
  | "why3" :: path ->
      begin try Env.base_language_builtin path
      with Not_found -> Mstr.map convert mm end
  | _ -> Mstr.map convert mm
693 694 695

let mlw_language = Env.register_language Env.base_language convert

696 697 698 699 700 701 702
module Hpath = Exthtbl.Make(struct
  type t = Env.pathname
  let hash = Hashtbl.hash
  let equal = (=)
end)

let mlw_language_builtin =
703 704 705 706 707 708 709 710
  let builtin s =
    if s = unit_module.mod_theory.th_name.id_string then unit_module else
    if s = builtin_theory.th_name.id_string then builtin_module else
    if s = highord_theory.th_name.id_string then highord_module else
    if s = bool_theory.th_name.id_string then bool_module else
    match tuple_theory_name s with
    | Some n -> tuple_module n
    | None -> raise Not_found in
711
  Hpath.memo 7 (function
712 713
    | [s] -> Mstr.singleton s (builtin s)
    | _   -> raise Not_found)
714

715 716
let () = Env.add_builtin mlw_language mlw_language_builtin

717 718 719 720
exception ModuleNotFound of Env.pathname * string

let read_module env path s =
  let path = if path = [] then ["why3"; s] else path in
721
  let mm = Env.read_library mlw_language env path in
722 723
  Mstr.find_exn (ModuleNotFound (path,s)) s mm

Andrei Paskevich's avatar
Andrei Paskevich committed
724 725
(* pretty-printing *)

726 727 728
let print_path fmt sl =
  Pp.print_list (Pp.constant_string ".") Format.pp_print_string fmt sl

Andrei Paskevich's avatar
Andrei Paskevich committed
729 730 731 732 733 734 735 736 737
let print_mname fmt {mod_theory = th} =
  List.iter (fun s ->
    Format.pp_print_string fmt s;
    Format.pp_print_char fmt '.') th.th_path;
  Format.pp_print_string fmt th.th_name.id_string

let rec print_unit fmt = function
  | Udecl d -> Pdecl.print_pdecl fmt d
  | Uuse m -> Format.fprintf fmt "use export %a" print_mname m
Andrei Paskevich's avatar
Andrei Paskevich committed
738
  | Uclone mi -> Format.fprintf fmt "clone export %a with ..."
Andrei Paskevich's avatar
Andrei Paskevich committed
739 740 741 742 743 744
      print_mname mi.mi_mod
  | Umeta (m,al) -> Format.fprintf fmt "@[<hov 2>meta %s %a@]"
      m.meta_name (Pp.print_list Pp.comma Pretty.print_meta_arg) al
  | Uscope (s,i,[Uuse m]) -> Format.fprintf fmt "use%s %a%s"
      (if i then " import" else "") print_mname m
      (if s = m.mod_theory.th_name.id_string then "" else " as " ^ s)
Andrei Paskevich's avatar
Andrei Paskevich committed
745
  | Uscope (s,i,[Uclone mi]) -> Format.fprintf fmt "clone%s %a%s with ..."
Andrei Paskevich's avatar
Andrei Paskevich committed
746 747 748 749 750 751 752 753 754
      (if i then " import" else "") print_mname mi.mi_mod
      (if s = mi.mi_mod.mod_theory.th_name.id_string then "" else " as " ^ s)
  | Uscope (s,i,ul) -> Format.fprintf fmt "@[<hov 2>scope%s %s@\n%a@]@\nend"
      (if i then " import" else "") s (Pp.print_list Pp.newline2 print_unit) ul

let print_module fmt m = Format.fprintf fmt
  "@[<hov 2>module %s@\n%a@]@\nend" m.mod_theory.th_name.id_string
  (Pp.print_list Pp.newline2 print_unit) m.mod_units

755 756 757 758
let () = Exn_printer.register (fun fmt e -> match e with
  | ModuleNotFound (sl,s) -> Format.fprintf fmt
      "Module %s not found in library %a" s print_path sl
  | _ -> raise e)