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

{-# 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
"^"

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

-- | Some high level utilities to translate a Copilot operator in a standard way
-- | The 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)

data UnhandledOp2 = forall a b c .
  UnhandledOp2 String (Type a) (Type b) (Type c)

handleOp1 ::
  -- 'm' is the monad in which the computation is made
  -- 'resT' is the desired return type of the expression being translated
  forall m expr _a _b resT. (Functor m) =>
  -- The desired return type
  Type resT ->
  -- The unary operator encountered and its argument
  (C.Op1 _a _b, C.Expr _a) ->
  -- The monadic function to translate an expression
  -- (for recursive calls to be mmadess)
  (forall t t'. Type t -> C.Expr t' -> m (expr t)) ->
  -- A function to deal with a operators not handled by copilot-kind
  (UnhandledOp1 -> m (expr resT)) ->
  -- The Op1 constructor of the 'expr' type
  (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)

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

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

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

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

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

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

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

-- See the 'handleOp1' function for documentation
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

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

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

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

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

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

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

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

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

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