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

24
type t
25

26
val get_env : t -> Env.env
27

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

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] *)