From a5a8d6f3713a799f018ee84917bb0894eeb6fed9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Jun 2020 15:17:49 +0200
Subject: [PATCH] [ivette] typescript API
---
ivette/.gitignore | 1 +
ivette/Makefile | 16 ++++++
ivette/api/server_tsc.ml | 99 ++++++++++++++++++++++++++++++++++
src/plugins/server/package.ml | 23 +++++---
src/plugins/server/package.mli | 8 +--
5 files changed, 136 insertions(+), 11 deletions(-)
create mode 100644 ivette/api/server_tsc.ml
diff --git a/ivette/.gitignore b/ivette/.gitignore
index da037a9e2fa..481007d7156 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 37b317bdb83..99550aae931 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 00000000000..7108f00ffbb
--- /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 2c1fdf16826..982269288b2 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 58364ba3fee..dd0de862fba 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 --- *)
--
GitLab