diff --git a/ivette/.gitignore b/ivette/.gitignore
index da037a9e2fa9fa6eb676dcadabf0f8486c4b79bf..481007d715638802c51aea2edccf5229190ae0fb 100644
--- a/ivette/.gitignore
+++ b/ivette/.gitignore
@@ -4,6 +4,7 @@
.dome-*.stamp
.dome-*.back
+.server-tsc
node_modules
yarn.lock
yarn-error.log
diff --git a/ivette/Makefile b/ivette/Makefile
index 37b317bdb838c21533eadc55362800d1c48e92c4..99550aae931471375f92fe7826a5a0edf84ab97a 100644
--- a/ivette/Makefile
+++ b/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
# --------------------------------------------------------------------------
diff --git a/ivette/api/server_tsc.ml b/ivette/api/server_tsc.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7108f00ffbb818c749f20f5bb2cc73968406594f
--- /dev/null
+++ b/ivette/api/server_tsc.ml
@@ -0,0 +1,99 @@
+(* -------------------------------------------------------------------------- *)
+(* --- 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
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/package.ml b/src/plugins/server/package.ml
index 2c1fdf16826a177a0118278ae6ab6cd9deb3c667..982269288b25969cb44a8e7c7d9510e92fd28503 100644
--- a/src/plugins/server/package.ml
+++ b/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 *)
diff --git a/src/plugins/server/package.mli b/src/plugins/server/package.mli
index 58364ba3fee2c48a553c01db72a1a6677474052d..dd0de862fba73c950c2e2cae3db5b421df80fbed 100644
--- a/src/plugins/server/package.mli
+++ b/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 --- *)