Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

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

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

32 33
(** errors *)

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

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
63 64 65
let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
66 67
  Format.kfprintf
    (fun _ ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
68 69 70 71 72 73
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
       error ?loc (AnyMessage s))
    fmt f

74
let rec print_qualid fmt = function
75
  | Qident s -> fprintf fmt "%s" s.id
76
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
77

78
let report fmt = function
79 80
  | Message s ->
      fprintf fmt "%s" s
81 82
  | ClashType s ->
      fprintf fmt "clash with previous type %s" s
83
  | DuplicateTypeVar s ->
84
      fprintf fmt "duplicate type parameter %s" s
85
  | TypeArity (id, a, n) ->
86
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
87 88
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
89
      fprintf fmt "Clash with previous symbol %s" id
90 91 92 93
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
94
  | BadNumberOfArguments (s, n, m) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
95
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short n;
96
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
97 98
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
99 100
  | ClashNamespace s ->
      fprintf fmt "clash with previous namespace %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
101 102
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
103 104
  | AlreadyTheory s ->
      fprintf fmt "already using a theory with name %s" s
105 106 107 108 109 110 111 112
  | 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
113 114 115 116
  | CyclicTypeDef ->
      fprintf fmt "cyclic type definition"
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
117 118 119 120
  | 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
121 122
  | AnyMessage s ->
      fprintf fmt "%s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
123

124 125
(** Environments *)

126
(** typing using destructive type variables
127

128 129 130 131 132 133
    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
134

135 136
*)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
137 138 139 140 141
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

142 143 144 145
(** Destructive typing environment, that is
    environment + local variables.
    It is only local to this module and created with [create_denv] below. *)

146
type denv = {
147 148 149 150 151
  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 *)
}

152 153 154
let create_denv uc = {
  uc = uc;
  utyvars = Hashtbl.create 17;
155 156 157 158 159 160 161 162 163 164 165 166
  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
167

168 169 170 171 172 173 174 175 176 177 178 179
(* parsed types -> intermediate types *)

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

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

let specialize_tysymbol loc p uc =
  let sl = string_list_of_qualid [] p in
180
  let ts =
181 182 183 184 185 186 187 188 189 190
    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
191
  | PPTtyvar {id=x} ->
192 193 194 195 196 197 198 199 200
      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
201
	| None ->
202
	    Tyapp (ts, tyl)
203
	| Some ty ->
204 205 206 207 208 209 210
	    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
211
  try find ns sl
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
  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

227
let specialize_fsymbol p uc =
228 229
  let loc = qloc p in
  let s, (tl, ty) = specialize_lsymbol p uc in
230 231 232
  match ty with
    | None -> error ~loc TermExpected
    | Some ty -> s, tl, ty
233

234
let specialize_psymbol p uc =
235 236
  let loc = qloc p in
  let s, (tl, ty) = specialize_lsymbol p uc in
237 238 239
  match ty with
    | None -> s, tl
    | Some _ -> error ~loc PredicateExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
240

241

242 243
(** Typing types *)

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

248
(** Typing terms and formulas *)
249

Andrei Paskevich's avatar
Andrei Paskevich committed
250 251 252 253 254 255 256 257
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

258 259
type uquant = string list * dty

260 261 262
type dterm = { dt_node : dterm_node; dt_ty : dty }

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

271
and dfmla =
272
  | Fapp of lsymbol * dterm list
273
  | Fquant of quant * uquant list * dtrigger list list * dfmla
274 275 276 277 278
  | 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
279
  | Flet of dterm * string * dfmla
280
  | Fmatch of dterm list * (dpattern list * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
281
  | Fnamed of string * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
282
  | Fvar of fmla
283

284 285 286 287
and dtrigger =
  | TRterm of dterm
  | TRfmla of dfmla

288 289 290 291 292 293
let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

294
let check_pat_linearity pl =
Andrei Paskevich's avatar
Andrei Paskevich committed
295
  let s = ref Sstr.empty in
296
  let add id =
297
    if Sstr.mem id.id !s then
298
      errorm ~loc:id.id_loc "duplicate variable %s" id.id;
Andrei Paskevich's avatar
Andrei Paskevich committed
299
    s := Sstr.add id.id !s
300 301 302 303 304 305 306
  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
307
  List.iter check pl
308

Andrei Paskevich's avatar
Andrei Paskevich committed
309 310 311 312 313
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
314
  | PPpwild ->
Andrei Paskevich's avatar
Andrei Paskevich committed
315
      let tv = create_tvsymbol (id_user "a" loc) in
316
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
317 318 319
      env, Pwild, ty
  | PPpvar {id=x} ->
      let tv = create_tvsymbol (id_user "a" loc) in
320
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
321
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
322 323
      env, Pvar x, ty
  | PPpapp (x, pl) ->
324
      let s, tyl, ty = specialize_fsymbol x env.uc in
Andrei Paskevich's avatar
Andrei Paskevich committed
325 326 327 328
      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
329
      let env = { env with dvars = Mstr.add x p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
330 331
      env, Pas (p,x), p.dp_ty

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

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

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

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

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

485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501
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

502 503 504 505
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
506
    | [], [] ->
507 508 509 510
	[]
    | 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
511
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
512 513 514 515 516 517
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

518
let rec pattern env p =
Andrei Paskevich's avatar
Andrei Paskevich committed
519 520 521
  let ty = ty_of_dty p.dp_ty in
  match p.dp_node with
  | Pwild -> env, pat_wild ty
522
  | Pvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
523
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
524
      Mstr.add x v env, pat_var v
525
  | Papp (s, pl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
526 527 528 529
      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
530
      let env, p = pattern (Mstr.add x v env) p in
Andrei Paskevich's avatar
Andrei Paskevich committed
531 532
      env, pat_as p v

533 534
let rec term env t = match t.dt_node with
  | Tvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
535 536
      assert (Mstr.mem x env);
      t_var (Mstr.find x env)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
537
  | Tconst c ->
538
      t_const c (ty_of_dty t.dt_ty)
539
  | Tapp (s, tl) ->
540
      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
541 542
  | Tlet (e1, x, e2) ->
      let ty = ty_of_dty e1.dt_ty in
543
      let e1 = term env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
544
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
545
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
546 547
      let e2 = term env e2 in
      t_let v e1 e2
548 549 550 551
  | 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
552 553 554
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).t_ty in
555
      t_case (List.map (term env) tl) bl ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
556 557 558
  | Tnamed (x, e1) ->
      let e1 = term env e1 in
      t_label_add x e1
Andrei Paskevich's avatar
Andrei Paskevich committed
559 560 561 562 563 564
  | 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
565

566 567 568 569
and fmla env = function
  | Ftrue ->
      f_true
  | Ffalse ->
570
      f_false
571 572 573 574 575 576
  | 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)
577
  | Fquant (q, uqu, trl, f1) ->
578
      (* TODO: shouldn't we localize this ident? *)
579 580 581
      let uquant env (xl,ty) =
        let ty = ty_of_dty ty in
        map_fold_left
582 583 584
          (fun env x ->
             let v = create_vsymbol (id_fresh x) ty in Mstr.add x v env, v)
          env xl
585
      in
586
      let env, vl = map_fold_left uquant env uqu in
587
      let trigger = function
588 589
	| TRterm t -> Term (term env t)
	| TRfmla f -> Fmla (fmla env f)
590 591 592
      in
      let trl = List.map (List.map trigger) trl in
      f_quant q (List.concat vl) trl (fmla env f1)
593 594
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
595
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
596
      let ty = ty_of_dty e1.dt_ty in
597
      let e1 = term env e1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
598
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
599
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
600 601
      let f2 = fmla env f2 in
      f_let v e1 f2
602 603 604 605
  | 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
606
      in
607
      f_case (List.map (term env) tl) (List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
608
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
609
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
610
      f_label_add x f1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
611 612
  | Fvar f ->
      f
613

614
(** Typing declarations, that is building environments. *)
615 616 617

open Ptree

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

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
716
let env_of_vsymbol_list vl =
Andrei Paskevich's avatar
Andrei Paskevich committed
717
  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
718

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