typing.ml 23.5 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
55 56 57 58 59 60 61

exception Error of error

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
115

116 117
(** Environments *)

118
module S = Set.Make(String)
119 120 121 122
module M = Map.Make(String)

type env = {
  loadpath : string list;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
123
  theories : theory M.t; (* local theories *)
124 125 126 127 128 129
}

let create lp = {
  loadpath = lp;
  theories = M.empty;
}
130 131

(** typing using destructive type variables 
132

133 134 135 136 137 138
    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
139

140 141 142 143 144 145 146 147 148 149 150 151 152 153
*)

(** 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;
}
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 } ->
159
      fprintf fmt "'%s" v.id_short
160
  | Tyapp (s, []) ->
161
      fprintf fmt "%s" s.ts_name.id_short
162
  | Tyapp (s, [t]) -> 
163
      fprintf fmt "%a %s" print_dty t s.ts_name.id_short
164
  | Tyapp (s, l) -> 
165 166
      fprintf fmt "(%a) %s" 
	(print_list comma print_dty) l s.ts_name.id_short
167

168 169
let create_type_var =
  let t = ref 0 in
170
  fun ~user tv -> 
171
    incr t; 
172
    { tag = !t; user = user; tvsymbol = tv; type_val = None }
173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200

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

201
(** Destructive typing environment, that is
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
202
    environment + local variables.
203
    It is only local to this module and created with [create_denv] below. *)
204 205

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

211 212
let create_denv th = { 
  th = th; 
213 214 215
  utyvars = Hashtbl.create 17; 
  dvars = M.empty;
}
216

217 218 219 220
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
221
    (* TODO: shouldn't we localize this ident? *)
222 223
    let v = create_tvsymbol (id_fresh x) in
    let v = create_type_var ~user:true v in
224 225 226
    Hashtbl.add env.utyvars x v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
227 228
(* Specialize *)

229
module Htv = Hid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
230

231
let find_type_var env tv =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
232 233 234 235 236 237 238
  try
    Htv.find env tv
  with Not_found ->
    let v = create_type_var ~user:false tv in
    Htv.add env tv v;
    v
 
239
let rec specialize env t = match t.ty_node with
240
  | Ty.Tyvar tv -> 
241
      Tyvar (find_type_var env tv)
242 243
  | Ty.Tyapp (s, tl) ->
      Tyapp (s, List.map (specialize env) tl)
244

245 246 247
(** generic find function using a path *)

let find_local_namespace {id=x; id_loc=loc} ns = 
248
  try Mnm.find x ns.ns_ns
249 250 251 252 253 254 255 256 257 258 259 260 261
  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 = 
262
  try Mnm.find x ns.ns_ts
263 264 265 266 267
  with Not_found -> error ~loc (UnboundType x)

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

268
let specialize_tysymbol x env =
269
  let s = find_tysymbol x env.th in
270
  let env = Htv.create 17 in
271
  s, List.map (find_type_var env) s.ts_args
272
	
273
let find_fsymbol {id=x; id_loc=loc} ns = 
274
  try Mnm.find x ns.ns_fs
275 276 277 278 279
  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
egalite  
Jean-Christophe Filliâtre committed
280
let specialize_fsymbol s =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
281 282 283 284
  let tl, t = s.fs_scheme in
  let env = Htv.create 17 in
  s, List.map (specialize env) tl, specialize env t

285
let find_psymbol {id=x; id_loc=loc} ns = 
286
  try Mnm.find x ns.ns_ps
287 288 289 290 291
  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
egalite  
Jean-Christophe Filliâtre committed
292
let specialize_psymbol s =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
293 294 295
  let env = Htv.create 17 in
  s, List.map (specialize env) s.ps_scheme

296 297
(** Typing types *)

298
let rec qloc = function
299
  | Qident x -> x.id_loc
300
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc
301 302

(* parsed types -> intermediate types *)
303 304 305 306 307

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)

308
let rec dty env = function
309
  | PPTtyvar {id=x} -> 
310
      Tyvar (find_user_type_var x env)
311
  | PPTtyapp (p, x) ->
312
      let loc = qloc x in
313
      let ts, tv = specialize_tysymbol x env in
314 315 316
      let np = List.length p in
      let a = List.length tv in
      if np <> a then error ~loc (TypeArity (x, a, np));
317 318 319 320 321 322 323 324
      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
325 326

(* intermediate types -> types *)
327
let rec ty_of_dty = function
328
  | Tyvar { type_val = Some t } ->
329
      ty_of_dty t
330 331 332
  | Tyvar { tvsymbol = tv } ->
      Ty.ty_var tv
  | Tyapp (s, tl) ->
333
      Ty.ty_app s (List.map ty_of_dty tl)
334

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

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

and dterm_node =
340
  | Tvar of string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
341
  | Tconst of constant
342 343 344 345 346 347 348
  | 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
349
  | Fquant of quant * string * dty * dfmla
350 351 352 353 354 355 356 357 358 359 360 361 362 363
  | 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

364 365 366 367 368
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
369 370 371 372 373 374
  | 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
375 376
      let s = find_fsymbol x env.th in
      let s, tyl, ty = specialize_fsymbol s in
377 378 379
      let n = List.length tyl in
      if n > 0 then error ~loc (BadNumberOfArguments (s.fs_name, 0, n));
      Tapp (s, []), ty
380
  | PPapp (x, tl) ->
Jean-Christophe Filliâtre's avatar
egalite  
Jean-Christophe Filliâtre committed
381 382
      let s = find_fsymbol x env.th in
      let s, tyl, ty = specialize_fsymbol s in
383 384
      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
385
  | PPconst (ConstInt _ as c) ->
386
      Tconst c, Tyapp (Ty.ts_int, [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
387
  | PPconst (ConstReal _ as c) ->
388
      Tconst c, Tyapp (Ty.ts_real, [])
389 390 391 392 393 394 395 396 397
  | 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
398

399 400 401 402 403 404 405 406 407 408 409
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)  
410
  | PPforall ({id=x}, ty, _, a) -> (* TODO: triggers *)
411
      let ty = dty env ty in
412 413 414
      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 *)
415
      let ty = dty env ty in
416 417
      let env = { env with dvars = M.add x ty env.dvars } in
      Fquant (Fexists, x, ty, dfmla env a)
418
  | PPapp (x, tl) ->
Jean-Christophe Filliâtre's avatar
egalite  
Jean-Christophe Filliâtre committed
419 420
      let s = find_psymbol x env.th in
      let s, tyl = specialize_psymbol s in
421 422
      let tl = dtype_args s.ps_name e.pp_loc env tyl tl in
      Fapp (s, tl)
423 424 425 426 427 428 429 430 431 432
  | 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
433

434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455
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
456
  | Tconst c ->
457
      t_const c (ty_of_dty t.dt_ty)
458
  | Tapp (s, tl) ->
459
      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
460 461
  | _ ->
      assert false (* TODO *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
462

463 464 465 466 467 468 469 470 471 472 473
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)
474
  | Fquant (q, x, t, f1) ->
475
      (* TODO: shouldn't we localize this ident? *)
476
      let v = create_vsymbol (id_fresh x) (ty_of_dty t) in
477
      let env = M.add x v env in
478
      f_quant q [v] [] (fmla env f1)
479 480 481
  | Fapp (s, tl) ->
      f_app s (List.map (term env) tl)

482

483
(** Typing declarations, that is building environments. *)
484 485 486

open Ptree

487
let add_types loc dl th =
488
  let ns = get_namespace th in
489 490 491 492
  let def = 
    List.fold_left 
      (fun def d -> 
	 let id = d.td_ident in
493 494
	 if M.mem id.id def || Mnm.mem id.id ns.ns_ts then 
	   error ~loc:id.id_loc (ClashType id.id);
495 496
	 M.add id.id d def) 
      M.empty dl 
497
  in
498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513
  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);
514
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
515 516 517 518
	     Hashtbl.add vars v.id i;
	     i)
	  d.td_params 
      in
519
      let id = id_user id d.td_ident.id_loc in
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
      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
548 549 550 551 552 553
  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
554
  let decl d = 
555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579
    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
580 581
  in
  let dl = List.map decl dl in
582
  add_decl th (create_type dl)
583

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
584 585 586 587
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
588
  let ns = get_namespace th in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
589 590
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
591
  let denvs = Hashtbl.create 17 in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
592 593 594
  (* 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
595
    if Hashtbl.mem denvs id || Mnm.mem id ns.ns_fs then error ~loc (Clash id);
596
    let v = id_user id loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
597
    let denv = create_denv th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
598
    Hashtbl.add denvs id denv;
599
    let type_ty (_,t) = ty_of_dty (dty denv t) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
600 601 602 603 604
    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;
605
	  add_decl th (create_logic [Lpredicate (ps, None)])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
606 607 608 609
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
	  let fs = create_fsymbol v (pl, t) false in
	  Hashtbl.add fsymbols id fs;
610
	  add_decl th (create_logic [Lfunction (fs, None)])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
611 612 613 614 615 616 617 618 619
  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
620 621 622
    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
623 624
    let create_var (x, _) ty = 
      let id = match x with 
625 626
	| 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
627 628 629
      in
      create_vsymbol id ty
    in
630
    let mk_vlist = List.map2 create_var d.ld_params in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
631 632 633
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
634
	begin match d.ld_def with
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
635
	  | None -> 
636
              Lpredicate (ps, None)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
637 638
	  | Some f -> 
	      let f = dfmla denv f in
639
	      let vl = mk_vlist ps.ps_scheme in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
640
	      let env = env_of_vsymbol_list vl in
641 642
              make_pdef ps vl (fmla env f)
        end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
643
    | Some ty -> (* function *)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
644
	let fs = Hashtbl.find fsymbols id in
645
	begin match d.ld_def with
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
646
	  | None -> 
647
              Lfunction (fs, None)
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
648
	  | Some t -> 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
649
	      let loc = t.pp_loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
650
	      let t = dterm denv t in
651
	      let vl = mk_vlist (fst fs.fs_scheme) in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
652
	      let env = env_of_vsymbol_list vl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
653 654 655 656 657 658
              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))))
659
        end
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
660 661
  in
  let dl = List.map type_decl dl in
662
  add_decl th (create_logic dl)
663

664

665 666 667
let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
668
  term M.empty t
669

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
670 671 672 673 674
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
675 676 677
let add_prop k loc s f th =
  let f = fmla th f in
  try
678
    add_decl th (create_prop k (id_user s.id loc) f)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
679 680
  with ClashSymbol _ ->
    error ~loc (Clash s.id)
681

682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707
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
708 709 710 711 712 713 714 715 716
  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
717

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

(* parse file and store all theories into parsed_theories *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
721 722 723 724 725 726 727
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
728

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
729
let prop_kind = function
730 731 732
  | Kaxiom -> Paxiom
  | Kgoal -> Pgoal
  | Klemma -> Plemma
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
733

734
let rec find_theory env q = match q with
735
  | Qident id -> 
736
      (* local theory *)
737 738 739 740 741
      begin 
	try M.find id.id env.theories 
	with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id) 
      end
  | Qdot (f, id) ->
742 743
      (* theory in file f *)
      let file = locate_file env f in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
744 745 746 747 748 749 750 751 752 753 754 755
      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;
756
      let h = Hashtbl.find loaded_theories file in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
757 758
      try Hashtbl.find h id.id
      with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id)
759 760

and type_theory env id pt =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
761
  (* TODO: use long name *)
762
  let n = id_user id.id id.id_loc in
763
  let th = create_theory n in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
764
  let th = add_decls env th pt.pt_decl in
765 766 767
  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
768

769
and add_decl env th = function
770 771
  | TypeDecl (loc, dl) ->
      add_types loc dl th
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
772 773
  | Logic (loc, dl) ->
      add_logics loc dl th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
774 775
  | Prop (loc, k, s, f) ->
      add_prop (prop_kind k) loc s f th
776
  | Use (loc, use) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
777 778
      let t = find_theory env use.use_theory in
      let n = match use.use_as with 
779 780
	| None -> t.th_name.id_short
	| Some x -> x.id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
781
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
782
      begin try match use.use_imp_exp with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
783 784 785 786 787 788 789 790 791 792 793 794
	| 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
795 796
      with Theory.ClashSymbol s ->
	error ~loc (Clash s)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
797
      end
798 799
  | Namespace (_, {id=id; id_loc=loc}, dl) ->
      let ns = get_namespace th in
800
      if Mnm.mem id ns.ns_ns then error ~loc (ClashNamespace id);
801
      let th = open_namespace th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
802
      let th = add_decls env th dl in
803
      close_namespace th id ~import:false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
804
  | Inductive_def _ ->
805
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
806

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
807 808 809
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);
810
  let t = type_theory env id pt in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
811 812 813 814 815
  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
816

817 818 819
let list_theory env = 
  M.fold (fun _ v acc -> v::acc) env.theories []

820 821
(*
Local Variables: 
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
822
compile-command: "make -C ../.. test"
823 824
End: 
*)