Skip to content
Snippets Groups Projects
states.ml 11.9 KiB
Newer Older
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2020                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

type 'a callback = ('a -> unit) -> unit

let install signal hook = function
  | None -> ()
  | Some add_hook ->
    let once = ref true in
    let install ok =
      if ok && !once then
        begin
          once := false ;
          add_hook hook ;
        end
    in Request.on_signal signal install

let install_emit signal add_hook =
  install signal (fun () -> Request.emit signal) add_hook

(* -------------------------------------------------------------------------- *)
(* --- Values                                                             --- *)
(* -------------------------------------------------------------------------- *)

Loïc Correnson's avatar
Loïc Correnson committed
let register_value (type a) ~package ~name ~descr
    ~(output : a Request.output) ~get
    ?(add_hook : unit callback option) ()
  =
  let open Markdown in
Loïc Correnson's avatar
Loïc Correnson committed
  let href = link ~name () in
  let module D = (val output) in
  let id = Package.declare_id
      ~package ~name ~descr (D_value D.jtype) in
Loïc Correnson's avatar
Loïc Correnson committed
  let signal = Request.signal
      ~package ~name:(Package.Derived.signal id).name
Loïc Correnson's avatar
Loïc Correnson committed
      ~descr:(plain "Signal for state" @ href) in
  let () = Request.register
      ~package ~name:(Package.Derived.getter id).name
Loïc Correnson's avatar
Loïc Correnson committed
      ~descr:(plain "Getter for state" @ href)
      ~kind:`GET ~input:(module Junit) ~output get in
  install_emit signal add_hook ;
(* -------------------------------------------------------------------------- *)
(* --- States                                                             --- *)
(* -------------------------------------------------------------------------- *)

Loïc Correnson's avatar
Loïc Correnson committed
let register_state (type a) ~package ~name ~descr
    ~(data : a data) ~get ~set
    ?(add_hook : unit callback option) () =
  let open Markdown in
Loïc Correnson's avatar
Loïc Correnson committed
  let module D = (val data) in
  let href = link ~name () in
  let id = Package.declare_id
      ~package ~name ~descr (D_state D.jtype) in
Loïc Correnson's avatar
Loïc Correnson committed
  let signal = Request.signal
      ~package ~name:(Package.Derived.signal id).name
Loïc Correnson's avatar
Loïc Correnson committed
      ~descr:(plain "Signal for state" @ href) in
  let () = Request.register
      ~package ~name:(Package.Derived.getter id).name
Loïc Correnson's avatar
Loïc Correnson committed
      ~descr:(plain "Getter for state" @ href)
      ~kind:`GET ~input:(module Junit) ~output:(module D) get in
  let () = Request.register
      ~package ~name:(Package.Derived.setter id).name
Loïc Correnson's avatar
Loïc Correnson committed
      ~descr:(plain "Setter for state" @ href)
      ~kind:`SET ~input:(module D) ~output:(module Junit) set in
  install_emit signal add_hook ;
  signal

(* -------------------------------------------------------------------------- *)
(* --- Model Signature                                                    --- *)
(* -------------------------------------------------------------------------- *)

Loïc Correnson's avatar
Loïc Correnson committed
type 'a column = Package.fieldInfo * ('a -> json)
type 'a model = 'a column list ref
let model () = ref []
Loïc Correnson's avatar
Loïc Correnson committed
let column (type a b) ~name ~descr
    ~(data: b Request.output) ~(get : a -> b) (model : a model) =
  let module D = (val data) in
  if name = "key" || name = "index" then
    raise (Invalid_argument "Server.States.column: invalid name") ;
Loïc Correnson's avatar
Loïc Correnson committed
  if List.exists (fun (fd,_) -> fd.Package.fd_name = name) !model then
    raise (Invalid_argument "Server.States.column: duplicate name") ;
Loïc Correnson's avatar
Loïc Correnson committed
  let fd = Package.{
      fd_name = name ;
Loïc Correnson's avatar
Loïc Correnson committed
      fd_type = D.jtype ;
      fd_descr = descr ;
    } in
  model := (fd , fun a -> D.to_json (get a)) :: !model

module Kmap = Map.Make(String)

(* -------------------------------------------------------------------------- *)
(* --- Model Content                                                      --- *)
(* -------------------------------------------------------------------------- *)

type 'a update = Remove | Add of 'a
type 'a content = {
  mutable cleared : bool ;
  mutable updates : 'a update Kmap.t ;
}

type 'a array = {
  signal : Request.signal ;
Loïc Correnson's avatar
Loïc Correnson committed
  fkey : string ;
  key : 'a -> string ;
  iter : ('a -> unit) -> unit ;
  getter : (string * ('a -> json)) list ;
  (* [LC+JS]
     The two following fields allow to keep an array in sync
     with the current project and still have a polymorphic data type. *)
  mutable current : 'a content option ; (* fast access to current project *)
  projects : (string , 'a content) Hashtbl.t ; (* indexed by project *)
}

let synchronize array =
  begin
    Project.register_after_set_current_hook
      ~user_only:false (fun _ -> array.current <- None) ;
      Hashtbl.remove array.projects (Project.get_unique_name p) in
    Project.register_before_remove_hook cleanup ;
    Project.register_todo_before_clear cleanup ;
    Request.on_signal array.signal
      (fun _ ->
         array.current <- None ;
         Hashtbl.clear array.projects ;
let content array =
  match array.current with
  | Some w -> w
  | None ->
    let prj = Project.(current () |> get_unique_name) in
    let content =
      try Hashtbl.find array.projects prj
      with Not_found ->
        let w = {
          cleared = true ;
          updates = Kmap.empty ;
        } in
        Hashtbl.add array.projects prj w ; w
    in
    array.current <- Some content ;
    Request.emit array.signal ;
    content
let reload array =
  let m = content array in
  m.cleared <- true ;
  m.updates <- Kmap.empty ;
  Request.emit array.signal
let update array k =
  let m = content array in
  if not m.cleared then
    begin
      m.updates <- Kmap.add (array.key k) (Add k) m.updates ;
      Request.emit array.signal ;
let remove array k =
  let m = content array in
  if not m.cleared then
    begin
      m.updates <- Kmap.add (array.key k) Remove m.updates ;
      Request.emit array.signal ;
let signal array = array.signal

(* -------------------------------------------------------------------------- *)
(* --- Fetch Model Updates                                                --- *)
(* -------------------------------------------------------------------------- *)

type buffer = {
  reload : bool ;
  mutable capacity : int ;
  mutable pending : int ;
  mutable removed : string list ;
  mutable updated : json list ;
}

Loïc Correnson's avatar
Loïc Correnson committed
let add_entry buffer cols fkey key v =
  let fjs = List.fold_left (fun fjs (fd,to_json) ->
      try (fd , to_json v) :: fjs
      with Not_found -> fjs
    ) [] cols in
Loïc Correnson's avatar
Loïc Correnson committed
  let row = (fkey, `String key) :: fjs in
  buffer.updated <- `Assoc row :: buffer.updated ;
  buffer.capacity <- pred buffer.capacity

let remove_entry buffer key =
  buffer.removed <- key :: buffer.removed ;
  buffer.capacity <- pred buffer.capacity

Loïc Correnson's avatar
Loïc Correnson committed
let update_entry buffer cols fkey key = function
  | Remove -> remove_entry buffer key
Loïc Correnson's avatar
Loïc Correnson committed
  | Add v -> add_entry buffer cols fkey key v
let fetch array n =
  let m = content array in
  let reload = m.cleared in
  let buffer = {
    reload ;
    capacity = n ;
    pending = 0 ;
    removed = [] ;
    updated = [] ;
  } in
  begin
    if reload then
      begin
        m.cleared <- false ;
        array.iter
            let key = array.key v in
            if buffer.capacity > 0 then
Loïc Correnson's avatar
Loïc Correnson committed
              add_entry buffer array.getter array.fkey key v
            else
              ( m.updates <- Kmap.add key (Add v) m.updates ;
                buffer.pending <- succ buffer.pending ) ;
          end ;
      end
    else
      m.updates <- Kmap.filter
          begin fun key upd ->
            if buffer.capacity > 0 then
Loïc Correnson's avatar
Loïc Correnson committed
              ( update_entry buffer array.getter array.fkey key upd ; false )
            else
              ( buffer.pending <- succ buffer.pending ; true )
          end m.updates ;
  end ;
  buffer

(* -------------------------------------------------------------------------- *)
(* --- Signature Registry                                                 --- *)
(* -------------------------------------------------------------------------- *)

Loïc Correnson's avatar
Loïc Correnson committed
let register_array ~package ~name ~descr ~key
    ?(keyName="key")
    ?(keyKind=name)
    ~(iter : 'a callback)
    ?(add_update_hook : 'a callback option)
    ?(add_remove_hook : 'a callback option)
    ?(add_reload_hook : unit callback option)
    model =
  let open Markdown in
Loïc Correnson's avatar
Loïc Correnson committed
  let href = link ~name () in
  let columns = List.rev !model in
  let fields = Package.{
      fd_name = "key" ;
      fd_type = Jkey keyKind ;
Loïc Correnson's avatar
Loïc Correnson committed
      fd_descr = plain "Entry identifier." ;
    } :: List.map fst columns in
  let id = Package.declare_id ~package:package ~name:name ~descr
Loïc Correnson's avatar
Loïc Correnson committed
      (D_array { arr_key = keyName ; arr_kind = keyKind }) in
Loïc Correnson's avatar
Loïc Correnson committed
  let signal = Request.signal
      ~package ~name:(Package.Derived.signal id).name
Loïc Correnson's avatar
Loïc Correnson committed
      ~descr:(plain "Signal for array" @ href) in
  let row = Package.declare_id
      ~package ~name:(Package.Derived.data id).name
      ~descr:(plain "Data for array rows" @ href)
Loïc Correnson's avatar
Loïc Correnson committed
      (D_record fields) in
  let fs = List.map Package.field fields in
  Data.derived ~package ~id:row (Jrecord fs) ;
Loïc Correnson's avatar
Loïc Correnson committed
  let getter =
    List.map Package.(fun (fd,to_js) -> fd.fd_name , to_js) !model in
  let array = {
Loïc Correnson's avatar
Loïc Correnson committed
    fkey = keyName ; key ; iter ; getter ; signal ;
    current = None ; projects = Hashtbl.create 0
  } in
Loïc Correnson's avatar
Loïc Correnson committed
  let signature = Request.signature ~input:(module Jint) () in
Loïc Correnson's avatar
Loïc Correnson committed
  let module Jkeys = Jlist(struct
Loïc Correnson's avatar
Loïc Correnson committed
      include Jstring
      let jtype = Package.Jkey name
    end) in
Loïc Correnson's avatar
Loïc Correnson committed
  let module Jrows = Jlist (struct
Loïc Correnson's avatar
Loïc Correnson committed
      include Jany
      let jtype = Package.Jdata row
    end) in
  let set_reload = Request.result signature
      ~name:"reload" ~descr:(plain "array fully reloaded")
      (module Jbool) in
  let set_removed = Request.result signature
      ~name:"removed" ~descr:(plain "removed entries")
Loïc Correnson's avatar
Loïc Correnson committed
      (module Jkeys) in
  let set_updated = Request.result signature
      ~name:"updated" ~descr:(plain "updated entries")
Loïc Correnson's avatar
Loïc Correnson committed
      (module Jrows) in
  let set_pending = Request.result signature
      ~name:"pending" ~descr:(plain "remaining entries to be fetched")
      (module Jint) in
Loïc Correnson's avatar
Loïc Correnson committed
  Request.register_sig
    ~package ~name:(Package.Derived.fetch id).name
Loïc Correnson's avatar
Loïc Correnson committed
    ~descr:(plain "Data fetcher for array" @ href)
    ~kind:`GET signature
      let buffer = fetch array n in
      set_reload rq buffer.reload ;
      set_removed rq buffer.removed ;
      set_updated rq buffer.updated ;
      set_pending rq buffer.pending ;
    end ;
Loïc Correnson's avatar
Loïc Correnson committed
  Request.register
    ~package ~name:(Package.Derived.reload id).name
Loïc Correnson's avatar
Loïc Correnson committed
    ~descr:(plain "Force full reload for array" @ href)
    ~kind:`GET ~input:(module Junit) ~output:(module Junit)
    (fun () -> reload array) ;
  synchronize array ;
  install signal (update array) add_update_hook ;
  install signal (remove array) add_remove_hook ;
  install signal (fun () -> reload array) add_reload_hook ;
  array

(* -------------------------------------------------------------------------- *)