diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in
index d5b7cf9e8dab5322982b805a00c69533c751197d..0c9644098263ac6ff133193aad18149ea977694a 100644
--- a/src/plugins/server/Makefile.in
+++ b/src/plugins/server/Makefile.in
@@ -79,7 +79,10 @@ include $(FRAMAC_SHARE)/Makefile.dynamic
##############
SERVER_API= \
- doc.mli syntax.mli data.mli request.mli states.mli
+ doc.mli syntax.mli data.mli request.mli states.mli \
+ kernel_main.mli \
+ kernel_ast.mli \
+ kernel_properties.mli
define Capitalize
$(shell printf "%s%s" \
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index ccc9b9a131f39e4f9e3643d15134d7aa82aa9c5e..fc2c301f10a7b9767efac7374f0807850a768a66 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -407,7 +407,7 @@ struct
}
type 'a tag = string
- type 'a prefix = string -> 'a tag
+ type 'a prefix = string
let tag_name tg = tg
let tag_label a = function
@@ -432,8 +432,6 @@ struct
let syntax (d : 'a dictionary) = d.syntax
let tag (d : 'a dictionary) ~name ?label ~descr ?value () : 'a tag =
- if d.published then
- invalid d.name (Printf.sprintf "published enum (%s)" name) ;
if Hashtbl.mem d.values name then
invalid d.name (Printf.sprintf "duplicate tag (%s)" name) ;
let tg = Syntax.{
@@ -448,17 +446,18 @@ struct
| Some v -> Hashtbl.add d.vindex v name
end ; name
- let prefix (d : 'a dictionary) ~prefix ?(var="*") ?label ~descr
- () : string -> 'a tag =
- if d.published then
- invalid d.name (Printf.sprintf "published enum (%s:*)" prefix) ;
- let make = Printf.sprintf "%s:%s" prefix in
+ let instance = Printf.sprintf "%s:%s"
+
+ let prefix (d : 'a dictionary) ~prefix ?(var="*") ?label ~descr () =
let tg = Syntax.{
- tag_name = make var ;
+ tag_name = instance prefix var ;
tag_label = tag_label (prefix ^ ".") label ;
tag_descr = descr ;
} in
- d.tags <- tg :: d.tags ; make
+ d.tags <- tg :: d.tags ; prefix
+
+ let extends d prefix ~name ?label ~descr ?value () =
+ tag d ~name:(instance prefix name) ?label ~descr ?value ()
let to_json name vindex v =
try `String (Hashtbl.find vindex v)
@@ -484,10 +483,9 @@ struct
type t = a
let descr = d.descr
let syntax =
- let tags = Syntax.tags ~title:d.title (List.rev d.tags) in
+ let tags () = [Syntax.tags ~title:d.title (List.rev d.tags)] in
Syntax.publish ~page:d.page ~name:d.name ~descr
- ~synopsis:(Syntax.string)
- ~details:[tags] ()
+ ~synopsis:(Syntax.string) ~generated:tags ()
let of_json = of_json d.name d.values
let to_json =
match tag with
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index 3297d75cbdae383ca6d3d1ac59698bdba41786ed..192bfc5b11cbfe2b68e74141c2a53bd6a24929c5 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -187,7 +187,7 @@ sig
type 'a dictionary
type 'a tag
- type 'a prefix = string -> 'a tag
+ type 'a prefix
val tag_name : 'a tag -> string
@@ -201,7 +201,9 @@ sig
The provided value, if any, will be used for decoding json tags.
If would be used also for encoding values to json tags if no [~tag]
function is provided when publishing the dictionnary.
- Registered values must be hashable with [Hashtbl.hash] function. *)
+ Registered values must be hashable with [Hashtbl.hash] function.
+
+ You may register a new tag {i after} the dictionary has been published. *)
val tag : 'a dictionary ->
name:string ->
?label:Markdown.text -> descr:Markdown.text ->
@@ -213,13 +215,26 @@ sig
To decoding from json is provided to prefix tags.
Encoding is done by emitting tags with form ['prefix:*'].
The variable part of the prefix is documented as ['prefix:xxx']
- when [~var:"xxx"] is provided. *)
+ when [~var:"xxx"] is provided.
+
+ You may register a new prefix-tag {i after} the dictionary has
+ been published. *)
val prefix : 'a dictionary ->
prefix:string -> ?var:string ->
?label:Markdown.text -> descr:Markdown.text ->
unit -> 'a prefix
- (** Obtain all the tags from the dictionnary. *)
+ (** Returns the tag for a value associated with the given prefix. *)
+ val instance : 'a prefix -> string -> 'a tag
+
+ (** Publish a new instance in the documentation. *)
+ val extends : 'a dictionary -> 'a prefix ->
+ name:string ->
+ ?label:Markdown.text -> descr:Markdown.text ->
+ ?value:'a ->
+ unit -> 'a tag
+
+ (** Obtain all the tags registered in the dictionnary so far. *)
val tags : 'a dictionary -> Tag.t list
val page : 'a dictionary -> Doc.page
diff --git a/src/plugins/server/doc.ml b/src/plugins/server/doc.ml
index cab11780aec9205349d18ca0595ccef333d7fcd3..92423076609535541797e43caf7a428fba7018ca 100644
--- a/src/plugins/server/doc.ml
+++ b/src/plugins/server/doc.ml
@@ -31,6 +31,8 @@ module Pages = Map.Make(String)
type chapter = [ `Protocol | `Kernel | `Plugin of string ]
+type section = (unit -> Markdown.elements)
+
type page = {
path : string ;
rootdir : string ; (* path to document root *)
@@ -38,7 +40,7 @@ type page = {
title : string ;
order : int ;
intro : Markdown.elements ;
- mutable sections : Markdown.elements list ;
+ mutable sections : section list ;
}
let order = ref 0
@@ -82,10 +84,15 @@ let page chapter ~title ~filename =
sections=[] } in
pages := Pages.add path page !pages ; page
-let publish ~page ?name ?(index=[]) ~title content sections =
+let static () = []
+
+let publish ~page ?name ?(index=[]) ~title
+ ?(contents=[])
+ ?(generated=static)
+ () =
let id = match name with Some id -> id | None -> title in
let href = Section( page.path , id ) in
- let section = Markdown.section ?name ~title (content @ sections) in
+ let section () = Markdown.section ?name ~title (contents @ generated ()) in
List.iter (fun entry -> entries := (entry , href) :: !entries) index ;
page.sections <- section :: page.sections ; href
@@ -203,12 +210,16 @@ let pp_one_page ~root ~page ~title body =
with Sys_error e ->
Senv.fatal "Could not open file %s for writing: %s" full_path e
+let rec build contents = function
+ | [] -> contents
+ | s::sections -> build (s () :: contents) sections
+
let dump ~root ?(meta=true) () =
begin
Pages.iter
(fun path page ->
Senv.feedback "[doc] Page: '%s'" path ;
- let body = Markdown.subsections page.intro (List.rev page.sections) in
+ let body = Markdown.subsections page.intro (build [] page.sections) in
let title = page.title in
pp_one_page ~root ~page:path ~title body ;
if meta then
diff --git a/src/plugins/server/doc.mli b/src/plugins/server/doc.mli
index e1b2c6414d3596de73f9c44b60e5b714486721a7..d3f3d2978bef014c929cf07bd9ffd42f40ba0767 100644
--- a/src/plugins/server/doc.mli
+++ b/src/plugins/server/doc.mli
@@ -56,9 +56,9 @@ val publish :
?name:string ->
?index:string list ->
title:string ->
- Markdown.elements ->
- Markdown.elements ->
- Markdown.href
+ ?contents:Markdown.elements ->
+ ?generated:(unit -> Markdown.elements) ->
+ unit -> Markdown.href
(** Dumps all published pages of documentations. Unless [~meta:false],
also generates METADATA for each page in
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 46e46b0f2507139bee3c1cd647de33d9436991b1..02c7e613c05e7fb111618322a3e2e3145d41a087 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -20,9 +20,7 @@
(* *)
(**************************************************************************)
-module Sy = Syntax
module Md = Markdown
-module Js = Yojson.Basic.Util
open Data
open Kernel_main
@@ -62,8 +60,6 @@ struct
let t_decreases = t_clause "decreases"
let t_assigns = t_clause "assigns"
let t_froms = t_kind "froms" "Clause `@assigns … \\from …`"
- let t_ext = Enum.prefix kinds ~prefix:"ext" ~var:"<clause>"
- ~descr:(Md.plain "ACSL extension `<clause>`") ()
let t_assert = t_clause "assert"
let t_loop_invariant = t_loop "invariant"
@@ -71,8 +67,6 @@ struct
let t_loop_variant = t_loop "variant"
let t_loop_allocates = t_loop "allocates"
let t_loop_pragma = t_loop "pragma"
- let t_loop_ext = Enum.prefix kinds ~prefix:"loop-ext" ~var:"<clause>"
- ~descr:(Md.plain "ACSL loop extension `loop <clause>`") ()
let t_reachable = t_kind "reachable" "Reachable statement"
let t_code_contract = t_kind "code-contract" "Statement Contract"
@@ -83,7 +77,14 @@ struct
let t_axiomatic = t_kind "axiomatic" "Axiomatic definitions"
let t_axiom = t_kind "axiom" "Logical axiom"
let t_lemma = t_kind "lemma" "Logical lemma"
- let t_other = Enum.prefix kinds ~prefix:"prop" ~var:"<prop>"
+
+ let p_ext = Enum.prefix kinds ~prefix:"ext" ~var:"<clause>"
+ ~descr:(Md.plain "ACSL extension `<clause>`") ()
+
+ let p_loop_ext = Enum.prefix kinds ~prefix:"loop-ext" ~var:"<clause>"
+ ~descr:(Md.plain "ACSL loop extension `loop <clause>`") ()
+
+ let p_other = Enum.prefix kinds ~prefix:"prop" ~var:"<prop>"
~descr:(Md.plain "Plugin Specific properties") ()
open Property
@@ -100,7 +101,7 @@ struct
| PKEnsures(_,Returns) -> t_returns
| PKTerminates -> t_terminates
end
- | IPExtended { ie_ext={ ext_name } } -> t_ext ext_name
+ | IPExtended { ie_ext={ ext_name } } -> Enum.instance p_ext ext_name
| IPAxiomatic _ -> t_axiomatic
| IPAxiom _ -> t_axiom
| IPLemma _ -> t_lemma
@@ -117,7 +118,7 @@ struct
| AAssigns _ -> t_loop_assigns
| AAllocation _ -> t_loop_allocates
| APragma _ -> t_loop_pragma
- | AExtended(_,_,{ext_name}) -> t_loop_ext ext_name
+ | AExtended(_,_,{ext_name}) -> Enum.instance p_loop_ext ext_name
end
| IPAllocation _ -> t_allocates
| IPAssigns _ -> t_assigns
@@ -127,7 +128,7 @@ struct
| IPPropertyInstance { ii_ip } -> tag ii_ip
| IPTypeInvariant _ -> t_type_invariant
| IPGlobalInvariant _ -> t_global_invariant
- | IPOther { io_name } -> t_other io_name
+ | IPOther { io_name } -> Enum.instance p_other io_name
let data = Enum.publish kinds ~tag ()
let () = Request.dictionary kinds
@@ -135,6 +136,14 @@ struct
include (val data : S with type t = Property.t)
end
+let register_propkind ~name ~kind ?label ~descr () =
+ let open PropKind in
+ let prefix = match kind with
+ | `Clause -> p_ext
+ | `Loop -> p_loop_ext
+ | `Other -> p_other
+ in ignore @@ Enum.extends kinds prefix ~name ?label ~descr ()
+
(* -------------------------------------------------------------------------- *)
(* --- Property Status --- *)
(* -------------------------------------------------------------------------- *)
@@ -247,4 +256,6 @@ let array =
~add_remove_hook:Property_status.register_property_remove_hook
model
+let reload () = States.reload array
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_properties.mli b/src/plugins/server/kernel_properties.mli
new file mode 100644
index 0000000000000000000000000000000000000000..9e7b4bf1e70f54b10d8de1340029d320cbfcdcdf
--- /dev/null
+++ b/src/plugins/server/kernel_properties.mli
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Documentation of ACSL extensions for [propkind] server data. *)
+val register_propkind :
+ name:string ->
+ kind:[`Clause | `Loop | `Other] ->
+ ?label:Markdown.text ->
+ descr:Markdown.text ->
+ unit -> unit
+
+(** Trigger a full reload for the table of property status. *)
+val reload : unit -> unit
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml
index eb32d1ed5ca668532e6a39459daaff739775fe9f..cb0de2eb1945f2321397535d0c48b6e741d5545c 100644
--- a/src/plugins/server/request.ml
+++ b/src/plugins/server/request.ml
@@ -99,10 +99,9 @@ let signal ~page ~name ~descr ?(details=[]) () =
check_page page name ;
let title = Printf.sprintf "`SIG` %s" name in
let index = [ Printf.sprintf "%s (`SIGNAL`)" name ] in
- let description = [ Block [Text descr] ; Block details] in
- let _ =
- Doc.publish ~page ~name ~title ~index description []
- in Main.signal name
+ let contents = [ Block [Text descr] ; Block details] in
+ let _ = Doc.publish ~page ~name ~title ~index ~contents () in
+ Main.signal name
let emit = Main.emit
let on_signal = Main.on_signal
@@ -343,13 +342,11 @@ let register_sig (type a b) (s : (a,b) signature) (process : rq -> a -> b) =
Syntax.define (plain "Input") (Syntax.text @@ sy_input s.input) in
let output =
Syntax.define (plain "Output") (Syntax.text @@ sy_output s.output) in
- let description =
+ let contents =
Block ( Text s.descr :: input :: output :: s.details ) ::
( doc_input s.input @ doc_output s.output )
in
- let _ =
- Doc.publish ~page:s.page ~name:s.name ~title ~index description []
- in
+ let _ = Doc.publish ~page:s.page ~name:s.name ~title ~index ~contents () in
Main.register s.kind s.name processor ;
s.defined <- true
diff --git a/src/plugins/server/states.ml b/src/plugins/server/states.ml
index 2cbb15085cd3322796a92ea0c8c8708ba8690360..bf7a29ee0de8247afb2de2bf1282dbc66915a1df 100644
--- a/src/plugins/server/states.ml
+++ b/src/plugins/server/states.ml
@@ -50,8 +50,8 @@ let register_value (type a) ~page ~name ~descr ?(details=[])
let open Markdown in
let title = Printf.sprintf "`VALUE` %s" name in
let index = [ Printf.sprintf "%s (`VALUE`)" name ] in
- let description = [ Block [Text descr] ; Block details] in
- let h = Doc.publish ~page ~name ~title ~index description [] in
+ let contents = [ Block [Text descr] ; Block details] in
+ let h = Doc.publish ~page ~name ~title ~index ~contents () in
let signal = Request.signal ~page ~name:(name ^ ".sig")
~descr:(plain "Signal for value " @ href h) () in
Request.register ~page ~kind:`GET ~name:(name ^ ".get")
@@ -70,8 +70,8 @@ let register_state (type a) ~page ~name ~descr ?(details=[])
let open Markdown in
let title = Printf.sprintf "`STATE` %s" name in
let index = [ Printf.sprintf "%s (`STATE`)" name ] in
- let description = [ Block [Text descr] ; Block details] in
- let h = Doc.publish ~page ~name ~title ~index description [] in
+ let contents = [ Block [Text descr] ; Block details] in
+ let h = Doc.publish ~page ~name ~title ~index ~contents () in
let signal = Request.signal ~page ~name:(name ^ ".sig")
~descr:(plain "Signal for state " @ href h) () in
Request.register ~page ~kind:`GET ~name:(name ^ ".get")
@@ -259,7 +259,7 @@ let register_array ~page ~name ~descr ?(details=[]) ~key
let title = Printf.sprintf "`ARRAY` %s" name in
let index = [ Printf.sprintf "%s (`ARRAY`)" name ] in
let columns = !model in
- let description = [
+ let contents = [
Block [Text descr] ;
Syntax.fields ~title:"Columns"
begin
@@ -271,7 +271,7 @@ let register_array ~page ~name ~descr ?(details=[]) ~key
end ;
Block details
] in
- let mref = Doc.publish ~page:page ~name:name ~title ~index description [] in
+ let mref = Doc.publish ~page:page ~name:name ~title ~index ~contents () in
let signal = Request.signal ~page ~name:(name ^ ".sig")
~descr:(plain "Signal for array " @ href mref) () in
let getter = List.map Syntax.(fun (fd,to_js) -> fd.fd_name , to_js) columns in
diff --git a/src/plugins/server/syntax.ml b/src/plugins/server/syntax.ml
index 61f376f45da2ce54d9a51c14046bab5831cbdcce..06abe8c24a54612a466b8d5212054e6b640f9010 100644
--- a/src/plugins/server/syntax.ml
+++ b/src/plugins/server/syntax.ml
@@ -63,7 +63,7 @@ let protect a =
let define left right =
Markdown.(Block_quote [Block[Text ( left @ plain ":=" @ right )]])
-let publish ~page ~name ~descr ~synopsis ?(details = []) () =
+let publish ~page ~name ~descr ~synopsis ?(details = []) ?generated () =
check_name name ;
check_page page name ;
let id = Printf.sprintf "data-%s" name in
@@ -72,11 +72,11 @@ let publish ~page ~name ~descr ~synopsis ?(details = []) () =
let dref = Doc.href page id in
let dlink = Markdown.href ~text:(Markdown.emph name) dref in
let data = Markdown.(plain "<" @ dlink @ plain ">") in
- let content = Markdown.(Block(
+ let contents = Markdown.(Block(
[ Text descr ; define data synopsis.text ]
)) :: details in
- let _href = Doc.publish ~page ~name:id ~title ~index content [] in
- atom dlink
+ let _href = Doc.publish ~page ~name:id ~title ~index ~contents ?generated ()
+ in atom dlink
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/syntax.mli b/src/plugins/server/syntax.mli
index 1e9233d51e3308ecaf82b9c4c63f1c0f077af23a..4f7ef4525cd795e1d947c13279a6c9523c9ce512 100644
--- a/src/plugins/server/syntax.mli
+++ b/src/plugins/server/syntax.mli
@@ -33,7 +33,10 @@ val text : t -> Markdown.text
the description block. *)
val publish :
page:Doc.page -> name:string -> descr:Markdown.text ->
- synopsis:t -> ?details:Markdown.elements -> unit -> t
+ synopsis:t ->
+ ?details:Markdown.elements ->
+ ?generated:(unit -> Markdown.elements) ->
+ unit -> t
val unit : t
val any : t