{-# LANGUAGE ExistentialQuantification, GADTs, LambdaCase #-}
{-# LANGUAGE Safe #-}
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)
type SeqId = String
data SeqIndex = Fixed Integer
| Var Integer
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)
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"
data Expr
= ConstB Bool
| ConstR Double
| ConstI Type Integer
| Ite Type Expr Expr Expr
| Op1 Type Op1 Expr
| Op2 Type Op2 Expr Expr
| SVal Type SeqId SeqIndex
| FunApp Type String [Expr]
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)
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
type PropId = String
data SeqDescr = SeqDescr
{ SeqDescr -> String
seqId :: SeqId
, SeqDescr -> Type
seqType :: Type
}
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
}
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)
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 -> ">"
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
_n_ :: SeqIndex
_n_ :: SeqIndex
_n_ = Integer -> SeqIndex
Var 0
_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)
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)