rename Env.create_env_of_loadpath to Env.create_env

also add Env.get_loadpath to use for Coq realisation

doc/api.tex

@@ -184,7 +184,7 @@ loaded first.
 \begin{verbatim}
 (* builds the environment from the [loadpath] *)
 let env : Env.env =
-  Env.create_env_of_loadpath (Whyconf.loadpath main)
+  Env.create_env (Whyconf.loadpath main)
 (* loading the Alt-Ergo driver *)
 let alt_ergo_driver : Driver.driver =
   try

examples/use_api.ml

@@ -84,8 +84,7 @@ let alt_ergo : Whyconf.config_prover =
     exit 0
 
 (* builds the environment from the [loadpath] *)
-let env : Env.env =
-  Env.create_env_of_loadpath (Whyconf.loadpath main)
+let env : Env.env = Env.create_env (Whyconf.loadpath main)
 
 (* loading the Alt-Ergo driver *)
 let alt_ergo_driver : Driver.driver =

src/bench/benchrc.ml

@@ -55,7 +55,7 @@ let read_tools absf wc map (name,section) =
   let timelimit = get_int ~default:(timelimit wc_main) section "timelimit" in
   let memlimit = get_int ~default:(memlimit wc_main) section "memlimit" in
   (* env *)
-  let env = Env.create_env_of_loadpath loadpath in
+  let env = Env.create_env loadpath in
   (* transformations *)
   let transforms = get_stringl ~default:[] section "transform" in
   let lookup acc t = (Trans.lookup_transform t env, lookup_transf t)::acc in

src/bench/whybench.ml

@@ -342,7 +342,7 @@ let () =
     (Theory.create_theory (Ident.id_fresh "cmdline"))
     !opt_metas) in
 
-  let env = Env.create_env_of_loadpath !opt_loadpath in
+  let env = Env.create_env !opt_loadpath in
 
   if !opt_redo then
     begin if not (Db.is_initialized ()) then

src/core/env.ml

@@ -37,10 +37,8 @@ exception ChannelNotFound of pathname
 exception TheoryNotFound of pathname * string
 exception AmbiguousPath of filename * filename
 
-type find_channel = fformat -> pathname -> filename * in_channel
-
 type env = {
-  env_find : find_channel;
+  env_path : filename list;
   env_memo : (pathname, theory Mstr.t) Hashtbl.t;
   env_tag  : Hashweak.tag;
 }
@@ -102,12 +100,20 @@ let list_formats () =
 
 (** Environment construction and utilisation *)
 
-let create_env = let c = ref (-1) in fun fc -> {
-  env_find = fc;
+let create_env = let c = ref (-1) in fun lp -> {
+  env_path = lp;
   env_memo = Hashtbl.create 17;
   env_tag  = (incr c; Hashweak.create_tag !c)
 }
 
+let create_env_of_loadpath lp =
+  Format.eprintf "WARNING: Env.create_env_of_loadpath is deprecated
+    and will be removed in future versions of Why3.
+    Replace it with Env.create_env.@.";
+  create_env lp
+
+let get_loadpath env = env.env_path
+
 (* looks for file [file] of format [name] in loadpath [lp] *)
 let locate_file name lp path =
   let file = List.fold_left Filename.concat "" path in
@@ -133,18 +139,13 @@ let check_qualifier s =
       find_dir_sep s)
   then raise (InvalidQualifier s)
 
-let create_env_of_loadpath lp =
-  let fc f sl =
-    List.iter check_qualifier sl;
-    let file = locate_file f lp sl in
-    file, open_in file
-  in
-  create_env fc
-
-let find_channel env = env.env_find
+let find_channel env f sl =
+  List.iter check_qualifier sl;
+  let file = locate_file f env.env_path sl in
+  file, open_in file
 
 let find_library env sl =
-  let file, ic = env.env_find "why" sl in
+  let file, ic = find_channel env "why" sl in
   try
     Hashtbl.replace env.env_memo sl Mstr.empty;
     let mth = real_read_channel ~format:"why" env sl file ic in

src/core/env.mli

@@ -80,20 +80,20 @@ val list_formats : unit -> (fformat * extension list) list
 
 (** Environment construction and utilisation *)
 
-type find_channel = fformat -> pathname -> filename * in_channel
-(** a function of type [find_channel] retrieves an input channel,
-    knowing its format and its name (presented as a list of strings);
-    a filename is also returned, to be used in logs or error messages. *)
-
-val create_env : find_channel -> env
-(** creates an environment of input library channels *)
+val create_env : filename list -> env
+(** creates an environment from a "loadpath", a list of directories
+    containing loadable Why3/WhyML/etc files *)
 
 val create_env_of_loadpath : filename list -> env
-(** a special case of [init_environment] that looks for files in
-    the given list of directories *)
+(** the same as [create_env], will be removed in some future version *)
+
+val get_loadpath : env -> filename list
+(** returns the loadpath of a given environment *)
 
-val find_channel : env -> find_channel
-(** finds an input channel in a given environment
+val find_channel : env -> fformat -> pathname -> filename * in_channel
+(** finds an input channel in a given environment, knowing its format
+    and its name (presented as a list of strings); a filename is also
+    returned, to be used in logs or error messages.
 
     @raise ChannelNotFound [sl] if the channel [sl] was not found
     @raise UnknownFormat [f] if the format is not registered *)

src/ide/gconfig.ml

@@ -132,7 +132,7 @@ let load_config config =
     | None -> default_ide
     | Some s -> load_ide s in
   (* temporary sets env to empty *)
-  let env = Env.create_env_of_loadpath [] in
+  let env = Env.create_env [] in
   set_labels_flag ide.ide_show_labels;
   set_locs_flag ide.ide_show_locs;
   { window_height = ide.ide_window_height;

src/ide/gmain.ml

@@ -116,7 +116,7 @@ let source_text fname =
 let gconfig =
   let c = Gconfig.config in
   let loadpath = (Whyconf.loadpath (get_main ())) @ List.rev !includes in
-  c.env <- Env.create_env_of_loadpath loadpath;
+  c.env <- Env.create_env loadpath;
 (*
   let provers = Whyconf.get_provers c.Gconfig.config in
   c.provers <-

src/ide/replay.ml

@@ -87,7 +87,7 @@ let config = Whyconf.read_config None
 let loadpath = (Whyconf.loadpath (Whyconf.get_main config))
   @ List.rev !includes
 
-let env = Env.create_env_of_loadpath loadpath
+let env = Env.create_env loadpath
 
 let provers = Whyconf.get_provers config
 

src/main.ml

@@ -504,7 +504,7 @@ let do_input env drv = function
 
 let () =
   try
-    let env = Env.create_env_of_loadpath !opt_loadpath in
+    let env = Env.create_env !opt_loadpath in
     let drv = Util.option_map (load_driver env) !opt_driver in
     Queue.iter (do_input env drv) opt_queue
   with e when not (Debug.test_flag Debug.stack_trace) ->

src/realize.ml

@@ -85,7 +85,7 @@ let () =
           let config = Whyconf.read_config None in
           let main = Whyconf.get_main config in
           let env =
-            Env.create_env_of_loadpath (!opt_loadpath @ Whyconf.loadpath main)
+            Env.create_env (!opt_loadpath @ Whyconf.loadpath main)
           in
           let coq =
             try Util.Mstr.find "coq-realize" (Whyconf.get_provers config)