typing.ml 31.9 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
13
open Ident
14
open Ptree
15
open Ty
16
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
17
open Decl
18
open Theory
19
open Dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
20
open Env
Andrei Paskevich's avatar
Andrei Paskevich committed
21

22
(** debug flags *)
23

24
let debug_parse_only = Debug.register_flag "parse_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
25
  ~desc:"Stop@ after@ parsing."
26

27
let debug_type_only  = Debug.register_flag "type_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
28
  ~desc:"Stop@ after@ type-checking."
29

30
(** errors *)
31

32 33 34
exception UnboundTypeVar of string
exception DuplicateTypeVar of string
exception ClashTheory of string
35

36
(** lazy declaration of tuples *)
37

38 39 40 41
let add_decl_with_tuples uc d =
  if Debug.test_flag Glob.flag then Sid.iter Glob.def d.d_news;
  add_decl_with_tuples uc d

42 43 44 45 46 47
let add_ty_decl uc ts      = add_decl_with_tuples uc (create_ty_decl ts)
let add_data_decl uc dl    = add_decl_with_tuples uc (create_data_decl dl)
let add_param_decl uc ls   = add_decl_with_tuples uc (create_param_decl ls)
let add_logic_decl uc dl   = add_decl_with_tuples uc (create_logic_decl dl)
let add_ind_decl uc s dl   = add_decl_with_tuples uc (create_ind_decl s dl)
let add_prop_decl uc k p f = add_decl_with_tuples uc (create_prop_decl k p f)
48

49
(** symbol lookup *)
50 51

let rec qloc = function
52 53 54
  | Qdot (p, id) -> Loc.join (qloc p) id.id_loc
  | Qident id    -> id.id_loc

55 56 57
let qloc_last = function
  | Qdot (_, id) | Qident id -> id.id_loc

58 59 60
let rec print_qualid fmt = function
  | Qdot (p, id) -> Format.fprintf fmt "%a.%s" print_qualid p id.id
  | Qident id    -> Format.fprintf fmt "%s" id.id
61

62 63 64 65 66
let string_list_of_qualid q =
  let rec sloq acc = function
    | Qdot (p, id) -> sloq (id.id :: acc) p
    | Qident id -> id.id :: acc in
  sloq [] q
67

68
exception UnboundSymbol of qualid
69

70
let find_qualid get_id find ns q =
71 72 73
  let sl = string_list_of_qualid q in
  let r = try find ns sl with Not_found ->
    Loc.error ~loc:(qloc q) (UnboundSymbol q) in
74
  if Debug.test_flag Glob.flag then Glob.use (qloc_last q) (get_id r);
75
  r
76

77 78 79
let find_prop_ns     ns q = find_qualid (fun pr -> pr.pr_name) ns_find_pr ns q
let find_tysymbol_ns ns q = find_qualid (fun ts -> ts.ts_name) ns_find_ts ns q
let find_lsymbol_ns  ns q = find_qualid (fun ls -> ls.ls_name) ns_find_ls ns q
80

81 82
let find_fsymbol_ns ns q =
  let ls = find_lsymbol_ns ns q in
83 84
  if ls.ls_value <> None then ls else
    Loc.error ~loc:(qloc q) (FunctionSymbolExpected ls)
85

86 87
let find_psymbol_ns ns q =
  let ls = find_lsymbol_ns ns q in
88 89
  if ls.ls_value = None then ls else
    Loc.error ~loc:(qloc q) (PredicateSymbolExpected ls)
90

91 92 93 94 95
let find_prop     uc q = find_prop_ns     (get_namespace uc) q
let find_tysymbol uc q = find_tysymbol_ns (get_namespace uc) q
let find_lsymbol  uc q = find_lsymbol_ns  (get_namespace uc) q
let find_fsymbol  uc q = find_fsymbol_ns  (get_namespace uc) q
let find_psymbol  uc q = find_psymbol_ns  (get_namespace uc) q
96

97 98
let find_namespace_ns ns q =
  find_qualid (fun _ -> Glob.dummy_id) ns_find_ns ns q
99

100 101 102
(** Parsing types *)

let create_user_tv =
103 104
  let hs = Hstr.create 17 in fun s ->
  try Hstr.find hs s with Not_found ->
105 106 107
  let tv = create_tvsymbol (id_fresh s) in
  Hstr.add hs s tv;
  tv
108

Andrei Paskevich's avatar
Andrei Paskevich committed
109
let ty_of_pty ?(noop=true) uc pty =
110 111 112 113 114 115
  let rec get_ty = function
    | PPTtyvar ({id_loc = loc}, true) when noop ->
        Loc.errorm ~loc "Opaqueness@ annotations@ are@ only@ \
          allowed@ in@ function@ and@ predicate@ prototypes"
    | PPTtyvar ({id = x}, _) ->
        ty_var (create_user_tv x)
116 117
    | PPTtyapp (q, tyl) ->
        let ts = find_tysymbol uc q in
118
        let tyl = List.map get_ty tyl in
119
        Loc.try2 ~loc:(qloc q) ty_app ts tyl
120 121 122 123 124 125 126 127 128 129
    | PPTtuple tyl ->
        let ts = ts_tuple (List.length tyl) in
        ty_app ts (List.map get_ty tyl)
    | PPTarrow (ty1, ty2) ->
        ty_func (get_ty ty1) (get_ty ty2)
    | PPTparen ty ->
        get_ty ty
  in
  get_ty pty

130
let opaque_tvs args =
131 132 133 134 135 136 137
  let rec opaque_tvs acc = function
    | PPTtyvar (id, true) -> Stv.add (create_user_tv id.id) acc
    | PPTtyvar (_, false) -> acc
    | PPTtyapp (_, pl)
    | PPTtuple pl -> List.fold_left opaque_tvs acc pl
    | PPTarrow (ty1, ty2) -> opaque_tvs (opaque_tvs acc ty1) ty2
    | PPTparen ty -> opaque_tvs acc ty in
138
  List.fold_left (fun acc (_,_,_,ty) -> opaque_tvs acc ty) Stv.empty args
139

140
(** typing using destructive type variables
141

142 143 144 145 146 147
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
148

149 150
(** Typing patterns, terms, and formulas *)

151 152 153 154 155
let create_user_id {id = n; id_lab = label; id_loc = loc} =
  let get_labels (label, loc) = function
    | Lstr lab -> Slab.add lab label, loc | Lpos loc -> label, loc in
  let label,loc = List.fold_left get_labels (Slab.empty,loc) label in
  id_user ~label n loc
156 157

let parse_record ~loc uc get_val fl =
158
  let fl = List.map (fun (q,e) -> find_lsymbol uc q, e) fl in
159 160 161 162
  let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known uc) fl in
  let get_val pj = get_val cs pj (Mls.find_opt pj flm) in
  cs, List.map get_val pjl

163 164 165 166
let rec dpattern uc { pat_desc = desc; pat_loc = loc } =
  Dterm.dpattern ~loc (match desc with
    | PPpwild -> DPwild
    | PPpvar x -> DPvar (create_user_id x)
167
    | PPpapp (q,pl) ->
168
        let pl = List.map (dpattern uc) pl in
169
        DPapp (find_lsymbol uc q, pl)
170 171 172 173 174 175 176 177 178 179 180
    | PPptuple pl ->
        let pl = List.map (dpattern uc) pl in
        DPapp (fs_tuple (List.length pl), pl)
    | PPprec fl ->
        let get_val _ _ = function
          | Some p -> dpattern uc p
          | None -> Dterm.dpattern DPwild in
        let cs,fl = parse_record ~loc uc get_val fl in
        DPapp (cs,fl)
    | PPpas (p, x) -> DPas (dpattern uc p, create_user_id x)
    | PPpor (p, q) -> DPor (dpattern uc p, dpattern uc q))
181 182 183 184 185 186

let quant_var uc (x,ty) =
  create_user_id x, match ty with
    | Some ty -> dty_of_ty (ty_of_pty uc ty)
    | None -> dty_fresh ()

187 188 189 190 191 192 193 194 195 196 197 198 199 200
let is_reusable dt = match dt.dt_node with
  | DTvar _ | DTgvar _ | DTconst _ | DTtrue | DTfalse -> true
  | DTapp (_,[]) -> true
  | _ -> false

let mk_var n dt =
  let dty = match dt.dt_dty with
    | None -> dty_of_ty ty_bool
    | Some dty -> dty in
  Dterm.dterm ?loc:dt.dt_loc (DTvar (n, dty))

let mk_let ~loc n dt node =
  DTlet (dt, id_user n loc, Dterm.dterm ~loc node)

201 202 203
let chainable_op uc op =
  (* non-bool -> non-bool -> bool *)
  op.id = "infix =" || op.id = "infix <>" ||
204 205 206 207 208 209
  match find_lsymbol uc (Qident op) with
  | {ls_args = [ty1;ty2]; ls_value = ty} ->
      Opt.fold (fun _ ty -> ty_equal ty ty_bool) true ty
      && not (ty_equal ty1 ty_bool)
      && not (ty_equal ty2 ty_bool)
  | _ -> false
210

211 212
type global_vs = Ptree.qualid -> vsymbol option

213 214 215 216 217 218 219 220 221 222 223 224 225
let mk_closure loc ls =
  let mk dt = Dterm.dterm ~loc dt in
  let id = id_user "fc" loc and dty = dty_fresh () in
  let mk_v i _ =
    id_user ("y" ^ string_of_int i) loc, dty_fresh () in
  let mk_t (id, dty) = mk (DTvar (id.pre_name, dty)) in
  let vl = Lists.mapi mk_v ls.ls_args in
  let tl = List.map mk_t vl in
  let app e1 e2 = DTapp (fs_func_app, [mk e1; e2]) in
  let e = List.fold_left app (DTvar ("fc", dty)) tl in
  let f = DTapp (ps_equ, [mk e; mk (DTapp (ls, tl))]) in
  DTeps (id, dty, mk (DTquant (Tforall, vl, [], mk f)))

226
let rec dterm uc gvars denv {pp_desc = desc; pp_loc = loc} =
227 228 229
  let func_app e el =
    List.fold_left (fun e1 (loc, e2) ->
      DTfapp (Dterm.dterm ~loc e1, e2)) e el
230
  in
231 232 233 234
  let rec apply_ls loc ls al l el = match l, el with
    | (_::l), (e::el) -> apply_ls loc ls (e::al) l el
    | [], _ -> func_app (DTapp (ls, List.rev_map snd al)) el
    | _, [] -> func_app (mk_closure loc ls) (List.rev_append al el)
235
  in
236 237
  let qualid_app q el = match gvars q with
    | Some vs -> func_app (DTgvar vs) el
238
    | None ->
239
        let ls = find_lsymbol uc q in
240
        apply_ls (qloc q) ls [] ls.ls_args el
241
  in
242
  let qualid_app q el = match q with
243 244
    | Qident {id = n} ->
        (match denv_get_opt denv n with
245 246 247 248 249 250 251 252 253 254 255 256
        | Some d -> func_app d el
        | None -> qualid_app q el)
    | _ -> qualid_app q el
  in
  let rec unfold_app e1 e2 el = match e1.pp_desc with
    | PPapply (e11,e12) ->
        let e12 = dterm uc gvars denv e12 in
        unfold_app e11 e12 ((e1.pp_loc, e2)::el)
    | PPident q ->
        qualid_app q ((e1.pp_loc, e2)::el)
    | _ ->
        func_app (DTfapp (dterm uc gvars denv e1, e2)) el
257
  in
258
  Dterm.dterm ~loc (match desc with
259
  | PPident q ->
260
      qualid_app q []
261
  | PPidapp (q, tl) ->
262 263
      let tl = List.map (dterm uc gvars denv) tl in
      DTapp (find_lsymbol uc q, tl)
264
  | PPapply (e1, e2) ->
265
      unfold_app e1 (dterm uc gvars denv e2) []
266
  | PPtuple tl ->
267
      let tl = List.map (dterm uc gvars denv) tl in
268 269 270 271 272
      DTapp (fs_tuple (List.length tl), tl)
  | PPinfix (e12, op2, e3)
  | PPinnfix (e12, op2, e3) ->
      let make_app de1 op de2 = if op.id = "infix <>" then
        let op = { op with id = "infix =" } in
273
        let ls = find_lsymbol uc (Qident op) in
274 275
        DTnot (Dterm.dterm ~loc (DTapp (ls, [de1;de2])))
      else
276
        DTapp (find_lsymbol uc (Qident op), [de1;de2])
277 278 279 280 281 282 283
      in
      let rec make_chain de1 = function
        | [op,de2] ->
            make_app de1 op de2
        | (op,de2) :: ch ->
            let de12 = Dterm.dterm ~loc (make_app de1 op de2) in
            let de23 = Dterm.dterm ~loc (make_chain de2 ch) in
284
            DTbinop (DTand, de12, de23)
285 286 287
        | [] -> assert false in
      let rec get_chain e12 acc = match e12.pp_desc with
        | PPinfix (e1, op1, e2) when chainable_op uc op1 ->
288
            get_chain e1 ((op1, dterm uc gvars denv e2) :: acc)
289
        | _ -> e12, acc in
290
      let ch = [op2, dterm uc gvars denv e3] in
291 292
      let e1, ch = if chainable_op uc op2
        then get_chain e12 ch else e12, ch in
293
      make_chain (dterm uc gvars denv e1) ch
294 295 296 297
  | PPconst c ->
      DTconst c
  | PPlet (x, e1, e2) ->
      let id = create_user_id x in
298
      let e1 = dterm uc gvars denv e1 in
299
      let denv = denv_add_let denv e1 id in
300
      let e2 = dterm uc gvars denv e2 in
301 302
      DTlet (e1, id, e2)
  | PPmatch (e1, bl) ->
303
      let e1 = dterm uc gvars denv e1 in
304 305 306
      let branch (p, e) =
        let p = dpattern uc p in
        let denv = denv_add_pat denv p in
307
        p, dterm uc gvars denv e in
308 309
      DTcase (e1, List.map branch bl)
  | PPif (e1, e2, e3) ->
310 311 312
      let e1 = dterm uc gvars denv e1 in
      let e2 = dterm uc gvars denv e2 in
      let e3 = dterm uc gvars denv e3 in
313 314 315 316 317 318
      DTif (e1, e2, e3)
  | PPtrue ->
      DTtrue
  | PPfalse ->
      DTfalse
  | PPunop (PPnot, e1) ->
319
      DTnot (dterm uc gvars denv e1)
320
  | PPbinop (e1, op, e2) ->
321 322
      let e1 = dterm uc gvars denv e1 in
      let e2 = dterm uc gvars denv e2 in
323
      let op = match op with
324 325 326 327 328 329
        | PPand -> DTand
        | PPand_asym -> DTand_asym
        | PPor -> DTor
        | PPor_asym -> DTor_asym
        | PPimplies -> DTimplies
        | PPiff -> DTiff in
330 331 332 333
      DTbinop (op, e1, e2)
  | PPquant (q, uqu, trl, e1) ->
      let qvl = List.map (quant_var uc) uqu in
      let denv = denv_add_quant denv qvl in
334 335 336
      let dterm e = dterm uc gvars denv e in
      let trl = List.map (List.map dterm) trl in
      let e1 = dterm e1 in
337 338 339 340 341 342 343 344 345 346 347 348 349 350 351
      begin match q with
        | PPforall -> DTquant (Tforall, qvl, trl, e1)
        | PPexists -> DTquant (Texists, qvl, trl, e1)
        | PPlambda ->
            let id = id_user "fc" loc and dty = dty_fresh () in
            let add acc ({id = x}, _) =
              let arg = Dterm.dterm ~loc (denv_get denv x) in
              DTapp (fs_func_app, [Dterm.dterm ~loc acc; arg]) in
            let app = List.fold_left add (DTvar ("fc",dty)) uqu in
            let f = DTapp (ps_equ, [Dterm.dterm ~loc app; e1]) in
            let f = DTquant (Tforall, qvl, trl, Dterm.dterm ~loc f) in
            DTeps (id, dty, Dterm.dterm ~loc f)
      end
  | PPrecord fl ->
      let get_val cs pj = function
352
        | Some e -> dterm uc gvars denv e
353 354 355 356
        | None -> Loc.error ~loc (RecordFieldMissing (cs,pj)) in
      let cs, fl = parse_record ~loc uc get_val fl in
      DTapp (cs, fl)
  | PPupdate (e1, fl) ->
357
      let e1 = dterm uc gvars denv e1 in
358 359
      let re = is_reusable e1 in
      let v = if re then e1 else mk_var "_q " e1 in
360
      let get_val _ pj = function
361
        | Some e -> dterm uc gvars denv e
362
        | None -> Dterm.dterm ~loc (DTapp (pj,[v])) in
363
      let cs, fl = parse_record ~loc uc get_val fl in
364 365
      let d = DTapp (cs, fl) in
      if re then d else mk_let ~loc "_q " e1 d
366
  | PPnamed (Lpos uloc, e1) ->
367
      DTuloc (dterm uc gvars denv e1, uloc)
368
  | PPnamed (Lstr lab, e1) ->
369
      DTlabel (dterm uc gvars denv e1, Slab.singleton lab)
370
  | PPcast (e1, ty) ->
371
      DTcast (dterm uc gvars denv e1, ty_of_pty uc ty))
372 373

(** Export for program parsing *)
Andrei Paskevich's avatar
Andrei Paskevich committed
374

375 376
let type_term uc gvars t =
  let t = dterm uc gvars denv_empty t in
377
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
378

379 380
let type_fmla uc gvars f =
  let f = dterm uc gvars denv_empty f in
381
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
382

383
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
384

Andrei Paskevich's avatar
Andrei Paskevich committed
385
let tyl_of_params ?(noop=false) uc pl =
386 387 388
  let ty_of_param (loc,_,gh,ty) =
    if gh then Loc.errorm ~loc
      "ghost parameters are not allowed in pure declarations";
Andrei Paskevich's avatar
Andrei Paskevich committed
389
    ty_of_pty ~noop uc ty in
390 391
  List.map ty_of_param pl

392
let add_types dl th =
393
  let def = List.fold_left
394
    (fun def d ->
395
      let id = d.td_ident.id in
396
      Mstr.add_new (Loc.Located (d.td_loc, ClashSymbol id)) id d def)
397
    Mstr.empty dl
398
  in
399
  let tysymbols = Hstr.create 17 in
400
  let rec visit x =
401
    let d = Mstr.find x def in
402
    try
403
      match Hstr.find tysymbols x with
404
        | None -> Loc.errorm ~loc:d.td_loc "Cyclic type definition"
405
        | Some ts -> ts
406
    with Not_found ->
407 408
      Hstr.add tysymbols x None;
      let vars = Hstr.create 17 in
409
      let vl = List.map (fun id ->
410
        if Hstr.mem vars id.id then
411
          Loc.error ~loc:id.id_loc (DuplicateTypeVar id.id);
412
        let i = create_user_tv id.id in
413
        Hstr.add vars id.id i;
414
        i) d.td_params
415
      in
416
      let id = create_user_id d.td_ident in
417
      let ts = match d.td_def with
418 419
        | TDalias ty ->
            let rec apply = function
420
              | PPTtyvar (v, _) ->
421
                  begin
422 423
                    try ty_var (Hstr.find vars v.id) with Not_found ->
                      Loc.error ~loc:v.id_loc (UnboundTypeVar v.id)
424
                  end
425
              | PPTtyapp (q, tyl) ->
426 427 428 429
                  let ts = match q with
                    | Qident x when Mstr.mem x.id def ->
                        visit x.id
                    | Qident _ | Qdot _ ->
430
                        find_tysymbol th q
431
                  in
432
                  Loc.try2 ~loc:(qloc q) ty_app ts (List.map apply tyl)
433 434 435
              | PPTtuple tyl ->
                  let ts = ts_tuple (List.length tyl) in
                  ty_app ts (List.map apply tyl)
436 437 438 439
              | PPTarrow (ty1, ty2) ->
                  ty_func (apply ty1) (apply ty2)
              | PPTparen ty ->
                  apply ty
440 441 442 443 444 445
            in
            create_tysymbol id vl (Some (apply ty))
        | TDabstract | TDalgebraic _ ->
            create_tysymbol id vl None
        | TDrecord _ ->
            assert false
446
      in
447
      Hstr.add tysymbols x (Some ts);
448 449
      ts
  in
450 451 452 453 454 455 456 457 458
  let th' =
    let add_ts (abstr,alias) d =
      let ts = visit d.td_ident.id in
      if ts.ts_def = None then ts::abstr, alias else abstr, ts::alias in
    let abstr,alias = List.fold_left add_ts ([],[]) dl in
    try
      let th = List.fold_left add_ty_decl th abstr in
      let th = List.fold_left add_ty_decl th alias in
      th
459 460
    with ClashSymbol s ->
      Loc.error ~loc:(Mstr.find s def).td_loc (ClashSymbol s)
461
  in
462
  let csymbols = Hstr.create 17 in
463
  let decl d (abstr,algeb,alias) =
464
    let ts = match Hstr.find tysymbols d.td_ident.id with
465
      | None ->
466
          assert false
467
      | Some ts ->
468
          ts
469
    in
470 471 472
    match d.td_def with
      | TDabstract -> ts::abstr, algeb, alias
      | TDalias _ -> abstr, algeb, ts::alias
473
      | TDalgebraic cl ->
474
          let ht = Hstr.create 17 in
475
          let constr = List.length cl in
476
          let opaque = Stv.of_list ts.ts_args in
477
          let ty = ty_app ts (List.map ty_var ts.ts_args) in
478
          let projection (_,id,_,_) fty = match id with
479
            | None -> None
480
            | Some ({ id = x; id_loc = loc } as id) ->
481
                try
482
                  let pj = Hstr.find ht x in
483
                  let ty = Opt.get pj.ls_value in
484
                  ignore (Loc.try2 ~loc ty_equal_check ty fty);
485
                  Some pj
486 487
                with Not_found ->
                  let fn = create_user_id id in
488
                  let pj = create_fsymbol ~opaque fn [ty] fty in
489 490
                  Hstr.replace csymbols x loc;
                  Hstr.replace ht x pj;
491
                  Some pj
492
          in
493
          let constructor (loc, id, pl) =
494
            let tyl = tyl_of_params ~noop:true th' pl in
495
            let pjl = List.map2 projection pl tyl in
496
            Hstr.replace csymbols id.id loc;
497
            create_fsymbol ~opaque ~constr (create_user_id id) tyl ty, pjl
498
          in
499
          abstr, (ts, List.map constructor cl) :: algeb, alias
500
      | TDrecord _ ->
501
          assert false
502
  in
503 504 505 506 507 508
  let abstr,algeb,alias = List.fold_right decl dl ([],[],[]) in
  try
    let th = List.fold_left add_ty_decl th abstr in
    let th = if algeb = [] then th else add_data_decl th algeb in
    let th = List.fold_left add_ty_decl th alias in
    th
509 510
  with
    | ClashSymbol s ->
511
        Loc.error ~loc:(Hstr.find csymbols s) (ClashSymbol s)
512
    | RecordFieldMissing ({ ls_name = { id_string = s }} as cs,ls) ->
513
        Loc.error ~loc:(Hstr.find csymbols s) (RecordFieldMissing (cs,ls))
514
    | DuplicateRecordField ({ ls_name = { id_string = s }} as cs,ls) ->
515
        Loc.error ~loc:(Hstr.find csymbols s) (DuplicateRecordField (cs,ls))
516

517 518
let prepare_typedef td =
  if td.td_model then
519
    Loc.errorm ~loc:td.td_loc "model types are not allowed in pure theories";
520
  if td.td_vis <> Public then
521
    Loc.errorm ~loc:td.td_loc "pure types cannot be abstract or private";
522
  if td.td_inv <> [] then
523
    Loc.errorm ~loc:td.td_loc "pure types cannot have invariants";
524
  match td.td_def with
525 526 527
  | TDabstract | TDalgebraic _ | TDalias _ ->
      td
  | TDrecord fl ->
528 529
      let field { f_loc = loc; f_ident = id; f_pty = ty;
                  f_mutable = mut; f_ghost = gh } =
530 531
        if mut then Loc.errorm ~loc "a logic record field cannot be mutable";
        if gh then Loc.errorm ~loc "a logic record field cannot be ghost";
532
        loc, Some id, false, ty
533
      in
534 535
      (* constructor for type t is "mk t" (and not String.capitalize t) *)
      let id = { td.td_ident with id = "mk " ^ td.td_ident.id } in
536 537 538
      { td with td_def = TDalgebraic [td.td_loc, id, List.map field fl] }

let add_types dl th =
539
  add_types (List.map prepare_typedef dl) th
540

541
let add_logics dl th =
542
  let lsymbols = Hstr.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
543
  (* 1. create all symbols and make an environment with these symbols *)
544
  let create_symbol th d =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
545
    let id = d.ld_ident.id in
546
    let v = create_user_id d.ld_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
547
    let pl = tyl_of_params th d.ld_params in
548 549 550 551 552 553 554 555
    let ty = Opt.map (ty_of_pty th) d.ld_type in
    let opaque = opaque_tvs d.ld_params in
    (* for abstract lsymbols fresh tyvars are opaque *)
    let opaque = if d.ld_def = None && ty <> None then
      let atvs = List.fold_left ty_freevars Stv.empty pl in
      let vtvs = oty_freevars Stv.empty ty in
      Stv.union opaque (Stv.diff vtvs atvs)
    else opaque in
556 557
    let ls = create_lsymbol ~opaque v pl ty in
    Hstr.add lsymbols id ls;
558
    Loc.try2 ~loc:d.ld_loc add_param_decl th ls
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
559 560 561
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
562
  let type_decl d (abst,defn) =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
563
    let id = d.ld_ident.id in
564
    let ls = Hstr.find lsymbols id in
565
    let create_var (loc,x,_,_) ty =
566
      let id = match x with
567
        | Some id -> create_user_id id
568 569
        | None -> id_user "_" loc in
      create_vsymbol id ty in
570
    let vl = List.map2 create_var d.ld_params ls.ls_args in
571 572 573 574
    let add_var mvs (_,x,_,_) vs = match x with
      | Some {id = id} -> Mstr.add_new (DuplicateVar id) id (DTgvar vs) mvs
      | None -> mvs in
    let denv = List.fold_left2 add_var denv_empty d.ld_params vl in
575 576 577
    match d.ld_def, d.ld_type with
    | None, _ -> ls :: abst, defn
    | Some e, None -> (* predicate *)
578
        let f = dterm th' (fun _ -> None) denv e in
579
        let f = fmla ~strict:true ~keep_loc:true f in
580
        abst, (ls, vl, f) :: defn
581
    | Some e, Some ty -> (* function *)
582 583
        let e = { e with pp_desc = PPcast (e, ty) } in
        let t = dterm th' (fun _ -> None) denv e in
584
        let t = term ~strict:true ~keep_loc:true t in
585
        abst, (ls, vl, t) :: defn
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
586
  in
587
  let abst,defn = List.fold_right type_decl dl ([],[]) in
588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619
  (* 3. detect opacity *)
  let ldefns defn =
    let ht = Hls.create 3 in
    let add_ls (ls,_,_) =
      let tvs = oty_freevars Stv.empty ls.ls_value in
      let tvs = List.fold_left ty_freevars tvs ls.ls_args in
      Hls.replace ht ls tvs in
    List.iter add_ls defn;
    let compared s ls args value =
      let sbs = oty_match Mtv.empty ls.ls_value value in
      let sbs = List.fold_left2 ty_match sbs ls.ls_args args in
      let opq = try Hls.find ht ls with Not_found -> ls.ls_opaque in
      Mtv.fold (fun _ ty s -> ty_freevars s ty) (Mtv.set_diff sbs opq) s in
    let check_ld fixp (ls,_,t) =
      let opq = Hls.find ht ls in
      let npq = Stv.diff opq (t_app_fold compared Stv.empty t) in
      Hls.replace ht ls npq;
      fixp && Stv.equal opq npq in
    let rec fixp () =
      if not (List.fold_left check_ld true defn) then fixp () in
    fixp ();
    let mk_sbs sbs ({ls_name = id} as ls,_,_) =
      let opaque = Stv.union ls.ls_opaque (Hls.find ht ls) in
      if Stv.equal ls.ls_opaque opaque then sbs else
      let nls = create_lsymbol ~opaque (id_clone id) ls.ls_args ls.ls_value in
      Mls.add ls nls sbs in
    let sbs = List.fold_left mk_sbs Mls.empty defn in
    let mk_ld (ls,vl,t) =
      let get_ls ls = Mls.find_def ls ls sbs in
      make_ls_defn (get_ls ls) vl (t_s_map (fun ty -> ty) get_ls t) in
    List.map mk_ld defn
  in
620
  let th = List.fold_left add_param_decl th abst in
621
  let th = if defn = [] then th else add_logic_decl th (ldefns defn) in
622
  th
623

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
624
let add_prop k loc s f th =
625
  let pr = create_prsymbol (create_user_id s) in
626
  let f = type_fmla th (fun _ -> None) f in
627
  Loc.try4 ~loc add_prop_decl th k pr f
628

629
let loc_of_id id = Opt.get id.Ident.id_loc
630

631
let add_inductives s dl th =
632
  (* 1. create all symbols and make an environment with these symbols *)
633
  let psymbols = Hstr.create 17 in
634
  let create_symbol th d =
635
    let id = d.in_ident.id in
636
    let v = create_user_id d.in_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
637
    let pl = tyl_of_params th d.in_params in
638
    let opaque = opaque_tvs d.in_params in
639
    let ps = create_psymbol ~opaque v pl in
640
    Hstr.add psymbols id ps;
641
    Loc.try2 ~loc:d.in_loc add_param_decl th ps
642
  in
643 644
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
645
  let propsyms = Hstr.create 17 in
646
  let type_decl d =
647
    let id = d.in_ident.id in
648
    let ps = Hstr.find psymbols id in
649
    let clause (loc, id, f) =
650
      Hstr.replace propsyms id.id loc;
651
      let f = type_fmla th' (fun _ -> None) f in
652
      create_prsymbol (create_user_id id), f
653 654 655
    in
    ps, List.map clause d.in_def
  in
656
  try add_ind_decl th s (List.map type_decl dl)
Andrei Paskevich's avatar
Andrei Paskevich committed
657
  with
658
  | ClashSymbol s ->
659
      Loc.error ~loc:(Hstr.find propsyms s) (ClashSymbol s)
660
  | InvalidIndDecl (ls,pr) ->
661
      Loc.error ~loc:(loc_of_id pr.pr_name) (InvalidIndDecl (ls,pr))
662
  | NonPositiveIndDecl (ls,pr,s) ->
663
      Loc.error ~loc:(loc_of_id pr.pr_name) (NonPositiveIndDecl (ls,pr,s))
664

665
(* parse declarations *)
666

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
667
let prop_kind = function
668 669 670
  | Kaxiom -> Paxiom
  | Kgoal -> Pgoal
  | Klemma -> Plemma
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
671

672 673
let find_theory env lenv q = match q with
  | Qident { id = id } -> (* local theory *)
674
      begin try Mstr.find id lenv
Andrei Paskevich's avatar
Andrei Paskevich committed
675
      with Not_found -> read_lib_theory env [] id end
676 677
  | Qdot (p, { id = id }) -> (* theory in file f *)
      read_lib_theory env (string_list_of_qualid p) id
678

679 680
let rec clone_ns kn sl path ns2 ns1 s =
  let qualid fmt path = Pp.print_list
681 682
    (fun fmt () -> Format.pp_print_char fmt '.')
    Format.pp_print_string fmt (List.rev path) in
683
  let s = Mstr.fold (fun nm ns1 acc ->
684 685
    let ns2 = Mstr.find_def empty_ns nm ns2.ns_ns in
    clone_ns kn sl (nm::path) ns2 ns1 acc) ns1.ns_ns s
686
  in
687
  let inst_ts = Mstr.fold (fun nm ts1 acc ->
688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708
    match Mstr.find_opt nm ns2.ns_ts with
    | Some ts2 when ts_equal ts1 ts2 -> acc
    | Some _ when not (Sid.mem ts1.ts_name sl) ->
        raise (NonLocal ts1.ts_name)
    | Some _ when ts1.ts_def <> None ->
        raise (CannotInstantiate ts1.ts_name)
    | Some ts2 ->
        begin match (Mid.find ts1.ts_name kn).d_node with
          | Decl.Dtype _ -> Mts.add_new (ClashSymbol nm) ts1 ts2 acc
          | _ -> raise (CannotInstantiate ts1.ts_name)
        end
    | None when not (Sid.mem ts1.ts_name sl) -> acc
    | None when ts1.ts_def <> None -> acc
    | None ->
        begin match (Mid.find ts1.ts_name kn).d_node with
          | Decl.Dtype _ -> Loc.errorm
              "type symbol %a not found in the target theory"
              qualid (nm::path)
          | _ -> acc
        end)
    ns1.ns_ts s.inst_ts
709
  in
710
  let inst_ls = Mstr.fold (fun nm ls1 acc ->
711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729
    match Mstr.find_opt nm ns2.ns_ls with
    | Some ls2 when ls_equal ls1 ls2 -> acc
    | Some _ when not (Sid.mem ls1.ls_name sl) ->
       raise (NonLocal ls1.ls_name)
    | Some ls2 ->
        begin match (Mid.find ls1.ls_name kn).d_node with
          | Decl.Dparam _ -> Mls.add_new (ClashSymbol nm) ls1 ls2 acc
          | _ -> raise (CannotInstantiate ls1.ls_name)
        end
    | None when not (Sid.mem ls1.ls_name sl) -> acc
    | None ->
        begin match (Mid.find ls1.ls_name kn).d_node with
          | Decl.Dparam _ -> Loc.errorm
              "%s symbol %a not found in the target theory"
              (if ls1.ls_value <> None then "function" else "predicate")
              qualid (nm::path)
          | _ -> acc
        end)
    ns1.ns_ls s.inst_ls
730 731 732
  in
  { s with inst_ts = inst_ts; inst_ls = inst_ls }

733
let add_decl loc th = function
734
  | Ptree.TypeDecl dl ->
735
      add_types dl th
736
  | Ptree.LogicDecl dl ->
737
      add_logics dl th
738
  | Ptree.IndDecl (s, dl) ->
739
      add_inductives s dl th
740
  | Ptree.PropDecl (k, s, f) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
741
      add_prop (prop_kind k) loc s f th
742
  | Ptree.Meta (id, al) ->
743
      let convert = function
744
        | PMAty (PPTtyapp (q,[]))
745
                   -> MAts (find_tysymbol th q)
746
        | PMAty ty -> MAty (ty_of_pty th ty)
747 748 749
        | PMAfs q  -> MAls (find_fsymbol th q)
        | PMAps q  -> MAls (find_psymbol th q)
        | PMApr q  -> MApr (find_prop th q)
750
        | PMAstr s -> MAstr s
751
        | PMAint i -> MAint i
752
      in
753
      let add s = add_meta th (lookup_meta s) (List.map convert al) in
754
      Loc.try1 ~loc add id.id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
755

756 757
let add_decl loc th d =
  if Debug.test_flag debug_parse_only then th else
758
  Loc.try3 ~loc add_decl loc th d
759

760 761 762
let type_inst th t s =
  let add_inst s = function
    | CSns (loc,p,q) ->
763 764
      let ns1 = Opt.fold find_namespace_ns t.th_export p in
      let ns2 = Opt.fold find_namespace_ns (get_namespace th) q in
765
      Loc.try6 ~loc clone_ns t.th_known t.th_local [] ns2 ns1 s
766
    | CStsym (loc,p,[],PPTtyapp (q,[])) ->
767 768
      let ts1 = find_tysymbol_ns t.th_export p in
      let ts2 = find_tysymbol th q in
769
      if Mts.mem ts1 s.inst_ts
770
      then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string);
771
      { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
772
    | CStsym (loc,p,tvl,pty) ->
773
      let ts1 = find_tysymbol_ns t.th_export p in
774 775 776
      let id = id_user (ts1.ts_name.id_string ^ "_subst") loc in
      let tvl = List.map (fun id -> create_user_tv id.id) tvl in
      let def = Some (ty_of_pty th pty) in
777
      let ts2 = Loc.try3 ~loc create_tysymbol id tvl def in
778
      if Mts.mem ts1 s.inst_ts
779
      then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string);
780
      { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
781
    | CSfsym (loc,p,q) ->
782 783
      let ls1 = find_fsymbol_ns t.th_export p in
      let ls2 = find_fsymbol th q in
784
      if Mls.mem ls1 s.inst_ls
785
      then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string);
Jean-Christophe Filliâtre's avatar