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

20 21
open Util
open Format
22
open Pp
23
open Ident
24
open Ty
25
open Term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26
open Ptree
27
open Theory
28

Andrei Paskevich's avatar
Andrei Paskevich committed
29 30
open Theory

31 32 33
(** errors *)

type error = 
34
  | Message of string
35
  | ClashType of string
36
  | DuplicateTypeVar of string
37
  | UnboundType of string
38
  | TypeArity of qualid * int * int
39
  | Clash of string
40 41
  | PredicateExpected
  | TermExpected
42
  | UnboundSymbol of string
43
  | BadNumberOfArguments of Ident.ident * int * int 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
44
  | ClashTheory of string
45
  | ClashNamespace of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
46
  | UnboundTheory of qualid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
47
  | AlreadyTheory of string
48
  | UnboundNamespace of string
49 50 51 52
  | UnboundFile of string
  | UnboundDir of string
  | AmbiguousPath of string * string
  | NotInLoadpath of string
53 54
  | CyclicTypeDef
  | UnboundTypeVar of string
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 66 67 68 69 70 71 72 73
let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
  Format.kfprintf 
    (fun _ -> 
       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
  | UnboundType s ->
86
       fprintf fmt "Unbound type '%s'" s
87
  | TypeArity (id, a, n) ->
88
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
89 90
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91
      fprintf fmt "Clash with previous symbol %s" id
92 93 94 95
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
96
  | UnboundSymbol s ->
97
       fprintf fmt "Unbound symbol '%s'" s
98
  | BadNumberOfArguments (s, n, m) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
99
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short n;
100
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
101 102
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
103 104
  | ClashNamespace s ->
      fprintf fmt "clash with previous namespace %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105 106
  | UnboundTheory q ->
      fprintf fmt "unbound theory %a" print_qualid q
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107 108
  | AlreadyTheory s ->
      fprintf fmt "already using a theory with name %s" s
109 110
  | UnboundNamespace s ->
      fprintf fmt "unbound namespace %s" s
111 112 113 114 115 116 117 118
  | 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
119 120 121 122
  | CyclicTypeDef ->
      fprintf fmt "cyclic type definition"
  | UnboundTypeVar s ->
      fprintf fmt "unbound type variable '%s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
123 124
  | AnyMessage s ->
      fprintf fmt "%s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
125

126 127
(** Environments *)

128
module S = Set.Make(String)
129 130 131 132
module M = Map.Make(String)

type env = {
  loadpath : string list;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
133
  loaded_theories : (string list, theory M.t) Hashtbl.t;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
134
  theories : theory M.t; (* local theories *)
135 136 137 138
}

let create lp = {
  loadpath = lp;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139
  loaded_theories = Hashtbl.create 17;
140 141
  theories = M.empty;
}
142 143

(** typing using destructive type variables 
144

145 146 147 148 149 150
    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
151

152 153 154 155 156 157 158 159 160 161 162 163 164
*)

(** types with destructive type variables *)

type dty =
  | Tyvar of type_var
  | Tyapp of tysymbol * dty list
      
and type_var = { 
  tag : int; 
  user : bool;
  tvsymbol : tvsymbol;
  mutable type_val : dty option;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
165
  type_var_loc : loc option;
166
}
167

168 169 170 171
let rec print_dty fmt = function
  | Tyvar { type_val = Some t } ->
      print_dty fmt t
  | Tyvar { type_val = None; tvsymbol = v } ->
172
      fprintf fmt "'%s" v.id_short
173
  | Tyapp (s, []) ->
174
      fprintf fmt "%s" s.ts_name.id_short
175
  | Tyapp (s, [t]) -> 
176
      fprintf fmt "%a %s" print_dty t s.ts_name.id_short
177
  | Tyapp (s, l) -> 
178 179
      fprintf fmt "(%a) %s" 
	(print_list comma print_dty) l s.ts_name.id_short
180

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181 182 183 184 185
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

186
let create_ty_decl_var =
187
  let t = ref 0 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
188
  fun ?loc ~user tv -> 
189
    incr t; 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
190 191
    { tag = !t; user = user; tvsymbol = tv; type_val = None;
      type_var_loc = loc }
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219

let rec occurs v = function
  | Tyvar { type_val = Some t } -> occurs v t
  | Tyvar { tag = t; type_val = None } -> v.tag = t
  | Tyapp (_, l) -> List.exists (occurs v) l

(* destructive type unification *)
let rec unify t1 t2 = match t1, t2 with
  | Tyvar { type_val = Some t1 }, _ ->
      unify t1 t2
  | _, Tyvar { type_val = Some t2 } ->
      unify t1 t2
  | Tyvar v1, Tyvar v2 when v1.tag = v2.tag ->
      true
	(* instantiable variables *)
  | Tyvar ({user=false} as v), t
  | t, Tyvar ({user=false} as v) ->
      not (occurs v t) && (v.type_val <- Some t; true)
	(* recursive types *)
  | Tyapp (s1, l1), Tyapp (s2, l2) ->
      s1 == s2 && List.length l1 = List.length l2 &&
	  List.for_all2 unify l1 l2
  | Tyapp _, _ | _, Tyapp _ ->
      false
	(* other cases *)
  | Tyvar {user=true; tag=t1}, Tyvar {user=true; tag=t2} -> 
      t1 = t2

220
(** Destructive typing environment, that is
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
221
    environment + local variables.
222
    It is only local to this module and created with [create_denv] below. *)
223 224

type denv = { 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225
  th : theory_uc; (* the theory under construction *)
226 227
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
  dvars : dty M.t; (* local variables, to be bound later *)
228 229
}

230 231
let create_denv th = { 
  th = th; 
232 233 234
  utyvars = Hashtbl.create 17; 
  dvars = M.empty;
}
235

236 237 238 239
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
240
    (* TODO: shouldn't we localize this ident? *)
241
    let v = create_tvsymbol (id_fresh x) in
242
    let v = create_ty_decl_var ~user:true v in
243 244 245
    Hashtbl.add env.utyvars x v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
246 247
(* Specialize *)

248
module Htv = Hid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
249

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
250
let find_type_var ~loc env tv =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
251 252 253
  try
    Htv.find env tv
  with Not_found ->
254
    let v = create_ty_decl_var ~loc ~user:false tv in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
255 256 257
    Htv.add env tv v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
258
let rec specialize ~loc env t = match t.ty_node with
259
  | Ty.Tyvar tv -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
260
      Tyvar (find_type_var ~loc env tv)
261
  | Ty.Tyapp (s, tl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
262
      Tyapp (s, List.map (specialize ~loc env) tl)
263

264 265 266
(** generic find function using a path *)

let find_local_namespace {id=x; id_loc=loc} ns = 
267
  try Mnm.find x ns.ns_ns
268 269 270 271 272 273 274 275 276 277 278 279
  with Not_found -> error ~loc (UnboundNamespace x)

let rec find_namespace q ns = match q with
  | Qident t -> find_local_namespace t ns
  | Qdot (q, t) -> let ns = find_namespace q ns in find_local_namespace t ns

let rec find f q ns = match q with
  | Qident x -> f x ns
  | Qdot (m, x) -> let ns = find_namespace m ns in f x ns

(** specific find functions using a path *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
280
let find_local_tysymbol {id=x; id_loc=loc} ns = 
281
  try Mnm.find x ns.ns_ts
282 283
  with Not_found -> error ~loc (UnboundType x)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284 285 286
let find_tysymbol_ns p ns =
  find find_local_tysymbol p ns

287
let find_tysymbol p th = 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
288
  find_tysymbol_ns p (get_namespace th)
289

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
290
let specialize_tysymbol ~loc x env =
291
  let s = find_tysymbol x env.th in
292
  let env = Htv.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
293
  s, List.map (find_type_var ~loc env) s.ts_args
294
	
295 296
let find_lsymbol {id=x; id_loc=loc} ns = 
  try Mnm.find x ns.ns_ls
297 298
  with Not_found -> error ~loc (UnboundSymbol x)

299 300
let find_lsymbol_ns p ns = 
  find find_lsymbol p ns
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
301

302 303
let find_lsymbol p th = 
  find_lsymbol_ns p (get_namespace th)
304

305
let find_prop {id=x; id_loc=loc} ns = 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
306 307 308
  try Mnm.find x ns.ns_pr
  with Not_found -> errorm ~loc "unbound formula %s" x

309 310 311
let find_prop_ns p ns =
  find find_prop p ns

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
312
let find_prop p th =
313
  find_prop_ns p (get_namespace th)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
314

315 316 317
let specialize_lsymbol ~loc s =
  let tl = s.ls_args in
  let t = s.ls_value in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
318
  let env = Htv.create 17 in
319
  s, List.map (specialize ~loc env) tl, option_map (specialize ~loc env) t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
320

321 322 323 324 325
let specialize_fsymbol ~loc s = 
  let s, tl, ty = specialize_lsymbol ~loc s in
  match ty with
    | None -> error ~loc TermExpected
    | Some ty -> s, tl, ty
326

327 328 329 330 331
let specialize_psymbol ~loc s = 
  let s, tl, ty = specialize_lsymbol ~loc s in
  match ty with
    | None -> s, tl
    | Some _ -> error ~loc PredicateExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
332

333 334
(** Typing types *)

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
339 340 341 342 343 344 345 346
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 split_qualid = function
  | Qident id -> [], id.id
  | Qdot (p, id) -> string_list_of_qualid [] p, id.id

347
(* parsed types -> intermediate types *)
348 349 350 351 352

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

353
let rec dty env = function
354
  | PPTtyvar {id=x} -> 
355
      Tyvar (find_user_type_var x env)
356
  | PPTtyapp (p, x) ->
357
      let loc = qloc x in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
358
      let ts, tv = specialize_tysymbol ~loc x env in
359 360 361
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
362 363 364 365 366 367 368 369
      let tyl = List.map (dty env) p in
      match ts.ts_def with
	| None -> 
	    Tyapp (ts, tyl)
	| Some ty -> 
	    let add m v t = Mid.add v t m in
            let s = List.fold_left2 add Mid.empty ts.ts_args tyl in
	    type_inst s ty
370 371

(* intermediate types -> types *)
372
let rec ty_of_dty = function
373
  | Tyvar { type_val = Some t } ->
374
      ty_of_dty t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
375 376
  | Tyvar { type_val = None; user = false; type_var_loc = loc } ->
      errorm ?loc "undefined type variable"
377 378 379
  | Tyvar { tvsymbol = tv } ->
      Ty.ty_var tv
  | Tyapp (s, tl) ->
380
      Ty.ty_app s (List.map ty_of_dty tl)
381

382
(** Typing terms and formulas *)
383

Andrei Paskevich's avatar
Andrei Paskevich committed
384 385 386 387 388 389 390 391
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

392 393
type uquant = string list * dty

394 395 396
type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
397
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
398
  | Tconst of constant
399
  | Tapp of lsymbol * dterm list
400
  | Tlet of dterm * string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
401
  | Tmatch of dterm * (dpattern * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
402
  | Tnamed of string * dterm
403 404 405
  | Teps of string * dfmla

and dfmla = 
406
  | Fapp of lsymbol * dterm list
407
  | Fquant of quant * uquant list * dtrigger list list * dfmla
408 409 410 411 412
  | 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
413
  | Flet of dterm * string * dfmla
Andrei Paskevich's avatar
Andrei Paskevich committed
414
  | Fmatch of dterm * (dpattern * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
415
  | Fnamed of string * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
416
  | Fvar of fmla
417

418 419 420 421
and dtrigger =
  | TRterm of dterm
  | TRfmla of dfmla

422 423 424 425 426 427
let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

428 429 430 431 432 433 434 435 436 437 438 439 440 441
let check_pat_linearity pat =
  let s = ref S.empty in
  let add id =
    if S.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := S.add id.id !s
  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
  check pat

Andrei Paskevich's avatar
Andrei Paskevich committed
442 443 444 445 446 447 448
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
  | PPpwild -> 
      let tv = create_tvsymbol (id_user "a" loc) in
449
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
450 451 452
      env, Pwild, ty
  | PPpvar {id=x} ->
      let tv = create_tvsymbol (id_user "a" loc) in
453
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
454 455 456 457 458 459 460 461 462 463 464 465
      let env = { env with dvars = M.add x ty env.dvars } in
      env, Pvar x, ty
  | PPpapp (x, pl) ->
      let s = find_lsymbol x env.th in
      let s, tyl, ty = specialize_fsymbol ~loc s in
      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
      let env = { env with dvars = M.add x p.dp_ty env.dvars } in
      env, Pas (p,x), p.dp_ty

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
466 467
and dpat_args s loc env el pl = 
  let n = List.length el and m = List.length pl in
Andrei Paskevich's avatar
Andrei Paskevich committed
468
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
469
  let rec check_arg env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
470
    | [], [] -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
471 472 473 474 475 476 477
	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
478 479 480
    | _ ->
	assert false
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
481
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
482

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
483
let rec trigger_not_a_term_exn = function
484
  | Error TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
485 486 487
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

488
let check_quant_linearity uqu =
489 490 491 492 493 494 495
  let s = ref S.empty in
  let check id = 
    if S.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := S.add id.id !s
  in
  List.iter (fun (idl, _) -> List.iter check idl) uqu

496 497 498 499 500
let rec dterm env t = 
  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
501 502 503 504 505 506
  | PPvar (Qident {id=x}) when M.mem x env.dvars ->
      (* local variable *)
      let ty = M.find x env.dvars in
      Tvar x, ty
  | PPvar x -> 
      (* 0-arity symbol (constant) *)
507
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
508
      let s, tyl, ty = specialize_fsymbol ~loc s in
509
      let n = List.length tyl in
510
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
511
      Tapp (s, []), ty
512
  | PPapp (x, tl) ->
513
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
514
      let s, tyl, ty = specialize_fsymbol ~loc s in
515
      let tl = dtype_args s.ls_name loc env tyl tl in
516
      Tapp (s, tl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
517
  | PPconst (ConstInt _ as c) ->
518
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
519
  | PPconst (ConstReal _ as c) ->
520
      Tconst c, Tyapp (Ty.ts_real, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
521 522 523 524 525 526
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
      let env = { env with dvars = M.add x ty env.dvars } in
      let e2 = dterm env e2 in
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
527
  | PPmatch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
528 529 530 531
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
      let tb = (* the type of all branches *)
	let tv = create_tvsymbol (id_user "a" loc) in
532
	Tyvar (create_ty_decl_var ~loc ~user:false tv) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
533
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
534
      let branch (pat, e) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
535
	let loc = pat.pat_loc in
536
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
537
        let env, pat = dpat env pat in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
538 539 540 541 542
	if not (unify pat.dp_ty ty) then term_expected_type ~loc pat.dp_ty ty;
	let loc = e.pp_loc in
	let e = dterm env e in
	if not (unify e.dt_ty tb) then term_expected_type ~loc e.dt_ty tb;
        pat, e
Andrei Paskevich's avatar
Andrei Paskevich committed
543 544 545
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).dt_ty in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
546
      Tmatch (e1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
547 548 549
  | 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
550 551 552 553 554 555
  | 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
556
  | PPquant _ | PPif _ 
557 558
  | PPprefix _ | PPinfix _ | PPfalse | PPtrue ->
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
559

560 561 562 563 564 565 566 567 568 569 570
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) ->
      Fif (dfmla env a, dfmla env b, dfmla env c)  
571
  | PPquant (q, uqu, trl, a) ->
572
      check_quant_linearity uqu;
573 574 575 576 577 578 579 580
      let uquant env (idl,ty) =
        let ty = dty env ty in
        let env, idl = 
          map_fold_left
            (fun env {id=x} -> { env with dvars = M.add x ty env.dvars }, x)
            env idl
        in
        env, (idl,ty)
581
      in
582
      let env, uqu = map_fold_left uquant env uqu in
583
      let trigger e =
584 585
	try 
	  TRterm (dterm env e) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
586 587
	with exn when trigger_not_a_term_exn exn ->
	  TRfmla (dfmla env e) 
588 589
      in
      let trl = List.map (List.map trigger) trl in
590 591 592 593 594
      let q = match q with 
        | PPforall -> Fforall 
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
595
  | PPapp (x, tl) ->
596
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
597
      let s, tyl = specialize_psymbol ~loc:e.pp_loc s in
598
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
599
      Fapp (s, tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
600 601 602 603 604 605
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
      let env = { env with dvars = M.add x ty env.dvars } in
      let e2 = dfmla env e2 in
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
606
  | PPmatch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
607 608
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
609
      let branch (pat, e) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
610
	let loc = pat.pat_loc in
611
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
612
        let env, pat = dpat env pat in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
613
	if not (unify pat.dp_ty ty) then term_expected_type ~loc pat.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
614 615
        pat, dfmla env e
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
616
      Fmatch (e1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
617 618 619
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
620
  | PPvar x -> 
621
      Fvar (find_prop x env.th).pr_fmla 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
622
  | PPconst _ | PPcast _ ->
623
      error ~loc:e.pp_loc PredicateExpected
624

625 626 627 628 629 630 631 632 633
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
    | [], [] -> 
	[]
    | 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
634
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
635 636 637 638 639 640
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

Andrei Paskevich's avatar
Andrei Paskevich committed
641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657
let rec pattern env p = 
  let ty = ty_of_dty p.dp_ty in
  match p.dp_node with
  | Pwild -> env, pat_wild ty
  | Pvar x -> 
      if M.mem x env then assert false; (* FIXME? *)
      let v = create_vsymbol (id_fresh x) ty in
      M.add x v env, pat_var v
  | Papp (s, pl) -> 
      let env, pl = map_fold_left pattern env pl in
      env, pat_app s pl ty
  | Pas (p, x) ->
      if M.mem x env then assert false; (* FIXME? *)
      let v = create_vsymbol (id_fresh x) ty in
      let env, p = pattern (M.add x v env) p in
      env, pat_as p v

658 659 660 661
let rec term env t = match t.dt_node with
  | Tvar x ->
      assert (M.mem x env);
      t_var (M.find x env)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
662
  | Tconst c ->
663
      t_const c (ty_of_dty t.dt_ty)
664
  | Tapp (s, tl) ->
665
      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
666 667 668 669 670 671 672
  | Tlet (e1, x, e2) ->
      let ty = ty_of_dty e1.dt_ty in
      let e1 = term env e1 in 
      let v = create_vsymbol (id_fresh x) ty in
      let env = M.add x v env in
      let e2 = term env e2 in
      t_let v e1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
673 674 675 676 677 678 679 680
  | Tmatch (e1, bl) ->
      let branch (pat,e) =
        let env, pat = pattern env pat in
        (pat, term env e)
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).t_ty in
      t_case (term env e1) bl ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
681 682 683
  | Tnamed (x, e1) ->
      let e1 = term env e1 in
      t_label_add x e1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
684 685
  | Teps _ ->
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
686

687 688 689 690 691 692 693 694 695 696 697
and fmla env = function
  | Ftrue ->
      f_true
  | Ffalse ->
      f_false 
  | 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)
698
  | Fquant (q, uqu, trl, f1) ->
699
      (* TODO: shouldn't we localize this ident? *)
700 701 702 703 704 705
      let uquant env (xl,ty) =
        let ty = ty_of_dty ty in
        map_fold_left
          (fun env x -> 
             let v = create_vsymbol (id_fresh x) ty in M.add x v env, v) 
          env xl 
706
      in
707
      let env, vl = map_fold_left uquant env uqu in
708 709 710 711 712 713
      let trigger = function
	| TRterm t -> TrTerm (term env t) 
	| TRfmla f -> TrFmla (fmla env f) 
      in
      let trl = List.map (List.map trigger) trl in
      f_quant q (List.concat vl) trl (fmla env f1)
714 715
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
716
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
717 718 719 720
      let ty = ty_of_dty e1.dt_ty in
      let e1 = term env e1 in 
      let v = create_vsymbol (id_fresh x) ty in
      let env = M.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
721 722
      let f2 = fmla env f2 in
      f_let v e1 f2
Andrei Paskevich's avatar
Andrei Paskevich committed
723 724 725 726 727 728
  | Fmatch (e1, bl) ->
      let branch (pat,e) =
        let env, pat = pattern env pat in
        (pat, fmla env e)
      in
      f_case (term env e1) (List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
729
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
730
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
731
      f_label_add x f1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
732 733
  | Fvar f ->
      f
734

735
(** Typing declarations, that is building environments. *)
736 737 738

open Ptree

739
let add_types dl th =
740
  let ns = get_namespace th in
741 742 743 744
  let def = 
    List.fold_left 
      (fun def d -> 
	 let id = d.td_ident in
745 746
	 if M.mem id.id def || Mnm.mem id.id ns.ns_ts then 
	   error ~loc:id.id_loc (ClashType id.id);
747 748
	 M.add id.id d def) 
      M.empty dl 
749
  in
750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765
  let tysymbols = Hashtbl.create 17 in
  let rec visit x = 
    try
      match Hashtbl.find tysymbols x with
	| None -> error CyclicTypeDef
	| Some ts -> ts
    with Not_found ->
      Hashtbl.add tysymbols x None;
      let d = M.find x def in
      let id = d.td_ident.id in
      let vars = Hashtbl.create 17 in
      let vl = 
	List.map 
	  (fun v -> 
	     if Hashtbl.mem vars v.id then 
	       error ~loc:v.id_loc (DuplicateTypeVar v.id);
766
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
767 768 769 770
	     Hashtbl.add vars v.id i;
	     i)
	  d.td_params 
      in
771
      let id = id_user id d.td_ident.id_loc in
772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799
      let ts = match d.td_def with
	| TDalias ty -> 
	    let rec apply = function
	      | PPTtyvar v -> 
		  begin 
		    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
		    | Qident x when M.mem x.id def ->
			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))
	| TDabstract | TDalgebraic _ -> 
	    create_tysymbol id vl None
      in
      Hashtbl.add tysymbols x (Some ts);
      ts
  in
800 801 802 803
  let th' = 
    let tsl = 
      M.fold (fun x _ tsl -> let ts = visit x in (ts, Tabstract) :: tsl) def []
    in
804
    add_decl th (create_ty_decl tsl)
805
  in
806
  let decl d = 
807 808 809 810 811 812 813 814
    let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
      | None -> 
	  assert false
      | Some ts -> 
	  let th' = create_denv th' in
	  let vars = th'.utyvars in
	  List.iter 
	    (fun v -> 
815
	       Hashtbl.add vars v.id_short (create_ty_decl_var ~user:true v)) 
816 817 818 819 820 821 822 823 824 825 826
	    ts.ts_args;
	  ts, th'
    in
    let d = match d.td_def with
      | TDabstract | TDalias _ -> 
	  Tabstract
      | TDalgebraic cl -> 
	  let ty = ty_app ts (List.map ty_var ts.ts_args) in
	  let constructor (loc, id, pl) = 
	    let param (_, t) = ty_of_dty (dty th' t) in
	    let tyl = List.map param pl in
827
	    create_fconstr (id_user id.id id.id_loc) tyl ty
828 829 830 831
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
832 833
  in
  let dl = List.map decl dl in
834
  add_decl th (create_ty_decl dl)
835

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
836 837 838
let env_of_vsymbol_list vl =
  List.fold_left (fun env v -> M.add v.vs_name.id_short v env) M.empty vl

839
let add_logics dl th =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
840
  let ns = get_namespace th in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
841 842
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
843
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
844 845 846
  (* 1. create all symbols and make an environment with these symbols *)
  let create_symbol th d = 
    let id = d.ld_ident.id in
847 848 849
    if Hashtbl.mem denvs id || Mnm.mem id ns.ns_ls 
      then error ~loc:d.ld_loc (Clash id);
    let v = id_user id d.ld_ident.id_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
850
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
851
    Hashtbl.add denvs id denv;
852
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
853 854 855 856 857
    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;
858
	  add_decl th (create_logic_decl [Lpredicate (ps, None)])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
859 860
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
861
	  let fs = create_fsymbol v pl t in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
862
	  Hashtbl.add fsymbols id fs;
863
	  add_decl th (create_logic_decl [Lfunction (fs, None)])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
864 865 866 867 868 869 870 871 872
  in
  let th' = List.fold_left create_symbol th dl in
  (* 2. then type-check all definitions *)
  let type_decl d = 
    let id = d.ld_ident.id in
    let dadd_var denv (x, ty) = match x with
      | None -> denv
      | Some id -> { denv with dvars = M.add id.id (dty denv ty) denv.dvars }
    in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
873 874 875
    let denv = Hashtbl.find denvs id in
    let denv = { denv with th = th' } in
    let denv = List.fold_left dadd_var denv d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
876 877
    let create_var (x, _) ty = 
      let id = match x with 
878 879
	| 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
880 881 882
      in
      create_vsymbol id ty
    in
883
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
884