Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

typing.ml 30.7 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 47 48 49 50 51
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 AlreadyTheory of string
exception UnboundFile of string
exception UnboundDir of string
exception AmbiguousPath of string * string
exception NotInLoadpath of string
exception CyclicTypeDef
exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list
52 53

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

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

68
let rec print_qualid fmt = function
69
  | Qident s -> fprintf fmt "%s" s.id
70
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
71

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

113 114
(** Environments *)

115
(** typing using destructive type variables
116

117 118 119 120 121 122
    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
123

124 125
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
126 127 128 129 130
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

131 132 133 134
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

135
type denv = {
136 137 138 139 140
  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 *)
}

141 142 143
let create_denv uc = {
  uc = uc;
  utyvars = Hashtbl.create 17;
144 145 146 147 148 149 150 151 152 153 154 155
  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
156

157 158 159 160
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 }

161 162 163 164 165 166 167 168 169 170 171 172
(* 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
173
  let ts =
174 175 176
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
  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
196
let add_ty_decls = with_tuples ~reset:true add_ty_decl
197 198

let add_logic_decl  = with_tuples add_logic_decl
199
let add_logic_decls = with_tuples ~reset:true add_logic_decl
200 201

let add_ind_decl  = with_tuples add_ind_decl
202
let add_ind_decls = with_tuples ~reset:true add_ind_decl
203

204 205
let add_prop_decl = with_tuples ~reset:true add_prop_decl

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

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
234
  try find ns sl
235 236
  with Not_found -> error ~loc (UnboundSymbol sl)

237
let find_prop_ns = find_ns ns_find_pr
238 239 240 241 242 243 244 245 246 247
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
248
  s, specialize_lsymbol ~loc:(qloc p) s
249

250
let specialize_fsymbol p uc =
251
  let s, (tl, ty) = specialize_lsymbol p uc in
252
  match ty with
253
    | None -> let loc = qloc p in error ~loc TermExpected
254
    | Some ty -> s, tl, ty
255

256
let specialize_psymbol p uc =
257
  let s, (tl, ty) = specialize_lsymbol p uc in
258 259
  match ty with
    | None -> s, tl
260 261 262 263 264
    | 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
265

266

267 268
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
269 270 271 272
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

273
(** Typing terms and formulas *)
274 275 276 277 278 279 280

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

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

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

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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
514 515 516 517 518 519 520
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
521

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

538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553
(** 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
554
    t_close_branch (pat_app cs al tyarg) (t_var vs)
555 556
  in
  let vs = create_vsymbol (id_fresh "u") tyarg in
557
  let t = t_case (t_var vs) (List.map per_cs cl) in
558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582
  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))

583
(** Typing declarations, that is building environments. *)
584 585 586

open Ptree

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

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
687
let env_of_vsymbol_list vl =
688
  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
689

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

767
let type_term denv env t =
768
  let t = dterm denv t in
769
  term env t
770

771
let term uc = type_term (create_denv uc) Mstr.empty
772

773
let type_fmla denv env f =
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
774
  let f = dfmla denv f in
775
  fmla env f
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
776

777
let fmla uc = type_fmla (create_denv uc) Mstr.empty
778

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
779
let add_prop k loc s f th =
780 781
  let pr = create_prsymbol (id_user s.id loc) in
  try add_prop_decl th k pr (fmla th f)
782
  with ClashSymbol s -> error ~loc (Clash s)
783

Andrei Paskevich's avatar
Andrei Paskevich committed
784 785 786
let loc_of_id id = match id.id_origin with
  | User loc -> loc
  | _ -> assert false
787

788 789
let add_inductives dl th =
  (* 1. create all symbols and make an environment with these symbols *)
790