Merge pull request #22 from uwplse/theories-dune

reorganize files under standard theories directory
uwplse · Oct 22, 2023 · 5c9318c · 5c9318c
2 parents 5193b97 + f7270aa
commit 5c9318c
Show file tree

Hide file tree

Showing 16 changed files with 23 additions and 15 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -1,21 +1,20 @@
--Q core Cheerios
--Q extraction Cheerios
+-Q theories Cheerios
 -Q runtime/coq Cheerios
 
-core/Types.v
-core/Tree.v
-core/ByteDecidable.v
-core/BasicSerializers.v
-core/Core.v
-core/Cheerios.v
-core/Tactics.v
-core/DeserializerMonad.v
-core/Combinators.v
+theories/Core/Types.v
+theories/Core/Tree.v
+theories/Core/ByteDecidable.v
+theories/Core/BasicSerializers.v
+theories/Core/Core.v
+theories/Core/Cheerios.v
+theories/Core/Tactics.v
+theories/Core/DeserializerMonad.v
+theories/Core/Combinators.v
 
-extraction/ExtrOcamlCheeriosFinInt.v
-extraction/ExtrOcamlCheeriosString.v
-extraction/ExtrOcamlCheeriosBasic.v
-extraction/ExtrOcamlCheeriosNatInt.v
+theories/Extraction/ExtrOcamlCheeriosFinInt.v
+theories/Extraction/ExtrOcamlCheeriosString.v
+theories/Extraction/ExtrOcamlCheeriosBasic.v
+theories/Extraction/ExtrOcamlCheeriosNatInt.v
 
 runtime/coq/ExtractPositiveSerializer.v
 runtime/coq/ExtractPositiveSerializerDeps.v

diff --git a/dune-project b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.5)
+(using coq 0.6)
+(name cheerios)
diff --git a/core/BasicSerializers.v → theories/Core/BasicSerializers.v b/core/BasicSerializers.v → theories/Core/BasicSerializers.v
diff --git a/core/ByteDecidable.v → theories/Core/ByteDecidable.v b/core/ByteDecidable.v → theories/Core/ByteDecidable.v
diff --git a/core/Cheerios.v → theories/Core/Cheerios.v b/core/Cheerios.v → theories/Core/Cheerios.v
diff --git a/core/Combinators.v → theories/Core/Combinators.v b/core/Combinators.v → theories/Core/Combinators.v
diff --git a/core/Core.v → theories/Core/Core.v b/core/Core.v → theories/Core/Core.v
diff --git a/core/DeserializerMonad.v → theories/Core/DeserializerMonad.v b/core/DeserializerMonad.v → theories/Core/DeserializerMonad.v
diff --git a/core/Tactics.v → theories/Core/Tactics.v b/core/Tactics.v → theories/Core/Tactics.v
diff --git a/core/Tree.v → theories/Core/Tree.v b/core/Tree.v → theories/Core/Tree.v
diff --git a/core/Types.v → theories/Core/Types.v b/core/Types.v → theories/Core/Types.v
diff --git a/extraction/ExtrOcamlCheeriosBasic.v → theories/Extraction/ExtrOcamlCheeriosBasic.v b/extraction/ExtrOcamlCheeriosBasic.v → theories/Extraction/ExtrOcamlCheeriosBasic.v
diff --git a/extraction/ExtrOcamlCheeriosFinInt.v → ...ries/Extraction/ExtrOcamlCheeriosFinInt.v b/extraction/ExtrOcamlCheeriosFinInt.v → ...ries/Extraction/ExtrOcamlCheeriosFinInt.v
diff --git a/extraction/ExtrOcamlCheeriosNatInt.v → ...ries/Extraction/ExtrOcamlCheeriosNatInt.v b/extraction/ExtrOcamlCheeriosNatInt.v → ...ries/Extraction/ExtrOcamlCheeriosNatInt.v
diff --git a/extraction/ExtrOcamlCheeriosString.v → ...ries/Extraction/ExtrOcamlCheeriosString.v b/extraction/ExtrOcamlCheeriosString.v → ...ries/Extraction/ExtrOcamlCheeriosString.v
diff --git a/theories/dune b/theories/dune
@@ -0,0 +1,6 @@
+(coq.theory
+ (name Cheerios)
+ (package coq-cheerios)
+ (synopsis "Coq library for verified serialization"))
+
+(include_subdirs qualified)