diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml index 44d1d3bbc2a966c5f39df96dc4faa6be21bea6c6..f600d853cb9f181fada64428153e236c825bb71f 100644 --- a/src/plugins/server/data.ml +++ b/src/plugins/server/data.ml @@ -63,6 +63,8 @@ let failure ?json msg = let failure_from_type_error msg json = failure ~json "%s" msg +let page = Doc.page `Kernel ~title:"Kernel Types" ~filename:"data.md" + (* -------------------------------------------------------------------------- *) (* --- Option --- *) (* -------------------------------------------------------------------------- *) @@ -347,19 +349,59 @@ struct end +module Jmarkdown : S with type t = Markdown.text = +struct + + type t = Markdown.text + let syntax = Syntax.publish ~page + ~name:"markdown" ~descr:(Markdown.plain "Markdown (inlined text)") + ~synopsis:Syntax.string () + let of_json js = Markdown.plain (Ju.to_string js) + let to_json txt = + `String (Pretty_utils.to_string (Markdown.pp_text ?page:None) txt) + +end + (* -------------------------------------------------------------------------- *) (* --- Enums --- *) (* -------------------------------------------------------------------------- *) +module Tag = Collection + (struct + type t = Syntax.tag + + let syntax = Syntax.publish ~page ~name:"tag" + ~descr:(Markdown.plain "Tag description") + ~synopsis:(Syntax.record [ + "name",Syntax.string ; + "label",Jmarkdown.syntax ; + "descr",Jmarkdown.syntax ; + ]) () + + let to_json tg = `Assoc [ + "name", `String tg.Syntax.tag_name ; + "label", Jmarkdown.to_json tg.tag_label ; + "descr" , Jmarkdown.to_json tg.tag_descr ; + ] + + let of_json js = Syntax.{ + tag_name = Ju.member "name" js |> Ju.to_string ; + tag_label = Ju.member "label" js |> Jmarkdown.of_json ; + tag_descr = Ju.member "descr" js |> Jmarkdown.of_json ; + } + end) + module Enum = struct type 'a dictionary = { page : Doc.page ; name : string ; + title : string ; descr : Markdown.text ; values : (string,'a option) Hashtbl.t ; vindex : ('a,string) Hashtbl.t ; + mutable syntax : Markdown.text ; mutable published : bool ; mutable tags : Syntax.tag list ; } @@ -367,13 +409,17 @@ struct type 'a tag = string type 'a prefix = string -> 'a tag - let name tg = tg + let tag_name tg = tg + let tag_label a = function + | None -> Markdown.plain (String.(capitalize_ascii (lowercase_ascii a))) + | Some lbl -> lbl - let dictionary ~page ~name ~descr () = { - page ; name ; descr ; + let dictionary ~page ~name ~title ~descr () = { + page ; name ; descr ; title ; published = false ; values = Hashtbl.create 0 ; vindex = Hashtbl.create 0 ; + syntax = [] ; tags = [] ; } @@ -381,12 +427,20 @@ struct let msg = Printf.sprintf "Server.Data.Enum.%s: %s" name reason in raise (Invalid_argument msg) - let tag (d : 'a dictionary) ~name ~descr ?value () : 'a tag = + let page (d : 'a dictionary) = d.page + let name (d : 'a dictionary) = d.name + 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.{ tag_name = name ; tag_descr = descr } in + let tg = Syntax.{ + tag_name = name ; + tag_label = tag_label name label ; + tag_descr = descr ; + } in d.tags <- tg :: d.tags ; Hashtbl.add d.values name value ; begin match value with @@ -394,13 +448,14 @@ struct | Some v -> Hashtbl.add d.vindex v name end ; name - let prefix (d : 'a dictionary) ~prefix ?(var="*") ~descr + 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 tg = Syntax.{ tag_name = make var ; + tag_label = tag_label (prefix ^ ".") label ; tag_descr = descr ; } in d.tags <- tg :: d.tags ; make @@ -419,6 +474,8 @@ struct | exception Not_found -> failure "[%s] Not registered tag '%s" name tag + let tags d = List.rev d.tags + let publish (type a) (d : a dictionary) ?tag () = if d.published then invalid d.name "already published" ; @@ -427,7 +484,7 @@ struct type t = a let descr = d.descr let syntax = - let tags = Syntax.tags ~title:"Tag" (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] () @@ -439,6 +496,7 @@ struct end in begin d.published <- true ; + d.syntax <- Syntax.text M.syntax ; (module M : S with type t = a) end diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli index 6950b98de51e5b1ba95e79d5fded2c51e9b4de5a..3297d75cbdae383ca6d3d1ac59698bdba41786ed 100644 --- a/src/plugins/server/data.mli +++ b/src/plugins/server/data.mli @@ -26,6 +26,7 @@ type json = Json.t +val page : Doc.page (** Page for builtin kernel data types *) val pretty : Format.formatter -> json -> unit module type S = @@ -89,6 +90,7 @@ module Jfloat : S_collection with type t = float module Jstring : S_collection with type t = string module Jident : S_collection with type t = string (** Syntax is {i ident}. *) module Jtext : S with type t = json (** Rich text encoding, see [Jbuffer] *) +module Jmarkdown : S with type t = Markdown.text (* -------------------------------------------------------------------------- *) (** {2 Records} *) @@ -158,6 +160,8 @@ end (** {2 Enums} *) (* -------------------------------------------------------------------------- *) +module Tag : S_collection with type t = Syntax.tag + (** Enum factory. You shall start by declaring a dictionnary with @@ -185,29 +189,42 @@ sig type 'a tag type 'a prefix = string -> 'a tag - val name : 'a tag -> string + val tag_name : 'a tag -> string (** Creates an opened, empty dictionnary. *) val dictionary : - page:Doc.page -> name:string -> descr:Markdown.text -> + page:Doc.page -> name:string -> title:string -> descr:Markdown.text -> unit -> 'a dictionary (** Register a new tag in the dictionnary. + The default label is the capitalized name. 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. *) val tag : 'a dictionary -> - name:string -> descr:Markdown.text -> ?value:'a -> + name:string -> + ?label:Markdown.text -> descr:Markdown.text -> + ?value:'a -> unit -> 'a tag (** Register a new prefix tag in the dictionnary. + The default label is the capitalized prefix. 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. *) val prefix : 'a dictionary -> - prefix:string -> ?var:string -> descr:Markdown.text -> unit -> 'a prefix + prefix:string -> ?var:string -> + ?label:Markdown.text -> descr:Markdown.text -> + unit -> 'a prefix + + (** Obtain all the tags from the dictionnary. *) + val tags : 'a dictionary -> Tag.t list + + val page : 'a dictionary -> Doc.page + val name : 'a dictionary -> string + val syntax : 'a dictionary -> Markdown.text (** Publish the dictionnary. To more tag nor prefix can be added after. If no [~tag] function is provided, registered values with tags diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index 3861b8cfc8e6eaaf5d9af641278beac026c911d7..2c68bdbac366a7352553419ba32431a04d4c576b 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -102,7 +102,7 @@ module PP = Printer_tag.Make(Tag) module Stmt = Data.Collection (struct type t = stmt - let syntax = Sy.publish ~page ~name:"stmt" + let syntax = Sy.publish ~page:Data.page ~name:"stmt" ~synopsis:Sy.ident ~descr:(Md.plain "Code statement identifier") () let to_json st = `String (Tag.of_stmt st) @@ -132,7 +132,7 @@ module Ki = Data.Collection module Kf = Data.Collection (struct type t = kernel_function - let syntax = Sy.publish ~page ~name:"fct-id" + let syntax = Sy.publish ~page:Data.page ~name:"fct-id" ~synopsis:Sy.ident ~descr:(Md.plain "Function identified by its global name.") () let to_json kf = diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml index 28e9a6574f00e5ab5f7a0fe3b397663b3fe0a0f9..67ec006f68be6abff406e2b5ca6ed9700e9a7d06 100644 --- a/src/plugins/server/kernel_main.ml +++ b/src/plugins/server/kernel_main.ml @@ -78,118 +78,114 @@ let () = (* --- File Positions --- *) (* -------------------------------------------------------------------------- *) -module RawSource = -struct - type t = Filepath.position - - let syntax = Sy.publish ~page ~name:"source" - ~synopsis:(Sy.record [ "file" , Sy.string ; "line" , Sy.int ]) - ~descr:(Md.plain "Source file positions.") - ~details:Md.([Block [Text (plain "The file path is normalized, \ - and the line number starts at one.")]]) - () +module LogSource = Collection + (struct + type t = Filepath.position - let to_json p = `Assoc [ - "file" , `String (p.Filepath.pos_path :> string) ; - "line" , `Int p.Filepath.pos_lnum ; - ] + let syntax = Sy.publish ~page:Data.page ~name:"source" + ~synopsis:(Sy.record [ "file" , Sy.string ; "line" , Sy.int ]) + ~descr:(Md.plain "Source file positions.") + ~details:Md.([Block [Text (plain "The file path is normalized, \ + and the line number starts at one.")]]) + () - let of_json = function - | `Assoc [ "file" , `String path ; "line" , `Int line ] - | `Assoc [ "line" , `Int line ; "file" , `String path ] - -> Log.source ~file:(Filepath.Normalized.of_string path) ~line - | js -> failure_from_type_error "Invalid source format" js + let to_json p = `Assoc [ + "file" , `String (p.Filepath.pos_path :> string) ; + "line" , `Int p.Filepath.pos_lnum ; + ] -end + let of_json = function + | `Assoc [ "file" , `String path ; "line" , `Int line ] + | `Assoc [ "line" , `Int line ; "file" , `String path ] + -> Log.source ~file:(Filepath.Normalized.of_string path) ~line + | js -> failure_from_type_error "Invalid source format" js -module LogSource = Collection(RawSource) + end) (* -------------------------------------------------------------------------- *) (* --- Log Lind --- *) (* -------------------------------------------------------------------------- *) -module RawKind = -struct - let kinds = Enum.dictionary ~page - ~name:"kind" - ~descr:(Md.plain "Frama-C message category.") - () +module LogKind = Collection + (struct - let t_kind value name descr = - Enum.tag kinds ~name ~descr:(Md.plain descr) ~value () + let kinds = Enum.dictionary ~page + ~name:"logkind" ~title:"Log Kind" + ~descr:(Md.plain "Frama-C message category.") + () - let t_error = t_kind Log.Error "ERROR" "User Error" - let t_warning = t_kind Log.Warning "WARNING" "User Warning" - let t_feedback = t_kind Log.Feedback "FEEDBACK" "Plugin Feedback" - let t_result = t_kind Log.Result "RESULT" "Plugin Result" - let t_failure = t_kind Log.Failure "FAILURE" "Plugin Failure" - let t_debug = t_kind Log.Debug "DEBUG" "Analyser Debug" + let t_kind value name descr = + Enum.tag kinds ~name ~descr:(Md.plain descr) ~value () - let tag = function - | Log.Error -> t_error - | Log.Warning -> t_warning - | Log.Feedback -> t_feedback - | Log.Result -> t_result - | Log.Failure -> t_failure - | Log.Debug -> t_debug + let t_error = t_kind Log.Error "ERROR" "User Error" + let t_warning = t_kind Log.Warning "WARNING" "User Warning" + let t_feedback = t_kind Log.Feedback "FEEDBACK" "Plugin Feedback" + let t_result = t_kind Log.Result "RESULT" "Plugin Result" + let t_failure = t_kind Log.Failure "FAILURE" "Plugin Failure" + let t_debug = t_kind Log.Debug "DEBUG" "Analyser Debug" - let data = Enum.publish kinds ~tag () + let tag = function + | Log.Error -> t_error + | Log.Warning -> t_warning + | Log.Feedback -> t_feedback + | Log.Result -> t_result + | Log.Failure -> t_failure + | Log.Debug -> t_debug - include (val data : S with type t = Log.kind) -end + let data = Enum.publish kinds ~tag () + let () = Request.dictionary kinds -module LogKind = Collection(RawKind) + include (val data : S with type t = Log.kind) + end) (* -------------------------------------------------------------------------- *) (* --- Log Events --- *) (* -------------------------------------------------------------------------- *) -module RawEvent = -struct - - type rlog - - let jlog : rlog Record.signature = Record.signature ~page - ~name:"log" ~descr:(Md.plain "Message event record.") () - - let kind = Record.field jlog ~name:"kind" - ~descr:(Md.plain "Message kind") (module LogKind) - let plugin = Record.field jlog ~name:"plugin" - ~descr:(Md.plain "Emitter plugin") (module Jstring) - let message = Record.field jlog ~name:"message" - ~descr:(Md.plain "Message text") (module Jstring) - let category = Record.option jlog ~name:"category" - ~descr:(Md.plain "Message category (DEBUG or WARNING)") (module Jstring) - let source = Record.option jlog ~name:"source" - ~descr:(Md.plain "Source file position") (module LogSource) - - module R = (val (Record.publish jlog) : Record.S with type r = rlog) - - type t = Log.event - let syntax = R.syntax - - let to_json evt = - R.default |> - R.set plugin evt.Log.evt_plugin |> - R.set kind evt.Log.evt_kind |> - R.set category evt.Log.evt_category |> - R.set source evt.Log.evt_source |> - R.set message evt.Log.evt_message |> - R.to_json - - let of_json js = - let r = R.of_json js in - { - Log.evt_plugin = R.get plugin r ; - Log.evt_kind = R.get kind r ; - Log.evt_category = R.get category r ; - Log.evt_source = R.get source r ; - Log.evt_message = R.get message r ; - } - -end - -module LogEvent = Collection(RawEvent) +module LogEvent = Collection + (struct + + type rlog + + let jlog : rlog Record.signature = Record.signature ~page + ~name:"log" ~descr:(Md.plain "Message event record.") () + + let kind = Record.field jlog ~name:"kind" + ~descr:(Md.plain "Message kind") (module LogKind) + let plugin = Record.field jlog ~name:"plugin" + ~descr:(Md.plain "Emitter plugin") (module Jstring) + let message = Record.field jlog ~name:"message" + ~descr:(Md.plain "Message text") (module Jstring) + let category = Record.option jlog ~name:"category" + ~descr:(Md.plain "Message category (DEBUG or WARNING)") (module Jstring) + let source = Record.option jlog ~name:"source" + ~descr:(Md.plain "Source file position") (module LogSource) + + module R = (val (Record.publish jlog) : Record.S with type r = rlog) + + type t = Log.event + let syntax = R.syntax + + let to_json evt = + R.default |> + R.set plugin evt.Log.evt_plugin |> + R.set kind evt.Log.evt_kind |> + R.set category evt.Log.evt_category |> + R.set source evt.Log.evt_source |> + R.set message evt.Log.evt_message |> + R.to_json + + let of_json js = + let r = R.of_json js in + { + Log.evt_plugin = R.get plugin r ; + Log.evt_kind = R.get kind r ; + Log.evt_category = R.get category r ; + Log.evt_source = R.get source r ; + Log.evt_message = R.get message r ; + } + + end) (* -------------------------------------------------------------------------- *) (* --- Log Monitoring --- *) diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml index fe71601a6558c596398a343ef5fc2128c5951921..46e46b0f2507139bee3c1cd647de33d9436991b1 100644 --- a/src/plugins/server/kernel_properties.ml +++ b/src/plugins/server/kernel_properties.ml @@ -37,7 +37,7 @@ let page = Doc.page `Kernel ~title:"Property Services" ~filename:"properties.md" module PropKind = struct let kinds = Enum.dictionary ~page - ~name:"propkind" + ~name:"propkind" ~title:"Kind" ~descr:(Md.plain "Property Kind") () @@ -129,8 +129,8 @@ struct | IPGlobalInvariant _ -> t_global_invariant | IPOther { io_name } -> t_other io_name - let data = Enum.publish kinds ~tag () + let () = Request.dictionary kinds include (val data : S with type t = Property.t) end @@ -142,36 +142,46 @@ end module PropStatus = struct - let status = Enum.dictionary ~page ~name:"status" + let status = Enum.dictionary ~page + ~name:"propstatus" ~title:"Status" ~descr:(Md.plain "Property Status (consolidated)") () - let t_status value name descr = - Enum.tag status ~name ~descr:(Md.plain descr) ~value () + let t_status value name ?label descr = + Enum.tag status ~name + ?label:(Extlib.opt_map Md.plain label) + ~descr:(Md.plain descr) ~value () open Property_status.Feedback let t_unknown = t_status Unknown "unknown" "Unknown status" let t_never_tried = - t_status Never_tried "never-tried" "Unknown status (never tried)" + t_status Never_tried "never_tried" + ~label:"Never tried" "Unknown status (never tried)" let t_inconsistent = t_status Inconsistent "inconsistent" "Inconsistent status" let t_valid = t_status Valid "valid" "Valid property" let t_valid_under_hyp = - t_status Valid_under_hyp "valid_under_hyp" "Valid (under hypotheses)" + t_status Valid_under_hyp "valid_under_hyp" + ~label:"Valid(?)" "Valid (under hypotheses)" let t_considered_valid = - t_status Considered_valid "considered_valid" "Valid (external assumption)" + t_status Considered_valid "considered_valid" + ~label:"Valid(!)" "Valid (external assumption)" let t_invalid = t_status Invalid "invalid" "Invalid property (counter example found)" let t_invalid_under_hyp = - t_status Invalid_under_hyp "invalid_under_hyp" "Invalid property (under hypotheses)" + t_status Invalid_under_hyp "invalid_under_hyp" + ~label:"Invalid(?)" "Invalid property (under hypotheses)" let t_invalid_but_dead = - t_status Invalid_but_dead "invalid_but_dead" "Dead property (but invalid)" + t_status Invalid_but_dead "invalid_but_dead" + ~label:"Invalid(âœ)" "Dead property (but invalid)" let t_valid_but_dead = - t_status Valid_but_dead "valid_but_dead" "Dead property (but valid)" + t_status Valid_but_dead "valid_but_dead" + ~label:"Valid(âœ)" "Dead property (but valid)" let t_unknown_but_dead = - t_status Unknown_but_dead "unknown_but_dead" "Dead property (but unknown)" + t_status Unknown_but_dead "unknown_but_dead" + ~label:"Unknown(âœ)" "Dead property (but unknown)" let tag = function | Valid -> t_valid @@ -187,6 +197,7 @@ struct | Inconsistent -> t_inconsistent let data = Enum.publish status ~tag () + let () = Request.dictionary status include (val data : S with type t = Property_status.Feedback.t) end diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml index ebd45441bbcf1162779895d7a78c6c4d0f17f730..51c2eb26c9068a0acc0e4260f297f1d380e2a8ad 100644 --- a/src/plugins/server/request.ml +++ b/src/plugins/server/request.ml @@ -81,6 +81,12 @@ let check_page page name = Senv.warning ~wkey:wkind "Request '%s' shall not be published in protocol pages" name +let page_prefix page = + match Doc.chapter page with + | `Kernel -> "kernel" + | `Plugin plugin -> plugin + | `Protocol -> "protocol" + (* -------------------------------------------------------------------------- *) (* --- Signals --- *) (* -------------------------------------------------------------------------- *) @@ -359,4 +365,15 @@ let register ~page ~kind ~name ~descr ?details ~input ~output process = (signature ~page ~kind ~name ~descr ?details ~input ~output ()) (fun _rq v -> process v) +let dictionary (d : 'a Data.Enum.dictionary) = + let name = Data.Enum.name d in + let page = Data.Enum.page d in + let descr = Markdown.plain "Returns all tags registered for" @ + Data.Enum.syntax d in + register ~kind:`GET ~page + ~name:(Printf.sprintf "%s.dictionary.%s" (page_prefix page) name) ~descr + ~input:(module Data.Junit) + ~output:(module Data.Tag.Jlist) + (fun () -> Data.Enum.tags d) + (* -------------------------------------------------------------------------- *) diff --git a/src/plugins/server/request.mli b/src/plugins/server/request.mli index 14e1a565476e15fe020f6c87b3f86463d10d8576..dbe3f5e133ce227aa860a2c1ae2a63db80415b4a 100644 --- a/src/plugins/server/request.mli +++ b/src/plugins/server/request.mli @@ -211,4 +211,10 @@ val result_opt : ('a,unit) signature -> descr:Markdown.text -> 'b output -> 'b option result +(** {2 Exporting Dictionaries} *) + +(** Register a [GET] request [dictionary.<name>] to retrieve all tags + registered in the dictionary. *) +val dictionary : 'a Data.Enum.dictionary -> unit + (* -------------------------------------------------------------------------- *) diff --git a/src/plugins/server/syntax.ml b/src/plugins/server/syntax.ml index 7c7a4778f4bf1856bea937d50518c67170340f74..79ccfcbde3a2b9b43440f146e2af480c1bbd895a 100644 --- a/src/plugins/server/syntax.ml +++ b/src/plugins/server/syntax.ml @@ -107,6 +107,7 @@ let option t = atom @@ Markdown.(protect t @ code "?") type tag = { tag_name : string ; + tag_label : Markdown.text ; tag_descr : Markdown.text ; } @@ -114,9 +115,10 @@ let tags ?(title="Tag") (tgs : tag list) = let open Markdown in let header = [ plain title, Left; + plain "Value", Left; plain "Description", Left ] in - let row tg = [ escaped tg.tag_name ; tg.tag_descr ] in + let row tg = [ tg.tag_label ; escaped tg.tag_name ; tg.tag_descr ] in Markdown.Table { caption = None ; header ; content = List.map row tgs ; } diff --git a/src/plugins/server/syntax.mli b/src/plugins/server/syntax.mli index b5f0367df2d3d7a4bf9ae402319a8a56f5700803..c9ac038bfc8c3a68e8d99a2c7b2560b1d3229020 100644 --- a/src/plugins/server/syntax.mli +++ b/src/plugins/server/syntax.mli @@ -51,7 +51,11 @@ val option : t -> t val record : (string * t) list -> t val data : string -> Markdown.href -> t -type tag = { tag_name : string ; tag_descr : Markdown.text } +type tag = { + tag_name : string ; + tag_label : Markdown.text ; + tag_descr : Markdown.text ; +} (** Builds a table with tags description. The [~title] is applied to the tag name column