diff --git a/ivette/src/frama-c/plugins/wp/tac.tsx b/ivette/src/frama-c/plugins/wp/tac.tsx
index 9142ea968db407fc44cfb7df1a19578007f92a90..787d5dbe87e9cc43c870e0db49cccc5f339fd0ae 100644
--- a/ivette/src/frama-c/plugins/wp/tac.tsx
+++ b/ivette/src/frama-c/plugins/wp/tac.tsx
@@ -21,6 +21,7 @@
/* ************************************************************************ */
import React, { Fragment } from 'react';
+
import { classes } from 'dome/misc/utils';
import { Icon } from 'dome/controls/icons';
import { IconButton, IconButtonKind } from 'dome/controls/buttons';
@@ -39,6 +40,7 @@ type Goal = WP.goal | undefined;
type Node = TIP.node | undefined;
type Prover = WP.prover | undefined;
type Tactic = TIP.tactic | undefined;
+type Mode = WP.InteractiveMode;
/* -------------------------------------------------------------------------- */
/* --- Use Actions --- */
@@ -61,6 +63,12 @@ function sendProverTime( node: Node, prover: Prover, timeout: number): void
}
}
+function sendProverInteractive(node: Node, prover: Prover, mode: Mode): void {
+ if (node && prover) {
+ Server.send(TIP.runProvers, { node, mode, provers: [prover] });
+ }
+}
+
function applyTactic(tactic: Tactic): void {
if (tactic) {
Server.send(TAC.applyTacticAndProve, tactic);
@@ -372,10 +380,10 @@ function Parameter(props: ParameterProps): JSX.Element | null
}
/* -------------------------------------------------------------------------- */
-/* --- Prover Configuration --- */
+/* --- Automatic Prover Configuration --- */
/* -------------------------------------------------------------------------- */
-export function ConfigureProver(props: ProverSelection): JSX.Element {
+export function ConfigureAutoProver(props: ProverSelection): JSX.Element {
const { node, selected: prover, setSelected } = props;
const { descr } = States.useSyncArrayElt(WP.ProverInfos, prover) ?? {};
const result = States.useRequestStable(TIP.getResult, { node, prover });
@@ -385,7 +393,8 @@ export function ConfigureProver(props: ProverSelection): JSX.Element {
getProverActions(result);
const [fwdTime, setFwdTime] = React.useState(0);
const [fwdArmed, setFwdArmed] = React.useState(false);
- const display = !!prover;
+ const auto = !States.useRequestStable(WP.isInteractiveProver, prover);
+ const display = auto && !!prover;
const action = running ? TIP.killProvers : TIP.runProvers;
const onPlay = (): void => sendProver(action, node, prover);
const onClear = (): void => sendProver(TIP.clearProvers, node, prover);
@@ -414,6 +423,25 @@ export function ConfigureProver(props: ProverSelection): JSX.Element {
className="dome-xToolBar dome-color-frame wp-configure"
display={display}
>
+ <Item
+ key='prover'
+ title='Selected Prover Configuration'
+ className="wp-config-tactic"
+ label={descr} />
+ <Separator />
+ <IconButton
+ key='clear'
+ icon='TRASH'
+ kind='negative'
+ enabled={clear}
+ title='Clear Prover Result'
+ onClick={onClear}
+ />
+ <Item
+ icon={icon}
+ kind={kind}
+ label={result.descr} />
+ <Filler />
<Label
icon='SETTINGS'
label='Process' title='Server Processes (shared by all provers)'
@@ -441,25 +469,7 @@ export function ConfigureProver(props: ProverSelection): JSX.Element {
/>
</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.STOP' : 'MEDIA.PLAY'}
@@ -486,6 +496,104 @@ export function ConfigureProver(props: ProverSelection): JSX.Element {
);
}
+/* -------------------------------------------------------------------------- */
+/* --- Interactive Prover Configuration --- */
+/* -------------------------------------------------------------------------- */
+
+export function ConfigureInteractiveProver(sel: ProverSelection): JSX.Element {
+ const { node, selected: prover, setSelected } = sel;
+ const { descr } = States.useSyncArrayElt(WP.ProverInfos, prover) ?? {};
+ const result = States.useRequestStable(TIP.getResult, { node, prover });
+ const interactive = States.useRequestStable(WP.isInteractiveProver, prover);
+ const [process = 1, setProcess] = States.useSyncState(WP.process);
+ const [timeout = 1, setTimeout] = States.useSyncState(WP.timeout);
+
+ const { icon, kind, clear=true, running=false } =
+ getProverActions(result);
+ const display = interactive && !!prover;
+ const kill =
+ (): void => sendProver(TIP.killProvers, node, prover);
+ const batch =
+ (): void => sendProverInteractive(node, prover, WP.InteractiveMode.batch);
+ const edit =
+ (): void => sendProverInteractive(node, prover, WP.InteractiveMode.edit);
+
+ const onClear = (): void => sendProver(TIP.clearProvers, node, prover);
+ const onClose = (): void => setSelected(undefined);
+ return (
+ <Hbox
+ className="dome-xToolBar dome-color-frame wp-configure"
+ display={display}
+ >
+ <Item
+ key='prover'
+ title='Selected Prover Configuration'
+ className="wp-config-tactic"
+ label={descr} />
+ <Separator />
+ <IconButton
+ key='clear'
+ icon='TRASH'
+ kind='negative'
+ enabled={clear}
+ title='Clear Prover Result'
+ onClick={onClear}
+ />
+ <Item
+ icon={icon}
+ kind={kind}
+ label={result.descr} />
+ <Filler />
+ <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"
+ onChange={setTimeout}
+ value={timeout}
+ vmin={1}
+ vmax={3600}
+ vstep={1}
+ />
+ </Label>
+ <Separator/>
+ <Hbox>
+ <IconButton
+ key='play'
+ icon={running ? 'MEDIA.STOP' : 'MEDIA.PLAY'}
+ title={running ? 'Stop Prover' : 'Run Prover'}
+ onClick={running ? kill : batch}
+ />
+ <IconButton
+ key='edit'
+ icon={'PAINTBRUSH'}
+ title={'Edit Prover Script'}
+ enabled={!running}
+ onClick={edit}
+ />
+ </Hbox>
+ <IconButton
+ key='close'
+ icon='CIRC.CLOSE'
+ title='Close Prover Configuration Panel'
+ onClick={onClose} />
+ </Hbox>
+ );
+}
+
/* -------------------------------------------------------------------------- */
/* --- Tactical Configuration --- */
/* -------------------------------------------------------------------------- */
@@ -570,6 +678,7 @@ export function ConfigureTactic(props: TacticSelection): JSX.Element {
title='Tactic Status'
{...statusDescr} />
<Fragment key='params'>{parameters}</Fragment>
+ <Separator/>
<IconButton
key='play'
icon={locked ? 'LOCK' : 'MEDIA.PLAY'}
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index 9bd335c039af3b8d8503cc39e4f018b095cfba7a..e25db7bee8b43fb9dcbf20dc196ec8d96b434bce 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -41,7 +41,12 @@ 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';
+import { Provers,
+ Tactics,
+ ConfigureAutoProver,
+ ConfigureInteractiveProver,
+ ConfigureTactic
+ } from './tac';
/* -------------------------------------------------------------------------- */
/* --- Sequent Printing Modes --- */
@@ -501,7 +506,12 @@ export function TIPView(props: TIPProps): JSX.Element {
/>
</Vbox>
</Hfill>
- <ConfigureProver
+ <ConfigureAutoProver
+ node={current}
+ selected={prover}
+ setSelected={onSelectedProver}
+ />
+ <ConfigureInteractiveProver
node={current}
selected={prover}
setSelected={onSelectedProver}
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 98ea44fc9cda45eae5b395d914736d62fefbfe8d..ea6c2a6c44fecd346f0c54571ec8301ea21454c1 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -159,8 +159,7 @@ let get_version = function
let iter_provers fn =
List.iter
(fun p ->
- if Why3Provers.is_auto p && Why3Provers.is_mainstream p then
- fn (VCS.Why3 p))
+ if Why3Provers.is_mainstream p then fn (VCS.Why3 p))
@@ Why3Provers.provers ()
let _ : VCS.prover S.array =
@@ -178,6 +177,50 @@ let _ : VCS.prover S.array =
~keyType:Prover.jtype
~iter:iter_provers model
+(* -------------------------------------------------------------------------- *)
+(* --- Interactive provers --- *)
+(* -------------------------------------------------------------------------- *)
+
+let _ =
+ R.register
+ ~package ~kind:`GET ~name:"isInteractiveProver"
+ ~descr:(Md.plain "Tells whether the prover is interactive")
+ ~input:(module Prover)
+ ~output:(module D.Jbool)
+ (fun p -> not @@ VCS.is_auto p)
+
+module InteractiveMode =
+struct
+ include D.Enum
+
+ let dictionary : VCS.mode dictionary = dictionary ()
+
+ let tag name descr value = tag ~name ~descr:(Md.plain descr) ~value dictionary
+
+ let batch = tag "batch" "Batch" VCS.Batch
+ let update = tag "update" "Update" VCS.Update
+ let edit = tag "edit" "Edit" VCS.Edit
+ let fix = tag "fix" "Fix" VCS.Fix
+ let fixup = tag "fixup" "FixUpdate" VCS.FixUpdate
+
+ let lookup = function
+ | VCS.Batch -> batch
+ | VCS.Update -> update
+ | VCS.Edit -> edit
+ | VCS.Fix -> fix
+ | VCS.FixUpdate -> fixup
+
+ let () =
+ set_lookup dictionary lookup
+
+ include
+ (val publish
+ ~package
+ ~descr:(Md.plain "interactive mode")
+ ~name:"InteractiveMode"
+ dictionary)
+end
+
(* -------------------------------------------------------------------------- *)
(* --- Counter Examples --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpApi.mli b/src/plugins/wp/wpApi.mli
index c9b285f9349a70a7c7d50018ced3ddac6f21e841..78200090a9bf65e59a827fb938b9bc924b7cde81 100644
--- a/src/plugins/wp/wpApi.mli
+++ b/src/plugins/wp/wpApi.mli
@@ -30,6 +30,7 @@ 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
+module InteractiveMode : Server.Data.S with type t = VCS.mode
val goals : Wpo.t Server.States.array
val getProvers : unit -> VCS.prover list
diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index f88d47a427ab866a57c51ba12117b19e08ae04a4..72f2b64510c059478c9de26d1d8f7a85b95198d3 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -532,7 +532,7 @@ let () =
(* --- Prover Scheduling --- *)
(* -------------------------------------------------------------------------- *)
-let runProvers ?timeout ?provers node =
+let runProvers ?mode ?timeout ?provers node =
let wpo = ProofEngine.goal node in
let provers = match provers with
| Some ps -> ps
@@ -540,6 +540,10 @@ let runProvers ?timeout ?provers node =
let timeout = match timeout with
| Some t -> t
| None -> Wp_parameters.Timeout.get () in
+ let mode = match mode with
+ | Some mode -> mode
+ | None -> VCS.parse_mode @@ Wp_parameters.Interactive.get () in
+ Kernel.feedback "Run prover with mode %a" VCS.pp_mode mode ;
let config =
let cfg = VCS.current () in
{ cfg with timeout = Some (float timeout) } in
@@ -552,7 +556,7 @@ let runProvers ?timeout ?provers node =
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 process () = Prover.prove ~config ~mode ~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 ;
@@ -571,6 +575,9 @@ let () =
let get_provers = R.param_opt iRunProvers (module WpApi.Provers)
~name:"provers"
~descr:(Md.plain "Prover selection (default: current") in
+ let get_mode = R.param_opt iRunProvers (module WpApi.InteractiveMode)
+ ~name:"mode"
+ ~descr:(Md.plain "Interactive provers mode") in
R.register_sig iRunProvers ~package ~kind:`SET
~name:"runProvers"
~descr:(Md.plain "Schedule provers on proof node")
@@ -578,7 +585,8 @@ let () =
let node = get_node rq in
let provers = get_provers rq in
let timeout = get_timeout rq in
- runProvers ?timeout ?provers node
+ let mode = get_mode rq in
+ runProvers ?mode ?timeout ?provers node
end
let killProvers ?provers node =
diff --git a/src/plugins/wp/wpTipApi.mli b/src/plugins/wp/wpTipApi.mli
index f4ad83e300b935dfe9d858578b5a86a70e1b0e08..0e40e18f68a1c972336672fc9e9bef439433887d 100644
--- a/src/plugins/wp/wpTipApi.mli
+++ b/src/plugins/wp/wpTipApi.mli
@@ -33,6 +33,7 @@ val selection : ProofEngine.node -> Tactical.selection
val setSelection : ProofEngine.node -> Tactical.selection -> unit
val runProvers :
+ ?mode:VCS.mode ->
?timeout:int ->
?provers:VCS.prover list ->
ProofEngine.node -> unit