typing.ml 33.9 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
3
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4
5
6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
7
(*    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
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)

234
235
236
let find_namespace_ns = find_ns ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)

237
238
let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
239
240
  let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
  s,tl,ty
241

242
let specialize_fsymbol p uc =
243
  let s,tl,ty = specialize_lsymbol p uc in
244
  match ty with
245
    | None -> let loc = qloc p in error ~loc TermExpected
246
    | Some ty -> s, tl, ty
247

248
let specialize_psymbol p uc =
249
  let s,tl,ty = specialize_lsymbol p uc in
250
251
  match ty with
    | None -> s, tl
252
253
    | Some _ -> let loc = qloc p in error ~loc PredicateExpected

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

258

259
260
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
261
262
263
264
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

265
(** Typing terms and formulas *)
266
267
268
269
270
271
272

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

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

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

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
357
358
359
360
361
362
363
364
365
let check_highord env x tl = match x with
  | Qident { id = x } when Mstr.mem x env.dvars -> true
  | _ -> List.length tl > List.length ((find_lsymbol x env.uc).ls_args)

let apply_highord loc x tl = match List.rev tl with
  | a::[] -> [{pp_loc = loc; pp_desc = PPvar x}; a]
  | a::tl -> [{pp_loc = loc; pp_desc = PPapp (x, List.rev tl)}; a]
  | [] -> assert false

366
367
368
369
370
371
372
373
374
375
let rec dterm ?(localize=false) env { pp_loc = loc; pp_desc = t } =
  let n, ty = dterm_node ~localize loc env t in
  let t = { dt_node = n; dt_ty = ty } in
  if localize then
    let n = Tnamed (Ident.label ~loc "", t) in
    { dt_node = n; dt_ty = ty }
  else
    t

and dterm_node ~localize loc env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
376
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
377
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
378
      let ty = Mstr.find x env.dvars in
379
      Tvar x, ty
380
  | PPvar x ->
381
      (* 0-arity symbol (constant) *)
382
      let s, tyl, ty = specialize_fsymbol x env.uc in
383
      let n = List.length tyl in
384
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
385
      Tapp (s, []), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
386
387
388
389
390
  | PPapp (x, tl) when check_highord env x tl ->
      let tl = apply_highord loc x tl in
      let atyl, aty = Denv.specialize_lsymbol ~loc fs_func_app in
      let tl = dtype_args fs_func_app.ls_name loc env atyl tl in
      Tapp (fs_func_app, tl), Util.of_option aty
391
  | PPapp (x, tl) ->
392
      let s, tyl, ty = specialize_fsymbol x env.uc in
393
      let tl = dtype_args s.ls_name loc env tyl tl in
394
      Tapp (s, tl), ty
395
396
397
398
399
400
401
  | 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
402
403
404
405
  | 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
406
  | PPconst (ConstInt _ as c) ->
407
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
408
  | PPconst (ConstReal _ as c) ->
409
      Tconst c, Tyapp (Ty.ts_real, [])
Andrei Paskevich's avatar
Andrei Paskevich committed
410
  | PPlet (x, e1, e2) ->
411
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
412
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
413
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
414
      let e2 = dterm ~localize env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
415
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
416
  | PPmatch (e1, bl) ->
417
      let t1 = dterm ~localize env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
418
      let ty1 = t1.dt_ty in
419
      let tb = fresh_type_var loc in (* the type of all branches *)
Andrei Paskevich's avatar
Andrei Paskevich committed
420
421
      let branch (p, e) =
        let env, p = dpat_list env ty1 p in
422
        let loc = e.pp_loc in
423
	let e = dterm ~localize env e in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
424
	if not (unify e.dt_ty tb) then term_expected_type ~loc e.dt_ty tb;
Andrei Paskevich's avatar
Andrei Paskevich committed
425
        p, e
Andrei Paskevich's avatar
Andrei Paskevich committed
426
427
428
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
429
      Tmatch (t1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
430
  | PPnamed (x, e1) ->
431
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
432
      Tnamed (x, e1), e1.dt_ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
433
434
  | PPcast (e1, ty) ->
      let loc = e1.pp_loc in
435
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
436
437
438
      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
439
440
  | PPif (e1, e2, e3) ->
      let loc = e3.pp_loc in
441
442
      let e2 = dterm ~localize env e2 in
      let e3 = dterm ~localize env e3 in
443
444
      if not (unify e2.dt_ty e3.dt_ty) then
        term_expected_type ~loc e3.dt_ty e2.dt_ty;
445
      Tif (dfmla ~localize env e1, e2, e3), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
446
  | PPeps (x, ty, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
447
      let ty = dty env ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
448
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
449
      let e1 = dfmla ~localize env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
450
      Teps (x, ty, e1), ty
451
  | PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
452
453
454
455
456
457
458
459
460
461
462
463
      check_quant_linearity uqu;
      let uquant env (idl,ty) =
        let ty = dty env ty in
        let id = match idl with
          | Some id -> id
          | None -> assert false
        in
        { env with dvars = Mstr.add id.id ty env.dvars }, (id,ty)
      in
      let env, uqu = map_fold_left uquant env uqu in
      let trigger e =
	try
464
	  TRterm (dterm ~localize env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
465
	with exn when trigger_not_a_term_exn exn ->
466
	  TRfmla (dfmla ~localize env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
467
468
      in
      let trl = List.map (List.map trigger) trl in
469
      let e = match q with
470
471
        | PPfunc -> TRterm (dterm ~localize env a)
        | PPpred -> TRfmla (dfmla ~localize env a)
472
473
474
475
        | PPlambda -> trigger a
        | _ -> assert false
      in
      let id, ty, f = match e with
Andrei Paskevich's avatar
Andrei Paskevich committed
476
        | TRterm t ->
477
            let id = { id = "fc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
478
479
480
481
482
483
484
485
486
487
488
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
              let nty = Tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
              uqu ([],t.dt_ty)
            in
            let h = { dt_node = Tvar id.id ; dt_ty = ty } in
            let h = List.fold_left2 (fun h (uid,uty) ty ->
              let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
              { dt_node = Tapp (fs_func_app, [h;u]) ; dt_ty = ty })
              h uqu tyl
            in
            id, ty, Fapp (ps_equ, [h;t])
Andrei Paskevich's avatar
Andrei Paskevich committed
489
        | TRfmla f ->
490
            let id = { id = "pc"; id_lab = []; id_loc = loc } in
Andrei Paskevich's avatar
Andrei Paskevich committed
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
            let (uid,uty),uqu = match List.rev uqu with
              | uq :: uqu -> uq, List.rev uqu
              | [] -> assert false
            in
            let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
              let nty = Tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
              uqu ([],Tyapp (ts_pred, [uty]))
            in
            let h = { dt_node = Tvar id.id ; dt_ty = ty } in
            let h = List.fold_left2 (fun h (uid,uty) ty ->
              let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
              { dt_node = Tapp (fs_func_app, [h;u]) ; dt_ty = ty })
              h uqu tyl
            in
            let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
            id, ty, Fbinop (Fiff, Fapp (ps_pred_app, [h;u]), f)
      in
      Teps (id, ty, Fquant (Fforall, uqu, trl, f)), ty
Andrei Paskevich's avatar
Andrei Paskevich committed
509
  | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
510
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
511

512
513
514
515
516
and dfmla ?(localize=false) env { pp_loc = loc; pp_desc = f } =
  let n = dfmla_node ~localize loc env f in
  if localize then Fnamed (Ident.label ~loc "", n) else n

and dfmla_node ~localize loc env = function
517
518
519
520
  | PPtrue ->
      Ftrue
  | PPfalse ->
      Ffalse
521
  | PPunop (PPnot, a) ->
522
      Fnot (dfmla ~localize env a)
523
  | PPbinop (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
524
      Fbinop (binop op, dfmla ~localize env a, dfmla ~localize env b)
525
  | PPif (a, b, c) ->
526
      Fif (dfmla ~localize env a, dfmla ~localize env b, dfmla ~localize env c)
527
  | PPquant (q, uqu, trl, a) ->
528
      check_quant_linearity uqu;
529
530
      let uquant env (idl,ty) =
        let ty = dty env ty in
531
        let id = match idl with
Andrei Paskevich's avatar
Andrei Paskevich committed
532
          | Some id -> id
533
          | None -> assert false
534
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
535
        { env with dvars = Mstr.add id.id ty env.dvars }, (id,ty)
536
      in
537
      let env, uqu = map_fold_left uquant env uqu in
538
      let trigger e =
539
	try
540
	  TRterm (dterm ~localize env e)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
541
	with exn when trigger_not_a_term_exn exn ->
542
	  TRfmla (dfmla ~localize env e)
543
544
      in
      let trl = List.map (List.map trigger) trl in
545
546
      let q = match q with
        | PPforall -> Fforall
547
        | PPexists -> Fexists
548
        | _ -> error ~loc PredicateExpected
549
      in
550
      Fquant (q, uqu, trl, dfmla ~localize env a)
Andrei Paskevich's avatar
Andrei Paskevich committed
551
  | PPapp (x, tl) when check_highord env x tl ->
552
553
554
      let tl = apply_highord loc x tl in
      let atyl, _ = Denv.specialize_lsymbol ~loc ps_pred_app in
      let tl = dtype_args ps_pred_app.ls_name loc env atyl tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
555
      Fapp (ps_pred_app, tl)
556
  | PPapp (x, tl) ->
557
      let s, tyl = specialize_psymbol x env.uc in
558
      let tl = dtype_args s.ls_name loc env tyl tl in
559
      Fapp (s, tl)
560
561
562
  | PPinfix (e12, op2, e3) ->
      begin match e12.pp_desc with
	| PPinfix (_, op1, e2) when is_psymbol (Qident op1) env.uc ->
563
564
	    let e23 = { pp_desc = PPinfix (e2, op2, e3); pp_loc = loc } in
	    Fbinop (Fand, dfmla ~localize env e12, dfmla ~localize env e23)
565
566
	| _ ->
	    let s, tyl = specialize_psymbol (Qident op2) env.uc in
567
	    let tl = dtype_args s.ls_name loc env tyl [e12; e3] in
568
569
	    Fapp (s, tl)
      end
Andrei Paskevich's avatar
Andrei Paskevich committed
570
  | PPlet (x, e1, e2) ->
571
      let e1 = dterm ~localize env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
572
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
573
      let env = { env with dvars = Mstr.add x.id ty env.dvars } in
574
      let e2 = dfmla ~localize env e2 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
575
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
576
  | PPmatch (e1, bl) ->
577
      let t1 = dterm ~localize env e1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
578
579
      let ty1 = t1.dt_ty in
      let branch (p, e) =
580
        let env, p = dpat_list env ty1 p in p, dfmla ~localize env e
Andrei Paskevich's avatar
Andrei Paskevich committed
581
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
582
      Fmatch (t1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
583
  | PPnamed (x, f1) ->
584
      let f1 = dfmla ~localize env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
585
      Fnamed (x, f1)
586
  | PPvar x ->
587
588
      let pr = find_prop x env.uc in
      Fvar (Decl.find_prop (Theory.get_known env.uc) pr)
589
  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ ->
590
      error ~loc PredicateExpected
591

Andrei Paskevich's avatar
Andrei Paskevich committed
592
593
594
595
596
597
598
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
599

600
601
602
603
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
604
    | [], [] ->
605
606
607
608
	[]
    | 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
609
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
610
611
612
613
614
615
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
(** 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
632
    t_close_branch (pat_app cs al tyarg) (t_var vs)
633
634
  in
  let vs = create_vsymbol (id_fresh "u") tyarg in
635
  let t = t_case (t_var vs) (List.map per_cs cl) in
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
  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))

661
(** Typing declarations, that is building environments. *)
662
663
664

open Ptree

665
let add_types dl th =
666
  let def = List.fold_left
667
    (fun def d ->
668
      let id = d.td_ident.id in
669
      if Mstr.mem id def then error ~loc:d.td_loc (Clash id);
670
671
      Mstr.add id d def)
    Mstr.empty dl
672
  in
673
  let tysymbols = Hashtbl.create 17 in
674
  let rec visit x =
675
676
677
678
679
680
    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
681
      let d = Mstr.find x def in
682
683
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
684
685
686
687
      let vl =
	List.map
	  (fun v ->
	     if Hashtbl.mem vars v.id then
688
	       error ~loc:v.id_loc (DuplicateTypeVar v.id);
689
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
690
691
	     Hashtbl.add vars v.id i;
	     i)
692
	  d.td_params
693
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
694
      let id = id_user id d.td_loc in
695
      let ts = match d.td_def with
696
	| TDalias ty ->
697
	    let rec apply = function
698
699
	      | PPTtyvar v ->
		  begin
700
701
702
703
704
		    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
705
		    | Qident x when Mstr.mem x.id def ->
706
707
708
709
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
710
		  begin try
711
		    ty_app ts (List.map apply tyl)
712
		  with Ty.BadTypeArity (_, tsal, tyll) ->
713
		    error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
714
715
716
717
		  end
	      | PPTtuple tyl ->
		  let ts = ts_tuple (List.length tyl) in
		  ty_app ts (List.map apply tyl)
718
719
	    in
	    create_tysymbol id vl (Some (apply ty))
720
	| TDabstract | TDalgebraic _ ->
721
722
723
724
725
	    create_tysymbol id vl None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
726
  let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in
727
  let th' = try add_ty_decl th tsl
728
    with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (Clash s)
729
  in
730
  let csymbols = Hashtbl.create 17 in
731
  let decl d =
732
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
733
      | None ->
734
	  assert false
735
      | Some ts ->
736
737
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
738
739
	  List.iter
	    (fun v ->
740
	       Hashtbl.add vars v.tv_name.id_string
741
                  (create_ty_decl_var ~user:true v))
742
743
744
745
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
746
      | TDabstract | TDalias _ ->
747
	  Tabstract
748
      | TDalgebraic cl ->
749
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
750
	  let constructor (loc, id, pl) =
751
	    let param (_,t) = ty_of_dty (dty th' t) in
752
	    let tyl = List.map param pl in
753
	    Hashtbl.replace csymbols id.id loc;
754
	    create_fsymbol (id_user id.id loc) tyl ty
755
756
757
758
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
759
  in
760
761
762
763
  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
764

Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
765
let env_of_vsymbol_list vl =
766
  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
767

768
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
769
770
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
771
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
772
  (* 1. create all symbols and make an environment with these symbols *)
773
  let create_symbol th d =
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
774
    let id = d.ld_ident.id in
Andrei Paskevich's avatar
Andrei Paskevich committed
775
    let v = id_user id d.ld_loc in
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
776
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
777
    Hashtbl.add denvs id denv;
778
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
779
    let pl = List.map type_ty d.ld_params in
780
    try match d.ld_type with
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
781
782
783
      | None -> (* predicate *)
	  let ps = create_psymbol v pl in
	  Hashtbl.add psymbols id ps;
784
	  add_logic_decl th [ps, None]
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
785
786
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
787
	  let fs = create_fsymbol v pl t in
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
788
	  Hashtbl.add fsymbols id fs;
789
	  add_logic_decl th [fs, None]
790
    with ClashSymbol s -> error ~loc:d.ld_loc (Clash s)
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
791
792
793
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
794
  let type_decl d =
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
795
796
797
    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
798
      | 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
799
    in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
800
    let denv = Hashtbl.find denvs id in
801
    let denv = { denv with uc = th' } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
802
    let denv = List.fold_left dadd_var denv d.ld_params in
803
804
    let create_var (x, _) ty =
      let id = match x with
805
806
	| 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
807
808
809
      in
      create_vsymbol id ty
    in
810
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
811
812
813
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
814
815
        begin match d.ld_def with
	  | None -> ps,None
816
	  | Some f ->
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
817
	      let f = dfmla denv f in
818
819
820
821
              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
822
	      let env = env_of_vsymbol_list vl in
823
824
              make_ps_defn ps vl (fmla env f)
        end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
825
    | Some ty -> (* function *)
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
826
	let fs = Hashtbl.find fsymbols id in
827
828
        begin match d.ld_def with
	  | None -> fs,None
829
	  | Some t ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
830
	      let loc = t.pp_loc in
831
	      let ty = dty denv ty in
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
832
	      let t = dterm denv t in
833
	      if not (unify t.dt_ty ty) then
834
		term_expected_type ~loc t.dt_ty ty;
835
836
837
838
              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
839
	      let env = env_of_vsymbol_list vl in
840
	      make_fs_defn fs vl (term env t)
841
        end
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
842
  in
843
  add_logic_decls th (List.map type_decl dl)
844

845
let type_term denv env t =
846
  let t = dterm denv t in
847
  term env t
848

849
let term uc = type_term (create_denv uc) Mstr.empty
850

851
let type_fmla denv env f =
Jean-Christophe Filliâtre's avatar
logic