typing.ml 19.3 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 34
  | ClashType of string
  | BadTypeArity 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 55 56 57 58 59

exception Error of error

let error ?loc e = match loc with
  | None -> raise (Error e)
  | Some loc -> raise (Loc.Located (loc, Error e))

60
let rec print_qualid fmt = function
61
  | Qident s -> fprintf fmt "%s" s.id
62
  | Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
63

64
let report fmt = function
65 66
  | Message s ->
      fprintf fmt "%s" s
67 68 69 70
  | ClashType s ->
      fprintf fmt "clash with previous type %s" s
  | BadTypeArity s ->
      fprintf fmt "duplicate type parameter %s" s
71
  | UnboundType s ->
72
       fprintf fmt "Unbound type '%s'" s
73
  | TypeArity (id, a, n) ->
74
      fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
75 76 77
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
      fprintf fmt "Clash with previous constant %s" id
78 79 80 81
  | PredicateExpected ->
      fprintf fmt "syntax error: predicate expected"
  | TermExpected ->
      fprintf fmt "syntax error: term expected"
82
  | UnboundSymbol s ->
83
       fprintf fmt "Unbound symbol '%s'" s
84
  | BadNumberOfArguments (s, n, m) ->
85
      fprintf fmt "@[Symbol `%s' is aplied to %d terms,@ " s.id_short n;
86 87 88 89
      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
90 91
  | ClashTheory s ->
      fprintf fmt "clash with previous theory %s" s
92 93
  | ClashNamespace s ->
      fprintf fmt "clash with previous namespace %s" s
94 95
  | UnboundTheory s ->
      fprintf fmt "unbound theory %s" s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96 97
  | AlreadyTheory s ->
      fprintf fmt "already using a theory with name %s" s
98 99
  | UnboundNamespace s ->
      fprintf fmt "unbound namespace %s" s
100 101 102 103 104 105 106 107
  | 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
108 109 110 111 112 113 114 115 116 117 118 119 120 121

(** Environments *)

module M = Map.Make(String)

type env = {
  loadpath : string list;
  theories : Theory.t M.t; (* local theories *)
}

let create lp = {
  loadpath = lp;
  theories = M.empty;
}
122 123

(** typing using destructive type variables 
124

125 126 127 128 129 130
    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
131

132 133 134 135 136 137 138 139 140 141 142 143 144 145
*)

(** 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;
}
146

147 148 149 150
let rec print_dty fmt = function
  | Tyvar { type_val = Some t } ->
      print_dty fmt t
  | Tyvar { type_val = None; tvsymbol = v } ->
151
      fprintf fmt "'%s" v.id_short
152
  | Tyapp (s, []) ->
153
      fprintf fmt "%s" s.ts_name.id_short
154
  | Tyapp (s, [t]) -> 
155
      fprintf fmt "%a %s" print_dty t s.ts_name.id_short
156
  | Tyapp (s, l) -> 
157 158
      fprintf fmt "(%a) %s" 
	(print_list comma print_dty) l s.ts_name.id_short
159

160 161
let create_type_var =
  let t = ref 0 in
162
  fun ~user tv -> 
163
    incr t; 
164
    { tag = !t; user = user; tvsymbol = tv; type_val = None }
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192

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

193
(** Destructive typing environment, that is
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
194
    environment + local variables.
195
    It is only local to this module and created with [create_denv] below. *)
196 197

type denv = { 
198
  th : Theory.th; (* the theory under construction *)
199 200
  utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
  dvars : dty M.t; (* local variables, to be bound later *)
201 202
}

203 204
let create_denv th = { 
  th = th; 
205 206 207
  utyvars = Hashtbl.create 17; 
  dvars = M.empty;
}
208

209 210 211 212
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
213 214
    (* TODO: shouldn't we localize this ident? *)
    let v = create_type_var ~user:true (id_fresh x x) in
215 216 217
    Hashtbl.add env.utyvars x v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
218 219
(* Specialize *)

220
module Htv = Hid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
221

222
let find_type_var env tv =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
223 224 225 226 227 228 229
  try
    Htv.find env tv
  with Not_found ->
    let v = create_type_var ~user:false tv in
    Htv.add env tv v;
    v
 
230
let rec specialize env t = match t.ty_node with
231
  | Ty.Tyvar tv -> 
232
      Tyvar (find_type_var env tv)
233 234
  | Ty.Tyapp (s, tl) ->
      Tyapp (s, List.map (specialize env) tl)
235

236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258
(** generic find function using a path *)

let find_local_namespace {id=x; id_loc=loc} ns = 
  try find_namespace ns x 
  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 = 
  try find_tysymbol ns x 
  with Not_found -> error ~loc (UnboundType x)

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

259
let specialize_tysymbol x env =
260
  let s = find_tysymbol x env.th in
261
  let env = Htv.create 17 in
262
  s, List.map (find_type_var env) s.ts_args
263
	
264 265 266 267 268 269 270
let find_fsymbol {id=x; id_loc=loc} ns = 
  try find_fsymbol ns x 
  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
271
let specialize_fsymbol x env =
272
  let s = find_fsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
273 274 275 276
  let tl, t = s.fs_scheme in
  let env = Htv.create 17 in
  s, List.map (specialize env) tl, specialize env t

277 278 279 280 281 282 283
let find_psymbol {id=x; id_loc=loc} ns = 
  try find_psymbol ns x 
  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
284
let specialize_psymbol x env =
285
  let s = find_psymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
286 287 288
  let env = Htv.create 17 in
  s, List.map (specialize env) s.ps_scheme

289 290
(** Typing types *)

291
let rec qloc = function
292
  | Qident x -> x.id_loc
293
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc
294 295 296

(* parsed types -> intermediate types *)
let rec dty env = function
297
  | PPTtyvar {id=x} -> 
298
      Tyvar (find_user_type_var x env)
299
  | PPTtyapp (p, x) ->
300
      let loc = qloc x in
301
      let s, tv = specialize_tysymbol x env in
302 303 304 305 306 307 308 309 310 311 312 313 314 315
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
      Tyapp (s, List.map (dty env) p)

(* intermediate types -> types *)
let rec ty = function
  | Tyvar { type_val = Some t } ->
      ty t
  | Tyvar { tvsymbol = tv } ->
      Ty.ty_var tv
  | Tyapp (s, tl) ->
      Ty.ty_app s (List.map ty tl)

316
(** Typing terms and formulas *)
317 318 319 320

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

and dterm_node =
321
  | Tvar of string
322 323 324 325 326 327 328
  | 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
329
  | Fquant of quant * string * dty * dfmla
330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
  | 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
  | _ -> assert false 

345 346 347 348 349
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
350 351 352 353 354 355
  | 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) *)
356 357 358 359
      let s, tyl, ty = specialize_fsymbol x env in
      let n = List.length tyl in
      if n > 0 then error ~loc (BadNumberOfArguments (s.fs_name, 0, n));
      Tapp (s, []), ty
360
  | PPapp (x, tl) ->
361 362 363
      let s, tyl, ty = specialize_fsymbol x env in
      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
364 365 366
  | _ ->
      assert false (*TODO*)

367 368 369 370 371 372 373 374 375 376 377 378 379
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)
  | PPinfix _ ->
      error ~loc:e.pp_loc PredicateExpected
  | PPif (a, b, c) ->
      Fif (dfmla env a, dfmla env b, dfmla env c)  
380
  | PPforall ({id=x}, ty, _, a) -> (* TODO: triggers *)
381
      let ty = dty env ty in
382 383 384
      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 *)
385
      let ty = dty env ty in
386 387
      let env = { env with dvars = M.add x ty env.dvars } in
      Fquant (Fexists, x, ty, dfmla env a)
388
  | PPapp (x, tl) ->
389
      let s, tyl = specialize_psymbol x env in
390 391
      let tl = dtype_args s.ps_name e.pp_loc env tyl tl in
      Fapp (s, tl)
392 393
  | _ ->
      assert false (*TODO*)
394

395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418
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)
  | Tapp (s, tl) ->
      t_app s (List.map (term env) tl) (ty t.dt_ty)
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
419 420
  | _ ->
      assert false (* TODO *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
421

422 423 424 425 426 427 428 429 430 431 432
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)
433
  | Fquant (q, x, t, f1) ->
434 435
      (* TODO: shouldn't we localize this ident? *)
      let v = create_vsymbol (id_fresh x x) (ty t) in
436 437 438 439 440
      let env = M.add x v env in
      f_quant q v (fmla env f1)
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)

441

442
(** Typing declarations, that is building environments. *)
443 444 445

open Ptree

446
let add_type loc sl {id=id} th =
447
  let ns = get_namespace th in
448
  if mem_tysymbol ns id then error ~loc (ClashType id);
449
  let tyvars = ref M.empty in
450
  let add_ty_var {id=x} =
451
    if M.mem x !tyvars then error ~loc (BadTypeArity x);
452 453
    (* TODO: shouldn't we localize this ident? *)
    let v = id_user x x loc in
454 455
    tyvars := M.add x v !tyvars;
    v
456
  in
457
  let vl = List.map add_ty_var sl in
458 459 460
  (* TODO: add the theory name to the long name *)
  let v = id_user id id loc in
  let ty = create_tysymbol v vl None in
461
  add_decl th (Dtype [ty, Ty_abstract])
462

463 464 465 466
let add_function loc pl t th {id=id} =
  let ns = get_namespace th in
  if mem_fsymbol ns id then error ~loc (Clash id);
  let denv = create_denv th in
467
  let pl = List.map (dty denv) pl and t = dty denv t in
468
  let pl = List.map ty pl and t = ty t in
469 470 471
  (* TODO: add the theory name to the long name *)
  let v = id_user id id loc in
  let s = create_fsymbol v (pl, t) false in
472
  add_decl th (Dlogic [Lfunction (s, None)])
473

474 475 476 477
let add_predicate loc pl th {id=id} =
  let ns = get_namespace th in
  if mem_psymbol ns id then error ~loc (Clash id);
  let denv = create_denv th in
478
  let pl = List.map (dty denv) pl in
479
  let pl = List.map ty pl in
480 481 482
  (* TODO: add the theory name to the long name *)
  let v = id_user id id loc in
  let s = create_psymbol v pl in
483
  add_decl th (Dlogic [Lpredicate (s, None)])
484

485 486 487
let fmla env f =
  let denv = create_denv env in
  let f = dfmla denv f in
488
  fmla M.empty f
489 490 491 492

let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
493
  term M.empty t
494 495 496 497 498

let axiom loc s f env =
  ignore (fmla env f);
  env

499
(***
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
500 501 502 503
let uses_theory env (as_t, q) =
  let loc = qloc q in
  let rec find_theory q = match q with
    | Qident t -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
504
	t.id, find_local_theory t env
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
505 506 507 508 509
    | Qdot (q, t) -> 
	let _, env = find_theory q in t.id, find_local_theory t env
  in
  let id, th = find_theory q in
  let id = match as_t with None -> id | Some x -> x.id in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
510
  if M.mem id (self env).theories then error ~loc (AlreadyTheory id);
511
  add_theory id th env
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
512 513 514 515

let open_theory t env =
  let loc = t.id_loc and id = t.id in
  if not (M.mem id env.theories) then error ~loc (UnboundTheory id);
516 517 518 519 520 521
  let th = M.find id env.theories in
  let open_map m1 m2 = M.fold M.add m1 m2 in
  { tysymbols = open_map th.tysymbols env.tysymbols;
    fsymbols  = open_map th.fsymbols  env.fsymbols;
    psymbols  = open_map th.psymbols  env.psymbols;
    theories  = open_map th.theories  env.theories }
522
***)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
523

524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557
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
  let file = match q with
    | Qident f -> find_in_loadpath env f
    | Qdot (p, f) -> let dir = locate_dir p in Filename.concat dir f.id
  in
  let file = file ^ ".why" in
  if not (Sys.file_exists file) then error ~loc:(qloc q) (UnboundFile file);
  file

558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581
type loaded_theory = {
  parsed : Ptree.theory;
  mutable typed : Theory.t option;
}

let loaded_theories = Hashtbl.create 17 (* file -> theory -> loaded_theory *)

(* parse file and store all theories into parsed_theories *)
let load_theories file =
  if not (Hashtbl.mem loaded_theories file) then begin
    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;
    let h = Hashtbl.create 17 in
    Hashtbl.add loaded_theories file h;
    List.iter 
      (fun pt -> 
	 Hashtbl.add h pt.th_name.id { parsed = pt; typed = None }) 
      tl
  end

let rec find_theory env q = match q with
582
  | Qident id -> 
583
      (* local theory *)
584 585 586 587 588
      begin 
	try M.find id.id env.theories 
	with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id) 
      end
  | Qdot (f, id) ->
589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605
      (* theory in file f *)
      let file = locate_file env f in
      load_theories file;
      let h = Hashtbl.find loaded_theories file in
      try 
	let t = Hashtbl.find h id.id in
	match t.typed with
	  | Some th -> 
	      th
	  | None -> 
	      let th = type_theory env id.id t.parsed in 
	      t.typed <- Some th; 
	      th
      with Not_found ->
	error ~loc:id.id_loc (UnboundTheory id.id);

and type_theory env id pt =
606 607
  (* TODO: shouldn't we localize this ident? *)
  let n = id_fresh id id in
608 609 610 611 612
  let th = create_theory n in
  let th = add_decls env th pt.th_decl in
  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
613

614
and add_decl env th = function
615
  | TypeDecl (loc, sl, s) ->
616
      add_type loc sl s th
617
  | Logic (loc, ids, PPredicate pl) ->
618
      List.fold_left (add_predicate loc pl) th ids
619
  | Logic (loc, ids, PFunction (pl, t)) ->
620
      List.fold_left (add_function loc pl t) th ids
621
  | Axiom (loc, s, f) ->
622
      axiom loc s f th
623
  | Use (loc, use) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
624 625 626
      let t = find_theory env use.use_theory in
      let n = match use.use_as with 
	| None -> t.t_name
627
	| Some x -> id_user x.id x.id loc
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
      in
      begin match use.use_imp_exp with
	| 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
      end
643 644 645 646
  | Namespace (_, {id=id; id_loc=loc}, dl) ->
      let ns = get_namespace th in
      if mem_namespace ns id then error ~loc (ClashNamespace id);
      let th = open_namespace th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
647
      let th = add_decls env th dl in
648
      let n = id_user id id loc in
649
      close_namespace th n ~import:false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
650 651 652 653 654
  | AlgType _ 
  | Goal _ 
  | Function_def _ 
  | Predicate_def _ 
  | Inductive_def _ ->
655
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
656

657 658 659 660
let add_theory env pt =
  let id = pt.th_name.id in
  if M.mem id env.theories then error ~loc:pt.th_loc (ClashTheory id);
  let t = type_theory env id pt in
661
  { env with theories = M.add id t env.theories }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
662

663 664 665 666 667
(*
Local Variables: 
compile-command: "make -C .. test"
End: 
*)