Initial Values that can inhabit Typ

lib/fine-types/fine-types.cabal

@@ -49,14 +49,17 @@ library
     src
   build-depends:
     base >=4.14.3.0
+    , bytestring
     , containers
     , megaparsec ^>= 9.2.1
     , parser-combinators
+    , text
   exposed-modules:
     Language.FineTypes
     Language.FineTypes.Module
     Language.FineTypes.Parser
     Language.FineTypes.Typ
+    Language.FineTypes.Value
 
 test-suite unit
   import:      language, opts-exe

lib/fine-types/src/Language/FineTypes/Value.hs

@@ -0,0 +1,122 @@
+-- | 'Value' represents the values that can inhabit 'Typ'.
+module Language.FineTypes.Value
+    ( -- * 'Value' data type.
+    Value (..)
+    , Ix
+    , ZeroF (..)
+    , OneF (..)
+    , TwoF (..)
+
+    -- * Type checking
+    , hasTyp
+    ) where
+
+import Prelude
+
+import Data.ByteString
+    ( ByteString )
+import Data.Text
+    ( Text )
+import Numeric.Natural
+    ( Natural )
+import Language.FineTypes.Typ
+    ( Typ )
+
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import qualified Language.FineTypes.Typ as Typ
+
+{-----------------------------------------------------------------------------
+    Values corresponding to Typ
+------------------------------------------------------------------------------}
+type Ix = Int
+
+data Value
+    = Zero ZeroF
+    | One (OneF Value)
+    | Two (TwoF Value Value)
+    | Product [Value]
+        -- ^ N-ary products.
+    | Sum Ix Value
+        -- ^ N-ary sums.
+    deriving (Eq, Ord, Show)
+
+-- | Values for predefined 'Typ's.
+data ZeroF
+    = Bool Bool
+    | Bytes ByteString
+    | Integer Integer
+    | Natural Natural
+    | Text Text
+    | Unit
+    deriving (Eq, Ord, Show)
+
+-- | Values for unary operations on 'Typ'.
+data OneF a
+    = Option (Maybe a)
+    | Sequence [a]
+    | PowerSet (Set.Set a)
+    deriving (Eq, Ord, Show)
+
+-- | Values for binary operations on 'Typ'.
+data TwoF a b
+    = FiniteMap (Map.Map a b)
+    deriving (Eq, Ord, Show)
+
+{-----------------------------------------------------------------------------
+    Type checking
+------------------------------------------------------------------------------}
+-- | Check whether a 'Value' inhabits the given 'Typ'.
+hasTyp :: Value -> Typ -> Bool
+hasTyp (Zero a) (Typ.Zero b)
+    = typOf0 a == b
+hasTyp (One a) (Typ.One op typ)
+    = hasTyp1 a op typ
+hasTyp (Product [a,b]) (Typ.Two Typ.Product2 ta tb)
+    = (a `hasTyp` ta) && (b `hasTyp` tb)
+hasTyp (Product as) (Typ.ProductN fields)
+    | length as == length fields
+        = and (zipWith hasTyp as $ map snd fields)
+    | otherwise
+        = False
+hasTyp (Sum 0 a) (Typ.Two Typ.Sum2 ta _)
+    = a `hasTyp` ta
+hasTyp (Sum 1 b) (Typ.Two Typ.Sum2 _ tb)
+    = b `hasTyp` tb
+hasTyp (Sum ix a) (Typ.SumN constructors)
+    | 0 <= ix && ix < length constructors
+        = a `hasTyp` (snd $ constructors !! ix)
+    | otherwise
+        = False
+hasTyp (Two a) (Typ.Two op typ1 typ2)
+    = hasTyp2 a op typ1 typ2
+hasTyp _ _
+    = False
+
+typOf0 :: ZeroF -> Typ.TypConst
+typOf0 a = case a of
+    Bool{} -> Typ.Bool
+    Bytes{} -> Typ.Bytes
+    Integer{} -> Typ.Integer
+    Natural{} -> Typ.Natural
+    Text{} -> Typ.Text
+    Unit -> Typ.Unit
+
+hasTyp1 :: OneF Value -> Typ.OpOne -> Typ -> Bool
+hasTyp1 (Option a) Typ.Option t
+    = all (`hasTyp` t) a
+hasTyp1 (Sequence as) Typ.Sequence t
+    = all (`hasTyp` t) as
+hasTyp1 (PowerSet as) Typ.PowerSet t
+    = all (`hasTyp` t) as
+hasTyp1 _ _ _
+    = False
+
+hasTyp2 :: TwoF Value Value -> Typ.OpTwo -> Typ -> Typ -> Bool
+hasTyp2 (FiniteMap m) Typ.PartialFunction ta tb
+    = all (`hasTyp` ta) (Map.keys m)
+    && all (`hasTyp` tb) (Map.elems m)
+hasTyp2 (FiniteMap m) Typ.FiniteSupport ta tb
+    = hasTyp2 (FiniteMap m) Typ.PartialFunction ta tb
+hasTyp2 _ _ _ _
+    = False