a little refactoring in Env

- create_env_of_loadpath is now provided in Env instead of Lexer
- find_channel functions now depend on format to determine the
  suitable extensions

Makefile.in

@@ -160,21 +160,15 @@ LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
 $(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
 $(LIBCMX): OFLAGS += -for-pack Why
 
-LIB_PARSER_POSTLUDE = \
-  "let logic_file_eof env = inside_env env logic_file_eof\nlet list0_decl_eof env lenv uc = inside_uc env lenv uc list0_decl_eof\n"
-
-LIB_PARSER_INTERFACE = \
-  -e "s/^val  *logic_file_eof *:/val logic_file_eof : Env.env ->/" \
-  -e "s/^val  *list0_decl_eof *:/val list0_decl_eof : Env.env -> \
-  Theory.theory Theory.Mnm.t -> Theory.theory_uc ->/"
+LIB_PARSER_POSTLUDE  = "let logic_file env = inside_env env logic_file\n"
+LIB_PARSER_INTERFACE = "s/^val  *logic_file *:/val logic_file : Env.env ->/"
 
 src/parser/parser.ml: src/parser/parser.pre.ml
-	cp src/parser/parser.pre.ml src/parser/parser.ml
-	printf $(LIB_PARSER_POSTLUDE) >> src/parser/parser.ml
+	cp $^ $@
+	printf $(LIB_PARSER_POSTLUDE) >> $@
 
 src/parser/parser.mli: src/parser/parser.pre.mli
-	sed $(LIB_PARSER_INTERFACE) src/parser/parser.pre.mli > \
-					src/parser/parser.mli
+	sed -e $(LIB_PARSER_INTERFACE) $^ > $@
 
 # build targets
 

examples/use_api.ml

@@ -49,7 +49,7 @@ let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2
 
 (* building the task for formula 1 alone *)
 let task1 : Task.task = None (* empty task *)
-let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1") 
+let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1")
 let task1 : Task.task = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1
 
 (* printing the task *)
@@ -57,9 +57,9 @@ let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1
 
 (* task for formula 2 *)
 let task2 = None
-let task2 = Task.add_logic_decl task2 [prop_var_A, None] 
-let task2 = Task.add_logic_decl task2 [prop_var_B, None] 
-let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2") 
+let task2 = Task.add_logic_decl task2 [prop_var_A, None]
+let task2 = Task.add_logic_decl task2 [prop_var_B, None]
+let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
 let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
 
 let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2
@@ -76,17 +76,20 @@ let main : Whyconf.main = Whyconf.get_main config
 let provers : Whyconf.config_prover Util.Mstr.t = Whyconf.get_provers config
 
 (* the [prover alt-ergo] section of the config file *)
-let alt_ergo : Whyconf.config_prover = 
+let alt_ergo : Whyconf.config_prover =
   try
-    Util.Mstr.find "alt-ergo" provers 
+    Util.Mstr.find "alt-ergo" provers
   with Not_found ->
     eprintf "Prover alt-ergo not installed or not configured@.";
     exit 0
 
 (* builds the environment from the [loadpath] *)
-let env : Env.env = Lexer.create_env (Whyconf.loadpath main)
+let env : Env.env =
+  Env.create_env_of_loadpath (Whyconf.loadpath main)
+
 (* loading the Alt-Ergo driver *)
-let alt_ergo_driver : Driver.driver = Driver.load_driver env alt_ergo.Whyconf.driver
+let alt_ergo_driver : Driver.driver =
+  Driver.load_driver env alt_ergo.Whyconf.driver
 
 (* call Alt-Ergo *)
 let result1 : Call_provers.prover_result =
@@ -98,7 +101,7 @@ let result1 : Call_provers.prover_result =
 let () = printf "@[On task 1, alt-ergo answers %a@."
   Call_provers.print_prover_result result1
 
-let result2 : Call_provers.prover_result = 
+let result2 : Call_provers.prover_result =
   Call_provers.wait_on_call
     (Driver.prove_task ~command:alt_ergo.Whyconf.command
     ~timelimit:10
@@ -118,25 +121,25 @@ An arithmetic goal: 2+2 = 4
 
 let two : Term.term = Term.t_const (Term.ConstInt "2")
 let four : Term.term = Term.t_const (Term.ConstInt "4")
-let int_theory : Theory.theory = 
+let int_theory : Theory.theory =
   Env.find_theory env ["int"] "Int"
-let plus_symbol : Term.lsymbol = 
+let plus_symbol : Term.lsymbol =
   Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
 let two_plus_two : Term.term = Term.fs_app plus_symbol [two;two] Ty.ty_int
-let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two] 
+let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two]
 let fmla3 : Term.term = Term.t_equ two_plus_two four
 
 let task3 = None
 let task3 = Task.use_export task3 int_theory
-let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3") 
+let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")
 let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3
 
 (*
 let () = printf "@[task 3 created:@\n%a@]@." Pretty.print_task task3
 *)
-let () = printf "@[task 3 created@]@." 
+let () = printf "@[task 3 created@]@."
 
-let result3 = 
+let result3 =
   Call_provers.wait_on_call
     (Driver.prove_task ~command:alt_ergo.Whyconf.command
     alt_ergo_driver task3 ()) ()
@@ -146,29 +149,29 @@ let () = printf "@[On task 3, alt-ergo answers %a@."
 
 (* quantifiers: let's build "forall x:int. x*x >= 0" *)
 let zero : Term.term = Term.t_const (Term.ConstInt "0")
-let mult_symbol : Term.lsymbol = 
+let mult_symbol : Term.lsymbol =
   Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
-let ge_symbol : Term.lsymbol = 
+let ge_symbol : Term.lsymbol =
   Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]
 
-let var_x : Term.vsymbol = 
+let var_x : Term.vsymbol =
   Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int
 let x : Term.term = Term.t_var var_x
-let x_times_x : Term.term = 
-  Term.t_app_infer mult_symbol [x;x] 
-let fmla4_aux : Term.term = 
+let x_times_x : Term.term =
+  Term.t_app_infer mult_symbol [x;x]
+let fmla4_aux : Term.term =
   Term.ps_app ge_symbol [x_times_x;zero]
-let fmla4_quant : Term.term_quant = 
+let fmla4_quant : Term.term_quant =
   Term.t_close_quant [var_x] [] fmla4_aux
 let fmla4 : Term.term =
   Term.t_forall fmla4_quant
 
 let task4 = None
 let task4 = Task.use_export task4 int_theory
-let goal_id4 = Decl.create_prsymbol (Ident.id_fresh "goal4") 
+let goal_id4 = Decl.create_prsymbol (Ident.id_fresh "goal4")
 let task4 = Task.add_prop_decl task4 Decl.Pgoal goal_id4 fmla4
 
-let result4 = 
+let result4 =
   Call_provers.wait_on_call
     (Driver.prove_task ~command:alt_ergo.Whyconf.command
     alt_ergo_driver task4 ()) ()

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 = Lexer.create_env loadpath in
+  let env = Env.create_env_of_loadpath 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 = Lexer.create_env !opt_loadpath in
+  let env = Env.create_env_of_loadpath !opt_loadpath in
 
   if !opt_redo then
     begin if not (Db.is_initialized ()) then

src/core/env.ml

@@ -20,131 +20,161 @@
 open Ident
 open Theory
 
-(** Environment *)
+(** Library environment *)
 
-type retrieve_channel = string list -> string * in_channel
+type fformat = string (* format name *)
+type filename = string (* file name *)
+type extension = string (* file extension *)
+type pathname = string list (* path in an environment *)
+
+exception KnownFormat of fformat
+exception UnknownFormat of fformat
+exception UnknownExtension of extension
+exception UnspecifiedFormat
+
+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_ret_chan : retrieve_channel;
-  env_retrieve : retrieve_theory;
-  env_memo     : (string list, theory Mnm.t) Hashtbl.t;
-  env_tag      : Hashweak.tag;
+  env_find : find_channel;
+  env_memo : (string list, theory Mnm.t) Hashtbl.t;
+  env_tag  : Hashweak.tag;
 }
 
-and retrieve_theory = env -> string list -> theory Mnm.t
+let env_tag env = env.env_tag
 
-let create_memo () =
-  let ht = Hashtbl.create 17 in
-  Hashtbl.add ht [] Mnm.empty;
-  ht
+module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end)
 
-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) }
+(** Input formats *)
 
-exception TheoryNotFound of string list * string
+type read_channel = env -> filename -> in_channel -> theory Mnm.t
 
-let get_builtin s =
-  if s = builtin_theory.th_name.id_string then builtin_theory else
-  if s = highord_theory.th_name.id_string then highord_theory else
-  match tuple_theory_name s with
-  | Some n -> tuple_theory n
-  | None -> raise (TheoryNotFound ([],s))
+let read_channel_table = Hashtbl.create 17 (* format name -> read_channel *)
+let extensions_table   = Hashtbl.create 17 (* suffix -> format name *)
 
-let find_builtin env s =
-  let m = Hashtbl.find env.env_memo [] in
-  try Mnm.find s m with Not_found ->
-    let th = get_builtin s in
-    let m = Mnm.add s th m in
-    Hashtbl.replace env.env_memo [] m;
-    th
+let register_format name exts rc =
+  if Hashtbl.mem read_channel_table name then raise (KnownFormat name);
+  Hashtbl.add read_channel_table name (rc,exts);
+  List.iter (fun s -> Hashtbl.replace extensions_table ("." ^ s) name) exts
 
-let find_library env sl =
-  try Hashtbl.find env.env_memo sl
-  with Not_found ->
-    Hashtbl.add env.env_memo sl Mnm.empty;
-    let m = env.env_retrieve env sl in
-    Hashtbl.replace env.env_memo sl m;
-    m
+let lookup_format name =
+  try Hashtbl.find read_channel_table name
+  with Not_found -> raise (UnknownFormat name)
 
-let find_theory env sl s =
-  if sl = [] then find_builtin env s
-  else try Mnm.find s (find_library env sl)
-  with Not_found -> raise (TheoryNotFound (sl, s))
+let get_extension file =
+  let s = try Filename.chop_extension file
+    with Invalid_argument _ -> raise UnspecifiedFormat in
+  let n = String.length s in
+  String.sub file n (String.length file - n)
 
-let find_channel env = env.env_ret_chan
+let get_format file =
+  let ext = get_extension file in
+  try Hashtbl.find extensions_table ext
+  with Not_found -> raise (UnknownExtension ext)
 
-let env_tag env = env.env_tag
+let read_channel ?format env file ic =
+  let name = match format with
+    | Some name -> name
+    | None -> get_format file in
+  let rc,_ = lookup_format name in
+  rc env file ic
 
-module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end)
+let read_file ?format env file =
+  let ic = open_in file in
+  try
+    let mth = read_channel ?format env file ic in
+    close_in ic;
+    mth
+  with e -> close_in ic; raise e
 
-(** Parsers *)
+let list_formats () =
+  let add n (_,l) acc = (n,l)::acc in
+  Hashtbl.fold add read_channel_table []
 
-type read_channel = env -> string -> in_channel -> theory Mnm.t
 
-let read_channel_table = Hashtbl.create 17 (* parser name -> read_channel *)
-let suffixes_table     = Hashtbl.create 17 (* suffix -> parser name *)
+(** Environment construction and utilisation *)
 
-let register_format name suffixes rc =
-  Hashtbl.add read_channel_table name rc;
-  List.iter (fun s -> Hashtbl.add suffixes_table ("." ^ s) name) suffixes
+let create_env = let c = ref (-1) in fun fc -> {
+  env_find = fc;
+  env_memo = Hashtbl.create 17;
+  env_tag  = (incr c; Hashweak.create_tag !c)
+}
 
-exception NoFormat
-exception UnknownExtension of string
-exception UnknownFormat of string (* parser name *)
+(* looks for file [file] of format [name] in loadpath [lp] *)
+let locate_file name lp file =
+  let _,sl = lookup_format name in
+  let add_sf sf = file ^ "." ^ sf in
+  let fl = if sl = [] then [file] else List.map add_sf sl in
+  let add_dir dir = List.map (Filename.concat dir) fl in
+  let fl = List.concat (List.map add_dir lp) in
+  match List.filter Sys.file_exists fl with
+  | [] -> raise Not_found
+  | [file] -> file
+  | file1 :: file2 :: _ -> raise (AmbiguousPath (file1, file2))
+
+let create_env_of_loadpath lp =
+  let fc f sl =
+    let file = List.fold_left Filename.concat "" sl in
+    let file = locate_file f lp file in
+    file, open_in file
+  in
+  create_env fc
 
-let parser_for_file ?format file = match format with
-  | None ->
-      begin try
-        let ext =
-          let s = Filename.chop_extension file in
-          let n = String.length s in
-          String.sub file n (String.length file - n)
-        in
-        try Hashtbl.find suffixes_table ext
-        with Not_found -> raise (UnknownExtension ext)
-      with Invalid_argument _ -> raise NoFormat end
-  | Some n -> n
+let find_channel env = env.env_find
 
-let find_parser table n =
-  try Hashtbl.find table n
-  with Not_found -> raise (UnknownFormat n)
+let find_library env sl =
+  let file, ic = env.env_find "why" sl in
+  try
+    Hashtbl.replace env.env_memo sl Mnm.empty;
+    let mth = read_channel ~format:"why" env file ic in
+    Hashtbl.replace env.env_memo sl mth;
+    close_in ic;
+    mth
+  with e ->
+    Hashtbl.remove env.env_memo sl;
+    close_in ic;
+    raise e
 
-let read_channel ?format env file ic =
-  let n = parser_for_file ?format file in
-  let rc = find_parser read_channel_table n in
-  rc env file ic
+let find_library env sl =
+  try Hashtbl.find env.env_memo sl
+  with Not_found -> find_library env sl
 
-let read_file ?format env file =
-  let cin = open_in file in
-  let m = read_channel ?format env file cin in
-  close_in cin;
-  m
+let get_builtin s =
+  if s = builtin_theory.th_name.id_string then builtin_theory else
+  if s = highord_theory.th_name.id_string then highord_theory else
+  match tuple_theory_name s with
+  | Some n -> tuple_theory n
+  | None -> raise (TheoryNotFound ([],s))
 
-let list_formats () =
-  let h = Hashtbl.create 17 in
-  let add s p =
-    let l = try Hashtbl.find h p with Not_found -> [] in
-    Hashtbl.replace h p (s :: l)
-  in
-  Hashtbl.iter add suffixes_table;
-  Hashtbl.fold (fun p l acc -> (p, l) :: acc) h []
+let find_theory env sl s =
+  if sl = [] then get_builtin s else
+  let mth = find_library env sl in
+  try Mnm.find s mth with Not_found ->
+  raise (TheoryNotFound (sl,s))
 
 (* Exception reporting *)
 
 let () = Exn_printer.register
   begin fun fmt exn -> match exn with
-  | TheoryNotFound (sl, s) ->
+  | ChannelNotFound sl ->
+      Format.fprintf fmt "Library not found: %a"
+        (Pp.print_list (Pp.constant_string ".") Format.pp_print_string) sl
+  | TheoryNotFound (sl,s) ->
       Format.fprintf fmt "Theory not found: %a.%s"
         (Pp.print_list (Pp.constant_string ".") Format.pp_print_string) sl s
+  | KnownFormat s ->
+      Format.fprintf fmt "Format %s is already registered" s
   | UnknownFormat s ->
       Format.fprintf fmt "Unknown input format: %s" s
   | UnknownExtension s ->
-      Format.fprintf fmt "Unknown file extension: %s" s
-  | NoFormat ->
-      Format.fprintf fmt "No input format given"
+      Format.fprintf fmt "Unknown file extension: `%s'" s
+  | UnspecifiedFormat ->
+      Format.fprintf fmt "Format not specified"
+  | AmbiguousPath (f1,f2) ->
+      Format.fprintf fmt "Ambiguous path:@ both `%s'@ and `%s'@ match" f1 f2
   | _ -> raise exn
   end
 

src/core/env.mli

@@ -17,9 +17,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Access to Environment, Load Path *)
-
-open Theory
+(** Library environment *)
 
 type env
 
@@ -27,54 +25,79 @@ val env_tag : env -> Hashweak.tag
 
 module Wenv : Hashweak.S with type key = env
 
-type retrieve_channel = string list -> string * in_channel
-  (** retrieves a channel from a given path; a filename is also returned,
-      for printing purposes only *)
+(** Local type aliases and exceptions *)
+
+type fformat = string (* format name *)
+type filename = string (* file name *)
+type extension = string (* file extension *)
+type pathname = string list (* path in an environment *)
+
+exception KnownFormat of fformat
+exception UnknownFormat of fformat
+exception UnknownExtension of extension
+exception UnspecifiedFormat
+
+exception ChannelNotFound of pathname
+exception TheoryNotFound of pathname * string
+
+(** Input formats *)
+
+open Theory
+
+type read_channel = env -> filename -> in_channel -> theory Mnm.t
+(** a function of type [read_channel] parses a channel using
+    its own syntax. The string argument indicates the origin of
+    the stream (e.g. file name) to be used in error messages. *)
 
-type retrieve_theory  = env -> string list -> theory Mnm.t
+val register_format : fformat -> extension list -> read_channel -> unit
+(** [register_format name extensions fn] registers a new format
+    called [name], for files with extensions in the string list
+    [extensions] (separating dot not included);
+    [fn] is the function to perform parsing.
 
-val create_env : retrieve_channel -> retrieve_theory -> env
+    @raise KnownFormat [name] if the format is already registered *)
 
-exception TheoryNotFound of string list * string
+val read_channel : ?format:fformat -> read_channel
+(** [read_channel ?format env file ch] returns the theories in [ch].
+    When given, [format] enforces the format, otherwise we choose
+    the format according to [file]'s extension. Nothing ensures
+    that [ch] corresponds to the contents of [f].
 
-val find_theory : env -> string list -> string -> theory
-  (** [find_theory e p n] finds the theory named [p.n] in environment [e]
-      @raise TheoryNotFound if theory not present in env [e] *)
+    @raise UnknownFormat [format] if the format is not registered
+    @raise UnknownExtension [s] if the extension [s] is not known
+      to any registered parser
+    @raise UnspecifiedFormat if format is not given and [file]
+      has no extension *)
 
-val find_channel : env -> string list -> string * in_channel
+val read_file : ?format:fformat -> env -> filename -> theory Mnm.t
+(** [read_file ?format env file] returns the theories in [file].
+    When given, [format] enforces the format, otherwise we choose
+    the format according to [file]'s extension. *)
 
-(** Parsers *)
+val list_formats : unit -> (fformat * extension list) list
 
-type read_channel = env -> string -> in_channel -> theory Mnm.t
-  (** a function of type [read_channel] parses the given channel using
-      its own syntax. The string argument indicates the origin of the stream
-      (e.g. file name) to be used in error messages *)
+(** Environment construction and utilisation *)
 
-val register_format : string -> string list -> read_channel -> unit
-  (** [register_format name extensions f] registers a new format
-      under name [name], for files with extensions in list [extensions];
-      [f] is the function to perform parsing *)
+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. *)
 
-exception NoFormat
-exception UnknownExtension of string
-exception UnknownFormat of string (* format name *)
+val create_env : find_channel -> env
+(** creates an environment of input library channels *)
 
-val read_channel : ?format:string -> read_channel
-(** [read_channel ?format env f c] returns the map of theories
-    in channel [c]. When given, [format] enforces the format, otherwise
-    the format is chosen according to [f]'s extension.
-    Beware that nothing ensures that [c] corresponds to the contents of [f]
+val create_env_of_loadpath : filename list -> env
+(** a special case of [init_environment] that looks for files in
+    the given list of directories *)
 
-    @raise NoFormat if [format] is not given and [f] has no extension
-    @raise UnknownExtension [s] if the extension [s] is not known in
-      any registered parser
-    @raise UnknownFormat [f] if the [format] is not registered
-*)
+val find_channel : env -> find_channel
+(** finds an input channel in a given environment
 
-val read_file : ?format:string -> env -> string -> theory Mnm.t
-(** [read_file ?format env f] returns the map of theories
-    in file [f]. When given, [format] enforces the format, otherwise
-    the format is chosen according to [f]'s extension. *)
+    @raise ChannelNotFound [sl] if the channel [sl] was not found
+    @raise UnknownFormat [f] if the format is not registered *)
 
-val list_formats : unit -> (string * string list) list
+val find_theory : env -> pathname -> string -> theory
+(** a special case of [find_channel] that returns a particular theory,
+    using the format ["why"]
 
+    @raise TheoryNotFound if the theory was not found in a channel *)

src/driver/driver.ml

@@ -247,16 +247,11 @@ let update_task drv task =
   add_tdecl task goal
 
 let prepare_task drv task =
-  let lookup_transform t = t, lookup_transform t drv.drv_env in
+  let lookup_transform t = lookup_transform t drv.drv_env in
   let transl = List.map lookup_transform drv.drv_transform in
-  let apply task (_t, tr) =
-(*  Format.printf "@\n@\n[%f] %s@." (Sys.time ()) t; *)
-    Trans.apply tr task
-  in
-(*Format.printf "@\n@\nTASK";*)
+  let apply task tr = Trans.apply tr task in
   let task = update_task drv task in
-  let task = List.fold_left apply task transl in
-  task
+  List.fold_left apply task transl
 
 
 let print_task_prepared ?old drv fmt task =

src/ide/gconfig.ml

@@ -93,7 +93,7 @@ let load_config config =
   let env = Lexer.create_env main.loadpath in
 *)
   (* temporary sets env to empty *)
-  let env = Lexer.create_env [] in
+  let env = Env.create_env_of_loadpath [] in
   { window_height = ide.ide_window_height;
     window_width  = ide.ide_window_width;
     tree_width    = ide.ide_tree_width;

src/ide/newmain.ml

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

src/ide/replay.ml

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

src/main.ml

@@ -515,7 +515,7 @@ let do_input env drv = function
 
 let () =
   try
-    let env = Lexer.create_env !opt_loadpath in
+    let env = Env.create_env_of_loadpath !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/parser/lexer.mli

@@ -17,17 +17,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Theory
-
 (** parsing entry points *)
 
-val create_env : string list -> Env.env
-  (** creates a new typing environment for a given loadpath *)
-
-val parse_list0_decl :
-  Env.env -> theory Mnm.t -> theory_uc -> Lexing.lexbuf -> theory_uc
-
-val parse_lexpr : Lexing.lexbuf -> Ptree.lexpr
+val parse_logic_file : Env.env -> Lexing.lexbuf -> Theory.theory Theory.Mnm.t
 
 val parse_program_file : Lexing.lexbuf -> Ptree.program_file
 

src/parser/lexer.mll

@@ -315,12 +315,7 @@ and string = parse
       | Loc.Located _ as e -> raise e
       | e -> raise (Loc.Located (loc lb, e))
 
-  let parse_logic_file env = with_location (logic_file_eof env token)
-
-  let parse_list0_decl env lenv uc =
-    with_location (list0_decl_eof env lenv uc token)
-
-  let parse_lexpr = with_location (lexpr_eof token)
+  let parse_logic_file env = with_location (logic_file env token)
 
   let parse_program_file = with_location (program_file token)
 
@@ -329,33 +324,6 @@ and string = parse
     Loc.set_file file lb;
     parse_logic_file env lb
 
-  (* searches file [f] in loadpath [lp] *)
-  let locate_file lp f =
-    let fl = List.map (fun dir -> Filename.concat dir f) lp in
-    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
-      let file = locate_file lp f in
-      file, open_in file
-    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
-    Env.create_env ret_chan retrieve
-
   let () = Env.register_format "why" ["why"] read_channel
 }
 

src/parser/parser.pre.mly

@@ -40,16 +40,6 @@
     ref_drop env_ref;
     res
 
-  let inside_uc env lenv uc rule lexer lexbuf =
-    ref_push env_ref env;
-      ref_push lenv_ref lenv;
-        ref_push uc_ref uc;
-    let res = rule lexer lexbuf in
-        ref_drop uc_ref;
-      ref_drop lenv_ref;
-    ref_drop env_ref;
-    res
-
   open Ptree
   open Parsing
 
@@ -236,28 +226,16 @@
 
 /* Entry points */
 
-%type <Ptree.lexpr> lexpr_eof
-%start lexpr_eof
-%type <Theory.theory_uc> list0_decl_eof
-%start list0_decl_eof
-%type <Theory.theory Theory.Mnm.t> logic_file_eof
-%start logic_file_eof
+%type <Theory.theory Theory.Mnm.t> logic_file
+%start logic_file