Commit 487d866f authored by Andrei Paskevich's avatar Andrei Paskevich

session: add optional "format" attribute for <file>

parent b0c5c8d7
......@@ -816,7 +816,7 @@ let () =
else
try
Debug.dprintf debug "[Info] adding file %s in database@." fn;
ignore (M.add_file (env_session()) fn)
ignore (M.add_file (env_session()) ?format:!opt_parser fn)
with e ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" fn
Exn_printer.exn_printer e;
......
......@@ -101,6 +101,7 @@ and 'a theory =
and 'a file =
{ mutable file_key : 'a;
file_name : string;
file_format : string option;
file_parent : 'a session;
mutable file_theories: 'a theory list;
(** Not mutated after the creation *)
......@@ -408,8 +409,8 @@ let save_theory provers fmt t =
fprintf fmt "@]@\n</theory>"
let save_file provers fmt _ f =
fprintf fmt "@\n@[<v 1><file@ name=\"%a\"@ verified=\"%b\"@ expanded=\"%b\">"
save_string f.file_name f.file_verified f.file_expanded;
fprintf fmt "@\n@[<v 1><file@ name=\"%a\"@ %averified=\"%b\"@ expanded=\"%b\">"
save_string f.file_name (opt "format") f.file_format f.file_verified f.file_expanded;
List.iter (save_theory provers fmt) f.file_theories;
fprintf fmt "@]@\n</file>"
......@@ -675,18 +676,19 @@ let raw_add_theory ~(keygen:'a keygen) mfile thname exp =
let mth = { theory_name = thname;
theory_key = key;
theory_parent = mfile;
theory_goals = [] ;
theory_goals = [];
theory_verified = false;
theory_expanded = exp;
}
in
mth
let raw_add_file ~(keygen:'a keygen) session f exp =
let raw_add_file ~(keygen:'a keygen) session f fmt exp =
let key = keygen () in
let mfile = { file_name = f;
file_key = key;
file_theories = [] ;
file_format = fmt;
file_theories = [];
file_verified = false;
file_expanded = exp;
file_parent = session;
......@@ -887,8 +889,9 @@ let load_file session old_provers f =
match f.Xml.name with
| "file" ->
let fn = string_attribute "name" f in
let fmt = load_option "format" f in
let exp = bool_attribute "expanded" f true in
let mf = raw_add_file ~keygen session fn exp in
let mf = raw_add_file ~keygen session fn fmt exp in
mf.file_theories <-
List.rev
(List.fold_left
......@@ -983,8 +986,8 @@ let raw_add_file ~x_keygen ~x_goal ~x_fold_theory ~x_fold_file =
let name,expl,task = x_goal goal in
raw_add_task ~keygen:x_keygen parent name expl task false in
g::acc in
let add_file session f_name file =
let rfile = raw_add_file ~keygen:x_keygen session f_name false in
let add_file session f_name fmt file =
let rfile = raw_add_file ~keygen:x_keygen session f_name fmt false in
let add_theory acc thname theory =
let rtheory = raw_add_theory ~keygen:x_keygen rfile thname false in
let parent = Parent_theory rtheory in
......@@ -1016,19 +1019,21 @@ module AddFile(X : sig
'a -> file -> 'a
end) = (struct
let add_file session fn f =
let add_file session fn ?format f =
let file = raw_add_file ~x_keygen:X.keygen ~x_goal:X.goal
~x_fold_theory:X.fold_theory ~x_fold_file:X.fold_file session fn f in
~x_fold_theory:X.fold_theory ~x_fold_file:X.fold_file session
fn format f in
check_file_verified notify file;
file
end : sig
val add_file : X.key session -> string -> X.file -> X.key file
val add_file :
X.key session -> string -> ?format:string -> X.file -> X.key file
end)
(* add a why file from a session *)
(** Read file and sort theories by location *)
let read_file env fn =
let theories = Env.read_file env fn in
let read_file env ?format fn =
let theories = Env.read_file env ?format fn in
let theories =
Util.Mstr.fold
(fun name th acc ->
......@@ -1049,19 +1054,19 @@ let goal_expl_task task =
let info = get_explanation gid task in
gid, info, task
let add_file ~keygen env filename =
let add_file ~keygen env ?format filename =
let x_keygen = keygen in
let x_goal = goal_expl_task in
let x_fold_theory f acc th =
let tasks = List.rev (Task.split_theory th None None) in
List.fold_left f acc tasks in
let x_fold_file f acc (env,fname) =
let theories = read_file env fname in
let theories = read_file env ?format fname in
List.fold_left (fun acc (_,thname,th) -> f acc thname th) acc theories in
dprintf debug "[Load] file '%s'@\n" filename;
let file = Filename.concat env.session.session_dir filename in
let add_file = raw_add_file ~x_keygen ~x_goal ~x_fold_theory ~x_fold_file in
let file = add_file env.session filename (env.env,file) in
let file = add_file env.session filename format (env.env,file) in
check_file_verified notify file;
file
......@@ -1706,7 +1711,8 @@ let update_session ~keygen ~allow_obsolete old_session env whyconf =
} in
let obsolete = PHstr.fold (fun _ old_file acc ->
dprintf debug "[Load] file '%s'@\n" old_file.file_name;
let new_file = add_file ~keygen new_env_session old_file.file_name in
let new_file = add_file ~keygen new_env_session
?format:old_file.file_format old_file.file_name in
merge_file ~keygen env ~allow_obsolete old_file new_file
|| acc)
old_session.session_files false in
......
......@@ -118,6 +118,7 @@ and 'a theory = private
and 'a file = private
{ mutable file_key : 'a;
file_name : string;
file_format : string option;
file_parent : 'a session;
mutable file_theories: 'a theory list;
(** Not mutated after the creation *)
......@@ -185,7 +186,7 @@ val load_prover : 'a env_session -> Whyconf.prover -> loaded_prover option
(** load a prover *)
val unload_provers : 'a env_session -> unit
(** forces unloading of all provers,
(** forces unloading of all provers,
to force reading again the configuration *)
(** {2 Update session} *)
......@@ -365,6 +366,7 @@ val remove_transformation : ?notify:'key notify -> 'key transf -> unit
val add_file :
keygen:'key keygen ->
'key env_session ->
?format:string ->
string ->
'key file
(** Add a real file by its filename. The filename must be relative to
......@@ -448,7 +450,8 @@ module AddFile(X : sig
'a -> file -> 'a
end) : sig
val add_file : X.key session -> string -> X.file -> X.key file
val add_file :
X.key session -> string -> ?format:string -> X.file -> X.key file
end
......
......@@ -319,8 +319,8 @@ let update_session ~allow_obsolete old_session env whyconf =
init_session env_session.session;
res
let add_file env_session f =
let mfile = add_file ~keygen:O.create env_session f in
let add_file env_session ?format f =
let mfile = add_file ~keygen:O.create env_session ?format f in
let any_file = (File mfile) in
init_any any_file;
O.notify any_file;
......
......@@ -109,7 +109,8 @@ module Make(O: OBSERVER) : sig
Same as {!Session.update_session} except initialization is done.
*)
val add_file : O.key env_session -> string -> O.key Session.file
val add_file :
O.key env_session -> ?format:string -> string -> O.key Session.file
(** [add_file es f] adds the file with filename [f] in the proof
session, the file name must be given relatively to the session
dir given to [open_session]
......
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