Commit 05ed85d0 authored by François Bobot's avatar François Bobot

driver : add the import directive which include the content

	 of a file into a driver

include "toto.drv.import"
parent 5ccab507
......@@ -57,11 +57,22 @@ let load_plugin dir (byte,nat) =
Config.Dynlink.loadfile_private file
let load_file file =
let basename = Filename.dirname file in
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let f = Driver_lexer.parse_file lb in
close_in c;
let to_close = Stack.create () in
Stack.push c to_close;
let input_lexer s =
let filename = Sysutil.absolutize_filename basename s in
let c = open_in filename in
Stack.push c to_close;
let lb = Lexing.from_channel c in
Loc.set_file filename lb;
lb
in
let f = Driver_lexer.parse_file input_lexer lb in
Stack.iter close_in to_close;
f
exception Duplicate of string
......@@ -124,8 +135,8 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
in
let add_local th = function
| Rprelude s ->
let l = try Mid.find th.th_name !thprelude with Not_found -> [] in
thprelude := Mid.add th.th_name (l @ [s]) !thprelude
let l = Mid.find_default th.th_name [] !thprelude in
thprelude := Mid.add th.th_name (s::l) !thprelude
| Rsyntaxts (c,q,s) ->
let td = syntax_type (find_ts th q) s in
add_meta th td (if c then meta_cl else meta)
......@@ -159,15 +170,14 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
List.iter (add_local th) trl
in
List.iter add_theory f.f_rules;
transform := List.rev !transform;
incr driver_tag;
{
drv_env = env;
drv_printer = !printer;
drv_prelude = !prelude;
drv_prelude = List.rev !prelude;
drv_filename = !filename;
drv_transform = !transform;
drv_thprelude = !thprelude;
drv_transform = List.rev !transform;
drv_thprelude = Mid.map List.rev !thprelude;
drv_meta = !meta;
drv_meta_cl = !meta_cl;
drv_regexps = List.rev !regexps;
......
......@@ -92,6 +92,8 @@ rule token = parse
{ OPERATOR op }
| "\""
{ STRING (string lexbuf) }
| "import" space* "\""
{ INPUT (string lexbuf) }
| eof
{ EOF }
| _ as c
......@@ -103,5 +105,21 @@ rule token = parse
let with_location f lb =
try f lb with e -> raise (Loc.Located (loc lb, e))
let parse_file = with_location (Driver_parser.file token)
let parse_file input_lexbuf lexbuf =
let s = Stack.create () in
Stack.push lexbuf s;
let rec multifile lex_dumb =
let lexbuf = Stack.top s in
let tok = token lexbuf in
Loc.transfer_loc lexbuf lex_dumb;
match tok with
| INPUT filename ->
Stack.push (input_lexbuf filename) s;
multifile lex_dumb
| EOF -> ignore (Stack.pop s);
if Stack.is_empty s then EOF else multifile lex_dumb
| _ -> tok in
let lex_dumb = Lexing.from_function (fun _ _ -> assert false) in
Loc.transfer_loc lexbuf lex_dumb;
with_location (Driver_parser.file multifile) lex_dumb
}
......@@ -26,6 +26,8 @@
let prefix s = "prefix " ^ s
%}
%token <string> INPUT /* never reaches the parser */
%token <int> INTEGER
%token <string> IDENT
%token <string> STRING
......
......@@ -163,11 +163,7 @@ let set_provers rc provers =
let family = Mstr.fold set_prover provers [] in
set_family rc "prover" family
let absolute_filename dirname f =
if Filename.is_relative f then
Filename.concat dirname f
else
f
let absolute_filename = Sysutil.absolutize_filename
let load_prover dirname provers (id,section) =
Mstr.add id
......
......@@ -30,6 +30,11 @@ let set_file file lb =
lb.Lexing.lex_curr_p <-
{ lb.Lexing.lex_curr_p with Lexing.pos_fname = file }
let transfer_loc lb_from lb_to =
lb_to.lex_start_p <- lb_from.lex_start_p;
lb_to.lex_curr_p <- lb_from.lex_curr_p
(*s Error locations. *)
let finally ff f x =
......@@ -86,6 +91,7 @@ let string =
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Located (loc,e) ->
fprintf fmt "%a:@\n%a@\n" gen_report_position loc Exn_printer.exn_printer e
fprintf fmt "%a:@\n%a@\n" gen_report_position loc
Exn_printer.exn_printer e
| _ -> raise exn)
......@@ -25,6 +25,8 @@ val current_offset : int ref
val reloc : Lexing.position -> Lexing.position
val set_file : string -> Lexing.lexbuf -> unit
val transfer_loc : Lexing.lexbuf -> Lexing.lexbuf -> unit
(* locations in files *)
type position
......
......@@ -174,6 +174,12 @@ let relativize_filename base f =
in
rebuild (aux (path_of_file base) (path_of_file f))
let absolutize_filename dirname f =
if Filename.is_relative f then
Filename.concat dirname f
else
f
(*
let p1 = relativize_filename "/bin/bash" "src/f.why"
......
......@@ -68,3 +68,7 @@ val path_of_file : string -> string list
val relativize_filename : string -> string -> string
(** [relativize_filename base filename] relativize the filename
[filename] according to [base] *)
val absolutize_filename : string -> string -> string
(** [absolutize_filename base filename] absolutize the filename
[filename] according to [base] *)
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