typing.ml 37.6 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7
(*    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 35 36 37 38 39 40 41 42 43 44 45 46
exception Message of string
exception DuplicateTypeVar of string
exception TypeArity of qualid * int * int
exception Clash of string
exception PredicateExpected
exception TermExpected
exception BadNumberOfArguments of Ident.ident * int * int
exception ClashTheory of string
exception UnboundTheory of qualid
exception CyclicTypeDef
exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list
47 48

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52 53 54
let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
55 56
  Format.kfprintf
    (fun _ ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
57 58 59
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
60
       error ?loc (Message s))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
61 62
    fmt f

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

67
let () = Exn_printer.register (fun fmt e -> match e with
68 69
  | Message s ->
      fprintf fmt "%s" s
70
  | DuplicateTypeVar s ->
71
      fprintf fmt "duplicate type parameter %s" s
72
  | TypeArity (id, a, n) ->
73
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
74 75
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76
      fprintf fmt "Clash with previous symbol %s" id
77 78 79 80
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
81
  | BadNumberOfArguments (s, n, m) ->
82
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_string n;
83
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84 85
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86 87
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
88 89 90 91
  | CyclicTypeDef ->
      fprintf fmt "cyclic type definition"
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
92 93 94 95
  | 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
96
  | _ -> raise e)
97

98 99 100
let debug_parse_only = Debug.register_flag "parse_only"
let debug_type_only  = Debug.register_flag "type_only"

101 102
(** Environments *)

103
(** typing using destructive type variables
104

105 106 107 108 109 110
    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
111

112 113
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114 115 116 117 118
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

119 120 121 122
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

123
type denv = {
124 125 126 127 128
  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 *)
}

129 130 131
let create_denv uc = {
  uc = uc;
  utyvars = Hashtbl.create 17;
132 133 134 135 136 137 138 139 140 141 142 143
  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
144

145 146 147 148
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 }

149 150 151
let print_denv fmt denv =
  Mstr.iter (fun x ty -> fprintf fmt "%s:%a,@ " x print_dty ty) denv.dvars

152 153 154 155 156 157 158 159 160 161 162 163
(* 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
164
  let ts =
165 166 167
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
168 169 170 171 172 173 174 175 176 177
  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 =
178
  Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n))
179 180 181 182 183 184 185 186
    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
187
let add_ty_decls = with_tuples ~reset:true add_ty_decl
188 189

let add_logic_decl  = with_tuples add_logic_decl
190
let add_logic_decls = with_tuples ~reset:true add_logic_decl
191 192

let add_ind_decl  = with_tuples add_ind_decl
193
let add_ind_decls = with_tuples ~reset:true add_ind_decl
194

195 196
let add_prop_decl = with_tuples ~reset:true add_prop_decl

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

let rec dty env = function
202
  | PPTtyvar {id=x} ->
203
      tyvar (find_user_type_var x env)
204 205
  | PPTtyapp (p, x) ->
      let loc = qloc x in
206
      let ts, a = specialize_tysymbol loc x env.uc in
207 208 209
      let np = List.length p in
      if np <> a then error ~loc (TypeArity (x, a, np));
      let tyl = List.map (dty env) p in
210
      begin match ts.ts_def with
211
	| None ->
212
	    tyapp (ts, tyl)
213
	| Some ty ->
214 215 216
	    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
217 218 219
      end
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
220
      tyapp (ts, List.map (dty env) tyl)
221 222 223 224

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
225
  try find ns sl
226 227
  with Not_found -> error ~loc (UnboundSymbol sl)

228
let find_prop_ns = find_ns ns_find_pr
229 230 231 232 233 234 235 236
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)

237 238 239
let find_namespace_ns = find_ns ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)

240 241
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
242 243
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
244

245
let specialize_fsymbol p uc =
246
  let s,tl,ty = specialize_lsymbol p uc in
247
  match ty with
248
    | None -> let loc = qloc p in error ~loc TermExpected
249
    | Some ty -> s, tl, ty
250

251
let specialize_psymbol p uc =
252
  let s,tl,ty = specialize_lsymbol p uc in
253 254
  match ty with
    | None -> s, tl
255 256
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

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

261

262 263
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
264 265 266 267
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

268
(** Typing terms and formulas *)
269 270 271 272 273 274 275

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

Andrei Paskevich's avatar
Andrei Paskevich committed
276
let check_pat_linearity p =
Andrei Paskevich's avatar
Andrei Paskevich committed
277
  let s = ref Sstr.empty in
278
  let add id =
279
    if Sstr.mem id.id !s then
280
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
Andrei Paskevich's avatar
Andrei Paskevich committed
281
    s := Sstr.add id.id !s
282 283 284 285
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
286
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
287
    | PPpas (p, id) -> check p; add id
Andrei Paskevich's avatar
Andrei Paskevich committed
288
    | PPpor (p, _) -> check p
289
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
290
  check p
291

292 293
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
294
  tyvar (create_ty_decl_var ~loc ~user:false tv)
295

Andrei Paskevich's avatar
Andrei Paskevich committed
296 297 298 299 300
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
301
  | PPpwild ->
302
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
303
      env, Pwild, ty
Andrei Paskevich's avatar
Andrei Paskevich committed
304
  | PPpvar x ->
305
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
306
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
307 308
      env, Pvar x, ty
  | PPpapp (x, pl) ->
309
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
310 311
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      env, Papp (s, pl), ty
312 313 314 315 316
  | 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
317
      let ty = tyapp (ts_tuple n, tyl) in
318
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
319
  | PPpas (p, x) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
320
      let env, p = dpat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
321
      let env = { env with dvars = Mstr.add x.id p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
322
      env, Pas (p,x), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
323 324 325 326 327 328
  | 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
329

330
and dpat_args s loc env el pl =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
331
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
332
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
333
  let rec check_arg env = function
334
    | [], [] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
335 336 337 338 339 340 341
	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
342 343 344
    | _ ->
	assert false
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
345
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
346

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
347
let rec trigger_not_a_term_exn = function
348
  | TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
349 350 351
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

352
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
353
  let s = ref Sstr.empty in
354
  let check id =
Andrei Paskevich's avatar
Andrei Paskevich committed
355 356
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
357
  in
358
  List.iter (fun (idl, _) -> Util.option_iter check idl) uqu
359

Andrei Paskevich's avatar
Andrei Paskevich committed
360 361 362 363 364 365 366 367 368
let check_highord env x tl = match x with
  | Qident { id = x } when Mstr.mem x env.dvars -> true
  | _ -> List.length tl > List.length ((find_lsymbol x env.uc).ls_args)

let apply_highord loc x tl = match List.rev tl with
  | a::[] -> [{pp_loc = loc; pp_desc = PPvar x}; a]
  | a::tl -> [{pp_loc = loc; pp_desc = PPapp (x, List.rev tl)}; a]
  | [] -> assert false

369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416
(* [is_projection uc ls] returns
   - [Some (ts, lsc, i)] if [ls] is the i-th projection of an
     algebraic datatype [ts] with only one constructor [lcs]
   - [None] otherwise 
 *)
let is_projection uc ls = 
  try
    let ts = match ls.ls_args, ls.ls_value with
      | [{ty_node = Ty.Tyapp (ts, _)}], Some _ -> ts
      | _ -> (* not a function with 1 argument *) raise Exit
    in
    let kn = get_known uc in
    let lsc = match Decl.find_constructors kn ts with
      | [lsc] -> lsc
      | _ -> (* 0 or several constructors *) raise Exit
    in
    let def = match Decl.find_logic_definition kn ls with
      | Some def -> def
      | None -> (* no definition *) raise Exit
    in
    let v, t = match Decl.open_fs_defn def with
      | [v], t -> v, t
      | _ -> assert false
    in
    let b = match t.t_node with
      | Tcase ({t_node=Term.Tvar v'}, [b]) when vs_equal v' v -> b
      | _ -> raise Exit
    in
    let p, t = t_open_branch b in
    let pl = match p with
      | { pat_node = Term.Papp (lsc', pl) } when ls_equal lsc lsc' -> pl
      | _ -> raise Exit
    in
    let i = match t.t_node with 
      | Term.Tvar xi -> 
	  let rec index i = function 
	    | [] -> raise Exit
	    | { pat_node = Term.Pvar v} :: _ when vs_equal v xi -> i
	    | _ :: l -> index (i+1) l
	  in
	  index 0 pl
      | _ -> 
	  raise Exit
    in
    Some (ts, lsc, i)
  with Exit ->
    None

417 418 419 420 421 422 423 424 425 426
let rec dterm ?(localize=false) env { pp_loc = loc; pp_desc = t } =
  let n, ty = dterm_node ~localize loc env t in
  let t = { dt_node = n; dt_ty = ty } in
  if localize then
    let n = Tnamed (Ident.label ~loc "", t) in
    { dt_node = n; dt_ty = ty }
  else
    t

and dterm_node ~localize loc env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
427
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
428
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
429
      let ty = Mstr.find x env.dvars in
430
      Tvar x, ty
431
  | PPvar x ->
432
      (* 0-arity symbol (constant) *)
433
      let s, tyl, ty = specialize_fsymbol x env.uc in
434
      let n = List.length tyl in
435
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
436
      Tapp (s, []), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
437 438 439 440 441
  | PPapp (x, tl) when check_highord env x tl ->
      let tl = apply_highord loc x tl in
      let atyl, aty = Denv.specialize_lsymbol ~loc fs_func_app in
      let tl = dtype_args fs_func_app.ls_name loc env atyl tl in
      Tapp (fs_func_app, tl), Util.of_option aty
442
  | PPapp (x, tl) ->
443
      let s, tyl, ty = specialize_fsymbol x env.uc in
444
      let tl = dtype_args s.ls_name loc env tyl tl in
445
      Tapp (s, tl), ty
446 447 448 449 450
  | 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
451
      let ty = tyapp (ts_tuple n, tyl) in
452
      Tapp (s, tl), ty
453 454 455 456
  | 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
457
  | PPconst (ConstInt _ as c) ->
458
      Tconst c, tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
459
  | PPconst (ConstReal _ as c) ->
460
      Tconst c, tyapp (Ty.ts_real, [])
Andrei Paskevich's avatar
Andrei Paskevich committed
461
  | PPlet (x, e1, e2) ->
462
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
463
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
464
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
465
      let e2 = dterm ~localize env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
466
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
467
  | PPmatch (e1, bl) ->
468
      let t1 = dterm ~localize env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
469
      let ty1 = t1.dt_ty in
470
      let tb = fresh_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
471 472
      let branch (p, e) =
        let env, p = dpat_list env ty1 p in
473
        let loc = e.pp_loc in
474
	let e = dterm ~localize env e in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
475
	if not (unify e.dt_ty tb) then term_expected_type ~loc e.dt_ty tb;
Andrei Paskevich's avatar
Andrei Paskevich committed
476
        p, e
Andrei Paskevich's avatar
Andrei Paskevich committed
477 478 479
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
480
      Tmatch (t1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
481
  | PPnamed (x, e1) ->
482
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
483
      Tnamed (x, e1), e1.dt_ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
484 485
  | PPcast (e1, ty) ->
      let loc = e1.pp_loc in
486
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
487 488 489
      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
490 491
  | PPif (e1, e2, e3) ->
      let loc = e3.pp_loc in
492 493
      let e2 = dterm ~localize env e2 in
      let e3 = dterm ~localize env e3 in
494 495
      if not (unify e2.dt_ty e3.dt_ty) then
        term_expected_type ~loc e3.dt_ty e2.dt_ty;
496
      Tif (dfmla ~localize env e1, e2, e3), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
497
  | PPeps (x, ty, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
498
      let ty = dty env ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
499
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
500
      let e1 = dfmla ~localize env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
501
      Teps (x, ty, e1), ty
502
  | PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
503 504 505 506 507 508 509 510 511 512 513 514
      check_quant_linearity uqu;
      let uquant env (idl,ty) =
        let ty = dty env ty in
        let id = match idl with
          | Some id -> id
          | None -> assert false
        in
        { env with dvars = Mstr.add id.id ty env.dvars }, (id,ty)
      in
      let env, uqu = map_fold_left uquant env uqu in
      let trigger e =
	try
515
	  TRterm (dterm ~localize env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
516
	with exn when trigger_not_a_term_exn exn ->
517
	  TRfmla (dfmla ~localize env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
518 519
      in
      let trl = List.map (List.map trigger) trl in
520
      let e = match q with
521 522
        | PPfunc -> TRterm (dterm ~localize env a)
        | PPpred -> TRfmla (dfmla ~localize env a)
523 524 525 526
        | PPlambda -> trigger a
        | _ -> assert false
      in
      let id, ty, f = match e with
Andrei Paskevich's avatar
Andrei Paskevich committed
527
        | TRterm t ->
528
            let id = { id = "fc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
529
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
530
              let nty = tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
Andrei Paskevich's avatar
Andrei Paskevich committed
531 532 533 534 535 536 537 538 539
              uqu ([],t.dt_ty)
            in
            let h = { dt_node = Tvar id.id ; dt_ty = ty } in
            let h = List.fold_left2 (fun h (uid,uty) ty ->
              let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
              { dt_node = Tapp (fs_func_app, [h;u]) ; dt_ty = ty })
              h uqu tyl
            in
            id, ty, Fapp (ps_equ, [h;t])
Andrei Paskevich's avatar
Andrei Paskevich committed
540
        | TRfmla f ->
541
            let id = { id = "pc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
542 543 544 545 546
            let (uid,uty),uqu = match List.rev uqu with
              | uq :: uqu -> uq, List.rev uqu
              | [] -> assert false
            in
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
547 548
              let nty = tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
              uqu ([],tyapp (ts_pred, [uty]))
Andrei Paskevich's avatar
Andrei Paskevich committed
549 550 551 552 553 554 555 556 557 558 559
            in
            let h = { dt_node = Tvar id.id ; dt_ty = ty } in
            let h = List.fold_left2 (fun h (uid,uty) ty ->
              let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
              { dt_node = Tapp (fs_func_app, [h;u]) ; dt_ty = ty })
              h uqu tyl
            in
            let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
            id, ty, Fbinop (Fiff, Fapp (ps_pred_app, [h;u]), f)
      in
      Teps (id, ty, Fquant (Fforall, uqu, trl, f)), ty
560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598
  | PPrecord fl ->
      let type_field (q, e) = 
	let loc = qloc q in
	let ls, tyl, ty = specialize_fsymbol q env.uc in
	match is_projection env.uc ls, tyl with
	  | None, _ -> 
	      errorm ~loc "this is not a record field"
	  | Some (ts, ls, i), [tya] -> 
	      let loce = e.pp_loc in
	      let e = dterm ~localize env e in
	      if not (unify e.dt_ty ty) then 
		term_expected_type ~loc:loce e.dt_ty ty;
	      ts, (loc, ls, i, tya), e
	  | _ -> 
	      assert false
      in
      let fl = List.map type_field fl in
      let ts,(_,ls,_,ty),_ = match fl with [] -> assert false | x :: _ -> x in
      let args = Array.create (List.length ls.ls_args) None in
      let check_field (ts', (loc, _, i, tye), e) = 
	if not (ts_equal ts' ts) then 
	  errorm ~loc "this should be a field for type %a" Pretty.print_ts ts;
	assert (0 <= i && i < Array.length args);
	if args.(i) <> None then
	  errorm ~loc "this record field is defined several times";
	args.(i) <- Some e;
	if not (unify tye ty) then 
	  errorm ~loc 
	    "@[this is a field for type %a,@ \
               but a field for type %a is expected@]"
	    print_dty tye print_dty ty
      in
      List.iter check_field fl;
      let add_arg e acc = match e with
	| None -> errorm ~loc "some record fields are missing"
	| Some e -> e :: acc
      in
      let fl = Array.fold_right add_arg args [] in
      Tapp (ls, fl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
599
  | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
600
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
601

602 603 604 605 606
and dfmla ?(localize=false) env { pp_loc = loc; pp_desc = f } =
  let n = dfmla_node ~localize loc env f in
  if localize then Fnamed (Ident.label ~loc "", n) else n

and dfmla_node ~localize loc env = function
607 608 609 610
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
611
  | PPunop (PPnot, a) ->
612
      Fnot (dfmla ~localize env a)
613
  | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
614
      Fbinop (binop op, dfmla ~localize env a, dfmla ~localize env b)
615
  | PPif (a, b, c) ->
616
      Fif (dfmla ~localize env a, dfmla ~localize env b, dfmla ~localize env c)
617
  | PPquant (q, uqu, trl, a) ->
618
      check_quant_linearity uqu;
619 620
      let uquant env (idl,ty) =
        let ty = dty env ty in
621
        let id = match idl with
Andrei Paskevich's avatar
Andrei Paskevich committed
622
          | Some id -> id
623
          | None -> assert false
624
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
625
        { env with dvars = Mstr.add id.id ty env.dvars }, (id,ty)
626
      in
627
      let env, uqu = map_fold_left uquant env uqu in
628
      let trigger e =
629
	try
630
	  TRterm (dterm ~localize env e)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
631
	with exn when trigger_not_a_term_exn exn ->
632
	  TRfmla (dfmla ~localize env e)
633 634
      in
      let trl = List.map (List.map trigger) trl in
635 636
      let q = match q with
        | PPforall -> Fforall
637
        | PPexists -> Fexists
638
        | _ -> error ~loc PredicateExpected
639
      in
640
      Fquant (q, uqu, trl, dfmla ~localize env a)
Andrei Paskevich's avatar
Andrei Paskevich committed
641
  | PPapp (x, tl) when check_highord env x tl ->
642 643 644
      let tl = apply_highord loc x tl in
      let atyl, _ = Denv.specialize_lsymbol ~loc ps_pred_app in
      let tl = dtype_args ps_pred_app.ls_name loc env atyl tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
645
      Fapp (ps_pred_app, tl)
646
  | PPapp (x, tl) ->
647
      let s, tyl = specialize_psymbol x env.uc in
648
      let tl = dtype_args s.ls_name loc env tyl tl in
649
      Fapp (s, tl)
650 651 652
  | PPinfix (e12, op2, e3) ->
      begin match e12.pp_desc with
	| PPinfix (_, op1, e2) when is_psymbol (Qident op1) env.uc ->
653 654
	    let e23 = { pp_desc = PPinfix (e2, op2, e3); pp_loc = loc } in
	    Fbinop (Fand, dfmla ~localize env e12, dfmla ~localize env e23)
655 656
	| _ ->
	    let s, tyl = specialize_psymbol (Qident op2) env.uc in
657
	    let tl = dtype_args s.ls_name loc env tyl [e12; e3] in
658 659
	    Fapp (s, tl)
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
660
  | PPlet (x, e1, e2) ->
661
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
662
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
663
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
664
      let e2 = dfmla ~localize env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
665
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
666
  | PPmatch (e1, bl) ->
667
      let t1 = dterm ~localize env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
668 669
      let ty1 = t1.dt_ty in
      let branch (p, e) =
670
        let env, p = dpat_list env ty1 p in p, dfmla ~localize env e
Andrei Paskevich's avatar
Andrei Paskevich committed
671
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
672
      Fmatch (t1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
673
  | PPnamed (x, f1) ->
674
      let f1 = dfmla ~localize env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
675
      Fnamed (x, f1)
676
  | PPvar (Qident s | Qdot (_,s) as x) when is_uppercase s.id.[0] ->
677 678
      let pr = find_prop x env.uc in
      Fvar (Decl.find_prop (Theory.get_known env.uc) pr)
679 680 681 682
  | PPvar x ->
      let s, tyl = specialize_psymbol x env.uc in
      let tl = dtype_args s.ls_name loc env tyl [] in
      Fapp (s, tl)
683
  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ | PPrecord _ ->
684
      error ~loc PredicateExpected
685

Andrei Paskevich's avatar
Andrei Paskevich committed
686 687 688 689 690 691 692
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
693

694 695 696 697
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
698
    | [], [] ->
699 700 701 702
	[]
    | 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
703
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
704 705 706 707 708 709
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725
(** 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
726
    t_close_branch (pat_app cs al tyarg) (t_var vs)
727 728
  in
  let vs = create_vsymbol (id_fresh "u") tyarg in
729
  let t = t_case (t_var vs) (List.map per_cs cl) in
730 731 732 733 734
  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
735
  | TDrecord _ -> assert false
736 737 738 739 740 741 742 743
  | 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
744 745 746
          | Some { id = id ; id_lab = labels ; id_loc = loc }
            when not (Mstr.mem id acc) ->
              let fn = id_user ~labels id loc in
747
              let fs = create_fsymbol fn [tc] ty in
748
              Mstr.add id (fs,tc,ty) acc
749 750 751 752 753 754 755 756
          | _ -> 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))

757
(** Typing declarations, that is building environments. *)
758 759 760

open Ptree

761
let add_types dl th =
762
  let def = List.fold_left
763
    (fun def d ->
764
      let id = d.td_ident.id in
765
      if Mstr.mem id def then error ~loc:d.td_loc (Clash id);
766 767
      Mstr.add id d def)
    Mstr.empty dl
768
  in
769
  let tysymbols = Hashtbl.create 17 in
770
  let rec visit x =
771 772 773 774 775 776
    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
777
      let d = Mstr.find x def in
778 779
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
780 781
      let vl =
	List.map
782 783 784 785
	  (fun { id = v ; id_lab = labels ; id_loc = loc } ->
	     if Hashtbl.mem vars v then error ~loc (DuplicateTypeVar v);
	     let i = create_tvsymbol (id_user ~labels v loc) in
	     Hashtbl.add vars v i;
786
	     i)
787
	  d.td_params
788
      in
789
      let id = id_user id ~labels:d.td_ident.id_lab d.td_loc in
790
      let ts = match d.td_def with
791
	| TDalias ty ->
792
	    let rec apply = function
793 794
	      | PPTtyvar v ->
		  begin
795 796 797 798 799
		    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
800
		    | Qident x when Mstr.mem x.id def ->
801 802 803 804
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
805
		  begin try
806
		    ty_app ts (List.map apply tyl)
807
		  with Ty.BadTypeArity (_, tsal, tyll) ->
808
		    error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
809 810 811 812
		  end
	      | PPTtuple tyl ->
		  let ts = ts_tuple (List.length tyl) in
		  ty_app ts (List.map apply tyl)
813 814
	    in
	    create_tysymbol id vl (Some (apply ty))
815
	| TDabstract | TDalgebraic _ ->
816
	    create_tysymbol id vl None
817 818
	| TDrecord _ ->
	    assert false
819 820 821 822
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in