    -- 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. (HasCallStack, 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. (HasCallStack, 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 (ZonkAny 0) -> 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 (ZonkAny 0)
    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. (HasCallStack, 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