[server] allows dictionary extensions

 - possibly delayed generation of documentation
 - prefix extension
 - API extension

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" \

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

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

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

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

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
+
 (* -------------------------------------------------------------------------- *)

src/plugins/server/kernel_properties.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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
+
+(* -------------------------------------------------------------------------- *)

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
 

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

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
 
 (* -------------------------------------------------------------------------- *)
 

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