test: add regression test for ITree.iter fix; simplify organization o…

…f tests

tests/Makefile

@@ -1,11 +1,18 @@
-.PHONY: all build extraction clean
+.PHONY: all extraction clean
 
 all: coq extraction
 
+coq: output
+
+EXTRDIR:=output
+
+$(EXTRDIR):
+	mkdir -p $(EXTRDIR)
+
 include ../common.mk
 
 extraction: coq
-	ocamlbuild extraction/MetaModule.native -no-links
+	sh extraction-test.sh
 
 clean: clean-coq
 	$(RM) -rf _build/

tests/_CoqProject

@@ -1,17 +1,13 @@
 -Q ../theories ITree
--Q extraction/ TestExtraction
--Q unit/ TestUnit
+-Q src/ ITreeTest
+
+src/Tests.v
 
 # Test to ensure extracted code is compilable
 # - MetaModule.v is a module that depends on the
 #   ITree library
 # - Extract.v contains the extraction command for
 #   MetaModule (and recursively its dependencies)
-# The ocamlbuild command is in Makefile
-
-extraction/MetaModule.v
-extraction/Extract.v
-
-# Unit tests
 
-unit/Unit.v
+src/MetaModule.v
+src/Extract.v

tests/extraction-test.sh

@@ -0,0 +1,9 @@
+set -xe
+cd output/
+
+ocamlbuild test.native
+./test.native
+
+ocamlbuild MetaModule.native
+./MetaModule.native
+# This executable should do absolutely nothing

tests/extraction/Extract.v → tests/src/Extract.v

@@ -1,10 +1,10 @@
-Require TestExtraction.MetaModule.
+Require ITreeTest.MetaModule.
 
 Require Extraction.
 
 Extraction Language OCaml.
 Extraction Blacklist String List Char Core Z.
 
-Cd "extraction".
+Cd "output".
 Recursive Extraction Library MetaModule.
 Cd "..".

tests/unit/Unit.v → tests/src/Tests.v

@@ -14,3 +14,13 @@ Proof.
   rewrite interp_id_h.
   reflexivity.
 Qed.
+
+(* Regression test for #182 ([ITree.iter] should be executable even when the loop is infinite
+   (the body is always [Ret (inl _)]) *)
+Definition iter_spin : itree void1 void :=
+  iter (C := ktree _) (fun _ : unit => Ret (@inl unit void tt)) tt.
+
+Require Extraction.
+
+(* This should NOT loop forever. *)
+Extraction "output/test.ml" iter_spin.