typing.ml 29.8 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) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short 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 163 164 165 166 167 168 169 170
(* 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
171
  let ts =
172 173 174 175 176 177 178 179 180 181
    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
182
  | PPTtyvar {id=x} ->
183 184 185 186 187 188 189 190 191
      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
192
	| None ->
193
	    Tyapp (ts, tyl)
194
	| Some ty ->
195 196 197 198 199 200 201
	    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
202
  try find ns sl
203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
  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
  s, specialize_lsymbol (qloc p) s

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

225
let specialize_psymbol p uc =
226 227
  let loc = qloc p in
  let s, (tl, ty) = specialize_lsymbol p uc in
228 229 230
  match ty with
    | None -> s, tl
    | Some _ -> error ~loc PredicateExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
231

232

233 234
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
235 236 237 238
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

239
(** Typing terms and formulas *)
240

Andrei Paskevich's avatar
Andrei Paskevich committed
241 242 243 244 245 246 247 248
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

249 250
type uquant = string list * dty

251 252 253
type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
254
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
255
  | Tconst of constant
256
  | Tapp of lsymbol * dterm list
257
  | Tlet of dterm * string * dterm
258
  | Tmatch of dterm list * (dpattern list * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
259
  | Tnamed of string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
260
  | Teps of string * dty * dfmla
261

262
and dfmla =
263
  | Fapp of lsymbol * dterm list
264
  | Fquant of quant * uquant list * dtrigger list list * dfmla
265 266 267 268 269
  | 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
270
  | Flet of dterm * string * dfmla
271
  | Fmatch of dterm list * (dpattern list * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
272
  | Fnamed of string * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
273
  | Fvar of fmla
274

275 276 277 278
and dtrigger =
  | TRterm of dterm
  | TRfmla of dfmla

279 280 281 282 283 284
let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

285
let check_pat_linearity pl =
Andrei Paskevich's avatar
Andrei Paskevich committed
286
  let s = ref Sstr.empty in
287
  let add id =
288
    if Sstr.mem id.id !s then
289
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
Andrei Paskevich's avatar
Andrei Paskevich committed
290
    s := Sstr.add id.id !s
291 292 293 294 295 296 297
  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
298
  List.iter check pl
299

Andrei Paskevich's avatar
Andrei Paskevich committed
300 301 302 303 304
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
305
  | PPpwild ->
Andrei Paskevich's avatar
Andrei Paskevich committed
306
      let tv = create_tvsymbol (id_user "a" loc) in
307
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
308 309 310
      env, Pwild, ty
  | PPpvar {id=x} ->
      let tv = create_tvsymbol (id_user "a" loc) in
311
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
312
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
313 314
      env, Pvar x, ty
  | PPpapp (x, pl) ->
315
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
316 317 318 319
      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
320
      let env = { env with dvars = Mstr.add x p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
321 322
      env, Pas (p,x), p.dp_ty

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

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

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

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

416 417 418 419 420 421 422 423 424 425
and dfmla env e = match e.pp_desc with
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
  | PPprefix (PPnot, a) ->
      Fnot (dfmla env a)
  | PPinfix (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
      Fbinop (binop op, dfmla env a, dfmla env b)
  | PPif (a, b, c) ->
426
      Fif (dfmla env a, dfmla env b, dfmla env c)
427
  | PPquant (q, uqu, trl, a) ->
428
      check_quant_linearity uqu;
429 430
      let uquant env (idl,ty) =
        let ty = dty env ty in
431
        let env, idl =
432
          map_fold_left
Andrei Paskevich's avatar
Andrei Paskevich committed
433
            (fun env {id=x} -> { env with dvars = Mstr.add x ty env.dvars }, x)
434 435 436
            env idl
        in
        env, (idl,ty)
437
      in
438
      let env, uqu = map_fold_left uquant env uqu in
439
      let trigger e =
440 441
	try
	  TRterm (dterm env e)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
442
	with exn when trigger_not_a_term_exn exn ->
443
	  TRfmla (dfmla env e)
444 445
      in
      let trl = List.map (List.map trigger) trl in
446 447
      let q = match q with
        | PPforall -> Fforall
448 449 450
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
451
  | PPapp (x, tl) ->
452
      let s, tyl = specialize_psymbol x env.uc in
453
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
454
      Fapp (s, tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
455 456 457
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
458
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
459 460
      let e2 = dfmla env e2 in
      Flet (e1, x, e2)
461 462 463 464 465
  | PPmatch (el, bl) ->
      let tl = List.map (dterm env) el in
      let branch (pl, e) =
        let env, pl = dpat_list env tl pl in
        pl, dfmla env e
Andrei Paskevich's avatar
Andrei Paskevich committed
466
      in
467
      Fmatch (tl, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
468 469 470
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
471
  | PPvar x ->
472
      Fvar (snd (find_prop x env.uc))
Andrei Paskevich's avatar
Andrei Paskevich committed
473
  | PPeps _ | PPconst _ | PPcast _ ->
474
      error ~loc:e.pp_loc PredicateExpected
475

476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492
and dpat_list env tl pl =
  check_pat_linearity pl;
  let pattern (env,pl) pat t =
    let loc = pat.pat_loc in
    let env, pat = dpat env pat in
    if not (unify pat.dp_ty t.dt_ty)
      then term_expected_type ~loc pat.dp_ty t.dt_ty;
    env, pat::pl
  in
  let loc = (List.hd pl).pat_loc in
  let env, pl = try List.fold_left2 pattern (env,[]) pl tl
    with Invalid_argument _ -> errorm ~loc
      "This pattern has length %d but is expected to have length %d"
      (List.length pl) (List.length tl)
  in
  env, List.rev pl

493 494 495 496
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
497
    | [], [] ->
498 499 500 501
	[]
    | 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
502
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
503 504 505 506 507 508
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

509
let rec pattern env p =
Andrei Paskevich's avatar
Andrei Paskevich committed
510 511 512
  let ty = ty_of_dty p.dp_ty in
  match p.dp_node with
  | Pwild -> env, pat_wild ty
513
  | Pvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
514
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
515
      Mstr.add x v env, pat_var v
516
  | Papp (s, pl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
517 518 519 520
      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
521
      let env, p = pattern (Mstr.add x v env) p in
Andrei Paskevich's avatar
Andrei Paskevich committed
522 523
      env, pat_as p v

524 525
let rec term env t = match t.dt_node with
  | Tvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
526 527
      assert (Mstr.mem x env);
      t_var (Mstr.find x env)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
528
  | Tconst c ->
529
      t_const c (ty_of_dty t.dt_ty)
530
  | Tapp (s, tl) ->
531
      t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
532 533
  | Tlet (e1, x, e2) ->
      let ty = ty_of_dty e1.dt_ty in
534
      let e1 = term env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
535
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
536
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
537 538
      let e2 = term env e2 in
      t_let v e1 e2
539 540 541 542
  | 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
543 544 545
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).t_ty in
546
      t_case (List.map (term env) tl) bl ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
547 548 549
  | Tnamed (x, e1) ->
      let e1 = term env e1 in
      t_label_add x e1
Andrei Paskevich's avatar
Andrei Paskevich committed
550 551 552 553 554 555
  | 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
556

557 558 559 560
and fmla env = function
  | Ftrue ->
      f_true
  | Ffalse ->
561
      f_false
562 563 564 565 566 567
  | 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)
568
  | Fquant (q, uqu, trl, f1) ->
569
      (* TODO: shouldn't we localize this ident? *)
570 571 572
      let uquant env (xl,ty) =
        let ty = ty_of_dty ty in
        map_fold_left
573 574 575
          (fun env x ->
             let v = create_vsymbol (id_fresh x) ty in Mstr.add x v env, v)
          env xl
576
      in
577
      let env, vl = map_fold_left uquant env uqu in
578
      let trigger = function
579 580
	| TRterm t -> Term (term env t)
	| TRfmla f -> Fmla (fmla env f)
581 582 583
      in
      let trl = List.map (List.map trigger) trl in
      f_quant q (List.concat vl) trl (fmla env f1)
584 585
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
586
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
587
      let ty = ty_of_dty e1.dt_ty in
588
      let e1 = term env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
589
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
590
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
591 592
      let f2 = fmla env f2 in
      f_let v e1 f2
593 594 595 596
  | 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
597
      in
598
      f_case (List.map (term env) tl) (List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
599
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
600
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
601
      f_label_add x f1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
602 603
  | Fvar f ->
      f
604

605
(** Typing declarations, that is building environments. *)
606 607 608

open Ptree

609
let add_types dl th =
610
  let def =
611
    List.fold_left (fun def d -> Mstr.add d.td_ident.id d def) Mstr.empty dl
612
  in
613
  let tysymbols = Hashtbl.create 17 in
614
  let rec visit x =
615 616 617 618 619 620
    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
621
      let d = Mstr.find x def in
622 623
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
624 625 626 627
      let vl =
	List.map
	  (fun v ->
	     if Hashtbl.mem vars v.id then
628
	       error ~loc:v.id_loc (DuplicateTypeVar v.id);
629
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
630 631
	     Hashtbl.add vars v.id i;
	     i)
632
	  d.td_params
633
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
634
      let id = id_user id d.td_loc in
635
      let ts = match d.td_def with
636
	| TDalias ty ->
637
	    let rec apply = function
638 639
	      | PPTtyvar v ->
		  begin
640 641 642 643 644
		    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
645
		    | Qident x when Mstr.mem x.id def ->
646 647 648 649 650 651 652 653 654 655 656
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
		  try
		    ty_app ts (List.map apply tyl)
		  with Ty.BadTypeArity ->
		    error ~loc:(qloc q) (TypeArity (q, List.length ts.ts_args,
						    List.length tyl))
	    in
	    create_tysymbol id vl (Some (apply ty))
657
	| TDabstract | TDalgebraic _ ->
658 659 660 661 662
	    create_tysymbol id vl None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
663 664
  let th' =
    let tsl =
Andrei Paskevich's avatar
Andrei Paskevich committed
665
      Mstr.fold (fun x _ tsl -> let ts = visit x in (ts, Tabstract) :: tsl) def []
666
    in
667
    add_decl th (create_ty_decl tsl)
668
  in
669
  let decl d =
670
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
671
      | None ->
672
	  assert false
673
      | Some ts ->
674 675
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
676 677 678 679
	  List.iter
	    (fun v ->
	       Hashtbl.add vars v.tv_name.id_short
                  (create_ty_decl_var ~user:true v))
680 681 682 683
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
684
      | TDabstract | TDalias _ ->
685
	  Tabstract
686
      | TDalgebraic cl ->
687
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
688
	  let constructor (loc, id, pl) =
689 690
	    let param (_, t) = ty_of_dty (dty th' t) in
	    let tyl = List.map param pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
691
	    create_fconstr (id_user id.id loc) tyl ty
692 693 694 695
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
696 697
  in
  let dl = List.map decl dl in
698
  List.fold_left add_decl th (create_ty_decls dl)
699

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
700
let env_of_vsymbol_list vl =
Andrei Paskevich's avatar
Andrei Paskevich committed
701
  List.fold_left (fun env v -> Mstr.add v.vs_name.id_short v env) Mstr.empty vl
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
702

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

let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
Andrei Paskevich's avatar
Andrei Paskevich committed
784
  term Mstr.empty t
785

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
786 787 788
let fmla env f =
  let denv = create_denv env in
  let f = dfmla denv f in
Andrei Paskevich's avatar
Andrei Paskevich committed
789
  fmla Mstr.empty f
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
790

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
791 792 793
let add_prop k loc s f th =
  let f = fmla th f in
  try
794
    add_decl th (create_prop_decl k (create_prsymbol (id_user s.id loc)) f)
795
  with ClashSymbol s -> error ~loc (Clash s)
796

Andrei Paskevich's avatar
Andrei Paskevich committed
797 798 799
let loc_of_id id = match id.id_origin with
  | User loc -> loc
  | _ -> assert false
800

801
let add_inductives dl th =
802 803 804 805 806 807 808 809 810 811 812 813
  (* 0. create all propositional symbols *)
  let propsyms = Hashtbl.create 17 in
  let create_prsyms th (loc, id, _) =
    let ps = create_prsymbol (id_user id.id loc) in
    Hashtbl.add propsyms id.id ps;
    try add_decl th (create_prop_decl Paxiom ps f_true)
    with ClashSymbol s -> error ~loc (Clash s)
  in
  let create_prsyms th d = 
    List.fold_left create_prsyms th d.in_def 
  in
  ignore (List.fold_left create_prsyms th dl);
814
  (* 1. create all symbols and make an environment with these symbols *)
815
  let psymbols = Hashtbl.create 17 in
816
  let create_symbol th d =
817
    let id = d.in_ident.id in
Andrei Paskevich's avatar
Andrei Paskevich committed
818
    let v = id_