Commit 1ccc8753 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'new_ide'

parents 201e0da2 ce5c39a0
......@@ -22,20 +22,24 @@
<transf name="remove" arg1="h1,h2">
<goal name="g3.0">
<transf name="case" arg1="x=0">
<goal name="g3.0.0">
<goal name="g3.0.0" expl="true case">
</goal>
<goal name="g3.0.1">
<goal name="g3.0.1" expl="false case">
</goal>
</transf>
<transf name="induction" arg1="x" arg2="from" arg3="42">
<goal name="g3.0.0">
<goal name="g3.0.0" expl="base case">
</goal>
<goal name="g3.0.1">
<goal name="g3.0.1" expl="recursive case">
</goal>
</transf>
</goal>
</transf>
<transf name="subst" arg1="x,y,z">
<transf name="subst" arg1="x,y">
<goal name="g3.0">
</goal>
</transf>
<transf name="subst" arg1="x,z">
<goal name="g3.0">
</goal>
</transf>
......
......@@ -168,6 +168,49 @@ let print_model_value_sanit fmt v =
let print_model_value = print_model_value_sanit
(******************************************)
(* Print values for humans *)
(******************************************)
let print_float_human fmt f =
match f with
| Plus_infinity ->
fprintf fmt "+∞"
| Minus_infinity ->
fprintf fmt "-∞"
| Plus_zero ->
fprintf fmt "+0"
| Minus_zero ->
fprintf fmt "-0"
| Not_a_number ->
fprintf fmt "NaN"
| Float_value (b, eb, sb) ->
fprintf fmt "float(%s,%s,%s)" b eb sb
let rec print_array_human fmt (arr: model_array) =
fprintf fmt "(";
List.iter (fun e ->
fprintf fmt "%s => %a," e.arr_index_key print_model_value_human e.arr_index_value)
arr.arr_indices;
fprintf fmt "others => %a)" print_model_value_human arr.arr_others
(* TODO there should be no record printed that way currently in Why3 *)
and print_record_human fmt r =
fprintf fmt "Record(";
List.iter (fun x -> fprintf fmt "%a" print_model_value_human x) r.fields;
fprintf fmt ")"
and print_model_value_human fmt (v: model_value) =
match v with
| Integer s -> fprintf fmt "%s" s
| Decimal (s1,s2) -> fprintf fmt "%s" (s1 ^ "." ^ s2)
| Float f -> print_float_human fmt f
| Boolean b -> fprintf fmt "%b" b
| Array arr -> print_array_human fmt arr
| Record r -> print_record_human fmt r
| Bitvector s -> fprintf fmt "%s" s
| Unparsed s -> fprintf fmt "%s" s
(*
***************************************************************
** Model elements
......@@ -265,7 +308,7 @@ type raw_model_parser = string -> model_element list
** Quering the model
***************************************************************
*)
let print_model_element me_name_trans fmt m_element =
let print_model_element print_model_value me_name_trans fmt m_element =
match m_element.me_name.men_kind with
| Error_message ->
fprintf fmt "%s" m_element.me_name.men_name
......@@ -274,10 +317,10 @@ let print_model_element me_name_trans fmt m_element =
fprintf fmt "%s = %a"
me_name print_model_value m_element.me_value
let print_model_elements ?(sep = "\n") me_name_trans fmt m_elements =
Pp.print_list (fun fmt () -> Pp.string fmt sep) (print_model_element me_name_trans) fmt m_elements
let print_model_elements ?(sep = "\n") print_model_value me_name_trans fmt m_elements =
Pp.print_list (fun fmt () -> Pp.string fmt sep) (print_model_element print_model_value me_name_trans) fmt m_elements
let print_model_file fmt me_name_trans filename model_file =
let print_model_file ~print_model_value fmt me_name_trans filename model_file =
(* Relativize does not work on nighly bench: using basename instead. It
hides the local paths. *)
let filename = Filename.basename filename in
......@@ -285,7 +328,7 @@ let print_model_file fmt me_name_trans filename model_file =
IntMap.iter
(fun line m_elements ->
fprintf fmt "@\nLine %d:@\n" line;
print_model_elements me_name_trans fmt m_elements)
print_model_elements print_model_value me_name_trans fmt m_elements)
model_file;
fprintf fmt "@\n"
......@@ -297,13 +340,24 @@ let why_name_trans me_name =
let print_model
?(me_name_trans = why_name_trans)
~print_model_value
fmt
model =
(* Simple and easy way to print file sorted alphabetically
FIXME: but StringMap.iter is supposed to iter in alphabetic order, so waste of time and memory here !
*)
let l = StringMap.bindings model.model_files in
List.iter (fun (k, e) -> print_model_file fmt me_name_trans k e) l
List.iter (fun (k, e) -> print_model_file ~print_model_value fmt me_name_trans k e) l
let print_model_human
?(me_name_trans = why_name_trans)
fmt
model = print_model ~me_name_trans ~print_model_value:print_model_value_human fmt model
let print_model ?(me_name_trans = why_name_trans)
fmt
model = print_model ~me_name_trans ~print_model_value fmt model
let model_to_string
?(me_name_trans = why_name_trans)
......@@ -335,7 +389,7 @@ let print_model_vc_term
let (filename, line_number, _, _) = Loc.get pos in
let model_file = get_model_file model.model_files filename in
let model_elements = get_elements model_file line_number in
print_model_elements ~sep me_name_trans fmt model_elements
print_model_elements ~sep print_model_value me_name_trans fmt model_elements
let model_vc_term_to_string
?(me_name_trans = why_name_trans)
......@@ -360,7 +414,7 @@ let interleave_line
line =
try
let model_elements = IntMap.find line_number model_file in
print_model_elements me_name_trans str_formatter model_elements ~sep:"; ";
print_model_elements print_model_value_human me_name_trans str_formatter model_elements ~sep:"; ";
let cntexmp_line =
(get_padding line) ^
start_comment ^
......
......@@ -149,6 +149,16 @@ val print_model :
@param model the counter-example model to print
*)
val print_model_human :
?me_name_trans:(model_element_name -> string) ->
Format.formatter ->
model ->
unit
(** Same as print_model but is intended to be human readable.
*)
val model_to_string :
?me_name_trans:(model_element_name -> string) ->
model ->
......
......@@ -219,6 +219,8 @@ let loadpath m =
Strings.split ':' d
with Not_found -> m.loadpath
let set_loadpath m l = { m with loadpath = l}
let timelimit m = m.timelimit
let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max
......
......@@ -72,6 +72,8 @@ val set_main : config -> main -> config
val libdir: main -> string
val datadir: main -> string
val loadpath: main -> string list
val set_loadpath : main -> string list -> main
val default_loadpath : string list
val timelimit: main -> int
val memlimit: main -> int
val running_provers_max: main -> int
......
......@@ -1503,7 +1503,14 @@ let on_selected_row r =
edited_view#source_buffer#set_text "(not yet available)";
edited_view#scroll_to_mark `INSERT;
counterexample_view#source_buffer#set_text "(not yet available)";
counterexample_view#scroll_to_mark `INSERT
counterexample_view#scroll_to_mark `INSERT;
let detached = get_node_detached id in
if detached then
task_view#source_buffer#set_text ""
else
let b = gconfig.intro_premises in
let c = gconfig.show_full_context in
send_request (Get_task(id,b,c,true))
| _ ->
let b = gconfig.intro_premises in
let c = gconfig.show_full_context in
......@@ -2127,7 +2134,6 @@ let check_uninstalled_prover =
uninstalled_prover_dialog gconfig p
end
let treat_notification n =
Protocol_why3ide.print_notify_debug n;
begin match n with
......
......@@ -659,6 +659,8 @@ let schedule_edition c id pr ~callback ~notification =
prover_tasks_edited;
run_timeout_handler ()
exception TransAlreadyExists of string * string
(*** { 2 transformations} *)
let schedule_transformation c id name args ~callback ~notification =
......@@ -690,6 +692,8 @@ let schedule_transformation c id name args ~callback ~notification =
end;
false
in
if Session_itp.check_if_already_exists c.controller_session id name args then
raise (TransAlreadyExists (name, List.fold_left (fun acc s -> s ^ " " ^ acc) "" args));
S.idle ~prio:0 apply_trans;
callback TSscheduled
......@@ -764,6 +768,7 @@ let schedule_tr_with_same_arguments
let args = get_transf_args s tr in
let name = get_transf_name s tr in
let callback = callback name args in
schedule_transformation c pn name args ~callback ~notification
let proof_is_complete pa =
......
......@@ -231,6 +231,7 @@ val prepare_edition :
of node [id] with prover [pr], using the file name given. The
editor is not launched. *)
exception TransAlreadyExists of string * string
val schedule_transformation :
controller ->
......
......@@ -18,6 +18,7 @@ type strategy = string
type node_ID = int
let root_node : node_ID = 0
let is_root n = n = root_node
type global_information =
{
......
......@@ -16,6 +16,8 @@ type strategy = string
type node_ID = int
val root_node : node_ID
val is_root : node_ID -> bool
(* --------------------------- types to be expanded if needed --------------------------------- *)
(** Global information known when server process has started and that can be
......
......@@ -111,6 +111,9 @@ let print_pr s id fmt t =
let print_pat s id fmt t =
let module P = (val (p s id)) in P.print_pat fmt t
let print_tdecl s id fmt t =
let module P = (val (p s id)) in P.print_tdecl fmt t
(* Exception reporting *)
(* TODO remove references to id.id_string in this function *)
......@@ -219,6 +222,10 @@ let get_exception_message ses id e =
Pp.sprintf "Transformation made no progress\n", Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans s ->
Pp.sprintf "Error in transformation function: %s \n" s, Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_decl (s, ld) ->
Pp.sprintf "Error in transformation %s during inclusion of following declarations:\n%a" s
(Pp.print_list (fun fmt () -> Format.fprintf fmt "\n") (print_tdecl ses id)) ld,
Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_term (s, t1, t2) ->
Pp.sprintf "Error in transformation %s during unification of following two terms:\n %a : %a \n %a : %a" s
(print_term ses id) t1 (print_opt_type ses id) t1.Term.t_ty
......@@ -904,7 +911,23 @@ end
let parid = pa.parent in
let name = Pp.string_of Whyconf.print_prover pa.prover in
let s, list_loc = task_of_id d parid do_intros show_full_context loc in
P.notify (Task (nid,s ^ "\n====================> Prover: " ^ name ^ "\n", list_loc))
let prover_text = s ^ "\n====================> Prover: " ^ name ^ "\n" in
(* Display the result of the prover *)
let prover_ce =
match pa.proof_state with
| Some res ->
let result =
Pp.string_of Call_provers.print_prover_answer
res.Call_provers.pr_answer
in
let ce_result =
Pp.string_of (Model_parser.print_model_human ?me_name_trans:None)
res.Call_provers.pr_model
in
result ^ "\n\n" ^ ce_result
| None -> "Result of the prover not available.\n"
in
P.notify (Task (nid, prover_text ^ prover_ce, list_loc))
| AFile f ->
P.notify (Task (nid, "File " ^ file_name f, []))
| ATn tid ->
......@@ -912,7 +935,8 @@ end
let args = get_transf_args d.cont.controller_session tid in
let parid = get_trans_parent d.cont.controller_session tid in
let s, list_loc = task_of_id d parid do_intros show_full_context loc in
P.notify (Task (nid, s ^ "\n====================> Transformation: " ^ String.concat " " (name :: args) ^ "\n", list_loc))
P.notify (Task (nid, s ^ "\n====================> Transformation: " ^
String.concat " " (name :: args) ^ "\n", list_loc))
(* -------------------- *)
......@@ -1106,16 +1130,10 @@ end
let apply_transform node_id t args =
let d = get_server_data () in
let check_if_already_exists s pid t args =
let sub_transfs = get_transformations s pid in
List.exists (fun tr_id -> get_transf_name s tr_id = t && get_transf_args s tr_id = args &&
not (is_detached s (ATn tr_id))) sub_transfs
in
let rec apply_transform nid t args =
match nid with
| APn id ->
if check_if_already_exists d.cont.controller_session id t args then
if Session_itp.check_if_already_exists d.cont.controller_session id t args then
P.notify (Message (Information "Transformation already applied"))
else
let callback = callback_update_tree_transform t args in
......@@ -1305,7 +1323,10 @@ end
| Get_task(nid,_,_,_) ->
Hint.mem model_any nid
| Command_req (nid, _) ->
Hint.mem model_any nid
if not (Itp_communication.is_root nid) then
Hint.mem model_any nid
else
true
(* ----------------- treat_request -------------------- *)
......@@ -1417,7 +1438,11 @@ end
end
| Exit_req -> exit 0
)
with e when not (Debug.test_flag Debug.stack_trace)->
with
| C.TransAlreadyExists (name,args) ->
P.notify (Message (Error
(Pp.sprintf "Transformation %s with arg [%s] already exists" name args)))
| e when not (Debug.test_flag Debug.stack_trace)->
P.notify (Message (Error (Pp.string_of
(fun fmt (r,e) -> Format.fprintf fmt
"There was an unrecoverable error during treatment of request:\n %a\nwith exception: %a"
......
......@@ -325,6 +325,11 @@ let set_obsolete s paid b =
let pa = get_proof_attempt_node s paid in
pa.proof_obsolete <- b
let check_if_already_exists s pid t args =
let sub_transfs = get_transformations s pid in
List.exists (fun tr_id ->
get_transf_name s tr_id = t && get_transf_args s tr_id = args &&
not (is_detached s (ATn tr_id))) sub_transfs
(* Iterations functions on the session tree *)
......
......@@ -119,6 +119,9 @@ val is_detached: session -> any -> bool
val get_encapsulating_theory: session -> any -> theory
val get_encapsulating_file: session -> any -> file
(* Check if a transformation already exists *)
val check_if_already_exists:
session -> proofNodeID -> string -> string list -> bool
(** {2 iterators on sessions} *)
......
......@@ -24,6 +24,7 @@ let usage_msg =
let conf_file = ref None
let autoprovers = ref false
let autoplugins = ref false
let resetloadpath = ref false
let opt_list_prover_ids = ref false
......@@ -49,8 +50,8 @@ let option_list = Arg.align [
" search for provers in $PATH";
"--detect-plugins", Arg.Set autoplugins,
" search for plugins in the default library directory";
"--detect", Arg.Unit (fun () -> autoprovers := true; autoplugins := true),
" search for both provers and plugins";
"--detect", Arg.Unit (fun () -> resetloadpath := true; autoprovers := true; autoplugins := true),
" search for both provers and plugins, and resets the default loadpath";
"--add-prover", Arg.Tuple
(let id = ref "" in
[Arg.Set_string id;
......@@ -162,7 +163,12 @@ let main () =
if not (Sys.file_exists conf_file) then begin
autoprovers := true;
autoplugins := true;
end;
end;
let config =
if !resetloadpath then
set_main config (set_loadpath (get_main config) default_loadpath)
else config
in
let config =
if !autoprovers
then Autodetection.run_auto_detection config
......
......@@ -372,44 +372,6 @@ let unfold unf hl =
end
| _ -> [d]) None
(* This function is used to find a specific ident in an equality:
(to_subst = term or term = to_subst) in order to subst and remove said
equality.
This function returns None if not found, Some (None, t1, t2) with t1 being
to_subst and t2 being term to substitute to if the equality found it a symbol
definition. If equality found is a a decl then it is returned:
Some (Some pr, t1, t2).
If the lsymbol to substitute appear in 2 equalities, only the first one is
used. *)
let find_eq (to_subst: Term.lsymbol list) =
fold (fun d (acc, used) ->
match d.d_node with
| Dprop (k, pr, t) when k != Pgoal ->
let acc, used = (match t.t_node with
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(* Allow to rewrite from the right *)
begin
match t1.t_node, t2.t_node with
| Tapp (ls, []), _ when List.exists (ls_equal ls) to_subst &&
not (List.exists (ls_equal ls) used) ->
Some (Some pr, t1, t2) :: acc, ls :: used
| _, Tapp (ls, []) when List.exists (ls_equal ls) to_subst &&
not (List.exists (ls_equal ls) used) ->
Some (Some pr, t2, t1) :: acc, ls :: used
| _ -> acc, used
end
| _ -> acc, used) in
acc, used
| Dlogic [(ls, ld)] when List.exists (ls_equal ls) to_subst &&
not (List.exists (ls_equal ls) used) ->
(* Function without arguments *)
let vl, e = open_ls_defn ld in
if vl = [] then
Some (None, t_app_infer ls [], e) :: acc, ls :: used
else
acc, used
| _ -> acc, used) ([],[])
(* This found any equality which at one side contains a single lsymbol and is
local. It gives same output as found_eq. *)
let find_eq2 is_local_decl =
......@@ -503,16 +465,6 @@ let subst_eq_list (found_eq_list, _) =
List.fold_left (fun acc_tr found_eq ->
Trans.compose (subst_eq found_eq) acc_tr) Trans.identity found_eq_list
let subst (to_subst: Term.lsymbol list) =
Trans.bind (find_eq to_subst) subst_eq_list
let subst (to_subst: Term.term list) =
(* TODO allow list of lsymbols in type of tactics *)
subst (List.map
(fun t -> match t.t_node with
| Tapp (ls, []) -> ls
| _ -> raise (Arg_trans "subst_eq")) to_subst)
let subst_all (is_local_decl: Decl.decl -> bool) =
Trans.bind (find_eq2 is_local_decl) subst_eq
......@@ -538,12 +490,10 @@ let rec repeat f task =
let repeat f = Trans.store (repeat f)
let () = wrap_and_register ~desc:"remove a literal using an equality on it"
"subst"
(Ttermlist Ttrans) subst
let subst_all = repeat subst_all
(* TODO implement subst_all as repeat subst ??? *)
let () =
wrap_and_register ~desc:"substitute all ident equalities and remove them"
"subst_all"
......@@ -570,3 +520,164 @@ let () = wrap_and_register
~desc:"apply <prop> [with] <list term> applies prop to the goal and \
uses the list of terms to instantiate the variables that are not found." "apply"
(Tprsymbol (Topt ("with", Ttermlist Ttrans_l))) (fun x y -> apply x y)
(*********)
(* Subst *)
(*********)
(* Creation of as structure that associates the replacement of terms as a
function of the
*)
type constant_subst_defining =
| Cls of lsymbol
| Cpr of prsymbol
module Csd = Stdlib.MakeMSHW (struct
type t = constant_subst_defining
let tag (c: t) = match c with
| Cls ls -> ls.ls_name.Ident.id_tag
| Cpr pr -> pr.pr_name.Ident.id_tag
end)
module Mcsd = Csd.M
(* We find the hypotheses that have a substitution equality for elements of the
to_subst list. We check that we never take more than one equality per
lsymbol to substitute.
*)
let find_eq_aux (to_subst: Term.lsymbol list) =
fold (fun d (acc, used) ->
match d.d_node with
| Dprop (k, pr, t) when k != Pgoal ->
let acc, used = (match t.t_node with
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(* Allow to rewrite from the right *)
begin
match t1.t_node, t2.t_node with
| Tapp (ls, []), _ when List.exists (ls_equal ls) to_subst &&
(* Check ls is not already taken *)
not (List.exists (ls_equal ls) used) ->
Mcsd.add (Cpr pr) (t1, t2) acc, ls :: used
| _, Tapp (ls, []) when List.exists (ls_equal ls) to_subst &&
(* Check ls is not already taken *)
not (List.exists (ls_equal ls) used) ->
Mcsd.add (Cpr pr) (t2, t1) acc, ls :: used
| _ -> acc, used
end
| _ -> acc, used) in
acc, used
| Dlogic [(ls, ld)] when List.exists (ls_equal ls) to_subst &&
(* Check ls is not already taken *)
not (List.exists (ls_equal ls) used) ->
(* Function without arguments *)
let vl, e = open_ls_defn ld in
if vl = [] then
Mcsd.add (Cls ls) (t_app_infer ls [], e) acc, ls :: used
else
acc, used
| _ -> acc, used) (Mcsd.empty,[])
(* Wrap-around function to parse lsymbol instead of terms *)
let find_eq to_subst =
let to_subst = (List.map
(fun t -> match t.t_node with
| Tapp (ls, []) -> ls
| _ -> raise (Arg_trans "subst_eq")) to_subst)
in
find_eq_aux to_subst
(* This produce an ordered list of tdecl which is the original task minus the
hypotheses/constants that were identified for substitution.
This shall be done on tdecl.
*)
let remove_hyp_and_constants (replacing_hyps, used_ls) =
(* The task_fold on tdecl is necessary as we *need* all the tdecl (in
particular to identify local decls).
*)
Task.task_fold (fun (subst, list_tdecl) td ->
match td.td_node with
| Decl d ->
begin
match d.d_node with
| Dprop (kind, pr, _t) when kind != Pgoal &&
Mcsd.mem (Cpr pr) replacing_hyps ->
let from_t, to_t = Mcsd.find (Cpr pr) replacing_hyps in
(* TODO find a way to be more efficient than this *)
let to_t = Generic_arg_trans_utils.replace_subst subst to_t in
Mterm.add from_t to_t subst, list_tdecl
| Dlogic [ls, _] when Mcsd.mem (Cls ls) replacing_hyps ->
let from_t, to_t = Mcsd.find (Cls ls) replacing_hyps in
(* TODO find a way to be more efficient than this *)
let to_t = Generic_arg_trans_utils.replace_subst subst to_t in
Mterm.add from_t to_t subst, list_tdecl
| Dparam ls when List.exists (ls_equal ls) used_ls ->
subst, list_tdecl
| _ ->
subst, (replace_tdecl subst td :: list_tdecl)
end
| _ -> (subst, td :: list_tdecl)
) (Mterm.empty, [])
let remove_hyp_and_constants (replacing_hyps, used_ls) =
Trans.store (remove_hyp_and_constants (replacing_hyps, used_ls))
let is_goal td =
match td.td_node with
| Decl d ->
begin
match d.d_node with
| Dprop (Pgoal, _, _) -> true
| _ -> false
end
| _ -> false
(* Use the list of tdecl that should be able to be readded into a task if there
was sufficiently few things that were removed to the task.
To do this, we use Task.add_tdecl (because we think its the safest).
Note that we also try to keep the order of the declarations (because
usability). So, each time we add a new declaration, we try to add all the
transformations that failed (supposedly because they use a variable declared
after it).
*)
let readd_decls (list_decls, subst: tdecl list * _) =
List.fold_left (fun (task_uc, list_to_add) (d: tdecl) ->
let d = replace_tdecl subst d in
let task_uc, list_to_add =
List.fold_left (fun (task_uc, list_to_add) (d: tdecl) ->
try
let new_task_uc = Task.add_tdecl task_uc d in
new_task_uc, list_to_add
with
(* TODO find all possible exceptions here *)
_ -> task_uc, d :: list_to_add)
(task_uc, []) list_to_add
in
(* We always need to add the goal last *)
if is_goal d then
if list_to_add != [] then
raise (Arg_trans_decl ("subst_eq", list_to_add))
else
try
(Task.add_tdecl task_uc d, [])
with
(* TODO find all possible exceptions here *)
_ -> raise (Arg_trans_decl ("subst_eq", [d]))
else
try
(Task.add_tdecl task_uc d, List.rev list_to_add)
with
_ -> (task_uc, List.rev (d :: list_to_add)))
(None, []) list_decls
let readd_decls (subst, list_decls) =
let (task, _l) = readd_decls (list_decls, subst) in
Trans.return task
let find args = Trans.bind (find_eq args) remove_hyp_and_constants
let subst args = Trans.bind (find args) readd_decls
let () = wrap_and_register ~desc:"remove a literal using an equality on it"
"subst"
(Ttermlist Ttrans) subst
......@@ -11,8 +11,10 @@
open Term
open Decl
open Theory
exception Arg_trans of string