typed-protocols: moved types to Core module

typed-protocols/src/Network/TypedProtocol/Core.hs

@@ -1,22 +1,23 @@
-{-# LANGUAGE BangPatterns             #-}
 {-# LANGUAGE ConstraintKinds          #-}
 {-# LANGUAGE DataKinds                #-}
+{-# LANGUAGE DerivingVia              #-}
 {-# LANGUAGE EmptyCase                #-}
 {-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE FlexibleInstances        #-}
 {-# LANGUAGE GADTs                    #-}
 {-# LANGUAGE MultiParamTypeClasses    #-}
+{-# LANGUAGE PatternSynonyms          #-}
 {-# LANGUAGE PolyKinds                #-}
 {-# LANGUAGE QuantifiedConstraints    #-}
 {-# LANGUAGE RankNTypes               #-}
 {-# LANGUAGE ScopedTypeVariables      #-}
 {-# LANGUAGE StandaloneDeriving       #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE TypeFamilies             #-}
 {-# LANGUAGE TypeFamilyDependencies   #-}
 {-# LANGUAGE TypeOperators            #-}
 -- need for 'Show' instance of 'ProtocolState'
 {-# LANGUAGE UndecidableInstances     #-}
+{-# LANGUAGE ViewPatterns             #-}
 
 -- | This module defines the core of the typed protocol framework.
 --
@@ -43,6 +44,9 @@ module Network.TypedProtocol.Core
   , IsPipelined (..)
   , Outstanding
   , N (..)
+  , Nat (Succ, Zero)
+  , natToInt
+  , unsafeIntToNat
   , ActiveAgency
   , ActiveAgency' (..)
   , IsActiveState (..)
@@ -51,6 +55,7 @@ module Network.TypedProtocol.Core
   ) where
 
 import           Data.Kind (Constraint, Type)
+import           Unsafe.Coerce (unsafeCoerce)
 
 import           Data.Singletons
 
@@ -504,3 +509,37 @@ type        Outstanding :: IsPipelined -> N
 type family Outstanding pl where
   Outstanding 'NonPipelined    = Z
   Outstanding ('Pipelined n _) = n
+
+-- | A value level inductive natural number, indexed by the corresponding type
+-- level natural number 'N'.
+--
+-- This is often needed when writing pipelined peers to be able to count the
+-- number of outstanding pipelined yields, and show to the type checker that
+-- 'SenderCollect' and 'SenderDone' are being used correctly.
+--
+newtype Nat (n :: N) = UnsafeInt Int
+  deriving Show via Int
+
+data IsNat (n :: N) where
+  IsZero ::          IsNat Z
+  IsSucc :: Nat n -> IsNat (S n)
+
+toIsNat :: Nat n -> IsNat n
+toIsNat (UnsafeInt 0) = unsafeCoerce IsZero
+toIsNat (UnsafeInt n) = unsafeCoerce (IsSucc (UnsafeInt (pred n)))
+
+pattern Zero :: () => Z ~ n => Nat n
+pattern Zero <- (toIsNat -> IsZero) where
+  Zero = UnsafeInt 0
+
+pattern Succ :: () => (m ~ S n) => Nat n -> Nat m
+pattern Succ n <- (toIsNat -> IsSucc n) where
+  Succ (UnsafeInt n) = UnsafeInt (succ n)
+
+{-# COMPLETE Zero, Succ #-}
+
+natToInt :: Nat n -> Int
+natToInt (UnsafeInt n) = n
+
+unsafeIntToNat :: Int -> Nat n
+unsafeIntToNat = UnsafeInt

typed-protocols/src/Network/TypedProtocol/Peer.hs

@@ -3,13 +3,11 @@
 {-# LANGUAGE DerivingVia              #-}
 {-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE GADTs                    #-}
-{-# LANGUAGE PatternSynonyms          #-}
 {-# LANGUAGE PolyKinds                #-}
 {-# LANGUAGE RankNTypes               #-}
 {-# LANGUAGE StandaloneDeriving       #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeOperators            #-}
-{-# LANGUAGE ViewPatterns             #-}
 
 -- | Protocol EDSL.
 --
@@ -28,7 +26,6 @@ module Network.TypedProtocol.Peer
   ) where
 
 import           Data.Kind (Type)
-import           Unsafe.Coerce (unsafeCoerce)
 
 import           Network.TypedProtocol.Core as Core
 
@@ -257,37 +254,3 @@ data Receiver ps pr st stdone m c where
                  -> Receiver ps pr st stdone m c
 
 deriving instance Functor m => Functor (Receiver ps pr st stdone m)
-
--- | A value level inductive natural number, indexed by the corresponding type
--- level natural number 'N'.
---
--- This is often needed when writing pipelined peers to be able to count the
--- number of outstanding pipelined yields, and show to the type checker that
--- 'SenderCollect' and 'SenderDone' are being used correctly.
---
-newtype Nat (n :: N) = UnsafeInt Int
-  deriving Show via Int
-
-data IsNat (n :: N) where
-  IsZero ::          IsNat Z
-  IsSucc :: Nat n -> IsNat (S n)
-
-toIsNat :: Nat n -> IsNat n
-toIsNat (UnsafeInt 0) = unsafeCoerce IsZero
-toIsNat (UnsafeInt n) = unsafeCoerce (IsSucc (UnsafeInt (pred n)))
-
-pattern Zero :: () => Z ~ n => Nat n
-pattern Zero <- (toIsNat -> IsZero) where
-  Zero = UnsafeInt 0
-
-pattern Succ :: () => (m ~ S n) => Nat n -> Nat m
-pattern Succ n <- (toIsNat -> IsSucc n) where
-  Succ (UnsafeInt n) = UnsafeInt (succ n)
-
-{-# COMPLETE Zero, Succ #-}
-
-natToInt :: Nat n -> Int
-natToInt (UnsafeInt n) = n
-
-unsafeIntToNat :: Int -> Nat n
-unsafeIntToNat = UnsafeInt

typed-protocols/src/Network/TypedProtocol/Peer/Client.hs

@@ -33,7 +33,7 @@ module Network.TypedProtocol.Peer.Client
 import           Data.Kind (Type)
 
 import           Network.TypedProtocol.Core
-import           Network.TypedProtocol.Peer (Peer, Nat (..))
+import           Network.TypedProtocol.Peer (Peer)
 import qualified Network.TypedProtocol.Peer as TP
 
 

typed-protocols/src/Network/TypedProtocol/Peer/Server.hs

@@ -33,7 +33,7 @@ module Network.TypedProtocol.Peer.Server
 import           Data.Kind (Type)
 
 import           Network.TypedProtocol.Core
-import           Network.TypedProtocol.Peer (Peer, Nat (..))
+import           Network.TypedProtocol.Peer (Peer)
 import qualified Network.TypedProtocol.Peer as TP