typing.ml 31.4 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
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
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
let rec print_qualid fmt = function
59 60
  | Qdot (p, id) -> Format.fprintf fmt "%a.%s" print_qualid p id.id_str
  | Qident id    -> Format.fprintf fmt "%s" id.id_str
61

62 63
let string_list_of_qualid q =
  let rec sloq acc = function
64 65
    | Qdot (p, id) -> sloq (id.id_str :: acc) p
    | Qident id -> id.id_str :: acc in
66
  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
(** Parsing types *)

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

123
let opaque_tvs args =
124
  let rec opaque_tvs acc = function
125 126 127 128 129 130
    | 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
131
  List.fold_left (fun acc (_,_,_,ty) -> opaque_tvs acc ty) Stv.empty args
132

133
(** typing using destructive type variables
134

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

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

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

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

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

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

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

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

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

209 210 211
let mk_closure loc ls =
  let mk dt = Dterm.dterm ~loc dt in
  let mk_v i _ =
212 213
    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
214
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
215
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
216

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

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

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

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

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

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

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

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

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

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

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

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

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

648
(* parse declarations *)
649

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

657 658
let rec clone_ns