typing.ml 30.9 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
8 9 10 11 12 13 14 15 16 17 18
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19

20 21
open Util
open Format
22
open Pp
Andrei Paskevich's avatar
Andrei Paskevich committed
23
open Ptree
24
open Ident
25
open Ty
26
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
27
open Decl
28
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
29
open Env
30
open Denv
Andrei Paskevich's avatar
Andrei Paskevich committed
31

32 33
(** errors *)

34
type error =
35
  | Message of string
36
  | DuplicateTypeVar of string
37
  | TypeArity of qualid * int * int
38
  | Clash of string
39 40
  | PredicateExpected
  | TermExpected
41
  | BadNumberOfArguments of Ident.ident * int * int
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
42
  | ClashTheory of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
43
  | UnboundTheory of qualid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
44
  | AlreadyTheory of string
45 46 47 48
  | UnboundFile of string
  | UnboundDir of string
  | AmbiguousPath of string * string
  | NotInLoadpath of string
49 50
  | CyclicTypeDef
  | UnboundTypeVar of string
51 52
  | UnboundType of string list
  | UnboundSymbol of string list
53 54 55 56 57 58 59

exception Error of error

let error ?loc e = match loc with
  | None -> raise (Error e)
  | Some loc -> raise (Loc.Located (loc, Error e))

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
60 61 62
let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
63 64
  Format.kfprintf
    (fun _ ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
65 66 67
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
68
       error ?loc (Message s))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
69 70
    fmt f

71
let rec print_qualid fmt = function
72
  | Qident s -> fprintf fmt "%s" s.id
73
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
74

75
let report fmt = function
76 77
  | Message s ->
      fprintf fmt "%s" s
78
  | DuplicateTypeVar s ->
79
      fprintf fmt "duplicate type parameter %s" s
80
  | TypeArity (id, a, n) ->
81
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
82 83
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84
      fprintf fmt "Clash with previous symbol %s" id
85 86 87 88
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
89
  | BadNumberOfArguments (s, n, m) ->
90
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_string n;
91
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
92 93
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94 95
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96 97
  | AlreadyTheory s ->
      fprintf fmt "already using a theory with name %s" s
98 99 100 101 102 103 104 105
  | UnboundFile s ->
      fprintf fmt "no such file %s" s
  | UnboundDir s ->
      fprintf fmt "no such directory %s" s
  | AmbiguousPath (f1, f2) ->
      fprintf fmt "@[ambiguous path:@ both `%s'@ and `%s'@ match@]" f1 f2
  | NotInLoadpath f ->
      fprintf fmt "cannot find `%s' in loadpath" f
106 107 108 109
  | CyclicTypeDef ->
      fprintf fmt "cyclic type definition"
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
110 111 112 113
  | UnboundType sl ->
       fprintf fmt "Unbound type '%a'" (print_list dot pp_print_string) sl
  | UnboundSymbol sl ->
       fprintf fmt "Unbound symbol '%a'" (print_list dot pp_print_string) sl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114

115 116
let () = Exn_printer.register
  (fun fmt exn -> match exn with
117 118 119 120
    | Error error -> 
	report fmt error
    | _ -> 
	raise exn)
121

122 123
(** Environments *)

124
(** typing using destructive type variables
125

126 127 128 129 130 131
    parsed trees        intermediate trees       typed trees
      (Ptree)               (D below)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
      lexpr      --dfmla-->   dfmla     --fmla-->    fmla
132

133 134
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
135 136 137 138 139
let term_expected_type ~loc ty1 ty2 =
  errorm ~loc
    "@[This term has type %a@ but is expected to have type@ %a@]"
    print_dty ty1 print_dty ty2

140 141 142 143
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

144
type denv = {
145 146 147 148 149
  uc : theory_uc; (* the theory under construction *)
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
  dvars : dty Mstr.t; (* local variables, to be bound later *)
}

150 151 152
let create_denv uc = {
  uc = uc;
  utyvars = Hashtbl.create 17;
153 154 155 156 157 158 159 160 161 162 163 164
  dvars = Mstr.empty;
}

let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
    (* TODO: shouldn't we localize this ident? *)
    let v = create_tvsymbol (id_fresh x) in
    let v = create_ty_decl_var ~user:true v in
    Hashtbl.add env.utyvars x v;
    v
165

166 167 168 169
let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars
let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars }

170 171 172 173 174 175 176 177 178 179 180 181
(* parsed types -> intermediate types *)

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

let rec string_list_of_qualid acc = function
  | Qident id -> id.id :: acc
  | Qdot (p, id) -> string_list_of_qualid (id.id :: acc) p

let specialize_tysymbol loc p uc =
  let sl = string_list_of_qualid [] p in
182
  let ts =
183 184 185
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
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
  ts, List.length ts.ts_args

(* lazy declaration of tuples *)

let tuples_needed = Hashtbl.create 17

let ts_tuple n = Hashtbl.replace tuples_needed n (); ts_tuple n
let fs_tuple n = Hashtbl.replace tuples_needed n (); fs_tuple n

let add_tuple_decls uc =
  Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n)) 
    tuples_needed uc

let with_tuples ?(reset=false) f uc x =
  let uc = f (add_tuple_decls uc) x in
  if reset then Hashtbl.clear tuples_needed;
  uc

let add_ty_decl  = with_tuples add_ty_decl
let add_ty_decls = with_tuples ~reset:true add_ty_decls

let add_logic_decl  = with_tuples add_logic_decl
let add_logic_decls = with_tuples ~reset:true add_logic_decls

let add_ind_decl  = with_tuples add_ind_decl
let add_ind_decls = with_tuples ~reset:true add_ind_decls
212 213 214 215 216 217

let rec type_inst s ty = match ty.ty_node with
  | Ty.Tyvar n -> Mtv.find n s
  | Ty.Tyapp (ts, tyl) -> Tyapp (ts, List.map (type_inst s) tyl)

let rec dty env = function
218
  | PPTtyvar {id=x} ->
219 220 221
      Tyvar (find_user_type_var x env)
  | PPTtyapp (p, x) ->
      let loc = qloc x in
222
      let ts, a = specialize_tysymbol loc x env.uc in
223 224 225
      let np = List.length p in
      if np <> a then error ~loc (TypeArity (x, a, np));
      let tyl = List.map (dty env) p in
226
      begin match ts.ts_def with
227
	| None ->
228
	    Tyapp (ts, tyl)
229
	| Some ty ->
230 231 232
	    let add m v t = Mtv.add v t m in
            let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
	    type_inst s ty
233 234 235 236
      end
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
      Tyapp (ts, List.map (dty env) tyl)
237 238 239 240

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
241
  try find ns sl
242 243
  with Not_found -> error ~loc (UnboundSymbol sl)

244
let find_prop_ns = find_ns ns_find_pr
245 246 247 248 249 250 251 252 253 254
let find_prop p uc = find_prop_ns p (get_namespace uc)

let find_tysymbol_ns = find_ns ns_find_ts
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)

let find_lsymbol_ns = find_ns ns_find_ls
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)

let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
255
  s, specialize_lsymbol ~loc:(qloc p) s
256

257
let specialize_fsymbol p uc =
258
  let s, (tl, ty) = specialize_lsymbol p uc in
259
  match ty with
260
    | None -> let loc = qloc p in error ~loc TermExpected
261
    | Some ty -> s, tl, ty
262

263
let specialize_psymbol p uc =
264
  let s, (tl, ty) = specialize_lsymbol p uc in
265 266
  match ty with
    | None -> s, tl
267 268 269 270 271
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

let is_psymbol p uc = 
  let s = find_lsymbol p uc in
  s.ls_value = None
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
272

273

274 275
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
276 277 278 279
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

280
(** Typing terms and formulas *)
281 282 283 284 285 286 287

let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

Andrei Paskevich's avatar
Andrei Paskevich committed
288
let check_pat_linearity p =
Andrei Paskevich's avatar
Andrei Paskevich committed
289
  let s = ref Sstr.empty in
290
  let add id =
291
    if Sstr.mem id.id !s then
292
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
Andrei Paskevich's avatar
Andrei Paskevich committed
293
    s := Sstr.add id.id !s
294 295 296 297
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
298
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
299
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
300
    | PPpor (p, _) -> check p
301
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
302
  check p
303

304 305 306 307
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
  Tyvar (create_ty_decl_var ~loc ~user:false tv)

Andrei Paskevich's avatar
Andrei Paskevich committed
308 309 310 311 312
let rec dpat env pat =
  let env, n, ty = dpat_node pat.pat_loc env pat.pat_desc in
  env, { dp_node = n; dp_ty = ty }

and dpat_node loc env = function
313
  | PPpwild ->
314
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
315
      env, Pwild, ty
Andrei Paskevich's avatar
Andrei Paskevich committed
316
  | PPpvar x ->
317
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
318
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
319 320
      env, Pvar x, ty
  | PPpapp (x, pl) ->
321
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
322 323
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      env, Papp (s, pl), ty
324 325 326 327 328 329 330
  | PPptuple pl ->
      let n = List.length pl in
      let s = fs_tuple n in
      let tyl = List.map (fun _ -> fresh_type_var loc) pl in
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      let ty = Tyapp (ts_tuple n, tyl) in
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
331
  | PPpas (p, x) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
332
      let env, p = dpat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
333
      let env = { env with dvars = Mstr.add x.id p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
334
      env, Pas (p,x), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
335 336 337 338 339 340
  | PPpor (p, q) ->
      let env, p = dpat env p in
      let env, q = dpat env q in
      if not (unify p.dp_ty q.dp_ty)
        then term_expected_type ~loc p.dp_ty q.dp_ty;
      env, Por (p,q), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
341

342
and dpat_args s loc env el pl =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
343
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
344
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
345
  let rec check_arg env = function
346
    | [], [] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
347 348 349 350 351 352 353
	env, []
    | a :: al, p :: pl ->
	let loc = p.pat_loc in
	let env, p = dpat env p in
	if not (unify a p.dp_ty) then term_expected_type ~loc p.dp_ty a;
	let env, pl = check_arg env (al, pl) in
	env, p :: pl
Andrei Paskevich's avatar
Andrei Paskevich committed
354 355 356
    | _ ->
	assert false
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
357
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
358

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
359
let rec trigger_not_a_term_exn = function
360
  | Error TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
361 362 363
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

364
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
365
  let s = ref Sstr.empty in
366
  let check id =
Andrei Paskevich's avatar
Andrei Paskevich committed
367 368
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
369
  in
370
  List.iter (fun (idl, _) -> Util.option_iter check idl) uqu
371

372
let rec dterm env t =
373 374 375 376
  let n, ty = dterm_node t.pp_loc env t.pp_desc in
  { dt_node = n; dt_ty = ty }

and dterm_node loc env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
377
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
378
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
379
      let ty = Mstr.find x env.dvars in
380
      Tvar x, ty
381
  | PPvar x ->
382
      (* 0-arity symbol (constant) *)
383
      let s, tyl, ty = specialize_fsymbol x env.uc in
384
      let n = List.length tyl in
385
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
386
      Tapp (s, []), ty
387
  | PPapp (x, tl) ->
388
      let s, tyl, ty = specialize_fsymbol x env.uc in
389
      let tl = dtype_args s.ls_name loc env tyl tl in
390
      Tapp (s, tl), ty
391 392 393 394 395 396 397
  | PPtuple tl ->
      let n = List.length tl in
      let s = fs_tuple n in
      let tyl = List.map (fun _ -> fresh_type_var loc) tl in
      let tl = dtype_args s.ls_name loc env tyl tl in
      let ty = Tyapp (ts_tuple n, tyl) in
      Tapp (s, tl), ty
398 399 400 401
  | PPinfix (e1, x, e2) ->
      let s, tyl, ty = specialize_fsymbol (Qident x) env.uc in
      let tl = dtype_args s.ls_name loc env tyl [e1; e2] in
      Tapp (s, tl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
402
  | PPconst (ConstInt _ as c) ->
403
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
404
  | PPconst (ConstReal _ as c) ->
405
      Tconst c, Tyapp (Ty.ts_real, [])
Andrei Paskevich's avatar
Andrei Paskevich committed
406
  | PPlet (x, e1, e2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
407 408
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
409
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410 411
      let e2 = dterm env e2 in
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
412 413 414
  | PPmatch (e1, bl) ->
      let t1 = dterm env e1 in
      let ty1 = t1.dt_ty in
415
      let tb = fresh_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
416 417
      let branch (p, e) =
        let env, p = dpat_list env ty1 p in
418
        let loc = e.pp_loc in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
419 420
	let e = dterm env e in
	if not (unify e.dt_ty tb) then term_expected_type ~loc e.dt_ty tb;
Andrei Paskevich's avatar
Andrei Paskevich committed
421
        p, e
Andrei Paskevich's avatar
Andrei Paskevich committed
422 423 424
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
425
      Tmatch (t1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
426 427 428
  | PPnamed (x, e1) ->
      let e1 = dterm env e1 in
      Tnamed (x, e1), e1.dt_ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429 430 431 432 433 434
  | PPcast (e1, ty) ->
      let loc = e1.pp_loc in
      let e1 = dterm env e1 in
      let ty = dty env ty in
      if not (unify e1.dt_ty ty) then term_expected_type ~loc e1.dt_ty ty;
      e1.dt_node, ty
435 436 437 438 439 440 441
  | PPif (e1, e2, e3) ->
      let loc = e3.pp_loc in
      let e2 = dterm env e2 in
      let e3 = dterm env e3 in
      if not (unify e2.dt_ty e3.dt_ty) then
        term_expected_type ~loc e3.dt_ty e2.dt_ty;
      Tif (dfmla env e1, e2, e3), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
442
  | PPeps (x, ty, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
443
      let ty = dty env ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
444
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
445 446
      let e1 = dfmla env e1 in
      Teps (x, ty, e1), ty
447
  | PPquant _
448
  | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
449
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
450

451 452 453 454 455
and dfmla env e = match e.pp_desc with
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
456
  | PPunop (PPnot, a) ->
457
      Fnot (dfmla env a)
458
  | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
459 460
      Fbinop (binop op, dfmla env a, dfmla env b)
  | PPif (a, b, c) ->
461
      Fif (dfmla env a, dfmla env b, dfmla env c)
462
  | PPquant (q, uqu, trl, a) ->
463
      check_quant_linearity uqu;
464 465
      let uquant env (idl,ty) =
        let ty = dty env ty in
466
        let id = match idl with
Andrei Paskevich's avatar
Andrei Paskevich committed
467
          | Some id -> id
468
          | None -> assert false
469
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
470
        { env with dvars = Mstr.add id.id ty env.dvars }, (id,ty)
471
      in
472
      let env, uqu = map_fold_left uquant env uqu in
473
      let trigger e =
474 475
	try
	  TRterm (dterm env e)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
476
	with exn when trigger_not_a_term_exn exn ->
477
	  TRfmla (dfmla env e)
478 479
      in
      let trl = List.map (List.map trigger) trl in
480 481
      let q = match q with
        | PPforall -> Fforall
482 483 484
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
485
  | PPapp (x, tl) ->
486
      let s, tyl = specialize_psymbol x env.uc in
487
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
488
      Fapp (s, tl)
489 490 491 492 493 494 495 496 497 498
  | PPinfix (e12, op2, e3) ->
      begin match e12.pp_desc with
	| PPinfix (_, op1, e2) when is_psymbol (Qident op1) env.uc ->
	    let e23 = { e with pp_desc = PPinfix (e2, op2, e3) } in
	    Fbinop (Fand, dfmla env e12, dfmla env e23)
	| _ ->
	    let s, tyl = specialize_psymbol (Qident op2) env.uc in
	    let tl = dtype_args s.ls_name e.pp_loc env tyl [e12; e3] in
	    Fapp (s, tl)
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
499
  | PPlet (x, e1, e2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
500 501
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
502
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
503 504
      let e2 = dfmla env e2 in
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
505 506 507 508 509
  | PPmatch (e1, bl) ->
      let t1 = dterm env e1 in
      let ty1 = t1.dt_ty in
      let branch (p, e) =
        let env, p = dpat_list env ty1 p in p, dfmla env e
Andrei Paskevich's avatar
Andrei Paskevich committed
510
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
511
      Fmatch (t1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
512 513 514
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
515
  | PPvar x ->
516 517
      let pr = find_prop x env.uc in
      Fvar (Decl.find_prop (Theory.get_known env.uc) pr)
518
  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ ->
519
      error ~loc:e.pp_loc PredicateExpected
520

Andrei Paskevich's avatar
Andrei Paskevich committed
521 522 523 524 525 526 527
and dpat_list env ty p =
  check_pat_linearity p;
  let loc = p.pat_loc in
  let env, p = dpat env p in
  if not (unify p.dp_ty ty)
    then term_expected_type ~loc p.dp_ty ty;
  env, p
528

529 530 531 532
and dtype_args s loc env el tl =
  let n = List.length el and m = List.length tl in
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
  let rec check_arg = function
533
    | [], [] ->
534 535 536 537
	[]
    | a :: al, t :: bl ->
	let loc = t.pp_loc in
	let t = dterm env t in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
538
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
539 540 541 542 543 544
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560
(** Add projection functions for the algebraic types *)

let add_projection cl p (fs,tyarg,tyval) th =
  let vs = create_vsymbol (id_fresh p) tyval in
  let per_cs (_,id,pl) =
    let cs = find_lsymbol (Qident id) th in
    let tc = match cs.ls_value with
      | None -> assert false
      | Some t -> t
    in
    let m = ty_match Mtv.empty tc tyarg in
    let per_param ty (n,_) = match n with
      | Some id when id.id = p -> pat_var vs
      | _ -> pat_wild (ty_inst m ty)
    in
    let al = List.map2 per_param cs.ls_args pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
561
    pat_app cs al tyarg, t_var vs
562 563
  in
  let vs = create_vsymbol (id_fresh "u") tyarg in
Andrei Paskevich's avatar
Andrei Paskevich committed
564
  let t = t_case (t_var vs) (List.map per_cs cl) tyval in
565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589
  let d = make_fs_defn fs [vs] t in
  add_logic_decl th [d]

let add_projections th d = match d.td_def with
  | TDabstract | TDalias _ -> th
  | TDalgebraic cl ->
      let per_cs acc (_,id,pl) =
        let cs = find_lsymbol (Qident id) th in
        let tc = match cs.ls_value with
          | None -> assert false
          | Some t -> t
        in
        let per_param acc ty (n,_) = match n with
          | Some id when not (Mstr.mem id.id acc) ->
              let fn = id_user id.id id.id_loc in
              let fs = create_fsymbol fn [tc] ty in
              Mstr.add id.id (fs,tc,ty) acc
          | _ -> acc
        in
        List.fold_left2 per_param acc cs.ls_args pl
      in
      let ps = List.fold_left per_cs Mstr.empty cl in
      try Mstr.fold (add_projection cl) ps th
      with e -> raise (Loc.Located (d.td_loc, e))

590
(** Typing declarations, that is building environments. *)
591 592 593

open Ptree

594
let add_types dl th =
595 596 597 598 599 600
  let def = List.fold_left 
    (fun def d ->
      let id = d.td_ident.id in 
      if Mstr.mem id def then error ~loc:d.td_loc (Clash id);
      Mstr.add id d def) 
    Mstr.empty dl 
601
  in
602
  let tysymbols = Hashtbl.create 17 in
603
  let rec visit x =
604 605 606 607 608 609
    try
      match Hashtbl.find tysymbols x with
	| None -> error CyclicTypeDef
	| Some ts -> ts
    with Not_found ->
      Hashtbl.add tysymbols x None;
Andrei Paskevich's avatar
Andrei Paskevich committed
610
      let d = Mstr.find x def in
611 612
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
613 614 615 616
      let vl =
	List.map
	  (fun v ->
	     if Hashtbl.mem vars v.id then
617
	       error ~loc:v.id_loc (DuplicateTypeVar v.id);
618
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
619 620
	     Hashtbl.add vars v.id i;
	     i)
621
	  d.td_params
622
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
623
      let id = id_user id d.td_loc in
624
      let ts = match d.td_def with
625
	| TDalias ty ->
626
	    let rec apply = function
627 628
	      | PPTtyvar v ->
		  begin
629 630 631 632 633
		    try ty_var (Hashtbl.find vars v.id)
		    with Not_found -> error ~loc:v.id_loc (UnboundTypeVar v.id)
		  end
	      | PPTtyapp (tyl, q) ->
		  let ts = match q with
Andrei Paskevich's avatar
Andrei Paskevich committed
634
		    | Qident x when Mstr.mem x.id def ->
635 636 637 638
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
639
		  begin try
640
		    ty_app ts (List.map apply tyl)
641
		  with Ty.BadTypeArity (_, tsal, tyll) ->
642
		    error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
643 644 645 646
		  end
	      | PPTtuple tyl ->
		  let ts = ts_tuple (List.length tyl) in
		  ty_app ts (List.map apply tyl)
647 648
	    in
	    create_tysymbol id vl (Some (apply ty))
649
	| TDabstract | TDalgebraic _ ->
650 651 652 653 654
	    create_tysymbol id vl None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
655
  let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in 
656
  let th' = try add_ty_decl th tsl
657
    with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (Clash s)
658
  in
659
  let csymbols = Hashtbl.create 17 in
660
  let decl d =
661
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
662
      | None ->
663
	  assert false
664
      | Some ts ->
665 666
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
667 668
	  List.iter
	    (fun v ->
669
	       Hashtbl.add vars v.tv_name.id_string
670
                  (create_ty_decl_var ~user:true v))
671 672 673 674
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
675
      | TDabstract | TDalias _ ->
676
	  Tabstract
677
      | TDalgebraic cl ->
678
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
679
	  let constructor (loc, id, pl) =
680
	    let param (_,t) = ty_of_dty (dty th' t) in
681
	    let tyl = List.map param pl in
682
	    Hashtbl.replace csymbols id.id loc;
683
	    create_fsymbol (id_user id.id loc) tyl ty
684 685 686 687
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
688
  in
689 690 691 692
  let th = try add_ty_decls th (List.map decl dl)
    with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
  in
  List.fold_left add_projections th dl
693

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
694
let env_of_vsymbol_list vl =
695
  List.fold_left (fun env v -> Mstr.add v.vs_name.id_string v env) Mstr.empty vl
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
696

697
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
698 699
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
700
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
701
  (* 1. create all symbols and make an environment with these symbols *)
702
  let create_symbol th d =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
703
    let id = d.ld_ident.id in
Andrei Paskevich's avatar
Andrei Paskevich committed
704
    let v = id_user id d.ld_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
705
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
706
    Hashtbl.add denvs id denv;
707
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
708
    let pl = List.map type_ty d.ld_params in
709
    try match d.ld_type with
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
710 711 712
      | None -> (* predicate *)
	  let ps = create_psymbol v pl in
	  Hashtbl.add psymbols id ps;
713
	  add_logic_decl th [ps, None]
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
714 715
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
716
	  let fs = create_fsymbol v pl t in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
717
	  Hashtbl.add fsymbols id fs;
718
	  add_logic_decl th [fs, None]
719
    with ClashSymbol s -> error ~loc:d.ld_loc (Clash s)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
720 721 722
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
723
  let type_decl d =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
724 725 726
    let id = d.ld_ident.id in
    let dadd_var denv (x, ty) = match x with
      | None -> denv
Andrei Paskevich's avatar
Andrei Paskevich committed
727
      | Some id -> { denv with dvars = Mstr.add id.id (dty denv ty) denv.dvars }
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
728
    in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
729
    let denv = Hashtbl.find denvs id in
730
    let denv = { denv with uc = th' } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
731
    let denv = List.fold_left dadd_var denv d.ld_params in
732 733
    let create_var (x, _) ty =
      let id = match x with
734 735
	| None -> id_fresh "%x"
	| Some id -> id_user id.id id.id_loc
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
736 737 738
      in
      create_vsymbol id ty
    in
739
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
740 741 742
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
743 744
        begin match d.ld_def with
	  | None -> ps,None
745
	  | Some f ->
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
746
	      let f = dfmla denv f in
747 748 749 750
              let vl = match ps.ls_value with
                | None -> mk_vlist ps.ls_args
                | _ -> assert false
              in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
751
	      let env = env_of_vsymbol_list vl in
752 753
              make_ps_defn ps vl (fmla env f)
        end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
754
    | Some ty -> (* function *)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
755
	let fs = Hashtbl.find fsymbols id in
756 757
        begin match d.ld_def with
	  | None -> fs,None
758
	  | Some t ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
759
	      let loc = t.pp_loc in
760
	      let ty = dty denv ty in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
761
	      let t = dterm denv t in
762 763
	      if not (unify t.dt_ty ty) then 
		term_expected_type ~loc t.dt_ty ty;
764 765 766 767
              let vl = match fs.ls_value with
                | Some _ -> mk_vlist fs.ls_args
                | _ -> assert false
              in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
768
	      let env = env_of_vsymbol_list vl in
769
	      make_fs_defn fs vl (term env t)
770
        end
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
771
  in
772
  add_logic_decls th (List.map type_decl dl)
773

774
let type_term denv env t =
775
  let t = dterm denv t in
776
  term env t
777

778
let term uc = type_term (create_denv uc) Mstr.empty
779

780
let type_fmla denv env f =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
781
  let f = dfmla denv f in
782
  fmla env f
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
783

784
let fmla uc = type_fmla (create_denv uc) Mstr.empty
785

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
786
let add_prop k loc s f th =
787 788
  let pr = create_prsymbol (id_user s.id loc) in
  try add_prop_decl th k pr (fmla th f)
789
  with ClashSymbol s -> error ~loc (Clash s)