mlw_typing.ml 28.9 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Util
23
open Ident
24 25 26
open Ty
open Term
open Decl
27 28 29
open Theory
open Env
open Ptree
30
open Mlw_dtree
31
open Mlw_ty
32
open Mlw_ty.T
33 34
open Mlw_expr
open Mlw_decl
35
open Mlw_module
36
open Mlw_dty
37

38 39
(** errors *)

40
exception DuplicateProgVar of string
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
exception DuplicateTypeVar of string
(*
exception PredicateExpected
exception TermExpected
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
exception ClashTheory of string
exception UnboundTheory of qualid
exception UnboundType of string list
*)
exception UnboundTypeVar of string
exception UnboundSymbol of string list

let error = Loc.error
let errorm = Loc.errorm

let rec print_qualid fmt = function
  | Qident s -> Format.fprintf fmt "%s" s.id
  | Qdot (m, s) -> Format.fprintf fmt "%a.%s" print_qualid m s.id

let () = Exn_printer.register (fun fmt e -> match e with
  | DuplicateTypeVar s ->
63 64 65
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
(*
  | PredicateExpected ->
      Format.fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      Format.fprintf fmt "syntax error: term expected"
  | FSymExpected ls ->
      Format.fprintf fmt "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls ->
      Format.fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls
  | ClashTheory s ->
      Format.fprintf fmt "Clash with previous theory %s" s
  | UnboundTheory q ->
      Format.fprintf fmt "unbound theory %a" print_qualid q
  | UnboundType sl ->
      Format.fprintf fmt "Unbound type '%a'"
        (Pp.print_list Pp.dot Pp.pp_print_string) sl
*)
  | UnboundTypeVar s ->
      Format.fprintf fmt "unbound type variable '%s" s
  | UnboundSymbol sl ->
      Format.fprintf fmt "Unbound symbol '%a'"
        (Pp.print_list Pp.dot Format.pp_print_string) sl
  | _ -> raise e)

(* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)

92 93 94 95 96 97
type denv = {
  uc     : module_uc;
  locals : (tvars * dity) Mstr.t;
  tvars  : tvars;
  denv   : Typing.denv; (* for user type variables only *)
}
98

99 100 101 102 103
let create_denv uc =
  { uc = uc;
    locals = Mstr.empty;
    tvars = empty_tvars;
    denv = Typing.create_denv (); }
104

105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
(** Typing type expressions *)

let rec dity_of_pty ~user denv = function
  | Ptree.PPTtyvar id ->
      create_user_type_variable id
  | Ptree.PPTtyapp (pl, p) ->
      let dl = List.map (dity_of_pty ~user denv) pl in
      let x = Typing.string_list_of_qualid [] p in
      begin
        try
          let its = ns_find_it (get_namespace denv.uc) x in
          its_app ~user its dl
        with Not_found -> try
          let ts = ns_find_ts (Theory.get_namespace (get_theory denv.uc)) x in
          ts_app ts dl
        with Not_found ->
          let loc = Typing.qloc p in
          errorm ~loc "unbound symbol %a" Typing.print_qualid p
      end
  | Ptree.PPTtuple pl ->
      ts_app (ts_tuple (List.length pl)) (List.map (dity_of_pty ~user denv) pl)
126 127 128 129 130 131 132 133 134 135 136

(** Typing program expressions *)

let rec extract_labels labs loc e = match e.Ptree.expr_desc with
  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (s :: labs) loc e
  | Ptree.Enamed (Ptree.Lpos p, e) -> extract_labels labs (Some p) e
  | Ptree.Ecast  (e, ty) ->
      let labs, loc, d = extract_labels labs loc e in
      labs, loc, Ptree.Ecast ({ e with Ptree.expr_desc = d }, ty)
  | e -> List.rev labs, loc, e

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
137 138 139 140 141
let unify_args args dity =
  let a = create_type_variable () in
  let dity' = make_arrow_type (List.map (fun a -> a.dexpr_type) args) a in
  unify dity dity';
  a
142

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
143
(*
144 145 146 147 148 149 150 151 152 153 154 155
let unify_args_prg ~loc prg args el = match prg with
  | PV { pv_vs = vs } ->
      errorm ~loc "%s: not a function" vs.vs_name.id_string
  | PL pl ->
      unify_args pl.pl_ls args el; []
  | PA { pa_name = id } | PS { ps_name = id } ->
      let rec unify_list = function
        | a :: args, e :: el -> unify_arg a e; unify_list (args, el)
        | args, [] -> args
        | [], _ :: _ -> errorm ~loc "too many arguments for %s" id.id_string
      in
      unify_list (args, el)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
156
*)
157 158 159 160

let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
161 162 163 164 165 166

(* value restriction *)
let rec is_fun e = match e.dexpr_desc with
  | DEfun _ -> true
  | DEmark (_, e) -> is_fun e
  | _ -> false
167

168 169 170 171 172 173 174 175 176 177
let rec dexpr ~userloc denv e =
  let loc = e.Ptree.expr_loc in
  let labs, userloc, d = extract_labels [] userloc e in
  let d, ty = dexpr_desc ~userloc denv loc d in
  let loc = def_option loc userloc in
  let e = {
    dexpr_desc = d; dexpr_loc = loc; dexpr_lab = labs; dexpr_type = ty; }
  in
  e

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
178
and dexpr_desc ~userloc denv loc = function
179 180
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
      (* local variable *)
181 182 183
      let tvs, dity = Mstr.find x denv.locals in
      let dity = specialize_scheme tvs dity in
      DElocal x, dity
184 185 186 187 188
  | Ptree.Eident p ->
      let x = Typing.string_list_of_qualid [] p in
      begin
        try
          let prg = ns_find_ps (get_namespace denv.uc) x in
189 190 191
          begin match prg with
            | PV pv -> DEglobal_pv pv, specialize_pvsymbol pv
            | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
192
            | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
193
          end
194 195
        with Not_found -> try
          let ls = ns_find_ls (Theory.get_namespace (get_theory denv.uc)) x in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
196
          DEglobal_ls ls, specialize_lsymbol ls
197 198 199 200 201 202 203
        with Not_found ->
          errorm ~loc "unbound symbol %a" Typing.print_qualid p
      end
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
      let e = dexpr ~userloc denv e in
      let el = List.map (dexpr ~userloc denv) el in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
204 205
      let res = unify_args el e.dexpr_type in
      DEapply (e, el), res
206 207 208 209 210 211 212 213 214
  | Ptree.Elet (id, e1, e2) ->
      let e1 = dexpr ~userloc denv e1 in
      let tvars =
        if is_fun e1 then denv.tvars else add_tvars denv.tvars e1.dexpr_type in
      let s = tvars, e1.dexpr_type in
      let denv =
        { denv with locals = Mstr.add id.id s denv.locals; tvars = tvars } in
      let e2 = dexpr ~userloc denv e2 in
      DElet (id, e1, e2), e2.dexpr_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232
  | Ptree.Efun (bl, tr) ->
      let dbinder denv (id, pty) =
        let dity = match pty with
          | Some pty -> dity_of_pty ~user:false denv pty
          | None -> create_type_variable ()
        in
        let tvars = add_tvars denv.tvars dity in
        let denv = { denv with
          locals = Mstr.add id.id (tvars, dity) denv.locals;
          tvars = tvars }
        in
        denv, (id, false, dity)
      in
      let denv, bl = Util.map_fold_left dbinder denv bl in
      let _,e,_ as tr = dtriple ~userloc denv tr in
      let dity =
        make_arrow_type (List.map (fun (_,_,d) -> d) bl) e.dexpr_type in
      DEfun (bl, tr), dity
233 234 235 236 237 238
  | Ptree.Ecast (e1, pty) ->
      let e1 = dexpr ~userloc denv e1 in
      unify e1.dexpr_type (dity_of_pty ~user:false denv pty);
      e1.dexpr_desc, e1.dexpr_type
  | Ptree.Enamed _ ->
      assert false
239 240 241
  | _ ->
      assert false (*TODO*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
242 243 244 245 246 247 248 249
and dtriple ~userloc denv (p, e, q) =
  let e = dexpr ~userloc denv e in
  let q = dpost denv q in
  p, e, q

and dpost _denv (q, _ql) =
  q, [] (* TODO *)

250
let id_user x = id_user x.id x.id_loc
251

252
let rec expr locals de = match de.dexpr_desc with
253 254 255
  | DElocal x ->
      assert (Mstr.mem x locals);
      begin match Mstr.find x locals with
256 257
      | LetV pv -> e_value pv
      | LetA ps -> e_cast ps (vty_of_dity de.dexpr_type)
258
      end
259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
  | DElet (x, { dexpr_desc = DEfun (bl, tr) }, de2) ->
      let def1 = expr_fun locals x bl tr in
      let locals = Mstr.add x.id (LetA def1.rec_ps) locals in
      let e2 = expr locals de2 in
      e_rec [def1] e2
  | DEfun (bl, tr) ->
      let x = { id = "fun"; id_loc = de.dexpr_loc; id_lab = [] } in
      let def = expr_fun locals x bl tr in
      let e2 = e_cast def.rec_ps (VTarrow def.rec_ps.ps_vta) in
      e_rec [def] e2
  | DElet (x, de1, de2) ->
      let e1 = expr locals de1 in
      let def1 = create_let_defn (id_user x) e1 in
      let locals = Mstr.add x.id def1.let_var locals in
      let e2 = expr locals de2 in
      e_let def1 e2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
275
  | DEapply (de1, del) ->
276
      let e1 = expr locals de1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
277 278 279 280 281 282
      let el = List.map (expr locals) del in
      begin match de1.dexpr_desc with
        | DEglobal_pl pls -> e_plapp pls el (ity_of_dity de.dexpr_type)
        | DEglobal_ls ls  -> e_lapp  ls  el (ity_of_dity de.dexpr_type)
        | _               -> e_app e1 el
      end
283 284 285 286
  | DEglobal_pv pv ->
      e_value pv
  | DEglobal_ps ps ->
      e_cast ps (vty_of_dity de.dexpr_type)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
287 288 289 290
  | DEglobal_pl pls ->
      e_plapp pls [] (ity_of_dity de.dexpr_type)
  | DEglobal_ls ls ->
      e_lapp ls [] (ity_of_dity de.dexpr_type)
291 292 293
  | _ ->
      assert false (*TODO*)

294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315
and expr_fun locals x bl (_, e1, _) =
  let binder (id, ghost, dity) =
    let vtv = vty_value ~ghost (ity_of_dity dity) in
    create_pvsymbol (id_user id) vtv in
  let pvl = List.map binder bl in
  let add_binder pv = Mstr.add pv.pv_vs.vs_name.id_string (LetV pv) in
  let locals' = List.fold_right add_binder pvl locals in
  let e1 = expr locals' e1 in
  let ty1 = match e1.e_vty with
    | VTarrow _ -> ty_tuple []
    | VTvalue vtv -> ty_of_ity vtv.vtv_ity in
  let res1 = create_vsymbol (id_fresh "result") ty1 in
  let lam = {
    l_args = pvl;
    l_variant = [];
    l_pre = t_true;                   (* TODO *)
    l_expr = e1;
    l_post = create_post res1 t_true; (* TODO *)
    l_xpost = Mexn.empty;             (* TODO *)
      } in
  create_fun_defn (id_user x) lam

316 317
(** Type declaration *)

318
type tys = ProgTS of itysymbol | PureTS of tysymbol
319 320 321 322 323 324 325 326 327

let find_tysymbol q uc =
  let loc = Typing.qloc q in
  let sl = Typing.string_list_of_qualid [] q in
  try ProgTS (ns_find_it (get_namespace uc) sl)
  with Not_found ->
  try PureTS (ns_find_ts (Theory.get_namespace (get_theory uc)) sl)
  with Not_found -> error ~loc (UnboundSymbol sl)

328 329 330
let look_for_loc tdl s =
  let look_id loc id = if id.id = s then Some id.id_loc else loc in
  let look_pj loc (id,_) = option_fold look_id loc id in
331 332 333
  let look_cs loc (csloc,id,pjl) =
    let loc = if id.id = s then Some csloc else loc in
    List.fold_left look_pj loc pjl in
334 335 336 337 338 339 340 341 342 343
  let look_fl loc f = look_id loc f.f_ident in
  let look loc d =
    let loc = look_id loc d.td_ident in
    match d.td_def with
      | TDabstract | TDalias _ -> loc
      | TDalgebraic csl -> List.fold_left look_cs loc csl
      | TDrecord fl -> List.fold_left look_fl loc fl
  in
  List.fold_left look None tdl

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 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415
let add_types uc tdl =
  let add m d =
    let id = d.td_ident.id in
    Mstr.add_new (Loc.Located (d.td_loc, ClashSymbol id)) id d m in
  let def = List.fold_left add Mstr.empty tdl in

  (* detect cycles *)

  let rec cyc_visit x d seen = match Mstr.find_opt x seen with
    | Some true -> seen
    | Some false -> errorm ~loc:d.td_loc "Cyclic type definition"
    | None ->
        let ts_seen seen = function
          | Qident { id = x } ->
              begin try cyc_visit x (Mstr.find x def) seen
              with Not_found -> seen end
          | _ -> seen in
        let rec check seen = function
          | PPTtyvar _ -> seen
          | PPTtyapp (tyl,q) -> List.fold_left check (ts_seen seen q) tyl
          | PPTtuple tyl -> List.fold_left check seen tyl in
        let seen = match d.td_def with
          | TDabstract | TDalgebraic _ | TDrecord _ -> seen
          | TDalias ty -> check (Mstr.add x false seen) ty in
        Mstr.add x true seen in
  ignore (Mstr.fold cyc_visit def Mstr.empty);

  (* detect mutable types *)

  let mutables = Hashtbl.create 5 in
  let rec mut_visit x =
    try Hashtbl.find mutables x
    with Not_found ->
      let ts_mut = function
        | Qident { id = x } when Mstr.mem x def -> mut_visit x
        | q ->
            begin match find_tysymbol q uc with
              | ProgTS s -> s.its_regs <> []
              | PureTS _ -> false end in
      let rec check = function
        | PPTtyvar _ -> false
        | PPTtyapp (tyl,q) -> ts_mut q || List.exists check tyl
        | PPTtuple tyl -> List.exists check tyl in
      Hashtbl.replace mutables x false;
      let mut = match (Mstr.find x def).td_def with
        | TDabstract -> false
        | TDalias ty -> check ty
        | TDalgebraic csl ->
            let proj (_,pty) = check pty in
            List.exists (fun (_,_,l) -> List.exists proj l) csl
        | TDrecord fl ->
            let field f = f.f_mutable || check f.f_pty in
            List.exists field fl in
      Hashtbl.replace mutables x mut;
      mut
  in
  Mstr.iter (fun x _ -> ignore (mut_visit x)) def;

  (* create type symbols and predefinitions for mutable types *)

  let tysymbols = Hashtbl.create 5 in
  let predefs = Hashtbl.create 5 in
  let rec its_visit x =
    try match Hashtbl.find tysymbols x with
      | Some ts -> ts
      | None ->
          let loc = (Mstr.find x def).td_loc in
          errorm ~loc "Mutable type in a recursive type definition"
    with Not_found ->
      let d = Mstr.find x def in
      let add_tv acc id =
        let e = Loc.Located (id.id_loc, DuplicateTypeVar id.id) in
416
        let tv = create_tvsymbol (Denv.create_user_id id) in
417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438
        Mstr.add_new e id.id tv acc in
      let vars = List.fold_left add_tv Mstr.empty d.td_params in
      let vl = List.map (fun id -> Mstr.find id.id vars) d.td_params in
      let id = Denv.create_user_id d.td_ident in
      let abst = d.td_vis = Abstract in
      let priv = d.td_vis = Private in
      Hashtbl.add tysymbols x None;
      let get_ts = function
        | Qident { id = x } when Mstr.mem x def -> ProgTS (its_visit x)
        | q -> find_tysymbol q uc
      in
      let rec parse = function
        | PPTtyvar { id = v ; id_loc = loc } ->
            let e = Loc.Located (loc, UnboundTypeVar v) in
            ity_var (Mstr.find_exn e v vars)
        | PPTtyapp (tyl,q) ->
            let tyl = List.map parse tyl in
            begin match get_ts q with
              | PureTS ts -> Loc.try2 (Typing.qloc q) ity_pur ts tyl
              | ProgTS ts -> Loc.try2 (Typing.qloc q) ity_app_fresh ts tyl
            end
        | PPTtuple tyl ->
439
            let ts = ts_tuple (List.length tyl) in
440 441 442 443 444
            ity_pur ts (List.map parse tyl)
      in
      let ts = match d.td_def with
        | TDalias ty ->
            let def = parse ty in
445 446
            let rl = Sreg.elements def.ity_vars.vars_reg in
            create_itysymbol id ~abst ~priv vl rl (Some def)
447
        | TDalgebraic csl when Hashtbl.find mutables x ->
448 449 450 451 452 453
            let projs = Hashtbl.create 5 in
            (* to check projections' types we must fix the tyvars *)
            let add s v = let t = ity_var v in ity_match s t t in
            let sbs = List.fold_left add ity_subst_empty vl in
            let mk_proj s (id,pty) =
              let ity = parse pty in
454
              let vtv = vty_value ity in
455 456
              match id with
                | None ->
457
                    let pv = create_pvsymbol (id_fresh "pj") vtv in
458
                    Sreg.union s ity.ity_vars.vars_reg, (pv, false)
459 460 461
                | Some id ->
                    try
                      let pv = Hashtbl.find projs id.id in
462
                      let ty = pv.pv_vtv.vtv_ity in
463 464
                      (* once we have ghost/mutable fields in algebraics,
                         don't forget to check here that they coincide, too *)
465
                      ignore (Loc.try3 id.id_loc ity_match sbs ty ity);
466 467
                      s, (pv, true)
                    with Not_found ->
468
                      let pv = create_pvsymbol (Denv.create_user_id id) vtv in
469
                      Hashtbl.replace projs id.id pv;
470
                      Sreg.union s ity.ity_vars.vars_reg, (pv, true)
471 472 473 474 475 476
            in
            let mk_constr s (_loc,cid,pjl) =
              let s,pjl = Util.map_fold_left mk_proj s pjl in
              s, (Denv.create_user_id cid, pjl)
            in
            let s,def = Util.map_fold_left mk_constr Sreg.empty csl in
477
            Hashtbl.replace predefs x def;
478
            create_itysymbol id ~abst ~priv vl (Sreg.elements s) None
479
        | TDrecord fl when Hashtbl.find mutables x ->
480 481 482 483 484
            let mk_field s f =
              let ghost = f.f_ghost in
              let ity = parse f.f_pty in
              let fid = Denv.create_user_id f.f_ident in
              let s,mut = if f.f_mutable then
485
                let r = create_region fid ity in
486 487
                Sreg.add r s, Some r
              else
488
                Sreg.union s ity.ity_vars.vars_reg, None
489
              in
490 491
              let vtv = vty_value ?mut ~ghost ity in
              s, (create_pvsymbol fid vtv, true)
492 493 494
            in
            let s,pjl = Util.map_fold_left mk_field Sreg.empty fl in
            let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in
495
            Hashtbl.replace predefs x [Denv.create_user_id cid, pjl];
496 497 498 499 500 501 502 503 504 505 506
            create_itysymbol id ~abst ~priv vl (Sreg.elements s) None
        | TDalgebraic _ | TDrecord _ | TDabstract ->
            create_itysymbol id ~abst ~priv vl [] None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
  Mstr.iter (fun x _ -> ignore (its_visit x)) def;

  (* create predefinitions for immutable types *)

507
  let def_visit d (abstr,algeb,alias) =
508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527
    let x = d.td_ident.id in
    let ts = Util.of_option (Hashtbl.find tysymbols x) in
    let add_tv s x v = Mstr.add x.id v s in
    let vars = List.fold_left2 add_tv Mstr.empty d.td_params ts.its_args in
    let get_ts = function
      | Qident { id = x } when Mstr.mem x def ->
          ProgTS (Util.of_option (Hashtbl.find tysymbols x))
      | q -> find_tysymbol q uc
    in
    let rec parse = function
      | PPTtyvar { id = v ; id_loc = loc } ->
          let e = Loc.Located (loc, UnboundTypeVar v) in
          ity_var (Mstr.find_exn e v vars)
      | PPTtyapp (tyl,q) ->
          let tyl = List.map parse tyl in
          begin match get_ts q with
            | PureTS ts -> Loc.try2 (Typing.qloc q) ity_pur ts tyl
            | ProgTS ts -> Loc.try3 (Typing.qloc q) ity_app ts tyl []
          end
      | PPTtuple tyl ->
528
          let ts = ts_tuple (List.length tyl) in
529 530 531
          ity_pur ts (List.map parse tyl)
    in
    match d.td_def with
532 533 534 535
      | TDabstract ->
          ts :: abstr, algeb, alias
      | TDalias _ ->
          abstr, algeb, ts :: alias
536
      | (TDalgebraic _ | TDrecord _) when Hashtbl.find mutables x ->
537
          abstr, (ts, Hashtbl.find predefs x) :: algeb, alias
538 539 540 541
      | TDalgebraic csl ->
          let projs = Hashtbl.create 5 in
          let mk_proj (id,pty) =
            let ity = parse pty in
542
            let vtv = vty_value ity in
543 544
            match id with
              | None ->
545
                  create_pvsymbol (id_fresh "pj") vtv, false
546 547 548
              | Some id ->
                  try
                    let pv = Hashtbl.find projs id.id in
549
                    let ty = pv.pv_vtv.vtv_ity in
550 551
                    (* once we have ghost/mutable fields in algebraics,
                       don't forget to check here that they coincide, too *)
552
                    Loc.try2 id.id_loc ity_equal_check ty ity;
553 554
                    pv, true
                  with Not_found ->
555
                    let pv = create_pvsymbol (Denv.create_user_id id) vtv in
556 557 558 559 560
                    Hashtbl.replace projs id.id pv;
                    pv, true
          in
          let mk_constr (_loc,cid,pjl) =
            Denv.create_user_id cid, List.map mk_proj pjl in
561
          abstr, (ts, List.map mk_constr csl) :: algeb, alias
562 563 564
      | TDrecord fl ->
          let mk_field f =
            let fid = Denv.create_user_id f.f_ident in
565 566
            let vtv = vty_value ~ghost:f.f_ghost (parse f.f_pty) in
            create_pvsymbol fid vtv, true in
567
          let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in
568 569
          let csl = [Denv.create_user_id cid, List.map mk_field fl] in
          abstr, (ts, csl) :: algeb, alias
570
  in
571
  let abstr,algeb,alias = List.fold_right def_visit tdl ([],[],[]) in
572 573

  (* detect pure type declarations *)
574

575 576 577
  let kn = get_known uc in
  let check its = Mid.mem its.its_pure.ts_name kn in
  let check ity = ity_s_any check Util.ffalse ity in
578
  let is_impure_type ts =
579
    ts.its_abst || ts.its_priv || ts.its_regs <> [] ||
580
    option_apply false check ts.its_def
581
  in
582
  let check (pv,_) =
583
    let vtv = pv.pv_vtv in
584
    vtv.vtv_ghost || vtv.vtv_mut <> None || check vtv.vtv_ity in
585 586 587
  let is_impure_data (ts,csl) =
    is_impure_type ts ||
    List.exists (fun (_,l) -> List.exists check l) csl
588
  in
589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610
  let mk_pure_decl (ts,csl) =
    let pjt = Hvs.create 3 in
    let ty = ty_app ts.its_pure (List.map ty_var ts.its_args) in
    let mk_proj (pv,f) =
      let vs = pv.pv_vs in
      if f then try vs.vs_ty, Some (Hvs.find pjt vs) with Not_found ->
        let pj = create_fsymbol (id_clone vs.vs_name) [ty] vs.vs_ty in
        Hvs.replace pjt vs pj;
        vs.vs_ty, Some pj
      else
        vs.vs_ty, None
    in
    let mk_constr (id,pjl) =
      let pjl = List.map mk_proj pjl in
      let cs = create_fsymbol id (List.map fst pjl) ty in
      cs, List.map snd pjl
    in
    ts.its_pure, List.map mk_constr csl
  in
  let add_type_decl uc ts =
    if is_impure_type ts then
      add_pdecl_with_tuples uc (create_ty_decl ts)
611
    else
612 613 614 615 616 617 618 619 620 621 622 623 624
      add_decl_with_tuples uc (Decl.create_ty_decl ts.its_pure)
  in
  try
    let uc = List.fold_left add_type_decl uc abstr in
    let uc = if algeb = [] then uc else
      if List.exists is_impure_data algeb then
        add_pdecl_with_tuples uc (create_data_decl algeb)
      else
        let d = List.map mk_pure_decl algeb in
        add_decl_with_tuples uc (Decl.create_data_decl d)
    in
    let uc = List.fold_left add_type_decl uc alias in
    uc
625
  with
626 627 628 629 630 631 632 633 634
    | ClashSymbol s ->
        error ?loc:(look_for_loc tdl s) (ClashSymbol s)
    | RecordFieldMissing ({ ls_name = { id_string = s }} as cs,ls) ->
        error ?loc:(look_for_loc tdl s) (RecordFieldMissing (cs,ls))
    | DuplicateRecordField ({ ls_name = { id_string = s }} as cs,ls) ->
        error ?loc:(look_for_loc tdl s) (DuplicateRecordField (cs,ls))
    | DuplicateVar { vs_name = { id_string = s }} ->
        errorm ?loc:(look_for_loc tdl s)
          "Field %s is used twice in the same constructor" s
635 636 637

(** Use/Clone of theories and modules *)

638 639 640 641
type mlw_contents = modul Mstr.t
type mlw_library = mlw_contents library
type mlw_file = mlw_contents * Theory.theory Mstr.t

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
let find_theory loc lib path s =
  (* search first in .mlw files (using lib) *)
  let thm =
    try Some (Env.read_lib_theory lib path s)
    with LibFileNotFound _ | TheoryNotFound _ -> None
  in
  (* search also in .why files *)
  let th =
    try Some (Env.find_theory (Env.env_of_library lib) path s)
    with LibFileNotFound _ | TheoryNotFound _ -> None
  in
  match thm, th with
    | Some _, Some _ ->
        Loc.errorm ~loc
          "a module/theory %s is defined both in Why and WhyML libraries" s
    | None, None -> Loc.error ~loc (Env.TheoryNotFound (path, s))
    | None, Some t | Some t, None -> t

let find_theory loc lib mt path s = match path with
  | [] -> (* local theory *)
      begin try Mstr.find s mt with Not_found -> find_theory loc lib [] s end
  | _ :: _ -> (* theory in file path *)
      find_theory loc lib path s

type theory_or_module = Theory of Theory.theory | Module of modul

668 669 670
let print_path fmt sl =
  Pp.print_list (Pp.constant_string ".") Format.pp_print_string fmt sl

671 672 673 674 675
let find_module loc lib path s =
  (* search first in .mlw files *)
  let m, thm =
    try
      let mm, mt = Env.read_lib_file lib path in
676
      Mstr.find_opt s mm, Mstr.find_opt s mt
677 678 679 680 681 682 683 684 685 686 687 688 689
    with
      | LibFileNotFound _ -> None, None
  in
  (* search also in .why files *)
  let th =
    try Some (Env.find_theory (Env.env_of_library lib) path s)
    with LibFileNotFound _ | TheoryNotFound _ -> None
  in
  match m, thm, th with
    | Some _, None, _ -> assert false
    | _, Some _, Some _ ->
        Loc.errorm ~loc
          "a module/theory %s is defined both in Why and WhyML libraries" s
690 691
    | None, None, None ->
        Loc.errorm ~loc "Theory/module not found: %a" print_path (path @ [s])
692 693 694
    | Some m, Some _, None -> Module m
    | None, Some t, None | None, None, Some t -> Theory t

695
let find_module loc lib mm mt path s = match path with
696 697 698 699 700 701 702
  | [] -> (* local module/theory *)
      begin try Module (Mstr.find s mm)
        with Not_found -> begin try Theory (Mstr.find s mt)
          with Not_found -> find_module loc lib [] s end end
  | _ :: _ -> (* module/theory in file path *)
      find_module loc lib path s

703 704
(** Main loop *)

705
let add_theory lib path mt m =
706 707
  let { id = id; id_loc = loc } = m.pth_name in
  if Mstr.mem id mt then Loc.errorm ~loc "clash with previous theory %s" id;
708
  let uc = create_theory ~path (Denv.create_user_id m.pth_name) in
709
  let rec add_decl uc = function
710 711
    | Dlogic d ->
        Typing.add_decl uc d
712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729
    | Duseclone (loc, use, inst) ->
        let path, s = Typing.split_qualid use.use_theory in
        let th = find_theory loc lib mt path s in
        (* open namespace, if any *)
        let uc =
          if use.use_imp_exp <> None then Theory.open_namespace uc else uc in
        (* use or clone *)
        let uc = match inst with
          | None -> Theory.use_export uc th
          | Some inst ->
              let inst = Typing.type_inst uc th inst in
              Theory.clone_export uc th inst
        in
        (* close namespace, if any *)
        begin match use.use_imp_exp with
          | None -> uc
          | Some imp -> Theory.close_namespace uc imp use.use_as
        end
730 731 732
    | Dnamespace (loc, name, import, dl) ->
        let uc = Theory.open_namespace uc in
        let uc = List.fold_left add_decl uc dl in
733
        Loc.try3 loc Theory.close_namespace uc import name
734 735 736 737
    | Dlet _ | Dletrec _ | Dparam _ | Dexn _ | Duse _ ->
        assert false
  in
  let uc = List.fold_left add_decl uc m.pth_decl in
738
  let th = close_theory uc in
739 740 741 742 743 744 745 746
  Mstr.add id th mt

let add_module lib path mm mt m =
  let { id = id; id_loc = loc } = m.mod_name in
  if Mstr.mem id mm then Loc.errorm ~loc "clash with previous module %s" id;
  if Mstr.mem id mt then Loc.errorm ~loc "clash with previous theory %s" id;
  let uc = create_module ~path (Denv.create_user_id m.mod_name) in
  let rec add_decl uc = function
747 748 749 750
    | Dlogic (TypeDecl tdl) ->
        add_types uc tdl
    | Dlogic d ->
        add_to_theory Typing.add_decl uc d
751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775
    | Duseclone (loc, use, inst) ->
        let path, s = Typing.split_qualid use.use_theory in
        let mth = find_module loc lib mm mt path s in
        (* open namespace, if any *)
        let uc = if use.use_imp_exp <> None then open_namespace uc else uc in
        (* use or clone *)
        let uc = match mth, inst with
          | Theory th, None -> use_export_theory uc th
          | Theory th, Some inst ->
              let inst = Typing.type_inst (get_theory uc) th inst in
              clone_export_theory uc th inst
          | Module m, None -> use_export uc m
          | Module m, Some inst ->
              let inst = Typing.type_inst (get_theory uc) m.mod_theory inst in
              clone_export uc m inst
        in
        (* close namespace, if any *)
        begin match use.use_imp_exp with
          | None -> uc
          | Some imp -> close_namespace uc imp use.use_as
        end
    | Dnamespace (loc, name, import, dl) ->
        let uc = open_namespace uc in
        let uc = List.fold_left add_decl uc dl in
        Loc.try3 loc close_namespace uc import name
776 777
    | Dlet (_id, e) ->
        let e = dexpr ~userloc:None (create_denv uc) e in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
778 779
        let e = expr Mstr.empty e in
        Format.eprintf "%a@." Mlw_pretty.print_expr e;
780 781 782 783 784
        uc
    | Dletrec _ | Dparam _ | Dexn _ ->
        assert false (* TODO *)
    | Duse _ ->
        assert false (*TO BE REMOVED EVENTUALLY *)
785 786 787 788
  in
  let uc = List.fold_left add_decl uc m.mod_decl in
  let m = close_module uc in
  Mstr.add id m mm, Mstr.add id m.mod_theory mt
789 790 791

let add_theory_module lib path (mm, mt) = function
  | Ptheory th -> mm, add_theory lib path mt th
792
  | Pmodule m -> add_module lib path mm mt m
793