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

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

32 33
(** errors *)

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

exception Error of error

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

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

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

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

115 116
(** 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 179 180 181 182 183 184 185
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
  ts, specialize_tysymbol ~loc ts

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
186
  | PPTtyvar {id=x} ->
187 188 189 190 191 192 193 194 195
      Tyvar (find_user_type_var x env)
  | PPTtyapp (p, x) ->
      let loc = qloc x in
      let ts, tv = specialize_tysymbol loc x env.uc in
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
      let tyl = List.map (dty env) p in
      match ts.ts_def with
196
	| None ->
197
	    Tyapp (ts, tyl)
198
	| Some ty ->
199 200 201 202 203 204 205
	    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

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
206
  try find ns sl
207 208 209 210 211 212 213 214 215 216 217 218 219
  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
220
  s, specialize_lsymbol ~loc:(qloc p) s
221

222
let specialize_fsymbol p uc =
223
  let s, (tl, ty) = specialize_lsymbol p uc in
224
  match ty with
225
    | None -> let loc = qloc p in error ~loc TermExpected
226
    | Some ty -> s, tl, ty
227

228
let specialize_psymbol p uc =
229
  let s, (tl, ty) = specialize_lsymbol p uc in
230 231
  match ty with
    | None -> s, tl
232 233 234 235 236
    | 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
237

238

239 240
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
241 242 243 244
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

245
(** Typing terms and formulas *)
246

Andrei Paskevich's avatar
Andrei Paskevich committed
247 248 249 250 251 252 253 254
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

255 256
type uquant = string list * dty

257 258 259
type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
260
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
261
  | Tconst of constant
262
  | Tapp of lsymbol * dterm list
263
  | Tif of dfmla * dterm * dterm
264
  | Tlet of dterm * string * dterm
265
  | Tmatch of dterm list * (dpattern list * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
266
  | Tnamed of string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
267
  | Teps of string * dty * dfmla
268

269
and dfmla =
270
  | Fapp of lsymbol * dterm list
271
  | Fquant of quant * uquant list * dtrigger list list * dfmla
272 273 274 275 276
  | 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
277
  | Flet of dterm * string * dfmla
278
  | Fmatch of dterm list * (dpattern list * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
279
  | Fnamed of string * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
280
  | Fvar of fmla
281

282 283 284 285
and dtrigger =
  | TRterm of dterm
  | TRfmla of dfmla

286 287 288 289 290 291
let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

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

Andrei Paskevich's avatar
Andrei Paskevich committed
307 308 309 310 311
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
312
  | PPpwild ->
Andrei Paskevich's avatar
Andrei Paskevich committed
313
      let tv = create_tvsymbol (id_user "a" loc) in
314
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
315 316 317
      env, Pwild, ty
  | PPpvar {id=x} ->
      let tv = create_tvsymbol (id_user "a" loc) in
318
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
319
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
320 321
      env, Pvar x, ty
  | PPpapp (x, pl) ->
322
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
323 324 325 326
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      env, Papp (s, pl), ty
  | PPpas (p, {id=x}) ->
      let env, p = dpat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
327
      let env = { env with dvars = Mstr.add x p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
328 329
      env, Pas (p,x), p.dp_ty

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
  | Error 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 358 359
  in
  List.iter (fun (idl, _) -> List.iter check idl) uqu

360
let rec dterm env t =
361 362 363 364
  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
365
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
366
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
367
      let ty = Mstr.find x env.dvars in
368
      Tvar x, ty
369
  | PPvar x ->
370
      (* 0-arity symbol (constant) *)
371
      let s, tyl, ty = specialize_fsymbol x env.uc in
372
      let n = List.length tyl in
373
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
374
      Tapp (s, []), ty
375
  | PPapp (x, tl) ->
376
      let s, tyl, ty = specialize_fsymbol x env.uc in
377
      let tl = dtype_args s.ls_name loc env tyl tl in
378
      Tapp (s, tl), ty
379 380 381 382
  | 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
383
  | PPconst (ConstInt _ as c) ->
384
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
385
  | PPconst (ConstReal _ as c) ->
386
      Tconst c, Tyapp (Ty.ts_real, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
387 388 389
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
390
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
391 392
      let e2 = dterm env e2 in
      Tlet (e1, x, e2), e2.dt_ty
393 394
  | PPmatch (el, bl) ->
      let tl = List.map (dterm env) el in
395
      let tyl = List.map (fun t -> t.dt_ty) tl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
396 397
      let tb = (* the type of all branches *)
	let tv = create_tvsymbol (id_user "a" loc) in
398
	Tyvar (create_ty_decl_var ~loc ~user:false tv)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
399
      in
400
      let branch (pl, e) =
401
        let env, pl = dpat_list env tyl pl in
402
        let loc = e.pp_loc in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
403 404
	let e = dterm env e in
	if not (unify e.dt_ty tb) then term_expected_type ~loc e.dt_ty tb;
405
        pl, e
Andrei Paskevich's avatar
Andrei Paskevich committed
406 407 408
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).dt_ty in
409
      Tmatch (tl, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
410 411 412
  | 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
413 414 415 416 417 418
  | 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
419 420 421 422 423 424 425
  | 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
426 427 428 429 430
  | 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
431
  | PPquant _
432
  | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
433
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
434

435 436 437 438 439
and dfmla env e = match e.pp_desc with
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
440
  | PPunop (PPnot, a) ->
441
      Fnot (dfmla env a)
442
  | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
443 444
      Fbinop (binop op, dfmla env a, dfmla env b)
  | PPif (a, b, c) ->
445
      Fif (dfmla env a, dfmla env b, dfmla env c)
446
  | PPquant (q, uqu, trl, a) ->
447
      check_quant_linearity uqu;
448 449
      let uquant env (idl,ty) =
        let ty = dty env ty in
450
        let env, idl =
451
          map_fold_left
Andrei Paskevich's avatar
Andrei Paskevich committed
452
            (fun env {id=x} -> { env with dvars = Mstr.add x ty env.dvars }, x)
453 454 455
            env idl
        in
        env, (idl,ty)
456
      in
457
      let env, uqu = map_fold_left uquant env uqu in
458
      let trigger e =
459 460
	try
	  TRterm (dterm env e)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
461
	with exn when trigger_not_a_term_exn exn ->
462
	  TRfmla (dfmla env e)
463 464
      in
      let trl = List.map (List.map trigger) trl in
465 466
      let q = match q with
        | PPforall -> Fforall
467 468 469
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
470
  | PPapp (x, tl) ->
471
      let s, tyl = specialize_psymbol x env.uc in
472
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
473
      Fapp (s, tl)
474 475 476 477 478 479 480 481 482 483
  | 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
484 485 486
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
487
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
488 489
      let e2 = dfmla env e2 in
      Flet (e1, x, e2)
490 491
  | PPmatch (el, bl) ->
      let tl = List.map (dterm env) el in
492
      let tyl = List.map (fun t -> t.dt_ty) tl in
493
      let branch (pl, e) =
494
        let env, pl = dpat_list env tyl pl in
495
        pl, dfmla env e
Andrei Paskevich's avatar
Andrei Paskevich committed
496
      in
497
      Fmatch (tl, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
498 499 500
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
501
  | PPvar x ->
502
      Fvar (snd (find_prop x env.uc))
Andrei Paskevich's avatar
Andrei Paskevich committed
503
  | PPeps _ | PPconst _ | PPcast _ ->
504
      error ~loc:e.pp_loc PredicateExpected
505

506
and dpat_list env tyl pl =
507
  check_pat_linearity pl;
508
  let pattern (env,pl) pat ty =
509 510
    let loc = pat.pat_loc in
    let env, pat = dpat env pat in
511 512
    if not (unify pat.dp_ty ty)
      then term_expected_type ~loc pat.dp_ty ty;
513 514 515
    env, pat::pl
  in
  let loc = (List.hd pl).pat_loc in
516
  let env, pl = try List.fold_left2 pattern (env,[]) pl tyl
517 518
    with Invalid_argument _ -> errorm ~loc
      "This pattern has length %d but is expected to have length %d"
519
      (List.length pl) (List.length tyl)
520 521 522
  in
  env, List.rev pl

523 524 525 526
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
527
    | [], [] ->
528 529 530 531
	[]
    | 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
532
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
533 534 535 536 537 538
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

539
let rec pattern env p =
Andrei Paskevich's avatar
Andrei Paskevich committed
540 541 542
  let ty = ty_of_dty p.dp_ty in
  match p.dp_node with
  | Pwild -> env, pat_wild ty
543
  | Pvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
544
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
545
      Mstr.add x v env, pat_var v
546
  | Papp (s, pl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
547 548 549 550
      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
551
      let env, p = pattern (Mstr.add x v env) p in
Andrei Paskevich's avatar
Andrei Paskevich committed
552 553
      env, pat_as p v

554 555
let rec term env t = match t.dt_node with
  | Tvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
556 557
      assert (Mstr.mem x env);
      t_var (Mstr.find x env)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
558
  | Tconst c ->
559
      t_const c (ty_of_dty t.dt_ty)
560
  | Tapp (s, tl) ->
561
      t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
562 563
  | 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
564 565
  | Tlet (e1, x, e2) ->
      let ty = ty_of_dty e1.dt_ty in
566
      let e1 = term env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
567
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
568
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
569 570
      let e2 = term env e2 in
      t_let v e1 e2
571 572 573 574
  | 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
575 576 577
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).t_ty in
578
      t_case (List.map (term env) tl) bl ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
579 580 581
  | Tnamed (x, e1) ->
      let e1 = term env e1 in
      t_label_add x e1
Andrei Paskevich's avatar
Andrei Paskevich committed
582 583 584 585 586 587
  | 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
588

589 590 591 592
and fmla env = function
  | Ftrue ->
      f_true
  | Ffalse ->
593
      f_false
594 595 596 597 598 599
  | 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)
600
  | Fquant (q, uqu, trl, f1) ->
601
      (* TODO: shouldn't we localize this ident? *)
602 603 604
      let uquant env (xl,ty) =
        let ty = ty_of_dty ty in
        map_fold_left
605 606 607
          (fun env x ->
             let v = create_vsymbol (id_fresh x) ty in Mstr.add x v env, v)
          env xl
608
      in
609
      let env, vl = map_fold_left uquant env uqu in
610
      let trigger = function
611 612
	| TRterm t -> Term (term env t)
	| TRfmla f -> Fmla (fmla env f)
613 614 615
      in
      let trl = List.map (List.map trigger) trl in
      f_quant q (List.concat vl) trl (fmla env f1)
616 617
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
618
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
619
      let ty = ty_of_dty e1.dt_ty in
620
      let e1 = term env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
621
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
622
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
623 624
      let f2 = fmla env f2 in
      f_let v e1 f2
625 626 627 628
  | 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
629
      in
630
      f_case (List.map (term env) tl) (List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
631
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
632
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
633
      f_label_add x f1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
634 635
  | Fvar f ->
      f
636

637
(** Typing declarations, that is building environments. *)
638 639 640

open Ptree

641
let add_types dl th =
642 643 644 645 646 647
  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 
648
  in
649
  let tysymbols = Hashtbl.create 17 in
650
  let rec visit x =
651 652 653 654 655 656
    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
657
      let d = Mstr.find x def in
658 659
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
660 661 662 663
      let vl =
	List.map
	  (fun v ->
	     if Hashtbl.mem vars v.id then
664
	       error ~loc:v.id_loc (DuplicateTypeVar v.id);
665
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
666 667
	     Hashtbl.add vars v.id i;
	     i)
668
	  d.td_params
669
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
670
      let id = id_user id d.td_loc in
671
      let ts = match d.td_def with
672
	| TDalias ty ->
673
	    let rec apply = function
674 675
	      | PPTtyvar v ->
		  begin
676 677 678 679 680
		    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
681
		    | Qident x when Mstr.mem x.id def ->
682 683 684 685 686 687
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
		  try
		    ty_app ts (List.map apply tyl)
688 689
		  with Ty.BadTypeArity (tsal, tyll) ->
		    error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
690 691
	    in
	    create_tysymbol id vl (Some (apply ty))
692
	| TDabstract | TDalgebraic _ ->
693 694 695 696 697
	    create_tysymbol id vl None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
698
  let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in 
699
  let th' = try add_ty_decl th tsl
700
    with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (Clash s)
701
  in
702
  let csymbols = Hashtbl.create 17 in
703
  let decl d =
704
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
705
      | None ->
706
	  assert false
707
      | Some ts ->
708 709
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
710 711
	  List.iter
	    (fun v ->
712
	       Hashtbl.add vars v.tv_name.id_string
713
                  (create_ty_decl_var ~user:true v))
714 715 716 717
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
718
      | TDabstract | TDalias _ ->
719
	  Tabstract
720
      | TDalgebraic cl ->
721
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
722
	  let constructor (loc, id, pl) =
723
	    let param t = ty_of_dty (dty th' t) in
724
	    let tyl = List.map param pl in
725
	    Hashtbl.replace csymbols id.id loc;
726
	    create_fsymbol (id_user id.id loc) tyl ty
727 728 729 730
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
731
  in
732
  try add_ty_decls th (List.map decl dl)
733
  with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
734

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
735
let env_of_vsymbol_list vl =
736
  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
737

738
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
739 740
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
741
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
742
  (* 1. create all symbols and make an environment with these symbols *)
743
  let create_symbol th d =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
744
    let id = d.ld_ident.id in
Andrei Paskevich's avatar
Andrei Paskevich committed
745
    let v = id_user id d.ld_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
746
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
747
    Hashtbl.add denvs id denv;
748
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
749
    let pl = List.map type_ty d.ld_params in
750
    try match d.ld_type with
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
751 752 753
      | None -> (* predicate *)
	  let ps = create_psymbol v pl in
	  Hashtbl.add psymbols id ps;
754
	  add_logic_decl th [ps, None]
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
755 756
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
757
	  let fs = create_fsymbol v pl t in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
758
	  Hashtbl.add fsymbols id fs;
759
	  add_logic_decl th [fs, None]
760
    with ClashSymbol s -> error ~loc:d.ld_loc (Clash s)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
761 762 763
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
764
  let type_decl d =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
765 766 767
    let id = d.ld_ident.id in
    let dadd_var denv (x, ty) = match x with
      | None -> denv