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