{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE OverloadedStrings         #-}
-- Copyright 2024 United States Government as represented by the Administrator
-- of the National Aeronautics and Space Administration. All Rights Reserved.
--
-- Disclaimers
--
-- Licensed under the Apache License, Version 2.0 (the "License"); you may
-- not use this file except in compliance with the License. You may obtain a
-- copy of the License at
--
--      https://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
-- License for the specific language governing permissions and limitations
-- under the License.
--
-- | Transform a state diagram into a Copilot specification.
module Command.Diagram
    ( diagram
    , DiagramOptions(..)
    , DiagramFormat(..)
    , DiagramMode(..)
    , DiagramPropFormat(..)
    , ErrorCode
    )
  where

-- External imports
import Control.Exception    as E
import Control.Monad.Except (runExceptT)
import Data.Aeson           (object, (.=))
import Data.Foldable        (for_)
import Data.Text.Lazy       (pack)
import System.FilePath      ((</>))

-- External imports: auxiliary
import System.Directory.Extra ( copyTemplate )

-- External imports: parsing expressions.
import qualified Language.Lustre.AbsLustre as Lustre
import qualified Language.Lustre.ParLustre as Lustre (myLexer, pBoolSpec)
import qualified Language.SMV.AbsSMV       as SMV
import qualified Language.SMV.ParSMV       as SMV (myLexer, pBoolSpec)

-- Internal imports: auxiliary
import Command.Errors      (ErrorTriplet (..))
import Command.Result      (Result (..))
import Data.Diagram.Parser (DiagramFormat (..), readDiagram)
import Data.ExprPair       (ExprPair (..), ExprPairT (..))
import Data.Location       (Location (..))
import Paths_ogma_core     (getDataDir)

-- Internal imports: language ASTs, transformers
import           Language.SMV.Substitution      (substituteBoolExpr)
import           Language.Trans.Diagram2Copilot (DiagramMode (..),
                                                 diagram2CopilotSpec)
import qualified Language.Trans.Lustre2Copilot  as Lustre (boolSpec2Copilot,
                                                           boolSpecNames)
import           Language.Trans.SMV2Copilot     as SMV (boolSpec2Copilot,
                                                        boolSpecNames)

-- | Generate a new Copilot monitor that implements a state machine described
-- in a diagram given as an input file.
--
-- PRE: The file given is readable, contains a valid file with recognizable
-- format, the formulas in the file do not use any identifiers that exist in
-- Copilot, or any of @stateMachine@, @externalState@, @main@, @spec@,
-- @stateMachine1@, @clock@, @ftp@, @notPreviousNot@. All identifiers used are
-- valid C99 identifiers. The template, if provided, exists and uses the
-- variables needed by the diagram application generator. The target directory
-- is writable and there's enough disk space to copy the files over.
diagram :: FilePath       -- ^ Path to a file containing a diagram
        -> DiagramOptions -- ^ Customization options
        -> IO (Result ErrorCode)
diagram :: [Char] -> DiagramOptions -> IO (Result Int)
diagram [Char]
fp DiagramOptions
options = do
  (SomeException -> IO (Result Int))
-> IO (Result Int) -> IO (Result Int)
forall e a. Exception e => (e -> IO a) -> IO a -> IO a
E.handle (Result Int -> IO (Result Int)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Int -> IO (Result Int))
-> (SomeException -> Result Int)
-> SomeException
-> IO (Result Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> SomeException -> Result Int
diagramTemplateError [Char]
fp) (IO (Result Int) -> IO (Result Int))
-> IO (Result Int) -> IO (Result Int)
forall a b. (a -> b) -> a -> b
$ do
    -- Sub-parser for edge expressions.
    let functions :: ExprPair
functions = DiagramPropFormat -> ExprPair
exprPair (DiagramOptions -> DiagramPropFormat
diagramPropFormat DiagramOptions
options)

    -- Convert the diagram into elements in a Copilot spec.
    copilotSpecElems <- [Char]
-> DiagramOptions
-> ExprPair
-> IO (Either [Char] ([Char], [Char]))
diagram' [Char]
fp DiagramOptions
options ExprPair
functions

    -- Convert the elements into a success or error result.
    let (mOutput, result) = diagramResult fp copilotSpecElems

    -- If the result is success, expand the template.
    for_ mOutput $ \([Char]
streamDefs, [Char]
triggers) -> do
      let subst :: Value
subst = [Pair] -> Value
object
                    [ Key
"streamDefs" Key -> Text -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Char] -> Text
pack [Char]
streamDefs
                    , Key
"specName"   Key -> Text -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Char] -> Text
pack (DiagramOptions -> [Char]
diagramFilename DiagramOptions
options)
                    , Key
"input"      Key -> Text -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Char] -> Text
pack (DiagramOptions -> [Char]
diagramInputVar DiagramOptions
options)
                    , Key
"state"      Key -> Text -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Char] -> Text
pack (DiagramOptions -> [Char]
diagramStateVar DiagramOptions
options)
                    , Key
"triggers"   Key -> Text -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Char] -> Text
pack [Char]
triggers
                    ]

      templateDir <- case DiagramOptions -> Maybe [Char]
diagramTemplateDir DiagramOptions
options of
                       Just [Char]
x  -> [Char] -> IO [Char]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
x
                       Maybe [Char]
Nothing -> do
                         dataDir <- IO [Char]
getDataDir
                         return $ dataDir </> "templates" </> "diagram"

      let targetDir = DiagramOptions -> [Char]
diagramTargetDir DiagramOptions
options

      copyTemplate templateDir subst targetDir

    return result

-- | Generate a new Copilot monitor that implements a state machine described
-- in a diagram given as an input file, using a subexpression handler.
--
-- PRE: The file given is readable, contains a valid file with recognizable
-- format, the formulas in the file do not use any identifiers that exist in
-- Copilot, or any of @stateMachine@, @externalState@, @main@, @spec@,
-- @stateMachine1@, @clock@, @ftp@, @notPreviousNot@. All identifiers used are
-- valid C99 identifiers. The template, if provided, exists and uses the
-- variables needed by the diagram application generator. The target directory
-- is writable and there's enough disk space to copy the files over.
diagram' :: FilePath
         -> DiagramOptions
         -> ExprPair
         -> IO (Either String (String, String))
diagram' :: [Char]
-> DiagramOptions
-> ExprPair
-> IO (Either [Char] ([Char], [Char]))
diagram' [Char]
fp DiagramOptions
options ExprPair
exprP = do
  diagramE <- ExceptT ErrorTriplet IO Diagram -> IO (Either ErrorTriplet Diagram)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT ErrorTriplet IO Diagram
 -> IO (Either ErrorTriplet Diagram))
-> ExceptT ErrorTriplet IO Diagram
-> IO (Either ErrorTriplet Diagram)
forall a b. (a -> b) -> a -> b
$ [Char]
-> DiagramFormat -> ExprPair -> ExceptT ErrorTriplet IO Diagram
readDiagram [Char]
fp (DiagramOptions -> DiagramFormat
diagramFormat DiagramOptions
options) ExprPair
exprP
  case diagramE of
    Left (ErrorTriplet Int
_ec [Char]
msg Location
_loc) -> Either [Char] ([Char], [Char])
-> IO (Either [Char] ([Char], [Char]))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [Char] ([Char], [Char])
 -> IO (Either [Char] ([Char], [Char])))
-> Either [Char] ([Char], [Char])
-> IO (Either [Char] ([Char], [Char]))
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ([Char], [Char])
forall a b. a -> Either a b
Left [Char]
msg
    Right Diagram
diagramR ->
      Either [Char] ([Char], [Char])
-> IO (Either [Char] ([Char], [Char]))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [Char] ([Char], [Char])
 -> IO (Either [Char] ([Char], [Char])))
-> Either [Char] ([Char], [Char])
-> IO (Either [Char] ([Char], [Char]))
forall a b. (a -> b) -> a -> b
$ ([Char], [Char]) -> Either [Char] ([Char], [Char])
forall a b. b -> Either a b
Right (([Char], [Char]) -> Either [Char] ([Char], [Char]))
-> ([Char], [Char]) -> Either [Char] ([Char], [Char])
forall a b. (a -> b) -> a -> b
$ Diagram -> DiagramMode -> ([Char], [Char])
diagram2CopilotSpec Diagram
diagramR (DiagramOptions -> DiagramMode
diagramMode DiagramOptions
options)

-- | Options used to customize the conversion of diagrams to Copilot code.
data DiagramOptions = DiagramOptions
  { DiagramOptions -> [Char]
diagramTargetDir   :: FilePath
  , DiagramOptions -> Maybe [Char]
diagramTemplateDir :: Maybe FilePath
  , DiagramOptions -> DiagramFormat
diagramFormat      :: DiagramFormat
  , DiagramOptions -> DiagramPropFormat
diagramPropFormat  :: DiagramPropFormat
  , DiagramOptions -> [Char]
diagramFilename    :: String
  , DiagramOptions -> DiagramMode
diagramMode        :: DiagramMode
  , DiagramOptions -> [Char]
diagramStateVar    :: String
  , DiagramOptions -> [Char]
diagramInputVar    :: String
  }

-- | Property formats supported.
data DiagramPropFormat = Lustre
                       | Inputs
                       | Literal
                       | SMV
  deriving (DiagramPropFormat -> DiagramPropFormat -> Bool
(DiagramPropFormat -> DiagramPropFormat -> Bool)
-> (DiagramPropFormat -> DiagramPropFormat -> Bool)
-> Eq DiagramPropFormat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DiagramPropFormat -> DiagramPropFormat -> Bool
== :: DiagramPropFormat -> DiagramPropFormat -> Bool
$c/= :: DiagramPropFormat -> DiagramPropFormat -> Bool
/= :: DiagramPropFormat -> DiagramPropFormat -> Bool
Eq, Int -> DiagramPropFormat -> [Char] -> [Char]
[DiagramPropFormat] -> [Char] -> [Char]
DiagramPropFormat -> [Char]
(Int -> DiagramPropFormat -> [Char] -> [Char])
-> (DiagramPropFormat -> [Char])
-> ([DiagramPropFormat] -> [Char] -> [Char])
-> Show DiagramPropFormat
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> DiagramPropFormat -> [Char] -> [Char]
showsPrec :: Int -> DiagramPropFormat -> [Char] -> [Char]
$cshow :: DiagramPropFormat -> [Char]
show :: DiagramPropFormat -> [Char]
$cshowList :: [DiagramPropFormat] -> [Char] -> [Char]
showList :: [DiagramPropFormat] -> [Char] -> [Char]
Show)

-- * Error codes

-- | Encoding of reasons why the command can fail.
--
-- The error code used is 1 for user error.
type ErrorCode = Int

-- | Error: the input file cannot be read due to it being unreadable or the
-- format being incorrect.
ecDiagramError :: ErrorCode
ecDiagramError :: Int
ecDiagramError = Int
1

-- | Error: diagram component generation failed during the copy/write
-- process.
ecDiagramTemplateError :: ErrorCode
ecDiagramTemplateError :: Int
ecDiagramTemplateError = Int
2

-- * Result

-- | Process the result of the transformation function.
diagramResult :: FilePath
              -> Either String a
              -> (Maybe a, Result ErrorCode)
diagramResult :: forall a. [Char] -> Either [Char] a -> (Maybe a, Result Int)
diagramResult [Char]
fp Either [Char] a
result = case Either [Char] a
result of
  Left [Char]
msg -> (Maybe a
forall a. Maybe a
Nothing, Int -> [Char] -> Location -> Result Int
forall a. a -> [Char] -> Location -> Result a
Error Int
ecDiagramError [Char]
msg ([Char] -> Location
LocationFile [Char]
fp))
  Right a
t  -> (a -> Maybe a
forall a. a -> Maybe a
Just a
t,  Result Int
forall a. Result a
Success)

-- | Report an error when trying to open or copy the template.
diagramTemplateError :: FilePath
                     -> E.SomeException
                     -> Result ErrorCode
diagramTemplateError :: [Char] -> SomeException -> Result Int
diagramTemplateError [Char]
fp SomeException
exception =
    Int -> [Char] -> Location -> Result Int
forall a. a -> [Char] -> Location -> Result a
Error Int
ecDiagramTemplateError [Char]
msg ([Char] -> Location
LocationFile [Char]
fp)
  where
    msg :: [Char]
msg =
      [Char]
"Diagram monitor generation failed during copy/write operation. Check"
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" that there's free space in the disk and that you have the necessary"
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" permissions to write in the destination directory. "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SomeException -> [Char]
forall a. Show a => a -> [Char]
show SomeException
exception

-- * Handler for boolean expressions in edges or transitions between states.

-- | Return a handler depending on the format used for edge or transition
-- properties.
exprPair :: DiagramPropFormat -> ExprPair
exprPair :: DiagramPropFormat -> ExprPair
exprPair DiagramPropFormat
Lustre = ExprPairT BoolSpec -> ExprPair
forall a. ExprPairT a -> ExprPair
ExprPair (ExprPairT BoolSpec -> ExprPair) -> ExprPairT BoolSpec -> ExprPair
forall a b. (a -> b) -> a -> b
$
  ([Char] -> Either [Char] BoolSpec)
-> ([([Char], [Char])] -> BoolSpec -> BoolSpec)
-> (BoolSpec -> [Char])
-> (BoolSpec -> [[Char]])
-> BoolSpec
-> ExprPairT BoolSpec
forall a.
([Char] -> Either [Char] a)
-> ([([Char], [Char])] -> a -> a)
-> (a -> [Char])
-> (a -> [[Char]])
-> a
-> ExprPairT a
ExprPairT
    ([Token] -> Either [Char] BoolSpec
Lustre.pBoolSpec ([Token] -> Either [Char] BoolSpec)
-> ([Char] -> [Token]) -> [Char] -> Either [Char] BoolSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Token]
Lustre.myLexer)
    (\[([Char], [Char])]
_ -> BoolSpec -> BoolSpec
forall a. a -> a
id)
    BoolSpec -> [Char]
Lustre.boolSpec2Copilot
    BoolSpec -> [[Char]]
Lustre.boolSpecNames
    (Ident -> BoolSpec
Lustre.BoolSpecSignal ([Char] -> Ident
Lustre.Ident [Char]
"undefined"))
exprPair DiagramPropFormat
Inputs = ExprPairT Int -> ExprPair
forall a. ExprPairT a -> ExprPair
ExprPair (ExprPairT Int -> ExprPair) -> ExprPairT Int -> ExprPair
forall a b. (a -> b) -> a -> b
$
  ([Char] -> Either [Char] Int)
-> ([([Char], [Char])] -> Int -> Int)
-> (Int -> [Char])
-> (Int -> [[Char]])
-> Int
-> ExprPairT Int
forall a.
([Char] -> Either [Char] a)
-> ([([Char], [Char])] -> a -> a)
-> (a -> [Char])
-> (a -> [[Char]])
-> a
-> ExprPairT a
ExprPairT
    ((Int -> Either [Char] Int
forall a b. b -> Either a b
Right (Int -> Either [Char] Int)
-> ([Char] -> Int) -> [Char] -> Either [Char] Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Int
forall a. Read a => [Char] -> a
read) :: String -> Either String Int)
    (\[([Char], [Char])]
_ -> Int -> Int
forall a. a -> a
id)
    (\Int
x -> [Char]
"input == " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
x)
    ([[Char]] -> Int -> [[Char]]
forall a b. a -> b -> a
const [])
    (-Int
1)
exprPair DiagramPropFormat
Literal = ExprPairT [Char] -> ExprPair
forall a. ExprPairT a -> ExprPair
ExprPair (ExprPairT [Char] -> ExprPair) -> ExprPairT [Char] -> ExprPair
forall a b. (a -> b) -> a -> b
$
  ([Char] -> Either [Char] [Char])
-> ([([Char], [Char])] -> [Char] -> [Char])
-> ([Char] -> [Char])
-> ([Char] -> [[Char]])
-> [Char]
-> ExprPairT [Char]
forall a.
([Char] -> Either [Char] a)
-> ([([Char], [Char])] -> a -> a)
-> (a -> [Char])
-> (a -> [[Char]])
-> a
-> ExprPairT a
ExprPairT
    [Char] -> Either [Char] [Char]
forall a b. b -> Either a b
Right
    (\[([Char], [Char])]
_ -> [Char] -> [Char]
forall a. a -> a
id)
    [Char] -> [Char]
forall a. a -> a
id
    ([[Char]] -> [Char] -> [[Char]]
forall a b. a -> b -> a
const [])
    [Char]
"undefined"
exprPair DiagramPropFormat
SMV = ExprPairT BoolSpec -> ExprPair
forall a. ExprPairT a -> ExprPair
ExprPair (ExprPairT BoolSpec -> ExprPair) -> ExprPairT BoolSpec -> ExprPair
forall a b. (a -> b) -> a -> b
$
  ([Char] -> Either [Char] BoolSpec)
-> ([([Char], [Char])] -> BoolSpec -> BoolSpec)
-> (BoolSpec -> [Char])
-> (BoolSpec -> [[Char]])
-> BoolSpec
-> ExprPairT BoolSpec
forall a.
([Char] -> Either [Char] a)
-> ([([Char], [Char])] -> a -> a)
-> (a -> [Char])
-> (a -> [[Char]])
-> a
-> ExprPairT a
ExprPairT
    ([Token] -> Either [Char] BoolSpec
SMV.pBoolSpec ([Token] -> Either [Char] BoolSpec)
-> ([Char] -> [Token]) -> [Char] -> Either [Char] BoolSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Token]
SMV.myLexer)
    [([Char], [Char])] -> BoolSpec -> BoolSpec
forall {t :: * -> *}.
Foldable t =>
t ([Char], [Char]) -> BoolSpec -> BoolSpec
substituteBoolExpr
    BoolSpec -> [Char]
SMV.boolSpec2Copilot
    BoolSpec -> [[Char]]
SMV.boolSpecNames
    (Ident -> BoolSpec
SMV.BoolSpecSignal ([Char] -> Ident
SMV.Ident [Char]
"undefined"))

-- * Backend