typing.ml 34.8 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   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 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
let rec elim_opaque = function
  | PTtyvar (id, _) -> PTtyvar (id, false)
  | PTtyapp (ts, pl) -> PTtyapp (ts, List.map elim_opaque pl)
  | PTtuple pl -> PTtuple (List.map elim_opaque pl)
  | PTarrow (ty1, ty2) -> PTarrow (elim_opaque ty1, elim_opaque ty2)
  | PTparen ty -> PTparen (elim_opaque ty)

let rec opaque_tvs acc = function
  | 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

let opaque_tvs_l args =
139
  List.fold_left (fun acc (_,_,_,ty) -> opaque_tvs acc ty) Stv.empty args
140

141
(** typing using destructive type variables
142

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

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

152
let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
153 154 155 156
  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
157 158

let parse_record ~loc uc get_val fl =
159
  let fl = List.map (fun (q,e) -> find_lsymbol uc q, e) fl in
160 161 162 163
  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

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

let quant_var uc (loc, id, gh, ty) =
  assert (not gh);
  let ty = match ty with
187
    | Some ty -> dty_of_ty (ty_of_pty uc ty)
188
    | None    -> dty_fresh () in
189
  Opt.map create_user_id id, ty, Some loc
190

191 192 193 194 195 196 197 198 199 200 201 202 203 204
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)

205 206
let chainable_op uc op =
  (* non-bool -> non-bool -> bool *)
207
  op.id_str = "infix =" || op.id_str = "infix <>" ||
208 209 210 211 212 213
  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
214

215 216
type global_vs = Ptree.qualid -> vsymbol option

217 218 219
let mk_closure loc ls =
  let mk dt = Dterm.dterm ~loc dt in
  let mk_v i _ =
220 221
    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
222
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
223
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
224

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

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

380 381
let type_term uc gvars t =
  let t = dterm uc gvars denv_empty t in
382
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
383

384 385
let type_fmla uc gvars f =
  let f = dterm uc gvars denv_empty f in
386
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
387

388
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
389

Andrei Paskevich's avatar
Andrei Paskevich committed
390
let tyl_of_params ?(noop=false) uc pl =
391 392 393
  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
394
    ty_of_pty ~noop uc ty in
395 396
  List.map ty_of_param pl

397
let add_types dl th =
398
  let def = List.fold_left
399
    (fun def d ->
400
      let id = d.td_ident.id_str in
401
      Mstr.add_new (Loc.Located (d.td_loc, ClashSymbol id)) id d def)
402
    Mstr.empty dl
403
  in
404
  let tysymbols = Hstr.create 17 in
405
  let rec visit x =
406
    let d = Mstr.find x def in
Clément Fumex's avatar
Clément Fumex committed
407 408 409
    try match Hstr.find tysymbols x with
      | None -> Loc.errorm ~loc:d.td_loc "Cyclic type definition"
      | Some ts -> ts
410
    with Not_found ->
411 412
      Hstr.add tysymbols x None;
      let vars = Hstr.create 17 in
413
      let vl = List.map (fun id ->
414 415 416 417
        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;
418
        i) d.td_params
419
      in
420
      let id = create_user_id d.td_ident in
421
      let ts = match d.td_def with
422 423
        | TDalias ty ->
            let rec apply = function
424
              | PTtyvar (v, _) ->
425
                  begin
426 427
                    try ty_var (Hstr.find vars v.id_str) with Not_found ->
                      Loc.error ~loc:v.id_loc (UnboundTypeVar v.id_str)
428
                  end
429
              | PTtyapp (q, tyl) ->
430
                  let ts = match q with
431 432
                    | Qident x when Mstr.mem x.id_str def ->
                        visit x.id_str
433
                    | Qident _ | Qdot _ ->
434
                        find_tysymbol th q
435
                  in
436
                  Loc.try2 ~loc:(qloc q) ty_app ts (List.map apply tyl)
437
              | PTtuple tyl ->
438 439
                  let ts = ts_tuple (List.length tyl) in
                  ty_app ts (List.map apply tyl)
440
              | PTarrow (ty1, ty2) ->
441
                  ty_func (apply ty1) (apply ty2)
442
              | PTparen ty ->
443
                  apply ty
444
            in
Clément Fumex's avatar
Clément Fumex committed
445 446 447 448 449 450 451 452 453
            create_tysymbol id vl (Alias (apply ty))
        | TDrange (lo,hi) ->
            let ir = { Number.ir_lower = lo;
                       Number.ir_upper = hi } in
            Loc.try2 ~loc:d.td_loc create_tysymbol id vl (Range ir)
        | TDfloat (eb,sb) ->
            let fp = { Number.fp_exponent_digits = eb;
                       Number.fp_significand_digits = sb } in
            Loc.try2 ~loc:d.td_loc create_tysymbol id vl (Float fp)
454
        | TDabstract | TDalgebraic _ ->
Clément Fumex's avatar
Clément Fumex committed
455
            create_tysymbol id vl NoDef
456 457
        | TDrecord _ ->
            assert false
458
      in
459
      Hstr.add tysymbols x (Some ts);
460 461
      ts
  in
462 463
  let th' =
    let add_ts (abstr,alias) d =
464
      let ts = visit d.td_ident.id_str in
Clément Fumex's avatar
Clément Fumex committed
465 466
      if is_alias_type_def ts.ts_def then
        abstr, ts::alias else ts::abstr, alias in
467 468 469 470 471
    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
472 473
    with ClashSymbol s ->
      Loc.error ~loc:(Mstr.find s def).td_loc (ClashSymbol s)
474
  in
475
  let csymbols = Hstr.create 17 in
476
  let decl d (abstr,algeb,alias) =
477
    let ts = match Hstr.find tysymbols d.td_ident.id_str with
478
      | None ->
479
          assert false
480
      | Some ts ->
481
          ts
482
    in
483
    match d.td_def with
Clément Fumex's avatar
Clément Fumex committed
484 485 486 487
      | TDabstract | TDrange _ | TDfloat _ ->
          ts::abstr, algeb, alias
      | TDalias _ ->
          abstr, algeb, ts::alias
488
      | TDalgebraic cl ->
489
          let ht = Hstr.create 17 in
490
          let constr = List.length cl in
491
          let opaque = Stv.of_list ts.ts_args in
492
          let ty = ty_app ts (List.map ty_var ts.ts_args) in
493
          let projection (_,id,_,_) fty = match id with
494
            | None -> None
495
            | Some ({ id_str = x; id_loc = loc } as id) ->
496
                try
497
                  let pj = Hstr.find ht x in
498
                  let ty = Opt.get pj.ls_value in
499
                  ignore (Loc.try2 ~loc ty_equal_check ty fty);
500
                  Some pj
501 502
                with Not_found ->
                  let fn = create_user_id id in
503
                  let pj = create_fsymbol ~opaque fn [ty] fty in
504 505
                  Hstr.replace csymbols x loc;
                  Hstr.replace ht x pj;
506
                  Some pj
507
          in
508
          let constructor (loc, id, pl) =
509
            let tyl = tyl_of_params ~noop:true th' pl in
510
            let pjl = List.map2 projection pl tyl in
511
            Hstr.replace csymbols id.id_str loc;
512
            create_fsymbol ~opaque ~constr (create_user_id id) tyl ty, pjl
513
          in
514
          abstr, (ts, List.map constructor cl) :: algeb, alias
515
      | TDrecord _ ->
516
          assert false
517
  in
518
  let abstr,algeb,alias = List.fold_right decl dl ([],[],[]) in
Clément Fumex's avatar
Clément Fumex committed
519 520 521 522
  let add_ty_decl uc ts =
    let uc = add_ty_decl uc ts in
    match ts.ts_def with
    | NoDef | Alias _ -> uc
523
    | Range rg ->
Clément Fumex's avatar
Clément Fumex committed
524 525 526 527 528
        (* FIXME: "t'to_int" is probably better *)
        let nm = ts.ts_name.id_string ^ "'int" in
        let id = id_derive nm ts.ts_name in
        let pj = create_fsymbol id [ty_app ts []] ty_int in
        let uc = add_param_decl uc pj in
529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548
        let uc = add_meta uc meta_range [MAts ts; MAls pj] in
        (* create max attribute *)
        let nm = ts.ts_name.id_string ^ "'maxInt" in
        let id = id_derive nm ts.ts_name in
        let ls = create_fsymbol id [] ty_int  in
        let t =
          t_const Number.(ConstInt (int_const_dec (BigInt.to_string rg.ir_upper)))
            ty_int
        in
        let uc = add_logic_decl uc [make_ls_defn ls [] t] in
        (* create min attribute *)
        let nm = ts.ts_name.id_string ^ "'minInt" in
        let id = id_derive nm ts.ts_name in
        let ls = create_fsymbol id [] ty_int  in
        let t =
          t_const Number.(ConstInt (int_const_dec (BigInt.to_string rg.ir_lower)))
            ty_int
        in
        add_logic_decl uc [make_ls_defn ls [] t]
    | Float fmt ->
Clément Fumex's avatar
Clément Fumex committed
549 550 551 552 553 554 555 556 557 558
        (* FIXME: "t'to_real" is probably better *)
        let nm = ts.ts_name.id_string ^ "'real" in
        let id = id_derive nm ts.ts_name in
        let pj = create_fsymbol id [ty_app ts []] ty_real in
        let uc = add_param_decl uc pj in
        (* FIXME: "t'is_finite" is probably better *)
        let nm = ts.ts_name.id_string ^ "'isFinite" in
        let id = id_derive nm ts.ts_name in
        let iF = create_psymbol id [ty_app ts []] in
        let uc = add_param_decl uc iF in
559 560 561 562 563 564 565 566 567 568 569 570 571
        let uc = add_meta uc meta_float [MAts ts; MAls pj; MAls iF] in
        (* create exponent digits attribute *)
        let nm = ts.ts_name.id_string ^ "'eb" in
        let id = id_derive nm ts.ts_name in
        let ls = create_fsymbol id [] ty_int  in
        let t = t_nat_const fmt.Number.fp_exponent_digits in
        let uc = add_logic_decl uc [make_ls_defn ls [] t] in
        (* create significand digits attribute *)
        let nm = ts.ts_name.id_string ^ "'sb" in
        let id = id_derive nm ts.ts_name in
        let ls = create_fsymbol id [] ty_int  in
        let t = t_nat_const fmt.Number.fp_significand_digits in
        add_logic_decl uc [make_ls_defn ls [] t]
Clément Fumex's avatar
Clément Fumex committed
572
  in
573 574 575 576 577
  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
578 579
  with
    | ClashSymbol s ->
580
        Loc.error ~loc:(Hstr.find csymbols s) (ClashSymbol s)
581
    | RecordFieldMissing ({ ls_name = { id_string = s }} as cs,ls) ->
582
        Loc.error ~loc:(Hstr.find csymbols s) (RecordFieldMissing (cs,ls))
583
    | DuplicateRecordField ({ ls_name = { id_string = s }} as cs,ls) ->
584
        Loc.error ~loc:(Hstr.find csymbols s) (DuplicateRecordField (cs,ls))
585

586 587
let prepare_typedef td =
  if td.td_model then
588
    Loc.errorm ~loc:td.td_loc "model types are not allowed in pure theories";
589
  if td.td_vis <> Public then
590
    Loc.errorm ~loc:td.td_loc "pure types cannot be abstract or private";
591
  if td.td_inv <> [] then
592
    Loc.errorm ~loc:td.td_loc "pure types cannot have invariants";
593
  match td.td_def with
Clément Fumex's avatar
Clément Fumex committed
594
  | TDabstract | TDrange _ | TDfloat _ | TDalgebraic _ | TDalias _ ->
595 596
      td
  | TDrecord fl ->
597 598
      let field { f_loc = loc; f_ident = id; f_pty = ty;
                  f_mutable = mut; f_ghost = gh } =
599 600
        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";
601
        loc, Some id, false, ty
602
      in
603
      (* constructor for type t is "mk t" (and not String.capitalize t) *)
604
      let id = { td.td_ident with id_str = "mk " ^ td.td_ident.id_str } in
605 606 607
      { td with td_def = TDalgebraic [td.td_loc, id, List.map field fl] }

let add_types dl th =
608
  add_types (List.map prepare_typedef dl) th
609

610
let add_logics dl th =
611
  let lsymbols = Hstr.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
612
  (* 1. create all symbols and make an environment with these symbols *)
613
  let create_symbol th d =
614
    let id = d.ld_ident.id_str in
615
    let v = create_user_id d.ld_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
616
    let pl = tyl_of_params th d.ld_params in
617 618
    let opaque = Opt.fold opaque_tvs (opaque_tvs_l d.ld_params) d.ld_type in
    let ty = Opt.map (ty_of_pty ~noop:false th) d.ld_type in
619 620
    let ls = create_lsymbol ~opaque v pl ty in
    Hstr.add lsymbols id ls;
621
    Loc.try2 ~loc:d.ld_loc add_param_decl th ls
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
622 623 624
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
625
  let type_decl d (abst,defn) =
626
    let id = d.ld_ident.id_str in
627
    let ls = Hstr.find lsymbols id in
628
    let create_var (loc,x,_,_) ty =
629
      let id = match x with
630
        | Some id -> create_user_id id
631 632
        | None -> id_user "_" loc in
      create_vsymbol id ty in
633
    let vl = List.map2 create_var d.ld_params ls.ls_args in
634
    let add_var mvs (_,x,_,_) vs = match x with
635
      | Some {id_str = x} -> Mstr.add_new (DuplicateVar x) x (DTgvar vs) mvs
636 637
      | None -> mvs in
    let denv = List.fold_left2 add_var denv_empty d.ld_params vl in
638 639 640
    match d.ld_def, d.ld_type with
    | None, _ -> ls :: abst, defn
    | Some e, None -> (* predicate *)
641
        let f = dterm th' (fun _ -> None) denv e in
642
        let f = fmla ~strict:true ~keep_loc:true f in
643
        abst, (ls, vl, f) :: defn
644
    | Some e, Some ty -> (* function *)
645
        let e = { e with term_desc = Tcast (e, elim_opaque ty) } in
646
        let t = dterm th' (fun _ -> None) denv e in
647
        let t = term ~strict:true ~keep_loc:true t in
648
        abst, (ls, vl, t) :: defn
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
649
  in
650
  let abst,defn = List.fold_right type_decl dl ([],[]) in
651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682
  (* 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
683
  let th = List.fold_left add_param_decl th abst in
684
  let th = if defn = [] then th else add_logic_decl th (ldefns defn) in
685
  th
686

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
687
let add_prop k loc s f th =
688
  let pr = create_prsymbol (create_user_id s) in
689
  let f = type_fmla th (fun _ -> None) f in
690
  Loc.try4 ~loc add_prop_decl th k pr f
691

692
let loc_of_id id = Opt.get id.Ident.id_loc
693

694
let add_inductives s dl th =
695
  (* 1. create all symbols and make an environment with these symbols *)
696
  let psymbols = Hstr.create 17 in
697
  let create_symbol th d =
698
    let id = d.in_ident.id_str in
699
    let v = create_user_id d.in_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
700
    let pl = tyl_of_params th d.in_params in
701
    let opaque = opaque_tvs_l d.in_params in
702
    let ps = create_psymbol ~opaque v pl in
703
    Hstr.add psymbols id ps;
704
    Loc.try2 ~loc:d.in_loc add_param_decl th ps
705
  in
706 707
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
708
  let propsyms = Hstr.create 17 in
709
  let type_decl d =
710
    let id = d.in_ident.id_str in
711
    let ps = Hstr.find psymbols id in
712
    let clause (loc, id, f) =
713
      Hstr.replace propsyms id.id_str loc;
714
      let f = type_fmla th' (fun _ -> None) f in
715
      create_prsymbol (create_user_id id), f
716 717 718
    in
    ps, List.map clause d.in_def
  in
719
  try add_ind_decl th s (List.map type_decl dl)
Andrei Paskevich's avatar
Andrei Paskevich committed
720
  with
721
  | ClashSymbol s ->
722
      Loc.error ~loc:(Hstr.find propsyms s) (ClashSymbol s)
723
  | InvalidIndDecl (ls,pr) ->
724
      Loc.error ~loc:(loc_of_id pr.pr_name) (InvalidIndDecl (ls,pr))
725
  | NonPositiveIndDecl (ls,pr,s) ->
726
      Loc.error ~loc:(loc_of_id pr.pr_name) (NonPositiveIndDecl (ls,pr,s))
727

728
(* parse declarations *)
729

730
let find_theory env lenv q = match q with
731
  | Qident { id_str = id } -> (* local theory *)
732
      begin try Mstr.find id lenv
733
      with Not_found -> read_theory env [] id end
734
  | Qdot (p, { id_str = id }) -> (* theory in file f *)
735
      read_theory env (string_list_of_qualid p) id
736