    -- 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.
    --
    -- | Formal analysis of diagrams.
    module Data.Diagram.Analysis
        ( analyzeDiagram
        , AnalysisResult(..)
        )
      where

    -- External imports
    import qualified Copilot.Core as Core

    -- Internal imports: auxiliary
    import Copilot.Core.Analysis          (exprIsConstant)
    import Copilot.Language.Reify.Extra   (reifySpec)
    import Data.Diagram                   (Diagram (..),
                                           diagramNumStates)
    import Language.Trans.Diagram2Copilot (diagram2Copilot)

    -- * Analysis of Specs

    -- | Result of analyzing a diagram.
    data AnalysisResult = AnalysisResult
      { AnalysisResult -> Int
    numStates     :: Int  -- ^ Number of states in the diagram.
      , AnalysisResult -> Bool
    deterministic :: Bool -- ^ True if the diagram is deterministic.
      }

    -- | Formally analyze a diagram.
    analyzeDiagram :: Diagram -> IO AnalysisResult
    analyzeDiagram :: Diagram -> IO AnalysisResult
    analyzeDiagram Diagram
    diagram = do

      let nStates :: Int
    nStates = Diagram -> Int
    diagramNumStates Diagram
    diagram

      coreSpec <- [(String, Maybe String)] -> String -> IO Spec
    reifySpec [(String, Maybe String)]
    defaultSpecImports (String -> IO Spec) -> String -> IO Spec
    forall a b. (a -> b) -> a -> b
    $ Diagram -> String
    showDiagram Diagram
    diagram

      let properties     = [String] -> [Expr Bool] -> [(String, Expr Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [String
    "deterministic"] [Expr Bool]
    propertyGuards
          propertyGuards = (Trigger -> Expr Bool) -> [Trigger] -> [Expr Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map Trigger -> Expr Bool
    Core.triggerGuard ([Trigger] -> [Expr Bool]) -> [Trigger] -> [Expr Bool]
    forall a b. (a -> b) -> a -> b
    $ Spec -> [Trigger]
    Core.specTriggers Spec
    coreSpec

      constantProperties <- mapM (uncurry $ exprIsConstant coreSpec) properties

      let numTrue = [(Bool, Bool)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([(Bool, Bool)] -> Int) -> [(Bool, Bool)] -> Int
    forall a b. (a -> b) -> a -> b
    $ ((Bool, Bool) -> Bool) -> [(Bool, Bool)] -> [(Bool, Bool)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool, Bool) -> Bool
    forall a b. (a, b) -> a
    fst [(Bool, Bool)]
    constantProperties

      let diagramDeterministic = Int
    numTrue Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0

      return $ AnalysisResult nStates diagramDeterministic

    -- | Default imports for a 'Spec' that was converted into a 'Copilot.Spec'.
    defaultSpecImports :: [(String, Maybe String)]
    defaultSpecImports :: [(String, Maybe String)]
    defaultSpecImports =
      [ (String
    "Control.Monad.Writer",  Maybe String
    forall a. Maybe a
    Nothing)
      , (String
    "Copilot.Language",      Maybe String
    forall a. Maybe a
    Nothing)
      , (String
    "Copilot.Language.Spec", Maybe String
    forall a. Maybe a
    Nothing)
      , (String
    "Data.Functor.Identity", Maybe String
    forall a. Maybe a
    Nothing)
      , (String
    "Data.List",             String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "L")
      , (String
    "Prelude",               String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "P")
      ]

    -- | Render a 'Diagram' as a Haskell definition of a 'Copilot.Spec'.
    --
    -- The shown 'Copilot.Spec' has a top-level triggers for the properties we are
    -- interested in, as well as several auxiliary definitions.
    showDiagram :: Diagram -> String
    showDiagram :: Diagram -> String
    showDiagram Diagram
    diagram = [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $
           [ String
    "do let" ]
        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    "       " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> [String]
    lines String
    auxiliaryDefinitions)
        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    "       " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> [String]
    lines String
    input)
        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    "       " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> [String]
    lines String
    diagramDefinitions)
        [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "   trigger \"deterministic\" (isDeterministic stateMachine1) []" ]

      where

        input :: String
    input = [String] -> String
    unlines
          [ String
    "input :: Stream Word8"
          , String
    "input = extern \"input\" Nothing"
          ]

        diagramDefinitions :: String
    diagramDefinitions = Diagram -> String
    diagram2Copilot Diagram
    diagram

    -- | Auxiliary definitions needed in the spec.
    auxiliaryDefinitions :: String
    auxiliaryDefinitions :: String
    auxiliaryDefinitions = [String] -> String
    unlines
      [ String
    "stateMachine :: (Eq a, Typed a)"
      , String
    "             => (a, a, Stream Bool, [(a, Stream Bool, a)], a)"
      , String
    "             -> Stream a"
      , String
    "stateMachine (initial, final, noInputData, transitions, bad) ="
      , String
    "    state"
      , String
    "  where"
      , String
    "    state         = ifThenElses transitions"
      , String
    "    previousState = [initial] ++ state"
      , String
    ""
      , String
    "    -- ifThenElses :: [(a, Stream Bool, a)] -> Stream a"
      , String
    "    ifThenElses [] ="
      , String
    "      ifThenElse"
      , String
    "        (previousState == constant final && noInputData)"
      , String
    "        (constant final)"
      , String
    "        (constant bad)"
      , String
    ""
      , String
    "    ifThenElses ((s1, i, s2):ss) ="
      , String
    "      ifThenElse"
      , String
    "        (previousState == constant s1 && i)"
      , String
    "        (constant s2)"
      , String
    "        (ifThenElses ss)"
      , String
    ""
      , String
    "isDeterministic :: (Ord a, Eq a, Typed a)"
      , String
    "                => (a, a, Stream Bool, [(a, Stream Bool, a)], a)"
      , String
    "                -> Stream Bool"
      , String
    "isDeterministic (_, _, _, ts, _) = all $"
      , String
    "    map"
      , String
    "      (\\s -> all (map not $ pairwise $ transitionsFrom s))"
      , String
    "      states"
      , String
    "  where"
      , String
    "    states = L.nub $ L.sort $ concat $"
      , String
    "      map (\\(s1, _, s2) -> [s1, s2]) ts"
      , String
    ""
      , String
    "    transitionsFrom s = [ t | (s1, t, _) <- ts, s P.== s1 ]"
      , String
    ""
      , String
    "completeMachine :: (Ord a, Eq a, Typed a)"
      , String
    "                => (a, a, Stream Bool, [(a, Stream Bool, a)], a)"
      , String
    "                -> Stream Bool"
      , String
    "completeMachine (_, _, _, ts, _) = all $"
      , String
    "    map (\\s -> or $ transitionsFrom s) states"
      , String
    "  where"
      , String
    "    states = L.nub $ L.sort $ concat $"
      , String
    "      map (\\(s1, _, s2) -> [s1, s2]) ts"
      , String
    "    transitionsFrom s = [ t | (s1, t, _) <- ts, s P.== s1 ]"
      , String
    ""
      , String
    "all [] = true"
      , String
    "all (x:xs) = x && all xs"
      , String
    ""
      , String
    "or [] = false"
      , String
    "or (x:xs) = x || or xs"
      , String
    ""
      , String
    "pairwise :: [ Stream Bool ] -> [ Stream Bool ]"
      , String
    "pairwise []      = []"
      , String
    "pairwise (x:[])  = []"
      , String
    "pairwise (x1:xs) ="
      , String
    "  (map (\\x2 -> (x1 && x2)) xs) P.++ pairwise xs"
      ]