Commit 37243e60 authored by Clément Fumex's avatar Clément Fumex

+ add some command to move from goal to goal (gu/gd/gr/gl/ng/pg)

+ modify the command that print the sessino tree to specify where we are in the tree with "**"
+ add some more comprehensible error messages to wraper function for parsing
parent 63f6b075
......@@ -159,9 +159,18 @@ let get_transfNode (s : session) (id : transID) =
let get_transformations (s : session) (id : proofNodeID) =
(get_proofNode s id).proofn_transformations
let get_proof_attempts (s : session) (id : proofNodeID) =
Hprover.fold (fun _ a l -> a.proofa_attempt :: l) (get_proofNode s id).proofn_attempts []
let get_sub_tasks (s : session) (id : transID) =
(get_transfNode s id).transf_subtasks
let get_transformation_name (s : session) (id : transID) =
(get_transfNode s id).transf_name
let get_proof_name (s : session) (id : proofNodeID) =
(get_proofNode s id).proofn_name
let get_proof_parent (s : session) (id : proofNodeID) =
(get_proofNode s id).proofn_parent
......
......@@ -41,7 +41,14 @@ Each goal
type proof_attempt
type proof_attempt = {
prover : Whyconf.prover;
limit : Call_provers.resource_limit;
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 *)
}
type transID
......@@ -91,8 +98,12 @@ val print_session : Format.formatter -> session -> unit
(* val get_proof_attempts : session -> proofNodeID -> proof_attempt Whyconf.Hprover.t *)
val get_transformations : session -> proofNodeID -> transID list
val get_proof_attempts : session -> proofNodeID -> proof_attempt list
val get_sub_tasks : session -> transID -> proofNodeID list
val get_transformation_name : session -> transID -> string
val get_proof_name : session -> proofNodeID -> Ident.ident
val get_proof_parent : session -> proofNodeID -> proof_parent
val get_trans_parent : session -> transID -> proofNodeID
......
open Task
open Ty
open Term
......@@ -21,15 +19,17 @@ let rec wrap : type a. a trans_typ -> a -> trans_with_args =
begin
match l with
| s :: tail ->
let n = int_of_string s in
wrap t' (f n) tail task
| _ -> assert false
(try
let n = int_of_string s in
wrap t' (f n) tail task
with Failure _ -> raise (Failure "Parsing error: expecting an integer."))
| _ -> failwith "Missing argument: expecting an integer."
end
| Tstring t' ->
begin
match l with
| s :: tail -> wrap t' (f s) tail task
| _ -> assert false
| _ -> failwith "Missing argument: expecting a string."
end
| Tterm t' ->
begin
......@@ -37,7 +37,7 @@ let rec wrap : type a. a trans_typ -> a -> trans_with_args =
| _s :: tail ->
let te = Term.t_true in (* TODO: parsing + typing of s *)
wrap t' (f te) tail task
| _ -> assert false
| _ -> failwith "Missing argument: expecting a term."
end
| Tty t' ->
begin
......@@ -45,7 +45,7 @@ let rec wrap : type a. a trans_typ -> a -> trans_with_args =
| _s :: tail ->
let ty = Ty.ty_int in (* TODO: parsing + typing of s *)
wrap t' (f ty) tail task
| _ -> assert false
| _ -> failwith "Missing argument: expecting a type."
end
| Ttysymbol t' ->
begin
......@@ -53,5 +53,5 @@ let rec wrap : type a. a trans_typ -> a -> trans_with_args =
| _s :: tail ->
let tys = Ty.ts_int in (* TODO: parsing + typing of s *)
wrap t' (f tys) tail task
| _ -> assert false
| _ -> failwith "Missing argument: expecting a type symbol."
end
......@@ -209,14 +209,10 @@ let list_transforms _fmt _args =
(Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair l)
let dump_session_raw fmt _args =
fprintf fmt "%a@." Session_itp.print_session cont.Controller_itp.controller_session
open Controller_itp
open Session_itp
(* type proof_cursor = Th of theory | Pn of proofNodeID | Tn of transID *)
(* _____________________________________________________________________ *)
(* -------------------- zipper ----------------------------------------- *)
type proof_hole =
Th of theory list * theory * theory list |
Pn of proofNodeID list * proofNodeID * proofNodeID list |
......@@ -307,56 +303,118 @@ let zipper_left () =
true
| _ -> false
(* _____________________________________________________________________ *)
(* -------------------- moving around ---------------------------------- *)
let rec next_node () =
zipper_down () || zipper_right () || (zipper_up () && next_node_no_down ())
and next_node_no_down () =
zipper_right () || (zipper_up () && next_node_no_down ())
let prev_node = zipper_left () || zipper_up ()
let prev_node () = zipper_left () || zipper_up ()
(* This function always move from current position to the next goal even when on a goal *)
let rec nearest_goal_right () =
if next_node () then
(* This function try to reach a goal from the current position using
the move function *)
let rec move_to_goal move =
if move () then
match zipper.cursor with
| Pn (_,pn,_) -> Some pn
| _ -> nearest_goal_right ()
| _ -> move_to_goal move
else
None
let print_position (s: session) (cursor: proof_zipper) fmt: unit =
match cursor.cursor with
| Th (_, th, _) -> fprintf fmt "%a@." (print_theory s) th
| Pn (_, pn, _) -> fprintf fmt "%a@." (print_proof_node s) pn
| Tn (_, tn, _) -> fprintf fmt "%a@." (print_trans_node s) tn
let print_position_p s cursor fmt _ = print_position s cursor fmt
(* This function try to get the id of the nearest goal right. If it can't, it tries
to get you to the first goal of the session. If this is still not possible,
it returns an error. *)
let ngr_ret () =
let move_to_goal_ret move =
match
(match nearest_goal_right () with
| None -> Printf.eprintf "No more goal right. You might want to go back to the root@.";
zipper_init(); nearest_goal_right ()
(match move_to_goal move with
| None -> Printf.eprintf "No more goal right; back to root@.";
zipper_init(); move_to_goal next_node
| Some id -> Some id) with
| None -> failwith "After initialization there is no goal to go to@."
| Some id -> id
let move_to_goal_ret_p move _ _ = ignore (move_to_goal_ret move)
(* The cursor of the zipper is on a goal *)
let is_goal_cursor () =
match zipper.cursor with
| Pn (_, pn, _) -> Some pn
| _ -> None
let ngr_ret_p _ _ = ignore (ngr_ret ())
(* If on goal, do nothing else go to next_goal *)
let nearest_goal () =
match (is_goal_cursor ()) with
| None -> ngr_ret ()
match is_goal_cursor () with
| None -> move_to_goal_ret next_node
| Some id -> id
(* _____________________________________________________________________ *)
(* -------------------- printing --------------------------------------- *)
let print_proof_attempt fmt pa =
fprintf fmt "%a tl=%d %a"
Whyconf.print_prover pa.prover
pa.limit.Call_provers.limit_time
(Pp.print_option Call_provers.print_prover_result) pa.proof_state
let rec print_proof_node s (fmt: Format.formatter) p =
let parent = match get_proof_parent s p with
| Theory t -> (theory_name t).Ident.id_string
| Trans id -> get_transformation_name s id
in
let current_goal =
match is_goal_cursor () with
| Some pn -> pn = p
| _ -> false
in
if current_goal then
fprintf fmt "**";
fprintf fmt
"@[<hv 2> Goal %s;@ parent %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%a]@]@]"
(get_proof_name s p).Ident.id_string parent
(Pp.print_list Pp.semi print_proof_attempt)
(get_proof_attempts s p)
(Pp.print_list Pp.semi (print_trans_node s)) (get_transformations s p);
if current_goal then
fprintf fmt "**"
and print_trans_node s fmt id =
let name = get_transformation_name s id in
let l = get_sub_tasks s id in
let parent = (get_proof_name s (get_trans_parent s id)).Ident.id_string in
fprintf fmt "@[<hv 2> Trans %s;@ parent %s;@ [%a]@]" name parent
(Pp.print_list Pp.semi (print_proof_node s)) l
let print_theory s fmt th : unit =
fprintf fmt "@[<hv 2> Theory %s;@ [%a]@]" (theory_name th).Ident.id_string
(Pp.print_list Pp.semi (fun fmt a -> print_proof_node s fmt a)) (theory_goals th)
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
let print_s s fmt =
fprintf fmt "@[%a@]" (Pp.print_list Pp.semi (print_file s))
let print_session fmt s =
let l = Stdlib.Hstr.fold (fun _ f acc -> (f,f.file_theories) :: acc) (get_files s) [] in
fprintf fmt "%a@." (print_s s) l;;
let dump_session_raw fmt _args =
fprintf fmt "%a@." print_session cont.Controller_itp.controller_session
let print_position (s: session) (cursor: proof_zipper) fmt: unit =
match cursor.cursor with
| Th (_, th, _) -> fprintf fmt "%a@." (print_theory s) th
| Pn (_, pn, _) -> fprintf fmt "%a@." (print_proof_node s) pn
| Tn (_, tn, _) -> fprintf fmt "%a@." (print_trans_node s) tn
let print_position_p s cursor fmt _ = print_position s cursor fmt
(* _____________________________________________________________________ *)
(* -------------------- test with transformations ---------------------- *)
let test_schedule_proof_attempt fmt _args =
(* temporary : get the first goal *)
let id = nearest_goal () in
......@@ -661,7 +719,12 @@ let commands =
*)
"ttr", "takes 2 arguments. Name of the transformation (with one term argument) and a term" , test_transformation_one_arg_term;
"tra", "test duplicate transformation", test_transformation_with_args;
"ngr", "get to the next goal right", ngr_ret_p;
"ng", "get to the next goal", move_to_goal_ret_p next_node;
"pg", "get to the prev goal", move_to_goal_ret_p prev_node;
"gu", "get to the goal up", move_to_goal_ret_p zipper_up;
"gd", "get to the goal up", move_to_goal_ret_p zipper_down;
"gr", "get to the goal up", move_to_goal_ret_p zipper_right;
"gl", "get to the goal up", move_to_goal_ret_p zipper_left;
"pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper);
"tt", "test a transformation having a term as argument", test_transformation_with_string_parsed_later;
"zu", "navigation up, parent", (fun _ _ -> ignore (zipper_up ()));
......
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