From b4cc2f4320854150dae297ccc8f6b7918b17a092 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 25 Jun 2020 01:53:06 +0200
Subject: [PATCH] [ivette] declaration dependencies
---
ivette/api/dive/index.ts | 8 +-
ivette/api/kernel/ast/index.ts | 110 +++++++++++++-------------
ivette/api/kernel/data/index.ts | 20 ++---
ivette/api/kernel/project/index.ts | 16 ++--
ivette/api/kernel/properties/index.ts | 66 ++++++++--------
ivette/api/kernel/services/index.ts | 20 ++---
ivette/api/server_tsc.ml | 42 +++++++++-
7 files changed, 160 insertions(+), 122 deletions(-)
diff --git a/ivette/api/dive/index.ts b/ivette/api/dive/index.ts
index 13457b8a843..cb63f717365 100644
--- a/ivette/api/dive/index.ts
+++ b/ivette/api/dive/index.ts
@@ -24,10 +24,6 @@ export interface variableName {
varName: string;
}
-/** Safe decoder for `variableName` */
-export const jVariableNameSafe: Json.Safe<variableName> =
- Json.jFail(jVariableName,'VariableName expected');
-
/** Loose decoder for `variableName` */
export const jVariableName: Json.Loose<variableName> =
Json.jObject({
@@ -35,6 +31,10 @@ export const jVariableName: Json.Loose<variableName> =
varName: Json.jFail(Json.jString,'String expected'),
});
+/** Safe decoder for `variableName` */
+export const jVariableNameSafe: Json.Safe<variableName> =
+ Json.jFail(jVariableName,'VariableName expected');
+
/** Natural order for `variableName` */
export const byVariableName: Compare.Order<variableName> =
Compare.byFields
diff --git a/ivette/api/kernel/ast/index.ts b/ivette/api/kernel/ast/index.ts
index aea3d3f0bdb..7d601286791 100644
--- a/ivette/api/kernel/ast/index.ts
+++ b/ivette/api/kernel/ast/index.ts
@@ -62,13 +62,13 @@ export enum markerKind {
property = 'property',
}
+/** Loose decoder for `markerKind` */
+export const jMarkerKind: Json.Loose<markerKind> = Json.jEnum(markerKind);
+
/** Safe decoder for `markerKind` */
export const jMarkerKindSafe: Json.Safe<markerKind> =
Json.jFail(Json.jEnum(markerKind),'kernel.ast.markerKind expected');
-/** Loose decoder for `markerKind` */
-export const jMarkerKind: Json.Loose<markerKind> = Json.jEnum(markerKind);
-
/** Natural order for `markerKind` */
export const byMarkerKind: Compare.Order<markerKind> =
Compare.byEnum(markerKind);
@@ -81,20 +81,6 @@ export const markerKindTags: Server.GetRequest<null,tag[]> = {
output: Json.jList(jTag),
};
-/** Marker informations */
-export const markerInfo: State.Array<'#markerInfo',markerInfoData> = {
- name: 'kernel.ast.markerInfo',
- key: 'key',
- signal: signalMarkerInfo,
- fetch: fetchMarkerInfo,
- reload: reloadMarkerInfo,
-};
-
-/** Signal for array [`markerInfo`](#markerinfo) */
-export const signalMarkerInfo: Server.Signal = {
- name: 'kernel.ast.signalMarkerInfo',
-};
-
/** Data for array rows [`markerInfo`](#markerinfo) */
export interface markerInfoData {
/** Entry identifier. */
@@ -107,10 +93,6 @@ export interface markerInfoData {
descr: string;
}
-/** Safe decoder for `markerInfoData` */
-export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> =
- Json.jFail(jMarkerInfoData,'MarkerInfoData expected');
-
/** Loose decoder for `markerInfoData` */
export const jMarkerInfoData: Json.Loose<markerInfoData> =
Json.jObject({
@@ -120,6 +102,10 @@ export const jMarkerInfoData: Json.Loose<markerInfoData> =
descr: Json.jFail(Json.jString,'String expected'),
});
+/** Safe decoder for `markerInfoData` */
+export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> =
+ Json.jFail(jMarkerInfoData,'MarkerInfoData expected');
+
/** Natural order for `markerInfoData` */
export const byMarkerInfoData: Compare.Order<markerInfoData> =
Compare.byFields
@@ -131,6 +117,19 @@ export const byMarkerInfoData: Compare.Order<markerInfoData> =
descr: Compare.primitive,
});
+/** Signal for array [`markerInfo`](#markerinfo) */
+export const signalMarkerInfo: Server.Signal = {
+ name: 'kernel.ast.signalMarkerInfo',
+};
+
+/** Force full reload for array [`markerInfo`](#markerinfo) */
+export const reloadMarkerInfo: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.ast.reloadMarkerInfo',
+ input: Json.jNull,
+ output: Json.jNull,
+};
+
/** Data fetcher for array [`markerInfo`](#markerinfo) */
export const fetchMarkerInfo: Server.GetRequest<number,
{ pending: number, updated: markerInfoData[],
@@ -146,12 +145,13 @@ export const fetchMarkerInfo: Server.GetRequest<number,
}),
};
-/** Force full reload for array [`markerInfo`](#markerinfo) */
-export const reloadMarkerInfo: Server.GetRequest<null,null> = {
- kind: Server.RqKind.GET,
- name: 'kernel.ast.reloadMarkerInfo',
- input: Json.jNull,
- output: Json.jNull,
+/** Marker informations */
+export const markerInfo: State.Array<'#markerInfo',markerInfoData> = {
+ name: 'kernel.ast.markerInfo',
+ key: 'key',
+ signal: signalMarkerInfo,
+ fetch: fetchMarkerInfo,
+ reload: reloadMarkerInfo,
};
/** Localizable AST markers */
@@ -160,10 +160,6 @@ export type marker =
Json.key<'#expr'> | Json.key<'#term'> | Json.key<'#global'> |
Json.key<'#property'>;
-/** Safe decoder for `marker` */
-export const jMarkerSafe: Json.Safe<marker> =
- Json.jFail(jMarker,'Marker expected');
-
/** Loose decoder for `marker` */
export const jMarker: Json.Loose<marker> =
Json.jUnion<Json.key<'#stmt'> | Json.key<'#decl'> | Json.key<'#lval'> |
@@ -178,6 +174,10 @@ export const jMarker: Json.Loose<marker> =
Json.jKey('#property'),
);
+/** Safe decoder for `marker` */
+export const jMarkerSafe: Json.Safe<marker> =
+ Json.jFail(jMarker,'Marker expected');
+
/** Natural order for `marker` */
export const byMarker: Compare.Order<marker> = Compare.structural;
@@ -197,20 +197,6 @@ export const printFunction: Server.GetRequest<Json.key<'#fct'>,text> = {
output: jText,
};
-/** AST Functions */
-export const functions: State.Array<'#functions',functionsData> = {
- name: 'kernel.ast.functions',
- key: 'key',
- signal: signalFunctions,
- fetch: fetchFunctions,
- reload: reloadFunctions,
-};
-
-/** Signal for array [`functions`](#functions) */
-export const signalFunctions: Server.Signal = {
- name: 'kernel.ast.signalFunctions',
-};
-
/** Data for array rows [`functions`](#functions) */
export interface functionsData {
/** Entry identifier. */
@@ -221,10 +207,6 @@ export interface functionsData {
signature: string;
}
-/** Safe decoder for `functionsData` */
-export const jFunctionsDataSafe: Json.Safe<functionsData> =
- Json.jFail(jFunctionsData,'FunctionsData expected');
-
/** Loose decoder for `functionsData` */
export const jFunctionsData: Json.Loose<functionsData> =
Json.jObject({
@@ -233,6 +215,10 @@ export const jFunctionsData: Json.Loose<functionsData> =
signature: Json.jFail(Json.jString,'String expected'),
});
+/** Safe decoder for `functionsData` */
+export const jFunctionsDataSafe: Json.Safe<functionsData> =
+ Json.jFail(jFunctionsData,'FunctionsData expected');
+
/** Natural order for `functionsData` */
export const byFunctionsData: Compare.Order<functionsData> =
Compare.byFields
@@ -242,6 +228,19 @@ export const byFunctionsData: Compare.Order<functionsData> =
signature: Compare.primitive,
});
+/** Signal for array [`functions`](#functions) */
+export const signalFunctions: Server.Signal = {
+ name: 'kernel.ast.signalFunctions',
+};
+
+/** Force full reload for array [`functions`](#functions) */
+export const reloadFunctions: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.ast.reloadFunctions',
+ input: Json.jNull,
+ output: Json.jNull,
+};
+
/** Data fetcher for array [`functions`](#functions) */
export const fetchFunctions: Server.GetRequest<number,
{ pending: number, updated: functionsData[],
@@ -257,12 +256,13 @@ export const fetchFunctions: Server.GetRequest<number,
}),
};
-/** Force full reload for array [`functions`](#functions) */
-export const reloadFunctions: Server.GetRequest<null,null> = {
- kind: Server.RqKind.GET,
- name: 'kernel.ast.reloadFunctions',
- input: Json.jNull,
- output: Json.jNull,
+/** AST Functions */
+export const functions: State.Array<'#functions',functionsData> = {
+ name: 'kernel.ast.functions',
+ key: 'key',
+ signal: signalFunctions,
+ fetch: fetchFunctions,
+ reload: reloadFunctions,
};
/** Get textual information about a marker */
diff --git a/ivette/api/kernel/data/index.ts b/ivette/api/kernel/data/index.ts
index 5550b01e4f1..0199b1c0fef 100644
--- a/ivette/api/kernel/data/index.ts
+++ b/ivette/api/kernel/data/index.ts
@@ -19,23 +19,19 @@ import * as State from 'frama-c/states';
/** Markdown (inlined) text. */
export type markdown = string;
+/** Loose decoder for `markdown` */
+export const jMarkdown: Json.Loose<markdown> = Json.jString;
+
/** Safe decoder for `markdown` */
export const jMarkdownSafe: Json.Safe<markdown> =
Json.jFail(Json.jString,'String expected');
-/** Loose decoder for `markdown` */
-export const jMarkdown: Json.Loose<markdown> = Json.jString;
-
/** Natural order for `markdown` */
export const byMarkdown: Compare.Order<markdown> = Compare.primitive;
/** Rich text format uses `[tag; …text ]` to apply the tag `tag` to the enclosed text. Empty tag `""` can also used to simply group text together. */
export type text = null | string | text[];
-/** Safe decoder for `text` */
-export const jTextSafe: Json.Safe<text> =
- (_x) => Json.jFail(jText,'Text expected')(_x);
-
/** Loose decoder for `text` */
export const jText: Json.Loose<text> =
(_x) => Json.jUnion<null | string | text[]>(
@@ -44,6 +40,10 @@ export const jText: Json.Loose<text> =
Json.jList(jText),
)(_x);
+/** Safe decoder for `text` */
+export const jTextSafe: Json.Safe<text> =
+ (_x) => Json.jFail(jText,'Text expected')(_x);
+
/** Natural order for `text` */
export const byText: Compare.Order<text> =
(_x,_y) => Compare.structural(_x,_y);
@@ -51,9 +51,6 @@ export const byText: Compare.Order<text> =
/** Enum Tag Description */
export type tag = { name: string, label: markdown, descr: markdown };
-/** Safe decoder for `tag` */
-export const jTagSafe: Json.Safe<tag> = Json.jFail(jTag,'Tag expected');
-
/** Loose decoder for `tag` */
export const jTag: Json.Loose<tag> =
Json.jObject({
@@ -62,6 +59,9 @@ export const jTag: Json.Loose<tag> =
descr: jMarkdownSafe,
});
+/** Safe decoder for `tag` */
+export const jTagSafe: Json.Safe<tag> = Json.jFail(jTag,'Tag expected');
+
/** Natural order for `tag` */
export const byTag: Compare.Order<tag> =
Compare.byFields
diff --git a/ivette/api/kernel/project/index.ts b/ivette/api/kernel/project/index.ts
index 912ef274e80..456217329fa 100644
--- a/ivette/api/kernel/project/index.ts
+++ b/ivette/api/kernel/project/index.ts
@@ -20,10 +20,6 @@ import * as State from 'frama-c/states';
export type projectInfo =
{ id: Json.key<'#project'>, name: string, current: boolean };
-/** Safe decoder for `projectInfo` */
-export const jProjectInfoSafe: Json.Safe<projectInfo> =
- Json.jFail(jProjectInfo,'ProjectInfo expected');
-
/** Loose decoder for `projectInfo` */
export const jProjectInfo: Json.Loose<projectInfo> =
Json.jObject({
@@ -32,6 +28,10 @@ export const jProjectInfo: Json.Loose<projectInfo> =
current: Json.jFail(Json.jBoolean,'Boolean expected'),
});
+/** Safe decoder for `projectInfo` */
+export const jProjectInfoSafe: Json.Safe<projectInfo> =
+ Json.jFail(jProjectInfo,'ProjectInfo expected');
+
/** Natural order for `projectInfo` */
export const byProjectInfo: Compare.Order<projectInfo> =
Compare.byFields
@@ -45,10 +45,6 @@ export const byProjectInfo: Compare.Order<projectInfo> =
export type projectRequest =
{ project: Json.key<'#project'>, request: string, data: Json.json };
-/** Safe decoder for `projectRequest` */
-export const jProjectRequestSafe: Json.Safe<projectRequest> =
- Json.jFail(jProjectRequest,'ProjectRequest expected');
-
/** Loose decoder for `projectRequest` */
export const jProjectRequest: Json.Loose<projectRequest> =
Json.jObject({
@@ -57,6 +53,10 @@ export const jProjectRequest: Json.Loose<projectRequest> =
data: Json.jAny,
});
+/** Safe decoder for `projectRequest` */
+export const jProjectRequestSafe: Json.Safe<projectRequest> =
+ Json.jFail(jProjectRequest,'ProjectRequest expected');
+
/** Natural order for `projectRequest` */
export const byProjectRequest: Compare.Order<projectRequest> =
Compare.byFields
diff --git a/ivette/api/kernel/properties/index.ts b/ivette/api/kernel/properties/index.ts
index 4c6a826fe51..bfe9af2c2bb 100644
--- a/ivette/api/kernel/properties/index.ts
+++ b/ivette/api/kernel/properties/index.ts
@@ -98,13 +98,13 @@ export enum propKind {
lemma = 'lemma',
}
+/** Loose decoder for `propKind` */
+export const jPropKind: Json.Loose<propKind> = Json.jEnum(propKind);
+
/** Safe decoder for `propKind` */
export const jPropKindSafe: Json.Safe<propKind> =
Json.jFail(Json.jEnum(propKind),'kernel.properties.propKind expected');
-/** Loose decoder for `propKind` */
-export const jPropKind: Json.Loose<propKind> = Json.jEnum(propKind);
-
/** Natural order for `propKind` */
export const byPropKind: Compare.Order<propKind> = Compare.byEnum(propKind);
@@ -142,13 +142,13 @@ export enum propStatus {
unknown_but_dead = 'unknown_but_dead',
}
+/** Loose decoder for `propStatus` */
+export const jPropStatus: Json.Loose<propStatus> = Json.jEnum(propStatus);
+
/** Safe decoder for `propStatus` */
export const jPropStatusSafe: Json.Safe<propStatus> =
Json.jFail(Json.jEnum(propStatus),'kernel.properties.propStatus expected');
-/** Loose decoder for `propStatus` */
-export const jPropStatus: Json.Loose<propStatus> = Json.jEnum(propStatus);
-
/** Natural order for `propStatus` */
export const byPropStatus: Compare.Order<propStatus> =
Compare.byEnum(propStatus);
@@ -201,13 +201,13 @@ export enum alarms {
bool_value = 'bool_value',
}
+/** Loose decoder for `alarms` */
+export const jAlarms: Json.Loose<alarms> = Json.jEnum(alarms);
+
/** Safe decoder for `alarms` */
export const jAlarmsSafe: Json.Safe<alarms> =
Json.jFail(Json.jEnum(alarms),'kernel.properties.alarms expected');
-/** Loose decoder for `alarms` */
-export const jAlarms: Json.Loose<alarms> = Json.jEnum(alarms);
-
/** Natural order for `alarms` */
export const byAlarms: Compare.Order<alarms> = Compare.byEnum(alarms);
@@ -219,20 +219,6 @@ export const alarmsTags: Server.GetRequest<null,tag[]> = {
output: Json.jList(jTag),
};
-/** Status of Registered Properties */
-export const status: State.Array<'#status',statusData> = {
- name: 'kernel.properties.status',
- key: 'key',
- signal: signalStatus,
- fetch: fetchStatus,
- reload: reloadStatus,
-};
-
-/** Signal for array [`status`](#status) */
-export const signalStatus: Server.Signal = {
- name: 'kernel.properties.signalStatus',
-};
-
/** Data for array rows [`status`](#status) */
export interface statusData {
/** Entry identifier. */
@@ -259,10 +245,6 @@ export interface statusData {
predicate?: string;
}
-/** Safe decoder for `statusData` */
-export const jStatusDataSafe: Json.Safe<statusData> =
- Json.jFail(jStatusData,'StatusData expected');
-
/** Loose decoder for `statusData` */
export const jStatusData: Json.Loose<statusData> =
Json.jObject({
@@ -279,6 +261,10 @@ export const jStatusData: Json.Loose<statusData> =
predicate: Json.jString,
});
+/** Safe decoder for `statusData` */
+export const jStatusDataSafe: Json.Safe<statusData> =
+ Json.jFail(jStatusData,'StatusData expected');
+
/** Natural order for `statusData` */
export const byStatusData: Compare.Order<statusData> =
Compare.byFields
@@ -299,6 +285,19 @@ export const byStatusData: Compare.Order<statusData> =
predicate: Compare.defined(Compare.primitive),
});
+/** Signal for array [`status`](#status) */
+export const signalStatus: Server.Signal = {
+ name: 'kernel.properties.signalStatus',
+};
+
+/** Force full reload for array [`status`](#status) */
+export const reloadStatus: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.properties.reloadStatus',
+ input: Json.jNull,
+ output: Json.jNull,
+};
+
/** Data fetcher for array [`status`](#status) */
export const fetchStatus: Server.GetRequest<number,
{ pending: number, updated: statusData[], removed: Json.key<'#status'>[],
@@ -314,12 +313,13 @@ export const fetchStatus: Server.GetRequest<number,
}),
};
-/** Force full reload for array [`status`](#status) */
-export const reloadStatus: Server.GetRequest<null,null> = {
- kind: Server.RqKind.GET,
- name: 'kernel.properties.reloadStatus',
- input: Json.jNull,
- output: Json.jNull,
+/** Status of Registered Properties */
+export const status: State.Array<'#status',statusData> = {
+ name: 'kernel.properties.status',
+ key: 'key',
+ signal: signalStatus,
+ fetch: fetchStatus,
+ reload: reloadStatus,
};
/* ------------------------------------- */
diff --git a/ivette/api/kernel/services/index.ts b/ivette/api/kernel/services/index.ts
index 9660798f216..fcfcf35b1fb 100644
--- a/ivette/api/kernel/services/index.ts
+++ b/ivette/api/kernel/services/index.ts
@@ -51,10 +51,6 @@ export const load: Server.SetRequest<string,string | undefined> = {
export type source =
{ dir: string, base: string, file: string, line: number };
-/** Safe decoder for `source` */
-export const jSourceSafe: Json.Safe<source> =
- Json.jFail(jSource,'Source expected');
-
/** Loose decoder for `source` */
export const jSource: Json.Loose<source> =
Json.jObject({
@@ -64,6 +60,10 @@ export const jSource: Json.Loose<source> =
line: Json.jFail(Json.jNumber,'Number expected'),
});
+/** Safe decoder for `source` */
+export const jSourceSafe: Json.Safe<source> =
+ Json.jFail(jSource,'Source expected');
+
/** Natural order for `source` */
export const bySource: Compare.Order<source> =
Compare.byFields
@@ -90,13 +90,13 @@ export enum logkind {
DEBUG = 'DEBUG',
}
+/** Loose decoder for `logkind` */
+export const jLogkind: Json.Loose<logkind> = Json.jEnum(logkind);
+
/** Safe decoder for `logkind` */
export const jLogkindSafe: Json.Safe<logkind> =
Json.jFail(Json.jEnum(logkind),'kernel.services.logkind expected');
-/** Loose decoder for `logkind` */
-export const jLogkind: Json.Loose<logkind> = Json.jEnum(logkind);
-
/** Natural order for `logkind` */
export const byLogkind: Compare.Order<logkind> = Compare.byEnum(logkind);
@@ -122,9 +122,6 @@ export interface log {
source?: source;
}
-/** Safe decoder for `log` */
-export const jLogSafe: Json.Safe<log> = Json.jFail(jLog,'Log expected');
-
/** Loose decoder for `log` */
export const jLog: Json.Loose<log> =
Json.jObject({
@@ -135,6 +132,9 @@ export const jLog: Json.Loose<log> =
source: jSource,
});
+/** Safe decoder for `log` */
+export const jLogSafe: Json.Safe<log> = Json.jFail(jLog,'Log expected');
+
/** Natural order for `log` */
export const byLog: Compare.Order<log> =
Compare.byFields
diff --git a/ivette/api/server_tsc.ml b/ivette/api/server_tsc.ml
index bf359e9c59e..3388bcd2311 100644
--- a/ivette/api/server_tsc.ml
+++ b/ivette/api/server_tsc.ml
@@ -380,7 +380,45 @@ let makeDeclaration fmt names d =
(* --- Declaration Ranking --- *)
(* -------------------------------------------------------------------------- *)
-let byRank _ _ = 0
+type ranking = {
+ mutable rank : int ;
+ mutable mark : int Pkg.IdMap.t ;
+}
+
+let depends d =
+ match d.Pkg.d_kind with
+ | D_loose(id,(Jtuple _ | Jarray _)) -> [Pkg.Derived.safe id]
+ | D_safe(id,_) -> [Pkg.Derived.loose id]
+ | D_array _ ->
+ let id = d.d_ident in
+ let data = Pkg.Derived.data id in
+ [
+ data ;
+ Pkg.Derived.loose data ;
+ Pkg.Derived.safe data ;
+ Pkg.Derived.order data ;
+ Pkg.Derived.signal id ;
+ Pkg.Derived.reload id ;
+ Pkg.Derived.fetch id ;
+ ]
+ | _ -> []
+
+let next m id =
+ let r = m.rank in
+ m.mark <- Pkg.IdMap.add id r m.mark ;
+ m.rank <- succ r
+
+let mark m d =
+ let id = d.Pkg.d_ident in
+ if not (Pkg.IdMap.mem id m.mark) then
+ ( List.iter (next m) (depends d) ; next m id )
+
+let ranking ds =
+ let m = { rank = 0 ; mark = Pkg.IdMap.empty } in
+ List.iter (mark m) ds ;
+ let rk = m.mark in
+ let getRank a = try Pkg.IdMap.find a.Pkg.d_ident rk with Not_found -> 0 in
+ List.sort (fun a b -> getRank a - getRank b) ds
(* -------------------------------------------------------------------------- *)
(* --- Package Generator --- *)
@@ -421,7 +459,7 @@ let makePackage pkg name fmt =
) names ;
List.iter
(makeDeclaration fmt names)
- (List.sort byRank pkg.p_content) ;
+ (ranking pkg.p_content) ;
Format.pp_print_newline fmt () ;
Format.fprintf fmt "/* ------------------------------------- */@." ;
end
--
GitLab