Move experimental files out of the main directory

DeepSpec · Nov 9, 2018 · c8ca4f7 · c8ca4f7
1 parent 0a16e74
commit c8ca4f7
Show file tree

Hide file tree

Showing 8 changed files with 18 additions and 8 deletions.
diff --git a/Makefile b/Makefile
@@ -1,7 +1,6 @@
 .PHONY: clean all coq test tests examples install uninstall depgraph \
   example-imp example-lc example-io example-nimp
 
-
 COQPATHFILE=$(wildcard _CoqPath)
 
 all: coq
@@ -37,7 +36,7 @@ example-io: examples/IO.v
 	  ocamlbuild io.native && ./io.native
 
 Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
+	coq_makefile -f $< -o $@
 
 clean: Makefile.coq
 	$(MAKE) -f Makefile.coq clean

diff --git a/_CoqConfig b/_CoqConfig
@@ -6,9 +6,6 @@ theories/ITree.v
 
 theories/Eq/Eq.v
 
-theories/CoAlgebra.v
-theories/Machine.v
-
 theories/Equivalence.v
 theories/Morphisms.v
 theories/MorphismsFacts.v
@@ -17,5 +14,3 @@ theories/UpTo.v
 theories/MutFix.v
 theories/Trace.v
 theories/MFixITree.v
-
-theories/Alternatives/IxEffect.v
diff --git a/theories/Alternatives.v → experiments/Alternatives.v b/theories/Alternatives.v → experiments/Alternatives.v
diff --git a/theories/CoAlgebra.v → experiments/CoAlgebra.v b/theories/CoAlgebra.v → experiments/CoAlgebra.v
diff --git a/theories/Alternatives/IxEffect.v → experiments/EffRec.v b/theories/Alternatives/IxEffect.v → experiments/EffRec.v
diff --git a/theories/Machine.v → experiments/Machine.v b/theories/Machine.v → experiments/Machine.v
@@ -24,10 +24,13 @@ From ExtLib.Structures Require Import
      Functor Applicative Monad.
 
 From ITree Require Import
-     CoAlgebra Eq.Eq.
+     Eq.Eq.
 
 From ITree Require ITree.
 
+From ITree.Experiments Require Import
+     CoAlgebra.
+
 Set Implicit Arguments.
 Set Contextual Implicit.
 

diff --git a/experiments/Makefile b/experiments/Makefile
@@ -0,0 +1,9 @@
+.PHONY: all build
+
+all: build
+
+build: Makefile.coq
+	make -f $<
+
+Makefile.coq: _CoqProject
+	coq_makefile -f $< -o $@
diff --git a/experiments/README.md b/experiments/README.md
@@ -0,0 +1,4 @@
+- `CoAlgebra.v`: Categories and coalgebras
+- `Machine.v`: Initial coalgebra
+- `EffRec.v`: equivalence between representations of effects as `Type -> Type`
+  or `{ action : Type; reaction : action -> Type }`