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

typing.ml 35.2 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
Andrei Paskevich's avatar
Andrei Paskevich committed
30

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
(** typing using destructive type variables 
129

130 131 132 133 134 135
    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
136

137 138 139 140 141 142 143 144 145 146 147 148 149
*)

(** 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
150
  type_var_loc : loc option;
151
}
152

153 154 155 156
let rec print_dty fmt = function
  | Tyvar { type_val = Some t } ->
      print_dty fmt t
  | Tyvar { type_val = None; tvsymbol = v } ->
157
      fprintf fmt "'%s" v.tv_name.id_short
158
  | Tyapp (s, []) ->
159
      fprintf fmt "%s" s.ts_name.id_short
160
  | Tyapp (s, [t]) -> 
161
      fprintf fmt "%a %s" print_dty t s.ts_name.id_short
162
  | Tyapp (s, l) -> 
163 164
      fprintf fmt "(%a) %s" 
	(print_list comma print_dty) l s.ts_name.id_short
165

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
166 167 168 169 170
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

171
let create_ty_decl_var =
172
  let t = ref 0 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
173
  fun ?loc ~user tv -> 
174
    incr t; 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
175 176
    { tag = !t; user = user; tvsymbol = tv; type_val = None;
      type_var_loc = loc }
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204

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

205
(** Destructive typing environment, that is
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
206
    environment + local variables.
207
    It is only local to this module and created with [create_denv] below. *)
208 209

type denv = { 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
210
  th : theory_uc; (* the theory under construction *)
211
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
Andrei Paskevich's avatar
Andrei Paskevich committed
212
  dvars : dty Mstr.t; (* local variables, to be bound later *)
213 214
}

215 216
let create_denv th = { 
  th = th; 
217
  utyvars = Hashtbl.create 17; 
Andrei Paskevich's avatar
Andrei Paskevich committed
218
  dvars = Mstr.empty;
219
}
220

221 222 223 224
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
225
    (* TODO: shouldn't we localize this ident? *)
226
    let v = create_tvsymbol (id_fresh x) in
227
    let v = create_ty_decl_var ~user:true v in
228 229 230
    Hashtbl.add env.utyvars x v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
231 232
(* Specialize *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
233
let find_type_var ~loc env tv =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
234 235 236
  try
    Htv.find env tv
  with Not_found ->
237
    let v = create_ty_decl_var ~loc ~user:false tv in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
238 239 240
    Htv.add env tv v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
241
let rec specialize ~loc env t = match t.ty_node with
242
  | Ty.Tyvar tv -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
243
      Tyvar (find_type_var ~loc env tv)
244
  | Ty.Tyapp (s, tl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
245
      Tyapp (s, List.map (specialize ~loc env) tl)
246

247 248 249
(** generic find function using a path *)

let find_local_namespace {id=x; id_loc=loc} ns = 
250
  try Mnm.find x ns.ns_ns
251 252 253 254 255 256 257 258 259 260 261 262
  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
263
let find_local_tysymbol {id=x; id_loc=loc} ns = 
264
  try Mnm.find x ns.ns_ts
265 266
  with Not_found -> error ~loc (UnboundType x)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
267 268 269
let find_tysymbol_ns p ns =
  find find_local_tysymbol p ns

270
let find_tysymbol p th = 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
271
  find_tysymbol_ns p (get_namespace th)
272

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
273
let specialize_tysymbol ~loc x env =
274
  let s = find_tysymbol x env.th in
275
  let env = Htv.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
276
  s, List.map (find_type_var ~loc env) s.ts_args
277
	
278 279
let find_lsymbol {id=x; id_loc=loc} ns = 
  try Mnm.find x ns.ns_ls
280 281
  with Not_found -> error ~loc (UnboundSymbol x)

282 283
let find_lsymbol_ns p ns = 
  find find_lsymbol p ns
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284

285 286
let find_lsymbol p th = 
  find_lsymbol_ns p (get_namespace th)
287

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

292 293 294
let find_prop_ns p ns =
  find find_prop p ns

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
295
let find_prop p th =
296
  find_prop_ns p (get_namespace th)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
297

298 299 300
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
301
  let env = Htv.create 17 in
302
  s, List.map (specialize ~loc env) tl, option_map (specialize ~loc env) t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
303

304 305 306 307 308
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
309

310 311 312 313 314
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
315

316 317
(** Typing types *)

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
322 323 324 325 326 327 328 329
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

330
(* parsed types -> intermediate types *)
331 332

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

336
let rec dty env = function
337
  | PPTtyvar {id=x} -> 
338
      Tyvar (find_user_type_var x env)
339
  | PPTtyapp (p, x) ->
340
      let loc = qloc x in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
341
      let ts, tv = specialize_tysymbol ~loc x env in
342 343 344
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
345 346 347 348 349
      let tyl = List.map (dty env) p in
      match ts.ts_def with
	| None -> 
	    Tyapp (ts, tyl)
	| Some ty -> 
350 351
	    let add m v t = Mtv.add v t m in
            let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
352
	    type_inst s ty
353 354

(* intermediate types -> types *)
355
let rec ty_of_dty = function
356
  | Tyvar { type_val = Some t } ->
357
      ty_of_dty t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
358 359
  | Tyvar { type_val = None; user = false; type_var_loc = loc } ->
      errorm ?loc "undefined type variable"
360 361 362
  | Tyvar { tvsymbol = tv } ->
      Ty.ty_var tv
  | Tyapp (s, tl) ->
363
      Ty.ty_app s (List.map ty_of_dty tl)
364

365
(** Typing terms and formulas *)
366

Andrei Paskevich's avatar
Andrei Paskevich committed
367 368 369 370 371 372 373 374
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

375 376
type uquant = string list * dty

377 378 379
type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
380
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
381
  | Tconst of constant
382
  | Tapp of lsymbol * dterm list
383
  | Tlet of dterm * string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
384
  | Tmatch of dterm * (dpattern * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
385
  | Tnamed of string * dterm
386 387 388
  | Teps of string * dfmla

and dfmla = 
389
  | Fapp of lsymbol * dterm list
390
  | Fquant of quant * uquant list * dtrigger list list * dfmla
391 392 393 394 395
  | 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
396
  | Flet of dterm * string * dfmla
Andrei Paskevich's avatar
Andrei Paskevich committed
397
  | Fmatch of dterm * (dpattern * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
398
  | Fnamed of string * dfmla
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
399
  | Fvar of fmla
400

401 402 403 404
and dtrigger =
  | TRterm of dterm
  | TRfmla of dfmla

405 406 407 408 409 410
let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

411
let check_pat_linearity pat =
Andrei Paskevich's avatar
Andrei Paskevich committed
412
  let s = ref Sstr.empty in
413
  let add id =
Andrei Paskevich's avatar
Andrei Paskevich committed
414 415
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
416 417 418 419 420 421 422 423 424
  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
425 426 427 428 429 430 431
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
432
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
433 434 435
      env, Pwild, ty
  | PPpvar {id=x} ->
      let tv = create_tvsymbol (id_user "a" loc) in
436
      let ty = Tyvar (create_ty_decl_var ~loc ~user:false tv) in
Andrei Paskevich's avatar
Andrei Paskevich committed
437
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
438 439 440 441 442 443 444 445
      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
Andrei Paskevich's avatar
Andrei Paskevich committed
446
      let env = { env with dvars = Mstr.add x p.dp_ty env.dvars } in
Andrei Paskevich's avatar
Andrei Paskevich committed
447 448
      env, Pas (p,x), p.dp_ty

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
449 450
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
451
  if n <> m then error ~loc (BadNumberOfArguments (s, m, n));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
452
  let rec check_arg env = function
Andrei Paskevich's avatar
Andrei Paskevich committed
453
    | [], [] -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
454 455 456 457 458 459 460
	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
461 462 463
    | _ ->
	assert false
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
464
  check_arg env (el, pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
465

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
466
let rec trigger_not_a_term_exn = function
467
  | Error TermExpected -> true
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
468 469 470
  | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
  | _ -> false

471
let check_quant_linearity uqu =
Andrei Paskevich's avatar
Andrei Paskevich committed
472
  let s = ref Sstr.empty in
473
  let check id = 
Andrei Paskevich's avatar
Andrei Paskevich committed
474 475
    if Sstr.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
    s := Sstr.add id.id !s
476 477 478
  in
  List.iter (fun (idl, _) -> List.iter check idl) uqu

479 480 481 482 483
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
Andrei Paskevich's avatar
Andrei Paskevich committed
484
  | PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
485
      (* local variable *)
Andrei Paskevich's avatar
Andrei Paskevich committed
486
      let ty = Mstr.find x env.dvars in
487 488 489
      Tvar x, ty
  | PPvar x -> 
      (* 0-arity symbol (constant) *)
490
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
491
      let s, tyl, ty = specialize_fsymbol ~loc s in
492
      let n = List.length tyl in
493
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
494
      Tapp (s, []), ty
495
  | PPapp (x, tl) ->
496
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
497
      let s, tyl, ty = specialize_fsymbol ~loc s in
498
      let tl = dtype_args s.ls_name loc env tyl tl in
499
      Tapp (s, tl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
500
  | PPconst (ConstInt _ as c) ->
501
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
502
  | PPconst (ConstReal _ as c) ->
503
      Tconst c, Tyapp (Ty.ts_real, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
504 505 506
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
507
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
508 509
      let e2 = dterm env e2 in
      Tlet (e1, x, e2), e2.dt_ty
Andrei Paskevich's avatar
Andrei Paskevich committed
510
  | PPmatch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
511 512 513 514
      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
515
	Tyvar (create_ty_decl_var ~loc ~user:false tv) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
516
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
517
      let branch (pat, e) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
518
	let loc = pat.pat_loc in
519
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
520
        let env, pat = dpat env pat in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
521 522 523 524 525
	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
526 527 528
      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
529
      Tmatch (e1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
530 531 532
  | 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
533 534 535 536 537 538
  | 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
539
  | PPquant _ | PPif _ 
540 541
  | PPprefix _ | PPinfix _ | PPfalse | PPtrue ->
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
542

543 544 545 546 547 548 549 550 551 552 553
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)  
554
  | PPquant (q, uqu, trl, a) ->
555
      check_quant_linearity uqu;
556 557 558 559
      let uquant env (idl,ty) =
        let ty = dty env ty in
        let env, idl = 
          map_fold_left
Andrei Paskevich's avatar
Andrei Paskevich committed
560
            (fun env {id=x} -> { env with dvars = Mstr.add x ty env.dvars }, x)
561 562 563
            env idl
        in
        env, (idl,ty)
564
      in
565
      let env, uqu = map_fold_left uquant env uqu in
566
      let trigger e =
567 568
	try 
	  TRterm (dterm env e) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
569 570
	with exn when trigger_not_a_term_exn exn ->
	  TRfmla (dfmla env e) 
571 572
      in
      let trl = List.map (List.map trigger) trl in
573 574 575 576 577
      let q = match q with 
        | PPforall -> Fforall 
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
578
  | PPapp (x, tl) ->
579
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
580
      let s, tyl = specialize_psymbol ~loc:e.pp_loc s in
581
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
582
      Fapp (s, tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
583 584 585
  | PPlet ({id=x}, e1, e2) ->
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
586
      let env = { env with dvars = Mstr.add x ty env.dvars } in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
587 588
      let e2 = dfmla env e2 in
      Flet (e1, x, e2)
Andrei Paskevich's avatar
Andrei Paskevich committed
589
  | PPmatch (e1, bl) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
590 591
      let e1 = dterm env e1 in
      let ty = e1.dt_ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
592
      let branch (pat, e) =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
593
	let loc = pat.pat_loc in
594
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
595
        let env, pat = dpat env pat in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
596
	if not (unify pat.dp_ty ty) then term_expected_type ~loc pat.dp_ty ty;
Andrei Paskevich's avatar
Andrei Paskevich committed
597 598
        pat, dfmla env e
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
599
      Fmatch (e1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
600 601 602
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
603
  | PPvar x -> 
604
      Fvar (snd (find_prop x env.th))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
605
  | PPconst _ | PPcast _ ->
606
      error ~loc:e.pp_loc PredicateExpected
607

608 609 610 611 612 613 614 615 616
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
617
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
618 619 620 621 622 623
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

Andrei Paskevich's avatar
Andrei Paskevich committed
624 625 626 627 628
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 -> 
Andrei Paskevich's avatar
Andrei Paskevich committed
629
      if Mstr.mem x env then assert false; (* FIXME? *)
Andrei Paskevich's avatar
Andrei Paskevich committed
630
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
631
      Mstr.add x v env, pat_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
632 633 634 635
  | Papp (s, pl) -> 
      let env, pl = map_fold_left pattern env pl in
      env, pat_app s pl ty
  | Pas (p, x) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
636
      if Mstr.mem x env then assert false; (* FIXME? *)
Andrei Paskevich's avatar
Andrei Paskevich committed
637
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
638
      let env, p = pattern (Mstr.add x v env) p in
Andrei Paskevich's avatar
Andrei Paskevich committed
639 640
      env, pat_as p v

641 642
let rec term env t = match t.dt_node with
  | Tvar x ->
Andrei Paskevich's avatar
Andrei Paskevich committed
643 644
      assert (Mstr.mem x env);
      t_var (Mstr.find x env)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
645
  | Tconst c ->
646
      t_const c (ty_of_dty t.dt_ty)
647
  | Tapp (s, tl) ->
648
      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
649 650 651 652
  | 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
Andrei Paskevich's avatar
Andrei Paskevich committed
653
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
654 655
      let e2 = term env e2 in
      t_let v e1 e2
Andrei Paskevich's avatar
Andrei Paskevich committed
656 657 658 659 660 661 662 663
  | 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
664 665 666
  | 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
667 668
  | Teps _ ->
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
669

670 671 672 673 674 675 676 677 678 679 680
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)
681
  | Fquant (q, uqu, trl, f1) ->
682
      (* TODO: shouldn't we localize this ident? *)
683 684 685 686
      let uquant env (xl,ty) =
        let ty = ty_of_dty ty in
        map_fold_left
          (fun env x -> 
Andrei Paskevich's avatar
Andrei Paskevich committed
687
             let v = create_vsymbol (id_fresh x) ty in Mstr.add x v env, v) 
688
          env xl 
689
      in
690
      let env, vl = map_fold_left uquant env uqu in
691
      let trigger = function
692 693
	| TRterm t -> Term (term env t) 
	| TRfmla f -> Fmla (fmla env f) 
694 695 696
      in
      let trl = List.map (List.map trigger) trl in
      f_quant q (List.concat vl) trl (fmla env f1)
697 698
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
699
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
700 701 702
      let ty = ty_of_dty e1.dt_ty in
      let e1 = term env e1 in 
      let v = create_vsymbol (id_fresh x) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
703
      let env = Mstr.add x v env in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
704 705
      let f2 = fmla env f2 in
      f_let v e1 f2
Andrei Paskevich's avatar
Andrei Paskevich committed
706 707 708 709 710 711
  | 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
712
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
713
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
714
      f_label_add x f1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
715 716
  | Fvar f ->
      f
717

718
(** Typing declarations, that is building environments. *)
719 720 721

open Ptree

722
let add_types dl th =
723
  let ns = get_namespace th in
724 725 726 727
  let def = 
    List.fold_left 
      (fun def d -> 
	 let id = d.td_ident in
Andrei Paskevich's avatar
Andrei Paskevich committed
728
	 if Mstr.mem id.id def || Mnm.mem id.id ns.ns_ts then 
729
	   error ~loc:id.id_loc (ClashType id.id);
Andrei Paskevich's avatar
Andrei Paskevich committed
730 731
	 Mstr.add id.id d def) 
      Mstr.empty dl 
732
  in
733 734 735 736 737 738 739 740
  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;
Andrei Paskevich's avatar
Andrei Paskevich committed
741
      let d = Mstr.find x def in
742 743 744 745 746 747 748
      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);
749
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
750 751 752 753
	     Hashtbl.add vars v.id i;
	     i)
	  d.td_params 
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
754
      let id = id_user id d.td_loc in
755 756 757 758 759 760 761 762 763 764
      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
Andrei Paskevich's avatar
Andrei Paskevich committed
765
		    | Qident x when Mstr.mem x.id def ->
766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782
			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
783 784
  let th' = 
    let tsl = 
Andrei Paskevich's avatar
Andrei Paskevich committed
785
      Mstr.fold (fun x _ tsl -> let ts = visit x in (ts, Tabstract) :: tsl) def []
786
    in
787
    add_decl th (create_ty_decl tsl)
788
  in
789
  let decl d = 
790 791 792 793 794 795 796 797
    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 -> 
798
	       Hashtbl.add vars v.tv_name.id_short 
799
                  (create_ty_decl_var ~user:true v)) 
800 801 802 803 804 805 806 807 808 809 810
	    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
Andrei Paskevich's avatar
Andrei Paskevich committed
811
	    create_fconstr (id_user id.id loc) tyl ty
812 813 814 815
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
816 817
  in
  let dl = List.map decl dl in
818
  List.fold_left add_decl th (create_ty_decls dl)
819

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