fix 'missing' errors

tamarin-prover · Jun 25, 2024 · 68bc845 · 68bc845
1 parent 0c146ad
commit 68bc845
Show file tree

Hide file tree

Showing 5 changed files with 82 additions and 23 deletions.
diff --git a/.gitignore b/.gitignore
@@ -16,4 +16,5 @@ run.sh
 
 .gitignore
 
-*.antlr
+*.antlr
+./src/grammar/syntax_error.ts
diff --git a/language-configuration.json b/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": [

diff --git a/src/extension.ts b/src/extension.ts
@@ -3,8 +3,9 @@ import * as child_process from 'child_process';
 import path = require('path');
 import { runShortcut } from './features/run_shortcut';
 import * as syntax_error from './features/syntax_error';
-import { LanguageClient } from 'vscode-languageclient/node';
-import { startLanguageServer } from './languageServer';
+
+
+
 
 function getTerminal(name: string = "serverTamarin") {
     let target = undefined;
@@ -22,6 +23,12 @@ function getTerminal(name: string = "serverTamarin") {
     return target;
 }
 
+function plugin_features(context : vscode.ExtensionContext){
+   runShortcut(context);
+   syntax_error.display_syntax_errors(context);
+
+}
+
 
 
 export function activate(context: vscode.ExtensionContext) {
@@ -135,13 +142,13 @@ export function activate(context: vscode.ExtensionContext) {
 
     });
 
-    runShortcut(context);
-   syntax_error.display_errors(context);
+    //Fonctionnalités du plugin 
+    plugin_features(context)
+
 
     context.subscriptions.push(checkSyntaxCommand);
     context.subscriptions.push(checkSemanticsCommand);
     context.subscriptions.push(runServerCommand);
     context.subscriptions.push(runConsoleProofCommand);
-    //startLanguageServer(context);
 
 }
diff --git a/src/features/syntax_error.ts b/src/features/syntax_error.ts
@@ -1,13 +1,29 @@
 import * as vscode from 'vscode'
-import {  QueryMatch, QueryCapture } from 'web-tree-sitter';
 import Parser =require( "web-tree-sitter");
 
 
 let diagnostics = vscode.languages.createDiagnosticCollection('Tamarin');
 
-async function detect_errors(context: vscode.ExtensionContext): Promise<void> {
+
+
+function get_child_index(node : Parser.SyntaxNode): number|null{
+    if(node.parent === null ){
+        return null;
+    }
+    const children = node.parent.children;
+    for (let i = 0; i < children.length; i++) {
+      if (children[i].id === node.id) {
+        return i >= 0 ? i : null;
+      }
+    }
+    return 0;
+
+}
+
+
+
+async function detect_errors(): Promise<void> {
     let editor = vscode.window.activeTextEditor;
-    //const parser = createParser();
     await Parser.init();
     const parser = new Parser();
     const Tamarin =   await Parser.Language.load('/Users/hugo/Documents/Telecom Nancy/2A/Stage/vscode-tamarin/src/grammar/parser-tamarin.wasm');
@@ -19,15 +35,50 @@ async function detect_errors(context: vscode.ExtensionContext): Promise<void> {
     let text = editor.document.getText();
     const tree =  parser.parse(text);
 
+    function build_error_display(node : Parser.SyntaxNode, editeur: vscode.TextEditor, message : string){
+        let start = node.startIndex;
+        let end = node.endIndex;
+        let positionStart = editeur.document.positionAt(start);
+        let positionEnd = editeur.document.positionAt(end);
+        let existingDiag = diags.find(d => d.range.contains(positionStart)); // Evite les superpositions de diagnostics
+        if (!existingDiag) {
+        diags.push(new vscode.Diagnostic(new vscode.Range(positionStart, positionStart.translate(0,0) ), message, vscode.DiagnosticSeverity.Error));
+        }
+    }
+
     function findMatches(node : Parser.SyntaxNode, editeur: vscode.TextEditor ) {
-        if ((node.toString().includes('MISSING') && node.childCount === 0)  || (node.toString().includes('ERROR') )) {
-            let start = node.startIndex;
-            let end = node.endIndex;
-            let position = editeur.document.positionAt(start);
-            let existingDiag = diags.find(d => d.range.contains(position));
-            let message = node.toString().slice(1,-1)
-            if (!existingDiag) {
-            diags.push(new vscode.Diagnostic(new vscode.Range(position, position.translate(0,0)), message, vscode.DiagnosticSeverity.Error));
+        if ((node.isMissing)) {
+            let myId = get_child_index(node);
+            if(myId === null){
+                return ;
+            }
+            if(node.parent?.child(myId-1)?.type === 'single_comment'){
+                let start ;
+                if(node.parent.child(myId-2) != null ){
+                    start = node.parent.child(myId-2)?.endIndex;
+                }
+                else {
+                    start = 0
+                }
+                let positionStart = editeur.document.positionAt(start?? 0);
+                let existingDiag = diags.find(d => d.range.contains(positionStart)); // Evite les superpositions de diagnostics
+                if (!existingDiag) {
+                    diags.push(new vscode.Diagnostic(new vscode.Range(positionStart, positionStart.translate(0,0) ), node.toString().slice(1, -1), vscode.DiagnosticSeverity.Error));
+                }
+            }
+            else {
+            build_error_display(node, editeur ,node.toString().slice(1,-1));
+            }
+        }
+        else if ( node.toString().includes('ERROR')){
+            if(node.toString().includes('built_in') && node.childCount === 1){
+                build_error_display(node, editeur, 'Incorrect built-in function name maybe "," is missing');
+            }
+           /* else if (node.parent?.toString().includes('function_identifier')){
+                build_error_display(node, editeur, 'Incorrect function definition')
+            }*/
+            else{
+                build_error_display(node, editeur ,node.toString().slice(1,-1));
             }
         }
         for (let child of node.children) {
@@ -44,15 +95,15 @@ async function detect_errors(context: vscode.ExtensionContext): Promise<void> {
 
 }
 
-export function display_errors(context: vscode.ExtensionContext) {
+export function display_syntax_errors(context: vscode.ExtensionContext) {
     let editor = vscode.window.activeTextEditor;
     if (editor) {
         let changed_content = vscode.workspace.onDidChangeTextDocument((event) => {
             if (event.document === editor.document) {
-                detect_errors(context);
+                detect_errors();
             }
         });
-        detect_errors(context);
+        detect_errors();
         context.subscriptions.push(changed_content, diagnostics);
     }
 }

diff --git a/syntaxes/tamarin.tmLanguage.json b/syntaxes/tamarin.tmLanguage.json
@@ -15,11 +15,11 @@
       "name": "comment.line"
     },
     {
-      "match": "\\b(equations|builtins|functions|protocol|property|begin|end|subsection|section|text|pb|lts|exists-trace|all-traces|enable|assertions|modulo|default_rules|anb-proto|in|let|Fresh|fresh|Public|public)\\b",
+      "match": "\\b(equations|functions|protocol|property|begin|end|subsection|section|text|pb|lts|exists-trace|all-traces|enable|assertions|modulo|default_rules|anb-proto|in|let|Fresh|fresh|Public|public)\b",
       "name": "keyword.control"
     },
     {
-      "match": "\\b(axiom|builtins|protocol|property|subsection|section|text)\\b",
+      "match": "\\b(axiom|builtins|protocol|property|subsection|section|text|functions|tactic|macros)\\b",
       "name": "keyword.control"
     },
     {
-Original file line number
+Diff line change
@@ Expand Up / @@ -16,4 +16,5 @@ run.sh @@
     .gitignore
-    *.antlr
+    *.antlr
+    ./src/grammar/syntax_error.ts