Commit b0e2ec55 authored by MARCHE Claude's avatar MARCHE Claude

why3shell: various new commands (print task, list provers and transforms)

parent f6e83a16
......@@ -413,7 +413,7 @@ let print_task args ?old:_ fmt task =
let () = register_printer "why3" print_task
~desc:"Printer@ for@ the@ logical@ format@ of@ Why3.@ Used@ for@ debugging."
let print_sequent args ?old:_ fmt =
let print_sequent _args ?old:_ fmt =
Trans.apply
(Printer.on_syntax_map
(fun sm ->
......@@ -421,11 +421,11 @@ let print_sequent args ?old:_ fmt =
Trans.store
(fun task ->
let task = Trans.apply (Trans.goal Introduction.intros) task in
print_th_prelude task fmt args.th_prelude;
(* print_th_prelude task fmt args.th_prelude; *)
let ut = Task.used_symbols (Task.used_theories task) in
let ld = Task.local_decls task ut in
List.iter (print_decl fmt) ld;
fprintf fmt "@\n@.")))
fprintf fmt "@[<v 0>%a@]"
(Pp.print_list Pp.newline print_decl) ld)))
let () = register_printer "why3_itp" print_sequent
......
......@@ -28,13 +28,14 @@ type transformation_status =
| TSscheduled of transID | TSdone of transID | TSfailed
type controller =
{ controller_session : Session_itp.session;
(* controller_env : Env.env; *)
{ mutable controller_session : Session_itp.session;
controller_env : Env.env;
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
}
let create_controller s = {
let create_controller env s = {
controller_session = s;
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
}
......@@ -212,11 +213,29 @@ let read_file env ?format fn =
in
List.map (fun (_,_,a) -> a) th
let add_file_to_session env s ?format fname =
let theories = read_file env ?format fname in
add_file_section s fname theories None
let add_file c ?format fname =
let theories = read_file c.controller_env ?format fname in
add_file_section c.controller_session fname theories None
let reload_session_files (_s : session) =
failwith "Controller_itp.reload_session_files not yet implemented"
(** reload files, associating old proof attempts and transformations
to the new goals. old theories and old goals for which we cannot
find a corresponding new theory resp. old goal are kept, with
tasks associated to them *)
let merge_file (_old_ses : session) (c : controller) _ file =
try
let theories =
read_file c.controller_env file.file_name ?format:file.file_format
in
add_file_section c.controller_session file.file_name theories None;
with _ -> (* TODO: filter only syntax error and typing errors *)
(* TODO: copy the old session with empty tasks *)
add_file_section c.controller_session file.file_name [] None
let reload_files (c : controller) =
let old_ses = c.controller_session in
c.controller_session <- empty_session ();
Stdlib.Hstr.iter (merge_file old_ses c) (get_files old_ses)
end
......@@ -50,12 +50,12 @@ module type Scheduler = sig
end
type controller = private
{ controller_session : Session_itp.session;
(* controller_env : Env.env; *)
{ mutable controller_session : Session_itp.session;
controller_env : Env.env;
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
}
val create_controller : Session_itp.session -> controller
val create_controller : Env.env -> Session_itp.session -> controller
module Make(S : Scheduler) : sig
......@@ -83,28 +83,53 @@ val schedule_transformations :
the transformation status changes. Typically at Scheluded, then
Done tid.*)
val add_file_to_session :
Env.env -> session -> ?format:Env.fformat -> string -> unit
(** [add_file_to_session env s ?fmt fname] parses the source file
[fname] and add the resulting theories to the session [s] *)
val reload_session_files : session -> unit
(** reload the given session with the given environment :
- the files are reloaded
- apply again the transformation
- if some goals appear try to find to which goal
in the given session it corresponds.
The last case meant that the session was obsolete.
It is authorized if [allow_obsolete] is [true],
otherwise the exception {!OutdatedSession} is raised.
If the session was obsolete is indicated by
the second result.
If the merge generated new unpaired goals is indicated by
the third result.
raises [OutdatedSession] if the session is obsolete and
[allow_obsolete] is false
*)
val add_file : controller -> ?format:Env.fformat -> string -> unit
(** [add_file_to_session cont ?fmt fname] parses the source file
[fname] and add the resulting theories to the session of [cont] *)
val reload_files : controller -> unit
(** 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])
- each new theory is associated to a theory of the former session if
the names match exactly. In case of no match:
. a new theory and its goals appear without any proof attempts in
it in the new session
. an unmatched old theory is kept in the new session together with
its former goals, proof attempts and transformations, but
without any tasks associated to goals and subgoals.
- within a new theory with a corresponding old theory, each goal is
in turn associated to a former goal if possible. the match is done
either on the goal name, or if no name match exactly, on the goal
shape.
. a new goal without match is added with an empty set of proof
attempts and transformations
. an old goal without match is kept with all its former proof
attempts and transformations, but no task is associated to it,
neither to its subgoals.
- on each new goal that has a matching old goal, old proof
attempts are attached, with the status obsolete if the task has
changed
- on each new goal that has a matching old goal, old
transformations are attached, and applied to the task, the
generated subgoals are in turn matched to the old sub-goals, in
the same manner as for goals in a theory
- TODO: the presence of obsolete goals should be returned somehow by
that function, as the presence of unmatch old theories or goals
*)
end
......@@ -15,6 +15,9 @@ type theory = {
mutable theory_checksum : Termcode.checksum option;
}
let theory_name t = t.theory_name
let theory_goals t = t. theory_goals
type proof_parent = Trans of transID | Theory of theory
type proof_attempt = {
......@@ -83,10 +86,13 @@ let session_iter_proof_attempt f =
(fun _ pan -> f pan.proofa_attempt)
pn.proofn_attempts)
type tree =
Tree of
(proofNodeID * string
* proof_attempt list * (transID * string * tree list) list)
type tree = {
tree_node_id : proofNodeID;
tree_goal_name : string;
tree_proof_attempts : proof_attempt list; (* proof attempts on this node *)
tree_transformations : (transID * string * tree list) list;
(* transformations on this node *)
}
let rec get_tree s id : tree =
let t = Hint.find s.proofNode_table id in
......@@ -94,22 +100,30 @@ let rec get_tree s id : tree =
Hprover.fold (fun _ pa acc -> pa.proofa_attempt::acc) t.proofn_attempts []
in
let trl = List.map (get_trans s) t.proofn_transformations in
Tree (id, t.proofn_name.Ident.id_string, pal, trl)
{ tree_node_id = id;
tree_goal_name = t.proofn_name.Ident.id_string;
tree_proof_attempts = pal;
tree_transformations = trl;
}
and get_trans s id =
let tr = Hint.find s.trans_table id in
(id, tr.transf_name, List.map (get_tree s) tr.transf_subtasks)
(*
let get_theories s =
Hstr.fold
(fun fn f acc ->
(fun _fn f acc ->
let c =
List.map
(fun th -> (th.theory_name.Ident.id_string, th.theory_goals))
f.file_theories
in
(fn,c) :: acc)
(f,c) :: acc)
s.session_files []
*)
let get_files s = s.session_files
let get_node (s : session) (n : int) =
let _ = Hint.find s.proofNode_table n in n
......@@ -174,18 +188,18 @@ let print_proof_attempt fmt pa =
pa.limit.Call_provers.limit_time
(Pp.print_option Call_provers.print_prover_result) pa.proof_state
let rec print_tree s fmt (Tree (id, name, pal ,trl)) =
let pn = get_proofNode s id in
let rec print_tree s fmt t =
let pn = get_proofNode s t.tree_node_id in
let parent = match pn.proofn_parent with
| Theory t -> t.theory_name.id_string
| Trans id -> (get_transfNode s id).transf_name
in
fprintf fmt
"@[<hv 2> Goal %s;@ parent %s;@ sum %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%a]@]@]"
name parent
t.tree_goal_name parent
(Opt.fold (fun _ a -> Termcode.string_of_checksum a) "None" pn.proofn_checksum)
(Pp.print_list Pp.semi print_proof_attempt) pal
(Pp.print_list Pp.semi (print_trans s)) trl
(Pp.print_list Pp.semi print_proof_attempt) t.tree_proof_attempts
(Pp.print_list Pp.semi (print_trans s)) t.tree_transformations
and print_trans s fmt (id, name, l) =
let tn = get_transfNode s id in
......@@ -194,18 +208,18 @@ and print_trans s fmt (id, name, l) =
(Pp.print_list Pp.semi (print_tree s)) l
let print_session fmt s =
let print_theory s fmt (thname, pnl) =
fprintf fmt "@[<hv 2> Theory %s;@ [%a]@]" thname
(Pp.print_list Pp.semi (fun fmt a -> print_tree s fmt (get_tree s a))) pnl
let print_theory s fmt th =
fprintf fmt "@[<hv 2> Theory %s;@ [%a]@]" th.theory_name.Ident.id_string
(Pp.print_list Pp.semi (fun fmt a -> print_tree s fmt (get_tree s a))) th.theory_goals
in
let print_file s fmt (filename, thl) =
fprintf fmt "@[<hv 2> File %s;@ [%a]@]" filename
let print_file s fmt (file, thl) =
fprintf fmt "@[<hv 2> File %s;@ [%a]@]" file.file_name
(Pp.print_list Pp.semi (print_theory s)) thl
in
let print_s s fmt =
fprintf fmt "@[%a@]" (Pp.print_list Pp.semi (print_file s))
in
let l = get_theories s in
let l = Hstr.fold (fun _ f acc -> (f,f.file_theories) :: acc) (get_files s) [] in
fprintf fmt "%a@." (print_s s) l;;
let empty_session ?shape_version () =
......
(** {1 New Proof sessions ("Refectoire")} *)
(** {2 upper level structure of sessions}
A [session] contains a collection of files, a [file] contains a
collection of theories, a [theory] contains a collection of goals. The
structure of goals remain abstract, each goal being identified by
unique identifiers of type [proofNodeId]
*)
type session
type transID
type proofNodeID
type theory
val theory_name : theory -> Ident.ident
val theory_goals : theory -> proofNodeID list
type file = private {
file_name : string;
file_format : string option;
file_theories : theory list;
}
val get_files : session -> file Stdlib.Hstr.t
(** {2 Proof trees}
Each goal
*)
type proof_attempt
type transID
type trans_arg =
| TAint of int
......@@ -10,13 +51,6 @@ type trans_arg =
| TAty of Ty.ty
| TAtysymbol of Ty.tysymbol
(* | ... *)
(* New Proof sessions ("Refectoire") *)
(* note: la fonction register des transformations doit permettre de
declarer les types des arguments
......@@ -25,21 +59,20 @@ type trans_arg =
*)
type tree =
Tree of
(proofNodeID * string
* proof_attempt list (* proof attempts on this node *)
* (transID * string * tree list) list) (* transformations on this node *)
type tree = {
tree_node_id : proofNodeID;
tree_goal_name : string;
tree_proof_attempts : proof_attempt list; (* proof attempts on this node *)
tree_transformations : (transID * string * tree list) list;
(* transformations on this node *)
}
(* a tree is a complete proof whenever at least one proof_attempf or
one transformation proves the goal, where a transformation proves a
goal when all subgoals have a complete proof. In other word, the
list of proof_attempt and transformation are "disjunctive" but the
list of tree below a transformation is "conjunctive" *)
val get_theories : session -> (string * (string * proofNodeID list) list) list
(** [get_theories s] returns a list of pairs [name,l] where [name] is a
file name and [l] is a list of pairs [thname,l'] where [thname] is
a theory name and [l'] is the list of goal ids *)
val get_tree : session -> proofNodeID -> tree
(** [get_tree s id] returns the proof tree of the goal identified by
......@@ -57,8 +90,6 @@ val print_session : Format.formatter -> session -> unit
val get_transformations : session -> proofNodeID -> transID list
val get_sub_tasks : session -> transID -> proofNodeID list
(* Note for big brother Andrei: grafting is the opposite of pruning *)
val empty_session : ?shape_version:int -> unit -> session
val add_file_section :
......@@ -105,31 +136,3 @@ val save_session : string -> session -> unit
val load_session : string -> session
(** [load_session f] load a session from a file [f]; all the tasks are
initialised to None *)
(*
couche au-dessus: "scheduler" cad modifications asynchrones de la
session
- gere une file de travaux de modifications a faire
- recupere les resultats de travaux , et les applique s'ils sont
encore valides
*)
(*
type theory =
{
goals : sequence of task
}
type file =
{
theories = sequence of theories
}
type session =
{
session_files : set of files
}
*)
......@@ -151,9 +151,11 @@ let option_list = [
let config, _, env =
Whyconf.Args.initialize option_list add_opt_file usage_msg
let main = Whyconf.get_main config
let driver_file s =
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))
else Filename.concat (Whyconf.datadir main) (Filename.concat "drivers" (s ^ ".drv"))
let opt_driver = ref (match List.rev_map driver_file !opt_driver with
| f::ef -> Some (f, ef)
......
......@@ -112,7 +112,7 @@ let spec = Arg.align [
]
let usage_str = Format.sprintf
"Usage: %s [options] <project directory>"
"Usage: %s [options] [ <file.xml> | <f1.why> <f2.mlw> ...]"
(Filename.basename Sys.argv.(0))
......@@ -137,11 +137,14 @@ let cont =
if Filename.check_suffix fname ".xml" then
Session_itp.load_session fname
else
let ses = Session_itp.empty_session () in
C.add_file_to_session env ses fname;
ses
begin
Queue.push fname files;
Session_itp.empty_session ()
end
in
Controller_itp.create_controller ses
let c = Controller_itp.create_controller env ses in
Queue.iter (fun fname -> C.add_file c fname) files;
c
(* loading the drivers *)
let () =
......@@ -209,13 +212,23 @@ let list_transforms _fmt _args =
let dump_session_raw fmt _args =
fprintf fmt "%a@." Session_itp.print_session cont.Controller_itp.controller_session
let first_goal () =
let files = Session_itp.get_files cont.Controller_itp.controller_session in
let file = ref None in
Stdlib.Hstr.iter (fun _ f -> file := Some f) files;
let file = Opt.get !file in
match file.Session_itp.file_theories with
| th::_ ->
begin
match Session_itp.theory_goals th with
| id :: _ -> id
| _ -> assert false
end
| _ -> assert false
let test_schedule_proof_attempt fmt _args =
(* temporary : get the first goal *)
let id =
match Session_itp.get_theories cont.Controller_itp.controller_session with
| (_n, (_thn, x::_)::_)::_ -> x
| _ -> assert false
in
let id = first_goal () in
let callback status =
fprintf fmt "status: %a@."
Controller_itp.print_status status
......@@ -230,17 +243,23 @@ let test_schedule_proof_attempt fmt _args =
cont id alt_ergo.Whyconf.prover
~limit ~callback
let task_driver = Driver.load_driver env "drivers/why3_itp.drv" []
let task_driver =
let d = Filename.concat (Whyconf.datadir main)
(Filename.concat "drivers" "why3_itp.drv")
in
Driver.load_driver env d []
let test_print_goal fmt _args =
(* temporary : get the first goal *)
let id =
match Session_itp.get_theories cont.Controller_itp.controller_session with
| (_n, (_thn, x::_)::_)::_ -> x
| _ -> assert false
in
let id = first_goal () in
let task = Session_itp.get_task cont.Controller_itp.controller_session id in
Driver.print_task ~cntexample:false task_driver fmt task
fprintf fmt "@[====================== Task =====================@\n%a@]@."
(Driver.print_task ~cntexample:false task_driver) task
let test_reload fmt _args =
fprintf fmt "Reloading... @?";
C.reload_files cont;
fprintf fmt "done @."
let commands =
[
......@@ -252,6 +271,7 @@ let commands =
"p", "print the session in raw form", dump_session_raw;
"t", "test schedule_proof_attempt with alt-ergo on the first goal", test_schedule_proof_attempt;
"g", "prints the first goal", test_print_goal;
"r", "reload the session (test only)", test_reload;
]
let commands_table = Stdlib.Hstr.create 17
......
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