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

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

32 33
(** errors *)

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

exception Error of error

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

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

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

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

115 116 117 118 119
let () = Exn_printer.register
  (fun fmt exn -> match exn with
    | Error error -> report fmt error
    | _ -> raise exn)

120 121
(** Environments *)

122
(** typing using destructive type variables
123

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

131 132
*)

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

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

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

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

164 165 166 167
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 }

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

(* lazy declaration of tuples *)

let tuples_needed = Hashtbl.create 17

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

let add_tuple_decls uc =
  Hashtbl.fold (fun n _ uc -> Theory.use_export uc (tuple_theory n)) 
    tuples_needed uc

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

let add_ty_decl  = with_tuples add_ty_decl
let add_ty_decls = with_tuples ~reset:true add_ty_decls

let add_logic_decl  = with_tuples add_logic_decl
let add_logic_decls = with_tuples ~reset:true add_logic_decls

let add_ind_decl  = with_tuples add_ind_decl
let add_ind_decls = with_tuples ~reset:true add_ind_decls
210 211 212 213 214 215

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

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
239
  try find ns sl
240 241 242 243 244 245 246 247 248 249 250 251 252
  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
253
  s, specialize_lsymbol ~loc:(qloc p) s
254

255
let specialize_fsymbol p uc =
256
  let s, (tl, ty) = specialize_lsymbol p uc in
257
  match ty with
258
    | None -> let loc = qloc p in error ~loc TermExpected
259
    | Some ty -> s, tl, ty
260

261
let specialize_psymbol p uc =
262
  let s, (tl, ty) = specialize_lsymbol p uc in
263 264
  match ty with
    | None -> s, tl
265 266 267 268 269
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

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

271

272 273
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
274 275 276 277
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

278
(** Typing terms and formulas *)
279 280 281 282 283 284 285

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

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

301 302 303 304
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
305 306 307 308 309
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
310
  | PPpwild ->
311
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
312 313
      env, Pwild, ty
  | PPpvar {id=x} ->
314
      let ty = fresh_type_var loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
315
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
316 317
      env, Pvar x, ty
  | PPpapp (x, pl) ->
318
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
319 320
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      env, Papp (s, pl), ty
321 322 323 324 325 326 327
  | 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
328 329
  | PPpas (p, {id=x}) ->
      let env, p = dpat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
330
      let env = { env with dvars = Mstr.add x p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
331 332
      env, Pas (p,x), p.dp_ty

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
350
let rec trigger_not_a_term_exn = function
351
  | Error TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
352 353 354
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

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

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

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

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

529 530 531 532
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
533
    | [], [] ->
534 535 536 537
	[]
    | 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
538
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
539 540 541 542 543 544
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

545
(** Typing declarations, that is building environments. *)
546 547 548

open Ptree

549
let add_types dl th =
550 551 552 553 554 555
  let def = List.fold_left 
    (fun def d ->
      let id = d.td_ident.id in 
      if Mstr.mem id def then error ~loc:d.td_loc (Clash id);
      Mstr.add id d def) 
    Mstr.empty dl 
556
  in
557
  let tysymbols = Hashtbl.create 17 in
558
  let rec visit x =
559 560 561 562 563 564
    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
565
      let d = Mstr.find x def in
566 567
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
568 569 570 571
      let vl =
	List.map
	  (fun v ->
	     if Hashtbl.mem vars v.id then
572
	       error ~loc:v.id_loc (DuplicateTypeVar v.id);
573
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
574 575
	     Hashtbl.add vars v.id i;
	     i)
576
	  d.td_params
577
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
578
      let id = id_user id d.td_loc in
579
      let ts = match d.td_def with
580
	| TDalias ty ->
581
	    let rec apply = function
582 583
	      | PPTtyvar v ->
		  begin
584 585 586 587 588
		    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
589
		    | Qident x when Mstr.mem x.id def ->
590 591 592 593
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
594
		  begin try
595
		    ty_app ts (List.map apply tyl)
596
		  with Ty.BadTypeArity (_, tsal, tyll) ->
597
		    error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
598 599 600 601
		  end
	      | PPTtuple tyl ->
		  let ts = ts_tuple (List.length tyl) in
		  ty_app ts (List.map apply tyl)
602 603
	    in
	    create_tysymbol id vl (Some (apply ty))
604
	| TDabstract | TDalgebraic _ ->
605 606 607 608 609
	    create_tysymbol id vl None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
610
  let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in 
611
  let th' = try add_ty_decl th tsl
612
    with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (Clash s)
613
  in
614
  let csymbols = Hashtbl.create 17 in
615
  let decl d =
616
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
617
      | None ->
618
	  assert false
619
      | Some ts ->
620 621
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
622 623
	  List.iter
	    (fun v ->
624
	       Hashtbl.add vars v.tv_name.id_string
625
                  (create_ty_decl_var ~user:true v))
626 627 628 629
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
630
      | TDabstract | TDalias _ ->
631
	  Tabstract
632
      | TDalgebraic cl ->
633
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
634
	  let constructor (loc, id, pl) =
635
	    let param (_,t) = ty_of_dty (dty th' t) in
636
	    let tyl = List.map param pl in
637
	    Hashtbl.replace csymbols id.id loc;
638
	    create_fsymbol (id_user id.id loc) tyl ty
639 640 641 642
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
643
  in
644
  try add_ty_decls th (List.map decl dl)
645
  with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
646

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
647
let env_of_vsymbol_list vl =
648
  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
649

650
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
651 652
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
653
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
654
  (* 1. create all symbols and make an environment with these symbols *)
655
  let create_symbol th d =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
656
    let id = d.ld_ident.id in
Andrei Paskevich's avatar
Andrei Paskevich committed
657
    let v = id_user id d.ld_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
658
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
659
    Hashtbl.add denvs id denv;
660
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
661
    let pl = List.map type_ty d.ld_params in
662
    try match d.ld_type with
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
663 664 665
      | None -> (* predicate *)
	  let ps = create_psymbol v pl in
	  Hashtbl.add psymbols id ps;
666
	  add_logic_decl th [ps, None]
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
667 668
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
669
	  let fs = create_fsymbol v pl t in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
670
	  Hashtbl.add fsymbols id fs;
671
	  add_logic_decl th [fs, None]
672
    with ClashSymbol s -> error ~loc:d.ld_loc (Clash s)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
673 674 675
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
676
  let type_decl d =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
677 678 679
    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
680
      | 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
681
    in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
682
    let denv = Hashtbl.find denvs id in
683
    let denv = { denv with uc = th' } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
684
    let denv = List.fold_left dadd_var denv d.ld_params in
685 686
    let create_var (x, _) ty =
      let id = match x with
687 688
	| 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
689 690 691
      in
      create_vsymbol id ty
    in
692
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
693 694 695
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
696 697
        begin match d.ld_def with
	  | None -> ps,None
698
	  | Some f ->
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
699
	      let f = dfmla denv f in
700 701 702 703
              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
704
	      let env = env_of_vsymbol_list vl in
705 706
              make_ps_defn ps vl (fmla env f)
        end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
707
    | Some ty -> (* function *)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
708
	let fs = Hashtbl.find fsymbols id in
709 710
        begin match d.ld_def with
	  | None -> fs,None
711
	  | Some t ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
712
	      let loc = t.pp_loc in
713
	      let ty = dty denv ty in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
714
	      let t = dterm denv t in
715 716
	      if not (unify t.dt_ty ty) then 
		term_expected_type ~loc t.dt_ty ty;
717 718 719 720
              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
721
	      let env = env_of_vsymbol_list vl in
722
	      make_fs_defn fs vl (term env t)
723
        end
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
724
  in
725
  add_logic_decls th (List.map type_decl dl)
726

727
let type_term denv env t =
728
  let t = dterm denv t in
729
  term env t
730

731
let term uc = type_term (create_denv uc) Mstr.empty
732

733
let type_fmla denv env f =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
734
  let f = dfmla denv f in
735
  fmla env f
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
736

737
let fmla uc = type_fmla (create_denv uc) Mstr.empty
738

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
739
let add_prop k loc s f th =
740 741
  let pr = create_prsymbol (id_user s.id loc) in
  try add_prop_decl th k pr (fmla th f)
742
  with ClashSymbol s -> error ~loc (Clash s)
743

Andrei Paskevich's avatar
Andrei Paskevich committed
744 745 746
let loc_of_id id = match id.id_origin with
  | User loc -> loc
  | _ -> assert false
747

748 749
let add_inductives dl th =
  (* 1. create all symbols and make an environment with these symbols *)
750
  let psymbols = Hashtbl.create 17 in
751
  let create_symbol th d =
752
    let id = d.in_ident.id in
Andrei Paskevich's avatar
Andrei Paskevich committed
753
    let v = id_user id d.in_loc in
754
    let denv = create_denv th in
755
    let type_ty (_,t) = ty_of_dty (dty denv t) in
756 757 758
    let pl = List.map type_ty d.in_params in
    let ps = create_psymbol v pl in
    Hashtbl.add psymbols id ps;
759
    try add_logic_decl th [ps, None]
760
    with ClashSymbol s -> error ~loc:d.in_loc (Clash s)
761
  in
762 763
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
764
  let propsyms = Hashtbl.create 17 in
765
  let type_decl d =