typing.ml 30.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-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 48 49 50

let rec qloc = function
  | Qident x -> x.id_loc
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc

51 52 53 54 55
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
56

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

61
exception UnboundSymbol of qualid
62

63 64 65 66 67 68
let find_ns get_id find q ns =
  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 q ns     = find_ns (fun pr -> pr.pr_name) ns_find_pr q ns
let find_tysymbol_ns q ns = find_ns (fun ts -> ts.ts_name) ns_find_ts q ns
let find_lsymbol_ns q ns  = find_ns (fun ls -> ls.ls_name) ns_find_ls q ns
73

74 75
let find_fsymbol_ns q ns =
  let ls = find_lsymbol_ns q ns 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 q ns =
  let ls = find_lsymbol_ns q ns in
81 82
  if ls.ls_value = None then ls else
    Loc.error ~loc:(qloc q) (PredicateSymbolExpected ls)
83

84 85 86 87 88 89 90 91
let find_prop q uc     = find_prop_ns q (get_namespace uc)
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)
let find_lsymbol q uc  = find_lsymbol_ns q (get_namespace uc)
let find_fsymbol q uc  = find_fsymbol_ns q (get_namespace uc)
let find_psymbol q uc  = find_psymbol_ns q (get_namespace uc)

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

93
(* dead code
94
let find_namespace q uc = find_namespace_ns q (get_namespace uc)
95
*)
96

97 98 99 100 101 102 103 104
(** Parsing types *)

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

106 107 108 109 110 111 112
let ty_of_pty_top ~noop uc pty =
  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)
113
    | PPTtyapp (x, tyl) ->
114
        let ts = find_tysymbol x uc in
115
        let tyl = List.map get_ty tyl in
116 117 118 119 120 121 122 123 124 125 126 127
        Loc.try2 ~loc:(qloc x) ty_app ts tyl
    | 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

let ty_of_pty uc pty = ty_of_pty_top ~noop:true uc pty
128

129
let opaque_tvs args =
130 131 132 133 134 135 136
  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
137
  List.fold_left (fun acc (_,_,_,ty) -> opaque_tvs acc ty) Stv.empty args
138

139
(** typing using destructive type variables
140

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

148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
(** Typing patterns, terms, and formulas *)

let create_user_id { id = x ; id_lab = ll ; id_loc = loc } =
  let get_labels (ll,p) = function
    | Lstr l -> Slab.add l ll, p
    | Lpos p -> ll, Some p in
  let label,p = List.fold_left get_labels (Slab.empty,None) ll in
  id_user ~label x (Opt.get_def loc p)

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

163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
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)
    | PPpapp (x,pl) ->
        let pl = List.map (dpattern uc) pl in
        DPapp (find_lsymbol x uc, pl)
    | PPptuple pl ->
        let pl = List.map (dpattern uc) pl in
        DPapp (fs_tuple (List.length pl), pl)
    | PPprec fl ->
        let get_val _ _ = function
          | Some p -> dpattern uc p
          | None -> Dterm.dpattern DPwild in
        let cs,fl = parse_record ~loc uc get_val fl in
        DPapp (cs,fl)
    | PPpas (p, x) -> DPas (dpattern uc p, create_user_id x)
    | PPpor (p, q) -> DPor (dpattern uc p, dpattern uc q))
181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196

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

let chainable_op uc op =
  (* non-bool -> non-bool -> bool *)
  op.id = "infix =" || op.id = "infix <>" ||
  match find_lsymbol (Qident op) uc 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

197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220
type global_vs = Ptree.qualid -> vsymbol option

let rec dterm uc (gvars: global_vs) denv {pp_desc = desc; pp_loc = loc} =
  let pterm denv pp = dterm uc gvars denv pp in
  let highord_app e1 e2 =
    DTapp (fs_func_app, [Dterm.dterm ~loc e1; pterm denv e2]) in
  let highord_app e1 el = List.fold_left highord_app e1 el in
  let qualid_app x el = match gvars x with
    | Some vs ->
        highord_app (DTgvar vs) el
    | None ->
        let ls = find_lsymbol x uc in
        let rec take al l el = match l, el with
          | (_::l), (e::el) -> take (pterm denv e :: al) l el
          | _, _ -> List.rev al, el in
        let al, el = take [] ls.ls_args el in
        highord_app (DTapp (ls,al)) el
  in
  let qualid_app x el = match x with
    | Qident {id = n} ->
        (match denv_get_opt denv n with
        | Some dt -> highord_app dt el
        | None -> qualid_app x el)
    | _ -> qualid_app x el
221
  in
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330
  Dterm.dterm ~loc (match desc with
  | PPvar x ->
      qualid_app x []
  | PPapp (x, tl) ->
      qualid_app x tl
  | PPhoapp (e1, e2) ->
      DTapp (fs_func_app, [pterm denv e1; pterm denv e2])
  | PPtuple tl ->
      let tl = List.map (pterm denv) tl in
      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
        let ls = find_lsymbol (Qident op) uc in
        DTnot (Dterm.dterm ~loc (DTapp (ls, [de1;de2])))
      else
        DTapp (find_lsymbol (Qident op) uc, [de1;de2])
      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
            DTbinop (Tand, de12, de23)
        | [] -> assert false in
      let rec get_chain e12 acc = match e12.pp_desc with
        | PPinfix (e1, op1, e2) when chainable_op uc op1 ->
            get_chain e1 ((op1, pterm denv e2) :: acc)
        | _ -> e12, acc in
      let ch = [op2, pterm denv e3] in
      let e1, ch = if chainable_op uc op2
        then get_chain e12 ch else e12, ch in
      make_chain (pterm denv e1) ch
  | PPconst c ->
      DTconst c
  | PPlet (x, e1, e2) ->
      let id = create_user_id x in
      let e1 = pterm denv e1 in
      let denv = denv_add_let denv e1 id in
      let e2 = pterm denv e2 in
      DTlet (e1, id, e2)
  | PPmatch (e1, bl) ->
      let e1 = pterm denv e1 in
      let branch (p, e) =
        let p = dpattern uc p in
        let denv = denv_add_pat denv p in
        p, pterm denv e in
      DTcase (e1, List.map branch bl)
  | PPif (e1, e2, e3) ->
      let e1 = pterm denv e1 in
      let e2 = pterm denv e2 in
      let e3 = pterm denv e3 in
      DTif (e1, e2, e3)
  | PPtrue ->
      DTtrue
  | PPfalse ->
      DTfalse
  | PPunop (PPnot, e1) ->
      DTnot (pterm denv e1)
  | PPbinop (e1, op, e2) ->
      let e1 = pterm denv e1 in
      let e2 = pterm denv e2 in
      let op = match op with
        | PPand -> Tand
        | PPor -> Tor
        | PPimplies -> Timplies
        | PPiff -> Tiff in
      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
      let trl = List.map (List.map (pterm denv)) trl in
      let e1 = pterm denv e1 in
      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
        | Some e -> pterm denv e
        | 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) ->
      let e1 = pterm denv e1 in
      let get_val _ pj = function
        | Some e -> pterm denv e
        | None -> Dterm.dterm ~loc (DTapp (pj,[e1])) in
      let cs, fl = parse_record ~loc uc get_val fl in
      DTapp (cs, fl)
  | PPnamed (Lpos uloc, e1) ->
      DTuloc (pterm denv e1, uloc)
  | PPnamed (Lstr lab, e1) ->
      DTlabel (pterm denv e1, Slab.singleton lab)
  | PPcast (e1, ty) ->
      DTcast (pterm denv e1, ty_of_pty uc ty))

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

332 333
let type_term uc gfn t =
  let t = dterm uc gfn denv_empty t in
334
  Dterm.term ~strict:true ~keep_loc:true t
Andrei Paskevich's avatar
Andrei Paskevich committed
335

336 337
let type_fmla uc gfn f =
  let f = dterm uc gfn denv_empty f in
338
  Dterm.fmla ~strict:true ~keep_loc:true f
Andrei Paskevich's avatar
Andrei Paskevich committed
339

340 341 342 343 344 345 346 347 348 349 350 351
let type_term_branch uc gfn p t =
  let p = dpattern uc p in
  let denv = denv_add_pat denv_empty p in
  let t = dterm uc gfn denv t in
  Dterm.term_branch ~strict:true ~keep_loc:true p t

let type_fmla_branch uc gfn p f =
  let p = dpattern uc p in
  let denv = denv_add_pat denv_empty p in
  let f = dterm uc gfn denv f in
  Dterm.fmla_branch ~strict:true ~keep_loc:true p f

352
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
353

354
let tyl_of_params ~noop uc pl =
355 356 357
  let ty_of_param (loc,_,gh,ty) =
    if gh then Loc.errorm ~loc
      "ghost parameters are not allowed in pure declarations";
358
    ty_of_pty_top ~noop uc ty in
359 360
  List.map ty_of_param pl

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

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

let add_types dl th =
508
  add_types (List.map prepare_typedef dl) th
509

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

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

598
let loc_of_id id = Opt.get id.Ident.id_loc
599

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

634
(* parse declarations *)
635

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
636
let prop_kind = function
637 638 639
  | Kaxiom -> Paxiom
  | Kgoal -> Pgoal
  | Klemma -> Plemma
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
640

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

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

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

725 726
let add_decl loc th d =
  if Debug.test_flag debug_parse_only then th else
727
  Loc.try3 ~loc add_decl loc th d
728

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

776
let add_use_clone env lenv th loc (use, subst) =
777
  if Debug.test_flag debug_parse_only then th else
778
  let use_or_clone th =
779 780
    let t = find_theory env lenv use.use_theory in
    if Debug.test_flag Glob.flag then Glob.use (qloc use.use_theory) t.th_name;
781
    match subst with
782
    | None -> use_export th t
783 784 785
    | Some s ->
        warn_clone_not_abstract loc t;
        clone_export th t (type_inst th t s)
786
  in
787 788
  let use_or_clone th = match use.use_import with
    | Some (import, use_as) ->
789
        (* use T = namespace T use_export T end *)
790
        let th = open_namespace th use_as in
791
        let th = use_or_clone th in
792
        close_namespace th import
793 794
    | None ->
        use_or_clone th
795
  in
796
  Loc.try1 ~loc use_or_clone th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
797

798
let close_theory lenv th =
799
  if Debug.test_flag debug_parse_only then lenv else
800 801
  let th = close_theory th in
  let id = th.th_name.id_string in
802
  let loc = th.th_name.Ident.id_loc in
803
  if Mstr.mem id lenv then Loc.error ?loc (ClashTheory id);
804
  Mstr.add id th lenv
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
805

806
let close_namespace loc import th =
807
  Loc.try2 ~loc close_namespace th import
808

809 810 811 812 813 814 815 816
(* incremental parsing *)

let open_file, close_file =
  let lenv = Stack.create () in
  let uc   = Stack.create () in
  let open_file env path =
    Stack.push Mstr.empty lenv;
    let open_theory id =
817
      Stack.push (Theory.create_theory ~path (create_user_id id)) uc in
818 819
    let close_theory () =
      Stack.push (close_theory (Stack.pop lenv) (Stack.pop uc)) lenv in
820 821 822 823
    let open_namespace name =