diff --git a/ivette/src/dome/misc/system.ts b/ivette/src/dome/misc/system.ts
index eb24e7169db8372fde06a3c1e3548b78cd5c222e..297ae8c92b7ddf3b16fd482d12780ccbb3dad6f2 100644
--- a/ivette/src/dome/misc/system.ts
+++ b/ivette/src/dome/misc/system.ts
@@ -108,7 +108,7 @@ export const platform = thePlatform;
// --------------------------------------------------------------------------
export const emitter = new Emitter();
-emitter.setMaxListeners(250);
+emitter.setMaxListeners(1_000);
// --------------------------------------------------------------------------
// --- At Exit
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 84c39050f29256945e2a7e898dc92dc4b0255cc2..c33edca169b1fd5ce813fcf95adb4e5c739e6cfe 100644
--- a/ivette/src/frama-c/plugins/wp/api/tip/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
@@ -108,7 +108,7 @@ const getNodeInfos_internal: Server.GetRequest<
node,
{ title: string, proved: boolean, pending: number, size: number,
stats: string, results: [ prover, result ][], tactic?: tactic,
- header?: string, child?: string, path: node[], children: node[] }
+ header?: string, childLabel?: string, path: node[], children: node[] }
> = {
kind: Server.RqKind.GET,
name: 'plugins.wp.tip.getNodeInfos',
@@ -122,7 +122,7 @@ const getNodeInfos_internal: Server.GetRequest<
results: Json.jArray(Json.jPair( jProver, jResult,)),
tactic: Json.jOption(jTactic),
header: Json.jOption(Json.jString),
- child: Json.jOption(Json.jString),
+ childLabel: Json.jOption(Json.jString),
path: Json.jArray(jNode),
children: Json.jArray(jNode),
}),
@@ -133,7 +133,7 @@ export const getNodeInfos: Server.GetRequest<
node,
{ title: string, proved: boolean, pending: number, size: number,
stats: string, results: [ prover, result ][], tactic?: tactic,
- header?: string, child?: string, path: node[], children: node[] }
+ header?: string, childLabel?: string, path: node[], children: node[] }
>= getNodeInfos_internal;
const getResult_internal: Server.GetRequest<
@@ -153,28 +153,33 @@ export const getResult: Server.GetRequest<
>= getResult_internal;
const getProofStatus_internal: Server.GetRequest<
- goal,
- { index: number, pending: number, current: node, above: node[],
- below: node[], tactic?: tactic }
+ { 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,
- above: Json.jArray(jNode),
- below: Json.jArray(jNode),
+ parents: Json.jArray(jNode),
tactic: Json.jOption(jTactic),
+ children: Json.jArray(jNode),
}),
signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
};
/** Current Proof Status of a Goal */
export const getProofStatus: Server.GetRequest<
- goal,
- { index: number, pending: number, current: node, above: node[],
- below: node[], tactic?: tactic }
+ { 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/style.css b/ivette/src/frama-c/plugins/wp/style.css
index b53b0b3718a35fc710c195e0d0068a5e54ead46e..b3537373833cbb32262f704c52755cf8f1b65af5 100644
--- a/ivette/src/frama-c/plugins/wp/style.css
+++ b/ivette/src/frama-c/plugins/wp/style.css
@@ -96,21 +96,22 @@
padding-right: 8px;
}
-.wp-navbar-node.parent {
+.wp-navbar-node:hover {
+ background-color: var(--code-hover);
}
-.wp-navbar-node.current {
- font-weight: bold;
- padding-left: 4px;
- background-color: var(--code-select);
+.wp-navbar-node.parent {
+ padding-left: 0px;
}
-.wp-navbar-node:hover {
- background-color: var(--code-hover);
+.wp-navbar-node.child {
+ padding-left: 12px;
}
-.wp-navbar-node.child {
- padding-left: 8px;
+.wp-navbar-node.current {
+ font-weight: bold;
+ padding-left: 0px;
+ background-color: var(--code-select);
}
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index f02d98eacca49c2bee30d74e808bce90f56f0588..e128cc03f03f9415200db3e0457f5166d401622d 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -117,37 +117,43 @@ function RFormatSelector(props: Selector<TIP.rformat>): JSX.Element {
interface NodeProps {
node: TIP.node;
- current: Node;
parent?: boolean;
+ child?: boolean;
+ hasChildren?: boolean;
}
function Node(props: NodeProps): JSX.Element {
const cellRef = React.useRef<HTMLLabelElement>(null);
- const { node, parent } = props;
- const current = node === props.current;
+ const {
+ node,
+ parent = false,
+ child = false,
+ hasChildren = false,
+ } = props;
const debug = `#${node}`;
const {
- title = debug, child = 'Script', header = debug,
+ title = debug, childLabel = 'Script', header,
proved = false, pending = 0, size = 0
} = States.useRequest(
TIP.getNodeInfos, node, { pending: null, onError: null }
) ?? {};
const elt = cellRef.current;
+ const current = !child && !parent;
React.useEffect(() => {
if (current && elt) elt.scrollIntoView();
}, [elt, current]);
const className = classes(
'wp-navbar-node',
parent && 'parent',
+ child && 'child',
current && 'current',
- !parent && !current && 'child',
);
const icon =
- current
- ? (parent ? 'TRIANGLE.DOWN' : 'TRIANGLE.RIGHT')
- : (parent ? 'ANGLE.DOWN' : 'ANGLE.RIGHT');
+ parent ? 'ANGLE.DOWN' :
+ child ? 'ANGLE.RIGHT' :
+ hasChildren ? 'TRIANGLE.RIGHT' : 'TRIANGLE.RIGHT';
const kind = proved ? 'positive' : (parent ? 'default' : 'warning');
- const nodeName = parent ? `${child}: ${header}` : child;
+ const nodeName = header ? `${childLabel}: ${header}` : childLabel;
const nodeRest = size <= 1 ? '?' : `${pending}/${size}`;
const nodeFull = size <= 1 ? nodeName : `${nodeName} (${size})`;
const nodeLabel = proved ? nodeFull : `${nodeName} (${nodeRest})`;
@@ -168,23 +174,28 @@ function Node(props: NodeProps): JSX.Element {
}
interface NavBarProps {
- above: TIP.node[];
- below: TIP.node[];
- current: Node;
+ current: TIP.node | undefined;
+ parents: TIP.node[];
+ subgoals: TIP.node[];
}
function NavBar(props: NavBarProps): JSX.Element {
- const { current } = props;
- const parents = props.above.map(n => (
- <Node key={n} node={n} parent current={current} />
+ const parents = props.parents.map(n => (
+ <Node key={n} node={n} parent />
)).reverse();
- const children = props.below.map(n => (
- <Node key={n} node={n} current={current} />
+ const children = props.subgoals.map(n => (
+ <Node key={n} node={n} child />
));
+ const hasChildren = children.length > 0;
+ const current = (n => n ?
+ <Node key={n} node={n} hasChildren={hasChildren} />
+ : undefined
+ )(props.current);
return (
<Vbox className='wp-navbar'>
<Vbox>
{parents}
+ {current}
{children}
</Vbox>
</Vbox>
@@ -226,13 +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, above = [], below = [], index = -1, pending = 0, tactic: nodeTactic
- } = States.useRequest(TIP.getProofStatus, goal, { pending: null }) ?? {};
+ current, index = -1, pending = 0, size = 0,
+ tactic: nodeTactic, parents = [], children = [],
+ } = 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 }) ?? {};
@@ -287,7 +304,7 @@ export function TIPView(props: TIPProps): JSX.Element {
};
// --- Delete button
- const deleteAble = locked || above.length > 0;
+ const deleteAble = locked || children.length > 0;
const onDelete = (): void => {
const request = locked ? TIP.clearNodeTactic : TIP.clearParentTactic;
Server.send(request, current);
@@ -324,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')}
@@ -390,9 +413,9 @@ export function TIPView(props: TIPProps): JSX.Element {
</ToolBar>
<Hfill>
<NavBar
- above={above}
- below={below}
current={current}
+ parents={parents}
+ subgoals={children}
/>
<Vfill className='dome-positionned'>
<Overlay display className='wp-printer'>
diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index 6a686258ec2e012071a4a33250bcf377a89569af..d8a6c7fe1c0657732a8b852b79567316264d1b78 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -99,7 +99,7 @@ let () =
let set_header = R.result_opt inode ~name:"header"
~descr:(Md.plain "Proof node tactic label (if any)")
(module D.Jstring) in
- let set_child = R.result_opt inode ~name:"child"
+ let set_child_label = R.result_opt inode ~name:"childLabel"
~descr:(Md.plain "Proof node child label (from parent, if any)")
(module D.Jstring) in
let set_path = R.result inode ~name:"path"
@@ -116,12 +116,12 @@ let () =
set_proved rq (ProofEngine.fully_proved node);
set_pending rq (ProofEngine.pending node);
let s = ProofEngine.stats node in
- set_size rq (Stats.subgoals @@ s);
+ set_size rq (Stats.subgoals s);
set_stats rq (Pretty_utils.to_string Stats.pretty s);
set_results rq (Wpo.get_results @@ ProofEngine.goal node);
set_tactic rq (ProofEngine.tactic node);
set_header rq (ProofEngine.tactic_label node);
- set_child rq (ProofEngine.child_label node);
+ set_child_label rq (ProofEngine.child_label node);
set_path rq (ProofEngine.path node);
set_children rq (ProofEngine.subgoals node);
end
@@ -142,59 +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_above = R.result state ~name:"above"
- ~descr:(Md.plain "Above nodes (up to current when internal)")
- (module Path) in
- let set_below = R.result state ~name:"below"
- ~descr:(Md.plain "Below nodes (including current when pending)")
+ 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
- R.register_sig ~package
+ let set_children = R.result status ~name:"children"
+ ~descr:(Md.plain "Children nodes")
+ (module Path) in
+ 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 ;
- let above = ProofEngine.path current in
- let below = ProofEngine.subgoals current in
- if below = [] then
- match above with
- | [] ->
- set_above rq [] ;
- set_below rq [] ;
- | p::_ ->
- set_above rq above ;
- set_below rq (ProofEngine.subgoals p) ;
- else
- begin
- set_above rq (current::above) ;
- set_below rq below ;
- end
+ 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
(* -------------------------------------------------------------------------- *)