Merge pull request #1 from hugotvn/master

Improved Vscode extension using Tree-sitter grammar.

.gitignore

@@ -14,4 +14,7 @@ out/
 
 run.sh
 
-.gitignore
+.gitignore
+
+*.antlr
+./src/grammar/syntax_error.ts

.vscode/launch.json

@@ -11,10 +11,10 @@
 			"request": "launch",
 			"runtimeExecutable": "${execPath}",
 			"args": [
-				"--extensionDevelopmentPath=${workspaceFolder}"
+				"--extensionDevelopmentPath=${workspaceRoot}"
 			],
 			"outFiles": [
-				"${workspaceFolder}/out/**/*.js"
+				"${workspaceRoot}/out/**/*.js"
 			],
 			"preLaunchTask": "${defaultBuildTask}"
 		},

CHANGELOG.md

@@ -1,11 +1,20 @@
 # Change Log
 
-## [0.0.3]
+## V1.0.0
+Initial release after fork from giclu-3.
 
-- Added support for marketplaces
+### Features:
 
-## [0.0.2]
+- Enhances giclu-3's syntax highlighting.
+- Adds comprehensive syntax error detection based on the grammar with ```MISSING``` or ```ERROR``` messages.
+- Provides various wellformedness checks:
+    - Checks position and usage of reserved facts (```Fr```, ```Out```, ```In```, ```K```, ```KD```, ```KU```).
+    - Checks whether variable are used consistly inside a rule, i.e., using the same capitalization and sort.
+    - Spellcheck on facts (must start with an uppercase letter).
+    - Checks whether all variables in the conclusion of a rule appear in the premises (except public variables).
+    - Checks the arity of facts and functions.
+    - Checks whether a lemma uses free terms.
+    - Checks whether all facts in the premises of the rules appear in the conclusion of some (other) rule (provides a quick fix by using the closest exisiting fact, based on editing distance).
 
-### Added
-
-- Initial version
+- 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```+```TAB``` to navigate through all occurences.

Contribute/README_TREE_SITTER.md

@@ -0,0 +1,37 @@
+ Using tree-sitter in the Tamarin plugin
+
+### Importing the grammar 
+All the files required to use the grammar in the plugin are located in src/grammar/tree-sitter-tamarin.
+
+To use tree-sitter with a new grammar, use the ```tree-sitter generate``` command.
+\
+ ⚠️ this command creates all the files needed to use the grammar with Typescript, for example grammar.js, as well as json and C files. In particular, the parser is created.
+
+### Importing the parser
+Then, to use the parser inside the vscode plugin, use: 
+\
+```tree-sitter build --wasm --output location_of_the_output```
+\
+To perform this command you need to have docker running or install the other applications suggested on tree sitter website:
+\
+ https://tree-sitter.github.io/tree-sitter/creating-parsers#command-build
+\
+This command creates a dynamic .wasm library which enables you to use the parser inside the vscode plugin.
+
+### Using the parser  
+There are many ways to create an instance of the parser using a new grammar. Here we use the following approach: 
+\
+```Typescript 
+import Parser =require( "web-tree-sitter");
+```
+\
+And then inside a function :
+
+```Typescript
+await Parser.init();
+const parser = new Parser();
+const Tamarin =   await Parser.Language.load('/absolute_path_to_wasm_file');
+parser.setLanguage(Tamarin);
+```
+
+

Contribute/Readme_dev.md

@@ -0,0 +1,66 @@
+# Organization of the plugin's git source repository
+
+ ### .json files
+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.
+
+<br>
+
+- ```language-configuration.json```: This allows you to define snippets to make coding more enjoyable.
+
+<br>
+
+- ``/syntaxes/tamarin.tmLanguage.json``: This file defines the syntax highlighting of code with the help of TextMate.
+
+## src folder
+
+The src folder is separated into various parts required for plugin operation.
+
+- ``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.
+
+<br>
+
+- ```grammar```: This folder contains the files needed to use a Tree-sitter grammar inside the plugin. Its use is detailed in the ``README_TREE_SITTER.md`` file.
+
+
+<br>
+
+- ``symbol_table``: contains a file used to create a symbol table for each open Tamarin file in the editor. The symbol table contains ```TamarinSymbol```,  each symbol is associated with:
+
+
+
+   - A tree node corresponding to the symbol itself, a type, another node corresponding to the context in which this symbol appears (rule, lemma, formula in a lemma), a name and associated range in the tamarin file, an arity if it's a fact or a function, a type if it's a variable (public, fresh ...), and a ``quantified_formula`` node for variables in lemmas.
+
+  <br>
+
+  - The various useful node types are listed in the ``DeclarationType`` enumeration.
+
+<br>
+
+- ```features```: Contains all the functionalities
+offered by the plugin .
+
+
+
+  - ```syntax_error.ts``` is the only file that will parse files that are opened in the vscode editor. Files are re-parsed as soon as they are modified. It also detects semantic errors and initiates creation of a symbol table for each file.
+
+  <br>
+
+  - ```run_shortcut.ts``` file provides a shortcut to launch tamarin in normal or auto sources mode in the bottom right-hand corner of the editor.
+
+  <br>
+
+  - ``welformedness_checks.ts`` This file contains all semantic checks based on the symbol table.
+
+  <br>
+
+  - ``rename.ts`` file contains the rename function, which is performed by right-clicking on a token. Variables with the same name in a rule are all renamed, and variables with the same name and quantifier in lemmas are renamed.
+
+  <br>
+
+   - ``go_to.ts`` file contains functionality to go to the function definition and navigate between the occurrences of a fact.
+
+<br>
+
+- ```test```: Contains files used to test the tree structure.

README.md

@@ -1,7 +1,23 @@
-# Tamarin Prover Extension for VSCode
+# Tamarin Visual Studio Code extension
 
-An extension for highlighting tamarin-prover syntax.
+A Visual Studio Code extension for Tamarin files (.spthy) based on [giclu-3's extension](https://github.com/gilcu3/vscode-tamarin) and using [Tamarin's tree-sitter grammar](https://github.com/tamarin-prover/tamarin-prover/pull/648).
 
-Also include some snippets to smooth developing
+![Example](./images/error.png)
 
-see <http://tamarin-prover.github.io/>
+Features:
+
+- Enhances giclu-3's syntax highlighting.
+- Adds comprehensive syntax error detection based on the grammar with ```MISSING``` or ```ERROR``` messages.
+- Provides various wellformedness checks:
+    - Checks position and usage of reserved facts (```Fr```, ```Out```, ```In```, ```K```, ```KD```, ```KU```).
+    - Checks whether variable are used consistly inside a rule, i.e., using the same capitalization and sort.
+    - Spellcheck on facts (must start with an uppercase letter).
+    - Checks whether all variables in the conclusion of a rule appear in the premises (except public variables).
+    - Checks the arity of facts and functions.
+    - Checks whether a lemma uses free terms.
+    - Checks whether all facts in the premises of the rules appear in the conclusion of some (other) rule (provides a quick fix by using the closest exisiting fact, based on editing distance).
+
+    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).
+
+- 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```+```TAB``` to navigate through all occurences.

language-configuration.json

@@ -11,7 +11,7 @@
         { "open": "'", "close": "'", "notIn": ["string", "comment"] },
         { "open": "\"", "close": "\"", "notIn": ["string"] },
         { "open": "`", "close": "`", "notIn": ["string", "comment"] },
-        { "open": "/**", "close": " */", "notIn": ["string"] }
+        { "open": "/*", "close": " */", "notIn": ["string"] }
     ],
     "autoCloseBefore": ";:.,=}])>` \n\t",
     "surroundingPairs": [
@@ -20,7 +20,8 @@
         ["(", ")"],
         ["'", "'"],
         ["\"", "\""],
-        ["`", "`"]
+        ["`", "`"],
+        ["<", ">"]
     ],
     "folding": {
         "markers": {