Initial commit

.github/workflows/ci.yml

@@ -0,0 +1,63 @@
+name: Build and test
+
+on:
+  pull_request:
+  push:
+
+jobs:
+
+  nix-dev-build:
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+    runs-on: ${{ matrix.os }}
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v3
+      with:
+        submodules: true
+    - name: Configure Dune
+      run: |
+        mkdir -p ~/.config/dune
+        cat <<EOF > ~/.config/dune/config
+        (lang dune 3.2)
+        (display short)
+        EOF
+    - uses: cachix/install-nix-action@v22
+      with:
+        nix_path: nixpkgs=channel:nixos-unstable
+    - run: nix develop -c bash -c "dune build"
+    - run: nix develop -c bash -c "dune runtest"
+
+  opam-dev-build:
+    strategy:
+      matrix:
+        os:
+          - macos-latest
+          - ubuntu-latest
+        ocaml-compiler:
+          #- "4.11.0"
+          - "4.14.1"
+    runs-on: ${{ matrix.os }}
+    steps:
+      - name: Checkout tree
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+      - name: Set-up OCaml ${{ matrix.ocaml-compiler }}
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+      - name: Install deps
+        env:
+          OPAMYES: true
+        run: |
+          opam install ./jasmin-language-server.opam --deps-only --with-doc --with-test
+      - name: Build jasmin-language-server
+        run: |
+          eval $(opam env)
+          dune build
+      - name: Unit tests
+        run: |
+          eval $(opam env)
+          dune runtest

.gitmodules

@@ -0,0 +1,6 @@
+[submodule "jasmin"]
+	path = jasmin
+	url = https://github.com/jasmin-lang/jasmin.git
+[submodule "jasmin-compiler"]
+	path = jasmin-compiler
+	url = https://gitlab.com/jasmin-lang/jasmin-compiler.git

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2023 Maxime Dénès
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

README.md

@@ -0,0 +1,2 @@
+# jasmin-language-server
+A language server (based on LSP) for Jasmin.

controller/README.md

@@ -0,0 +1,8 @@
+### Language Server
+
+The module [lspManager](lspManager.mli) implements the main SEL event `lsp`
+which deals with LSP requests plus some VSCoq specific messages.
+
+[vscoqtop](vscoqtop.ml) is a Coq toplevel that initializes Coq and then runs
+a SEL loop for the `lsp` event.
+

controller/documentManager.ml

@@ -0,0 +1,31 @@
+open Lsp.Types
+open Jasminlsp.LspData
+open Parsing
+
+type state = {
+  ast : Jasmin.Syntax.pprogram option;
+  cst : Parsing.Syntax.Concrete.node option;
+  parsing_diagnostics : Diagnostic.t list;
+}
+
+let range_of_lexpos startp endp =
+  let open Lexing in
+  let start = Position.{ line = startp.pos_lnum-1; character = startp.pos_cnum - startp.pos_bol; } in
+  let end_ = Position.{ line = endp.pos_lnum-1; character = endp.pos_cnum - endp.pos_bol; } in
+  Range.{ start; end_}
+
+let init ~fname ~text =
+  let input = BatIO.input_string text in
+  let cst, errors, ast = Parse.parse_program ~fname input in
+  let mk_diag (startp, endp) =
+    let range = range_of_lexpos startp endp in
+    let message = "Parsing error." in
+    Diagnostic.create ~range ~message ~severity:DiagnosticSeverity.Error ()
+  in
+  let parsing_diagnostics = List.map mk_diag errors in
+  { parsing_diagnostics; ast = Some ast; cst = Some cst }
+
+let parsing_diagnostics st = st.parsing_diagnostics
+let concrete_syntax_tree st = st.cst
+
+let get_ast st = st.ast

controller/documentManager.mli

@@ -0,0 +1,9 @@
+open Lsp.Types
+
+type state
+
+val init : fname:string -> text:string -> state
+
+val parsing_diagnostics : state -> Diagnostic.t list
+val concrete_syntax_tree : state -> Parsing.Syntax.Concrete.node option
+val get_ast : state -> Jasmin.Syntax.pprogram option

controller/dune

@@ -0,0 +1,30 @@
+;(menhir
+; (flags "--table" "--explain" "--inspection" "--external-tokens" "Jasmin.Parser")
+; (modules raw_parser))
+
+;(rule
+;  (action (with-stdout-to parserMessages.ml
+;    (run menhir
+;      %{dep:raw_parser.mly}
+;      --compile-errors %{dep:parserMessages.messages}
+;    )
+;  ))
+;)
+
+(executable
+ (name jasminlsp)
+ (public_name jasminlsp)
+ (flags (:standard -rectypes -linkall))
+ (package jasmin-language-server)
+ (modules jasminlsp)
+ (libraries jasmin.jasmin sel yojson lsp jsonrpc parsing language controller)
+)
+
+(library
+  (name controller)
+  (modules :standard \ jasminlsp)
+  (flags (:standard -rectypes -linkall))
+  (libraries jasmin.jasmin sel yojson lsp parsing language)
+ (preprocess
+   (pps ppx_yojson_conv))
+)

controller/jasminlsp.ml

@@ -0,0 +1,21 @@
+(** This module implements the entry point of the Jasmin language server *)
+open Controller
+
+let log msg = Format.eprintf "              [%d, %f] %s" (Unix.getpid ()) (Unix.gettimeofday ()) msg
+
+let loop () =
+  let rec loop (todo : LspManager.event Sel.Todo.t) =
+    flush_all ();
+    let ready, todo = Sel.pop todo in
+    let new_events = LspManager.handle_event ready in
+    let todo = Sel.Todo.add todo new_events in
+    loop todo
+  in
+  let todo = Sel.Todo.add Sel.Todo.empty [LspManager.lsp] in
+  try loop todo
+  with exn ->
+    log @@ "Exception raised: " ^ (Printexc.to_string exn)
+
+let _ =
+  Sys.(set_signal sigint Signal_ignore);
+  loop ()