Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

Commit 42e2dbe1 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

format-specific environment

parent 0c23f68f
...@@ -374,7 +374,7 @@ install_local: bin/why3 ...@@ -374,7 +374,7 @@ install_local: bin/why3
######## ########
PGM_FILES = pgm_ttree pgm_types pgm_pretty \ PGM_FILES = pgm_ttree pgm_types pgm_pretty \
pgm_module pgm_wp pgm_env pgm_typing pgm_ocaml pgm_main pgm_module pgm_wp pgm_typing pgm_ocaml pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES)) PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
......
...@@ -70,12 +70,11 @@ let scanf s = ...@@ -70,12 +70,11 @@ let scanf s =
(** the main function *) (** the main function *)
let read_channel env path filename cin = let read_channel env path filename cin =
(** Find the int theory and the needed operation *) (** Find the int theory and the needed operation *)
let th_int = Env.find_theory env ["int"] "Int" in let th_int = Env.find_theory (Env.env_of_library env) ["int"] "Int" in
let leq = ns_find_ls th_int.th_export ["infix <"] 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 plus_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix +"] in
let mult_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix *"] in let mult_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix *"] in
let zero = t_int_const "0" in let zero = t_int_const "0" in
(** create a contraint : polynome <= constant *) (** create a contraint : polynome <= constant *)
...@@ -128,6 +127,6 @@ let read_channel env path filename cin = ...@@ -128,6 +127,6 @@ let read_channel env path filename cin =
(** Read all the file *) (** Read all the file *)
let th_uc = Sysutil.fold_channel fold th_uc cin in let th_uc = Sysutil.fold_channel fold th_uc cin in
(** Return the map with the theory *) (** Return the map with the theory *)
Mstr.singleton "EqLin" (close_theory th_uc) (), Mstr.singleton "EqLin" (close_theory th_uc)
let () = Env.register_format "EquLin" ["equlin"] read_channel let library_of_env = Env.register_format "EquLin" ["equlin"] read_channel
...@@ -252,10 +252,10 @@ and comment_line = parse ...@@ -252,10 +252,10 @@ and comment_line = parse
let lb = Lexing.from_channel c in let lb = Lexing.from_channel c in
Loc.set_file file lb; Loc.set_file file lb;
let ast = with_location (tptp_file token) lb in let ast = with_location (tptp_file token) lb in
Tptp_typing.typecheck env path ast (), Tptp_typing.typecheck env path ast
(* let () = Env.register_format "tptp" ["p";"ax"] read_channel *) (* let library_of_env = Env.register_format "tptp" ["p";"ax"] read_channel *)
let () = Env.register_format "tff1" ["p";"ax"] read_channel let library_of_env = Env.register_format "tff1" ["p";"ax"] read_channel
} }
(* (*
......
...@@ -17,6 +17,6 @@ ...@@ -17,6 +17,6 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
val typecheck : Why3.Env.env -> Why3.Env.pathname -> val typecheck : unit Why3.Env.library -> Why3.Env.pathname ->
Tptp_ast.tptp_file -> Why3.Theory.theory Why3.Util.Mstr.t Tptp_ast.tptp_file -> Why3.Theory.theory Why3.Util.Mstr.t
...@@ -26,20 +26,19 @@ open Theory ...@@ -26,20 +26,19 @@ open Theory
type fformat = string (* format name *) type fformat = string (* format name *)
type filename = string (* file name *) type filename = string (* file name *)
type extension = string (* file extension *) type extension = string (* file extension *)
type pathname = string list (* path in an environment *) type pathname = string list (* library path *)
exception KnownFormat of fformat exception KnownFormat of fformat
exception UnknownFormat of fformat exception UnknownFormat of fformat
exception UnknownExtension of extension exception UnknownExtension of extension
exception UnspecifiedFormat exception UnspecifiedFormat
exception ChannelNotFound of pathname exception LibFileNotFound of pathname
exception TheoryNotFound of pathname * string exception TheoryNotFound of pathname * string
exception AmbiguousPath of filename * filename exception AmbiguousPath of filename * filename
type env = { type env = {
env_path : filename list; env_path : filename list;
env_memo : (pathname, theory Mstr.t) Hashtbl.t;
env_tag : Hashweak.tag; env_tag : Hashweak.tag;
} }
...@@ -47,27 +46,30 @@ let env_tag env = env.env_tag ...@@ -47,27 +46,30 @@ 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)
(** Input formats *) (** Environment construction and utilisation *)
type read_channel = let create_env = let c = ref (-1) in fun lp -> {
env -> pathname -> filename -> in_channel -> theory Mstr.t env_path = lp;
env_tag = (incr c; Hashweak.create_tag !c)
}
let read_channel_table = Hashtbl.create 17 (* format name -> read_channel *) let get_loadpath env = env.env_path
let extensions_table = Hashtbl.create 17 (* suffix -> format name *)
let register_format name exts rc = let read_format_table = Hashtbl.create 17 (* format name -> read_format *)
if Hashtbl.mem read_channel_table name then raise (KnownFormat name); let extensions_table = Hashtbl.create 17 (* suffix -> format name *)
Hashtbl.add read_channel_table name (rc,exts);
List.iter (fun s -> Hashtbl.replace extensions_table ("." ^ s) name) exts
let lookup_format name = let lookup_format name =
try Hashtbl.find read_channel_table name try Hashtbl.find read_format_table name
with Not_found -> raise (UnknownFormat name) with Not_found -> raise (UnknownFormat name)
let list_formats () =
let add n (_,_,l) acc = (n,l)::acc in
Hashtbl.fold add read_format_table []
let get_extension file = let get_extension file =
let s = try Filename.chop_extension file let s = try Filename.chop_extension file
with Invalid_argument _ -> raise UnspecifiedFormat in with Invalid_argument _ -> raise UnspecifiedFormat in
let n = String.length s in let n = String.length s + 1 in
String.sub file n (String.length file - n) String.sub file n (String.length file - n)
let get_format file = let get_format file =
...@@ -75,15 +77,12 @@ let get_format file = ...@@ -75,15 +77,12 @@ let get_format file =
try Hashtbl.find extensions_table ext try Hashtbl.find extensions_table ext
with Not_found -> raise (UnknownExtension ext) with Not_found -> raise (UnknownExtension ext)
let real_read_channel ?format env path file ic = let read_channel ?format env file ic =
let name = match format with let name = match format with
| Some name -> name | Some name -> name
| None -> get_format file in | None -> get_format file in
let rc,_ = lookup_format name in let rc,_,_ = lookup_format name in
rc env path file ic rc env file ic
let read_channel ?format env file ic =
real_read_channel ?format env [] file ic
let read_file ?format env file = let read_file ?format env file =
let ic = open_in file in let ic = open_in file in
...@@ -93,69 +92,78 @@ let read_file ?format env file = ...@@ -93,69 +92,78 @@ let read_file ?format env file =
mth mth
with e -> close_in ic; raise e with e -> close_in ic; raise e
let list_formats () = let read_theory ~format env path th =
let add n (_,l) acc = (n,l)::acc in let _,rl,_ = lookup_format format in
Hashtbl.fold add read_channel_table [] rl env path th
let find_theory = read_theory ~format:"why"
(** Environment construction and utilisation *) (** Navigation in the library *)
let create_env = let c = ref (-1) in fun lp -> { exception InvalidQualifier of string
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 let check_qualifier s =
if (s = Filename.parent_dir_name ||
s = Filename.current_dir_name ||
Filename.basename s <> s)
then raise (InvalidQualifier s)
(* looks for file [file] of format [name] in loadpath [lp] *) let locate_lib_file env path exts =
let locate_file name lp path = List.iter check_qualifier path;
let file = List.fold_left Filename.concat "" path in let file = List.fold_left Filename.concat "" path in
let _,sl = lookup_format name in let add_ext ext = file ^ "." ^ ext in
let add_sf sf = file ^ "." ^ sf in let fl = if exts = [] then [file] else List.map add_ext exts 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 add_dir dir = List.map (Filename.concat dir) fl in
let fl = List.concat (List.map add_dir lp) in let fl = List.concat (List.map add_dir env.env_path) in
match List.filter Sys.file_exists fl with match List.filter Sys.file_exists fl with
| [] -> raise (ChannelNotFound path) | [] -> raise (LibFileNotFound path)
| [file] -> file | [file] -> file
| file1 :: file2 :: _ -> raise (AmbiguousPath (file1, file2)) | file1 :: file2 :: _ -> raise (AmbiguousPath (file1, file2))
exception InvalidQualifier of string (** Input formats *)
let check_qualifier s = exception CircularDependency of pathname
if (s = Filename.parent_dir_name ||
s = Filename.current_dir_name || type 'a contents = 'a * theory Mstr.t
Filename.basename s <> s)
then raise (InvalidQualifier s)
let find_channel env f sl = type 'a library = {
List.iter check_qualifier sl; lib_env : env;
let file = locate_file f env.env_path sl in lib_read : 'a read_format;
file, open_in file lib_exts : extension list;
lib_memo : (pathname, 'a contents option) Hashtbl.t;
}
and 'a read_format =
'a library -> pathname -> filename -> in_channel -> 'a contents
let mk_library read exts env = {
lib_env = env;
lib_read = read;
lib_exts = exts;
lib_memo = Hashtbl.create 17;
}
let env_of_library lib = lib.lib_env
let find_library env sl = let read_lib_file lib path =
let file, ic = find_channel env "why" sl in let file = locate_lib_file lib.lib_env path lib.lib_exts in
let ic = open_in file in
try try
Hashtbl.replace env.env_memo sl Mstr.empty; Hashtbl.replace lib.lib_memo path None;
let mth = real_read_channel ~format:"why" env sl file ic in let res = lib.lib_read lib path file ic in
Hashtbl.replace env.env_memo sl mth; Hashtbl.replace lib.lib_memo path (Some res);
close_in ic; close_in ic;
mth res
with e -> with e ->
Hashtbl.remove env.env_memo sl; Hashtbl.remove lib.lib_memo path;
close_in ic; close_in ic;
raise e raise e
let find_library env sl = let read_lib_file lib path =
try Hashtbl.find env.env_memo sl try match Hashtbl.find lib.lib_memo path with
with Not_found -> find_library env sl | Some res -> res
| None -> raise (CircularDependency path)
with Not_found -> read_lib_file lib path
let get_builtin s = let get_builtin s =
if s = builtin_theory.th_name.id_string then builtin_theory else if s = builtin_theory.th_name.id_string then builtin_theory else
...@@ -165,22 +173,40 @@ let get_builtin s = ...@@ -165,22 +173,40 @@ let get_builtin s =
| Some n -> tuple_theory n | Some n -> tuple_theory n
| None -> raise (TheoryNotFound ([],s)) | None -> raise (TheoryNotFound ([],s))
let find_theory env sl s = let read_lib_theory lib path th =
if sl = [] then get_builtin s else if path = [] then get_builtin th else
let mth = find_library env sl in let _,mth = read_lib_file lib path in
try Mstr.find s mth with Not_found -> try Mstr.find th mth with Not_found ->
raise (TheoryNotFound (sl,s)) raise (TheoryNotFound (path,th))
let read_lib_file lib path = fst (read_lib_file lib path)
let register_format name exts read =
if Hashtbl.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
Hashtbl.add read_format_table name (rc,rl,exts);
List.iter (fun s -> Hashtbl.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
(* Exception reporting *) (* Exception reporting *)
let print_path fmt sl =
Pp.print_list (Pp.constant_string ".") Format.pp_print_string fmt sl
let () = Exn_printer.register let () = Exn_printer.register
begin fun fmt exn -> match exn with begin fun fmt exn -> match exn with
| ChannelNotFound sl -> | CircularDependency sl ->
Format.fprintf fmt "Library not found: %a" Format.fprintf fmt "Circular dependency in %a" print_path sl
(Pp.print_list (Pp.constant_string ".") Format.pp_print_string) sl | LibFileNotFound sl ->
Format.fprintf fmt "Library file not found: %a" print_path sl
| TheoryNotFound (sl,s) -> | TheoryNotFound (sl,s) ->
Format.fprintf fmt "Theory not found: %a.%s" Format.fprintf fmt "Theory not found: %a.%s" print_path sl s
(Pp.print_list (Pp.constant_string ".") Format.pp_print_string) sl s
| KnownFormat s -> | KnownFormat s ->
Format.fprintf fmt "Format %s is already registered" s Format.fprintf fmt "Format %s is already registered" s
| UnknownFormat s -> | UnknownFormat s ->
......
...@@ -17,53 +17,44 @@ ...@@ -17,53 +17,44 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
(** Library environment *) open Util
open Theory
type env
val env_tag : env -> Hashweak.tag
module Wenv : Hashweak.S with type key = env
(** Local type aliases and exceptions *) (** Local type aliases and exceptions *)
type fformat = string (* format name *) type fformat = string (* format name *)
type filename = string (* file name *) type filename = string (* file name *)
type extension = string (* file extension *) type extension = string (* file extension *)
type pathname = string list (* path in an environment *) type pathname = string list (* library path *)
exception KnownFormat of fformat exception KnownFormat of fformat
exception UnknownFormat of fformat exception UnknownFormat of fformat
exception UnknownExtension of extension exception UnknownExtension of extension
exception UnspecifiedFormat exception UnspecifiedFormat
exception LibFileNotFound of pathname
exception ChannelNotFound of pathname
exception TheoryNotFound of pathname * string exception TheoryNotFound of pathname * string
(** Input formats *) (** Library environment *)
open Theory type env
val env_tag : env -> Hashweak.tag
type read_channel = module Wenv : Hashweak.S with type key = env
env -> pathname -> filename -> in_channel -> theory Util.Mstr.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. *)
val register_format : fformat -> extension list -> read_channel -> unit val create_env : filename list -> env
(** [register_format name extensions fn] registers a new format (** creates an environment from a "loadpath", a list of directories
called [name], for files with extensions in the string list containing loadable Why3/WhyML/etc files *)
[extensions] (separating dot not included);
[fn] is the function to perform parsing.
@raise KnownFormat [name] if the format is already registered *) val get_loadpath : env -> filename list
(** returns the loadpath of a given environment *)
val read_channel : val read_channel :
?format:fformat -> env -> filename -> in_channel -> theory Util.Mstr.t ?format:fformat -> env -> filename -> in_channel -> theory Mstr.t
(** [read_channel ?format env path file ch] returns the theories in [ch]. (** [read_channel ?format env path file ch] returns the theories in [ch].
When given, [format] enforces the format, otherwise we choose When given, [format] enforces the format, otherwise we choose
the format according to [file]'s extension. Nothing ensures the format according to [file]'s extension. Nothing ensures
that [ch] corresponds to the contents of [f]. that [ch] corresponds to the contents of [file].
@raise UnknownFormat [format] if the format is not registered @raise UnknownFormat [format] if the format is not registered
@raise UnknownExtension [s] if the extension [s] is not known @raise UnknownExtension [s] if the extension [s] is not known
...@@ -71,35 +62,79 @@ val read_channel : ...@@ -71,35 +62,79 @@ val read_channel :
@raise UnspecifiedFormat if format is not given and [file] @raise UnspecifiedFormat if format is not given and [file]
has no extension *) has no extension *)
val read_file : ?format:fformat -> env -> filename -> theory Util.Mstr.t val read_file : ?format:fformat -> env -> filename -> theory Mstr.t
(** [read_file ?format env file] returns the theories in [file]. (** [read_file ?format env file] returns the theories in [file].
When given, [format] enforces the format, otherwise we choose When given, [format] enforces the format, otherwise we choose
the format according to [file]'s extension. *) the format according to [file]'s extension. *)
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] speicifies the format
of the library file to look for.
@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 find_theory : env -> pathname -> string -> theory
(** the same as [read_theory ~format:"why"]
This function is left for compatibility purposes and may be
removed in future versions of Why3. *)
(** Input formats *)
type 'a library
(** part of the environment restricted to a particular format *)
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 register_format :
fformat -> extension list -> 'a read_format -> (env -> 'a library)
(** [register_format fname exts read] registers a new format [fname]
for files with extensions from the string list [exts] (without
the separating dot); [read] is the function to perform parsing.
Returns a function that maps an environment to a format-specific
library inside it.
@raise KnownFormat [name] if the format is already registered *)
val env_of_library : 'a library -> env
(** [env_of_library lib] returns the environment of [lib] *)
val list_formats : unit -> (fformat * extension list) list val list_formats : unit -> (fformat * extension list) list
(** [list_formats ()] returns the list of registered formats *)
(** Environment construction and utilisation *) val read_lib_file : 'a library -> pathname -> 'a
(** [read_lib_file lib path] retrieves the contents of a library file
val create_env : filename list -> env @raise LibFileNotFound [path] if the library file was not found *)
(** creates an environment from a "loadpath", a list of directories
containing loadable Why3/WhyML/etc files *)
val create_env_of_loadpath : filename list -> env val read_lib_theory : 'a library -> pathname -> string -> theory
(** the same as [create_env], will be removed in some future version *) (** [read_lib_theory lib path th] returns the theory [path.th]
from the library. This is the same as [read_theory] above,
but the format is determined by [lib] and not by the extra
[format] parameter.
val get_loadpath : env -> filename list @raise LibFileNotFound [path] if the library file was not found
(** returns the loadpath of a given environment *) @raise TheoryNotFound if the theory was not found in the file *)
val find_channel : env -> fformat -> pathname -> filename * in_channel val locate_lib_file : env -> fformat -> pathname -> filename
(** finds an input channel in a given environment, knowing its format (** [locate_lib_file env format path] finds a library file in a given
and its name (presented as a list of strings); a filename is also environment, knowing its format and its library path
returned, to be used in logs or error messages.
@raise ChannelNotFound [sl] if the channel [sl] was not found This is a low-level function that allows to accees a library file
@raise UnknownFormat [f] if the format is not registered *) without parsing it. Do not use it without a good reason to do.
val find_theory : env -> pathname -> string -> theory @raise LibFileNotFound [path] if the library file was not found
(** a special case of [find_channel] that returns a particular theory, @raise UnknownFormat [format] if the format is not registered *)
using the format ["why"]
@raise TheoryNotFound if the theory was not found in a channel *)
...@@ -174,7 +174,8 @@ let load_driver = let driver_tag = ref (-1) in fun env file -> ...@@ -174,7 +174,8 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
let add_theory { thr_name = (loc,q); thr_rules = trl } = let add_theory { thr_name = (loc,q); thr_rules = trl } =
let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
let th = let th =
try Env.find_theory env f id with e -> raise (Loc.Located (loc,e)) try Env.read_theory ~format:"why" env f id
with e -> raise (Loc.Located (loc,e))
in in
qualid := q; qualid := q;
List.iter (add_local th) trl List.iter (add_local th) trl
......
...@@ -394,18 +394,13 @@ let output_theory drv fname _tname th task dir = ...@@ -394,18 +394,13 @@ let output_theory drv fname _tname th task dir =
Driver.print_task ?old drv (formatter_of_out_channel cout) task; Driver.print_task ?old drv (formatter_of_out_channel cout) task;
close_out cout