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

20 21
open Util
open Format
22
open Pp
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

29 30 31
(** errors *)

type error = 
32
  | Message of string
33
  | ClashType of string
34
  | DuplicateTypeVar of string
35
  | UnboundType of string
36
  | TypeArity of qualid * int * int
37
  | Clash of string
38 39
  | PredicateExpected
  | TermExpected
40
  | UnboundSymbol of string
41
  | BadNumberOfArguments of Ident.ident * int * int 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
42
  | ClashTheory of string
43
  | ClashNamespace of string
44
  | UnboundTheory of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
45
  | AlreadyTheory of string
46
  | UnboundNamespace 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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
53
  | AnyMessage of string
54 55 56 57 58 59 60

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
61 62 63 64 65 66 67 68 69 70 71
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

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

76
let report fmt = function
77 78
  | Message s ->
      fprintf fmt "%s" s
79 80
  | ClashType s ->
      fprintf fmt "clash with previous type %s" s
81
  | DuplicateTypeVar s ->
82
      fprintf fmt "duplicate type parameter %s" s
83
  | UnboundType s ->
84
       fprintf fmt "Unbound type '%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
  | UnboundSymbol s ->
95
       fprintf fmt "Unbound symbol '%s'" s
96
  | BadNumberOfArguments (s, n, m) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
97
      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short n;
98
      fprintf fmt "but is expecting %d arguments@]" m
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
99 100
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
101 102
  | ClashNamespace s ->
      fprintf fmt "clash with previous namespace %s" s
103 104
  | UnboundTheory s ->
      fprintf fmt "unbound theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105 106
  | AlreadyTheory s ->
      fprintf fmt "already using a theory with name %s" s
107 108
  | UnboundNamespace s ->
      fprintf fmt "unbound namespace %s" s
109 110 111 112 113 114 115 116
  | 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
117 118 119 120
  | 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
121 122
  | AnyMessage s ->
      fprintf fmt "%s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
123

124 125
(** Environments *)

126
module S = Set.Make(String)
127 128 129 130
module M = Map.Make(String)

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

let create lp = {
  loadpath = lp;
  theories = M.empty;
}
138 139

(** typing using destructive type variables 
140

141 142 143 144 145 146
    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
147

148 149 150 151 152 153 154 155 156 157 158 159 160
*)

(** 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
161
  type_var_loc : loc option;
162
}
163

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
177 178 179 180 181
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

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

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

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

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

226 227
let create_denv th = { 
  th = th; 
228 229 230
  utyvars = Hashtbl.create 17; 
  dvars = M.empty;
}
231

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

244
module Htv = Hid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
245

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

260 261 262
(** generic find function using a path *)

let find_local_namespace {id=x; id_loc=loc} ns = 
263
  try Mnm.find x ns.ns_ns
264 265 266 267 268 269 270 271 272 273 274 275
  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
276
let find_local_tysymbol {id=x; id_loc=loc} ns = 
277
  try Mnm.find x ns.ns_ts
278 279
  with Not_found -> error ~loc (UnboundType x)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
280 281 282
let find_tysymbol_ns p ns =
  find find_local_tysymbol p ns

283
let find_tysymbol p th = 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284
  find_tysymbol_ns p (get_namespace th)
285

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

295 296
let find_lsymbol_ns p ns = 
  find find_lsymbol p ns
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
297

298 299
let find_lsymbol p th = 
  find_lsymbol_ns p (get_namespace th)
300

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

307 308 309 310 311
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
312

313 314 315 316 317
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
318

319 320
(** Typing types *)

321
let rec qloc = function
322
  | Qident x -> x.id_loc
323
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc
324 325

(* parsed types -> intermediate types *)
326 327 328 329 330

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)

331
let rec dty env = function
332
  | PPTtyvar {id=x} -> 
333
      Tyvar (find_user_type_var x env)
334
  | PPTtyapp (p, x) ->
335
      let loc = qloc x in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
336
      let ts, tv = specialize_tysymbol ~loc x env in
337 338 339
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
340 341 342 343 344 345 346 347
      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
348 349

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

360
(** Typing terms and formulas *)
361

Andrei Paskevich's avatar
Andrei Paskevich committed
362 363 364 365 366 367 368 369
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

370 371
type uquant = string list * dty

372 373 374
type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
375
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
376
  | Tconst of constant
377
  | Tapp of lsymbol * dterm list
378
  | Tlet of dterm * string * dterm
Andrei Paskevich's avatar
Andrei Paskevich committed
379
  | Tmatch of dterm * (dpattern * dterm) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
380
  | Tnamed of string * dterm
381 382 383
  | Teps of string * dfmla

and dfmla = 
384
  | Fapp of lsymbol * dterm list
385
  | Fquant of quant * uquant list * dtrigger list list * dfmla
386 387 388 389 390
  | 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
391
  | Flet of dterm * string * dfmla
Andrei Paskevich's avatar
Andrei Paskevich committed
392
  | Fmatch of dterm * (dpattern * dfmla) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
393
  | Fnamed of string * dfmla
394

395 396 397 398
and dtrigger =
  | TRterm of dterm
  | TRfmla of dfmla

399 400 401 402 403 404
let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

405 406 407 408 409 410 411 412 413 414 415 416 417 418
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
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462
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
      let ty = Tyvar (create_type_var ~loc ~user:false tv) in
      env, Pwild, ty
  | PPpvar {id=x} ->
      let tv = create_tvsymbol (id_user "a" loc) in
      let ty = Tyvar (create_type_var ~loc ~user:false tv) in
      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

and dpat_args s loc env el pl = assert false (* TODO *)
(*
  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
	if not (unify a t.dt_ty) then
	  error ~loc (TermExpectedType ((fun f -> print_dty f t.dt_ty),
					(fun f -> print_dty f a)));
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)
*)

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

468
let check_quant_linearity uqu =
469 470 471 472 473 474 475
  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

476 477 478 479 480
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
481 482 483 484 485 486
  | 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) *)
487
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
488
      let s, tyl, ty = specialize_fsymbol ~loc s in
489
      let n = List.length tyl in
490
      if n > 0 then error ~loc (BadNumberOfArguments (s.ls_name, 0, n));
491
      Tapp (s, []), ty
492
  | PPapp (x, tl) ->
493
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
494
      let s, tyl, ty = specialize_fsymbol ~loc s in
495
      let tl = dtype_args s.ls_name loc env tyl tl in
496
      Tapp (s, tl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
497
  | PPconst (ConstInt _ as c) ->
498
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
499
  | PPconst (ConstReal _ as c) ->
500
      Tconst c, Tyapp (Ty.ts_real, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
501 502 503 504 505 506
  | 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
507 508 509 510
  | PPmatch (e1, bl) ->
      (* TODO: unify e1.type with patterns *)
      (* TODO: unify branch types with each other *)
      let branch (pat, e) =
511
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
512 513 514 515 516 517
        let env, pat = dpat env pat in
        pat, dterm env e
      in
      let bl = List.map branch bl in
      let ty = (snd (List.hd bl)).dt_ty in
      Tmatch (dterm env e1, bl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
518 519 520
  | 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
521 522 523 524 525 526
  | 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
527
  | PPquant _ | PPif _ 
528 529
  | PPprefix _ | PPinfix _ | PPfalse | PPtrue ->
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
530

531 532 533 534 535 536 537 538 539 540 541
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)  
542
  | PPquant (q, uqu, trl, a) ->
543
      check_quant_linearity uqu;
544 545 546 547 548 549 550 551
      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)
552
      in
553
      let env, uqu = map_fold_left uquant env uqu in
554 555 556
      let trigger e = (* FIXME? *)
	try 
	  TRterm (dterm env e) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
557 558
	with exn when trigger_not_a_term_exn exn ->
	  TRfmla (dfmla env e) 
559 560
      in
      let trl = List.map (List.map trigger) trl in
561 562 563 564 565
      let q = match q with 
        | PPforall -> Fforall 
        | PPexists -> Fexists
      in
      Fquant (q, uqu, trl, dfmla env a)
566
  | PPapp (x, tl) ->
567
      let s = find_lsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
568
      let s, tyl = specialize_psymbol ~loc:e.pp_loc s in
569
      let tl = dtype_args s.ls_name e.pp_loc env tyl tl in
570
      Fapp (s, tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
571 572 573 574 575 576
  | 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
577 578 579 580
  | PPmatch (e1, bl) ->
      (* TODO: unify e1.type with patterns *)
      (* TODO: unify branch types with each other *)
      let branch (pat, e) =
581
	check_pat_linearity pat;
Andrei Paskevich's avatar
Andrei Paskevich committed
582 583 584 585
        let env, pat = dpat env pat in
        pat, dfmla env e
      in
      Fmatch (dterm env e1, List.map branch bl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
586 587 588
  | PPnamed (x, f1) ->
      let f1 = dfmla env f1 in
      Fnamed (x, f1)
589 590
  | PPvar _ -> 
      assert false (* TODO *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
591
  | PPconst _ | PPcast _ ->
592
      error ~loc:e.pp_loc PredicateExpected
593

594 595 596 597 598 599 600 601 602
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
603
	if not (unify a t.dt_ty) then term_expected_type ~loc t.dt_ty a;
604 605 606 607 608 609
	t :: check_arg (al, bl)
    | _ ->
	assert false
  in
  check_arg (el, tl)

Andrei Paskevich's avatar
Andrei Paskevich committed
610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626
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

627 628 629 630
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
631
  | Tconst c ->
632
      t_const c (ty_of_dty t.dt_ty)
633
  | Tapp (s, tl) ->
634
      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
635 636 637 638 639 640 641
  | 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
642 643 644 645 646 647 648 649
  | 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
650 651 652
  | 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
653 654
  | Teps _ ->
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
655

656 657 658 659 660 661 662 663 664 665 666
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)
667
  | Fquant (q, uqu, trl, f1) ->
668
      (* TODO: shouldn't we localize this ident? *)
669 670 671 672 673 674
      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 
675
      in
676 677 678
      let env, vl = map_fold_left uquant env uqu in
      (* TODO: triggers *)
      f_quant q (List.concat vl) [] (fmla env f1)
679 680
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
681
  | Flet (e1, x, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
682 683 684 685
      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
686 687
      let f2 = fmla env f2 in
      f_let v e1 f2
Andrei Paskevich's avatar
Andrei Paskevich committed
688 689 690 691 692 693
  | 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
694
  | Fnamed (x, f1) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
695
      let f1 = fmla env f1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
696
      f_label_add x f1
697

698
(** Typing declarations, that is building environments. *)
699 700 701

open Ptree

702
let add_types loc dl th =
703
  let ns = get_namespace th in
704 705 706 707
  let def = 
    List.fold_left 
      (fun def d -> 
	 let id = d.td_ident in
708 709
	 if M.mem id.id def || Mnm.mem id.id ns.ns_ts then 
	   error ~loc:id.id_loc (ClashType id.id);
710 711
	 M.add id.id d def) 
      M.empty dl 
712
  in
713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728
  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);
729
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
730 731 732 733
	     Hashtbl.add vars v.id i;
	     i)
	  d.td_params 
      in
734
      let id = id_user id d.td_ident.id_loc in
735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762
      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
763 764 765 766 767 768
  let th' = 
    let tsl = 
      M.fold (fun x _ tsl -> let ts = visit x in (ts, Tabstract) :: tsl) def []
    in
    add_decl th (create_type tsl)
  in
769
  let decl d = 
770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789
    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 -> 
	       Hashtbl.add vars v.id_short (create_type_var ~user:true v)) 
	    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
790
	    create_fconstr (id_user id.id id.id_loc) tyl ty
791 792 793 794
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
795 796
  in
  let dl = List.map decl dl in
797
  add_decl th (create_type dl)
798

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

let add_logics loc dl th =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
803
  let ns = get_namespace th in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
804 805
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
806
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
807 808 809
  (* 1. create all symbols and make an environment with these symbols *)
  let create_symbol th d = 
    let id = d.ld_ident.id in
810
    if Hashtbl.mem denvs id || Mnm.mem id ns.ns_ls then error ~loc (Clash id);
811
    let v = id_user id loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
812
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
813
    Hashtbl.add denvs id denv;
814
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
815 816 817 818 819
    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;
820
	  add_decl th (create_logic [Lpredicate (ps, None)])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
821 822
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
823
	  let fs = create_fsymbol v pl t in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
824
	  Hashtbl.add fsymbols id fs;
825
	  add_decl th (create_logic [Lfunction (fs, None)])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
826 827 828 829 830 831 832 833 834
  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
835 836 837
    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
838 839
    let create_var (x, _) ty = 
      let id = match x with 
840 841
	| 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
842 843 844
      in
      create_vsymbol id ty
    in
845
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
846 847 848
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
849 850
        let defn = match d.ld_def with
	  | None -> None
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
851 852
	  | Some f -> 
	      let f = dfmla denv f in
853 854 855 856
              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
857
	      let env = env_of_vsymbol_list vl in
858 859 860
              Some (make_ps_defn ps vl (fmla env f))
        in
        Lpredicate (ps, defn)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
861
    | Some ty -> (* function *)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
862
	let fs = Hashtbl.find fsymbols id in
863 864
        let defn = match d.ld_def with
	  | None -> None
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
865
	  | Some t -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
866
	      let loc = t.pp_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
867
	      let t = dterm denv t in
868 869 870 871
              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
872
	      let env = env_of_vsymbol_list vl in
873
              try Some (make_fs_defn fs vl (term env t))
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
874
	      with _ -> term_expected_type ~loc t.dt_ty (dty denv ty)
875 876
        in
        Lfunction (fs, defn)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
877 878
  in
  let dl = List.map type_decl dl in
879
  add_decl th (create_logic dl)
880

881

882 883 884
let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
885
  term M.empty t
886

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
887 888 889 890 891
let fmla env f =
  let denv = create_denv env in
  let f = dfmla denv f in
  fmla M.empty f

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
892 893 894
let add_prop k loc s f th =
  let f = fmla th f in
  try
895
    add_decl th (create_prop k (id_user s.id loc) f)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
896 897
  with ClashSymbol _ ->
    error ~loc (Clash s.id)
898

899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924
let find_in_loadpath env f =
  let rec find c lp = match lp, c with
    | [], None -> 
	error ~loc:f.id_loc (NotInLoadpath f.id)
    | [], Some file ->
	file
    | dir :: lp, _ ->
	let file = Filename.concat dir f.id in
	if Sys.file_exists file then begin match c with
	  | None -> find (Some file) lp
	  | Some file' -> error ~loc:f.id_loc (AmbiguousPath (file, file'))
	end else
	  find c lp
  in
  find None env.loadpath

let locate_file env q = 
  let rec locate_dir = function
    | Qident d ->
	find_in_loadpath env d
    | Qdot (q, d) -> 
	let dir = locate_dir q in
	let dir = Filename.concat dir d.id in
	if not (Sys.file_exists dir) then error ~loc:d.id_loc (UnboundDir dir);
	dir
  in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
925 926 927 928 929 930 931 932 933
  match q with
    | Qident f -> 
	find_in_loadpath env { f with id = f.id ^ ".why" }
    | Qdot (p, f) -> 
	let dir = locate_dir p in 
	let file = Filename.concat dir f.id ^ ".why" in
	if not (Sys.file_exists file) then 
	  error ~loc:(qloc q) (UnboundFile file);
	file
934

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
935
let loaded_theories = Hashtbl.create 17 (* file -> string -> Theory.t *)
936 937

(* parse file and store all theories into parsed_theories *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
938 939 940 941 942 943 944
let load_file file =