    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE GADTs                     #-}
    {-# LANGUAGE LambdaCase                #-}
    {-# LANGUAGE Safe                      #-}

    -- | This module implements the specification language for the IL format, an
    -- intermediate representation used in copilot-theorem to facilitate model
    -- checking.
    --
    -- A Copilot program is translated into a list of quantifier-free equations
    -- over integer sequences, implicitly universally quantified by a free variable
    -- n. Each sequence roughly corresponds to a stream.
    --
    -- This representation is partly inspired by the IL language described in
    -- Hagen, G.E., /VERIFYING SAFETY PROPERTIES OF LUSTRE PROGRAMS: AN SMT-BASED/
    -- /APPROACH/, 2008.

    module Copilot.Theorem.IL.Spec
      ( Type (..)
      , Op1  (..)
      , Op2  (..)
      , SeqId
      , SeqIndex (..)
      , SeqDescr (..)
      , VarDescr (..)
      , Expr (..)
      , IL (..)
      , PropId
      , typeOf
      , _n_
      , _n_plus
      , evalAt
      ) where

    import Data.Map (Map)
    import Data.Function (on)

    -- | Identifier of a sequence.
    type SeqId    =  String

    -- | Index within a sequence.
    data SeqIndex = Fixed Integer -- ^ An absolute index in the sequence.
                  | Var Integer   -- ^ An index relative to the current time-step.
      deriving (SeqIndex -> SeqIndex -> Bool
    (SeqIndex -> SeqIndex -> Bool)
    -> (SeqIndex -> SeqIndex -> Bool) -> Eq SeqIndex
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SeqIndex -> SeqIndex -> Bool
    == :: SeqIndex -> SeqIndex -> Bool
    $c/= :: SeqIndex -> SeqIndex -> Bool
    /= :: SeqIndex -> SeqIndex -> Bool
    Eq, Eq SeqIndex
    Eq SeqIndex =>
    (SeqIndex -> SeqIndex -> Ordering)
    -> (SeqIndex -> SeqIndex -> Bool)
    -> (SeqIndex -> SeqIndex -> Bool)
    -> (SeqIndex -> SeqIndex -> Bool)
    -> (SeqIndex -> SeqIndex -> Bool)
    -> (SeqIndex -> SeqIndex -> SeqIndex)
    -> (SeqIndex -> SeqIndex -> SeqIndex)
    -> Ord SeqIndex
    SeqIndex -> SeqIndex -> Bool
    SeqIndex -> SeqIndex -> Ordering
    SeqIndex -> SeqIndex -> SeqIndex
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: SeqIndex -> SeqIndex -> Ordering
    compare :: SeqIndex -> SeqIndex -> Ordering
    $c< :: SeqIndex -> SeqIndex -> Bool
    < :: SeqIndex -> SeqIndex -> Bool
    $c<= :: SeqIndex -> SeqIndex -> Bool
    <= :: SeqIndex -> SeqIndex -> Bool
    $c> :: SeqIndex -> SeqIndex -> Bool
    > :: SeqIndex -> SeqIndex -> Bool
    $c>= :: SeqIndex -> SeqIndex -> Bool
    >= :: SeqIndex -> SeqIndex -> Bool
    $cmax :: SeqIndex -> SeqIndex -> SeqIndex
    max :: SeqIndex -> SeqIndex -> SeqIndex
    $cmin :: SeqIndex -> SeqIndex -> SeqIndex
    min :: SeqIndex -> SeqIndex -> SeqIndex
    Ord, Int -> SeqIndex -> ShowS
    [SeqIndex] -> ShowS
    SeqIndex -> String
    (Int -> SeqIndex -> ShowS)
    -> (SeqIndex -> String) -> ([SeqIndex] -> ShowS) -> Show SeqIndex
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SeqIndex -> ShowS
    showsPrec :: Int -> SeqIndex -> ShowS
    $cshow :: SeqIndex -> String
    show :: SeqIndex -> String
    $cshowList :: [SeqIndex] -> ShowS
    showList :: [SeqIndex] -> ShowS
    Show)

    -- | Idealized types. These differ from Copilot types in that, notionally,
    -- reals actually denote real numbers.
    data Type = Bool  | Real
      | SBV8 | SBV16 | SBV32 | SBV64
      | BV8  | BV16 | BV32 | BV64
      deriving (Type -> Type -> Bool
    (Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Type -> Type -> Bool
    == :: Type -> Type -> Bool
    $c/= :: Type -> Type -> Bool
    /= :: Type -> Type -> Bool
    Eq, Eq Type
    Eq Type =>
    (Type -> Type -> Ordering)
    -> (Type -> Type -> Bool)
    -> (Type -> Type -> Bool)
    -> (Type -> Type -> Bool)
    -> (Type -> Type -> Bool)
    -> (Type -> Type -> Type)
    -> (Type -> Type -> Type)
    -> Ord Type
    Type -> Type -> Bool
    Type -> Type -> Ordering
    Type -> Type -> Type
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Type -> Type -> Ordering
    compare :: Type -> Type -> Ordering
    $c< :: Type -> Type -> Bool
    < :: Type -> Type -> Bool
    $c<= :: Type -> Type -> Bool
    <= :: Type -> Type -> Bool
    $c> :: Type -> Type -> Bool
    > :: Type -> Type -> Bool
    $c>= :: Type -> Type -> Bool
    >= :: Type -> Type -> Bool
    $cmax :: Type -> Type -> Type
    max :: Type -> Type -> Type
    $cmin :: Type -> Type -> Type
    min :: Type -> Type -> Type
    Ord)

    instance Show Type where
      show :: Type -> String
    show = \case
        Type
    Bool  -> String
    "Bool"
        Type
    Real  -> String
    "Real"
        Type
    SBV8  -> String
    "SBV8"
        Type
    SBV16 -> String
    "SBV16"
        Type
    SBV32 -> String
    "SBV32"
        Type
    SBV64 -> String
    "SBV64"
        Type
    BV8   -> String
    "BV8"
        Type
    BV16  -> String
    "BV16"
        Type
    BV32  -> String
    "BV32"
        Type
    BV64  -> String
    "BV64"

    -- | Idealized representation of a Copilot expression.
    data Expr
      = ConstB Bool                 -- ^ Constant boolean.
      | ConstR Double               -- ^ Constant real.
      | ConstI Type Integer         -- ^ Constant integer.
      | Ite    Type Expr Expr Expr  -- ^ If-then-else.
      | Op1    Type Op1 Expr        -- ^ Apply a unary operator.
      | Op2    Type Op2 Expr Expr   -- ^ Apply a binary operator.
      | SVal   Type SeqId SeqIndex  -- ^ Refer to a value in another sequence.
      | FunApp Type String [Expr]   -- ^ Function application.
      deriving (Expr -> Expr -> Bool
    (Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Expr -> Expr -> Bool
    == :: Expr -> Expr -> Bool
    $c/= :: Expr -> Expr -> Bool
    /= :: Expr -> Expr -> Bool
    Eq, Eq Expr
    Eq Expr =>
    (Expr -> Expr -> Ordering)
    -> (Expr -> Expr -> Bool)
    -> (Expr -> Expr -> Bool)
    -> (Expr -> Expr -> Bool)
    -> (Expr -> Expr -> Bool)
    -> (Expr -> Expr -> Expr)
    -> (Expr -> Expr -> Expr)
    -> Ord Expr
    Expr -> Expr -> Bool
    Expr -> Expr -> Ordering
    Expr -> Expr -> Expr
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Expr -> Expr -> Ordering
    compare :: Expr -> Expr -> Ordering
    $c< :: Expr -> Expr -> Bool
    < :: Expr -> Expr -> Bool
    $c<= :: Expr -> Expr -> Bool
    <= :: Expr -> Expr -> Bool
    $c> :: Expr -> Expr -> Bool
    > :: Expr -> Expr -> Bool
    $c>= :: Expr -> Expr -> Bool
    >= :: Expr -> Expr -> Bool
    $cmax :: Expr -> Expr -> Expr
    max :: Expr -> Expr -> Expr
    $cmin :: Expr -> Expr -> Expr
    min :: Expr -> Expr -> Expr
    Ord, Int -> Expr -> ShowS
    [Expr] -> ShowS
    Expr -> String
    (Int -> Expr -> ShowS)
    -> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Expr -> ShowS
    showsPrec :: Int -> Expr -> ShowS
    $cshow :: Expr -> String
    show :: Expr -> String
    $cshowList :: [Expr] -> ShowS
    showList :: [Expr] -> ShowS
    Show)

    -- | A description of a variable (or function) together with its type.
    data VarDescr = VarDescr
      { VarDescr -> String
    varName :: String
      , VarDescr -> Type
    varType :: Type
      , VarDescr -> [Type]
    args    :: [Type]
      }

    instance Eq VarDescr where
      == :: VarDescr -> VarDescr -> Bool
    (==) = String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (String -> String -> Bool)
    -> (VarDescr -> String) -> VarDescr -> VarDescr -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` VarDescr -> String
    varName

    instance Ord VarDescr where
      compare :: VarDescr -> VarDescr -> Ordering
    compare = String -> String -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (String -> String -> Ordering)
    -> (VarDescr -> String) -> VarDescr -> VarDescr -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` VarDescr -> String
    varName

    -- | Identifier for a property.
    type PropId = String

    -- | Description of a sequence.
    data SeqDescr = SeqDescr
      { SeqDescr -> String
    seqId    :: SeqId
      , SeqDescr -> Type
    seqType  :: Type
      }

    -- | An IL specification.
    data IL = IL
      { IL -> [Expr]
    modelInit   :: [Expr]
      , IL -> [Expr]
    modelRec    :: [Expr]
      , IL -> Map String ([Expr], Expr)
    properties  :: Map PropId ([Expr], Expr)
      , IL -> Bool
    inductive   :: Bool
      }

    -- | Unary operators.
    data Op1 = Not | Neg | Abs | Exp | Sqrt | Log | Sin | Tan | Cos | Asin | Atan
             | Acos | Sinh | Tanh | Cosh | Asinh | Atanh | Acosh
             deriving (Op1 -> Op1 -> Bool
    (Op1 -> Op1 -> Bool) -> (Op1 -> Op1 -> Bool) -> Eq Op1
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Op1 -> Op1 -> Bool
    == :: Op1 -> Op1 -> Bool
    $c/= :: Op1 -> Op1 -> Bool
    /= :: Op1 -> Op1 -> Bool
    Eq, Eq Op1
    Eq Op1 =>
    (Op1 -> Op1 -> Ordering)
    -> (Op1 -> Op1 -> Bool)
    -> (Op1 -> Op1 -> Bool)
    -> (Op1 -> Op1 -> Bool)
    -> (Op1 -> Op1 -> Bool)
    -> (Op1 -> Op1 -> Op1)
    -> (Op1 -> Op1 -> Op1)
    -> Ord Op1
    Op1 -> Op1 -> Bool
    Op1 -> Op1 -> Ordering
    Op1 -> Op1 -> Op1
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Op1 -> Op1 -> Ordering
    compare :: Op1 -> Op1 -> Ordering
    $c< :: Op1 -> Op1 -> Bool
    < :: Op1 -> Op1 -> Bool
    $c<= :: Op1 -> Op1 -> Bool
    <= :: Op1 -> Op1 -> Bool
    $c> :: Op1 -> Op1 -> Bool
    > :: Op1 -> Op1 -> Bool
    $c>= :: Op1 -> Op1 -> Bool
    >= :: Op1 -> Op1 -> Bool
    $cmax :: Op1 -> Op1 -> Op1
    max :: Op1 -> Op1 -> Op1
    $cmin :: Op1 -> Op1 -> Op1
    min :: Op1 -> Op1 -> Op1
    Ord)

    -- | Binary operators.
    data Op2 = Eq | And | Or | Le | Lt | Ge | Gt | Add | Sub | Mul | Mod | Fdiv | Pow
             deriving (Op2 -> Op2 -> Bool
    (Op2 -> Op2 -> Bool) -> (Op2 -> Op2 -> Bool) -> Eq Op2
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Op2 -> Op2 -> Bool
    == :: Op2 -> Op2 -> Bool
    $c/= :: Op2 -> Op2 -> Bool
    /= :: Op2 -> Op2 -> Bool
    Eq, Eq Op2
    Eq Op2 =>
    (Op2 -> Op2 -> Ordering)
    -> (Op2 -> Op2 -> Bool)
    -> (Op2 -> Op2 -> Bool)
    -> (Op2 -> Op2 -> Bool)
    -> (Op2 -> Op2 -> Bool)
    -> (Op2 -> Op2 -> Op2)
    -> (Op2 -> Op2 -> Op2)
    -> Ord Op2
    Op2 -> Op2 -> Bool
    Op2 -> Op2 -> Ordering
    Op2 -> Op2 -> Op2
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Op2 -> Op2 -> Ordering
    compare :: Op2 -> Op2 -> Ordering
    $c< :: Op2 -> Op2 -> Bool
    < :: Op2 -> Op2 -> Bool
    $c<= :: Op2 -> Op2 -> Bool
    <= :: Op2 -> Op2 -> Bool
    $c> :: Op2 -> Op2 -> Bool
    > :: Op2 -> Op2 -> Bool
    $c>= :: Op2 -> Op2 -> Bool
    >= :: Op2 -> Op2 -> Bool
    $cmax :: Op2 -> Op2 -> Op2
    max :: Op2 -> Op2 -> Op2
    $cmin :: Op2 -> Op2 -> Op2
    min :: Op2 -> Op2 -> Op2
    Ord)

    instance Show Op1 where
      show :: Op1 -> String
    show Op1
    op = case Op1
    op of
        Op1
    Neg   -> String
    "-"
        Op1
    Not   -> String
    "not"
        Op1
    Abs   -> String
    "abs"
        Op1
    Exp   -> String
    "exp"
        Op1
    Sqrt  -> String
    "sqrt"
        Op1
    Log   -> String
    "log"
        Op1
    Sin   -> String
    "sin"
        Op1
    Tan   -> String
    "tan"
        Op1
    Cos   -> String
    "cos"
        Op1
    Asin  -> String
    "asin"
        Op1
    Atan  -> String
    "atan"
        Op1
    Acos  -> String
    "acos"
        Op1
    Sinh  -> String
    "sinh"
        Op1
    Tanh  -> String
    "tanh"
        Op1
    Cosh  -> String
    "cosh"
        Op1
    Asinh -> String
    "asinh"
        Op1
    Atanh -> String
    "atanh"
        Op1
    Acosh -> String
    "acosh"

    instance Show Op2 where
      show :: Op2 -> String
    show Op2
    op = case Op2
    op of
        Op2
    And  -> String
    "and"
        Op2
    Or   -> String
    "or"

        Op2
    Add  -> String
    "+"
        Op2
    Sub  -> String
    "-"
        Op2
    Mul  -> String
    "*"

        Op2
    Mod  -> String
    "mod"

        Op2
    Fdiv -> String
    "/"

        Op2
    Pow  -> String
    "^"

        Op2
    Eq   -> String
    "="

        Op2
    Le   -> String
    "<="
        Op2
    Ge   -> String
    ">="
        Op2
    Lt   -> String
    "<"
        Op2
    Gt   -> String
    ">"

    -- | Return the type of an expression.
    typeOf :: Expr -> Type
    typeOf :: Expr -> Type
    typeOf Expr
    e = case Expr
    e of
      ConstB Bool
    _       -> Type
    Bool
      ConstR Double
    _       -> Type
    Real
      ConstI Type
    t Integer
    _     -> Type
    t
      Ite    Type
    t Expr
    _ Expr
    _ Expr
    _ -> Type
    t
      Op1    Type
    t Op1
    _ Expr
    _   -> Type
    t
      Op2    Type
    t Op2
    _ Expr
    _ Expr
    _ -> Type
    t
      SVal   Type
    t String
    _ SeqIndex
    _   -> Type
    t
      FunApp Type
    t String
    _ [Expr]
    _   -> Type
    t

    -- | An index to the current element of a sequence.
    _n_ :: SeqIndex
    _n_ :: SeqIndex
    _n_ = Integer -> SeqIndex
    Var Integer
    0

    -- | An index to a future element of a sequence.
    _n_plus :: (Integral a) => a -> SeqIndex
    _n_plus :: forall a. Integral a => a -> SeqIndex
    _n_plus a
    d = Integer -> SeqIndex
    Var (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    d)

    -- | Evaluate an expression at specific index in the sequence.
    evalAt :: SeqIndex -> Expr -> Expr
    evalAt :: SeqIndex -> Expr -> Expr
    evalAt SeqIndex
    _ e :: Expr
    e@(ConstB Bool
    _) = Expr
    e
    evalAt SeqIndex
    _ e :: Expr
    e@(ConstR Double
    _) = Expr
    e
    evalAt SeqIndex
    _ e :: Expr
    e@(ConstI Type
    _ Integer
    _) = Expr
    e
    evalAt SeqIndex
    i (Op1 Type
    t Op1
    op Expr
    e) = Type -> Op1 -> Expr -> Expr
    Op1 Type
    t Op1
    op (SeqIndex -> Expr -> Expr
    evalAt SeqIndex
    i Expr
    e)
    evalAt SeqIndex
    i (Op2 Type
    t Op2
    op Expr
    e1 Expr
    e2) = Type -> Op2 -> Expr -> Expr -> Expr
    Op2 Type
    t Op2
    op (SeqIndex -> Expr -> Expr
    evalAt SeqIndex
    i Expr
    e1) (SeqIndex -> Expr -> Expr
    evalAt SeqIndex
    i Expr
    e2)
    evalAt SeqIndex
    i (Ite Type
    t Expr
    c Expr
    e1 Expr
    e2) = Type -> Expr -> Expr -> Expr -> Expr
    Ite Type
    t (SeqIndex -> Expr -> Expr
    evalAt SeqIndex
    i Expr
    c) (SeqIndex -> Expr -> Expr
    evalAt SeqIndex
    i Expr
    e1) (SeqIndex -> Expr -> Expr
    evalAt SeqIndex
    i Expr
    e2)
    evalAt SeqIndex
    i (FunApp Type
    t String
    name [Expr]
    args) = Type -> String -> [Expr] -> Expr
    FunApp Type
    t String
    name ([Expr] -> Expr) -> [Expr] -> Expr
    forall a b. (a -> b) -> a -> b
    $ (Expr -> Expr) -> [Expr] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Expr
    e -> SeqIndex -> Expr -> Expr
    evalAt SeqIndex
    i Expr
    e) [Expr]
    args

    evalAt SeqIndex
    _ e :: Expr
    e@(SVal Type
    _ String
    _ (Fixed Integer
    _)) = Expr
    e
    evalAt (Fixed Integer
    n) (SVal Type
    t String
    s (Var Integer
    d)) = Type -> String -> SeqIndex -> Expr
    SVal Type
    t String
    s (Integer -> SeqIndex
    Fixed (Integer -> SeqIndex) -> Integer -> SeqIndex
    forall a b. (a -> b) -> a -> b
    $ Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    d)
    evalAt (Var   Integer
    k) (SVal Type
    t String
    s (Var Integer
    d)) = Type -> String -> SeqIndex -> Expr
    SVal Type
    t String
    s (Integer -> SeqIndex
    Var   (Integer -> SeqIndex) -> Integer -> SeqIndex
    forall a b. (a -> b) -> a -> b
    $ Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    d)