From ee021c6790b3e606dfdc20e2291bb5cd3b107b46 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 3 Dec 2019 09:39:49 +0100
Subject: [PATCH] [wp/gui] fix tree node feedback
---
src/plugins/wp/GuiProof.ml | 43 ++++++++++++----------------------
src/plugins/wp/ProofEngine.ml | 24 +++----------------
src/plugins/wp/ProofEngine.mli | 7 ++----
3 files changed, 20 insertions(+), 54 deletions(-)
diff --git a/src/plugins/wp/GuiProof.ml b/src/plugins/wp/GuiProof.ml
index d352290613b..1b984174b7b 100644
--- a/src/plugins/wp/GuiProof.ml
+++ b/src/plugins/wp/GuiProof.ml
@@ -26,12 +26,10 @@ let rec rootchain node ns =
| Some p -> rootchain p (p::ns)
let pp_status fmt node =
- match ProofEngine.state node with
- | `Opened -> Format.fprintf fmt "@{<red>opened@}"
- | `Proved | `Pending 0 -> Format.fprintf fmt "@{<green>proved@}"
- | `Pending 1 -> Format.fprintf fmt "@{<orange>pending@}"
- | `Pending n -> Format.fprintf fmt "@{<orange>pending %d@}" n
- | `Script n -> Format.fprintf fmt "script with %d leaves" n
+ match ProofEngine.pending node with
+ | 0 -> Format.fprintf fmt "@{<green>proved@}"
+ | 1 -> Format.fprintf fmt "@{<orange>pending@}"
+ | n -> Format.fprintf fmt "@{<orange>pending %d@}" n
class printer (text : Wtext.text) =
let nodes : ProofEngine.position Wtext.marker = text#marker in
@@ -66,36 +64,25 @@ class printer (text : Wtext.text) =
VCS.pp_prover prv VCS.pp_result res
) (Wpo.get_results wpo)
- method private pp_state fmt node =
- match ProofEngine.state node with
- | `Proved -> Format.pp_print_string fmt "proved"
- | `Opened -> Format.pp_print_string fmt "opened"
- | `Pending 0 -> Format.pp_print_string fmt "terminated"
- | `Pending 1 -> Format.pp_print_string fmt "pending"
- | `Pending n -> Format.fprintf fmt "pending(%d)" n
- | `Script 0 -> Format.pp_print_string fmt "script"
- | `Script n -> Format.fprintf fmt "script(%d)" n
-
method private tactic header node =
+ text#printf "@{<bf>Tactical@}@} %s:" header ;
match ProofEngine.children node with
| [] ->
- text#printf "@{<bf>Tactical@}@} %s: @{<green>proved@} (Qed).@\n" header
+ text#printf "@{<green>proved@} (Qed).@\n"
| [_,child] ->
- text#printf "@{<bf>Tactical@} %a: %a.@\n" self#pp_node child self#pp_state child
+ text#printf "%a (%a).@\n" pp_status child self#pp_node child
| children ->
- begin match ProofEngine.pending node with
- | 0 -> text#printf "@{<green>@{<bf>Tactical@}@} %s: @{<green>proved@}.@\n" header
- | 1 -> text#printf "@{<bf>Tactical@} %s: @{<orange>pending@}.@\n" header ;
- | n -> text#printf "@{<bf>Tactical@} %s: @{<orange>pending(%d)@}.@\n" header n ;
- end ;
- List.iter
- (fun (part,child) -> text#printf "@{<bf>SubGoal@} %s : %a.@\n"
- part self#pp_state child)
- children
+ begin
+ text#printf " (%a)@\n@{<bf>Sub Goals:@}" pp_status node ;
+ List.iter
+ (fun (part,child) -> text#printf "@\n - %s : %a" part pp_status child)
+ children ;
+ text#printf "@." ;
+ end
method private alternative g a =
let open ProofScript in match a with
- | Tactic(0,{ header },_) -> text#printf "@{<bf>Script@} %s: terminating.@\n" header
+ | Tactic(0,{ header },_) -> text#printf "@{<bf>Script@} %s: finished.@\n" header
| Tactic(n,{ header },_) -> text#printf "@{<bf>Script@} %s: pending %d.@\n" header n
| Error(msg,_) -> text#printf "@{<bf>Script@} Error (%S).@\n" msg
| Prover(p,r) ->
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index f86ec63be01..d049b1ee2eb 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -206,33 +206,15 @@ let children n =
(* -------------------------------------------------------------------------- *)
type status = [ `Main | `Proved | `Pending of int ]
-type state = [ `Opened | `Proved | `Pending of int | `Script of int ]
let status t : status =
match t.root with
| None ->
if Wpo.is_proved t.main then `Proved else `Main
| Some root ->
- `Pending (pending root)
-
-
-let opened n = not (Wpo.is_proved n.goal)
-
-let state n =
- if Wpo.is_proved n.goal then `Proved else
- match n.script with
- | Opened -> `Opened
- | Script s ->
- begin
- match List.partition ProofScript.is_prover s with
- | [] , s -> `Script (ProofScript.status s)
- | p , [] -> `Pending (ProofScript.status p)
- | provers , scripts ->
- let np = ProofScript.status provers in
- let ns = ProofScript.status scripts in
- `Script( min ns np )
- end
- | Tactic _ -> `Pending (pending n)
+ match root.script with
+ | Opened | Script _ -> `Main
+ | Tactic _ -> `Pending (pending root)
(* -------------------------------------------------------------------------- *)
(* --- Navigation --- *)
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index b36f120911b..2150cbae4c1 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -36,7 +36,6 @@ val validate : ?incomplete:bool -> tree -> unit
(** Leaves are numbered from 0 to n-1 *)
type status = [ `Main | `Proved | `Pending of int ]
-type state = [ `Opened | `Proved | `Pending of int | `Script of int ]
type current = [ `Main | `Internal of node | `Leaf of int * node ]
type position = [ `Main | `Node of node | `Leaf of int ]
@@ -53,13 +52,11 @@ val head : tree -> Wpo.t
val goal : node -> Wpo.t
val tree_context : tree -> WpContext.t
val node_context : node -> WpContext.t
-val opened : node -> bool (** not proved *)
-val proved : node -> bool (** not opened *)
val title : node -> string
-val state : node -> state
+val proved : node -> bool
+val pending : node -> int (** 0 means proved *)
val parent : node -> node option
-val pending : node -> int
val children : node -> (string * node) list
val tactical : node -> ProofScript.jtactic option
val get_strategies : node -> int * Strategy.t array (* current index *)
--
GitLab