externalize lsp

.gitignore

@@ -1 +1,6 @@
 node_modules
+src/*.interp
+src/*.tokens
+src/.antlr/
+out/
+dist/

CHANGELOG.md

@@ -0,0 +1,25 @@
+# Change Log
+All notable changes to the "jml-vscode" extension will be documented in this file.
+
+## Changelog
+
+* **0.3.0** (upcoming-2022)
+  - Changing to `SemanticTokenProvider` interface to highlight JML annotation texts inside Java files. 
+    There is no text mate grammar anymore. 
+
+  - Language Server added on the basis of the [jmlparser
+    project](https://github.com/wadoon/jmlparser).
+
+  - Simple support for KeY files
+
+    Syntax highlighting and snippets.
+
+* **0.2.0** (04.04.2019)
+  - Fixes by @csicar
+
+* **0.1.0** (14.02.2019)
+  - First release
+  - ADDED support for some jml clauses and backslash keywords. 
+
+* **0.0.0** (unpublished)
+  - Start with the `java` language definition of VS Code.

examples/Example.java

@@ -8,21 +8,11 @@ public class Example {
     public int foo = 2;
 
     /*@
-    public model_behavior test :
-    requires true;
+    model_behavior
+    requires req1 : true;
     ensures true;
     assignable \nothing;
     public model int bar(int a);
     */
-
-
-    /*@
-    public behavior my_contract: 
-        requires (\exists int i; a*b == i*2);
-        ensures \result >= 2;
-    */
-    public void baz(int a, int b) {
-        //@ assert true;
-    }
 }
 

examples/firstOrderRules.key

@@ -0,0 +1,247 @@
+// This file contains quantifier and equality rules which used to be in genericRules.key
+
+\sorts {
+    \generic G, S1, S2, H;
+}
+
+\schemaVariables {
+    \term G e, s, t, e0;
+    \term H t1;
+    \term S1 t2;
+    \skolemTerm G sk;
+    \formula b, c;
+    \variables G u, e2;
+
+    \term G commEqLeft;
+    \term H commEqRight;
+
+    \term [rigid] G sr;
+    \term [rigid] H tr;
+
+    \term S1 ind1, ind2, target;
+}
+
+\rules {
+
+    // Gamma rules
+    allLeft {
+        \find(\forall u; b ==>)
+        \add({\subst u; t}(b) ==>)
+        \heuristics(gamma)
+    };
+    exRight {
+        \find( ==> \exists u; b)
+        \add( ==> {\subst u; t}(b))
+        \heuristics(gamma)
+    };
+    allLeftHide {
+        \find(\forall u; b ==>)
+        \replacewith({\subst u; t}(b) ==>)
+        \addrules(
+            insert_hidden {
+                \add(\forall u; b ==>)
+            })
+        \heuristics(gamma_destructive)
+    };
+    exRightHide {
+        \find( ==> \exists u; b)
+        \replacewith( ==> {\subst u; t}(b))
+        \addrules(
+            insert_hidden {
+                \add( ==> \exists u; b)
+            })
+        \heuristics(gamma_destructive)
+    };
+
+    instAll {
+        \assumes(\forall u; b ==>)
+        \find(t)
+        \add({\subst u; t}(b) ==>)
+    };
+    instEx {
+        \assumes( ==> \exists u; b)
+        \find(t)
+        \add( ==> {\subst u; t}(b))
+    };
+
+    // delta rules
+    allRight {
+        \find( ==> \forall u; b)
+        \varcond(\newDependingOn(sk, b))
+        \replacewith( ==> {\subst u; sk}b) \heuristics(delta)
+    };
+    exLeft {
+        \find(\exists u; b ==>)
+        \varcond(\newDependingOn(sk, b))
+        \replacewith({\subst u; sk}b ==>) \heuristics(delta)
+    };
+
+    // simplification
+    all_unused {
+        \find(\forall u; b)
+        \varcond(\notFreeIn(u, b))
+        \replacewith(b)
+        \heuristics(elimQuantifier)
+    };
+    ex_unused {
+        \find(\exists u; b)
+        \varcond(\notFreeIn(u, b))
+        \replacewith(b)
+        \heuristics(elimQuantifier)
+    };
+
+    // equality
+    eqClose {
+        \find(s = s)
+        \replacewith(true) \heuristics(concrete)
+    };
+
+    eqSymm {
+        \find(commEqLeft = commEqRight)
+        \replacewith(commEqRight = commEqLeft)
+        \heuristics(order_terms)
+    };
+
+    make_insert_eq {
+        \find(sr = tr ==>)
+        \addrules(
+            insert_eq {
+                \find(sr)
+                \replacewith(tr)
+            })
+    };
+
+    make_insert_eq_nonrigid {
+        \find(s = t ==>)
+        \addrules(
+            insert_eq_nonrigid {
+                \find(s)
+                \sameUpdateLevel
+                \replacewith(t)
+                \displayname "insert_eq"
+            })
+    };
+    insert_eq_all {
+        \find(sr = tr ==>)
+        \replacewith( ==>)
+        \addrules(
+            auto_insert_eq {
+                \find(sr)
+                \replacewith(tr)
+                \heuristics(simplify)
+            })
+    };
+
+    // wary substitutions
+    apply_subst {
+        \find({\subst u; t}target)
+        // it is enough to rebuild the same term, as substitutions
+        // are automatically applied in this situation
+        \replacewith({\subst u; t}target)
+        \heuristics(try_apply_subst)
+    };
+
+    apply_subst_for {
+        \schemaVar \formula phi;
+        \find({\subst u; t}phi)
+        // it is enough to rebuild the same term, as substitutions
+        // are automatically applied in this situation
+        \replacewith({\subst u; t}phi)
+        \heuristics(try_apply_subst)
+        \displayname "apply_subst"
+    };
+
+    subst_to_eq {
+        \find({\subst u; t}target)
+        \sameUpdateLevel
+        \varcond(\newDependingOn(sk, t))
+        \replacewith({\subst u; sk}target)
+        \add(sk = t ==>)
+        \heuristics(simplify)
+    };
+
+    subst_to_eq_for {
+        \schemaVar \formula phi;
+        \find({\subst u; t}phi)
+        \sameUpdateLevel
+        \varcond(\newDependingOn(sk, t))
+        \replacewith({\subst u; sk}phi)
+        \add(sk = t ==>)
+        \heuristics(simplify)
+        \displayname "subst_to_eq"
+    };
+
+    ///////////////////////////////////////////////////////////////////////////////
+
+
+    applyEq {
+        \assumes(s = t1 ==>)
+        \find(s)
+        \sameUpdateLevel
+        \replacewith(t1)
+        \heuristics(apply_equations, apply_select_eq)
+        \displayname "applyEq"
+    };
+
+    applyEqReverse {
+        \assumes(s = t1 ==>)
+        \find(t1)
+        \sameUpdateLevel
+        \replacewith(s)
+        \heuristics(apply_auxiliary_eq)
+        \displayname "applyEqReverse"
+    };
+
+    applyEqRigid {
+        \schemaVar \term [rigid] H tr1;
+
+        \assumes(sr = tr1 ==>)
+        \find(sr)
+        \replacewith(tr1)
+        \heuristics(apply_equations)
+        \displayname "applyEq"
+    };
+
+    pullOut {
+        \find(t)
+        \sameUpdateLevel
+        \varcond(\newDependingOn(sk, t))
+        \replacewith(sk)
+        \add(t = sk ==>)
+        \heuristics(semantics_blasting)
+    };
+
+    \lemma
+    eqTermCut {
+        \find(t)
+        \sameUpdateLevel
+        "Assume #t  = #s":
+            \add(t = s ==>);
+        "Assume #t != #s":
+            \add(t != s ==>)
+    };
+
+    \lemma
+    equivAllRight {
+        \find( ==> \forall u; b <-> \forall e2; c)
+        \varcond(\notFreeIn(u, c), \notFreeIn(e2, b))
+        \add( ==> \forall u; (b <-> ({\subst e2; u}c)))
+    };
+
+    // --------------------------------------------------------------------------
+    // rule for unique function symbols
+    // --------------------------------------------------------------------------
+
+    equalUnique {
+        \schemaVar \term any f, f2;
+        \schemaVar \formula result;
+
+        \find(f = f2)
+        \varcond(\equalUnique(f, f2, result))
+
+        \replacewith(result)
+
+        \heuristics(concrete)
+    };
+
+}