typing.ml 30.7 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   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 42 43
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)
44

45
(** symbol lookup *)
46 47

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

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
54

55 56 57 58 59
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
60

61
exception UnboundSymbol of qualid
62

63
let find_qualid get_id find ns q =
64 65 66 67 68
  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
  if Debug.test_flag Glob.flag then Glob.use (qloc q) (get_id r);
  r
69

70 71 72
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
73

74 75
let find_fsymbol_ns ns q =
  let ls = find_lsymbol_ns ns q in
76 77
  if ls.ls_value <> None then ls else
    Loc.error ~loc:(qloc q) (FunctionSymbolExpected ls)
78

79 80
let find_psymbol_ns ns q =
  let ls = find_lsymbol_ns ns q in
81 82
  if ls.ls_value = None then ls else
    Loc.error ~loc:(qloc q) (PredicateSymbolExpected ls)
83

84 85 86 87 88
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
89

90 91
let find_namespace_ns ns q =
  find_qualid (fun _ -> Glob.dummy_id) ns_find_ns ns q
92

93 94 95
(** Parsing types *)

let create_user_tv =
96 97
  let hs = Hstr.create 17 in fun s ->
  try Hstr.find hs s with Not_found ->
98 99 100
  let tv = create_tvsymbol (id_fresh s) in
  Hstr.add hs s tv;
  tv
101

Andrei Paskevich's avatar
Andrei Paskevich committed
102
let ty_of_pty ?(noop=true) uc pty =
103 104 105 106 107 108
  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)
109 110
    | PPTtyapp (q, tyl) ->
        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 114 115 116 117 118 119 120 121 122
    | 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

123
let opaque_tvs args =
124 125 126 127 128 129 130
  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
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 145 146 147 148
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
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 158 159
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)
160
    | PPpapp (q,pl) ->
161
        let pl = List.map (dpattern uc) pl in
162
        DPapp (find_lsymbol uc q, pl)
163 164 165 166 167 168 169 170 171 172 173
    | 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))
174 175 176 177 178 179

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 ()

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

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

204 205
type global_vs = Ptree.qualid -> vsymbol option

206 207 208 209 210 211 212 213 214 215 216 217
let rec dterm uc gvars denv {pp_desc = desc; pp_loc = loc} =
  let func_app loc e el =
    let app (loc, e) e1 = Loc.join loc e1.pp_loc,
      DTfapp (Dterm.dterm ~loc e, dterm uc gvars denv e1) in
    snd (List.fold_left app (loc, e) el)
  in
  let rec take loc al l el = match l, el with
    | (_::l), (e::el) ->
        take (Loc.join loc e.pp_loc) (dterm uc gvars denv e :: al) l el
    | _, _ -> loc, List.rev al, el
  in
  let qualid_app loc q el = match gvars q with
218
    | Some vs ->
219
        func_app loc (DTgvar vs) el
220
    | None ->
221
        let ls = find_lsymbol uc q in
222 223
        let loc, al, el = take loc [] ls.ls_args el in
        func_app loc (DTapp (ls,al)) el
224
  in
225
  let qualid_app loc q el = match q with
226 227
    | Qident {id = n} ->
        (match denv_get_opt denv n with
228 229 230
        | Some d -> func_app loc d el
        | None -> qualid_app loc q el)
    | _ -> qualid_app loc q el
231
  in
232
  Dterm.dterm ~loc (match desc with
233
  | PPident q ->
234
      qualid_app loc q []
235
  | PPidapp (q, tl) ->
236
      qualid_app (qloc q) q tl
237
  | PPapply (e1, e2) ->
238
      DTfapp (dterm uc gvars denv e1, dterm uc gvars denv e2)
239
  | PPtuple tl ->
240
      let tl = List.map (dterm uc gvars denv) tl in
241 242 243 244 245
      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
246
        let ls = find_lsymbol uc (Qident op) in
247 248
        DTnot (Dterm.dterm ~loc (DTapp (ls, [de1;de2])))
      else
249
        DTapp (find_lsymbol uc (Qident op), [de1;de2])
250 251 252 253 254 255 256
      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
257
            DTbinop (DTand, de12, de23)
258 259 260
        | [] -> assert false in
      let rec get_chain e12 acc = match e12.pp_desc with
        | PPinfix (e1, op1, e2) when chainable_op uc op1 ->
261
            get_chain e1 ((op1, dterm uc gvars denv e2) :: acc)
262
        | _ -> e12, acc in
263
      let ch = [op2, dterm uc gvars denv e3] in
264 265
      let e1, ch = if chainable_op uc op2
        then get_chain e12 ch else e12, ch in
266
      make_chain (dterm uc gvars denv e1) ch
267 268 269 270
  | PPconst c ->
      DTconst c
  | PPlet (x, e1, e2) ->
      let id = create_user_id x in
271
      let e1 = dterm uc gvars denv e1 in
272
      let denv = denv_add_let denv e1 id in
273
      let e2 = dterm uc gvars denv e2 in
274 275
      DTlet (e1, id, e2)
  | PPmatch (e1, bl) ->
276
      let e1 = dterm uc gvars denv e1 in
277 278 279
      let branch (p, e) =
        let p = dpattern uc p in
        let denv = denv_add_pat denv p in
280
        p, dterm uc gvars denv e in
281 282
      DTcase (e1, List.map branch bl)
  | PPif (e1, e2, e3) ->
283 284 285
      let e1 = dterm uc gvars denv e1 in
      let e2 = dterm uc gvars denv e2 in
      let e3 = dterm uc gvars denv e3 in
286 287 288 289 290 291
      DTif (e1, e2, e3)
  | PPtrue ->
      DTtrue
  | PPfalse ->
      DTfalse
  | PPunop (PPnot, e1) ->
292
      DTnot (dterm uc gvars denv e1)
293
  | PPbinop (e1, op, e2) ->
294 295
      let e1 = dterm uc gvars denv e1 in
      let e2 = dterm uc gvars denv e2 in
296
      let op = match op with
297 298 299 300 301 302
        | PPand -> DTand
        | PPand_asym -> DTand_asym
        | PPor -> DTor
        | PPor_asym -> DTor_asym
        | PPimplies -> DTimplies
        | PPiff -> DTiff in
303 304 305 306
      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
307 308 309
      let dterm e = dterm uc gvars denv e in
      let trl = List.map (List.map dterm) trl in
      let e1 = dterm e1 in
310 311 312 313 314 315 316 317 318 319 320 321 322 323 324
      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
325
        | Some e -> dterm uc gvars denv e
326 327 328 329
        | 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) ->
330
      let e1 = dterm uc gvars denv e1 in
331 332
      let re = is_reusable e1 in
      let v = if re then e1 else mk_var "_q " e1 in
333
      let get_val _ pj = function
334
        | Some e -> dterm uc gvars denv e
335
        | None -> Dterm.dterm ~loc (DTapp (pj,[v])) in
336
      let cs, fl = parse_record ~loc uc get_val fl in
337 338
      let d = DTapp (cs, fl) in
      if re then d else mk_let ~loc "_q " e1 d
339
  | PPnamed (Lpos uloc, e1) ->
340
      DTuloc (dterm uc gvars denv e1, uloc)
341
  | PPnamed (Lstr lab, e1) ->
342
      DTlabel (dterm uc gvars denv e1, Slab.singleton lab)
343
  | PPcast (e1, ty) ->
344
      DTcast (dterm uc gvars denv e1, ty_of_pty uc ty))
345 346

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

348 349
let type_term uc gvars t =
  let t = dterm uc gvars denv_empty t in
350
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
351

352 353
let type_fmla uc gvars f =
  let f = dterm uc gvars denv_empty f in
354
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
355

356
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
357

Andrei Paskevich's avatar
Andrei Paskevich committed
358
let tyl_of_params ?(noop=false) uc pl =
359 360 361
  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
362
    ty_of_pty ~noop uc ty in
363 364
  List.map ty_of_param pl

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

490 491
let prepare_typedef td =
  if td.td_model then
492
    Loc.errorm ~loc:td.td_loc "model types are not allowed in pure theories";
493
  if td.td_vis <> Public then
494
    Loc.errorm ~loc:td.td_loc "pure types cannot be abstract or private";
495
  if td.td_inv <> [] then
496
    Loc.errorm ~loc:td.td_loc "pure types cannot have invariants";
497
  match td.td_def with
498 499 500
  | TDabstract | TDalgebraic _ | TDalias _ ->
      td
  | TDrecord fl ->
501 502
      let field { f_loc = loc; f_ident = id; f_pty = ty;
                  f_mutable = mut; f_ghost = gh } =
503 504
        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";
505
        loc, Some id, false, ty
506
      in
507 508
      (* 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
509 510 511
      { td with td_def = TDalgebraic [td.td_loc, id, List.map field fl] }

let add_types dl th =
512
  add_types (List.map prepare_typedef dl) th
513

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
597
let add_prop k loc s f th =
598
  let pr = create_prsymbol (create_user_id s) in
599
  let f = type_fmla th (fun _ -> None) f in
600
  Loc.try4 ~loc add_prop_decl th k pr f
601

602
let loc_of_id id = Opt.get id.Ident.id_loc
603

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

638
(* parse declarations *)
639

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
640
let prop_kind = function
641 642 643
  | Kaxiom -> Paxiom
  | Kgoal -> Pgoal
  | Klemma -> Plemma
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
644

645 646
let find_theory env lenv q = match q with
  | Qident { id = id } -> (* local theory *)
647
      begin try Mstr.find id lenv
Andrei Paskevich's avatar
Andrei Paskevich committed
648
      with Not_found -> read_lib_theory env [] id end
649 650
  | Qdot (p, { id = id }) -> (* theory in file f *)
      read_lib_theory env (string_list_of_qualid p) id
651

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

706
let add_decl loc th = function
707
  | Ptree.TypeDecl dl ->
708
      add_types dl th
709
  | Ptree.LogicDecl dl ->
710
      add_logics dl th
711
  | Ptree.IndDecl (s, dl) ->
712
      add_inductives s dl th
713
  | Ptree.PropDecl (k, s, f) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
714
      add_prop (prop_kind k) loc s f th
715
  | Ptree.Meta (id, al) ->
716
      let convert = function
717
        | PMAty (PPTtyapp (q,[]))
718
                   -> MAts (find_tysymbol th q)
719
        | PMAty ty -> MAty (ty_of_pty th ty)
720 721 722
        | PMAfs q  -> MAls (find_fsymbol th q)
        | PMAps q  -> MAls (find_psymbol th q)
        | PMApr q  -> MApr (find_prop th q)
723
        | PMAstr s -> MAstr s
724
        | PMAint i -> MAint i
725
      in
726
      let add s = add_meta th (lookup_meta s) (List.map convert al) in
727
      Loc.try1 ~loc add id.id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
728

729 730
let add_decl loc th d =
  if Debug.test_flag debug_parse_only then th else
731
  Loc.try3 ~loc add_decl loc th d
732

733 734 735
let type_inst th t s =
  let add_inst s = function
    | CSns (loc,p,q) ->
736 737
      let ns1 = Opt.fold find_namespace_ns t.th_export p in
      let ns2 = Opt.fold find_namespace_ns (get_namespace th) q in
738
      Loc.try6 ~loc clone_ns t.th_known t.th_local [] ns2 ns1 s
739
    | CStsym (loc,p,[],PPTtyapp (q,[])) ->
740 741
      let ts1 = find_tysymbol_ns t.th_export p in
      let ts2 = find_tysymbol th q in
742
      if Mts.mem ts1 s.inst_ts
743
      then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string);
744
      { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
745
    | CStsym (loc,p,tvl,pty) ->
746
      let ts1 = find_tysymbol_ns t.th_export p in
747 748 749
      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
750
      let ts2 = Loc.try3 ~loc create_tysymbol id tvl def in
751
      if Mts.mem ts1 s.inst_ts
752
      then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string);
753
      { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
754
    | CSfsym (loc,p,q) ->
755 756
      let ls1 = find_fsymbol_ns t.th_export p in
      let ls2 = find_fsymbol th q in
757
      if Mls.mem ls1 s.inst_ls
758
      then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string);
759 760
      { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
    | CSpsym (loc,p,q) ->
761 762
      let ls1 = find_psymbol_ns t.th_export p in
      let ls2 = find_psymbol th q in
763
      if Mls.mem ls1 s.inst_ls
764
      then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string);
765 766
      { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
    | CSlemma (loc,p) ->
767
      let pr = find_prop_ns t.th_export p in
768
      if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
769
      then Loc.error ~loc (ClashSymbol pr.pr_name.id_string);
770 771
      { s with inst_lemma = Spr.add pr s.inst_lemma }
    | CSgoal (loc,p) ->
772
      let pr = find_prop_ns t.th_export p in
773
      if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
774
      then Loc.error ~loc (ClashSymbol pr.pr_name.id_string);