typing.ml 28.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 35 36 37 38 39 40 41 42 43 44 45 46
exception Message of string
exception DuplicateTypeVar of string
exception TypeArity of qualid * int * int
exception Clash of string
exception PredicateExpected
exception TermExpected
exception BadNumberOfArguments of Ident.ident * int * int
exception ClashTheory of string
exception UnboundTheory of qualid
exception CyclicTypeDef
exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list
47 48

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
52 53 54
let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
55 56
  Format.kfprintf
    (fun _ ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
57 58 59
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
60
       error ?loc (Message s))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
61 62
    fmt f

63
let rec print_qualid fmt = function
64
  | Qident s -> fprintf fmt "%s" s.id
65
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
66

67
let () = Exn_printer.register (fun fmt e -> match e with
68 69
  | Message s ->
      fprintf fmt "%s" s
70
  | DuplicateTypeVar s ->
71
      fprintf fmt "duplicate type parameter %s" s
72
  | TypeArity (id, a, n) ->
73
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
74 75
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76
      fprintf fmt "Clash with previous symbol %s" id
77 78 79 80
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
81
  | BadNumberOfArguments (s, n, m) ->
82
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_string n;
83
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84 85
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
86 87
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
88 89 90 91
  | CyclicTypeDef ->
      fprintf fmt "cyclic type definition"
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
92 93 94 95
  | UnboundType sl ->
       fprintf fmt "Unbound type '%a'" (print_list dot pp_print_string) sl
  | UnboundSymbol sl ->
       fprintf fmt "Unbound symbol '%a'" (print_list dot pp_print_string) sl
96
  | _ -> raise e)
97

98 99 100
let debug_parse_only = Debug.register_flag "parse_only"
let debug_type_only  = Debug.register_flag "type_only"

101 102
(** Environments *)

103
(** typing using destructive type variables
104

105 106 107 108 109 110
    parsed trees        intermediate trees       typed trees
      (Ptree)               (D below)               (Term)
   -----------------------------------------------------------
     ppure_type  ---dty--->   dty       ---ty--->    ty
      lexpr      --dterm-->   dterm     --term-->    term
      lexpr      --dfmla-->   dfmla     --fmla-->    fmla
111

112 113
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114 115 116 117 118
let term_expected_type ~loc ty1 ty2 =
  errorm ~loc
    "@[This term has type %a@ but is expected to have type@ %a@]"
    print_dty ty1 print_dty ty2

119 120 121 122
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

123
type denv = {
124 125 126 127 128
  uc : theory_uc; (* the theory under construction *)
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
  dvars : dty Mstr.t; (* local variables, to be bound later *)
}

129 130 131
let create_denv uc = {
  uc = uc;
  utyvars = Hashtbl.create 17;
132 133 134 135 136 137 138 139 140 141 142 143
  dvars = Mstr.empty;
}

let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
    (* TODO: shouldn't we localize this ident? *)
    let v = create_tvsymbol (id_fresh x) in
    let v = create_ty_decl_var ~user:true v in
    Hashtbl.add env.utyvars x v;
    v
144

145 146 147 148
let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars
let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars }

149 150 151 152 153 154 155 156 157 158 159 160
(* parsed types -> intermediate types *)

let rec qloc = function
  | Qident x -> x.id_loc
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc

let rec string_list_of_qualid acc = function
  | Qident id -> id.id :: acc
  | Qdot (p, id) -> string_list_of_qualid (id.id :: acc) p

let specialize_tysymbol loc p uc =
  let sl = string_list_of_qualid [] p in
161
  let ts =
162 163 164
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
165 166 167 168 169 170 171 172 173 174
  ts, List.length ts.ts_args

(* lazy declaration of tuples *)

let tuples_needed = Hashtbl.create 17

let ts_tuple n = Hashtbl.replace tuples_needed n (); ts_tuple n
let fs_tuple n = Hashtbl.replace tuples_needed n (); fs_tuple n

let add_tuple_decls uc =
175
  Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n))
176 177 178 179 180 181 182 183
    tuples_needed uc

let with_tuples ?(reset=false) f uc x =
  let uc = f (add_tuple_decls uc) x in
  if reset then Hashtbl.clear tuples_needed;
  uc

let add_ty_decl  = with_tuples add_ty_decl
184
let add_ty_decls = with_tuples ~reset:true add_ty_decl
185 186

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

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

192 193
let add_prop_decl = with_tuples ~reset:true add_prop_decl

194 195 196 197 198
let rec type_inst s ty = match ty.ty_node with
  | Ty.Tyvar n -> Mtv.find n s
  | Ty.Tyapp (ts, tyl) -> Tyapp (ts, List.map (type_inst s) tyl)

let rec dty env = function
199
  | PPTtyvar {id=x} ->
200 201 202
      Tyvar (find_user_type_var x env)
  | PPTtyapp (p, x) ->
      let loc = qloc x in
203
      let ts, a = specialize_tysymbol loc x env.uc in
204 205 206
      let np = List.length p in
      if np <> a then error ~loc (TypeArity (x, a, np));
      let tyl = List.map (dty env) p in
207
      begin match ts.ts_def with
208
	| None ->
209
	    Tyapp (ts, tyl)
210
	| Some ty ->
211 212 213
	    let add m v t = Mtv.add v t m in
            let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
	    type_inst s ty
214 215 216 217
      end
  | PPTtuple tyl ->
      let ts = ts_tuple (List.length tyl) in
      Tyapp (ts, List.map (dty env) tyl)
218 219 220 221

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

225
let find_prop_ns = find_ns ns_find_pr
226 227 228 229 230 231 232 233 234 235
let find_prop p uc = find_prop_ns p (get_namespace uc)

let find_tysymbol_ns = find_ns ns_find_ts
let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)

let find_lsymbol_ns = find_ns ns_find_ls
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)

let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
236
  s, specialize_lsymbol ~loc:(qloc p) s
237

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

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

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

254

255 256
(** Typing types *)

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

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

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

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

285 286 287 288
let fresh_type_var loc =
  let tv = create_tvsymbol (id_user "a" loc) in
  Tyvar (create_ty_decl_var ~loc ~user:false tv)

Andrei Paskevich's avatar
Andrei Paskevich committed
289 290 291 292 293
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
294
  | PPpwild ->
295
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
296
      env, Pwild, ty
Andrei Paskevich's avatar
Andrei Paskevich committed
297
  | PPpvar x ->
298
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
299
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
300 301
      env, Pvar x, ty
  | PPpapp (x, pl) ->
302
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
303 304
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      env, Papp (s, pl), ty
305 306 307 308 309 310 311
  | PPptuple pl ->
      let n = List.length pl in
      let s = fs_tuple n in
      let tyl = List.map (fun _ -> fresh_type_var loc) pl in
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      let ty = Tyapp (ts_tuple n, tyl) in
      env, Papp (s, pl), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
312
  | PPpas (p, x) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
313
      let env, p = dpat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
314
      let env = { env with dvars = Mstr.add x.id p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
315
      env, Pas (p,x), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
316 317 318 319 320 321
  | PPpor (p, q) ->
      let env, p = dpat env p in
      let env, q = dpat env q in
      if not (unify p.dp_ty q.dp_ty)
        then term_expected_type ~loc p.dp_ty q.dp_ty;
      env, Por (p,q), p.dp_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
322

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
  | 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
  in
351
  List.iter (fun (idl, _) -> Util.option_iter check idl) uqu
352

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
372 373 374 375 376 377 378
  | PPtuple tl ->
      let n = List.length tl in
      let s = fs_tuple n in
      let tyl = List.map (fun _ -> fresh_type_var loc) tl in
      let tl = dtype_args s.ls_name loc env tyl tl in
      let ty = Tyapp (ts_tuple n, tyl) in
      Tapp (s, tl), ty
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, [])
Andrei Paskevich's avatar
Andrei Paskevich committed
387
  | PPlet (x, e1, e2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
388 389
      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.id 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
Andrei Paskevich's avatar
Andrei Paskevich committed
393 394 395
  | PPmatch (e1, bl) ->
      let t1 = dterm env e1 in
      let ty1 = t1.dt_ty in
396
      let tb = fresh_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
397 398
      let branch (p, e) =
        let env, p = dpat_list env ty1 p in
399
        let loc = e.pp_loc in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
400 401
	let e = dterm env e in
	if not (unify e.dt_ty tb) then term_expected_type ~loc e.dt_ty tb;
Andrei Paskevich's avatar
Andrei Paskevich committed
402
        p, e
Andrei Paskevich's avatar
Andrei Paskevich committed
403 404 405
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
406
      Tmatch (t1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
407 408 409
  | 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
410 411 412 413 414 415
  | 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
416 417 418 419 420 421 422
  | 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
423
  | PPeps (x, ty, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
424
      let ty = dty env ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
425
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
426 427
      let e1 = dfmla env e1 in
      Teps (x, ty, e1), ty
428
  | PPquant _
429
  | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
430
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
431

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

Andrei Paskevich's avatar
Andrei Paskevich committed
502 503 504 505 506 507 508
and dpat_list env ty p =
  check_pat_linearity p;
  let loc = p.pat_loc in
  let env, p = dpat env p in
  if not (unify p.dp_ty ty)
    then term_expected_type ~loc p.dp_ty ty;
  env, p
509

510 511 512 513
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
514
    | [], [] ->
515 516 517 518
	[]
    | 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
519
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
520 521 522 523 524 525
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541
(** Add projection functions for the algebraic types *)

let add_projection cl p (fs,tyarg,tyval) th =
  let vs = create_vsymbol (id_fresh p) tyval in
  let per_cs (_,id,pl) =
    let cs = find_lsymbol (Qident id) th in
    let tc = match cs.ls_value with
      | None -> assert false
      | Some t -> t
    in
    let m = ty_match Mtv.empty tc tyarg in
    let per_param ty (n,_) = match n with
      | Some id when id.id = p -> pat_var vs
      | _ -> pat_wild (ty_inst m ty)
    in
    let al = List.map2 per_param cs.ls_args pl in
542
    t_close_branch (pat_app cs al tyarg) (t_var vs)
543 544
  in
  let vs = create_vsymbol (id_fresh "u") tyarg in
545
  let t = t_case (t_var vs) (List.map per_cs cl) in
546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570
  let d = make_fs_defn fs [vs] t in
  add_logic_decl th [d]

let add_projections th d = match d.td_def with
  | TDabstract | TDalias _ -> th
  | TDalgebraic cl ->
      let per_cs acc (_,id,pl) =
        let cs = find_lsymbol (Qident id) th in
        let tc = match cs.ls_value with
          | None -> assert false
          | Some t -> t
        in
        let per_param acc ty (n,_) = match n with
          | Some id when not (Mstr.mem id.id acc) ->
              let fn = id_user id.id id.id_loc in
              let fs = create_fsymbol fn [tc] ty in
              Mstr.add id.id (fs,tc,ty) acc
          | _ -> acc
        in
        List.fold_left2 per_param acc cs.ls_args pl
      in
      let ps = List.fold_left per_cs Mstr.empty cl in
      try Mstr.fold (add_projection cl) ps th
      with e -> raise (Loc.Located (d.td_loc, e))

571
(** Typing declarations, that is building environments. *)
572 573 574

open Ptree

575
let add_types dl th =
576
  let def = List.fold_left
577
    (fun def d ->
578
      let id = d.td_ident.id in
579
      if Mstr.mem id def then error ~loc:d.td_loc (Clash id);
580 581
      Mstr.add id d def)
    Mstr.empty dl
582
  in
583
  let tysymbols = Hashtbl.create 17 in
584
  let rec visit x =
585 586 587 588 589 590
    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
591
      let d = Mstr.find x def in
592 593
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
594 595 596 597
      let vl =
	List.map
	  (fun v ->
	     if Hashtbl.mem vars v.id then
598
	       error ~loc:v.id_loc (DuplicateTypeVar v.id);
599
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
600 601
	     Hashtbl.add vars v.id i;
	     i)
602
	  d.td_params
603
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
604
      let id = id_user id d.td_loc in
605
      let ts = match d.td_def with
606
	| TDalias ty ->
607
	    let rec apply = function
608 609
	      | PPTtyvar v ->
		  begin
610 611 612 613 614
		    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
615
		    | Qident x when Mstr.mem x.id def ->
616 617 618 619
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
620
		  begin try
621
		    ty_app ts (List.map apply tyl)
622
		  with Ty.BadTypeArity (_, tsal, tyll) ->
623
		    error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
624 625 626 627
		  end
	      | PPTtuple tyl ->
		  let ts = ts_tuple (List.length tyl) in
		  ty_app ts (List.map apply tyl)
628 629
	    in
	    create_tysymbol id vl (Some (apply ty))
630
	| TDabstract | TDalgebraic _ ->
631 632 633 634 635
	    create_tysymbol id vl None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
636
  let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in
637
  let th' = try add_ty_decl th tsl
638
    with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (Clash s)
639
  in
640
  let csymbols = Hashtbl.create 17 in
641
  let decl d =
642
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
643
      | None ->
644
	  assert false
645
      | Some ts ->
646 647
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
648 649
	  List.iter
	    (fun v ->
650
	       Hashtbl.add vars v.tv_name.id_string
651
                  (create_ty_decl_var ~user:true v))
652 653 654 655
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
656
      | TDabstract | TDalias _ ->
657
	  Tabstract
658
      | TDalgebraic cl ->
659
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
660
	  let constructor (loc, id, pl) =
661
	    let param (_,t) = ty_of_dty (dty th' t) in
662
	    let tyl = List.map param pl in
663
	    Hashtbl.replace csymbols id.id loc;
664
	    create_fsymbol (id_user id.id loc) tyl ty
665 666 667 668
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
669
  in
670 671 672 673
  let th = try add_ty_decls th (List.map decl dl)
    with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
  in
  List.fold_left add_projections th dl
674

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
675
let env_of_vsymbol_list vl =
676
  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
677

678
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
679 680
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
681
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
682
  (* 1. create all symbols and make an environment with these symbols *)
683
  let create_symbol th d =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
684
    let id = d.ld_ident.id in
Andrei Paskevich's avatar
Andrei Paskevich committed
685
    let v = id_user id d.ld_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
686
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
687
    Hashtbl.add denvs id denv;
688
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
689
    let pl = List.map type_ty d.ld_params in
690
    try match d.ld_type with
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
691 692 693
      | None -> (* predicate *)
	  let ps = create_psymbol v pl in
	  Hashtbl.add psymbols id ps;
694
	  add_logic_decl th [ps, None]
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
695 696
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
697
	  let fs = create_fsymbol v pl t in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
698
	  Hashtbl.add fsymbols id fs;
699
	  add_logic_decl th [fs, None]
700
    with ClashSymbol s -> error ~loc:d.ld_loc (Clash s)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
701 702 703
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
704
  let type_decl d =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
705 706 707
    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
708
      | 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
709
    in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
710
    let denv = Hashtbl.find denvs id in
711
    let denv = { denv with uc = th' } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
712
    let denv = List.fold_left dadd_var denv d.ld_params in
713 714
    let create_var (x, _) ty =
      let id = match x with
715 716
	| 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
717 718 719
      in
      create_vsymbol id ty
    in
720
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
721 722 723
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
724 725
        begin match d.ld_def with
	  | None -> ps,None
726
	  | Some f ->
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
727
	      let f = dfmla denv f in
728 729 730 731
              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
732
	      let env = env_of_vsymbol_list vl in
733 734
              make_ps_defn ps vl (fmla env f)
        end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
735
    | Some ty -> (* function *)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
736
	let fs = Hashtbl.find fsymbols id in
737 738
        begin match d.ld_def with
	  | None -> fs,None
739
	  | Some t ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
740
	      let loc = t.pp_loc in
741
	      let ty = dty denv ty in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
742
	      let t = dterm denv t in
743
	      if not (unify t.dt_ty ty) then
744
		term_expected_type ~loc t.dt_ty ty;
745 746 747 748
              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
749
	      let env = env_of_vsymbol_list vl in
750
	      make_fs_defn fs vl (term env t)
751
        end
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
752
  in
753
  add_logic_decls th (List.map type_decl dl)
754

755
let type_term denv env t =
756
  let t = dterm denv t in
757
  term env t
758

759
let term uc = type_term (create_denv uc) Mstr.empty
760

761
let type_fmla denv env f =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
762
  let f = dfmla denv f in
763
  fmla env f
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
764

765
let fmla uc = type_fmla (create_denv uc) Mstr.empty
766

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
767
let add_prop k loc s f th =
768 769
  let pr = create_prsymbol (id_user s.id loc) in
  try add_prop_decl th k pr (fmla th f)
770
  with ClashSymbol s -> error ~loc (Clash s)
771