typing.ml 19 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
      fprintf fmt "but is applied to %d argument(s)@]" n
  | Clash id ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
77
      fprintf fmt "Clash with previous symbol %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) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85
      fprintf fmt "@[Symbol `%s' is applied 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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
(****

  | OpenTheory ->
      fprintf fmt "cannot open a new theory in a non-empty context"
  | CloseTheory ->
      fprintf fmt "cannot close theory: there are still unclosed namespaces"
  | NoOpenedTheory ->
      fprintf fmt "no opened theory"
  | NoOpenedNamespace ->
      fprintf fmt "no opened namespace"
  | RedeclaredIdent id ->
      fprintf fmt "cannot redeclare identifier %s" id.id_short
  | CannotInstantiate ->
      fprintf fmt "cannot instantiate a defined symbol"

****)


127 128 129 130 131 132
(** Environments *)

module M = Map.Make(String)

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

let create lp = {
  loadpath = lp;
  theories = M.empty;
}
140 141

(** typing using destructive type variables 
142

143 144 145 146 147 148
    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
149

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

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

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

178 179
let create_type_var =
  let t = ref 0 in
180
  fun ~user tv -> 
181
    incr t; 
182
    { tag = !t; user = user; tvsymbol = tv; type_val = None }
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210

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

211
(** Destructive typing environment, that is
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
212
    environment + local variables.
213
    It is only local to this module and created with [create_denv] below. *)
214 215

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

221 222
let create_denv th = { 
  th = th; 
223 224 225
  utyvars = Hashtbl.create 17; 
  dvars = M.empty;
}
226

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

238
module Htv = Hid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
239

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

254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276
(** 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)

277
let specialize_tysymbol x env =
278
  let s = find_tysymbol x env.th in
279
  let env = Htv.create 17 in
280
  s, List.map (find_type_var env) s.ts_args
281
	
282 283 284 285 286 287 288
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
289
let specialize_fsymbol x env =
290
  let s = find_fsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
291 292 293 294
  let tl, t = s.fs_scheme in
  let env = Htv.create 17 in
  s, List.map (specialize env) tl, specialize env t

295 296 297 298 299 300 301
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
302
let specialize_psymbol x env =
303
  let s = find_psymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
304 305 306
  let env = Htv.create 17 in
  s, List.map (specialize env) s.ps_scheme

307 308
(** Typing types *)

309
let rec qloc = function
310
  | Qident x -> x.id_loc
311
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc
312 313 314

(* parsed types -> intermediate types *)
let rec dty env = function
315
  | PPTtyvar {id=x} -> 
316
      Tyvar (find_user_type_var x env)
317
  | PPTtyapp (p, x) ->
318
      let loc = qloc x in
319
      let s, tv = specialize_tysymbol x env in
320 321 322 323 324 325 326 327 328 329 330 331 332 333
      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)

334
(** Typing terms and formulas *)
335 336 337 338

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

and dterm_node =
339
  | Tvar of string
340 341 342 343 344 345 346
  | 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
347
  | Fquant of quant * string * dty * dfmla
348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
  | 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 

363 364 365 366 367
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
368 369 370 371 372 373
  | 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) *)
374 375 376 377
      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
378
  | PPapp (x, tl) ->
379 380 381
      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
382 383 384
  | _ ->
      assert false (*TODO*)

385 386 387 388 389 390 391 392 393 394 395 396 397
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)  
398
  | PPforall ({id=x}, ty, _, a) -> (* TODO: triggers *)
399
      let ty = dty env ty in
400 401 402
      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 *)
403
      let ty = dty env ty in
404 405
      let env = { env with dvars = M.add x ty env.dvars } in
      Fquant (Fexists, x, ty, dfmla env a)
406
  | PPapp (x, tl) ->
407
      let s, tyl = specialize_psymbol x env in
408 409
      let tl = dtype_args s.ps_name e.pp_loc env tyl tl in
      Fapp (s, tl)
410 411
  | _ ->
      assert false (*TODO*)
412

413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436
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
437 438
  | _ ->
      assert false (* TODO *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
439

440 441 442 443 444 445 446 447 448 449 450
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)
451
  | Fquant (q, x, t, f1) ->
452 453
      (* TODO: shouldn't we localize this ident? *)
      let v = create_vsymbol (id_fresh x x) (ty t) in
454 455 456 457 458
      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)

459

460
(** Typing declarations, that is building environments. *)
461 462 463

open Ptree

464
let add_type loc sl {id=id} th =
465
  let tyvars = ref M.empty in
466
  let add_ty_var {id=x} =
467
    if M.mem x !tyvars then error ~loc (BadTypeArity x);
468 469
    (* TODO: shouldn't we localize this ident? *)
    let v = id_user x x loc in
470 471
    tyvars := M.add x v !tyvars;
    v
472
  in
473
  let vl = List.map add_ty_var sl in
474 475 476
  (* 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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
477 478 479 480 481
  try
    add_decl th (Dtype [ty, Ty_abstract])
  with Theory.ClashSymbol _ ->
    error ~loc (ClashType id)

482

483 484 485 486
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
487
  let pl = List.map (dty denv) pl and t = dty denv t in
488
  let pl = List.map ty pl and t = ty t in
489 490 491
  (* 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
492
  add_decl th (Dlogic [Lfunction (s, None)])
493

494 495 496 497
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
498
  let pl = List.map (dty denv) pl in
499
  let pl = List.map ty pl in
500 501 502
  (* TODO: add the theory name to the long name *)
  let v = id_user id id loc in
  let s = create_psymbol v pl in
503
  add_decl th (Dlogic [Lpredicate (s, None)])
504

505 506 507
let fmla env f =
  let denv = create_denv env in
  let f = dfmla denv f in
508
  fmla M.empty f
509 510 511 512

let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
513
  term M.empty t
514 515 516 517 518

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

519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544
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
545 546 547 548 549 550 551 552 553
  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
554

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

(* parse file and store all theories into parsed_theories *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
558 559 560 561 562 563 564
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
565 566

let rec find_theory env q = match q with
567
  | Qident id -> 
568
      (* local theory *)
569 570 571 572 573
      begin 
	try M.find id.id env.theories 
	with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id) 
      end
  | Qdot (f, id) ->
574 575
      (* theory in file f *)
      let file = locate_file env f in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
576 577 578 579 580 581 582 583 584 585 586 587
      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;
588
      let h = Hashtbl.find loaded_theories file in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
589 590
      try Hashtbl.find h id.id
      with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id)
591 592

and type_theory env id pt =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
593 594
  (* TODO: use long name *)
  let n = id_user id.id id.id id.id_loc in
595
  let th = create_theory n in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
596
  let th = add_decls env th pt.pt_decl in
597 598 599
  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
600

601
and add_decl env th = function
602
  | TypeDecl (loc, sl, s) ->
603
      add_type loc sl s th
604
  | Logic (loc, ids, PPredicate pl) ->
605
      List.fold_left (add_predicate loc pl) th ids
606
  | Logic (loc, ids, PFunction (pl, t)) ->
607
      List.fold_left (add_function loc pl t) th ids
608
  | Axiom (loc, s, f) ->
609
      axiom loc s f th
610
  | Use (loc, use) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
611 612
      let t = find_theory env use.use_theory in
      let n = match use.use_as with 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
613
	| None -> id_clone t.th_name
614
	| Some x -> id_user x.id x.id loc
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
615
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
616
      begin try match use.use_imp_exp with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
617 618 619 620 621 622 623 624 625 626 627 628
	| 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
629 630
      with Theory.ClashSymbol s ->
	error ~loc (Clash s)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
631
      end
632 633 634 635
  | 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
636
      let th = add_decls env th dl in
637
      let n = id_user id id loc in
638
      close_namespace th n ~import:false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
639 640 641 642 643
  | AlgType _ 
  | Goal _ 
  | Function_def _ 
  | Predicate_def _ 
  | Inductive_def _ ->
644
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
645

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
646 647 648
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);
649
  let t = type_theory env id pt in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
650 651 652 653 654
  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
655

656 657 658 659 660
(*
Local Variables: 
compile-command: "make -C .. test"
End: 
*)