{-# LANGUAGE OverloadedStrings #-}

-- |
-- Module      :  Swarm.Language.Pipeline
-- Copyright   :  Brent Yorgey
-- Maintainer  :  byorgey@gmail.com
--
-- 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',
  showTypeErrorPos,
) where

import Data.Bifunctor (first)
import Data.Data (Data)
import Data.Text (Text)
import Data.Yaml as Y
import GHC.Generics (Generic)
import Swarm.Language.Context
import Swarm.Language.Elaborate
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

-- | A record containing the results of the language processing
--   pipeline.  Put a 'Term' in, and get one of these out.
data ProcessedTerm
  = ProcessedTerm
      Term
      -- ^ The elaborated term
      TModule
      -- ^ The type of the term (and of any embedded definitions)
      Requirements
      -- ^ Requirements of the term
      ReqCtx
      -- ^ Capability context for any definitions embedded in the term
  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)

instance FromJSON ProcessedTerm where
  parseJSON :: Value -> Parser ProcessedTerm
parseJSON = forall a. String -> (Text -> Parser a) -> Value -> Parser a
withText String
"Term" Text -> Parser ProcessedTerm
tryProcess
   where
    tryProcess :: Text -> Y.Parser ProcessedTerm
    tryProcess :: Text -> Parser ProcessedTerm
tryProcess Text
t = case Text -> Either Text (Maybe ProcessedTerm)
processTerm Text
t of
      Left Text
err -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Could not parse term: " forall a. [a] -> [a] -> [a]
++ forall source target. From source target => source -> target
from Text
err
      Right Maybe ProcessedTerm
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Term was only whitespace"
      Right (Just ProcessedTerm
pt) -> forall (m :: * -> *) a. Monad m => a -> m a
return ProcessedTerm
pt

instance ToJSON ProcessedTerm where
  toJSON :: ProcessedTerm -> Value
toJSON (ProcessedTerm Term
t TModule
_ Requirements
_ ReqCtx
_) = Text -> Value
String forall a b. (a -> b) -> a -> b
$ forall a. PrettyPrec a => a -> Text
prettyText Term
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 TypeErr ProcessedTerm
processParsedTerm :: Syntax -> Either TypeErr ProcessedTerm
processParsedTerm = TCtx -> ReqCtx -> Syntax -> Either TypeErr 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 -> TypeErr -> Text
prettyTypeErr 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 TypeErr ProcessedTerm
processParsedTerm' TCtx
ctx ReqCtx
capCtx) Maybe Syntax
mt

prettyTypeErr :: Text -> TypeErr -> Text
prettyTypeErr :: Text -> TypeErr -> Text
prettyTypeErr Text
code TypeErr
te = Text
teLoc forall a. Semigroup a => a -> a -> a
<> forall a. PrettyPrec a => a -> Text
prettyText TypeErr
te
 where
  teLoc :: Text
teLoc = case TypeErr -> Maybe Location
getTypeErrLocation TypeErr
te of
    Just (Location Int
s Int
e) -> (forall source target. From source target => source -> target
from forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Text -> (Int, Int) -> ((Int, Int), (Int, Int))
getLocRange Text
code (Int
s, Int
e)) forall a. Semigroup a => a -> a -> a
<> Text
": "
    Maybe Location
_anyOtherLoc -> Text
""

showTypeErrorPos :: Text -> TypeErr -> ((Int, Int), (Int, Int), Text)
showTypeErrorPos :: Text -> TypeErr -> ((Int, Int), (Int, Int), Text)
showTypeErrorPos Text
code TypeErr
te = (forall {a} {b}. (Num a, Num b) => (a, b) -> (a, b)
minusOne (Int, Int)
start, forall {a} {b}. (Num a, Num b) => (a, b) -> (a, b)
minusOne (Int, Int)
end, Text
msg)
 where
  minusOne :: (a, b) -> (a, b)
minusOne (a
x, b
y) = (a
x forall a. Num a => a -> a -> a
- a
1, b
y forall a. Num a => a -> a -> a
- b
1)

  ((Int, Int)
start, (Int, Int)
end) = case TypeErr -> Maybe Location
getTypeErrLocation TypeErr
te of
    Just (Location Int
s Int
e) -> Text -> (Int, Int) -> ((Int, Int), (Int, Int))
getLocRange Text
code (Int
s, Int
e)
    Maybe Location
_anyOtherLoc -> ((Int
1, Int
1), (Int
65535, Int
65535)) -- unknown loc spans the whole document
  msg :: Text
msg = forall a. PrettyPrec a => a -> Text
prettyText TypeErr
te

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