Env: added a retrieve_channel capability, for use in programs

parent 1676db4a
......@@ -65,7 +65,7 @@ let alt_ergo : Whyconf.config_prover =
exit 0
(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Lexer.retrieve (Whyconf.loadpath main))
let env : Env.env = Lexer.create_env (Whyconf.loadpath main)
(* loading the Alt-Ergo driver *)
let alt_ergo_driver : Driver.driver = Driver.load_driver env alt_ergo.Whyconf.driver
......
......@@ -286,7 +286,7 @@ let () =
in
opt_task := List.fold_left add_meta !opt_task !opt_metas;
let env = Env.create_env (Lexer.retrieve !opt_loadpath) in
let env = Lexer.create_env !opt_loadpath in
let map_prover s =
let prover = try Mstr.find s (get_provers config) with
| Not_found -> eprintf "Prover %s not found.@." s; exit 1
......
......@@ -46,7 +46,7 @@ let cprovers = Whyconf.get_provers config
let timelimit = timelimit main
let env = Env.create_env (Lexer.retrieve (loadpath main))
let env = Lexer.create_env (loadpath main)
let provers = Hashtbl.create 17
......
......@@ -22,7 +22,10 @@ open Theory
(** Environment *)
type retrieve_channel = string list -> in_channel
type env = {
env_ret_chan : retrieve_channel;
env_retrieve : retrieve_theory;
env_memo : (string list, theory Mnm.t) Hashtbl.t;
env_tag : Hashweak.tag;
......@@ -35,7 +38,8 @@ let create_memo () =
Hashtbl.add ht [] Mnm.empty;
ht
let create_env = let c = ref (-1) in fun retrieve -> {
let create_env = let c = ref (-1) in fun ret_chan retrieve -> {
env_ret_chan = ret_chan;
env_retrieve = retrieve;
env_memo = create_memo ();
env_tag = (incr c; Hashweak.create_tag !c) }
......@@ -72,7 +76,7 @@ let find_theory env sl s =
let env_tag env = env.env_tag
module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end)
(* module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end) *)
(** Parsers *)
......
......@@ -25,11 +25,13 @@ type env
val env_tag : env -> Hashweak.tag
module Wenv : Hashweak.S with type key = env
(* module Wenv : Hashweak.S with type key = env *)
type retrieve_theory = env -> string list -> theory Mnm.t
type retrieve_channel = string list -> in_channel
val create_env : retrieve_theory -> env
type retrieve_theory = env -> string list -> theory Mnm.t
val create_env : retrieve_channel -> retrieve_theory -> env
exception TheoryNotFound of string list * string
......
......@@ -93,10 +93,10 @@ let load_config config =
let provers = get_provers config in
*)
(*
let env = Env.create_env (Lexer.retrieve main.loadpath) in
let env = Lexer.create_env main.loadpath in
*)
(* temporary sets env to empty *)
let env = Env.create_env (Lexer.retrieve []) in
let env = Lexer.create_env [] in
{ window_height = ide.ide_window_height;
window_width = ide.ide_window_width;
tree_width = ide.ide_tree_width;
......
......@@ -94,7 +94,7 @@ let source_text fname =
let gconfig =
let c = Gconfig.config in
let loadpath = (get_main ()).loadpath @ List.rev !includes in
c.env <- Env.create_env (Lexer.retrieve loadpath);
c.env <- Lexer.create_env loadpath;
let provers = Whyconf.get_provers c.Gconfig.config in
c.provers <- Util.Mstr.fold (Gconfig.get_prover_data c.env) provers Util.Mstr.empty;
c
......
......@@ -150,7 +150,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 (Lexer.retrieve loadpath);
c.env <- Lexer.create_env loadpath;
let provers = Whyconf.get_provers c.Gconfig.config in
c.provers <-
Util.Mstr.fold (Gconfig.get_prover_data c.env) provers Util.Mstr.empty;
......
......@@ -434,7 +434,7 @@ let do_input env drv = function
let () =
try
let env = Env.create_env (Lexer.retrieve !opt_loadpath) in
let env = Lexer.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) ->
......
......@@ -21,7 +21,7 @@ open Theory
(** parsing entry points *)
val retrieve : string list -> Env.retrieve_theory
val create_env : string list -> Env.env
(** creates a new typing environment for a given loadpath *)
val parse_list0_decl :
......
......@@ -271,21 +271,31 @@ and string = parse
Loc.set_file file lb;
parse_logic_file env lb
let retrieve lp env sl =
let f = List.fold_left Filename.concat "" sl ^ ".why" in
(* searches file [f] in loadpath [lp] *)
let locate_file lp f =
let fl = List.map (fun dir -> Filename.concat dir f) lp in
let file = match List.filter Sys.file_exists fl with
match List.filter Sys.file_exists fl with
| [] -> raise Not_found
| [file] -> file
| file1 :: file2 :: _ -> raise (AmbiguousPath (file1, file2))
let create_env lp =
let ret_chan sl =
let f = List.fold_left Filename.concat "" sl in
open_in (locate_file lp f)
in
let retrieve env sl =
let f = List.fold_left Filename.concat "" sl ^ ".why" in
let file = locate_file lp f in
let c = open_in file in
try
let tl = read_channel env file c in
close_in c;
tl
with
| e -> close_in c; raise e
in
let c = open_in file in
try
let tl = read_channel env file c in
close_in c;
tl
with
| e -> close_in c; raise e
Env.create_env ret_chan retrieve
let () = Env.register_format "why" ["why"] read_channel
}
......
open Why
open Util
open Ident
open Ty
open Theory
open Term
open Decl
type t
(* environments *)
val tag : t -> Hashweak.tag
type env = private {
uc : theory_uc;
globals : (lsymbol * type_v) Mstr.t;
exceptions : lsymbol Mstr.t;
(* predefined symbols *)
ts_arrow: tysymbol;
ts_bool : tysymbol;
ts_label: tysymbol;
ts_ref : tysymbol;
ts_exn : tysymbol;
ts_unit : tysymbol;
ls_at : lsymbol;
ls_bang : lsymbol;
ls_old : lsymbol;
ls_True : lsymbol;
ls_False: lsymbol;
ls_andb : lsymbol;
ls_orb : lsymbol;
ls_notb : lsymbol;
ls_unit : lsymbol;
ls_lt : lsymbol;
ls_gt : lsymbol;
ls_le : lsymbol;
ls_ge : lsymbol;
ls_add : lsymbol;
}
val create : Env.env -> t
val empty_env : theory_uc -> env
val add_global : preid -> type_v -> env -> lsymbol * env
val add_decl : decl -> env -> env
val logic_lexpr : Loc.position * string -> Ptree.lexpr
val logic_decls : Loc.position * string -> Env.env -> env -> env
val add_exception : preid -> ty option -> env -> lsymbol * env
val t_True : env -> term
val type_v_unit : env -> type_v
exception ModuleNotFound of string list * string
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] *)
......@@ -49,7 +49,7 @@ type esymbol = lsymbol
val ts_arrow : tysymbol
val purify :type_v -> ty
val purify : type_v -> ty
(* operations on program types *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment