diff --git a/ivette/api/dive/index.ts b/ivette/api/dive/index.ts index 13457b8a8437d45428cc7af1eec1303a844f8fbe..cb63f717365c646ff9a9096cc973c33ace8a641f 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 aea3d3f0bdba01973b0e554b3e797350a039562f..7d601286791e8c558e22d14179256be5705b43a5 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 5550b01e4f17696a3b048792d87c1417dacfaa7d..0199b1c0fef3e13e81b684717a6cfccc5956c4cb 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 912ef274e80499f15b020d7939f46e26081f73c4..456217329fafb750acee4fcda807ce0c6519dc78 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 4c6a826fe51688403b479207f5d389d18b8f8237..bfe9af2c2bb4b638f0c63126d0e0c4a3b8d91a77 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 9660798f216dde9577c7a914cbfd711e86c7bb01..fcfcf35b1fbe3b9ca7c272b7cabd9754cc24bbfa 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 bf359e9c59e686d0d30c1deb84c40696ea785aa7..3388bcd231114a6f40673b35e468b597ed759b8c 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