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 a3109482 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Env: separate library memoization tables per Env.env

parent f34fcfd3
...@@ -40,7 +40,7 @@ module Wenv = Weakhtbl.Make(struct type t = env let tag = env_tag end) ...@@ -40,7 +40,7 @@ module Wenv = Weakhtbl.Make(struct type t = env let tag = env_tag end)
(** Environment construction and utilisation *) (** Environment construction and utilisation *)
let create_env = let c = ref (-1) in fun lp -> { let create_env = let c = ref (-1) in fun lp -> {
env_path = List.fold_right Sstr.add lp Sstr.empty; env_path = Sstr.of_list lp;
env_tag = (incr c; Weakhtbl.create_tag !c) env_tag = (incr c; Weakhtbl.create_tag !c)
} }
...@@ -59,18 +59,18 @@ module Hpath = Hashtbl.Make(struct ...@@ -59,18 +59,18 @@ module Hpath = Hashtbl.Make(struct
end) end)
type 'a language = { type 'a language = {
memo : 'a Hpath.t; memo : 'a Hpath.t Wenv.t;
push : pathname -> 'a -> unit; push : env -> pathname -> 'a -> unit;
regf : format_info -> unit format_parser -> unit; regf : format_info -> unit format_parser -> unit;
regb : (pathname -> unit) -> unit; regb : (env -> pathname -> unit) -> unit;
mutable fmts : unit format_parser Mstr.t; mutable fmts : unit format_parser Mstr.t;
mutable bins : (pathname -> unit) list; mutable bins : (env -> pathname -> unit) list;
mutable info : format_info list; mutable info : format_info list;
} }
let base_language = { let base_language = {
memo = Hpath.create 17; memo = Wenv.create 3;
push = (fun _ _ -> ()); push = (fun _ _ _ -> ());
regf = (fun _ _ -> ()); regf = (fun _ _ -> ());
regb = (fun _ -> ()); regb = (fun _ -> ());
fmts = Mstr.empty; fmts = Mstr.empty;
...@@ -80,19 +80,17 @@ let base_language = { ...@@ -80,19 +80,17 @@ let base_language = {
exception LibraryConflict of pathname exception LibraryConflict of pathname
let store lang path c = let store lang env path c =
lang.push path c; let ht = try Wenv.find lang.memo env with Not_found ->
Hpath.add lang.memo path c let ht = Hpath.create 17 in Wenv.set lang.memo env ht; ht in
match path with
let store lang path c = match path with
| "why3" :: _ -> | "why3" :: _ ->
begin try begin try
let d = Hpath.find lang.memo path in if Hpath.find ht path != c then raise (LibraryConflict path)
if c != d then raise (LibraryConflict path) with Not_found -> lang.push env path c; Hpath.add ht path c end
with Not_found -> store lang path c end
| _ -> | _ ->
assert (path = [] || not (Hpath.mem lang.memo path)); assert (path = [] || not (Hpath.mem ht path));
store lang path c lang.push env path c; Hpath.add ht path c
let register_format lang (ff,_,_ as inf) fp = let register_format lang (ff,_,_ as inf) fp =
lang.regf inf fp; lang.regf inf fp;
...@@ -104,8 +102,8 @@ let add_builtin lang bp = ...@@ -104,8 +102,8 @@ let add_builtin lang bp =
lang.bins <- bp :: lang.bins lang.bins <- bp :: lang.bins
let register_language parent convert = { let register_language parent convert = {
memo = Hpath.create 17; memo = Wenv.create 3;
push = (fun path c -> store parent path (convert c)); push = (fun env path c -> store parent env path (convert c));
regf = (fun inf fp -> register_format parent inf fp); regf = (fun inf fp -> register_format parent inf fp);
regb = (fun bp -> add_builtin parent bp); regb = (fun bp -> add_builtin parent bp);
fmts = Mstr.empty; fmts = Mstr.empty;
...@@ -116,13 +114,13 @@ let register_language parent convert = { ...@@ -116,13 +114,13 @@ let register_language parent convert = {
let extension_table = ref Mstr.empty let extension_table = ref Mstr.empty
let register_format ~desc lang ff extl fp = let register_format ~desc lang ff extl fp =
let fp env path fn ch = store lang path (fp env path fn ch) in let fp env path fn ch = store lang env path (fp env path fn ch) in
register_format lang (ff,extl,desc) fp; register_format lang (ff,extl,desc) fp;
let add_ext m e = Mstr.add e ff m in let add_ext m e = Mstr.add e ff m in
extension_table := List.fold_left add_ext !extension_table extl extension_table := List.fold_left add_ext !extension_table extl
let add_builtin lang bp = let add_builtin lang bp =
let bp path = store lang ("why3" :: path) (bp path) in let bp env path = store lang env ("why3" :: path) (bp path) in
add_builtin lang bp add_builtin lang bp
let list_formats lang = let list_formats lang =
...@@ -154,9 +152,8 @@ let get_parser lang ff = ...@@ -154,9 +152,8 @@ let get_parser lang ff =
let read_channel ?format lang env file ch = let read_channel ?format lang env file ch =
let ff = get_format ?format file in let ff = get_format ?format file in
let fp = get_parser lang ff in get_parser lang ff env [] file ch;
fp env [] file ch; Hpath.find (Wenv.find lang.memo env) []
Hpath.find lang.memo []
let read_lib_file ?format lang env path file = let read_lib_file ?format lang env path file =
let ff = get_format ?format file in let ff = get_format ?format file in
...@@ -167,7 +164,7 @@ let read_lib_file ?format lang env path file = ...@@ -167,7 +164,7 @@ let read_lib_file ?format lang env path file =
let read_file ?format lang env file = let read_file ?format lang env file =
read_lib_file ?format lang env [] file; read_lib_file ?format lang env [] file;
Hpath.find lang.memo [] Hpath.find (Wenv.find lang.memo env) []
(** Library file parsing *) (** Library file parsing *)
...@@ -196,7 +193,7 @@ exception CircularDependency of pathname ...@@ -196,7 +193,7 @@ exception CircularDependency of pathname
let read_library lang env = function let read_library lang env = function
| "why3" :: path -> | "why3" :: path ->
let read bp = try bp path with Not_found -> () in let read bp = try bp env path with Not_found -> () in
List.iter read lang.bins List.iter read lang.bins
| path -> | path ->
let file = locate_library env path in let file = locate_library env path in
...@@ -217,9 +214,9 @@ let read_library lang env path = ...@@ -217,9 +214,9 @@ let read_library lang env path =
let read_library lang env path = let read_library lang env path =
let path = if path = [] then ["why3"] else path in let path = if path = [] then ["why3"] else path in
try Hpath.find lang.memo path with Not_found -> try Hpath.find (Wenv.find lang.memo env) path with Not_found ->
read_library lang env path; read_library lang env path;
try Hpath.find lang.memo path with Not_found -> try Hpath.find (Wenv.find lang.memo env) path with Not_found ->
raise (LibraryNotFound path) raise (LibraryNotFound path)
let read_theory env path s = let read_theory env path s =
......
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