typing.ml 30.4 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) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short 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
(** Environments *)

117
(** typing using destructive type variables
118

119
120
121
122
123
124
    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
125

126
127
*)

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

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

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

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

159
160
161
162
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 }

163
164
165
166
167
168
169
170
171
172
173
174
(* 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
175
  let ts =
176
177
178
179
180
181
182
183
184
185
    try ns_find_ts (get_namespace uc) sl
    with Not_found -> error ~loc (UnboundType sl)
  in
  ts, specialize_tysymbol ~loc ts

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

let rec dty env = function
186
  | PPTtyvar {id=x} ->
187
188
189
190
191
192
193
194
195
      Tyvar (find_user_type_var x env)
  | PPTtyapp (p, x) ->
      let loc = qloc x in
      let ts, tv = specialize_tysymbol loc x env.uc in
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
      let tyl = List.map (dty env) p in
      match ts.ts_def with
196
	| None ->
197
	    Tyapp (ts, tyl)
198
	| Some ty ->
199
200
201
202
203
204
205
	    let add m v t = Mtv.add v t m in
            let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
	    type_inst s ty

let find_ns find p ns =
  let loc = qloc p in
  let sl = string_list_of_qualid [] p in
206
  try find ns sl
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
  with Not_found -> error ~loc (UnboundSymbol sl)

let find_prop_ns = find_ns ns_find_prop
let find_prop p uc = find_prop_ns p (get_namespace uc)

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

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

let specialize_lsymbol p uc =
  let s = find_lsymbol p uc in
  s, specialize_lsymbol (qloc p) s

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

228
let specialize_psymbol p uc =
229
  let s, (tl, ty) = specialize_lsymbol p uc in
230
231
  match ty with
    | None -> s, tl
232
233
234
235
236
    | 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
237

238

239
240
(** Typing types *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
241
242
243
244
let split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

245
(** Typing terms and formulas *)
246

Andrei Paskevich's avatar
Andrei Paskevich committed
247
248
249
250
251
252
253
254
type dpattern = { dp_node : dpattern_node; dp_ty : dty }

and dpattern_node =
  | Pwild
  | Pvar of string
  | Papp of lsymbol * dpattern list
  | Pas of dpattern * string

255
256
type uquant = string list * dty

257
258
259
type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
260
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
261
  | Tconst of constant
262
  | Tapp of lsymbol * dterm list
263
  | Tlet of dterm * string * dterm
264
  | Tmatch of dterm list * (dpattern list * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265
  | Tnamed of string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
266
  | Teps of string * dty * dfmla
267

268
and dfmla =
269
  | Fapp of lsymbol * dterm list
270
  | Fquant of quant * uquant list * dtrigger list list * dfmla
271
272
273
274
275
  | Fbinop of binop * dfmla * dfmla
  | Fnot of dfmla
  | Ftrue
  | Ffalse
  | Fif of dfmla * dfmla * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
276
  | Flet of dterm * string * dfmla
277
  | Fmatch of dterm list * (dpattern list * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
278
  | Fnamed of string * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
279
  | Fvar of fmla
280

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
306
307
308
309
310
let rec dpat env pat =
  let env, n, ty = dpat_node pat.pat_loc env pat.pat_desc in
  env, { dp_node = n; dp_ty = ty }

and dpat_node loc env = function
311
  | PPpwild ->
Andrei Paskevich's avatar
Andrei Paskevich committed
312
      let tv = create_tvsymbol (id_user "a" loc) in
313
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
314
315
316
      env, Pwild, ty
  | PPpvar {id=x} ->
      let tv = create_tvsymbol (id_user "a" loc) in
317
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
318
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
319
320
      env, Pvar x, ty
  | PPpapp (x, pl) ->
321
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
322
323
324
325
      let env, pl = dpat_args s.ls_name loc env tyl pl in
      env, Papp (s, pl), ty
  | PPpas (p, {id=x}) ->
      let env, p = dpat env p in
Andrei Paskevich's avatar
Andrei Paskevich committed
326
      let env = { env with dvars = Mstr.add x p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
327
328
      env, Pas (p,x), p.dp_ty

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

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

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

359
let rec dterm env t =
360
361
362
363
  let n, ty = dterm_node t.pp_loc env t.pp_desc in
  { dt_node = n; dt_ty = ty }

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

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

496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
and dpat_list env tl pl =
  check_pat_linearity pl;
  let pattern (env,pl) pat t =
    let loc = pat.pat_loc in
    let env, pat = dpat env pat in
    if not (unify pat.dp_ty t.dt_ty)
      then term_expected_type ~loc pat.dp_ty t.dt_ty;
    env, pat::pl
  in
  let loc = (List.hd pl).pat_loc in
  let env, pl = try List.fold_left2 pattern (env,[]) pl tl
    with Invalid_argument _ -> errorm ~loc
      "This pattern has length %d but is expected to have length %d"
      (List.length pl) (List.length tl)
  in
  env, List.rev pl

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

529
let rec pattern env p =
Andrei Paskevich's avatar
Andrei Paskevich committed
530
531
532
  let ty = ty_of_dty p.dp_ty in
  match p.dp_node with
  | Pwild -> env, pat_wild ty
533
  | Pvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
534
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
535
      Mstr.add x v env, pat_var v
536
  | Papp (s, pl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
537
538
539
540
      let env, pl = map_fold_left pattern env pl in
      env, pat_app s pl ty
  | Pas (p, x) ->
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
541
      let env, p = pattern (Mstr.add x v env) p in
Andrei Paskevich's avatar
Andrei Paskevich committed
542
543
      env, pat_as p v

544
545
let rec term env t = match t.dt_node with
  | Tvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
546
547
      assert (Mstr.mem x env);
      t_var (Mstr.find x env)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
548
  | Tconst c ->
549
      t_const c (ty_of_dty t.dt_ty)
550
  | Tapp (s, tl) ->
551
      t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
552
553
  | Tlet (e1, x, e2) ->
      let ty = ty_of_dty e1.dt_ty in
554
      let e1 = term env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
555
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
556
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
557
558
      let e2 = term env e2 in
      t_let v e1 e2
559
560
561
562
  | Tmatch (tl, bl) ->
      let branch (pl,e) =
        let env, pl = map_fold_left pattern env pl in
        (pl, term env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
563
564
565
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).t_ty in
566
      t_case (List.map (term env) tl) bl ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
567
568
569
  | Tnamed (x, e1) ->
      let e1 = term env e1 in
      t_label_add x e1
Andrei Paskevich's avatar
Andrei Paskevich committed
570
571
572
573
574
575
  | Teps (x, ty, e1) ->
      let ty = ty_of_dty ty in
      let v = create_vsymbol (id_fresh x) ty in
      let env = Mstr.add x v env in
      let e1 = fmla env e1 in
      t_eps v e1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
576

577
578
579
580
and fmla env = function
  | Ftrue ->
      f_true
  | Ffalse ->
581
      f_false
582
583
584
585
586
587
  | Fnot f ->
      f_not (fmla env f)
  | Fbinop (op, f1, f2) ->
      f_binary op (fmla env f1) (fmla env f2)
  | Fif (f1, f2, f3) ->
      f_if (fmla env f1) (fmla env f2) (fmla env f3)
588
  | Fquant (q, uqu, trl, f1) ->
589
      (* TODO: shouldn't we localize this ident? *)
590
591
592
      let uquant env (xl,ty) =
        let ty = ty_of_dty ty in
        map_fold_left
593
594
595
          (fun env x ->
             let v = create_vsymbol (id_fresh x) ty in Mstr.add x v env, v)
          env xl
596
      in
597
      let env, vl = map_fold_left uquant env uqu in
598
      let trigger = function
599
600
	| TRterm t -> Term (term env t)
	| TRfmla f -> Fmla (fmla env f)
601
602
603
      in
      let trl = List.map (List.map trigger) trl in
      f_quant q (List.concat vl) trl (fmla env f1)
604
605
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
606
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
607
      let ty = ty_of_dty e1.dt_ty in
608
      let e1 = term env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
609
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
610
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
611
612
      let f2 = fmla env f2 in
      f_let v e1 f2
613
614
615
616
  | Fmatch (tl, bl) ->
      let branch (pl,e) =
        let env, pl = map_fold_left pattern env pl in
        (pl, fmla env e)
Andrei Paskevich's avatar
Andrei Paskevich committed
617
      in
618
      f_case (List.map (term env) tl) (List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
619
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
620
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
621
      f_label_add x f1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
622
623
  | Fvar f ->
      f
624

625
(** Typing declarations, that is building environments. *)
626
627
628

open Ptree

629
let add_types dl th =
630
631
632
633
634
635
  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 
636
  in
637
  let tysymbols = Hashtbl.create 17 in
638
  let rec visit x =
639
640
641
642
643
644
    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
645
      let d = Mstr.find x def in
646
647
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
648
649
650
651
      let vl =
	List.map
	  (fun v ->
	     if Hashtbl.mem vars v.id then
652
	       error ~loc:v.id_loc (DuplicateTypeVar v.id);
653
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
654
655
	     Hashtbl.add vars v.id i;
	     i)
656
	  d.td_params
657
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
658
      let id = id_user id d.td_loc in
659
      let ts = match d.td_def with
660
	| TDalias ty ->
661
	    let rec apply = function
662
663
	      | PPTtyvar v ->
		  begin
664
665
666
667
668
		    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
669
		    | Qident x when Mstr.mem x.id def ->
670
671
672
673
674
675
			visit x.id
		    | Qident _ | Qdot _ ->
			find_tysymbol q th
		  in
		  try
		    ty_app ts (List.map apply tyl)
676
677
		  with Ty.BadTypeArity (tsal, tyll) ->
		    error ~loc:(qloc q) (TypeArity (q, tsal, tyll))
678
679
	    in
	    create_tysymbol id vl (Some (apply ty))
680
	| TDabstract | TDalgebraic _ ->
681
682
683
684
685
	    create_tysymbol id vl None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
686
  let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in 
687
  let th' = try add_ty_decl th tsl
688
    with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (Clash s)
689
  in
690
  let csymbols = Hashtbl.create 17 in
691
  let decl d =
692
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
693
      | None ->
694
	  assert false
695
      | Some ts ->
696
697
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
698
699
700
701
	  List.iter
	    (fun v ->
	       Hashtbl.add vars v.tv_name.id_short
                  (create_ty_decl_var ~user:true v))
702
703
704
705
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
706
      | TDabstract | TDalias _ ->
707
	  Tabstract
708
      | TDalgebraic cl ->
709
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
710
	  let constructor (loc, id, pl) =
711
712
	    let param (_, t) = ty_of_dty (dty th' t) in
	    let tyl = List.map param pl in
713
	    Hashtbl.replace csymbols id.id loc;
714
	    create_fsymbol (id_user id.id loc) tyl ty
715
716
717
718
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
719
  in
720
  try add_ty_decls th (List.map decl dl)
721
  with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
722

Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
723
let env_of_vsymbol_list vl =
Andrei Paskevich's avatar
Andrei Paskevich committed
724
  List.fold_left (fun env v -> Mstr.add v.vs_name.id_short v env) Mstr.empty vl
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
725

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

803
let type_term denv env t =
804
  let t = dterm denv t in
805
  term env t
806

807
let term uc = type_term (create_denv uc) Mstr.empty
808

809
let type_fmla denv env f =
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
810
  let f = dfmla denv f in
811
  fmla env f
Jean-Christophe Filliâtre's avatar
logic    
Jean-Christophe Filliâtre committed
812

813
let fmla uc = type_fmla (create_denv uc) Mstr.empty
814

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
815
let add_prop k loc s f th =
816
817
  let pr = create_prsymbol (id_user s.id loc) in
  try add_prop_decl th k pr (fmla th f)
818
  with ClashSymbol s -> error ~loc (Clash s)
819

Andrei Paskevich's avatar
Andrei Paskevich committed
820
821
822
let loc_of_id id = match id.id_origin with
  | User loc -> loc
  | _ -> assert false
823

824
825
let add_inductives dl th =
  (* 1. create all symbols and make an environment with these symbols *)
826
  let psymbols = Hashtbl.create 17 in
827
  let create_symbol th d =
828
    let id = d.in_ident.id in
Andrei Paskevich's avatar
Andrei Paskevich committed
829
    let v = id_user id d.in_loc in
830
831
832
833
834
    let denv = create_denv th in
    let type_ty t = ty_of_dty (dty denv t) in
    let pl = List.map type_ty d.in_params in
    let ps = create_psymbol v pl in
    Hashtbl.add psymbols id ps;
835
    try add_logic_decl th [ps, None]
836
    with ClashSymbol s -> error ~loc:d.in_loc (Clash s)
837
  in
838
839
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
840
  let propsyms = Hashtbl.create 17 in
841
  let type_decl d =
842
843
    let id = d.in_ident.id in
    let ps = Hashtbl.find psymbols id in
844
    let clause (loc, id, f) =
845
846
      Hashtbl.replace propsyms id.id loc;
      create_prsymbol (id_user id.id loc), fmla th' f
847
848
849
    in
    ps, List.map clause d.in_def
  in
850
  try add_ind_decls th (List.map type_decl dl)
Andrei Paskevich's avatar
Andrei Paskevich committed
851
  with
852
  | ClashSymbol s -> error ~loc:(Hashtbl.find propsyms s) (Clash s)
853
  | InvalidIndDecl (_,pr) -> errorm ~loc:(loc_of_id pr.pr_name)
Andrei Paskevich's avatar
Andrei Paskevich committed
854
      "not a clausal form"
855
  | NonPositiveIndDecl (_,pr,s) -> errorm ~loc:(loc_of_id pr.pr_name)
Andrei Paskevich's avatar
Andrei Paskevich committed