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

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

21
(** debug flags *)
22

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

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

29
(** errors *)
30

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

35
(** lazy declaration of tuples *)
36

37 38 39 40
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

41 42 43 44 45 46
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)
47

48
(** symbol lookup *)
49 50

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

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

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

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

67
exception UnboundSymbol of qualid
68

69
let find_qualid get_id find ns q =
70 71 72
  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
73
  if Debug.test_flag Glob.flag then Glob.use (qloc_last q) (get_id r);
74
  r
75

76 77 78
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
79

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

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

90 91 92 93 94
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
95

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

99 100
(** Parsing types *)

Andrei Paskevich's avatar
Andrei Paskevich committed
101
let ty_of_pty ?(noop=true) uc pty =
102
  let rec get_ty = function
103
    | PTtyvar ({id_loc = loc}, true) when noop ->
104 105
        Loc.errorm ~loc "Opaqueness@ annotations@ are@ only@ \
          allowed@ in@ function@ and@ predicate@ prototypes"
106
    | PTtyvar ({id_str = x}, _) ->
107
        ty_var (tv_of_string x)
108
    | PTtyapp (q, tyl) ->
109
        let ts = find_tysymbol uc q in
110
        let tyl = List.map get_ty tyl in
111
        Loc.try2 ~loc:(qloc q) ty_app ts tyl
112
    | PTtuple tyl ->
113 114
        let ts = ts_tuple (List.length tyl) in
        ty_app ts (List.map get_ty tyl)
115
    | PTarrow (ty1, ty2) ->
116
        ty_func (get_ty ty1) (get_ty ty2)
117
    | PTparen ty ->
118 119 120 121
        get_ty ty
  in
  get_ty pty

122
let opaque_tvs args =
123
  let rec opaque_tvs acc = function
124 125 126 127 128 129
    | PTtyvar (id, true) -> Stv.add (tv_of_string id.id_str) acc
    | PTtyvar (_, false) -> acc
    | PTtyapp (_, pl)
    | PTtuple pl -> List.fold_left opaque_tvs acc pl
    | PTarrow (ty1, ty2) -> opaque_tvs (opaque_tvs acc ty1) ty2
    | PTparen ty -> opaque_tvs acc ty in
130
  List.fold_left (fun acc (_,_,_,ty) -> opaque_tvs acc ty) Stv.empty args
131

132
(** typing using destructive type variables
133

134 135 136 137 138 139
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
140

141 142
(** Typing patterns, terms, and formulas *)

143
let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
144 145 146 147
  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
148 149

let parse_record ~loc uc get_val fl =
150
  let fl = List.map (fun (q,e) -> find_lsymbol uc q, e) fl in
151 152 153 154
  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

155 156
let rec dpattern uc { pat_desc = desc; pat_loc = loc } =
  Dterm.dpattern ~loc (match desc with
157 158 159
    | Ptree.Pwild -> DPwild
    | Ptree.Pvar x -> DPvar (create_user_id x)
    | Ptree.Papp (q,pl) ->
160
        let pl = List.map (dpattern uc) pl in
161
        DPapp (find_lsymbol uc q, pl)
162
    | Ptree.Ptuple pl ->
163 164
        let pl = List.map (dpattern uc) pl in
        DPapp (fs_tuple (List.length pl), pl)
165
    | Ptree.Prec fl ->
166 167 168 169 170
        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)
171
    | Ptree.Pas (p, x) -> DPas (dpattern uc p, create_user_id x)
172 173
    | Ptree.Por (p, q) -> DPor (dpattern uc p, dpattern uc q)
    | Ptree.Pcast (p, ty) -> DPcast (dpattern uc p, ty_of_pty uc ty))
174 175 176 177

let quant_var uc (loc, id, gh, ty) =
  assert (not gh);
  let ty = match ty with
178
    | Some ty -> dty_of_ty (ty_of_pty uc ty)
179
    | None    -> dty_fresh () in
180
  Opt.map create_user_id id, ty, Some loc
181

182 183 184 185 186 187 188 189 190 191 192 193 194 195
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)

196 197
let chainable_op uc op =
  (* non-bool -> non-bool -> bool *)
198
  op.id_str = "infix =" || op.id_str = "infix <>" ||
199 200 201 202 203 204
  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
205

206 207
type global_vs = Ptree.qualid -> vsymbol option

208 209 210
let mk_closure loc ls =
  let mk dt = Dterm.dterm ~loc dt in
  let mk_v i _ =
211 212
    Some (id_user ("y" ^ string_of_int i) loc), dty_fresh (), None in
  let mk_t (id, dty, _) = mk (DTvar ((Opt.get id).pre_name, dty)) in
213
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
214
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
215

216
let rec dterm uc gvars denv {term_desc = desc; term_loc = loc} =
217 218 219
  let func_app e el =
    List.fold_left (fun e1 (loc, e2) ->
      DTfapp (Dterm.dterm ~loc e1, e2)) e el
220
  in
221 222 223 224
  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)
225
  in
226 227
  let qualid_app q el = match gvars q with
    | Some vs -> func_app (DTgvar vs) el
228
    | None ->
229
        let ls = find_lsymbol uc q in
230
        apply_ls (qloc q) ls [] ls.ls_args el
231
  in
232
  let qualid_app q el = match q with
233
    | Qident {id_str = n} ->
234
        (match denv_get_opt denv n with
235 236 237 238
        | Some d -> func_app d el
        | None -> qualid_app q el)
    | _ -> qualid_app q el
  in
239 240
  let rec unfold_app e1 e2 el = match e1.term_desc with
    | Tapply (e11,e12) ->
241
        let e12 = dterm uc gvars denv e12 in
242 243 244
        unfold_app e11 e12 ((e1.term_loc, e2)::el)
    | Tident q ->
        qualid_app q ((e1.term_loc, e2)::el)
245 246
    | _ ->
        func_app (DTfapp (dterm uc gvars denv e1, e2)) el
247
  in
248
  Dterm.dterm ~loc (match desc with
249
  | Ptree.Tident q ->
250
      qualid_app q []
251
  | Ptree.Tidapp (q, tl) ->
252 253
      let tl = List.map (dterm uc gvars denv) tl in
      DTapp (find_lsymbol uc q, tl)
254
  | Ptree.Tapply (e1, e2) ->
255
      unfold_app e1 (dterm uc gvars denv e2) []
256
  | Ptree.Ttuple tl ->
257
      let tl = List.map (dterm uc gvars denv) tl in
258
      DTapp (fs_tuple (List.length tl), tl)
259 260 261 262
  | Ptree.Tinfix (e12, op2, e3)
  | Ptree.Tinnfix (e12, op2, e3) ->
      let make_app de1 op de2 = if op.id_str = "infix <>" then
        let op = { op with id_str = "infix =" } in
263
        let ls = find_lsymbol uc (Qident op) in
264 265
        DTnot (Dterm.dterm ~loc (DTapp (ls, [de1;de2])))
      else
266
        DTapp (find_lsymbol uc (Qident op), [de1;de2])
267 268 269 270 271 272 273
      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
274
            DTbinop (DTand, de12, de23)
275
        | [] -> assert false in
276 277
      let rec get_chain e12 acc = match e12.term_desc with
        | Tinfix (e1, op1, e2) when chainable_op uc op1 ->
278
            get_chain e1 ((op1, dterm uc gvars denv e2) :: acc)
279
        | _ -> e12, acc in
280
      let ch = [op2, dterm uc gvars denv e3] in
281 282
      let e1, ch = if chainable_op uc op2
        then get_chain e12 ch else e12, ch in
283
      make_chain (dterm uc gvars denv e1) ch
284
  | Ptree.Tconst c ->
285
      DTconst c
286
  | Ptree.Tlet (x, e1, e2) ->
287
      let id = create_user_id x in
288
      let e1 = dterm uc gvars denv e1 in
289
      let denv = denv_add_let denv e1 id in
290
      let e2 = dterm uc gvars denv e2 in
291
      DTlet (e1, id, e2)
292
  | Ptree.Tmatch (e1, bl) ->
293
      let e1 = dterm uc gvars denv e1 in
294 295 296
      let branch (p, e) =
        let p = dpattern uc p in
        let denv = denv_add_pat denv p in
297
        p, dterm uc gvars denv e in
298
      DTcase (e1, List.map branch bl)
299
  | Ptree.Tif (e1, e2, e3) ->
300 301 302
      let e1 = dterm uc gvars denv e1 in
      let e2 = dterm uc gvars denv e2 in
      let e3 = dterm uc gvars denv e3 in
303
      DTif (e1, e2, e3)
304
  | Ptree.Ttrue ->
305
      DTtrue
306
  | Ptree.Tfalse ->
307
      DTfalse
308
  | Ptree.Tunop (Ptree.Tnot, e1) ->
309
      DTnot (dterm uc gvars denv e1)
310
  | Ptree.Tbinop (e1, op, e2) ->
311 312
      let e1 = dterm uc gvars denv e1 in
      let e2 = dterm uc gvars denv e2 in
313
      let op = match op with
314 315 316 317 318 319
        | Ptree.Tand -> DTand
        | Ptree.Tand_asym -> DTand_asym
        | Ptree.Tor -> DTor
        | Ptree.Tor_asym -> DTor_asym
        | Ptree.Timplies -> DTimplies
        | Ptree.Tiff -> DTiff in
320
      DTbinop (op, e1, e2)
321
  | Ptree.Tquant (q, uqu, trl, e1) ->
322 323
      let qvl = List.map (quant_var uc) uqu in
      let denv = denv_add_quant denv qvl in
324 325 326
      let dterm e = dterm uc gvars denv e in
      let trl = List.map (List.map dterm) trl in
      let e1 = dterm e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
327 328 329 330 331
      let q = match q with
        | Ptree.Tforall -> DTforall
        | Ptree.Texists -> DTexists
        | Ptree.Tlambda -> DTlambda in
      DTquant (q, qvl, trl, e1)
332
  | Ptree.Trecord fl ->
333
      let get_val cs pj = function
334
        | Some e -> dterm uc gvars denv e
335 336 337
        | None -> Loc.error ~loc (RecordFieldMissing (cs,pj)) in
      let cs, fl = parse_record ~loc uc get_val fl in
      DTapp (cs, fl)
338
  | Ptree.Tupdate (e1, fl) ->
339
      let e1 = dterm uc gvars denv e1 in
340 341
      let re = is_reusable e1 in
      let v = if re then e1 else mk_var "_q " e1 in
342
      let get_val _ pj = function
343
        | Some e -> dterm uc gvars denv e
344
        | None -> Dterm.dterm ~loc (DTapp (pj,[v])) in
345
      let cs, fl = parse_record ~loc uc get_val fl in
346 347
      let d = DTapp (cs, fl) in
      if re then d else mk_let ~loc "_q " e1 d
348
  | Ptree.Tnamed (Lpos uloc, e1) ->
349
      DTuloc (dterm uc gvars denv e1, uloc)
350
  | Ptree.Tnamed (Lstr lab, e1) ->
351
      DTlabel (dterm uc gvars denv e1, Slab.singleton lab)
352
  | Ptree.Tcast (e1, ty) ->
353
      DTcast (dterm uc gvars denv e1, ty_of_pty uc ty))
354 355

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

357 358
let type_term uc gvars t =
  let t = dterm uc gvars denv_empty t in
359
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
360

361 362
let type_fmla uc gvars f =
  let f = dterm uc gvars denv_empty f in
363
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
364

365
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
366

Andrei Paskevich's avatar
Andrei Paskevich committed
367
let tyl_of_params ?(noop=false) uc pl =
368 369 370
  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
371
    ty_of_pty ~noop uc ty in
372 373
  List.map ty_of_param pl

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

499 500
let prepare_typedef td =
  if td.td_model then
501
    Loc.errorm ~loc:td.td_loc "model types are not allowed in pure theories";
502
  if td.td_vis <> Public then
503
    Loc.errorm ~loc:td.td_loc "pure types cannot be abstract or private";
504
  if td.td_inv <> [] then
505
    Loc.errorm ~loc:td.td_loc "pure types cannot have invariants";
506
  match td.td_def with
507 508 509
  | TDabstract | TDalgebraic _ | TDalias _ ->
      td
  | TDrecord fl ->
510 511
      let field { f_loc = loc; f_ident = id; f_pty = ty;
                  f_mutable = mut; f_ghost = gh } =
512 513
        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";
514
        loc, Some id, false, ty
515
      in
516
      (* constructor for type t is "mk t" (and not String.capitalize t) *)
517
      let id = { td.td_ident with id_str = "mk " ^ td.td_ident.id_str } in
518 519 520
      { td with td_def = TDalgebraic [td.td_loc, id, List.map field fl] }

let add_types dl th =
521
  add_types (List.map prepare_typedef dl) th
522

523
let add_logics dl th =
524
  let lsymbols = Hstr.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
525
  (* 1. create all symbols and make an environment with these symbols *)
526
  let create_symbol th d =
527
    let id = d.ld_ident.id_str in
528
    let v = create_user_id d.ld_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
529
    let pl = tyl_of_params th d.ld_params in
530 531 532 533 534 535 536 537
    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
538 539
    let ls = create_lsymbol ~opaque v pl ty in
    Hstr.add lsymbols id ls;
540
    Loc.try2 ~loc:d.ld_loc add_param_decl th ls
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
541 542 543
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
544
  let type_decl d (abst,defn) =
545
    let id = d.ld_ident.id_str in
546
    let ls = Hstr.find lsymbols id in
547
    let create_var (loc,x,_,_) ty =
548
      let id = match x with
549
        | Some id -> create_user_id id
550 551
        | None -> id_user "_" loc in
      create_vsymbol id ty in
552
    let vl = List.map2 create_var d.ld_params ls.ls_args in
553
    let add_var mvs (_,x,_,_) vs = match x with
554
      | Some {id_str = x} -> Mstr.add_new (DuplicateVar x) x (DTgvar vs) mvs
555 556
      | None -> mvs in
    let denv = List.fold_left2 add_var denv_empty d.ld_params vl in
557 558 559
    match d.ld_def, d.ld_type with
    | None, _ -> ls :: abst, defn
    | Some e, None -> (* predicate *)
560
        let f = dterm th' (fun _ -> None) denv e in
561
        let f = fmla ~strict:true ~keep_loc:true f in
562
        abst, (ls, vl, f) :: defn
563
    | Some e, Some ty -> (* function *)
564
        let e = { e with term_desc = Tcast (e, ty) } in
565
        let t = dterm th' (fun _ -> None) denv e in
566
        let t = term ~strict:true ~keep_loc:true t in
567
        abst, (ls, vl, t) :: defn
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
568
  in
569
  let abst,defn = List.fold_right type_decl dl ([],[]) in
570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601
  (* 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
602
  let th = List.fold_left add_param_decl th abst in
603
  let th = if defn = [] then th else add_logic_decl th (ldefns defn) in
604
  th
605

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
606
let add_prop k loc s f th =
607
  let pr = create_prsymbol (create_user_id s) in
608
  let f = type_fmla th (fun _ -> None) f in
609
  Loc.try4 ~loc add_prop_decl th k pr f
610

611
let loc_of_id id = Opt.get id.Ident.id_loc
612

613
let add_inductives s dl th =
614
  (* 1. create all symbols and make an environment with these symbols *)
615
  let psymbols = Hstr.create 17 in
616
  let create_symbol th d =
617
    let id = d.in_ident.id_str in
618
    let v = create_user_id d.in_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
619
    let pl = tyl_of_params th d.in_params in
620
    let opaque = opaque_tvs d.in_params in
621
    let ps = create_psymbol ~opaque v pl in
622
    Hstr.add psymbols id ps;
623
    Loc.try2 ~loc:d.in_loc add_param_decl th ps
624
  in
625 626
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
627
  let propsyms = Hstr.create 17 in
628
  let type_decl d =
629
    let id = d.in_ident.id_str in
630
    let ps = Hstr.find psymbols id in
631
    let clause (loc, id, f) =
632
      Hstr.replace propsyms id.id_str loc;
633
      let f = type_fmla th' (fun _ -> None) f in
634
      create_prsymbol (create_user_id id), f
635 636 637
    in
    ps, List.map clause d.in_def
  in
638
  try add_ind_decl th s (List.map type_decl dl)
Andrei Paskevich's avatar
Andrei Paskevich committed
639
  with
640
  | ClashSymbol s ->
641
      Loc.error ~loc:(Hstr.find propsyms s) (ClashSymbol s)
642
  | InvalidIndDecl (ls,pr) ->
643
      Loc.error ~loc:(loc_of_id pr.pr_name) (InvalidIndDecl (ls,pr))
644
  | NonPositiveIndDecl (ls,pr,s) ->
645
      Loc.error ~loc:(loc_of_id pr.pr_name) (NonPositiveIndDecl (ls,pr,s))
646

647
(* parse declarations *)
648

649
let find_theory env lenv q = match q with
650
  | Qident { id_str = id } -> (* local theory *)
651
      begin try Mstr.find id lenv
652
      with Not_found -> read_theory env [] id end
653
  | Qdot (p, { id_str = id }) -> (* theory in file f *)
654
      read_theory env (string_list_of_qualid p) id
655

656 657
let rec clone_ns kn sl path ns2 ns1 s =
  let qualid fmt path = Pp.print_list
658 659
    (fun fmt () -> Format.pp_print_char fmt '.')
    Format.pp_print_string fmt (List.rev path) in
660
  let s = Mstr.fold (fun nm ns1 acc ->
661 662
    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
663
  in
664
  let inst_ts = Mstr.fold (fun nm ts1 acc ->
665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685
    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
686
  in
687
  let inst_ls = Mstr.fold (fun nm ls1 acc ->
688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706
    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
707 708 709
  in
  { s with inst_ts = inst_ts; inst_ls = inst_ls }

710
let add_decl loc th = function
711
  | Ptree.Dtype dl ->
712
      add_types dl th
713
  | Ptree.Dlogic dl ->
714
      add_logics dl th
715
  | Ptree.Dind (s, dl) ->
716
      add_inductives s dl th
717 718 719
  | Ptree.Dprop (k, s, f) ->
      add_prop k loc s f th
  | Ptree.Dmeta (id, al) ->
720
      let convert = function
721 722 723 724 725 726