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

let add_logic_decl  = with_tuples add_logic_decl
187
let add_logic_decls = with_tuples ~reset:true add_logic_decl
188 189

let add_ind_decl  = with_tuples add_ind_decl
190
let add_ind_decls = with_tuples ~reset:true add_ind_decl
191

192 193
let add_prop_decl = with_tuples ~reset:true add_prop_decl

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

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
222
  try find ns sl
223 224
  with Not_found -> error ~loc (UnboundSymbol sl)

225
let find_prop_ns = find_ns ns_find_pr
226 227 228 229 230 231 232 233 234 235
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
236 237
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
238

239
let specialize_fsymbol p uc =
240
  let s,tl,ty = specialize_lsymbol p uc in
241
  match ty with
242
    | None -> let loc = qloc p in error ~loc TermExpected
243
    | Some ty -> s, tl, ty
244

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

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

255

256 257
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
258 259 260 261
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

262
(** Typing terms and formulas *)
263 264 265 266 267 268 269

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

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
341
let rec trigger_not_a_term_exn = function
342
  | TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
343 344 345
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

346
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
347
  let s = ref Sstr.empty in
348
  let check id =
Andrei Paskevich's avatar
Andrei Paskevich committed
349 350
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
351
  in
352
  List.iter (fun (idl, _) -> Util.option_iter check idl) uqu
353

Andrei Paskevich's avatar
Andrei Paskevich committed
354 355 356 357 358 359 360 361 362
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

363 364 365 366 367 368 369 370 371 372
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
373
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
374
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
375
      let ty = Mstr.find x env.dvars in
376
      Tvar x, ty
377
  | PPvar x ->
378
      (* 0-arity symbol (constant) *)
379
      let s, tyl, ty = specialize_fsymbol x env.uc in
380
      let n = List.length tyl in
381
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
382
      Tapp (s, []), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
383 384 385 386 387
  | 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
388
  | PPapp (x, tl) ->
389
      let s, tyl, ty = specialize_fsymbol x env.uc in
390
      let tl = dtype_args s.ls_name loc env tyl tl in
391
      Tapp (s, tl), ty
392 393 394 395 396 397 398
  | 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
399 400 401 402
  | 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
403
  | PPconst (ConstInt _ as c) ->
404
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
405
  | PPconst (ConstReal _ as c) ->
406
      Tconst c, Tyapp (Ty.ts_real, [])
Andrei Paskevich's avatar
Andrei Paskevich committed
407
  | PPlet (x, e1, e2) ->
408
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
409
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
410
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
411
      let e2 = dterm ~localize env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
413
  | PPmatch (e1, bl) ->
414
      let t1 = dterm ~localize env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
415
      let ty1 = t1.dt_ty in
416
      let tb = fresh_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
417 418
      let branch (p, e) =
        let env, p = dpat_list env ty1 p in
419
        let loc = e.pp_loc in
420
	let e = dterm ~localize env e in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
421
	if not (unify e.dt_ty tb) then term_expected_type ~loc e.dt_ty tb;
Andrei Paskevich's avatar
Andrei Paskevich committed
422
        p, e
Andrei Paskevich's avatar
Andrei Paskevich committed
423 424 425
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
426
      Tmatch (t1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
427
  | PPnamed (x, e1) ->
428
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429
      Tnamed (x, e1), e1.dt_ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
430 431
  | PPcast (e1, ty) ->
      let loc = e1.pp_loc in
432
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
433 434 435
      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
436 437
  | PPif (e1, e2, e3) ->
      let loc = e3.pp_loc in
438 439
      let e2 = dterm ~localize env e2 in
      let e3 = dterm ~localize env e3 in
440 441
      if not (unify e2.dt_ty e3.dt_ty) then
        term_expected_type ~loc e3.dt_ty e2.dt_ty;
442
      Tif (dfmla ~localize env e1, e2, e3), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
443
  | PPeps (x, ty, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
444
      let ty = dty env ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
445
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
446
      let e1 = dfmla ~localize env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
447
      Teps (x, ty, e1), ty
448
  | PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
449 450 451 452 453 454 455 456 457 458 459 460
      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
461
	  TRterm (dterm ~localize env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
462
	with exn when trigger_not_a_term_exn exn ->
463
	  TRfmla (dfmla ~localize env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
464 465
      in
      let trl = List.map (List.map trigger) trl in
466
      let e = match q with
467 468
        | PPfunc -> TRterm (dterm ~localize env a)
        | PPpred -> TRfmla (dfmla ~localize env a)
469 470 471 472
        | PPlambda -> trigger a
        | _ -> assert false
      in
      let id, ty, f = match e with
Andrei Paskevich's avatar
Andrei Paskevich committed
473
        | TRterm t ->
474
            let id = { id = "fc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
475 476 477 478 479 480 481 482 483 484 485
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
              let nty = Tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
              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
486
        | TRfmla f ->
487
            let id = { id = "pc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505
            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) ->
              let nty = Tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
              uqu ([],Tyapp (ts_pred, [uty]))
            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
Andrei Paskevich's avatar
Andrei Paskevich committed
506
  | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
507
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
508

509 510 511 512 513
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
514 515 516 517
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
518
  | PPunop (PPnot, a) ->
519
      Fnot (dfmla ~localize env a)
520
  | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
521
      Fbinop (binop op, dfmla ~localize env a, dfmla ~localize env b)
522
  | PPif (a, b, c) ->
523
      Fif (dfmla ~localize env a, dfmla ~localize env b, dfmla ~localize env c)
524
  | PPquant (q, uqu, trl, a) ->
525
      check_quant_linearity uqu;
526 527
      let uquant env (idl,ty) =
        let ty = dty env ty in
528
        let id = match idl with
Andrei Paskevich's avatar
Andrei Paskevich committed
529
          | Some id -> id
530
          | None -> assert false
531
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
532
        { env with dvars = Mstr.add id.id ty env.dvars }, (id,ty)
533
      in
534
      let env, uqu = map_fold_left uquant env uqu in
535
      let trigger e =
536
	try
537
	  TRterm (dterm ~localize env e)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
538
	with exn when trigger_not_a_term_exn exn ->
539
	  TRfmla (dfmla ~localize env e)
540 541
      in
      let trl = List.map (List.map trigger) trl in
542 543
      let q = match q with
        | PPforall -> Fforall
544
        | PPexists -> Fexists
545
        | _ -> error ~loc PredicateExpected
546
      in
547
      Fquant (q, uqu, trl, dfmla ~localize env a)
Andrei Paskevich's avatar
Andrei Paskevich committed
548
  | PPapp (x, tl) when check_highord env x tl ->
549 550 551
      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
552
      Fapp (ps_pred_app, tl)
553
  | PPapp (x, tl) ->
554
      let s, tyl = specialize_psymbol x env.uc in
555
      let tl = dtype_args s.ls_name loc env tyl tl in
556
      Fapp (s, tl)
557 558 559
  | PPinfix (e12, op2, e3) ->
      begin match e12.pp_desc with
	| PPinfix (_, op1, e2) when is_psymbol (Qident op1) env.uc ->
560 561
	    let e23 = { pp_desc = PPinfix (e2, op2, e3); pp_loc = loc } in
	    Fbinop (Fand, dfmla ~localize env e12, dfmla ~localize env e23)
562 563
	| _ ->
	    let s, tyl = specialize_psymbol (Qident op2) env.uc in
564
	    let tl = dtype_args s.ls_name loc env tyl [e12; e3] in
565 566
	    Fapp (s, tl)
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
567
  | PPlet (x, e1, e2) ->
568
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
569
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
570
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
571
      let e2 = dfmla ~localize env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
572
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
573
  | PPmatch (e1, bl) ->
574
      let t1 = dterm ~localize env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
575 576
      let ty1 = t1.dt_ty in
      let branch (p, e) =
577
        let env, p = dpat_list env ty1 p in p, dfmla ~localize env e
Andrei Paskevich's avatar
Andrei Paskevich committed
578
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
579
      Fmatch (t1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
580
  | PPnamed (x, f1) ->
581
      let f1 = dfmla ~localize env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
582
      Fnamed (x, f1)
583
  | PPvar x ->
584 585
      let pr = find_prop x env.uc in
      Fvar (Decl.find_prop (Theory.get_known env.uc) pr)
586
  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ ->
587
      error ~loc PredicateExpected
588

Andrei Paskevich's avatar
Andrei Paskevich committed
589 590 591 592 593 594 595
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
596

597 598 599 600
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
601
    | [], [] ->
602 603 604 605
	[]
    | 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
606
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
607 608 609 610 611 612
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628
(** 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
629
    t_close_branch (pat_app cs al tyarg) (t_var vs)
630 631
  in
  let vs = create_vsymbol (id_fresh "u") tyarg in
632
  let t = t_case (t_var vs) (List.map per_cs cl) in
633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657
  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))

658
(** Typing declarations, that is building environments. *)
659 660 661

open Ptree

662
let add_types dl th =
663
  let def = List.fold_left
664
    (fun def d ->
665
      let id = d.td_ident.id in
666
      if Mstr.mem id def then error ~loc:d.td_loc (Clash id);
667 668
      Mstr.add id d def)
    Mstr.empty dl
669
  in
670
  let tysymbols = Hashtbl.create 17 in
671
  let rec visit x =
672 673 674 675 676 677
    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
678
      let d = Mstr.find x def in
679 680
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
681 682 683 684
      let vl =
	List.map
	  (fun v ->
	     if Hashtbl.mem vars v.id then
685
	       error ~loc:v.id_loc (DuplicateTypeVar v.id);
686
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
687 688
	     Hashtbl.add vars v.id i;
	     i)
689
	  d.td_params
690
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
691
      let id = id_user id d.td_loc in
692
      let ts = match d.td_def with
693
	| TDalias ty ->
694
	    let rec apply = function
695 696
	      | PPTtyvar v ->
		  begin
697 698 699 700 701
		    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
702
		    | Qident x when Mstr.mem x.id def ->
703 704 705 706
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
707
		  begin try
708
		    ty_app ts (List.map apply tyl)
709
		  with Ty.BadTypeArity (_, tsal, tyll) ->
710
		    error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
711 712 713 714
		  end
	      | PPTtuple tyl ->
		  let ts = ts_tuple (List.length tyl) in
		  ty_app ts (List.map apply tyl)
715 716
	    in
	    create_tysymbol id vl (Some (apply ty))
717
	| TDabstract | TDalgebraic _ ->
718 719 720 721 722
	    create_tysymbol id vl None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
723
  let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in
724
  let th' = try add_ty_decl th tsl
725
    with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (Clash s)
726
  in
727
  let csymbols = Hashtbl.create 17 in
728
  let decl d =
729
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
730
      | None ->
731
	  assert false
732
      | Some ts ->
733 734
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
735 736
	  List.iter
	    (fun v ->
737
	       Hashtbl.add vars v.tv_name.id_string
738
                  (create_ty_decl_var ~user:true v))
739 740 741 742
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
743
      | TDabstract | TDalias _ ->
744
	  Tabstract
745
      | TDalgebraic cl ->
746
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
747
	  let constructor (loc, id, pl) =
748
	    let param (_,t) = ty_of_dty (dty th' t) in
749
	    let tyl = List.map param pl in
750
	    Hashtbl.replace csymbols id.id loc;
751
	    create_fsymbol (id_user id.id loc) tyl ty
752 753 754 755
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
756
  in
757 758 759 760
  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
761

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
762
let env_of_vsymbol_list vl =
763
  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
764

765
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
766 767
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
768
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
769
  (* 1. create all symbols and make an environment with these symbols *)
770
  let create_symbol th d =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
771
    let id = d.ld_ident.id in
Andrei Paskevich's avatar
Andrei Paskevich committed
772
    let v = id_user id d.ld_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
773
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
774
    Hashtbl.add denvs id denv;
775
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
776
    let pl = List.map type_ty d.ld_params in
777
    try match d.ld_type with
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
778 779 780
      | None -> (* predicate *)