refactor: Factor out Utils module.

Author: solomon-b

lambda-calculus-hs.cabal

@@ -43,6 +43,13 @@ common common-settings
     -Wpartial-fields
     -Werror=missing-home-modules
 
+library utils
+  import:              common-settings
+  visibility:          private
+  exposed-modules:     Utils
+  hs-source-dirs:      lib
+  build-depends:       base >= 2 && <5, these, semialign
+
 library test-harness
   import:              common-settings
   visibility:          private
@@ -108,70 +115,70 @@ executable 00-SimplyTypedEvaluation
   import:              common-settings
   main-is:             00-SimplyTypedEvaluation.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, utils
 
 executable 01-BidirectionalTypechecking
   import:              common-settings
   main-is:             01-BidirectionalTypechecking.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, test-harness, utils
 
 executable 02-NormalizationByEvaluation
   import:              common-settings
   main-is:             02-NormalizationByEvaluation.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, test-harness, utils
 
 executable 03-Elaboration
   import:              common-settings
   main-is:             03-Elaboration.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, test-harness, utils
 
 executable 04-TypedHoles
   import:              common-settings
   main-is:             04-TypedHoles.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, test-harness, utils
 
 executable 05-SystemT
   import:              common-settings
   main-is:             05-SystemT.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, test-harness, utils
 
 executable 06-Records
   import:              common-settings
   main-is:             06-Records.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, test-harness, utils
 
 executable 07-SumTypes
   import:              common-settings
   main-is:             07-SumTypes.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, test-harness, utils
 
 executable 08-Subtyping
   import:              common-settings
   main-is:             08-Subtyping.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, scientific, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, scientific, test-harness, utils
 
 executable 09-NominalInductiveTypes
   import:              common-settings
   main-is:             09-NominalInductiveTypes.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, scientific, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, scientific, test-harness, utils
 
 executable 09b-IsoInductiveTypes
   import:              common-settings
   main-is:             09b-IsoInductiveTypes.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, scientific, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, scientific, test-harness, utils
 
 executable 10-SystemF
   import:              common-settings
   main-is:             10-SystemF.hs
   hs-source-dirs:      main
-  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, scientific, test-harness
+  build-depends:       base >= 2 && <5, mtl, transformers, containers, these, semialign, scientific, test-harness, utils

lib/Utils.hs

@@ -0,0 +1,45 @@
+module Utils
+  ( SnocList (..)
+  , nth
+  , alignWithM
+  ) where
+
+import Data.Align (Semialign, align)
+import Data.These (These)
+
+-- | A list that grows on the right. We use this as our environment
+-- representation because it matches the structure of de Bruijn
+-- indices: the most recently bound variable is at the end (index 0),
+-- and older bindings are further left (higher indices).
+--
+-- A regular list would work too, but snoc lists make the
+-- correspondence between binding order and index explicit.
+data SnocList a
+  = Snoc (SnocList a) a
+  | Nil
+  deriving (Show, Eq, Ord, Functor, Foldable)
+
+-- | Look up a value by de Bruijn index, counting from the right
+-- (most recent binding).
+nth :: SnocList a -> Int -> Maybe a
+nth xs i
+  | i < 0 = Nothing
+  | otherwise =
+      let go = \case
+            (Nil, _) -> Nothing
+            (Snoc _ x, 0) -> Just x
+            (Snoc xs' _, i') -> go (xs', i' - 1)
+       in go (xs, i)
+
+-- | Align two structures and traverse the result. Used by record
+-- tactics to check term fields against type fields: 'These' means
+-- both present, 'This' means a field in the type but not the term
+-- (missing), 'That' means a field in the term but not the type
+-- (extra).
+alignWithM ::
+  (Traversable t, Applicative f, Semialign t) =>
+  (These a b1 -> f b2) ->
+  t a ->
+  t b1 ->
+  f (t b2)
+alignWithM f as = traverse f . align as

main/00-SimplyTypedEvaluation.hs

@@ -15,33 +15,7 @@ module Main where
 
 import Data.Maybe (fromMaybe)
 import Data.String
-
---------------------------------------------------------------------------------
--- Utils
-
--- | A list that grows on the right. We use this as our environment
--- representation because it matches the structure of de Bruijn indices: the
--- most recently bound variable is at the end (index 0), and older bindings are
--- further left (higher indices).
---
--- A regular list would work too, but snoc lists make the correspondence between
--- binding order and index explicit.
-data SnocList a
-  = Snoc (SnocList a) a
-  | Nil
-  deriving (Show, Eq, Ord, Functor, Foldable)
-
--- | Look up a value by de Bruijn index, counting from the right (most recent
--- binding).
-nth :: SnocList a -> Int -> Maybe a
-nth xs i
-  | i < 0 = Nothing
-  | otherwise =
-      let go = \case
-            (Nil, _) -> Nothing
-            (Snoc _ x, 0) -> Just x
-            (Snoc xs' _, i') -> go (xs', i' - 1)
-       in go (xs, i)
+import Utils (SnocList (..), nth)
 
 --------------------------------------------------------------------------------
 -- Syntax

main/01-BidirectionalTypechecking.hs

@@ -23,33 +23,7 @@ import Data.String
 import PrettyTerm (Prec, appPrec, arrowPrec, arrowSym, atomPrec, lamPrec, lambdaSym, parensIf)
 import PrettyTerm qualified as PP
 import TestHarness (RunResult (..), runTest, runTestErr, section)
-
---------------------------------------------------------------------------------
--- Utils
-
--- | A list that grows on the right. We use this as our environment
--- representation because it matches the structure of de Bruijn indices: the
--- most recently bound variable is at the end (index 0), and older bindings are
--- further left (higher indices).
---
--- A regular list would work too, but snoc lists make the correspondence between
--- binding order and index explicit.
-data SnocList a
-  = Snoc (SnocList a) a
-  | Nil
-  deriving (Show, Eq, Ord, Functor, Foldable)
-
--- | Look up a value by de Bruijn index, counting from the right (most recent
--- binding).
-nth :: SnocList a -> Int -> Maybe a
-nth xs i
-  | i < 0 = Nothing
-  | otherwise =
-      let go = \case
-            (Nil, _) -> Nothing
-            (Snoc _ x, 0) -> Just x
-            (Snoc xs' _, i') -> go (xs', i' - 1)
-       in go (xs, i)
+import Utils (SnocList (..), nth)
 
 --------------------------------------------------------------------------------
 -- Syntax

main/02-NormalizationByEvaluation.hs

@@ -26,33 +26,7 @@ import Data.String
 import PrettyTerm (Prec, appPrec, arrowPrec, arrowSym, atomPrec, lamPrec, lambdaSym, parensIf)
 import PrettyTerm qualified as PP
 import TestHarness (RunResult (..), runTest, runTestErr, section)
-
---------------------------------------------------------------------------------
--- Utils
-
--- | A list that grows on the right. We use this as our environment
--- representation because it matches the structure of de Bruijn indices: the
--- most recently bound variable is at the end (index 0), and older bindings are
--- further left (higher indices).
---
--- A regular list would work too, but snoc lists make the correspondence between
--- binding order and index explicit.
-data SnocList a
-  = Snoc (SnocList a) a
-  | Nil
-  deriving (Show, Eq, Ord, Functor, Foldable)
-
--- | Look up a value by de Bruijn index, counting from the right (most recent
--- binding).
-nth :: SnocList a -> Int -> Maybe a
-nth xs i
-  | i < 0 = Nothing
-  | otherwise =
-      let go = \case
-            (Nil, _) -> Nothing
-            (Snoc _ x, 0) -> Just x
-            (Snoc xs' _, i') -> go (xs', i' - 1)
-       in go (xs, i)
+import Utils (SnocList (..), nth)
 
 --------------------------------------------------------------------------------
 -- Syntax

main/03-Elaboration.hs

@@ -27,33 +27,7 @@ import Data.String
 import PrettyTerm (Prec, appPrec, arrowPrec, arrowSym, atomPrec, lamPrec, lambdaSym, parensIf)
 import PrettyTerm qualified as PP
 import TestHarness (RunResult (..), runTest, runTestErr, section)
-
---------------------------------------------------------------------------------
--- Utils
-
--- | A list that grows on the right. We use this as our environment
--- representation because it matches the structure of de Bruijn indices: the
--- most recently bound variable is at the end (index 0), and older bindings are
--- further left (higher indices).
---
--- A regular list would work too, but snoc lists make the correspondence between
--- binding order and index explicit.
-data SnocList a
-  = Snoc (SnocList a) a
-  | Nil
-  deriving (Show, Eq, Ord, Functor, Foldable)
-
--- | Look up a value by de Bruijn index, counting from the right (most recent
--- binding).
-nth :: SnocList a -> Int -> Maybe a
-nth xs i
-  | i < 0 = Nothing
-  | otherwise =
-      let go = \case
-            (Nil, _) -> Nothing
-            (Snoc _ x, 0) -> Just x
-            (Snoc xs' _, i') -> go (xs', i' - 1)
-       in go (xs, i)
+import Utils (SnocList (..), nth)
 
 --------------------------------------------------------------------------------
 -- Syntax

main/04-TypedHoles.hs

@@ -27,33 +27,7 @@ import Data.String
 import PrettyTerm (Prec, appPrec, arrowPrec, arrowSym, atomPrec, lamPrec, lambdaSym, parensIf)
 import PrettyTerm qualified as PP
 import TestHarness (RunResult (..), runTest, runTestErr, section)
-
---------------------------------------------------------------------------------
--- Utils
-
--- | A list that grows on the right. We use this as our environment
--- representation because it matches the structure of de Bruijn indices: the
--- most recently bound variable is at the end (index 0), and older bindings are
--- further left (higher indices).
---
--- A regular list would work too, but snoc lists make the correspondence between
--- binding order and index explicit.
-data SnocList a
-  = Snoc (SnocList a) a
-  | Nil
-  deriving (Show, Eq, Ord, Functor, Foldable)
-
--- | Look up a value by de Bruijn index, counting from the right (most recent
--- binding).
-nth :: SnocList a -> Int -> Maybe a
-nth xs i
-  | i < 0 = Nothing
-  | otherwise =
-      let go = \case
-            (Nil, _) -> Nothing
-            (Snoc _ x, 0) -> Just x
-            (Snoc xs' _, i') -> go (xs', i' - 1)
-       in go (xs, i)
+import Utils (SnocList (..), nth)
 
 --------------------------------------------------------------------------------
 -- Syntax

main/05-SystemT.hs

@@ -27,33 +27,7 @@ import Data.String
 import PrettyTerm (Prec, appPrec, arrowPrec, arrowSym, atomPrec, lamPrec, lambdaSym, parensIf)
 import PrettyTerm qualified as PP
 import TestHarness (RunResult (..), runTest, runTestErr, section)
-
---------------------------------------------------------------------------------
--- Utils
-
--- | A list that grows on the right. We use this as our environment
--- representation because it matches the structure of de Bruijn indices: the
--- most recently bound variable is at the end (index 0), and older bindings are
--- further left (higher indices).
---
--- A regular list would work too, but snoc lists make the correspondence between
--- binding order and index explicit.
-data SnocList a
-  = Snoc (SnocList a) a
-  | Nil
-  deriving (Show, Eq, Ord, Functor, Foldable)
-
--- | Look up a value by de Bruijn index, counting from the right (most recent
--- binding).
-nth :: SnocList a -> Int -> Maybe a
-nth xs i
-  | i < 0 = Nothing
-  | otherwise =
-      let go = \case
-            (Nil, _) -> Nothing
-            (Snoc _ x, 0) -> Just x
-            (Snoc xs' _, i') -> go (xs', i' - 1)
-       in go (xs, i)
+import Utils (SnocList (..), nth)
 
 --------------------------------------------------------------------------------
 -- Syntax