    -- 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
    ")"