-- 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
  IORef (Map ())
refStreams <- Map () -> IO (IORef (Map ()))
forall a. a -> IO (IORef a)
newIORef Map ()
forall a. Map a
M.empty
  (Trigger -> IO ()) -> [Trigger] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IORef (Map ()) -> Trigger -> IO ()
analyzeTrigger  IORef (Map ())
refStreams) ([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)
  (Observer -> IO ()) -> [Observer] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IORef (Map ()) -> Observer -> IO ()
analyzeObserver IORef (Map ())
refStreams) ([SpecItem] -> [Observer]
observers ([SpecItem] -> [Observer]) -> [SpecItem] -> [Observer]
forall a b. (a -> b) -> a -> b
$ Spec' a -> [SpecItem]
forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec)
  (Property -> IO ()) -> [Property] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IORef (Map ()) -> Property -> IO ()
analyzeProperty IORef (Map ())
refStreams) ([SpecItem] -> [Property]
properties ([SpecItem] -> [Property]) -> [SpecItem] -> [Property]
forall a b. (a -> b) -> a -> b
$ Spec' a -> [SpecItem]
forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec)
  (Property -> IO ()) -> [Property] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IORef (Map ()) -> Property -> IO ()
analyzeProperty IORef (Map ())
refStreams) (((Property, UProof) -> Property)
-> [(Property, UProof)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (Property, UProof) -> Property
forall a b. (a, b) -> a
fst ([(Property, UProof)] -> [Property])
-> [(Property, UProof)] -> [Property]
forall a b. (a -> b) -> a -> b
$ [SpecItem] -> [(Property, UProof)]
theorems ([SpecItem] -> [(Property, UProof)])
-> [SpecItem] -> [(Property, UProof)]
forall a b. (a -> b) -> a -> b
$ Spec' a -> [SpecItem]
forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec)
  IORef (Map ()) -> Spec' a -> IO ExternEnv
forall a. IORef (Map ()) -> Spec' a -> IO ExternEnv
specExts IORef (Map ())
refStreams Spec' a
spec IO ExternEnv -> (ExternEnv -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ExternEnv -> IO ()
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
  Bool
b <- IORef (Map ()) -> IO Bool
mapCheck IORef (Map ())
refStreams
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (AnalyzeException -> IO ()
forall a e. Exception e => e -> a
throw AnalyzeException
TooMuchRecursion)
  SeenExtern -> Map () -> Stream a -> IO ()
forall b. SeenExtern -> Map () -> Stream b -> IO ()
go SeenExtern
NoExtern Map ()
forall a. Map a
M.empty Stream a
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
    DynStableName
dstn <- Stream b -> IO DynStableName
forall a. a -> IO DynStableName
makeDynStableName Stream b
e0
    Stream b -> DynStableName -> Map () -> IO ()
forall a. Stream a -> DynStableName -> Map () -> IO ()
assertNotVisited Stream b
e0 DynStableName
dstn Map ()
nodes
    let nodes' :: Map ()
nodes' = DynStableName -> () -> Map () -> Map ()
forall a. DynStableName -> a -> Map a -> Map a
M.insert DynStableName
dstn () Map ()
nodes
    case Stream b
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. 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
  Map ()
ref <- IORef (Map ()) -> IO (Map ())
forall a. IORef a -> IO a
readIORef IORef (Map ())
refStreams
  Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Map () -> Int
forall a. Map a -> Int
getSize Map ()
ref Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
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
  Map ()
streams <- IORef (Map ()) -> IO (Map ())
forall a. IORef a -> IO a
readIORef IORef (Map ())
refStreams
  case DynStableName -> Map () -> Maybe ()
forall v. DynStableName -> Map v -> Maybe v
M.lookup DynStableName
dstn Map ()
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. 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. 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. 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. 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. 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. Exception e => e -> a
throw (String -> AnalyzeException
BadFunctionArgType String
name)
        else AnalyzeException -> m (String, t a)
forall a e. 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
  ExternEnv
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)
  ExternEnv
env1 <- (ExternEnv -> Observer -> IO ExternEnv)
-> ExternEnv -> [Observer] -> IO ExternEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ExternEnv -> Observer -> IO ExternEnv
observerExts
            ExternEnv
env0
            ([SpecItem] -> [Observer]
observers ([SpecItem] -> [Observer]) -> [SpecItem] -> [Observer]
forall a b. (a -> b) -> a -> b
$ Spec' a -> [SpecItem]
forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec)
  ExternEnv
env2 <- (ExternEnv -> Property -> IO ExternEnv)
-> ExternEnv -> [Property] -> IO ExternEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ExternEnv -> Property -> IO ExternEnv
propertyExts
            ExternEnv
env1
            ([SpecItem] -> [Property]
properties ([SpecItem] -> [Property]) -> [SpecItem] -> [Property]
forall a b. (a -> b) -> a -> b
$ Spec' a -> [SpecItem]
forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec)
  (ExternEnv -> (Property, UProof) -> IO ExternEnv)
-> ExternEnv -> [(Property, UProof)] -> IO ExternEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ExternEnv -> (Property, UProof) -> IO ExternEnv
theoremExts ExternEnv
env2 ([SpecItem] -> [(Property, UProof)]
theorems ([SpecItem] -> [(Property, UProof)])
-> [SpecItem] -> [(Property, UProof)]
forall a b. (a -> b) -> a -> b
$ Spec' a -> [SpecItem]
forall a. Spec' a -> [SpecItem]
runSpec Spec' a
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
    ExternEnv
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
    (ExternEnv -> Arg -> IO ExternEnv)
-> ExternEnv -> [Arg] -> IO ExternEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
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'')
          ExternEnv
env' [Arg]
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
  Bool
b <- IORef (Map ()) -> IO Bool
mapCheck IORef (Map ())
refStreams
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (AnalyzeException -> IO ()
forall a e. Exception e => e -> a
throw AnalyzeException
TooMuchRecursion)
  Map () -> ExternEnv -> Stream a -> IO ExternEnv
forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
go Map ()
forall a. Map a
M.empty ExternEnv
env_ Stream a
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
    DynStableName
dstn <- Stream b -> IO DynStableName
forall a. a -> IO DynStableName
makeDynStableName Stream b
stream
    Stream b -> DynStableName -> Map () -> IO ()
forall a. Stream a -> DynStableName -> Map () -> IO ()
assertNotVisited Stream b
stream DynStableName
dstn Map ()
nodes

    case Stream b
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 ExternEnv
env' <- Map () -> ExternEnv -> Stream a1 -> IO ExternEnv
forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
go Map ()
nodes ExternEnv
env Stream a1
e1
                                   Map () -> ExternEnv -> Stream b -> IO ExternEnv
forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
go Map ()
nodes ExternEnv
env' Stream b
e2
      Op3 Op3 a1 b c b
_ Stream a1
e1 Stream b
e2 Stream c
e3         -> do ExternEnv
env' <- Map () -> ExternEnv -> Stream a1 -> IO ExternEnv
forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
go Map ()
nodes ExternEnv
env Stream a1
e1
                                   ExternEnv
env'' <- Map () -> ExternEnv -> Stream b -> IO ExternEnv
forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
go Map ()
nodes ExternEnv
env' Stream b
e2
                                   Map () -> ExternEnv -> Stream c -> IO ExternEnv
forall b. Map () -> ExternEnv -> Stream b -> IO ExternEnv
go Map ()
nodes ExternEnv
env'' Stream c
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)