mlw_typing.ml 40.6 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_pretty
36
open Mlw_module
37
open Mlw_dty
38

39 40
(** errors *)

41
exception DuplicateProgVar of string
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
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 ->
64 65 66
      Format.fprintf fmt "Type parameter %s is used twice" s
  | DuplicateProgVar s ->
      Format.fprintf fmt "Parameter %s is used twice" s
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 92
(*
  | 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 *)

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

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

107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
(** 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)
128 129 130

(** Typing program expressions *)

131 132
let dity_int  = ts_app ts_int []
let dity_real = ts_app ts_real []
133
let dity_bool = ts_app ts_bool []
134
let dity_unit = ts_app (ts_tuple 0) []
135 136 137 138

let expected_type e dity =
  unify e.dexpr_type dity

139 140 141 142 143 144 145 146
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

147 148 149
let rec decompose_app args e = match e.Ptree.expr_desc with
  | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
  | _ -> e, args
150

151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
(* record parsing *)

let parse_record uc fll =
  let pl = match fll with
    | [] -> raise EmptyRecord
    | (pl,_)::_ -> pl in
  let its = match pl.pl_args with
    | [{ vtv_ity = { ity_node = Ityapp (its,_,_) }}] -> its
    | _ -> raise (BadRecordField pl.pl_ls) in
  let cs, pjl = match find_constructors (get_known uc) its with
    | [cs,pjl] -> cs, List.map (exn_option (BadRecordField pl.pl_ls)) pjl
    | _ -> raise (BadRecordField pl.pl_ls) in
  let pjs = List.fold_left (fun s pj -> Sls.add pj.pl_ls s) Sls.empty pjl in
  let flm = List.fold_left (fun m (pj,v) -> let pj = pj.pl_ls in
    if not (Sls.mem pj pjs) then raise (BadRecordField pj) else
      Mls.add_new (DuplicateRecordField (cs.pl_ls,pj)) pj v m)
    Mls.empty fll
  in
  cs,pjl,flm

let find_field ~loc uc (p,e) =
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
    | PL pl -> (pl,e)
175
    | _ -> errorm ~loc "bad record field %a" Typing.print_qualid p
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218
  with Not_found -> errorm ~loc "unbound symbol %a" Typing.print_qualid p

let find_pure_field ~loc uc (p,e) =
  let x = Typing.string_list_of_qualid [] p in
  try ns_find_ls (Theory.get_namespace (get_theory uc)) x, e
  with Not_found -> errorm ~loc "unbound symbol %a" Typing.print_qualid p

let pure_record ~loc uc = function
  | [] -> error ~loc Decl.EmptyRecord
  | (p,_)::_ ->
      let x = Typing.string_list_of_qualid [] p in
      begin try ignore (ns_find_ps (get_namespace uc) x); false
      with Not_found -> true end

let hidden_pl ~loc pl =
  { dexpr_desc = DEglobal_pl pl;
    dexpr_type = specialize_plsymbol pl;
    dexpr_loc  = loc; dexpr_lab = [] }

let hidden_ls ~loc ls =
  { dexpr_desc = DEglobal_ls ls;
    dexpr_type = specialize_lsymbol ls;
    dexpr_loc  = loc; dexpr_lab = [] }

(* helper functions for let-expansion *)
let test_var e = match e.dexpr_desc with
  | DElocal _ | DEglobal_pv _ -> true
  | _ -> false

let mk_var e =
  if test_var e then e else
  { dexpr_desc = DElocal "q";
    dexpr_type = e.dexpr_type;
    dexpr_loc  = e.dexpr_loc;
    dexpr_lab  = [] }

let mk_let ~loc ~userloc e (desc,dity) =
  if test_var e then desc, dity else
  let loc = def_option loc userloc in
  let e1 = {
    dexpr_desc = desc; dexpr_type = dity; dexpr_loc = loc; dexpr_lab = [] } in
  DElet ({ id = "q"; id_lab = []; id_loc = loc }, e, e1), dity

219 220 221 222 223 224 225 226 227 228 229 230 231
(* patterns *)

let add_var id dity denv =
  let tvars = add_tvars denv.tvars dity in
  let locals = Mstr.add id.id (tvars,dity) denv.locals in
  { denv with locals = locals; tvars = tvars }

let specialize_qualid ~loc uc p =
  let x = Typing.string_list_of_qualid [] p in
  try match ns_find_ps (get_namespace uc) x with
    | PV pv -> DEglobal_pv pv, specialize_pvsymbol pv
    | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
    | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
232
    | PX xs -> errorm ~loc "unexpected exception symbol %a" print_xs xs
233 234 235 236 237 238 239 240 241 242 243 244 245 246
  with Not_found -> try
    let ls = ns_find_ls (Theory.get_namespace (get_theory uc)) x in
    DEglobal_ls ls, specialize_lsymbol ls
  with Not_found ->
    errorm ~loc "unbound symbol %a" Typing.print_qualid p

let mk_dexpr desc dity loc labs =
  { dexpr_desc = desc; dexpr_type = dity; dexpr_loc = loc; dexpr_lab = labs }

let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
  | Ptree.PPpwild ->
      PPwild, create_type_variable (), denv
  | Ptree.PPpvar id ->
      let dity = create_type_variable () in
247
      PPvar (Denv.create_user_id id), dity, add_var id dity denv
248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
  | Ptree.PPpapp (q,ppl) ->
      let sym, dity = specialize_qualid ~loc denv.uc q in
      dpat_app denv (mk_dexpr sym dity loc []) ppl
  | Ptree.PPprec fl when pure_record ~loc denv.uc fl ->
      let kn = Theory.get_known (get_theory denv.uc) in
      let fl = List.map (find_pure_field ~loc denv.uc) fl in
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let wild = { pat_desc = Ptree.PPpwild; pat_loc = loc } in
      let get_val pj = Mls.find_def wild pj flm in
      dpat_app denv (hidden_ls ~loc cs) (List.map get_val pjl)
  | Ptree.PPprec fl ->
      let fl = List.map (find_field ~loc denv.uc) fl in
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let wild = { pat_desc = Ptree.PPpwild; pat_loc = loc } in
      let get_val pj = Mls.find_def wild pj.pl_ls flm in
      dpat_app denv (hidden_pl ~loc cs) (List.map get_val pjl)
  | Ptree.PPptuple ppl ->
      let cs = fs_tuple (List.length ppl) in
      dpat_app denv (hidden_ls ~loc cs) ppl
  | Ptree.PPpor (pp1, pp2) ->
      let pp1, dity1, denv = dpattern denv pp1 in
      let pp2, dity2, denv = dpattern denv pp2 in
      Loc.try2 loc unify dity1 dity2;
      PPor (pp1, pp2), dity1, denv
  | Ptree.PPpas (pp, id) ->
      let pp, dity, denv = dpattern denv pp in
274
      PPas (pp, Denv.create_user_id id), dity, add_var id dity denv
275 276 277 278 279 280 281 282

and dpat_app denv ({ dexpr_loc = loc } as de) ppl =
  let add_pp pp (ppl, tyl, denv) =
    let pp,ty,denv = dpattern denv pp in pp::ppl,ty::tyl,denv in
  let ppl, tyl, denv = List.fold_right add_pp ppl ([],[],denv) in
  let pp = match de.dexpr_desc with
    | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl)
    | DEglobal_ls ls -> PPlapp (ls, ppl)
283 284
    | DEglobal_pv pv -> errorm ~loc "%a is not a constructor" print_pv pv
    | DEglobal_ps ps -> errorm ~loc "%a is not a constructor" print_ps ps
285 286 287 288 289 290
    | _ -> assert false
  in
  let res = create_type_variable () in
  Loc.try2 loc unify de.dexpr_type (make_arrow_type tyl res);
  pp, res, denv

291 292 293 294 295
(* value restriction *)
let rec is_fun e = match e.dexpr_desc with
  | DEfun _ -> true
  | DEmark (_, e) -> is_fun e
  | _ -> false
296

297 298 299 300 301 302
let dexpr_app e el =
  let res = create_type_variable () in
  let tyl = List.map (fun a -> a.dexpr_type) el in
  expected_type e (make_arrow_type tyl res);
  DEapply (e, el), res

303 304 305 306 307
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
308
  mk_dexpr d ty loc labs
309

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
310
and dexpr_desc ~userloc denv loc = function
311 312
  | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
      (* local variable *)
313 314 315
      let tvs, dity = Mstr.find x denv.locals in
      let dity = specialize_scheme tvs dity in
      DElocal x, dity
316
  | Ptree.Eident p ->
317
      specialize_qualid ~loc denv.uc p
318 319 320
  | Ptree.Eapply (e1, e2) ->
      let e, el = decompose_app [e2] e1 in
      let el = List.map (dexpr ~userloc denv) el in
321
      dexpr_app (dexpr ~userloc denv e) el
322 323
  | Ptree.Elet (id, e1, e2) ->
      let e1 = dexpr ~userloc denv e1 in
324 325 326 327
      let dity = e1.dexpr_type in
      let tvars = if is_fun e1 then denv.tvars else add_tvars denv.tvars dity in
      let locals = Mstr.add id.id (tvars, dity) denv.locals in
      let denv = { denv with locals = locals; tvars = tvars } in
328 329
      let e2 = dexpr ~userloc denv e2 in
      DElet (id, e1, e2), e2.dexpr_type
Andrei Paskevich's avatar
Andrei Paskevich committed
330
  | Ptree.Eletrec (rdl, e1) ->
331 332 333 334
      let rdl = dletrec ~userloc denv rdl in
      let add_one denv ({ id = id }, dity, _, _, _) =
        { denv with locals = Mstr.add id (denv.tvars, dity) denv.locals } in
      let denv = List.fold_left add_one denv rdl in
Andrei Paskevich's avatar
Andrei Paskevich committed
335
      let e1 = dexpr ~userloc denv e1 in
336
      DEletrec (rdl, e1), e1.dexpr_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
337
  | Ptree.Efun (bl, tr) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
338
      let bl, _, tr, dity = dlambda ~userloc denv bl None tr in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
339
      DEfun (bl, tr), dity
340 341
  | Ptree.Ecast (e1, pty) ->
      let e1 = dexpr ~userloc denv e1 in
342
      expected_type e1 (dity_of_pty ~user:false denv pty);
343 344 345
      e1.dexpr_desc, e1.dexpr_type
  | Ptree.Enamed _ ->
      assert false
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
  | Ptree.Esequence (e1, e2) ->
      let e1 = dexpr ~userloc denv e1 in
      expected_type e1 dity_unit;
      let e2 = dexpr ~userloc denv e2 in
      DElet ({ id = "_"; id_lab = []; id_loc = loc }, e1, e2), e2.dexpr_type
  | Ptree.Eif (e1, e2, e3) ->
      let e1 = dexpr ~userloc denv e1 in
      expected_type e1 dity_bool;
      let e2 = dexpr ~userloc denv e2 in
      let e3 = dexpr ~userloc denv e3 in
      expected_type e3 e2.dexpr_type;
      DEif (e1, e2, e3), e2.dexpr_type
  | Ptree.Etuple el ->
      let ls = fs_tuple (List.length el) in
      let el = List.map (dexpr ~userloc denv) el in
      dexpr_app (hidden_ls ~loc ls) el
  | Ptree.Erecord fl when pure_record ~loc denv.uc fl ->
      let kn = Theory.get_known (get_theory denv.uc) in
      let fl = List.map (find_pure_field ~loc denv.uc) fl in
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let get_val pj = match Mls.find_opt pj flm with
        | Some e -> dexpr ~userloc denv e
        | None -> error ~loc (Decl.RecordFieldMissing (cs,pj)) in
      dexpr_app (hidden_ls ~loc cs) (List.map get_val pjl)
  | Ptree.Erecord fl ->
      let fl = List.map (find_field ~loc denv.uc) fl in
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let get_val pj = match Mls.find_opt pj.pl_ls flm with
        | Some e -> dexpr ~userloc denv e
        | None -> error ~loc (Decl.RecordFieldMissing (cs.pl_ls,pj.pl_ls)) in
      dexpr_app (hidden_pl ~loc cs) (List.map get_val pjl)
  | Ptree.Eupdate (e1, fl) when pure_record ~loc denv.uc fl ->
      let e1 = dexpr ~userloc denv e1 in
      let e0 = mk_var e1 in
      let kn = Theory.get_known (get_theory denv.uc) in
      let fl = List.map (find_pure_field ~loc denv.uc) fl in
      let cs,pjl,flm = Loc.try2 loc Decl.parse_record kn fl in
      let get_val pj = match Mls.find_opt pj flm with
        | Some e -> dexpr ~userloc denv e
        | None ->
386 387
            let d, dity = dexpr_app (hidden_ls ~loc pj) [e0] in
            mk_dexpr d dity loc [] in
388 389 390 391 392 393 394 395 396 397
      let res = dexpr_app (hidden_ls ~loc cs) (List.map get_val pjl) in
      mk_let ~loc ~userloc e1 res
  | Ptree.Eupdate (e1, fl) ->
      let e1 = dexpr ~userloc denv e1 in
      let e0 = mk_var e1 in
      let fl = List.map (find_field ~loc denv.uc) fl in
      let cs,pjl,flm = Loc.try2 loc parse_record denv.uc fl in
      let get_val pj = match Mls.find_opt pj.pl_ls flm with
        | Some e -> dexpr ~userloc denv e
        | None ->
398 399
            let d, dity = dexpr_app (hidden_pl ~loc pj) [e0] in
            mk_dexpr d dity loc [] in
400 401
      let res = dexpr_app (hidden_pl ~loc cs) (List.map get_val pjl) in
      mk_let ~loc ~userloc e1 res
Andrei Paskevich's avatar
Andrei Paskevich committed
402
  | Ptree.Eassign (e1, q, e2) ->
403 404
      let fl = { expr_desc = Eident q; expr_loc = loc } in
      let e1 = { expr_desc = Eapply (fl,e1); expr_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
405 406 407 408
      let e1 = dexpr ~userloc denv e1 in
      let e2 = dexpr ~userloc denv e2 in
      expected_type e2 e1.dexpr_type;
      DEassign (e1, e2), dity_unit
409 410 411 412 413 414 415 416 417 418 419 420 421 422
  | Ptree.Econstant (ConstInt _ as c) ->
      DEconstant c, dity_int
  | Ptree.Econstant (ConstReal _ as c) ->
      DEconstant c, dity_real
  | Ptree.Enot e1 ->
      let e1 = dexpr ~userloc denv e1 in
      expected_type e1 dity_bool;
      DEnot e1, dity_bool
  | Ptree.Elazy (op, e1, e2) ->
      let e1 = dexpr ~userloc denv e1 in
      let e2 = dexpr ~userloc denv e2 in
      expected_type e1 dity_bool;
      expected_type e2 dity_bool;
      DElazy (op, e1, e2), dity_bool
423 424 425 426 427 428 429 430 431 432
  | Ptree.Ematch (e1, bl) ->
      let e1 = dexpr ~userloc denv e1 in
      let res = create_type_variable () in
      let branch (pp,e) =
        let ppat, dity, denv = dpattern denv pp in
        let e = dexpr ~userloc denv e in
        Loc.try2 pp.pat_loc unify dity e1.dexpr_type;
        expected_type e res;
        ppat, e in
      DEmatch (e1, List.map branch bl), res
433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449
  | Ptree.Eloop (_ann, _e1) ->
      assert false (*TODO*)
  | Ptree.Eabsurd ->
      assert false (*TODO*)
  | Ptree.Eraise (_q, _e1) ->
      assert false (*TODO*)
  | Ptree.Etry (_e1, _cl) ->
      assert false (*TODO*)
  | Ptree.Efor (_id, _e1, _dir, _e2, _lexpr_opt, _e3) ->
      assert false (*TODO*)
  | Ptree.Eassert (_ass, _lexpr) ->
      assert false (*TODO*)
  | Ptree.Emark (_id, _e1) ->
      assert false (*TODO*)
  | Ptree.Eany (_type_c) ->
      assert false (*TODO*)
  | Ptree.Eabstract (_e1, _post) ->
450 451
      assert false (*TODO*)

Andrei Paskevich's avatar
Andrei Paskevich committed
452 453 454 455
and dletrec ~userloc denv rdl =
  (* add all functions into environment *)
  let add_one denv (id, bl, var, tr) =
    let res = create_type_variable () in
456 457 458 459
    let tvars = add_tvars denv.tvars res in
    let locals = Mstr.add id.id (tvars, res) denv.locals in
    let denv = { denv with locals = locals; tvars = tvars } in
    denv, (id, res, bl, var, tr) in
Andrei Paskevich's avatar
Andrei Paskevich committed
460 461 462 463 464 465
  let denv, rdl = Util.map_fold_left add_one denv rdl in
  (* then type-check all of them and unify *)
  let type_one (id, res, bl, var, tr) =
    let bl, var, tr, dity = dlambda ~userloc denv bl var tr in
    Loc.try2 id.id_loc unify dity res;
    id, dity, bl, var, tr in
466
  List.map type_one rdl
Andrei Paskevich's avatar
Andrei Paskevich committed
467 468 469 470 471 472 473 474 475

and dlambda ~userloc denv bl _var (p, e, q) =
  let dbinder denv (id, pty) =
    let dity = match pty with
      | Some pty -> dity_of_pty ~user:false denv pty
      | None -> create_type_variable () in
    add_var id dity denv, (id, false, dity) in
  let denv, bl = Util.map_fold_left dbinder denv bl in
  let tyl = List.map (fun (_,_,d) -> d) bl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
476 477
  let e = dexpr ~userloc denv e in
  let q = dpost denv q in
Andrei Paskevich's avatar
Andrei Paskevich committed
478
  bl, [], (p, e, q), make_arrow_type tyl e.dexpr_type
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
479 480 481 482

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

483
let rec expr locals de = match de.dexpr_desc with
484 485 486
  | DElocal x ->
      assert (Mstr.mem x locals);
      begin match Mstr.find x locals with
487 488
      | LetV pv -> e_value pv
      | LetA ps -> e_cast ps (vty_of_dity de.dexpr_type)
489
      end
490 491 492 493 494 495
  | 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) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
496
      let x = { id = "fn"; id_loc = de.dexpr_loc; id_lab = [] } in
497 498 499 500 501
      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
502
      let def1 = create_let_defn (Denv.create_user_id x) e1 in
503 504 505
      let locals = Mstr.add x.id def1.let_var locals in
      let e2 = expr locals de2 in
      e_let def1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
506 507 508 509 510
  | DEletrec (rdl, de1) ->
      let rdl = expr_rec locals rdl in
      let add_rd { rec_ps = ps } = Mstr.add ps.ps_name.id_string (LetA ps) in
      let e1 = expr (List.fold_right add_rd rdl locals) de1 in
      e_rec rdl e1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
511 512 513 514 515
  | DEapply (de1, del) ->
      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)
Andrei Paskevich's avatar
Andrei Paskevich committed
516
        | _               -> e_app (expr locals de1) el
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
517
      end
518 519 520 521
  | DEglobal_pv pv ->
      e_value pv
  | DEglobal_ps ps ->
      e_cast ps (vty_of_dity de.dexpr_type)
Andrei Paskevich's avatar
Andrei Paskevich committed
522 523 524
  | DEglobal_pl pl ->
      assert (pl.pl_ls.ls_args = []);
      e_plapp pl [] (ity_of_dity de.dexpr_type)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
525
  | DEglobal_ls ls ->
Andrei Paskevich's avatar
Andrei Paskevich committed
526
      assert (ls.ls_args = []);
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
527
      e_lapp ls [] (ity_of_dity de.dexpr_type)
528 529
  | DEif (de1, de2, de3) ->
      e_if (expr locals de1) (expr locals de2) (expr locals de3)
Andrei Paskevich's avatar
Andrei Paskevich committed
530 531
  | DEassign (de1, de2) ->
      e_assign (expr locals de1) (expr locals de2)
532 533 534 535 536 537 538 539
  | DEconstant c ->
      e_const c
  | DElazy (LazyAnd, de1, de2) ->
      e_lazy_and (expr locals de1) (expr locals de2)
  | DElazy (LazyOr, de1, de2) ->
      e_lazy_or (expr locals de1) (expr locals de2)
  | DEnot de1 ->
      e_not (expr locals de1)
540 541 542 543 544 545 546 547
  | DEmatch (de1, bl) ->
      let e1 = expr locals de1 in
      let vtv = vtv_of_expr e1 in
      let branch (pp,de) =
        let vm, pp = make_ppattern pp vtv in
        let locals = Mstr.fold (fun s pv -> Mstr.add s (LetV pv)) vm locals in
        pp, expr locals de in
      e_case e1 (List.map branch bl)
548 549 550
  | _ ->
      assert false (*TODO*)

Andrei Paskevich's avatar
Andrei Paskevich committed
551 552 553 554 555
and expr_rec locals rdl =
  let step1 locals (id, dity, bl, var, tr) =
    let vta = match vty_of_dity dity with
      | VTarrow vta -> vta
      | VTvalue _ -> assert false in
556
    let ps = create_psymbol (Denv.create_user_id id) vta vars_empty in
Andrei Paskevich's avatar
Andrei Paskevich committed
557 558 559 560 561 562 563 564
    Mstr.add id.id (LetA ps) locals, (ps, bl, var, tr)
  in
  let locals, rdl = Util.map_fold_left step1 locals rdl in
  let step2 (ps, bl, var, tr) = ps, expr_lam locals bl var tr in
  create_rec_defn (List.map step2 rdl)

and expr_fun locals x bl tr =
  let lam = expr_lam locals bl [] tr in
565
  create_fun_defn (Denv.create_user_id x) lam
Andrei Paskevich's avatar
Andrei Paskevich committed
566 567

and expr_lam locals bl _var (_, e, _) =
568 569
  let binder (id, ghost, dity) =
    let vtv = vty_value ~ghost (ity_of_dity dity) in
570
    create_pvsymbol (Denv.create_user_id id) vtv in
571 572
  let pvl = List.map binder bl in
  let add_binder pv = Mstr.add pv.pv_vs.vs_name.id_string (LetV pv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
573 574 575
  let locals = List.fold_right add_binder pvl locals in
  let e = expr locals e in
  let ty = match e.e_vty with
576 577
    | VTarrow _ -> ty_tuple []
    | VTvalue vtv -> ty_of_ity vtv.vtv_ity in
Andrei Paskevich's avatar
Andrei Paskevich committed
578 579 580
  let res = create_vsymbol (id_fresh "result") ty in
  { l_args = pvl;
    l_variant = [];                   (* TODO *)
581
    l_pre = t_true;                   (* TODO *)
Andrei Paskevich's avatar
Andrei Paskevich committed
582 583
    l_expr = e;
    l_post = create_post res t_true;  (* TODO *)
584
    l_xpost = Mexn.empty;             (* TODO *)
Andrei Paskevich's avatar
Andrei Paskevich committed
585
  }
586

587 588
(** Type declaration *)

589
type tys = ProgTS of itysymbol | PureTS of tysymbol
590 591 592 593 594 595 596 597 598

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)

599 600 601
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
602 603 604
  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
605 606 607 608 609 610 611 612 613 614
  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

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 681 682 683 684 685 686
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
687
        let tv = create_tvsymbol (Denv.create_user_id id) in
688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709
        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 ->
710
            let ts = ts_tuple (List.length tyl) in
711 712 713 714 715
            ity_pur ts (List.map parse tyl)
      in
      let ts = match d.td_def with
        | TDalias ty ->
            let def = parse ty in
716 717
            let rl = Sreg.elements def.ity_vars.vars_reg in
            create_itysymbol id ~abst ~priv vl rl (Some def)
718
        | TDalgebraic csl when Hashtbl.find mutables x ->
719 720 721 722 723 724
            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
725
              let vtv = vty_value ity in
726 727
              match id with
                | None ->
728
                    let pv = create_pvsymbol (id_fresh "pj") vtv in
729
                    Sreg.union s ity.ity_vars.vars_reg, (pv, false)
730 731 732
                | Some id ->
                    try
                      let pv = Hashtbl.find projs id.id in
733
                      let ty = pv.pv_vtv.vtv_ity in
734 735
                      (* once we have ghost/mutable fields in algebraics,
                         don't forget to check here that they coincide, too *)
736
                      ignore (Loc.try3 id.id_loc ity_match sbs ty ity);
737 738
                      s, (pv, true)
                    with Not_found ->
739
                      let pv = create_pvsymbol (Denv.create_user_id id) vtv in
740
                      Hashtbl.replace projs id.id pv;
741
                      Sreg.union s ity.ity_vars.vars_reg, (pv, true)
742 743 744 745 746 747
            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
748
            Hashtbl.replace predefs x def;
749
            create_itysymbol id ~abst ~priv vl (Sreg.elements s) None
750
        | TDrecord fl when Hashtbl.find mutables x ->
751 752 753 754 755
            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
756
                let r = create_region fid ity in
757 758
                Sreg.add r s, Some r
              else
759
                Sreg.union s ity.ity_vars.vars_reg, None
760
              in
761 762
              let vtv = vty_value ?mut ~ghost ity in
              s, (create_pvsymbol fid vtv, true)
763 764 765
            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
766
            Hashtbl.replace predefs x [Denv.create_user_id cid, pjl];
767 768 769 770 771 772 773 774 775 776 777
            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 *)

778
  let def_visit d (abstr,algeb,alias) =
779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798
    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 ->
799
          let ts = ts_tuple (List.length tyl) in
800 801 802
          ity_pur ts (List.map parse tyl)
    in
    match d.td_def with
803 804 805 806
      | TDabstract ->
          ts :: abstr, algeb, alias
      | TDalias _ ->
          abstr, algeb, ts :: alias
807
      | (TDalgebraic _ | TDrecord _) when Hashtbl.find mutables x ->
808
          abstr, (ts, Hashtbl.find predefs x) :: algeb, alias
809 810 811 812
      | TDalgebraic csl ->
          let projs = Hashtbl.create 5 in
          let mk_proj (id,pty) =
            let ity = parse pty in
813
            let vtv = vty_value ity in
814 815
            match id with
              | None ->
816
                  create_pvsymbol (id_fresh "pj") vtv, false
817 818 819
              | Some id ->
                  try
                    let pv = Hashtbl.find projs id.id in
820
                    let ty = pv.pv_vtv.vtv_ity in
821 822
                    (* once we have ghost/mutable fields in algebraics,
                       don't forget to check here that they coincide, too *)
823
                    Loc.try2 id.id_loc ity_equal_check ty ity;
824 825
                    pv, true
                  with Not_found ->
826
                    let pv = create_pvsymbol (Denv.create_user_id id) vtv in
827 828 829 830 831
                    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
832
          abstr, (ts, List.map mk_constr csl) :: algeb, alias
833 834 835
      | TDrecord fl ->
          let mk_field f =
            let fid = Denv.create_user_id f.f_ident in
836 837
            let vtv = vty_value ~ghost:f.f_ghost (parse f.f_pty) in
            create_pvsymbol fid vtv, true in
838
          let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in
839 840
          let csl = [Denv.create_user_id cid, List.map mk_field fl] in
          abstr, (ts, csl) :: algeb, alias
841
  in
842
  let abstr,algeb,alias = List.fold_right def_visit tdl ([],[],[]) in
843 844

  (* detect pure type declarations *)
845

846 847 848
  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
849
  let is_impure_type ts =
850
    ts.its_abst || ts.its_priv || ts.its_regs <> [] ||
851
    option_apply false check ts.its_def
852
  in
853
  let check (pv,_) =
854
    let vtv = pv.pv_vtv in
855
    vtv.vtv_ghost || vtv.vtv_mut <> None || check vtv.vtv_ity in
856 857 858
  let is_impure_data (ts,csl) =
    is_impure_type ts ||
    List.exists (fun (_,l) -> List.exists check l) csl
859
  in
860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881
  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)
882
    else
883 884 885 886 887 888 889 890 891 892 893 894 895
      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
896
  with
897 898 899 900 901 902 903 904 905
    | 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
906 907 908

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

909 910 911 912
type mlw_contents = modul Mstr.t
type mlw_library = mlw_contents library
type mlw_file = mlw_contents * Theory.theory Mstr.t

913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938
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

939 940 941
let print_path fmt sl =
  Pp.print_list (Pp.constant_string ".") Format.pp_print_string fmt sl

942 943 944 945 946
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
947
      Mstr.find_opt s mm, Mstr.find_opt s mt
948 949 950 951 952 953 954 955 956 957 958 959 960
    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
961 962
    | None, None, None ->
        Loc.errorm ~loc "Theory/module not found: %a" print_path (path @ [s])
963 964 965
    | Some m, Some _, None -> Module m
    | None, Some t, None | None, None, Some t -> Theory t

966
let find_module loc lib mm mt path s = match path with
967 968 969 970 971 972 973
  | [] -> (* 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

974 975
(** Main loop *)

976
let add_theory lib path mt m =
977 978
  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;
979
  let uc = create_theory ~path (Denv.create_user_id m.pth_name) in
980
  let rec add_decl uc = function
981 982
    | Dlogic d ->
        Typing.add_decl uc d
983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000
    | 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
1001 1002 1003
    | Dnamespace (loc, name, import, dl) ->
        let uc = Theory.open_namespace uc in
        let uc = List.fold_left add_decl uc dl in
1004
        Loc.try3 loc Theory.close_namespace uc import name
1005 1006 1007 1008
    | Dlet _ | Dletrec _ | Dparam _ | Dexn _ | Duse _ ->
        assert false
  in
  let uc = List.fold_left add_decl uc m.pth_decl in
1009
  let th = close_theory uc in
1010 1011 1012 1013 1014 1015 1016 1017
  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
1018 1019 1020 1021
    | Dlogic (TypeDecl tdl) ->
        add_types uc tdl
    | Dlogic d ->
        add_to_theory Typing.add_decl uc d
1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046
    | 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
1047
    | Dlet (id, e) ->
1048
        let e = dexpr ~userloc:None (create_denv uc) e in
1049 1050 1051 1052 1053 1054
        let pd = match e.dexpr_desc with
          | DEfun (bl, tr) ->
              let def = expr_fun Mstr.empty id bl tr in
              create_rec_decl [def]
          | _ ->
              let e = expr Mstr.empty e in
1055
              let def = create_let_defn (Denv.create_user_id id) e in
1056 1057 1058
              create_let_decl def
        in
        Loc.try2 loc add_pdecl_with_tuples uc pd
Andrei Paskevich's avatar
Andrei Paskevich committed
1059
    | Dletrec rdl ->
1060
        let rdl = dletrec ~userloc:None (create_denv uc) rdl in
Andrei Paskevich's avatar
Andrei Paskevich committed
1061 1062 1063
        let rdl = expr_rec Mstr.empty rdl in
        let pd = create_rec_decl rdl in
        Loc.try2 loc add_pdecl_with_tuples uc pd
1064 1065 1066 1067 1068 1069 1070 1071
    | Dexn (id, pty) ->
        let ity = match pty with
          | Some pty ->
              ity_of_dity (dity_of_pty ~user:false (create_denv uc) pty)
          | None -> ity_unit in
        let xs = create_xsymbol (Denv.create_user_id id) ity in
        let pd = create_exn_decl xs in
        Loc.try2 loc add_pdecl_with_tuples uc pd
Andrei Paskevich's avatar
Andrei Paskevich committed
1072 1073 1074
    | Dparam _ ->
        assert false (*TODO*)
    | Duse _ ->
1075
        assert false (*TO BE REMOVED EVENTUALLY *)
1076 1077 1078 1079
  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
1080 1081 1082

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