-- 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 Language.Trans.Diagram2Copilot
    ( DiagramMode(..)
    , diagram2CopilotSpec
    , diagram2Copilot
    )
  where

-- External imports
import Data.List (intercalate, nub, sort)

-- Internal imports: auxiliary
import Data.Diagram (Diagram (..), diagramBadState, diagramFinalState,
                     diagramInitialState)

-- | Modes of operation.
data DiagramMode = CheckState   -- ^ Check if given state matches expectation
                 | ComputeState -- ^ Compute expected state
                 | CheckMoves   -- ^ Check if transitioning to a state would be
                                --   possible.
  deriving (DiagramMode -> DiagramMode -> Bool
(DiagramMode -> DiagramMode -> Bool)
-> (DiagramMode -> DiagramMode -> Bool) -> Eq DiagramMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DiagramMode -> DiagramMode -> Bool
== :: DiagramMode -> DiagramMode -> Bool
$c/= :: DiagramMode -> DiagramMode -> Bool
/= :: DiagramMode -> DiagramMode -> Bool
Eq, Int -> DiagramMode -> ShowS
[DiagramMode] -> ShowS
DiagramMode -> String
(Int -> DiagramMode -> ShowS)
-> (DiagramMode -> String)
-> ([DiagramMode] -> ShowS)
-> Show DiagramMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DiagramMode -> ShowS
showsPrec :: Int -> DiagramMode -> ShowS
$cshow :: DiagramMode -> String
show :: DiagramMode -> String
$cshowList :: [DiagramMode] -> ShowS
showList :: [DiagramMode] -> ShowS
Show)

-- | Convert the diagram into a set of Copilot definitions, and a list of
-- indented trigger definitions to include in the Copilot spec.
diagram2CopilotSpec :: Diagram -> DiagramMode -> (String, String)
diagram2CopilotSpec :: Diagram -> DiagramMode -> (String, String)
diagram2CopilotSpec Diagram
diag DiagramMode
mode = (String
machine, String
triggers)
  where
    machine :: String
machine = [String] -> String
unlines
      [ String
"stateMachineS :: Stream Word8"
      , String
"stateMachineS = stateMachineGF stateMachine1"
      , String
""
      , String
"stateMachineProp :: Stream Bool"
      , String
"stateMachineProp = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
propExpr
      , String
""
      ]
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Diagram -> String
diagram2Copilot Diagram
diag

    -- Elements of the spec.
    propExpr :: String
propExpr = case DiagramMode
mode of
                 DiagramMode
CheckState   -> String
"stateMachineS /= externalState"
                 DiagramMode
ComputeState -> String
"true"
                 DiagramMode
CheckMoves   -> String
"true"

    triggers :: String
triggers = String
"  trigger \"handler\" stateMachineProp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
arguments

    -- Arguments for the handler.
    arguments :: String
arguments = String
"[ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"arg " String -> ShowS
forall a. [a] -> [a] -> [a]
++) [String]
argExprs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ]"

    argExprs :: [String]
argExprs = case DiagramMode
mode of
      DiagramMode
CheckState   -> [ String
"stateMachineS" ]
      DiagramMode
ComputeState -> [ String
"stateMachineS" ]
      DiagramMode
CheckMoves   -> (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall {a}. Show a => a -> String
stateCheckExpr [Int]
states

    stateCheckExpr :: a -> String
stateCheckExpr a
stateId =
      String
"(checkValidTransition transitions externalState " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. Show a => a -> String
show a
stateId String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

    -- States and transitions from the diagram.
    transitions :: [(Int, String, Int)]
transitions = Diagram -> [(Int, String, Int)]
diagramTransitions Diagram
diag
    states :: [Int]
states      = [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Int
x, Int
y] | (Int
x, String
_, Int
y) <- [(Int, String, Int)]
transitions ]

-- | Convert the diagram into a set of Copilot definitions.
diagram2Copilot :: Diagram -> String
diagram2Copilot :: Diagram -> String
diagram2Copilot Diagram
diag = [String] -> String
unlines
    [ String
"stateMachine1 :: ( Word8"
    , String
"                 , Word8"
    , String
"                 , Stream Bool"
    , String
"                 , [(Word8, Stream Bool, Word8)]"
    , String
"                 , Word8"
    , String
"                 )"
    , String
"stateMachine1 ="
    , String
"  (initialState, finalState, noInput, transitions, badState)"
    , String
""
    , String
"-- Check"
    , String
"initialState :: Word8"
    , String
"initialState = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. Show a => a -> String
show Int
initialState
    , String
""
    , String
"-- Check"
    , String
"finalState :: Word8"
    , String
"finalState = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. Show a => a -> String
show Int
finalState
    , String
""
    , String
"noInput :: Stream Bool"
    , String
"noInput = false"
    , String
""
    , String
"badState :: Word8"
    , String
"badState = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. Show a => a -> String
show Int
badState
    , String
""
    , String
"transitions = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showTransitions
    ]

  where

    initialState :: Int
initialState = Diagram -> Int
diagramInitialState Diagram
diag
    finalState :: Int
finalState   = Diagram -> Int
diagramFinalState Diagram
diag
    badState :: Int
badState     = Diagram -> Int
diagramBadState Diagram
diag

    transitions :: [(Int, String, Int)]
transitions = Diagram -> [(Int, String, Int)]
diagramTransitions Diagram
diag

    showTransitions :: String
    showTransitions :: String
showTransitions =
      String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (((Int, String, Int) -> String) -> [(Int, String, Int)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, String, Int) -> String
showTransition [(Int, String, Int)]
transitions) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

    showTransition :: (Int, String, Int) -> String
    showTransition :: (Int, String, Int) -> String
showTransition (Int
a, String
b, Int
c) =
      String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. Show a => a -> String
show Int
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. Show a => a -> String
show Int
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"