Move format descriptions under single path

yeslogic · Sep 9, 2022 · ff7112f · ff7112f
1 parent 8c0dc84
commit ff7112f
Show file tree

Hide file tree

Showing 11 changed files with 20 additions and 21 deletions.
diff --git a/experiments/idris/fathom.ipkg b/experiments/idris/fathom.ipkg
@@ -20,12 +20,11 @@ modules = Fathom
         , Fathom.Data.Iso
         , Fathom.Data.Sing
         , Fathom.Data.Word
-
-        , Fathom.Closed.IndexedInductive
-        , Fathom.Closed.IndexedInductiveCustom
-        , Fathom.Closed.InductiveRecursive
-        , Fathom.Closed.InductiveRecursiveCustom
-        , Fathom.Open.Record
+        , Fathom.Format.IndexedInductive
+        , Fathom.Format.IndexedInductiveCustom
+        , Fathom.Format.InductiveRecursive
+        , Fathom.Format.InductiveRecursiveCustom
+        , Fathom.Format.Record
 
         , Playground
         , Playground.OpenType.IndexedInductive

diff --git a/experiments/idris/src/Fathom.idr b/experiments/idris/src/Fathom.idr
@@ -1,7 +1,7 @@
 ||| A sketch of core Fathom in Idris 2
 
 import public Fathom.Base
-import public Fathom.Closed.IndexedInductive
-import public Fathom.Closed.InductiveRecursive
-import public Fathom.Closed.InductiveRecursiveCustom
-import public Fathom.Open.Record
+import public Fathom.Format.IndexedInductive
+import public Fathom.Format.InductiveRecursive
+import public Fathom.Format.InductiveRecursiveCustom
+import public Fathom.Format.Record
diff --git a/...is/src/Fathom/Closed/IndexedInductive.idr → ...is/src/Fathom/Format/IndexedInductive.idr b/...is/src/Fathom/Closed/IndexedInductive.idr → ...is/src/Fathom/Format/IndexedInductive.idr
@@ -1,7 +1,7 @@
 ||| A closed universe of format descriptions as an inductive type, where the
 ||| in-memory representation is tracked as an index on the type.
 
-module Fathom.Closed.IndexedInductive
+module Fathom.Format.IndexedInductive
 
 
 import Data.Colist

diff --git a/.../Fathom/Closed/IndexedInductiveCustom.idr → .../Fathom/Format/IndexedInductiveCustom.idr b/.../Fathom/Closed/IndexedInductiveCustom.idr → .../Fathom/Format/IndexedInductiveCustom.idr
@@ -1,7 +1,7 @@
 ||| A closed universe of format descriptions as an inductive type, where the
 ||| in-memory representation is tracked as an index on the type.
 
-module Fathom.Closed.IndexedInductiveCustom
+module Fathom.Format.IndexedInductiveCustom
 
 
 import Data.Colist

diff --git a/.../src/Fathom/Closed/InductiveRecursive.idr → .../src/Fathom/Format/InductiveRecursive.idr b/.../src/Fathom/Closed/InductiveRecursive.idr → .../src/Fathom/Format/InductiveRecursive.idr
@@ -19,7 +19,7 @@
 ||| Inspiration for this approach is taken from [“The Power of Pi”](https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf)
 ||| by Oury and Swierstra.
 
-module Fathom.Closed.InductiveRecursive
+module Fathom.Format.InductiveRecursive
 
 
 import Data.Colist

diff --git a/...athom/Closed/InductiveRecursiveCustom.idr → ...athom/Format/InductiveRecursiveCustom.idr b/...athom/Closed/InductiveRecursiveCustom.idr → ...athom/Format/InductiveRecursiveCustom.idr
@@ -1,7 +1,7 @@
 ||| Experimenting with an approach to extending inductive-recursive format
 ||| descriptions with custom formats.
 
-module Fathom.Closed.InductiveRecursiveCustom
+module Fathom.Format.InductiveRecursiveCustom
 
 
 import Data.Bits

diff --git a/experiments/idris/src/Fathom/Open/Record.idr → ...iments/idris/src/Fathom/Format/Record.idr b/experiments/idris/src/Fathom/Open/Record.idr → ...iments/idris/src/Fathom/Format/Record.idr
@@ -8,7 +8,7 @@
 ||| universes’ that [some type theorists were proposing](https://www.cmu.edu/dietrich/philosophy/hott/slides/shulman-2022-05-12.pdf#page=79),
 ||| but I may be mistaken.
 
-module Fathom.Open.Record
+module Fathom.Format.Record
 
 
 import Data.Colist

diff --git a/experiments/idris/src/Playground.idr b/experiments/idris/src/Playground.idr
@@ -6,9 +6,9 @@ import Data.Vect
 
 import Fathom.Base
 import Fathom.Data.Sing
-import Fathom.Closed.InductiveRecursive as IndRec
-import Fathom.Closed.IndexedInductive as Indexed
-import Fathom.Open.Record as Record
+import Fathom.Format.InductiveRecursive as IndRec
+import Fathom.Format.IndexedInductive as Indexed
+import Fathom.Format.Record as Record
 
 
 -- Experiment with converting between the different styles of format universes

diff --git a/experiments/idris/src/Playground/OpenType/IndexedInductive.idr b/experiments/idris/src/Playground/OpenType/IndexedInductive.idr
@@ -4,7 +4,7 @@ module Playground.OpenType.IndexedInductive
 
 
 import Fathom.Data.Sing
-import Fathom.Closed.IndexedInductiveCustom
+import Fathom.Format.IndexedInductiveCustom
 
 
 namespace FormatOf

diff --git a/experiments/idris/src/Playground/OpenType/InductiveRecursive.idr b/experiments/idris/src/Playground/OpenType/InductiveRecursive.idr
@@ -4,7 +4,7 @@ module Playground.OpenType.InductiveRecursive
 
 
 import Fathom.Data.Sing
-import Fathom.Closed.InductiveRecursiveCustom
+import Fathom.Format.InductiveRecursiveCustom
 
 
 namespace Format

diff --git a/experiments/idris/src/Playground/OpenType/Record.idr b/experiments/idris/src/Playground/OpenType/Record.idr
@@ -4,7 +4,7 @@ module Playground.OpenType.Record
 
 
 import Fathom.Data.Sing
-import Fathom.Open.Record
+import Fathom.Format.Record
 
 
 namespace Format