    -- 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 :: AnalyzeException -> String
    show AnalyzeException
    DropAppliedToNonAppend = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $  String
    "Drop applied to non-append operation!"
      show AnalyzeException
    DropIndexOverflow      = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $  String
    "Drop index overflow!"
      show AnalyzeException
    ReferentialCycle       = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $  String
    "Referential cycle!"
      show AnalyzeException
    DropMaxViolation       = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $  String
    "Maximum drop violation (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                                      DropIdx -> String
    forall a. Show a => a -> String
    show (DropIdx
    forall a. Bounded a => a
    maxBound :: DropIdx) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")!"
      show AnalyzeException
    NestedArray            = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        String
    "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 AnalyzeException
    TooMuchRecursion       = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        String
    "You have exceeded the limit of " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    maxRecursion String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " 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 AnalyzeException
    InvalidField           = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        String
    "A struct can only take external variables, arrays, or other structs as fields."
      show (DifferentTypes String
    name) = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        String
    "The external symbol \'" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    name String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "\' has been declared to have two different types!"
      show (Redeclared String
    name) = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        String
    "The external symbol \'" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    name String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "\' 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 String
    name) = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        String
    "The function symbol \'" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    name String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "\' has been redeclared to have different number of arguments."
      show (BadFunctionArgType String
    name) = ShowS
    forall a. String -> a
    badUsage ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        String
    "The function symbol \'" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    name String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "\' 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 :: Int
    maxRecursion = Int
    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 :: forall a. Spec' a -> IO ()
    analyze Spec' a
    spec = do
      refStreams <- Map () -> IO (IORef (Map ()))
    forall a. a -> IO (IORef a)
    newIORef Map ()
    forall a. Map a
    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 :: IORef (Map ()) -> Trigger -> IO ()
    analyzeTrigger IORef (Map ())
    refStreams (Trigger String
    _ Stream Bool
    e0 [Arg]
    args) =
      IORef (Map ()) -> Stream Bool -> IO ()
    forall a. IORef (Map ()) -> Stream a -> IO ()
    analyzeExpr IORef (Map ())
    refStreams Stream Bool
    e0 IO () -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (Arg -> IO ()) -> [Arg] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Arg -> IO ()
    analyzeTriggerArg [Arg]
    args

      where
      analyzeTriggerArg :: Arg -> IO ()
      analyzeTriggerArg :: Arg -> IO ()
    analyzeTriggerArg (Arg Stream a
    e) = IORef (Map ()) -> Stream a -> IO ()
    forall a. IORef (Map ()) -> Stream a -> IO ()
    analyzeExpr IORef (Map ())
    refStreams Stream a
    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 :: IORef (Map ()) -> Observer -> IO ()
    analyzeObserver IORef (Map ())
    refStreams (Observer String
    _ Stream a
    e) = IORef (Map ()) -> Stream a -> IO ()
    forall a. IORef (Map ()) -> Stream a -> IO ()
    analyzeExpr IORef (Map ())
    refStreams Stream a
    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 :: IORef (Map ()) -> Property -> IO ()
    analyzeProperty IORef (Map ())
    refStreams (Property String
    _ Prop a
    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.
      IORef (Map ()) -> Stream Bool -> IO ()
    forall a. IORef (Map ()) -> Stream a -> IO ()
    analyzeExpr IORef (Map ())
    refStreams (Prop a -> Stream Bool
    forall a. Prop a -> Stream Bool
    extractProp Prop a
    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 :: forall a. IORef (Map ()) -> Stream a -> IO ()
    analyzeExpr IORef (Map ())
    refStreams Stream a
    s = do
      b <- IORef (Map ()) -> IO Bool
    mapCheck IORef (Map ())
    refStreams
      when b (throw TooMuchRecursion)
      go NoExtern M.empty s

      where
      go :: SeenExtern -> Env -> Stream b -> IO ()
      go :: forall b. SeenExtern -> Map () -> Stream b -> IO ()
    go SeenExtern
    seenExt Map ()
    nodes Stream b
    e0 = do
        dstn <- Stream b -> IO DynStableName
    forall a. a -> IO DynStableName
    makeDynStableName Stream b
    e0
        assertNotVisited e0 dstn nodes
        let nodes' = DynStableName -> () -> Map () -> Map ()
    forall a. DynStableName -> a -> Map a -> Map a
    M.insert DynStableName
    dstn () Map ()
    nodes
        case e0 of
          Append [b]
    _ Maybe (Stream Bool)
    _ Stream b
    e        -> IORef (Map ())
    -> DynStableName
    -> Stream b
    -> ()
    -> (IORef (Map ()) -> Stream b -> IO ())
    -> IO ()
    forall a b.
    IORef (Map ())
    -> DynStableName
    -> Stream a
    -> b
    -> (IORef (Map ()) -> Stream a -> IO b)
    -> IO b
    analyzeAppend IORef (Map ())
    refStreams DynStableName
    dstn Stream b
    e () IORef (Map ()) -> Stream b -> IO ()
    forall a. IORef (Map ()) -> Stream a -> IO ()
    analyzeExpr
          Const b
    _             -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Drop Int
    k Stream b
    e1           -> Int -> Stream b -> IO ()
    forall a. Int -> Stream a -> IO ()
    analyzeDrop (Int -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    k) Stream b
    e1
          Extern String
    _ Maybe [b]
    _          -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Local Stream a1
    e Stream a1 -> Stream b
    f           -> SeenExtern -> Map () -> Stream a1 -> IO ()
    forall b. SeenExtern -> Map () -> Stream b -> IO ()
    go SeenExtern
    seenExt Map ()
    nodes' Stream a1
    e IO () -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                 SeenExtern -> Map () -> Stream b -> IO ()
    forall b. SeenExtern -> Map () -> Stream b -> IO ()
    go SeenExtern
    seenExt Map ()
    nodes' (Stream a1 -> Stream b
    f (String -> Stream a1
    forall a. Typed a => String -> Stream a
    Var String
    "dummy"))
          Var String
    _               -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Op1 Op1 a1 b
    _ Stream a1
    e             -> SeenExtern -> Map () -> Stream a1 -> IO ()
    forall b. SeenExtern -> Map () -> Stream b -> IO ()
    go SeenExtern
    seenExt Map ()
    nodes' Stream a1
    e
          Op2 Op2 a1 b b
    _ Stream a1
    e1 Stream b
    e2         -> SeenExtern -> Map () -> Stream a1 -> IO ()
    forall b. SeenExtern -> Map () -> Stream b -> IO ()
    go SeenExtern
    seenExt Map ()
    nodes' Stream a1
    e1 IO () -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                 SeenExtern -> Map () -> Stream b -> IO ()
    forall b. SeenExtern -> Map () -> Stream b -> IO ()
    go SeenExtern
    seenExt Map ()
    nodes' Stream b
    e2
          Op3 Op3 a1 b c b
    _ Stream a1
    e1 Stream b
    e2 Stream c
    e3      -> SeenExtern -> Map () -> Stream a1 -> IO ()
    forall b. SeenExtern -> Map () -> Stream b -> IO ()
    go SeenExtern
    seenExt Map ()
    nodes' Stream a1
    e1 IO () -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                 SeenExtern -> Map () -> Stream b -> IO ()
    forall b. SeenExtern -> Map () -> Stream b -> IO ()
    go SeenExtern
    seenExt Map ()
    nodes' Stream b
    e2 IO () -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                 SeenExtern -> Map () -> Stream c -> IO ()
    forall b. SeenExtern -> Map () -> Stream b -> IO ()
    go SeenExtern
    seenExt Map ()
    nodes' Stream c
    e3
          Label String
    _ Stream b
    e           -> SeenExtern -> Map () -> Stream b -> IO ()
    forall b. SeenExtern -> Map () -> Stream b -> IO ()
    go SeenExtern
    seenExt Map ()
    nodes' Stream b
    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 :: forall a. Stream a -> DynStableName -> Map () -> IO ()
    assertNotVisited (Append [a]
    _ Maybe (Stream Bool)
    _ Stream a
    _) DynStableName
    _    Map ()
    _     = () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    assertNotVisited Stream a
    _              DynStableName
    dstn Map ()
    nodes =
      case DynStableName -> Map () -> Maybe ()
    forall v. DynStableName -> Map v -> Maybe v
    M.lookup DynStableName
    dstn Map ()
    nodes of
        Just () -> AnalyzeException -> IO ()
    forall a e. (HasCallStack, Exception e) => e -> a
    throw AnalyzeException
    ReferentialCycle
        Maybe ()
    Nothing -> () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | Check that the level of recursion is not above the max recursion allowed.
    mapCheck :: IORef Env -> IO Bool
    mapCheck :: IORef (Map ()) -> IO Bool
    mapCheck IORef (Map ())
    refStreams = do
      ref <- IORef (Map ()) -> IO (Map ())
    forall a. IORef a -> IO a
    readIORef IORef (Map ())
    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 :: forall a b.
    IORef (Map ())
    -> DynStableName
    -> Stream a
    -> b
    -> (IORef (Map ()) -> Stream a -> IO b)
    -> IO b
    analyzeAppend IORef (Map ())
    refStreams DynStableName
    dstn Stream a
    e b
    b IORef (Map ()) -> Stream a -> IO b
    f = do
      streams <- IORef (Map ()) -> IO (Map ())
    forall a. IORef a -> IO a
    readIORef IORef (Map ())
    refStreams
      case M.lookup dstn streams of
        Just () -> b -> IO b
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return b
    b
        Maybe ()
    Nothing -> do
          IORef (Map ()) -> (Map () -> Map ()) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    modifyIORef IORef (Map ())
    refStreams ((Map () -> Map ()) -> IO ()) -> (Map () -> Map ()) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ DynStableName -> () -> Map () -> Map ()
    forall a. DynStableName -> a -> Map a -> Map a
    M.insert DynStableName
    dstn ()
          IORef (Map ()) -> Stream a -> IO b
    f IORef (Map ())
    refStreams Stream a
    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 :: forall a. Int -> Stream a -> IO ()
    analyzeDrop Int
    k (Append [a]
    xs Maybe (Stream Bool)
    _ Stream a
    _)
      | Int
    k Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= [a] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [a]
    xs                         = AnalyzeException -> IO ()
    forall a e. (HasCallStack, Exception e) => e -> a
    throw AnalyzeException
    DropIndexOverflow
      | Int
    k Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > DropIdx -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (DropIdx
    forall a. Bounded a => a
    maxBound :: DropIdx) = AnalyzeException -> IO ()
    forall a e. (HasCallStack, Exception e) => e -> a
    throw AnalyzeException
    DropMaxViolation
      | Bool
    otherwise                              = () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
    analyzeDrop Int
    _ Stream a
    _                            = AnalyzeException -> IO ()
    forall a e. (HasCallStack, Exception e) => e -> a
    throw AnalyzeException
    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
      { ExternEnv -> [(String, SimpleType)]
    externVarEnv  :: [(String, C.SimpleType)]
      , ExternEnv -> [(String, SimpleType)]
    externArrEnv  :: [(String, C.SimpleType)]
      , ExternEnv -> [(String, SimpleType)]
    externStructEnv  :: [(String, C.SimpleType)]
      , ExternEnv -> [(String, [SimpleType])]
    externStructArgs :: [(String, [C.SimpleType])]
      }

    -- | Make sure external variables, functions, arrays, and structs are correctly
    -- typed.
    analyzeExts :: ExternEnv -> IO ()
    analyzeExts :: ExternEnv -> IO ()
    analyzeExts ExternEnv { externVarEnv :: ExternEnv -> [(String, SimpleType)]
    externVarEnv  = [(String, SimpleType)]
    vars
                          , externArrEnv :: ExternEnv -> [(String, SimpleType)]
    externArrEnv  = [(String, SimpleType)]
    arrs
                          , externStructEnv :: ExternEnv -> [(String, SimpleType)]
    externStructEnv  = [(String, SimpleType)]
    datastructs
                          , externStructArgs :: ExternEnv -> [(String, [SimpleType])]
    externStructArgs = [(String, [SimpleType])]
    struct_args }
        = do
        [(String, SimpleType)] -> [(String, SimpleType)] -> IO ()
    forall a b. [(String, a)] -> [(String, b)] -> IO ()
    findDups [(String, SimpleType)]
    vars [(String, SimpleType)]
    arrs

        [(String, SimpleType)] -> [(String, SimpleType)] -> IO ()
    forall a b. [(String, a)] -> [(String, b)] -> IO ()
    findDups [(String, SimpleType)]
    vars [(String, SimpleType)]
    datastructs

        [(String, SimpleType)] -> [(String, SimpleType)] -> IO ()
    forall a b. [(String, a)] -> [(String, b)] -> IO ()
    findDups [(String, SimpleType)]
    arrs [(String, SimpleType)]
    datastructs

        [(String, SimpleType)] -> IO ()
    conflictingTypes [(String, SimpleType)]
    vars
        [(String, SimpleType)] -> IO ()
    conflictingTypes [(String, SimpleType)]
    arrs

        [(String, [SimpleType])] -> IO ()
    funcArgCheck [(String, [SimpleType])]
    struct_args

      where
      findDups :: [(String, a)] -> [(String, b)] -> IO ()
      findDups :: forall a b. [(String, a)] -> [(String, b)] -> IO ()
    findDups [(String, a)]
    ls0 [(String, b)]
    ls1 = ((String, a) -> IO ()) -> [(String, a)] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\(String
    name,a
    _) -> String -> IO ()
    dup String
    name) [(String, a)]
    ls0
        where
        dup :: String -> IO ()
    dup String
    nm = ((String, b) -> IO ()) -> [(String, b)] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ( \(String
    name',b
    _) -> if String
    name' String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    nm
                                         then AnalyzeException -> IO ()
    forall a e. (HasCallStack, Exception e) => e -> a
    throw (String -> AnalyzeException
    Redeclared String
    nm)
                                         else () -> IO ()
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                       ) [(String, b)]
    ls1

      conflictingTypes :: [(String, C.SimpleType)] -> IO ()
      conflictingTypes :: [(String, SimpleType)] -> IO ()
    conflictingTypes [(String, SimpleType)]
    ls =
        let grps :: [[(String, SimpleType)]]
    grps = [(String, SimpleType)] -> [[(String, SimpleType)]]
    forall a. [(String, a)] -> [[(String, a)]]
    groupByPred [(String, SimpleType)]
    ls in
        ([(String, SimpleType)] -> IO ())
    -> [[(String, SimpleType)]] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ [(String, SimpleType)] -> IO ()
    sameType [[(String, SimpleType)]]
    grps
        where
        sameType :: [(String, C.SimpleType)] -> IO ()
        sameType :: [(String, SimpleType)] -> IO ()
    sameType [(String, SimpleType)]
    grp = (String -> SimpleType -> SimpleType -> IO (String, SimpleType))
    -> [(String, SimpleType)] -> IO ()
    forall a.
    (String -> a -> a -> IO (String, a)) -> [(String, a)] -> IO ()
    foldCheck String -> SimpleType -> SimpleType -> IO (String, SimpleType)
    forall {b} {m :: * -> *}.
    (Eq b, Monad m) =>
    String -> b -> b -> m (String, b)
    check [(String, SimpleType)]
    grp
        check :: String -> b -> b -> m (String, b)
    check String
    name b
    c0 b
    c1 = if b
    c0 b -> b -> Bool
    forall a. Eq a => a -> a -> Bool
    == b
    c1 then (String, b) -> m (String, b)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String
    name,b
    c0) -- a dummy---we
                                                             -- discard the result
                             else AnalyzeException -> m (String, b)
    forall a e. (HasCallStack, Exception e) => e -> a
    throw (String -> AnalyzeException
    DifferentTypes String
    name)

      funcArgCheck :: [(String, [C.SimpleType])] -> IO ()
      funcArgCheck :: [(String, [SimpleType])] -> IO ()
    funcArgCheck [(String, [SimpleType])]
    ls =
        let grps :: [[(String, [SimpleType])]]
    grps = [(String, [SimpleType])] -> [[(String, [SimpleType])]]
    forall a. [(String, a)] -> [[(String, a)]]
    groupByPred [(String, [SimpleType])]
    ls in
        ([(String, [SimpleType])] -> IO ())
    -> [[(String, [SimpleType])]] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ [(String, [SimpleType])] -> IO ()
    argCheck [[(String, [SimpleType])]]
    grps
        where
        argCheck :: [(String, [C.SimpleType])] -> IO ()
        argCheck :: [(String, [SimpleType])] -> IO ()
    argCheck [(String, [SimpleType])]
    grp = (String
     -> [SimpleType] -> [SimpleType] -> IO (String, [SimpleType]))
    -> [(String, [SimpleType])] -> IO ()
    forall a.
    (String -> a -> a -> IO (String, a)) -> [(String, a)] -> IO ()
    foldCheck String -> [SimpleType] -> [SimpleType] -> IO (String, [SimpleType])
    forall {t :: * -> *} {a} {m :: * -> *}.
    (Foldable t, Eq (t a), Monad m) =>
    String -> t a -> t a -> m (String, t a)
    check [(String, [SimpleType])]
    grp
        check :: String -> t a -> t a -> m (String, t a)
    check String
    name t a
    args0 t a
    args1 =
          if t a -> Int
    forall a. t a -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length t a
    args0 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == t a -> Int
    forall a. t a -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length t a
    args1
            then if t a
    args0 t a -> t a -> Bool
    forall a. Eq a => a -> a -> Bool
    == t a
    args1
                   then (String, t a) -> m (String, t a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String
    name,t a
    args0) -- a dummy---we discard the
                                            -- result
                   else AnalyzeException -> m (String, t a)
    forall a e. (HasCallStack, Exception e) => e -> a
    throw (String -> AnalyzeException
    BadFunctionArgType String
    name)
            else AnalyzeException -> m (String, t a)
    forall a e. (HasCallStack, Exception e) => e -> a
    throw (String -> AnalyzeException
    BadNumberOfArgs String
    name)

      groupByPred :: [(String, a)] -> [[(String, a)]]
      groupByPred :: forall a. [(String, a)] -> [[(String, a)]]
    groupByPred = ((String, a) -> (String, a) -> Bool)
    -> [(String, a)] -> [[(String, a)]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    groupBy (\(String
    n0,a
    _) (String
    n1,a
    _) -> String
    n0 String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    n1)

      foldCheck :: (String -> a -> a -> IO (String, a)) -> [(String, a)] -> IO ()
      foldCheck :: forall a.
    (String -> a -> a -> IO (String, a)) -> [(String, a)] -> IO ()
    foldCheck String -> a -> a -> IO (String, a)
    check [(String, a)]
    grp =
        ((String, a) -> (String, a) -> IO (String, a))
    -> (String, a) -> [(String, a)] -> IO ()
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m ()
    foldM_ ( \(String
    name, a
    c0) (String
    _, a
    c1) -> String -> a -> a -> IO (String, a)
    check String
    name a
    c0 a
    c1)
               ([(String, a)] -> (String, a)
    forall a. HasCallStack => [a] -> a
    head [(String, a)]
    grp) -- should be typesafe, since this is from groupBy
               [(String, a)]
    grp

    -- | Obtain all the externs in a specification.
    specExts :: IORef Env -> Spec' a -> IO ExternEnv
    specExts :: forall a. IORef (Map ()) -> Spec' a -> IO ExternEnv
    specExts IORef (Map ())
    refStreams Spec' a
    spec = do
      env0 <- (ExternEnv -> Trigger -> IO ExternEnv)
    -> ExternEnv -> [Trigger] -> IO ExternEnv
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM ExternEnv -> Trigger -> IO ExternEnv
    triggerExts
                ([(String, SimpleType)]
    -> [(String, SimpleType)]
    -> [(String, SimpleType)]
    -> [(String, [SimpleType])]
    -> ExternEnv
    ExternEnv [] [] [] [])
                ([SpecItem] -> [Trigger]
    triggers ([SpecItem] -> [Trigger]) -> [SpecItem] -> [Trigger]
    forall a b. (a -> b) -> a -> b
    $ Spec' a -> [SpecItem]
    forall a. Spec' a -> [SpecItem]
    runSpec Spec' a
    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 :: ExternEnv -> Observer -> IO ExternEnv
    observerExts ExternEnv
    env (Observer String
    _ Stream a
    stream) = IORef (Map ()) -> Stream a -> ExternEnv -> IO ExternEnv
    forall a.
    Typed a =>
    IORef (Map ()) -> Stream a -> ExternEnv -> IO ExternEnv
    collectExts IORef (Map ())
    refStreams Stream a
    stream ExternEnv
    env

      triggerExts :: ExternEnv -> Trigger -> IO ExternEnv
      triggerExts :: ExternEnv -> Trigger -> IO ExternEnv
    triggerExts ExternEnv
    env (Trigger String
    _ Stream Bool
    guard [Arg]
    args) = do
        env' <- IORef (Map ()) -> Stream Bool -> ExternEnv -> IO ExternEnv
    forall a.
    Typed a =>
    IORef (Map ()) -> Stream a -> ExternEnv -> IO ExternEnv
    collectExts IORef (Map ())
    refStreams Stream Bool
    guard ExternEnv
    env
        foldM (\ExternEnv
    env'' (Arg Stream a
    arg_) -> IORef (Map ()) -> Stream a -> ExternEnv -> IO ExternEnv
    forall a.
    Typed a =>
    IORef (Map ()) -> Stream a -> ExternEnv -> IO ExternEnv
    collectExts IORef (Map ())
    refStreams Stream a
    arg_ ExternEnv
    env'')
              env' args

      propertyExts :: ExternEnv -> Property -> IO ExternEnv
      propertyExts :: ExternEnv -> Property -> IO ExternEnv
    propertyExts ExternEnv
    env (Property String
    _ Prop a
    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.
        IORef (Map ()) -> Stream Bool -> ExternEnv -> IO ExternEnv
    forall a.
    Typed a =>
    IORef (Map ()) -> Stream a -> ExternEnv -> IO ExternEnv
    collectExts IORef (Map ())
    refStreams (Prop a -> Stream Bool
    forall a. Prop a -> Stream Bool
    extractProp Prop a
    p) ExternEnv
    env

      theoremExts :: ExternEnv -> (Property, UProof) -> IO ExternEnv
      theoremExts :: ExternEnv -> (Property, UProof) -> IO ExternEnv
    theoremExts ExternEnv
    env (Property
    p, UProof
    _) = ExternEnv -> Property -> IO ExternEnv
    propertyExts ExternEnv
    env Property
    p

    -- | Obtain all the externs in a stream.
    collectExts :: C.Typed a => IORef Env -> Stream a -> ExternEnv -> IO ExternEnv
    collectExts :: forall a.
    Typed a =>
    IORef (Map ()) -> Stream a -> ExternEnv -> IO ExternEnv
    collectExts IORef (Map ())
    refStreams Stream a
    stream_ ExternEnv
    env_ = do
      b <- IORef (Map ()) -> IO Bool
    mapCheck IORef (Map ())
    refStreams
      when b (throw TooMuchRecursion)
      go M.empty env_ stream_

      where
      go :: Env -> ExternEnv -> Stream b -> IO ExternEnv
      go :: forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
    go Map ()
    nodes ExternEnv
    env Stream b
    stream = do
        dstn <- Stream b -> IO DynStableName
    forall a. a -> IO DynStableName
    makeDynStableName Stream b
    stream
        assertNotVisited stream dstn nodes

        case stream of
          Append [b]
    _ Maybe (Stream Bool)
    _ Stream b
    e           -> IORef (Map ())
    -> DynStableName
    -> Stream b
    -> ExternEnv
    -> (IORef (Map ()) -> Stream b -> IO ExternEnv)
    -> IO ExternEnv
    forall a b.
    IORef (Map ())
    -> DynStableName
    -> Stream a
    -> b
    -> (IORef (Map ()) -> Stream a -> IO b)
    -> IO b
    analyzeAppend IORef (Map ())
    refStreams DynStableName
    dstn Stream b
    e ExternEnv
    env
                                      (\IORef (Map ())
    refs Stream b
    str -> IORef (Map ()) -> Stream b -> ExternEnv -> IO ExternEnv
    forall a.
    Typed a =>
    IORef (Map ()) -> Stream a -> ExternEnv -> IO ExternEnv
    collectExts IORef (Map ())
    refs Stream b
    str ExternEnv
    env)
          Const b
    _                -> ExternEnv -> IO ExternEnv
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ExternEnv
    env
          Drop Int
    _ Stream b
    e1              -> Map () -> ExternEnv -> Stream b -> IO ExternEnv
    forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
    go Map ()
    nodes ExternEnv
    env Stream b
    e1
          Extern String
    name Maybe [b]
    _          ->
            let ext :: (String, SimpleType)
    ext = ( String
    name, Stream b -> SimpleType
    forall a. Typed a => Stream a -> SimpleType
    getSimpleType Stream b
    stream ) in
            ExternEnv -> IO ExternEnv
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ExternEnv
    env { externVarEnv = ext : externVarEnv env }

          Local Stream a1
    e Stream a1 -> Stream b
    _              -> Map () -> ExternEnv -> Stream a1 -> IO ExternEnv
    forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
    go Map ()
    nodes ExternEnv
    env Stream a1
    e
          Var String
    _                  -> ExternEnv -> IO ExternEnv
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ExternEnv
    env
          Op1 Op1 a1 b
    _ Stream a1
    e                -> Map () -> ExternEnv -> Stream a1 -> IO ExternEnv
    forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
    go Map ()
    nodes ExternEnv
    env Stream a1
    e
          Op2 Op2 a1 b b
    _ Stream a1
    e1 Stream b
    e2            -> do env' <- Map () -> ExternEnv -> Stream a1 -> IO ExternEnv
    forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
    go Map ()
    nodes ExternEnv
    env Stream a1
    e1
                                       go nodes env' e2
          Op3 Op3 a1 b c b
    _ Stream a1
    e1 Stream b
    e2 Stream c
    e3         -> do env' <- Map () -> ExternEnv -> Stream a1 -> IO ExternEnv
    forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
    go Map ()
    nodes ExternEnv
    env Stream a1
    e1
                                       env'' <- go nodes env' e2
                                       go nodes env'' e3
          Label String
    _ Stream b
    e              -> Map () -> ExternEnv -> Stream b -> IO ExternEnv
    forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
    go Map ()
    nodes ExternEnv
    env Stream b
    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 :: forall a. Typed a => Stream a -> SimpleType
    getSimpleType Stream a
    _ = Type a -> SimpleType
    forall a. Typed a => Type a -> SimpleType
    C.simpleType (Type a
    forall a. Typed a => Type a
    C.typeOf :: C.Type a)