typing.ml 29.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-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

12
open Stdlib
13
open Ident
14
open Ptree
15
open Ty
16
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
17
open Decl
18
open Theory
19
open Dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
20
open Env
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

37 38
exception UnboundTypeVar of string
exception DuplicateTypeVar of string
39

40
(** lazy declaration of tuples *)
41

42 43 44 45
let add_decl_with_tuples uc d =
  if Debug.test_flag Glob.flag then Sid.iter Glob.def d.d_news;
  add_decl_with_tuples uc d

46 47 48 49 50 51
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)
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

95 96 97 98 99
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
100

101 102
let find_namespace_ns ns q =
  find_qualid (fun _ -> Glob.dummy_id) ns_find_ns ns q
103

104 105
(** Parsing types *)

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

124
(** typing using destructive type variables
125

126 127 128 129 130 131
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
132

133 134
(** Typing patterns, terms, and formulas *)

135
let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
136 137 138 139
  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
140 141

let parse_record ~loc uc get_val fl =
142
  let fl = List.map (fun (q,e) -> find_lsymbol uc q, e) fl in
143 144 145 146
  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

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

let quant_var uc (loc, id, gh, ty) =
  assert (not gh);
  let ty = match ty with
170
    | Some ty -> dty_of_ty (ty_of_pty uc ty)
171
    | None    -> dty_fresh () in
172
  Opt.map create_user_id id, ty, Some loc
173

174 175 176 177 178 179 180 181 182 183 184 185 186 187
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)

188 189
let chainable_op uc op =
  (* non-bool -> non-bool -> bool *)
190
  op.id_str = "infix =" || op.id_str = "infix <>" ||
191 192 193 194 195 196
  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
197

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

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

345
(* TODO
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
351
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
352

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

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

359
let tyl_of_params uc pl =
360 361 362
  let ty_of_param (loc,_,gh,ty) =
    if gh then Loc.errorm ~loc
      "ghost parameters are not allowed in pure declarations";
363
    ty_of_pty uc ty in
364 365
  List.map ty_of_param pl

366
let add_types dl th =
367
  let def = List.fold_left
368
    (fun def d ->
369
      let id = d.td_ident.id_str in
370
      Mstr.add_new (Loc.Located (d.td_loc, ClashSymbol id)) id d def)
371
    Mstr.empty dl
372
  in
373
  let tysymbols = Hstr.create 17 in
374
  let rec visit x =
375
    let d = Mstr.find x def in
376
    try
377
      match Hstr.find tysymbols x with
378
        | None -> Loc.errorm ~loc:d.td_loc "Cyclic type definition"
379
        | Some ts -> ts
380
    with Not_found ->
381 382
      Hstr.add tysymbols x None;
      let vars = Hstr.create 17 in
383
      let vl = List.map (fun id ->
384 385 386 387
        if Hstr.mem vars id.id_str then
          Loc.error ~loc:id.id_loc (DuplicateTypeVar id.id_str);
        let i = tv_of_string id.id_str in
        Hstr.add vars id.id_str i;
388
        i) d.td_params
389
      in
390
      let id = create_user_id d.td_ident in
391
      let ts = match d.td_def with
392 393
        | TDalias ty ->
            let rec apply = function
394
              | PTtyvar v ->
395
                  begin
396 397
                    try ty_var (Hstr.find vars v.id_str) with Not_found ->
                      Loc.error ~loc:v.id_loc (UnboundTypeVar v.id_str)
398
                  end
399
              | PTtyapp (q, tyl) ->
400
                  let ts = match q with
401 402
                    | Qident x when Mstr.mem x.id_str def ->
                        visit x.id_str
403
                    | Qident _ | Qdot _ ->
404
                        find_tysymbol th q
405
                  in
406
                  Loc.try2 ~loc:(qloc q) ty_app ts (List.map apply tyl)
407
              | PTtuple tyl ->
408 409
                  let ts = ts_tuple (List.length tyl) in
                  ty_app ts (List.map apply tyl)
410
              | PTarrow (ty1, ty2) ->
411
                  ty_func (apply ty1) (apply ty2)
412
              | PTparen ty ->
413
                  apply ty
414 415 416 417 418 419
            in
            create_tysymbol id vl (Some (apply ty))
        | TDabstract | TDalgebraic _ ->
            create_tysymbol id vl None
        | TDrecord _ ->
            assert false
420
      in
421
      Hstr.add tysymbols x (Some ts);
422 423
      ts
  in
424 425
  let th' =
    let add_ts (abstr,alias) d =
426
      let ts = visit d.td_ident.id_str in
427 428 429 430 431 432
      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
433 434
    with ClashSymbol s ->
      Loc.error ~loc:(Mstr.find s def).td_loc (ClashSymbol s)
435
  in
436
  let csymbols = Hstr.create 17 in
437
  let decl d (abstr,algeb,alias) =
438
    let ts = match Hstr.find tysymbols d.td_ident.id_str with
439
      | None ->
440
          assert false
441
      | Some ts ->
442
          ts
443
    in
444 445 446
    match d.td_def with
      | TDabstract -> ts::abstr, algeb, alias
      | TDalias _ -> abstr, algeb, ts::alias
447
      | TDalgebraic cl ->
448
          let ht = Hstr.create 17 in
449
          let constr = List.length cl 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_str = 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 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 th' pl in
468
            let pjl = List.map2 projection pl tyl in
469
            Hstr.replace csymbols id.id_str loc;
470
            create_fsymbol ~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
let prepare_typedef td =
491
  if td.td_vis <> Public then
492
    Loc.errorm ~loc:td.td_loc "pure types cannot be abstract or private";
493 494
  if td.td_mut then
    Loc.errorm ~loc:td.td_loc "pure types cannot be mutable";
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
      (* constructor for type t is "mk t" (and not String.capitalize t) *)
508
      let id = { td.td_ident with id_str = "mk " ^ td.td_ident.id_str } 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 =
518
    let id = d.ld_ident.id_str 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
    let ty = Opt.map (ty_of_pty th) d.ld_type in
522
    let ls = create_lsymbol v pl ty in
523
    Hstr.add lsymbols id ls;
524
    Loc.try2 ~loc:d.ld_loc add_param_decl th ls
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
525 526 527
  in
  let th' = List.fold_left create_symbol th dl in
  (* 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 554
  let abst,defn = List.fold_right type_decl dl ([],[]) in
  let th = List.fold_left add_param_decl th abst in
555
  if defn = [] then th else add_logic_decl th defn
556

557
let add_prop k s f th =
558
  let pr = create_prsymbol (create_user_id s) in
559
  let f = type_fmla th (fun _ -> None) f in
560
  add_prop_decl th k pr f
561

562
let loc_of_id id = Opt.get id.Ident.id_loc
563

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

597
(* parse declarations *)
598

599
let find_theory env file q = match q with
600
  | Qident { id_str = id } -> (* local theory *)
601
      begin try (Mstr.find id file).Pmodule.mod_theory
602
      with Not_found -> read_theory env [] id end
603
  | Qdot (p, { id_str = id }) -> (* theory in file f *)
604
      read_theory env (string_list_of_qualid p) id
605

606 607
let rec clone_ns kn sl path ns2 ns1 s =
  let qualid fmt path = Pp.print_list
608 609
    (fun fmt () -> Format.pp_print_char fmt '.')
    Format.pp_print_string fmt (List.rev path) in
610
  let s = Mstr.fold (fun nm ns1 acc ->
611 612
    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
613
  in
614
  let inst_ts = Mstr.fold (fun nm ts1 acc ->
615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635
    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
636
  in
637
  let inst_ls = Mstr.fold (fun nm ls1 acc ->
638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656
    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