{-# LANGUAGE GADTs, ExistentialQuantification, LambdaCase, ScopedTypeVariables,
RankNTypes #-}
{-# LANGUAGE Safe #-}
module Copilot.Theorem.TransSys.Operators where
import qualified Copilot.Core as C
import Copilot.Theorem.TransSys.Cast
import Copilot.Theorem.TransSys.Type
import Copilot.Theorem.Misc.Error as Err
data Op1 a where
Not :: Op1 Bool
Neg :: Op1 a
Abs :: Op1 a
Exp :: Op1 a
Sqrt :: Op1 a
Log :: Op1 a
Sin :: Op1 a
Tan :: Op1 a
Cos :: Op1 a
Asin :: Op1 a
Atan :: Op1 a
Acos :: Op1 a
Sinh :: Op1 a
Tanh :: Op1 a
Cosh :: Op1 a
Asinh :: Op1 a
Atanh :: Op1 a
Acosh :: Op1 a
data Op2 a b where
Eq :: Op2 a Bool
And :: Op2 Bool Bool
Or :: Op2 Bool Bool
Le :: (Num a) => Op2 a Bool
Lt :: (Num a) => Op2 a Bool
Ge :: (Num a) => Op2 a Bool
Gt :: (Num a) => Op2 a Bool
Add :: (Num a) => Op2 a a
Sub :: (Num a) => Op2 a a
Mul :: (Num a) => Op2 a a
Mod :: (Num a) => Op2 a a
Fdiv :: (Num a) => Op2 a a
Pow :: (Num a) => Op2 a a
instance Show (Op1 a) where
show :: Op1 a -> String
show op :: Op1 a
op = case Op1 a
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 a b) where
show :: Op2 a b -> String
show op :: Op2 a b
op = case Op2 a b
op of
Eq -> "="
Le -> "<="
Lt -> "<"
Ge -> ">="
Gt -> ">"
And -> "and"
Or -> "or"
Add -> "+"
Sub -> "-"
Mul -> "*"
Mod -> "mod"
Fdiv -> "/"
Pow -> "^"
data UnhandledOp1 = forall a b .
UnhandledOp1 String (Type a) (Type b)
data UnhandledOp2 = forall a b c .
UnhandledOp2 String (Type a) (Type b) (Type c)
handleOp1 ::
forall m expr _a _b resT. (Functor m)
=> Type resT
-> (C.Op1 _a _b, C.Expr _a)
-> (forall t t'. Type t -> C.Expr t' -> m (expr t))
-> (UnhandledOp1 -> m (expr resT))
-> (forall t . Type t -> Op1 t -> expr t -> expr t)
-> m (expr resT)
handleOp1 :: Type resT
-> (Op1 _a _b, Expr _a)
-> (forall t t'. Type t -> Expr t' -> m (expr t))
-> (UnhandledOp1 -> m (expr resT))
-> (forall t. Type t -> Op1 t -> expr t -> expr t)
-> m (expr resT)
handleOp1 resT :: Type resT
resT (op :: Op1 _a _b
op, e :: Expr _a
e) handleExpr :: forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr notHandledF :: UnhandledOp1 -> m (expr resT)
notHandledF mkOp :: forall t. Type t -> Op1 t -> expr t -> expr t
mkOp = case Op1 _a _b
op of
C.Not -> Op1 Bool -> m (expr Bool) -> m (expr resT)
boolOp Op1 Bool
Not (Type Bool -> Expr _a -> m (expr Bool)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Bool
Bool Expr _a
e)
C.Abs _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Abs
C.Sign ta :: Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta "sign"
C.Recip ta :: Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta "recip"
C.Exp _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Exp
C.Sqrt _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Sqrt
C.Log _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Log
C.Sin _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Sin
C.Tan _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Tan
C.Cos _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Cos
C.Asin _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Asin
C.Atan _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Atan
C.Acos _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Acos
C.Sinh _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Sinh
C.Tanh _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Tanh
C.Cosh _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Cosh
C.Asinh _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Asinh
C.Atanh _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Atanh
C.Acosh _ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Acosh
C.BwNot ta :: Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta "bwnot"
C.Cast _ tb :: Type _b
tb -> Type _b -> m (expr resT)
forall ctb. Type ctb -> m (expr resT)
castTo Type _b
tb
where
boolOp :: Op1 Bool -> m (expr Bool) -> m (expr resT)
boolOp :: Op1 Bool -> m (expr Bool) -> m (expr resT)
boolOp op :: Op1 Bool
op e :: m (expr Bool)
e = case Type resT
resT of
Bool -> (Type resT -> Op1 resT -> expr resT -> expr resT
forall t. Type t -> Op1 t -> expr t -> expr t
mkOp Type resT
resT Op1 resT
Op1 Bool
op) (expr resT -> expr resT) -> m (expr resT) -> m (expr resT)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (expr resT)
m (expr Bool)
e
_ -> String -> m (expr resT)
forall a. String -> a
Err.impossible String
typeErrMsg
numOp :: Op1 resT -> m (expr resT)
numOp :: Op1 resT -> m (expr resT)
numOp op :: Op1 resT
op = (Type resT -> Op1 resT -> expr resT -> expr resT
forall t. Type t -> Op1 t -> expr t -> expr t
mkOp Type resT
resT Op1 resT
op) (expr resT -> expr resT) -> m (expr resT) -> m (expr resT)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type resT -> Expr _a -> m (expr resT)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type resT
resT Expr _a
e)
castTo :: C.Type ctb -> m (expr resT)
castTo :: Type ctb -> m (expr resT)
castTo tb :: Type ctb
tb = Type ctb -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
forall t a. Type t -> (forall t'. Type t' -> a) -> a
casting Type ctb
tb ((forall t'. Type t' -> m (expr resT)) -> m (expr resT))
-> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ \tb' :: Type t'
tb' -> case (Type t'
tb', Type resT
resT) of
(Integer, Integer) -> Type Integer -> Expr _a -> m (expr Integer)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Integer
Integer Expr _a
e
(Real, Real) -> Type Double -> Expr _a -> m (expr Double)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Double
Real Expr _a
e
_ -> String -> m (expr resT)
forall a. String -> a
Err.impossible String
typeErrMsg
notHandled ::
C.Type a -> String -> m (expr resT)
notHandled :: Type a -> String -> m (expr resT)
notHandled ta :: Type a
ta s :: String
s = Type a -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
forall t a. Type t -> (forall t'. Type t' -> a) -> a
casting Type a
ta ((forall t'. Type t' -> m (expr resT)) -> m (expr resT))
-> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ \ta' :: Type t'
ta' ->
UnhandledOp1 -> m (expr resT)
notHandledF (UnhandledOp1 -> m (expr resT)) -> UnhandledOp1 -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ String -> Type t' -> Type resT -> UnhandledOp1
forall a b. String -> Type a -> Type b -> UnhandledOp1
UnhandledOp1 String
s Type t'
ta' Type resT
resT
handleOp2 ::
forall m expr _a _b _c resT . (Monad m)
=> Type resT
-> (C.Op2 _a _b _c, C.Expr _a, C.Expr _b)
-> (forall t t'. Type t -> C.Expr t' -> m (expr t))
-> (UnhandledOp2 -> m (expr resT))
-> (forall t a . Type t -> Op2 a t -> expr a -> expr a -> expr t)
-> (expr Bool -> expr Bool)
-> m (expr resT)
handleOp2 :: Type resT
-> (Op2 _a _b _c, Expr _a, Expr _b)
-> (forall t t'. Type t -> Expr t' -> m (expr t))
-> (UnhandledOp2 -> m (expr resT))
-> (forall t a. Type t -> Op2 a t -> expr a -> expr a -> expr t)
-> (expr Bool -> expr Bool)
-> m (expr resT)
handleOp2 resT :: Type resT
resT (op :: Op2 _a _b _c
op, e1 :: Expr _a
e1, e2 :: Expr _b
e2) handleExpr :: forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr notHandledF :: UnhandledOp2 -> m (expr resT)
notHandledF mkOp :: forall t a. Type t -> Op2 a t -> expr a -> expr a -> expr t
mkOp notOp :: expr Bool -> expr Bool
notOp = case Op2 _a _b _c
op of
C.And -> Op2 Bool Bool -> m (expr resT)
boolConnector Op2 Bool Bool
And
C.Or -> Op2 Bool Bool -> m (expr resT)
boolConnector Op2 Bool Bool
Or
C.Add _ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Add
C.Sub _ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Sub
C.Mul _ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Mul
C.Mod _ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Mod
C.Div ta :: Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta "div"
C.Fdiv _ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Fdiv
C.Pow _ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Pow
C.Logb ta :: Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta "logb"
C.Eq ta :: Type _a
ta -> Type _a -> m (expr resT)
forall cta. Type cta -> m (expr resT)
eqOp Type _a
ta
C.Ne ta :: Type _a
ta -> Type _a -> m (expr resT)
forall cta. Type cta -> m (expr resT)
neqOp Type _a
ta
C.Le ta :: Type _a
ta -> Type _a -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
forall cta.
Type cta -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
numComp Type _a
ta forall num. Num num => Op2 num Bool
Le
C.Ge ta :: Type _a
ta -> Type _a -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
forall cta.
Type cta -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
numComp Type _a
ta forall num. Num num => Op2 num Bool
Ge
C.Lt ta :: Type _a
ta -> Type _a -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
forall cta.
Type cta -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
numComp Type _a
ta forall num. Num num => Op2 num Bool
Lt
C.Gt ta :: Type _a
ta -> Type _a -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
forall cta.
Type cta -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
numComp Type _a
ta forall num. Num num => Op2 num Bool
Gt
C.BwAnd ta :: Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta "bwand"
C.BwOr ta :: Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta "bwor"
C.BwXor ta :: Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta "bwxor"
C.BwShiftL ta :: Type _a
ta _tb :: Type _b
_tb -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta "bwshiftl"
C.BwShiftR ta :: Type _a
ta _tb :: Type _b
_tb -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta "bwshiftr"
where
boolOp :: Op2 a Bool -> expr a -> expr a -> expr resT
boolOp :: Op2 a Bool -> expr a -> expr a -> expr resT
boolOp op :: Op2 a Bool
op e1' :: expr a
e1' e2' :: expr a
e2' = case Type resT
resT of
Bool -> Type resT -> Op2 a resT -> expr a -> expr a -> expr resT
forall t a. Type t -> Op2 a t -> expr a -> expr a -> expr t
mkOp Type resT
resT Op2 a resT
Op2 a Bool
op expr a
e1' expr a
e2'
_ -> String -> expr resT
forall a. String -> a
Err.impossible String
typeErrMsg
boolConnector :: Op2 Bool Bool -> m (expr resT)
boolConnector :: Op2 Bool Bool -> m (expr resT)
boolConnector op :: Op2 Bool Bool
op = do
expr Bool
e1' <- Type Bool -> Expr _a -> m (expr Bool)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Bool
Bool Expr _a
e1
expr Bool
e2' <- Type Bool -> Expr _b -> m (expr Bool)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Bool
Bool Expr _b
e2
expr resT -> m (expr resT)
forall (m :: * -> *) a. Monad m => a -> m a
return (expr resT -> m (expr resT)) -> expr resT -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ Op2 Bool Bool -> expr Bool -> expr Bool -> expr resT
forall a. Op2 a Bool -> expr a -> expr a -> expr resT
boolOp Op2 Bool Bool
op expr Bool
e1' expr Bool
e2'
eqOp :: C.Type cta -> m (expr resT)
eqOp :: Type cta -> m (expr resT)
eqOp ta :: Type cta
ta = Type cta -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
forall t a. Type t -> (forall t'. Type t' -> a) -> a
casting Type cta
ta ((forall t'. Type t' -> m (expr resT)) -> m (expr resT))
-> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ \ta' :: Type t'
ta' -> do
expr t'
e1' <- Type t' -> Expr _a -> m (expr t')
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type t'
ta' Expr _a
e1
expr t'
e2' <- Type t' -> Expr _b -> m (expr t')
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type t'
ta' Expr _b
e2
expr resT -> m (expr resT)
forall (m :: * -> *) a. Monad m => a -> m a
return (expr resT -> m (expr resT)) -> expr resT -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ Op2 t' Bool -> expr t' -> expr t' -> expr resT
forall a. Op2 a Bool -> expr a -> expr a -> expr resT
boolOp Op2 t' Bool
forall a. Op2 a Bool
Eq expr t'
e1' expr t'
e2'
neqOp :: C.Type cta -> m (expr resT)
neqOp :: Type cta -> m (expr resT)
neqOp ta :: Type cta
ta = case Type resT
resT of
Bool -> do
expr resT
e <- Type cta -> m (expr resT)
forall cta. Type cta -> m (expr resT)
eqOp Type cta
ta
expr Bool -> m (expr resT)
forall (m :: * -> *) a. Monad m => a -> m a
return (expr Bool -> m (expr resT)) -> expr Bool -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ expr Bool -> expr Bool
notOp expr resT
expr Bool
e
_ -> String -> m (expr resT)
forall a. String -> a
Err.impossible String
typeErrMsg
numOp :: (forall num . (Num num) => Op2 num num) -> m (expr resT)
numOp :: (forall num. Num num => Op2 num num) -> m (expr resT)
numOp op :: forall num. Num num => Op2 num num
op = case Type resT
resT of
Integer -> do
expr Integer
e1' <- Type Integer -> Expr _a -> m (expr Integer)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Integer
Integer Expr _a
e1
expr Integer
e2' <- Type Integer -> Expr _b -> m (expr Integer)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Integer
Integer Expr _b
e2
expr resT -> m (expr resT)
forall (m :: * -> *) a. Monad m => a -> m a
return (expr resT -> m (expr resT)) -> expr resT -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ Type resT -> Op2 resT resT -> expr resT -> expr resT -> expr resT
forall t a. Type t -> Op2 a t -> expr a -> expr a -> expr t
mkOp Type resT
resT Op2 resT resT
forall num. Num num => Op2 num num
op expr resT
expr Integer
e1' expr resT
expr Integer
e2'
Real -> do
expr Double
e1' <- Type Double -> Expr _a -> m (expr Double)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Double
Real Expr _a
e1
expr Double
e2' <- Type Double -> Expr _b -> m (expr Double)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Double
Real Expr _b
e2
expr resT -> m (expr resT)
forall (m :: * -> *) a. Monad m => a -> m a
return (expr resT -> m (expr resT)) -> expr resT -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ Type resT -> Op2 resT resT -> expr resT -> expr resT -> expr resT
forall t a. Type t -> Op2 a t -> expr a -> expr a -> expr t
mkOp Type resT
resT Op2 resT resT
forall num. Num num => Op2 num num
op expr resT
expr Double
e1' expr resT
expr Double
e2'
_ -> String -> m (expr resT)
forall a. String -> a
Err.impossible String
typeErrMsg
numComp ::
C.Type cta ->
(forall num . (Num num) => Op2 num Bool) -> m (expr resT)
numComp :: Type cta -> (forall num. Num num => Op2 num Bool) -> m (expr resT)
numComp ta :: Type cta
ta op :: forall num. Num num => Op2 num Bool
op = Type cta -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
forall t a. Type t -> (forall t'. Type t' -> a) -> a
casting Type cta
ta ((forall t'. Type t' -> m (expr resT)) -> m (expr resT))
-> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ \case
Integer -> do
expr Integer
e1' <- Type Integer -> Expr _a -> m (expr Integer)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Integer
Integer Expr _a
e1
expr Integer
e2' <- Type Integer -> Expr _b -> m (expr Integer)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Integer
Integer Expr _b
e2
expr resT -> m (expr resT)
forall (m :: * -> *) a. Monad m => a -> m a
return (expr resT -> m (expr resT)) -> expr resT -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ Op2 Integer Bool -> expr Integer -> expr Integer -> expr resT
forall a. Op2 a Bool -> expr a -> expr a -> expr resT
boolOp Op2 Integer Bool
forall num. Num num => Op2 num Bool
op expr Integer
e1' expr Integer
e2'
Real -> do
expr Double
e1' <- Type Double -> Expr _a -> m (expr Double)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Double
Real Expr _a
e1
expr Double
e2' <- Type Double -> Expr _b -> m (expr Double)
forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr Type Double
Real Expr _b
e2
expr resT -> m (expr resT)
forall (m :: * -> *) a. Monad m => a -> m a
return (expr resT -> m (expr resT)) -> expr resT -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ Op2 Double Bool -> expr Double -> expr Double -> expr resT
forall a. Op2 a Bool -> expr a -> expr a -> expr resT
boolOp Op2 Double Bool
forall num. Num num => Op2 num Bool
op expr Double
e1' expr Double
e2'
_ -> String -> m (expr resT)
forall a. String -> a
Err.impossible String
typeErrMsg
notHandled :: forall a . C.Type a -> String -> m (expr resT)
notHandled :: Type a -> String -> m (expr resT)
notHandled ta :: Type a
ta s :: String
s = Type a -> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
forall t a. Type t -> (forall t'. Type t' -> a) -> a
casting Type a
ta ((forall t'. Type t' -> m (expr resT)) -> m (expr resT))
-> (forall t'. Type t' -> m (expr resT)) -> m (expr resT)
forall a b. (a -> b) -> a -> b
$ \ta' :: Type t'
ta' ->
UnhandledOp2 -> m (expr resT)
notHandledF (String -> Type t' -> Type t' -> Type t' -> UnhandledOp2
forall a b c. String -> Type a -> Type b -> Type c -> UnhandledOp2
UnhandledOp2 String
s Type t'
ta' Type t'
ta' Type t'
ta')
typeErrMsg :: String
typeErrMsg :: String
typeErrMsg = "Unexpected type error in 'Misc.CoreOperators'"