Merge branch 'feature/wp/fix-ivette-events' into 'master'

[Ivette/WP] Better proof tree navigation

See merge request frama-c/frama-c!4560

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

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> = {

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);
 }
 
 /* -------------------------------------------------------------------------- */

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'>

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
 
 (* -------------------------------------------------------------------------- *)