diff --git a/ivette/src/dome/misc/format.ts b/ivette/src/dome/misc/format.ts
new file mode 100644
index 0000000000000000000000000000000000000000..feee25f0517b547b1f3834cd771037521594f1c4
--- /dev/null
+++ b/ivette/src/dome/misc/format.ts
@@ -0,0 +1,49 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/* ************************************************************************ */
+
+// --------------------------------------------------------------------------
+// --- Formatting Utilities
+// --------------------------------------------------------------------------
+
+/**
+ @packageDocumentation
+ @module dome/misc/format
+ */
+
+/**
+ Formats a duration, specified in seconds, into hour, minutes, seconds,
+ milliseconds or nanoseconds, depending on range.
+
+ For instance, returns `'250ms'` for an input time of `.25`.
+ */
+export function duration(time : number) : string {
+ if (time < 1.0e-3) return `${Math.round(time * 1.0e6)}µs`;
+ if (time < 1.0) return `${Math.round(time * 1.0e3)}ms`;
+ if (time < 60) return `${Math.round(time)}s`;
+ if (time < 3600) return `${Math.round(time / 60)}m`;
+ const h = Math.round(time / 3600);
+ const r = time - h * 3600;
+ const m = Math.round(r / 60);
+ return `${h}h ${m}m`;
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/misc/system.ts b/ivette/src/dome/misc/system.ts
index d3c6f8e5a7f6c01cfae4946ba67ec25d644d47d4..eb8b3ab6d98eae128290d02666fd97d5953b766e 100644
--- a/ivette/src/dome/misc/system.ts
+++ b/ivette/src/dome/misc/system.ts
@@ -36,6 +36,7 @@ import Emitter from 'events';
import Exec from 'child_process';
import fspath from 'path';
import fs from 'fs';
+import { clipboard } from 'electron';
// --------------------------------------------------------------------------
// --- Logging
@@ -618,6 +619,26 @@ export function spawn(
});
}
+// --------------------------------------------------------------------------
+// --- ClipBoard
+// --------------------------------------------------------------------------
+
+/**
+ Get plain text from system clipboard.
+*/
+export function readClipboardText(): string
+{
+ return clipboard.readText();
+}
+
+/**
+ Copy plain text to system clipboard.
+*/
+export function writeClipboardText(text: string): void
+{
+ clipboard.writeText(text);
+}
+
// --------------------------------------------------------------------------
// --- Window Management
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/renderer/controls/buttons.tsx b/ivette/src/dome/renderer/controls/buttons.tsx
index 15314c84a7eca2e4506515234ac7a68a5a92b751..3120b6ff51ccae5bf60c165f3075267a45cffccb 100644
--- a/ivette/src/dome/renderer/controls/buttons.tsx
+++ b/ivette/src/dome/renderer/controls/buttons.tsx
@@ -475,6 +475,8 @@ export interface SelectProps {
disabled?: boolean;
/** Currently selected value. */
value?: string;
+ /** Keep focus when selected (default to false). */
+ focus?: boolean;
/** Callback to selected values. */
onChange?: (newValue?: string) => void;
/** Default selected value. */
@@ -497,7 +499,7 @@ export interface SelectProps {
*/
export function Select(props: SelectProps): JSX.Element {
- const { onChange, placeholder } = props;
+ const { onChange, placeholder, focus=false } = props;
const className = classes(
'dome-xSelect dome-xBoxButton dome-xButton-default dome-xButton-label',
props.className,
@@ -505,6 +507,8 @@ export function Select(props: SelectProps): JSX.Element {
const disabled = onChange ? DISABLED(props) : true;
const callback = (evt: React.ChangeEvent<HTMLSelectElement>): void => {
if (onChange) onChange(evt.target.value);
+ const target = evt.target;
+ if (!focus) setImmediate(() => target.blur());
};
return (
<select
@@ -522,6 +526,64 @@ export function Select(props: SelectProps): JSX.Element {
);
}
+// --------------------------------------------------------------------------
+// --- Spinner
+// --------------------------------------------------------------------------
+
+export interface SpinnerProps {
+ /** Field identifier (to make forms or labels) */
+ id?: string;
+ /** Button tooltip */
+ title?: string;
+ /** Button placeholder */
+ placeholder?: string;
+ /** Defaults to `true`. */
+ enabled?: boolean;
+ /** Defaults to `false`. */
+ disabled?: boolean;
+ /** Currently selected value. */
+ value?: number;
+ /** Minimum value. */
+ vmin?: number;
+ /** Maximum value. */
+ vmax?: number;
+ /** Increment and Decrement step. */
+ vstep?: number;
+ /** Callback to selected values. */
+ onChange?: (newValue: number) => void;
+ /** Default selected value. */
+ className?: string;
+ /** Additional style for the `< dov /> ` container of Raiods */
+ style?: React.CSSProperties;
+}
+
+export function Spinner(props: SpinnerProps): JSX.Element {
+ const { onChange } = props;
+ const className = classes( 'dome-xSpinner', props.className );
+ const disabled = onChange ? DISABLED(props) : true;
+ const callback = (evt: React.ChangeEvent<HTMLInputElement>): void => {
+ if (onChange) {
+ const newValue = Number.parseInt(evt.target.value);
+ if (!Number.isNaN(newValue)) onChange(newValue);
+ }
+ };
+ return (
+ <input
+ id={props.id}
+ type="number"
+ value={props.value}
+ min={props.vmin}
+ max={props.vmax}
+ step={props.vstep}
+ className={className}
+ style={props.style}
+ disabled={disabled}
+ placeholder={props.placeholder}
+ onChange={callback}
+ />
+ );
+}
+
// --------------------------------------------------------------------------
// --- Text Input
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/renderer/controls/gallery.json b/ivette/src/dome/renderer/controls/gallery.json
index efae6ebd9938395b4f9028873133d3e3c4689b80..abba175abcc93fa95f87b43eb17ac615db306378 100644
--- a/ivette/src/dome/renderer/controls/gallery.json
+++ b/ivette/src/dome/renderer/controls/gallery.json
@@ -175,6 +175,12 @@
"viewBox": "0 0 26 24",
"path": "M23.853 12.469q0-0.469-0.71-0.469h-14.571q-0.536 0-1.145 0.288t-0.958 0.703l-3.938 4.862q-0.241 0.321-0.241 0.536 0 0.469 0.71 0.469h14.571q0.536 0 1.152-0.295t0.951-0.71l3.938-4.862q0.241-0.295 0.241-0.522zM8.571 10.286h10.286v-2.143q0-0.536-0.375-0.911t-0.911-0.375h-7.714q-0.536 0-0.911-0.375t-0.375-0.911v-0.857q0-0.536-0.375-0.911t-0.911-0.375h-4.286q-0.536 0-0.911 0.375t-0.375 0.911v11.424l3.429-4.219q0.589-0.71 1.554-1.172t1.875-0.462zM25.567 12.469q0 0.83-0.616 1.607l-3.951 4.862q-0.576 0.71-1.554 1.172t-1.875 0.462h-14.571q-1.232 0-2.116-0.884t-0.884-2.116v-12.857q0-1.232 0.884-2.116t2.116-0.884h4.286q1.232 0 2.116 0.884t0.884 2.116v0.429h7.286q1.232 0 2.116 0.884t0.884 2.116v2.143h2.571q0.723 0 1.326 0.328t0.897 0.944q0.201 0.429 0.201 0.911z"
},
+ "EJECT": {
+ "section": "Desktop",
+ "title": "Eject Device",
+ "viewBox": "0 0 32 32",
+ "path": "M0 24h32v4h-32zM16 4l16 16h-32z"
+ },
"DISPLAY": {
"section": "Desktop",
"viewBox": "0 0 24 24",
diff --git a/ivette/src/dome/renderer/controls/icons.tsx b/ivette/src/dome/renderer/controls/icons.tsx
index 2821f316da391314a136d2d4f213932c5b99bc72..158adb3266357546e38bcfdf488f7ac158e1443e 100644
--- a/ivette/src/dome/renderer/controls/icons.tsx
+++ b/ivette/src/dome/renderer/controls/icons.tsx
@@ -81,7 +81,6 @@ export function SVG(props: SVGprops): null | JSX.Element {
return (
<svg
height={size}
- width={size}
style={{ bottom: offset }}
viewBox={viewBox}
className={className}
@@ -97,7 +96,7 @@ export function SVG(props: SVGprops): null | JSX.Element {
// --------------------------------------------------------------------------
export type IconKind =
- 'disabled' | 'selected' | 'positive' | 'negative' | 'warning';
+ 'disabled' | 'selected' | 'positive' | 'negative' | 'warning' | 'default';
/** Icon Component Properties */
export interface IconProps extends SVGprops {
@@ -123,15 +122,14 @@ export interface IconProps extends SVGprops {
*/
export function Icon(props: IconProps): JSX.Element {
const {
- id, title, onClick, fill, kind,
+ id, title, onClick, fill, kind='default',
size, className, offset, style,
visible = true, display = true,
} = props;
const divClass = classes(
- 'dome-xIcon',
+ 'dome-xIcon', `dome-xIcon-${kind}`,
!visible && 'dome-control-hidden',
!display && 'dome-control-erased',
- kind && ('dome-xIcon-' + kind),
className
);
const divStyle = styles(fill && { fill }, style);
diff --git a/ivette/src/dome/renderer/controls/labels.tsx b/ivette/src/dome/renderer/controls/labels.tsx
index f098e54ab8b2e4f8977b2332114875d273a8894c..7eefc1f4a9fe635b38d8ca32f4c1093a32f38209 100644
--- a/ivette/src/dome/renderer/controls/labels.tsx
+++ b/ivette/src/dome/renderer/controls/labels.tsx
@@ -115,6 +115,7 @@ const DESCR = 'dome-xLabel dome-text-descr';
const TDATA = 'dome-xLabel dome-text-data';
const TCODE = 'dome-xLabel dome-text-code';
const TCELL = 'dome-xLabel dome-text-cell';
+const TITEM = 'dome-xLabel dome-text-item';
// --------------------------------------------------------------------------
// --- Components
@@ -138,4 +139,7 @@ export const Code = React.forwardRef(makeLabel(TCODE));
/** Selectable inlined source-code content with default cursor. */
export const Cell = React.forwardRef(makeLabel(TCELL));
+/** Non-selectable inlined source-code content with default cursor. */
+export const Item = React.forwardRef(makeLabel(TITEM));
+
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/renderer/controls/style.css b/ivette/src/dome/renderer/controls/style.css
index 4962ceb30e4ac250abcc607f2d1214b6ecadb419..b3c4e6c2e57b450dba94f73a3b92bd4bddfd9a3b 100644
--- a/ivette/src/dome/renderer/controls/style.css
+++ b/ivette/src/dome/renderer/controls/style.css
@@ -10,8 +10,7 @@
}
.dome-xLabel.dome-text-descr {
- overflow: auto ;
- white-space: wrap ;
+ white-space: normal ;
}
/* -------------------------------------------------------------------------- */
@@ -29,12 +28,12 @@
position:relative ;
}
-.dome-xIcon-default { fill: var(--var-info-text-discrete) ; }
+.dome-xIcon-default { fill: var(--text-discrete) ; }
.dome-xIcon-disabled { fill: var(--background-intense) ; }
.dome-xIcon-selected { fill: var(--activated-button-color) ; }
.dome-xIcon-positive { fill: var(--positive-button-color) ; }
.dome-xIcon-negative { fill: var(--negative-button-color) ; }
-.dome-xIcon-warning { fill: var(--warning-button-color) ; }
+.dome-xIcon-warning { fill: var(--warning-button-hover) ; }
.dome-xBadge {
flex: 0 0 auto ;
@@ -415,6 +414,16 @@ meter::-webkit-meter-even-less-good-value {
width: max-content ;
}
+/* -------------------------------------------------------------------------- */
+/* --- Styling Spinner --- */
+/* -------------------------------------------------------------------------- */
+
+.dome-xSpinner {
+ text-align: right ;
+ padding-left: 12px ;
+ width: 80px ;
+}
+
/* -------------------------------------------------------------------------- */
/* --- Styling Field --- */
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/dome/renderer/dark.css b/ivette/src/dome/renderer/dark.css
index b58523a06c79376636c1d4d56faa593f08686e7d..48b30c7062056c07916cccb823805f7eec88da50 100644
--- a/ivette/src/dome/renderer/dark.css
+++ b/ivette/src/dome/renderer/dark.css
@@ -56,7 +56,7 @@
--positive-button-hover: #28661a;
--positive-button-active: #226014;
- --negative-button-color: #bc150e;
+ --negative-button-color: #a10f0f;
--negative-led-img: radial-gradient(circle at center, #df3b36, #c72a25c7);
--negative-button-img: linear-gradient(to bottom, #bc150e 0%, #cf1c17 100%);
--negative-button-hover: #b60f08;
diff --git a/ivette/src/dome/renderer/dome.tsx b/ivette/src/dome/renderer/dome.tsx
index 789b04d5cd2d432f0fe01bc19314b9515fc57a18..27e7814d7493fb54ed50a164f7b825cd206b8c82 100644
--- a/ivette/src/dome/renderer/dome.tsx
+++ b/ivette/src/dome/renderer/dome.tsx
@@ -784,51 +784,71 @@ export function useTimer(period: number, callback: () => void): void
}, [period, callback]);
}
-/** Protected callback against unmounted component.
+type Callback<A> = (arg: A) => void;
- The returned callback will not fired only when the component is mounted.
-
- Unless constant, first create the callback with `React.useCallback()`, then
- give it to `useActive()`.
+/**
+ Protected callback against unmounted component.
+ The returned callback will be only fired when the component is mounted.
+ The provided callback need not be memoized.
*/
-export function useActive<A>(
- callback: (arg: A) => void,
-): (arg:A) => void
+export function useProtected<A>(fn: Callback<A> | undefined): Callback<A>
{
- const active = React.useRef(false);
+ const cb = React.useRef<Callback<A>>();
React.useEffect(() => {
- active.current = true;
- return () => { active.current = false; };
+ cb.current = fn;
+ return () => { cb.current = undefined; };
+ }, [fn]);
+ const trigger = React.useCallback((arg: A) => {
+ const fn = cb.current;
+ if (fn) fn(arg);
}, []);
- return React.useCallback((arg: A) => {
- if (active.current) callback(arg);
- }, [callback]);
+ return trigger;
}
-/** Debounced callback (period in milliseconds).
-
- The debounceded callback will not be fired when the component is unmounted.
-
- Unless constant, first create the callback with `React.useCallback()`, then
- give it to `useDebounced()`.
+/**
+ Debounced callback (waiting time in milliseconds).
+ The returned callback will be only fired when the component is mounted.
+ The provided callback need not be memoized.
*/
export function useDebounced<A=void>(
- callback: (arg: A) => void,
- period: number,
-): (arg:A) => void
+ fn: Callback<A> | undefined,
+ delay: number
+): Callback<A>
{
- const active = React.useRef(false);
+ const cb = React.useRef<Callback<A>>();
React.useEffect(() => {
- active.current = true;
- return () => { active.current = false; };
- }, []);
- return React.useMemo(() =>
- _.debounce(
- (arg: A) => {
- if (active.current) callback(arg);
- }, period
- ), [callback, period]
- );
+ cb.current = fn;
+ return () => { cb.current = undefined; };
+ }, [fn]);
+ const trigger = React.useMemo(
+ () => _.debounce((arg: A) => {
+ const fn = cb.current;
+ if (fn) fn(arg);
+ }, delay), [delay]);
+ return trigger;
+}
+
+/**
+ Throttled callback (waiting time in milliseconds).
+ The returned callback will be only fired when the component is mounted.
+ The provided callback need not be memoized.
+ */
+export function useThrottled<A=void>(
+ fn: Callback<A> | undefined,
+ period: number
+): Callback<A>
+{
+ const cb = React.useRef<Callback<A>>();
+ React.useEffect(() => {
+ cb.current = fn;
+ return () => { cb.current = undefined; };
+ }, [fn]);
+ const trigger = React.useMemo(
+ () => _.throttle((arg: A) => {
+ const fn = cb.current;
+ if (fn) fn(arg);
+ }, period), [period]);
+ return trigger;
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/renderer/frame/style.css b/ivette/src/dome/renderer/frame/style.css
index 0f744024de94cbe6fae015aa249bd0959828b03f..43dd9b6fd4a060fbc5e2a4cbf1689456cd26978e 100644
--- a/ivette/src/dome/renderer/frame/style.css
+++ b/ivette/src/dome/renderer/frame/style.css
@@ -107,6 +107,7 @@
.dome-xSideBarSection-title {
position: sticky ;
+ z-index: +1;
top: 0px ;
padding-top: 0px;
padding-bottom: 0px ;
diff --git a/ivette/src/dome/renderer/frame/toolbars.tsx b/ivette/src/dome/renderer/frame/toolbars.tsx
index a824168884bdd63fd4ed9d38fa53650c132b3060..51f7355c2b27223f1aaed805f0e0ae4031d1526a 100644
--- a/ivette/src/dome/renderer/frame/toolbars.tsx
+++ b/ivette/src/dome/renderer/frame/toolbars.tsx
@@ -161,6 +161,8 @@ export interface ButtonProps<A> {
selection?: A;
/** Selection callback. Receives the button's value. */
onClick?: (value: A | undefined) => void;
+ /** Right-Click callback. Receives the button's value. */
+ onContextMenu?: (value: A | undefined) => void;
/** Button contents */
children?: React.ReactNode;
}
@@ -172,7 +174,7 @@ export function Button<A = undefined>(
const { visible = true, hidden = false } = props;
if (!visible || hidden) return null;
const { enabled = true, disabled = false } = props;
- const { selected, value, selection, onClick } = props;
+ const { selected, value, selection, onClick, onContextMenu } = props;
const isSelected = selected !== undefined
? selected
: (value !== undefined && value === selection);
@@ -182,6 +184,7 @@ export function Button<A = undefined>(
disabled={disabled || !enabled}
className={isSelected ? SELECT : (BUTTON + KIND(props.kind))}
onClick={onClick && (() => onClick(value))}
+ onContextMenu={onContextMenu && (() => onContextMenu(value))}
title={props.title}
>
{props.icon && <SVG id={props.icon} />}
@@ -280,6 +283,12 @@ export function ButtonGroup<A>(props: ButtonGroupProps<A>): JSX.Element {
// --- ToolBar Menu
// --------------------------------------------------------------------------
+export interface SelectProps extends SelectionProps<string>
+{
+ className?: string;
+ style?: React.CSSProperties;
+}
+
/** Toolbar Selector Menu.
Behaves likes a standard `<select>` element, except that callback directly
@@ -287,15 +296,20 @@ export function ButtonGroup<A>(props: ButtonGroupProps<A>): JSX.Element {
The list of options shall be given with standard
`<option value={...} label={...}>` elements.
*/
-export function Select(props: SelectionProps<string>): JSX.Element {
+export function Select(props: SelectProps): JSX.Element {
const { enabled = true, disabled = false, onChange } = props;
const callback =
(evt: React.ChangeEvent<HTMLSelectElement>): void => {
if (onChange) onChange(evt.target.value);
};
+ const className = classes(
+ 'dome-xToolBar-control dome-color-frame',
+ props.className
+ );
return (
<select
- className="dome-xToolBar-control dome-color-frame"
+ className={className}
+ style={props.style}
title={props.title}
value={props.value}
disabled={disabled || !enabled}
diff --git a/ivette/src/dome/renderer/layout/boxes.tsx b/ivette/src/dome/renderer/layout/boxes.tsx
index 5606a8d469736c6ec1b449e95604ddede8376a80..b32ab949deea22e7537d2e8aab5aed25de915b5d 100644
--- a/ivette/src/dome/renderer/layout/boxes.tsx
+++ b/ivette/src/dome/renderer/layout/boxes.tsx
@@ -235,4 +235,34 @@ export const Folder = (props: FolderProps): JSX.Element => {
);
};
-// --------------------------------------------------------------------------
+/* -------------------------------------------------------------------------- */
+/* --- Overlay Boxes --- */
+/* -------------------------------------------------------------------------- */
+
+export interface OverlayProps {
+ /** Overlay displayed (default is false). */
+ display?: boolean;
+ /** Class of the overlay contents. */
+ className?: string;
+ /** Additional style of the overlay contents. */
+ style?: React.CSSProperties;
+ /** Contents of the overlay. */
+ children?: React.ReactNode;
+}
+
+export function Overlay(props: OverlayProps): JSX.Element {
+ const {
+ className, display=false, style, children,
+ } = props;
+ const anchor = classes('dome-xOverlay-anchor', !display && 'dome-erased');
+ const contents = classes('dome-xOverlay-contents', className);
+ return (
+ <div className={anchor}>
+ <div className={contents} style={style}>
+ {children}
+ </div>
+ </div>
+ );
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/dome/renderer/layout/style.css b/ivette/src/dome/renderer/layout/style.css
index fd96bab00f3b41f4612e3f4e0bb9b51769350525..a83d879a0141e6fe35a12ac0cc7dd8350da0684e 100644
--- a/ivette/src/dome/renderer/layout/style.css
+++ b/ivette/src/dome/renderer/layout/style.css
@@ -20,9 +20,8 @@
.dome-xBoxes-grid
{
- flex: 1 1 auto ;
- overflow: auto ;
- display: grid ;
+ flex: 1 1 auto;
+ overflow: auto;
display: grid;
grid-auto-rows: auto;
grid-auto-flow: row;
@@ -513,3 +512,17 @@
}
/* -------------------------------------------------------------------------- */
+/* --- Overlay --- */
+/* -------------------------------------------------------------------------- */
+
+.dome-xOverlay-anchor {
+ display: inline-block;
+ width: 0px;
+ height: 0px;
+}
+
+.dome-xOverlay-contents {
+ z-index: 1;
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/dome/renderer/light.css b/ivette/src/dome/renderer/light.css
index 919c24be478240035817a130e9419aa90c1ab458..55a5cf4c0d591dccd0ef50fa77088d17cc8bf8e8 100644
--- a/ivette/src/dome/renderer/light.css
+++ b/ivette/src/dome/renderer/light.css
@@ -64,7 +64,7 @@
--warning-button-color: #fece72;
--warning-led-img: radial-gradient(circle at center, #ffc749, #ecd44f);
- --warning-button-img: linear-gradient(to bottom, #fece72 0%, #fcaa0e 100%);
+ --warning-button-img: linear-gradient(to bottom, #ffb000 0%, #ffb449 100%);
--warning-button-hover: orange;
--warning-button-active: #ffffff;
diff --git a/ivette/src/dome/renderer/style.css b/ivette/src/dome/renderer/style.css
index 89cb548cbcc943fde53f3b25fac3491b51d41c1f..ad640de4533911ff329e887669ac8c19cf4bf3e6 100644
--- a/ivette/src/dome/renderer/style.css
+++ b/ivette/src/dome/renderer/style.css
@@ -39,6 +39,10 @@ body {
visibility: hidden !important;
}
+.dome-positionned {
+ position: relative;
+}
+
.dome-color-frame {
fill: var(--text-discrete) ;
color: var(--text-discrete) ;
@@ -94,10 +98,11 @@ div.dome-dragged {
}
.dome-text-descr {
+ font-weight: lighter ;
font-family: sans-serif ;
font-size: smaller ;
user-select: none ;
- white-space: wrap ;
+ white-space: normal ;
text-overflow: ellipsis ;
}
@@ -127,6 +132,15 @@ div.dome-dragged {
text-overflow: clip ;
}
+.dome-text-item {
+ cursor: default ;
+ user-select: none ;
+ font-family: 'Andale mono', monospace ;
+ font-size: 9pt ;
+ white-space: nowrap ;
+ text-overflow: clip ;
+}
+
/* -------------------------------------------------------------------------- */
/* --- Theme-compliant Scrollbars --- */
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/dome/renderer/text/richtext.tsx b/ivette/src/dome/renderer/text/richtext.tsx
index 03859f53447d43b877d70910a16cf0b431fbf111..02ea5b7a143800453597a82069a72213b64e9254 100644
--- a/ivette/src/dome/renderer/text/richtext.tsx
+++ b/ivette/src/dome/renderer/text/richtext.tsx
@@ -53,6 +53,12 @@ export function byOffset(a : Offset, b : Offset): number
type View = CM.EditorView | null;
+const clipRange = (a: number, value: number, b: number): number => {
+ if (value < a) return a;
+ if (value > b) return b;
+ return value;
+};
+
/* -------------------------------------------------------------------------- */
/* --- Text View Updates --- */
/* -------------------------------------------------------------------------- */
@@ -68,13 +74,17 @@ function dispatchContents(view: CM.EditorView, text: string | CS.Text): void {
}
function dispatchReplace(view: CM.EditorView, rg: Range, text: string): void {
- const { offset: from, length } = rg;
- view.dispatch({ changes: { from, to: from + length, insert: text } });
+ const docLength = view.state.doc.length;
+ const { offset, length } = rg;
+ const endOffset = offset + length;
+ if (0 <= offset && offset <= endOffset && endOffset <= docLength)
+ view.dispatch({ changes: { from: offset, to: endOffset, insert: text } });
}
function dispatchScroll(view: CM.EditorView, rg: Range): void {
- const anchor = rg.offset;
- const head = anchor + rg.length;
+ const length = view.state.doc.length;
+ const anchor = clipRange(0, rg.offset, length);
+ const head = clipRange(anchor, anchor + rg.length, length);
view.dispatch({ scrollIntoView: true, selection: { anchor, head } });
}
@@ -179,8 +189,11 @@ export class TextProxy {
/** Returns 1 also when disconnected. */
lineAt(offset: number): number {
+ if (offset < 0) return -1;
const doc = this.toText();
if (!doc) return -1;
+ const length = doc.length;
+ if (offset > length) return -1;
return doc.lineAt(offset).number;
}
@@ -401,7 +414,10 @@ class Field<A> extends Extension {
const annot = CS.Annotation.define<A>();
const field = CS.StateField.define<A>({
create: () => init,
- update: (fd: A, tr: CS.Transaction) => tr.annotation(annot) ?? fd,
+ update: (fd: A, tr: CS.Transaction): A => {
+ const newValue = tr.annotation(annot);
+ return newValue !== undefined ? newValue : fd;
+ }
});
this.annot = annot;
this.field = field;
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index 5e73797a2f571719550adfa4714fdb0b2c4391b3..031e5b95806b3fc8df1c84536c3f8a8a5b28191a 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -78,6 +78,192 @@ export const byProver: Compare.Order<prover> = Compare.string;
/** Default value for `prover` */
export const proverDefault: prover = Json.jKey<'#prover'>('#prover')('');
+/** Signal for state [`provers`](#provers) */
+export const signalProvers: Server.Signal = {
+ name: 'plugins.wp.signalProvers',
+};
+
+const getProvers_internal: Server.GetRequest<null,prover[]> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.getProvers',
+ input: Json.jNull,
+ output: Json.jArray(jProver),
+ signals: [],
+};
+/** Getter for state [`provers`](#provers) */
+export const getProvers: Server.GetRequest<null,prover[]>= getProvers_internal;
+
+const setProvers_internal: Server.SetRequest<prover[],null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.setProvers',
+ input: Json.jArray(jProver),
+ output: Json.jNull,
+ signals: [],
+};
+/** Setter for state [`provers`](#provers) */
+export const setProvers: Server.SetRequest<prover[],null>= setProvers_internal;
+
+const provers_internal: State.State<prover[]> = {
+ name: 'plugins.wp.provers',
+ signal: signalProvers,
+ getter: getProvers,
+ setter: setProvers,
+};
+/** Selected Provers */
+export const provers: State.State<prover[]> = provers_internal;
+
+/** Signal for state [`process`](#process) */
+export const signalProcess: Server.Signal = {
+ name: 'plugins.wp.signalProcess',
+};
+
+const getProcess_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.getProcess',
+ input: Json.jNull,
+ output: Json.jNumber,
+ signals: [],
+};
+/** Getter for state [`process`](#process) */
+export const getProcess: Server.GetRequest<null,number>= getProcess_internal;
+
+const setProcess_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.setProcess',
+ input: Json.jNumber,
+ output: Json.jNull,
+ signals: [],
+};
+/** Setter for state [`process`](#process) */
+export const setProcess: Server.SetRequest<number,null>= setProcess_internal;
+
+const process_internal: State.State<number> = {
+ name: 'plugins.wp.process',
+ signal: signalProcess,
+ getter: getProcess,
+ setter: setProcess,
+};
+/** Server Processes */
+export const process: State.State<number> = process_internal;
+
+/** Signal for state [`timeout`](#timeout) */
+export const signalTimeout: Server.Signal = {
+ name: 'plugins.wp.signalTimeout',
+};
+
+const getTimeout_internal: Server.GetRequest<null,number> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.getTimeout',
+ input: Json.jNull,
+ output: Json.jNumber,
+ signals: [],
+};
+/** Getter for state [`timeout`](#timeout) */
+export const getTimeout: Server.GetRequest<null,number>= getTimeout_internal;
+
+const setTimeout_internal: Server.SetRequest<number,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.setTimeout',
+ input: Json.jNumber,
+ output: Json.jNull,
+ signals: [],
+};
+/** Setter for state [`timeout`](#timeout) */
+export const setTimeout: Server.SetRequest<number,null>= setTimeout_internal;
+
+const timeout_internal: State.State<number> = {
+ name: 'plugins.wp.timeout',
+ signal: signalTimeout,
+ getter: getTimeout,
+ setter: setTimeout,
+};
+/** Prover's Timeout */
+export const timeout: State.State<number> = timeout_internal;
+
+/** Data for array rows [`ProverInfos`](#proverinfos) */
+export interface ProverInfosData {
+ /** Entry identifier. */
+ prover: prover;
+ /** Prover Name */
+ name: string;
+ /** Prover Version */
+ version: string;
+ /** Prover Full Name (description) */
+ descr: string;
+}
+
+/** Decoder for `ProverInfosData` */
+export const jProverInfosData: Json.Decoder<ProverInfosData> =
+ Json.jObject({
+ prover: jProver,
+ name: Json.jString,
+ version: Json.jString,
+ descr: Json.jString,
+ });
+
+/** Natural order for `ProverInfosData` */
+export const byProverInfosData: Compare.Order<ProverInfosData> =
+ Compare.byFields
+ <{ prover: prover, name: string, version: string, descr: string }>({
+ prover: byProver,
+ name: Compare.alpha,
+ version: Compare.alpha,
+ descr: Compare.alpha,
+ });
+
+/** Signal for array [`ProverInfos`](#proverinfos) */
+export const signalProverInfos: Server.Signal = {
+ name: 'plugins.wp.signalProverInfos',
+};
+
+const reloadProverInfos_internal: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.reloadProverInfos',
+ input: Json.jNull,
+ output: Json.jNull,
+ signals: [],
+};
+/** Force full reload for array [`ProverInfos`](#proverinfos) */
+export const reloadProverInfos: Server.GetRequest<null,null>= reloadProverInfos_internal;
+
+const fetchProverInfos_internal: Server.GetRequest<
+ number,
+ { reload: boolean, removed: prover[], updated: ProverInfosData[],
+ pending: number }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.fetchProverInfos',
+ input: Json.jNumber,
+ output: Json.jObject({
+ reload: Json.jBoolean,
+ removed: Json.jArray(jProver),
+ updated: Json.jArray(jProverInfosData),
+ pending: Json.jNumber,
+ }),
+ signals: [],
+};
+/** Data fetcher for array [`ProverInfos`](#proverinfos) */
+export const fetchProverInfos: Server.GetRequest<
+ number,
+ { reload: boolean, removed: prover[], updated: ProverInfosData[],
+ pending: number }
+ >= fetchProverInfos_internal;
+
+const ProverInfos_internal: State.Array<prover,ProverInfosData> = {
+ name: 'plugins.wp.ProverInfos',
+ getkey: ((d:ProverInfosData) => d.prover),
+ signal: signalProverInfos,
+ fetch: fetchProverInfos,
+ reload: reloadProverInfos,
+ order: byProverInfosData,
+};
+/** Available Provers */
+export const ProverInfos: State.Array<prover,ProverInfosData> = ProverInfos_internal;
+
+/** Default value for `ProverInfosData` */
+export const ProverInfosDataDefault: ProverInfosData =
+ { prover: proverDefault, name: '', version: '', descr: '' };
+
/** Prover Result */
export type result =
{ descr: string, cached: boolean, verdict: string, solverTime: number,
@@ -167,16 +353,6 @@ export const byStats: Compare.Order<stats> =
export const statsDefault: stats =
{ summary: '', tactics: 0, proved: 0, total: 0 };
-const getAvailableProvers_internal: Server.GetRequest<null,prover[]> = {
- kind: Server.RqKind.GET,
- name: 'plugins.wp.getAvailableProvers',
- input: Json.jNull,
- output: Json.jArray(jProver),
- signals: [],
-};
-/** Returns the list of configured provers from why3 */
-export const getAvailableProvers: Server.GetRequest<null,prover[]>= getAvailableProvers_internal;
-
/** Data for array rows [`goals`](#goals) */
export interface goalsData {
/** Entry identifier. */
@@ -203,6 +379,8 @@ export interface goalsData {
status: status;
/** Prover Stats Summary */
stats: stats;
+ /** Proof Tree */
+ proof: boolean;
/** Script File */
script?: string;
/** Saved Script */
@@ -224,6 +402,7 @@ export const jGoalsData: Json.Decoder<goalsData> =
passed: Json.jBoolean,
status: jStatus,
stats: jStats,
+ proof: Json.jBoolean,
script: Json.jOption(Json.jString),
saved: Json.jBoolean,
});
@@ -234,7 +413,7 @@ export const byGoalsData: Compare.Order<goalsData> =
<{ wpo: goal, marker: marker, scope?: decl, property: marker,
fct?: string, bhv?: string, thy?: string, name: string,
smoke: boolean, passed: boolean, status: status, stats: stats,
- script?: string, saved: boolean }>({
+ proof: boolean, script?: string, saved: boolean }>({
wpo: byGoal,
marker: byMarker,
scope: Compare.defined(byDecl),
@@ -247,6 +426,7 @@ export const byGoalsData: Compare.Order<goalsData> =
passed: Compare.boolean,
status: byStatus,
stats: byStats,
+ proof: Compare.boolean,
script: Compare.defined(Compare.string),
saved: Compare.boolean,
});
@@ -303,7 +483,7 @@ export const goalsDataDefault: goalsData =
{ wpo: goalDefault, marker: markerDefault, scope: undefined,
property: markerDefault, fct: undefined, bhv: undefined, thy: undefined,
name: '', smoke: false, passed: false, status: statusDefault,
- stats: statsDefault, script: undefined, saved: false };
+ stats: statsDefault, proof: false, script: undefined, saved: false };
/** Proof Server Activity */
export const serverActivity: Server.Signal = {
diff --git a/ivette/src/frama-c/plugins/wp/api/tac/index.ts b/ivette/src/frama-c/plugins/wp/api/tac/index.ts
index ee290243ed1d4610fe4ce2b696a50a7522296b46..f2c0881779d2d0711821f09746271545a2ba2c58 100644
--- a/ivette/src/frama-c/plugins/wp/api/tac/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tac/index.ts
@@ -40,11 +40,19 @@ import * as State from 'frama-c/states';
//@ts-ignore
import { byNode } from 'frama-c/plugins/wp/api/tip';
//@ts-ignore
+import { byTactic } from 'frama-c/plugins/wp/api/tip';
+//@ts-ignore
import { jNode } from 'frama-c/plugins/wp/api/tip';
//@ts-ignore
+import { jTactic } from 'frama-c/plugins/wp/api/tip';
+//@ts-ignore
import { node } from 'frama-c/plugins/wp/api/tip';
//@ts-ignore
import { nodeDefault } from 'frama-c/plugins/wp/api/tip';
+//@ts-ignore
+import { tactic } from 'frama-c/plugins/wp/api/tip';
+//@ts-ignore
+import { tacticDefault } from 'frama-c/plugins/wp/api/tip';
/** Parameter kind */
export type kind =
@@ -173,7 +181,7 @@ export const parameterDefault: parameter =
/** Data for array rows [`tactical`](#tactical) */
export interface tacticalData {
/** Entry identifier. */
- id: Json.key<'#tactic'>;
+ id: tactic;
/** Tactic name */
label: string;
/** Tactic description */
@@ -189,7 +197,7 @@ export interface tacticalData {
/** Decoder for `tacticalData` */
export const jTacticalData: Json.Decoder<tacticalData> =
Json.jObject({
- id: Json.jKey<'#tactic'>('#tactic'),
+ id: jTactic,
label: Json.jString,
title: Json.jString,
error: Json.jOption(Json.jString),
@@ -200,9 +208,9 @@ export const jTacticalData: Json.Decoder<tacticalData> =
/** Natural order for `tacticalData` */
export const byTacticalData: Compare.Order<tacticalData> =
Compare.byFields
- <{ id: Json.key<'#tactic'>, label: string, title: string, error?: string,
+ <{ id: tactic, label: string, title: string, error?: string,
status: status, params: parameter[] }>({
- id: Compare.string,
+ id: byTactic,
label: Compare.string,
title: Compare.string,
error: Compare.defined(Compare.string),
@@ -227,7 +235,7 @@ export const reloadTactical: Server.GetRequest<null,null>= reloadTactical_intern
const fetchTactical_internal: Server.GetRequest<
number,
- { reload: boolean, removed: Json.key<'#tactic'>[], updated: tacticalData[],
+ { reload: boolean, removed: tactic[], updated: tacticalData[],
pending: number }
> = {
kind: Server.RqKind.GET,
@@ -235,7 +243,7 @@ const fetchTactical_internal: Server.GetRequest<
input: Json.jNumber,
output: Json.jObject({
reload: Json.jBoolean,
- removed: Json.jArray(Json.jKey<'#tactic'>('#tactic')),
+ removed: Json.jArray(jTactic),
updated: Json.jArray(jTacticalData),
pending: Json.jNumber,
}),
@@ -244,11 +252,11 @@ const fetchTactical_internal: Server.GetRequest<
/** Data fetcher for array [`tactical`](#tactical) */
export const fetchTactical: Server.GetRequest<
number,
- { reload: boolean, removed: Json.key<'#tactic'>[], updated: tacticalData[],
+ { reload: boolean, removed: tactic[], updated: tacticalData[],
pending: number }
>= fetchTactical_internal;
-const tactical_internal: State.Array<Json.key<'#tactic'>,tacticalData> = {
+const tactical_internal: State.Array<tactic,tacticalData> = {
name: 'plugins.wp.tac.tactical',
getkey: ((d:tacticalData) => d.id),
signal: signalTactical,
@@ -257,33 +265,32 @@ const tactical_internal: State.Array<Json.key<'#tactic'>,tacticalData> = {
order: byTacticalData,
};
/** Tactical Configurations */
-export const tactical: State.Array<Json.key<'#tactic'>,tacticalData> = tactical_internal;
+export const tactical: State.Array<tactic,tacticalData> = tactical_internal;
/** Default value for `tacticalData` */
export const tacticalDataDefault: tacticalData =
- { id: Json.jKey<'#tactic'>('#tactic')(''), label: '', title: '',
- error: undefined, status: statusDefault, params: [] };
+ { id: tacticDefault, label: '', title: '', error: undefined,
+ status: statusDefault, params: [] };
-const configureTactics_internal: Server.ExecRequest<{ node: node },null> = {
+const configureTactics_internal: Server.ExecRequest<node,null> = {
kind: Server.RqKind.EXEC,
name: 'plugins.wp.tac.configureTactics',
- input: Json.jObject({ node: jNode,}),
+ input: jNode,
output: Json.jNull,
signals: [ { name: 'plugins.wp.tip.printStatus' } ],
};
/** Configure all tactics */
-export const configureTactics: Server.ExecRequest<{ node: node },null>= configureTactics_internal;
+export const configureTactics: Server.ExecRequest<node,null>= configureTactics_internal;
const setParameter_internal: Server.ExecRequest<
- { node: node, tactic: Json.key<'#tactic'>, param: Json.key<'#param'>,
- value: Json.json },
+ { node: node, tactic: tactic, param: Json.key<'#param'>, value: Json.json },
null
> = {
kind: Server.RqKind.EXEC,
name: 'plugins.wp.tac.setParameter',
input: Json.jObject({
node: jNode,
- tactic: Json.jKey<'#tactic'>('#tactic'),
+ tactic: jTactic,
param: Json.jKey<'#param'>('#param'),
value: Json.jAny,
}),
@@ -292,19 +299,28 @@ const setParameter_internal: Server.ExecRequest<
};
/** Configure tactical parameter */
export const setParameter: Server.ExecRequest<
- { node: node, tactic: Json.key<'#tactic'>, param: Json.key<'#param'>,
- value: Json.json },
+ { node: node, tactic: tactic, param: Json.key<'#param'>, value: Json.json },
null
>= setParameter_internal;
-const applyTactic_internal: Server.ExecRequest<Json.key<'#tactic'>,node[]> = {
+const applyTactic_internal: Server.ExecRequest<tactic,node[]> = {
kind: Server.RqKind.EXEC,
name: 'plugins.wp.tac.applyTactic',
- input: Json.jKey<'#tactic'>('#tactic'),
+ input: jTactic,
output: Json.jArray(jNode),
signals: [],
};
/** Applies the (configured) tactic */
-export const applyTactic: Server.ExecRequest<Json.key<'#tactic'>,node[]>= applyTactic_internal;
+export const applyTactic: Server.ExecRequest<tactic,node[]>= applyTactic_internal;
+
+const applyTacticAndProve_internal: Server.ExecRequest<tactic,node[]> = {
+ kind: Server.RqKind.EXEC,
+ name: 'plugins.wp.tac.applyTacticAndProve',
+ input: jTactic,
+ output: Json.jArray(jNode),
+ signals: [],
+};
+/** Applies tactic and run provers on children */
+export const applyTacticAndProve: Server.ExecRequest<tactic,node[]>= applyTacticAndProve_internal;
/* ------------------------------------- */
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 f1c3ac6961a529da08f2a64c9a231de1b44b2590..84c39050f29256945e2a7e898dc92dc4b0255cc2 100644
--- a/ivette/src/frama-c/plugins/wp/api/tip/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
@@ -75,6 +75,11 @@ export const proofStatus: Server.Signal = {
name: 'plugins.wp.tip.proofStatus',
};
+/** Updated TIP printer */
+export const printStatus: Server.Signal = {
+ name: 'plugins.wp.tip.printStatus',
+};
+
/** Proof Node index */
export type node = Json.index<'#node'>;
@@ -87,55 +92,90 @@ export const byNode: Compare.Order<node> = Compare.number;
/** Default value for `node` */
export const nodeDefault: node = Json.jIndex<'#node'>('#node')(-1);
+/** Tactic identifier */
+export type tactic = Json.key<'#tactic'>;
+
+/** Decoder for `tactic` */
+export const jTactic: Json.Decoder<tactic> = Json.jKey<'#tactic'>('#tactic');
+
+/** Natural order for `tactic` */
+export const byTactic: Compare.Order<tactic> = Compare.string;
+
+/** Default value for `tactic` */
+export const tacticDefault: tactic = Json.jKey<'#tactic'>('#tactic')('');
+
const getNodeInfos_internal: Server.GetRequest<
node,
- { result: string, proved: boolean, pending: number, size: number,
- stats: string, results: [ prover, result ][], tactic: string,
- children: [ string, node ][] }
+ { title: string, proved: boolean, pending: number, size: number,
+ stats: string, results: [ prover, result ][], tactic?: tactic,
+ header?: string, child?: string, path: node[], children: node[] }
> = {
kind: Server.RqKind.GET,
name: 'plugins.wp.tip.getNodeInfos',
input: jNode,
output: Json.jObject({
- result: Json.jString,
+ title: Json.jString,
proved: Json.jBoolean,
pending: Json.jNumber,
size: Json.jNumber,
stats: Json.jString,
results: Json.jArray(Json.jPair( jProver, jResult,)),
- tactic: Json.jString,
- children: Json.jArray(Json.jPair( Json.jString, jNode,)),
+ tactic: Json.jOption(jTactic),
+ header: Json.jOption(Json.jString),
+ child: Json.jOption(Json.jString),
+ path: Json.jArray(jNode),
+ children: Json.jArray(jNode),
}),
signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
};
/** Proof node information */
export const getNodeInfos: Server.GetRequest<
node,
- { result: string, proved: boolean, pending: number, size: number,
- stats: string, results: [ prover, result ][], tactic: string,
- children: [ string, node ][] }
+ { title: string, proved: boolean, pending: number, size: number,
+ stats: string, results: [ prover, result ][], tactic?: tactic,
+ header?: string, child?: string, path: node[], children: node[] }
>= getNodeInfos_internal;
-const getProofState_internal: Server.GetRequest<
+const getResult_internal: Server.GetRequest<
+ { node: node, prover: prover },
+ result
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.tip.getResult',
+ input: Json.jObject({ node: jNode, prover: jProver,}),
+ output: jResult,
+ signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
+};
+/** Result for specified node and prover */
+export const getResult: Server.GetRequest<
+ { node: node, prover: prover },
+ result
+ >= getResult_internal;
+
+const getProofStatus_internal: Server.GetRequest<
goal,
- { current: node, path: node[], index: number, pending: number }
+ { index: number, pending: number, current: node, above: node[],
+ below: node[], tactic?: tactic }
> = {
kind: Server.RqKind.GET,
- name: 'plugins.wp.tip.getProofState',
+ name: 'plugins.wp.tip.getProofStatus',
input: jGoal,
output: Json.jObject({
- current: jNode,
- path: Json.jArray(jNode),
index: Json.jNumber,
pending: Json.jNumber,
+ current: jNode,
+ above: Json.jArray(jNode),
+ below: Json.jArray(jNode),
+ tactic: Json.jOption(jTactic),
}),
signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
};
/** Current Proof Status of a Goal */
-export const getProofState: Server.GetRequest<
+export const getProofStatus: Server.GetRequest<
goal,
- { current: node, path: node[], index: number, pending: number }
- >= getProofState_internal;
+ { index: number, pending: number, current: node, above: node[],
+ below: node[], tactic?: tactic }
+ >= getProofStatus_internal;
const goForward_internal: Server.SetRequest<goal,null> = {
kind: Server.RqKind.SET,
@@ -177,15 +217,45 @@ const goToNode_internal: Server.SetRequest<node,null> = {
/** Set current node of associated proof tree */
export const goToNode: Server.SetRequest<node,null>= goToNode_internal;
-const removeNode_internal: Server.SetRequest<node,null> = {
+const clearNode_internal: Server.SetRequest<node,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.tip.clearNode',
+ input: jNode,
+ output: Json.jNull,
+ signals: [],
+};
+/** Cancel all node results and sub-tree (if any) */
+export const clearNode: Server.SetRequest<node,null>= clearNode_internal;
+
+const clearNodeTactic_internal: Server.SetRequest<node,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.tip.clearNodeTactic',
+ input: jNode,
+ output: Json.jNull,
+ signals: [],
+};
+/** Cancel node current tactic */
+export const clearNodeTactic: Server.SetRequest<node,null>= clearNodeTactic_internal;
+
+const clearParentTactic_internal: Server.SetRequest<node,null> = {
kind: Server.RqKind.SET,
- name: 'plugins.wp.tip.removeNode',
+ name: 'plugins.wp.tip.clearParentTactic',
input: jNode,
output: Json.jNull,
signals: [],
};
-/** Remove node from tree and go to parent */
-export const removeNode: Server.SetRequest<node,null>= removeNode_internal;
+/** Cancel parent node tactic */
+export const clearParentTactic: Server.SetRequest<node,null>= clearParentTactic_internal;
+
+const clearGoal_internal: Server.SetRequest<goal,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.tip.clearGoal',
+ input: jGoal,
+ output: Json.jNull,
+ signals: [],
+};
+/** Remove the complete goal proof tree */
+export const clearGoal: Server.SetRequest<goal,null>= clearGoal_internal;
/** Proof part marker */
export type part = Json.key<'#part'>;
@@ -211,11 +281,6 @@ export const byTerm: Compare.Order<term> = Compare.string;
/** Default value for `term` */
export const termDefault: term = Json.jKey<'#term'>('#term')('');
-/** Updated TIP printer */
-export const printStatus: Server.Signal = {
- name: 'plugins.wp.tip.printStatus',
-};
-
/** Integer constants format */
export type iformat = "dec" | "hex" | "bin";
@@ -318,7 +383,8 @@ const getSelection_internal: Server.GetRequest<
part: Json.jOption(jPart),
term: Json.jOption(jTerm),
}),
- signals: [ { name: 'plugins.wp.tip.printStatus' } ],
+ signals: [ { name: 'plugins.wp.tip.printStatus' },
+ { name: 'plugins.wp.tip.proofStatus' } ],
};
/** Get current selection in proof node */
export const getSelection: Server.GetRequest<
@@ -326,4 +392,112 @@ export const getSelection: Server.GetRequest<
{ part?: part, term?: term }
>= getSelection_internal;
+const runProvers_internal: Server.SetRequest<
+ { node: node, timeout?: number, provers?: prover[] },
+ null
+ > = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.tip.runProvers',
+ input: Json.jObject({
+ node: jNode,
+ timeout: Json.jOption(Json.jNumber),
+ provers: Json.jOption(Json.jArray(jProver)),
+ }),
+ output: Json.jNull,
+ signals: [],
+};
+/** Schedule provers on proof node */
+export const runProvers: Server.SetRequest<
+ { node: node, timeout?: number, provers?: prover[] },
+ null
+ >= runProvers_internal;
+
+const killProvers_internal: Server.SetRequest<
+ { node: node, provers?: prover[] },
+ null
+ > = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.tip.killProvers',
+ input: Json.jObject({
+ node: jNode,
+ provers: Json.jOption(Json.jArray(jProver)),
+ }),
+ output: Json.jNull,
+ signals: [],
+};
+/** Interrupt running provers on proof node */
+export const killProvers: Server.SetRequest<
+ { node: node, provers?: prover[] },
+ null
+ >= killProvers_internal;
+
+const clearProvers_internal: Server.SetRequest<
+ { node: node, provers?: prover[] },
+ null
+ > = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.tip.clearProvers',
+ input: Json.jObject({
+ node: jNode,
+ provers: Json.jOption(Json.jArray(jProver)),
+ }),
+ output: Json.jNull,
+ signals: [],
+};
+/** Remove prover results from proof node */
+export const clearProvers: Server.SetRequest<
+ { node: node, provers?: prover[] },
+ null
+ >= clearProvers_internal;
+
+const getScriptStatus_internal: Server.GetRequest<
+ goal,
+ { proof: boolean, script?: string, saved: boolean }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.tip.getScriptStatus',
+ input: jGoal,
+ output: Json.jObject({
+ proof: Json.jBoolean,
+ script: Json.jOption(Json.jString),
+ saved: Json.jBoolean,
+ }),
+ signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
+};
+/** Script Status for a given Goal */
+export const getScriptStatus: Server.GetRequest<
+ goal,
+ { proof: boolean, script?: string, saved: boolean }
+ >= getScriptStatus_internal;
+
+const saveScript_internal: Server.SetRequest<goal,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.tip.saveScript',
+ input: jGoal,
+ output: Json.jNull,
+ signals: [],
+};
+/** Save Script for the Goal */
+export const saveScript: Server.SetRequest<goal,null>= saveScript_internal;
+
+const runScript_internal: Server.SetRequest<goal,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.tip.runScript',
+ input: jGoal,
+ output: Json.jNull,
+ signals: [],
+};
+/** Replay Saved Script for the Goal (if any) */
+export const runScript: Server.SetRequest<goal,null>= runScript_internal;
+
+const clearProofScript_internal: Server.SetRequest<goal,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.tip.clearProofScript',
+ input: jGoal,
+ output: Json.jNull,
+ signals: [],
+};
+/** Clear Proof and Remove any Saved Script for the Goal */
+export const clearProofScript: Server.SetRequest<goal,null>= clearProofScript_internal;
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index 349d1f2c2f144105788669a60323f107f3e731c9..167f55efeff29a8f73a99be6ad935f2e2a01beb0 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -21,13 +21,39 @@
/* ************************************************************************ */
import React from 'react';
-import { IconKind, Cell } from 'dome/controls/labels';
+import { Icon } from 'dome/controls/icons';
+import { IconKind, Cell, Descr } from 'dome/controls/labels';
import { Filter } from 'dome/table/models';
import { Table, Column } from 'dome/table/views';
import * as States from 'frama-c/states';
import * as Ast from 'frama-c/kernel/api/ast';
import * as WP from 'frama-c/plugins/wp/api';
+/* -------------------------------------------------------------------------- */
+/* --- Table Cells --- */
+/* -------------------------------------------------------------------------- */
+
+interface IconProps {
+ icon?: string;
+ title?: string;
+}
+
+function renderIcon(s : IconProps): JSX.Element {
+ const { icon=' ', title } = s;
+ return <Icon id={icon} title={title} />;
+}
+
+interface CellProps {
+ icon: string;
+ label: string;
+ kind: IconKind;
+ title: string;
+}
+
+function renderCell(s : CellProps): JSX.Element {
+ return <Cell {...s} />;
+}
+
/* -------------------------------------------------------------------------- */
/* --- Scope Column --- */
/* -------------------------------------------------------------------------- */
@@ -36,27 +62,44 @@ function getScope(g : WP.goalsData): string {
if (g.bhv && g.fct) return `${g.fct} — {g.bhv}}`;
if (g.fct) return g.fct;
if (g.thy) return g.thy;
- return '';
+ return 'Global';
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Script Column --- */
+/* -------------------------------------------------------------------------- */
+
+/* eslint-disable max-len */
+const savedScript: IconProps = { icon: 'FOLDER', title: 'Saved Script' };
+const updatedScript: IconProps = { icon: 'FOLDER.OPEN', title: 'Updated Script' };
+const proofEdit: IconProps = { icon: 'CODE', title: 'Proof Under Construction' };
+const proofNone: IconProps = { title: 'No Proof Script' };
+/* eslint-enable max-len */
+
+export function getScript(g : WP.goalsData): IconProps {
+ const { script, saved, proof } = g;
+ return (
+ script ? (saved ? savedScript : updatedScript)
+ : (proof ? proofEdit : proofNone)
+ );
}
/* -------------------------------------------------------------------------- */
/* --- Status Column --- */
/* -------------------------------------------------------------------------- */
-interface IconStatus {
+const noResult : CellProps =
+ { icon: 'MINUS', label: 'No Result', kind: 'disabled', title: 'No Result' };
+
+interface BaseProps {
icon: string;
label: string;
kind: IconKind;
title: string;
}
-interface Status extends IconStatus { label: string }
-
-const noResult : IconStatus =
- { icon: 'MINUS', label: 'No Result', kind: 'disabled', title: 'No Result' };
-
/* eslint-disable max-len */
-const baseStatus : { [key:string]: IconStatus } = {
+const baseStatus : { [key:string]: BaseProps } = {
'VALID': { icon: 'CHECK', label: 'Valid', kind: 'positive', title: 'Valid Goal' },
'PASSED': { icon: 'CHECK', label: 'Passed', kind: 'positive', title: 'Passed Test' },
'DOOMED': { icon: 'CROSS', label: 'Doomed', kind: 'negative', title: 'Doomed Test' },
@@ -68,15 +111,11 @@ const baseStatus : { [key:string]: IconStatus } = {
};
/* eslint-enable max-len */
-export function getStatus(g : WP.goalsData): Status {
+export function getStatus(g : WP.goalsData): CellProps {
const { label, ...base } = baseStatus[g.status] ?? noResult;
return { ...base, label: label + g.stats.summary };
}
-function renderStatus(s : Status): JSX.Element {
- return <Cell {...s} />;
-}
-
/* -------------------------------------------------------------------------- */
/* --- Goals Filter --- */
/* -------------------------------------------------------------------------- */
@@ -99,6 +138,7 @@ function filterGoal(
export interface GoalTableProps {
display: boolean;
failed: boolean;
+ scoped: boolean;
scope: Ast.decl | undefined;
current: WP.goal | undefined;
setCurrent: (goal: WP.goal) => void;
@@ -109,8 +149,8 @@ export interface GoalTableProps {
export function GoalTable(props: GoalTableProps): JSX.Element {
const {
- display, scope, failed,
- current, setCurrent, setTIP,
+ display, scoped, failed,
+ scope, current, setCurrent, setTIP,
setGoals, setTotal,
} = props;
const { model } = States.useSyncArrayProxy(WP.goals);
@@ -128,16 +168,27 @@ export function GoalTable(props: GoalTableProps): JSX.Element {
);
React.useEffect(() => {
- if (failed || !!scope) {
+ if (failed || scoped) {
model.setFilter(filterGoal(failed, scope));
} else {
model.setFilter();
}
- }, [model, scope, failed]);
+ }, [model, failed, scoped, scope]);
React.useEffect(() => setGoals(goals), [goals, setGoals]);
React.useEffect(() => setTotal(total), [total, setTotal]);
+ const renderEmpty = React.useCallback(() => {
+ const kind = failed ? ' failed' : '';
+ const loc = scoped ? ' in current scope' : '';
+ const icon = scoped ? 'CURSOR' : failed ? 'CIRC.INFO' : 'INFO';
+ return (
+ <Descr
+ className='wp-empty-goals'
+ icon={icon} label={`No${kind} goals${loc}`} />
+ );
+ }, [scoped, failed]);
+
return (
<Table
model={model}
@@ -146,15 +197,19 @@ export function GoalTable(props: GoalTableProps): JSX.Element {
selection={current}
onSelection={onSelection}
onDoubleClick={onDoubleClick}
+ renderEmpty={renderEmpty}
>
<Column id='scope' label='Scope'
width={150}
getter={getScope} />
<Column id='name' label='Property'
width={150} />
+ <Column id='script' icon='FILE'
+ fixed width={30}
+ getter={getScript} render={renderIcon} />
<Column id='status' label='Status'
fill={true}
- getter={getStatus} render={renderStatus} />
+ getter={getStatus} render={renderCell} />
</Table>
);
}
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index df58d4caa73ab40343036ccf7d77205a3d389c30..77e5de598048bea2e1d8efd22a0460e1dcbf4d59 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -75,16 +75,17 @@ function WPGoals(): JSX.Element {
selected={failed}
onClick={flipFailed} />
<IconButton
- icon={tip ? 'ITEMS.LIST' : 'MEDIA.PLAY'}
- kind={tip ? 'warning' : 'positive'}
+ icon='MEDIA.PLAY'
title={tip ? 'Back to Goals' : 'Interactive Proof Transformer'}
enabled={!!current}
+ selected={tip}
onClick={() => setTip(!tip)} />
</Ivette.TitleBar>
<GoalTable
display={!tip}
- scope={scope}
failed={failed}
+ scoped={scoped}
+ scope={scope}
current={current}
setCurrent={setCurrent}
setTIP={() => setTip(true)}
@@ -93,7 +94,9 @@ function WPGoals(): JSX.Element {
/>
<TIPView
display={tip}
- goal={current} />
+ goal={current}
+ onClose={() => setTip(false)}
+ />
</>
);
}
@@ -112,17 +115,21 @@ Ivette.registerComponent({
/* -------------------------------------------------------------------------- */
function ServerActivity(): JSX.Element {
- const rq = States.useRequest(WP.getScheduledTasks, null);
- const active = rq ? rq.active > 0 : false;
- const status = active ? 'active' : 'inactive';
+ const rq = States.useRequest(WP.getScheduledTasks, null, { pending: null });
+ const procs = rq ? rq.procs : 0;
+ const active = rq ? rq.active : 0;
+ const status = active > 0 ? 'active' : 'inactive';
const done = rq ? rq.done : 0;
const todo = rq ? rq.todo : 0;
const total = done + todo;
+ const progress = done + active;
+ const objective = done + todo + procs;
+ const title = `${done} / ${todo} (${active} running, ${procs} procs)`;
return (
- <Group display={total > 0}>
+ <Group display={total > 0} title={title}>
<LED status={status} />
<Label>WP</Label>
- <Meter value={done} min={0} max={done + total} />
+ <Meter min={0} value={progress} max={objective} />
<Inset />
</Group>
);
diff --git a/ivette/src/frama-c/plugins/wp/seq.tsx b/ivette/src/frama-c/plugins/wp/seq.tsx
index aadc99da689378d28b63cd60d49d2642aa2e6453..aaf2809e5019141c689d7421356640b075c768d1 100644
--- a/ivette/src/frama-c/plugins/wp/seq.tsx
+++ b/ivette/src/frama-c/plugins/wp/seq.tsx
@@ -115,10 +115,11 @@ class Sequent {
const gutters: GutterDecoration[] = [];
if (tag) {
const selection: Range = { offset: tag.offset, length: 0 };
- const lineFrom = proxy.lineAt(tag.offset+1);
- const lineTo = proxy.lineAt(tag.endOffset);
- for (let line = lineFrom; line <= lineTo; line++)
- gutters.push({ className: 'wp-gutter-part', gutter: '|', line });
+ const lineP = proxy.lineAt(tag.offset+1);
+ const lineQ = proxy.lineAt(tag.endOffset);
+ if (0 <= lineP && 0 <= lineQ)
+ for (let line = lineP; line <= lineQ; line++)
+ gutters.push({ className: 'wp-gutter-part', gutter: '|', line });
return { selection, gutters };
} else
return { selection: undefined, gutters };
@@ -155,6 +156,7 @@ class Sequent {
export interface GoalViewProps {
node: Node;
+ locked: boolean;
autofocus: boolean;
unmangled: boolean;
iformat: TIP.iformat;
@@ -162,13 +164,18 @@ export interface GoalViewProps {
}
export function GoalView(props: GoalViewProps): JSX.Element {
- const { node } = props;
+ const { node, locked } = props;
const jtext = States.useRequest(TIP.printSequent, props, {
pending: null,
offline: undefined,
onError: '',
}) ?? null;
- const { part, term } = States.useRequest(TIP.getSelection, node) ?? {};
+ const { part, term } =
+ States.useRequest(TIP.getSelection, node, {
+ pending: null,
+ offline: {},
+ onError: {},
+ }) ?? {};
const proxy = React.useMemo(() => new TextProxy(), []);
const sequent = React.useMemo(() => new Sequent(jtext), [jtext]);
React.useEffect(() => proxy.updateContents(sequent.text), [proxy, sequent]);
@@ -190,7 +197,7 @@ export function GoalView(props: GoalViewProps): JSX.Element {
Server.send(TIP.setSelection, { node, part, term });
return;
}
- }
+ } // otherwise
Server.send(TIP.clearSelection, node);
}, [sequent, node]);
return (
@@ -201,7 +208,7 @@ export function GoalView(props: GoalViewProps): JSX.Element {
selection={selection}
decorations={[hover, sequent.decorations, gutters]}
onHover={onHover}
- onClick={onClick}
+ onClick={locked ? undefined : onClick}
/>
);
}
diff --git a/ivette/src/frama-c/plugins/wp/style.css b/ivette/src/frama-c/plugins/wp/style.css
index eab44e5565f0e23534e141a1f2eb3d820a7ae515..b53b0b3718a35fc710c195e0d0068a5e54ead46e 100644
--- a/ivette/src/frama-c/plugins/wp/style.css
+++ b/ivette/src/frama-c/plugins/wp/style.css
@@ -1,5 +1,15 @@
/* -------------------------------------------------------------------------- */
-/* --- WP Panel Styles --- */
+/* --- WP Goals --- */
+/* -------------------------------------------------------------------------- */
+
+.wp-empty-goals {
+ position: absolute;
+ top: 12px;
+ left: 20px;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Sequent Editor --- */
/* -------------------------------------------------------------------------- */
.wp .cm-gutter {
@@ -15,3 +25,192 @@
{
background: var(--code-hover);
}
+
+.wp-printer
+{
+ position: absolute;
+ right: 18px;
+ top: 2px;
+ background: var(--background-report);
+}
+
+.wp-printer-field
+{
+ margin: 0px;
+ fill: var(--text-discrete);
+ color: var(--text-discrete);
+ font-size: x-small;
+ border-radius: 6px;
+ background: var(--background-report);
+}
+
+.wp-printer-field.selected
+{
+ font-weight: bolder;
+ fill: var(--positive-button-color);
+ color: var(--positive-button-color);
+}
+
+.wp-printer-field:hover
+{
+ /* fill: var(--default-button-color); */
+ /* color: var(--default-button-color); */
+ background: var(--background-button-hover) !important;
+}
+
+.wp-printer-button
+{
+ width: 30px;
+ padding: 5px 4px 5px 4px;
+}
+
+.wp-printer-locked
+{
+ fill: var(--negative-button-color);
+}
+
+.wp-printer-button dome-xIcon {
+ margin: 0px;
+ padding: 0px;
+}
+
+.wp-printer-select
+{
+ border: none;
+ box-shadow: none;
+ text-align: right;
+ padding: 0px;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Navigation Bar --- */
+/* -------------------------------------------------------------------------- */
+
+.wp-navbar {
+ overflow-x: hidden;
+ overflow-y: auto;
+ background: var(--background-sidebar);
+}
+
+.wp-navbar-node {
+ padding-right: 8px;
+}
+
+.wp-navbar-node.parent {
+}
+
+.wp-navbar-node.current {
+ font-weight: bold;
+ padding-left: 4px;
+ background-color: var(--code-select);
+}
+
+.wp-navbar-node:hover {
+ background-color: var(--code-hover);
+}
+
+.wp-navbar-node.child {
+ padding-left: 8px;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Tactics View --- */
+/* -------------------------------------------------------------------------- */
+
+.wp-sidebar-view {
+ padding: 2px 0px 2px 3px;
+ align-content: flex-start;
+ overflow-y: auto;
+ border-width: 1px;
+ border-left-style: solid;
+}
+
+.wp-tactical-item {
+ flex: 0 0 auto;
+ margin: 2px;
+ width: 120px;
+ border-style: solid;
+ border-width: 1px;
+ border-radius: 6px;
+}
+
+.wp-tactical-item.selected {
+ background: var(--code-select);
+}
+
+.wp-tactical-item:hover {
+ background: var(--code-hover);
+}
+
+.wp-tactical-cell {
+ flex: 1 0 90px;
+ margin-right: 0px;
+ text-overflow: ellipsis;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Tactic Configuration --- */
+/* -------------------------------------------------------------------------- */
+
+.wp-configure {
+ min-height: 32px;
+ align-items: baseline;
+ align-content: center;
+}
+
+.wp-configure .dome-xLabel {
+ padding: 0px 3px 0px 3px;
+ margin: 0px 3px 0px 3px;
+}
+
+.wp-configure .dome-xIconButton {
+ padding: 2px 5px 2px 5px;
+ width: 20px;
+}
+
+.wp-configure .dome-xIconButton.dome-control-enabled:hover {
+ border-radius: 4px;
+ background: var(--background-interaction);
+}
+
+.wp-config-tactic {
+ font-weight: bold;
+}
+
+.wp-config-info {
+ overflow: hidden;
+}
+
+.wp-config-field {
+ border: none;
+ margin-left: 4px;
+ border-radius: 4px;
+ background: var(--background-interaction);
+}
+
+.wp-config-checkbox .dome-xIcon-disabled {
+ fill: var(--disabled-text);
+}
+
+.wp-config-checkbox:hover {
+ border-radius: 6px;
+ background: var(--background-interaction);
+}
+
+.wp-config-switch {
+ padding-top: 0px;
+ padding-bottom: 0px;
+}
+
+.wp-config-spinner {
+ width: 60px;
+ color: var(--text-discrete);
+ background: var(--background-interaction);
+}
+
+input.wp-config-spinner:disabled {
+ color: var(--text-disabled);
+ background: var(--background-profound);
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/wp/tac.tsx b/ivette/src/frama-c/plugins/wp/tac.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..b5cc19e36f857e4799b7caf88591e5f7ae2e94cf
--- /dev/null
+++ b/ivette/src/frama-c/plugins/wp/tac.tsx
@@ -0,0 +1,602 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/* ************************************************************************ */
+
+import React, { Fragment } from 'react';
+import { classes } from 'dome/misc/utils';
+import { Icon } from 'dome/controls/icons';
+import { IconButton, IconButtonKind } from 'dome/controls/buttons';
+import { Spinner, Select } from 'dome/controls/buttons';
+import { Label, Item, Descr } from 'dome/controls/labels';
+import { Hbox, Vbox, Filler } from 'dome/layout/boxes';
+import { Separator } from 'dome/frame/toolbars';
+import * as Dnd from 'dome/dnd';
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
+import * as WP from 'frama-c/plugins/wp/api';
+import * as TIP from 'frama-c/plugins/wp/api/tip';
+import * as TAC from 'frama-c/plugins/wp/api/tac';
+
+type Goal = WP.goal | undefined;
+type Node = TIP.node | undefined;
+type Prover = WP.prover | undefined;
+type Tactic = TIP.tactic | undefined;
+
+/* -------------------------------------------------------------------------- */
+/* --- Use Actions --- */
+/* -------------------------------------------------------------------------- */
+
+type ProverRequest =
+ Server.SetRequest<{ node: TIP.node, provers?: WP.prover[] }, null>;
+
+function sendProver( rq: ProverRequest, node: Node, prover: Prover ): void
+{
+ if (node && prover) {
+ Server.send(rq, { node, provers: [prover] });
+ }
+}
+
+function sendProverTime( node: Node, prover: Prover, timeout: number): void
+{
+ if (node && prover && timeout > 0) {
+ Server.send(TIP.runProvers, { node, timeout, provers: [prover] });
+ }
+}
+
+function applyTactic(tactic: Tactic): void {
+ if (tactic) {
+ Server.send(TAC.applyTacticAndProve, tactic);
+ }
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Prover Feedback --- */
+/* -------------------------------------------------------------------------- */
+
+interface ProverActionProps {
+ icon: string;
+ kind: IconButtonKind;
+ play?: boolean;
+ clear?: boolean;
+ forward?: number;
+ running?: boolean;
+}
+
+function getProverActions(result : WP.result) : ProverActionProps {
+ switch(result.verdict) {
+ case '':
+ case 'none':
+ return { icon: 'CIRC.INFO', kind: 'default', play: true, clear: false };
+ case 'computing':
+ return { icon: 'EXECUTE', kind: 'default', running: true, clear: false };
+ case 'valid':
+ return { icon: 'CIRC.CHECK', kind: 'positive' };
+ case 'unknown':
+ case 'stepout':
+ return { icon: 'CIRC.CLOSE', kind: 'warning' };
+ case 'timeout':
+ {
+ const forward = result.proverTime * 2;
+ return { icon: 'CIRC.QUESTION', kind: 'warning', forward };
+ }
+ case 'failed':
+ default:
+ return { icon: 'WARNING', kind: 'negative' };
+ }
+}
+
+interface ProverItemProps {
+ node: Node;
+ prover: WP.prover;
+ result: WP.result;
+ inactive?: boolean;
+ selected: Prover;
+ setSelected: (prv: Prover) => void;
+}
+
+function ProverItem(props : ProverItemProps): JSX.Element
+{
+ const { node, prover, inactive=false, result, selected, setSelected } = props;
+ const { name } = States.useSyncArrayElt(WP.ProverInfos, prover) ?? {};
+ const { descr='No Result' } = result;
+ const { icon: status, kind, running=false, play=false } =
+ getProverActions(result);
+ const isSelected = prover === selected;
+ const className = classes(
+ 'dome-color-frame wp-tactical-item',
+ isSelected && 'selected',
+ );
+ const enabled = !inactive && (play || running);
+ const icon =
+ inactive ? 'LOCK' : running ? 'MEDIA.PAUSE' : 'MEDIA.PLAY';
+ const title =
+ inactive ? undefined :
+ running ? 'Interrupt Prover' : 'Run Prover';
+ const action = running ? TIP.killProvers : TIP.runProvers;
+ return (
+ <Hbox
+ className={className}
+ onClick={() => setSelected(prover)}
+ >
+ <Item
+ icon={status}
+ kind={kind}
+ className='wp-tactical-cell'
+ label={name}
+ title={inactive ? `${descr} (Inactive)` : descr}
+ />
+ <IconButton
+ icon={icon}
+ title={title}
+ kind={running ? 'warning' : 'positive'}
+ enabled={enabled}
+ onClick={() => sendProver(action, node, prover)}
+ />
+ </Hbox>
+ );
+}
+
+export interface ProverSelection {
+ node: Node;
+ selected: Prover;
+ setSelected: (prv: Prover) => void;
+}
+
+export function Provers(props: ProverSelection): JSX.Element {
+ const { node, selected, setSelected } = props;
+ const { results=[] } = States.useRequest(
+ TIP.getNodeInfos, node, { pending: null, onError: null }
+ ) ?? {};
+ const [ provers=[], setProvers ] = States.useSyncState(WP.provers);
+ const setItems = (prvs: string[]): void => setProvers(prvs.map(WP.jProver));
+ const children = [...provers].sort().map((prover) => {
+ const res = results.find(([p]) => p === prover);
+ const result = res ? res[1] : WP.resultDefault;
+ return (
+ <Dnd.Item id={prover} key={prover}>
+ <ProverItem
+ node={node}
+ prover={prover}
+ result={result}
+ selected={selected}
+ setSelected={setSelected} />
+ </Dnd.Item>
+ );
+ });
+ const isInactive = (p: WP.prover): boolean => (
+ p !== 'qed' && p !== 'script' && !provers.some(q => p === q)
+ );
+ const inactive =
+ results
+ .filter(([p]) => isInactive(p))
+ .map(([p, r]) => {
+ return (
+ <ProverItem
+ key={p}
+ node={node}
+ prover={p}
+ result={r}
+ inactive
+ selected={selected}
+ setSelected={setSelected} />
+ );
+ });
+ return (
+ <>
+ <Vbox>
+ <Dnd.List items={provers} setItems={setItems}>
+ {node ? children : null}
+ </Dnd.List>
+ </Vbox>
+ {inactive}
+ </>
+ );
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Tactical Item --- */
+/* -------------------------------------------------------------------------- */
+
+export interface TacticSelection {
+ goal: Goal;
+ node: Node;
+ locked: boolean;
+ selected: Tactic;
+ setSelected: (tac: Tactic) => void;
+}
+
+interface TacticItemProps extends TAC.tacticalData, TacticSelection {}
+
+function TacticItem(props: TacticItemProps): JSX.Element | null {
+ const { id: tactic, status, locked, selected, setSelected } = props;
+ if (status === 'NotApplicable') return null;
+ const ready = !locked && status === 'Applicable';
+ const isSelected = selected === tactic;
+ const onSelect = (): void => setSelected(tactic);
+ const onPlay = (): void => {
+ if (ready) {
+ applyTactic(tactic);
+ setSelected(undefined);
+ }
+ };
+ const className = classes(
+ 'dome-color-frame wp-tactical-item',
+ isSelected && 'selected',
+ );
+ return (
+ <Hbox
+ className={className}
+ onClick={onSelect}
+ onDoubleClick={onPlay}
+ >
+ <Item className="wp-tactical-cell" {...props}/>
+ <IconButton
+ icon={locked ? 'LOCK' : 'MEDIA.PLAY'}
+ title='Apply Tactic'
+ kind='positive'
+ enabled={ready}
+ onClick={onPlay} />
+ </Hbox>
+ );
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- All Tactics View --- */
+/* -------------------------------------------------------------------------- */
+
+export function Tactics(props: TacticSelection): JSX.Element {
+ const { node } = props;
+ const tactics = States.useSyncArrayData(TAC.tactical);
+ const items =
+ node
+ ? tactics.map(tac => <TacticItem key={tac.id} {...props} {...tac} />)
+ : null;
+ return <>{items}</>;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Tactical Parameter --- */
+/* -------------------------------------------------------------------------- */
+
+interface ParameterProps extends TAC.parameter {
+ node: TIP.node;
+ locked: boolean;
+ tactic: TIP.tactic;
+}
+
+function CheckBoxParam(props: ParameterProps): JSX.Element
+{
+ const { id: param, locked, node, tactic, label, title, value } = props;
+ const active = value === true;
+ const onClick = (): void => {
+ if (!locked)
+ Server.send(TAC.setParameter, { node, tactic, param, value: !active });
+ };
+ return (
+ <Label
+ className="wp-config-checkbox"
+ label={label}
+ title={title}
+ onClick={onClick} >
+ <Icon
+ className="wp-config-switch"
+ size={14}
+ offset={-2}
+ kind={locked ? 'disabled' : 'default'}
+ id={active ? 'SWITCH.ON' : 'SWITCH.OFF'} />
+ </Label>
+ );
+}
+
+function SpinnerParam(props: ParameterProps): JSX.Element
+{
+ const {
+ id: param, locked, node, tactic, label, title,
+ vmin, vmax, vstep, value: jval
+ } = props;
+ const onChange = (value: number): void => {
+ if (!locked)
+ Server.send(TAC.setParameter, { node, tactic, param, value });
+ };
+ const value = typeof(jval)==='number' ? jval : undefined;
+ return (
+ <Label label={label} title={title}>
+ <Spinner
+ className="wp-config-field wp-config-spinner"
+ value={value}
+ vmin={vmin}
+ vmax={vmax}
+ vstep={vstep}
+ disabled={locked}
+ onChange={onChange}
+ />
+ </Label>
+ );
+}
+
+function SelectorParam(props: ParameterProps): JSX.Element
+{
+ const {
+ id: param, locked, node, tactic, label, title,
+ value: jval, vlist=[]
+ } = props;
+ const value = typeof(jval) === 'string' ? jval : undefined;
+ const options = vlist.map(({ id, label, title }) =>
+ <option key={id} value={id} title={title}>{label}</option>
+ );
+ const onChange = (value: string | undefined): void => {
+ if (!locked)
+ Server.send(TAC.setParameter, { node, tactic, param, value });
+ };
+ return (
+ <Label label={label} title={title}>
+ <Select
+ className="wp-config-field wp-config-select"
+ value={value}
+ disabled={locked}
+ onChange={onChange}
+ >{options}</Select>
+ </Label>
+ );
+}
+
+function Parameter(props: ParameterProps): JSX.Element | null
+{
+ if (!props.enabled) return null;
+ switch(props.kind) {
+ case 'checkbox':
+ return <CheckBoxParam {...props} />;
+ case 'spinner':
+ return <SpinnerParam {...props} />;
+ case 'selector':
+ return <SelectorParam {...props} />;
+ default:
+ return null;
+ }
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Prover Configuration --- */
+/* -------------------------------------------------------------------------- */
+
+export function ConfigureProver(props: ProverSelection): JSX.Element {
+ const { node, selected: prover, setSelected } = props;
+ const { descr } = States.useSyncArrayElt(WP.ProverInfos, prover) ?? {};
+ const result = States.useRequest(
+ TIP.getResult, { node, prover }, { pending: null, onError: null }
+ ) ?? WP.resultDefault;
+ const [process = 1, setProcess] = States.useSyncState(WP.process);
+ const [timeout = 1, setTimeout] = States.useSyncState(WP.timeout);
+ const { icon, kind, clear=true, running=false, play=false, forward=0 } =
+ getProverActions(result);
+ const [fwdTime, setFwdTime] = React.useState(0);
+ const [fwdArmed, setFwdArmed] = React.useState(false);
+ const display = !!prover;
+ const action = running ? TIP.killProvers : TIP.runProvers;
+ const onPlay = (): void => sendProver(action, node, prover);
+ const onClear = (): void => sendProver(TIP.clearProvers, node, prover);
+ const onClose = (): void => setSelected(undefined);
+ const timedOut = forward > 0 && result.proverTime < timeout;
+ const enabled = play || running || timedOut;
+ const forwardTitle =
+ forward > 0 ? `Run Prover with ${forward}s` : 'Run Prover with Extra Time';
+ const onForward = (): void => {
+ setFwdTime(forward);
+ sendProverTime(node, prover, forward);
+ };
+ React.useEffect(() => {
+ if (fwdTime > 0) {
+ if (fwdArmed && !running) {
+ setFwdArmed(false);
+ setFwdTime(0);
+ }
+ if (!fwdArmed && running) {
+ setFwdArmed(true);
+ }
+ }
+ }, [running, fwdTime, fwdArmed] );
+ return (
+ <Hbox
+ className="dome-xToolBar dome-color-frame wp-configure"
+ display={display}
+ >
+ <Label
+ icon='SETTINGS'
+ label='Process' title='Server Processes (shared by all provers)'
+ >
+ <Spinner
+ className="wp-config-field wp-config-spinner"
+ onChange={setProcess}
+ value={process}
+ vmin={1}
+ vmax={36}
+ vstep={1}
+ />
+ </Label>
+ <Label
+ label='Timeout' title='Prover Timeout (shared by all provers)'
+ >
+ <Spinner
+ className="wp-config-field wp-config-spinner"
+ enabled={fwdTime===0}
+ onChange={setTimeout}
+ value={fwdTime > 0 ? fwdTime : timeout}
+ vmin={1}
+ vmax={3600}
+ vstep={1}
+ />
+ </Label>
+ <Separator />
+ <Item
+ key='prover'
+ title='Selected Prover Configuration'
+ className="wp-config-tactic"
+ label={descr} />
+ <Item
+ icon={icon}
+ kind={kind}
+ label={result.descr} />
+ <Filler />
+ <Hbox>
+ <IconButton
+ key='clear'
+ icon='MEDIA.PREV'
+ kind='negative'
+ enabled={clear}
+ title='Clear Prover Result'
+ onClick={onClear}
+ />
+ <IconButton
+ key='play'
+ icon={running ? 'MEDIA.PAUSE' : 'MEDIA.PLAY'}
+ kind={running ? 'warning' : 'positive'}
+ title={running ? 'Interrupt Prover' : 'Run Prover'}
+ enabled={enabled}
+ onClick={onPlay}
+ />
+ <IconButton
+ key='forward'
+ icon='MEDIA.NEXT'
+ kind='positive'
+ enabled={forward > 0}
+ title={forwardTitle}
+ onClick={onForward}
+ />
+ </Hbox>
+ <IconButton
+ key='close'
+ icon='CIRC.CLOSE'
+ title='Close Prover Configuration Panel'
+ onClick={onClose} />
+ </Hbox>
+ );
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Tactical Configuration --- */
+/* -------------------------------------------------------------------------- */
+
+const noTactic: TAC.tacticalData = {
+ ...TAC.tacticalDataDefault,
+ status: 'NotApplicable'
+};
+
+function useTactic(selected: Tactic): TAC.tacticalData {
+ const data = States.useSyncArrayElt(TAC.tactical, selected);
+ return data ?? noTactic;
+}
+
+interface StatusDescr {
+ icon: string;
+ kind: 'warning' | 'positive' | 'default';
+ label: string;
+}
+
+const Locked: StatusDescr = {
+ icon: 'CHECK',
+ kind: 'default',
+ label: 'Applied',
+};
+
+function getStatusDescription(tactical: TAC.tacticalData): StatusDescr {
+ const { status, error, params } = tactical;
+ if (error)
+ return { icon: 'WARNING', kind: 'warning', label: error };
+ if (status === 'NotConfigured')
+ return { icon: 'WARNING', kind: 'warning', label: 'Missing fields' };
+ if (params.length)
+ return { icon: 'CHECK', kind: 'positive', label: 'Configured' };
+ return { icon: 'CHECK', kind: 'positive', label: 'Ready' };
+}
+
+export function ConfigureTactic(props: TacticSelection): JSX.Element {
+ const { node, locked, selected: tactic, setSelected } = props;
+ const tactical = useTactic(tactic);
+ States.useRequest(TAC.configureTactics, node, { onError: null });
+ const { status, label, title, params } = tactical;
+ const isReady = !locked && status==='Applicable';
+ const display = !!tactic && (locked || status !== 'NotApplicable');
+ const statusDescr = locked ? Locked : getStatusDescription(tactical);
+ const onClose = (): void => setSelected(undefined);
+ const onPlay = (): void => { if (isReady) applyTactic(tactic); };
+ const onClear = (): void => {
+ Server.send(TIP.clearNode, node);
+ setSelected(undefined);
+ };
+ const parameters =
+ (node && tactic)
+ ? params.map((prm: TAC.parameter) =>
+ <Parameter
+ key={prm.id}
+ node={node}
+ tactic={tactic}
+ locked={locked}
+ {...prm}/>
+ ) : null;
+ return (
+ <Hbox
+ className="dome-xToolBar dome-color-frame wp-configure"
+ display={display}
+ >
+ <Item
+ key='tactic'
+ icon='TUNINGS'
+ title='Selected Tactic Configuration'
+ className="wp-config-tactic"
+ label={label} />
+ <Descr
+ key='info'
+ icon='CIRC.INFO'
+ className="wp-config-info"
+ label={title} />
+ <Filler key='filler'/>
+ <Descr
+ key='status'
+ className="wp-config-info"
+ title='Tactic Status'
+ {...statusDescr} />
+ <Fragment key='params'>{parameters}</Fragment>
+ <IconButton
+ key='play'
+ icon={locked ? 'LOCK' : 'MEDIA.PLAY'}
+ kind='positive'
+ title='Apply Tactic'
+ enabled={isReady}
+ display={!locked}
+ onClick={onPlay} />
+ <IconButton
+ key='clear'
+ icon='MEDIA.PREV'
+ kind='negative'
+ display={locked}
+ title='Cancel Tactic and Remove Sub-Tree'
+ onClick={onClear} />
+ <IconButton
+ key='close'
+ icon='CIRC.CLOSE'
+ title='Close Tactic Configuration Panel'
+ disabled={locked}
+ onClick={onClose} />
+ </Hbox>
+ );
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index 04f97441ccc80019792a7d75edd17761a0fecabd..dd937e929831375ad89fcebc0e07fe48957d0c07 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -23,53 +23,59 @@
import React from 'react';
import * as Dome from 'dome';
-import { json } from 'dome/data/json';
-import { Cell } from 'dome/controls/labels';
-import { ToolBar, Select, Filler } from 'dome/frame/toolbars';
-import { Vfill } from 'dome/layout/boxes';
+import { classes } from 'dome/misc/utils';
+import { Icon } from 'dome/controls/icons';
+import { Cell, Item } from 'dome/controls/labels';
+import { IconButton } from 'dome/controls/buttons';
+import {
+ ToolBar, Select, Filler,
+ Button, ButtonGroup
+} from 'dome/frame/toolbars';
+import { Hfill, Vfill, Vbox, Overlay } from 'dome/layout/boxes';
+import { writeClipboardText } from 'dome/system';
+
+import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
import * as WP from 'frama-c/plugins/wp/api';
import * as TIP from 'frama-c/plugins/wp/api/tip';
import { getStatus } from './goals';
import { GoalView } from './seq';
+import { Provers, Tactics, ConfigureProver, ConfigureTactic } from './tac';
/* -------------------------------------------------------------------------- */
/* --- Sequent Printing Modes --- */
/* -------------------------------------------------------------------------- */
-type Focus = 'AUTOFOCUS' | 'FULLCONTEXT' | 'MEMORY' | 'RAW';
+type Node = TIP.node | undefined;
+type Prover = WP.prover | undefined;
+type Tactic = TIP.tactic | undefined;
interface Selector<A> {
value: A;
setValue: (value: A) => void;
}
-function jFocus(js: json): Focus {
- switch(js) {
- case 'AUTOFOCUS':
- case 'FULLCONTEXT':
- case 'MEMORY':
- case 'RAW':
- return (js as Focus);
- default:
- return 'AUTOFOCUS';
- }
+interface BoolSelector extends Selector<boolean> {
+ label: string;
+ title: string;
}
-function FocusSelector(props: Selector<Focus>): JSX.Element {
+function AFormatSelector(props: BoolSelector): JSX.Element {
const { value, setValue } = props;
+ const className = classes(
+ 'wp-printer-field wp-printer-button',
+ value && 'selected'
+ );
return (
- <Select
- value={value}
- title='Autofocus Mode'
- onChange={(v) => setValue(jFocus(v))}
+ <Item
+ className={className}
+ label={props.label}
+ title={props.title}
+ onClick={() => setValue(!value)}
>
- <option value='AUTOFOCUS'>Auto Focus</option>
- <option value='FULLCONTEXT'>Full Context</option>
- <option value='MEMORY'>Memory Model</option>
- <option value='RAW'>Raw Proof</option>
- </Select>
+ <Icon id={value ? 'SWITCH.ON' : 'SWITCH.OFF'} />
+ </Item>
);
}
@@ -77,13 +83,14 @@ function IFormatSelector(props: Selector<TIP.iformat>): JSX.Element {
const { value, setValue } = props;
return (
<Select
+ className='wp-printer-field wp-printer-select'
value={value}
- title='Large Integers Format'
+ title='Large integers format.'
onChange={(v) => setValue(TIP.jIformat(v))}
>
- <option value='dec'>Int</option>
- <option value='hex'>Hex</option>
- <option value='bin'>Bin</option>
+ <option value='dec' title='Integer'>int</option>
+ <option value='hex' title='Hex.'>hex</option>
+ <option value='bin' title='Binary'>bin</option>
</Select>
);
}
@@ -92,84 +99,353 @@ function RFormatSelector(props: Selector<TIP.rformat>): JSX.Element {
const { value, setValue } = props;
return (
<Select
+ className='wp-printer-field wp-printer-select'
value={value}
- title='Floatting Point Constants Format'
+ title='Floatting point format.'
onChange={(v) => setValue(TIP.jRformat(v))}
>
- <option value='ratio'>Real</option>
- <option value='float'>Float</option>
- <option value='double'>Double</option>
+ <option value='ratio' title='Rational fraction'>frac</option>
+ <option value='float' title='IEEE Float 32-bits'>f32</option>
+ <option value='double' title='IEEE Float 64-bits'>f64</option>
</Select>
);
}
/* -------------------------------------------------------------------------- */
-/* --- TIP View --- */
+/* --- Node Path --- */
/* -------------------------------------------------------------------------- */
-interface ProofState {
- current: TIP.node | undefined;
- index: number;
- pending: number;
+interface NodeProps {
+ node: TIP.node;
+ current: Node;
+ parent?: boolean;
}
-function useProofState(target: WP.goal | undefined): ProofState {
- const DefaultProofState: ProofState = {
- current: undefined, index: 0, pending: 0
- };
- return States.useRequest(
- TIP.getProofState,
- target,
- { onError: DefaultProofState }
- ) ?? DefaultProofState;
+function Node(props: NodeProps): JSX.Element
+{
+ const cellRef = React.useRef<HTMLLabelElement>(null);
+ const { node, parent } = props;
+ const current = node === props.current;
+ const debug = `#${node}`;
+ const {
+ title=debug, child='Script', header=debug,
+ proved=false, pending=0, size=0
+ } = States.useRequest(
+ TIP.getNodeInfos, node, { pending: null, onError: null }
+ ) ?? {};
+ const elt = cellRef.current;
+ React.useEffect(() => {
+ if (current && elt) elt.scrollIntoView();
+ }, [elt, current]);
+ const className = classes(
+ 'wp-navbar-node',
+ parent && 'parent',
+ current && 'current',
+ !parent && !current && 'child',
+ );
+ const icon =
+ current
+ ? (parent ? 'TRIANGLE.DOWN' : 'TRIANGLE.RIGHT')
+ : (parent ? 'ANGLE.DOWN' : 'ANGLE.RIGHT');
+ const kind = proved ? 'positive' : (parent ? 'default' : 'warning');
+ const nodeName = parent ? `${child}: ${header}` : child;
+ const nodeRest = size <= 1 ? '?' : `${pending}/${size}`;
+ const nodeFull = size <= 1 ? nodeName : `${nodeName} (${size})`;
+ const nodeLabel = proved ? nodeFull : `${nodeName} (${nodeRest})`;
+ const proofState =
+ proved ? 'proved' :
+ pending < size ? `pending ${pending}/${size}` : 'unproved';
+ const fullTitle = `${title} (${proofState})`;
+ const onSelection = (): void => { Server.send(TIP.goToNode, node); };
+ return (
+ <Item
+ ref={cellRef} className={className}
+ icon={icon} kind={kind}
+ label={nodeLabel}
+ title={fullTitle}
+ onClick={onSelection}
+ />
+ );
+}
+
+interface NavBarProps {
+ above: TIP.node[];
+ below: TIP.node[];
+ current: Node;
+}
+
+function NavBar(props: NavBarProps): JSX.Element {
+ const { current } = props;
+ const parents = props.above.map(n => (
+ <Node key={n} node={n} parent current={current} />
+ )).reverse();
+ const children = props.below.map(n => (
+ <Node key={n} node={n} current={current} />
+ ));
+ return (
+ <Vbox className='wp-navbar'>
+ <Vbox>
+ {parents}
+ {children}
+ </Vbox>
+ </Vbox>
+ );
}
-function useTarget(target: WP.goal | undefined) : WP.goalsData {
- return States.useSyncArrayElt( WP.goals, target ) ?? WP.goalsDataDefault;
+/* -------------------------------------------------------------------------- */
+/* --- Available Provers --- */
+/* -------------------------------------------------------------------------- */
+
+interface ProverConfig {
+ available: WP.ProverInfosData[];
+ provers: WP.prover[];
+ setProvers: (prvs: WP.prover[]) => void;
+}
+
+export function popupProvers(config: ProverConfig): void {
+ const { available, provers, setProvers } = config;
+ Dome.popupMenu(
+ available.map(({ prover: id, descr: label }) => {
+ const checked = provers.some(p => p === id);
+ const updated =
+ checked ? provers.filter(p => p !== id) : provers.concat(id);
+ const onClick = (): void => setProvers(updated);
+ return { id, label, checked, onClick };
+ })
+ );
}
+/* -------------------------------------------------------------------------- */
+/* --- TIP View --- */
+/* -------------------------------------------------------------------------- */
+
export interface TIPProps {
display: boolean;
goal: WP.goal | undefined;
+ onClose: () => void;
}
export function TIPView(props: TIPProps): JSX.Element {
- const { display, goal } = props;
- const infos = useTarget(goal);
- const { current, index, pending } = useProofState(goal);
- const [ focus, setFocus ] = Dome.useWindowSettings<Focus>(
- 'wp.tip.focus', jFocus, 'AUTOFOCUS'
- );
+ const { display, goal, onClose } = props;
+ // --- 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 } ) ?? {};
+ // --- script status
+ const { saved=false, proof=false, script } =
+ States.useRequest( TIP.getScriptStatus, goal, { pending: null } ) ?? {};
+ // --- provers
+ const available = States.useSyncArrayData(WP.ProverInfos);
+ const [ provers=[], setProvers ] = States.useSyncState(WP.provers);
+ // --- sidebar & toolbar states
+ const [ copied, setCopied ] = React.useState(false);
+ const [ tactic, setTactic ] = React.useState<Tactic>();
+ const [ prover, setProver ] = React.useState<Prover>();
+ // --- printer settings
+ const [ autofocus, setAF ] = Dome.useBoolSettings('wp.tip.autofocus', true);
+ const [ memory, setMEM ] = Dome.useBoolSettings('wp.tip.unmangled', true);
const [ iformat, setIformat ] = Dome.useWindowSettings<TIP.iformat>(
'wp.tip.iformat', TIP.jIformat, 'dec'
);
const [ rformat, setRformat ] = Dome.useWindowSettings<TIP.rformat>(
'wp.tip.rformat', TIP.jRformat, 'ratio'
);
- const autofocus = focus === 'AUTOFOCUS' || focus === 'MEMORY';
- const unmangled = focus === 'MEMORY' || focus === 'RAW';
+
+ // --- Script buttons
+ const onSave = (): void => { Server.send(TIP.saveScript, goal); };
+ const onReload = (): void => { Server.send(TIP.runScript, goal); };
+ const onTrash = (): void => { Server.send(TIP.clearProofScript, goal); };
+ const onCopied = Dome.useDebounced(() => setCopied(false), 1000);
+ const copyTitle = copied ? 'Copied' : `Script: ${script} (Click to copy)`;
+ const onCopy = (): void => {
+ if (script) writeClipboardText(script);
+ setCopied(true);
+ onCopied();
+ };
+
+ // --- derived states
+ const locked = nodeTactic !== undefined;
+ const configuredTactic = nodeTactic ?? tactic;
+
+ // --- current prover
+ const onSelectedProver = React.useCallback((prv) => {
+ setTactic(undefined);
+ setProver(prv);
+ }, []);
+
+ // --- current tactic
+ const onSelectedTactic = React.useCallback((tac) => {
+ setTactic(tac);
+ setProver(undefined);
+ }, []);
+
+ // --- prover selection
+ const onProverSelection = (): void => {
+ popupProvers({ available, provers, setProvers });
+ };
+
+ // --- Delete button
+ const deleteAble = locked || above.length > 0;
+ const onDelete = (): void => {
+ const request = locked ? TIP.clearNodeTactic : TIP.clearParentTactic;
+ Server.send(request, current);
+ };
+ const deleteTitle = locked ? 'Cancel Node Tactic' : 'Cancel Last Tactic';
+
+ // --- Next button
+ const nextIndex =
+ pending <= 0 ? undefined :
+ pending === 1 ? (index === 0 ? undefined : 0) :
+ (index + 1 < pending ? index + 1 : 0);
+ const prevIndex =
+ pending <= 0 ? undefined :
+ pending === 1 ? (index === 0 ? undefined : 0) :
+ (index < 1 ? pending - 1 : index - 1);
+ const nextAble = goal !== undefined && nextIndex !== undefined;
+ const prevAble = goal !== undefined && prevIndex !== undefined;
+ const nextTitle =
+ nextIndex !== undefined
+ ? `Goto Next Pending Goal (#${nextIndex+1} / ${pending})`
+ : `Goto Next Pending Goal (if any)`;
+ const prevTitle =
+ prevIndex !== undefined
+ ? `Goto Previous Pending Goal (#${prevIndex+1} / ${pending})`
+ : `Goto Previous Pending Goal (if any)`;
+ const onNext = (): void => {
+ Server.send(TIP.goToIndex, [goal, nextIndex]);
+ };
+ const onPrev = (): void => {
+ Server.send(TIP.goToIndex, [goal, prevIndex]);
+ };
+
+ // --- Component
return (
<Vfill display={display}>
<ToolBar>
<Cell
icon='HOME'
label={infos.wpo} title='Goal identifier' />
- <Cell
+ <Item
icon='CODE'
display={0 <= index && index < pending && 1 < pending}
label={`${index+1}/${pending}`} title='Pending proof nodes'/>
- <Cell {...getStatus(infos)}/>
+ <Item {...getStatus(infos)}/>
<Filler/>
- <FocusSelector value={focus} setValue={setFocus}/>
- <IFormatSelector value={iformat} setValue={setIformat}/>
- <RFormatSelector value={rformat} setValue={setRformat}/>
+ <IconButton
+ icon={copied ? 'DUPLICATE' : (saved ? 'FOLDER' : 'FOLDER.OPEN')}
+ visible={script !== undefined}
+ title={copyTitle}
+ onClick={onCopy} />
+ <ButtonGroup>
+ <Button
+ icon='RELOAD'
+ enabled={ script !== undefined && !saved }
+ title='Replay Proof Script from Disk'
+ onClick={onReload}
+ />
+ <Button
+ icon='SAVE'
+ enabled={ proof && !saved }
+ title='Save Proof Script on Disk'
+ onClick={onSave}
+ />
+ </ButtonGroup>
+ <ButtonGroup>
+ <Button
+ icon='MEDIA.PREV'
+ kind='negative'
+ enabled={deleteAble}
+ title={deleteTitle}
+ onClick={onDelete} />
+ <Button
+ icon='CROSS'
+ kind='negative'
+ enabled={ proof || script !== undefined }
+ title='Clear Proof and Remove Script (if any)'
+ onClick={onTrash}
+ />
+ </ButtonGroup>
+ <ButtonGroup>
+ <Button
+ icon='ANGLE.LEFT'
+ enabled={prevAble}
+ title={prevTitle}
+ onClick={onPrev} />
+ <Button
+ icon='EJECT'
+ title='Close Proof Transformer (back to goals)'
+ onClick={onClose} />
+ <Button
+ icon='ANGLE.RIGHT'
+ enabled={nextAble}
+ title={nextTitle}
+ onClick={onNext} />
+ </ButtonGroup>
+ <Button
+ icon='SETTINGS'
+ title='Active Provers Selection'
+ onClick={onProverSelection} />
</ToolBar>
- <GoalView
+ <Hfill>
+ <NavBar
+ above={above}
+ below={below}
+ current={current}
+ />
+ <Vfill className='dome-positionned'>
+ <Overlay display className='wp-printer'>
+ <Icon
+ id='LOCK'
+ title='Tactical Selection Locked'
+ className='wp-printer-locked'
+ display={locked} />
+ <AFormatSelector
+ value={autofocus} setValue={setAF}
+ label='AF' title='Autofocus mode.' />
+ <AFormatSelector
+ value={memory} setValue={setMEM}
+ label='MEM' title='Memory model internals.' />
+ <IFormatSelector value={iformat} setValue={setIformat}/>
+ <RFormatSelector value={rformat} setValue={setRformat}/>
+ </Overlay>
+ <GoalView
+ node={current}
+ locked={locked}
+ autofocus={autofocus}
+ unmangled={!memory}
+ iformat={iformat}
+ rformat={rformat}
+ />
+ </Vfill>
+ <Vbox className='wp-sidebar-view dome-color-frame'>
+ <Provers
+ node={current}
+ selected={prover}
+ setSelected={onSelectedProver}
+ />
+ <Tactics
+ goal={goal}
+ node={current}
+ locked={locked}
+ selected={configuredTactic}
+ setSelected={onSelectedTactic}
+ />
+ </Vbox>
+ </Hfill>
+ <ConfigureProver
+ node={current}
+ selected={prover}
+ setSelected={onSelectedProver}
+ />
+ <ConfigureTactic
+ goal={goal}
node={current}
- autofocus={autofocus}
- unmangled={unmangled}
- iformat={iformat}
- rformat={rformat}
+ locked={locked}
+ selected={configuredTactic}
+ setSelected={onSelectedTactic}
/>
</Vfill>
);
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 3e857376950ae9d44da9b3801bf9d45d93d9031d..13644db3a403696352168de1b8cc81d216b26b53 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -72,19 +72,18 @@ export interface UseRequestOptions<A> {
Options can be used to tune more precisely the behavior of the hook.
*/
-export function useRequest<In, Out>(
- rq: Server.GetRequest<In, Out>,
+export function useRequest<Kd extends Server.RqKind, In, Out>(
+ rq: Server.Request<Kd, In, Out>,
params: In | undefined,
options: UseRequestOptions<Out> = {},
): Out | undefined {
const initial = options.offline ?? undefined;
const [response, setResponse] = React.useState<Out | undefined>(initial);
- const doUpdateResponse = React.useCallback(
+ const updateResponse = Dome.useProtected(
(opt: Out | undefined | null): void => {
if (opt !== null) setResponse(opt);
- }, []);
- const updateResponse = Dome.useActive(doUpdateResponse);
-
+ }
+ );
// Fetch Request
async function trigger(): Promise<void> {
if (Server.isRunning() && params !== undefined) {
@@ -93,7 +92,7 @@ export function useRequest<In, Out>(
const r = await Server.send(rq, params);
updateResponse(r);
} catch (error) {
- if (options.onError !== undefined) {
+ if (options.onError === undefined) {
D.error(`Fail in useRequest '${rq.name}'. ${error}`);
}
updateResponse(options.onError);
@@ -211,6 +210,7 @@ class SyncState<A> extends GlobalState<A | undefined> {
super(undefined);
this.handler = h;
this.fetch = this.fetch.bind(this);
+ this.update = this.update.bind(this);
}
signal(): Server.Signal { return this.handler.signal; }
@@ -235,7 +235,24 @@ class SyncState<A> extends GlobalState<A | undefined> {
}
} catch (error) {
D.error(
- `Fail to update SyncState '${this.handler.name}'.`,
+ `Fail to fetch state '${this.handler.name}'.`,
+ `${error}`,
+ );
+ this.setValue(undefined);
+ }
+ }
+
+ async update(value: A): Promise<void> {
+ try {
+ if (Server.isRunning() && this.handler.setter) {
+ this.status = SyncStatus.Loading;
+ await Server.send(this.handler.setter, value);
+ this.status = SyncStatus.Loaded;
+ this.setValue(value);
+ }
+ } catch (error) {
+ D.error(
+ `Fail to update state '${this.handler.name}'.`,
`${error}`,
);
this.setValue(undefined);
@@ -276,7 +293,8 @@ export function useSyncState<A>(
const st = lookupSyncState(state);
Server.useSignal(st.signal(), st.fetch);
st.online();
- return useGlobalState(st);
+ const [v] = useGlobalState(st);
+ return [v, st.update];
}
/** Synchronization with a (projectified) server value. */
diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx
index 42501b3e8f700935a47e0029efe1655488504167..8cf3fe1e9c6190168c3419d781fd9c033cf2470e 100644
--- a/ivette/src/renderer/Application.tsx
+++ b/ivette/src/renderer/Application.tsx
@@ -83,7 +83,7 @@ export default function Application(): JSX.Element {
settings="frama-c.labview"
/>
</LSplit>
- <Toolbar.ToolBar>
+ <Toolbar.ToolBar className="statusbar">
<Controller.Status />
<>{StatusBar}</>
<Toolbar.Filler />
diff --git a/ivette/src/renderer/Sidebar.tsx b/ivette/src/renderer/Sidebar.tsx
index 8ac673ab020f27eef06be8137f4a7f58ea9823a6..1e5a41d4b5d0e2af0965795308e646dfbe642071 100644
--- a/ivette/src/renderer/Sidebar.tsx
+++ b/ivette/src/renderer/Sidebar.tsx
@@ -73,6 +73,7 @@ function Wrapper(props: WrapperProps): JSX.Element {
return (
<SideBar className={className}>
+ <div className="sidebar-ruler"/>
<Catch label={props.id}>
{props.children}
</Catch>
@@ -121,7 +122,7 @@ export function Panel(): JSX.Element {
);
return (
- <div className="sidebar-ruler">
+ <div className="sidebar-view">
<div className={selectorClasses}>
{items}
</div>
diff --git a/ivette/src/renderer/style.css b/ivette/src/renderer/style.css
index b65e65bdfe1e361742681f4f44ed56452b703f1d..1fc9fc6ef8ef7a843480238b892c2407be800b9c 100644
--- a/ivette/src/renderer/style.css
+++ b/ivette/src/renderer/style.css
@@ -2,20 +2,25 @@
/* --- Main Frame --- */
/* -------------------------------------------------------------------------- */
-.sidebar-ruler {
+.sidebar-view {
display: flex;
height: 100%;
overflow-x: hidden;
overflow-y: auto;
}
+.sidebar-ruler {
+ width: 120px;
+ height: 0px;
+}
+
.sidebar-items.dome-color-frame
{
background: var(--background-intense) ;
}
.sidebar-selector {
- min-width: 35px;
+ min-width: 35px;
text-align: center;
}
@@ -52,6 +57,10 @@
font-size: smaller;
}
+.statusbar {
+ height: 26px;
+}
+
/* -------------------------------------------------------------------------- */
/* --- Styling LabViews --- */
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/sandbox/icons.tsx b/ivette/src/sandbox/icons.tsx
index 1c8f3b23a45723dceb647fad90602e909f27e067..9cf1b1153066f79a45469a020841d4ac6fd3f72c 100644
--- a/ivette/src/sandbox/icons.tsx
+++ b/ivette/src/sandbox/icons.tsx
@@ -52,7 +52,7 @@ function Gallery(): JSX.Element {
gallery.forEach((icons, section) => {
sections.push(
<Section key={section} defaultUnfold label={section}>
- <Grid columns="auto auto">{icons}</Grid>
+ <Grid style={{ paddingLeft: 24 }} columns="auto auto">{icons}</Grid>
</Section>
);
});
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index bdaa0d0c3158856866febda02f142ddcd1b5b644..c3229cdde4a054cfb8912468b514f1538d0ea104 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -593,6 +593,7 @@ sig
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val find : key -> 'a t -> 'a
+ val remove : key -> 'a t -> 'a t
end
module type Index =
@@ -601,6 +602,7 @@ sig
type tag
val get : t -> tag
val find : tag -> t
+ val remove : t -> unit
val clear : unit -> unit
end
@@ -611,6 +613,7 @@ sig
val clear : index -> unit
val get : index -> M.key -> int
val find : index -> int -> M.key
+ val remove : index -> M.key -> unit
val to_json : index -> M.key -> json
val of_json : index -> json -> M.key
end =
@@ -643,6 +646,13 @@ struct
m.index <- M.add a id m.index ;
Hashtbl.add m.lookup id a ; id
+ let remove m a =
+ try
+ let id = M.find a m.index in
+ Hashtbl.remove m.lookup id ;
+ m.index <- M.remove a m.index ;
+ with Not_found -> ()
+
let find m id = Hashtbl.find m.lookup id
let to_json m a = `Int (get m a)
@@ -662,6 +672,7 @@ struct
let clear () = INDEX.clear index
let get = INDEX.get index
let find = INDEX.find index
+ let remove = INDEX.remove index
include
(struct
type t = M.key
@@ -694,6 +705,7 @@ struct
let index () = STATE.get ()
let clear () = INDEX.clear (index())
+ let remove a = INDEX.remove (index()) a
let get a = INDEX.get (index()) a
let find id = INDEX.find (index()) id
@@ -761,6 +773,11 @@ struct
let hash = lookup () in
if not (Hashtbl.mem hash tag) then Hashtbl.add hash tag x ; tag
+ let remove x =
+ let tag = A.id x in
+ let hash = lookup () in
+ Hashtbl.remove hash tag
+
include
(struct
type t = A.t
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index c9fe14a36a55800db6d21a507ce99a6cf9d3d637..36a02e94a652e4255a27648b4034323a1bc0dd55 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -357,6 +357,7 @@ sig
val empty : 'a t
val add : key -> 'a -> 'a t -> 'a t
val find : key -> 'a t -> 'a
+ val remove : key -> 'a t -> 'a t
end
(** Datatype extended with access to value identifiers. *)
@@ -368,6 +369,9 @@ sig
val find : tag -> t
(** @raise Not_found if not registered. *)
+ val remove : t -> unit
+ (** Remove item from index tables. Use with extreme care. *)
+
val clear : unit -> unit
(** Clear index tables. Use with extreme care. *)
end
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 9363447b71ea9d618e8682575207ebef3f9af3f1..8e5c71255249e55f85e0ba1f708a8c1d572ffd68 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -381,10 +381,19 @@ let in_range ~min:a ~max:b v = min (max a v) b
let kill () = raise Killed
+let rooters = ref []
let daemons = ref []
+let once callback = rooters := !rooters @ [ callback ]
let on callback = daemons := !daemons @ [ callback ]
let set_active activity =
- List.iter (fun f -> try f activity with _ -> ()) !daemons
+ begin
+ if activity then
+ begin
+ List.iter (fun f -> try f () with _ -> ()) !rooters ;
+ rooters := [] ;
+ end ;
+ List.iter (fun f -> try f activity with _ -> ()) !daemons ;
+ end
let create ~pretty ?(equal=(=)) ~fetch () =
let polling = in_range ~min:1 ~max:200 (Senv.Polling.get ()) in
diff --git a/src/plugins/server/main.mli b/src/plugins/server/main.mli
index 9215a456db54f9aa3020f2401f945b964f1e678e..94bf6707567fe04c70e9e3b174887e2658b45161 100644
--- a/src/plugins/server/main.mli
+++ b/src/plugins/server/main.mli
@@ -141,6 +141,12 @@ val on_signal : signal -> (bool -> unit) -> unit
Callbacks shall {i never} raise any exception. *)
val on : (bool -> unit) -> unit
+(** Register a callback to listen for server initialization. All callbacks are
+ executed once, in their order of registration, and before activity
+ callbacks.
+ Callbacks shall {i never} raise any exception. *)
+val once : (unit -> unit) -> unit
+
(** Register an asynchronous task on the server.
When the server is not working in background, this is
equivalent to [Task.call] ; otherwize,
diff --git a/src/plugins/server/states.ml b/src/plugins/server/states.ml
index 9d9ccc7357709b48a4965bb547839e161cb26e12..b7cfc0b2018bffb1107cbd114cdff273cf5dd714 100644
--- a/src/plugins/server/states.ml
+++ b/src/plugins/server/states.ml
@@ -192,6 +192,7 @@ type 'a array = {
key : 'a -> string ;
iter : ('a -> unit) -> unit ;
getter : (string * ('a -> json option)) list ;
+ preload : ('a -> unit) option ;
(* [LC+JS]
The two following fields allow to keep an array in sync
with the current project and still have a polymorphic data type. *)
@@ -267,13 +268,14 @@ type buffer = {
mutable updated : json list ;
}
-let add_entry buffer cols fkey key v =
+let add_entry array buffer key v =
+ Option.iter (fun f -> f v) array.preload ;
let fjs = List.fold_left (fun fjs (fd,to_json) ->
match to_json v with
| Some js -> (fd , js) :: fjs
| None | exception Not_found -> fjs
- ) [] cols in
- let row = (fkey, `String key) :: fjs in
+ ) [] array.getter in
+ let row = (array.fkey, `String key) :: fjs in
buffer.updated <- `Assoc row :: buffer.updated ;
buffer.capacity <- pred buffer.capacity
@@ -281,9 +283,9 @@ let remove_entry buffer key =
buffer.removed <- key :: buffer.removed ;
buffer.capacity <- pred buffer.capacity
-let update_entry buffer cols fkey key = function
+let update_entry array buffer key = function
| Remove -> remove_entry buffer key
- | Add v -> add_entry buffer cols fkey key v
+ | Add v -> add_entry array buffer key v
let fetch array n =
let m = content array in
@@ -303,7 +305,7 @@ let fetch array n =
begin fun v ->
let key = array.key v in
if buffer.capacity > 0 then
- add_entry buffer array.getter array.fkey key v
+ add_entry array buffer key v
else
( m.updates <- Kmap.add key (Add v) m.updates ;
buffer.pending <- succ buffer.pending ) ;
@@ -313,7 +315,7 @@ let fetch array n =
m.updates <- Kmap.filter
begin fun key upd ->
if buffer.capacity > 0 then
- ( update_entry buffer array.getter array.fkey key upd ; false )
+ ( update_entry array buffer key upd ; false )
else
( buffer.pending <- succ buffer.pending ; true )
end m.updates ;
@@ -334,6 +336,7 @@ let register_array ~package ~name ~descr ~key
?(keyName="key")
?(keyType=Package.Jkey name)
~(iter : 'a callback)
+ ?(preload : ('a -> unit) option)
?(add_update_hook : 'a callback option)
?(add_remove_hook : 'a callback option)
?(add_reload_hook : unit callback option)
@@ -375,7 +378,7 @@ let register_array ~package ~name ~descr ~key
let getter =
List.map Package.(fun (fd,to_js) -> fd.fd_name , to_js) !model in
let array = {
- fkey = keyName ; key ; iter ; getter ; signal ;
+ fkey = keyName ; key ; iter ; preload ; getter ; signal ;
current = None ; projects = Hashtbl.create 0
} in
let signature = Request.signature ~input:(module Jint) () in
diff --git a/src/plugins/server/states.mli b/src/plugins/server/states.mli
index ff52812c698287bced7066dda914765051118b63..1d73e64cf1e57c3026063b50eed84d716251f3eb 100644
--- a/src/plugins/server/states.mli
+++ b/src/plugins/server/states.mli
@@ -161,6 +161,10 @@ val signal : 'a array -> Request.signal
Columns added to the model after registration are {i not} taken into
account.
+ The optional [~preload] function will be called just before
+ every column getters. Notice that column getters are called in
+ registration order.
+
If provided, the [~add_xxx_hook] options are used to register hooks
to notify the server of corresponding array updates.
Each hook will be installed only once the client starts to listen for array
@@ -177,6 +181,7 @@ val register_array :
?keyName:string ->
?keyType:jtype ->
iter:('a callback) ->
+ ?preload:('a -> unit) ->
?add_update_hook:('a callback) ->
?add_remove_hook:('a callback) ->
?add_reload_hook:(unit callback) ->
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 3ee82fe8b4aea89b7d1ec7a6d6de393a42d5f709..090482b711c92fca8f90279b30762822e69779d1 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -37,7 +37,8 @@ let get_miss () = !miss
let get_removed () = !removed
let mark_cache ~mode hash =
- if mode = Cleanup || Fc_config.is_gui then Hashtbl.replace cleanup hash ()
+ if mode = Cleanup || Wp_parameters.is_interactive () then
+ Hashtbl.replace cleanup hash ()
module CACHEDIR = WpContext.StaticGenerator(Datatype.Unit)
(struct
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index 7bb611619a4158a1763e98c00dbf3b052746d62b..f2b8583fdf6e9359e7084c203252befb03b22c62 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -27,9 +27,10 @@
type node = {
tree : Wpo.t ; (* root, to check consistency *)
goal : Wpo.t ; (* only GoalAnnot of a sequent *)
+ child : string option ; (* child name from parent node *)
parent : node option ;
mutable script : script ;
- mutable stats : Stats.stats ;
+ mutable stats : Stats.stats option ; (* memoized *)
mutable strategy : string option ; (* hint *)
mutable search_index : int ;
mutable search_space : Strategy.t array ; (* sorted by priority *)
@@ -53,6 +54,7 @@ type tree = {
main : Wpo.t ; (* Main goal to be proved. *)
mutable pool : Lang.F.pool option ; (* Global pool variable *)
mutable saved : bool ; (* Saved on Disk. *)
+ mutable dirty : bool ; (* Tactical result is outdated *)
mutable gid : int ; (* WPO goal numbering *)
mutable head : node option ; (* the current node *)
mutable root : node option ; (* the root node *)
@@ -70,24 +72,76 @@ module PROOFS = WpContext.StaticGenerator(Wpo.S)
pool = None ;
head = None ;
root = None ;
+ dirty = true ;
saved = false ;
}
end)
-let () = Wpo.add_removed_hook PROOFS.remove
-let () = Wpo.add_cleared_hook PROOFS.clear
+module NODES = WpContext.Static
+ (struct
+ type key = Wpo.t
+ type data = node
+ let name = "Wp.ProofEngine.Nodes"
+ let compare = Wpo.S.compare
+ let pretty = Wpo.S.pretty
+ end)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Signaling --- *)
+(* -------------------------------------------------------------------------- *)
+
+let goal_hooks = ref []
+let clear_hooks = ref []
+let remove_hooks = ref []
+let update_hooks = ref []
+
+let add_goal_hook fn = goal_hooks := !goal_hooks @ [fn]
+let add_clear_hook fn = clear_hooks := !clear_hooks @ [fn]
+let add_remove_hook fn = remove_hooks := !remove_hooks @ [fn]
+let add_update_hook fn = update_hooks := !update_hooks @ [fn]
+
+let signal_goal g = List.iter (fun fn -> fn g) !goal_hooks
+let signal_node n = List.iter (fun fn -> fn n) !update_hooks
+
+let dirty_root g =
+ try
+ let tree = PROOFS.find g in
+ if not tree.dirty then
+ begin
+ tree.dirty <- true ;
+ signal_goal g ;
+ end
+ with Not_found -> ()
+
+let rec dirty_node n =
+ match n.stats with
+ | None -> ()
+ | Some _ ->
+ n.stats <- None ;
+ signal_node n ;
+ match n.parent with
+ | Some p -> dirty_node p
+ | None -> dirty_root n.tree
+
+let self_updating = ref false
+
+let dirty_goal g =
+ if not !self_updating then
+ match NODES.get g with
+ | Some n -> dirty_node n
+ | None -> dirty_root g
let get wpo =
try
- let proof = PROOFS.get wpo in
+ let proof = PROOFS.find wpo in
match proof.root with
| None | Some { script = Opened | Script _ } -> raise Not_found
| Some { script = Tactic _ } -> if proof.saved then `Saved else `Proof
with Not_found ->
if ProofSession.exists wpo then `Script else `None
-let iter_all f ns = List.iter (fun (_,n) -> f n) ns
-let map_all f ns = List.map (fun (k,n) -> k,f n) ns
+let iter_children f ns = List.iter (fun m -> f (snd m)) ns
+let map_children f ns = List.map (fun m -> fst m,f m) ns
let pool tree =
match tree.pool with
@@ -98,47 +152,99 @@ let pool tree =
tree.pool <- Some pool ; pool
(* -------------------------------------------------------------------------- *)
-(* --- Constructors --- *)
+(* --- Proofs --- *)
(* -------------------------------------------------------------------------- *)
let proof ~main =
assert (not (Wpo.is_tactic main)) ;
PROOFS.get main
-let rec reset_node n =
- Wpo.clear_results n.goal ;
- if Wpo.is_tactic n.goal then Wpo.remove n.goal ;
+let saved t = t.saved
+let set_saved t s = t.saved <- s ; signal_goal t.main
+
+(* -------------------------------------------------------------------------- *)
+(* --- Removal --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rec revert_tactic t n =
n.strategy <- None ;
match n.script with
| Opened | Script _ -> ()
| Tactic(_,children) ->
- n.script <- Opened ; iter_all reset_node children
-
-let reset_root = function None -> () | Some n -> reset_node n
-
-let reset t =
+ t.saved <- false ;
+ n.script <- Opened ;
+ iter_children (remove_node t) children
+
+and remove_node t n =
+ NODES.remove n.goal ;
+ if Wpo.is_tactic n.goal then
+ Wpo.remove n.goal
+ else
+ Wpo.clear_results n.goal ;
+ List.iter (fun f -> f n) !remove_hooks ;
+ Option.iter (fun n0 -> if n0 == n then t.head <- None) t.head ;
+ revert_tactic t n
+
+let clear_tree t =
begin
- Wpo.clear_results t.main ;
- reset_root t.root ;
+ Option.iter (remove_node t) t.root ;
t.gid <- 0 ;
t.head <- None ;
t.root <- None ;
t.saved <- false ;
+ List.iter (fun fn -> fn t.main) !clear_hooks ;
+ signal_goal t.main ;
end
-let clear w = if PROOFS.mem w then reset (PROOFS.get w)
+let clear_node_tactic t n =
+ revert_tactic t n ; dirty_node n ;
+ if t.head = None then t.head <- Some n
-let saved t = t.saved
-let set_saved t s = t.saved <- s
+let clear_parent_tactic t n =
+ match n.parent with
+ | None -> clear_tree t
+ | Some p as h -> revert_tactic t p ; dirty_node p ; t.head <- h
+
+let clear_node t n =
+ Wpo.clear_results n.goal ;
+ clear_node_tactic t n
+
+let clear_goal w =
+ try clear_tree (PROOFS.find w)
+ with Not_found -> Wpo.clear_results w
+
+(* -------------------------------------------------------------------------- *)
+(* --- Removal From Wpo --- *)
+(* -------------------------------------------------------------------------- *)
+
+let removed_from_wpo g =
+ if not @@ Wpo.is_tactic g then
+ begin
+ try
+ clear_tree (PROOFS.find g) ;
+ PROOFS.remove g ;
+ with Not_found ->
+ signal_goal g
+ end
+
+let cleared_from_wpo () =
+ begin
+ NODES.clear () ;
+ PROOFS.clear () ;
+ end
+
+let () = Wpo.add_removed_hook removed_from_wpo
+let () = Wpo.add_cleared_hook cleared_from_wpo
+let () = Wpo.add_modified_hook dirty_goal
(* -------------------------------------------------------------------------- *)
(* --- Walking --- *)
(* -------------------------------------------------------------------------- *)
let rec walk f node =
- if not (Wpo.is_valid node.goal) then
+ if not (Wpo.is_locally_valid node.goal) then
match node.script with
- | Tactic (_,children) -> iter_all (walk f) children
+ | Tactic (_,children) -> iter_children (walk f) children
| Opened | Script _ -> f node
let iteri f tree =
@@ -157,50 +263,79 @@ let rec depth node =
(* --- Consolidating --- *)
(* -------------------------------------------------------------------------- *)
-let proved n = Wpo.is_valid n.goal
-
let pending n =
let k = ref 0 in
walk (fun _ -> incr k) n ; !k
-let is_prover_result (p,_) = p <> VCS.Tactical
+let locally_proved n = Wpo.is_locally_valid n.goal
+
+let fully_proved n =
+ let exception HasPending in
+ try walk (fun _ -> raise HasPending) n ; true
+ with HasPending -> false
+
+let is_prover (p,_) = VCS.is_prover p
let prover_stats ~smoke goal =
Stats.results ~smoke @@
- List.filter is_prover_result @@
+ List.filter is_prover @@
Wpo.get_results goal
let rec consolidate ~smoke n =
- let s =
- if Wpo.is_valid n.goal then
- prover_stats ~smoke n.goal
- else
- match n.script with
- | Opened | Script _ -> prover_stats ~smoke n.goal
- | Tactic(_,children) ->
- let qed = Wpo.qed_time n.goal in
- let results = List.map (fun (_,n) -> consolidate ~smoke n) children in
- Stats.tactical ~qed results
- in n.stats <- s ; s
-
-let validate tree =
+ match n.stats with
+ | Some s -> s
+ | None -> let s = compute ~smoke n in n.stats <- Some s ; s
+
+and compute ~smoke n =
+ if Wpo.is_locally_valid n.goal then
+ prover_stats ~smoke n.goal
+ else
+ match n.script with
+ | Opened | Script _ -> prover_stats ~smoke n.goal
+ | Tactic(_,children) ->
+ Stats.tactical ~qed:(Wpo.qed_time n.goal) @@
+ List.map (fun (_,n) -> consolidate ~smoke n) children
+
+let tactical tree =
match tree.root with
- | None -> ()
+ | None -> VCS.no_result
| Some root ->
- let main = tree.main in
- if not (Wpo.is_valid main) then
- let stats = consolidate ~smoke:(Wpo.is_smoke_test main) root in
- Wpo.set_result tree.main Tactical (Stats.script stats)
+ let smoke = Wpo.is_smoke_test tree.main in
+ Stats.script @@ consolidate ~smoke root
+
+let validate tree =
+ if tree.dirty then
+ let result =
+ if Wpo.is_locally_valid tree.main then VCS.no_result else tactical tree
+ in
+ try
+ self_updating := true ;
+ Wpo.set_result tree.main VCS.Tactical result ;
+ tree.dirty <- false ;
+ self_updating := false ;
+ with exn ->
+ self_updating := false ;
+ raise exn
let consolidated wpo =
let smoke = Wpo.is_smoke_test wpo in
try
- if smoke || not (PROOFS.mem wpo) then raise Not_found ;
- match PROOFS.get wpo with
- | { root = Some { stats ; script = Tactic _ } } -> stats
+ match (PROOFS.find wpo).root with
+ | Some node -> consolidate ~smoke node
| _ -> raise Not_found
with Not_found -> prover_stats ~smoke wpo
+let consolidate wpo =
+ try validate (PROOFS.find wpo) with Not_found -> ()
+
+let results wpo = consolidate wpo ; Wpo.get_results wpo
+
+let stats node =
+ match node.stats with Some s -> s | None ->
+ let smoke = Wpo.is_smoke_test node.tree in
+ let s = compute ~smoke node in
+ node.stats <- Some s ; s
+
(* -------------------------------------------------------------------------- *)
(* --- Accessors --- *)
(* -------------------------------------------------------------------------- *)
@@ -213,23 +348,42 @@ let head_goal t = match t.head with
let tree n = proof ~main:n.tree
let goal n = n.goal
-let stats n = n.stats
let tree_context t = Wpo.get_context t.main
let node_context n = Wpo.get_context n.goal
let parent n = n.parent
let title n = n.goal.Wpo.po_name
+
let tactical n =
match n.script with
| Tactic(tactic,_) -> Some tactic
| Opened | Script _ -> None
+
let get_strategies n = n.search_index , n.search_space
let set_strategies n ?(index=0) hs =
- n.search_index <- index ; n.search_space <- hs
+ n.search_index <- index ; n.search_space <- hs ; signal_node n
+
let children n =
match n.script with
| Tactic(_,children) -> children
| Opened | Script _ -> []
+let subgoals n = List.map snd @@ children n
+
+let rec path n = match n.parent with
+ | None -> []
+ | Some p -> p::path p
+
+let child_label n = n.child
+
+let tactic_label n =
+ match n.script with Tactic({ header }, _) -> Some header | _ -> None
+
+let tactic n =
+ match n.script with
+ | Tactic({ tactic }, _) ->
+ begin try Some (Tactical.lookup ~id:tactic) with Not_found -> None end
+ | _ -> None
+
(* -------------------------------------------------------------------------- *)
(* --- State & Status --- *)
(* -------------------------------------------------------------------------- *)
@@ -246,7 +400,7 @@ type status = [
let status t : status =
match t.root with
| None ->
- if Wpo.is_valid t.main
+ if Wpo.is_locally_valid t.main
then if Wpo.is_smoke_test t.main then `Invalid else `Proved
else if Wpo.is_smoke_test t.main then `Passed else `Unproved
| Some root ->
@@ -255,6 +409,9 @@ let status t : status =
if Wpo.is_smoke_test t.main then `Passed else `Unproved
| Tactic _ ->
let n = pending root in
+ if n = 0 then
+ if Wpo.is_smoke_test t.main then `Invalid else `Proved
+ else
if Wpo.is_smoke_test t.main then `StillResist n else `Pending n
(* -------------------------------------------------------------------------- *)
@@ -273,41 +430,38 @@ let current t : current =
type position = [ `Main | `Node of node | `Leaf of int ]
let goto t = function
| `Main ->
- t.head <- t.root
+ t.head <- t.root ; signal_goal t.main
| `Node n ->
- if n.tree == t.main then t.head <- Some n
+ if n.tree == t.main then t.head <- Some n ; signal_goal t.main
| `Leaf k ->
t.head <- t.root ;
- iteri (fun i n -> if i = k then t.head <- Some n) t
+ iteri (fun i n -> if i = k then t.head <- Some n) t ;
+ signal_goal t.main
let fetch t node =
try
t.head <- t.root ;
- walk (fun n -> t.head <- Some n ; raise Exit) node ; false
+ walk (fun n -> t.head <- Some n ; raise Exit) node ;
+ false
with Exit -> true
let rec forward t =
match t.head with
- | None -> t.head <- t.root
+ | None -> t.head <- t.root ; signal_goal t.main
| Some hd ->
- if not (fetch t hd) then
- begin
- t.head <- hd.parent ;
- forward t ;
- end
+ if not (fetch t hd)
+ then ( t.head <- hd.parent ; forward t )
+ else signal_goal t.main
-let remove t node =
- begin
- Wpo.clear_results node.goal ;
- t.head <- node.parent ;
- if t.head = None then t.root <- None ;
- reset_node node ;
- end
+let cancel_parent_tactic t =
+ match t.head with
+ | None -> ()
+ | Some n -> clear_parent_tactic t n
-let cancel t =
+let cancel_current_node t =
match t.head with
| None -> ()
- | Some node -> remove t node
+ | Some node -> clear_node t node
(* -------------------------------------------------------------------------- *)
(* --- Sub-Goal --- *)
@@ -330,29 +484,19 @@ let mk_goal t ~title ~part ~axioms sequent =
po_formula = mk_formula ~main:t.main.po_formula axioms sequent ;
})
-let mk_tree_node ~tree ~anchor goal = {
- tree = tree.main ; goal ;
- parent = Some anchor ;
- script = Opened ;
- stats = Stats.empty ;
- search_index = 0 ;
- search_space = [| |] ;
- strategy = None ;
-}
-
-let mk_root_node goal = {
- tree = goal ; goal ;
- parent = None ;
- script = Opened ;
- stats = Stats.empty ;
- strategy = None ;
- search_index = 0 ;
- search_space = [| |] ;
-}
+let mk_node ~main ?parent ?child goal =
+ let node = {
+ tree=main ; parent ; child ; goal ;
+ script = Opened ;
+ stats = None ;
+ search_index = 0 ;
+ search_space = [| |] ;
+ strategy = None ;
+ } in NODES.define goal node ; node
let mk_root ~tree =
- let goal = tree.main in
- let node = mk_root_node goal in
+ let main = tree.main in
+ let node = mk_node ~main main in
let root = Some node in
tree.root <- root ;
tree.head <- root ;
@@ -385,7 +529,7 @@ struct
(fun (part,s) -> part , mk_goal tree ~title ~part ~axioms s) dseqs
in { tree ; tactic ; anchor ; goals }
- let iter f w = iter_all f w.goals
+ let iter f w = iter_children f w.goals
let header frk = frk.tactic.ProofScript.header
end
@@ -411,35 +555,37 @@ let anchor tree ?node () =
let commit fork =
List.iter (fun (_,wp) -> ignore (Wpo.resolve wp)) fork.Fork.goals ;
let tree = fork.Fork.tree in
- let anchor = fork.Fork.anchor in
- let children = map_all (mk_tree_node ~tree ~anchor) fork.Fork.goals in
+ let parent = fork.Fork.anchor in
+ let subnode (child,goal) = mk_node ~main:tree.main ~parent ~child goal in
+ let children = map_children subnode fork.Fork.goals in
tree.saved <- false ;
- anchor.script <- Tactic( fork.Fork.tactic , children ) ;
- anchor , children
+ parent.script <- Tactic( fork.Fork.tactic , children ) ;
+ dirty_node parent ;
+ parent , children
(* -------------------------------------------------------------------------- *)
(* --- Scripting --- *)
(* -------------------------------------------------------------------------- *)
-let results wpo =
- List.map (fun (p,r) -> ProofScript.a_prover p r) (Wpo.get_results wpo)
+let script_provers wpo =
+ List.map (fun (p,r) -> ProofScript.a_prover p r) @@
+ Wpo.get_prover_results wpo
let rec script_node (node : node) =
- let provers = results node.goal in
- let scripts =
+ script_provers node.goal @
+ begin
match node.script with
| Script s -> List.filter ProofScript.is_tactic s
| Tactic( tactic , children ) ->
[ ProofScript.a_tactic tactic (List.map subscript_node children) ]
| Opened -> []
- in
- provers @ scripts
+ end
and subscript_node (key,node) = key , script_node node
let script tree =
match tree.root with
- | None -> results tree.main
+ | None -> script_provers tree.main
| Some node -> script_node node
let bind node script =
@@ -449,14 +595,39 @@ let bind node script =
()
| Opened | Script _ ->
(*TODO: saveback the previous script *)
- node.script <- Script script
+ node.script <- Script script ;
+ signal_node node ;
+ signal_goal node.tree
let bound node =
match node.script with
| Tactic _ | Opened -> []
| Script s -> s
+let is_script_result ~margin (prv,res) =
+ VCS.is_extern prv && VCS.is_valid res &&
+ res.prover_time > margin
+
+let has_result tree =
+ let margin = float_of_string @@ Wp_parameters.TimeMargin.get () in
+ let results = Wpo.get_results tree.main in
+ List.exists (is_script_result ~margin) results
+
+let has_tactics tree =
+ match tree.root with
+ | None -> false
+ | Some node ->
+ match node.script with
+ | Opened -> false
+ | Tactic _ -> true
+ | Script s -> List.exists ProofScript.is_tactic s
+
+let has_script tree = has_tactics tree || has_result tree
+let has_proof wpo =
+ try has_script @@ PROOFS.find wpo
+ with Not_found -> false
+
let get_hint node = node.strategy
-let set_hint node strategy = node.strategy <- Some strategy
+let set_hint node strategy = node.strategy <- Some strategy ; signal_node node
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 5fdb346c81be8070ef5fb335450a5a36d9c04788..8e10e532600d53355127561f064e6d0f7458f19d 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -41,15 +41,19 @@ end
val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
val proof : main:Wpo.t -> tree
-val reset : tree -> unit
-val clear : Wpo.t -> unit
-(** Re-compute stats & set status of the entire script *)
+(** Consolidate and update status of the entire script (memoized). *)
val validate : tree -> unit
-(** Consolidate statistics wrt current script or prover results *)
+(** Consolidate proof tree (memoized). *)
+val consolidate : Wpo.t -> unit
+
+(** Consolidated statistics (memoized). *)
val consolidated : Wpo.t -> Stats.stats
+(** Consolidated results (memoized). *)
+val results : Wpo.t -> (VCS.prover * VCS.result) list
+
(** Leaves are numbered from 0 to n-1 *)
type status = [
@@ -80,11 +84,17 @@ val tree_context : tree -> WpContext.t
val node_context : node -> WpContext.t
val title : node -> string
-val proved : node -> bool
+val fully_proved : node -> bool
+val locally_proved : node -> bool
val pending : node -> int
val stats : node -> Stats.stats
-val parent : node -> node option
val depth : node -> int
+val path : node -> node list
+val parent : node -> node option
+val tactic : node -> Tactical.t option
+val child_label : node -> string option
+val tactic_label : node -> string option
+val subgoals : node -> node list
val children : node -> (string * node) list
val tactical : node -> ProofScript.jtactic option
val get_strategies : node -> int * Strategy.t array (* current index *)
@@ -93,8 +103,19 @@ val get_hint : node -> string option
val set_hint : node -> string -> unit
val forward : tree -> unit
-val cancel : tree -> unit
-val remove : tree -> node -> unit
+val clear_goal : Wpo.t -> unit
+val clear_tree : tree -> unit
+val clear_node : tree -> node -> unit
+val clear_node_tactic : tree -> node -> unit
+val clear_parent_tactic : tree -> node -> unit
+
+val add_goal_hook : (Wpo.t -> unit) -> unit
+val add_clear_hook : (Wpo.t -> unit) -> unit
+val add_remove_hook : (node -> unit) -> unit
+val add_update_hook : (node -> unit) -> unit
+
+val cancel_parent_tactic : tree -> unit
+val cancel_current_node : tree -> unit
type fork
val anchor : tree -> ?node:node -> unit -> node
@@ -103,6 +124,8 @@ val iter : (Wpo.t -> unit) -> fork -> unit
val commit : fork -> node * (string * node) list
val pretty : Format.formatter -> fork -> unit
+val has_proof : Wpo.t -> bool
+val has_script : tree -> bool
val script : tree -> ProofScript.jscript
val bind : node -> ProofScript.jscript -> unit
val bound : node -> ProofScript.jscript
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 5d9686beb84f92aa96946e05e5da760662cb2c03..7f4a4c06386f9693d09b5ff0b2796cb3b10111aa 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -449,9 +449,9 @@ let apply env node jtactic subscripts =
| Some fork ->
let _,children = ProofEngine.commit fork in
reconcile children subscripts ; (*TODO: saveback forgiven script ? *)
- let ok = List.for_all
- (fun (_,node) -> ProofEngine.proved node)
- children in
+ let ok =
+ List.for_all
+ (fun (_,node) -> ProofEngine.locally_proved node) children in
if ok then [] else children
(* -------------------------------------------------------------------------- *)
@@ -524,7 +524,7 @@ let rec process env node =
schedule
begin fun () ->
Wp_parameters.debug ~dkey:dkey_pp_allgoals "%a" (pp_subgoal env) node ;
- if ProofEngine.proved node then
+ if ProofEngine.locally_proved node then
begin
env.pending <- pred env.pending ;
Env.validate env ;
diff --git a/src/plugins/wp/ProverTask.mli b/src/plugins/wp/ProverTask.mli
index 8ff7feaf7f467e47cdd23960747b4610aab0111c..e617e446ed679722af845fa55773beef1ce6dbe9 100644
--- a/src/plugins/wp/ProverTask.mli
+++ b/src/plugins/wp/ProverTask.mli
@@ -86,6 +86,7 @@ class virtual command : string ->
end
+(** If provided, the number of procs is forwarded to the Why3 and the server *)
val server : ?procs:int -> unit -> Task.server
val schedule : 'a Task.task -> unit
diff --git a/src/plugins/wp/TacArray.ml b/src/plugins/wp/TacArray.ml
index bab1eb2dfbb2197d5685eaf44330010237a0ac63..ab01c284899fb4ac682129923a27292fb3450032 100644
--- a/src/plugins/wp/TacArray.ml
+++ b/src/plugins/wp/TacArray.ml
@@ -42,7 +42,7 @@ class array =
object
inherit Tactical.make ~id:"Wp.array"
~title:"Array"
- ~descr:"Decompose array access-update patterns"
+ ~descr:"Decompose access-update patterns"
~params:[]
method select feedback (s : Tactical.selection) =
diff --git a/src/plugins/wp/TacBitrange.ml b/src/plugins/wp/TacBitrange.ml
index 4d8ec46291f09168e0420b8b0db364fe6135bc01..4bd424657a8e8169b14172cbe4d82029432b5676 100644
--- a/src/plugins/wp/TacBitrange.ml
+++ b/src/plugins/wp/TacBitrange.ml
@@ -205,14 +205,14 @@ open Tactical
let positive_land =
Tactical.checkbox
~id:"positive-land"
- ~title:"Force positive logical-and"
+ ~title:"Pos."
~descr:"Requires to obtain a result from (at least one) positive operands"
~default:true ()
let positive_lor =
Tactical.checkbox
~id:"positive-lor"
- ~title:"Force negative logical-or"
+ ~title:"Neg."
~descr:"Restrict to obtain a positive result from (all) positive operands"
~default:true ()
@@ -221,7 +221,7 @@ class bitrange =
inherit Tactical.make
~id:"Wp.bitrange"
~title:"Bit Range"
- ~descr:"Bounds of Bitwise Operators"
+ ~descr:"Compute bounds of bitwise operators."
~params:[snd positive_land;snd positive_lor]
method select feedback = function
@@ -283,7 +283,7 @@ class autobitrange =
method id = "wp:bitrange"
method title = "Auto Bit-Range"
- method descr = "Apply Bit-Range on comparison with bitwised operations"
+ method descr = "Compute bounds of bitwise operations."
method search push (seq : Conditions.sequent) =
let goal = snd seq in
diff --git a/src/plugins/wp/TacBittest.ml b/src/plugins/wp/TacBittest.ml
index 3921f2ed49516856267ece33fbc2c46d5741f147..f71958c8110f001a45da83d5a739dabff94238a1 100644
--- a/src/plugins/wp/TacBittest.ml
+++ b/src/plugins/wp/TacBittest.ml
@@ -55,7 +55,7 @@ class bittestrange =
inherit Tactical.make
~id:"Wp.bittestrange"
~title:"Bit-Test Range"
- ~descr:"Tighten Bounds with respect to bits"
+ ~descr:"Compute bounds with respect to bits."
~params:[]
method select _feedback selection =
@@ -106,7 +106,7 @@ class autobittestrange : Strategy.heuristic =
method id = "wp:bittestrange"
method title = "Auto Bit-Test Range"
- method descr = "Apply Bit-Test Range on bit-tests"
+ method descr = "Apply bitwise tactics on bit-tests expressions."
method search push (seq : Conditions.sequent) =
Conditions.iter
diff --git a/src/plugins/wp/TacBitwised.ml b/src/plugins/wp/TacBitwised.ml
index f9a56c88cb3831f156ac10f9919a2882af1ccbc3..80ccfb200cc3a6f3f2a406e9330bd0db04827109 100644
--- a/src/plugins/wp/TacBitwised.ml
+++ b/src/plugins/wp/TacBitwised.ml
@@ -43,14 +43,14 @@ let rewrite descr u v = Tactical.rewrite [ descr , F.p_true , u , v ]
let vrange,prange = Tactical.spinner ~id:"Wp.bitwised.range"
~vmin:0 ~vmax:64 ~default:32
- ~title:"Bits" ~descr:"Number of bits for bitwise equality" ()
+ ~title:"Bits" ~descr:"Size of bitwise equality." ()
class bitcase =
object(self)
inherit Tactical.make
~id:"Wp.bitwised"
~title:"Bitwise Eq."
- ~descr:"Decompose Bitwise Equality"
+ ~descr:"Decompose bitwise equality."
~params:[prange]
(* range:(0 <= a < 2^n && 0 <= b < 2^n)
@@ -124,7 +124,7 @@ class autobitwise =
Printf.sprintf "Auto Bitwise Eq. (%d)" self#nbits
method descr =
- Printf.sprintf "Apply Bitwise Equality on wordsize bits (%d)" self#nbits
+ Printf.sprintf "Consider %d-bits bitwise equality." self#nbits
method search push (seq : Conditions.sequent) =
let goal = snd seq in
diff --git a/src/plugins/wp/TacChoice.ml b/src/plugins/wp/TacChoice.ml
index b760331b12d9dcbbeb1e4b55d517e9c06c744897..47e2c544432a1c613b969daf6d041c21b87d3052 100644
--- a/src/plugins/wp/TacChoice.ml
+++ b/src/plugins/wp/TacChoice.ml
@@ -33,7 +33,7 @@ class choice =
inherit Tactical.make
~id:"Wp.choice"
~title:"Choice"
- ~descr:"Select a Goal Alternative"
+ ~descr:"Select one alternative to be proved."
~params:[]
method select _feedback (s : Tactical.selection) =
@@ -54,7 +54,7 @@ class absurd =
inherit Tactical.make
~id:"Wp.absurd"
~title:"Absurd"
- ~descr:"Contradict the Goal or an Hypothesis"
+ ~descr:"Contradict the selected clause."
~params:[]
method select _feedback (s : Tactical.selection) =
@@ -88,7 +88,7 @@ class contrapose =
inherit Tactical.make
~id:"Wp.contrapose"
~title:"Contrapose"
- ~descr:"Swap and Negate Hypothesis with Conclusion"
+ ~descr:"Swap hypothesis with conclusion."
~params:[]
method select _feedback (s : Tactical.selection) =
@@ -100,7 +100,7 @@ class contrapose =
match s.condition with
| Have p | When p | Core p | Init p | Type p ->
let contrapose (hs,goal) =
- let descr = "Contrapose" in
+ let descr = "Contrapose the goal." in
let goal = F.p_not goal in
let goal = Conditions.(step ~descr (Have goal)) in
let hs = Conditions.replace ~at:s.id goal (hs , F.p_false) in
diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
index 99dcf83aea4e751b2f251d8286782c5db42459e0..111ab4645f771dfa7c9c5f06ba52e2baeef590b9 100644
--- a/src/plugins/wp/TacClear.ml
+++ b/src/plugins/wp/TacClear.ml
@@ -128,7 +128,7 @@ class clear =
object(_)
inherit Tactical.make ~id:"Wp.clear"
~title:"Clear"
- ~descr:"Remove Hypothesis"
+ ~descr:"Remove the selected hypothesis."
~params:[]
method select _feedback sel =
diff --git a/src/plugins/wp/TacCompound.ml b/src/plugins/wp/TacCompound.ml
index 5a60ac450f2fe5cd46c2bd6facac637bb0d8a018..5b0c1224e78a08d99e6d5bd2678a71557a8c8566 100644
--- a/src/plugins/wp/TacCompound.ml
+++ b/src/plugins/wp/TacCompound.ml
@@ -155,7 +155,7 @@ let process_expand (feedback : Tactical.feedback) ?at e =
let pool = feedback#pool in
let eq,cmp = get_compound_equality e in
feedback#set_title "Compound (%s)" (name eq) ;
- feedback#set_descr "Expand %s %s" (kind cmp) (equality eq) ;
+ feedback#set_descr "Expand %s %s." (kind cmp) (equality eq) ;
let e' = (if eq then conj else disj) (clause ~pool cmp) in
let cases = [feedback#get_title,F.p_true,e,F.e_prop e'] in
Tactical.rewrite ?at cases
@@ -167,14 +167,14 @@ let process_have (feedback : Tactical.feedback) s =
if eq then
begin
feedback#set_title "Compound (eq)" ;
- feedback#set_descr "Expand %s equality" (kind cmp) ;
+ feedback#set_descr "Expand %s equality." (kind cmp) ;
let cases = ["Compound (eq)",When (conj (clause ~pool cmp))] in
Tactical.replace ~at:s.id cases
end
else
begin
feedback#set_title "Compound (split)" ;
- feedback#set_descr "Split %s dis-equality" (kind cmp) ;
+ feedback#set_descr "Split %s dis-equality." (kind cmp) ;
let cases = List.map negative (clause ~pool cmp) in
Tactical.replace ~at:s.id cases
end
@@ -185,13 +185,13 @@ let process_goal (feedback : Tactical.feedback) p =
if eq then
begin
feedback#set_title "Compound (split)" ;
- feedback#set_descr "Split %s equality" (kind cmp) ;
+ feedback#set_descr "Split %s equality." (kind cmp) ;
Tactical.split (clause ~pool cmp) ;
end
else
begin
feedback#set_title "Compound (neq)" ;
- feedback#set_descr "Expand compound dis-equality" ;
+ feedback#set_descr "Expand compound dis-equality." ;
let cases = ["Compound (neq)",disj (clause ~pool cmp)] in
Tactical.split cases
end
@@ -200,7 +200,7 @@ class compound =
object
inherit Tactical.make ~id:"Wp.compound"
~title:"Compound"
- ~descr:"Decompose compound equalities"
+ ~descr:"Decompose compound equalities."
~params:[]
method select feedback (s : Tactical.selection) =
diff --git a/src/plugins/wp/TacCompute.ml b/src/plugins/wp/TacCompute.ml
index 07cbeb1d70043b2755ce29dcf33438576fa958cf..bc051433dd3f71553b90a7c7fd7f5f697f9ec862 100644
--- a/src/plugins/wp/TacCompute.ml
+++ b/src/plugins/wp/TacCompute.ml
@@ -57,18 +57,18 @@ let process (fd : Tactical.feedback) ?at e =
let p = F.p_bool c in
let q = F.p_not p in
fd#set_title "Compute (split)" ;
- fd#set_descr "Split on if-then-else condition" ;
+ fd#set_descr "Split on if-then-else condition." ;
Applicable (Tactical.rewrite ?at ["If-Then",p,e,a;"If-Else",q,e,b])
| Unfold(e,f,d) ->
fd#set_title "Compute (def)" ;
- fd#set_descr "Unfold definition of '%s'" (Lang.name_of_lfun f) ;
+ fd#set_descr "Unfold definition of '%s'." (Lang.name_of_lfun f) ;
Applicable (Tactical.rewrite ?at ["Definition",F.p_true,e,d])
class compute : Tactical.tactical =
object
inherit Tactical.make ~id:"Wp.compute"
~title:"Compute"
- ~descr:"Unfold definitions and split on conditions"
+ ~descr:"Unfold definitions and split on conditions."
~params:[]
method select feedback (s : Tactical.selection) =
process feedback ?at:(Tactical.at s) (Tactical.selected s)
diff --git a/src/plugins/wp/TacCongruence.ml b/src/plugins/wp/TacCongruence.ml
index 1e140e1a7313bc0c1ef6e78778b1f6530f44c3d3..a8fbfdad47457597d2ecaf180c925241ace632da 100644
--- a/src/plugins/wp/TacCongruence.ml
+++ b/src/plugins/wp/TacCongruence.ml
@@ -186,7 +186,7 @@ class congruence =
inherit Tactical.make
~id:"Wp.congruence"
~title:"Congruence"
- ~descr:"Euclidian Comparisons"
+ ~descr:"Resolve congruences with euclidian divisions."
~params:[]
method select _feedback = function
@@ -211,7 +211,7 @@ class autodiv =
method id = "wp:congruence"
method title = "Auto Congruence"
- method descr = "Resolve Divisions and Multiplications"
+ method descr = "Resolve divisions and multiplications."
method search push (seq : Conditions.sequent) =
try
let p = snd seq in
diff --git a/src/plugins/wp/TacCut.ml b/src/plugins/wp/TacCut.ml
index c0c6d2cd5c2494aa31ab6b846f61d73d55610b53..424340d4bb4dbd58414993fbb5f497dcbfdc5883 100644
--- a/src/plugins/wp/TacCut.ml
+++ b/src/plugins/wp/TacCut.ml
@@ -32,7 +32,7 @@ let fclause,pclause =
Tactical.composer
~id:"clause"
~title:"Clause"
- ~descr:"Clause to Cut with"
+ ~descr:"Clause to cut with."
~filter:F.is_prop
()
@@ -42,18 +42,22 @@ let fmode,pmode =
Tactical.selector
~id:"case"
~title:"Mode"
- ~descr:"Select How the Clause is Used"
+ ~descr:"Select how the clause is used."
~default:MODUS
~options:Tactical.[
- { title="Case Analysis" ; descr="" ; vid="CASES" ; value=CASES } ;
- { title="Modus Ponens" ; descr="" ; vid="MODUS" ; value=MODUS } ;
+ { title="Case Analysis" ;
+ descr="Consider P->Q and !P->Q." ;
+ vid="CASES" ; value=CASES } ;
+ { title="Modus Ponens" ;
+ descr="Consider P and P->Q." ;
+ vid="MODUS" ; value=MODUS } ;
] ()
class cut =
object(self)
inherit Tactical.make ~id:"Wp.cut"
~title:"Cut"
- ~descr:"Use Intermerdiate Hypothesis"
+ ~descr:"Use intermerdiate hypothesis."
~params:[pmode;pclause]
method select feedback sel =
@@ -70,7 +74,7 @@ class cut =
else
match mode with
| MODUS ->
- feedback#set_descr "Prove then Insert the Clause" ;
+ feedback#set_descr "Prove then insert the clause." ;
let clause = F.p_bool (Tactical.selected cut) in
let step = Conditions.step ~descr:"Cut" (Have clause) in
let at = Tactical.at sel in
@@ -81,7 +85,7 @@ class cut =
"Assume" , (fst assume,snd sequent) ]
end
| CASES ->
- feedback#set_descr "Proof by Case in the Clause" ;
+ feedback#set_descr "Proof by case in the clause." ;
let positive = F.p_bool (Tactical.selected cut) in
let negative = F.p_not positive in
Applicable
diff --git a/src/plugins/wp/TacFilter.ml b/src/plugins/wp/TacFilter.ml
index 19f2d51a940b9e7af67c9a89c782272c8217c206..3643f773c7301f96122c1131c88dbd40c823a172 100644
--- a/src/plugins/wp/TacFilter.ml
+++ b/src/plugins/wp/TacFilter.ml
@@ -29,14 +29,14 @@ open Tactical
let vanti,panti =
Tactical.checkbox ~id:"anti"
~title:"Absurd"
- ~descr:"Find Contradiction in Side Hypotheses"
+ ~descr:"Find contradiction in extra hypotheses."
~default:false ()
class filter =
object(self)
inherit Tactical.make ~id:"Wp.filter"
~title:"Filter"
- ~descr:"Dependent Erasure of Hypotheses"
+ ~descr:"Eliminates extra hypotheses."
~params:[panti]
method select feedback _sel =
diff --git a/src/plugins/wp/TacHavoc.ml b/src/plugins/wp/TacHavoc.ml
index 989769ccfbd39efbded43a3fa560b2f52b3c6c9f..412c49592ae8c9f2ff585d46d69f49c4f714c85f 100644
--- a/src/plugins/wp/TacHavoc.ml
+++ b/src/plugins/wp/TacHavoc.ml
@@ -45,7 +45,7 @@ class havoc =
object
inherit Tactical.make ~id:"Wp.havoc"
~title:"Havoc"
- ~descr:"Go Through Assigns"
+ ~descr:"Go through assigns."
~params:[]
method select _feedback sel =
@@ -93,7 +93,7 @@ class separated =
object
inherit Tactical.make ~id:"Wp.separated"
~title:"Separated"
- ~descr:"Expand Separation Cases"
+ ~descr:"Split over separated and overlapping cases."
~params:[]
method select _feedback sel =
@@ -176,7 +176,7 @@ class validity =
inherit Tactical.make ~id:"Wp.valid"
~title:"Validity Range"
- ~descr:"Unfold validity and range definitions"
+ ~descr:"Unfold validity and range definitions."
~params:[]
method select _feedback (s : Tactical.selection) =
diff --git a/src/plugins/wp/TacInduction.ml b/src/plugins/wp/TacInduction.ml
index 1403da9adbac755c49caa03aabbbbf8f6dd87e0a..316d9f2db8bb9658da5af70f1ce290d95a51b7c4 100644
--- a/src/plugins/wp/TacInduction.ml
+++ b/src/plugins/wp/TacInduction.ml
@@ -84,14 +84,14 @@ let process value n0 sequent =
(* -------------------------------------------------------------------------- *)
let vbase,pbase = Tactical.composer ~id:"base"
- ~title:"Base" ~descr:"Value of base case" ()
+ ~title:"Base" ~descr:"Value of base case." ()
class induction =
object(self)
inherit Tactical.make
~id:"Wp.induction"
~title:"Induction"
- ~descr:"Proof by integer induction"
+ ~descr:"Proof by integer induction."
~params:[pbase]
method private get_base () =
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index a73274c60faa70efd4decfa5192bb901bd958797..f9099ad4e314de47fffd5f2eb6776f95746890d6 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -30,10 +30,10 @@ module L = Qed.Logic
(* -------------------------------------------------------------------------- *)
let descr = function
- | 1 -> "First Parameter"
- | 2 -> "Second Parameter"
- | 3 -> "Third Parameter"
- | n -> Printf.sprintf "%d-th Parameter" n
+ | 1 -> "First parameter."
+ | 2 -> "Second parameter."
+ | 3 -> "Third parameter."
+ | n -> Printf.sprintf "%d-th parameter." n
let mkparam k =
Tactical.composer
@@ -142,7 +142,7 @@ class instance =
object(self)
inherit Tactical.make ~id:"Wp.instance"
~title:"Instance"
- ~descr:"Instantiate properties"
+ ~descr:"Instantiate properties."
~params
method private wrap env lemma fields =
@@ -177,10 +177,10 @@ class instance =
match cardinal 1000 bindings with
| Some n ->
if n > 1 then
- feedback#set_descr "Generates %d instances" n ;
+ feedback#set_descr "Generates %d instances." n ;
Applicable (bind ~side bindings (F.p_bool phi))
| None ->
- feedback#set_error "More than 1,000 instances" ;
+ feedback#set_error "More than 1,000 instances." ;
Not_configured
else Not_configured
else
diff --git a/src/plugins/wp/TacLemma.ml b/src/plugins/wp/TacLemma.ml
index a304e9efe891837b4d8e0f4130edda56364e842a..929660ba310bf714e0f20431992e478ee8386864 100644
--- a/src/plugins/wp/TacLemma.ml
+++ b/src/plugins/wp/TacLemma.ml
@@ -86,7 +86,7 @@ type lemma = Definitions.dlemma Tactical.named
let find thm = named (Definitions.find_name thm)
let search,psearch =
- Tactical.search ~id:"lemma" ~title:"Lemma" ~descr:"Lemma to Instantiate"
+ Tactical.search ~id:"lemma" ~title:"Lemma" ~descr:"Lemma to instantiate."
~browse ~find ()
@@ -99,7 +99,7 @@ class instance =
object(self)
inherit Tactical.make ~id:"Wp.lemma"
~title:"Lemma"
- ~descr:"Search & Instantiate Lemma"
+ ~descr:"Search and instantiate lemmas."
~params:(psearch :: TacInstance.params)
method private hide (feedback : Tactical.feedback) fields =
@@ -139,7 +139,7 @@ class instance =
match TacInstance.cardinal 1000 bindings with
| Some n ->
if n > 1 then
- feedback#set_descr "Generates %d instances" n ;
+ feedback#set_descr "Generates %d instances." n ;
let at = Tactical.at selection in
Applicable
(TacInstance.instance_have ~title ?at bindings lemma)
diff --git a/src/plugins/wp/TacModMask.ml b/src/plugins/wp/TacModMask.ml
index c2e7cd09ba2e358847157112f9845f147ca124c0..d6b86ee987063db35037e28ede8feae3c04c71e6 100644
--- a/src/plugins/wp/TacModMask.ml
+++ b/src/plugins/wp/TacModMask.ml
@@ -28,7 +28,7 @@ let title_revert = "Revert (current: m & a -> a % m+1)"
let v_revert,p_revert =
Tactical.checkbox ~id:"Wp.modmask.revert"
~title:title_no_revert
- ~descr:"Changes operands for modulo"
+ ~descr:"Changes operands for modulo."
~default:false ()
class modmask =
@@ -36,7 +36,7 @@ class modmask =
inherit Tactical.make
~id:"Wp.modmask"
~title:"Mod-Mask"
- ~descr:"Converts modulo from/to bitmask"
+ ~descr:"Converts modulo from/to bitmask."
~params:[p_revert]
method select feedback selection =
diff --git a/src/plugins/wp/TacNormalForm.ml b/src/plugins/wp/TacNormalForm.ml
index f996f7fb5385a89e90876ec6a8cdb29a221f9ff2..dcddbdd06544a41192d364154e00fbc341cfc0aa 100644
--- a/src/plugins/wp/TacNormalForm.ml
+++ b/src/plugins/wp/TacNormalForm.ml
@@ -29,7 +29,7 @@ open Tactical
let str_case = "Case"
let sub_cases phi = function
| [] -> List.map (fun t -> phi str_case (F.p_bool t))
- | [descr] -> List.map (fun t -> phi descr (F.p_bool t))
+ | [descr] -> List.map (fun t -> phi descr (F.p_bool t))
| infos -> List.map2 (fun info t -> phi info (F.p_bool t)) infos
(* split into n sequents: [hyps] |- [subcases]_i *)
@@ -79,7 +79,7 @@ class normal_form =
object
inherit Tactical.make ~id:"Wp.normal_form"
~title:"Intuition"
- ~descr:"Decompose with Conjunctive/Disjunctive Normal Form"
+ ~descr:"Decompose into conjunctive or disjunctive normal form."
~params:[]
method select feedback (s : Tactical.selection) =
diff --git a/src/plugins/wp/TacOverflow.ml b/src/plugins/wp/TacOverflow.ml
index c28c055e8728f1793bed1d114fd0d559d22429c7..8591c6d8f8b4b24a2e03795a71f6252ac15972db 100644
--- a/src/plugins/wp/TacOverflow.ml
+++ b/src/plugins/wp/TacOverflow.ml
@@ -28,7 +28,7 @@ class overflow =
inherit Tactical.make
~id:"Wp.overflow"
~title:"Overflow"
- ~descr:"Split integer overflow into in and out of range"
+ ~descr:"Split integer overflow into in and out of range."
~params:[]
method select _feedback selection =
diff --git a/src/plugins/wp/TacRange.ml b/src/plugins/wp/TacRange.ml
index 0184d4e8ffd7b6620b2c8b0c4522194f9df6a3b1..6e4e8362682eca7b6d88e8fed658c4ccc0a13596 100644
--- a/src/plugins/wp/TacRange.ml
+++ b/src/plugins/wp/TacRange.ml
@@ -42,15 +42,15 @@ let enum ?at e a b sequent =
Tactical.insert ?at cases sequent
let vmin,pmin = Tactical.spinner ~id:"inf"
- ~title:"Inf" ~descr:"Range Lower Bound (inclusive)" ()
+ ~title:"Inf" ~descr:"Range lower bound (inclusive)." ()
let vmax,pmax = Tactical.spinner ~id:"sup"
- ~title:"Sup" ~descr:"Range Upper Bound (inclusive)" ()
+ ~title:"Sup" ~descr:"Range upper bound (inclusive)." ()
class range =
object(self)
inherit Tactical.make ~id:"Wp.range"
~title:"Range"
- ~descr:"Enumerate a range of values for an integer term"
+ ~descr:"Enumerate a range of values for an integer term."
~params:[pmin;pmax]
method select feedback (s : Tactical.selection) =
@@ -65,7 +65,7 @@ class range =
Not_configured )
else
( feedback#set_title "Range (%d-%d)" a b ;
- feedback#set_descr "Enumerate (lower,%d-%d,upper)" a b ;
+ feedback#set_descr "Enumerate lower, range %d-%d and upper." a b ;
Applicable(enum ?at e a b) )
end
else
diff --git a/src/plugins/wp/TacRewrite.ml b/src/plugins/wp/TacRewrite.ml
index 2395be03dc095ccce711e52b3830ca98465da712..51c52f4efda6904736ec3791f7b4b585465753d6 100644
--- a/src/plugins/wp/TacRewrite.ml
+++ b/src/plugins/wp/TacRewrite.ml
@@ -53,7 +53,7 @@ class rewrite dir =
let title = if dir then "Rewrite (<-)" else "Rewrite (->)" in
object
inherit Tactical.make
- ~id ~title ~descr:"Rewrite from equality" ~params:[]
+ ~id ~title ~descr:"Rewrite from equality." ~params:[]
method select _feedback select =
try
@@ -106,7 +106,7 @@ class auto_rewrite =
object
method id = "wp:replace"
method title = "Auto Replace"
- method descr = "Lookup for equalities to Rewrite"
+ method descr = "Lookup for equalities to rewrite with."
method search (push : Strategy.strategy -> unit) (hyps,goal) =
Conditions.iter
(fun s ->
diff --git a/src/plugins/wp/TacSequence.ml b/src/plugins/wp/TacSequence.ml
index e9899747565a61d46c6f4b3634ef1048ee5080c2..09a4144379129f026c3570a6e90638a215028621 100644
--- a/src/plugins/wp/TacSequence.ml
+++ b/src/plugins/wp/TacSequence.ml
@@ -35,14 +35,14 @@ let sum n = match F.repr n with
(* -------------------------------------------------------------------------- *)
let vmode,pmode =
- Tactical.selector ~id:"seq.side" ~title:"Mode" ~descr:"Unrolling mode"
+ Tactical.selector ~id:"seq.side" ~title:"Mode" ~descr:"Unrolling mode."
~options:[
{ vid = "left" ; title = "Unroll left" ;
- descr = "Transform (A^n) into (A.A^n-1)" ; value = `Left } ;
+ descr = "Transform (A^n) into (A.A^n-1)." ; value = `Left } ;
{ vid = "right" ; title = "Unroll right" ;
- descr = "Transform (A^n) into (A^n-1.A)" ; value = `Right } ;
+ descr = "Transform (A^n) into (A^n-1.A)." ; value = `Right } ;
{ vid = "sum" ; title = "Concat sum" ;
- descr = "Transform A^(p+q) into (A^p.A^q)" ; value = `Sum }
+ descr = "Transform A^(p+q) into (A^p.A^q)." ; value = `Sum }
] ()
class sequence =
@@ -50,7 +50,7 @@ class sequence =
inherit Tactical.make
~id:"Wp.sequence"
~title:"Sequence"
- ~descr:"Unroll repeat-sequence operator"
+ ~descr:"Unroll repeat-sequence operator."
~params:[pmode]
method select feedback (s : Tactical.selection) =
@@ -67,7 +67,7 @@ class sequence =
match sum n with
| [ s ] ->
feedback#set_descr
- "Cannot unroll with selected option, '%a' is not a sum"
+ "Cannot unroll: '%a' is not a sum."
F.pp_term s ;
Tactical.Not_configured
| ns ->
@@ -76,7 +76,7 @@ class sequence =
let cat =
concat ~result (List.map (repeat ~result a) ns) in
feedback#set_descr
- "Unroll repeat-sequence: unroll sum" ;
+ "Unroll repeat-sequence: unroll sum." ;
Tactical.Applicable (
Tactical.condition "Positive" pos @@
Tactical.rewrite ?at [ "Unroll" , pos , value , cat ])
@@ -87,7 +87,7 @@ class sequence =
let p = F.e_add n F.e_minus_one in
let unroll = concat ~result [a ; repeat ~result a p] in
feedback#set_descr
- "Unroll repeat-sequence: unroll first element" ;
+ "Unroll repeat-sequence: unroll first element." ;
Tactical.Applicable(
Tactical.rewrite ?at [
"Nil", negative n , value , concat ~result [] ;
@@ -99,7 +99,7 @@ class sequence =
let p = F.e_add n F.e_minus_one in
let unroll = concat ~result [repeat ~result a p ; a] in
feedback#set_descr
- "Unroll repeat-sequence: unroll last element" ;
+ "Unroll repeat-sequence: unroll last element." ;
Tactical.Applicable(
Tactical.rewrite ?at [
"Nil", negative n , value , concat ~result [] ;
diff --git a/src/plugins/wp/TacShift.ml b/src/plugins/wp/TacShift.ml
index dc0bda06d57698ec26922046127da26b0b9f92b5..d35bf081ae86e53c821807d57c502db95fe2e839 100644
--- a/src/plugins/wp/TacShift.ml
+++ b/src/plugins/wp/TacShift.ml
@@ -53,7 +53,7 @@ class shift =
inherit Tactical.make
~id:"Wp.shift"
~title:"Logical Shift"
- ~descr:"Transform Shifts into Div/Mult"
+ ~descr:"Transform logical shifts into divisions and multiplications."
~params:[]
method select feedback selection =
@@ -104,7 +104,7 @@ class autoshift =
method id = "wp:bitshift"
method title = "Auto Bit-Shift"
- method descr = "Apply Bit-Shift in Goal"
+ method descr = "Decompose logical shifts from current goal."
method search push (seq : Conditions.sequent) =
let goal = snd seq in
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 0e1e31f1e1e64650d38e9585f6be8390aa834e96..023633e34a2f7711cf3948eb23075ead12106d20 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -164,14 +164,14 @@ class split =
inherit Tactical.make
~id:"Wp.split"
~title:"Split"
- ~descr:"Decompose Logical Connectives and Conditionals"
+ ~descr:"Decompose logical connectives and conditionals."
~params:[]
method select feedback (s : Tactical.selection) =
let split_cmp at title x y =
feedback#set_title title ;
feedback#set_descr
- "Decompose into three comparisons (lt, eq, gt)" ;
+ "Decompose into three comparisons (lt, eq, gt)." ;
let cases = [
"Lt",F.p_bool (e_lt x y);
"Eq",F.p_bool (e_eq x y);
@@ -199,7 +199,7 @@ class split =
| Neq(x,y) when not (is_prop x || is_prop y) -> split_neq at x y
| _ when F.is_prop e ->
feedback#set_title "Split (true,false)" ;
- feedback#set_descr "Decompose between True and False values" ;
+ feedback#set_descr "Decompose between boolean values." ;
let cases = ["True",F.p_bool e;"False",F.p_not (F.p_bool e)] in
let at = Tactical.at s in
Applicable (Tactical.insert ?at cases)
@@ -218,7 +218,7 @@ class split =
(* unbound condition: proceed by case *)
feedback#set_title "Split (exists if)" ;
feedback#set_descr
- "Split unbound Condition into Branches" ;
+ "Split unbound condition into branches." ;
let p = F.e_imply [c] (bind Exists ~vars p) in
let q = F.e_imply [e_not c] (bind Exists ~vars q) in
Applicable (Tactical.split [
@@ -230,8 +230,8 @@ class split =
begin
feedback#set_title "Split (rewrite exists if)" ;
feedback#set_descr
- "Rewrite the Conditional in a Disjunction \
- and Distribute the Quantifier under" ;
+ "Rewrite into a disjunction \
+ and distribute the quantifier under." ;
let p = bind Exists ~vars (F.e_and [c;p]) in
let q = bind Exists ~vars (F.e_and [(e_not c); q]) in
let cases = [ "Split" , F.p_bool (F.e_or [p;q]) ] in
@@ -240,14 +240,14 @@ class split =
| Or es ->
feedback#set_title "Split (exists or)" ;
feedback#set_descr
- "Distributes the Quantifier under the Disjunction" ;
+ "Distributes the quantifier under the disjunction." ;
let p = F.e_or (List.map (bind Exists ~vars) es) in
let cases = [ "Split" , F.p_bool p ] in
Applicable (Tactical.split cases)
| Imply (es, p) ->
feedback#set_title "Split (exists imply)" ;
feedback#set_descr
- "Distributes the Quantifier under the Imply" ;
+ "Distributes the quantifier under the implication." ;
let p = F.e_imply (List.map (bind Forall ~vars) es)
(bind Exists ~vars p) in
let cases = [ "Split" , F.p_bool p ] in
@@ -258,7 +258,7 @@ class split =
else begin
feedback#set_title "Split (exists and)" ;
feedback#set_descr
- "Decompose the Quantifier into %d Blocks" nb_parts ;
+ "Decompose the quantifier into %d parts." nb_parts ;
let bind es =
bind Exists ~vars (F.e_and (F.Tset.elements es)) in
let goal i n es =
@@ -271,26 +271,26 @@ class split =
let n = List.length es in
feedback#set_title "Split (and)" ;
feedback#set_descr
- "Decompose between the %d parts of the Conjunction" n ;
+ "Decompose between the %d parts of the conjunction." n ;
let goal i n e = Printf.sprintf "Goal %d/%d" i n , F.p_bool e in
Applicable (Tactical.split (Tactical.mapi goal es))
| Eq(x,y) when (F.is_prop x) && (F.is_prop y) ->
feedback#set_title "Split (iff)" ;
- feedback#set_descr "Turn Equivalence into Implications" ;
+ feedback#set_descr "Turn equivalence into implications." ;
let p = F.p_bool (F.e_imply [x] y) in
let q = F.p_bool (F.e_imply [y] x) in
let cases = [ "Necessity" , p ; "Sufficiency" , q ] in
Applicable (Tactical.split cases)
| Neq(x,y) when (F.is_prop x) && (F.is_prop y) ->
feedback#set_title "Split (xor)" ;
- feedback#set_descr "Turn Dis-Equivalence into Implications" ;
+ feedback#set_descr "Turn dis-equivalence into implications" ;
let p = F.p_bool (F.e_imply [x] (e_not y)) in
let q = F.p_bool (F.e_imply [y] (e_not x)) in
let cases = [ "Necessity" , p ; "Sufficiency" , q ] in
Applicable (Tactical.split cases)
| If(c,p,q) -> (* Split + intro *)
feedback#set_title "Split (if)" ;
- feedback#set_descr "Decompose Conditional into Branches" ;
+ feedback#set_descr "Decompose conditional into branches." ;
let p = F.p_bool (F.e_imply [c] p) in
let q = F.p_bool (F.e_imply [e_not c] q) in
let cases = [ "Then" , p ; "Else" , q ] in
@@ -304,13 +304,13 @@ class split =
| State _ | Probe _ -> Not_applicable
| Branch(p,_,_) ->
feedback#set_title "Split (branch)" ;
- feedback#set_descr "Decompose Conditional into Branches" ;
+ feedback#set_descr "Decompose conditional into branches." ;
let cases = [ "Then" , p ; "Else" , p_not p ] in
Applicable (Tactical.insert ~at:step.id cases)
| Either seqs ->
let n = List.length seqs in
feedback#set_title "Split (switch)" ;
- feedback#set_descr "Decompose each %d Cases" n ;
+ feedback#set_descr "Decompose each %d cases." n ;
let either i n s = Printf.sprintf "Case %d/%d" i n , Either [s] in
let cases = Tactical.mapi either seqs in
Applicable (Tactical.replace ~at:step.id cases)
@@ -325,7 +325,7 @@ class split =
if F.Vars.is_empty (F.Vars.inter (F.vars c) vars) then
begin (* unbound condition: so, the If is considered as a disjunction *)
feedback#set_title "Split (forall if)" ;
- feedback#set_descr "Decompose unbound conditional into Branches" ;
+ feedback#set_descr "Decompose unbound conditional into branches." ;
let p = F.p_bool (F.e_and [c; (bind Exists ~vars p)]) in
let q = F.p_bool (F.e_and [(e_not c); (bind Exists ~vars q)]) in
let cases = [ "Then" , When p ; "Else" , When q ] in
@@ -334,7 +334,7 @@ class split =
else
begin
feedback#set_title "Split (rewrite forall if)" ;
- feedback#set_descr "Rewrite the Conditional in a Conjunction and Distributes the Quantifier under the Conjunction" ;
+ feedback#set_descr "Rewrite the conjunction and distribute the quantifier." ;
let p = bind Exists ~vars (F.e_imply [c] p) in
let q = bind Exists ~vars (F.e_imply [e_not c] q) in
let cases = [ "Split (rewrite exists if)" , When (F.p_bool (F.e_and [p;q])) ] in
@@ -342,7 +342,7 @@ class split =
end
| And es ->
feedback#set_title "Split (forall and)" ;
- feedback#set_descr "Distributes the Quantifier under the Conjunction" ;
+ feedback#set_descr "Distributes the quantifier under the conjunction." ;
let p = F.p_bool (F.e_and (List.map (bind Forall ~vars) es)) in
let cases = [ "Split (distrib forall and)" , When p ] in
Applicable (Tactical.replace ~at:step.id cases)
@@ -351,7 +351,7 @@ class split =
if nb_parts=1 then Not_applicable
else begin
feedback#set_title "Split (forall or)" ;
- feedback#set_descr "Decompose the Quantifier between %d parts of the Disjunction" nb_parts ;
+ feedback#set_descr "Decompose the quantifier between %d parts of the disjunction." nb_parts ;
let bind es = bind Forall ~vars (F.e_or (F.Tset.elements es)) in
let goal i n es = Printf.sprintf "Goal %d/%d" i n , When (F.p_bool (bind es)) in
let cases = Tactical.mapi goal parts in
@@ -362,13 +362,13 @@ class split =
| Or xs ->
let n = List.length xs in
feedback#set_title "Split (or)" ;
- feedback#set_descr "Distinguish the %d parts of the Disjunction" n ;
+ feedback#set_descr "Distinguish the %d parts of the disjunction." n ;
let hyp i n e = Printf.sprintf "Case %d/%d" i n , When (F.p_bool e) in
let cases = Tactical.mapi hyp xs in
Applicable (Tactical.replace ~at:step.id cases)
| Eq(x,y) when (F.is_prop x)&&(F.is_prop y) ->
feedback#set_title "Split (iff)";
- feedback#set_descr "Decompose Equivalence into both True/False" ;
+ feedback#set_descr "Decompose equivalence into booleans." ;
let p = F.p_bool x in
let q = F.p_bool y in
let cases = [
@@ -378,7 +378,7 @@ class split =
Applicable (Tactical.replace ~at:step.id cases)
| Neq(x,y) when (F.is_prop x)&&(F.is_prop y) ->
feedback#set_title "Split (xor)";
- feedback#set_descr "Decompose Dis-Equivalence into alternated True/False" ;
+ feedback#set_descr "Decompose Dis-equivalence into booleans." ;
let p = F.p_bool x in
let q = F.p_bool y in
let cases = [
@@ -396,7 +396,7 @@ class split =
split_leq (Some step.id) x y
| If(c,p,q) ->
feedback#set_title "Split (if)" ;
- feedback#set_descr "Split Conditional into Branches" ;
+ feedback#set_descr "Split conditional into branches." ;
let p = F.p_bool (F.e_and [c;p]) in
let q = F.p_bool (F.e_and [e_not c;q]) in
let cases = [ "Then" , When p ; "Else" , When q ] in
@@ -412,7 +412,7 @@ class split =
| _ -> assert false (* see above pattern matching *)
in
feedback#set_title "Split (conjunction)" ;
- feedback#set_descr "Split conjunction into steps" ;
+ feedback#set_descr "Split conjunction into different steps." ;
let ps = List.map (fun p -> cond @@ p_bool p) ps in
Applicable (Tactical.replace_step ~at:step.id ps)
| _ ->
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index 588d32aaa93d789c2a6f5de7e8619fd75b485378..ccc1bf0eb15c3c4fb78359e1e3c2f2a3995160f7 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/src/plugins/wp/TacUnfold.ml
@@ -171,7 +171,7 @@ class unfold =
object
inherit Tactical.make ~id:"Wp.unfold"
~title:"Definition"
- ~descr:"Unfold predicate and logic function definition"
+ ~descr:"Unfold definitions of predicates and functions."
~params:[]
method select _feedback (s : Tactical.selection) =
diff --git a/src/plugins/wp/VC.ml b/src/plugins/wp/VC.ml
index 59be9f01aad647c7b2da65501c65788dd767f30f..4cbd4b35863037c79ba2a0fbd6be9d942101f581 100644
--- a/src/plugins/wp/VC.ml
+++ b/src/plugins/wp/VC.ml
@@ -36,9 +36,9 @@ let get_description = Wpo.get_label
let get_property = Wpo.get_property
let get_sequent w = snd (Wpo.compute w)
let get_result = Wpo.get_result
-let get_results = Wpo.get_results
+let get_results = ProofEngine.results
let is_trivial = Wpo.is_trivial
-let is_valid = Wpo.is_valid
+let is_valid = Wpo.is_fully_valid
let is_passed = Wpo.is_passed
let has_unknown = Wpo.has_unknown
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 1fef10ad99975088ac10a8bc0a17ff13f3108b1b..88ed31052135da2d5017e5e7a46fe4231c64e771 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -117,19 +117,21 @@ let is_prover = function
| Qed | Why3 _ -> true
| Tactical -> false
+let is_extern = function
+ | Qed | Tactical -> false
+ | Why3 _ -> true
+
let is_auto = function
| Qed -> true
| Tactical -> false
- | Why3 p ->
- match p.prover_name with
- | "Alt-Ergo" | "CVC4" | "Z3" -> true
- | "Coq" -> false
- | _ ->
- let config = Why3Provers.config () in
- try
- let prover_config = Why3.Whyconf.get_prover_config config p in
- not prover_config.interactive
- with Not_found -> true
+ | Why3 p -> Why3Provers.is_auto p
+
+let eq_prover p q =
+ match p,q with
+ | Qed,Qed -> true
+ | Tactical,Tactical -> true
+ | Why3 p, Why3 q -> Why3Provers.compare p q = 0
+ | (Why3 _ | Qed | Tactical) , _ -> false
let has_counter_examples = function
| Qed | Tactical -> false
@@ -232,12 +234,12 @@ type result = {
let is_result = function
| Valid | Invalid | Unknown | Timeout | Stepout | Failed -> true
| NoResult | Computing _ -> false
-
let is_verdict r = is_result r.verdict
let is_valid = function { verdict = Valid } -> true | _ -> false
let is_trivial r = is_valid r && r.prover_time = 0.0
let is_not_valid r = is_verdict r && not (is_valid r)
let is_computing = function { verdict=Computing _ } -> true | _ -> false
+let is_none = function { verdict=NoResult } -> true | _ -> false
let is_proved ~smoke = function
| NoResult | Computing _ | Failed -> false
| Valid -> not smoke
@@ -337,8 +339,9 @@ let pp_perf_shell fmt r =
if not (Wp_parameters.has_dkey dkey_shell) then
pp_perf_forced fmt r
-let name_of_verdict = function
- | NoResult | Computing _ -> "none"
+let name_of_verdict ?(computing=false) = function
+ | NoResult -> "none"
+ | Computing _ -> if computing then "computing" else "none"
| Valid -> "valid"
| Invalid -> "invalid"
| Failed -> "failed"
@@ -400,7 +403,6 @@ let pp_model fmt model =
) model
let vrank = function
- | Computing _ -> 0
| NoResult -> 1
| Failed -> 2
| Unknown -> 3
@@ -408,13 +410,17 @@ let vrank = function
| Stepout -> 5
| Valid -> 6
| Invalid -> 7
+ | Computing _ -> 8
let conjunction a b =
- match a,b with
- | Valid,Valid -> Valid
- | Valid, r -> r
- | r , Valid -> r
- | _ -> if vrank b > vrank a then b else a
+ if a == b then a else
+ match a,b with
+ | Computing p , Computing q -> Computing (fun () -> p () ; q ())
+ | Computing _ , _ -> a
+ | _ , Computing _ -> b
+ | Valid,Valid -> Valid
+ | Valid,r | r,Valid -> r
+ | _ -> if vrank b > vrank a then b else a
let msize m = Probe.Map.fold (fun _ _ n -> succ n) m 0
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 62a7f6b5d91a1546eccaaaba409ee49884e0f22e..d8751c8fa69115c4cc1447424afffff009c162dd 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -55,6 +55,7 @@ val parse_prover : string -> prover option
val pp_prover : Format.formatter -> prover -> unit
val pp_mode : Format.formatter -> mode -> unit
+val eq_prover : prover -> prover -> bool
val cmp_prover : prover -> prover -> int
(* -------------------------------------------------------------------------- *)
@@ -124,7 +125,9 @@ val result : ?model:model -> ?cached:bool ->
val is_auto : prover -> bool
val has_counter_examples : prover -> bool
val is_prover : prover -> bool
+val is_extern : prover -> bool
val is_result : verdict -> bool
+val is_none : result -> bool
val is_verdict : result -> bool
val is_valid: result -> bool
val is_trivial: result -> bool
@@ -135,7 +138,7 @@ val is_proved: smoke:bool -> verdict -> bool
val configure : result -> config
val autofit : result -> bool (** Result that fits the default configuration *)
-val name_of_verdict : verdict -> string
+val name_of_verdict : ?computing:bool -> verdict -> string
val pp_result : Format.formatter -> result -> unit
val pp_model : Format.formatter -> model -> unit
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 068faf90639e77bfab3b14a73f96c956dd044db0..6bf0e1ee14dd77c16f3e667dd3752f6a02603cae 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -32,7 +32,7 @@ let cfg = lazy
Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn
end
-let version = Why3.Config.version
+let why3_version = Why3.Config.version
let config () = Lazy.force cfg
let set_procs = Why3.Controller_itp.set_session_max_tasks
@@ -106,7 +106,20 @@ let title ?(version=true) p =
if version then Pretty_utils.to_string Why3.Whyconf.print_prover p
else p.Why3.Whyconf.prover_name
let compare = Why3.Whyconf.Prover.compare
+let name p = p.Why3.Whyconf.prover_name
+let version p = p.Why3.Whyconf.prover_version
+let altern p = p.Why3.Whyconf.prover_altern
let is_mainstream p = p.Why3.Whyconf.prover_altern = ""
+let is_auto (p : t) =
+ match p.prover_name with
+ | "Coq" | "Isabelle" -> false
+ | "Alt-Ergo" | "Z3" | "CVC4" | "CVC5" | "Colibri2" -> true
+ | _ ->
+ let config = config () in
+ try
+ let prover_config = Why3.Whyconf.get_prover_config config p in
+ not prover_config.interactive
+ with Not_found -> true
let has_counter_examples p =
List.mem "counterexamples" @@
String.split_on_char '+' p.Why3.Whyconf.prover_altern
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index 7992e2b140e31a5bcb2875896f5be6fca71d9924..0142173be48e4b1e529858398f9aebcd2c679bbf 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-val version : string
+val why3_version : string
val config : unit -> Why3.Whyconf.config
val configure : unit -> unit
val set_procs : int -> unit
@@ -35,10 +35,14 @@ val find_fallback : string -> fallback
val ident_why3 : t -> string
val ident_wp : t -> string
val title : ?version:bool -> t -> string
+val name : t -> string
+val version : t -> string
+val altern : t -> string
val compare : t -> t -> int
val provers : unit -> t list
val provers_set : unit -> Why3.Whyconf.Sprover.t
+val is_auto : t -> bool
val is_available : t -> bool
val is_mainstream : t -> bool
val has_counter_examples : t -> bool
diff --git a/src/plugins/wp/gui/GuiComposer.ml b/src/plugins/wp/gui/GuiComposer.ml
index 629091a8ffd4be16babd3e5345dfd97b79874f00..c8ed0c1c2d5bf1db5876f961bd121a4b3ccf5afc 100644
--- a/src/plugins/wp/gui/GuiComposer.ml
+++ b/src/plugins/wp/gui/GuiComposer.ml
@@ -179,7 +179,7 @@ class composer (focused : GuiSequent.focused) =
method print (cc : GuiTactic.composer) ~quit fmt =
begin
- focused#set_target Tactical.Empty ;
+ focused#highlight Tactical.Empty ;
Format.fprintf fmt "@{<bf>Selection:@} @{<ul>%s@} %t%t@\n"
cc#title
(focused#button ~title:"Help" ~callback:self#openhelp)
@@ -266,7 +266,7 @@ class browser (focused : GuiSequent.focused) =
method print ( cc : GuiTactic.browser ) ~quit fmt =
begin
- focused#set_target cc#target ;
+ focused#highlight cc#target ;
let ptitle = if paging = 10 then "5/page" else "10/page" in
let ctitle () = paging <- if paging = 10 then 5 else 10 ; update () in
Format.fprintf fmt "@{<bf>Selection for %s:@} %t%t@\n@\n"
diff --git a/src/plugins/wp/gui/GuiGoal.ml b/src/plugins/wp/gui/GuiGoal.ml
index d16760abc2e6427d6fe042034b0ceb232dcf9d8c..e05f708a0e5af765fb1783d3551ee4baabdbe5a9 100644
--- a/src/plugins/wp/gui/GuiGoal.ml
+++ b/src/plugins/wp/gui/GuiGoal.ml
@@ -161,8 +161,8 @@ class pane (gprovers : GuiConfig.provers) =
scripter#on_click self#goto ;
scripter#on_backtrack self#backtrack ;
gprovers#connect self#register_provers ;
- delete#connect (fun () -> self#interrupt ProofEngine.reset) ;
- cancel#connect (fun () -> self#interrupt ProofEngine.cancel) ;
+ delete#connect (fun () -> self#interrupt ProofEngine.cancel_current_node) ;
+ cancel#connect (fun () -> self#interrupt ProofEngine.cancel_parent_tactic) ;
forward#connect (fun () -> self#forward) ;
next#connect (fun () -> self#navigate succ) ;
prev#connect (fun () -> self#navigate pred) ;
@@ -279,7 +279,7 @@ class pane (gprovers : GuiConfig.provers) =
method private play_script =
match state with
| Proof p ->
- ProofEngine.reset p ;
+ ProofEngine.clear_tree p ;
ProverScript.spawn
~provers:self#provers
~result:
@@ -382,7 +382,7 @@ class pane (gprovers : GuiConfig.provers) =
method private update_tactics = function
| None ->
- printer#set_target Tactical.Empty ;
+ printer#highlight Tactical.Empty ;
autosearch#connect None ;
strategies#connect None ;
List.iter (fun tactic -> tactic#clear) tactics
@@ -403,7 +403,7 @@ class pane (gprovers : GuiConfig.provers) =
tactic#select ~process ~composer ~browser ~tree sel
) tactics ;
(* target selection feedback *)
- printer#set_target
+ printer#highlight
(if List.exists (fun tactics -> tactics#targeted) tactics
then sel else Tactical.Empty)
end ()
@@ -561,7 +561,7 @@ class pane (gprovers : GuiConfig.provers) =
text#hrule ;
scripter#tree proof ;
text#hrule ;
- text#printf "%a@." printer#pp_goal (ProofEngine.head_goal proof) ;
+ text#printf "@\n%a@." printer#pp_goal (ProofEngine.head_goal proof) ;
text#printf "@{<bf>Goal id:@} %s@." main.po_gid ;
text#printf "@{<bf>Short id:@} %s@." main.po_sid ;
text#hrule ;
@@ -577,7 +577,7 @@ class pane (gprovers : GuiConfig.provers) =
self#update in
text#printf "%t@." (composer#print cc ~quit) ;
text#hrule ;
- text#printf "%a@." printer#pp_goal (ProofEngine.head_goal proof) ;
+ text#printf "@\n%a@." printer#pp_goal (ProofEngine.head_goal proof) ;
end ()
| Browser(proof,cc,tgt) ->
on_proof_context proof
@@ -589,7 +589,7 @@ class pane (gprovers : GuiConfig.provers) =
self#update in
text#printf "%t@." (browser#print cc ~quit) ;
text#hrule ;
- text#printf "%a@." printer#pp_goal (ProofEngine.head_goal proof) ;
+ text#printf "@\n%a@." printer#pp_goal (ProofEngine.head_goal proof) ;
end ()
| Forking _ -> ()
diff --git a/src/plugins/wp/gui/GuiNavigator.ml b/src/plugins/wp/gui/GuiNavigator.ml
index 3a1b08139c846a72deae247b8619c57214ab1703..20891f104b667857c6f733f41fcd0857fa788a9b 100644
--- a/src/plugins/wp/gui/GuiNavigator.ml
+++ b/src/plugins/wp/gui/GuiNavigator.ml
@@ -128,7 +128,7 @@ class behavior
list#reload ;
let to_prove g =
not (Wpo.is_smoke_test g) &&
- not (Wpo.is_valid g || Wpo.reduce g) in
+ not (Wpo.is_fully_valid g || Wpo.reduce g) in
let has_proof g =
match ProofEngine.get g with
| `None -> false
@@ -298,7 +298,7 @@ class behavior
method private popup_delete_script () =
match popup_target with
- | Some(w,_) -> ProofEngine.clear w ; ProofSession.remove w
+ | Some(w,_) -> ProofEngine.clear_goal w ; ProofSession.remove w
| None -> ()
method private popup_run mode () =
diff --git a/src/plugins/wp/gui/GuiProof.ml b/src/plugins/wp/gui/GuiProof.ml
index 390f2a7e2759f93d4e69ca0affb209e7d954e2fd..a7fda271b84c90c7511a93f11539b3a7204cd343 100644
--- a/src/plugins/wp/gui/GuiProof.ml
+++ b/src/plugins/wp/gui/GuiProof.ml
@@ -193,7 +193,7 @@ class printer (text : Wtext.text) =
| `Internal here | `Leaf(_,here) ->
begin
let root,path = rootchain here [here] in
- let qed = if Wpo.is_valid (ProofEngine.main tree) then "Qed" else "End"
+ let qed = if Wpo.is_fully_valid (ProofEngine.main tree) then "Qed" else "End"
in text#printf "@[<hv 0>@{<bf>Proof@}:%a@\n@{<bf>%s@}.@]@."
(self#proofstep ~prefix:" " ~direct:" " ~path ~here) root qed ;
end
diff --git a/src/plugins/wp/ptip.ml b/src/plugins/wp/ptip.ml
index 76c0393e81500d32f4836c81862b01646a846117..2a4a5acd1da2c2568ec01cb666e65ee9a2eb1c95 100644
--- a/src/plugins/wp/ptip.ml
+++ b/src/plugins/wp/ptip.ml
@@ -488,7 +488,7 @@ class pseq
method selected =
begin
- self#set_target self#selection ;
+ self#highlight self#selection ;
List.iter (fun f -> f ()) demon ;
end
@@ -534,7 +534,22 @@ class pseq
in if selected then self#selected
end
- method set_target tgt =
+ method set_selection sel =
+ let current = self#selection in
+ if not @@ Tactical.equal current sel then
+ let target =
+ match sel with
+ | Tactical.Empty | Tactical.Compose _ | Tactical.Multi _ ->
+ Term, None
+ | Tactical.Clause(Goal p) -> Goal, Some (F.e_prop p)
+ | Tactical.Clause(Step s as clause) ->
+ Step s, Some (F.e_prop @@ Tactical.head clause)
+ | Tactical.Inside(Goal _,t) -> Goal, Some t
+ | Tactical.Inside(Step s,t) -> Step s, Some t
+ in
+ self#restore ~focus:`Focus target
+
+ method highlight tgt =
match tgt with
| Tactical.Empty | Tactical.Compose _ | Tactical.Multi _ ->
begin
@@ -584,7 +599,7 @@ class pseq
pcond#pp_esequent env fmt s
method pp_goal fmt w =
- Format.fprintf fmt "@\n@{<wp:clause>Goal@} %a:@\n" Wpo.pp_title w ;
+ Format.fprintf fmt "@{<wp:clause>Goal@} %a:@\n" Wpo.pp_title w ;
let _,sequent = Wpo.compute w in
self#pp_sequent fmt sequent
diff --git a/src/plugins/wp/ptip.mli b/src/plugins/wp/ptip.mli
index 38ac0c1bba86edff43d7b5e5dbc63a82c2ef1724..2616b91eca0dc59723bc9fe95d919d0e700fb260 100644
--- a/src/plugins/wp/ptip.mli
+++ b/src/plugins/wp/ptip.mli
@@ -149,7 +149,8 @@ class pseq :
method sequent : Conditions.sequent
method selection : Tactical.selection
- method set_target : Tactical.selection -> unit
+ method set_selection : Tactical.selection -> unit
+ method highlight : Tactical.selection -> unit
method pp_term : F.term printer
method pp_pred : F.pred printer
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index aa5f216834730e120fd970205bda9514730b3d83..f4beb94b109d5d22fa3f753bb5d7bfaeb344c3f2 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -76,7 +76,7 @@ let do_print_current fmt tree =
| `Internal node | `Leaf(_,node) -> do_print_parents fmt node
let do_print_goal_status fmt (g : Wpo.t) =
- if not (Wpo.is_valid g || Wpo.is_smoke_test g) then
+ if not (Wpo.is_fully_valid g || Wpo.is_smoke_test g) then
begin
do_print_index fmt g.po_idx ;
Wpo.pp_goal fmt g ;
@@ -405,7 +405,7 @@ let do_wpo_success ~shell ~cache goal success =
Wp_parameters.feedback ~ontty:`Silent
"[Generated] Goal %s (%a)" (Wpo.get_gid goal) VCS.pp_prover prover
else
- let gui = Frama_c_very_first.Gui_init.is_gui in
+ let gui = Wp_parameters.is_interactive () in
let smoke = Wpo.is_smoke_test goal in
let cstats = ProofEngine.consolidated goal in
let success = Wpo.is_passed goal in
@@ -890,7 +890,7 @@ let () = Cmdline.run_after_setting_files
let () = Cmdline.run_after_configuring_stage Why3Provers.configure
let do_prover_detect () =
- if not Fc_config.is_gui && Wp_parameters.Detect.get () then
+ if Wp_parameters.Detect.get () && not @@ Wp_parameters.is_interactive () then
let provers = Why3Provers.provers () in
if provers = [] then
Wp_parameters.result "No Why3 provers detected."
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index fb612438d63376095cbad85324c2ff2f114cdbd3..71e7be36bbfd89d60f199b51726344c16e3e367e 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -82,6 +82,106 @@ struct
| None -> D.failure "Unknown prover name"
end
+module Provers = D.Jlist(Prover)
+
+let signal = ref None
+let provers = ref None
+
+let getProvers () =
+ match !provers with
+ | Some prvs -> prvs
+ | None ->
+ let cmdline =
+ match Wp_parameters.Provers.get () with
+ | [] -> [ "alt-ergo" ]
+ | prvs -> prvs in
+ let parse s =
+ match VCS.parse_prover s with
+ | None -> None
+ | Some (Qed | Tactical) -> None
+ | Some prv as result -> if VCS.is_auto prv then result else None in
+ let selection = List.filter_map parse cmdline in
+ provers := Some selection ; selection
+
+let updProvers prv = provers := Some prv
+let setProvers prv = updProvers prv ; Option.iter (fun s -> R.emit s) !signal
+
+let () =
+ let s =
+ S.register_state ~package ~name:"provers"
+ ~descr:(Md.plain "Selected Provers")
+ ~data:(module Provers)
+ ~get:getProvers
+ ~set:updProvers ()
+ in signal := Some s
+
+(* -------------------------------------------------------------------------- *)
+(* --- Server Processes --- *)
+(* -------------------------------------------------------------------------- *)
+
+let _ =
+ S.register_state ~package
+ ~name:"process"
+ ~descr:(Md.plain "Server Processes")
+ ~data:(module D.Jint)
+ ~get:Wp_parameters.Procs.get
+ ~set:(fun procs ->
+ Wp_parameters.Procs.set procs ;
+ ignore @@ ProverTask.server ~procs ())
+ ~add_hook:Wp_parameters.Procs.add_hook_on_update ()
+
+(* -------------------------------------------------------------------------- *)
+(* --- Provers Timeout --- *)
+(* -------------------------------------------------------------------------- *)
+
+let _ =
+ S.register_state ~package
+ ~name:"timeout"
+ ~descr:(Md.plain "Prover's Timeout")
+ ~data:(module D.Jint)
+ ~get:Wp_parameters.Timeout.get
+ ~set:Wp_parameters.Timeout.set
+ ~add_hook:Wp_parameters.Timeout.add_hook_on_update ()
+
+(* -------------------------------------------------------------------------- *)
+(* --- Available Provers --- *)
+(* -------------------------------------------------------------------------- *)
+
+let get_name = function
+ | VCS.Qed -> "Qed"
+ | VCS.Tactical -> "Script"
+ | VCS.Why3 p -> Why3Provers.name p
+
+let get_version = function
+ | VCS.Qed | Tactical -> Fc_config.version_and_codename
+ | Why3 p -> Why3Provers.version p
+
+let iter_provers fn =
+ List.iter
+ (fun p ->
+ if Why3Provers.is_auto p && Why3Provers.is_mainstream p then
+ fn (VCS.Why3 p))
+ @@ Why3Provers.provers ()
+
+let _ : VCS.prover S.array =
+ let model = S.model () in
+ S.column ~name:"name" ~descr:(Md.plain "Prover Name")
+ ~data:(module D.Jalpha) ~get:get_name model ;
+ S.column ~name:"version" ~descr:(Md.plain "Prover Version")
+ ~data:(module D.Jalpha) ~get:get_version model ;
+ S.column ~name:"descr" ~descr:(Md.plain "Prover Full Name (description)")
+ ~data:(module D.Jalpha) ~get:(VCS.title_of_prover ~version:true) model ;
+ S.register_array ~package
+ ~name:"ProverInfos" ~descr:(Md.plain "Available Provers")
+ ~key:VCS.name_of_prover
+ ~keyName:"prover"
+ ~keyType:Prover.jtype
+ ~iter:iter_provers model
+
+(* -------------------------------------------------------------------------- *)
+(* --- Results and Stats --- *)
+(* -------------------------------------------------------------------------- *)
+
module Result =
struct
type t = VCS.result
@@ -99,7 +199,7 @@ struct
let to_json (r : VCS.result) = `Assoc [
"descr", `String (Pretty_utils.to_string VCS.pp_result r) ;
"cached", `Bool r.cached ;
- "verdict", `String (VCS.name_of_verdict r.verdict) ;
+ "verdict", `String (VCS.name_of_verdict ~computing:true r.verdict) ;
"solverTime", `Float r.solver_time ;
"proverTime", `Float r.prover_time ;
"proverSteps", `Int r.prover_steps ;
@@ -157,14 +257,6 @@ struct
]
end
-let () = R.register ~package ~kind:`GET ~name:"getAvailableProvers"
- ~descr:(Md.plain "Returns the list of configured provers from why3")
- ~input:(module D.Junit) ~output:(module D.Jlist(Prover))
- (fun () ->
- List.map (fun p -> VCS.Why3 p) @@
- List.filter Why3Provers.is_mainstream @@
- Why3Provers.provers ())
-
(* -------------------------------------------------------------------------- *)
(* --- Goal Array --- *)
(* -------------------------------------------------------------------------- *)
@@ -250,6 +342,11 @@ let () = S.column gmodel ~name:"stats"
~descr:(Md.plain "Prover Stats Summary")
~data:(module STATS) ~get:ProofEngine.consolidated
+let () = S.column gmodel ~name:"proof"
+ ~descr:(Md.plain "Proof Tree")
+ ~data:(module D.Jbool)
+ ~get:ProofEngine.has_proof
+
let () = S.option gmodel ~name:"script"
~descr:(Md.plain "Script File")
~data:(module D.Jstring)
@@ -263,15 +360,25 @@ let () = S.column gmodel ~name:"saved"
~data:(module D.Jbool)
~get:(fun wpo -> ProofEngine.get wpo = `Saved)
-let _ = S.register_array ~package ~name:"goals"
+let filter hook fn = hook (fun g -> if not @@ Wpo.is_tactic g then fn g)
+let (++) h1 h2 fn = h1 fn ; h2 fn
+
+let goals =
+ let add_remove_hook =
+ filter Wpo.add_removed_hook in
+ let add_update_hook =
+ filter Wpo.add_modified_hook ++ ProofEngine.add_goal_hook in
+ let add_reload_hook = Wpo.add_cleared_hook in
+ S.register_array ~package ~name:"goals"
~descr:(Md.plain "Generated Goals")
~key:indexGoal
~keyName:"wpo"
~keyType:Goal.jtype
- ~iter:Wpo.iter_on_goals
- ~add_update_hook:Wpo.add_modified_hook
- ~add_remove_hook:Wpo.add_removed_hook
- ~add_reload_hook:Wpo.add_cleared_hook
+ ~iter:(filter Wpo.iter_on_goals)
+ ~preload:ProofEngine.consolidate
+ ~add_remove_hook
+ ~add_update_hook
+ ~add_reload_hook
gmodel
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpApi.mli b/src/plugins/wp/wpApi.mli
index a2323ddac91d5b7e4a088deab6246f466fad8f67..89db11c333a78558ff655cd9aeaf86a355665dfb 100644
--- a/src/plugins/wp/wpApi.mli
+++ b/src/plugins/wp/wpApi.mli
@@ -27,7 +27,12 @@
val package : Server.Package.package
module Prover : Server.Data.S with type t = VCS.prover
+module Provers : Server.Data.S with type t = VCS.prover list
module Result : Server.Data.S with type t = VCS.result
module Goal : Server.Data.S with type t = Wpo.t
+val goals : Wpo.t Server.States.array
+val getProvers : unit -> VCS.prover list
+val setProvers : VCS.prover list -> unit
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpContext.ml b/src/plugins/wp/wpContext.ml
index 238d6c163ac643dac8ed5d664298ac9d988eb6c0..b940a579c95cdcc6921da6a0edbfc270b591129c 100644
--- a/src/plugins/wp/wpContext.ml
+++ b/src/plugins/wp/wpContext.ml
@@ -173,8 +173,8 @@ sig
val id : basename:string -> key -> string
val mem : key -> bool
- val find : key -> data
val get : key -> data option
+ val find : key -> data
val clear : unit -> unit
val remove : key -> unit
val define : key -> data -> unit
@@ -493,6 +493,7 @@ sig
val mem : key -> bool
val get : key -> data
val set : key -> data -> unit
+ val find : key -> data
val remove : key -> unit
val clear : unit -> unit
end
@@ -509,6 +510,7 @@ struct
type key = D.key
type data = D.data
let get = G.memoize D.compile
+ let find = G.find
let set = G.update
let mem = G.mem
let clear = G.clear
@@ -529,6 +531,7 @@ struct
let get = G.memoize D.compile
let set = G.update
let mem = G.mem
+ let find = G.find
let clear = G.clear
let remove = G.remove
end
@@ -547,6 +550,7 @@ struct
let get = G.memoize (fun k -> D.compile k (G.id ~basename:(D.basename k) k))
let set = G.update
let mem = G.mem
+ let find = G.find
let clear = G.clear
let remove = G.remove
end
@@ -565,6 +569,7 @@ struct
let get = G.memoize (fun k -> D.compile k (G.id ~basename:(D.basename k) k))
let set = G.update
let mem = G.mem
+ let find = G.find
let clear = G.clear
let remove = G.remove
end
diff --git a/src/plugins/wp/wpContext.mli b/src/plugins/wp/wpContext.mli
index c1cd19d4c0f58db0c274a19707e3d2dcdd3e415f..bba749f0a9e4932e38ee560228bf7b09a1b70cf0 100644
--- a/src/plugins/wp/wpContext.mli
+++ b/src/plugins/wp/wpContext.mli
@@ -108,8 +108,8 @@ sig
val id : basename:string -> key -> string
val mem : key -> bool
- val find : key -> data
val get : key -> data option
+ val find : key -> data
val clear : unit -> unit
val remove : key -> unit
val define : key -> data -> unit
@@ -167,6 +167,7 @@ sig
val mem : key -> bool
val get : key -> data
val set : key -> data -> unit
+ val find : key -> data
val remove : key -> unit
val clear : unit -> unit
end
diff --git a/src/plugins/wp/wpTacApi.ml b/src/plugins/wp/wpTacApi.ml
index 8aec7bffc6a821cfcd523ab067e4bc09417a9c80..fc8fed00054113b2e975393eccc114fd4a23f081 100644
--- a/src/plugins/wp/wpTacApi.ml
+++ b/src/plugins/wp/wpTacApi.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
-(* --- Server API for WP --- *)
+(* --- Server API for Tactics --- *)
(* -------------------------------------------------------------------------- *)
module P = Server.Package
@@ -30,22 +30,11 @@ module R = Server.Request
module S = Server.States
module Md = Markdown
module AST = Server.Kernel_ast
+module Jtactic = WpTipApi.Tactic
let package = P.package ~plugin:"wp" ~name:"tac"
~title:"WP Tactics" ()
-(* -------------------------------------------------------------------------- *)
-(* --- Tacticals --- *)
-(* -------------------------------------------------------------------------- *)
-
-module Jtactic : D.S with type t = Tactical.t =
-struct
- type t = Tactical.t
- let jtype = P.Jkey "tactic"
- let to_json (t : Tactical.t) = `String t#id
- let of_json (js : Json.t) = Tactical.lookup ~id:(js |> Json.string)
-end
-
(* -------------------------------------------------------------------------- *)
(* --- Tactical Kind --- *)
(* -------------------------------------------------------------------------- *)
@@ -405,6 +394,7 @@ class configurator (tactic : Tactical.tactical) =
let jtactic = ProofScript.jtactic tactic target in
let fork = ProofEngine.fork tree ~anchor:node jtactic process in
let children = snd @@ ProofEngine.commit fork in
+ ProofEngine.forward tree ;
List.map snd children
with exn ->
local <- None ;
@@ -465,20 +455,35 @@ let tactics =
(* --- Tactical Target Configuration --- *)
(* -------------------------------------------------------------------------- *)
+let configure jtactic node =
+ let sequent = snd @@ Wpo.compute @@ ProofEngine.goal node in
+ match ProofScript.configure jtactic sequent with
+ | None -> ()
+ | Some(tactical,selection) ->
+ begin
+ let console = (configurator tactical :> Tactical.feedback) in
+ console#set_title "%s" tactical#title ;
+ WpTipApi.setSelection node selection ;
+ end
+
let () =
- let configureTactics = R.signature ~output:(module D.Junit) () in
- let get_node = R.param configureTactics ~name:"node"
- ~descr:(Md.plain "Proof node target") (module WpTipApi.Node) in
- R.register_sig ~package ~kind:`EXEC
+ R.register ~package
+ ~kind:`EXEC
~name:"configureTactics"
~descr:(Md.plain "Configure all tactics")
+ ~input:(module WpTipApi.Node)
+ ~output:(module D.Junit)
~signals:[WpTipApi.printStatus]
- configureTactics
- begin fun rq () ->
- let node = get_node rq in
- let selection = WpTipApi.selection node in
- iter (fun cfg -> cfg#configure node selection) ;
- S.reload tactics ;
+ begin fun node ->
+ match ProofEngine.tactical node with
+ | None ->
+ let selection = WpTipApi.selection node in
+ iter (fun cfg -> cfg#configure node selection) ;
+ S.reload tactics ;
+ | Some jtactic ->
+ let ctxt = ProofEngine.node_context node in
+ WpContext.on_context ctxt (configure jtactic) node ;
+ S.reload tactics ;
end
(* -------------------------------------------------------------------------- *)
@@ -528,4 +533,19 @@ let () = R.register
children
end
+let () = R.register
+ ~package ~kind:`EXEC
+ ~name:"applyTacticAndProve"
+ ~descr:(Md.plain "Applies tactic and run provers on children")
+ ~input:(module Jtactic)
+ ~output:(module D.Jlist(WpTipApi.Node))
+ begin fun tactic ->
+ let cfg = configurator tactic in
+ let children = cfg#apply in
+ S.update tactics cfg ;
+ List.iter WpTipApi.runProvers children ;
+ children
+ end
+
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index 256d87982b99c0a9ffe972dd30d9db65fcd2e377..6a686258ec2e012071a4a33250bcf377a89569af 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -24,7 +24,7 @@
(* --- Server API for WP --- *)
(* -------------------------------------------------------------------------- *)
-open WpApi
+module W = WpApi
module P = Server.Package
module D = Server.Data
module R = Server.Request
@@ -36,12 +36,19 @@ let package = P.package ~plugin:"wp" ~name:"tip"
~title:"WP Interactive Prover" ()
(* -------------------------------------------------------------------------- *)
-(* --- Proof Node --- *)
+(* --- Signals --- *)
(* -------------------------------------------------------------------------- *)
let proofStatus = R.signal ~package ~name:"proofStatus"
~descr:(Md.plain "Proof Status has changed")
+let printStatus = R.signal ~package ~name:"printStatus"
+ ~descr:(Md.plain "Updated TIP printer")
+
+(* -------------------------------------------------------------------------- *)
+(* --- Proof Node --- *)
+(* -------------------------------------------------------------------------- *)
+
module Node = D.Index
(Map.Make(ProofEngine.Node))
(struct
@@ -50,9 +57,30 @@ module Node = D.Index
let descr = Md.plain "Proof Node index"
end)
+let () = Server.Main.once
+ begin fun () ->
+ ProofEngine.add_remove_hook Node.remove ;
+ ProofEngine.add_clear_hook (fun _ -> Node.clear ()) ;
+ let signal _ = R.emit proofStatus in
+ ProofEngine.add_update_hook signal ;
+ ProofEngine.add_goal_hook signal ;
+ Wpo.add_modified_hook signal ;
+ end
+
+module Tactic : D.S with type t = Tactical.t =
+struct
+ type t = Tactical.t
+ let jtype = D.declare ~package ~name:"tactic"
+ ~descr:(Md.plain "Tactic identifier") @@ P.Jkey "tactic"
+ let to_json (t : Tactical.t) = `String t#id
+ let of_json (js : Json.t) = Tactical.lookup ~id:(js |> Json.string)
+end
+
+module Path = D.Jlist(Node)
+
let () =
let inode = R.signature ~input:(module Node) () in
- let set_title = R.result inode ~name:"result"
+ let set_title = R.result inode ~name:"title"
~descr:(Md.plain "Proof node title") (module D.Jstring) in
let set_proved = R.result inode ~name:"proved"
~descr:(Md.plain "Proof node complete") (module D.Jbool) in
@@ -64,65 +92,109 @@ let () =
~descr:(Md.plain "Node statistics") (module D.Jstring) in
let set_results = R.result inode ~name:"results"
~descr:(Md.plain "Prover results for current node")
- (module D.Jlist(D.Jpair(Prover)(Result))) in
- let set_tactic = R.result inode ~name:"tactic"
- ~descr:(Md.plain "Proof node tactic header (if any)")
+ (module D.Jlist(D.Jpair(W.Prover)(W.Result))) in
+ let set_tactic = R.result_opt inode ~name:"tactic"
+ ~descr:(Md.plain "Applied tactic (if any)")
+ (module Tactic) in
+ 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"
+ ~descr:(Md.plain "Proof node child label (from parent, if any)")
+ (module D.Jstring) in
+ let set_path = R.result inode ~name:"path"
+ ~descr:(Md.plain "Proof node path from goal")
+ (module Path) in
let set_children = R.result inode ~name:"children"
~descr:(Md.plain "Proof node tactic children (id any)")
- (module D.Jlist(D.Jpair(D.Jstring)(Node))) in
- R.register_sig ~package ~kind:`GET ~name:"getNodeInfos"
- ~descr:(Md.plain "Proof node information") inode
+ (module Path) in
+ R.register_sig inode ~package ~kind:`GET ~name:"getNodeInfos"
+ ~descr:(Md.plain "Proof node information")
~signals:[proofStatus]
begin fun rq node ->
- set_title rq (ProofEngine.title node) ;
- set_proved rq (ProofEngine.proved node) ;
- set_pending rq (ProofEngine.pending node) ;
+ set_title rq (ProofEngine.title node);
+ set_proved rq (ProofEngine.fully_proved node);
+ set_pending rq (ProofEngine.pending node);
let s = ProofEngine.stats node in
- let tactic =
- match ProofEngine.tactical node with
- | None -> ""
- | Some { header } -> header in
- 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 tactic ;
- set_children rq (ProofEngine.children node) ;
+ 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_path rq (ProofEngine.path node);
+ set_children rq (ProofEngine.subgoals node);
+ end
+
+let () =
+ let iresult = R.signature ~output:(module W.Result) () in
+ let get_node = R.param iresult ~name:"node"
+ ~descr:(Md.plain "Proof node") (module Node) in
+ let get_prover = R.param iresult ~name:"prover"
+ ~descr:(Md.plain "Prover") (module W.Prover) in
+ R.register_sig iresult ~package ~kind:`GET ~name:"getResult"
+ ~descr:(Md.plain "Result for specified node and prover")
+ ~signals:[proofStatus]
+ begin fun rq () ->
+ let node = get_node rq in
+ let prover = get_prover rq in
+ Wpo.get_result (ProofEngine.goal node) prover
end
(* -------------------------------------------------------------------------- *)
-(* --- Proof Tree --- *)
+(* --- Proof Cursor --- *)
(* -------------------------------------------------------------------------- *)
let () =
- let state = R.signature ~input:(module Goal) () in
- let set_current = R.result state ~name:"current"
- ~descr:(Md.plain "Current proof node") (module Node) in
- let set_path = R.result state ~name:"path"
- ~descr:(Md.plain "Proof node parents") (module D.Jlist(Node)) in
+ let state = R.signature ~input:(module W.Goal) () in
let set_index = R.result state ~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"
~descr:(Md.plain "Pending proof nodes") (module D.Jint) in
+ let set_current = R.result state ~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)")
+ (module Path) in
+ let set_tactic = R.result_opt state ~name:"tactic"
+ ~descr:(Md.plain "Applied tactic (if any)")
+ (module Tactic) in
R.register_sig ~package
- ~kind:`GET ~name:"getProofState"
+ ~kind:`GET ~name:"getProofStatus"
~descr:(Md.plain "Current Proof Status of a Goal") state
~signals:[proofStatus]
begin fun rq wpo ->
- let tree = ProofEngine.proof ~main:wpo in
- let current,index =
+ let tree = ProofEngine.proof ~main:wpo in
+ let root = ProofEngine.root tree in
+ set_pending rq (ProofEngine.pending root) ;
+ let current, index =
match ProofEngine.current tree with
- | `Main -> ProofEngine.root tree,-1
- | `Internal node -> node,-1
- | `Leaf(idx,node) -> node,idx in
- let rec path node = match ProofEngine.parent node with
- | None -> []
- | Some p -> p::path p in
- set_current rq current ;
- set_path rq (path current) ;
+ | `Main -> root, -1
+ | `Internal node -> node, -1
+ | `Leaf(idx,node) -> node, idx
+ in
set_index rq index ;
- set_pending rq (ProofEngine.pending current) ;
+ set_current rq 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
end
(* -------------------------------------------------------------------------- *)
@@ -131,29 +203,26 @@ let () =
let () = R.register ~package ~kind:`SET ~name:"goForward"
~descr:(Md.plain "Go to to first pending node, or root if none")
- ~input:(module Goal) ~output:(module D.Junit)
+ ~input:(module W.Goal) ~output:(module D.Junit)
begin fun goal ->
let tree = ProofEngine.proof ~main:goal in
ProofEngine.forward tree ;
- R.emit proofStatus ;
end
let () = R.register ~package ~kind:`SET ~name:"goToRoot"
~descr:(Md.plain "Go to root of proof tree")
- ~input:(module Goal) ~output:(module D.Junit)
+ ~input:(module W.Goal) ~output:(module D.Junit)
begin fun goal ->
let tree = ProofEngine.proof ~main:goal in
ProofEngine.goto tree `Main ;
- R.emit proofStatus ;
end
let () = R.register ~package ~kind:`SET ~name:"goToIndex"
~descr:(Md.plain "Go to k-th pending node of proof tree")
- ~input:(module D.Jpair(Goal)(D.Jint)) ~output:(module D.Junit)
+ ~input:(module D.Jpair(W.Goal)(D.Jint)) ~output:(module D.Junit)
begin fun (goal,index) ->
let tree = ProofEngine.proof ~main:goal in
ProofEngine.goto tree (`Leaf index) ;
- R.emit proofStatus ;
end
let () = R.register ~package ~kind:`SET ~name:"goToNode"
@@ -162,16 +231,38 @@ let () = R.register ~package ~kind:`SET ~name:"goToNode"
begin fun node ->
let tree = ProofEngine.tree node in
ProofEngine.goto tree (`Node node) ;
- R.emit proofStatus ;
end
-let () = R.register ~package ~kind:`SET ~name:"removeNode"
- ~descr:(Md.plain "Remove node from tree and go to parent")
+let () = R.register ~package ~kind:`SET ~name:"clearNode"
+ ~descr:(Md.plain "Cancel all node results and sub-tree (if any)")
+ ~input:(module Node) ~output:(module D.Junit)
+ begin fun node ->
+ let tree = ProofEngine.tree node in
+ ProofEngine.clear_node tree node ;
+ end
+
+let () = R.register ~package ~kind:`SET ~name:"clearNodeTactic"
+ ~descr:(Md.plain "Cancel node current tactic")
~input:(module Node) ~output:(module D.Junit)
begin fun node ->
let tree = ProofEngine.tree node in
- ProofEngine.remove tree node ;
- R.emit proofStatus ;
+ ProofEngine.clear_node_tactic tree node ;
+ end
+
+let () = R.register ~package ~kind:`SET ~name:"clearParentTactic"
+ ~descr:(Md.plain "Cancel parent node tactic")
+ ~input:(module Node) ~output:(module D.Junit)
+ begin fun node ->
+ let tree = ProofEngine.tree node in
+ ProofEngine.clear_parent_tactic tree node ;
+ end
+
+let () = R.register ~package ~kind:`SET ~name:"clearGoal"
+ ~descr:(Md.plain "Remove the complete goal proof tree")
+ ~input:(module W.Goal) ~output:(module D.Junit)
+ begin fun goal ->
+ let tree = ProofEngine.proof ~main:goal in
+ ProofEngine.clear_tree tree ;
end
(* -------------------------------------------------------------------------- *)
@@ -259,9 +350,6 @@ class printer () : Ptip.pseq =
(* --- Printer Registry --- *)
(* -------------------------------------------------------------------------- *)
-let printStatus = R.signal ~package ~name:"printStatus"
- ~descr:(Md.plain "Updated TIP printer")
-
module PRINTER = State_builder.Ref
(Datatype.Make
(struct
@@ -287,17 +375,17 @@ let () = Wpo.add_cleared_hook
let registry = PRINTER.get () in
Hashtbl.clear registry)
-let lookup_printer (node : ProofEngine.node) : printer =
+let lookup (node : ProofEngine.node) : printer =
let tree = ProofEngine.tree node in
let wpo = ProofEngine.main tree in
let registry = PRINTER.get () in
try Hashtbl.find registry wpo.po_gid with Not_found ->
let pp = new printer () in
+ pp#on_selection (fun () -> R.emit printStatus) ;
Hashtbl.add registry wpo.po_gid pp ; pp
-let selection node =
- let pp = lookup_printer node in
- pp#selection
+let selection node = (lookup node)#selection
+let setSelection node = (lookup node)#set_selection
(* -------------------------------------------------------------------------- *)
(* --- PrintSequent Request --- *)
@@ -344,7 +432,7 @@ let () =
match get_node rq with
| None -> D.jtext ""
| Some node ->
- let pp = lookup_printer node in
+ let pp = lookup node in
let indent = get_indent rq in
let margin = get_margin rq in
Option.iter pp#set_iformat (get_iformat rq) ;
@@ -366,10 +454,9 @@ let () =
~input:(module Node)
~output:(module D.Junit)
begin fun node ->
- let pp = lookup_printer node in
+ let pp = lookup node in
pp#reset ;
pp#selected ;
- R.emit printStatus
end
let () =
@@ -393,10 +480,9 @@ let () =
let part = get_part rq in
let term = get_term rq in
let extend = get_extend rq in
- let pp = lookup_printer node in
+ let pp = lookup node in
let part = to_part (fst pp#sequent) part in
pp#restore ~focus:(if extend then `Extend else `Focus) (part,term) ;
- R.emit printStatus
end
let () =
@@ -409,12 +495,193 @@ let () =
~kind:`GET
~name:"getSelection"
~descr:(Md.plain "Get current selection in proof node")
- ~signals:[printStatus]
+ ~signals:[printStatus;proofStatus]
getSelection
begin fun rq node ->
- let (part,term) = (lookup_printer node)#target in
+ let (part,term) = (lookup node)#target in
set_part rq (if part <> Term then Some (of_part part) else None);
set_term rq term;
end
(* -------------------------------------------------------------------------- *)
+(* --- Prover Scheduling --- *)
+(* -------------------------------------------------------------------------- *)
+
+let runProvers ?timeout ?provers node =
+ let wpo = ProofEngine.goal node in
+ let provers = match provers with
+ | Some ps -> ps
+ | None -> WpApi.getProvers () in
+ let timeout = match timeout with
+ | Some t -> t
+ | None -> Wp_parameters.Timeout.get () in
+ let config =
+ let cfg = VCS.current () in
+ { cfg with timeout = Some (float timeout) } in
+ if not @@ Wpo.is_trivial wpo then
+ List.iter
+ (fun prv ->
+ let backup = Wpo.get_result wpo prv in
+ let result _ p r =
+ if p = VCS.Qed && VCS.is_valid r then
+ Wpo.set_result wpo prv VCS.no_result
+ else if not @@ VCS.is_verdict r then
+ Wpo.set_result wpo prv backup in
+ let process () = Prover.prove ~config ~result wpo prv in
+ let thread = Task.thread @@ Task.later process () in
+ let status = VCS.computing (fun () -> Task.cancel thread) in
+ Wpo.set_result wpo prv status ;
+ let server = ProverTask.server () in
+ Task.spawn server thread ;
+ Task.launch server ;
+ ) provers
+
+let () =
+ let iRunProvers = R.signature ~output:(module D.Junit) () in
+ let get_node = R.param iRunProvers (module Node)
+ ~name:"node" ~descr:(Md.plain "Proof node") in
+ let get_timeout = R.param_opt iRunProvers (module D.Jint)
+ ~name:"timeout"
+ ~descr:(Md.plain "Prover timeout (in seconds, default: current)") in
+ let get_provers = R.param_opt iRunProvers (module WpApi.Provers)
+ ~name:"provers"
+ ~descr:(Md.plain "Prover selection (default: current") in
+ R.register_sig iRunProvers ~package ~kind:`SET
+ ~name:"runProvers"
+ ~descr:(Md.plain "Schedule provers on proof node")
+ begin fun rq () ->
+ let node = get_node rq in
+ let provers = get_provers rq in
+ let timeout = get_timeout rq in
+ runProvers ?timeout ?provers node
+ end
+
+let killProvers ?provers node =
+ let wpo = ProofEngine.goal node in
+ let filter =
+ match provers with
+ | None | Some [] -> fun _ -> true
+ | Some prvs -> fun p -> List.exists (VCS.eq_prover p) prvs
+ in
+ List.iter
+ (fun (prv,res) ->
+ match res.VCS.verdict with
+ | Computing kill when filter prv -> kill ()
+ | _ -> ()
+ ) @@ Wpo.get_results wpo
+
+let () =
+ let iKillProvers = R.signature ~output:(module D.Junit) () in
+ let get_node = R.param iKillProvers (module Node)
+ ~name:"node" ~descr:(Md.plain "Proof node") in
+ let get_provers = R.param_opt iKillProvers (module WpApi.Provers)
+ ~name:"provers"
+ ~descr:(Md.plain "Prover selection (default: all running provers") in
+ R.register_sig iKillProvers ~package ~kind:`SET
+ ~name:"killProvers"
+ ~descr:(Md.plain "Interrupt running provers on proof node")
+ begin fun rq () ->
+ let node = get_node rq in
+ let provers = get_provers rq in
+ killProvers ?provers node
+ end
+
+let clearProvers ?provers node =
+ let wpo = ProofEngine.goal node in
+ let clear p = if VCS.is_extern p then Wpo.set_result wpo p VCS.no_result in
+ begin
+ match provers with
+ | None -> List.iter (fun (prv,_) -> clear prv) @@ Wpo.get_results wpo ;
+ | Some prvs -> List.iter clear prvs
+ end
+
+let () =
+ let iClearProvers = R.signature ~output:(module D.Junit) () in
+ let get_node = R.param iClearProvers (module Node)
+ ~name:"node" ~descr:(Md.plain "Proof node") in
+ let get_provers = R.param_opt iClearProvers (module WpApi.Provers)
+ ~name:"provers"
+ ~descr:(Md.plain "Prover selection (default: all results") in
+ R.register_sig iClearProvers ~package ~kind:`SET
+ ~name:"clearProvers"
+ ~descr:(Md.plain "Remove prover results from proof node")
+ begin fun rq () ->
+ let node = get_node rq in
+ let provers = get_provers rq in
+ clearProvers ?provers node
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Script Management --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () =
+ let script = R.signature ~input:(module WpApi.Goal) () in
+ let set_proof = R.result script (module D.Jbool)
+ ~name:"proof" ~descr:(Md.plain "Some Proof Tree can be Saved") in
+ let set_script = R.result_opt script (module D.Jstring)
+ ~name:"script" ~descr:(Md.plain "Script File (if any)") in
+ let set_saved = R.result script (module D.Jbool)
+ ~name:"saved" ~descr:(Md.plain "Current Proof Script has been Saved") in
+ R.register_sig script ~package ~kind:`GET
+ ~name:"getScriptStatus"
+ ~descr:(Md.plain "Script Status for a given Goal")
+ ~signals:[proofStatus]
+ begin fun rq goal ->
+ let tree = ProofEngine.proof ~main:goal in
+ set_saved rq (ProofEngine.saved tree) ;
+ set_proof rq (ProofEngine.has_script tree) ;
+ set_script rq
+ begin
+ match ProofSession.get goal with
+ | NoScript -> None | Script file | Deprecated file ->
+ Some (file :> string)
+ end ;
+ end
+
+let () =
+ R.register ~package ~kind:`SET
+ ~name:"saveScript" ~descr:(Md.plain "Save Script for the Goal")
+ ~input:(module WpApi.Goal)
+ ~output:(module D.Junit)
+ begin fun goal ->
+ let tree = ProofEngine.proof ~main:goal in
+ let json = ProofScript.encode (ProofEngine.script tree) in
+ ProofSession.save ~stdout:false goal json ;
+ ProofEngine.set_saved tree true ;
+ end
+
+let () =
+ R.register ~package ~kind:`SET
+ ~name:"runScript"
+ ~descr:(Md.plain "Replay Saved Script for the Goal (if any)")
+ ~input:(module WpApi.Goal)
+ ~output:(module D.Junit)
+ begin fun goal ->
+ let tree = ProofEngine.proof ~main:goal in
+ ProofEngine.clear_tree tree ;
+ ProverScript.spawn
+ ~provers:(WpApi.getProvers())
+ ~success:(fun _ _ -> ProofEngine.forward tree)
+ goal ;
+ let server = ProverTask.server () in
+ Task.launch server ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Full Trash --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () =
+ R.register ~package ~kind:`SET
+ ~name:"clearProofScript"
+ ~descr:(Md.plain "Clear Proof and Remove any Saved Script for the Goal")
+ ~input:(module WpApi.Goal)
+ ~output:(module D.Junit)
+ begin fun goal ->
+ let tree = ProofEngine.proof ~main:goal in
+ ProofEngine.clear_tree tree ;
+ ProofSession.remove goal ;
+ end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpTipApi.mli b/src/plugins/wp/wpTipApi.mli
index 7ffb03f69460e1812662c498ac389f19d700aa87..89461a68543d9ccbf65c4ff49b2732c151266140 100644
--- a/src/plugins/wp/wpTipApi.mli
+++ b/src/plugins/wp/wpTipApi.mli
@@ -25,8 +25,24 @@
(* -------------------------------------------------------------------------- *)
module Node : Server.Data.S with type t = ProofEngine.node
+module Tactic : Server.Data.S with type t = Tactical.t
+val proofStatus : Server.Request.signal
val printStatus : Server.Request.signal
val selection : ProofEngine.node -> Tactical.selection
+val setSelection : ProofEngine.node -> Tactical.selection -> unit
+
+val runProvers :
+ ?timeout:int ->
+ ?provers:VCS.prover list ->
+ ProofEngine.node -> unit
+
+val killProvers :
+ ?provers:VCS.prover list ->
+ ProofEngine.node -> unit
+
+val clearProvers :
+ ?provers:VCS.prover list ->
+ ProofEngine.node -> unit
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 8eab81d849685d385cb46cb915e8370ae914f8b5..88cdfd069baf8bd39d04844d7c9a4d934d747f87 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -45,6 +45,10 @@ let on_reset f = resetdemon := f :: !resetdemon
let reset () = List.iter (fun f -> f ()) !resetdemon
let has_dkey (k:category) = is_debug_key_enabled k
+let server = ref false
+let () = Server.Main.once (fun () -> server := true)
+let is_interactive () = Fc_config.is_gui || !server
+
(* ------------------------------------------------------------------------ *)
(* --- WP Generation --- *)
(* ------------------------------------------------------------------------ *)
@@ -1220,17 +1224,13 @@ let base_output () =
let output =
let dir = OutputDir.get () in
if Fc_Filepath.Normalized.is_empty dir then
- if Fc_config.is_gui
+ if is_interactive ()
then make_gui_dir ()
else make_tmp_dir ()
- else begin
- make_output_dir dir ;
- dir
- end
- in
+ else
+ ( make_output_dir dir ; dir ) in
base_output := Some output;
- Fc_Filepath.(add_symbolic_dir "WPOUT" output) ;
- output
+ Fc_Filepath.add_symbolic_dir "WPOUT" output ; output
| Some output -> output
let get_output () =
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 02ddb77250bba27096a59804668363c1282a48a6..9a00ddf2b3acfb3a39ce18fcd051c43865cebb37 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -24,6 +24,7 @@ include Plugin.S
val reset : unit -> unit
val hypothesis : 'a Log.pretty_printer
+val is_interactive : unit -> bool
(** {2 Function Selection} *)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 7dc808882fd5efbe61ff6ccc72cef48d287013f5..a213a36292b037cdd639a3723327b8a64bf6e65a 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -453,27 +453,28 @@ struct
mutable dps : result Pmap.t ;
}
- let not_computing _ r =
- match r.verdict with VCS.Computing _ -> false | _ -> true
-
let create () = { dps = Pmap.empty }
let get w p =
Pmap.find p w.dps
- let clear w = w.dps <- Pmap.empty
+ let clear w =
+ Pmap.iter (fun _ r ->
+ match r.verdict with
+ | VCS.Computing kill -> kill ()
+ | _ -> ()
+ ) w.dps ;
+ w.dps <- Pmap.empty
let replace w p r =
begin
if p = Qed then
- begin
- w.dps <- Pmap.filter not_computing w.dps ;
- end ;
+ (w.dps <- Pmap.filter (fun _ r -> VCS.is_verdict r) w.dps) ;
w.dps <- Pmap.add p r w.dps
end
let list w =
- List.filter (fun (_,r) -> VCS.is_verdict r) @@ Pmap.bindings w.dps
+ List.filter (fun (_,r) -> not @@ VCS.is_none r) @@ Pmap.bindings w.dps
end
@@ -725,9 +726,12 @@ let get_result g p : VCS.result =
let get_results g =
let system = SYSTEM.get () in
- try Results.list (WPOmap.find g system.results)
+ try Results.list @@ WPOmap.find g system.results
with Not_found -> []
+let get_prover_results g =
+ List.filter (fun (p,_) -> VCS.is_prover p) @@ get_results g
+
let is_trivial g =
VC_Annot.is_trivial g.po_formula
@@ -754,23 +758,28 @@ let compute g =
let seq = WpContext.on_context ctxt (GOAL.compute_descr ~pid) goal in
if not qed then modified g ; seq
-let is_valid g =
- is_trivial g || List.exists (fun (_,r) -> VCS.is_valid r) (get_results g)
+let is_fully_valid g =
+ is_trivial g ||
+ List.exists (fun (_,r) -> VCS.is_valid r) @@ get_results g
+
+let is_locally_valid g =
+ is_trivial g ||
+ List.exists (fun (p,r) -> VCS.is_prover p && VCS.is_valid r) @@ get_results g
let all_not_valid g =
not (is_trivial g) &&
- List.for_all (fun (_,r) -> VCS.is_not_valid r) (get_results g)
+ List.for_all (fun (_,r) -> VCS.is_not_valid r) @@ get_results g
let is_passed g =
if is_smoke_test g then
all_not_valid g
else
- is_valid g
+ is_fully_valid g
let has_unknown g =
- not (is_valid g) &&
+ not (is_fully_valid g) &&
List.exists
- (fun (_,r) -> VCS.is_verdict r && not (VCS.is_valid r))
+ (fun (p,r) -> VCS.is_prover p && VCS.is_verdict r && not (VCS.is_valid r))
(get_results g)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index 6838763a3c5c734aff5bff71246636ddc1b80c0c..b781e4e72cf9a9c400078ba918f70d81e5a0b9b1 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -150,9 +150,12 @@ val has_verdict : t -> prover -> bool
(** Raw prover result (without any respect to smoke tests) *)
val get_result : t -> prover -> result
-(** All raw prover results (without any respect to smoke tests) *)
+(** Return all results (without any respect to smoke tests). *)
val get_results : t -> (prover * result) list
+(** Return all prover results (without any respect to smoke tests). *)
+val get_prover_results : t -> (prover * result) list
+
(** Consolidated wrt to associated property and smoke test. *)
val get_proof : t -> [`Passed|`Failed|`Unknown] * Property.t
@@ -162,8 +165,11 @@ val get_target : t -> Property.t
val is_trivial : t -> bool
(** Currently trivial sequent (no forced simplification) *)
-val is_valid : t -> bool
-(** Checks for some prover with valid verdict (no forced simplification) *)
+val is_fully_valid : t -> bool
+(** Checks for some prover or script with valid verdict (no forced qed) *)
+
+val is_locally_valid : t -> bool
+(** Checks for some prover (no tactic) with valid verdict (no forced qed) *)
val all_not_valid : t -> bool
(** Checks for all provers to give a non-valid, computed verdict *)