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

20 21
open Util
open Format
22
open Pp
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 42
  | TermExpectedType of (formatter -> unit) * (formatter -> unit) 
      (* actual / expected *)
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
46
  | UnboundTheory of string
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 101 102 103
      fprintf fmt "but is expecting %d arguments@]" m
  | TermExpectedType (ty1, ty2) ->
      fprintf fmt "@[This term has type "; ty1 fmt; 
      fprintf fmt "@ but is expected to have type@ "; ty2 fmt; fprintf fmt "@]"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104 105
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
106 107
  | ClashNamespace s ->
      fprintf fmt "clash with previous namespace %s" s
108 109
  | UnboundTheory s ->
      fprintf fmt "unbound theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
110 111
  | AlreadyTheory s ->
      fprintf fmt "already using a theory with name %s" s
112 113
  | UnboundNamespace s ->
      fprintf fmt "unbound namespace %s" s
114 115 116 117 118 119 120 121
  | 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
122 123 124 125
  | 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
126 127
  | AnyMessage s ->
      fprintf fmt "%s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
128

129 130
(** Environments *)

131
module S = Set.Make(String)
132 133 134 135
module M = Map.Make(String)

type env = {
  loadpath : string list;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
136
  theories : theory M.t; (* local theories *)
137 138 139 140 141 142
}

let create lp = {
  loadpath = lp;
  theories = M.empty;
}
143 144

(** typing using destructive type variables 
145

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

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

(** 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
166
  type_var_loc : loc option;
167
}
168

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

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 276
  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 *)

let find_tysymbol {id=x; id_loc=loc} ns = 
277
  try Mnm.find x ns.ns_ts
278 279 280 281 282
  with Not_found -> error ~loc (UnboundType x)

let find_tysymbol p th = 
  find find_tysymbol p (get_namespace th)

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

let find_fsymbol p th = 
  find find_fsymbol p (get_namespace th)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
295
let specialize_fsymbol ~loc s =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
296 297
  let tl, t = s.fs_scheme in
  let env = Htv.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
298
  s, List.map (specialize ~loc env) tl, specialize ?loc env t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
299

300
let find_psymbol {id=x; id_loc=loc} ns = 
301
  try Mnm.find x ns.ns_ps
302 303 304 305 306
  with Not_found -> error ~loc (UnboundSymbol x)

let find_psymbol p th =
  find find_psymbol p (get_namespace th)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
307
let specialize_psymbol ~loc s =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
308
  let env = Htv.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
309
  s, List.map (specialize ~loc env) s.ps_scheme
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
310

311 312
(** Typing types *)

313
let rec qloc = function
314
  | Qident x -> x.id_loc
315
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc
316 317

(* parsed types -> intermediate types *)
318 319 320 321 322

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)

323
let rec dty env = function
324
  | PPTtyvar {id=x} -> 
325
      Tyvar (find_user_type_var x env)
326
  | PPTtyapp (p, x) ->
327
      let loc = qloc x in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
328
      let ts, tv = specialize_tysymbol ~loc x env in
329 330 331
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
332 333 334 335 336 337 338 339
      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
340 341

(* intermediate types -> types *)
342
let rec ty_of_dty = function
343
  | Tyvar { type_val = Some t } ->
344
      ty_of_dty t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
345 346
  | Tyvar { type_val = None; user = false; type_var_loc = loc } ->
      errorm ?loc "undefined type variable"
347 348 349
  | Tyvar { tvsymbol = tv } ->
      Ty.ty_var tv
  | Tyapp (s, tl) ->
350
      Ty.ty_app s (List.map ty_of_dty tl)
351

352
(** Typing terms and formulas *)
353 354 355 356

type dterm = { dt_node : dterm_node; dt_ty : dty }

and dterm_node =
357
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
358
  | Tconst of constant
359 360 361 362 363 364 365
  | Tapp of fsymbol * dterm list
  | Tlet of dterm * string * dterm
(*   | Tcase of dterm * tbranch list *)
  | Teps of string * dfmla

and dfmla = 
  | Fapp of psymbol * dterm list
366
  | Fquant of quant * string * dty * dfmla
367 368 369 370 371 372 373 374 375 376 377 378 379 380
  | Fbinop of binop * dfmla * dfmla
  | Fnot of dfmla
  | Ftrue
  | Ffalse
  | Fif of dfmla * dfmla * dfmla
(*   | Flet of dterm * string * dfmla *)
(*   | Fcase of dterm * (pattern * dfmla) list *)

let binop = function
  | PPand -> Fand
  | PPor -> For
  | PPimplies -> Fimplies
  | PPiff -> Fiff

381 382 383 384 385
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
386 387 388 389 390 391
  | 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) *)
Jean-Christophe Filliâtre's avatar
egalite  
Jean-Christophe Filliâtre committed
392
      let s = find_fsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
393
      let s, tyl, ty = specialize_fsymbol ~loc s in
394 395 396
      let n = List.length tyl in
      if n > 0 then error ~loc (BadNumberOfArguments (s.fs_name, 0, n));
      Tapp (s, []), ty
397
  | PPapp (x, tl) ->
Jean-Christophe Filliâtre's avatar
egalite  
Jean-Christophe Filliâtre committed
398
      let s = find_fsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
399
      let s, tyl, ty = specialize_fsymbol ~loc s in
400 401
      let tl = dtype_args s.fs_name loc env tyl tl in
      Tapp (s, tl), ty
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
402
  | PPconst (ConstInt _ as c) ->
403
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
404
  | PPconst (ConstReal _ as c) ->
405
      Tconst c, Tyapp (Ty.ts_real, [])
406 407 408 409 410 411 412 413 414
  | PPmatch _ ->
      assert false (* TODO *)
  | PPlet _ ->
      assert false (* TODO *)
  | PPnamed _ ->
      assert false (* TODO *)
  | PPexists _ | PPforall _ | PPif _ 
  | PPprefix _ | PPinfix _ | PPfalse | PPtrue ->
      error ~loc TermExpected
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
415

416 417 418 419 420 421 422 423 424 425 426
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)  
427
  | PPforall ({id=x}, ty, _, a) -> (* TODO: triggers *)
428
      let ty = dty env ty in
429 430 431
      let env = { env with dvars = M.add x ty env.dvars } in
      Fquant (Fforall, x, ty, dfmla env a)
  | PPexists ({id=x}, ty, a) -> (* TODO: triggers *)
432
      let ty = dty env ty in
433 434
      let env = { env with dvars = M.add x ty env.dvars } in
      Fquant (Fexists, x, ty, dfmla env a)
435
  | PPapp (x, tl) ->
Jean-Christophe Filliâtre's avatar
egalite  
Jean-Christophe Filliâtre committed
436
      let s = find_psymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
437
      let s, tyl = specialize_psymbol ~loc:e.pp_loc s in
438 439
      let tl = dtype_args s.ps_name e.pp_loc env tyl tl in
      Fapp (s, tl)
440 441 442 443 444 445 446 447 448 449
  | PPmatch _ ->
      assert false (* TODO *)
  | PPlet _ ->
      assert false (* TODO *)
  | PPnamed _ ->
      assert false (* TODO *)
  | PPvar _ -> 
      assert false (* TODO *)
  | PPconst _ | PPprefix (PPneg, _) ->
      error ~loc:e.pp_loc PredicateExpected
450

451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472
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
	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)

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
473
  | Tconst c ->
474
      t_const c (ty_of_dty t.dt_ty)
475
  | Tapp (s, tl) ->
476
      t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
477 478
  | _ ->
      assert false (* TODO *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
479

480 481 482 483 484 485 486 487 488 489 490
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)
491
  | Fquant (q, x, t, f1) ->
492
      (* TODO: shouldn't we localize this ident? *)
493
      let v = create_vsymbol (id_fresh x) (ty_of_dty t) in
494
      let env = M.add x v env in
495
      f_quant q [v] [] (fmla env f1)
496 497 498
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)

499

500
(** Typing declarations, that is building environments. *)
501 502 503

open Ptree

504
let add_types loc dl th =
505
  let ns = get_namespace th in
506 507 508 509
  let def = 
    List.fold_left 
      (fun def d -> 
	 let id = d.td_ident in
510 511
	 if M.mem id.id def || Mnm.mem id.id ns.ns_ts then 
	   error ~loc:id.id_loc (ClashType id.id);
512 513
	 M.add id.id d def) 
      M.empty dl 
514
  in
515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530
  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);
531
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
532 533 534 535
	     Hashtbl.add vars v.id i;
	     i)
	  d.td_params 
      in
536
      let id = id_user id d.td_ident.id_loc in
537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564
      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
565 566 567 568 569 570
  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
571
  let decl d = 
572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596
    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
	    create_fsymbol (id_user id.id id.id_loc) (tyl, ty) true
	  in
	  Talgebraic (List.map constructor cl)
    in
    ts, d
597 598
  in
  let dl = List.map decl dl in
599
  add_decl th (create_type dl)
600

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
601 602 603 604
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
605
  let ns = get_namespace th in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
606 607
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
608
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
609 610 611
  (* 1. create all symbols and make an environment with these symbols *)
  let create_symbol th d = 
    let id = d.ld_ident.id in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
612
    if Hashtbl.mem denvs id || Mnm.mem id ns.ns_fs then error ~loc (Clash id);
613
    let v = id_user id loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
614
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
615
    Hashtbl.add denvs id denv;
616
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
617 618 619 620 621
    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;
622
	  add_decl th (create_logic [Lpredicate (ps, None)])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
623 624 625 626
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
	  let fs = create_fsymbol v (pl, t) false in
	  Hashtbl.add fsymbols id fs;
627
	  add_decl th (create_logic [Lfunction (fs, None)])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
628 629 630 631 632 633 634 635 636
  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
637 638 639
    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
640 641
    let create_var (x, _) ty = 
      let id = match x with 
642 643
	| 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
644 645 646
      in
      create_vsymbol id ty
    in
647
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
648 649 650
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
651
	begin match d.ld_def with
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
652
	  | None -> 
653
              Lpredicate (ps, None)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
654 655
	  | Some f -> 
	      let f = dfmla denv f in
656
	      let vl = mk_vlist ps.ps_scheme in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
657
	      let env = env_of_vsymbol_list vl in
658 659
              make_pdef ps vl (fmla env f)
        end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
660
    | Some ty -> (* function *)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
661
	let fs = Hashtbl.find fsymbols id in
662
	begin match d.ld_def with
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
663
	  | None -> 
664
              Lfunction (fs, None)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
665
	  | Some t -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
666
	      let loc = t.pp_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
667
	      let t = dterm denv t in
668
	      let vl = mk_vlist (fst fs.fs_scheme) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
669
	      let env = env_of_vsymbol_list vl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
670 671 672 673 674 675
              try 
		make_fdef fs vl (term env t) 
	      with _ -> 
		error ~loc (TermExpectedType 
			      ((fun f -> print_dty f t.dt_ty),
			       (fun f -> print_dty f (dty denv ty))))
676
        end
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
677 678
  in
  let dl = List.map type_decl dl in
679
  add_decl th (create_logic dl)
680

681

682 683 684
let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
685
  term M.empty t
686

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
687 688 689 690 691
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
692 693 694
let add_prop k loc s f th =
  let f = fmla th f in
  try
695
    add_decl th (create_prop k (id_user s.id loc) f)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
696 697
  with ClashSymbol _ ->
    error ~loc (Clash s.id)
698

699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724
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
725 726 727 728 729 730 731 732 733
  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
734

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

(* parse file and store all theories into parsed_theories *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
738 739 740 741 742 743 744
let load_file file =
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
  let tl = Lexer.parse_logic_file lb in 
  close_in c;
  tl
745

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
746
let prop_kind = function
747 748 749
  | Kaxiom -> Paxiom
  | Kgoal -> Pgoal
  | Klemma -> Plemma
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
750

751
let rec find_theory env q = match q with
752
  | Qident id -> 
753
      (* local theory *)
754 755 756 757 758
      begin 
	try M.find id.id env.theories 
	with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id) 
      end
  | Qdot (f, id) ->
759 760
      (* theory in file f *)
      let file = locate_file env f in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
761 762 763 764 765 766 767 768 769 770 771 772
      if not (Hashtbl.mem loaded_theories file) then begin
	let tl = load_file file in
	let h = Hashtbl.create 17 in
	Hashtbl.add loaded_theories file h;
	let env = { env with theories = M.empty } in
	let add env pt =
	  let t, env = add_theory env pt in
	  Hashtbl.add h t.th_name.id_short t;
	  env
	in
	ignore (List.fold_left add env tl);
      end;
773
      let h = Hashtbl.find loaded_theories file in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
774 775
      try Hashtbl.find h id.id
      with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id)
776 777

and type_theory env id pt =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
778
  (* TODO: use long name *)
779
  let n = id_user id.id id.id_loc in
780
  let th = create_theory n in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
781
  let th = add_decls env th pt.pt_decl in
782 783 784
  close_theory th

and add_decls env th = List.fold_left (add_decl env) th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
785

786
and add_decl env th = function
787 788
  | TypeDecl (loc, dl) ->
      add_types loc dl th
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
789 790
  | Logic (loc, dl) ->
      add_logics loc dl th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
791 792
  | Prop (loc, k, s, f) ->
      add_prop (prop_kind k) loc s f th
793
  | Use (loc, use) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
794 795
      let t = find_theory env use.use_theory in
      let n = match use.use_as with 
796 797
	| None -> t.th_name.id_short
	| Some x -> x.id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
798
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
799
      begin try match use.use_imp_exp with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
800 801 802 803 804 805 806 807 808 809 810 811
	| Nothing ->
	    (* use T = namespace T use_export T end *)
	    let th = open_namespace th in
	    let th = use_export th t in
	    close_namespace th n ~import:false
	| Import ->
	    (* use import T = namespace T use_export T end import T *)
	    let th = open_namespace th in
	    let th = use_export th t in
	    close_namespace th n ~import:true
	| Export ->
	    use_export th t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
812 813
      with Theory.ClashSymbol s ->
	error ~loc (Clash s)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
814
      end
815 816
  | Namespace (_, {id=id; id_loc=loc}, dl) ->
      let ns = get_namespace th in
817
      if Mnm.mem id ns.ns_ns then error ~loc (ClashNamespace id);
818
      let th = open_namespace th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
819
      let th = add_decls env th dl in
820
      close_namespace th id ~import:false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
821
  | Inductive_def _ ->
822
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
823

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
824 825 826
and add_theory env pt =
  let id = pt.pt_name in
  if M.mem id.id env.theories then error ~loc:pt.pt_loc (ClashTheory id.id);
827
  let t = type_theory env id pt in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
828 829 830 831 832
  t, { env with theories = M.add id.id t env.theories }

let add_theories =
  List.fold_left
    (fun env pt -> let _, env = add_theory env pt in env) 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
833

834 835 836
let list_theory env = 
  M.fold (fun _ v acc -> v::acc) env.theories []

837 838
(*
Local Variables: 
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
839
compile-command: "make -C ../.. test"
840 841
End: 
*)