infix operators and readme release

Contribute/Readme_release.md

@@ -0,0 +1,23 @@
+## Documentation on how to release the extension 
+
+The plugin is available on two different websites :
+ - https://marketplace.visualstudio.com/items?itemName=tamarin-prover.tamarin-prover
+
+ - https://open-vsx.org/extension/tamarin-prover/tamarin-prover
+
+
+ For each website you will need an access token in order to publish the extension. This you can create using you azure dev ops account as described here :
+ \
+  https://code.visualstudio.com/api/working-with-extensions/publishing-extension
+ \
+ or your Eclipse account as described here : https://github.com/eclipse/openvsx/wiki/Publishing-Extensions
+\
+For vscode the access token is required before publishing using ```vsce login private_access_token```.
+
+In order to push a new version or release you will need to use the following commands : 
+```vsce publish version_n°``` for vscode and ```npx ovsx publish -p private_access_token``` for openVSX
+
+Make sure to remove all the errors otherwise it won't publish. The error messages are quite clear to help you debug. For vscode you can specify in the ```package.json``` file the files you want to include in the extension. Make sure everything necessary to run your code is present. 
+
+
+

package.json

@@ -180,8 +180,11 @@
     "binding.gyp",
     "prebuilds/**",
     "bindings/node/*",
-    "src/**",
-    "syntaxes/**",
+    "src/features/**",
+    "src/grammar/parser-tamarin.wasm",
+    "src/features/**",
+    "src/extension.ts",
+    "syntaxes/tamarin.tmLanguage.json",
     "out/**",
     "LICENSE",
     "package.json",

src/features/rename.ts

@@ -23,7 +23,7 @@ async function replace_symbol(symbol : TamarinSymbol, editor : vscode.TextEditor
   const newNameLength = newName.length;
   const newRange = new vscode.Range(
     range.start,
-    editor.document.positionAt(editor.document.offsetAt(range.start) + newNameLength)
+    editor.document.positionAt(editor.document.offsetAt(range.start) + newNameLength - oldNameLength)
   );
   const edit = new vscode.WorkspaceEdit();
   edit.replace(editor.document.uri, range, newText);

src/features/syntax_errors.ts

@@ -192,6 +192,7 @@ export function display_syntax_errors(context: vscode.ExtensionContext): void {
                         throw new Error('Could not determine file name');
                     }  
                     symbolTables.set(fileName, table);
+                    console.log(symbolTables)   // pour regarder le contenu de la table pour débugger
                 }
             }
         });

src/features/wellformedness_checks.ts

@@ -432,7 +432,8 @@ function check_free_term_in_lemma(symbol_table : TamarinSymbolTable, editor: vsc
                     gt_list = get_child_grammar_type(search_context);
                     } 
                 }
-                if(search_context.grammarType === DeclarationType.Lemma || search_context.grammarType === DeclarationType.Restriction){
+                // En même temps on définit le contexte pour le rename 
+                if(search_context.grammarType === DeclarationType.Lemma || search_context.grammarType === DeclarationType.Restriction || search_context.grammarType === 'diff_lemma'){
                     set_associated_qf(lemma_vars[i], search_context.child(4));
                 }
                 else if(search_context.grammarType === DeclarationType.NF){
@@ -479,6 +480,49 @@ function check_macro_not_in_equation(symbol_table : TamarinSymbolTable, editor:
 }
 
 
+function return_builtins(symbol_table: TamarinSymbolTable): string[]{
+let builtins : string[]  = [];
+    for (let symbol of symbol_table.getSymbols()){
+        if(symbol.declaration === DeclarationType.Builtin){
+            if(symbol.name)
+            builtins.push(symbol.name);
+        }
+    } 
+    return builtins;
+}
+
+function check_infix_operators(symbol_table : TamarinSymbolTable, editor : vscode.TextEditor, diags : vscode.Diagnostic[], root : Parser.SyntaxNode){
+
+    function display_infix_error(builtin : string, symbol : string, child : Parser.SyntaxNode):void {
+        let current_builtins = return_builtins(symbol_table);
+            if(! current_builtins.includes(builtin)){
+                build_error_display(child, editor, diags, "Error : symbol "+ symbol +" cannot be used without "+ builtin +" builtin")
+            }
+    }
+
+    for (let child of root.children){
+        if(child.grammarType === '^' || child.grammarType === '*'){
+            let current_builtins = return_builtins(symbol_table);
+            if(! current_builtins.includes('diffie-hellman')){
+                build_error_display(child, editor, diags, "Error : symbols ^ or * cannot be used without diffie-hellman builtin")
+            }
+        }
+        else if (child.grammarType === '⊕'){
+            display_infix_error('xor','⊕', child);
+        }
+        else if (child.grammarType === '++'){
+            display_infix_error('multiset', '++', child);
+        }
+        else if (child.grammarType === '%+'){
+            display_infix_error('natural-numbers', '%+', child)
+        }
+        else (check_infix_operators(symbol_table,editor,diags,child));
+    }
+
+
+}
+
+
 
 const fixMap = new Map<vscode.Diagnostic, vscode.CodeAction>();
 
@@ -496,12 +540,13 @@ vscode.languages.registerCodeActionsProvider('tamarin', {
 });
 
 
-export function checks_with_table(symbol_table : TamarinSymbolTable, editor: vscode.TextEditor, diags: vscode.Diagnostic[]){
+export function checks_with_table(symbol_table : TamarinSymbolTable, editor: vscode.TextEditor, diags: vscode.Diagnostic[], root : Parser.SyntaxNode){
     check_variables_type_is_consistent_inside_a_rule(symbol_table, editor, diags);
     check_case_sensitivity(symbol_table, editor, diags);
     check_variable_is_defined_in_premise(symbol_table, editor, diags);
     check_action_fact(symbol_table, editor, diags);
     check_function_macros_and_facts_arity(symbol_table, editor, diags);
     check_free_term_in_lemma(symbol_table, editor, diags);
     check_macro_not_in_equation(symbol_table, editor, diags)
+    check_infix_operators(symbol_table, editor, diags, root);
 };

src/symbol_table/create_symbol_table.ts

@@ -14,7 +14,7 @@ export const createSymbolTable = (root : Parser.SyntaxNode, editor :vscode.TextE
     const symbolTableVisitor = new SymbolTableVisitor();
     let symbolTable = symbolTableVisitor.visit(root, editor, diags);
     convert_linear_facts(symbolTable);
-    checks_with_table(symbolTable, editor, diags)
+    checks_with_table(symbolTable, editor, diags, root)
     diagCollection.set(editor.document.uri, diags)
     return {symbolTable};
 };