pgm_env.mli 1.85 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7 8 9 10 11 12 13 14 15 16 17 18
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  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
open Why3
21
open Theory
22
open Pgm_module
23

24
type t
25

26
val get_env : t -> Env.env
27

28
type module_file = Theory.theory Util.Mstr.t * Pgm_module.t Util.Mstr.t
29 30

type retrieve_module = t -> string -> in_channel -> module_file
31

32
val create : Env.env -> retrieve_module -> t
33

34
exception ModuleNotFound of string list * string
35

36 37 38
val find_module : t -> string list -> string -> Pgm_module.t
  (** [find_module e p n] finds the module named [p.n] in environment [e]
      @raise ModuleNotFound if module not present in env [e] *)