Test the TODO output

the-little-typer · May 4, 2018 · fa05d5a · fa05d5a
1 parent 82a7706
commit fa05d5a
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 0 deletions.
diff --git a/test-todo-output.rkt b/test-todo-output.rkt
@@ -0,0 +1,8 @@
+#lang racket/base
+
+(require rackunit racket/port)
+
+(check-equal?
+ (with-output-to-string
+   (lambda () (dynamic-require "todo-test.pie" #f)))
+ "<pkgs>/pie/todo-test.pie:10.15: TODO:\n           n : Nat\n         n-1 : Nat\n peas-of-n-1 : (Vec Atom n-1)\n------------------------------\n Atom\n\n\n<pkgs>/pie/todo-test.pie:10.20: TODO:\n           n : Nat\n         n-1 : Nat\n peas-of-n-1 : (Vec Atom n-1)\n------------------------------\n (Vec Atom n-1)\n\n\n<pkgs>/pie/todo-test.pie:13.17: TODO: Nat\n\n<pkgs>/pie/todo-test.pie:15.19: TODO: \n (Π ((n Nat))\n  (Vec Atom n))\n\n\n")
diff --git a/todo-test.pie b/todo-test.pie
@@ -0,0 +1,15 @@
+#lang pie
+
+(claim peas (Pi ((n Nat)) (Vec Atom n)))
+(define peas
+  (λ (n)
+    (ind-Nat n
+      (lambda (k) (Vec Atom k))
+      vecnil
+      (λ (n-1 peas-of-n-1)
+        (vec:: TODO TODO)))))
+
+(claim some-nat Nat)
+(define some-nat TODO)
+(claim multi-line (Pi ((n Nat)) (Vec Atom n)))
+(define multi-line TODO)