Env: organize supported languages in a tree

examples/use_api/logic.ml

@@ -122,7 +122,7 @@ An arithmetic goal: 2+2 = 4
 let two : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "2"))
 let four : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "4"))
 let int_theory : Theory.theory =
-  Env.find_theory env ["int"] "Int"
+  Env.read_theory env ["int"] "Int"
 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
@@ -301,13 +301,10 @@ declaration of
 
 *)
 
-
 (* import the ref.Ref module *)
 
-let ref_modules, ref_theories =
-  Env.read_lib_file (Mlw_main.library_of_env env) ["ref"]
-
-let ref_module : Mlw_module.modul = Stdlib.Mstr.find "Ref" ref_modules
+let ref_module : Mlw_module.modul =
+  Mlw_module.read_module env ["ref"] "Ref"
 
 let ref_type : Mlw_ty.T.itysymbol =
   Mlw_module.ns_find_its ref_module.Mlw_module.mod_export ["ref"]

examples/use_api/mlw.ml

@@ -31,7 +31,7 @@ let provers : Whyconf.config_prover Whyconf.Mprover.t =
 let env : Env.env = Env.create_env (Whyconf.loadpath main)
 
 let int_theory : Theory.theory =
-  Env.find_theory env ["int"] "Int"
+  Env.read_theory env ["int"] "Int"
 
 let mul_int : Term.lsymbol =
   Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
@@ -96,10 +96,8 @@ declaration of
 
 (* import the ref.Ref module *)
 
-let ref_modules, ref_theories =
-  Env.read_lib_file (Mlw_main.library_of_env env) ["ref"]
-
-let ref_module : Mlw_module.modul = Stdlib.Mstr.find "Ref" ref_modules
+let ref_module : Mlw_module.modul =
+  Mlw_module.read_module env ["ref"] "Ref"
 
 let ref_type : Mlw_ty.T.itysymbol =
   Mlw_module.ns_find_its ref_module.Mlw_module.mod_export ["ref"]

examples/use_api/mlw_tree.ml

@@ -31,7 +31,7 @@ let provers : Whyconf.config_prover Whyconf.Mprover.t =
 let env : Env.env = Env.create_env (Whyconf.loadpath main)
 
 let int_theory : Theory.theory =
-  Env.find_theory env ["int"] "Int"
+  Env.read_theory env ["int"] "Int"
 
 let mul_int : Term.lsymbol =
   Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
@@ -40,11 +40,9 @@ let unit_type = Ty.ty_tuple []
 
 (* start a parsing *)
 
-let lib = Mlw_main.library_of_env env
-
 let pathname = [] (* dummy pathname *)
 
-let t : Ptree.incremental = Mlw_typing.open_file lib pathname
+let t : Ptree.incremental = Mlw_typing.open_file env pathname
 
 open Ptree
 

plugins/parser/dimacs.mll

@@ -125,22 +125,17 @@ let parse th_uc filename cin =
     let th_uc, vars = init_vars th_uc nb_vars in
     file th_uc vars 0 lexbuf) lb
 
-
 let parse _env _path filename cin =
   let th_uc = Theory.create_theory (Ident.id_fresh "Cnf") in
   let th_uc = parse th_uc filename cin in
   let pr = Decl.create_prsymbol (Ident.id_fresh "false") in
   let th_uc = Theory.add_prop_decl th_uc Decl.Pgoal pr Term.t_false in
-  (), Mstr.singleton "Cnf" (Theory.close_theory th_uc)
+  Mstr.singleton "Cnf" (Theory.close_theory th_uc)
 
-let library_of_env = Env.register_format "Dimacs" ["cnf"] parse
+let () = Env.register_format "dimacs" ["cnf"] Env.base_language parse
   ~desc:"@[<hov>Parser for dimacs format.@]"
-
-
 }
 
-
-
 (*
 Local Variables:
 compile-command: "unset LANG; make -C ../.."

plugins/parser/genequlin.ml

@@ -61,7 +61,7 @@ let scanf s =
 (** the main function *)
 let read_channel env path filename cin =
   (** Find the int theory and the needed operation *)
-  let th_int = Env.find_theory (Env.env_of_library env) ["int"] "Int" in
+  let th_int = Env.read_theory env ["int"] "Int" in
   let leq = ns_find_ls th_int.th_export ["infix <"] in
   let plus_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix +"] in
   let neg_symbol = Theory.ns_find_ls th_int.Theory.th_export ["prefix -"] in
@@ -123,9 +123,9 @@ let read_channel env path filename cin =
   (** Read all the file *)
   let th_uc = Sysutil.fold_channel fold th_uc cin in
   (** Return the map with the theory *)
-  (), Mstr.singleton "EquLin" (close_theory th_uc)
+  Mstr.singleton "EquLin" (close_theory th_uc)
 
-let library_of_env = Env.register_format "EquLin" ["equlin"] read_channel
+let () = Env.register_format "equlin" ["equlin"] Env.base_language read_channel
   ~desc:"@[<hov>Generate@ random@ linear@ arithmetic@ problems.@ \
     The@ first@ line@ gives@ the@ seed.@ Each@ other@ line@ \
     describes@ a@ goal@ and@ contains@ three@ numbers:@]@\n  \

plugins/tptp/tptp_lexer.mll

@@ -246,9 +246,9 @@ and comment_line = parse
     let lb = Lexing.from_channel c in
     Loc.set_file file lb;
     let ast = Loc.with_location (tptp_file token) lb in
-    (), Tptp_typing.typecheck env path ast
+    Tptp_typing.typecheck env path ast
 
-  let _library_of_env = Env.register_format "tptp" ["p";"ax"] read_channel
+  let () = Env.register_format "tptp" ["p";"ax"] Env.base_language read_channel
     ~desc:"TPTP format (CNF FOF FOFX TFF)"
 
 }

plugins/tptp/tptp_typing.ml

@@ -82,9 +82,8 @@ type denv = {
   ts_rat   : tysymbol;
 }
 
-let make_denv lib =
-  let env = Env.env_of_library lib in
-  let get_theory = Env.read_theory ~format:"why" env ["tptp"] in
+let make_denv env =
+  let get_theory s = Env.read_theory env ["tptp"] s in
   let th_univ = get_theory "Univ" in
   let th_ghost = get_theory "Ghost" in
   let th_rat = get_theory "Rat" in
@@ -125,7 +124,7 @@ let defined_arith ~loc denv env impl dw tl =
     | { t_ty = Some {ty_node = Tyapp (ts,[]) }}::_ -> ts
     | _::_ -> error ~loc NonNumeric
     | [] -> error ~loc BadArity in
-  let get_theory = Env.read_theory ~format:"why" denv.de_env ["tptp"] in
+  let get_theory s = Env.read_theory denv.de_env ["tptp"] s in
   let get_int_theory = function
     | DF DFquot -> errorm ~loc "$quotient/2 is not defined on $int"
     | DF (DFquot_e|DFrem_e) -> get_theory "IntDivE"
@@ -667,4 +666,3 @@ let typecheck lib path ast =
     | [] -> add_prop_decl uc Pgoal pr_false t_false
   in
   Mstr.singleton "T" (close_theory uc)
-

plugins/tptp/tptp_typing.mli

@@ -9,6 +9,6 @@
 (*                                                                  *)
 (********************************************************************)
 
-val typecheck : unit Why3.Env.library -> Why3.Env.pathname ->
+val typecheck : Why3.Env.env -> Why3.Env.pathname ->
   Tptp_ast.tptp_file -> Why3.Theory.theory Why3.Stdlib.Mstr.t
 

src/coq-tactic/why3tac.ml

@@ -303,9 +303,9 @@ let print_dep fmt =
 (* the task under construction *)
 let task = ref None
 
-let th_int = lazy (Env.find_theory env ["int"] "Int")
-let th_eucl = lazy (Env.find_theory env ["int"] "EuclideanDivision")
-let th_real = lazy (Env.find_theory env ["real"] "Real")
+let th_int = lazy (Env.read_theory env ["int"] "Int")
+let th_eucl = lazy (Env.read_theory env ["int"] "EuclideanDivision")
+let th_real = lazy (Env.read_theory env ["real"] "Real")
 
 let why_constant_int dep s =
   task := Task.use_export !task (Lazy.force th_int);

src/core/env.ml

@@ -10,8 +10,6 @@
 (********************************************************************)
 
 open Stdlib
-open Ident
-open Theory
 
 (** Library environment *)
 
@@ -22,10 +20,13 @@ type pathname = string list (* library path *)
 
 exception KnownFormat of fformat
 exception UnknownFormat of fformat
-exception UnknownExtension of extension
+exception InvalidFormat of fformat
 exception UnspecifiedFormat
 
-exception LibFileNotFound of pathname
+exception KnownExtension of extension * fformat
+exception UnknownExtension of extension
+
+exception LibraryNotFound of pathname
 exception TheoryNotFound of pathname * string
 exception AmbiguousPath of filename * filename
 
@@ -47,16 +48,80 @@ let create_env = let c = ref (-1) in fun lp -> {
 
 let get_loadpath env = Sstr.elements env.env_path
 
-let read_format_table = Hstr.create 17 (* format name -> read_format *)
-let extensions_table  = Hstr.create 17 (* suffix -> format name *)
+(** Input languages *)
+
+type 'a format_parser = env -> pathname -> filename -> in_channel -> 'a
+
+module Hpath = Hashtbl.Make(struct
+  type t = pathname
+  let hash = Hashtbl.hash
+  let equal = (=)
+end)
+
+type 'a language = {
+  memo : 'a Hpath.t;
+  push : pathname -> 'a -> unit;
+  mutable fmts : (fformat * extension list * Pp.formatted) list;
+}
+
+let base_language = {
+  memo = Hpath.create 17;
+  push = (fun _ _ -> ());
+  fmts = [];
+}
+
+exception LibraryConflict of pathname
+
+let store lang path c =
+  lang.push path c;
+  Hpath.add lang.memo path c
+
+let store lang path c =
+  if path = [] then store lang path c
+  else try
+    let d = Hpath.find lang.memo path in
+    if c != d then raise (LibraryConflict path)
+  with Not_found -> store lang path c
+
+let retrieve_file lang ff path =
+  try Hpath.find lang.memo path
+  with Not_found -> raise (InvalidFormat ff)
+
+let retrieve_lib lang path =
+  try Hpath.find lang.memo path
+  with Not_found -> raise (LibraryNotFound path)
+
+let register_language parent convert = {
+  memo = Hpath.create 17;
+  push = (fun path c -> store parent path (convert c));
+  fmts = [];
+}
+
+let extension_table = ref Mstr.empty
+let format_table = ref Mstr.empty
+let builtin_list = ref []
+
+let register_format ~desc ff extl lang fp =
+  let fp env path fn ch = store lang path (fp env path fn ch) in
+  format_table := Mstr.add_new (KnownFormat ff) ff fp !format_table;
+  let add_ext m e = Mstr.change (function
+    | Some ff -> raise (KnownExtension (e,ff))
+    | None -> Some ff) e m in
+  extension_table := List.fold_left add_ext !extension_table extl;
+  lang.fmts <- (ff,extl,desc) :: lang.fmts
+
+let list_formats lang = List.rev lang.fmts (* older to newer *)
 
-let lookup_format name =
-  try Hstr.find read_format_table name
-  with Not_found -> raise (UnknownFormat name)
+let add_builtin lang bp =
+  let bp path = store lang ("why3" :: path) (bp path) in
+  builtin_list := bp :: !builtin_list
 
-let list_formats () =
-  let add n (_,_,l,desc) acc = (n,l,desc)::acc in
-  Hstr.fold add read_format_table []
+let read_builtin lang path =
+  let read bp = try bp path with Not_found -> () in
+  List.iter read !builtin_list;
+  retrieve_lib lang ("why3" :: path)
+
+(** Input file parsing *)
 
 let get_extension file =
   let s = try Filename.chop_extension file
@@ -66,131 +131,117 @@ let get_extension file =
 
 let get_format file =
   let ext = get_extension file in
-  try Hstr.find extensions_table ext
-  with Not_found -> raise (UnknownExtension ext)
-
-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
-
-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
+  Mstr.find_exn (UnknownExtension ext) ext !extension_table
 
-let read_theory ~format env path th =
-  let _,rl,_,_ = lookup_format format in
-  rl env path th
+let get_format ?format file = match format with
+  | Some ff -> ff
+  | None -> get_format file
 
-let find_theory = read_theory ~format:"why"
+let get_parser ff =
+  Mstr.find_exn (UnknownFormat ff) ff !format_table
 
-(** Navigation in the library *)
+let read_channel ?format lang env file ch =
+  let ff = get_format ?format file in
+  let fp = get_parser ff in
+  fp env [] file ch;
+  retrieve_file lang ff []
+
+let read_file_raw ?format lang env path file =
+  let ff = get_format ?format file in
+  let fp = get_parser ff in
+  let ch = open_in file in
+  begin try fp env path file ch; close_in ch
+  with exn -> close_in ch; raise exn; end;
+  retrieve_file lang ff path
 
-exception InvalidQualifier of string
+let read_file ?format lang env file =
+  read_file_raw ?format lang env [] file
 
-let check_qualifier s =
+(** Navigation in the library *)
+
+let locate_library env path =
+  if path = [] || path = ["why3"]
+    then invalid_arg "Env.locate_library";
+  let check_qualifier s =
     if (s = Filename.parent_dir_name ||
         s = Filename.current_dir_name ||
         Filename.basename s <> s)
-  then raise (InvalidQualifier s)
-
-let locate_lib_file env path exts =
-  if path = [] || path = ["why3"] then raise (LibFileNotFound path);
+    then invalid_arg "Env.locate_library" in
   List.iter check_qualifier path;
   let file = List.fold_left Filename.concat "" path in
   let add_ext ext = file ^ "." ^ ext in
-  let fl = if exts = [] then [file] else List.map add_ext exts in
+  let fl = List.map add_ext (Mstr.keys !extension_table) in
+  if fl = [] then failwith "Env.locate_library (no formats)";
   let add_dir dir = List.map (Filename.concat dir) fl in
   let fl = List.concat (List.map add_dir (get_loadpath env)) in
+  if fl = [] then failwith "Env.locate_library (empty loadpath)";
   match List.filter Sys.file_exists fl with
-  | [] -> raise (LibFileNotFound path)
+  | [] -> raise (LibraryNotFound path)
   | [file] -> file
   | file1 :: file2 :: _ -> raise (AmbiguousPath (file1, file2))
 
-(** Input formats *)
-
 exception CircularDependency of pathname
 
-type 'a contents = 'a * theory Mstr.t
-
-module Hpath = Hashtbl.Make(struct
-  type t = pathname
-  let hash = Hashtbl.hash
-  let equal = (=)
-end)
-
-type 'a library = {
-  lib_env  : env;
-  lib_read : 'a read_format;
-  lib_exts : extension list;
-  lib_memo : ('a contents option) Hpath.t;
-}
+let read_library lang env path =
+  let file = locate_library env path in
+  read_file_raw lang env path file
 
-and 'a read_format =
-  'a library -> pathname -> filename -> in_channel -> 'a contents
+let libstack = Hpath.create 17
 
-let mk_library read exts env = {
-  lib_env  = env;
-  lib_read = read;
-  lib_exts = exts;
-  lib_memo = Hpath.create 17;
-}
-
-let env_of_library lib = lib.lib_env
-
-let read_lib_file lib path =
-  let file = locate_lib_file lib.lib_env path lib.lib_exts in
-  let ic = open_in file in
+let read_library lang env path =
+  if Hpath.mem libstack path then
+    raise (CircularDependency path);
+  Hpath.add libstack path ();
   try
-    Hpath.replace lib.lib_memo path None;
-    let res = lib.lib_read lib path file ic in
-    Hpath.replace lib.lib_memo path (Some res);
-    close_in ic;
-    res
+    let c = read_library lang env path in
+    Hpath.remove libstack path;
+    c
   with e ->
-    Hpath.remove lib.lib_memo path;
-    close_in ic;
+    Hpath.remove libstack path;
     raise e
 
-let read_lib_file lib path =
-  try match Hpath.find lib.lib_memo path with
-    | Some res -> res
-    | None -> raise (CircularDependency path)
-  with Not_found -> read_lib_file lib path
+let read_library lang env = function
+  | "why3" :: path -> read_builtin lang path
+  | path -> read_library lang env path
+
+let read_library lang env path =
+  let path = if path = [] then ["why3"] else path in
+  try Hpath.find lang.memo path with Not_found ->
+  if Hpath.mem base_language.memo path then begin
+    match path with (* loaded for another format *)
+    | "why3" :: _ ->
+        raise (LibraryNotFound path)
+    | _ ->
+        let file = locate_library env path in
+        raise (InvalidFormat (get_format file))
+  end else
+    read_library lang env path
+
+let read_theory env path s =
+  let path = if path = [] then ["why3"; s] else path in
+  let mt = read_library base_language env path in
+  Mstr.find_exn (TheoryNotFound (path,s)) s mt
+
+(* Builtin theories *)
 
-let get_builtin s =
+open Ident
+open Theory
+
+let base_builtin path =
+  let 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
     if s = bool_theory.th_name.id_string then bool_theory else
     if s = unit_theory.th_name.id_string then unit_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_lib_theory lib path th =
-  if path = [] || path = ["why3"] then get_builtin th else
-  let _,mth = read_lib_file lib path in
-  try Mstr.find th mth with Not_found ->
-  raise (TheoryNotFound (path,th))
-
-let register_format ~(desc:Pp.formatted) name exts read =
-  if Hstr.mem read_format_table name then raise (KnownFormat name);
-  let getlib = Wenv.memoize 5 (mk_library read exts) in
-  let rc env file ic = snd (read (getlib env) [] file ic) in
-  let rl env path th = read_lib_theory (getlib env) path th in
-  Hstr.add read_format_table name (rc,rl,exts,desc);
-  List.iter (fun s -> Hstr.replace extensions_table s name) exts;
-  getlib
-
-let locate_lib_file env format path =
-  let _,_,exts,_ = lookup_format format in
-  locate_lib_file env path exts
+    | None -> raise Not_found
+  in
+  match path with
+  | [s] -> Mstr.singleton s (builtin s)
+  | _   -> raise Not_found
+
+let () = add_builtin base_language base_builtin
 
 (* Exception reporting *)
 
@@ -199,24 +250,27 @@ let print_path fmt sl =
 
 let () = Exn_printer.register
   begin fun fmt exn -> match exn with
-  | CircularDependency sl ->
-      Format.fprintf fmt "Circular dependency in %a" print_path sl
-  | LibFileNotFound sl ->
-      Format.fprintf fmt "Library file not found: %a" print_path sl
-  | TheoryNotFound (sl,s) ->
-      Format.fprintf fmt "Theory not found: %a" print_path (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
-  | UnspecifiedFormat ->
-      Format.fprintf fmt "Format not specified"
-  | AmbiguousPath (f1,f2) ->
-      Format.fprintf fmt "Ambiguous path:@ both `%s'@ and `%s'@ match" f1 f2
-  | InvalidQualifier s ->
-      Format.fprintf fmt "Invalid qualifier `%s'" s
+  | CircularDependency sl -> Format.fprintf fmt
+      "Circular dependency in %a" print_path sl
+  | LibraryNotFound sl -> Format.fprintf fmt
+      "Library file not found: %a" print_path sl
+  | TheoryNotFound (sl,s) -> Format.fprintf fmt
+      "Theory %s not found in library %a" s print_path sl
+  | 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
+  | KnownExtension (s,f) -> Format.fprintf fmt
+      "File extension `%s' is already registered for input format %s" s f
+  | UnspecifiedFormat -> Format.fprintf fmt
+      "Format not specified"
+  | AmbiguousPath (f1,f2) -> Format.fprintf fmt
+      "Ambiguous path:@ both %s@ and %s@ match" f1 f2
+  | InvalidFormat f -> Format.fprintf fmt
+      "Input format %s is unsuitable for the desired content" f
+  | LibraryConflict sl -> Format.fprintf fmt
+      "Conflicting definitions for library %a" print_path sl
   | _ -> raise exn
   end
-

src/core/env.mli

@@ -10,22 +10,14 @@
 (********************************************************************)
 
 open Stdlib
-open Theory
 
-(** Local type aliases and exceptions *)
+(** Local type aliases *)
 
 type fformat = string (* format name *)
 type filename = string (* file name *)
 type extension = string (* file extension *)
 type pathname = string list (* library path *)
 
-exception KnownFormat of fformat
-exception UnknownFormat of fformat
-exception UnknownExtension of extension
-exception UnspecifiedFormat
-exception LibFileNotFound of pathname
-exception TheoryNotFound of pathname * string
-
 (** Library environment *)
 
 type env
@@ -41,93 +33,138 @@ val create_env : filename list -> env
 val get_loadpath : env -> filename list
 (** returns the loadpath of a given environment *)
 
-val read_channel :
-  ?format:fformat -> env -> filename -> in_channel -> theory Mstr.t
-(** [read_channel ?format env path 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 [file].
+(** Input languages *)
+
+type 'a language
+
+val base_language : Theory.theory Mstr.t language
+(** [base_language] is the root of the tree of supported languages.
+    Any input language must be translatable into pure theories for
+    the purposes of verification. *)
+
+val register_language : 'a language -> ('b -> 'a) -> 'b language
+(** [register_language parent convert] adds a leaf to the language tree.
+    The [convert] function provides translation from the new language to
+    [parent]. *)
+
+val add_builtin : 'a language -> (pathname -> 'a) -> unit
+(** [add_builtin lang builtin] adds new builtin libraries to [lang].
+    The [builtin] function is called by [read_library] (below) for any
+    library path that starts with "why3" (this prefix is not passed to
+    [builtin]). For all library paths not covered by [builtin] it must
+    raise [Not_found].
+
+    By convention, every builtin theory of the base language is placed
+    under a separate pathname that ends with the name of the theory.
+    For example, the full qualified name of the [Builtin] theory is
+    [why3.Builtin.Builtin]. The name of the theory is duplicated in
+    the library path to ensure that every builtin theory is obtained
+    from a separate call to [builtin], which permits to generate
+    builtin theories on demand.
+
+    If there are several definitions of a builtin library for a given
+    language and path, they must be physically identical, otherwise
+    [LibraryConflict] is raised. For example, if an offspring language
+    provides extended definitions of builtin theories, they must be
+    [convert]'ed into exactly the same singleton [theory Mstr.t] maps
+    as stored for the base language. *)
+
+type 'a format_parser = env -> pathname -> filename -> in_channel -> 'a
+(** [(fn : 'a format_parser) env path file ch] parses the in_channel [ch]
+    and returns the language-specific contents of type ['a]. References
+    to libraries in the input file are resolved via [env]. If the parsed
+    file is itself a library file, the argument [path] contains the fully
+    qualified library path of the file, which can be put in the identifiers.
+    The string argument [file] indicates the origin of the stream (file name)
+    to be used in error messages. *)
 
-    @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 *)
+exception KnownFormat of fformat
+exception KnownExtension of extension * fformat
 
-val read_file : ?format:fformat -> env -> filename -> theory Mstr.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. *)
+val register_format :
+  desc:Pp.formatted ->
+  fformat -> extension list -> 'a language -> 'a format_parser -> unit
+(** [register_format ~desc format_name exts lang parser] registers a new
+    format [fname] for files with extensions from the string list [exts]
+    (without the separating dot).
 
-val read_theory : format:fformat -> env -> pathname -> string -> theory
-(** [read_theory ~format env path th] returns the theory [path.th]
-    from the library. The parameter [format] specifies the format
-    of the library file to look for.
+    @raise KnownFormat [name] if the format is already registered
+    @raise KnownExtension [ext,name] if a parser for [ext] is already
+      registered for format [name] *)
 
-    @raise UnknownFormat [format] if the format is not registered
-    @raise LibFileNotFound [path] if the library file was not found
-    @raise TheoryNotFound if the theory was not found in the file *)
+val list_formats :
+  'a language -> (fformat * extension list * Pp.formatted) list
+(** [list_formats lang] returns the list of registered formats that can
+    be translated to [lang]. Use [list_formats base_language] to obtain
+    the list of all registered formats. *)
 
-val find_theory : env -> pathname -> string -> theory
-(** the same as [read_theory ~format:"why"]
+(** Language-specific parsers *)
 
-    This function is left for compatibility purposes and may be
-    removed in future versions of Why3. *)
+exception InvalidFormat of fformat
+exception UnknownFormat of fformat
+exception UnknownExtension of extension
+exception UnspecifiedFormat
 
-(** Input formats *)
+val read_channel :
+  ?format:fformat -> 'a language -> env -> filename -> in_channel -> 'a
+(** [read_channel ?format lang env file ch] returns the contents of [ch]
+    in language [lang]. When given, [format] enforces the format, otherwise
+    we choose the parser according to [file]'s extension. Nothing ensures
+    that [ch] corresponds to the contents of [file].
 
-type 'a library
-(** part of the environment restricted to a particular format *)
+    @raise InvalidFormat [format] if the format, given in the parameter
+      or determined from the file's extension, does not translate to [lang]
+    @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 *)
 
-type 'a read_format =
-  'a library -> pathname -> filename -> in_channel -> 'a * theory Mstr.t
-(** [(fn : 'a read_format) lib path file ch] parses the channel [ch]
-    and returns the format-specific contents of type ['a] and a set of
-    logical theories. References to the library files of the same format
-    are resolved via [lib]. If the parsed file is itself a part of
-    the library, the argument [path] contains the fully qualified
-    library name of the file, which can be put in the identifiers.
-    The string argument [file] indicates the origin of the stream
-    (e.g. file name) to be used in error messages. *)
+val read_file : ?format:fformat -> 'a language -> env -> filename -> 'a
+(** an open-close wrapper around [read_channel] *)
 
-val register_format :
-  desc:Pp.formatted ->
-  fformat -> extension list -> 'a read_format -> (env -> 'a library)
-(** [register_format fname exts read] registers a new format [fname]
-