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

{-# LANGUAGE GADTs, ExistentialQuantification, LambdaCase, ScopedTypeVariables,
             RankNTypes #-}
{-# LANGUAGE Safe #-}

-- | Operators in modular transition systems and their translation.
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

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

-- | Unary operators.
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

-- | Binary operators.
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  -> "^"

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

-- | Unhandled unary operator.
--
--   Unhandled operators are monomorphic, and their names are labeled so that
--   each name corresponds to a unique uninterpreted function with a
--   monomorphic type.
data UnhandledOp1 = forall a b .
  UnhandledOp1 String (Type a) (Type b)

-- | Unhandled binary operator.
--
--   Unhandled operators are monomorphic, and their names are labeled so that
--   each name corresponds to a unique uninterpreted function with a
--   monomorphic type.
data UnhandledOp2 = forall a b c .
  UnhandledOp2 String (Type a) (Type b) (Type c)

-- | Translate an Op1.
--
-- This function is parameterized so that it can be used to translate
-- in different contexts and with different targets.
--
-- 'm' is the monad in which the computation is made
--
-- 'resT' is the desired return type of the expression being translated
handleOp1 ::
  forall m expr _a _b resT. (Functor m)

  => Type resT
     -- ^ The desired return type

  -> (C.Op1 _a _b, C.Expr _a)
     -- ^ The unary operator encountered and its argument

  -> (forall t t'. Type t -> C.Expr t' -> m (expr t))
     -- ^ The monadic function to translate an expression

  -> (UnhandledOp1 -> m (expr resT))
      -- ^ A function to deal with a operators not handled

  -> (forall t . Type t -> Op1 t -> expr t -> expr t)
     -- ^ The Op1 constructor of the 'expr' type

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

  -- Numeric operators
  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"

  -- Fractional operators
  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"

  -- Floating operators
  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

  -- Bitwise operators.
  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"

  -- Casting operator.
  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)

    -- Casting from Integer (Only possible solution)
    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

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

-- | Translate an Op2.
--
-- This function is parameterized so that it can be used to translate
-- in different contexts and with different targets.
--
-- 'm' is the monad in which the computation is made
--
-- 'resT' is the desired return type of the expression being translated
handleOp2 ::
  forall m expr _a _b _c resT . (Monad m)

  => Type resT
     -- ^ The desired return type

  -> (C.Op2 _a _b _c, C.Expr _a, C.Expr _b)
     -- ^ The binary operator encountered and its arguments

  -> (forall t t'. Type t -> C.Expr t' -> m (expr t))
     -- ^ The monadic function to translate an expression

  -> (UnhandledOp2 -> m (expr resT))
      -- ^ A function to deal with a operators not handled

  -> (forall t a . Type t -> Op2 a t -> expr a -> expr a -> expr t)
     -- ^ The Op2 constructor of the 'expr' type

  -> (expr Bool -> expr Bool)
     -- ^ The Op1 for boolean negation

  -> 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

  -- Numeric operators
  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

  -- Integral operators.
  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"

  -- Fractional operators.
  C.Fdiv _    -> (forall num. Num num => Op2 num num) -> m (expr resT)
numOp forall num. Num num => Op2 num num
Fdiv

  -- Floating operators.
  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"

  -- Equality operators.
  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

  -- Relational operators.
  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

  -- Bitwise operators.
  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"

  -- In fact, '_tb' is ignored caused it can only
  -- be casted to 'Integer', like 'ta'
  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')

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

-- | Error message for unexpected behavior / internal errors.
typeErrMsg :: String
typeErrMsg :: String
typeErrMsg = "Unexpected type error in 'Misc.CoreOperators'"

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