diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..92fd3e8
--- /dev/null
+++ b/.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
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000..6b16c3d
--- /dev/null
+++ b/.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
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..16434b4
--- /dev/null
+++ b/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.
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..eeb5292
--- /dev/null
+++ b/README.md
@@ -0,0 +1,2 @@
+# jasmin-language-server
+A language server (based on LSP) for Jasmin.
diff --git a/controller/README.md b/controller/README.md
new file mode 100644
index 0000000..cb0dc5e
--- /dev/null
+++ b/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.
+
diff --git a/controller/documentManager.ml b/controller/documentManager.ml
new file mode 100644
index 0000000..4af3c87
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/controller/documentManager.mli b/controller/documentManager.mli
new file mode 100644
index 0000000..50c97c9
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/controller/dune b/controller/dune
new file mode 100644
index 0000000..aaa7a4b
--- /dev/null
+++ b/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))
+)
diff --git a/controller/jasminlsp.ml b/controller/jasminlsp.ml
new file mode 100644
index 0000000..604fc40
--- /dev/null
+++ b/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 ()
diff --git a/controller/lspManager.ml b/controller/lspManager.ml
new file mode 100644
index 0000000..92c3b25
--- /dev/null
+++ b/controller/lspManager.ml
@@ -0,0 +1,265 @@
+open Jasminlsp
+
+let workspace = ref Workspace.empty_workspace
+
+let server_info = Lsp.Types.InitializeResult.create_serverInfo
+  ~name:"jasmin-language-server"
+  ~version: "0.0.1"
+  ()
+
+let log msg = Format.eprintf "       [%d, %f] %s\n" (Unix.getpid ()) (Unix.gettimeofday ()) msg
+
+type lsp_event = 
+  | JsonRpc of Jsonrpc.Packet.t option
+
+type event =
+ | LspManagerEvent of lsp_event
+
+type events = event Sel.Event.t list
+
+let lsp : event Sel.Event.t =
+  Sel.On.httpcle Unix.stdin (function
+    | Ok buff ->
+      begin
+        log "UI req ready";
+        try LspManagerEvent (JsonRpc (Some (Jsonrpc.Packet.t_of_yojson (Yojson.Safe.from_string (Bytes.to_string buff)))))
+        with _exn ->
+          log @@ "failed to decode json";
+          LspManagerEvent (JsonRpc None)
+      end
+    | Error exn ->
+        log @@ ("failed to read message: " ^ Printexc.to_string exn);
+        exit 0)
+
+let output_json obj =
+  let msg  = Yojson.Safe.pretty_to_string ~std:true obj in
+  let size = String.length msg in
+  let s = Printf.sprintf "Content-Length: %d\r\n\r\n%s" size msg in
+  log @@ "sent: " ^ msg;
+  ignore(Unix.write_substring Unix.stdout s 0 (String.length s)) (* TODO ERROR *)
+
+let do_initialize params =
+  begin match params.Lsp.Types.InitializeParams.rootUri with
+  | None -> ()
+  | Some uri ->
+    workspace := Workspace.init ~root:uri
+  end;
+  let open Lsp.Types in
+  let legend = SemanticTokensLegend.{
+    tokenTypes = Language.SemanticTokens.token_types;
+    tokenModifiers = Language.SemanticTokens.token_modifiers;
+  }
+  in
+  let semanticTokensOptions = SemanticTokensOptions.{
+    legend;
+    range = None;
+    full = None;
+    workDoneProgress = None;
+  }
+  in
+  let jazz_pattern = FileOperationPattern.{
+    glob = "**/*.jazz";
+    matches = None;
+    options = None;
+  }
+  in
+  let jinc_pattern = FileOperationPattern.{
+    glob = "**/*.jinc";
+    matches = None;
+    options = None;
+  }
+  in
+  let jazz_filter = FileOperationFilter.{
+    scheme = None;
+    pattern = jazz_pattern;
+  }
+  in
+  let jinc_filter = FileOperationFilter.{
+    scheme = None;
+    pattern = jinc_pattern;
+  }
+  in
+  let filters = [jazz_filter; jinc_filter] in
+  let fileOperationRegistrationOptions = FileOperationRegistrationOptions.{
+    filters;
+  }
+  in
+  let didCreate = fileOperationRegistrationOptions in
+  let willCreate = fileOperationRegistrationOptions in
+  let didRename = fileOperationRegistrationOptions in
+  let willRename = fileOperationRegistrationOptions in
+  let didDelete = fileOperationRegistrationOptions in
+  let willDelete = fileOperationRegistrationOptions in
+  let fileOperations = (FileOperationOptions.create
+    ~didCreate ~willCreate ~didRename ~willRename ~didDelete ~willDelete ())
+  in
+  let textDocumentSync = `TextDocumentSyncKind TextDocumentSyncKind.Full in
+  let completionProvider = CompletionOptions.create () in 
+  let hoverProvider = `Bool true in
+  let semanticTokensProvider = `SemanticTokensOptions semanticTokensOptions in
+  let definitionProvider = `Bool true in
+  let workspace = ServerCapabilities.create_workspace ~fileOperations () in
+  let capabilities = Lsp.Types.ServerCapabilities.create
+    ~textDocumentSync ~completionProvider ~hoverProvider ~semanticTokensProvider ~definitionProvider ~workspace ()
+  in
+  let result = Lsp.Types.InitializeResult.{
+    capabilities = capabilities; 
+    serverInfo = Some server_info;
+  }
+  in
+  Ok result, []
+
+let do_semanticsTokensFull params =
+  let uri = params.Lsp.Types.SemanticTokensParams.textDocument.uri in
+  let fname = Lsp.Uri.to_path uri in
+  let doc = Workspace.get_document !workspace ~fname in
+  let data = match (DocumentManager.concrete_syntax_tree doc) with
+    | None -> log "semantic tokens requested but no cst"; [||]
+    | Some cst -> Array.of_list @@ Language.SemanticTokens.compute_tokens cst
+  in
+  let result = Lsp.Types.SemanticTokens.create ~data () in
+  Ok (Some result), []
+
+let do_definition params =
+  let uri = params.Lsp.Types.DefinitionParams.textDocument.uri in
+  let pos = params.Lsp.Types.DefinitionParams.position in
+  let fname = Lsp.Uri.to_path uri in
+  let result = Workspace.goto_definition !workspace ~fname pos in
+  Ok (Some (`Location (Option.to_list result))), []
+
+let do_shutdown () =
+  Ok (), []
+
+let publish_diagnostics fname diagnostics =
+  let uri = Lsp.Uri.of_path fname in
+  let params = Lsp.Types.PublishDiagnosticsParams.create ~diagnostics ~uri () in
+  let notification = Lsp.Server_notification.PublishDiagnostics params in
+  output_json @@ Jsonrpc.Notification.yojson_of_t @@ Lsp.Server_notification.to_jsonrpc notification
+
+let publish_all_diagnostics () =
+  PathMap.iter publish_diagnostics @@ Workspace.get_diagnostics !workspace
+
+let textDocumentDidOpen params =
+  let Lsp.Types.DidOpenTextDocumentParams.{ textDocument } = params in
+  let fname = Lsp.Uri.to_path textDocument.uri in
+  workspace := Workspace.open_document !workspace ~fname ~text:textDocument.text;
+  publish_all_diagnostics (); (* FIXME restrict to changed diagnostics *)
+  []
+
+let textDocumentDidChange params =
+  let Lsp.Types.DidChangeTextDocumentParams.{ textDocument; contentChanges } = params in
+  begin match contentChanges with
+  | [change] ->
+    let fname = Lsp.Uri.to_path textDocument.uri in
+    workspace := Workspace.open_document !workspace ~fname ~text:change.text;
+    publish_all_diagnostics (); (* FIXME restrict to changed diagnostics *)
+  | _ -> ()
+  end;
+  []
+
+let textDocumentDidClose params =
+  let Lsp.Types.DidCloseTextDocumentParams.{ textDocument } = params in
+  let fname = Lsp.Uri.to_path textDocument.uri in
+  workspace := Workspace.close_document !workspace ~fname;
+  []
+
+(*
+let textDocumentDidChange params =
+  let open Yojson.Safe.Util in
+  let textDocument = params |> member "textDocument" in
+  let uri = textDocument |> member "uri" |> to_string in
+  let contentChanges = params |> member "contentChanges" |> to_list in
+  let read_edit edit =
+    let text = edit |> member "text" |> to_string in
+    let range = Range.t_of_yojson (edit |> member "range") in
+    range, text
+  in
+  let textEdits = List.map read_edit contentChanges in
+  let st = Hashtbl.find states uri in
+  let st = Dm.DocumentManager.apply_text_edits st textEdits in
+  let (st, events) = 
+    if !check_mode = Settings.Mode.Continuous then 
+      Dm.DocumentManager.interpret_to_end st 
+    else 
+      (st, [])
+  in
+  Hashtbl.replace states uri st;
+  publish_diagnostics uri st;
+  uri, events
+
+let textDocumentHover ~id params = 
+  let open Yojson.Safe.Util in
+  let textDocument = params |> member "textDocument" in
+  let uri = textDocument |> member "uri" |> to_string in
+  let loc = params |> member "position" |> parse_loc in 
+  let st = Hashtbl.find states uri in 
+  match Dm.DocumentManager.hover st loc with
+  (* Response: result: Hover | null *)
+  | None -> output_json @@ Response.(yojson_of_t { id; result = Ok (`Null) })
+  | Some (Ok contents) ->
+    let result = Ok (Hover.(yojson_of_t {contents})) in
+    output_json @@ Response.(yojson_of_t { id; result })
+  | _ -> ()
+  *)
+
+let dispatch_request : type a. a Lsp.Client_request.t -> (a, string) result * events =
+  fun req ->
+  match req with
+  | Initialize params ->
+    do_initialize params (* TODO send initial diagnostics *)
+  | SemanticTokensFull params ->
+    do_semanticsTokensFull params
+  | TextDocumentDefinition params ->
+    do_definition params
+  | Shutdown ->
+    do_shutdown ()
+  | _ -> Error "Received unknown request", []
+
+let dispatch_notification =
+  let open Lsp.Client_notification in function
+  | TextDocumentDidOpen params ->
+    textDocumentDidOpen params
+  | TextDocumentDidChange params ->
+    textDocumentDidChange params
+  | TextDocumentDidClose params ->
+    textDocumentDidClose params
+  | _ -> []
+
+let handle_lsp_event = function
+  | JsonRpc None ->
+      [lsp]
+  | JsonRpc (Some rpc) ->
+    lsp ::
+    match rpc with
+    | Request req ->
+        log @@ "ui request: " ^ req.method_;
+        begin match Lsp.Client_request.of_jsonrpc req with
+          | Error message ->
+            log @@ "Error decoding request: " ^ message; []
+          | Ok(E r) ->
+            let resp, events = dispatch_request r in
+            begin match resp with
+            | Error message ->
+              output_json @@ Jsonrpc.Response.(yojson_of_t @@ error req.id (Error.make ~code:RequestFailed ~message ()))
+            | Ok resp ->
+              let resp = Lsp.Client_request.yojson_of_result r resp in
+              output_json Jsonrpc.Response.(yojson_of_t @@ ok req.id resp)
+            end;
+            events
+        end
+    | Notification notif ->
+      begin match Lsp.Client_notification.of_jsonrpc notif with
+      | Ok notif ->
+        dispatch_notification notif
+      | Error e -> log @@ "error decoding notification: " ^ e; []
+      end
+    | Response _resp ->
+        log @@ "got unknown response";
+        []
+    | Batch_response _ -> log "Unsupported batch response received"; []
+    | Batch_call _ -> log "Unsupported batch call received"; []
+
+let handle_event = function
+  | LspManagerEvent e -> handle_lsp_event e
+
+
diff --git a/controller/lspManager.mli b/controller/lspManager.mli
new file mode 100644
index 0000000..646bc9a
--- /dev/null
+++ b/controller/lspManager.mli
@@ -0,0 +1,6 @@
+type event
+type events = event Sel.Event.t list
+
+val lsp : event Sel.Event.t
+
+val handle_event : event -> events
\ No newline at end of file
diff --git a/controller/projectFile.ml b/controller/projectFile.ml
new file mode 100644
index 0000000..42b9e17
--- /dev/null
+++ b/controller/projectFile.ml
@@ -0,0 +1,28 @@
+type architecture = Jasmin.Glob_options.architecture
+
+let architecture_of_yojson = function
+  | `String "x86-64" -> Jasmin.Glob_options.X86_64
+  | `String "arm-m4" -> Jasmin.Glob_options.ARM_M4
+  | _ -> raise (Invalid_argument "architecture_of_yojson")
+
+let yojson_of_architecture = function
+  | Jasmin.Glob_options.X86_64 -> `String "x86-64"
+  | Jasmin.Glob_options.ARM_M4 -> `String "arm-m4"
+
+type source_module = {
+  path: string;
+  architecture: architecture;
+} [@@deriving yojson]
+
+type sources_data = {
+  root: string;
+  modules: source_module list option; [@yojson.option]
+} [@@deriving yojson]
+
+type project_data = {
+  project_name: string;
+  sources: sources_data;
+} [@@deriving yojson]
+
+let parse_project_file ~fname =
+  Yojson.Safe.(from_file fname |> project_data_of_yojson)
\ No newline at end of file
diff --git a/controller/workspace.ml b/controller/workspace.ml
new file mode 100644
index 0000000..4aee0ac
--- /dev/null
+++ b/controller/workspace.ml
@@ -0,0 +1,126 @@
+open Lsp.Types
+open Jasminlsp
+open Language
+
+type root_doc = {
+  prog : Typing.program option;
+  global_env : Typing.global_env;
+  architecture : Jasmin.Glob_options.architecture;
+}
+
+type workspace = {
+  project_data: ProjectFile.project_data option;
+  diagnostics : Diagnostic.t list PathMap.t;
+  references : References.reference_map;
+  open_documents : DocumentManager.state PathMap.t;
+  root_documents : root_doc PathMap.t;
+  revdeps : string PathMap.t;
+}
+
+let empty_workspace = {
+  project_data = None;
+  diagnostics = PathMap.empty;
+  references = References.empty_reference_map;
+  open_documents = PathMap.empty;
+  root_documents = PathMap.empty;
+  revdeps = PathMap.empty;
+}
+
+let find_files ~root acc =
+  let rec explore acc = function
+    | [] -> acc
+    | hd :: tl when Sys.is_directory hd ->
+      let files = List.map (Filename.concat hd) @@ Array.to_list (Sys.readdir hd) in
+      explore acc (files @ tl)
+    | hd :: tl when Filename.extension hd = ".jazz" && not (PathMap.mem hd acc) ->
+      let architecture = Jasmin.Glob_options.ARM_M4 in
+      explore (PathMap.add hd architecture acc) tl
+    | _ :: tl -> explore acc tl
+  in
+  explore acc [root]
+
+let add_parsing_diagnostics workspace diagnostics =
+  let add fname diags =
+    match PathMap.find_opt fname workspace.open_documents with (* FIXME what about parsing errors on non opened files? Are they considered part of typing errors? *)
+    | None -> diags
+    | Some st -> DocumentManager.parsing_diagnostics st @ diags
+  in
+  PathMap.mapi add diagnostics
+
+let analyze_file fname architecture workspace =
+  Printf.eprintf "Analyzing file %s\n" fname;
+  let get_ast ~fname = Option.bind (PathMap.find_opt fname workspace.open_documents) (fun st -> DocumentManager.get_ast st) in 
+  let Typing.{ diagnostics; references; global_env; program; revdeps } = Typing.type_program get_ast ~fname architecture in
+  let diagnostics = add_parsing_diagnostics workspace diagnostics in
+  let diagnostics = PathMap.union (fun _ v _ -> Some v) diagnostics workspace.diagnostics in
+  let root_doc = { global_env; prog = program; architecture } in
+  let root_documents = PathMap.add fname root_doc workspace.root_documents in
+  let revdeps = PathMap.union (fun _ v _ -> Some v) revdeps workspace.revdeps in
+  { workspace with diagnostics; references; root_documents; revdeps }
+
+let init ~root =
+  let path = Lsp.Uri.to_path root in
+  let project_file_name = Filename.concat path "jasmin-project.json" in
+  let project_data = if Sys.file_exists project_file_name then
+    try
+      let open ProjectFile in
+      let data = parse_project_file ~fname:project_file_name in
+      Jasmin.Glob_options.idirs := (data.project_name, data.sources.root)::!Jasmin.Glob_options.idirs; (* FIXME do not rely on glob options *)
+      Some data
+    with Ppx_yojson_conv_lib.Yojson_conv.Of_yojson_error (_,_) ->
+      Format.eprintf "Error parsing jasmin project file\n";
+      None
+  else None
+  in
+  let root_path, modules = match project_data with
+    | Some { sources = { root; modules } } ->
+      let modules = match modules with None -> [] | Some l -> l in
+      Filename.concat path root, modules
+    | None -> path, []
+  in
+  let root_files = List.fold_left (fun acc source_module -> PathMap.add source_module.ProjectFile.path source_module.architecture acc) PathMap.empty modules in
+  let root_files = find_files ~root:root_path root_files in
+  let workspace = 
+  {
+  project_data;
+  diagnostics = PathMap.empty;
+  references = References.empty_reference_map;
+  open_documents = PathMap.empty;
+  root_documents = PathMap.empty;
+  revdeps = PathMap.empty;
+  }
+  in
+  Format.eprintf "Analyzing files from workspace\n";
+  PathMap.fold analyze_file root_files workspace
+
+let open_document workspace ~fname ~text =
+  let doc = DocumentManager.init ~fname ~text in
+  let open_documents = PathMap.add fname doc workspace.open_documents in
+  let workspace = { workspace with open_documents } in
+  match PathMap.find_opt fname workspace.revdeps with
+  | None -> Printf.eprintf "Cannot find root document for %s\n" fname; workspace
+  | Some root_fname ->
+    Printf.eprintf "Opening %s, found root %s\n" fname root_fname;
+    match PathMap.find_opt root_fname workspace.root_documents with
+    | Some root_doc -> analyze_file root_fname root_doc.architecture workspace
+    | None -> Printf.eprintf "Cannot find root document %s\n" root_fname; workspace
+
+let get_document workspace ~fname =
+  PathMap.find fname workspace.open_documents
+
+let close_document workspace ~fname =
+  let open_documents = PathMap.remove fname workspace.open_documents in
+  { workspace with open_documents }
+
+let get_diagnostics workspace =
+  workspace.diagnostics
+
+let goto_definition workspace ~fname pos =
+  match PathMap.find_opt fname workspace.revdeps with
+  | None -> Printf.eprintf "Cannot find root document for %s\n" fname; None
+  | Some root_fname ->
+    Printf.eprintf "Opening %s, found root %s\n" fname root_fname;
+    match PathMap.find_opt root_fname workspace.root_documents with
+    | Some root_doc ->
+      Typing.find_definition ~fname root_doc.global_env workspace.references pos
+    | None -> Printf.eprintf "Cannot find root document %s\n" root_fname; None
diff --git a/controller/workspace.mli b/controller/workspace.mli
new file mode 100644
index 0000000..62979fa
--- /dev/null
+++ b/controller/workspace.mli
@@ -0,0 +1,19 @@
+open Lsp.Types
+open Jasminlsp
+open LspData
+
+type workspace
+
+val empty_workspace : workspace
+val init : root:Lsp.Uri.t -> workspace
+
+val open_document : workspace -> fname:string -> text:string -> workspace
+val get_document : workspace -> fname:string -> DocumentManager.state
+val close_document : workspace -> fname:string -> workspace
+
+val get_diagnostics : workspace -> Diagnostic.t list PathMap.t
+
+val goto_definition : workspace -> fname:string -> Position.t -> Location.t option
+
+(** Internal, for tests *)
+val analyze_file : string -> Jasmin.Glob_options.architecture -> workspace -> workspace
\ No newline at end of file
diff --git a/dune b/dune
new file mode 100644
index 0000000..670ec98
--- /dev/null
+++ b/dune
@@ -0,0 +1,7 @@
+(alias
+   (name default)
+    (deps jasmin-language-server.install))
+(env
+ (dev     (flags :standard -w -9))
+ (release     (flags :standard -w -9)))
+(vendored_dirs jasmin-compiler)
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..483262c
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.2)
+(name jasmin-language-server)
+(license MIT)
+(authors "The Jasmin development team")
+(using menhir 2.1)
\ No newline at end of file
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..dcf533d
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,60 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1692799911,
+        "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1693851727,
+        "narHash": "sha256-CK2uuR2xpRKipdcI3EZJPyNTJsaxwAIquqpnddmoVak=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "6a2fd5e262c552ad8c6b00b86af0a2d58cb7af0a",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..0d7a4ae
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,63 @@
+{
+  description = "A language server for Jasmin based on LSP";
+
+  inputs = {
+
+    flake-utils.url = "github:numtide/flake-utils";
+    nixpkgs.url = "github:NixOS/nixpkgs";
+
+  };
+
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem (system:
+
+    let pkgs = import nixpkgs { inherit system; }; in
+
+    rec {
+
+     packages.default = self.packages.${system}.jasmin-language-server;
+
+     packages.jasmin-language-server =
+       pkgs.ocamlPackages.buildDunePackage {
+         duneVersion = "3";
+         pname = "jasmin-language-server";
+         version = "0.0.1";
+         src = ./.;
+         buildInputs = [
+            pkgs.dune_3
+          ] ++ pkgs.jasmin-compiler.buildInputs
+          ++ (with pkgs.ocamlPackages; [
+           ocaml
+           yojson
+           findlib
+           ppx_inline_test
+           ppx_assert
+           ppx_sexp_conv
+           ppx_deriving
+           sexplib
+           ppx_yojson_conv
+           jsonrpc
+           lsp
+           menhirLib
+           sel
+         ]);
+         propagatedBuildInputs = 
+            pkgs.jasmin-compiler.propagatedBuildInputs;
+         nativeBuildInputs = 
+            pkgs.jasmin-compiler.nativeBuildInputs;
+       };
+
+     devShells.default =
+       with import nixpkgs { inherit system; };
+       mkShell {
+         buildInputs =
+           self.packages.${system}.jasmin-language-server.buildInputs
+           ++ (with ocamlPackages; [
+             ocaml-lsp
+           ]);
+          propagatedBuildInputs = self.packages.${system}.jasmin-language-server.propagatedBuildInputs;
+          nativeBuildInputs = self.packages.${system}.jasmin-language-server.nativeBuildInputs;
+       };
+
+  });
+}
diff --git a/jasmin-compiler b/jasmin-compiler
new file mode 160000
index 0000000..ee48918
--- /dev/null
+++ b/jasmin-compiler
@@ -0,0 +1 @@
+Subproject commit ee4891878fc6a11d7d4a5be31a50b01e8eaa259e
diff --git a/jasmin-language-server.opam b/jasmin-language-server.opam
new file mode 100644
index 0000000..f4d0488
--- /dev/null
+++ b/jasmin-language-server.opam
@@ -0,0 +1,38 @@
+opam-version: "2.0"
+name: "jasmin-language-server"
+maintainer: "Maxime Dénès <maxime.denes@inria.fr>"
+authors: [ "Maxime Dénès" ]
+license: "MIT"
+
+build: [
+  [ "dune" "build" "-p" "jasmin-language-server" "--display=short"] 
+]
+depends: [
+  "dune" {>= "3.2"}
+  "yojson" {>= "1.6.0"}
+  "ocamlfind"
+  "ppx_inline_test"
+  "ppx_assert"
+  "ppx_sexp_conv"
+  "ppx_yojson_conv" {< "v0.16.0"}
+  "ppx_deriving"
+  "sexplib"
+  "menhirLib"
+  "lsp" { >= "1.15"}
+  "jsonrpc" { >= "1.15"}
+  "sel" {>= "0.4.0"}
+#From jasmin-compiler
+  "ocaml" { >= "4.11" & build }
+  "batteries" {>= "3.4"}
+  "cmdliner" {>= "1.1" & build }
+  "menhir" {>= "20160825" & build }
+  "camlidl"
+  "zarith" {>= "1.9"}
+  "apron" {>= "v0.9.12"}
+  "conf-ppl"
+  "ocamlbuild" { build }
+]
+synopsis: "Jasmin language server"
+description: """
+LSP based language server for Jasmin
+"""
diff --git a/language/dune b/language/dune
new file mode 100644
index 0000000..0050237
--- /dev/null
+++ b/language/dune
@@ -0,0 +1,6 @@
+(library
+ (name language)
+ (flags (:standard -rectypes -linkall))
+ (public_name jasmin-language-server.language)
+ (libraries jasmin.jasmin jasminlsp parsing)
+)
diff --git a/language/references.ml b/language/references.ml
new file mode 100644
index 0000000..78dbe50
--- /dev/null
+++ b/language/references.ml
@@ -0,0 +1,76 @@
+open Jasminlsp
+open LspData
+
+module PositionMap = Map.Make(Position)
+
+type reference_r =
+  | RefFun of Jasmin.Annotations.symbol
+
+type reference =
+  { range : Lsp.Types.Range.t; reference: reference_r }
+
+type reference_map = reference PositionMap.t PathMap.t
+
+let empty_reference_map = PathMap.empty
+
+let positions_of_iloc iloc =
+  let loc = iloc.Jasmin.Location.base_loc in
+  let (l1, c1) = loc.loc_start in
+  let (l2, c2) = loc.loc_end in
+  Position.{ line = l1-1; character = c1}, Position.{ line = l2-1; character = c2}
+
+let rec collect_instr_references acc instr =
+  match instr.Jasmin.Prog.i_desc with
+  | Jasmin.Prog.Cassgn (_, _, _, _) -> acc
+  | Jasmin.Prog.Copn (_, _, _, _) -> acc
+  | Jasmin.Prog.Csyscall (_, _, _) -> acc
+  | Jasmin.Prog.Cif (_, stmt1, stmt2) ->
+    let acc = collect_prog_references acc stmt1 in
+    collect_prog_references acc stmt2
+  | Jasmin.Prog.Cfor (_, _, stmt) ->
+    collect_prog_references acc stmt
+  | Jasmin.Prog.Cwhile (_, stmt1, _, stmt2) ->
+    let acc = collect_prog_references acc stmt1 in
+    collect_prog_references acc stmt2
+  | Jasmin.Prog.Ccall (_, _, funname, _) ->
+    let (start, end_) = positions_of_iloc instr.i_loc in
+    let range = Lsp.Types.Range.{ start; end_ } in
+    let r = { range; reference = RefFun funname.fn_name } in
+    let fname = instr.i_loc.base_loc.loc_fname in
+    PathMap.update fname (function None -> Some (PositionMap.singleton start r) | Some map -> Some (PositionMap.add start r map)) acc
+
+and collect_prog_references acc prog =
+  List.fold_left collect_instr_references acc prog
+
+let collect_mod_references acc m =
+  match m with
+  | Jasmin.Prog.MIfun { f_body } -> collect_prog_references acc f_body
+  | Jasmin.Prog.MIparam _ -> acc
+  | Jasmin.Prog.MIglobal _ -> acc
+
+let collect_references prog =
+  List.fold_left collect_mod_references PathMap.empty prog
+
+let find_reference refmap pos =
+  Printf.eprintf "Search for reference at line %d char %d\n" pos.Position.line pos.character;
+  match PositionMap.find_last_opt (fun start -> Position.compare start pos <= 0) refmap with
+  | None -> None
+  | Some (_,r) ->
+    Printf.eprintf "Found reference close to pos, ends line %d char %d\n" r.range.end_.line r.range.end_.character;
+    if Position.compare r.range.end_ pos >= 0 then Some r else None
+
+let find_definition env refmap ~fname pos =
+  begin match PathMap.find_opt fname refmap with
+  | None -> None
+  | Some map ->
+    Printf.eprintf "Found map\n";
+    begin match find_reference map pos with
+    | None -> None
+    | Some { reference = RefFun funname } ->
+      Printf.eprintf "Found function reference %s\n" funname;
+      begin match Jasmin.Pretyping.Env.Funs.find funname env with
+      | None -> None
+      | Some (func,_ty) -> Some (Location.of_jasmin_loc func.f_loc)
+      end
+    end
+  end
\ No newline at end of file
diff --git a/language/references.mli b/language/references.mli
new file mode 100644
index 0000000..a30327f
--- /dev/null
+++ b/language/references.mli
@@ -0,0 +1,9 @@
+open Jasminlsp.LspData
+
+type reference_map
+
+val empty_reference_map : reference_map
+
+val collect_references : ('info, 'asm) Jasmin.Prog.pprog -> reference_map
+
+val find_definition : 'asm Jasmin.Pretyping.Env.env -> reference_map -> fname:string -> Lsp.Types.Position.t -> Location.t option
\ No newline at end of file
diff --git a/language/semanticTokens.ml b/language/semanticTokens.ml
new file mode 100644
index 0000000..ad72707
--- /dev/null
+++ b/language/semanticTokens.ml
@@ -0,0 +1,36 @@
+let token_types = ["function"; "keyword"]
+
+let token_modifiers = []
+
+let _log msg = Format.eprintf "       [%d, %f] %s" (Unix.getpid ()) (Unix.gettimeofday ()) msg
+
+let push_token tokens ~deltaLine ~deltaStart ~length ~tokenType ~tokenModifiers =
+  tokenModifiers :: tokenType :: length :: deltaStart :: deltaLine :: tokens
+
+let delta_loc lastLine lastStart loc =
+  let newLine, newStart = loc.Jasmin.Location.loc_start in
+  let newLine = newLine - 1 in
+  let deltaLine = newLine - lastLine in
+  let deltaStart = if deltaLine > 0 then newStart else newStart - lastStart in
+  (deltaLine, deltaStart, newLine, newStart)
+
+let is_keyword (token : Jasmin.Parser.token) =
+  BatHashtbl.exists (fun _ t -> t = token) Jasmin.Lexer.keywords
+
+let compute_token (lastLine,lastStart,tokens) node =
+  (* log ("cst = " ^ Syntax.Concrete.show_tree node); *)
+  let open Parsing.Syntax.Concrete in
+  let Jasmin.Location.{ pl_loc; pl_desc = green } = node.green in
+  let length = pl_loc.loc_echar - pl_loc.loc_bchar in
+  let parent_green = Option.bind node.top (fun x -> Some x.green.pl_desc) in
+  let (deltaLine, deltaStart, newLine, newStart) = delta_loc lastLine lastStart pl_loc in
+  match green, parent_green with
+  | Terminal (Jasmin.Parser.NID _), Some (NonTerminal { kind = (X Jasmin.Parser.MenhirInterpreter.N_pfundef) }) -> 
+    newLine, newStart, push_token tokens ~deltaLine ~deltaStart ~length ~tokenType:0 ~tokenModifiers:0
+  | Terminal token, _ when is_keyword token ->
+    newLine, newStart, push_token tokens ~deltaLine ~deltaStart ~length ~tokenType:1 ~tokenModifiers:0
+  | _ -> lastLine, lastStart, tokens
+
+let compute_tokens cst =
+  let _,_,tokens = Parsing.Syntax.Concrete.fold compute_token (0,0,[]) cst in
+  List.rev tokens
\ No newline at end of file
diff --git a/language/semanticTokens.mli b/language/semanticTokens.mli
new file mode 100644
index 0000000..695ac25
--- /dev/null
+++ b/language/semanticTokens.mli
@@ -0,0 +1,3 @@
+val token_types : string list
+val token_modifiers : string list
+val compute_tokens : Parsing.Syntax.Concrete.node -> int list
\ No newline at end of file
diff --git a/language/typing.ml b/language/typing.ml
new file mode 100644
index 0000000..e3d448e
--- /dev/null
+++ b/language/typing.ml
@@ -0,0 +1,134 @@
+open Lsp.Types
+open Jasminlsp
+open LspData
+
+module type ArchCoreWithAnalyze = sig
+  module C : Jasmin.Arch_full.Core_arch
+end
+
+open Jasmin.Pretyping
+
+type global_env =
+  GlobEnv : 'asm Jasmin.Pretyping.Env.env -> global_env
+
+type program =
+  Program : ('asm, 'info) Jasmin.Prog.pprog -> program
+
+type typing_result = {
+  diagnostics : Diagnostic.t list PathMap.t;
+  references : References.reference_map;
+  global_env : global_env;
+  program : program option;
+  revdeps : string PathMap.t;
+}
+
+let push_diag fname diag diagnostics =
+  let update = function None -> Some [diag] | Some l -> Some (diag::l) in
+  PathMap.update fname update diagnostics
+
+let rec type_item get_ast arch_info (env, diagnostics, revdeps) pt ~root_fname =
+  let check pt =
+    let open Jasmin.Syntax in
+    match Jasmin.Location.unloc pt with
+    | PParam  pp -> tt_param  arch_info.pd env (L.loc pt) pp, diagnostics, revdeps
+    | PFundef pf -> tt_fundef arch_info env (L.loc pt) pf, diagnostics, revdeps
+    | PGlobal pg -> tt_global arch_info.pd env (L.loc pt) pg, diagnostics, revdeps
+    | Pexec   pf ->
+      Env.Exec.push (L.loc pt) (fst (tt_fun env pf.pex_name)).Jasmin.Prog.f_name pf.pex_mem env, diagnostics, revdeps
+    | Prequire (from, fs) -> 
+      List.fold_left (fun acc req -> type_file_loc get_ast arch_info from acc ~root_fname req) (env, diagnostics, revdeps) fs
+  in
+  try
+    check pt
+  with
+  | Jasmin.Pretyping.TyError (loc, code) ->
+    let range = Range.of_jasmin_loc loc in
+    let buf = Buffer.create 128 in
+    let fmt = Format.formatter_of_buffer buf in
+    Jasmin.Pretyping.pp_tyerror fmt code;
+    Format.pp_print_flush fmt ();
+    let message = Buffer.contents buf in
+    let diag = Diagnostic.create ~range ~message ~severity:DiagnosticSeverity.Error () in
+    let diagnostics = push_diag loc.loc_fname diag diagnostics in
+    (env, diagnostics, revdeps)
+
+and type_file_loc get_ast arch_info from env ~root_fname req =
+  let loc = Jasmin.Location.loc req in
+  let fname = Jasmin.Location.unloc req in
+  fst (type_file get_ast arch_info env from (Some loc) ~root_fname ~fname)
+
+and type_file get_ast arch_info (env, diagnostics, revdeps) from loc ~root_fname ~fname =
+  match Env.enter_file env from loc fname with
+  | None -> (env, diagnostics, revdeps), [] (* already checked *)
+  | Some(env, fname) ->
+    let revdeps = PathMap.add fname root_fname revdeps in
+    try
+      let ast = match get_ast ~fname with (* FIXME add parsing diags here *)
+        | None ->
+          let ast = Parsing.Parse.parse_program ~fname in
+          let _,_,ast =  BatFile.with_file_in fname ast in ast
+        | Some ast -> ast
+      in
+      let diagnostics = PathMap.add fname [] diagnostics in
+      let (env, diagnostics, revdeps) = List.fold_left (type_item get_ast arch_info ~root_fname) (env, diagnostics, revdeps) ast in
+      (Env.exit_file env, diagnostics, revdeps), ast
+    with Sys_error message ->
+      let diagnostics = match loc with
+      | None -> diagnostics
+      | Some loc ->
+        let fname = loc.loc_fname in
+        let range = Range.of_jasmin_loc loc in
+        let diag = Diagnostic.create ~range ~message ~severity:DiagnosticSeverity.Error () in
+        push_diag fname diag diagnostics
+      in
+      (Env.exit_file env, diagnostics, revdeps), []
+
+let type_program get_ast ~fname target_arch =
+  let (module P : ArchCoreWithAnalyze) =
+    match target_arch with
+    | Jasmin.Glob_options.X86_64 ->
+       (module struct
+          module C = (val Jasmin.CoreArchFactory.core_arch_x86 ~use_lea:!Jasmin.Glob_options.lea ~use_set0:!Jasmin.Glob_options.set0 !Jasmin.Glob_options.call_conv)
+        end)
+    | ARM_M4 ->
+       (module struct
+          module C = Jasmin.CoreArchFactory.Core_arch_ARM
+        end)
+  in
+  let module Arch = Jasmin.Arch_full.Arch_from_Core_arch (P.C) in
+  let env =
+    List.fold_left Jasmin.Pretyping.Env.add_from Jasmin.Pretyping.Env.empty
+      !Jasmin.Glob_options.idirs (* FIXME do not rely on glob options *)
+  in
+  Jasmin.Glob_options.target_arch := target_arch; 
+  let diagnostics = PathMap.singleton fname [] in
+  let revdeps = PathMap.empty in
+  let (env, diagnostics, revdeps), _ast = type_file get_ast Arch.arch_info (env, diagnostics, revdeps) None None ~root_fname:fname ~fname in
+  let pprog = Jasmin.Pretyping.Env.decls env in
+  let references = References.collect_references pprog in (* FIXME do this analysis on ast, before typing *)
+  begin try
+    let _prog = Jasmin.Compile.preprocess Arch.reg_size Arch.asmOp pprog in
+    {
+      diagnostics;
+      references;
+      global_env = GlobEnv env;
+      program = Some (Program pprog);
+      revdeps;
+    }
+  with Jasmin.Typing.TyError(loc, message) ->
+    let range = Range.of_jasmin_loc loc.base_loc in
+    let fname = loc.base_loc.loc_fname in
+    let diag = Diagnostic.create ~range ~message ~severity:DiagnosticSeverity.Error () in
+    let diagnostics = PathMap.singleton fname [diag] in
+    {
+      diagnostics;
+      references;
+      global_env = GlobEnv env;
+      program = None;
+      revdeps;
+    }
+  end
+
+let find_definition ~fname global_env references pos =
+  let GlobEnv env = global_env in
+  References.find_definition env references ~fname pos
\ No newline at end of file
diff --git a/language/typing.mli b/language/typing.mli
new file mode 100644
index 0000000..8ee41eb
--- /dev/null
+++ b/language/typing.mli
@@ -0,0 +1,22 @@
+open Lsp.Types
+open Jasminlsp
+open LspData
+
+type global_env
+type program
+
+type typing_result = {
+  diagnostics : Diagnostic.t list PathMap.t;
+  references : References.reference_map;
+  global_env : global_env;
+  program : program option;
+  revdeps : string PathMap.t;
+}
+
+val type_program :
+  (fname:string -> Jasmin.Syntax.pprogram option) ->
+  fname:string ->
+  Jasmin.Glob_options.architecture ->
+  typing_result
+
+val find_definition : fname:string -> global_env -> References.reference_map -> Lsp.Types.Position.t -> Location.t option
\ No newline at end of file
diff --git a/lsp/dune b/lsp/dune
new file mode 100644
index 0000000..df071e5
--- /dev/null
+++ b/lsp/dune
@@ -0,0 +1,7 @@
+(library
+ (name jasminlsp)
+ (public_name jasmin-language-server.lsp)
+ (libraries lsp sexplib yojson jasmin.jasmin)
+ (flags (:standard -rectypes -linkall))
+ (preprocess
+   (pps ppx_sexp_conv ppx_yojson_conv)))
diff --git a/lsp/lspData.ml b/lsp/lspData.ml
new file mode 100644
index 0000000..e256f4a
--- /dev/null
+++ b/lsp/lspData.ml
@@ -0,0 +1,96 @@
+module Position = struct
+  
+  include Lsp.Types.Position
+
+  let compare pos1 pos2 =
+    match Int.compare pos1.line pos2.line with
+    | 0 -> Int.compare pos1.character pos2.character
+    | x -> x
+
+  let to_string pos = Format.sprintf "(%i,%i)" pos.line pos.character
+
+end
+
+module Range = struct
+
+  include Lsp.Types.Range
+
+  let of_jasmin_loc Jasmin.Location.{ loc_start; loc_end } =
+    let (start_line, start_char) = loc_start in
+    let (end_line, end_char) = loc_end in
+    let start = Position.{ line = start_line-1; character = start_char; } in
+    let end_ = Position.{ line = end_line-1; character = end_char; } in
+    { start; end_}
+
+end 
+
+module Location = struct
+
+  include Lsp.Types.Location
+
+  let of_jasmin_loc loc =
+    let uri = Lsp.Uri.of_path loc.Jasmin.Location.loc_fname in
+    let (l1, c1) = loc.Jasmin.Location.loc_start in
+    let (l2, c2) = loc.Jasmin.Location.loc_end in
+    let start = Lsp.Types.Position.{ line = l1; character = c1} in
+    let end_ = Lsp.Types.Position.{ line = l2; character = c2} in
+    let range = Lsp.Types.Range.{ start; end_ } in
+    { uri; range }
+
+end
+
+module Settings = struct
+
+  module DelegationMode = struct
+
+  type t = 
+    | None
+    | Skip 
+    | Delegate 
+
+  let yojson_of_t = function
+  | None -> `String "None"
+  | Skip -> `String "Skip"
+  | Delegate -> `String "Delegate"
+
+  let t_of_yojson = function
+  | `String "None" -> None
+  | `String "Skip" -> Skip
+  | `String "Delegate" -> Delegate
+  | _ -> Yojson.json_error "invalid value"
+
+  end
+  
+  module Mode = struct
+
+    type t =
+    | Continuous 
+    | Manual
+    [@@deriving yojson]
+      
+    let yojson_of_t = function
+    | Manual -> `Int 0
+    | Continuous -> `Int 1
+  
+    let t_of_yojson = function
+    | `Int 0 -> Manual
+    | `Int 1 -> Continuous
+    | _ -> Yojson.json_error @@ "invalid value "
+  
+  end
+
+  module Proof = struct
+
+    type t = {
+      delegation: DelegationMode.t;
+      workers: int option;
+      mode: Mode.t;
+    } [@@deriving yojson] [@@yojson.allow_extra_fields]
+
+  end
+
+  type t = {
+    proof: Proof.t;
+  } [@@deriving yojson] [@@yojson.allow_extra_fields]
+
+end
\ No newline at end of file
diff --git a/lsp/pathMap.ml b/lsp/pathMap.ml
new file mode 100644
index 0000000..d233671
--- /dev/null
+++ b/lsp/pathMap.ml
@@ -0,0 +1 @@
+include Map.Make(String)
\ No newline at end of file
diff --git a/lsp/uriMap.ml b/lsp/uriMap.ml
new file mode 100644
index 0000000..fb12033
--- /dev/null
+++ b/lsp/uriMap.ml
@@ -0,0 +1 @@
+include Map.Make(Lsp.Uri)
\ No newline at end of file
diff --git a/parsing/dune b/parsing/dune
new file mode 100644
index 0000000..9f7f05a
--- /dev/null
+++ b/parsing/dune
@@ -0,0 +1,8 @@
+(library
+ (name parsing)
+ (flags (:standard -rectypes -linkall))
+ (public_name jasmin-language-server.parsing)
+ (libraries jasmin.jasmin)
+ (preprocess
+  (pps ppx_deriving.show))
+)
diff --git a/parsing/lexer.ml b/parsing/lexer.ml
new file mode 100644
index 0000000..941f4c9
--- /dev/null
+++ b/parsing/lexer.ml
@@ -0,0 +1,59 @@
+type triple = Jasmin.Parser.token * Lexing.position * Lexing.position
+
+let buffer =
+  ref []
+
+let size =
+  ref 0
+
+let more = ref (fun () -> assert false)
+
+let initialize lexbuf =
+  more := Jasmin.Parser.MenhirInterpreter.lexer_lexbuf_to_supplier Jasmin.Lexer.main lexbuf;
+  buffer := [];
+  size := 0
+
+type t = int
+
+let start = 0
+
+let get pos =
+  List.nth !buffer (!size - pos)
+
+let token_of_ptoken (p, _, _) = p
+
+(*
+let current_position_of_ptoken (_, start, stop) =
+  Position.lex_join start stop
+
+let current_position pos =
+  current_position_of_ptoken (get pos)
+  *)
+
+let get' pos =
+  token_of_ptoken (get pos)
+
+let next pos =
+  if pos >= !size - 1 then (
+    buffer := !more () :: !buffer;
+    incr size;
+  );
+  let pos = pos + 1 in
+  (get pos, pos)
+
+let skip_until_before pred pos =
+  let rec aux pos =
+    let token, _, _ = get pos in
+    if token = Jasmin.Parser.EOF then pos
+    else if pred token then pos - 1
+    else aux (snd (next pos))
+  in
+  aux pos
+
+let lex_until_before pred pos =
+  let rec aux acc ((token,_,_ as triple),pos) =
+    if token = Jasmin.Parser.EOF then List.rev (triple::acc), pos
+    else if pred token then List.rev acc, pos - 1
+    else aux (triple::acc) (next pos)
+  in
+  aux [] (get pos, pos)
\ No newline at end of file
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
new file mode 100644
index 0000000..ea95fca
--- /dev/null
+++ b/parsing/lexer.mli
@@ -0,0 +1,12 @@
+type t
+type triple = Jasmin.Parser.token * Lexing.position * Lexing.position
+val initialize : Lexing.lexbuf -> unit
+val start : t
+val next  : t -> triple * t
+val get   : t -> triple
+val get'  : t -> Jasmin.Parser.token
+(*
+val current_position : t -> Position.t
+*)
+val skip_until_before : (Jasmin.Parser.token -> bool) -> t -> t
+val lex_until_before : (Jasmin.Parser.token -> bool) -> t -> triple list * t
\ No newline at end of file
diff --git a/parsing/parse.ml b/parsing/parse.ml
new file mode 100644
index 0000000..a731cae
--- /dev/null
+++ b/parsing/parse.ml
@@ -0,0 +1,460 @@
+module L = MenhirLib.LexerUtil
+module E = MenhirLib.ErrorReports
+
+module P = Jasmin.Parser
+
+module I = P.MenhirInterpreter
+
+type token = Jasmin.Parser.token =
+  | WHILE
+  | UNDERSCORE
+  | T_U8
+  | T_U64
+  | T_U32
+  | T_U256
+  | T_U16
+  | T_U128
+  | T_INT
+  | T_BOOL
+  | TRUE
+  | TO
+  | SWSIZE of (Jasmin.Syntax.swsize) [@printer fun fmt _ -> fprintf fmt "SWSIZE"]
+  | SVSIZE of (Jasmin.Syntax.svsize) [@printer fun fmt _ -> fprintf fmt "SVSIZE"]
+  | STRING of (string)
+  | STAR
+  | STACK
+  | SLASH
+  | SHARP
+  | SEMICOLON
+  | RPAREN
+  | ROR
+  | ROL
+  | RETURN
+  | REQUIRE
+  | REG
+  | RBRACKET
+  | RBRACE
+  | RARROW
+  | QUESTIONMARK
+  | POINTER
+  | PLUS
+  | PIPEPIPE
+  | PIPE
+  | PERCENT
+  | PARAM
+  | NID of (string)
+  | MUTABLE
+  | MINUS
+  | LTLT
+  | LT of (Jasmin.Syntax.sign) [@printer fun fmt _ -> fprintf fmt "LT"]
+  | LPAREN
+  | LE of (Jasmin.Syntax.sign) [@printer fun fmt _ -> fprintf fmt "LE"]
+  | LBRACKET
+  | LBRACE
+  | INT of (Z.t) [@printer fun fmt _ -> fprintf fmt "INT"] 
+  | INLINE
+  | IF
+  | HAT
+  | GTGT of (Jasmin.Syntax.sign) [@printer fun fmt _ -> fprintf fmt "GTGT"]
+  | GT of (Jasmin.Syntax.sign) [@printer fun fmt _ -> fprintf fmt "GT"]
+  | GLOBAL
+  | GE of (Jasmin.Syntax.sign) [@printer fun fmt _ -> fprintf fmt "GE"]
+  | FROM
+  | FOR
+  | FN
+  | FALSE
+  | EXPORT
+  | EXEC
+  | EQEQ
+  | EQ
+  | EOF
+  | ELSE
+  | DOWNTO
+  | DOT
+  | CONSTANT
+  | COMMA
+  | COLON
+  | BANGEQ
+  | BANG
+  | ARRAYINIT
+  | AMPAMP
+  | AMP
+[@@deriving show]
+
+
+(* -------------------------------------------------------------------- *)
+open MenhirLib.General
+open I
+
+module Printers = struct
+
+  let buf = Buffer.create 16
+  let print s = Buffer.add_string buf s
+
+  let print_nt : type a. a nonterminal -> string =
+    fun nt ->
+    match nt with
+    | N_writable -> "writable"
+    | N_var -> "var"
+    | N_utype -> "utype"
+    | N_top_annotation -> "top_annotation"
+    | N_top -> "top"
+    | N_swsize -> "swsize"
+    | N_svsize -> "svsize"
+    | N_struct_annot -> "struct_annot"
+    | N_storage -> "storage"
+    | N_stor_type -> "stor_type"
+    | N_simple_attribute -> "simple_attribute"
+    | N_separated_nonempty_list_option_COMMA__var_ -> "separated_nonempty_list_option_COMMA__var_"
+    | N_separated_nonempty_list_empty_var_ -> "separated_nonempty_list_empty_var_"
+    | N_separated_nonempty_list_COMMA_var_ -> "separated_nonempty_list_COMMA_var_"
+    | N_separated_nonempty_list_COMMA_range_ -> "separated_nonempty_list_COMMA_range_"
+    | N_separated_nonempty_list_COMMA_plvalue_ -> "separated_nonempty_list_COMMA_plvalue_"
+    | N_separated_nonempty_list_COMMA_pexpr_ -> "separated_nonempty_list_COMMA_pexpr_"
+    | N_separated_nonempty_list_COMMA_annotation_ -> "separated_nonempty_list_COMMA_annotation_"
+    | N_separated_nonempty_list_COMMA_annot_stor_type_ -> "separated_nonempty_list_COMMA_annot_stor_type_"
+    | N_separated_nonempty_list_COMMA_annot_pvardecl_ -> "separated_nonempty_list_COMMA_annot_pvardecl_"
+    | N_range -> "range"
+    | N_ptype -> "ptype"
+    | N_ptr -> "ptr"
+    | N_prim -> "prim"
+    | N_prequire1 -> "prequire1"
+    | N_prequire -> "prequire"
+    | N_pparam -> "pparam"
+    | N_pointer -> "pointer"
+    | N_plvalues -> "plvalues"
+    | N_plvalue -> "plvalue"
+    | N_pinstr_r -> "pinstr_r"
+    | N_pinstr -> "pinstr"
+    | N_pif -> "pif"
+    | N_pglobal -> "pglobal"
+    | N_pgexpr -> "pgexpr"
+    | N_pfundef -> "pfundef"
+    | N_pfunbody -> "pfunbody"
+    | N_pexpr -> "pexpr"
+    | N_pexec -> "pexec"
+    | N_peqop -> "peqop"
+    | N_pelseif -> "pelseif"
+    | N_pelse -> "pelse"
+    | N_pblock -> "pblock"
+    | N_option_writable_ -> "option_writable_"
+    | N_option_utype_ -> "option_utype_"
+    | N_option_prefix_RARROW_tuple_annot_stor_type___ -> "option_prefix_RARROW_tuple_annot_stor_type___"
+    | N_option_prefix_IF_pexpr__ -> "option_prefix_IF_pexpr__"
+    | N_option_pointer_ -> "option_pointer_"
+    | N_option_pblock_ -> "option_pblock_"
+    | N_option_parens_utype__ -> "option_parens_utype__"
+    | N_option_mem_ofs_ -> "option_mem_ofs_"
+    | N_option_from_ -> "option_from_"
+    | N_option_call_conv_ -> "option_call_conv_"
+    | N_option_attribute_ -> "option_attribute_"
+    | N_option_arr_access_len_ -> "option_arr_access_len_"
+    | N_option_DOT_ -> "option_DOT_"
+    | N_option_COMMA_ -> "option_COMMA_"
+    | N_nonempty_list_prequire1_ -> "nonempty_list_prequire1_"
+    | N_module_ -> "module_"
+    | N_loption_separated_nonempty_list_COMMA_var__ -> "loption_separated_nonempty_list_COMMA_var__"
+    | N_loption_separated_nonempty_list_COMMA_range__ -> "loption_separated_nonempty_list_COMMA_range__"
+    | N_loption_separated_nonempty_list_COMMA_pexpr__ -> "loption_separated_nonempty_list_COMMA_pexpr__"
+    | N_loption_separated_nonempty_list_COMMA_annotation__ -> "loption_separated_nonempty_list_COMMA_annotation__"
+    | N_loption_separated_nonempty_list_COMMA_annot_stor_type__ -> "loption_separated_nonempty_list_COMMA_annot_stor_type__"
+    | N_loption_separated_nonempty_list_COMMA_annot_pvardecl__ -> "loption_separated_nonempty_list_COMMA_annot_pvardecl__"
+    | N_list_top_annotation_ -> "list_top_annotation_"
+    | N_list_pinstr_ -> "list_pinstr_"
+    | N_keyword -> "keyword"
+    | N_int -> "int"
+    | N_implicites -> "implicites"
+    | N_from -> "from"
+    | N_castop1 -> "castop1"
+    | N_castop -> "castop"
+    | N_cast -> "cast"
+    | N_call_conv -> "call_conv"
+    | N_attribute -> "attribute"
+    | N_arr_access_len -> "arr_access_len"
+    | N_arr_access_i -> "arr_access_i"
+    | N_arr_access -> "arr_access"
+    | N_annotations -> "annotations"
+    | N_annotationlabel -> "annotationlabel"
+    | N_annotation -> "annotation"
+    | N_annot_stor_type -> "annot_stor_type"
+    | N_annot_pvardecl -> "annot_pvardecl"
+    | N_ptype_r -> "ptype_r"
+    | N_plvalue_r -> "plvalue_r"
+    | N_pexpr_r -> "pexpr_r"
+    | N_pblock_r -> "pblock_r"
+    | N_option_loc_castop1__ -> "option_loc_castop1"
+    | N_option___anonymous_1_ -> "option___anonymous_1"
+    | N_list_loc_top__ -> "list_loc_top"
+
+  let print_terminal : type a. a terminal -> string =
+    fun t -> match t with
+    | T_error -> "error"
+    | T_WHILE -> "WHILE"
+    | T_UNDERSCORE -> "UNDERSCORE"
+    | T_T_U8 -> "T_U8"
+    | T_T_U64 -> "T_U64"
+    | T_T_U32 -> "T_U32"
+    | T_T_U256 -> "T_U256"
+    | T_T_U16 -> "T_U16"
+    | T_T_U128 -> "T_U128"
+    | T_T_INT -> "T_INT"
+    | T_T_BOOL -> "T_BOOL"
+    | T_TRUE -> "TRUE"
+    | T_TO -> "TO"
+    | T_SWSIZE -> "SWSIZE"
+    | T_SVSIZE -> "SVSIZE"
+    | T_STRING -> "STRING"
+    | T_STAR -> "STAR"
+    | T_STACK -> "STACK"
+    | T_SLASH -> "SLASH"
+    | T_SHARP -> "SHARP"
+    | T_SEMICOLON -> "SEMICOLON"
+    | T_RPAREN -> "RPAREN"
+    | T_ROR -> "ROR"
+    | T_ROL -> "ROL"
+    | T_RETURN -> "RETURN"
+    | T_REQUIRE -> "REQUIRE"
+    | T_REG -> "REG"
+    | T_RBRACKET -> "RBRACKET"
+    | T_RBRACE -> "RBRACE"
+    | T_RARROW -> "RARROW"
+    | T_QUESTIONMARK -> "QUESTIONMARK"
+    | T_POINTER -> "POINTER"
+    | T_PLUS -> "PLUS"
+    | T_PIPEPIPE -> "PIPEPIPE"
+    | T_PIPE -> "PIPE"
+    | T_PERCENT -> "PERCENT"
+    | T_PARAM -> "PARAM"
+    | T_NID -> "NID"
+    | T_MUTABLE -> "MUTABLE"
+    | T_MINUS -> "MINUS"
+    | T_LTLT -> "LTLT"
+    | T_LT -> "LT"
+    | T_LPAREN -> "LPAREN"
+    | T_LE -> "LE"
+    | T_LBRACKET -> "LBRACKET"
+    | T_LBRACE -> "LBRACE"
+    | T_INT -> "INT"
+    | T_INLINE -> "INLINE"
+    | T_IF -> "IF"
+    | T_HAT -> "HAT"
+    | T_GTGT -> "GTGT"
+    | T_GT -> "GT"
+    | T_GLOBAL -> "GLOBAL"
+    | T_GE -> "GE"
+    | T_FROM -> "FROM"
+    | T_FOR -> "FOR"
+    | T_FN -> "FN"
+    | T_FALSE -> "FALSE"
+    | T_EXPORT -> "EXPORT"
+    | T_EXEC -> "EXEC"
+    | T_EQEQ -> "EQEQ"
+    | T_EQ -> "EQ"
+    | T_EOF -> "EOF"
+    | T_ELSE -> "ELSE"
+    | T_DOWNTO -> "DOWNTO"
+    | T_DOT -> "DOT"
+    | T_CONSTANT -> "CONSTANT"
+    | T_COMMA -> "COMMA"
+    | T_COLON -> "COLON"
+    | T_BANGEQ -> "BANGEQ"
+    | T_BANG -> "BANG"
+    | T_ARRAYINIT -> "ARRAYINIT"
+    | T_AMPAMP -> "AMPAMP"
+    | T_AMP -> "AMP"
+
+  let print_symbol (symbol : xsymbol) =
+    let s = match symbol with
+    | X (T t) -> print_terminal t
+    | X (N nt) -> print_nt nt
+    in
+    Buffer.add_string buf s
+
+  let print_element = Some (fun _e -> Buffer.add_string buf "EL")
+
+  let reset () = Buffer.reset buf
+
+end
+
+module Print = MenhirLib.Printers.Make(I)(Printers)
+
+let string_of_symbol symb =
+  Printers.reset ();
+  Printers.print_symbol symb;
+  Buffer.contents Printers.buf
+
+type 'a last_reduction =
+  | FoundTopAt of 'a
+  | FoundInstructionAt of 'a
+  | FoundNothingAt of 'a
+
+type 'a recovery_state = {
+  last_reduction : 'a last_reduction;
+  new_symbols : int;
+}
+
+let rec reduce_cst n nt cst acc =
+  match cst with
+  | [] -> if n > 0 then raise (Failure "More symbols but empty cst")
+    else [Syntax.Concrete.make_nonterminal nt acc]
+  | Jasmin.Location.{ pl_desc = Syntax.Concrete.NonTerminal { kind = Error } } as symb :: cst' ->
+    (* Error nodes should not count as RHS symbols *)
+    reduce_cst n nt cst' (symb::acc)
+  | symb :: cst' ->
+    if n > 0 then reduce_cst (n-1) nt cst' (symb::acc)
+    else Syntax.Concrete.make_nonterminal nt acc :: cst
+
+let update_recovery_state_reduce inputneeded production recovery_state =
+  match lhs production with
+  | X (N N_top) ->
+     { last_reduction = FoundTopAt inputneeded; new_symbols = 0 }
+  | X (N N_pinstr) ->
+     { last_reduction = FoundInstructionAt inputneeded; new_symbols = 0 }
+  | _ ->
+     { recovery_state with new_symbols = recovery_state.new_symbols - List.length (rhs production) + 1}
+
+let update_recovery_state_input recovery_state =
+  { recovery_state with new_symbols = recovery_state.new_symbols + 1 }
+
+let take_symbols n l =
+  if n > 0 then match l with
+    | [] -> l
+    | Jasmin.Location.{ pl_desc = Syntax.Concrete.NonTerminal { kind = Error } } as hd :: tl -> hd :: take n tl
+    | hd :: tl -> hd :: take (n-1) tl
+  else l
+
+let resume_on_error recovery_state cst extra_tokens lex =
+  match recovery_state.last_reduction with
+  | FoundInstructionAt (checkpoint, cst') ->
+     let extra_tokens', lex =
+       Lexer.lex_until_before (fun t -> t = SEMICOLON || t = RBRACE) lex
+     in
+     let (token,_,_), lex' = Lexer.next lex in
+     let lex =
+       if token = SEMICOLON then lex' else lex
+     in
+     let extra = List.rev_map (fun (v,startp,endp) -> Syntax.Concrete.make_terminal startp endp v) extra_tokens' in
+     let extra = List.rev_append extra_tokens extra in
+     let error_children = List.rev_append (take_symbols recovery_state.new_symbols cst) extra in
+     let error = Syntax.Concrete.(make_nonterminal Error error_children) in
+     let cst = error :: cst' in
+     let recovery_state = { recovery_state with new_symbols = 0 } in
+     lex, checkpoint, cst, recovery_state
+  | (FoundNothingAt (checkpoint, cst') | FoundTopAt (checkpoint, cst')) ->
+     let extra_tokens', lex = Lexer.lex_until_before
+        (function EOF | FN | (* SHARP | *) EXPORT | INLINE | PARAM | EXEC | REQUIRE | FROM (* TODO add pglobal *) -> true | _ -> false)
+        lex
+     in
+     let extra = List.rev_map (fun (v,startp,endp) -> Syntax.Concrete.make_terminal startp endp v) extra_tokens' in
+     let extra = List.rev_append extra_tokens extra in
+     let error_children = List.rev_append (take_symbols recovery_state.new_symbols cst) extra in
+     let error = Syntax.Concrete.(make_nonterminal Error error_children) in
+     let cst = error :: cst' in
+     let recovery_state = { recovery_state with new_symbols = 0 } in
+     lex, checkpoint, cst, recovery_state
+
+let extract_nonterminal symb =
+  match symb with
+  | I.(X T _) -> assert false
+  | I.(X N nt) -> Syntax.Concrete.X nt
+
+
+let rec show_green n g =
+  let open Syntax.Concrete in
+  match g.Jasmin.Location.pl_desc with
+  | Terminal token -> String.make n ' ' ^  show_token token
+  | NonTerminal { kind = Error; children } ->
+    String.make n ' ' ^  "ERROR\n" ^ String.concat "\n" (List.map (show_green (n+2)) children)
+  | NonTerminal { kind = X nt; children } ->
+    String.make n ' ' ^ Printers.print_nt nt ^ "\n" ^ String.concat "\n" (List.map (show_green (n+2)) children)
+
+let show_green g = show_green 0 g
+
+let show_tree node =
+  let open Syntax.Concrete in
+  let show_node x =
+    Format.sprintf "%s" (show_green x.green)
+  in
+  fold (fun acc x -> acc ^ " " ^ show_node x) "" node
+
+let rec loop lexer inputneeded cst recovery_state extra_tokens errors (checkpoint : 'a I.checkpoint) =
+  match checkpoint with
+  | I.InputNeeded _env ->
+      let (token, startp, endp as triple), lexer = Lexer.next lexer in
+      let extra_tokens = Syntax.Concrete.make_terminal startp endp token :: extra_tokens in
+      let recovery_state = update_recovery_state_input recovery_state in
+      loop lexer (checkpoint, cst) cst recovery_state extra_tokens errors (I.offer checkpoint triple)
+  | I.Shifting _ ->
+      let checkpoint = I.resume checkpoint in
+      let cst = List.append extra_tokens cst in
+      loop lexer inputneeded cst recovery_state [] errors checkpoint
+  | I.AboutToReduce (_env, production) ->
+      let n = List.length (rhs production) in
+      let nt = extract_nonterminal (lhs production) in
+      let cst = reduce_cst n nt cst [] in
+      let checkpoint = I.resume checkpoint in
+      loop lexer inputneeded cst (update_recovery_state_reduce inputneeded production recovery_state) extra_tokens errors checkpoint
+  | I.Rejected -> assert false
+  | I.HandlingError env ->
+    let lexer, after_error, cst, recovery_state = resume_on_error recovery_state cst extra_tokens lexer in
+    let error = positions env in
+    loop lexer inputneeded cst recovery_state [] (error::errors) after_error
+  | I.Accepted _v ->
+    begin match cst with
+    | [root] -> Syntax.Concrete.mk_root root, errors
+    | _ ->
+      List.iter (fun v -> Printf.eprintf "Non-unique root when accepting: %s\n" (show_green v)) cst;
+      assert false
+    end
+
+let program_cst ~fname (inc : Jasmin.Utils.IO.input) =
+  let ch = Jasmin.Utils.IO.to_input_channel inc in
+  let lexbuf = L.init fname (Lexing.from_channel ch) in
+  Lexer.initialize lexbuf;
+  let checkpoint = P.Incremental.module_ lexbuf.lex_curr_p in
+  let recovery_state = { last_reduction = FoundNothingAt (checkpoint, []); new_symbols = 0 } in
+  loop Lexer.start (checkpoint, []) [] recovery_state [] [] checkpoint
+
+let succeed v = v
+
+let fail buffer _checkpoint =
+  let (p1,p2) = E.last buffer in
+  let location = Jasmin.Location.make p1 p2 in
+  let message = "Parsing error" in
+  raise (Jasmin.Syntax.ParseError (location, Some message))
+
+let parse_program_from_tokens startp supplier =
+  let buffer, supplier = E.wrap_supplier supplier in
+  let checkpoint = P.Incremental.module_ startp in
+  I.loop_handle succeed (fail buffer) supplier checkpoint
+
+let pos_of_loc l =
+  let open Lexing in
+  let open Jasmin.Location in
+  let pos_fname = l.loc_fname in
+  let (pos_lnum_start, pos_char_start) = l.loc_start in
+  let (pos_lnum_end, pos_char_end) = l.loc_end in
+  let pos_bol_start = l.loc_bchar - pos_char_start in
+  let pos_bol_end = l.loc_echar - pos_char_end in
+  let startp = { pos_fname; pos_lnum = pos_lnum_start; pos_cnum = l.loc_bchar; pos_bol = pos_bol_start } in
+  let endp = { pos_fname; pos_lnum = pos_lnum_end; pos_cnum = l.loc_echar; pos_bol = pos_bol_end } in
+  (startp, endp)
+
+let tokens_of_cst cst =
+  Syntax.Concrete.fold_skip_errors (fun acc node -> match node.green.pl_desc with Terminal x -> let (startp,endp) = pos_of_loc node.green.pl_loc in (x, startp, endp) :: acc | _ -> acc) [] cst
+
+let dispenser_of_token_list l =
+  let d = Seq.to_dispenser (List.to_seq l) in
+  fun () -> Option.get (d ())
+
+let parse_program ~fname inc =
+  let cst, errors = program_cst ~fname inc in
+  let startp = Lexing.{
+    pos_fname = fname;
+    pos_lnum  = 1;
+    pos_bol   = 0;
+    pos_cnum  = 0
+  }
+  in
+  let tokens = List.rev (tokens_of_cst cst) in
+  cst, errors, parse_program_from_tokens startp (dispenser_of_token_list tokens)
\ No newline at end of file
diff --git a/parsing/parse.mli b/parsing/parse.mli
new file mode 100644
index 0000000..b097b7e
--- /dev/null
+++ b/parsing/parse.mli
@@ -0,0 +1,8 @@
+open Jasmin.Parser.MenhirInterpreter
+
+val string_of_symbol : xsymbol -> string
+
+val parse_program_from_tokens : Lexing.position -> (unit -> token * Lexing.position * Lexing.position) -> Jasmin.Syntax.pprogram
+val parse_program : fname:string -> Jasmin.Utils.IO.input -> Syntax.Concrete.node * (Lexing.position * Lexing.position) list * Jasmin.Syntax.pprogram
+
+val show_tree : Syntax.Concrete.node -> string
\ No newline at end of file
diff --git a/parsing/syntax.ml b/parsing/syntax.ml
new file mode 100644
index 0000000..84bd66f
--- /dev/null
+++ b/parsing/syntax.ml
@@ -0,0 +1,58 @@
+module Concrete = struct
+
+  type xnonterminal =
+    | X : 'a Jasmin.Parser.MenhirInterpreter.nonterminal -> xnonterminal
+    | Error : xnonterminal
+
+  type green_r =
+  | Terminal of Jasmin.Parser.token
+  | NonTerminal of {
+      kind : xnonterminal;
+      children : green list;
+    }
+
+  and green = green_r Jasmin.Location.located
+
+  type node = {
+    green: green;
+    top: node option; (* TODO can we express that this is not a leaf? *)
+  }
+
+  let node_children node =
+    let mk_child green =
+      { green; top = Some node; }
+    in
+    match node.green.pl_desc with
+    | Terminal _ -> []
+    | NonTerminal { children } ->
+      List.map mk_child children
+
+  let make_terminal start stop token = Jasmin.Location.(mk_loc @@ make start stop) (Terminal token)
+
+  let make_nonterminal kind children =
+    let rec last_stop = function
+    | [] -> assert false
+    | [x] -> x.Jasmin.Location.pl_loc
+    | _ :: tl -> last_stop tl
+    in
+    let start, stop = match children with
+    | [] -> Jasmin.Location._dummy, Jasmin.Location._dummy
+    | _ -> (List.hd children).Jasmin.Location.pl_loc, last_stop children
+    in
+    Jasmin.Location.(mk_loc @@ merge start stop) (NonTerminal { kind; children })
+
+  let rec fold f acc node =
+    let acc = f acc node in
+    List.fold_left (fold f) acc (node_children node)
+
+  let rec fold_skip_errors f acc node =
+    match node.green.pl_desc with
+    | NonTerminal { kind = Error } -> acc
+    | _ ->
+      let acc = f acc node in
+      List.fold_left (fold_skip_errors f) acc (node_children node)
+
+  let mk_root green =
+    { green; top = None }
+
+end
\ No newline at end of file
diff --git a/parsing/syntax.mli b/parsing/syntax.mli
new file mode 100644
index 0000000..96de430
--- /dev/null
+++ b/parsing/syntax.mli
@@ -0,0 +1,38 @@
+module Concrete :
+  sig
+
+    type xnonterminal =
+    | X : 'a Jasmin.Parser.MenhirInterpreter.nonterminal -> xnonterminal
+    | Error : xnonterminal
+
+    type green_r =
+    | Terminal of Jasmin.Parser.token
+    | NonTerminal of {
+        kind : xnonterminal;
+        children : green list;
+      }
+
+    and green = green_r Jasmin.Location.located
+
+    type node = {
+      green: green;
+      top: node option;
+    }
+
+    val make_terminal :
+      Lexing.position -> Lexing.position -> Jasmin.Parser.token -> green
+
+    val make_nonterminal :
+      xnonterminal -> green list -> green
+
+    val fold : ('a -> node -> 'a) -> 'a -> node -> 'a
+
+    val fold_skip_errors : ('a -> node -> 'a) -> 'a -> node -> 'a
+
+    val mk_root : green -> node
+
+    (*
+    val show_tree : node -> string
+    *)
+
+  end
diff --git a/tests/diagnostics.ml b/tests/diagnostics.ml
new file mode 100644
index 0000000..ef4b2ca
--- /dev/null
+++ b/tests/diagnostics.ml
@@ -0,0 +1,74 @@
+open Base
+open Controller
+open Language
+open Lsp
+open Jasminlsp
+
+let uri = Uri.of_path "test_file.jazz"
+let fname = "test_file.jazz"
+let architecture = Jasmin.Glob_options.X86_64
+
+let %test_unit "diagnostics: parsing error is detected" =
+  let text = "fn foo(reg u64 bar) -> reg u64 { reg u4 r; return r; }" in
+  let doc = DocumentManager.init ~fname ~text in
+  let parse_diags = DocumentManager.parsing_diagnostics doc in
+  [%test_eq: int] (List.length parse_diags) 1
+
+let %test_unit "diagnostics: typing error is detected" =
+  let text = "fn foo(reg u64 bar) -> reg u32 { reg u64 r; return r; }" in
+  let doc = DocumentManager.init ~fname ~text in
+  let fname' = fname in
+  let get_ast ~fname = if String.equal fname fname' then DocumentManager.get_ast doc else None in
+  let result = Typing.type_program get_ast architecture ~fname in
+  let diags = PathMap.find_opt fname result.diagnostics in
+  [%test_eq: int option] (Option.map diags ~f:List.length) (Some 1)
+
+let %test_unit "diagnostics: errors are combined correctly" =
+  let text = "fn foo(reg u64 bar) -> reg u32 { reg u64 r; reg baz; return r; }" in
+  let workspace = ref Workspace.empty_workspace in
+  for _i = 1 to 2 do
+  workspace := Workspace.open_document !workspace ~fname ~text;
+  workspace := Workspace.analyze_file fname Jasmin.Glob_options.X86_64 !workspace;
+  let diags = Workspace.get_diagnostics !workspace in
+  [%test_eq: int] (List.length (PathMap.bindings diags)) 1;
+  let diags = PathMap.find_opt fname diags in
+  [%test_eq: int option] (Option.map diags ~f:List.length) (Some 2)
+  done
+
+let %test_unit "diagnostics: parsing errors are resolved correctly" =
+  let text = "fn foo(reg u64 bar) -> reg u32 { reg u64 r; reg baz; return r; }" in
+  let workspace = Workspace.empty_workspace in
+  let workspace = Workspace.open_document workspace ~fname ~text in
+  let workspace = Workspace.analyze_file fname Jasmin.Glob_options.X86_64 workspace in
+  let text = "fn foo(reg u64 bar) -> reg u32 { reg u64 r; reg u64 baz; return r; }" in
+  let workspace = Workspace.open_document workspace ~fname ~text in
+  let diags = Workspace.get_diagnostics workspace in
+  [%test_eq: int] (List.length (PathMap.bindings diags)) 1;
+  let diags = PathMap.find_opt fname diags in
+  [%test_eq: int option] (Option.map diags ~f:List.length) (Some 1)
+
+let %test_unit "diagnostics: typing errors are resolved correctly" =
+  let text = "fn foo(reg u64 bar) -> reg u32 { reg u64 r; reg baz; return r; }" in
+  let workspace = Workspace.empty_workspace in
+  let workspace = Workspace.open_document workspace ~fname ~text in
+  let text = "fn foo(reg u64 bar) -> reg u64 { reg u64 r; reg baz; return r; }" in
+  let workspace = Workspace.analyze_file fname Jasmin.Glob_options.X86_64 workspace in
+  let workspace = Workspace.open_document workspace ~fname ~text in
+  let workspace = Workspace.analyze_file fname Jasmin.Glob_options.X86_64 workspace in
+  let diags = Workspace.get_diagnostics workspace in
+  [%test_eq: int] (List.length (PathMap.bindings diags)) 1;
+  let diags = PathMap.find_opt fname diags in
+  [%test_eq: int option] (Option.map diags ~f:List.length) (Some 1)
+
+let %test_unit "diagnostics: all errors are resolved correctly" =
+  let text = "fn foo(reg u64 bar) -> reg u32 { reg u64 r; reg baz; return r; }" in
+  let workspace = Workspace.empty_workspace in
+  let workspace = Workspace.open_document workspace ~fname ~text in
+  let workspace = Workspace.analyze_file fname Jasmin.Glob_options.X86_64 workspace in
+  let text = "fn foo(reg u64 bar) -> reg u64 { reg u64 r; reg u64 baz; return r; }" in
+  let workspace = Workspace.open_document workspace ~fname ~text in
+  let workspace = Workspace.analyze_file fname Jasmin.Glob_options.X86_64 workspace in
+  let diags = Workspace.get_diagnostics workspace in
+  [%test_eq: int] (List.length (PathMap.bindings diags)) 1;
+  let diags = PathMap.find_opt fname diags in
+  [%test_eq: int option] (Option.map diags ~f:List.length) (Some 0)
\ No newline at end of file
diff --git a/tests/dune b/tests/dune
new file mode 100644
index 0000000..cee47e3
--- /dev/null
+++ b/tests/dune
@@ -0,0 +1,7 @@
+(library
+  (name tests)
+  (flags (:standard -rectypes))
+  (libraries controller)
+  (preprocess
+    (pps ppx_sexp_conv ppx_inline_test ppx_assert))
+  (inline_tests))