Commit a3f4f927 authored by MARCHE Claude's avatar MARCHE Claude

semble ok mais fichier passe a Alt-ERgo vide !

parent 2f478925
......@@ -148,6 +148,7 @@ type transf_data =
type goal = {
mutable goal_id : db_ident;
mutable goal_origin : goal_origin;
mutable task : Why.Task.task;
mutable task_checksum: string;
mutable proved : bool;
......@@ -180,6 +181,12 @@ let transf_data t = t.transf_data
let transf_obsolete t = t.transf_obsolete
let subgoals t = t.subgoals
let rec string_from_origin o =
match o with
| Goal p -> p.Why.Decl.pr_name.Why.Ident.id_long
let goal_name g = string_from_origin g.goal_origin
module Loc = struct
......@@ -1169,19 +1176,45 @@ let root_goals () =
let string_from_result = function
| Why.Driver.Valid -> "Valid"
| Why.Driver.Invalid -> "Invalid"
| Why.Driver.Unknown s -> "Unknown " ^ s
| Why.Driver.Failure s -> "Failure " ^ s
| Why.Driver.Timeout -> "Timeout"
| Why.Driver.HighFailure -> "HighFailure"
exception AlreadyAttempted
let try_prover ~timelimit:_int ?memlimit:_int (_g : goal) (_d: prover_data) : unit =
assert false (* TODO *)
let try_prover ~timelimit ?memlimit (g : goal) (d: prover_data) : unit -> unit =
(* TODO: check if attempt already present *)
(* TODO: add attempt as "Running" *)
begin
match memlimit with None -> ()
| Some _ -> Format.eprintf "Db.try_prover warning: memlimit is ignored@."
end;
let callback = Why.Driver.call_prover_ext ~debug:true ~timeout:timelimit d.driver g.task
in
fun () ->
let r = callback () in
Format.eprintf "prover returned %s in %f seconds@."
(string_from_result r.Why.Call_provers.pr_answer)
r.Why.Call_provers.pr_time;
Format.eprintf "stdout: %s@." r.Why.Call_provers.pr_stdout;
Format.eprintf "stderr: %s@." r.Why.Call_provers.pr_stderr;
(* TODO : update attempt depending on r = Valid *)
()
let add_transformation (_g : goal) (_t : transf) : unit =
assert false (* TODO *)
let add_or_replace_task (_name : string) (t : Why.Task.task) : goal =
let add_or_replace_task (name : Why.Decl.prsymbol) (t : Why.Task.task) : goal =
(* TODO: replace if already exists *)
let g = {
goal_id = 0L;
goal_origin = Goal name;
task = t;
task_checksum = ""; (* TODO: md5sum (marshall ?) *)
proved = false;
......
......@@ -88,6 +88,9 @@ type goal_origin =
type goal
val goal_proved : goal -> bool
val goal_name : goal -> string
module Goal : sig
type t = goal
......@@ -153,19 +156,27 @@ val root_goals : unit -> goal list
exception AlreadyAttempted
val try_prover :
timelimit:int -> ?memlimit:int -> goal -> prover_data -> unit
(** attempts to prove goal with the given prover. This function adds
a new corresponding attempt for that goal, sets its current
status to Running, launches the prover in a separate process and
returns immediately.
Upon termination of the external process, the prover's answer is
retrieved and database is updated. The [proved] field of the
database is updated, and also these of any goal affected, according
to invariant above. Goal observers are notified of any change
of goal statuses.
timelimit:int -> ?memlimit:int -> goal -> prover_data -> (unit -> unit)
(** attempts to prove goal with the given prover. This function
prepares the goal for that prover, adds it as an new
external_proof attempt, setting its current status to Running,
and returns immmediately a function. When called, this function
actually launches the prover, and waits for its
termination. Upon termination of the external process, the
prover's answer is retrieved and database is updated. The
[proved] field of the database is updated, and also these of any
goal affected, according to invariant above.
Although goal preparation is not re-entrant, the function
returned initially is re-entrant, thus is suitable for being executed
in a thread, in contexts where background execution of provers is wanted.
@param timelimit CPU time limit given for that attempt, in
seconds, must be positive. (unlimited attempts are not allowed
with this function)
@param timelimit CPU time limit given for that attempt, must be positive
@param memlimit memory limit given for that attempt, must be
positive. If not given, does not limit memory consumption
@raise AlreadyAttempted if there already exists a non-obsolete
external proof attempt with the same driver and time limit, or
......@@ -202,7 +213,7 @@ val add_transformation: goal -> transf -> unit
(* {2 goal updates} *)
val add_or_replace_task: string -> Why.Task.task -> goal
val add_or_replace_task: Why.Decl.prsymbol -> Why.Task.task -> goal
(** updates the database with the new goal. If a goal with the same
origin already exists, it is checked whether the task to
prove is different or not. If it is the same, proof attempts are
......
......@@ -54,24 +54,32 @@ let config =
eprintf "Error while reading config file: %a@." Whyconf.report e;
exit 1
let provers = Util.Mstr.fold (fun name _ acc -> name :: acc) config.provers []
let () = printf "Load path is: %a@." (Pp.print_list Pp.comma Pp.string) config.loadpath
let () =
printf "Provers: ";
List.iter
(fun name ->
printf " %s, " name) provers;
printf "@."
let env = Why.Env.create_env (Why.Typing.retrieve config.loadpath)
let fname = "tests/test-claude"
let get_driver name =
let pi = Util.Mstr.find name config.provers in
Why.Driver.load_driver pi.Whyconf.driver env
let loadpath = config.loadpath
let provers_data =
printf "Provers: ";
let l =
Util.Mstr.fold
(fun id conf acc ->
let name = conf.Whyconf.name in
printf " %s, " name;
{ Db.prover_name = name;
Db.driver = get_driver id; } :: acc
) config.provers []
in
printf "@.";
l
let () = printf "Load path is: %a@." (Pp.print_list Pp.comma Pp.string) loadpath
let env = Why.Env.create_env (Why.Typing.retrieve loadpath)
let fname = "tests/test-claude"
let () = Db.init_base (fname ^ ".prm")
......@@ -114,7 +122,38 @@ let m : Why.Theory.theory Why.Theory.Mnm.t =
let do_task (tname : string) (_th : Why.Theory.theory) (task : Why.Task.task) : unit =
let add_task (tname : string) (task : Why.Task.task) acc =
match task with
| None -> assert false
| Some t ->
match t.Why.Task.task_decl with
| Why.Task.Use _ | Why.Task.Clone _ -> assert false
| Why.Task.Decl d ->
match d.Why.Decl.d_node with
| Why.Decl.Dtype _ | Why.Decl.Dlogic _ | Why.Decl.Dind _ -> assert false
| Why.Decl.Dprop (_kind,name,_f) ->
eprintf "doing task: tname=%s, name=%s@." tname
name.Why.Decl.pr_name.Why.Ident.id_long;
Db.add_or_replace_task name task :: acc
let do_theory tname th glist =
(*
let add acc (x,l) =
let pr = try Why.Theory.ns_find_pr th.Why.Theory.th_export l with Not_found ->
Format.eprintf "Goal '%s' not found in theory '%s'.@." x tname;
exit 1
in
Why.Decl.Spr.add pr acc
in
*)
(*
let prs = Some (Queue.fold add Why.Decl.Spr.empty glist) in
let prs = if Queue.is_empty glist then None else prs in
*)
let tasks = Why.Task.split_theory th None in
List.fold_right (add_task tname) tasks glist
(*
if !opt_prove then begin
let res = Driver.call_prover ~debug:!opt_debug ?timeout drv task in
......@@ -141,46 +180,75 @@ let do_task (tname : string) (_th : Why.Theory.theory) (task : Why.Task.task) :
fprintf fmt "@[%a@]@?" (Driver.print_task drv) task;
close_out cout
*)
match task with
| None -> assert false
| Some t ->
match t.Why.Task.task_decl with
| Why.Task.Use _ | Why.Task.Clone _ -> assert false
| Why.Task.Decl d ->
match d.Why.Decl.d_node with
| Why.Decl.Dtype _ | Why.Decl.Dlogic _ | Why.Decl.Dind _ -> assert false
| Why.Decl.Dprop (_kind,name,_f) ->
eprintf "doing task: tname=%s, name=%s@." tname
name.Why.Decl.pr_name.Why.Ident.id_long;
let _g = Db.add_or_replace_task tname task in
()
let do_theory tname th glist =
let add acc (x,l) =
let pr = try Why.Theory.ns_find_pr th.Why.Theory.th_export l with Not_found ->
Format.eprintf "Goal '%s' not found in theory '%s'.@." x tname;
exit 1
in
Why.Decl.Spr.add pr acc
in
let prs = Some (Queue.fold add Why.Decl.Spr.empty glist) in
let prs = if Queue.is_empty glist then None else prs in
let tasks = Why.Task.split_theory th prs in
List.iter (do_task tname th) tasks
let goal_menu g =
try
while true do
printf "Menu:@.";
printf " 0: exit@.";
let _,menu = List.fold_left
(fun (i,acc) p ->
let i = succ i in
printf "%2d: try %s@." i p.Db.prover_name;
(i,(i,p)::acc)) (0,[]) provers_data
in
printf "Select a choice:@.";
let s = read_line () in
(try
let i = int_of_string s in
if i=0 then raise Exit;
let p = List.assoc i menu in
let call = Db.try_prover ~timelimit:10 g p in
call ()
with Not_found | Failure _ ->
printf "unknown choice@.");
done
with Exit -> ()
let main_loop goals =
try
while true do
printf "Menu:@.";
printf " 0: exit@.";
let _,menu = List.fold_left
(fun (i,acc) g ->
let i = succ i in
printf "%2d: name='%s', proved=%b@." i (Db.goal_name g) (Db.goal_proved g);
(i,(i,g)::acc)) (0,[]) goals
in
printf "Select a choice:@.";
let s = read_line () in
(try
let i = int_of_string s in
if i=0 then raise Exit;
goal_menu (List.assoc i menu)
with Not_found | Failure _ ->
printf "unknown choice@.");
done
with Exit -> ()
let () =
eprintf "looking for goals@.";
(*
let glist = Queue.create () in
*)
let add_th t th mi =
eprintf "adding theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_long t;
Why.Ident.Mid.add th.Why.Theory.th_name (t,th) mi
in
let do_th _ (t,th) =
let do_th _ (t,th) glist =
eprintf "doing theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_long t;
do_theory t th glist
do_theory t th glist
in
Why.Ident.Mid.iter do_th (Why.Theory.Mnm.fold add_th m Why.Ident.Mid.empty);
eprintf "Done@."
let goals =
Why.Ident.Mid.fold do_th (Why.Theory.Mnm.fold add_th m Why.Ident.Mid.empty) []
in
eprintf "Production of goals done@.";
try
main_loop goals
with Exit -> eprintf "Exiting...@."
(*
......
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