typing.ml 18 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 Ty
24
open Term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
25
open Ptree
26
open Theory
27

28 29 30
(** errors *)

type error = 
31
  | Message of string
32 33
  | ClashType of string
  | BadTypeArity of string
34
  | UnboundType of string
35
  | TypeArity of qualid * int * int
36
  | Clash of string
37 38
  | PredicateExpected
  | TermExpected
39
  | UnboundSymbol of string
40 41 42
  | TermExpectedType of (formatter -> unit) * (formatter -> unit) 
      (* actual / expected *)
  | BadNumberOfArguments of Name.t * int * int 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
43
  | ClashTheory of string
44
  | ClashNamespace of string
45
  | UnboundTheory of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
46
  | AlreadyTheory of string
47
  | UnboundNamespace of string
48 49 50 51
  | UnboundFile of string
  | UnboundDir of string
  | AmbiguousPath of string * string
  | NotInLoadpath of string
52 53 54 55 56 57 58

exception Error of error

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

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

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

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

(** typing using destructive type variables 
123

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

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

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

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

159 160
let create_type_var =
  let t = ref 0 in
161
  fun ~user tv -> 
162
    incr t; 
163
    { tag = !t; user = user; tvsymbol = tv; type_val = None }
164 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

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

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

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

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

208 209 210 211 212 213 214 215
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
    let v = create_type_var ~user:true (Name.from_string x) in
    Hashtbl.add env.utyvars x v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
216 217 218 219
(* Specialize *)

module Htv = Hashtbl.Make(Name)

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

234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256
(** 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)

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

275 276 277 278 279 280 281
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
282
let specialize_psymbol x env =
283
  let s = find_psymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
284 285 286
  let env = Htv.create 17 in
  s, List.map (specialize env) s.ps_scheme

287 288
(** Typing types *)

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

(* parsed types -> intermediate types *)
let rec dty env = function
295
  | PPTtyvar {id=x} -> 
296
      Tyvar (find_user_type_var x env)
297
  | PPTtyapp (p, x) ->
298
      let loc = qloc x in
299
      let s, tv = specialize_tysymbol x env in
300 301 302 303 304 305 306 307 308 309 310 311 312 313
      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)

314
(** Typing terms and formulas *)
315 316 317 318

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

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

343 344 345 346 347
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
348 349 350 351 352 353
  | 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) *)
354 355 356 357
      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
358
  | PPapp (x, tl) ->
359 360 361
      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
362 363 364
  | _ ->
      assert false (*TODO*)

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

393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416
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
417 418
  | _ ->
      assert false (* TODO *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
419

420 421 422 423 424 425 426 427 428 429 430
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)
431 432 433 434 435 436 437
  | Fquant (q, x, t, f1) ->
      let v = create_vsymbol (Name.from_string x) (ty t) in
      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)

438

439
(** Typing declarations, that is building environments. *)
440 441 442

open Ptree

443 444 445
let add_type loc sl s th =
  let ns = get_namespace th in
  if mem_tysymbol ns s.id then error ~loc (ClashType s.id);
446
  let tyvars = ref M.empty in
447
  let add_ty_var {id=x} =
448
    if M.mem x !tyvars then error ~loc (BadTypeArity x);
449
    let v = Name.from_string x in
450 451
    tyvars := M.add x v !tyvars;
    v
452
  in
453
  let vl = List.map add_ty_var sl in
454
  let ty = Ty.create_tysymbol (Name.from_string s.id) vl None in
455
  add_decl th (Dtype [ty, Ty_abstract])
456

457 458 459 460
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
461
  let pl = List.map (dty denv) pl and t = dty denv t in
462
  let pl = List.map ty pl and t = ty t in
463
  let s = create_fsymbol (Name.from_string id) (pl, t) false in
464
  add_decl th (Dlogic [Lfunction (s, None)])
465

466 467 468 469
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
470
  let pl = List.map (dty denv) pl in
471
  let pl = List.map ty pl in
472
  let s = create_psymbol (Name.from_string id) pl in
473
  add_decl th (Dlogic [Lpredicate (s, None)])
474

475 476 477
let fmla env f =
  let denv = create_denv env in
  let f = dfmla denv f in
478
  fmla M.empty f
479 480 481 482

let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
483
  term M.empty t
484 485 486 487 488

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

489
(***
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
490 491 492 493
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
494
	t.id, find_local_theory t env
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
495 496 497 498 499
    | 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
500
  if M.mem id (self env).theories then error ~loc (AlreadyTheory id);
501
  add_theory id th env
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
502 503 504 505

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);
506 507 508 509 510 511
  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 }
512
***)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
513

514 515 516 517 518 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 545 546 547 548 549 550 551 552 553 554 555 556
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

let find_theory env q = match q with
  | Qident id -> 
      begin 
	try M.find id.id env.theories 
	with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id) 
      end
  | Qdot (f, id) ->
      let f = locate_file env f in
      assert false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
557 558

let rec add_decl env th = function
559
  | TypeDecl (loc, sl, s) ->
560
      add_type loc sl s th
561
  | Logic (loc, ids, PPredicate pl) ->
562
      List.fold_left (add_predicate loc pl) th ids
563
  | Logic (loc, ids, PFunction (pl, t)) ->
564
      List.fold_left (add_function loc pl t) th ids
565
  | Axiom (loc, s, f) ->
566
      axiom loc s f th
567
  | Use (loc, use) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586
      let t = find_theory env use.use_theory in
      let n = match use.use_as with 
	| None -> t.t_name
	| Some x -> Name.from_string x.id
      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
587 588 589 590
  | 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
591
      let th = add_decls env th dl in
592 593
      let n = Name.from_string id in
      close_namespace th n ~import:false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
594 595 596 597 598
  | AlgType _ 
  | Goal _ 
  | Function_def _ 
  | Predicate_def _ 
  | Inductive_def _ ->
599
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
600

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

603
and type_theory env id pt =
604 605
  let n = Name.from_string id in
  let th = create_theory n in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
606
  let th = add_decls env th pt.th_decl in
607 608 609 610 611 612
  close_theory th

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
613
  { env with theories = M.add id t env.theories }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
614

615 616 617 618 619
(*
Local Variables: 
compile-command: "make -C .. test"
End: 
*)