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

{-# 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 (SeqIndex -> SeqIndex -> Bool
(SeqIndex -> SeqIndex -> Bool)
-> (SeqIndex -> SeqIndex -> Bool) -> Eq SeqIndex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SeqIndex -> SeqIndex -> Bool
$c/= :: SeqIndex -> SeqIndex -> Bool
== :: SeqIndex -> SeqIndex -> Bool
$c== :: 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
min :: SeqIndex -> SeqIndex -> SeqIndex
$cmin :: SeqIndex -> SeqIndex -> SeqIndex
max :: SeqIndex -> SeqIndex -> SeqIndex
$cmax :: SeqIndex -> SeqIndex -> SeqIndex
>= :: SeqIndex -> SeqIndex -> Bool
$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
compare :: SeqIndex -> SeqIndex -> Ordering
$ccompare :: SeqIndex -> SeqIndex -> Ordering
$cp1Ord :: Eq 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
showList :: [SeqIndex] -> ShowS
$cshowList :: [SeqIndex] -> ShowS
show :: SeqIndex -> String
$cshow :: SeqIndex -> String
showsPrec :: Int -> SeqIndex -> ShowS
$cshowsPrec :: Int -> 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
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: 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
min :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$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
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
$cp1Ord :: Eq Type
Ord)

instance Show Type where
  show :: Type -> String
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 (Expr -> Expr -> Bool
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c== :: 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
min :: Expr -> Expr -> Expr
$cmin :: Expr -> Expr -> Expr
max :: Expr -> Expr -> Expr
$cmax :: Expr -> Expr -> Expr
>= :: Expr -> Expr -> Bool
$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
compare :: Expr -> Expr -> Ordering
$ccompare :: Expr -> Expr -> Ordering
$cp1Ord :: Eq 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
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> 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
/= :: Op1 -> Op1 -> Bool
$c/= :: Op1 -> Op1 -> Bool
== :: Op1 -> Op1 -> Bool
$c== :: 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
min :: Op1 -> Op1 -> Op1
$cmin :: Op1 -> Op1 -> Op1
max :: Op1 -> Op1 -> Op1
$cmax :: Op1 -> Op1 -> Op1
>= :: Op1 -> Op1 -> Bool
$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
compare :: Op1 -> Op1 -> Ordering
$ccompare :: Op1 -> Op1 -> Ordering
$cp1Ord :: Eq 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
/= :: Op2 -> Op2 -> Bool
$c/= :: Op2 -> Op2 -> Bool
== :: Op2 -> Op2 -> Bool
$c== :: 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
min :: Op2 -> Op2 -> Op2
$cmin :: Op2 -> Op2 -> Op2
max :: Op2 -> Op2 -> Op2
$cmax :: Op2 -> Op2 -> Op2
>= :: Op2 -> Op2 -> Bool
$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
compare :: Op2 -> Op2 -> Ordering
$ccompare :: Op2 -> Op2 -> Ordering
$cp1Ord :: Eq Op2
Ord)

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

instance Show Op1 where
  show :: Op1 -> String
show op :: Op1
op = case Op1
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 :: Op2 -> String
show op :: Op2
op = case Op2
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 :: Expr -> Type
typeOf e :: Expr
e = case Expr
e of
  ConstB _       -> Type
Bool
  ConstR _       -> Type
Real
  ConstI t :: Type
t _     -> Type
t
  Ite    t :: Type
t _ _ _ -> Type
t
  Op1    t :: Type
t _ _   -> Type
t
  Op2    t :: Type
t _ _ _ -> Type
t
  SVal   t :: Type
t _ _   -> Type
t
  FunApp t :: Type
t _ _   -> Type
t

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

-- | An index to a future element of a sequence.
_n_plus :: (Integral a) => a -> SeqIndex
_n_plus :: a -> SeqIndex
_n_plus d :: 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 _ e :: Expr
e@(ConstB _) = Expr
e
evalAt _ e :: Expr
e@(ConstR _) = Expr
e
evalAt _ e :: Expr
e@(ConstI _ _) = Expr
e
evalAt i :: SeqIndex
i (Op1 t :: Type
t op :: Op1
op e :: Expr
e) = Type -> Op1 -> Expr -> Expr
Op1 Type
t Op1
op (SeqIndex -> Expr -> Expr
evalAt SeqIndex
i Expr
e)
evalAt i :: SeqIndex
i (Op2 t :: Type
t op :: Op2
op e1 :: Expr
e1 e2 :: 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 i :: SeqIndex
i (Ite t :: Type
t c :: Expr
c e1 :: Expr
e1 e2 :: 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 i :: SeqIndex
i (FunApp t :: Type
t name :: String
name args :: [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 (\e :: Expr
e -> SeqIndex -> Expr -> Expr
evalAt SeqIndex
i Expr
e) [Expr]
args

evalAt _ e :: Expr
e@(SVal _ _ (Fixed _)) = Expr
e
evalAt (Fixed n :: Integer
n) (SVal t :: Type
t s :: String
s (Var d :: 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   k :: Integer
k) (SVal t :: Type
t s :: String
s (Var d :: 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)

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