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

tests/README.md

@@ -0,0 +1,5 @@
+**Test files for mm0 and mmu**
+
+This folder holds various tests for MM0, MM1, MMU, and MMB.
+
+* `mm0_mmu/{pass, fail}`: Integration tests for MM0 + MMU that should pass or fail.

tests/mm0_mmu/fail/bad-id1.mm0

@@ -0,0 +1,2 @@
+--  empty id
+sort ;

tests/mm0_mmu/fail/bad-id1.mmu

@@ -0,0 +1,2 @@
+--  empty id
+(sort )

tests/mm0_mmu/fail/bad-id2.mm0

@@ -0,0 +1,3 @@
+--  blank id
+sort  
+ ;

tests/mm0_mmu/fail/bad-id2.mmu

@@ -0,0 +1,3 @@
+--  blank id
+(sort  
+ )

tests/mm0_mmu/fail/bad-id3.mm0

@@ -0,0 +1,2 @@
+--  id starting with a digit
+sort 0;

tests/mm0_mmu/fail/bad-id3.mmu

@@ -0,0 +1,2 @@
+--  id starting with a digit
+(sort 0)

tests/mm0_mmu/fail/bad-id4.mm0

@@ -0,0 +1,2 @@
+-- id with forbidden char -
+sort sot-;

tests/mm0_mmu/fail/bad-id4.mmu

@@ -0,0 +1,2 @@
+-- id with forbidden char -
+(sort sot-)

tests/mm0_mmu/fail/bad-id5.mm0

@@ -0,0 +1,2 @@
+--  id that is a single underscore _
+sort _;

tests/mm0_mmu/fail/bad-id5.mmu

@@ -0,0 +1,2 @@
+--  id that is a single underscore _
+(sort _)

tests/mm0_mmu/fail/bad-whitespace1.mm0

@@ -0,0 +1,2 @@
+--     v-- this is a TAB
+sort s	;

tests/mm0_mmu/fail/bad-whitespace1.mmu

@@ -0,0 +1,2 @@
+--      v-- this is a TAB
+(sort s	)

tests/mm0_mmu/fail/bad-whitespace2.mm0

@@ -0,0 +1,2 @@
+--     v-- this is a LINE TABULATION
+sort s;

tests/mm0_mmu/fail/bad-whitespace2.mmu

@@ -0,0 +1,2 @@
+--      v-- this is a LINE TABULATION
+(sort s)

tests/mm0_mmu/fail/bad-whitespace3.mm0

@@ -0,0 +1,2 @@
+--     v-- this is a FORM FEED
+sort s;

tests/mm0_mmu/fail/bad-whitespace3.mmu

@@ -0,0 +1,2 @@
+--      v-- this is a FORM FEED
+(sort s)

tests/mm0_mmu/fail/bad-whitespace4.mm0

@@ -0,0 +1,2 @@
+--     v-- this is a CARRIAGE RETURN
+sort s;

tests/mm0_mmu/fail/bad-whitespace4.mmu

@@ -0,0 +1,2 @@
+--      v-- this is a CARRIAGE RETURN
+(sort s)

tests/mm0_mmu/fail/non-ascii1.mm0

@@ -0,0 +1 @@
+sort ß;

tests/mm0_mmu/fail/non-ascii1.mmu

@@ -0,0 +1 @@
+(sort ß)

tests/mm0_mmu/fail/non-ascii2.mm0

@@ -0,0 +1,2 @@
+--    v- non-break space
+sort s ;

tests/mm0_mmu/fail/non-ascii2.mmu

@@ -0,0 +1,2 @@
+--     v- non-break space
+(sort s )

tests/mm0_mmu/pass/id.mm0

@@ -0,0 +1,4 @@
+-- identifier ::= [a-zA-Z_][a-zA-Z0-9_]*
+sort id_1;
+sort Id2_;
+sort _id3;

tests/mm0_mmu/pass/id.mmu

@@ -0,0 +1,4 @@
+-- identifier ::= [a-zA-Z_][a-zA-Z0-9_]*
+(sort id_1)
+(sort Id2_)
+(sort _id3)

tests/mm0_mmu/pass/whitespace1.mm0

@@ -0,0 +1,2 @@
+--    v-- this is a SPACE
+sort s ;

tests/mm0_mmu/pass/whitespace1.mmu

@@ -0,0 +1,2 @@
+--     v-- this is a SPACE
+(sort s )

tests/mm0_mmu/pass/whitespace2.mm0

@@ -0,0 +1,3 @@
+--    v-- this is a LINE FEED
+sort s
+;

tests/mm0_mmu/pass/whitespace2.mmu

@@ -0,0 +1,3 @@
+--     v-- this is a LINE FEED
+(sort s
+)

tests/mm0_mmu/run-mm0-hs.sh

@@ -0,0 +1,5 @@
+#!/bin/sh
+
+# Usage: ./run-mm0-hs.sh pass/TEST
+#                     or fail/TEST
+mm0-hs verify $1.mm0 $1.mmu