diff --git a/ivette/src/dome/renderer/frame/toolbars.tsx b/ivette/src/dome/renderer/frame/toolbars.tsx
index eebb53c3d73861bf0fe7873e79fafbae3cadb556..a824168884bdd63fd4ed9d38fa53650c132b3060 100644
--- a/ivette/src/dome/renderer/frame/toolbars.tsx
+++ b/ivette/src/dome/renderer/frame/toolbars.tsx
@@ -229,6 +229,7 @@ export function Switch(props: SwitchProps): JSX.Element | null {
// --------------------------------------------------------------------------
export interface SelectionProps<A> {
+ title?: string;
/** Enabled Group (default `true`). */
enabled?: boolean;
/** Disabled Group (default `false`). */
@@ -295,6 +296,7 @@ export function Select(props: SelectionProps<string>): JSX.Element {
return (
<select
className="dome-xToolBar-control dome-color-frame"
+ title={props.title}
value={props.value}
disabled={disabled || !enabled}
onChange={callback}
diff --git a/ivette/src/dome/renderer/table/views.tsx b/ivette/src/dome/renderer/table/views.tsx
index d2e29169c2af9106dc3c346ef7d70827dce311e7..3e40f7a12e1c0ff658050d2a82d8aa175f194d22 100644
--- a/ivette/src/dome/renderer/table/views.tsx
+++ b/ivette/src/dome/renderer/table/views.tsx
@@ -181,6 +181,8 @@ export interface TableProps<Key, Row> {
selection?: Key;
/** Selection callback. */
onSelection?: (row: Row, key: Key, index: number) => void;
+ /** Double click callback. */
+ onDoubleClick?: (row: Row, index: number) => void;
/** Context menu callback. */
onContextMenu?: (row: Row, index: number) => void;
/** Fallback for rendering an empty table. */
@@ -337,6 +339,8 @@ class TableState<Key, Row> {
selectedIndex?: number; // Current selected index
sortBy?: string; // last sorting dataKey
sortDirection?: SortDirectionType; // last sorting direction
+ onSelection?: (data: Row, key: Key, index: number) => void; // main callback
+ onDoubleClick?: (row: Row, index: number) => void; // double click callback
onContextMenu?: (row: Row, index: number) => void; // context menu callback
range?: IndexRange;
rowCount = 0;
@@ -350,6 +354,7 @@ class TableState<Key, Row> {
this.rowClassName = this.rowClassName.bind(this);
this.onHeaderMenu = this.onHeaderMenu.bind(this);
this.onRowClick = this.onRowClick.bind(this);
+ this.onRowDoubleClick = this.onRowDoubleClick.bind(this);
this.onRowRightClick = this.onRowRightClick.bind(this);
this.onKeyDown = this.onKeyDown.bind(this);
this.onSorting = this.onSorting.bind(this);
@@ -363,6 +368,7 @@ class TableState<Key, Row> {
this.signal = undefined;
this.onSelection = undefined;
this.onContextMenu = undefined;
+ this.onDoubleClick = undefined;
}
forceUpdate(): void {
@@ -509,8 +515,6 @@ class TableState<Key, Row> {
// ---- Selection Management
- onSelection?: (data: Row, key: Key, index: number) => void;
-
onRowClick(info: RowMouseEventHandlerParams): void {
const { index } = info;
const data = info.rowData as (Row | undefined);
@@ -529,7 +533,8 @@ class TableState<Key, Row> {
rowClassName({ index }: Index): string {
if (this.selectedIndex === index) return 'dome-xTable-selected';
- return (index & 1 ? 'dome-xTable-even' : 'dome-xTable-odd'); // eslint-disable-line no-bitwise
+ // eslint-disable-next-line no-bitwise
+ return (index & 1 ? 'dome-xTable-even' : 'dome-xTable-odd');
}
keyStepper(index: number): void {
@@ -563,7 +568,17 @@ class TableState<Key, Row> {
// ---- Row Events
- onRowRightClick({ event, rowData, index }: RowMouseEventHandlerParams): void {
+ onRowDoubleClick({ event, rowData, index }: RowMouseEventHandlerParams): void
+ {
+ const callback = this.onDoubleClick;
+ if (callback) {
+ event.stopPropagation();
+ callback(rowData, index);
+ }
+ }
+
+ onRowRightClick({ event, rowData, index }: RowMouseEventHandlerParams): void
+ {
const callback = this.onContextMenu;
if (callback) {
event.stopPropagation();
@@ -1092,6 +1107,7 @@ function makeTable<Key, Row>(
headerRowRenderer={headerRowRenderer}
onRowsRendered={state.onRowsRendered}
onRowClick={state.onRowClick}
+ onRowDoubleClick={state.onRowDoubleClick}
onRowRightClick={state.onRowRightClick}
sortBy={state.sortBy}
sortDirection={state.sortDirection}
@@ -1152,6 +1168,7 @@ export function Table<Key, Row>(props: TableProps<Key, Row>): JSX.Element {
state.setSorting(props.sorting);
state.setRendering(props.rendering);
state.onSelection = props.onSelection;
+ state.onDoubleClick = props.onDoubleClick;
state.onContextMenu = props.onContextMenu;
return state.unwind;
});
diff --git a/ivette/src/dome/renderer/text/editor.tsx b/ivette/src/dome/renderer/text/editor.tsx
index 6c0254593d4ada245d8482c3776ab346406deb7b..a2bfc2004bcab29a85f50fb0a9d8395ad042b2ab 100644
--- a/ivette/src/dome/renderer/text/editor.tsx
+++ b/ivette/src/dome/renderer/text/editor.tsx
@@ -488,13 +488,11 @@ export function selectLine(
): void {
if (!view || view.state.doc.lines < line) return;
const doc = view.state.doc;
- const { from: here } = doc.lineAt(view.state.selection.main.from);
- const { from: goto } = doc.line(Math.max(line, 1));
- if (focus) view.dispatch({ selection: { anchor: goto } });
- if (here === goto) return;
+ const { from: anchor } = doc.line(Math.max(line, 1));
+ if (focus) view.dispatch({ selection: { anchor } });
if (isVisible(view, line)) return;
const verticalScroll = atTop ? 'start' : 'center';
- const effects = EditorView.scrollIntoView(goto, { y: verticalScroll });
+ const effects = EditorView.scrollIntoView(anchor, { y: verticalScroll });
view.dispatch({ effects });
}
diff --git a/ivette/src/dome/renderer/text/richtext.tsx b/ivette/src/dome/renderer/text/richtext.tsx
index 674f49f0e50c036620013ac169531b16ae3f5297..03859f53447d43b877d70910a16cf0b431fbf111 100644
--- a/ivette/src/dome/renderer/text/richtext.tsx
+++ b/ivette/src/dome/renderer/text/richtext.tsx
@@ -114,7 +114,8 @@ class DiffBuffer {
function updateContents(view: CM.EditorView, newText: string): void {
const buffer = new DiffBuffer();
diffLines(view.state.doc.toString(), newText).forEach(buffer.add);
- view.dispatch({ changes: buffer.flush() });
+ const changes = buffer.flush();
+ view.dispatch({ changes });
}
/* -------------------------------------------------------------------------- */
@@ -641,7 +642,7 @@ export interface GutterDecoration extends LineDecoration {
}
export type Decoration = MarkDecoration | LineDecoration | GutterDecoration;
-export type Decorations = null | Decoration | readonly Decoration[];
+export type Decorations = null | Decoration | readonly Decorations[];
/* -------------------------------------------------------------------------- */
/* --- Decoration Builder --- */
@@ -814,17 +815,6 @@ interface Decorator {
gutters : CS.RangeSet<CM.GutterMarker>;
}
-function compareDecorations(a : Decorations, b : Decorations): boolean
-{
- if (a === b) return true;
- if (!Array.isArray(a)) return false;
- if (!Array.isArray(b)) return false;
- const n = a.length;
- if (n !== b.length) return false;
- for (let k = 0; k < n; k++) if (a[k] !== b[k]) return false;
- return true;
-}
-
const DecoratorSpec = CS.Annotation.define<Decorations>();
const DecoratorState = CS.StateField.define<Decorator>({
@@ -837,7 +827,7 @@ const DecoratorState = CS.StateField.define<Decorator>({
update(value: Decorator, tr: CS.Transaction) {
const newSpec : Decorations = tr.annotation(DecoratorSpec) ?? null;
- if (newSpec !== null && !compareDecorations(newSpec, value.spec)) {
+ if (newSpec !== null) {
const builder = new DecorationsBuilder(tr.newDoc);
builder.addSpec(newSpec);
return {
@@ -912,7 +902,7 @@ function createView(parent: Element): CM.EditorView {
/* -------------------------------------------------------------------------- */
export interface TextViewProps {
- text?: TextProxy;
+ text?: TextProxy | string;
readOnly?: boolean;
onChange?: Callback;
selection?: Range;
@@ -938,10 +928,13 @@ export function TextView(props: TextViewProps) : JSX.Element {
// --- Text Proxy
const { text } = props;
React.useEffect(() => {
- if (text) {
+ if (text instanceof TextProxy) {
text.connect(view);
if (view) return () => text.connect(null);
}
+ if (typeof(text)==='string' && view) {
+ dispatchContents(view, text);
+ }
return undefined;
}, [text, view]);
diff --git a/ivette/src/frama-c/kernel/api/properties/index.ts b/ivette/src/frama-c/kernel/api/properties/index.ts
index 7103e001bbf796b192369a4bbc6a9177ee19445d..da82af1774b8290511d55975a7f7a57716b1abee 100644
--- a/ivette/src/frama-c/kernel/api/properties/index.ts
+++ b/ivette/src/frama-c/kernel/api/properties/index.ts
@@ -140,6 +140,8 @@ export enum propKind {
check_lemma = 'check_lemma',
/** ACSL extension */
extension = 'extension',
+ /** Generic Property */
+ generic = 'generic',
}
/** Decoder for `propKind` */
diff --git a/ivette/src/frama-c/plugins/eva/api/values/index.ts b/ivette/src/frama-c/plugins/eva/api/values/index.ts
index 652447eeab0359dc124d20a8336bb5125569ef59..26435c8173c9a2c32c156f992225a67d0f8dc7a7 100644
--- a/ivette/src/frama-c/plugins/eva/api/values/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/values/index.ts
@@ -59,18 +59,19 @@ export const changed: Server.Signal = {
name: 'plugins.eva.values.changed',
};
-export type callstack = Json.index<'#eva-callstack-id'>;
+/** Callstack identifier */
+export type callstack = Json.index<'#callstack'>;
/** Decoder for `callstack` */
export const jCallstack: Json.Decoder<callstack> =
- Json.jIndex<'#eva-callstack-id'>('#eva-callstack-id');
+ Json.jIndex<'#callstack'>('#callstack');
/** Natural order for `callstack` */
export const byCallstack: Compare.Order<callstack> = Compare.number;
/** Default value for `callstack` */
export const callstackDefault: callstack =
- Json.jIndex<'#eva-callstack-id'>('#eva-callstack-id')(-1);
+ Json.jIndex<'#callstack'>('#callstack')(-1);
/** Call site infos */
export type callsite =
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index 18aff5d59f41c6ffbe0531d327255d6b29cb231c..5e73797a2f571719550adfa4714fdb0b2c4391b3 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -181,10 +181,12 @@ export const getAvailableProvers: Server.GetRequest<null,prover[]>= getAvailable
export interface goalsData {
/** Entry identifier. */
wpo: goal;
- /** Property Marker */
- property: marker;
+ /** Associated Marker */
+ marker: marker;
/** Associated declaration, if any */
scope?: decl;
+ /** Property Marker */
+ property: marker;
/** Associated function name, if any */
fct?: string;
/** Associated behavior name, if any */
@@ -211,8 +213,9 @@ export interface goalsData {
export const jGoalsData: Json.Decoder<goalsData> =
Json.jObject({
wpo: jGoal,
- property: jMarker,
+ marker: jMarker,
scope: Json.jOption(jDecl),
+ property: jMarker,
fct: Json.jOption(Json.jString),
bhv: Json.jOption(Json.jString),
thy: Json.jOption(Json.jString),
@@ -228,12 +231,14 @@ export const jGoalsData: Json.Decoder<goalsData> =
/** Natural order for `goalsData` */
export const byGoalsData: Compare.Order<goalsData> =
Compare.byFields
- <{ wpo: goal, property: marker, scope?: decl, fct?: string, bhv?: string,
- thy?: string, name: string, smoke: boolean, passed: boolean,
- status: status, stats: stats, script?: string, saved: boolean }>({
+ <{ 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 }>({
wpo: byGoal,
- property: byMarker,
+ marker: byMarker,
scope: Compare.defined(byDecl),
+ property: byMarker,
fct: Compare.defined(Compare.string),
bhv: Compare.defined(Compare.string),
thy: Compare.defined(Compare.string),
@@ -295,10 +300,10 @@ export const goals: State.Array<goal,goalsData> = goals_internal;
/** Default value for `goalsData` */
export const goalsDataDefault: goalsData =
- { wpo: goalDefault, property: markerDefault, scope: undefined,
- fct: undefined, bhv: undefined, thy: undefined, name: '', smoke: false,
- passed: false, status: statusDefault, stats: statsDefault,
- script: undefined, saved: false };
+ { 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 };
/** 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 b39fef289e3cf56bf3093f04bd01f0da82030c82..ee290243ed1d4610fe4ce2b696a50a7522296b46 100644
--- a/ivette/src/frama-c/plugins/wp/api/tac/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tac/index.ts
@@ -37,6 +37,14 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
+//@ts-ignore
+import { byNode } from 'frama-c/plugins/wp/api/tip';
+//@ts-ignore
+import { jNode } 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';
/** Parameter kind */
export type kind =
@@ -256,31 +264,25 @@ export const tacticalDataDefault: tacticalData =
{ id: Json.jKey<'#tactic'>('#tactic')(''), label: '', title: '',
error: undefined, status: statusDefault, params: [] };
-const configureTactics_internal: Server.ExecRequest<
- { node: Json.index<'#node'> },
- null
- > = {
+const configureTactics_internal: Server.ExecRequest<{ node: node },null> = {
kind: Server.RqKind.EXEC,
name: 'plugins.wp.tac.configureTactics',
- input: Json.jObject({ node: Json.jIndex<'#node'>('#node'),}),
+ input: Json.jObject({ node: jNode,}),
output: Json.jNull,
signals: [ { name: 'plugins.wp.tip.printStatus' } ],
};
/** Configure all tactics */
-export const configureTactics: Server.ExecRequest<
- { node: Json.index<'#node'> },
- null
- >= configureTactics_internal;
+export const configureTactics: Server.ExecRequest<{ node: node },null>= configureTactics_internal;
const setParameter_internal: Server.ExecRequest<
- { node: Json.index<'#node'>, tactic: Json.key<'#tactic'>,
- param: Json.key<'#param'>, value: Json.json },
+ { node: node, tactic: Json.key<'#tactic'>, param: Json.key<'#param'>,
+ value: Json.json },
null
> = {
kind: Server.RqKind.EXEC,
name: 'plugins.wp.tac.setParameter',
input: Json.jObject({
- node: Json.jIndex<'#node'>('#node'),
+ node: jNode,
tactic: Json.jKey<'#tactic'>('#tactic'),
param: Json.jKey<'#param'>('#param'),
value: Json.jAny,
@@ -290,25 +292,19 @@ const setParameter_internal: Server.ExecRequest<
};
/** Configure tactical parameter */
export const setParameter: Server.ExecRequest<
- { node: Json.index<'#node'>, tactic: Json.key<'#tactic'>,
- param: Json.key<'#param'>, value: Json.json },
+ { node: node, tactic: Json.key<'#tactic'>, param: Json.key<'#param'>,
+ value: Json.json },
null
>= setParameter_internal;
-const applyTactic_internal: Server.ExecRequest<
- Json.key<'#tactic'>,
- Json.index<'#node'>[]
- > = {
+const applyTactic_internal: Server.ExecRequest<Json.key<'#tactic'>,node[]> = {
kind: Server.RqKind.EXEC,
name: 'plugins.wp.tac.applyTactic',
input: Json.jKey<'#tactic'>('#tactic'),
- output: Json.jArray(Json.jIndex<'#node'>('#node')),
+ output: Json.jArray(jNode),
signals: [],
};
/** Applies the (configured) tactic */
-export const applyTactic: Server.ExecRequest<
- Json.key<'#tactic'>,
- Json.index<'#node'>[]
- >= applyTactic_internal;
+export const applyTactic: Server.ExecRequest<Json.key<'#tactic'>,node[]>= applyTactic_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 eb10c5fa0d0feb9258c952d18a4ff006bac568ed..f1c3ac6961a529da08f2a64c9a231de1b44b2590 100644
--- a/ivette/src/frama-c/plugins/wp/api/tip/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
@@ -75,60 +75,66 @@ export const proofStatus: Server.Signal = {
name: 'plugins.wp.tip.proofStatus',
};
+/** Proof Node index */
+export type node = Json.index<'#node'>;
+
+/** Decoder for `node` */
+export const jNode: Json.Decoder<node> = Json.jIndex<'#node'>('#node');
+
+/** Natural order for `node` */
+export const byNode: Compare.Order<node> = Compare.number;
+
+/** Default value for `node` */
+export const nodeDefault: node = Json.jIndex<'#node'>('#node')(-1);
+
const getNodeInfos_internal: Server.GetRequest<
- Json.index<'#node'>,
+ node,
{ result: string, proved: boolean, pending: number, size: number,
- stats: string }
+ stats: string, results: [ prover, result ][], tactic: string,
+ children: [ string, node ][] }
> = {
kind: Server.RqKind.GET,
name: 'plugins.wp.tip.getNodeInfos',
- input: Json.jIndex<'#node'>('#node'),
+ input: jNode,
output: Json.jObject({
result: 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,)),
}),
signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
};
/** Proof node information */
export const getNodeInfos: Server.GetRequest<
- Json.index<'#node'>,
+ node,
{ result: string, proved: boolean, pending: number, size: number,
- stats: string }
+ stats: string, results: [ prover, result ][], tactic: string,
+ children: [ string, node ][] }
>= getNodeInfos_internal;
const getProofState_internal: Server.GetRequest<
goal,
- { current: Json.index<'#node'>, parents: Json.index<'#node'>[],
- pending: number, index: number, results: [ prover, result ][],
- tactic: string, children: [ string, Json.index<'#node'> ][] }
+ { current: node, path: node[], index: number, pending: number }
> = {
kind: Server.RqKind.GET,
name: 'plugins.wp.tip.getProofState',
input: jGoal,
output: Json.jObject({
- current: Json.jIndex<'#node'>('#node'),
- parents: Json.jArray(Json.jIndex<'#node'>('#node')),
- pending: Json.jNumber,
+ current: jNode,
+ path: Json.jArray(jNode),
index: Json.jNumber,
- results: Json.jArray(Json.jPair( jProver, jResult,)),
- tactic: Json.jString,
- children: Json.jArray(
- Json.jPair(
- Json.jString,
- Json.jIndex<'#node'>('#node'),
- )),
+ pending: Json.jNumber,
}),
signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
};
/** Current Proof Status of a Goal */
export const getProofState: Server.GetRequest<
goal,
- { current: Json.index<'#node'>, parents: Json.index<'#node'>[],
- pending: number, index: number, results: [ prover, result ][],
- tactic: string, children: [ string, Json.index<'#node'> ][] }
+ { current: node, path: node[], index: number, pending: number }
>= getProofState_internal;
const goForward_internal: Server.SetRequest<goal,null> = {
@@ -161,25 +167,49 @@ const goToIndex_internal: Server.SetRequest<[ goal, number ],null> = {
/** Go to k-th pending node of proof tree */
export const goToIndex: Server.SetRequest<[ goal, number ],null>= goToIndex_internal;
-const goToNode_internal: Server.SetRequest<Json.index<'#node'>,null> = {
+const goToNode_internal: Server.SetRequest<node,null> = {
kind: Server.RqKind.SET,
name: 'plugins.wp.tip.goToNode',
- input: Json.jIndex<'#node'>('#node'),
+ input: jNode,
output: Json.jNull,
signals: [],
};
/** Set current node of associated proof tree */
-export const goToNode: Server.SetRequest<Json.index<'#node'>,null>= goToNode_internal;
+export const goToNode: Server.SetRequest<node,null>= goToNode_internal;
-const removeNode_internal: Server.SetRequest<Json.index<'#node'>,null> = {
+const removeNode_internal: Server.SetRequest<node,null> = {
kind: Server.RqKind.SET,
name: 'plugins.wp.tip.removeNode',
- input: Json.jIndex<'#node'>('#node'),
+ input: jNode,
output: Json.jNull,
signals: [],
};
/** Remove node from tree and go to parent */
-export const removeNode: Server.SetRequest<Json.index<'#node'>,null>= removeNode_internal;
+export const removeNode: Server.SetRequest<node,null>= removeNode_internal;
+
+/** Proof part marker */
+export type part = Json.key<'#part'>;
+
+/** Decoder for `part` */
+export const jPart: Json.Decoder<part> = Json.jKey<'#part'>('#part');
+
+/** Natural order for `part` */
+export const byPart: Compare.Order<part> = Compare.string;
+
+/** Default value for `part` */
+export const partDefault: part = Json.jKey<'#part'>('#part')('');
+
+/** Term marker */
+export type term = Json.key<'#term'>;
+
+/** Decoder for `term` */
+export const jTerm: Json.Decoder<term> = Json.jKey<'#term'>('#term');
+
+/** Natural order for `term` */
+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 = {
@@ -220,16 +250,15 @@ export const byRformat: Compare.Order<rformat> = Compare.structural;
/** Default value for `rformat` */
export const rformatDefault: rformat = "ratio";
-const printSequent_internal: Server.ExecRequest<
- { node: Json.index<'#node'>, indent?: number, margin?: number,
- iformat?: iformat, rformat?: rformat, autofocus?: boolean,
- unmangled?: boolean },
+const printSequent_internal: Server.GetRequest<
+ { node?: node, indent?: number, margin?: number, iformat?: iformat,
+ rformat?: rformat, autofocus?: boolean, unmangled?: boolean },
text
> = {
- kind: Server.RqKind.EXEC,
+ kind: Server.RqKind.GET,
name: 'plugins.wp.tip.printSequent',
input: Json.jObject({
- node: Json.jIndex<'#node'>('#node'),
+ node: Json.jOption(jNode),
indent: Json.jOption(Json.jNumber),
margin: Json.jOption(Json.jNumber),
iformat: Json.jOption(jIformat),
@@ -241,34 +270,32 @@ const printSequent_internal: Server.ExecRequest<
signals: [ { name: 'plugins.wp.tip.printStatus' } ],
};
/** Pretty-print the associated node */
-export const printSequent: Server.ExecRequest<
- { node: Json.index<'#node'>, indent?: number, margin?: number,
- iformat?: iformat, rformat?: rformat, autofocus?: boolean,
- unmangled?: boolean },
+export const printSequent: Server.GetRequest<
+ { node?: node, indent?: number, margin?: number, iformat?: iformat,
+ rformat?: rformat, autofocus?: boolean, unmangled?: boolean },
text
>= printSequent_internal;
-const clearSelection_internal: Server.SetRequest<Json.index<'#node'>,null> = {
+const clearSelection_internal: Server.SetRequest<node,null> = {
kind: Server.RqKind.SET,
name: 'plugins.wp.tip.clearSelection',
- input: Json.jIndex<'#node'>('#node'),
+ input: jNode,
output: Json.jNull,
signals: [],
};
/** Reset node selection */
-export const clearSelection: Server.SetRequest<Json.index<'#node'>,null>= clearSelection_internal;
+export const clearSelection: Server.SetRequest<node,null>= clearSelection_internal;
const setSelection_internal: Server.SetRequest<
- { node: Json.index<'#node'>, part?: Json.key<'#part'>,
- term?: Json.key<'#term'>, extend?: boolean },
+ { node: node, part?: part, term?: term, extend?: boolean },
null
> = {
kind: Server.RqKind.SET,
name: 'plugins.wp.tip.setSelection',
input: Json.jObject({
- node: Json.jIndex<'#node'>('#node'),
- part: Json.jOption(Json.jKey<'#part'>('#part')),
- term: Json.jOption(Json.jKey<'#term'>('#term')),
+ node: jNode,
+ part: Json.jOption(jPart),
+ term: Json.jOption(jTerm),
extend: Json.jOption(Json.jBoolean),
}),
output: Json.jNull,
@@ -276,9 +303,27 @@ const setSelection_internal: Server.SetRequest<
};
/** Set node selection */
export const setSelection: Server.SetRequest<
- { node: Json.index<'#node'>, part?: Json.key<'#part'>,
- term?: Json.key<'#term'>, extend?: boolean },
+ { node: node, part?: part, term?: term, extend?: boolean },
null
>= setSelection_internal;
+const getSelection_internal: Server.GetRequest<
+ node,
+ { part?: part, term?: term }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.tip.getSelection',
+ input: jNode,
+ output: Json.jObject({
+ part: Json.jOption(jPart),
+ term: Json.jOption(jTerm),
+ }),
+ signals: [ { name: 'plugins.wp.tip.printStatus' } ],
+};
+/** Get current selection in proof node */
+export const getSelection: Server.GetRequest<
+ node,
+ { part?: part, term?: term }
+ >= getSelection_internal;
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index 87d94e61690e7501b6352fd8ef3e61f925d501ee..349d1f2c2f144105788669a60323f107f3e731c9 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -33,7 +33,7 @@ import * as WP from 'frama-c/plugins/wp/api';
/* -------------------------------------------------------------------------- */
function getScope(g : WP.goalsData): string {
- if (g.bhv && g.fct) return `${g.fct}@{g.bhv}}`;
+ if (g.bhv && g.fct) return `${g.fct} — {g.bhv}}`;
if (g.fct) return g.fct;
if (g.thy) return g.thy;
return '';
@@ -45,6 +45,7 @@ function getScope(g : WP.goalsData): string {
interface IconStatus {
icon: string;
+ label: string;
kind: IconKind;
title: string;
}
@@ -52,22 +53,24 @@ interface IconStatus {
interface Status extends IconStatus { label: string }
const noResult : IconStatus =
- { icon: 'MINUS', kind: 'disabled', title: 'No Result' };
+ { icon: 'MINUS', label: 'No Result', kind: 'disabled', title: 'No Result' };
+/* eslint-disable max-len */
const baseStatus : { [key:string]: IconStatus } = {
- 'VALID': { icon: 'CHECK', kind: 'positive', title: 'Valid Goal' },
- 'PASSED': { icon: 'CHECK', kind: 'positive', title: 'Passed Test' },
- 'DOOMED': { icon: 'CROSS', kind: 'negative', title: 'Doomed Test' },
- 'FAILED': { icon: 'WARNING', kind: 'negative', title: 'Prover Failure' },
- 'UNKNOWN': { icon: 'ATTENTION', kind: 'warning', title: 'Prover Stucked' },
- 'TIMEOUT': { icon: 'HELP', kind: 'warning', title: 'Prover Timeout' },
- 'STEPOUT': { icon: 'HELP', kind: 'warning', title: 'Prover Stepout' },
- 'COMPUTING': { icon: 'EXECUTE', kind: 'default', title: 'Computing…' },
+ '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' },
+ 'FAILED': { icon: 'WARNING', label: 'Failed', kind: 'negative', title: 'Prover Failure' },
+ 'UNKNOWN': { icon: 'ATTENTION', label: 'Unknown', kind: 'warning', title: 'Prover Stucked' },
+ 'TIMEOUT': { icon: 'HELP', label: 'Timeout', kind: 'warning', title: 'Prover Timeout' },
+ 'STEPOUT': { icon: 'HELP', label: 'Stepout', kind: 'warning', title: 'Prover Stepout' },
+ 'COMPUTING': { icon: 'EXECUTE', label: 'Running', kind: 'default', title: 'Prover is running' },
};
+/* eslint-enable max-len */
-function getStatus(g : WP.goalsData): Status {
- const base = baseStatus[g.status] ?? noResult;
- return { ...base, label: g.stats.summary };
+export function getStatus(g : WP.goalsData): Status {
+ const { label, ...base } = baseStatus[g.status] ?? noResult;
+ return { ...base, label: label + g.stats.summary };
}
function renderStatus(s : Status): JSX.Element {
@@ -94,21 +97,35 @@ function filterGoal(
/* -------------------------------------------------------------------------- */
export interface GoalTableProps {
- scope: Ast.decl | undefined;
+ display: boolean;
failed: boolean;
- onFilter: (goals: number, total: number) => void;
+ scope: Ast.decl | undefined;
+ current: WP.goal | undefined;
+ setCurrent: (goal: WP.goal) => void;
+ setTIP: (goal: WP.goal) => void;
+ setGoals: (goals: number) => void;
+ setTotal: (total: number) => void;
}
export function GoalTable(props: GoalTableProps): JSX.Element {
- const { scope, failed, onFilter } = props;
- const model = States.useSyncArrayModel(WP.goals);
- const [wpoSelection, setWpoSelection] = React.useState(WP.goalDefault);
-
- const onWpoSelection = React.useCallback(
- ({ wpo, property }: WP.goalsData) => {
- States.setSelected(property);
- setWpoSelection(wpo);
- }, []);
+ const {
+ display, scope, failed,
+ current, setCurrent, setTIP,
+ setGoals, setTotal,
+ } = props;
+ const { model } = States.useSyncArrayProxy(WP.goals);
+ const goals = model.getRowCount();
+ const total = model.getTotalRowCount();
+ const onSelection = React.useCallback(
+ ({ wpo, marker }: WP.goalsData) => {
+ States.setSelected(marker);
+ setCurrent(wpo);
+ }, [setCurrent]);
+ const onDoubleClick = React.useCallback(
+ ({ wpo }: WP.goalsData) => {
+ setTIP(wpo);
+ }, [setTIP]
+ );
React.useEffect(() => {
if (failed || !!scope) {
@@ -116,17 +133,19 @@ export function GoalTable(props: GoalTableProps): JSX.Element {
} else {
model.setFilter();
}
- const goals = model.getRowCount();
- const total = model.getTotalRowCount();
- onFilter(goals, total);
- }, [model, scope, failed, onFilter]);
+ }, [model, scope, failed]);
+
+ React.useEffect(() => setGoals(goals), [goals, setGoals]);
+ React.useEffect(() => setTotal(total), [total, setTotal]);
return (
<Table
model={model}
+ display={display}
settings='wp.goals'
- onSelection={onWpoSelection}
- selection={wpoSelection}
+ selection={current}
+ onSelection={onSelection}
+ onDoubleClick={onDoubleClick}
>
<Column id='scope' label='Scope'
width={150}
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index bc8223ad4143546381f9b300657c90104da712af..df58d4caa73ab40343036ccf7d77205a3d389c30 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -31,8 +31,10 @@ import { IconButton } from 'dome/controls/buttons';
import { LED, Meter } from 'dome/controls/displays';
import { Group, Inset } from 'dome/frame/toolbars';
import * as Ivette from 'ivette';
+import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
import { GoalTable } from './goals';
+import { TIPView } from './tip';
import * as WP from 'frama-c/plugins/wp/api';
import './style.css';
@@ -40,33 +42,60 @@ import './style.css';
/* --- Goal Component --- */
/* -------------------------------------------------------------------------- */
+type Goal = WP.goal | undefined;
+
function WPGoals(): JSX.Element {
const [scoped, flipScoped] = Dome.useFlipSettings('frama-c.wp.goals.scoped');
const [failed, flipFailed] = Dome.useFlipSettings('frama-c.wp.goals.failed');
+ const [tip, setTip] = React.useState(false);
+ const [current, setCurrent] = React.useState<Goal>(undefined);
+ Server.useShutdown(() => { setTip(false); setCurrent(undefined); });
const scope = States.useCurrentScope();
const [goals, setGoals] = React.useState(0);
const [total, setTotal] = React.useState(0);
- const onFilter = React.useCallback((goals, total) => {
- setGoals(goals);
- setTotal(total);
- }, [setGoals, setTotal]);
- const current = scoped ? scope : undefined;
- return (
- <>
- <Ivette.TitleBar>
- <Label display={goals < total}>
- {goals} / {total}
- </Label>
- <Inset />
- <IconButton icon='COMPONENT' title='Current Scope Only'
- enabled={!!current}
- selected={scoped} onClick={flipScoped} />
- <IconButton icon='CIRC.QUESTION' title='Unresolved Goals Only'
- selected={failed} onClick={flipFailed} />
- </Ivette.TitleBar>
- <GoalTable scope={scope} failed={failed} onFilter={onFilter} />
- </>
- );
+ const hasGoals = total > 0;
+ return (
+ <>
+ <Ivette.TitleBar
+ label={tip ? 'WP — TIP' : 'WP — Goals'}
+ title={tip ? 'Interactive Proof Transformer' : 'Generated Goals'}
+ >
+ <Label display={goals < total}>
+ {goals} / {total}
+ </Label>
+ <Inset />
+ <IconButton
+ icon='CURSOR' title='Current Scope Only'
+ enabled={hasGoals}
+ selected={scoped}
+ onClick={flipScoped} />
+ <IconButton
+ icon='CIRC.QUESTION' title='Unresolved Goals Only'
+ enabled={hasGoals}
+ selected={failed}
+ onClick={flipFailed} />
+ <IconButton
+ icon={tip ? 'ITEMS.LIST' : 'MEDIA.PLAY'}
+ kind={tip ? 'warning' : 'positive'}
+ title={tip ? 'Back to Goals' : 'Interactive Proof Transformer'}
+ enabled={!!current}
+ onClick={() => setTip(!tip)} />
+ </Ivette.TitleBar>
+ <GoalTable
+ display={!tip}
+ scope={scope}
+ failed={failed}
+ current={current}
+ setCurrent={setCurrent}
+ setTIP={() => setTip(true)}
+ setGoals={setGoals}
+ setTotal={setTotal}
+ />
+ <TIPView
+ display={tip}
+ goal={current} />
+ </>
+ );
}
Ivette.registerComponent({
diff --git a/ivette/src/frama-c/plugins/wp/seq.tsx b/ivette/src/frama-c/plugins/wp/seq.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..aadc99da689378d28b63cd60d49d2642aa2e6453
--- /dev/null
+++ b/ivette/src/frama-c/plugins/wp/seq.tsx
@@ -0,0 +1,209 @@
+/* ************************************************************************ */
+/* */
+/* 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 from 'react';
+
+import { jOption } from 'dome/data/json';
+import {
+ MarkDecoration, GutterDecoration, Decorations,
+ Position, Range, TextProxy, TextView,
+} from 'dome/text/richtext';
+
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
+import * as RichText from 'frama-c/richtext';
+import type { text } from 'frama-c/kernel/api/data';
+import * as TIP from 'frama-c/plugins/wp/api/tip';
+
+/* -------------------------------------------------------------------------- */
+/* --- Sequent Decorations --- */
+/* -------------------------------------------------------------------------- */
+
+type Node = TIP.node | undefined;
+type Location = { part?: RichText.Tag, term?: RichText.Tag };
+type Target = { selection?: Range, gutters: GutterDecoration[] };
+
+class Sequent {
+ private readonly contents: string;
+ private readonly tags: RichText.Tags;
+ private readonly style: MarkDecoration[];
+ private readonly index: RichText.TagIndex;
+
+ constructor(jtext: text) {
+ this.contents = RichText.textToString(jtext);
+ this.style = [];
+ const addStyle = (tg: RichText.Tag, className: string): void => {
+ const { offset, endOffset } = tg;
+ const length = endOffset - offset;
+ this.style.push({ className, offset, length });
+ };
+ const filter = (t: RichText.Tag): boolean => {
+ switch(t.tag) {
+ case 'wp:comment':
+ case 'wp:property':
+ addStyle(t, 'cm-comment');
+ return false;
+ case 'wp:stmt':
+ case 'wp:clause':
+ case 'wp:warning':
+ addStyle(t, 'cm-keyword');
+ return false;
+ case 'wp:label':
+ addStyle(t, 'cm-def');
+ return false;
+ case 'wp:var':
+ addStyle(t, 'cm-type');
+ return false;
+ case 'wp:focus':
+ addStyle(t, 'cm-multiple-code');
+ return false;
+ case 'wp:target':
+ addStyle(t, 'cm-selected-code');
+ return false;
+ }
+ return t.tag.startsWith('#');
+ };
+ const { index, tags } = RichText.textToTags(jtext, filter);
+ this.tags = tags;
+ this.index = index;
+ }
+
+ get text(): string {
+ return this.contents;
+ }
+
+ get decorations(): Decorations {
+ return this.style;
+ }
+
+ find(tg: string | undefined) : RichText.Tags {
+ return tg ? this.index.get(tg) ?? [] : [];
+ }
+
+ select(part?: TIP.part, term?: TIP.term): RichText.Tag | undefined {
+ const ptags = this.find(part);
+ if (!ptags) return;
+ const etags = this.find(term);
+ if (etags) {
+ const tg = etags.find(e => ptags.find(p => RichText.contains(p, e)));
+ if (tg) return tg;
+ }
+ return ptags[0];
+ }
+
+ target(proxy: TextProxy, part?: TIP.part, term?: TIP.term): Target {
+ const tag = this.select(part, term);
+ 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 });
+ return { selection, gutters };
+ } else
+ return { selection: undefined, gutters };
+ }
+
+ locate(position: number): Location {
+ const isPart = ({ tag }: RichText.Tag): boolean => {
+ return tag === '#goal' || tag.startsWith('#s');
+ };
+ const part = RichText.findTag(this.tags, position, isPart);
+ if (!part) return {};
+ const term = RichText.findTag(part.children, position);
+ return { part, term };
+ }
+
+ hover(pos: Position | null): Decorations {
+ if (pos) {
+ const { part, term } = this.locate(pos.offset);
+ const range = term ?? part;
+ if (range) {
+ const { offset, endOffset } = range;
+ const length = endOffset - offset;
+ return { className: 'wp cm-hovered-code', offset, length };
+ }
+ }
+ return null;
+ }
+
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Sequent View --- */
+/* -------------------------------------------------------------------------- */
+
+export interface GoalViewProps {
+ node: Node;
+ autofocus: boolean;
+ unmangled: boolean;
+ iformat: TIP.iformat;
+ rformat: TIP.rformat;
+}
+
+export function GoalView(props: GoalViewProps): JSX.Element {
+ const { node } = props;
+ const jtext = States.useRequest(TIP.printSequent, props, {
+ pending: null,
+ offline: undefined,
+ onError: '',
+ }) ?? null;
+ const { part, term } = States.useRequest(TIP.getSelection, node) ?? {};
+ const proxy = React.useMemo(() => new TextProxy(), []);
+ const sequent = React.useMemo(() => new Sequent(jtext), [jtext]);
+ React.useEffect(() => proxy.updateContents(sequent.text), [proxy, sequent]);
+ const { selection, gutters } = React.useMemo(
+ () => sequent.target(proxy, part, term),
+ [sequent, proxy, part, term]
+ );
+ const [hover, setHover] = React.useState<Decorations>(null);
+ const onHover = React.useCallback((pos: Position | null) => {
+ setHover(sequent.hover(pos));
+ }, [sequent]);
+ const onClick = React.useCallback((pos: Position | null) => {
+ setHover(null);
+ if (node && pos) {
+ const loc = sequent.locate(pos.offset);
+ const part = jOption(TIP.jPart)(loc.part?.tag);
+ const term = jOption(TIP.jTerm)(loc.term?.tag);
+ if (part || term) {
+ Server.send(TIP.setSelection, { node, part, term });
+ return;
+ }
+ }
+ Server.send(TIP.clearSelection, node);
+ }, [sequent, node]);
+ return (
+ <TextView
+ readOnly
+ className='wp'
+ text={proxy}
+ selection={selection}
+ decorations={[hover, sequent.decorations, gutters]}
+ onHover={onHover}
+ onClick={onClick}
+ />
+ );
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/wp/style.css b/ivette/src/frama-c/plugins/wp/style.css
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..eab44e5565f0e23534e141a1f2eb3d820a7ae515 100644
--- a/ivette/src/frama-c/plugins/wp/style.css
+++ b/ivette/src/frama-c/plugins/wp/style.css
@@ -0,0 +1,17 @@
+/* -------------------------------------------------------------------------- */
+/* --- WP Panel Styles --- */
+/* -------------------------------------------------------------------------- */
+
+.wp .cm-gutter {
+ width: 3px;
+}
+
+.wp-gutter-part {
+ background: red;
+}
+
+.wp.cm-hovered-code,
+.wp.cm-hovered-code > span
+{
+ background: var(--code-hover);
+}
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..04f97441ccc80019792a7d75edd17761a0fecabd
--- /dev/null
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -0,0 +1,178 @@
+/* ************************************************************************ */
+/* */
+/* 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 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 * 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';
+
+/* -------------------------------------------------------------------------- */
+/* --- Sequent Printing Modes --- */
+/* -------------------------------------------------------------------------- */
+
+type Focus = 'AUTOFOCUS' | 'FULLCONTEXT' | 'MEMORY' | 'RAW';
+
+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';
+ }
+}
+
+function FocusSelector(props: Selector<Focus>): JSX.Element {
+ const { value, setValue } = props;
+ return (
+ <Select
+ value={value}
+ title='Autofocus Mode'
+ onChange={(v) => setValue(jFocus(v))}
+ >
+ <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>
+ );
+}
+
+function IFormatSelector(props: Selector<TIP.iformat>): JSX.Element {
+ const { value, setValue } = props;
+ return (
+ <Select
+ value={value}
+ 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>
+ </Select>
+ );
+}
+
+function RFormatSelector(props: Selector<TIP.rformat>): JSX.Element {
+ const { value, setValue } = props;
+ return (
+ <Select
+ value={value}
+ title='Floatting Point Constants Format'
+ onChange={(v) => setValue(TIP.jRformat(v))}
+ >
+ <option value='ratio'>Real</option>
+ <option value='float'>Float</option>
+ <option value='double'>Double</option>
+ </Select>
+ );
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- TIP View --- */
+/* -------------------------------------------------------------------------- */
+
+interface ProofState {
+ current: TIP.node | undefined;
+ index: number;
+ pending: number;
+}
+
+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 useTarget(target: WP.goal | undefined) : WP.goalsData {
+ return States.useSyncArrayElt( WP.goals, target ) ?? WP.goalsDataDefault;
+}
+
+export interface TIPProps {
+ display: boolean;
+ goal: WP.goal | undefined;
+}
+
+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 [ 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';
+ return (
+ <Vfill display={display}>
+ <ToolBar>
+ <Cell
+ icon='HOME'
+ label={infos.wpo} title='Goal identifier' />
+ <Cell
+ icon='CODE'
+ display={0 <= index && index < pending && 1 < pending}
+ label={`${index+1}/${pending}`} title='Pending proof nodes'/>
+ <Cell {...getStatus(infos)}/>
+ <Filler/>
+ <FocusSelector value={focus} setValue={setFocus}/>
+ <IFormatSelector value={iformat} setValue={setIformat}/>
+ <RFormatSelector value={rformat} setValue={setRformat}/>
+ </ToolBar>
+ <GoalView
+ node={current}
+ autofocus={autofocus}
+ unmangled={unmangled}
+ iformat={iformat}
+ rformat={rformat}
+ />
+ </Vfill>
+ );
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/richtext.tsx b/ivette/src/frama-c/richtext.tsx
index aa96434523bfcc635fe253f699de218802b3ec58..2fd37ff7ce138fda8ae9c13e454d90af87d7b65b 100644
--- a/ivette/src/frama-c/richtext.tsx
+++ b/ivette/src/frama-c/richtext.tsx
@@ -30,11 +30,131 @@
*/
import React from 'react';
-import * as Dome from 'dome';
import * as KernelData from 'frama-c/kernel/api/data';
import { classes } from 'dome/misc/utils';
-const D = new Dome.Debug('Utils');
+// --------------------------------------------------------------------------
+// --- Kernel Text Utilities
+// --------------------------------------------------------------------------
+
+/** Unstructured text contents */
+export function textToString(text: KernelData.text): string {
+ if (text===null) return '';
+ if (typeof(text)==='string') return text;
+ // documented to be faster than map & join
+ let buffer='';
+ // skip tag mark
+ for(let k=1; k<text.length; k++)
+ buffer += textToString(text[k]);
+ return buffer;
+}
+
+// --------------------------------------------------------------------------
+// --- Text Tag Tree
+// --------------------------------------------------------------------------
+
+/** Tag Tree */
+export type Tags = readonly Tag[];
+export type Tag = {
+ tag: string,
+ offset: number,
+ endOffset: number,
+ children: Tags
+};
+
+export type TagIndex = Map<string, Tags>;
+
+export function contains(a: Tag, b: Tag): boolean {
+ return a.offset <= b.offset && b.endOffset <= a.endOffset;
+}
+
+/** Extract a Tag forest from a text. */
+export function textToTags(
+ text: KernelData.text,
+ filter?: (tag: Tag) => boolean,
+): {
+ index: TagIndex,
+ tags: Tags
+} {
+ const walk =
+ (buffer: Tag[], offset: number, text: KernelData.text): number => {
+ if (text===null) return offset;
+ if (typeof(text)==='string') return offset + text.length;
+ let endOffset = offset;
+ const t0 = text[0];
+ if (t0 && typeof(t0)==='string') {
+ const tag = typeof(t0)==='string' ? t0 : '';
+ const children: Tag[] = [];
+ for(let k=1; k<text.length; k++)
+ endOffset = walk(children, endOffset, text[k]);
+ const tg = { tag, offset, endOffset, children };
+ if (!filter || filter(tg)) {
+ const tgs = index.get(tag);
+ if (tgs===undefined) index.set(tag, [tg]); else tgs.push(tg);
+ buffer.push(tg);
+ } else {
+ children.forEach(t => buffer.push(t));
+ }
+ } else {
+ for(let k=1; k<text.length; k++)
+ endOffset = walk(buffer, endOffset, text[k]);
+ }
+ return endOffset;
+ };
+ const index = new Map<string, Tag[]>();
+ const tags : Tag[] = [];
+ walk(tags, 0, text);
+ return { index, tags };
+}
+
+// --------------------------------------------------------------------------
+// --- Text Tag Index
+// --------------------------------------------------------------------------
+
+/** Lookup for the top-most tag containing the offset */
+export function findChildTag(tags: Tags, offset: number) : Tag | undefined
+{
+ let p = 0;
+ let q = tags.length - 1;
+ if (q < p) return undefined;
+ let a = tags[p];
+ let b = tags[q];
+ if (offset < a.offset) return undefined;
+ if (offset > b.endOffset) return undefined;
+ if (offset <= a.endOffset) return a;
+ if (b.offset <= offset) return b;
+ // @invariant Range: 0 <= p <= q < tags.length;
+ // @invariant Tags: a = tags[p] /\ b = tags[q];
+ // @invariant Offset: a.endOffset < offset < b.offset;
+ // @variant q-p;
+ for(;;) {
+ const d = q-p;
+ if (d <= 1) return undefined;
+ const r = Math.floor(p + d / 2);
+ const c = tags[r];
+ if (offset < c.offset) { b = c; q = r; continue; }
+ if (c.endOffset < offset) { a = c; p = r; continue; }
+ return c;
+ }
+}
+
+/** Lookup for the deepest tag containing the offset and satisfying the
+ filtering condition. */
+export function findTag(
+ tags: Tags,
+ offset: number,
+ filter?: (tag: Tag) => boolean,
+): Tag | undefined {
+ type Result = Tag | undefined;
+ const lookup = (tags: Tags, res: Result): Result => {
+ const r = findChildTag(tags, offset);
+ if (r && (!filter || filter(r)))
+ return lookup(r.children, r);
+ else
+ return res;
+ };
+ return lookup(tags, undefined);
+}
// --------------------------------------------------------------------------
// --- Lightweight Text Renderer
@@ -80,13 +200,13 @@ export interface TextProps {
export function Text(props: TextProps): JSX.Element {
const className = classes('kernel-text', 'dome-text-code', props.className);
- function makeContents(text: KernelData.text): React.ReactNode {
+ const makeContents = (text: KernelData.text): React.ReactNode => {
if (Array.isArray(text)) {
const tag = text[0];
const marker = tag && typeof (tag) === 'string';
const array = marker ? text.slice(1) : text;
const contents = React.Children.toArray(array.map(makeContents));
- if (marker) {
+ if (marker)
return (
<Marker
marker={tag}
@@ -96,14 +216,10 @@ export function Text(props: TextProps): JSX.Element {
{contents}
</Marker>
);
- }
return <>{contents}</>;
- } if (typeof text === 'string') {
- return text;
}
- D.error('Unexpected text', text);
- return null;
- }
+ return text;
+ };
return <div className={className}>{makeContents(props.text)}</div>;
}
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 7e1ee641c1dc5aa6f933319034bd1e8031f02acd..3e857376950ae9d44da9b3801bf9d45d93d9031d 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -409,6 +409,7 @@ export function reloadArray<K, A>(arr: Array<K, A>): void {
/** Access to Synchronized Array elements. */
export interface ArrayProxy<K, A> {
+ model: CompactModel<K, A>;
length: number;
getData(elt: K | undefined): (A | undefined);
forEach(fn: (row: A, elt: K) => void): void;
@@ -429,6 +430,7 @@ function arrayProxy<K, A>(
_stamp: number,
): ArrayProxy<K, A> {
return {
+ model,
length: model.length(),
getData: (elt) => elt ? model.getData(elt) : undefined,
forEach: (fn) => model.forEach((r) => fn(r, model.getkey(r))),
diff --git a/ivette/src/sandbox/icons.tsx b/ivette/src/sandbox/icons.tsx
index a3d4335767f47718dce1a8fcc26b52845a4adbc4..1c8f3b23a45723dceb647fad90602e909f27e067 100644
--- a/ivette/src/sandbox/icons.tsx
+++ b/ivette/src/sandbox/icons.tsx
@@ -45,12 +45,8 @@ function Gallery(): JSX.Element {
icons = [];
gallery.set(section, icons);
}
- icons.push(
- <>
- <Code icon={id} label={id} />
- <Label>{title}</Label>
- </>
- );
+ icons.push(<Code key={'C'+id} icon={id} label={id} />);
+ icons.push(<Label key={'L'+id} label={title} />);
});
const sections : JSX.Element[] = [];
gallery.forEach((icons, section) => {
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 6f9dacae8d65a17eb9d921f1cc2f8be20900caf4..4c308de170471e471992249ceb341effc711f526 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -212,15 +212,14 @@ end
(* --- Domain Utilities --- *)
(* -------------------------------------------------------------------------- *)
-module Jcallstack : S with type t = Callstack.t = struct
- module I = Data.Index
- (Callstack.Map)
- (struct let name = "eva-callstack-id" end)
- let jtype = Data.declare ~package ~name:"callstack" I.jtype
- type t = I.t
- let to_json = I.to_json
- let of_json = I.of_json
-end
+module Jcallstack : S with type t = Callstack.t =
+ Data.Index
+ (Callstack.Map)
+ (struct
+ let package = package
+ let name = "callstack"
+ let descr = Md.plain "Callstack identifier"
+ end)
module Jcalls : Request.Output with type t = Callstack.t = struct
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index df47ca96eaf56881c0733506aa192983a93c9603..bdaa0d0c3158856866febda02f142ddcd1b5b644 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -237,6 +237,7 @@ struct
end
let jpretty = Jbuffer.to_json
+let jtext s = `String s
(* -------------------------------------------------------------------------- *)
(* --- Functional API --- *)
@@ -579,7 +580,9 @@ end
module type Info =
sig
+ val package: package
val name: string
+ val descr: Markdown.text
end
(** Simplified [Map.S] *)
@@ -662,7 +665,8 @@ struct
include
(struct
type t = M.key
- let jtype = Jindex I.name
+ let jtype =
+ declare ~package:I.package ~name:I.name ~descr:I.descr (Jindex I.name)
let of_json = INDEX.of_json index
let to_json = INDEX.to_json index
end)
@@ -697,7 +701,8 @@ struct
include
(struct
type t = M.key
- let jtype = Jindex I.name
+ let jtype =
+ declare ~package:I.package ~name:I.name ~descr:I.descr (Jindex I.name)
let of_json js = INDEX.of_json (index()) js
let to_json v = INDEX.to_json (index()) v
end)
@@ -754,14 +759,13 @@ struct
let get x =
let tag = A.id x in
let hash = lookup () in
- if not (Hashtbl.mem hash tag) then
- Hashtbl.add hash tag x ;
- tag
+ if not (Hashtbl.mem hash tag) then Hashtbl.add hash tag x ; tag
include
(struct
type t = A.t
- let jtype = T.jtype I.name
+ let jtype =
+ declare ~package:I.package ~descr:I.descr ~name:I.name (T.jtype I.name)
let to_json a = T.to_json (get a)
let of_json js =
let k = T.of_json js in
@@ -794,8 +798,8 @@ sig
end
module Tagged(A : TaggedType)(I : Info)
- : Index with type t = A.t and type tag := string =
- HASHED
+ : Index with type t = A.t and type tag := string
+ = HASHED
(struct
include Jstring
type tag = string
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index e88927103f77c3ca79c14e6e775dafecf8b942bd..c9fe14a36a55800db6d21a507ce99a6cf9d3d637 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -85,12 +85,15 @@ module Jalpha : S with type t = string
(** Rich text encoding, see [Jbuffer]. *)
module Jtext : S with type t = json
-module Jmarkdown : S with type t = Markdown.text
+(** Simple string a Jtext *)
+val jtext : string -> Jtext.t
(** All-in-one formatter. Return the JSON encoding of formatted text. *)
val jpretty : ?indent:int -> ?margin:int ->
(Format.formatter -> 'a -> unit) -> 'a -> Jtext.t
+module Jmarkdown : S with type t = Markdown.text
+
(* -------------------------------------------------------------------------- *)
(** {2 Constructors} *)
(* -------------------------------------------------------------------------- *)
@@ -338,10 +341,12 @@ end
*)
(* -------------------------------------------------------------------------- *)
-(** Datatype information. *)
+(** Datatype registration information. *)
module type Info =
sig
+ val package: package
val name: string
+ val descr: Markdown.text
end
(** Simplified [Map.S]. *)
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index dfcb841190cb37d092abcd887af7f6cc8586f625..78c179100d96b421ab445e4db6b558164252f1c9 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -84,15 +84,7 @@ struct
let t_check_lemma = t_kind "check_lemma" "Logical check lemma"
let t_ext = t_kind "extension" "ACSL extension"
-
- let p_ext = Enum.prefix kinds ~name:"ext" ~var:"<clause>"
- ~descr:(Md.plain "ACSL extension `<clause>`")
-
- let p_loop_ext = Enum.prefix kinds ~name:"loop_ext" ~var:"<clause>"
- ~descr:(Md.plain "ACSL loop extension `loop <clause>`")
-
- let p_other = Enum.prefix kinds ~name:"prop" ~var:"<prop>"
- ~descr:(Md.plain "Plugin Specific properties")
+ let t_other = t_kind "generic" "Generic Property"
open Property
@@ -138,7 +130,7 @@ struct
| IPPropertyInstance _ -> t_instance
| IPTypeInvariant _ -> t_type_invariant
| IPGlobalInvariant _ -> t_global_invariant
- | IPOther { io_name } -> Enum.instance p_other io_name
+ | IPOther _ -> t_other
let () = Enum.set_lookup kinds lookup
let data = Request.dictionary ~package
@@ -149,14 +141,6 @@ struct
include (val data : S with type t = Property.t)
end
-let register_propkind ~name ~kind ?label ~descr () =
- let open PropKind in
- let prefix = match kind with
- | `Clause -> p_ext
- | `Loop -> p_loop_ext
- | `Other -> p_other
- in ignore @@ Enum.extends prefix ~name ?label ~descr
-
(* -------------------------------------------------------------------------- *)
(* --- Property Status --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_properties.mli b/src/plugins/server/kernel_properties.mli
index 9d6a044eb6188993058ea6d97ed43fb28165a2f1..3a828a88139363c9351b09c5809aeac692420a97 100644
--- a/src/plugins/server/kernel_properties.mli
+++ b/src/plugins/server/kernel_properties.mli
@@ -22,14 +22,6 @@
(** Kernel Property Status *)
-(** Documentation of ACSL extensions for [propkind] server data. *)
-val register_propkind :
- name:string ->
- kind:[`Clause | `Loop | `Other] ->
- ?label:Markdown.text ->
- descr:Markdown.text ->
- unit -> unit
-
(** Trigger a full reload for the table of property status. *)
val reload : unit -> unit
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index f25cd68bb036deb7974539b8c51293cb38fc1af5..26910b42448f6a4b5ed06ceec7f6e9358b5c85b6 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -52,17 +52,18 @@ module INDEX = State_builder.Ref
let default () = Hashtbl.create 0
end)
+let indexGoal g =
+ let id = g.Wpo.po_gid in
+ let index = INDEX.get () in
+ if not (Hashtbl.mem index id) then Hashtbl.add index id g ; id
+
module Goal : D.S with type t = Wpo.t =
struct
type t = Wpo.t
let jtype = D.declare ~package ~name:"goal"
~descr:(Md.plain "Proof Obligations") (Jkey "wpo")
let of_json js = Hashtbl.find (INDEX.get ()) (Json.string js)
- let to_json g =
- let id = g.Wpo.po_gid in
- let index = INDEX.get () in
- if not (Hashtbl.mem index id) then Hashtbl.add index id g ;
- `String id
+ let to_json g = `String (indexGoal g)
end
(* -------------------------------------------------------------------------- *)
@@ -123,13 +124,13 @@ struct
let to_json { smoke ; verdict } =
`String begin
match verdict with
- | VCS.Valid -> if smoke then "DOOMED" else "VALID"
- | VCS.Unknown -> if smoke then "PASSED" else "UNKNOWN"
+ | Valid -> if smoke then "DOOMED" else "VALID"
+ | Unknown -> if smoke then "PASSED" else "UNKNOWN"
+ | Timeout -> if smoke then "PASSED" else "TIMEOUT"
+ | Stepout -> if smoke then "PASSED" else "STEPOUT"
| Failed -> "FAILED"
| NoResult -> "NORESULT"
| Computing _ -> "COMPUTING"
- | Timeout -> "TIMEOUT"
- | Stepout -> "STEPOUT"
end
end
@@ -169,6 +170,18 @@ let () = R.register ~package ~kind:`GET ~name:"getAvailableProvers"
let gmodel : Wpo.t S.model = S.model ()
+let get_property g = Printer_tag.PIP (WpPropId.property_of_id g.Wpo.po_pid)
+
+let get_marker g =
+ match g.Wpo.po_formula.source with
+ | Some(stmt,_) -> Printer_tag.localizable_of_stmt stmt
+ | None ->
+ let ip = WpPropId.property_of_id g.Wpo.po_pid in
+ match ip with
+ | IPOther { io_loc = OLStmt(_,stmt) } ->
+ Printer_tag.localizable_of_stmt stmt
+ | _ -> Printer_tag.PIP ip
+
let get_decl g = match g.Wpo.po_idx with
| Function(kf,_) -> Some (Printer_tag.SFunction kf)
| Axiomatic _ -> None (* TODO *)
@@ -191,15 +204,18 @@ let get_status g =
verdict = (ProofEngine.consolidated g).best ;
}
-let () = S.column gmodel ~name:"property"
- ~descr:(Md.plain "Property Marker")
- ~data:(module AST.Marker)
- ~get:(fun g -> Printer_tag.PIP (WpPropId.property_of_id g.Wpo.po_pid))
+let () = S.column gmodel ~name:"marker"
+ ~descr:(Md.plain "Associated Marker")
+ ~data:(module AST.Marker) ~get:get_marker
let () = S.column gmodel ~name:"scope"
~descr:(Md.plain "Associated declaration, if any")
~data:(module D.Joption(AST.Decl)) ~get:get_decl
+let () = S.column gmodel ~name:"property"
+ ~descr:(Md.plain "Property Marker")
+ ~data:(module AST.Marker) ~get:get_property
+
let () = S.option gmodel ~name:"fct"
~descr:(Md.plain "Associated function name, if any")
~data:(module D.Jstring) ~get:get_fct
@@ -248,7 +264,7 @@ let () = S.column gmodel ~name:"saved"
let _ = S.register_array ~package ~name:"goals"
~descr:(Md.plain "Generated Goals")
- ~key:(fun g -> g.Wpo.po_gid)
+ ~key:indexGoal
~keyName:"wpo"
~keyType:Goal.jtype
~iter:Wpo.iter_on_goals
diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index 2bceb850f9990f3d6ddfb2ddf1e26d71e08779d5..256d87982b99c0a9ffe972dd30d9db65fcd2e377 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -42,30 +42,52 @@ let package = P.package ~plugin:"wp" ~name:"tip"
let proofStatus = R.signal ~package ~name:"proofStatus"
~descr:(Md.plain "Proof Status has changed")
-module Node = D.Index(Map.Make(ProofEngine.Node))(struct let name = "node" end)
+module Node = D.Index
+ (Map.Make(ProofEngine.Node))
+ (struct
+ let package = package
+ let name = "node"
+ let descr = Md.plain "Proof Node index"
+ end)
let () =
- let snode = R.signature ~input:(module Node) () in
- let set_title = R.result snode ~name:"result"
+ let inode = R.signature ~input:(module Node) () in
+ let set_title = R.result inode ~name:"result"
~descr:(Md.plain "Proof node title") (module D.Jstring) in
- let set_proved = R.result snode ~name:"proved"
+ let set_proved = R.result inode ~name:"proved"
~descr:(Md.plain "Proof node complete") (module D.Jbool) in
- let set_pending = R.result snode ~name:"pending"
+ let set_pending = R.result inode ~name:"pending"
~descr:(Md.plain "Pending children") (module D.Jint) in
- let set_size = R.result snode ~name:"size"
+ let set_size = R.result inode ~name:"size"
~descr:(Md.plain "Proof size") (module D.Jint) in
- let set_stats = R.result snode ~name:"stats"
+ let set_stats = R.result inode ~name:"stats"
~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.Jstring) 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") snode
+ ~descr:(Md.plain "Proof node information") inode
~signals:[proofStatus]
begin fun rq node ->
set_title rq (ProofEngine.title node) ;
set_proved rq (ProofEngine.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) ;
end
(* -------------------------------------------------------------------------- *)
@@ -76,22 +98,13 @@ 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_parents = R.result state ~name:"parents"
+ let set_path = R.result state ~name:"path"
~descr:(Md.plain "Proof node parents") (module D.Jlist(Node)) in
- let set_pending = R.result state ~name:"pending"
- ~descr:(Md.plain "Pending proof nodes") (module D.Jint) 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_results = R.result state ~name:"results"
- ~descr:(Md.plain "Prover results for current node")
- (module D.Jlist(D.Jpair(Prover)(Result))) in
- let set_tactic = R.result state ~name:"tactic"
- ~descr:(Md.plain "Proof node tactic header (if any)")
- (module D.Jstring) in
- let set_children = R.result state ~name:"children"
- ~descr:(Md.plain "Proof node tactic children (id any)")
- (module D.Jlist(D.Jpair(D.Jstring)(Node))) in
+ let set_pending = R.result state ~name:"pending"
+ ~descr:(Md.plain "Pending proof nodes") (module D.Jint) in
R.register_sig ~package
~kind:`GET ~name:"getProofState"
~descr:(Md.plain "Current Proof Status of a Goal") state
@@ -103,19 +116,13 @@ let () =
| `Main -> ProofEngine.root tree,-1
| `Internal node -> node,-1
| `Leaf(idx,node) -> node,idx in
- let rec parents node = match ProofEngine.parent node with
+ let rec path node = match ProofEngine.parent node with
| None -> []
- | Some p -> p::parents p in
- let tactic = match ProofEngine.tactical current with
- | None -> ""
- | Some { header } -> header in
+ | Some p -> p::path p in
set_current rq current ;
- set_parents rq (parents current) ;
+ set_path rq (path current) ;
set_index rq index ;
set_pending rq (ProofEngine.pending current) ;
- set_results rq (Wpo.get_results (ProofEngine.goal current)) ;
- set_tactic rq tactic ;
- set_children rq (ProofEngine.children current) ;
end
(* -------------------------------------------------------------------------- *)
@@ -171,13 +178,6 @@ let () = R.register ~package ~kind:`SET ~name:"removeNode"
(* --- Sequent Indexers --- *)
(* -------------------------------------------------------------------------- *)
-module Term = D.Tagged
- (struct
- type t = Lang.F.term
- let id t = Printf.sprintf "#e%d" (Lang.F.QED.id t)
- end)
- (struct let name = "term" end)
-
module Part = D.Tagged
(struct
type t = [ `Term | `Goal | `Step of int ]
@@ -186,12 +186,27 @@ module Part = D.Tagged
| `Goal -> "#goal"
| `Step k -> Printf.sprintf "#s%d" k
end)
- (struct let name = "part" end)
+ (struct
+ let package = package
+ let name = "part"
+ let descr = Md.plain "Proof part marker"
+ end)
+
+module Term = D.Tagged
+ (struct
+ type t = Lang.F.term
+ let id t = Printf.sprintf "#e%d" (Lang.F.QED.id t)
+ end)
+ (struct
+ let package = package
+ let name = "term"
+ let descr = Md.plain "Term marker"
+ end)
let of_part = function
- | Ptip.Term -> "#term"
- | Ptip.Goal -> "#goal"
- | Ptip.Step s -> Printf.sprintf "#s%d" s.id
+ | Ptip.Term -> `Term
+ | Ptip.Goal -> `Goal
+ | Ptip.Step s -> `Step s.id
let to_part sequent = function
| `Term -> Ptip.Term
@@ -217,21 +232,27 @@ class printer () : Ptip.pseq =
end in
let focus : Ptip.term_wrapper =
object
- method wrap pp fmt t = wrap "wp:focus" pp fmt t
+ method wrap pp fmt t = wrap "wp:focus" (terms#wrap pp) fmt t
end in
let target : Ptip.term_wrapper =
object
- method wrap pp fmt t = wrap "wp:target" pp fmt t
+ method wrap pp fmt t = wrap "wp:target" (terms#wrap pp) fmt t
end in
let parts : Ptip.part_marker =
object
- method wrap pp fmt p = wrap (of_part p) pp fmt p
+ method wrap pp fmt p = wrap (Part.get @@ of_part p) pp fmt p
method mark : 'a. Ptip.part -> 'a Ptip.printer -> 'a Ptip.printer
- = fun p pp fmt x -> wrap (of_part p) pp fmt x
+ = fun p pp fmt x -> wrap (Part.get @@ of_part p) pp fmt x
+ end in
+ let target_part : Ptip.part_marker =
+ object
+ method wrap pp fmt p = wrap "wp:target" (parts#wrap pp) fmt p
+ method mark : 'a. Ptip.part -> 'a Ptip.printer -> 'a Ptip.printer
+ = fun p pp fmt x -> wrap "wp:target" (parts#mark p pp) fmt x
end in
let autofocus = new Ptip.autofocus in
let plang = new Ptip.plang ~terms ~focus ~target ~autofocus in
- let pcond = new Ptip.pcond ~parts ~target:parts ~autofocus ~plang in
+ let pcond = new Ptip.pcond ~parts ~target:target_part ~autofocus ~plang in
Ptip.pseq ~autofocus ~plang ~pcond
(* -------------------------------------------------------------------------- *)
@@ -300,7 +321,7 @@ let rformat : Plang.rformat R.input =
let () =
let printSequent = R.signature ~output:(module D.Jtext) () in
- let get_node = R.param printSequent ~name:"node"
+ let get_node = R.param_opt printSequent ~name:"node"
~descr:(Md.plain "Proof Node") (module Node) in
let get_indent = R.param_opt printSequent ~name:"indent"
~descr:(Md.plain "Number of identation spaces") (module D.Jint) in
@@ -315,20 +336,22 @@ let () =
let get_unmangled = R.param_opt printSequent ~name:"unmangled"
~descr:(Md.plain "Unmangled memory model") (module D.Jbool) in
R.register_sig ~package
- ~kind:`EXEC
+ ~kind:`GET
~name:"printSequent"
~descr:(Md.plain "Pretty-print the associated node")
~signals:[printStatus] printSequent
begin fun rq () ->
- let node = get_node rq in
- let pp = lookup_printer node in
- let indent = get_indent rq in
- let margin = get_margin rq in
- Option.iter pp#set_iformat (get_iformat rq) ;
- Option.iter pp#set_rformat (get_rformat rq) ;
- Option.iter pp#set_focus_mode (get_autofocus rq) ;
- Option.iter pp#set_unmangled (get_unmangled rq) ;
- D.jpretty ?indent ?margin pp#pp_goal (ProofEngine.goal node)
+ match get_node rq with
+ | None -> D.jtext ""
+ | Some node ->
+ let pp = lookup_printer node in
+ let indent = get_indent rq in
+ let margin = get_margin rq in
+ Option.iter pp#set_iformat (get_iformat rq) ;
+ Option.iter pp#set_rformat (get_rformat rq) ;
+ Option.iter pp#set_focus_mode (get_autofocus rq) ;
+ Option.iter pp#set_unmangled (get_unmangled rq) ;
+ D.jpretty ?indent ?margin pp#pp_goal (ProofEngine.goal node)
end
(* -------------------------------------------------------------------------- *)
@@ -344,7 +367,9 @@ let () =
~output:(module D.Junit)
begin fun node ->
let pp = lookup_printer node in
- pp#reset ; R.emit printStatus
+ pp#reset ;
+ pp#selected ;
+ R.emit printStatus
end
let () =
@@ -374,4 +399,22 @@ let () =
R.emit printStatus
end
+let () =
+ let getSelection = R.signature ~input:(module Node) () in
+ let set_part = R.result_opt getSelection ~name:"part"
+ ~descr:(Md.plain "Selected part") (module Part) in
+ let set_term = R.result_opt getSelection ~name:"term"
+ ~descr:(Md.plain "Selected term") (module Term) in
+ R.register_sig ~package
+ ~kind:`GET
+ ~name:"getSelection"
+ ~descr:(Md.plain "Get current selection in proof node")
+ ~signals:[printStatus]
+ getSelection
+ begin fun rq node ->
+ let (part,term) = (lookup_printer node)#target in
+ set_part rq (if part <> Term then Some (of_part part) else None);
+ set_term rq term;
+ end
+
(* -------------------------------------------------------------------------- *)