Skip to content

GitLab

why3
why3
Commit c6a742ba authored by Clément Fumex's avatar Clément Fumex
Browse files
Options

session controller entrance

parent 633ba1d2
Hide whitespace changes
Inline Side-by-side
Showing with 351 additions and 101 deletions
Makefile.in
View file @ c6a742ba
......@@ -190,8 +190,9 @@ LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
mlw_dexpr mlw_typing mlw_driver mlw_exec mlw_ocaml \
mlw_main mlw_interp
LIB_SESSION = compress xml termcode session session_itp session_tools strategy \
strategy_parser session_scheduler
LIB_SESSION = compress xml termcode session session_itp \
controller_itp session_tools strategy strategy_parser \
session_scheduler
LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/core/, $(LIB_CORE)) \
......
examples/use_api/itp.ml
View file @ c6a742ba
......@@ -15,8 +15,6 @@ Small text-based interactive prover using new Why3 session format, to be run in
******************)
(*
#load "unix.cma";;
#load "nums.cma";;
#load "dynlink.cma";;
......@@ -30,11 +28,8 @@ Small text-based interactive prover using new Why3 session format, to be run in
#directory "../../lib/why3";;
#load_rec "why3.cma";;
*)
open Format
(* opening the Why3 library *)
open Why3
......@@ -67,15 +62,40 @@ let provers =
provers
[]
open Session_itp;;
open Format;;
let (s,b) = Session_itp.load_session "../bitwalker/why3session.xml";;
let th = Session_itp.get_theories s;;
let (_,_,id) = match th with
(n, (thn, _::_::x::_)::_)::_ -> (n,thn,x);;
let (s,b) = Session_itp.load_session "../bitwalker/why3session.xml"
let t = Session_itp.get_tree s id;;
printf "%a@." (print_tree s) t;;
(* let n = Session_itp.get_node s 19;;
let s' = Session_itp.graft_transf s n "blabla" [] [];;
let t = Session_itp.get_tree s;;
let _ = Session_itp.remove_transformation s s';;
let _ = remove_transformation s (get_trans s 15);;
let t = Session_itp.get_tree s;;
let my_session = Session_itp.empty_session "test.xml";;
let s' = Session_itp.graft_transf s n "blabla" [] [];;
let t = Session_itp.get_tree s;; *)
(* excerpt from src/session/session.ml *)
let read_file env ?format fn =
let read_file env ?format fn =
let theories = Env.read_file Env.base_language env ?format fn in
let ltheories =
Stdlib.Mstr.fold
......@@ -88,31 +108,42 @@ let read_file env ?format fn =
| None -> (Loc.dummy_position,th_name,th)::acc)
theories []
in
List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
ltheories,theories
let th = List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
ltheories
in
List.map (fun (_,_,a) -> a) th;;
let my_session = empty_session ();;
(* adds a file in the new session *)
let file : unit (* Session_itp.file *) =
let fname = "../logic/hello_proof.why" in
try
let ordered_theories,theories = read_file env fname in
Session_itp.add_file my_session fname ordered_theories;
let theories = read_file env fname in
add_file_section my_session fname theories None;
with e ->
eprintf "@[Error while reading file@ '%s':@ %a@.@]" fname
Exn_printer.exn_printer e;
exit 1
exit 1;;
(* explore the theories in that file *)
let theories = get_theories my_session;;
let () = eprintf "%d theories found@." (List.length theories)
let (_,_,id) = match theories with
(n, (thn, x::_)::_)::_ -> (n,thn,x);;
let t = Session_itp.get_tree my_session id;;
print_session my_session;;
let l = graft_transf my_session id "toto" [] [];;
(* explore the theories in that file *)
let theories = file.Session.file_theories
let () = eprintf "%d theories found@." (List.length theories)
printf "%a@." (print_tree my_session) t;;
(* add proof attempts for each goals in the theories *)
(*
let add_proofs_attempts g =
List.iter
(fun (p,d) ->
......@@ -136,3 +167,4 @@ let () =
(* save the session on disk *)
let () = Session.save_session config env_session.Session.session
*)
src/session/controller_itp.ml 0 → 100644
View file @ c6a742ba
open Session_itp
(** State of a proof *)
type proof_attempt_status =
| Unedited (** editor not yet run for interactive proof *)
| JustEdited (** edited but not run yet *)
| Interrupted (** external proof has never completed *)
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *)
type transformation_status = TSscheduled of transID | TSdone of transID | TSfailed
let schedule_proof_attempt s id pr ~timelimit ~callback =
graft_proof_attempt s id pr ~timelimit;
callback Scheduled
let schedule_transformations s id name args ~callback =
let tid = graft_transf s id name args in
callback (TSscheduled tid)
let read_file env ?format fn =
let theories = Env.read_file Env.base_language env ?format fn in
let ltheories =
Stdlib.Mstr.fold
(fun name th acc ->
(* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *)
let th_name =
Ident.id_register (Ident.id_derive name th.Theory.th_name) in
match th.Theory.th_name.Ident.id_loc with
| Some l -> (l,th_name,th)::acc
| None -> (Loc.dummy_position,th_name,th)::acc)
theories []
in
let th = List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
ltheories
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
src/session/controller_itp.mli 0 → 100644
View file @ c6a742ba
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Session_itp
(** State of a proof *)
type proof_attempt_status =
| Unedited (** editor not yet run for interactive proof *)
| JustEdited (** edited but not run yet *)
| Interrupted (** external proof has never completed *)
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *)
val schedule_proof_attempt :
session ->
proofNodeID ->
Whyconf.prover ->
timelimit:int ->
callback:(proof_attempt_status -> unit) -> unit
(** [schedule_proof_attempt s id p tl cb] schedules a proof attempt for
a goal specified by [id] with the prover [p] with time limit [tl];
the function [cb] will be called each time the proof attempt status
changes. Typically at Scheduled, then Running, then Done. If there
is already a proof attempt with [p] it is updated. *)
type transformation_status = TSscheduled of transID | TSdone of transID | TSfailed
val schedule_transformations :
session ->
proofNodeID ->
string ->
trans_arg list ->
callback:(transformation_status -> unit) -> unit
(** [schedule_transformations s id cb] schedules a transformation for a
goal specified by [id]; the function [cb] will be called each time
the transformation status changes. Typically at Scheluded, then
Done tid.*)
val add_file_to_session : Env.env -> session -> 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 environnement :
- 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
*)
src/session/session_itp.ml
View file @ c6a742ba
......@@ -18,14 +18,14 @@ type theory = {
type proof_parent = Trans of transID | Theory of theory
type proof_attempt = {
prover : Whyconf.prover;
timelimit : int;
memlimit : int;
stepslimit : int;
proof_state : Call_provers.prover_result option;
prover : Whyconf.prover;
timelimit : int;
memlimit : int;
stepslimit : int;
mutable proof_state : Call_provers.prover_result option;
(* None means that the call was not done or never returned *)
proof_obsolete : bool;
proof_script : string option; (* non empty for external ITP *)
proof_obsolete : bool;
proof_script : string option; (* non empty for external ITP *)
}
type proof_attempt_node = {
......@@ -50,10 +50,10 @@ type trans_arg =
(* | ... *)
type transformation_node = {
transf_name : string;
transf_args : trans_arg list;
transf_subtasks : proofNodeID list;
transf_parent : proofNodeID;
transf_name : string;
transf_args : trans_arg list;
mutable transf_subtasks : proofNodeID list;
transf_parent : proofNodeID;
}
type file = {
......@@ -63,46 +63,45 @@ type file = {
}
type session = {
proofNode_table : proof_node Hint.t;
proofNode_table : proof_node Hint.t;
mutable next_proofNodeID : int;
trans_table : transformation_node Hint.t;
mutable next_transID : int;
session_files : file Hstr.t;
mutable session_shape_version : int;
session_prover_ids : int Hprover.t;
session_file_name : string;
}
type tree =
Tree of
(int * string * int * (int * string * int * tree list) list)
Tree of
(proofNodeID * string * (transID * string * tree list) list)
let rec get_goal s id : tree =
let rec get_tree s id : tree =
let t = Hint.find s.proofNode_table id in
let parent = match t.proofn_parent with
| Theory _ -> -1
| Trans n -> n
in
let trl = List.map (get_trans s) t.proofn_transformations in
Tree (id,t.proofn_name.Ident.id_string,parent,trl)
Tree (id, t.proofn_name.Ident.id_string, trl)
and get_trans s id =
let tr = Hint.find s.trans_table id in
(id,tr.transf_name,tr.transf_parent,List.map (get_goal s) tr.transf_subtasks)
(id, tr.transf_name, List.map (get_tree s) tr.transf_subtasks)
let get_tree s =
let get_theories s =
Hstr.fold
(fun fn f acc ->
let c =
List.map
(fun th ->
let goals = List.map (get_goal s) th.theory_goals in
(th.theory_name.Ident.id_string,goals))
(fun th -> (th.theory_name.Ident.id_string, th.theory_goals))
f.file_theories
in
(fn,c) :: acc)
s.session_files []
let get_node (s : session) (n : int) =
let _ = Hint.find s.proofNode_table n in n
let get_trans (s : session) (n : int) =
let _ = Hint.find s.trans_table n in n
let gen_transID (s : session) =
let id = s.next_transID in
s.next_transID <- id + 1;
......@@ -124,7 +123,46 @@ let get_transfNode (s : session) (id : transID) =
Hint.find s.trans_table id
with Not_found -> raise BadID
let empty_session ?shape_version (file : string) =
let get_transformations (s : session) (id : proofNodeID) =
(get_proofNode s id).proofn_transformations
let get_sub_tasks (s : session) (id : transID) =
(get_transfNode s id).transf_subtasks
open Format
open Ident
let rec print_tree s fmt (Tree (id, name, l)) =
let pn = get_proofNode s 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;@ [%a]@]" name parent
(Pp.print_list Pp.semi (print_trans s)) l
and print_trans s fmt (id, name, l) =
let tn = get_transfNode s id in
let parent = (get_proofNode s tn.transf_parent).proofn_name.id_string in
fprintf fmt "@[<hv 2> Trans %s;@ parent %s;@ [%a]@]" name parent
(Pp.print_list Pp.semi (print_tree s)) l
let print_session 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
in
let print_file s fmt (filename, thl) =
fprintf fmt "@[<hv 2> File %s;@ [%a]@]" filename
(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
printf "%a@." (print_s s) l;;
let empty_session ?shape_version () =
let shape_version = match shape_version with
| Some v -> v
| None -> Termcode.current_shape_version
......@@ -136,37 +174,27 @@ let empty_session ?shape_version (file : string) =
session_files = Hstr.create 3;
session_shape_version = shape_version;
session_prover_ids = Hprover.create 7;
session_file_name = file;
}
let add_file_section (s:session) (fn:string) ?format (ths:Theory.theory list): unit =
let theories = []
(*
List.rev_map
(fun (_,thname,th) ->
let tasks =
List.rev_map
(fun t -> t)
(Task.split_theory th None None)
in
{ theory_name = thname;
theory_checksum = None;
theory_goals = tasks }) ths
*)
in
let f = { file_name = fn;
file_format = format;
file_theories = List.rev theories }
in
Hstr.add s.session_files fn f
exception BadID
let graft_proof_attempt (s : session) (id : proofNodeID) (pa : proof_attempt) =
let pn = get_proofNode s id in
let node = { proofa_parent = id; proofa_attempt = pa } in
let mk_proof_attempt session pid pa =
let pn = get_proofNode session pid in
let node = { proofa_parent = pid; proofa_attempt = pa } in
Hprover.replace pn.proofn_attempts pa.prover node
let graft_proof_attempt (s : session) (id : proofNodeID) (pr : Whyconf.prover)
~timelimit =
let pa = {
prover = pr;
timelimit = timelimit;
memlimit = 0;
stepslimit = -1;
proof_state = None;
proof_obsolete = false;
proof_script = None; } in
mk_proof_attempt s id pa
let remove_proof_attempt (s : session) (id : proofNodeID)
(prover : Whyconf.prover) =
let pn = get_proofNode s id in
......@@ -192,8 +220,7 @@ let mk_proof_node_task (s : session) (t : Task.task)
let name,_,_ = Termcode.goal_expl_task ~root:false t in
mk_proof_node s name t parent node_id
let mk_transf_proof_node (s : session) (tid : int)
(t : Task.task) =
let mk_transf_proof_node (s : session) (tid : int) (t : Task.task) =
let id = gen_proofNodeID s in
mk_proof_node_task s t (Trans tid) id;
id
......@@ -208,18 +235,29 @@ let mk_transf_node (s : session) (id : proofNodeID) (node_id : transID)
Hint.add s.trans_table node_id tn;
pn.proofn_transformations <- node_id::pn.proofn_transformations
let set_transf_tasks (s : session) (id : transID) (tl : Task.task list) =
let tn = get_transfNode s id in
assert (tn.transf_subtasks = []);
let sub_tasks = List.map (mk_transf_proof_node s id) tl in
tn.transf_subtasks <- sub_tasks
let graft_transf (s : session) (id : proofNodeID) (name : string)
(args : trans_arg list) (tl : Task.task list) =
(args : trans_arg list) =
let tid = gen_transID s in
let sub_tasks = List.map (mk_transf_proof_node s tid) tl in
mk_transf_node s id tid name args sub_tasks
mk_transf_node s id tid name args [];
tid
let remove_transformation (s : session) (id : transID) =
let nt = get_transfNode s id in
Hint.remove s.trans_table id;
let pn = get_proofNode s nt.transf_parent in
let trans_up = List.filter (fun tid -> tid != id) pn.proofn_transformations in
pn.proofn_transformations <- trans_up;
pn.proofn_transformations <- trans_up
let update_proof_attempt s id pr st =
let n = get_proofNode s id in
let pa = Hprover.find n.proofn_attempts pr in
pa.proofa_attempt.proof_state <- st
(************************)
(* saving state on disk *)
......@@ -428,7 +466,7 @@ and load_proof_or_transf session old_provers pid a =
proof_obsolete = obsolete;
proof_script = edit;
} in
graft_proof_attempt session pid pa
mk_proof_attempt session pid pa
with Failure _ | Not_found ->
Warning.emit "[Error] prover id not listed in header '%s'@." prover;
raise (LoadError (a,"prover not listing in header"))
......@@ -436,13 +474,13 @@ and load_proof_or_transf session old_provers pid a =
| "transf" ->
let trname = string_attribute "name" a in
let tid = gen_transID session in
let subtasks = List.fold_left (fun goals th -> match th.Xml.name with
let subtasks_ids = List.rev (List.fold_left (fun goals th -> match th.Xml.name with
| "goal" -> (gen_proofNodeID session) :: goals
| _ -> goals) [] a.Xml.elements in
mk_transf_node session pid tid trname [] subtasks;
| _ -> goals) [] a.Xml.elements) in
mk_transf_node session pid tid trname [] subtasks_ids;
List.iter2
(load_goal session old_provers (Trans tid))
a.Xml.elements subtasks;
a.Xml.elements subtasks_ids;
| "metas" -> ()
| "label" -> ()
| s ->
......@@ -456,9 +494,9 @@ let load_theory session old_provers acc th =
let thname = load_ident th in
let csum = string_attribute_opt "sum" th in
let checksum = Opt.map Termcode.checksum_of_string csum in
let goals = List.fold_left (fun goals th -> match th.Xml.name with
let goals = List.rev (List.fold_left (fun goals th -> match th.Xml.name with
| "goal" -> (gen_proofNodeID session) :: goals
| _ -> goals) [] th.Xml.elements in
| _ -> goals) [] th.Xml.elements) in
let mth = { theory_name = thname;
theory_checksum = checksum;
theory_goals = goals; } in
......@@ -529,7 +567,7 @@ let build_session (s : session) xml =
s
let load_session (file : string) =
let session = empty_session file in
let session = empty_session () in
let use_shapes =
(* If the xml is present we read it, otherwise we consider it empty *)
if Sys.file_exists file then
......@@ -552,3 +590,44 @@ let load_session (file : string) =
else false
in
session, use_shapes
(* add a why file from a session *)
(** Read file and sort theories by location *)
let read_file env ?format fn =
let theories = Env.read_file Env.base_language env ?format fn in
let ltheories =
Mstr.fold
(fun name th acc ->
(* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *)
let th_name =
Ident.id_register (Ident.id_derive name th.Theory.th_name) in
match th.Theory.th_name.Ident.id_loc with
| Some l -> (l,th_name,th)::acc
| None -> (Loc.dummy_position,th_name,th)::acc)
theories []
in
List.sort
(fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
ltheories,theories
let add_file_section (s:session) (fn:string) (theories:Theory.theory list) format : unit =
let add_theory acc (th : Theory.theory) =
let add_goal parent goal id =
let name,_expl,task = Termcode.goal_expl_task ~root:true goal in
mk_proof_node s name task parent id;
in
let tasks = List.rev (Task.split_theory th None None) in
let goalsID = List.map (fun _ -> gen_proofNodeID s) tasks in
let theory = { theory_name = th.Theory.th_name;
theory_checksum = None;
theory_goals = goalsID; } in
let parent = Theory theory in
List.iter2 (add_goal parent) tasks goalsID;
theory::acc
in
let theories = List.fold_left add_theory [] theories in
let f = { file_name = fn;
file_format = format;
file_theories = List.rev theories }
in
Hstr.add s.session_files fn f
src/session/session_itp.mli
View file @ c6a742ba
......@@ -15,35 +15,62 @@ type trans_arg
*)
type tree =
Tree of
(int * string * int * (int * string * int * tree list) list)
Tree of
(proofNodeID * string * (transID * string * tree list) list)
val get_tree : session -> (string * (string * tree list) list) list
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 [thnmae,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
[id] *)
(* temp *)
val get_node : session -> int -> proofNodeID
val get_trans : session -> int -> transID
val print_tree : session -> Format.formatter -> tree -> unit
val print_session : session -> unit
(* val get_proof_attempts : session -> proofNodeID -> proof_attempt Whyconf.Hprover.t *)
val get_transformations : session -> proofNodeID -> transID list
val get_sub_tasks : session -> transID -> proofNodeID list