typing.ml 29.5 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 Format
14
open Ident
15
open Ptree
16
open Ty
17
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
18
open Decl
19
open Theory
20
open Dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
21
open Env
Andrei Paskevich's avatar
Andrei Paskevich committed
22

23
(** debug flags *)
24

25
let debug_parse_only = Debug.register_flag "parse_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
26
  ~desc:"Stop@ after@ parsing."
27

28
let debug_type_only  = Debug.register_flag "type_only"
Andrei Paskevich's avatar
Andrei Paskevich committed
29
  ~desc:"Stop@ after@ type-checking."
30

31
(** errors *)
32

33 34 35
exception UnboundTypeVar of string
exception DuplicateTypeVar of string
exception ClashTheory of string
36

37
(** lazy declaration of tuples *)
38

39 40 41 42 43 44
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)
45

46
(** symbol lookup *)
47 48 49 50 51

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

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

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

62
exception UnboundSymbol of qualid
63

64 65 66 67 68 69
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
70

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

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

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

85 86 87 88 89 90 91 92
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
93

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

98 99 100 101 102 103 104 105
(** 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
106

107
let rec ty_of_pty uc = function
108
  | PPTtyvar ({id=x}, _) ->
109
      ty_var (create_user_tv x)
110
  | PPTtyapp (x, p) ->
111 112
      let ts = find_tysymbol x uc in
      let tyl = List.map (ty_of_pty uc) p in
113
      Loc.try2 ~loc:(qloc x) ty_app ts tyl
114 115 116
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
      ty_app ts (List.map (ty_of_pty uc) tyl)
117 118 119 120
  | PPTarrow (ty1, ty2) ->
      ty_func (ty_of_pty uc ty1) (ty_of_pty uc ty2)
  | PPTparen ty ->
      ty_of_pty uc ty
121 122

let opaque_tvs args value =
123 124 125 126 127 128 129
  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
130 131 132
  let acc = Opt.fold opaque_tvs Stv.empty value in
  List.fold_left (fun acc (_,_,_,ty) -> opaque_tvs acc ty) acc args

133
(** typing using destructive type variables
134

135 136 137 138 139 140
    parsed trees        intermediate trees       typed trees
      (Ptree)                (Dterm)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
*)
141

142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
(** 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

let dpattern uc pat =
  let rec ppat { pat_desc = desc; pat_loc = loc } =
    dpattern ~loc (match desc with
      | PPpwild -> DPwild
      | PPpvar x -> DPvar (create_user_id x)
      | PPpapp (x,pl) -> DPapp (find_lsymbol x uc, List.map ppat pl)
      | PPptuple pl -> DPapp (fs_tuple (List.length pl), List.map ppat pl)
      | PPprec fl ->
          let get_val _ _ = function
            Some p -> ppat p | None -> dpattern DPwild in
          let cs,fl = parse_record ~loc uc get_val fl in
          DPapp (cs,fl)
      | PPpas (p, x) -> DPas (ppat p, create_user_id x)
      | PPpor (p, q) -> DPor (ppat p, ppat q))
171
  in
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 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
  ppat pat

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

let dterm uc gvars denv pp =
  let rec pterm denv { pp_desc = desc; pp_loc = loc } =
    let highord_app e1 e2 =
      DTapp (fs_func_app, [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
    in
    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 ~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 ~loc (make_app de1 op de2) in
              let de23 = 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 ~loc (denv_get denv x) in
                DTapp (fs_func_app, [dterm ~loc acc; arg]) in
              let app = List.fold_left add (DTvar ("fc",dty)) uqu in
              let f = DTapp (ps_equ, [dterm ~loc app; e1]) in
              let f = DTquant (Tforall, qvl, trl, dterm ~loc f) in
              DTeps (id, dty, 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 ~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))
319
  in
320
  pterm denv pp
Andrei Paskevich's avatar
Andrei Paskevich committed
321

322 323 324
let type_term uc gfn t =
  let t = dterm uc gfn denv_empty t in
  Dterm.term ~strict:true ~keep_loc:true Mstr.empty t
Andrei Paskevich's avatar
Andrei Paskevich committed
325

326 327 328
let type_fmla uc gfn f =
  let f = dterm uc gfn denv_empty f in
  Dterm.fmla ~strict:true ~keep_loc:true Mstr.empty f
Andrei Paskevich's avatar
Andrei Paskevich committed
329

330
(** Typing declarations *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331

332 333 334 335 336
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
337 338
  List.map ty_of_param pl

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

464 465
let prepare_typedef td =
  if td.td_model then
466
    Loc.errorm ~loc:td.td_loc "model types are not allowed in pure theories";
467
  if td.td_vis <> Public then
468
    Loc.errorm ~loc:td.td_loc "pure types cannot be abstract or private";
469
  if td.td_inv <> [] then
470
    Loc.errorm ~loc:td.td_loc "pure types cannot have invariants";
471
  match td.td_def with
472 473 474
  | TDabstract | TDalgebraic _ | TDalias _ ->
      td
  | TDrecord fl ->
475 476
      let field { f_loc = loc; f_ident = id; f_pty = ty;
                  f_mutable = mut; f_ghost = gh } =
477 478
        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";
479
        loc, Some id, false, ty
480
      in
481 482
      (* 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
483 484 485
      { td with td_def = TDalgebraic [td.td_loc, id, List.map field fl] }

let add_types dl th =
486
  add_types (List.map prepare_typedef dl) th
487

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
565
let add_prop k loc s f th =
566
  let pr = create_prsymbol (create_user_id s) in
567
  let f = type_fmla th (fun _ -> None) f in
568
  Loc.try4 ~loc add_prop_decl th k pr f
569

570
let loc_of_id id = Opt.get id.Ident.id_loc
571

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

606
(* parse declarations *)
607

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
608
let prop_kind = function
609 610 611
  | Kaxiom -> Paxiom
  | Kgoal -> Pgoal
  | Klemma -> Plemma
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
612

613 614
let find_theory env lenv q = match q with
  | Qident { id = id } -> (* local theory *)
615
      begin try Mstr.find id lenv
Andrei Paskevich's avatar
Andrei Paskevich committed
616
      with Not_found -> read_lib_theory env [] id end
617 618
  | Qdot (p, { id = id }) -> (* theory in file f *)
      read_lib_theory env (string_list_of_qualid p) id
619

620 621 622 623
let rec clone_ns kn sl path ns2 ns1 s =
  let qualid fmt path = Pp.print_list
    (fun fmt () -> pp_print_char fmt '.')
    pp_print_string fmt (List.rev path) in
624
  let s = Mstr.fold (fun nm ns1 acc ->
625 626
    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
627
  in
628
  let inst_ts = Mstr.fold (fun nm ts1 acc ->
629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649
    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
650
  in
651
  let inst_ls = Mstr.fold (fun nm ls1 acc ->
652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670
    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
671 672 673
  in
  { s with inst_ts = inst_ts; inst_ls = inst_ls }

674
let add_decl loc th = function
675
  | Ptree.TypeDecl dl ->
676
      add_types dl th
677
  | Ptree.LogicDecl dl ->
678
      add_logics dl th
679
  | Ptree.IndDecl (s, dl) ->
680
      add_inductives s dl th
681
  | Ptree.PropDecl (k, s, f) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
682
      add_prop (prop_kind k) loc s f th
683
  | Ptree.Meta (id, al) ->
684
      let convert = function
685 686
        | PMAty (PPTtyapp (q,[]))
                   -> MAts (find_tysymbol q th)
687
        | PMAty ty -> MAty (ty_of_pty th ty)
688 689
        | PMAfs q  -> MAls (find_fsymbol q th)
        | PMAps q  -> MAls (find_psymbol q th)
690 691
        | PMApr q  -> MApr (find_prop q th)
        | PMAstr s -> MAstr s
692
        | PMAint i -> MAint i
693
      in
694
      let add s = add_meta th (lookup_meta s) (List.map convert al) in
695
      Loc.try1 ~loc add id.id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
696

697 698
let add_decl loc th d =
  if Debug.test_flag debug_parse_only then th else
699
  Loc.try3 ~loc add_decl loc th d
700

701 702 703 704
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
705 706
      let ns1 = Opt.fold find t.th_export p in
      let ns2 = Opt.fold find (get_namespace th) q in
707
      Loc.try6 ~loc clone_ns t.th_known t.th_local [] ns2 ns1 s
708
    | CStsym (loc,p,[],PPTtyapp (q,[])) ->
709 710 711
      let ts1 = find_tysymbol_ns p t.th_export in
      let ts2 = find_tysymbol q th in
      if Mts.mem ts1 s.inst_ts
712
      then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string);
713
      { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
714 715 716 717 718
    | 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
719
      let ts2 = Loc.try3 ~loc create_tysymbol id tvl def in
720
      if Mts.mem ts1 s.inst_ts
721
      then Loc.error ~loc (ClashSymbol ts1.ts_name.id_string);
722
      { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
723 724 725 726
    | 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
727
      then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string);
728 729 730 731 732
      { 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
733
      then Loc.error ~loc (ClashSymbol ls1.ls_name.id_string);
734 735 736 737
      { 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
738
      then Loc.error ~loc (ClashSymbol pr.pr_name.id_string);
739 740 741 742
      { 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
743
      then Loc.error ~loc (ClashSymbol pr.pr_name.id_string);
744 745 746 747
      { s with inst_goal = Spr.add pr s.inst_goal }
  in
  List.fold_left add_inst empty_inst s

748
let add_use_clone env lenv th loc (use, subst) =
749
  if Debug.test_flag debug_parse_only then th else
750
  let use_or_clone th =
751 752
    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;
753
    match subst with
754
    | None -> use_export th t
755 756 757
    | Some s ->
        warn_clone_not_abstract loc t;
        clone_export th t (type_inst th t s)
758
  in
759 760
  let use_or_clone th = match use.use_import with
    | Some (import, use_as) ->
761
        (* use T = namespace T use_export T end *)
762
        let th = open_namespace th use_as in
763
        let th = use_or_clone th in
764
        close_namespace th import
765 766
    | None ->
        use_or_clone th
767
  in
768
  Loc.try1 ~loc use_or_clone th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
769

770
let close_theory lenv th =
771
  if Debug.test_flag debug_parse_only then lenv else
772 773
  let th = close_theory th in
  let id = th.th_name.id_string in
774
  let loc = th.th_name.Ident.id_loc in
775
  if Mstr.mem id lenv then Loc.error ?loc (ClashTheory id);
776
  Mstr.add id th lenv
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
777

778
let close_namespace loc import th =
779
  Loc.try2 ~loc close_namespace th import
780

781 782 783 784 785 786 787 788
(* 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 =
789
      Stack.push (Theory.create_theory ~path (create_user_id id)) uc in
790 791
    let close_theory () =
      Stack.push (close_theory (Stack.pop lenv) (Stack.pop uc)) lenv in
792 793 794 795
    let open_namespace name =
      Stack.push (Theory.open_namespace (Stack.pop uc) name) uc in
    let close_namespace loc imp =
      Stack.push (close_namespace loc imp (Stack.pop uc)) uc in
796 797 798 799 800 801 802 803 804 805 806 807 808
    let new_decl loc d =
      Stack.push (add_decl loc (Stack.pop uc) d) uc in
    let use_clone loc use =
      let lenv = Stack.top lenv in
      Stack.push (add_use_clone env lenv (Stack.pop uc) loc use) uc in
    { open_theory = open_theory;
      close_theory = close_theory;
      open_namespace = open_namespace;
      close_namespace = close_namespace;
      new_decl = new_decl;
      use_clone = use_clone;
      open_module = (fun _ -> assert false);
      close_module = (fun _ -> assert false);
809
      new_pdecl = (fun _ -> assert false); }
810 811 812 813
  in
  let close_file () = Stack.pop lenv in
  open_file, close_file

814 815 816 817 818 819 820 821 822 823 824 825 826
(** Exception printing *)

let () = Exn_printer.register (fun fmt e -> match e with
  | UnboundSymbol q ->
      fprintf fmt "unbound symbol '%a'" print_qualid q
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
  | DuplicateTypeVar s ->
      fprintf fmt "duplicate type parameter '%s" s
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
  | _ -> raise e)

827
(*
828
Local Variables:
829
compile-command: "unset LANG; make -C ../.."
830
End:
831
*)