From ec105eb9ce93b2eb345640f698962088676fd62e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 9 Apr 2024 22:05:21 +0200
Subject: [PATCH] [ivette/wp] filtering sub-goals navigation
---
.../src/frama-c/plugins/wp/api/tip/index.ts | 19 ++++---
ivette/src/frama-c/plugins/wp/tip.tsx | 21 ++++++--
src/plugins/wp/wpTipApi.ml | 49 ++++++++++++++-----
3 files changed, 64 insertions(+), 25 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/api/tip/index.ts b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
index b5b88e457df..c33edca169b 100644
--- a/ivette/src/frama-c/plugins/wp/api/tip/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
@@ -153,14 +153,19 @@ export const getResult: Server.GetRequest<
>= getResult_internal;
const getProofStatus_internal: Server.GetRequest<
- goal,
- { index: number, pending: number, current: node, parents: node[],
- tactic?: tactic, children: node[] }
+ { main: goal, unproved?: boolean, subtree?: boolean },
+ { size: number, index: number, pending: number, current: node,
+ parents: node[], tactic?: tactic, children: node[] }
> = {
kind: Server.RqKind.GET,
name: 'plugins.wp.tip.getProofStatus',
- input: jGoal,
+ input: Json.jObject({
+ main: jGoal,
+ unproved: Json.jOption(Json.jBoolean),
+ subtree: Json.jOption(Json.jBoolean),
+ }),
output: Json.jObject({
+ size: Json.jNumber,
index: Json.jNumber,
pending: Json.jNumber,
current: jNode,
@@ -172,9 +177,9 @@ const getProofStatus_internal: Server.GetRequest<
};
/** Current Proof Status of a Goal */
export const getProofStatus: Server.GetRequest<
- goal,
- { index: number, pending: number, current: node, parents: node[],
- tactic?: tactic, children: node[] }
+ { main: goal, unproved?: boolean, subtree?: boolean },
+ { size: number, index: number, pending: number, current: node,
+ parents: node[], tactic?: tactic, children: node[] }
>= getProofStatus_internal;
const goForward_internal: Server.SetRequest<goal,null> = {
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index 56143ae93d7..e128cc03f03 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -237,14 +237,19 @@ export interface TIPProps {
export function TIPView(props: TIPProps): JSX.Element {
const { display, goal, onClose } = props;
+ // --- navbar settings
+ const [unproved, flipU] = Dome.useFlipSettings('frama-c.wp.goals.unproved');
+ const [subtree, flipT] = Dome.useFlipSettings('frama-c.wp.goals.subtree');
// --- current goal
const infos =
States.useSyncArrayElt(WP.goals, goal) ?? WP.goalsDataDefault;
// --- proof status
const {
- current, index = -1, pending = 0,
+ current, index = -1, pending = 0, size = 0,
tactic: nodeTactic, parents = [], children = [],
- } = States.useRequest(TIP.getProofStatus, goal, { pending: null }) ?? {};
+ } = States.useRequest(TIP.getProofStatus, goal ? {
+ main: goal, unproved, subtree,
+ } : undefined, { pending: null }) ?? {};
// --- script status
const { saved = false, proof = false, script } =
States.useRequest(TIP.getScriptStatus, goal, { pending: null }) ?? {};
@@ -336,14 +341,20 @@ export function TIPView(props: TIPProps): JSX.Element {
return (
<Vfill display={display}>
<ToolBar>
- <Cell
- icon='HOME'
- label={infos.wpo} title='Goal identifier' />
+ <Cell icon='HOME' label={infos.wpo} title='Goal identifier' />
<Item
icon='CODE'
display={0 <= index && index < pending && 1 < pending}
label={`${index + 1}/${pending}`} title='Pending proof nodes' />
<Item {...getStatus(infos)} />
+ <IconButton
+ display={size > 1}
+ icon='CIRC.PLUS' selected={subtree} onClick={flipT}
+ title='Show all tactic nodes' />
+ <IconButton
+ display={size > 1}
+ icon='CIRC.CHECK' selected={unproved} onClick={flipU}
+ title='Show unproved sub-goals only' />
<Filler />
<IconButton
icon={copied ? 'DUPLICATE' : (saved ? 'FOLDER' : 'FOLDER.OPEN')}
diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index e8582771a6c..d8a6c7fe1c0 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -142,46 +142,69 @@ let () =
end
(* -------------------------------------------------------------------------- *)
-(* --- Proof Cursor --- *)
+(* --- Proof Status --- *)
(* -------------------------------------------------------------------------- *)
let () =
- let state = R.signature ~input:(module W.Goal) () in
- let set_index = R.result state ~name:"index"
+ let status = R.signature () in
+ let get_main = R.param status ~name:"main"
+ ~descr:(Md.plain "Proof Obligation") (module W.Goal) in
+ let get_unproved = R.param status ~name:"unproved" ~default:false
+ ~descr:(Md.plain "Report unproved children only")
+ (module D.Jbool) in
+ let get_subtree = R.param status ~name:"subtree" ~default:false
+ ~descr:(Md.plain "Report subtree children only")
+ (module D.Jbool) in
+ let set_size = R.result status ~name:"size"
+ ~descr:(Md.plain "Proof size") (module D.Jint) in
+ let set_index = R.result status ~name:"index"
~descr:(Md.plain "Current node index among pending nodes (else -1)")
(module D.Jint) in
- let set_pending = R.result state ~name:"pending"
+ let set_pending = R.result status ~name:"pending"
~descr:(Md.plain "Pending proof nodes") (module D.Jint) in
- let set_current = R.result state ~name:"current"
+ let set_current = R.result status ~name:"current"
~descr:(Md.plain "Current proof node") (module Node) in
- let set_parents = R.result state ~name:"parents"
+ let set_parents = R.result status ~name:"parents"
~descr:(Md.plain "parents nodes")
(module Path) in
- let set_tactic = R.result_opt state ~name:"tactic"
+ let set_tactic = R.result_opt status ~name:"tactic"
~descr:(Md.plain "Applied tactic (if any)")
(module Tactic) in
- let set_children = R.result state ~name:"children"
+ let set_children = R.result status ~name:"children"
~descr:(Md.plain "Children nodes")
(module Path) in
- R.register_sig ~package
+ R.register_sig ~package status
~kind:`GET ~name:"getProofStatus"
- ~descr:(Md.plain "Current Proof Status of a Goal") state
+ ~descr:(Md.plain "Current Proof Status of a Goal")
~signals:[proofStatus]
- begin fun rq wpo ->
- let tree = ProofEngine.proof ~main:wpo in
+ begin fun rq () ->
+ let tree = ProofEngine.proof ~main:(get_main rq) in
let root = ProofEngine.root tree in
set_pending rq (ProofEngine.pending root) ;
+ set_size rq (Stats.subgoals @@ ProofEngine.stats root);
let current, index =
match ProofEngine.current tree with
| `Main -> root, -1
| `Internal node -> node, -1
| `Leaf(idx,node) -> node, idx
in
+ let subgoals = ProofEngine.subgoals current in
set_index rq index ;
set_current rq current ;
set_parents rq @@ ProofEngine.path current ;
set_tactic rq @@ ProofEngine.tactic current ;
- set_children rq @@ ProofEngine.subgoals current ;
+ set_children rq @@
+ match get_unproved rq, get_subtree rq with
+ | false, false -> subgoals
+ | false, true ->
+ List.filter (fun n -> ProofEngine.subgoals n <> []) subgoals
+ | true, false ->
+ List.filter (fun n -> ProofEngine.pending n > 0) subgoals
+ | true, true ->
+ List.filter (fun n ->
+ ProofEngine.pending n > 0 ||
+ ProofEngine.subgoals n <> []
+ ) subgoals
end
(* -------------------------------------------------------------------------- *)
--
GitLab