{-# 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)