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

ITP: a nicer printing of sessions

parent b093a9ac
......@@ -115,6 +115,83 @@ let update_trans_node c id b =
propagate_proof c (get_trans_parent c.controller_session id)
(* printing *)
module PSession = struct
open Stdlib
type any =
| Session
| File of file
| Theory of theory
| Goal of proofNodeID
| Transf of transID
| ProofAttempt of proof_attempt
type 'a t = { tcont : controller;
tkind : any }
let decomp x =
let s = x.tcont.controller_session in
let n y acc = { x with tkind = y } :: acc in
match x.tkind with
| Session -> "", Hstr.fold (fun _ f -> n (File f)) (get_files s) []
| File f ->
f.file_name,
List.fold_right (fun th -> n (Theory th)) f.file_detached_theories
(List.fold_right (fun th -> n (Theory th)) f.file_theories [])
| Theory th ->
let id = theory_name th in
let name = id.Ident.id_string in
let name = if th_proved x.tcont id then name else name^"?" in
name,
List.fold_right (fun g -> n (Goal g)) (theory_goals th)
(List.fold_right (fun g -> n (Goal g)) (theory_detached_goals th) [])
| Goal id ->
let gid = get_proof_name s id in
let name = gid.Ident.id_string in
let name = if pn_proved x.tcont id then name else name^"?" in
let pas = get_proof_attempts s id in
let trs = get_transformations s id in
name,
List.fold_right (fun g -> n (Transf g)) trs
(List.fold_right (fun g -> n (ProofAttempt g)) pas [])
| ProofAttempt pa ->
Pp.sprintf_wnl "%a%s%s"
Whyconf.print_prover pa.prover
(match pa.Session_itp.proof_state with
| Some { Call_provers.pr_answer = Call_provers.Valid} -> ""
| _ -> "?")
(if pa.proof_obsolete then "O" else ""), []
| Transf id ->
let name = get_transf_name s id in
let name = if tn_proved x.tcont id then name else name^"?" in
let sts = get_sub_tasks s id in
let dsts = get_detached_sub_tasks s id in
name,
List.fold_right (fun g -> n (Goal g)) sts
(List.fold_right (fun g -> n (Goal g)) dsts [])
end
module P = Print_tree.PMake(PSession)
let print_session fmt c =
P.print fmt { PSession.tcont = c; PSession.tkind = PSession.Session }
(*********)
module type Scheduler = sig
val timeout: ms:int -> (unit -> bool) -> unit
val idle: prio:int -> (unit -> bool) -> unit
......
......@@ -87,6 +87,8 @@ val tn_proved: controller -> Session_itp.transID -> bool
val pn_proved: controller -> Session_itp.proofNodeID -> bool
val th_proved: controller -> Ident.ident -> bool
val print_session : Format.formatter -> controller -> unit
module Make(S : Scheduler) : sig
val schedule_proof_attempt :
......
......@@ -67,14 +67,14 @@ type file = {
module Proofnodeid = struct
type t = proofNodeID
let compare (x : proofNodeID) y = Pervasives.compare x y
let _compare (x : proofNodeID) y = Pervasives.compare x y
let equal (x : proofNodeID) y = x = y
let hash (x : proofNodeID) = x
end
module Transid = struct
type t = transID
let compare (x : transID) y = Pervasives.compare x y
let _compare (x : transID) y = Pervasives.compare x y
let equal (x : transID) y = x = y
let hash (x : transID) = x
end
......@@ -274,28 +274,6 @@ and print_trans_node s fmt id =
fprintf fmt "@[<hv 1> Trans %s;@ args %a;@ parent %s;@ [%a]@]" name (Pp.print_list Pp.colon pp_print_string) args parent
(Pp.print_list Pp.semi (print_proof_node s)) l
(*
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]@]@]"
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) 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
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_theory s fmt th : unit =
fprintf fmt "@[<hv 2> Theory %s;@ [%a]@]" th.theory_name.Ident.id_string
(Pp.print_list Pp.semi (fun fmt a -> print_proof_node s fmt a)) th.theory_goals
......@@ -307,10 +285,11 @@ let print_file s fmt (file, thl) =
let print_s s fmt =
fprintf fmt "@[%a@]" (Pp.print_list Pp.semi (print_file s))
let print_session fmt s =
let _print_session fmt s =
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 dir =
let shape_version = match shape_version with
| Some v -> v
......@@ -747,7 +726,7 @@ module AssoGoals = Termcode.Pairing(Goal)(Goal)
let found_obsolete = ref false
let found_missed_goals_in_theory = ref false
let save_detached_goals env old_s detached_goals_id s parent =
let save_detached_goals _env old_s detached_goals_id s parent =
let save_proof parent old_pa_n =
let old_pa = old_pa_n.proofa_attempt in
add_proof_attempt s old_pa.prover old_pa.limit
......
......@@ -44,13 +44,6 @@ val get_files : session -> file Stdlib.Hstr.t
val get_dir : session -> string
val get_shape_version : session -> int
(** {2 Proof trees}
Each goal
*)
type proof_attempt = {
prover : Whyconf.prover;
......@@ -64,48 +57,8 @@ type proof_attempt = {
type proof_parent = Trans of transID | Theory of theory
(* This is not needed
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_tree : session -> proofNodeID -> tree
(** [get_tree s id] returns the proof tree of the goal identified by
[id] *)
*)
val get_task : session -> proofNodeID -> Task.task
(* temp *)
(*
val get_node : session -> int -> proofNodeID
val get_trans : session -> int -> transID
*)
(* [print_proof_node s fmt t]: From definition of s, print on fmt the tree
rooted at element t *)
val print_proof_node : session -> Format.formatter -> proofNodeID -> unit
(* [print_theory s fmt t]: From definition of s, print on fmt the theory t *)
val print_theory : session -> Format.formatter -> theory -> unit
(* [print_trans s fmt tn]: From definition of s, print on fmt the tree originating
from transformation tn *)
val print_trans_node : session -> Format.formatter -> transID -> unit
val print_session : Format.formatter -> session -> unit
val get_transformations : session -> proofNodeID -> transID list
val get_proof_attempts : session -> proofNodeID -> proof_attempt list
val get_sub_tasks : session -> transID -> proofNodeID list
......
......@@ -446,6 +446,8 @@ let print_session fmt s =
let dump_session_raw fmt _args =
fprintf fmt "%a@." print_session cont.Controller_itp.controller_session
let display_session fmt _args =
fprintf fmt "%a@." Controller_itp.print_session cont
let print_position (s: session) (cursor: proof_zipper) fmt: unit =
match cursor.cursor with
......@@ -484,7 +486,7 @@ let test_schedule_proof_attempt fmt (args: string list) =
let id = nearest_goal () in
let callback status =
match status with
| Done _prover_result -> (dump_session_raw fmt []; test_print_goal fmt [];
| Done _prover_result -> (display_session fmt []; test_print_goal fmt [];
fprintf fmt "status: %a@."
Controller_itp.print_status status)
| Scheduled | Running -> ()
......@@ -545,7 +547,7 @@ let test_transform_and_display fmt args =
Controller_itp.print_trans_status status;
match status with
| TSdone _tid -> (ignore (move_to_goal_ret next_node);
dump_session_raw fmt []; test_print_goal fmt [])
display_session fmt []; test_print_goal fmt [])
| _ -> ()
in
C.schedule_transformation cont id tr tl ~callback
......@@ -652,7 +654,8 @@ let commands =
"list-strategies", "list available strategies", list_strategies;
"a", "<transname> <args>: apply the transformation <transname> with arguments <args>", apply_transform;
"t", "<transname> <args>: behave like 'a' but add function to display into the callback", test_transform_and_display;
"p", "print the session in raw form", dump_session_raw;
"pr", "print the session in raw form", dump_session_raw;
"p", "print the session", display_session;
"c", "<provername> [timelimit [memlimit]] run a prover on the current goal", test_schedule_proof_attempt;
"st", "<c> apply the strategy whose shortcut is 'c'", run_strategy;
"print", "<s> print the declaration where s was defined", test_print_id;
......
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