From 266e6dee6ed7452a9f801b0891173234fb0e1928 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 6 Feb 2023 17:34:02 +0100
Subject: [PATCH] [wp/server] proof navigation
---
ivette/src/frama-c/plugins/wp/api/index.ts | 50 +++++++++++++++++
src/plugins/wp/ProofEngine.ml | 26 ++++-----
src/plugins/wp/ProofEngine.mli | 5 +-
src/plugins/wp/gui/GuiNavigator.ml | 2 +-
src/plugins/wp/wpApi.ml | 65 +++++++++++++++++++---
5 files changed, 124 insertions(+), 24 deletions(-)
diff --git a/ivette/src/frama-c/plugins/wp/api/index.ts b/ivette/src/frama-c/plugins/wp/api/index.ts
index bd48d1e056b..4a62dc61ded 100644
--- a/ivette/src/frama-c/plugins/wp/api/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/index.ts
@@ -325,4 +325,54 @@ export const getProofState: Server.GetRequest<
parents: Json.index<'#node'>[], current: Json.index<'#node'> }
>= getProofState_internal;
+const goToRoot_internal: Server.SetRequest<goal,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.goToRoot',
+ input: jGoal,
+ output: Json.jNull,
+ signals: [],
+};
+/** Go to root of proof tree */
+export const goToRoot: Server.SetRequest<goal,null>= goToRoot_internal;
+
+const goToPending_internal: Server.SetRequest<[ goal, number ],null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.goToPending',
+ input: Json.jPair( jGoal, Json.jNumber,),
+ output: Json.jNull,
+ signals: [],
+};
+/** Go to k-th pending node of proof tree */
+export const goToPending: Server.SetRequest<[ goal, number ],null>= goToPending_internal;
+
+const goForward_internal: Server.SetRequest<goal,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.goForward',
+ input: jGoal,
+ output: Json.jNull,
+ signals: [],
+};
+/** Forward to next pending node */
+export const goForward: Server.SetRequest<goal,null>= goForward_internal;
+
+const goToNode_internal: Server.SetRequest<Json.index<'#node'>,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.goToNode',
+ input: Json.jIndex<'#node'>('#node'),
+ output: Json.jNull,
+ signals: [],
+};
+/** Set current node of associated proof tree */
+export const goToNode: Server.SetRequest<Json.index<'#node'>,null>= goToNode_internal;
+
+const removeNode_internal: Server.SetRequest<Json.index<'#node'>,null> = {
+ kind: Server.RqKind.SET,
+ name: 'plugins.wp.removeNode',
+ input: Json.jIndex<'#node'>('#node'),
+ output: Json.jNull,
+ signals: [],
+};
+/** Forward to next pending node */
+export const removeNode: Server.SetRequest<Json.index<'#node'>,null>= removeNode_internal;
+
/* ------------------------------------- */
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index 18afa7f14d7..95f598ec56e 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -109,7 +109,8 @@ let rec reset_node n =
if Wpo.is_tactic n.goal then Wpo.remove n.goal ;
match n.script with
| Opened | Script _ -> ()
- | Tactic(_,children) -> iter_all reset_node children
+ | Tactic(_,children) ->
+ n.script <- Opened ; iter_all reset_node children
let reset_root = function None -> () | Some n -> reset_node n
@@ -123,7 +124,7 @@ let reset t =
t.saved <- false ;
end
-let remove w = if PROOFS.mem w then reset (PROOFS.get w)
+let clear w = if PROOFS.mem w then reset (PROOFS.get w)
let saved t = t.saved
let set_saved t s = t.saved <- s
@@ -195,6 +196,7 @@ let main t = t.main
let head t = match t.head with
| None -> t.main
| Some n -> n.goal
+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
@@ -279,20 +281,18 @@ let rec forward t =
forward t ;
end
+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 t =
match t.head with
| None -> ()
- | Some node ->
- begin
- Wpo.clear_results node.goal ;
- match node.script with
- | Opened ->
- t.head <- node.parent ;
- if t.head = None then t.root <- None ;
- | Tactic _ | Script _ ->
- (*TODO: save the current script *)
- node.script <- Opened ;
- end
+ | Some node -> remove t node
(* -------------------------------------------------------------------------- *)
(* --- Sub-Goal --- *)
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index eb17cd87687..4e0cd3d9f62 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -42,7 +42,7 @@ end
val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
val proof : main:Wpo.t -> tree
val reset : tree -> unit
-val remove : Wpo.t -> unit
+val clear : Wpo.t -> unit
(** Re-compute stats & set status of the entire script *)
val validate : tree -> unit
@@ -70,10 +70,10 @@ val set_saved : tree -> bool -> unit
val status : tree -> status
val current : tree -> current
val goto : tree -> position -> unit
-
val root : tree -> node
val main : tree -> Wpo.t
val head : tree -> Wpo.t
+val tree : node -> tree
val goal : node -> Wpo.t
val tree_context : tree -> WpContext.t
val node_context : node -> WpContext.t
@@ -89,6 +89,7 @@ val get_strategies : node -> int * Strategy.t array (* current index *)
val set_strategies : node -> ?index:int -> Strategy.t array -> unit
val forward : tree -> unit
val cancel : tree -> unit
+val remove : tree -> node -> unit
type fork
val anchor : tree -> ?node:node -> unit -> node
diff --git a/src/plugins/wp/gui/GuiNavigator.ml b/src/plugins/wp/gui/GuiNavigator.ml
index 5deefdb1887..5f1ed5226ab 100644
--- a/src/plugins/wp/gui/GuiNavigator.ml
+++ b/src/plugins/wp/gui/GuiNavigator.ml
@@ -298,7 +298,7 @@ class behavior
method private popup_delete_script () =
match popup_target with
- | Some(w,_) -> ProofEngine.remove w ; ProofSession.remove w
+ | Some(w,_) -> ProofEngine.clear w ; ProofSession.remove w
| None -> ()
method private popup_run mode () =
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 1288c3437da..3ff25c452dd 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -52,7 +52,7 @@ module INDEX = State_builder.Ref
let default () = Hashtbl.create 0
end)
-module WPO : D.S with type t = Wpo.t =
+module Goal : D.S with type t = Wpo.t =
struct
type t = Wpo.t
let jtype = D.declare ~package ~name:"goal"
@@ -146,7 +146,7 @@ let () = R.register ~package ~kind:`GET ~name:"getAvailableProvers"
Why3Provers.provers ())
(* -------------------------------------------------------------------------- *)
-(* --- WPO Array --- *)
+(* --- Goal Array --- *)
(* -------------------------------------------------------------------------- *)
let gmodel : Wpo.t S.model = S.model ()
@@ -261,10 +261,10 @@ let () = R.register ~package ~kind:`SET ~name:"cancelProofTasks"
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 name = "node" end)
let () =
- let snode = R.signature ~input:(module NODE) () in
+ let snode = R.signature ~input:(module Node) () in
let set_title = R.result snode ~name:"result"
~descr:(Md.plain "Proof node title") (module D.Jstring) in
let set_proved = R.result snode ~name:"proved"
@@ -292,11 +292,11 @@ let () =
(* -------------------------------------------------------------------------- *)
let () =
- let state = R.signature ~input:(module WPO) () in
+ 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
+ ~descr:(Md.plain "Current proof node.") (module Node) in
let set_parents = R.result state ~name:"parents"
- ~descr:(Md.plain "Proof node parents.") (module D.Jlist(NODE)) in
+ ~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"
@@ -310,7 +310,7 @@ let () =
(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
+ (module D.Jlist(D.Jpair(D.Jstring)(Node))) in
R.register_sig ~package
~kind:`GET ~name:"getProofState"
~descr:(Md.plain "Current Proof Status of a Goal") state
@@ -338,3 +338,52 @@ let () =
end
(* -------------------------------------------------------------------------- *)
+(* --- Proof Tree Management --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = R.register ~package ~kind:`SET ~name:"goToRoot"
+ ~descr:(Md.plain "Go to root of proof tree")
+ ~input:(module 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:"goToPending"
+ ~descr:(Md.plain "Go to k-th pending node of proof tree")
+ ~input:(module D.Jpair(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:"goForward"
+ ~descr:(Md.plain "Forward to next pending node")
+ ~input:(module 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:"goToNode"
+ ~descr:(Md.plain "Set current node of associated proof tree")
+ ~input:(module Node) ~output:(module D.Junit)
+ 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 "Forward to next pending node")
+ ~input:(module Node) ~output:(module D.Junit)
+ begin fun node ->
+ let tree = ProofEngine.tree node in
+ ProofEngine.remove tree node ;
+ R.emit proofStatus ;
+ end
+
+(* -------------------------------------------------------------------------- *)
--
GitLab