typing.ml 32.7 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
(** Environments *)

117
(** typing using destructive type variables
118

119 120 121 122 123 124
    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
125

126 127
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
128 129 130 131 132
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

133 134 135 136
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

137
type denv = {
138 139 140 141 142
  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 *)
}

143 144 145
let create_denv uc = {
  uc = uc;
  utyvars = Hashtbl.create 17;
146 147 148 149 150 151 152 153 154 155 156 157
  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
158

159 160 161 162
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 }

163 164 165 166 167 168 169 170 171 172 173 174
(* 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
175
  let ts =
176 177 178
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
  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
205 206 207 208 209 210

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
211
  | PPTtyvar {id=x} ->
212 213 214
      Tyvar (find_user_type_var x env)
  | PPTtyapp (p, x) ->
      let loc = qloc x in
215
      let ts, a = specialize_tysymbol loc x env.uc in
216 217 218
      let np = List.length p in
      if np <> a then error ~loc (TypeArity (x, a, np));
      let tyl = List.map (dty env) p in
219
      begin match ts.ts_def with
220
	| None ->
221
	    Tyapp (ts, tyl)
222
	| Some ty ->
223 224 225
	    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
226 227 228 229
      end
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
      Tyapp (ts, List.map (dty env) tyl)
230 231 232 233

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
234
  try find ns sl
235 236 237 238 239 240 241 242 243 244 245 246 247
  with Not_found -> error ~loc (UnboundSymbol sl)

let find_prop_ns = find_ns ns_find_prop
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
248
  s, specialize_lsymbol ~loc:(qloc p) s
249

250
let specialize_fsymbol p uc =
251
  let s, (tl, ty) = specialize_lsymbol p uc in
252
  match ty with
253
    | None -> let loc = qloc p in error ~loc TermExpected
254
    | Some ty -> s, tl, ty
255

256
let specialize_psymbol p uc =
257
  let s, (tl, ty) = specialize_lsymbol p uc in
258 259
  match ty with
    | None -> s, tl
260 261 262 263 264
    | 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
265

266

267 268
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
269 270 271 272
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

273
(** Typing terms and formulas *)
274

Andrei Paskevich's avatar
Andrei Paskevich committed
275 276 277 278 279 280 281 282
type dpattern = { dp_node : dpattern_node; dp_ty : dty }

and dpattern_node =
  | Pwild
  | Pvar of string
  | Papp of lsymbol * dpattern list
  | Pas of dpattern * string

283 284
type uquant = string list * dty

285 286 287
type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
288
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
289
  | Tconst of constant
290
  | Tapp of lsymbol * dterm list
291
  | Tif of dfmla * dterm * dterm
292
  | Tlet of dterm * string * dterm
293
  | Tmatch of dterm list * (dpattern list * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
294
  | Tnamed of string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
295
  | Teps of string * dty * dfmla
296

297
and dfmla =
298
  | Fapp of lsymbol * dterm list
299
  | Fquant of quant * uquant list * dtrigger list list * dfmla
300 301 302 303 304
  | Fbinop of binop * dfmla * dfmla
  | Fnot of dfmla
  | Ftrue
  | Ffalse
  | Fif of dfmla * dfmla * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
305
  | Flet of dterm * string * dfmla
306
  | Fmatch of dterm list * (dpattern list * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
307
  | Fnamed of string * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
308
  | Fvar of fmla
309

310 311 312 313
and dtrigger =
  | TRterm of dterm
  | TRfmla of dfmla

314 315 316 317 318 319
let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

320
let check_pat_linearity pl =
Andrei Paskevich's avatar
Andrei Paskevich committed
321
  let s = ref Sstr.empty in
322
  let add id =
323
    if Sstr.mem id.id !s then
324
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
Andrei Paskevich's avatar
Andrei Paskevich committed
325
    s := Sstr.add id.id !s
326 327 328 329
  in
  let rec check p = match p.pat_desc with
    | PPpwild -> ()
    | PPpvar id -> add id
330
    | PPpapp (_, pl) | PPptuple pl -> List.iter check pl
331 332
    | PPpas (p, id) -> check p; add id
  in
333
  List.iter check pl
334

335 336 337 338
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
339 340 341 342 343
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
344
  | PPpwild ->
345
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
346 347
      env, Pwild, ty
  | PPpvar {id=x} ->
348
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
349
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
350 351
      env, Pvar x, ty
  | PPpapp (x, pl) ->
352
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
353 354
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      env, Papp (s, pl), ty
355 356 357 358 359 360 361
  | 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
362 363
  | PPpas (p, {id=x}) ->
      let env, p = dpat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
364
      let env = { env with dvars = Mstr.add x p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
365 366
      env, Pas (p,x), p.dp_ty

367
and dpat_args s loc env el pl =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
368
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
369
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
370
  let rec check_arg env = function
371
    | [], [] ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
372 373 374 375 376 377 378
	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
379 380 381
    | _ ->
	assert false
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
382
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
383

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
384
let rec trigger_not_a_term_exn = function
385
  | Error TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
386 387 388
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

389
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
390
  let s = ref Sstr.empty in
391
  let check id =
Andrei Paskevich's avatar
Andrei Paskevich committed
392 393
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
394 395 396
  in
  List.iter (fun (idl, _) -> List.iter check idl) uqu

397
let rec dterm env t =
398 399 400 401
  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
402
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
403
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
404
      let ty = Mstr.find x env.dvars in
405
      Tvar x, ty
406
  | PPvar x ->
407
      (* 0-arity symbol (constant) *)
408
      let s, tyl, ty = specialize_fsymbol x env.uc in
409
      let n = List.length tyl in
410
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
411
      Tapp (s, []), ty
412
  | PPapp (x, tl) ->
413
      let s, tyl, ty = specialize_fsymbol x env.uc in
414
      let tl = dtype_args s.ls_name loc env tyl tl in
415
      Tapp (s, tl), ty
416 417 418 419 420 421 422
  | 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
423 424 425 426
  | 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
427
  | PPconst (ConstInt _ as c) ->
428
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
429
  | PPconst (ConstReal _ as c) ->
430
      Tconst c, Tyapp (Ty.ts_real, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
431 432 433
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
434
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
435 436
      let e2 = dterm env e2 in
      Tlet (e1, x, e2), e2.dt_ty
437 438
  | PPmatch (el, bl) ->
      let tl = List.map (dterm env) el in
439
      let tyl = List.map (fun t -> t.dt_ty) tl in
440
      let tb = fresh_type_var loc in (* the type of all branches *)
441
      let branch (pl, e) =
442
        let env, pl = dpat_list env tyl pl in
443
        let loc = e.pp_loc in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
444 445
	let e = dterm env e in
	if not (unify e.dt_ty tb) then term_expected_type ~loc e.dt_ty tb;
446
        pl, e
Andrei Paskevich's avatar
Andrei Paskevich committed
447 448 449
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).dt_ty in
450
      Tmatch (tl, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
451 452 453
  | 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
454 455 456 457 458 459
  | 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
460 461 462 463 464 465 466
  | 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
467 468 469 470 471
  | PPeps ({id=x}, ty, e1) ->
      let ty = dty env ty in
      let env = { env with dvars = Mstr.add x ty env.dvars } in
      let e1 = dfmla env e1 in
      Teps (x, ty, e1), ty
472
  | PPquant _
473
  | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
474
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
475

476 477 478 479 480
and dfmla env e = match e.pp_desc with
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
481
  | PPunop (PPnot, a) ->
482
      Fnot (dfmla env a)
483
  | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
484 485
      Fbinop (binop op, dfmla env a, dfmla env b)
  | PPif (a, b, c) ->
486
      Fif (dfmla env a, dfmla env b, dfmla env c)
487
  | PPquant (q, uqu, trl, a) ->
488
      check_quant_linearity uqu;
489 490
      let uquant env (idl,ty) =
        let ty = dty env ty in
491
        let env, idl =
492
          map_fold_left
Andrei Paskevich's avatar
Andrei Paskevich committed
493
            (fun env {id=x} -> { env with dvars = Mstr.add x ty env.dvars }, x)
494 495 496
            env idl
        in
        env, (idl,ty)
497
      in
498
      let env, uqu = map_fold_left uquant env uqu in
499
      let trigger e =
500 501
	try
	  TRterm (dterm env e)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
502
	with exn when trigger_not_a_term_exn exn ->
503
	  TRfmla (dfmla env e)
504 505
      in
      let trl = List.map (List.map trigger) trl in
506 507
      let q = match q with
        | PPforall -> Fforall
508 509 510
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
511
  | PPapp (x, tl) ->
512
      let s, tyl = specialize_psymbol x env.uc in
513
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
514
      Fapp (s, tl)
515 516 517 518 519 520 521 522 523 524
  | 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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
525 526 527
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
528
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
529 530
      let e2 = dfmla env e2 in
      Flet (e1, x, e2)
531 532
  | PPmatch (el, bl) ->
      let tl = List.map (dterm env) el in
533
      let tyl = List.map (fun t -> t.dt_ty) tl in
534
      let branch (pl, e) =
535
        let env, pl = dpat_list env tyl pl in
536
        pl, dfmla env e
Andrei Paskevich's avatar
Andrei Paskevich committed
537
      in
538
      Fmatch (tl, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
539 540 541
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
542
  | PPvar x ->
543
      Fvar (snd (find_prop x env.uc))
544
  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ ->
545
      error ~loc:e.pp_loc PredicateExpected
546

547
and dpat_list env tyl pl =
548
  check_pat_linearity pl;
549
  let pattern (env,pl) pat ty =
550 551
    let loc = pat.pat_loc in
    let env, pat = dpat env pat in
552 553
    if not (unify pat.dp_ty ty)
      then term_expected_type ~loc pat.dp_ty ty;
554 555 556
    env, pat::pl
  in
  let loc = (List.hd pl).pat_loc in
557
  let env, pl = try List.fold_left2 pattern (env,[]) pl tyl
558 559
    with Invalid_argument _ -> errorm ~loc
      "This pattern has length %d but is expected to have length %d"
560
      (List.length pl) (List.length tyl)
561 562 563
  in
  env, List.rev pl

564 565 566 567
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
568
    | [], [] ->
569 570 571 572
	[]
    | 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
573
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
574 575 576 577 578 579
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

580
let rec pattern env p =
Andrei Paskevich's avatar
Andrei Paskevich committed
581 582 583
  let ty = ty_of_dty p.dp_ty in
  match p.dp_node with
  | Pwild -> env, pat_wild ty
584
  | Pvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
585
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
586
      Mstr.add x v env, pat_var v
587
  | Papp (s, pl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
588 589 590 591
      let env, pl = map_fold_left pattern env pl in
      env, pat_app s pl ty
  | Pas (p, x) ->
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
592
      let env, p = pattern (Mstr.add x v env) p in
Andrei Paskevich's avatar
Andrei Paskevich committed
593 594
      env, pat_as p v

595 596
let rec term env t = match t.dt_node with
  | Tvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
597 598
      assert (Mstr.mem x env);
      t_var (Mstr.find x env)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
599
  | Tconst c ->
600
      t_const c (ty_of_dty t.dt_ty)
601
  | Tapp (s, tl) ->
602
      t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
603 604
  | Tif (f, t1, t2) ->
      t_if (fmla env f) (term env t1) (term env t2)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
605 606
  | Tlet (e1, x, e2) ->
      let ty = ty_of_dty e1.dt_ty in
607
      let e1 = term env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
608
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
609
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
610 611
      let e2 = term env e2 in
      t_let v e1 e2
612 613 614 615
  | Tmatch (tl, bl) ->
      let branch (pl,e) =
        let env, pl = map_fold_left pattern env pl in
        (pl, term env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
616 617 618
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).t_ty in
619
      t_case (List.map (term env) tl) bl ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
620 621 622
  | Tnamed (x, e1) ->
      let e1 = term env e1 in
      t_label_add x e1
Andrei Paskevich's avatar
Andrei Paskevich committed
623 624 625 626 627 628
  | Teps (x, ty, e1) ->
      let ty = ty_of_dty ty in
      let v = create_vsymbol (id_fresh x) ty in
      let env = Mstr.add x v env in
      let e1 = fmla env e1 in
      t_eps v e1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
629

630 631 632 633
and fmla env = function
  | Ftrue ->
      f_true
  | Ffalse ->
634
      f_false
635 636 637 638 639 640
  | Fnot f ->
      f_not (fmla env f)
  | Fbinop (op, f1, f2) ->
      f_binary op (fmla env f1) (fmla env f2)
  | Fif (f1, f2, f3) ->
      f_if (fmla env f1) (fmla env f2) (fmla env f3)
641
  | Fquant (q, uqu, trl, f1) ->
642
      (* TODO: shouldn't we localize this ident? *)
643 644 645
      let uquant env (xl,ty) =
        let ty = ty_of_dty ty in
        map_fold_left
646 647 648
          (fun env x ->
             let v = create_vsymbol (id_fresh x) ty in Mstr.add x v env, v)
          env xl
649
      in
650
      let env, vl = map_fold_left uquant env uqu in
651
      let trigger = function
652 653
	| TRterm t -> Term (term env t)
	| TRfmla f -> Fmla (fmla env f)
654 655 656
      in
      let trl = List.map (List.map trigger) trl in
      f_quant q (List.concat vl) trl (fmla env f1)
657 658
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
659
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
660
      let ty = ty_of_dty e1.dt_ty in
661
      let e1 = term env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
662
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
663
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
664 665
      let f2 = fmla env f2 in
      f_let v e1 f2
666 667 668 669
  | Fmatch (tl, bl) ->
      let branch (pl,e) =
        let env, pl = map_fold_left pattern env pl in
        (pl, fmla env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
670
      in
671
      f_case (List.map (term env) tl) (List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
672
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
673
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
674
      f_label_add x f1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
675 676
  | Fvar f ->
      f
677

678
(** Typing declarations, that is building environments. *)
679 680 681

open Ptree

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

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
780
let env_of_vsymbol_list vl =
781
  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
782

783
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
784 785
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
786
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
787
  (* 1. crea