first tests for (mm0 parser, mmu parser, mm0+mmu proof checker)

tests/README.md

@@ -0,0 +1,13 @@
+**positive and negative tests for mm0 and mmu**
+
+This folder holds positive (pass folder) and negative (fail folder) tests for mm0 and mmu, inside subfolders
+
+Those subfolders contain mm0 and mmu files that can be used to test :
+- mm0 parsers (parsingMM0 and parsingBoth folder)
+- mmu parsers (parsingMMU and ParsingBoth folder)
+- mm0 vs mmu proofChecker (all folders):
+  - parsingMM0, parsingMMU and ParsingBoth handle the parsing stage
+  - matching handles match between mm0 statements and mmu directives
+  - registering handles the process of recording joined mm0 statements/mmu directives to form a coherent context
+  - dynamicParsing handles the behavior of a dynamic parser built on a coherent context 
+  - proofchecking handles the proof checking of a (mm0, mmu) pair

tests/fail/parsingBoth/chars cannot be outside a subset of the ascii charset.mm0

@@ -0,0 +1,6 @@
+-- lexeme ::= symbol | identifier | number | math-string
+-- symbol ::= '*' | '.' | ':' | ';' | '(' | ')' | '>' | '{' | '}' | '=' | '_'
+-- identifier ::= [a-zA-Z_][a-zA-Z0-9_]*
+-- number ::= 0 | [1-9][0-9]*
+-- math-string ::= '$' [^$]* '$'
+sort s…;

tests/fail/parsingBoth/chars cannot be outside a subset of the ascii charset.mmu

@@ -0,0 +1,6 @@
+-- Whitespace is ignored except to separate tokens
+-- Line comments are written --comment and extend until the next \n; line comments act like whitespace
+-- An identifier token matches [0-9a-zA-Z_:]+
+-- Characters ( ) are single character symbol tokens
+-- Anything else is forbidden
+(sort s…)

tests/fail/parsingBoth/chars cannot be outside a subset of the ascii charset2.mm0

@@ -0,0 +1,6 @@
+-- lexeme ::= symbol | identifier | number | math-string
+-- symbol ::= '*' | '.' | ':' | ';' | '(' | ')' | '>' | '{' | '}' | '=' | '_'
+-- identifier ::= [a-zA-Z_][a-zA-Z0-9_]*
+-- number ::= 0 | [1-9][0-9]*
+-- math-string ::= '$' [^$]* '$'
+sort s ;

tests/fail/parsingBoth/chars cannot be outside a subset of the ascii charset2.mmu

@@ -0,0 +1,6 @@
+-- Whitespace is ignored except to separate tokens
+-- Line comments are written --comment and extend until the next \n; line comments act like whitespace
+-- An identifier token matches [0-9a-zA-Z_:]+
+-- Characters ( ) are single character symbol tokens
+-- Anything else is forbidden
+(sort s )