Feature/issue 117 lsp vscode extension

regression/modulebad10/functor.slf

@@ -0,0 +1,18 @@
+package regression.modulebad10
+
+module functor
+
+requires
+
+abstract syntax e
+
+judgment eq: e = e
+
+  --- eq-refl
+  e = e
+
+provides
+
+terminals nil
+
+syntax l ::= nil | e, l

regression/modulebad10/test.slf

@@ -0,0 +1,14 @@
+package regression.modulebad10
+
+module test provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
+judgment nat-eq: n = n
+
+  --- nat-refl
+  n = n
+
+module m = regression.modulebad10.functor[n, nat-eq] //!

regression/modulebad11/nats.slf

@@ -0,0 +1,8 @@
+package regression.modulebad11
+
+module nats provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+

regression/modulebad11/test.slf

@@ -0,0 +1,10 @@
+package regression.modulebad11
+
+module test
+
+requires
+
+syntax n = regression.modulebad11.nats.n //! should be in 'imports' section, not 'requires'
+
+provides
+

regression/modulegood05/test.slf

@@ -82,12 +82,11 @@ end theorem
 
 module boolbt = regression.modulegood05.foldablebt
 [
-  boolid, 
-  boolnonid, 
-  b, 
-  lor, 
-  lor-left-id, 
-  lor-right-id, 
+  boolid,
+  boolnonid,
+  lor,
+  lor-left-id,
+  lor-right-id,
   lor-commutative
 ]
 

regression/modulegood06/test.slf

@@ -76,7 +76,7 @@ theorem lor-total:
   proof by unproved //!
 end theorem
 
-module boolbt = regression.modulegood06.foldablebt[boolid, boolnonid, b, lor, lor-commutative, lor-associative, lor-total]
+module boolbt = regression.modulegood06.foldablebt[boolid, boolnonid, lor, lor-commutative, lor-associative, lor-total]
 
 syntax bt = boolbt.bt ::= Leaf | Node bt b bt
 

regression/modulegood11/functor.slf

@@ -0,0 +1,20 @@
+package regression.modulegood11
+
+module functor
+
+requires
+
+abstract syntax e
+
+judgment eq: e = e
+
+  --- eq-refl
+  e = e
+
+provides
+
+theorem self-equal:
+  forall e1
+  exists e1 = e1
+  proof by rule eq-refl
+end theorem

regression/modulegood11/test.slf

@@ -0,0 +1,17 @@
+package regression.modulegood11
+
+module test provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
+module m = regression.modulegood11.functor[n]
+
+judgment n-eq = m.eq : n = n
+
+theorem nat-self-equal:
+  forall n1
+  exists n1 = n1
+  proof by rule m.eq-refl
+end theorem

regression/modulegood12/functor.slf

@@ -0,0 +1,18 @@
+package regression.modulegood12
+
+module functor
+
+imports
+  syntax n = regression.modulegood12.nats.n
+
+requires
+  abstract syntax e
+
+provides
+
+terminals wrap
+
+syntax w ::= wrap e
+
+judgment wrap-n: w = n
+

regression/modulegood12/nats.slf

@@ -0,0 +1,13 @@
+package regression.modulegood12
+
+module nats provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
+judgment equal: n = n
+
+  --- eq-refl
+  n = n
+

regression/modulegood12/test.slf

@@ -0,0 +1,12 @@
+package regression.modulegood12
+
+module test provides
+
+terminals zero succ
+
+syntax n ::= zero | succ n
+
+module m = regression.modulegood12.functor[n]
+
+syntax mw = m.w
+

regression/test1/set.slf

@@ -28,7 +28,7 @@ provides
 
 terminals in notin ok
 
-module repm = regression.test1.list[e,elem-eq]
+module repm = regression.test1.list[e]
 
 syntax r = repm.l
   ::= 0

regression/test1/test.slf

@@ -7,7 +7,7 @@ module nat = org.sasylf.util.Natural
 syntax n = nat.n
 
 module setb =
-regression.test1.set[n,nat.equal,nat.notequal,nat.ne-anti-reflexive,nat.eq-or-ne]
+regression.test1.set[n,nat.notequal,nat.ne-anti-reflexive,nat.eq-or-ne]
 
 terminals in
 

sasylf-lsp.mf

@@ -0,0 +1 @@
+Main-Class: edu.cmu.cs.sasylf.lsp.SASyLFLspLauncher