Commit 2b086611 authored by Andrei Paskevich's avatar Andrei Paskevich

Env: only read libraries of appropriate languages

parent 89d56e7e
...@@ -132,7 +132,7 @@ let parse _env _path filename cin = ...@@ -132,7 +132,7 @@ let parse _env _path filename cin =
let th_uc = Theory.add_prop_decl th_uc Decl.Pgoal pr Term.t_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 () = Env.register_format "dimacs" ["cnf"] Env.base_language parse let () = Env.register_format Env.base_language "dimacs" ["cnf"] parse
~desc:"@[<hov>Parser for dimacs format.@]" ~desc:"@[<hov>Parser for dimacs format.@]"
} }
......
...@@ -125,7 +125,7 @@ let read_channel env path filename cin = ...@@ -125,7 +125,7 @@ let read_channel env path filename cin =
(** Return the map with the theory *) (** Return the map with the theory *)
Mstr.singleton "EquLin" (close_theory th_uc) Mstr.singleton "EquLin" (close_theory th_uc)
let () = Env.register_format "equlin" ["equlin"] Env.base_language read_channel let () = Env.register_format Env.base_language "equlin" ["equlin"] read_channel
~desc:"@[<hov>Generate@ random@ linear@ arithmetic@ problems.@ \ ~desc:"@[<hov>Generate@ random@ linear@ arithmetic@ problems.@ \
The@ first@ line@ gives@ the@ seed.@ Each@ other@ line@ \ The@ first@ line@ gives@ the@ seed.@ Each@ other@ line@ \
describes@ a@ goal@ and@ contains@ three@ numbers:@]@\n \ describes@ a@ goal@ and@ contains@ three@ numbers:@]@\n \
......
...@@ -248,7 +248,7 @@ and comment_line = parse ...@@ -248,7 +248,7 @@ and comment_line = parse
let ast = Loc.with_location (tptp_file token) lb in let ast = Loc.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"] Env.base_language read_channel let () = Env.register_format Env.base_language "tptp" ["p";"ax"] read_channel
~desc:"TPTP format (CNF FOF FOFX TFF)" ~desc:"TPTP format (CNF FOF FOFX TFF)"
} }
......
...@@ -52,6 +52,8 @@ let get_loadpath env = Sstr.elements env.env_path ...@@ -52,6 +52,8 @@ let get_loadpath env = Sstr.elements env.env_path
type 'a format_parser = env -> pathname -> filename -> in_channel -> 'a type 'a format_parser = env -> pathname -> filename -> in_channel -> 'a
type format_info = fformat * extension list * Pp.formatted
module Hpath = Hashtbl.Make(struct module Hpath = Hashtbl.Make(struct
type t = pathname type t = pathname
let hash = Hashtbl.hash let hash = Hashtbl.hash
...@@ -61,13 +63,21 @@ end) ...@@ -61,13 +63,21 @@ end)
type 'a language = { type 'a language = {
memo : 'a Hpath.t; memo : 'a Hpath.t;
push : pathname -> 'a -> unit; push : pathname -> 'a -> unit;
mutable fmts : (fformat * extension list * Pp.formatted) list; regf : format_info -> unit format_parser -> unit;
regb : (pathname -> unit) -> unit;
mutable fmts : unit format_parser Mstr.t;
mutable bins : (pathname -> unit) list;
mutable info : format_info list;
} }
let base_language = { let base_language = {
memo = Hpath.create 17; memo = Hpath.create 17;
push = (fun _ _ -> ()); push = (fun _ _ -> ());
fmts = []; regf = (fun _ _ -> ());
regb = (fun _ -> ());
fmts = Mstr.empty;
bins = [];
info = [];
} }
exception LibraryConflict of pathname exception LibraryConflict of pathname
...@@ -76,50 +86,50 @@ let store lang path c = ...@@ -76,50 +86,50 @@ let store lang path c =
lang.push path c; lang.push path c;
Hpath.add lang.memo path c Hpath.add lang.memo path c
let store lang path c = let store lang path c = match path with
if path = [] then store lang path c | "why3" :: _ ->
else try begin try
let d = Hpath.find lang.memo path in let d = Hpath.find lang.memo path in
if c != d then raise (LibraryConflict path) if c != d then raise (LibraryConflict path)
with Not_found -> store lang path c with Not_found -> store lang path c end
| _ ->
let retrieve_file lang ff path = assert (path = [] || not (Hpath.mem lang.memo path));
try Hpath.find lang.memo path store lang path c
with Not_found -> raise (InvalidFormat ff)
let register_format lang (ff,_,_ as inf) fp =
lang.regf inf fp;
lang.fmts <- Mstr.add_new (KnownFormat ff) ff fp lang.fmts;
lang.info <- inf :: lang.info
let retrieve_lib lang path = let add_builtin lang bp =
try Hpath.find lang.memo path lang.regb bp;
with Not_found -> raise (LibraryNotFound path) lang.bins <- bp :: lang.bins
let register_language parent convert = { let register_language parent convert = {
memo = Hpath.create 17; memo = Hpath.create 17;
push = (fun path c -> store parent path (convert c)); push = (fun path c -> store parent path (convert c));
fmts = []; regf = (fun inf fp -> register_format parent inf fp);
regb = (fun bp -> add_builtin parent bp);
fmts = Mstr.empty;
bins = [];
info = [];
} }
let extension_table = ref Mstr.empty 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 register_format ~desc lang ff extl 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 let add_ext m e = Mstr.change (function
| Some ff -> raise (KnownExtension (e,ff)) | Some ff -> raise (KnownExtension (e,ff))
| None -> Some ff) e m in | None -> Some ff) e m in
extension_table := List.fold_left add_ext !extension_table extl; extension_table := List.fold_left add_ext !extension_table extl;
lang.fmts <- (ff,extl,desc) :: lang.fmts let fp env path fn ch = store lang path (fp env path fn ch) in
register_format lang (ff,extl,desc) fp
let list_formats lang = List.rev lang.fmts (* older to newer *)
let add_builtin lang bp = let add_builtin lang bp =
let bp path = store lang ("why3" :: path) (bp path) in let bp path = store lang ("why3" :: path) (bp path) in
builtin_list := bp :: !builtin_list add_builtin lang bp
let read_builtin lang path = let list_formats lang = List.rev lang.info (* older to newer *)
let read bp = try bp path with Not_found -> () in
List.iter read !builtin_list;
retrieve_lib lang ("why3" :: path)
(** Input file parsing *) (** Input file parsing *)
...@@ -129,35 +139,37 @@ let get_extension file = ...@@ -129,35 +139,37 @@ let get_extension file =
let n = String.length s + 1 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 ext = get_extension file in
Mstr.find_exn (UnknownExtension ext) ext !extension_table
let get_format ?format file = match format with let get_format ?format file = match format with
| Some ff -> ff | Some ff -> ff
| None -> get_format file | None ->
let ext = get_extension file in
Mstr.find_exn (UnknownExtension ext) ext !extension_table
let get_parser ff = let get_parser lang ff =
Mstr.find_exn (UnknownFormat ff) ff !format_table try Mstr.find ff lang.fmts
with Not_found ->
if Mstr.mem ff base_language.fmts
then raise (InvalidFormat ff)
else raise (UnknownFormat 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 ff in let fp = get_parser lang ff in
fp env [] file ch; fp env [] file ch;
retrieve_file lang ff [] Hpath.find lang.memo []
let read_file_raw ?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
let fp = get_parser ff in let fp = get_parser lang ff in
let ch = open_in file in let ch = open_in file in
begin try fp env path file ch; close_in ch try fp env path file ch; close_in ch
with exn -> close_in ch; raise exn; end; with exn -> close_in ch; raise exn
retrieve_file lang ff path
let read_file ?format lang env file = let read_file ?format lang env file =
read_file_raw ?format lang env [] file read_lib_file ?format lang env [] file;
Hpath.find lang.memo []
(** Navigation in the library *) (** Library file parsing *)
let locate_library env path = let locate_library env path =
if path = [] || path = ["why3"] if path = [] || path = ["why3"]
...@@ -182,40 +194,33 @@ let locate_library env path = ...@@ -182,40 +194,33 @@ let locate_library env path =
exception CircularDependency of pathname exception CircularDependency of pathname
let read_library lang env path = let read_library lang env = function
let file = locate_library env path in | "why3" :: path ->
read_file_raw lang env path file let read bp = try bp path with Not_found -> () in
List.iter read lang.bins
| path ->
let file = locate_library env path in
read_lib_file lang env path file
let libstack = Hpath.create 17 let libstack = Hpath.create 17
let read_library lang env path = let read_library lang env path =
if Hpath.mem libstack path then if Hpath.mem libstack path then
raise (CircularDependency path); raise (CircularDependency path);
Hpath.add libstack path ();
try try
let c = read_library lang env path in Hpath.add libstack path ();
Hpath.remove libstack path; read_library lang env path;
c Hpath.remove libstack path
with e -> with exn ->
Hpath.remove libstack path; Hpath.remove libstack path;
raise e raise exn
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 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 lang.memo path with Not_found ->
if Hpath.mem base_language.memo path then begin read_library lang env path;
match path with (* loaded for another format *) try Hpath.find lang.memo path with Not_found ->
| "why3" :: _ -> raise (LibraryNotFound path)
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 read_theory env path s =
let path = if path = [] then ["why3"; s] else path in let path = if path = [] then ["why3"; s] else path in
...@@ -269,8 +274,8 @@ let () = Exn_printer.register ...@@ -269,8 +274,8 @@ let () = Exn_printer.register
| AmbiguousPath (f1,f2) -> Format.fprintf fmt | AmbiguousPath (f1,f2) -> Format.fprintf fmt
"Ambiguous path:@ both %s@ and %s@ match" f1 f2 "Ambiguous path:@ both %s@ and %s@ match" f1 f2
| InvalidFormat f -> Format.fprintf fmt | InvalidFormat f -> Format.fprintf fmt
"Input format %s is unsuitable for the desired content" f "Input format `%s' is unsuitable for the desired content" f
| LibraryConflict sl -> Format.fprintf fmt | LibraryConflict sl -> Format.fprintf fmt
"Conflicting definitions for library %a" print_path sl "Conflicting definitions for builtin library %a" print_path sl
| _ -> raise exn | _ -> raise exn
end end
...@@ -83,10 +83,10 @@ exception KnownExtension of extension * fformat ...@@ -83,10 +83,10 @@ exception KnownExtension of extension * fformat
val register_format : val register_format :
desc:Pp.formatted -> desc:Pp.formatted ->
fformat -> extension list -> 'a language -> 'a format_parser -> unit 'a language -> fformat -> extension list -> 'a format_parser -> unit
(** [register_format ~desc format_name exts lang parser] registers a new (** [register_format ~desc lang fname exts parser] registers a new format
format [fname] for files with extensions from the string list [exts] [fname] for files with extensions from the string list [exts] (without
(without the separating dot). the separating dot).
@raise KnownFormat [name] if the format is already registered @raise KnownFormat [name] if the format is already registered
@raise KnownExtension [ext,name] if a parser for [ext] is already @raise KnownExtension [ext,name] if a parser for [ext] is already
......
...@@ -9,10 +9,4 @@ ...@@ -9,10 +9,4 @@
(* *) (* *)
(********************************************************************) (********************************************************************)
val parse_logic_file : val parse_program_file : Ptree.incremental -> Lexing.lexbuf -> unit
Env.env -> Env.pathname -> Lexing.lexbuf -> Theory.theory Stdlib.Mstr.t
val parse_program_file :
Ptree.incremental -> Lexing.lexbuf -> unit
val token_counter : Lexing.lexbuf -> int * int
...@@ -232,26 +232,13 @@ rule token = parse ...@@ -232,26 +232,13 @@ rule token = parse
open_file token (Lexing.from_string "") inc; open_file token (Lexing.from_string "") inc;
Loc.with_location (program_file token) lb Loc.with_location (program_file token) lb
let token_counter lb =
let rec loop in_annot a p =
match token lb with
| LEFTBRC -> assert (not in_annot); loop true a p
| RIGHTBRC -> assert in_annot; loop false a p
| EOF -> assert (not in_annot); (a,p)
| _ ->
if in_annot
then loop in_annot (a+1) p
else loop in_annot a (p+1)
in
loop false 0 0
let read_channel env path file c = let read_channel env path file c =
let lb = Lexing.from_channel c in let lb = Lexing.from_channel c in
Loc.set_file file lb; Loc.set_file file lb;
parse_logic_file env path lb parse_logic_file env path lb
let () = Env.register_format "why" ["why"] Env.base_language read_channel let () = Env.register_format Env.base_language "why" ["why"] read_channel
~desc:"Why@ logical@ language" ~desc:"WhyML@ logical@ language"
} }
(* (*
......
...@@ -31,5 +31,5 @@ let read_channel env path file c = ...@@ -31,5 +31,5 @@ let read_channel env path file c =
end; end;
mm, tm mm, tm
let () = Env.register_format "whyml" ["mlw"] mlw_language read_channel let () = Env.register_format mlw_language "whyml" ["mlw"] read_channel
~desc:"WhyML programming language" ~desc:"WhyML@ programming@ language"
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