content: -- 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 (ArrayWrongSize name expectedSize)                                      =
      badUsage $ "in the environment for external array " ++ name
        ++ ", we expect a list of length " ++ show expectedSize
        ++ ", but the length of the array you supplied is of a different length."
    ---------------------------------------
    show (ArrayIdxOutofBounds name index size)                                   =
      badUsage $ "in the environment for external array " ++ name
        ++ ", you gave an index of " ++ show index
        ++ " where the size of the array is " ++ show size ++ "; the size must "
        ++ " be strictly greater than the index."
    ---------------------------------------
    show DivideByZero                                                            =
      badUsage "divide by zero."
    ---------------------------------------
    show (NotEnoughValues name k)                                                =
      badUsage $ "on the " ++ show k ++ "th iteration, we ran out of "
        ++ "values for simulating the external element " ++ name ++ "."
    ---------------------------------------
    show (NoExtsInterp name)                                                     =
      badUsage $ "in a call of external symbol " ++ name ++ ", you did not "
        ++ "provide an expression for interpretation.  In your external "
        ++ "declaration, you need to provide a 'Just strm', where 'strm' is "
        ++ "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
    { 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.
  
    , interpObservers :: [(String, [Output])]
      -- ^ Map from observer names to their outputs.
    }
    deriving 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 k spec =
  
    let initStrms = map initStrm (specStreams spec)             in
  
    let strms = evalStreams k (specStreams spec) initStrms      in
  
    let trigs = map (evalTrigger showType k strms)
                    (specTriggers spec)                         in
  
    let obsvs = map (evalObserver showType k strms)
                    (specObservers spec)                        in
  
    strms `seq` ExecTrace
                  { interpTriggers  =
                      zip (map triggerName  (specTriggers  spec)) trigs
                  , interpObservers =
                      zip (map observerName (specObservers spec)) 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_ k e0 locs strms = case e0 of
    Const _ x                          -> x
    Drop t i id                        ->
      let Just buff = lookup id strms >>= fromDynamic in
      reverse buff !! (fromIntegral i + k)
    Local t1 _ name e1 e2              ->
      let x     = evalExpr_ k e1 locs strms in
      let locs' = (name, toDyn x) : locs  in
      x `seq` locs' `seq` evalExpr_ k e2  locs' strms
    Var t name                         -> fromJust $ lookup name locs >>= fromDynamic
    ExternVar _ name xs                -> evalExternVar k name xs
    Op1 op e1                          ->
      let ev1 = evalExpr_ k e1 locs strms in
      let op1 = evalOp1 op                in
      ev1 `seq` op1 `seq` op1 ev1
    Op2 op e1 e2                       ->
      let ev1 = evalExpr_ k e1 locs strms in
      let ev2 = evalExpr_ k e2 locs strms in
      let op2 = evalOp2 op                in
      ev1 `seq` ev2 `seq` op2 `seq` op2 ev1 ev2
    Op3 op e1 e2 e3                    ->
      let ev1 = evalExpr_ k e1 locs strms in
      let ev2 = evalExpr_ k e2 locs strms in
      let ev3 = evalExpr_ k e3 locs strms in
      let op3 = evalOp3 op                in
      ev1 `seq` ev2 `seq` ev3 `seq` op3 `seq` op3 ev1 ev2 ev3
    Label _ _ e1                         ->
      let ev1 = evalExpr_ k e1 locs strms in
      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 k name exts =
    case exts of
      Nothing -> throw (NoExtsInterp name)
      Just xs ->
        case safeIndex k xs of
          Nothing -> throw (NotEnoughValues name k)
          Just x  -> 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 op = case op of
      Not        -> P.not
      Abs _      -> P.abs
      Sign _     -> P.signum
      Recip _    -> P.recip
      Exp _      -> P.exp
      Sqrt _     -> P.sqrt
      Log _      -> P.log
      Sin _      -> P.sin
      Tan _      -> P.tan
      Cos _      -> P.cos
      Asin _     -> P.asin
      Atan _     -> P.atan
      Acos _     -> P.acos
      Sinh _     -> P.sinh
      Tanh _     -> P.tanh
      Cosh _     -> P.cosh
      Asinh _    -> P.asinh
      Atanh _    -> P.atanh
      Acosh _    -> P.acosh
      Ceiling _  -> P.fromIntegral . idI . P.ceiling
      Floor _    -> P.fromIntegral . idI . P.floor
      BwNot _    -> complement
      Cast _ _   -> P.fromIntegral
      GetField (Struct _) _ f -> unfield . f
    where
      -- Used to help GHC pick a return type for ceiling/floor
      idI :: Integer -> Integer
      idI = P.id
  
      -- Extract value from field
      unfield (Field v) = 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 op = case op of
    And          -> (&&)
    Or           -> (||)
    Add _        -> (+)
    Sub _        -> (-)
    Mul _        -> (*)
    Mod _        -> (catchZero P.mod)
    Div _        -> (catchZero P.quot)
    Fdiv _       -> (P./)
    Pow _        -> (P.**)
    Logb _       -> P.logBase
    Atan2 _      -> P.atan2
    Eq _         -> (==)
    Ne _         -> (/=)
    Le _         -> (<=)
    Ge _         -> (>=)
    Lt _         -> (<)
    Gt _         -> (>)
    BwAnd _      -> (.&.)
    BwOr  _      -> (.|.)
    BwXor _      -> (xor)
    BwShiftL _ _ -> ( \ !a !b -> shiftL a $! fromIntegral b )
    BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )
    Index    _   -> \xs n -> (arrayElems xs) !! (fromIntegral n)
  
    UpdateField (Struct _) ty (fieldAccessor :: a -> Field s b) ->
      \stream fieldValue ->
        let newField :: Field s b
            newField = Field fieldValue
        in updateField stream (Value ty 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 _ _ 0 = throw DivideByZero
  catchZero f x y = f x 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 (Mux         _)  = \ !v !x !y -> if v then x else y
  evalOp3 (UpdateArray ty) = \xs n x -> arrayUpdate xs (fromIntegral n) x
  
  -- | Turn a stream into a key-value pair that can be added to an 'Env' for
  -- simulation.
  initStrm :: Stream -> (Id, Dynamic)
  initStrm Stream { streamId       = id
                  , streamBuffer   = buffer
                  , streamExprType = t } =
    (id, toDyn (reverse 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 top specStrms 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]
    evalStreams_ 0 initStrms
    where
    evalStreams_ :: Int -> Env Id -> Env Id
    evalStreams_ k strms | k == top  = strms
    evalStreams_ k strms | otherwise =
      evalStreams_ (k+1) $! strms_
      where
      strms_ = map evalStream specStrms
      evalStream Stream { streamId       = id
                        , streamExpr     = e
                        , streamExprType = t } =
        let xs = fromJust $ lookup id strms >>= fromDynamic      in
        let x  = evalExpr_ k e [] strms                          in
        let ls = x `seq` (x:xs)                                  in
        (id, toDyn 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 k strms
    Trigger
      { triggerGuard = e
      , triggerArgs  = args
      } = map tag (zip bs vs)
  
    where
    tag :: (Bool, a) -> Maybe a
    tag (True,  x) = Just x
    tag (False, _) = Nothing
  
    -- Is the guard true?
    bs :: [Bool]
    bs = evalExprs_ k e strms
  
    -- The argument outputs.
    vs :: [[Output]]
    vs = if null args then replicate k []  -- might be 0 args.
           else transpose $ map evalUExpr args
  
    evalUExpr :: UExpr -> [Output]
    evalUExpr (UExpr t e1) =
      map (showWithType showType t) (evalExprs_ k e1 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 k strms
    Observer
      { observerExpr     = e
      , observerExprType = t }
    = map (showWithType showType t) (evalExprs_ k e 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_ k e strms =
    map (\i -> evalExpr_ i e [] strms) [0..(k-1)]
  
  -- | Safe indexing (!!) on possibly infininite lists.
  safeIndex :: Int -> [a] -> Maybe a
  safeIndex i ls =
    let ls' = take (i+1) ls in
    if length ls' > i then Just (ls' !! i)
      else 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 showT t x =
    case showT of
      C         -> case t of
                     Bool -> if x then "1" else "0"
                     _    -> sw
      Haskell   -> case t of
                     Bool -> if x then "true" else "false"
                     _    -> sw
    where
    sw = case showWit t of
           ShowWit -> show 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 t =
    case t of
      Bool   -> ShowWit
      Int8   -> ShowWit
      Int16  -> ShowWit
      Int32  -> ShowWit
      Int64  -> ShowWit
      Word8  -> ShowWit
      Word16 -> ShowWit
      Word32 -> ShowWit
      Word64 -> ShowWit
      Float  -> ShowWit
      Double -> ShowWit
      Array t -> ShowWit
      Struct t -> ShowWit
  