typing.ml 22.7 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 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
(****

  | 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"

****)


133 134
(** Environments *)

135
module S = Set.Make(String)
136 137 138 139
module M = Map.Make(String)

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

let create lp = {
  loadpath = lp;
  theories = M.empty;
}
147 148

(** typing using destructive type variables 
149

150 151 152 153 154 155
    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
156

157 158 159 160 161 162 163 164 165 166 167 168 169 170
*)

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

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

185 186
let create_type_var =
  let t = ref 0 in
187
  fun ~user tv -> 
188
    incr t; 
189
    { tag = !t; user = user; tvsymbol = tv; type_val = None }
190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217

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

218
(** Destructive typing environment, that is
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
219
    environment + local variables.
220
    It is only local to this module and created with [create_denv] below. *)
221 222

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

228 229
let create_denv th = { 
  th = th; 
230 231 232
  utyvars = Hashtbl.create 17; 
  dvars = M.empty;
}
233

234 235 236 237
let find_user_type_var x env =
  try
    Hashtbl.find env.utyvars x
  with Not_found ->
238
    (* TODO: shouldn't we localize this ident? *)
239 240
    let v = create_tvsymbol (id_fresh x) in
    let v = create_type_var ~user:true v in
241 242 243
    Hashtbl.add env.utyvars x v;
    v
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
244 245
(* Specialize *)

246
module Htv = Hid
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
247

248
let find_type_var env tv =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
249 250 251 252 253 254 255
  try
    Htv.find env tv
  with Not_found ->
    let v = create_type_var ~user:false tv in
    Htv.add env tv v;
    v
 
256
let rec specialize env t = match t.ty_node with
257
  | Ty.Tyvar tv -> 
258
      Tyvar (find_type_var env tv)
259 260
  | Ty.Tyapp (s, tl) ->
      Tyapp (s, List.map (specialize env) tl)
261

262 263 264
(** generic find function using a path *)

let find_local_namespace {id=x; id_loc=loc} ns = 
265
  try Mnm.find x ns.ns_ns
266 267 268 269 270 271 272 273 274 275 276 277 278
  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 = 
279
  try Mnm.find x ns.ns_ts
280 281 282 283 284
  with Not_found -> error ~loc (UnboundType x)

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

285
let specialize_tysymbol x env =
286
  let s = find_tysymbol x env.th in
287
  let env = Htv.create 17 in
288
  s, List.map (find_type_var env) s.ts_args
289
	
290
let find_fsymbol {id=x; id_loc=loc} ns = 
291
  try Mnm.find x ns.ns_fs
292 293 294 295 296
  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
297
let specialize_fsymbol x env =
298
  let s = find_fsymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
299 300 301 302
  let tl, t = s.fs_scheme in
  let env = Htv.create 17 in
  s, List.map (specialize env) tl, specialize env t

303
let find_psymbol {id=x; id_loc=loc} ns = 
304
  try Mnm.find x ns.ns_ps
305 306 307 308 309
  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
310
let specialize_psymbol x env =
311
  let s = find_psymbol x env.th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
312 313 314
  let env = Htv.create 17 in
  s, List.map (specialize env) s.ps_scheme

315 316
(** Typing types *)

317
let rec qloc = function
318
  | Qident x -> x.id_loc
319
  | Qdot (m, x) -> Loc.join (qloc m) x.id_loc
320 321 322

(* parsed types -> intermediate types *)
let rec dty env = function
323
  | PPTtyvar {id=x} -> 
324
      Tyvar (find_user_type_var x env)
325
  | PPTtyapp (p, x) ->
326
      let loc = qloc x in
327
      let s, tv = specialize_tysymbol x env in
328 329 330 331 332 333 334 335 336 337 338 339 340 341
      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)

342
(** Typing terms and formulas *)
343 344 345 346

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

and dterm_node =
347
  | Tvar of string
348 349 350 351 352 353 354
  | 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
355
  | Fquant of quant * string * dty * dfmla
356 357 358 359 360 361 362 363 364 365 366 367 368 369 370
  | 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 

371 372 373 374 375
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
376 377 378 379 380 381
  | 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) *)
382 383 384 385
      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
386
  | PPapp (x, tl) ->
387 388 389
      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
390 391 392
  | _ ->
      assert false (*TODO*)

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

421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444
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
445 446
  | _ ->
      assert false (* TODO *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
447

448 449 450 451 452 453 454 455 456 457 458
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)
459
  | Fquant (q, x, t, f1) ->
460
      (* TODO: shouldn't we localize this ident? *)
461
      let v = create_vsymbol (id_fresh x) (ty t) in
462 463 464 465 466
      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)

467

468
(** Typing declarations, that is building environments. *)
469 470 471

open Ptree

472 473 474 475 476 477 478 479
let add_types loc dl th =
  let def = 
    List.fold_left 
      (fun def d -> 
	 let id = d.td_ident in
	 if M.mem id.id def then error ~loc:id.id_loc (ClashType id.id);
	 M.add id.id d def) 
      M.empty dl 
480
  in
481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496
  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);
497
	     let i = create_tvsymbol (id_user v.id v.id_loc) in
498 499 500 501
	     Hashtbl.add vars v.id i;
	     i)
	  d.td_params 
      in
502
      let id = id_user id d.td_ident.id_loc in
503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536
      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
  M.iter (fun x _ -> ignore (visit x)) def;
  let decl d = 
    (match Hashtbl.find tysymbols d.td_ident.id with
       | None -> assert false
       | Some ts -> ts),
    (match d.td_def with
537
       | TDabstract | TDalias _ -> Tabstract
538 539 540
       | TDalgebraic _ -> assert false (*TODO*))
  in
  let dl = List.map decl dl in
541
  add_decl th (create_type dl)
542

543 544
let add_function loc pl t th {id=id} =
  let ns = get_namespace th in
545
  if Mnm.mem id ns.ns_fs then error ~loc (Clash id);
546
  let denv = create_denv th in
547
  let pl = List.map (dty denv) pl and t = dty denv t in
548
  let pl = List.map ty pl and t = ty t in
549
  (* TODO: add the theory name to the long name *)
550
  let v = id_user id loc in
551
  let s = create_fsymbol v (pl, t) false in
552
  add_decl th (create_logic [Lfunction (s, None)])
553

554 555
let add_predicate loc pl th {id=id} =
  let ns = get_namespace th in
556
  if Mnm.mem id ns.ns_ps then error ~loc (Clash id);
557
  let denv = create_denv th in
558
  let pl = List.map (dty denv) pl in
559
  let pl = List.map ty pl in
560
  (* TODO: add the theory name to the long name *)
561
  let v = id_user id loc in
562
  let s = create_psymbol v pl in
563
  add_decl th (create_logic [Lpredicate (s, None)])
564

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
565 566 567 568 569 570 571 572 573
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 =
  let fsymbols = Hashtbl.create 17 in
  let psymbols = Hashtbl.create 17 in
  (* 1. create all symbols and make an environment with these symbols *)
  let create_symbol th d = 
    let id = d.ld_ident.id in
574
    let v = id_user id loc in
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
575 576 577 578 579 580 581
    let denv = create_denv th in
    let type_ty (_,t) = ty (dty denv t) in
    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;
582
	  add_decl th (create_logic [Lpredicate (ps, None)])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
583 584 585 586
      | Some t -> (* function *)
	  let t = type_ty (None, t) in
	  let fs = create_fsymbol v (pl, t) false in
	  Hashtbl.add fsymbols id fs;
587
	  add_decl th (create_logic [Lfunction (fs, None)])
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
588 589 590 591 592 593 594 595 596 597 598 599
  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
    let denv = List.fold_left dadd_var (create_denv th') d.ld_params in
    let create_var (x, _) ty = 
      let id = match x with 
600 601
	| 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
602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631
      in
      create_vsymbol id ty
    in
    match d.ld_type with
    | None -> (* predicate *)
	let ps = Hashtbl.find psymbols id in
	let def = match d.ld_def with
	  | None -> 
	      None
	  | Some f -> 
	      let f = dfmla denv f in
	      let vl = List.map2 create_var d.ld_params ps.ps_scheme in
	      let env = env_of_vsymbol_list vl in
	      Some (vl, fmla env f)
	in
	Lpredicate (ps, def)
    | Some t -> (* function *)
	let fs = Hashtbl.find fsymbols id in
	let def = match d.ld_def with
	  | None -> 
	      None
	  | Some t -> 
	      let t = dterm denv t in
	      let vl = List.map2 create_var d.ld_params (fst fs.fs_scheme) in
	      let env = env_of_vsymbol_list vl in
	      Some (vl, term env t)
	in
	Lfunction (fs, def)
  in
  let dl = List.map type_decl dl in
632
  add_decl th (create_logic dl)
633 634 635 636

let term env t =
  let denv = create_denv env in
  let t = dterm denv t in
637
  term M.empty t
638

Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
639 640 641 642 643
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
644 645 646
let add_prop k loc s f th =
  let f = fmla th f in
  try
647
    add_decl th (create_prop k (id_user s.id loc) f)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
648 649
  with ClashSymbol _ ->
    error ~loc (Clash s.id)
650

651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676
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
677 678 679 680 681 682 683 684 685
  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
686

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

(* parse file and store all theories into parsed_theories *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
690 691 692 693 694 695 696
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
697

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
698
let prop_kind = function
699 700 701
  | Kaxiom -> Paxiom
  | Kgoal -> Pgoal
  | Klemma -> Plemma
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
702

703
let rec find_theory env q = match q with
704
  | Qident id -> 
705
      (* local theory *)
706 707 708 709 710
      begin 
	try M.find id.id env.theories 
	with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id) 
      end
  | Qdot (f, id) ->
711 712
      (* theory in file f *)
      let file = locate_file env f in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
713 714 715 716 717 718 719 720 721 722 723 724
      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;
725
      let h = Hashtbl.find loaded_theories file in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
726 727
      try Hashtbl.find h id.id
      with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id)
728 729

and type_theory env id pt =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
730
  (* TODO: use long name *)
731
  let n = id_user id.id id.id_loc in
732
  let th = create_theory n in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
733
  let th = add_decls env th pt.pt_decl in
734 735 736
  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
737

738
and add_decl env th = function
739 740
  | TypeDecl (loc, dl) ->
      add_types loc dl th
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
741 742
  | Logic (loc, dl) ->
      add_logics loc dl th
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
743 744
  | Prop (loc, k, s, f) ->
      add_prop (prop_kind k) loc s f th
745
  | Use (loc, use) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
746 747
      let t = find_theory env use.use_theory in
      let n = match use.use_as with 
748 749
	| None -> t.th_name.id_short
	| Some x -> x.id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
750
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
751
      begin try match use.use_imp_exp with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
752 753 754 755 756 757 758 759 760 761 762 763
	| 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
764 765
      with Theory.ClashSymbol s ->
	error ~loc (Clash s)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
766
      end
767 768
  | Namespace (_, {id=id; id_loc=loc}, dl) ->
      let ns = get_namespace th in
769
      if Mnm.mem id ns.ns_ns then error ~loc (ClashNamespace id);
770
      let th = open_namespace th in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
771
      let th = add_decls env th dl in
772
      close_namespace th id ~import:false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
773
  | Inductive_def _ ->
774
      assert false (*TODO*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
775

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
776 777 778
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);
779
  let t = type_theory env id pt in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
780 781 782 783 784
  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
785

786 787
(*
Local Variables: 
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
788
compile-command: "make -C ../.. test"
789 790
End: 
*)