content: -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
  
  {-# LANGUAGE DeriveDataTypeable  #-}
  {-# LANGUAGE GADTs               #-}
  {-# LANGUAGE Safe                #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  -- | Copilot specification sanity check.
  
  module Copilot.Language.Analyze
    ( AnalyzeException (..)
    , analyze
    ) where
  
  import Copilot.Core (DropIdx)
  import qualified Copilot.Core as C
  import Copilot.Language.Stream (Stream (..))
  import Copilot.Language.Spec
  import Copilot.Language.Error (badUsage)
  import Copilot.Theorem.Prove (UProof)
  
  import Data.List (groupBy)
  import Data.IORef
  import Data.Typeable
  import System.Mem.StableName.Dynamic
  import System.Mem.StableName.Map (Map(..))
  import qualified System.Mem.StableName.Map as M
  import Control.Monad (when, foldM_, foldM)
  import Control.Exception (Exception, throw)
  
  -- | Exceptions or kinds of errors in Copilot specifications that the analysis
  -- implemented is able to detect.
  data AnalyzeException
    = DropAppliedToNonAppend
    | DropIndexOverflow
    | ReferentialCycle
    | DropMaxViolation
    | NestedArray
    | TooMuchRecursion
    | InvalidField
    | DifferentTypes String
    | Redeclared String
    | BadNumberOfArgs String
    | BadFunctionArgType String
    deriving Typeable
  
  -- | Show instance that prints a detailed message for each kind of exception.
  instance Show AnalyzeException where
    show DropAppliedToNonAppend = badUsage $  "Drop applied to non-append operation!"
    show DropIndexOverflow      = badUsage $  "Drop index overflow!"
    show ReferentialCycle       = badUsage $  "Referential cycle!"
    show DropMaxViolation       = badUsage $  "Maximum drop violation (" ++
                                    show (maxBound :: DropIdx) ++ ")!"
    show NestedArray            = badUsage $
      "An external function cannot take another external function or external array as an argument.  Try defining a stream, and using the stream values in the other definition."
    show TooMuchRecursion       = badUsage $
      "You have exceeded the limit of " ++ show maxRecursion ++ " recursive calls in a stream definition.  Likely, you have accidently defined a circular stream, such as 'x = x'.  Another possibility is you have defined a a polymorphic function with type constraints that references other streams.  For example,\n\n  nats :: (Typed a, Num a) => Stream a\n  nats = [0] ++ nats + 1\n\nis not allowed.  Make the definition monomorphic, or add a level of indirection, like \n\n  nats :: (Typed a, Num a) => Stream a\n  nats = n\n    where\n      n = [0] ++ n + 1\n\nFinally, you may have intended to generate a very large expression.  You can try shrinking the expression by using local variables.  It all else fails, you can increase the maximum size of ecursive calls by modifying 'maxRecursion' in copilot-language."
    show InvalidField           = badUsage $
      "A struct can only take external variables, arrays, or other structs as fields."
    show (DifferentTypes name) = badUsage $
      "The external symbol \'" ++ name ++ "\' has been declared to have two different types!"
    show (Redeclared name) = badUsage $
      "The external symbol \'" ++ name ++ "\' has been redeclared to be a different symbol (e.g., a variable and an array, or a variable and a funciton symbol, etc.)."
    show (BadNumberOfArgs name) = badUsage $
      "The function symbol \'" ++ name ++ "\' has been redeclared to have different number of arguments."
    show (BadFunctionArgType name) = badUsage $
      "The function symbol \'" ++ name ++ "\' has been redeclared to an argument with different types."
  
  -- | 'Exception' instance so we can throw and catch 'AnalyzeExcetion's.
  instance Exception AnalyzeException
  
  -- | Max level of recursion supported. Any level above this constant
  -- will result in a 'TooMuchRecursion' exception.
  maxRecursion :: Int
  maxRecursion = 100000
  
  -- | An environment that contains the nodes visited.
  type Env = Map ()
  
  -- | Analyze a Copilot specification and report any errors detected.
  --
  -- This function can fail with one of the exceptions in 'AnalyzeException'.
  analyze :: Spec' a -> IO ()
  analyze spec = do
    refStreams <- newIORef M.empty
    mapM_ (analyzeTrigger  refStreams) (triggers  $ runSpec spec)
    mapM_ (analyzeObserver refStreams) (observers $ runSpec spec)
    mapM_ (analyzeProperty refStreams) (properties $ runSpec spec)
    mapM_ (analyzeProperty refStreams) (map fst $ theorems $ runSpec spec)
    specExts refStreams spec >>= analyzeExts
  
  -- | Analyze a Copilot trigger and report any errors detected.
  --
  -- This function can fail with one of the exceptions in 'AnalyzeException'.
  analyzeTrigger :: IORef Env -> Trigger -> IO ()
  analyzeTrigger refStreams (Trigger _ e0 args) =
    analyzeExpr refStreams e0 >> mapM_ analyzeTriggerArg args
  
    where
    analyzeTriggerArg :: Arg -> IO ()
    analyzeTriggerArg (Arg e) = analyzeExpr refStreams e
  
  -- | Analyze a Copilot observer and report any errors detected.
  --
  -- This function can fail with one of the exceptions in 'AnalyzeException'.
  analyzeObserver :: IORef Env -> Observer -> IO ()
  analyzeObserver refStreams (Observer _ e) = analyzeExpr refStreams e
  
  -- | Analyze a Copilot property and report any errors detected.
  --
  -- This function can fail with one of the exceptions in 'AnalyzeException'.
  analyzeProperty :: IORef Env -> Property -> IO ()
  analyzeProperty refStreams (Property _ p) =
    -- Soundness note: it is OK to call `extractProp` here to drop the quantifier
    -- from the proposition `p`, as the analysis does not depend on what the
    -- quantifier is.
    analyzeExpr refStreams (extractProp p)
  
  data SeenExtern = NoExtern
                  | SeenFun
                  | SeenArr
                  | SeenStruct
  
  -- | Analyze a Copilot stream and report any errors detected.
  --
  -- This function can fail with one of the exceptions in 'AnalyzeException'.
  analyzeExpr :: IORef Env -> Stream a -> IO ()
  analyzeExpr refStreams s = do
    b <- mapCheck refStreams
    when b (throw TooMuchRecursion)
    go NoExtern M.empty s
  
    where
    go :: SeenExtern -> Env -> Stream b -> IO ()
    go seenExt nodes e0 = do
      dstn <- makeDynStableName e0
      assertNotVisited e0 dstn nodes
      let nodes' = M.insert dstn () nodes
      case e0 of
        Append _ _ e        -> analyzeAppend refStreams dstn e () analyzeExpr
        Const _             -> return ()
        Drop k e1           -> analyzeDrop (fromIntegral k) e1
        Extern _ _          -> return ()
        Local e f           -> go seenExt nodes' e >>
                               go seenExt nodes' (f (Var "dummy"))
        Var _               -> return ()
        Op1 _ e             -> go seenExt nodes' e
        Op2 _ e1 e2         -> go seenExt nodes' e1 >>
                               go seenExt nodes' e2
        Op3 _ e1 e2 e3      -> go seenExt nodes' e1 >>
                               go seenExt nodes' e2 >>
                               go seenExt nodes' e3
        Label _ e           -> go seenExt nodes' e
  
  -- | Detect whether the given stream name has already been visited.
  --
  -- This function throws a 'ReferentialCycle' exception if the second argument
  -- represents a name that has already been visited.
  assertNotVisited :: Stream a -> DynStableName -> Env -> IO ()
  assertNotVisited (Append _ _ _) _    _     = return ()
  assertNotVisited _              dstn nodes =
    case M.lookup dstn nodes of
      Just () -> throw ReferentialCycle
      Nothing -> return ()
  
  -- | Check that the level of recursion is not above the max recursion allowed.
  mapCheck :: IORef Env -> IO Bool
  mapCheck refStreams = do
    ref <- readIORef refStreams
    return $ getSize ref > maxRecursion
  
  -- | Analyze a Copilot stream append and report any errors detected.
  analyzeAppend ::
       IORef Env -> DynStableName -> Stream a -> b
    -> (IORef Env -> Stream a -> IO b) -> IO b
  analyzeAppend refStreams dstn e b f = do
    streams <- readIORef refStreams
    case M.lookup dstn streams of
      Just () -> return b
      Nothing -> do
        modifyIORef refStreams $ M.insert dstn ()
        f refStreams e
  
  -- | Analyze a Copilot stream drop and report any errors detected.
  --
  -- This function can fail if the drop is exercised over a stream that is not an
  -- append, or if the length of the drop is larger than that of the subsequent
  -- append.
  analyzeDrop :: Int -> Stream a -> IO ()
  analyzeDrop k (Append xs _ _)
    | k >= length xs                         = throw DropIndexOverflow
    | k > fromIntegral (maxBound :: DropIdx) = throw DropMaxViolation
    | otherwise                              = return ()
  analyzeDrop _ _                            = throw DropAppliedToNonAppend
  
  -- Analyzing external variables.  We check that every reference to an external
  -- variable has the same type, and for external functions, they have the same
  -- typed arguments.
  
  -- | An environment to store external variables, arrays, functions and structs,
  -- so that we can check types in the expression---e.g., if we declare the same
  -- external to have two different types.
  data ExternEnv = ExternEnv
    { externVarEnv  :: [(String, C.SimpleType)]
    , externArrEnv  :: [(String, C.SimpleType)]
    , externStructEnv  :: [(String, C.SimpleType)]
    , externStructArgs :: [(String, [C.SimpleType])]
    }
  
  -- | Make sure external variables, functions, arrays, and structs are correctly
  -- typed.
  analyzeExts :: ExternEnv -> IO ()
  analyzeExts ExternEnv { externVarEnv  = vars
                        , externArrEnv  = arrs
                        , externStructEnv  = datastructs
                        , externStructArgs = struct_args }
      = do
      findDups vars arrs
  
      findDups vars datastructs
  
      findDups arrs datastructs
  
      conflictingTypes vars
      conflictingTypes arrs
  
      funcArgCheck struct_args
  
    where
    findDups :: [(String, a)] -> [(String, b)] -> IO ()
    findDups ls0 ls1 = mapM_ (\(name,_) -> dup name) ls0
      where
      dup nm = mapM_ ( \(name',_) -> if name' == nm
                                       then throw (Redeclared nm)
                                       else return ()
                     ) ls1
  
    conflictingTypes :: [(String, C.SimpleType)] -> IO ()
    conflictingTypes ls =
      let grps = groupByPred ls in
      mapM_ sameType grps
      where
      sameType :: [(String, C.SimpleType)] -> IO ()
      sameType grp = foldCheck check grp
      check name c0 c1 = if c0 == c1 then return (name,c0) -- a dummy---we
                                                           -- discard the result
                           else throw (DifferentTypes name)
  
    funcArgCheck :: [(String, [C.SimpleType])] -> IO ()
    funcArgCheck ls =
      let grps = groupByPred ls in
      mapM_ argCheck grps
      where
      argCheck :: [(String, [C.SimpleType])] -> IO ()
      argCheck grp = foldCheck check grp
      check name args0 args1 =
        if length args0 == length args1
          then if args0 == args1
                 then return (name,args0) -- a dummy---we discard the
                                          -- result
                 else throw (BadFunctionArgType name)
          else throw (BadNumberOfArgs name)
  
    groupByPred :: [(String, a)] -> [[(String, a)]]
    groupByPred = groupBy (\(n0,_) (n1,_) -> n0 == n1)
  
    foldCheck :: (String -> a -> a -> IO (String, a)) -> [(String, a)] -> IO ()
    foldCheck check grp =
      foldM_ ( \(name, c0) (_, c1) -> check name c0 c1)
             (head grp) -- should be typesafe, since this is from groupBy
             grp
  
  -- | Obtain all the externs in a specification.
  specExts :: IORef Env -> Spec' a -> IO ExternEnv
  specExts refStreams spec = do
    env0 <- foldM triggerExts
              (ExternEnv [] [] [] [])
              (triggers $ runSpec spec)
    env1 <- foldM observerExts
              env0
              (observers $ runSpec spec)
    env2 <- foldM propertyExts
              env1
              (properties $ runSpec spec)
    foldM theoremExts env2 (theorems $ runSpec spec)
  
    where
    observerExts :: ExternEnv -> Observer -> IO ExternEnv
    observerExts env (Observer _ stream) = collectExts refStreams stream env
  
    triggerExts :: ExternEnv -> Trigger -> IO ExternEnv
    triggerExts env (Trigger _ guard args) = do
      env' <- collectExts refStreams guard env
      foldM (\env'' (Arg arg_) -> collectExts refStreams arg_ env'')
            env' args
  
    propertyExts :: ExternEnv -> Property -> IO ExternEnv
    propertyExts env (Property _ p) =
      -- Soundness note: it is OK to call `extractProp` here to drop the
      -- quantifier from the proposition `p`. This is because we are simply
      -- gathering externs from `p`, and the presence of externs does not depend
      -- on what the quantifier is.
      collectExts refStreams (extractProp p) env
  
    theoremExts :: ExternEnv -> (Property, UProof) -> IO ExternEnv
    theoremExts env (p, _) = propertyExts env p
  
  -- | Obtain all the externs in a stream.
  collectExts :: C.Typed a => IORef Env -> Stream a -> ExternEnv -> IO ExternEnv
  collectExts refStreams stream_ env_ = do
    b <- mapCheck refStreams
    when b (throw TooMuchRecursion)
    go M.empty env_ stream_
  
    where
    go :: Env -> ExternEnv -> Stream b -> IO ExternEnv
    go nodes env stream = do
      dstn <- makeDynStableName stream
      assertNotVisited stream dstn nodes
  
      case stream of
        Append _ _ e           -> analyzeAppend refStreams dstn e env
                                    (\refs str -> collectExts refs str env)
        Const _                -> return env
        Drop _ e1              -> go nodes env e1
        Extern name _          ->
          let ext = ( name, getSimpleType stream ) in
          return env { externVarEnv = ext : externVarEnv env }
  
        Local e _              -> go nodes env e
        Var _                  -> return env
        Op1 _ e                -> go nodes env e
        Op2 _ e1 e2            -> do env' <- go nodes env e1
                                     go nodes env' e2
        Op3 _ e1 e2 e3         -> do env' <- go nodes env e1
                                     env'' <- go nodes env' e2
                                     go nodes env'' e3
        Label _ e              -> go nodes env e
  
  -- | Return the simple C type representation of the type of the values carried
  -- by a stream.
  getSimpleType :: forall a. C.Typed a => Stream a -> C.SimpleType
  getSimpleType _ = C.simpleType (C.typeOf :: C.Type a)
  