[ivette] typescript API

ivette/.gitignore

@@ -4,6 +4,7 @@
 
 .dome-*.stamp
 .dome-*.back
+.server-tsc
 node_modules
 yarn.lock
 yarn-error.log

ivette/Makefile

@@ -30,6 +30,22 @@ fixlint: dome-pkg dome-templ
 
 tsc: typecheck fixlint
 
+# --------------------------------------------------------------------------
+# --- Frama-C API
+# --------------------------------------------------------------------------
+
+.PHONY: api
+
+api: .server-tsc
+
+.server-tsc: ../bin/toplevel.byte api/server_tsc.ml
+	@echo "[Ivette] Generating TypeScript API"
+	../bin/frama-c.byte -load-module api/server_tsc.ml -server-tsc
+	@touch $@
+
+../bin/toplevel.byte:
+	make -C .. -kj byte
+
 # --------------------------------------------------------------------------
 # --- Ivette Documentation
 # --------------------------------------------------------------------------

ivette/api/server_tsc.ml

+(* -------------------------------------------------------------------------- *)
+(* --- Frama-C TypeScript API Generator                                   --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Self = Plugin.Register
+  (struct
+    let name = "Server TypeScript API"
+    let shortname = "server-tsc"
+    let help = "Generate TypeScript API for Server"
+  end)
+
+module TSC = Self.Action
+    (struct
+      let option_name = "-server-tsc"
+      let help = "Generate TypeScript API"
+    end)
+
+module OUT = Self.String
+    (struct
+      let option_name = "-server-tsc-out"
+      let arg_name = "dir"
+      let default = "api"
+      let help = "Output directory (default is './api')"
+    end)
+
+module Md = Markdown
+module Pkg = Server.Package
+
+(* -------------------------------------------------------------------------- *)
+(* --- TS Utils                                                           --- *)
+(* -------------------------------------------------------------------------- *)
+
+let keywords = [
+  "break"; "case"; "catch"; "class"; "const"; "continue"; "debugger";
+  "default"; "delete"; "do"; "else"; "enum"; "export"; "extends"; "false";
+  "finally"; "for"; "function"; "if"; "import"; "in"; "instanceof"; "new";
+  "null"; "return"; "super"; "switch"; "this"; "throw"; "true"; "try";
+  "typeof"; "var"; "void"; "while"; "with"; "as"; "implements"; "interface";
+  "let"; "package"; "private"; "protected"; "public"; "static"; "yield"; "any";
+  "boolean"; "constructor"; "declare"; "get"; "module"; "require"; "number";
+  "set"; "string"; "symbol"; "type"; "from"; "of";
+  "Json";
+]
+
+let pp_descr = Md.pp_text ?page:None
+
+(* -------------------------------------------------------------------------- *)
+(* --- Main Generator                                                     --- *)
+(* -------------------------------------------------------------------------- *)
+
+let makePackage pkg name fmt =
+  begin
+    let open Pkg in
+    Format.fprintf fmt "/* --- Generated Frama-C Server API --- */@\n" ;
+    Format.fprintf fmt "/**@\n%a@\n" pp_descr pkg.p_descr ;
+    Format.fprintf fmt "  @@packageDocumentation@\n" ;
+    Format.fprintf fmt "  @@module frama-c/%s@\n" name ;
+    Format.fprintf fmt "*/@\n" ;
+    let names = Pkg.resolve ~keywords pkg in
+    Format.fprintf fmt "import * as Json from 'dome/data/json'@\n" ;
+    Pkg.IdMap.iter
+      (fun id name ->
+         let pkg = Pkg.name_of_pkg ~sep:"/" id.plugin id.package in
+         if id.name = name then
+           Format.fprintf fmt "import { %s } from '%s';@\n"
+             name pkg
+         else
+           Format.fprintf fmt "import { %s: %s } from '%s';@\n"
+             id.name name pkg
+      ) names ;
+    List.iter
+      (fun d ->
+         Format.fprintf fmt "// Declare '%a'@\n" Pkg.pp_ident d.d_ident
+      ) pkg.p_content
+  end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Main Generator                                                     --- *)
+(* -------------------------------------------------------------------------- *)
+
+let generate () =
+  begin
+    Pkg.iter
+      begin fun pkg ->
+        Self.feedback "Package %a" Pkg.pp_pkgname pkg ;
+        let name = Pkg.name_of_pkginfo ~sep:"/" pkg in
+        let file = Printf.sprintf "%s/%s.ts" (OUT.get ()) name in
+        let dir = Filename.dirname file in
+        Format.eprintf "DIR %S@." dir ;
+        if not (Sys.file_exists dir && Sys.is_directory dir) then
+          Extlib.mkdir ~parents:true dir 0o755 ;
+        Command.print_file file (makePackage pkg name) ;
+      end
+  end
+
+
+let () = Db.Main.extend generate
+
+(* -------------------------------------------------------------------------- *)

src/plugins/server/package.ml

@@ -44,7 +44,7 @@ let pp_plugin_step fmt = function
 let pp_ident fmt { plugin ; package ; name } =
   ( pp_plugin_step fmt plugin ;
     List.iter (pp_step fmt) package ;
-    Format.pp_print_string fmt name )
+    pp_step fmt name )
 
 (* -------------------------------------------------------------------------- *)
 (* --- Name Resolution                                                    --- *)
@@ -232,15 +232,22 @@ type packageInfo = {
   p_content : declInfo list ;
 }
 
-let name_of_ident id =
-  String.concat "." @@ match id.plugin with
+let name_of_ident ?(sep=".") id =
+  String.concat sep @@ match id.plugin with
   | Kernel -> "kernel" :: id.package @ [ id.name ]
   | Plugin p -> p :: (id.package @ [id.name ])
 
-let name_of_pkginfo pkg =
-  String.concat "." @@ match pkg.p_plugin with
-  | Kernel -> "kernel" :: pkg.p_package
-  | Plugin p -> p :: pkg.p_package
+let name_of_pkg ?(sep=".") plugin package =
+  String.concat sep @@ match plugin with
+  | Kernel -> "kernel" :: package
+  | Plugin p -> p :: package
+
+let name_of_pkginfo ?sep { p_plugin ; p_package } =
+  name_of_pkg ?sep p_plugin p_package
+
+let pp_pkgname fmt { p_plugin ; p_package } =
+  ( pp_plugin_step fmt p_plugin ;
+    List.iter (pp_step fmt) p_package )
 
 (* -------------------------------------------------------------------------- *)
 (* --- Visitors                                                           --- *)
@@ -293,7 +300,7 @@ type package = {
   mutable revDecl : declInfo list ; (* in reverse order *)
 }
 
-let name_of_package pkg = name_of_pkginfo pkg.pkgInfo
+let name_of_package ?sep pkg = name_of_pkginfo ?sep pkg.pkgInfo
 
 let registry = ref IdSet.empty (* including packages *)
 let packages = ref [] (* in reverse order *)

src/plugins/server/package.mli

@@ -97,6 +97,7 @@ type packageInfo = {
 (* -------------------------------------------------------------------------- *)
 
 val pp_plugin : Format.formatter -> plugin -> unit
+val pp_pkgname : Format.formatter -> packageInfo -> unit
 val pp_ident : Format.formatter -> ident -> unit
 val pp_jtype : Format.formatter -> jtype -> unit
 
@@ -185,9 +186,10 @@ val iter : (packageInfo -> unit) -> unit
 (** Assigns non-classing names for each identifier. *)
 val resolve : ?keywords: string list -> packageInfo -> string IdMap.t
 
-val name_of_pkginfo : packageInfo -> string
-val name_of_package : package -> string
-val name_of_ident : ident -> string
+val name_of_pkg : ?sep:string -> plugin -> string list -> string
+val name_of_pkginfo : ?sep:string -> packageInfo -> string
+val name_of_package : ?sep:string -> package -> string
+val name_of_ident : ?sep:string -> ident -> string
 
 (* -------------------------------------------------------------------------- *)
 (* --- Markdown Generation                                                --- *)