Commit 27de37d5 authored by MARCHE Claude's avatar MARCHE Claude

in progress: support for detached nodes

The 'file' nodes in sessions now have a boolean field, to tell if
they are detached or not.

The functions Session_itp.merge_files, Controller_itp.reload_files and
Controller_itp.add_file now return the set of parsing or typing errors that
occurred, instead of throwing exceptions.
parent b9e41718
......@@ -71,13 +71,14 @@ let controller = Controller_itp.create_controller config env session
(* adds a file in the new session *)
let file : Session_itp.file =
let file_name = "examples/logic/hello_proof.why" in
try
Controller_itp.add_file controller file_name;
Session_itp.get_file session file_name
with e ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" file_name
Exn_printer.exn_printer e;
exit 1
let errors = Controller_itp.add_file controller file_name in
match errors with
| None ->
Session_itp.get_file session file_name
| Some e ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" file_name
Exn_printer.exn_printer e;
exit 1
(* explore the theories in that file *)
let theories = Session_itp.file_theories file
......
......@@ -235,9 +235,14 @@ let reload_files (c : controller) ~use_shapes =
raise e
let add_file c ?format fname =
let theories = Session_itp.read_file c.controller_env ?format fname in
let (_ : file) = add_file_section c.controller_session fname theories format in
()
try
let theories = Session_itp.read_file c.controller_env ?format fname in
let (_ : file) = add_file_section c.controller_session fname (Some theories) format in
None
with e ->
let (_ : file) = add_file_section c.controller_session fname None format in
Some e
module type Scheduler = sig
......
......@@ -107,14 +107,14 @@ val print_session : Format.formatter -> controller -> unit
val reload_files : controller -> use_shapes:bool -> bool * bool
val reload_files : controller -> use_shapes:bool -> exn list * bool * bool
(** reload the files of the given session:
- each file is parsed again and theories/goals extracted from it. If
some syntax error or parsing error occurs, then the corresponding
file is kept in the session, without any corresponding new theory,
that is as if it was an empty file (TODO: such errors should be
returned somehow by the function [reload_files])
that is as if it was an empty file (detached mode)
(those errors are returned as first component
- each new theory is associated to a theory of the former session if
the names match exactly. In case of no match:
......@@ -152,16 +152,18 @@ val reload_files : controller -> use_shapes:bool -> bool * bool
it, neither to its subgoals.
[reload_files] It returns a pair of boolean (o, d): o true means there are
[reload_files] It returns a triple (e, o, d): o true means there are
obsolete goals, d means there are missed objects (goals, transformations,
theories or files) that are now detached in the session returned.
[e] is the list of parsing of typing errors
*)
val add_file : controller -> ?format:Env.fformat -> string -> unit
val add_file : controller -> ?format:Env.fformat -> string -> exn option
(** [add_fil cont ?fmt fname] parses the source file
[fname] and add the resulting theories to the session of [cont] *)
[fname] and add the resulting theories to the session of [cont].
parsing or typing errors are signaled by a non-none result
*)
val remove_subtree: notification:notifier -> removed:notifier ->
controller -> any -> unit
......
......@@ -640,22 +640,30 @@ end
Loc.user_position f l b e
let capture_parse_or_type_errors f cont =
try let _ = f cont in None with
| Loc.Located (loc, e) ->
let rel_loc = relativize_location cont.controller_session loc in
let s = Format.asprintf "%a" Exn_printer.exn_printer e in
Some (loc, rel_loc, s)
| e when not (Debug.test_flag Debug.stack_trace) ->
let s = Format.asprintf "%a" Exn_printer.exn_printer e in
Some (Loc.dummy_position, Loc.dummy_position, s)
List.map
(function
| Loc.Located (loc, e) ->
let rel_loc = relativize_location cont.controller_session loc in
let s = Format.asprintf "%a" Exn_printer.exn_printer e in
(loc, rel_loc, s)
| e when not (Debug.test_flag Debug.stack_trace) ->
let s = Format.asprintf "%a" Exn_printer.exn_printer e in
(Loc.dummy_position, Loc.dummy_position, s)
| e -> raise e)
(f cont)
(* Reload_files that is used even if the controller is not correct. It can
be incorrect and end up in a correct state. *)
let reload_files cont ~use_shapes =
capture_parse_or_type_errors (reload_files ~use_shapes) cont
capture_parse_or_type_errors
(fun c -> let (e,_,_) = reload_files ~use_shapes c in e) cont
let add_file cont ?format fname =
capture_parse_or_type_errors (fun c -> add_file c ?format fname) cont
capture_parse_or_type_errors
(fun c ->
match add_file c ?format fname with
| None -> []
| Some e -> [e]) cont
(* ----------------------------------- ------------------------------------- *)
......@@ -932,14 +940,18 @@ end
if (Sys.file_exists f) then
begin
match add_file cont f with
| None ->
| [] ->
let file = get_file cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (file_name file);
P.notify (Message (Information "file added in session"))
| Some(loc,rel_loc,s) ->
| l ->
read_and_send fn;
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s)))
List.iter
(function
| (loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s))))
l
end
else
P.notify (Message (Open_File_Error ("File not found: " ^ f)))
......@@ -998,10 +1010,13 @@ end
focus on a specific node. *)
get_focused_label := None;
match x with
| None ->
| [] ->
P.notify (Message (Information "Session initialized succesfully"))
| Some(loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s)))
| l ->
List.iter
(function (loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s))))
l
(* ----------------- Schedule proof attempt -------------------- *)
......@@ -1210,12 +1225,15 @@ end
unfocus ();
clear_tables ();
match reload_files d.cont ~use_shapes:true with
| None ->
(* TODO: try to restore the previous focus : focused_node := old_focus; *)
| [] ->
(* TODO: try to restore the previous focus : focused_node := old_focus; *)
reset_and_send_the_whole_tree ();
P.notify (Message (Information "Session refresh successful"))
| Some(loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s)))
| l ->
List.iter
(function (loc,rel_loc,s) ->
P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s))))
l
let replay ~valid_only nid : unit =
let d = get_server_data () in
......
......@@ -85,7 +85,8 @@ type transformation_node = {
type file = {
file_name : string;
file_format : string option;
mutable file_theories : theory list;
file_is_detached : bool;
mutable file_theories : theory list;
}
let file_name f = f.file_name
......@@ -280,7 +281,7 @@ let get_detached_trans (_s: session) (_id: proofNodeID) =
let rec is_detached (s: session) (a: any) =
match a with
| AFile _file -> false
| AFile file -> file.file_is_detached
| ATh th -> th.theory_is_detached
| ATn tn ->
let pn_id = get_trans_parent s tn in
......@@ -1136,6 +1137,7 @@ let load_file session old_provers f =
(load_theory session fn old_provers) [] f.Xml.elements) in
let mf = { file_name = fn;
file_format = fmt;
file_is_detached = true;
file_theories = ft;
} in
Hstr.add session.session_files fn mf;
......@@ -1634,7 +1636,7 @@ let make_theory_section ?merge ~detached (s:session) parent_name (th:Theory.theo
(* add a why file to a session *)
let add_file_section (s:session) (fn:string)
(theories:Theory.theory list) format : file =
(theories:Theory.theory list option) format : file =
let fn = Sysutil.relativize_filename s.session_dir fn in
Debug.dprintf debug "[Session_itp.add_file_section] fn = %s@." fn;
if Hstr.mem s.session_files fn then
......@@ -1643,22 +1645,33 @@ let add_file_section (s:session) (fn:string)
assert false
end
else
let f = { file_name = fn;
file_format = format;
file_theories = [] }
in
Hstr.add s.session_files fn f;
let theories = List.map (make_theory_section ~detached:false s fn) theories in
f.file_theories <- theories;
f
(* add a why file to a session and try to merge its theories with the
match theories with
| None ->
let f = { file_name = fn;
file_format = format;
file_is_detached = true;
file_theories = [] }
in
Hstr.add s.session_files fn f;
f
| Some ths ->
let f = { file_name = fn;
file_format = format;
file_is_detached = false;
file_theories = [] }
in
Hstr.add s.session_files fn f;
let theories = List.map (make_theory_section ~detached:false s fn) ths in
f.file_theories <- theories;
f
(* add a why file to a session and try to merge its theories with the
provided ones with matching names *)
let merge_file_section ~use_shapes ~old_ses ~old_theories ~env
(s:session) (fn:string) (theories:Theory.theory list) format
: unit =
Debug.dprintf debug_merge "[Session_itp.merge_file_section] fn = %s@." fn;
let f = add_file_section s fn [] format in
let f = add_file_section s fn (Some []) format in
let fn = f.file_name in
let theories,detached =
let old_th_table = Hstr.create 7 in
......@@ -1717,21 +1730,25 @@ let merge_file ~use_shapes env (ses : session) (old_ses : session) file =
let format = file_format file in
let old_theories = file_theories file in
let file_name = Filename.concat (get_dir old_ses) (file_name file) in
let new_theories =
try
read_file env file_name ?format
with e -> (* TODO: filter only syntax error and typing errors *)
raise e
in
merge_file_section
ses ~use_shapes ~old_ses ~old_theories
~env file_name new_theories format
try
let new_theories = read_file env file_name ?format in
merge_file_section
ses ~use_shapes ~old_ses ~old_theories
~env file_name new_theories format;
None
with e -> (* TODO: capture only parsing and typing errors *)
Some e
let merge_files ~use_shapes env (ses:session) (old_ses : session) =
Stdlib.Hstr.iter
(fun _ f -> merge_file ~use_shapes env ses old_ses f)
(get_files old_ses);
!found_obsolete,!found_detached
let errors =
Stdlib.Hstr.fold
(fun _ f acc ->
match merge_file ~use_shapes env ses old_ses f with
| None -> acc
| Some e -> e :: acc)
(get_files old_ses) []
in
(errors,!found_obsolete,!found_detached)
(************************)
......
......@@ -153,7 +153,7 @@ val empty_session : ?from:session -> string -> session
argument *)
val add_file_section :
session -> string -> (Theory.theory list) ->
session -> string -> Theory.theory list option ->
Env.fformat option -> file
(** [add_file_section s fn ths] adds a new
'file' section in session [s], named [fn], containing fresh theory
......@@ -167,15 +167,16 @@ val read_file :
signaled with exceptions. *)
val merge_files :
use_shapes:bool -> Env.env -> session -> session -> bool * bool
use_shapes:bool -> Env.env -> session -> session -> exn list * bool * bool
(** [merge_files ~use_shapes env ses old_ses] merges the file sections
of session [s] with file sections of the same name in old session
[old_ses]. Recursively, for each theory whose name is identical to
old theories, it is attempted to associate the old goals,
proof_attempts and transformations to the goals of the new theory.
Returns a pair [(o,d)] such that [o] is true when obsolete proof
attempts where found and [d] is true id detached theories, goals
or transformations were found. *)
Returns a triple [(e,o,d)] such that [e] is the list of parsing or
typing errors found, [o] is true when obsolete proof attempts
where found and [d] is true if detached theories, goals or
transformations were found. *)
val graft_proof_attempt : ?file:string -> session -> proofNodeID ->
Whyconf.prover -> limit:Call_provers.resource_limit -> proofAttemptID
......
......@@ -355,14 +355,15 @@ let () =
let ses,use_shapes = S.load_session dir in
let cont = Controller_itp.create_controller config env ses in
(* update the session *)
let found_obs, found_detached =
try
Controller_itp.reload_files cont ~use_shapes;
with
| e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
exit 1
let errors, found_obs, found_detached =
Controller_itp.reload_files cont ~use_shapes;
in
begin match errors with
| [] -> ()
| l ->
List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
exit 1
end;
Debug.dprintf debug " done.@.";
if !opt_obsolete_only && not (found_detached || found_obs)
then
......
......@@ -88,14 +88,16 @@ let read_update_session ~allow_obsolete env config fname =
S.update_session ~ctxt session env config
*)
let cont = Controller_itp.create_controller config env session in
let found_obs, some_merge_miss =
try
Controller_itp.reload_files cont ~use_shapes
with
| e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
exit 1
let errors, found_obs, some_merge_miss =
Controller_itp.reload_files cont ~use_shapes
in
begin
match errors with
| [] -> ()
| l ->
List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
exit 1
end;
if (found_obs || some_merge_miss) && not allow_obsolete then raise Exit;
cont, found_obs, some_merge_miss
......
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