Recursive analysis

.github/workflows/ci.yml

@@ -2,9 +2,9 @@ name: Tamarin Prover LSP CI
 
 on:
   push:
-    branches: [ "main" ]
+    branches: [ "master" ]
   pull_request:
-    branches: [ "main" ]
+    branches: [ "master"]
   workflow_dispatch:
 
 jobs:

CHANGELOG.md

@@ -1,5 +1,13 @@
+
 # Change Log
-## V1.2.0
+## V2.1.0
+Recursive Analysis has been implemented.
+- Symbols imported from other Tamarin files are no longer reported as errors.
+- Syntax highlighting has been updated
+- Few wellformedness Checks has been updated as well of a few tests
+- 2 new unitary tests to test wellformedness checks with symbols imported from another file.
+- .splib parsing has been added , now imported files must be .splib
+## V2.0.0
 ### Language Server Protocol
 Lsp has been fully implemented : This includes
 - Redesign of plugin's structure

CONTRIBUTE.md

@@ -9,7 +9,7 @@ How to start using the git repository:
 - Press Ctrl+Shift+B To compile the plugin
 - Press Ctrl+Shift+D , click on the green arrow "Run Client" in the top left-hand corner
 - Then in the test window open a Tamarin document (.spthy) and test the code. (There is no need to uninstal tamarin-prover official VsCode extension)
-- You can see debug logs in the output section , selecting "Tamarin Language Server" instead of tasks at the right.
-
+- You can see debug logs in the output section of the terminal , selecting "Tamarin Language Server" instead of tasks at the right.
+- Run ` npm clean` to remove all packages and compiled files.
 
 More documentation is located in Documentation folder.

Documentation/Overview.md

@@ -5,6 +5,7 @@ At the root of the project there are several .json files:
 - ```package.json```: This file contains basic informations about the extension (name, version, ...), defines the type of file extension the plugin can be used with, allows you to define custom commands and associate keyboard shortcuts ("keybindings") or add actions for menus or right-clicks. Finally, it can be used to indicate executable scripts and specify dependencies. The package-lock.json file is automatically generated by executing the ``npm build`` command.
 - ```language-configuration.json```: This allows you to define snippets to make coding more enjoyable.
 - ``/syntaxes/tamarin.tmLanguage.json``: This file defines the syntax highlighting of code with the help of TextMate.
+- ``` .github/workflows``` : this file setups the pipeline. 
 
 ### Miscellaneous files
 -  ```jest.config.js``` : This file contains basic informations to run the tests.
@@ -27,4 +28,10 @@ The server folder is separated into various parts required for plugin operation.
 ### Client folder
 - ``src/extension.ts``: This is the file used to launch the extension. It contains the ``activate`` function, which contains all the tasks performed when the plugin is activated.
 -  ```src/run_shortcut.ts```: This file provides a shortcut to launch tamarin in normal or auto sources mode in the bottom right-hand corner of the editor.
-- ```src/languageServer.ts``` : This file setup the lsp.
+- ```src/languageServer.ts``` : This file setup the lsp.
+
+## spthy and splib files.
+- This plugin supports two file types:
+    - spthy is the default format for Tamarin files.
+    - splib files are library files that do not contain the theory name, "begin" and "end". They can be imported using ``` include "file.splib"```.
+- Non spthy or splib files that are labeled as Tamarin files are considered as spthy files , unless they are imported and considered instead as splib files.

Documentation/Parser.md

@@ -1,7 +1,8 @@
 # Using tree-sitter in the Tamarin plugin
-
-First you will need to go to server/grammar/tree-sitter-tamarin folder.
-```cd server/grammar/tree-sitter-tamarin```
+First you will need to go to server/grammar/ folder
+```cd server/grammar/```
+There is two parsers. One for .spthy files and one for .splib files
+Those two parsers uses common_grammar.js.
 
 ## Installing dependencies
 ### On macOS
@@ -18,12 +19,12 @@ These commands are necessary to build the parser.
 ## Updating the grammar
 This plugin uses [tamarin's grammar](https://github.com/tamarin-prover/tamarin-prover/blob/develop/tree-sitter/tree-sitter-spthy/grammar.js)
 This grammar might be outdated compared to the tamarin's newest grammar, missing new functionalities.
+In order to update the grammar , you must change the content of common_grammar.js file in server/grammar/ folder to the current one (copy paste it and remove any rule that is present in spthy and splib grammars).
 
-In order to update the grammar , you must change the content of grammar.js file in server/grammar/tree-sitter-tamarin folder to the current one (copy paste it).
-
-Then , do the following commands.
+Then , do the following commands for spthy and splib.
 ```tree-sitter generate``` This command creates all the files needed to use the grammar with Typescript
 ```tree-sitter build-wasm``` This command creates a dynamic .wasm library which enables you to use the parser inside the vscode plugin (server/grammar/tree-sitter-tamarin/tree-sitter-spthy.wasm).
+Finally, move both parsers into server/grammar/tree-sitter-tamarin folder
 
 ### Things you must consider when updating the grammar
 Updating the grammar may take the symbol table and textmate grammar obsolete, be careful.

README.md

@@ -21,8 +21,11 @@ Features:
     - Provides a quick fix for function names (suggestions based on editing distance).
     - Checks wether built-ins are imported when encountering corresponding functions or symbols (provides a quick fix to import the right built-in).
     This is a subset of the checks performed by Tamarin. For more details on Tamarin's wellformedness checks, see the corresponding [Tamarin Prover manual section](https://tamarin-prover.com/manual/master/book/010_modeling-issues.html).
-- Implements Language Server Protocol
-- Adds 62 unitary tests 
+- Supports two file types:
+    - spthy is the default format for Tamarin files.
+    - splib files are library files that do not contain the theory name, "begin" and "end". They can be imported using ``` include "file.splib"```.
+- Supports recursive analysis, ie, included files are taken into account for wellformedness checks .
 
 - Use right click and ```Rename``` on an indentifier to rename all occurences of it inside a rule or a lemma.
 - Use right click and ```Search Definition``` on facts or function names and press ```CTRL```+```ALT```+```n``` to navigate through all occurences.
+

client/package.json

@@ -1,7 +1,7 @@
 {
 	"name": "tamarin-prover-vscode-client",
 	"license": "MIT",
-	"version": "1.1.6",
+	"version": "2.1.0",
 	"repository": {
 		"type": "git",
 		"url": "https://github.com/tamarin-prover/vscode-tamarin.git"

client/src/languageServer.ts

@@ -14,14 +14,18 @@ export const startLanguageServer= async(context: ExtensionContext) =>{
 		run: { module: serverModule, transport: TransportKind.ipc },
 		debug: { module: serverModule, transport: TransportKind.ipc }
 	};
-    const parserPath = context.asAbsolutePath(
+    const SpthyParserPath = context.asAbsolutePath(
         path.join('server', 'out', 'grammar', 'tree-sitter-tamarin', 'tree-sitter-spthy.wasm')
     );
+    const SplibParserPath = context.asAbsolutePath(
+        path.join('server', 'out', 'grammar', 'tree-sitter-tamarin', 'tree-sitter-splib.wasm')
+    );
     const clientOptions: LanguageClientOptions = {
         documentSelector: [{scheme: 'file', language: 'tamarin'}],
         outputChannelName: 'Tamarin Language Server',
         initializationOptions: {
-            parserPath: parserPath
+            SpthyParserPath: SpthyParserPath,
+            SplibParserPath: SplibParserPath
         }
     }
     client = new LanguageClient(