Move typing tests to t/typing/

runtimeverification · Dec 5, 2018 · aaa447d · aaa447d
1 parent f639991
commit aaa447d
Show file tree

Hide file tree

Showing 25 changed files with 71 additions and 3 deletions.
diff --git a/lib/build.py b/lib/build.py
@@ -84,7 +84,7 @@ def test_strict(input):
 
 def test_typing(input):
     global typing_tests
-    expected = input + '.typing.expected'
+    expected = input + '.expected'
     typing_tests += [ do_test(typing, input, expected) ]
 
 # Basic tests
@@ -98,7 +98,6 @@ def test_typing(input):
 # We need distinct exptected and actual files for these.
 test_ocaml('t/bytestring.plc')
 test_java('t/bytestring.plc')
-test_typing('t/builtin-app.plc')
 
 # Cryptography
 # ------------
@@ -124,7 +123,11 @@ def test_typing(input):
 test('t/sum.plc')
 test('t/fact.plc')
 
-# test_typing('t/lists/nil.plc')
+# Typing tests
+# ------------
+
+test_typing('t/typing/builtin-app.plc')
+
 test_typing('t/typing/add-integer.plc')
 test_typing('t/typing/error.plc')
 test_typing('t/typing/int-id-app.plc')

diff --git a/t/add-integer.plc.typing.expected b/t/add-integer.plc.typing.expected
diff --git a/t/builtin-app.plc.typing.expected b/t/builtin-app.plc.typing.expected
diff --git a/t/error.plc.typing.expected b/t/error.plc.typing.expected
diff --git a/t/int-id-app.plc.typing.expected b/t/int-id-app.plc.typing.expected
diff --git a/t/int-id-poly-inst.plc.typing.expected b/t/int-id-poly-inst.plc.typing.expected
diff --git a/t/int-id-poly.plc.typing.expected b/t/int-id-poly.plc.typing.expected
diff --git a/t/int-id.plc.typing.expected b/t/int-id.plc.typing.expected
diff --git a/t/int.plc.typing.expected b/t/int.plc.typing.expected
diff --git a/t/add-integer.plc → t/typing/add-integer.plc b/t/add-integer.plc → t/typing/add-integer.plc
diff --git a/t/typing/add-integer.plc.expected b/t/typing/add-integer.plc.expected
@@ -0,0 +1,8 @@
+<generatedTop>
+  <k>
+    ( all $s ( size ) ( fun [ ( con integer ) $s ] ( fun [ ( con integer ) $s ] [ ( con integer ) $s ] ) ) ) :: ( type )
+  </k>
+  <env>
+    .
+  </env>
+</generatedTop>
diff --git a/t/typing/builtin-app.plc b/t/typing/builtin-app.plc
@@ -0,0 +1 @@
+(program 0.1.0 [ [ {(builtin addInteger) (con 1)} (con 1 ! 1)] (con 1 ! 1) ])
diff --git a/t/typing/builtin-app.plc.expected b/t/typing/builtin-app.plc.expected
@@ -0,0 +1,8 @@
+<generatedTop>
+  <k>
+    [ ( con integer ) ( con 1 ) ] :: ( type )
+  </k>
+  <env>
+    .
+  </env>
+</generatedTop>
diff --git a/t/error.plc → t/typing/error.plc b/t/error.plc → t/typing/error.plc
diff --git a/t/typing/error.plc.expected b/t/typing/error.plc.expected
@@ -0,0 +1,8 @@
+<generatedTop>
+  <k>
+    ( fun [ ( con integer ) ( con 1 ) ] [ ( con integer ) ( con 1 ) ] ) :: ( type )
+  </k>
+  <env>
+    .
+  </env>
+</generatedTop>
diff --git a/t/int-id-app.plc → t/typing/int-id-app.plc b/t/int-id-app.plc → t/typing/int-id-app.plc
diff --git a/t/typing/int-id-app.plc.expected b/t/typing/int-id-app.plc.expected
@@ -0,0 +1,8 @@
+<generatedTop>
+  <k>
+    [ ( con integer ) ( con 1 ) ] :: ( type )
+  </k>
+  <env>
+    .
+  </env>
+</generatedTop>
diff --git a/t/int-id-poly-inst.plc → t/typing/int-id-poly-inst.plc b/t/int-id-poly-inst.plc → t/typing/int-id-poly-inst.plc
diff --git a/t/typing/int-id-poly-inst.plc.expected b/t/typing/int-id-poly-inst.plc.expected
@@ -0,0 +1,8 @@
+<generatedTop>
+  <k>
+    ( fun [ ( con integer ) ( con 3 ) ] [ ( con integer ) ( con 3 ) ] ) :: ( type )
+  </k>
+  <env>
+    .
+  </env>
+</generatedTop>
diff --git a/t/int-id-poly.plc → t/typing/int-id-poly.plc b/t/int-id-poly.plc → t/typing/int-id-poly.plc
diff --git a/t/typing/int-id-poly.plc.expected b/t/typing/int-id-poly.plc.expected
@@ -0,0 +1,8 @@
+<generatedTop>
+  <k>
+    ( all s ( size ) ( fun [ ( con integer ) s ] [ ( con integer ) s ] ) ) :: ( type )
+  </k>
+  <env>
+    .
+  </env>
+</generatedTop>
diff --git a/t/int-id.plc → t/typing/int-id.plc b/t/int-id.plc → t/typing/int-id.plc
diff --git a/t/typing/int-id.plc.expected b/t/typing/int-id.plc.expected
@@ -0,0 +1,8 @@
+<generatedTop>
+  <k>
+    ( fun [ ( con integer ) ( con 1 ) ] [ ( con integer ) ( con 1 ) ] ) :: ( type )
+  </k>
+  <env>
+    .
+  </env>
+</generatedTop>
diff --git a/t/int.plc → t/typing/int.plc b/t/int.plc → t/typing/int.plc
diff --git a/t/typing/int.plc.expected b/t/typing/int.plc.expected
@@ -0,0 +1,8 @@
+<generatedTop>
+  <k>
+    [ ( con integer ) ( con 1 ) ] :: ( type )
+  </k>
+  <env>
+    .
+  </env>
+</generatedTop>