Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

typing.ml 30 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
  | ClashType of string
37
  | DuplicateTypeVar of string
38
  | TypeArity of qualid * int * int
39
  | Clash of string
40 41
  | PredicateExpected
  | TermExpected
42
  | BadNumberOfArguments of Ident.ident * int * int
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
43
  | ClashTheory of string
44
  | ClashNamespace of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45
  | UnboundTheory of qualid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
46
  | AlreadyTheory of string
47 48 49 50
  | UnboundFile of string
  | UnboundDir of string
  | AmbiguousPath of string * string
  | NotInLoadpath of string
51 52
  | CyclicTypeDef
  | UnboundTypeVar of string
53 54
  | UnboundType of string list
  | UnboundSymbol of string list
55 56 57 58 59 60 61

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

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

77
let report fmt = function
78 79
  | Message s ->
      fprintf fmt "%s" s
80 81
  | ClashType s ->
      fprintf fmt "clash with previous type %s" s
82
  | DuplicateTypeVar s ->
83
      fprintf fmt "duplicate type parameter %s" s
84
  | TypeArity (id, a, n) ->
85
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
86 87
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
88
      fprintf fmt "Clash with previous symbol %s" id
89 90 91 92
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
93
  | BadNumberOfArguments (s, n, m) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short n;
95
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96 97
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
98 99
  | ClashNamespace s ->
      fprintf fmt "clash with previous namespace %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
100 101
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
102 103
  | AlreadyTheory s ->
      fprintf fmt "already using a theory with name %s" s
104 105 106 107 108 109 110 111
  | 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
112 113 114 115
  | CyclicTypeDef ->
      fprintf fmt "cyclic type definition"
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
116 117 118 119
  | 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
120

121 122
(** Environments *)

123
(** typing using destructive type variables
124

125 126 127 128 129 130
    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
131

132 133
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
134 135 136 137 138
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

139 140 141 142
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

143
type denv = {
144 145 146 147 148
  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 *)
}

149 150 151
let create_denv uc = {
  uc = uc;
  utyvars = Hashtbl.create 17;
152 153 154 155 156 157 158 159 160 161 162 163
  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
164

165 166 167 168 169 170 171 172 173 174 175 176
(* 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
177
  let ts =
178 179 180 181 182 183 184 185 186 187
    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
188
  | PPTtyvar {id=x} ->
189 190 191 192 193 194 195 196 197
      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
198
	| None ->
199
	    Tyapp (ts, tyl)
200
	| Some ty ->
201 202 203 204 205 206 207
	    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
208
  try find ns sl
209 210 211 212 213 214 215 216 217 218 219 220 221 222 223
  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

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

231
let specialize_psymbol p uc =
232 233
  let loc = qloc p in
  let s, (tl, ty) = specialize_lsymbol p uc in
234 235 236
  match ty with
    | None -> s, tl
    | Some _ -> error ~loc PredicateExpected
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
  | Tlet of dterm * string * dterm
264
  | Tmatch of dterm list * (dpattern list * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265
  | Tnamed of string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
266
  | Teps of string * dty * dfmla
267

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

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

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

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

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

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

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

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

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

422 423 424 425 426 427 428 429 430 431
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) ->
432
      Fif (dfmla env a, dfmla env b, dfmla env c)
433
  | PPquant (q, uqu, trl, a) ->
434
      check_quant_linearity uqu;
435 436
      let uquant env (idl,ty) =
        let ty = dty env ty in
437
        let env, idl =
438
          map_fold_left
Andrei Paskevich's avatar
Andrei Paskevich committed
439
            (fun env {id=x} -> { env with dvars = Mstr.add x ty env.dvars }, x)
440 441 442
            env idl
        in
        env, (idl,ty)
443
      in
444
      let env, uqu = map_fold_left uquant env uqu in
445
      let trigger e =
446 447
	try
	  TRterm (dterm env e)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
448
	with exn when trigger_not_a_term_exn exn ->
449
	  TRfmla (dfmla env e)
450 451
      in
      let trl = List.map (List.map trigger) trl in
452 453
      let q = match q with
        | PPforall -> Fforall
454 455 456
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
457
  | PPapp (x, tl) ->
458
      let s, tyl = specialize_psymbol x env.uc in
459
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
460
      Fapp (s, tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
461 462 463
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
464
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
465 466
      let e2 = dfmla env e2 in
      Flet (e1, x, e2)
467 468 469 470 471
  | 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
472
      in
473
      Fmatch (tl, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
474 475 476
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
477
  | PPvar x ->
478
      Fvar (snd (find_prop x env.uc))
Andrei Paskevich's avatar
Andrei Paskevich committed
479
  | PPeps _ | PPconst _ | PPcast _ ->
480
      error ~loc:e.pp_loc PredicateExpected
481

482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498
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

499 500 501 502
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
503
    | [], [] ->
504 505 506 507
	[]
    | 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
508
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
509 510 511 512 513 514
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

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

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

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

611
(** Typing declarations, that is building environments. *)
612 613 614

open Ptree

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

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
713
let env_of_vsymbol_list vl =
Andrei Paskevich's avatar
Andrei Paskevich committed
714
  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
715

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