{-# 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 Op1 a
op = case Op1 a
op of
Op1 a
Neg -> String
"-"
Op1 a
Not -> String
"not"
Op1 a
Abs -> String
"abs"
Op1 a
Exp -> String
"exp"
Op1 a
Sqrt -> String
"sqrt"
Op1 a
Log -> String
"log"
Op1 a
Sin -> String
"sin"
Op1 a
Tan -> String
"tan"
Op1 a
Cos -> String
"cos"
Op1 a
Asin -> String
"asin"
Op1 a
Atan -> String
"atan"
Op1 a
Acos -> String
"acos"
Op1 a
Sinh -> String
"sinh"
Op1 a
Tanh -> String
"tanh"
Op1 a
Cosh -> String
"cosh"
Op1 a
Asinh -> String
"asinh"
Op1 a
Atanh -> String
"atanh"
Op1 a
Acosh -> String
"acosh"
instance Show (Op2 a b) where
show :: Op2 a b -> String
show Op2 a b
op = case Op2 a b
op of
Op2 a b
Eq -> String
"="
Op2 a b
Le -> String
"<="
Op2 a b
Lt -> String
"<"
Op2 a b
Ge -> String
">="
Op2 a b
Gt -> String
">"
Op2 a b
And -> String
"and"
Op2 a b
Or -> String
"or"
Op2 a b
Add -> String
"+"
Op2 a b
Sub -> String
"-"
Op2 a b
Mul -> String
"*"
Op2 a b
Mod -> String
"mod"
Op2 a b
Fdiv -> String
"/"
Op2 a b
Pow -> String
"^"
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 Type resT
resT (Op1 _a _b
op, Expr _a
e) forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr UnhandledOp1 -> m (expr resT)
notHandledF forall t. Type t -> Op1 t -> expr t -> expr t
mkOp = case Op1 _a _b
op of
Op1 _a _b
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 Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Abs
C.Sign Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta String
"sign"
C.Recip Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta String
"recip"
C.Exp Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Exp
C.Sqrt Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Sqrt
C.Log Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Log
C.Sin Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Sin
C.Tan Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Tan
C.Cos Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Cos
C.Asin Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Asin
C.Atan Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Atan
C.Acos Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Acos
C.Sinh Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Sinh
C.Tanh Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Tanh
C.Cosh Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Cosh
C.Asinh Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Asinh
C.Atanh Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Atanh
C.Acosh Type _a
_ -> Op1 resT -> m (expr resT)
numOp Op1 resT
forall a. Op1 a
Acosh
C.BwNot Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta String
"bwnot"
C.Cast Type _a
_ 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 Op1 Bool
op m (expr Bool)
e = case Type resT
resT of
Type resT
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
Type resT
_ -> 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 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 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
$ \Type t'
tb' -> case (Type t'
tb', Type resT
resT) of
(Type t'
Integer, Type resT
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
(Type t'
Real, Type resT
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
(Type t', Type resT)
_ -> 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 Type a
ta 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
$ \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 Type resT
resT (Op2 _a _b _c
op, Expr _a
e1, Expr _b
e2) forall t t'. Type t -> Expr t' -> m (expr t)
handleExpr UnhandledOp2 -> m (expr resT)
notHandledF forall t a. Type t -> Op2 a t -> expr a -> expr a -> expr t
mkOp expr Bool -> expr Bool
notOp = case Op2 _a _b _c
op of
Op2 _a _b _c
C.And -> Op2 Bool Bool -> m (expr resT)
boolConnector Op2 Bool Bool
And
Op2 _a _b _c
C.Or -> Op2 Bool Bool -> m (expr resT)
boolConnector Op2 Bool Bool
Or
C.Add Type _a
_ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Add
C.Sub Type _a
_ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Sub
C.Mul Type _a
_ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Mul
C.Mod Type _a
_ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Mod
C.Div Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta String
"div"
C.Fdiv Type _a
_ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Fdiv
C.Pow Type _a
_ -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Pow
C.Logb Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta String
"logb"
C.Eq Type _a
ta -> Type _a -> m (expr resT)
forall cta. Type cta -> m (expr resT)
eqOp Type _a
ta
C.Ne Type _a
ta -> Type _a -> m (expr resT)
forall cta. Type cta -> m (expr resT)
neqOp Type _a
ta
C.Le 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 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 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 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 Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta String
"bwand"
C.BwOr Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta String
"bwor"
C.BwXor Type _a
ta -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta String
"bwxor"
C.BwShiftL Type _a
ta Type _b
_tb -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta String
"bwshiftl"
C.BwShiftR Type _a
ta Type _b
_tb -> Type _a -> String -> m (expr resT)
forall a. Type a -> String -> m (expr resT)
notHandled Type _a
ta String
"bwshiftr"
where
boolOp :: Op2 a Bool -> expr a -> expr a -> expr resT
boolOp :: Op2 a Bool -> expr a -> expr a -> expr resT
boolOp Op2 a Bool
op expr a
e1' expr a
e2' = case Type resT
resT of
Type resT
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'
Type resT
_ -> 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 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 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
$ \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 Type cta
ta = case Type resT
resT of
Type resT
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 Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (expr Bool -> m (expr Bool)) -> expr Bool -> m (expr Bool)
forall a b. (a -> b) -> a -> b
$ expr Bool -> expr Bool
notOp expr resT
expr Bool
e
Type resT
_ -> 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 forall num. Num num => Op2 num num
op = case Type resT
resT of
Type resT
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'
Type resT
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'
Type resT
_ -> 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 Type cta
ta 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
Type t'
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'
Type t'
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'
Type t'
_ -> 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 Type a
ta 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
$ \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 = String
"Unexpected type error in 'Misc.CoreOperators'"