{-# LANGUAGE OverloadedStrings #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Some convenient functions for putting together the whole Swarm
-- language processing pipeline: parsing, type checking, capability
-- checking, and elaboration.  If you want to simply turn some raw
-- text representing a Swarm program into something useful, this is
-- probably the module you want.
module Swarm.Language.Pipeline (
  ProcessedTerm (..),
  processTerm,
  processParsedTerm,
  processTerm',
  processParsedTerm',
  processTermEither,
) where

import Control.Lens ((^.))
import Data.Bifunctor (first)
import Data.Data (Data)
import Data.Text (Text)
import Data.Text qualified as T
import Data.Yaml as Y
import GHC.Generics (Generic)
import Swarm.Language.Context
import Swarm.Language.Elaborate
import Swarm.Language.Module
import Swarm.Language.Parse
import Swarm.Language.Pretty
import Swarm.Language.Requirement
import Swarm.Language.Syntax
import Swarm.Language.Typecheck
import Swarm.Language.Types
import Witch (into)

-- | A record containing the results of the language processing
--   pipeline.  Put a 'Term' in, and get one of these out.  A
--   'ProcessedTerm' contains:
--
--   * The elaborated + type-annotated term, plus the types of any
--     embedded definitions ('TModule')
--
--   * The 'Requirements' of the term
--
--   * The requirements context for any definitions embedded in the
--     term ('ReqCtx')
data ProcessedTerm = ProcessedTerm TModule Requirements ReqCtx
  deriving (Typeable ProcessedTerm
ProcessedTerm -> DataType
ProcessedTerm -> Constr
(forall b. Data b => b -> b) -> ProcessedTerm -> ProcessedTerm
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 u. Int -> (forall d. Data d => d -> u) -> ProcessedTerm -> u
forall u. (forall d. Data d => d -> u) -> ProcessedTerm -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProcessedTerm -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProcessedTerm -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProcessedTerm -> m ProcessedTerm
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProcessedTerm -> m ProcessedTerm
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProcessedTerm
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProcessedTerm -> c ProcessedTerm
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProcessedTerm)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProcessedTerm)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProcessedTerm -> m ProcessedTerm
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProcessedTerm -> m ProcessedTerm
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProcessedTerm -> m ProcessedTerm
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProcessedTerm -> m ProcessedTerm
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProcessedTerm -> m ProcessedTerm
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProcessedTerm -> m ProcessedTerm
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ProcessedTerm -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ProcessedTerm -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> ProcessedTerm -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ProcessedTerm -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProcessedTerm -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProcessedTerm -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProcessedTerm -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProcessedTerm -> r
gmapT :: (forall b. Data b => b -> b) -> ProcessedTerm -> ProcessedTerm
$cgmapT :: (forall b. Data b => b -> b) -> ProcessedTerm -> ProcessedTerm
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProcessedTerm)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProcessedTerm)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProcessedTerm)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProcessedTerm)
dataTypeOf :: ProcessedTerm -> DataType
$cdataTypeOf :: ProcessedTerm -> DataType
toConstr :: ProcessedTerm -> Constr
$ctoConstr :: ProcessedTerm -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProcessedTerm
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProcessedTerm
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProcessedTerm -> c ProcessedTerm
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProcessedTerm -> c ProcessedTerm
Data, Int -> ProcessedTerm -> ShowS
[ProcessedTerm] -> ShowS
ProcessedTerm -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProcessedTerm] -> ShowS
$cshowList :: [ProcessedTerm] -> ShowS
show :: ProcessedTerm -> String
$cshow :: ProcessedTerm -> String
showsPrec :: Int -> ProcessedTerm -> ShowS
$cshowsPrec :: Int -> ProcessedTerm -> ShowS
Show, ProcessedTerm -> ProcessedTerm -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProcessedTerm -> ProcessedTerm -> Bool
$c/= :: ProcessedTerm -> ProcessedTerm -> Bool
== :: ProcessedTerm -> ProcessedTerm -> Bool
$c== :: ProcessedTerm -> ProcessedTerm -> Bool
Eq, forall x. Rep ProcessedTerm x -> ProcessedTerm
forall x. ProcessedTerm -> Rep ProcessedTerm x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ProcessedTerm x -> ProcessedTerm
$cfrom :: forall x. ProcessedTerm -> Rep ProcessedTerm x
Generic)

processTermEither :: Text -> Either Text ProcessedTerm
processTermEither :: Text -> Either Text ProcessedTerm
processTermEither Text
t = case Text -> Either Text (Maybe ProcessedTerm)
processTerm Text
t of
  Left Text
err -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unwords [Text
"Could not parse term:", Text
err]
  Right Maybe ProcessedTerm
Nothing -> forall a b. a -> Either a b
Left Text
"Term was only whitespace"
  Right (Just ProcessedTerm
pt) -> forall a b. b -> Either a b
Right ProcessedTerm
pt

instance FromJSON ProcessedTerm where
  parseJSON :: Value -> Parser ProcessedTerm
parseJSON = forall a. String -> (Text -> Parser a) -> Value -> Parser a
withText String
"Term" forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall target source. From source target => source -> target
into @String) forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either Text ProcessedTerm
processTermEither

instance ToJSON ProcessedTerm where
  toJSON :: ProcessedTerm -> Value
toJSON (ProcessedTerm TModule
t Requirements
_ ReqCtx
_) = Text -> Value
String forall a b. (a -> b) -> a -> b
$ forall a. PrettyPrec a => a -> Text
prettyText (forall s t. Module s t -> Syntax' s
moduleAST TModule
t)

-- | Given a 'Text' value representing a Swarm program,
--
--   1. Parse it (see "Swarm.Language.Parse")
--   2. Typecheck it (see "Swarm.Language.Typecheck")
--   3. Elaborate it (see "Swarm.Language.Elaborate")
--   4. Check what capabilities it requires (see "Swarm.Language.Capability")
--
--   Return either the end result (or @Nothing@ if the input was only
--   whitespace) or a pretty-printed error message.
processTerm :: Text -> Either Text (Maybe ProcessedTerm)
processTerm :: Text -> Either Text (Maybe ProcessedTerm)
processTerm = TCtx -> ReqCtx -> Text -> Either Text (Maybe ProcessedTerm)
processTerm' forall t. Ctx t
empty forall t. Ctx t
empty

-- | Like 'processTerm', but use a term that has already been parsed.
processParsedTerm :: Syntax -> Either ContextualTypeErr ProcessedTerm
processParsedTerm :: Syntax -> Either ContextualTypeErr ProcessedTerm
processParsedTerm = TCtx -> ReqCtx -> Syntax -> Either ContextualTypeErr ProcessedTerm
processParsedTerm' forall t. Ctx t
empty forall t. Ctx t
empty

-- | Like 'processTerm', but use explicit starting contexts.
processTerm' :: TCtx -> ReqCtx -> Text -> Either Text (Maybe ProcessedTerm)
processTerm' :: TCtx -> ReqCtx -> Text -> Either Text (Maybe ProcessedTerm)
processTerm' TCtx
ctx ReqCtx
capCtx Text
txt = do
  Maybe Syntax
mt <- Text -> Either Text (Maybe Syntax)
readTerm Text
txt
  forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Text -> ContextualTypeErr -> Text
prettyTypeErrText Text
txt) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (TCtx -> ReqCtx -> Syntax -> Either ContextualTypeErr ProcessedTerm
processParsedTerm' TCtx
ctx ReqCtx
capCtx) Maybe Syntax
mt

-- | Like 'processTerm'', but use a term that has already been parsed.
processParsedTerm' :: TCtx -> ReqCtx -> Syntax -> Either ContextualTypeErr ProcessedTerm
processParsedTerm' :: TCtx -> ReqCtx -> Syntax -> Either ContextualTypeErr ProcessedTerm
processParsedTerm' TCtx
ctx ReqCtx
capCtx Syntax
t = do
  TModule
m <- TCtx -> Syntax -> Either ContextualTypeErr TModule
inferTop TCtx
ctx Syntax
t
  let (Requirements
caps, ReqCtx
capCtx') = ReqCtx -> Term -> (Requirements, ReqCtx)
requirements ReqCtx
capCtx (Syntax
t forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) (Term' ty)
sTerm)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ TModule -> Requirements -> ReqCtx -> ProcessedTerm
ProcessedTerm (TModule -> TModule
elaborateModule TModule
m) Requirements
caps ReqCtx
capCtx'

elaborateModule :: TModule -> TModule
elaborateModule :: TModule -> TModule
elaborateModule (Module Syntax' (Poly Type)
ast TCtx
ctx) = forall s t. Syntax' s -> Ctx t -> Module s t
Module (Syntax' (Poly Type) -> Syntax' (Poly Type)
elaborate Syntax' (Poly Type)
ast) TCtx
ctx