-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- A 'Module' packages together a type-annotated syntax tree along
-- with a context of top-level definitions.
module Swarm.Language.Module (
  -- * Modules
  Module (..),
  TModule,
  UModule,
  trivMod,
) where

import Data.Data (Data)
import Data.Yaml (FromJSON, ToJSON)
import GHC.Generics (Generic)
import Swarm.Language.Context (Ctx, empty)
import Swarm.Language.Syntax (Syntax')
import Swarm.Language.Types (Polytype, UPolytype, UType)

------------------------------------------------------------
-- Modules
------------------------------------------------------------

-- | A module generally represents the result of performing type
--   inference on a top-level expression, which in particular can
--   contain definitions ('Swarm.Language.Syntax.TDef').  A module
--   contains the type-annotated AST of the expression itself, as well
--   as the context giving the types of any defined variables.
data Module s t = Module {forall s t. Module s t -> Syntax' s
moduleAST :: Syntax' s, forall s t. Module s t -> Ctx t
moduleCtx :: Ctx t}
  deriving (Int -> Module s t -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s t. (Show s, Show t) => Int -> Module s t -> ShowS
forall s t. (Show s, Show t) => [Module s t] -> ShowS
forall s t. (Show s, Show t) => Module s t -> String
showList :: [Module s t] -> ShowS
$cshowList :: forall s t. (Show s, Show t) => [Module s t] -> ShowS
show :: Module s t -> String
$cshow :: forall s t. (Show s, Show t) => Module s t -> String
showsPrec :: Int -> Module s t -> ShowS
$cshowsPrec :: forall s t. (Show s, Show t) => Int -> Module s t -> ShowS
Show, Module s t -> Module s t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s t. (Eq s, Eq t) => Module s t -> Module s t -> Bool
/= :: Module s t -> Module s t -> Bool
$c/= :: forall s t. (Eq s, Eq t) => Module s t -> Module s t -> Bool
== :: Module s t -> Module s t -> Bool
$c== :: forall s t. (Eq s, Eq t) => Module s t -> Module s t -> Bool
Eq, forall a b. a -> Module s b -> Module s a
forall a b. (a -> b) -> Module s a -> Module s b
forall s a b. a -> Module s b -> Module s a
forall s a b. (a -> b) -> Module s a -> Module s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Module s b -> Module s a
$c<$ :: forall s a b. a -> Module s b -> Module s a
fmap :: forall a b. (a -> b) -> Module s a -> Module s b
$cfmap :: forall s a b. (a -> b) -> Module s a -> Module s b
Functor, Module s t -> DataType
Module s t -> Constr
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall {s} {t}. (Data s, Data t) => Typeable (Module s t)
forall s t. (Data s, Data t) => Module s t -> DataType
forall s t. (Data s, Data t) => Module s t -> Constr
forall s t.
(Data s, Data t) =>
(forall b. Data b => b -> b) -> Module s t -> Module s t
forall s t u.
(Data s, Data t) =>
Int -> (forall d. Data d => d -> u) -> Module s t -> u
forall s t u.
(Data s, Data t) =>
(forall d. Data d => d -> u) -> Module s t -> [u]
forall s t r r'.
(Data s, Data t) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
forall s t r r'.
(Data s, Data t) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
forall s t (m :: * -> *).
(Data s, Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
forall s t (m :: * -> *).
(Data s, Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
forall s t (c :: * -> *).
(Data s, Data t) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Module s t)
forall s t (c :: * -> *).
(Data s, Data t) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Module s t -> c (Module s t)
forall s t (t :: * -> *) (c :: * -> *).
(Data s, Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Module s t))
forall s t (t :: * -> * -> *) (c :: * -> *).
(Data s, Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Module s t))
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Module s t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Module s t -> c (Module s t)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Module s t))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
$cgmapMo :: forall s t (m :: * -> *).
(Data s, Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
$cgmapMp :: forall s t (m :: * -> *).
(Data s, Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
$cgmapM :: forall s t (m :: * -> *).
(Data s, Data t, Monad m) =>
(forall d. Data d => d -> m d) -> Module s t -> m (Module s t)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Module s t -> u
$cgmapQi :: forall s t u.
(Data s, Data t) =>
Int -> (forall d. Data d => d -> u) -> Module s t -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Module s t -> [u]
$cgmapQ :: forall s t u.
(Data s, Data t) =>
(forall d. Data d => d -> u) -> Module s t -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
$cgmapQr :: forall s t r r'.
(Data s, Data t) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
$cgmapQl :: forall s t r r'.
(Data s, Data t) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Module s t -> r
gmapT :: (forall b. Data b => b -> b) -> Module s t -> Module s t
$cgmapT :: forall s t.
(Data s, Data t) =>
(forall b. Data b => b -> b) -> Module s t -> Module s t
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Module s t))
$cdataCast2 :: forall s t (t :: * -> * -> *) (c :: * -> *).
(Data s, Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Module s t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Module s t))
$cdataCast1 :: forall s t (t :: * -> *) (c :: * -> *).
(Data s, Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Module s t))
dataTypeOf :: Module s t -> DataType
$cdataTypeOf :: forall s t. (Data s, Data t) => Module s t -> DataType
toConstr :: Module s t -> Constr
$ctoConstr :: forall s t. (Data s, Data t) => Module s t -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Module s t)
$cgunfold :: forall s t (c :: * -> *).
(Data s, Data t) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Module s t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Module s t -> c (Module s t)
$cgfoldl :: forall s t (c :: * -> *).
(Data s, Data t) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Module s t -> c (Module s t)
Data, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s t x. Rep (Module s t) x -> Module s t
forall s t x. Module s t -> Rep (Module s t) x
$cto :: forall s t x. Rep (Module s t) x -> Module s t
$cfrom :: forall s t x. Module s t -> Rep (Module s t) x
Generic, forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
forall s t.
(FromJSON s, FromJSON t) =>
Value -> Parser [Module s t]
forall s t.
(FromJSON s, FromJSON t) =>
Value -> Parser (Module s t)
parseJSONList :: Value -> Parser [Module s t]
$cparseJSONList :: forall s t.
(FromJSON s, FromJSON t) =>
Value -> Parser [Module s t]
parseJSON :: Value -> Parser (Module s t)
$cparseJSON :: forall s t.
(FromJSON s, FromJSON t) =>
Value -> Parser (Module s t)
FromJSON, forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
forall s t. (ToJSON t, ToJSON s) => [Module s t] -> Encoding
forall s t. (ToJSON t, ToJSON s) => [Module s t] -> Value
forall s t. (ToJSON t, ToJSON s) => Module s t -> Encoding
forall s t. (ToJSON t, ToJSON s) => Module s t -> Value
toEncodingList :: [Module s t] -> Encoding
$ctoEncodingList :: forall s t. (ToJSON t, ToJSON s) => [Module s t] -> Encoding
toJSONList :: [Module s t] -> Value
$ctoJSONList :: forall s t. (ToJSON t, ToJSON s) => [Module s t] -> Value
toEncoding :: Module s t -> Encoding
$ctoEncoding :: forall s t. (ToJSON t, ToJSON s) => Module s t -> Encoding
toJSON :: Module s t -> Value
$ctoJSON :: forall s t. (ToJSON t, ToJSON s) => Module s t -> Value
ToJSON)

-- | A 'TModule' is the final result of the type inference process on
--   an expression: we get a polytype for the expression, and a
--   context of polytypes for the defined variables.
type TModule = Module Polytype Polytype

-- | A 'UModule' represents the type of an expression at some
--   intermediate stage during the type inference process.  We get a
--   'UType' (/not/ a 'UPolytype') for the expression, which may
--   contain some free unification or type variables, as well as a
--   context of 'UPolytype's for any defined variables.
type UModule = Module UType UPolytype

-- | The trivial module for a given AST, with the empty context.
trivMod :: Syntax' s -> Module s t
trivMod :: forall s t. Syntax' s -> Module s t
trivMod Syntax' s
t = forall s t. Syntax' s -> Ctx t -> Module s t
Module Syntax' s
t forall t. Ctx t
empty