typing.ml 31.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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 Ity
21 22 23 24 25
(*
open Pdecl
open Pmodule
open Dexpr
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
26

27
(** debug flags *)
28

29
let debug_parse_only = Debug.register_flag "parse_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
30
  ~desc:"Stop@ after@ parsing."
31

32
let debug_type_only  = Debug.register_flag "type_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
33
  ~desc:"Stop@ after@ type-checking."
34

35
(** errors *)
36

Andrei Paskevich's avatar
Andrei Paskevich committed
37
(*
38 39
exception UnboundTypeVar of string
exception DuplicateTypeVar of string
Andrei Paskevich's avatar
Andrei Paskevich committed
40
*)
41

42
(** lazy declaration of tuples *)
43

Andrei Paskevich's avatar
Andrei Paskevich committed
44
(*
45 46 47 48 49 50
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)
Andrei Paskevich's avatar
Andrei Paskevich committed
51
*)
52

53
(** symbol lookup *)
54 55

let rec qloc = function
56 57 58
  | Qdot (p, id) -> Loc.join (qloc p) id.id_loc
  | Qident id    -> id.id_loc

59 60 61
let qloc_last = function
  | Qdot (_, id) | Qident id -> id.id_loc

62
let rec print_qualid fmt = function
63 64
  | Qdot (p, id) -> Format.fprintf fmt "%a.%s" print_qualid p id.id_str
  | Qident id    -> Format.fprintf fmt "%s" id.id_str
65

66 67
let string_list_of_qualid q =
  let rec sloq acc = function
68 69
    | Qdot (p, id) -> sloq (id.id_str :: acc) p
    | Qident id -> id.id_str :: acc in
70
  sloq [] q
71

72
exception UnboundSymbol of qualid
73

74
let find_qualid get_id find ns q =
75 76 77
  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
78
  if Debug.test_flag Glob.flag then Glob.use (qloc_last q) (get_id r);
79
  r
80

81 82 83
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
84

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

90 91
let find_psymbol_ns ns q =
  let ls = find_lsymbol_ns ns q in
92 93
  if ls.ls_value = None then ls else
    Loc.error ~loc:(qloc q) (PredicateSymbolExpected ls)
94

Andrei Paskevich's avatar
Andrei Paskevich committed
95 96 97 98 99
let find_prop     uc q = find_prop_ns     (Theory.get_namespace uc) q
let find_tysymbol uc q = find_tysymbol_ns (Theory.get_namespace uc) q
let find_lsymbol  uc q = find_lsymbol_ns  (Theory.get_namespace uc) q
let find_fsymbol  uc q = find_fsymbol_ns  (Theory.get_namespace uc) q
let find_psymbol  uc q = find_psymbol_ns  (Theory.get_namespace uc) q
100

Andrei Paskevich's avatar
Andrei Paskevich committed
101 102 103 104 105 106
let find_itysymbol_ns ns q =
  find_qualid (fun s -> s.its_ts.ts_name) Pmodule.ns_find_its ns q

let get_namespace uc = List.hd uc.Pmodule.muc_import

let find_itysymbol uc q = find_itysymbol_ns (get_namespace uc) q
107

108 109
(** Parsing types *)

110
let ty_of_pty uc pty =
111
  let rec get_ty = function
112
    | PTtyvar {id_str = x} ->
113
        ty_var (tv_of_string x)
114
    | PTtyapp (q, tyl) ->
115
        let ts = find_tysymbol uc q in
116
        let tyl = List.map get_ty tyl in
117
        Loc.try2 ~loc:(qloc q) ty_app ts tyl
118
    | PTtuple tyl ->
119 120
        let ts = ts_tuple (List.length tyl) in
        ty_app ts (List.map get_ty tyl)
121
    | PTarrow (ty1, ty2) ->
122
        ty_func (get_ty ty1) (get_ty ty2)
123
    | PTparen ty ->
124 125 126 127
        get_ty ty
  in
  get_ty pty

128
(** typing using destructive type variables
129

130 131 132 133 134 135
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
136

137 138
(** Typing patterns, terms, and formulas *)

139
let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
140 141 142 143
  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
144 145

let parse_record ~loc uc get_val fl =
146
  let fl = List.map (fun (q,e) -> find_lsymbol uc q, e) fl in
147 148 149 150
  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

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

let quant_var uc (loc, id, gh, ty) =
  assert (not gh);
  let ty = match ty with
174
    | Some ty -> dty_of_ty (ty_of_pty uc ty)
175
    | None    -> dty_fresh () in
176
  Opt.map create_user_id id, ty, Some loc
177

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

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

202 203 204
let mk_closure loc ls =
  let mk dt = Dterm.dterm ~loc dt in
  let mk_v i _ =
205 206
    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
207
  let vl = Lists.mapi mk_v ls.ls_args in
Andrei Paskevich's avatar
Andrei Paskevich committed
208
  DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
209

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

349
(* TODO
350
(** Export for program parsing *)
Andrei Paskevich's avatar
Andrei Paskevich committed
351

352 353
let type_term uc gvars t =
  let t = dterm uc gvars denv_empty t in
354
  Dterm.term ~strict:true ~keep_loc:true t
355
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
356

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

361
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
362

Andrei Paskevich's avatar
Andrei Paskevich committed
363 364
open Pdecl
open Pmodule
365

366
let add_pdecl ~vc uc d =
Andrei Paskevich's avatar
Andrei Paskevich committed
367
  if Debug.test_flag Glob.flag then Sid.iter Glob.def d.pd_news;
368
  add_pdecl ~vc uc d
Andrei Paskevich's avatar
Andrei Paskevich committed
369

370
let add_decl uc d = add_pdecl ~vc:false uc (create_pure_decl d)
Andrei Paskevich's avatar
Andrei Paskevich committed
371 372 373 374 375 376 377 378 379 380 381

let add_types uc tdl =
  let add m d =
    let x = d.td_ident.id_str in
    Mstr.add_new (Loc.Located (d.td_loc, ClashSymbol x)) x d m in
  let def = List.fold_left add Mstr.empty tdl in
  let hts = Hstr.create 5 in
  let htd = Hstr.create 5 in
  let rec visit ~alias ~alg x d = if not (Hstr.mem htd x) then
    let id = create_user_id d.td_ident and loc = d.td_loc in
    let args = List.map (fun id -> tv_of_string id.id_str) d.td_params in
382
    match d.td_def with
Andrei Paskevich's avatar
Andrei Paskevich committed
383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405
    | TDabstract ->
        if d.td_inv <> [] then Loc.errorm ~loc
          "Abstract non-record types cannot have invariants";
        let itd = create_abstract_type_decl id args d.td_mut in
        Hstr.add hts x itd.itd_its; Hstr.add htd x itd
    | TDalias pty ->
        if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
          "Alias types cannot be abstract, private. or mutable";
        if d.td_inv <> [] then Loc.errorm ~loc
          "Alias types cannot have invariants";
        let alias = Sstr.add x alias in
        let ity = parse ~loc ~alias ~alg pty in
        if not (Hstr.mem htd x) then
        let itd = create_alias_decl id args ity in
        Hstr.add hts x itd.itd_its; Hstr.add htd x itd
    | TDalgebraic csl ->
        if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
          "Algebraic types cannot be abstract, private. or mutable";
        if d.td_inv <> [] then Loc.errorm ~loc
          "Algebraic types cannot have invariants";
        let hfd = Hstr.create 5 in
        let alias = Sstr.empty in
        let alg = Mstr.add x (id,args) alg in
406 407 408 409 410
        let get_pj nms (_, id, ghost, pty) = match id with
          | Some ({id_str = nm} as id) ->
              let exn = Loc.Located (id.id_loc, Loc.Message ("Field " ^
                nm ^ " is used more than once in the same constructor")) in
              let nms = Sstr.add_new exn nm nms in
Andrei Paskevich's avatar
Andrei Paskevich committed
411
              let ity = parse ~loc ~alias ~alg pty in
412
              let v = try Hstr.find hfd nm with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
413
                let v = create_pvsymbol (create_user_id id) ~ghost ity in
414
                Hstr.add hfd nm v;
Andrei Paskevich's avatar
Andrei Paskevich committed
415 416
                v in
              if not (ity_equal v.pv_ity ity && ghost = v.pv_ghost) then
417 418
                Loc.errorm ~loc "Conflicting definitions for field %s" nm;
              nms, (true, v)
Andrei Paskevich's avatar
Andrei Paskevich committed
419 420
          | None ->
              let ity = parse ~loc ~alias ~alg pty in
421 422 423 424 425 426 427 428 429 430 431 432 433
              nms, (false, create_pvsymbol (id_fresh "a") ~ghost ity) in
        let get_cs oms (_, id, pjl) =
          let nms, pjl = Lists.map_fold_left get_pj Sstr.empty pjl in
          if Sstr.equal oms nms then create_user_id id, pjl else
            let df = Sstr.union (Sstr.diff oms nms) (Sstr.diff nms oms) in
            Loc.errorm ~loc "Field %s is missing in some constructors"
              (Sstr.choose df) in
        let csl = match csl with
          | (_, id, pjl)::csl ->
              let oms, pjl = Lists.map_fold_left get_pj Sstr.empty pjl in
              (create_user_id id, pjl) :: List.map (get_cs oms) csl
          | [] -> assert false in
        if not (Hstr.mem htd x) then
Andrei Paskevich's avatar
Andrei Paskevich committed
434 435 436 437 438 439 440 441 442
        begin match try Some (Hstr.find hts x) with Not_found -> None with
        | Some s ->
            Hstr.add htd x (create_rec_variant_decl s csl)
        | None ->
            let itd = create_flat_variant_decl id args csl in
            Hstr.add hts x itd.itd_its; Hstr.add htd x itd end
    | TDrecord fl ->
        let alias = Sstr.empty in
        let alg = Mstr.add x (id,args) alg in
443 444 445 446 447
        let get_fd nms fd =
          let {id_str = nm; id_loc = loc} = fd.f_ident in
          let exn = Loc.Located (loc, Loc.Message ("Field " ^
            nm ^ " is used more than once in a record")) in
          let nms = Sstr.add_new exn nm nms in
Andrei Paskevich's avatar
Andrei Paskevich committed
448 449 450
          let id = create_user_id fd.f_ident in
          let ity = parse ~loc ~alias ~alg fd.f_pty in
          let ghost = d.td_vis = Abstract || fd.f_ghost in
451 452 453
          nms, (fd.f_mutable, create_pvsymbol id ~ghost ity) in
        let _,fl = Lists.map_fold_left get_fd Sstr.empty fl in
        if not (Hstr.mem htd x) then
Andrei Paskevich's avatar
Andrei Paskevich committed
454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481
        begin match try Some (Hstr.find hts x) with Not_found -> None with
        | Some s ->
            if d.td_vis <> Public || d.td_mut then Loc.errorm ~loc
              "Recursive types cannot be abstract, private. or mutable";
            if d.td_inv <> [] then Loc.errorm ~loc
              "Recursive types cannot have invariants";
            let get_fd (mut, fd) = if mut then Loc.errorm ~loc
              "Recursive types cannot have mutable fields" else fd in
            Hstr.add htd x (create_rec_record_decl s (List.map get_fd fl))
        | None ->
            let priv = d.td_vis <> Public and mut = d.td_mut in
            let add_fd m (_, {pv_vs = v}) =
              Mstr.add v.vs_name.id_string v m in
            let gvars = List.fold_left add_fd Mstr.empty fl in
            let gvars q = match q with
              | Qident x -> Mstr.find_opt x.id_str gvars | _ -> None in
            let invl = List.map (type_fmla uc.muc_theory gvars) d.td_inv in
            let itd = create_flat_record_decl id args priv mut fl invl in
            Hstr.add hts x itd.itd_its; Hstr.add htd x itd end

  and parse ~loc ~alias ~alg pty =
    let rec down = function
      | PTtyvar id ->
          ity_var (tv_of_string id.id_str)
      | PTtyapp (q,tyl) ->
          let s = match q with
            | Qident {id_str = x} when Sstr.mem x alias ->
                Loc.errorm ~loc "Cyclic type definition"
482 483
            | Qident {id_str = x} when Hstr.mem hts x ->
                Hstr.find hts x
Andrei Paskevich's avatar
Andrei Paskevich committed
484 485 486
            | Qident {id_str = x} when Mstr.mem x alg ->
                let id, args = Mstr.find x alg in
                let s = create_itysymbol_pure id args in
487 488 489
                Hstr.add hts x s;
                visit ~alias ~alg x (Mstr.find x def);
                s
Andrei Paskevich's avatar
Andrei Paskevich committed
490
            | Qident {id_str = x} when Mstr.mem x def ->
491
                visit ~alias ~alg x (Mstr.find x def);
Andrei Paskevich's avatar
Andrei Paskevich committed
492 493 494 495 496 497 498 499 500 501 502
                Hstr.find hts x
            | _ ->
                find_itysymbol uc q in
          Loc.try2 ~loc:(qloc q) ity_app_fresh s (List.map down tyl)
      | PTtuple tyl -> ity_tuple (List.map down tyl)
      | PTarrow (ty1,ty2) -> ity_func (down ty1) (down ty2)
      | PTparen ty -> down ty in
    down pty in

  Mstr.iter (visit ~alias:Mstr.empty ~alg:Mstr.empty) def;
  let tdl = List.map (fun d -> Hstr.find htd d.td_ident.id_str) tdl in
503
  add_pdecl ~vc:true uc (create_type_decl tdl)
504

Andrei Paskevich's avatar
Andrei Paskevich committed
505 506 507 508 509 510
let tyl_of_params uc pl =
  let ty_of_param (loc,_,gh,ty) =
    if gh then Loc.errorm ~loc
      "ghost parameters are not allowed in pure declarations";
    ty_of_pty uc ty in
  List.map ty_of_param pl
511

Andrei Paskevich's avatar
Andrei Paskevich committed
512 513
let add_logics uc dl =
  let th = uc.muc_theory in
514
  let lsymbols = Hstr.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
515
  (* 1. create all symbols and make an environment with these symbols *)
Andrei Paskevich's avatar
Andrei Paskevich committed
516
  let create_symbol uc d =
517
    let id = d.ld_ident.id_str in
518
    let v = create_user_id d.ld_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
519
    let pl = tyl_of_params th d.ld_params in
520
    let ty = Opt.map (ty_of_pty th) d.ld_type in
521
    let ls = create_lsymbol v pl ty in
522
    Hstr.add lsymbols id ls;
Andrei Paskevich's avatar
Andrei Paskevich committed
523
    Loc.try2 ~loc:d.ld_loc add_decl uc (create_param_decl ls)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
524
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
525 526
  let uc' = List.fold_left create_symbol uc dl in
  let th' = uc'.muc_theory in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
527
  (* 2. then type-check all definitions *)
528
  let type_decl d (abst,defn) =
529
    let id = d.ld_ident.id_str in
530
    let ls = Hstr.find lsymbols id in
531
    let create_var (loc,x,_,_) ty =
532
      let id = match x with
533
        | Some id -> create_user_id id
534 535
        | None -> id_user "_" loc in
      create_vsymbol id ty in
536
    let vl = List.map2 create_var d.ld_params ls.ls_args in
537
    let add_var mvs (_,x,_,_) vs = match x with
538
      | Some {id_str = x} -> Mstr.add_new (DuplicateVar x) x (DTgvar vs) mvs
539 540
      | None -> mvs in
    let denv = List.fold_left2 add_var denv_empty d.ld_params vl in
541 542 543
    match d.ld_def, d.ld_type with
    | None, _ -> ls :: abst, defn
    | Some e, None -> (* predicate *)
544
        let f = dterm th' (fun _ -> None) denv e in
545
        let f = fmla ~strict:true ~keep_loc:true f in
546
        abst, (make_ls_defn ls vl f) :: defn
547
    | Some e, Some ty -> (* function *)
548
        let e = { e with term_desc = Tcast (e, ty) } in
549
        let t = dterm th' (fun _ -> None) denv e in
550
        let t = term ~strict:true ~keep_loc:true t in
551
        abst, (make_ls_defn ls vl t) :: defn
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
552
  in
553
  let abst,defn = List.fold_right type_decl dl ([],[]) in
Andrei Paskevich's avatar
Andrei Paskevich committed
554 555 556 557
  let add_param_decl uc s = add_decl uc (create_param_decl s) in
  let add_logic_decl uc l = add_decl uc (create_logic_decl l) in
  let uc = List.fold_left add_param_decl uc abst in
  if defn = [] then uc else add_logic_decl uc defn
558

Andrei Paskevich's avatar
Andrei Paskevich committed
559
let add_inductives uc s dl =
560
  (* 1. create all symbols and make an environment with these symbols *)
Andrei Paskevich's avatar
Andrei Paskevich committed
561
  let th = uc.muc_theory in
562
  let psymbols = Hstr.create 17 in
Andrei Paskevich's avatar
Andrei Paskevich committed
563
  let create_symbol uc d =
564
    let id = d.in_ident.id_str in
565
    let v = create_user_id d.in_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
566
    let pl = tyl_of_params th d.in_params in
567
    let ps = create_psymbol v pl in
568
    Hstr.add psymbols id ps;
Andrei Paskevich's avatar
Andrei Paskevich committed
569
    Loc.try2 ~loc:d.in_loc add_decl uc (create_param_decl ps)
570
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
571 572
  let uc' = List.fold_left create_symbol uc dl in
  let th' = uc'.muc_theory in
573
  (* 2. then type-check all definitions *)
574
  let propsyms = Hstr.create 17 in
575
  let type_decl d =
576
    let id = d.in_ident.id_str in
577
    let ps = Hstr.find psymbols id in
578
    let clause (loc, id, f) =
579
      Hstr.replace propsyms id.id_str loc;
580
      let f = type_fmla th' (fun _ -> None) f in
581
      create_prsymbol (create_user_id id), f
582 583 584
    in
    ps, List.map clause d.in_def
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
585 586
  let loc_of_id id = Opt.get id.Ident.id_loc in
  try add_decl uc (create_ind_decl s (List.map type_decl dl))
Andrei Paskevich's avatar
Andrei Paskevich committed
587
  with
588
  | ClashSymbol s ->
589
      Loc.error ~loc:(Hstr.find propsyms s) (ClashSymbol s)
590
  | InvalidIndDecl (ls,pr) ->
591
      Loc.error ~loc:(loc_of_id pr.pr_name) (InvalidIndDecl (ls,pr))
592
  | NonPositiveIndDecl (ls,pr,s) ->
593
      Loc.error ~loc:(loc_of_id pr.pr_name) (NonPositiveIndDecl (ls,pr,s))
594

Andrei Paskevich's avatar
Andrei Paskevich committed
595 596 597 598 599 600
let add_prop uc k s f =
  let th = uc.muc_theory in
  let pr = create_prsymbol (create_user_id s) in
  let f = type_fmla th (fun _ -> None) f in
  add_decl uc (create_prop_decl k pr f)

601
(* parse declarations *)
602

Andrei Paskevich's avatar
Andrei Paskevich committed
603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630
let add_decl uc inth = function
  | Ptree.Dtype dl ->
      add_types uc dl
  | Ptree.Dlogic dl ->
      add_logics uc dl
  | Ptree.Dind (s,dl) ->
      add_inductives uc s dl
  | Ptree.Dprop (k,s,f) ->
      add_prop uc k s f
  | Ptree.Dmeta (id,al) ->
      let th = uc.muc_theory in
      let convert = function
        | Ptree.Mty (PTtyapp (q,[]))
                       -> MAts (find_tysymbol th q)
        | Ptree.Mty ty -> MAty (ty_of_pty th ty)
        | Ptree.Mfs q  -> MAls (find_fsymbol th q)
        | Ptree.Mps q  -> MAls (find_psymbol th q)
        | Ptree.Mpr q  -> MApr (find_prop th q)
        | Ptree.Mstr s -> MAstr s
        | Ptree.Mint i -> MAint i in
      add_meta uc (lookup_meta id.id_str) (List.map convert al)
  | _ when inth ->
      Loc.errorm "Program declarations are not allowed in pure theories"
  | Ptree.Dval _
  | Ptree.Dlet _
  | Ptree.Dfun _
  | Ptree.Drec _
  | Ptree.Dexn _ -> assert false (* TODO *)
631

Andrei Paskevich's avatar
Andrei Paskevich committed
632
(* TODO
633 634
let rec clone_ns kn sl path ns2 ns1 s =
  let qualid fmt path = Pp.print_list
635 636
    (fun fmt () -> Format.pp_print_char fmt '.')
    Format.pp_print_string fmt (List.rev path) in
637
  let s = Mstr.fold (fun nm ns1 acc ->
638 639
    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
640
  in
641
  let inst_ts = Mstr.fold (fun nm ts1 acc ->
642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662
    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
663
  in
664
  let inst_ls = Mstr.fold (fun nm ls1 acc ->
665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683
    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
684 685 686
  in
  { s with inst_ts = inst_ts; inst_ls = inst_ls }

Andrei Paskevich's avatar
Andrei Paskevich committed
687 688
let find_namespace_ns ns q =
  find_qualid (fun _ -> Glob.dummy_id) ns_find_ns ns q
689

690 691 692
let type_inst th t s =
  let add_inst s = function
    | CSns (loc,p,q) ->
693 694
      let ns1 = Opt.fold find_namespace_ns t.th_export p in
      let ns2 = Opt.fold find_namespace_ns (get_namespace th) q in
695
      Loc.try6 ~loc clone_ns t.th_known t.th_local [] ns2 ns1 s
696
    | CStsym (loc,p,[],PTtyapp (q,[])) ->
697 698
      let ts1 = find_tysymbol_ns t.th_export p in
      let ts2 = find_tysymbol th q in
699
      if Mts.mem ts1 s.inst_ts
700
      then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string);
701
      { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
702
    | CStsym (loc,p,tvl,pty) ->
703
      let ts1 = find_tysymbol_ns t.th_export p in
704
      let id = id_user (ts1.ts_name.id_string ^ "_subst") loc in
705
      let tvl = List.map (fun id -> tv_of_string id.id_str) tvl in
706
      let def = Some (ty_of_pty th pty) in
707
      let ts2 = Loc.try3 ~loc create_tysymbol id tvl def in
708
      if Mts.mem ts1 s.inst_ts
709
      then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string);
710
      { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
711
    | CSfsym (loc,p,q) ->
712 713
      let ls1 = find_fsymbol_ns t.th_export p in
      let ls2 = find_fsymbol th q in
714
      if Mls.mem ls1 s.inst_ls
715
      then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string);
716 717
      { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
    | CSpsym (loc,p,q) ->
718 719
      let ls1 = find_psymbol_ns t.th_export p in
      let ls2 = find_psymbol th q in
720
      if Mls.mem ls1 s.inst_ls
721
      then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string);
722
      { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
Andrei Paskevich's avatar
Andrei Paskevich committed
723 724 725
    | CSvsym (loc,_,_) ->
      Loc.errorm ~loc "program symbol instantiation \
        is not supported in pure theories"
726
    | CSlemma (loc,p) ->
727
      let pr = find_prop_ns t.th_export p in
728
      if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
729
      then Loc.error ~loc (ClashSymbol pr.pr_name.id_string);
730 731
      { s with inst_lemma = Spr.add pr s.inst_lemma }
    | CSgoal (loc,p) ->
732
      let pr = find_prop_ns t.th_export p in
733
      if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
734
      then Loc.error ~loc (ClashSymbol pr.pr_name.id_string);
735 736 737
      { s with inst_goal = Spr.add pr s.inst_goal }
  in
  List.fold_left add_inst empty_inst s
Andrei Paskevich's avatar
Andrei Paskevich committed
738
*)
739

Andrei Paskevich's avatar
Andrei Paskevich committed
740 741 742 743 744 745 746 747 748
let use_clone loc uc env file (use, subst) =
  let find_module env file q = match q with
    | Qident { id_str = id } -> (* local module *)
        begin try Mstr.find id file
        with Not_found -> read_module env [] id end
    | Qdot (p, { id_str = id }) -> (* module in file f *)
        read_module env (string_list_of_qualid p) id in
  let use_or_clone uc =
    let m = find_module env file use.use_module in
749
    if Debug.test_flag Glob.flag then
Andrei Paskevich's avatar
Andrei Paskevich committed
750
      Glob.use (qloc_last use.use_module) m.mod_theory.th_name;
751
    match subst with
Andrei Paskevich's avatar
Andrei Paskevich committed
752 753 754 755
    | None -> use_export uc m
    | Some _ ->
        warn_clone_not_abstract loc m.mod_theory;
        Loc.errorm ~loc "cloning coming soon" (* TODO *)
756
  in
757 758 759
  match use.use_import with
  | Some (import, use_as) ->
      (* use T = namespace T use_export T end *)
Andrei Paskevich's avatar
Andrei Paskevich committed
760 761 762
      let uc = open_namespace uc use_as in
      let uc = use_or_clone uc in
      close_namespace uc ~import
763
  | None ->
Andrei Paskevich's avatar
Andrei Paskevich committed
764
      use_or_clone uc
765

766 767
(* incremental parsing *)

768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825
type slice = {
  env           : Env.env;
  path          : Env.pathname;
  pure          : bool;
  mutable file  : pmodule Mstr.t;
  mutable muc   : pmodule_uc option;
  mutable inth  : bool;
}

let state = (Stack.create () : slice Stack.t)

let open_file env path ~pure =
  assert (Stack.is_empty state || (Stack.top state).muc <> None);
  Stack.push { env = env; path = path; pure = pure;
               file = Mstr.empty; muc = None; inth = false } state

let close_file () =
  assert (not (Stack.is_empty state) && (Stack.top state).muc = None);
  (Stack.pop state).file

let open_module ({id_str = nm; id_loc = loc} as id) ~theory =
  assert (not (Stack.is_empty state) && (Stack.top state).muc = None);
  let slice = Stack.top state in
  if Mstr.mem nm slice.file then Loc.errorm ~loc
    "module %s is already defined in this file" nm;
  if slice.pure && not theory then Loc.errorm ~loc
    "this file can only contain pure theories";
  let muc = create_module slice.env ~path:slice.path (create_user_id id) in
  slice.muc <- Some muc; slice.inth <- theory

let close_module loc =
  assert (not (Stack.is_empty state) && (Stack.top state).muc <> None);
  let slice = Stack.top state in
  if Debug.test_noflag debug_parse_only then begin
    let m = Loc.try1 ~loc close_module (Opt.get slice.muc) in
    if Debug.test_flag Glob.flag then Glob.def m.mod_theory.th_name;
    slice.file <- Mstr.add m.mod_theory.th_name.id_string m slice.file;
  end;
  slice.muc <- None

let open_namespace nm =
  assert (not (Stack.is_empty state) && (Stack.top state).muc <> None);
  if Debug.test_noflag debug_parse_only then
    let slice = Stack.top state in
    slice.muc <- Some (open_namespace (Opt.get slice.muc) nm.id_str)

let close_namespace loc ~import =
  assert (not (Stack.is_empty state) && (Stack.top state).muc <> None);
  if Debug.test_noflag debug_parse_only then
    let slice = Stack.top state in
    let muc = Loc.try1 ~loc (close_namespace ~import) (Opt.get slice.muc) in
    slice.muc <- Some muc

let add_decl loc d =
  assert (not (Stack.is_empty state) && (Stack.top state).muc <> None);
  if Debug.test_noflag debug_parse_only then
    let slice = Stack.top state in
    let muc = Loc.try3 ~loc add_decl (Opt.get slice.muc) slice.inth d in
Andrei Paskevich's avatar
Andrei Paskevich committed
826
    slice.muc <- Some muc
827 828 829 830 831 832 833

let use_clone loc use =
  assert (not (Stack.is_empty state) && (Stack.top state).muc <> None);
  if Debug.test_noflag debug_parse_only then
    let slice = Stack.top state in
    let muc = Loc.try5 ~loc use_clone loc
      (Opt.get slice.muc) slice.env slice.file use in
Andrei Paskevich's avatar
Andrei Paskevich committed
834
    slice.muc <- Some muc
835

836 837 838 839
(** Exception printing *)

let () = Exn_printer.register (fun fmt e -> match e with
  | UnboundSymbol q ->
840
      Format.fprintf fmt "unbound symbol '%a'" print_qualid q
Andrei Paskevich's avatar
Andrei Paskevich committed
841
(* TODO
842
  | UnboundTypeVar s ->
843
      Format.fprintf fmt "unbound type variable '%s" s
844
  | DuplicateTypeVar s ->
845
      Format.fprintf fmt "duplicate type parameter '%s" s
Andrei Paskevich's avatar
Andrei Paskevich committed
846
*)
847
  | _ -> raise e)