From 08b4ec9aa68c8d3344b49e5481d3352ec3e120dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 4 Dec 2023 19:02:47 +0100
Subject: [PATCH] [server] indexed types registration
---
.../frama-c/plugins/eva/api/values/index.ts | 7 ++-
.../src/frama-c/plugins/wp/api/tip/index.ts | 34 +++++++++--
src/plugins/eva/api/values_request.ml | 17 +++---
src/plugins/server/data.ml | 19 +++---
src/plugins/server/data.mli | 4 +-
src/plugins/wp/wpTipApi.ml | 59 ++++++++++++-------
6 files changed, 91 insertions(+), 49 deletions(-)
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 652447eeab0..26435c8173c 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/tip/index.ts b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
index 45e9f700b57..6efc2cf639a 100644
--- a/ivette/src/frama-c/plugins/wp/api/tip/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
@@ -187,6 +187,30 @@ const removeNode_internal: Server.SetRequest<node,null> = {
/** Remove node from tree and go to parent */
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 = {
name: 'plugins.wp.tip.printStatus',
@@ -263,16 +287,15 @@ const clearSelection_internal: Server.SetRequest<node,null> = {
export const clearSelection: Server.SetRequest<node,null>= clearSelection_internal;
const setSelection_internal: Server.SetRequest<
- { node: 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: jNode,
- part: Json.jOption(Json.jKey<'#part'>('#part')),
- term: Json.jOption(Json.jKey<'#term'>('#term')),
+ part: Json.jOption(jPart),
+ term: Json.jOption(jTerm),
extend: Json.jOption(Json.jBoolean),
}),
output: Json.jNull,
@@ -280,8 +303,7 @@ const setSelection_internal: Server.SetRequest<
};
/** Set node selection */
export const setSelection: Server.SetRequest<
- { node: node, part?: Json.key<'#part'>, term?: Json.key<'#term'>,
- extend?: boolean },
+ { node: node, part?: part, term?: term, extend?: boolean },
null
>= setSelection_internal;
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 6f9dacae8d6..4c308de1704 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 c1b7a350ae7..bdaa0d0c315 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -580,7 +580,9 @@ end
module type Info =
sig
+ val package: package
val name: string
+ val descr: Markdown.text
end
(** Simplified [Map.S] *)
@@ -663,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)
@@ -698,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)
@@ -755,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
@@ -795,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 812c0d5189d..c9fe14a36a5 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -341,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/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index 734f8f74d4c..6ed15dd834f 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -42,12 +42,13 @@ let package = P.package ~plugin:"wp" ~name:"tip"
let proofStatus = R.signal ~package ~name:"proofStatus"
~descr:(Md.plain "Proof Status has changed")
-module Node =
-struct
- include D.Index(Map.Make(ProofEngine.Node))(struct let name = "node" end)
- let jtype =
- D.declare ~package ~name:"node" ~descr:(Md.plain "Proof Node index") jtype
-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 inode = R.signature ~input:(module Node) () in
@@ -177,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 ]
@@ -192,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
@@ -223,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 (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 (of_part p) pp fmt x
+ = 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
(* -------------------------------------------------------------------------- *)
--
GitLab