-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.

-- | A tagless interpreter for Copilot specifications.

{-# LANGUAGE BangPatterns        #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE Safe                #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Copilot.Interpret.Eval
  ( Env
  , Output
  , ExecTrace (..)
  , eval
  , ShowType (..)
  ) where

import Copilot.Core            (Expr (..), Field (..), Id, Name, Observer (..),
                                Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),
                                Trigger (..), Type (..), UExpr (..), Value (..),
				arrayElems, arrayUpdate, specObservers,
                                specStreams, specTriggers, updateField)
import Copilot.Interpret.Error (badUsage)

import           Prelude hiding (id)
import qualified Prelude as P

import Control.Exception (Exception, throw)
import Data.Bits         (complement, shiftL, shiftR, xor, (.&.), (.|.))
import Data.Dynamic      (Dynamic, fromDynamic, toDyn)
import Data.List         (transpose)
import Data.Maybe        (fromJust)
import Data.Typeable     (Typeable)
import GHC.TypeLits      (KnownNat, Nat, natVal)

-- | Exceptions that may be thrown during interpretation of a Copilot
-- specification.
data InterpException
  = ArrayWrongSize Name Int           -- ^ Extern array has incorrect size.
  | ArrayIdxOutofBounds Name Int Int  -- ^ Index out-of-bounds exception.
  | DivideByZero                      -- ^ Division by zero.
  | NotEnoughValues Name Int          -- ^ For one or more streams, not enough
                                      --   values are available to simulate the
                                      --   number of steps requested.
  | NoExtsInterp Name                 -- ^ One of the externs used by the
                                      --   specification does not declare
                                      --   sample values to be used during
                                      --   simulation.
  deriving Typeable

-- | Show a descriptive message of the exception.
instance Show InterpException where
  ---------------------------------------
  show :: InterpException -> String
show (ArrayWrongSize String
name Int
expectedSize)                                      =
    ShowS
forall a. String -> a
badUsage ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"in the environment for external array " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", we expect a list of length " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
expectedSize
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", but the length of the array you supplied is of a different length."
  ---------------------------------------
  show (ArrayIdxOutofBounds String
name Int
index Int
size)                                   =
    ShowS
forall a. String -> a
badUsage ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"in the environment for external array " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", you gave an index of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
index
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" where the size of the array is " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
size String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"; the size must "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" be strictly greater than the index."
  ---------------------------------------
  show InterpException
DivideByZero                                                            =
    ShowS
forall a. String -> a
badUsage String
"divide by zero."
  ---------------------------------------
  show (NotEnoughValues String
name Int
k)                                                =
    ShowS
forall a. String -> a
badUsage ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"on the " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"th iteration, we ran out of "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"values for simulating the external element " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
  ---------------------------------------
  show (NoExtsInterp String
name)                                                     =
    ShowS
forall a. String -> a
badUsage ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"in a call of external symbol " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", you did not "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"provide an expression for interpretation.  In your external "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"declaration, you need to provide a 'Just strm', where 'strm' is "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"some stream with which to simulate the function."
  ---------------------------------------

-- | Allow throwing and catching 'InterpException' using Haskell's standard
-- exception mechanisms.
instance Exception InterpException

-- | An environment that contains an association between (stream or extern)
-- names and their values.
type Env nm = [(nm, Dynamic)]

-- | The simulation output is defined as a string. Different backends may
-- choose to format their results differently.
type Output = String

-- | An execution trace, containing the traces associated to each individual
-- monitor trigger and observer.
data ExecTrace = ExecTrace
  { ExecTrace -> [(String, [Maybe [String]])]
interpTriggers  :: [(String, [Maybe [Output]])]

    -- ^ Map from trigger names to their optional output, which is a list of
    -- strings representing their values. The output may be 'Nothing' if the
    -- guard for the trigger was false. The order is important, since we
    -- compare the arg lists between the interpreter and backends.

  , ExecTrace -> [(String, [String])]
interpObservers :: [(String, [Output])]
    -- ^ Map from observer names to their outputs.
  }
  deriving Int -> ExecTrace -> ShowS
[ExecTrace] -> ShowS
ExecTrace -> String
(Int -> ExecTrace -> ShowS)
-> (ExecTrace -> String)
-> ([ExecTrace] -> ShowS)
-> Show ExecTrace
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExecTrace -> ShowS
showsPrec :: Int -> ExecTrace -> ShowS
$cshow :: ExecTrace -> String
show :: ExecTrace -> String
$cshowList :: [ExecTrace] -> ShowS
showList :: [ExecTrace] -> ShowS
Show

-- We could write this in a beautiful lazy style like above, but that creates a
-- space leak in the interpreter that is hard to fix while maintaining laziness.
-- We take a more brute-force appraoch below.

-- | Evaluate a specification for a number of steps.
eval :: ShowType   -- ^ Show booleans as @0@\/@1@ (C) or @True@\/@False@
                   --   (Haskell).
     -> Int        -- ^ Number of steps to evaluate.
     -> Spec       -- ^ Specification to evaluate.
     -> ExecTrace
eval :: ShowType -> Int -> Spec -> ExecTrace
eval ShowType
showType Int
k Spec
spec =

  let initStrms :: [(Int, Dynamic)]
initStrms = (Stream -> (Int, Dynamic)) -> [Stream] -> [(Int, Dynamic)]
forall a b. (a -> b) -> [a] -> [b]
map Stream -> (Int, Dynamic)
initStrm (Spec -> [Stream]
specStreams Spec
spec)             in

  let strms :: [(Int, Dynamic)]
strms = Int -> [Stream] -> [(Int, Dynamic)] -> [(Int, Dynamic)]
evalStreams Int
k (Spec -> [Stream]
specStreams Spec
spec) [(Int, Dynamic)]
initStrms      in

  let trigs :: [[Maybe [String]]]
trigs = (Trigger -> [Maybe [String]]) -> [Trigger] -> [[Maybe [String]]]
forall a b. (a -> b) -> [a] -> [b]
map (ShowType -> Int -> [(Int, Dynamic)] -> Trigger -> [Maybe [String]]
evalTrigger ShowType
showType Int
k [(Int, Dynamic)]
strms)
                  (Spec -> [Trigger]
specTriggers Spec
spec)                         in

  let obsvs :: [[String]]
obsvs = (Observer -> [String]) -> [Observer] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (ShowType -> Int -> [(Int, Dynamic)] -> Observer -> [String]
evalObserver ShowType
showType Int
k [(Int, Dynamic)]
strms)
                  (Spec -> [Observer]
specObservers Spec
spec)                        in

  [(Int, Dynamic)]
strms [(Int, Dynamic)] -> ExecTrace -> ExecTrace
forall a b. a -> b -> b
`seq` ExecTrace
                { interpTriggers :: [(String, [Maybe [String]])]
interpTriggers  =
                    [String] -> [[Maybe [String]]] -> [(String, [Maybe [String]])]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Trigger -> String) -> [Trigger] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Trigger -> String
triggerName  (Spec -> [Trigger]
specTriggers  Spec
spec)) [[Maybe [String]]]
trigs
                , interpObservers :: [(String, [String])]
interpObservers =
                    [String] -> [[String]] -> [(String, [String])]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Observer -> String) -> [Observer] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Observer -> String
observerName (Spec -> [Observer]
specObservers Spec
spec)) [[String]]
obsvs
                }

-- | An environment that contains an association between (stream or extern)
-- names and their values.
type LocalEnv = [(Name, Dynamic)]

-- | Evaluate an expression for a number of steps, obtaining the value
-- of the sample at that time.
evalExpr_ :: Typeable a => Int -> Expr a -> LocalEnv -> Env Id -> a
evalExpr_ :: forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr a
e0 LocalEnv
locs [(Int, Dynamic)]
strms = case Expr a
e0 of
  Const Type a
_ a
x                          -> a
x
  Drop Type a
t DropIdx
i Int
id                        ->
    let Just [a]
buff = Int -> [(Int, Dynamic)] -> Maybe Dynamic
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
id [(Int, Dynamic)]
strms Maybe Dynamic -> (Dynamic -> Maybe [a]) -> Maybe [a]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Dynamic -> Maybe [a]
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic in
    [a] -> [a]
forall a. [a] -> [a]
reverse [a]
buff [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! (DropIdx -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral DropIdx
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k)
  Local Type a1
t1 Type a
_ String
name Expr a1
e1 Expr a
e2              ->
    let x :: a1
x     = Int -> Expr a1 -> LocalEnv -> [(Int, Dynamic)] -> a1
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr a1
e1 LocalEnv
locs [(Int, Dynamic)]
strms in
    let locs' :: LocalEnv
locs' = (String
name, a1 -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a1
x) (String, Dynamic) -> LocalEnv -> LocalEnv
forall a. a -> [a] -> [a]
: LocalEnv
locs  in
    a1
x a1 -> a -> a
forall a b. a -> b -> b
`seq` LocalEnv
locs' LocalEnv -> a -> a
forall a b. a -> b -> b
`seq` Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr a
e2  LocalEnv
locs' [(Int, Dynamic)]
strms
  Var Type a
t String
name                         -> Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe a -> a) -> Maybe a -> a
forall a b. (a -> b) -> a -> b
$ String -> LocalEnv -> Maybe Dynamic
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
name LocalEnv
locs Maybe Dynamic -> (Dynamic -> Maybe a) -> Maybe a
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic
  ExternVar Type a
_ String
name Maybe [a]
xs                -> Int -> String -> Maybe [a] -> a
forall a. Int -> String -> Maybe [a] -> a
evalExternVar Int
k String
name Maybe [a]
xs
  Op1 Op1 a1 a
op Expr a1
e1                          ->
    let ev1 :: a1
ev1 = Int -> Expr a1 -> LocalEnv -> [(Int, Dynamic)] -> a1
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr a1
e1 LocalEnv
locs [(Int, Dynamic)]
strms in
    let op1 :: a1 -> a
op1 = Op1 a1 a -> a1 -> a
forall a b. Op1 a b -> a -> b
evalOp1 Op1 a1 a
op                in
    a1
ev1 a1 -> a -> a
forall a b. a -> b -> b
`seq` a1 -> a
op1 (a1 -> a) -> a -> a
forall a b. a -> b -> b
`seq` a1 -> a
op1 a1
ev1
  Op2 Op2 a1 b a
op Expr a1
e1 Expr b
e2                       ->
    let ev1 :: a1
ev1 = Int -> Expr a1 -> LocalEnv -> [(Int, Dynamic)] -> a1
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr a1
e1 LocalEnv
locs [(Int, Dynamic)]
strms in
    let ev2 :: b
ev2 = Int -> Expr b -> LocalEnv -> [(Int, Dynamic)] -> b
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr b
e2 LocalEnv
locs [(Int, Dynamic)]
strms in
    let op2 :: a1 -> b -> a
op2 = Op2 a1 b a -> a1 -> b -> a
forall a b c. Op2 a b c -> a -> b -> c
evalOp2 Op2 a1 b a
op                in
    a1
ev1 a1 -> a -> a
forall a b. a -> b -> b
`seq` b
ev2 b -> a -> a
forall a b. a -> b -> b
`seq` a1 -> b -> a
op2 (a1 -> b -> a) -> a -> a
forall a b. a -> b -> b
`seq` a1 -> b -> a
op2 a1
ev1 b
ev2
  Op3 Op3 a1 b c a
op Expr a1
e1 Expr b
e2 Expr c
e3                    ->
    let ev1 :: a1
ev1 = Int -> Expr a1 -> LocalEnv -> [(Int, Dynamic)] -> a1
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr a1
e1 LocalEnv
locs [(Int, Dynamic)]
strms in
    let ev2 :: b
ev2 = Int -> Expr b -> LocalEnv -> [(Int, Dynamic)] -> b
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr b
e2 LocalEnv
locs [(Int, Dynamic)]
strms in
    let ev3 :: c
ev3 = Int -> Expr c -> LocalEnv -> [(Int, Dynamic)] -> c
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr c
e3 LocalEnv
locs [(Int, Dynamic)]
strms in
    let op3 :: a1 -> b -> c -> a
op3 = Op3 a1 b c a -> a1 -> b -> c -> a
forall a b c d. Op3 a b c d -> a -> b -> c -> d
evalOp3 Op3 a1 b c a
op                in
    a1
ev1 a1 -> a -> a
forall a b. a -> b -> b
`seq` b
ev2 b -> a -> a
forall a b. a -> b -> b
`seq` c
ev3 c -> a -> a
forall a b. a -> b -> b
`seq` a1 -> b -> c -> a
op3 (a1 -> b -> c -> a) -> a -> a
forall a b. a -> b -> b
`seq` a1 -> b -> c -> a
op3 a1
ev1 b
ev2 c
ev3
  Label Type a
_ String
_ Expr a
e1                         ->
    let ev1 :: a
ev1 = Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr a
e1 LocalEnv
locs [(Int, Dynamic)]
strms in
    a
ev1

-- | Evaluate an extern stream for a number of steps, obtaining the value of
-- the sample at that time.
evalExternVar :: Int -> Name -> Maybe [a] -> a
evalExternVar :: forall a. Int -> String -> Maybe [a] -> a
evalExternVar Int
k String
name Maybe [a]
exts =
  case Maybe [a]
exts of
    Maybe [a]
Nothing -> InterpException -> a
forall a e. Exception e => e -> a
throw (String -> InterpException
NoExtsInterp String
name)
    Just [a]
xs ->
      case Int -> [a] -> Maybe a
forall a. Int -> [a] -> Maybe a
safeIndex Int
k [a]
xs of
        Maybe a
Nothing -> InterpException -> a
forall a e. Exception e => e -> a
throw (String -> Int -> InterpException
NotEnoughValues String
name Int
k)
        Just a
x  -> a
x

-- | Evaluate an 'Copilot.Core.Operators.Op1' by producing an equivalent
-- Haskell function operating on the same types as the
-- 'Copilot.Core.Operators.Op1'.
evalOp1 :: Op1 a b -> (a -> b)
evalOp1 :: forall a b. Op1 a b -> a -> b
evalOp1 Op1 a b
op = case Op1 a b
op of
    Op1 a b
Not        -> a -> b
Bool -> Bool
P.not
    Abs Type a
_      -> a -> a
a -> b
forall a. Num a => a -> a
P.abs
    Sign Type a
_     -> a -> a
a -> b
forall a. Num a => a -> a
P.signum
    Recip Type a
_    -> a -> a
a -> b
forall a. Fractional a => a -> a
P.recip
    Exp Type a
_      -> a -> a
a -> b
forall a. Floating a => a -> a
P.exp
    Sqrt Type a
_     -> a -> a
a -> b
forall a. Floating a => a -> a
P.sqrt
    Log Type a
_      -> a -> a
a -> b
forall a. Floating a => a -> a
P.log
    Sin Type a
_      -> a -> a
a -> b
forall a. Floating a => a -> a
P.sin
    Tan Type a
_      -> a -> a
a -> b
forall a. Floating a => a -> a
P.tan
    Cos Type a
_      -> a -> a
a -> b
forall a. Floating a => a -> a
P.cos
    Asin Type a
_     -> a -> a
a -> b
forall a. Floating a => a -> a
P.asin
    Atan Type a
_     -> a -> a
a -> b
forall a. Floating a => a -> a
P.atan
    Acos Type a
_     -> a -> a
a -> b
forall a. Floating a => a -> a
P.acos
    Sinh Type a
_     -> a -> a
a -> b
forall a. Floating a => a -> a
P.sinh
    Tanh Type a
_     -> a -> a
a -> b
forall a. Floating a => a -> a
P.tanh
    Cosh Type a
_     -> a -> a
a -> b
forall a. Floating a => a -> a
P.cosh
    Asinh Type a
_    -> a -> a
a -> b
forall a. Floating a => a -> a
P.asinh
    Atanh Type a
_    -> a -> a
a -> b
forall a. Floating a => a -> a
P.atanh
    Acosh Type a
_    -> a -> a
a -> b
forall a. Floating a => a -> a
P.acosh
    Ceiling Type a
_  -> Integer -> b
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Integer -> b) -> (a -> Integer) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
idI (Integer -> Integer) -> (a -> Integer) -> a -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall b. Integral b => a -> b
forall a b. (RealFrac a, Integral b) => a -> b
P.ceiling
    Floor Type a
_    -> Integer -> b
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Integer -> b) -> (a -> Integer) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
idI (Integer -> Integer) -> (a -> Integer) -> a -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall b. Integral b => a -> b
forall a b. (RealFrac a, Integral b) => a -> b
P.floor
    BwNot Type a
_    -> a -> a
a -> b
forall a. Bits a => a -> a
complement
    Cast Type a
_ Type b
_   -> a -> b
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral
    GetField (Struct a
_) Type b
_ a -> Field s b
f -> Field s b -> b
forall {s :: Symbol} {t}. Field s t -> t
unfield (Field s b -> b) -> (a -> Field s b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Field s b
f
  where
    -- Used to help GHC pick a return type for ceiling/floor
    idI :: Integer -> Integer
    idI :: Integer -> Integer
idI = Integer -> Integer
forall a. a -> a
P.id

    -- Extract value from field
    unfield :: Field s t -> t
unfield (Field t
v) = t
v

-- | Evaluate an 'Copilot.Core.Operators.Op2' by producing an equivalent
-- Haskell function operating on the same types as the
-- 'Copilot.Core.Operators.Op2'.
evalOp2 :: Op2 a b c -> (a -> b -> c)
evalOp2 :: forall a b c. Op2 a b c -> a -> b -> c
evalOp2 Op2 a b c
op = case Op2 a b c
op of
  Op2 a b c
And          -> a -> b -> c
Bool -> Bool -> Bool
(&&)
  Op2 a b c
Or           -> a -> b -> c
Bool -> Bool -> Bool
(||)
  Add Type a
_        -> a -> a -> a
a -> b -> c
forall a. Num a => a -> a -> a
(+)
  Sub Type a
_        -> (-)
  Mul Type a
_        -> a -> a -> a
a -> b -> c
forall a. Num a => a -> a -> a
(*)
  Mod Type a
_        -> ((a -> a -> a) -> a -> a -> a
forall a. Integral a => (a -> a -> a) -> a -> a -> a
catchZero a -> a -> a
forall a. Integral a => a -> a -> a
P.mod)
  Div Type a
_        -> ((a -> a -> a) -> a -> a -> a
forall a. Integral a => (a -> a -> a) -> a -> a -> a
catchZero a -> a -> a
forall a. Integral a => a -> a -> a
P.quot)
  Fdiv Type a
_       -> a -> a -> a
a -> b -> c
forall a. Fractional a => a -> a -> a
(P./)
  Pow Type a
_        -> a -> a -> a
a -> b -> c
forall a. Floating a => a -> a -> a
(P.**)
  Logb Type a
_       -> a -> a -> a
a -> b -> c
forall a. Floating a => a -> a -> a
P.logBase
  Atan2 Type a
_      -> a -> a -> a
a -> b -> c
forall a. RealFloat a => a -> a -> a
P.atan2
  Eq Type a
_         -> a -> a -> Bool
a -> b -> c
forall a. Eq a => a -> a -> Bool
(==)
  Ne Type a
_         -> a -> a -> Bool
a -> b -> c
forall a. Eq a => a -> a -> Bool
(/=)
  Le Type a
_         -> a -> a -> Bool
a -> b -> c
forall a. Ord a => a -> a -> Bool
(<=)
  Ge Type a
_         -> a -> a -> Bool
a -> b -> c
forall a. Ord a => a -> a -> Bool
(>=)
  Lt Type a
_         -> a -> a -> Bool
a -> b -> c
forall a. Ord a => a -> a -> Bool
(<)
  Gt Type a
_         -> a -> a -> Bool
a -> b -> c
forall a. Ord a => a -> a -> Bool
(>)
  BwAnd Type a
_      -> a -> a -> a
a -> b -> c
forall a. Bits a => a -> a -> a
(.&.)
  BwOr  Type a
_      -> a -> a -> a
a -> b -> c
forall a. Bits a => a -> a -> a
(.|.)
  BwXor Type a
_      -> (a -> a -> a
a -> b -> c
forall a. Bits a => a -> a -> a
xor)
  BwShiftL Type a
_ Type b
_ -> ( \ !a
a !b
b -> c -> Int -> c
forall a. Bits a => a -> Int -> a
shiftL a
c
a (Int -> c) -> Int -> c
forall a b. (a -> b) -> a -> b
$! b -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
b )
  BwShiftR Type a
_ Type b
_ -> ( \ !a
a !b
b -> c -> Int -> c
forall a. Bits a => a -> Int -> a
shiftR a
c
a (Int -> c) -> Int -> c
forall a b. (a -> b) -> a -> b
$! b -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
b )
  Index    Type (Array n c)
_   -> \a
xs b
n -> (Array n c -> [c]
forall (n :: Nat) a. Array n a -> [a]
arrayElems a
Array n c
xs) [c] -> Int -> c
forall a. HasCallStack => [a] -> Int -> a
!! (b -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
n)

  UpdateField (Struct a
_) Type b
ty (a -> Field s b
fieldAccessor :: a -> Field s b) ->
    \a
stream b
fieldValue ->
      let newField :: Field s b
          newField :: Field s b
newField = b -> Field s b
forall (s :: Symbol) t. t -> Field s t
Field b
fieldValue
      in c -> Value Any -> c
forall t. c -> Value t -> c
forall a t. Struct a => a -> Value t -> a
updateField a
c
stream (Type b -> Field s b -> Value Any
forall a (s :: Symbol) t.
(Typeable t, KnownSymbol s, Show t) =>
Type t -> Field s t -> Value a
Value Type b
ty Field s b
newField)

-- | Apply a function to two numbers, so long as the second one is
-- not zero.
--
-- Used to detect attempts at dividing by zero and produce the appropriate
-- 'InterpException'.
catchZero :: Integral a => (a -> a -> a) -> (a -> a -> a)
catchZero :: forall a. Integral a => (a -> a -> a) -> a -> a -> a
catchZero a -> a -> a
_ a
_ a
0 = InterpException -> a
forall a e. Exception e => e -> a
throw InterpException
DivideByZero
catchZero a -> a -> a
f a
x a
y = a -> a -> a
f a
x a
y

-- | Evaluate an 'Copilot.Core.Operators.Op3' by producing an equivalent
-- Haskell function operating on the same types as the
-- 'Copilot.Core.Operators.Op3'.
evalOp3 :: Op3 a b c d -> (a -> b -> c -> d)
evalOp3 :: forall a b c d. Op3 a b c d -> a -> b -> c -> d
evalOp3 (Mux         Type b
_)  = \ !a
v !b
x !c
y -> if a
Bool
v then b
d
x else c
d
y
evalOp3 (UpdateArray Type (Array n c)
ty) = \a
xs b
n c
x -> Array n c -> Int -> c -> Array n c
forall (n :: Nat) a. Array n a -> Int -> a -> Array n a
arrayUpdate a
Array n c
xs (b -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
n) c
x

-- | Turn a stream into a key-value pair that can be added to an 'Env' for
-- simulation.
initStrm :: Stream -> (Id, Dynamic)
initStrm :: Stream -> (Int, Dynamic)
initStrm Stream { streamId :: Stream -> Int
streamId       = Int
id
                , streamBuffer :: ()
streamBuffer   = [a]
buffer
                , streamExprType :: ()
streamExprType = Type a
t } =
  (Int
id, [a] -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
buffer))

-- | Evaluate several streams for a number of steps, producing the environment
-- at the end of the evaluation.
evalStreams :: Int -> [Stream] -> Env Id -> Env Id
evalStreams :: Int -> [Stream] -> [(Int, Dynamic)] -> [(Int, Dynamic)]
evalStreams Int
top [Stream]
specStrms [(Int, Dynamic)]
initStrms =
  -- XXX actually only need to compute until shortest stream is of length k
  -- XXX this should just be a foldl' over [0,1..k]
  Int -> [(Int, Dynamic)] -> [(Int, Dynamic)]
evalStreams_ Int
0 [(Int, Dynamic)]
initStrms
  where
  evalStreams_ :: Int -> Env Id -> Env Id
  evalStreams_ :: Int -> [(Int, Dynamic)] -> [(Int, Dynamic)]
evalStreams_ Int
k [(Int, Dynamic)]
strms | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
top  = [(Int, Dynamic)]
strms
  evalStreams_ Int
k [(Int, Dynamic)]
strms | Bool
otherwise =
    Int -> [(Int, Dynamic)] -> [(Int, Dynamic)]
evalStreams_ (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([(Int, Dynamic)] -> [(Int, Dynamic)])
-> [(Int, Dynamic)] -> [(Int, Dynamic)]
forall a b. (a -> b) -> a -> b
$! [(Int, Dynamic)]
strms_
    where
    strms_ :: [(Int, Dynamic)]
strms_ = (Stream -> (Int, Dynamic)) -> [Stream] -> [(Int, Dynamic)]
forall a b. (a -> b) -> [a] -> [b]
map Stream -> (Int, Dynamic)
evalStream [Stream]
specStrms
    evalStream :: Stream -> (Int, Dynamic)
evalStream Stream { streamId :: Stream -> Int
streamId       = Int
id
                      , streamExpr :: ()
streamExpr     = Expr a
e
                      , streamExprType :: ()
streamExprType = Type a
t } =
      let xs :: [a]
xs = Maybe [a] -> [a]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [a] -> [a]) -> Maybe [a] -> [a]
forall a b. (a -> b) -> a -> b
$ Int -> [(Int, Dynamic)] -> Maybe Dynamic
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
id [(Int, Dynamic)]
strms Maybe Dynamic -> (Dynamic -> Maybe [a]) -> Maybe [a]
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Dynamic -> Maybe [a]
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic      in
      let x :: a
x  = Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
k Expr a
e [] [(Int, Dynamic)]
strms                          in
      let ls :: [a]
ls = a
x a -> [a] -> [a]
forall a b. a -> b -> b
`seq` (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs)                                  in
      (Int
id, [a] -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn [a]
ls)

-- | Evaluate a trigger for a number of steps.
evalTrigger :: ShowType          -- ^ Show booleans as @0@/@1@ (C) or
                                 --   @True@/@False@ (Haskell).
            -> Int               -- ^ Number of steps to evaluate.
            -> Env Id            -- ^ Environment to use with known
                                 --   stream-value associations.
            -> Trigger           -- ^ Trigger to evaluate.
            -> [Maybe [Output]]
evalTrigger :: ShowType -> Int -> [(Int, Dynamic)] -> Trigger -> [Maybe [String]]
evalTrigger ShowType
showType Int
k [(Int, Dynamic)]
strms
  Trigger
    { triggerGuard :: Trigger -> Expr Bool
triggerGuard = Expr Bool
e
    , triggerArgs :: Trigger -> [UExpr]
triggerArgs  = [UExpr]
args
    } = ((Bool, [String]) -> Maybe [String])
-> [(Bool, [String])] -> [Maybe [String]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, [String]) -> Maybe [String]
forall a. (Bool, a) -> Maybe a
tag ([Bool] -> [[String]] -> [(Bool, [String])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Bool]
bs [[String]]
vs)

  where
  tag :: (Bool, a) -> Maybe a
  tag :: forall a. (Bool, a) -> Maybe a
tag (Bool
True,  a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
  tag (Bool
False, a
_) = Maybe a
forall a. Maybe a
Nothing

  -- Is the guard true?
  bs :: [Bool]
  bs :: [Bool]
bs = Int -> Expr Bool -> [(Int, Dynamic)] -> [Bool]
forall a. Typeable a => Int -> Expr a -> [(Int, Dynamic)] -> [a]
evalExprs_ Int
k Expr Bool
e [(Int, Dynamic)]
strms

  -- The argument outputs.
  vs :: [[Output]]
  vs :: [[String]]
vs = if [UExpr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UExpr]
args then Int -> [String] -> [[String]]
forall a. Int -> a -> [a]
replicate Int
k []  -- might be 0 args.
         else [[String]] -> [[String]]
forall a. [[a]] -> [[a]]
transpose ([[String]] -> [[String]]) -> [[String]] -> [[String]]
forall a b. (a -> b) -> a -> b
$ (UExpr -> [String]) -> [UExpr] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map UExpr -> [String]
evalUExpr [UExpr]
args

  evalUExpr :: UExpr -> [Output]
  evalUExpr :: UExpr -> [String]
evalUExpr (UExpr Type a
t Expr a
e1) =
    (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowType -> Type a -> a -> String
forall a. ShowType -> Type a -> a -> String
showWithType ShowType
showType Type a
t) (Int -> Expr a -> [(Int, Dynamic)] -> [a]
forall a. Typeable a => Int -> Expr a -> [(Int, Dynamic)] -> [a]
evalExprs_ Int
k Expr a
e1 [(Int, Dynamic)]
strms)

-- | Evaluate an observer for a number of steps.
evalObserver :: ShowType  -- ^ Show booleans as @0@/@1@ (C) or @True@/@False@
                          --   (Haskell).
             -> Int       -- ^ Number of steps to evaluate.
             -> Env Id    -- ^ Environment to use with known stream-value
                          --   associations.
             -> Observer  -- ^ Observer to evaluate.
             -> [Output]
evalObserver :: ShowType -> Int -> [(Int, Dynamic)] -> Observer -> [String]
evalObserver ShowType
showType Int
k [(Int, Dynamic)]
strms
  Observer
    { observerExpr :: ()
observerExpr     = Expr a
e
    , observerExprType :: ()
observerExprType = Type a
t }
  = (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowType -> Type a -> a -> String
forall a. ShowType -> Type a -> a -> String
showWithType ShowType
showType Type a
t) (Int -> Expr a -> [(Int, Dynamic)] -> [a]
forall a. Typeable a => Int -> Expr a -> [(Int, Dynamic)] -> [a]
evalExprs_ Int
k Expr a
e [(Int, Dynamic)]
strms)

-- | Evaluate an expression for a number of steps, producing a list with the
-- changing value of the expression until that time.
evalExprs_ :: Typeable a => Int -> Expr a -> Env Id -> [a]
evalExprs_ :: forall a. Typeable a => Int -> Expr a -> [(Int, Dynamic)] -> [a]
evalExprs_ Int
k Expr a
e [(Int, Dynamic)]
strms =
  (Int -> a) -> [Int] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
forall a.
Typeable a =>
Int -> Expr a -> LocalEnv -> [(Int, Dynamic)] -> a
evalExpr_ Int
i Expr a
e [] [(Int, Dynamic)]
strms) [Int
0..(Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]

-- | Safe indexing (!!) on possibly infininite lists.
safeIndex :: Int -> [a] -> Maybe a
safeIndex :: forall a. Int -> [a] -> Maybe a
safeIndex Int
i [a]
ls =
  let ls' :: [a]
ls' = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [a]
ls in
  if [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ls' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i then a -> Maybe a
forall a. a -> Maybe a
Just ([a]
ls' [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
    else Maybe a
forall a. Maybe a
Nothing

-- * Auxiliary

-- Are we proving equivalence with a C backend, in which case we want to show
-- Booleans as '0' and '1'.

-- | Target language for showing a typed value. Used to adapt the
-- representation of booleans.
data ShowType = C | Haskell

-- | Show a value. The representation depends on the type and the target
-- language. Booleans are represented differently depending on the backend.
showWithType :: ShowType -> Type a -> a -> String
showWithType :: forall a. ShowType -> Type a -> a -> String
showWithType ShowType
showT Type a
t a
x =
  case ShowType
showT of
    ShowType
C         -> case Type a
t of
                   Type a
Bool -> if a
Bool
x then String
"1" else String
"0"
                   Type a
_    -> String
sw
    ShowType
Haskell   -> case Type a
t of
                   Type a
Bool -> if a
Bool
x then String
"true" else String
"false"
                   Type a
_    -> String
sw
  where
  sw :: String
sw = case Type a -> ShowWit a
forall a. Type a -> ShowWit a
showWit Type a
t of
         ShowWit a
ShowWit -> a -> String
forall a. Show a => a -> String
show a
x

-- * Auxiliary show instance

-- | Witness datatype for showing a value, used by 'showWithType'.
data ShowWit a = Show a => ShowWit

-- | Turn a type into a show witness.
showWit :: Type a -> ShowWit a
showWit :: forall a. Type a -> ShowWit a
showWit Type a
t =
  case Type a
t of
    Type a
Bool   -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Int8   -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Int16  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Int32  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Int64  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Word8  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Word16 -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Word32 -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Word64 -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Float  -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Type a
Double -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Array Type t
t -> ShowWit a
forall a. Show a => ShowWit a
ShowWit
    Struct a
t -> ShowWit a
forall a. Show a => ShowWit a
ShowWit