--------------------------------------------------------------------------------

{-# LANGUAGE ExistentialQuantification, GADTs, 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 (Eq, Ord, 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 (Eq, Ord)

instance Show Type where
  show = \case
    Bool  -> "Bool"
    Real  -> "Real"
    SBV8  -> "SBV8"
    SBV16 -> "SBV16"
    SBV32 -> "SBV32"
    SBV64 -> "SBV64"
    BV8   -> "BV8"
    BV16  -> "BV16"
    BV32  -> "BV32"
    BV64  -> "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 (Eq, Ord, Show)

--------------------------------------------------------------------------------

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

instance Eq VarDescr where
  (==) = (==) `on` varName

instance Ord VarDescr where
  compare = compare `on` varName

--------------------------------------------------------------------------------

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

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

-- | An IL specification.
data IL = IL
  { modelInit   :: [Expr]
  , modelRec    :: [Expr]
  , properties  :: Map PropId ([Expr], Expr)
  , 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 (Eq, Ord)

-- | Binary operators.
data Op2 = Eq | And | Or | Le | Lt | Ge | Gt | Add | Sub | Mul | Mod | Fdiv | Pow
         deriving (Eq, Ord)

-------------------------------------------------------------------------------

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

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

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

    Mod  -> "mod"

    Fdiv -> "/"

    Pow  -> "^"

    Eq   -> "="

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

-------------------------------------------------------------------------------

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

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

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

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

evalAt _ e@(SVal _ _ (Fixed _)) = e
evalAt (Fixed n) (SVal t s (Var d)) = SVal t s (Fixed $ n + d)
evalAt (Var   k) (SVal t s (Var d)) = SVal t s (Var   $ k + d)

--------------------------------------------------------------------------------