-- | This module defines the concept of expressions and expression transformers.
--
-- An expression is a type constructor of kind
--
-- > * -> * -> *
--
-- where the first argument denotes the \"role\" of the expression, and the
-- second argument is the type of the value computed by the expression.
--
-- An expression transformer is a type constructor of kind
--
-- > (* -> * -> *) -> (* -> * -> *)
--
-- i.e. a expression parameterized by an expression.

module Feldspar.DSL.Expression where



import Data.Typeable
import Unsafe.Coerce



-- | Expression type with no constructors. Can be used to turn an expression
-- transformer to an expression.
data Empty role a

-- | Equality for expressions. The difference between 'Eq' and 'ExprEq' is that
-- 'ExprEq' allows comparison of expressions with different role and value type.
-- It is assumed that when the types differ, the expressions also differ. The
-- reason for allowing comparison of different types is that this is convenient
-- when the types are existentially quantified.
class ExprEq expr
  where
    exprEq :: expr ra a -> expr rb b -> Bool

instance ExprEq Empty
  where
    exprEq _ _ = undefined

instance Eq (Empty role a)
  where
    (==) = exprEq

-- | Evaluation of expressions
class Eval expr
  where
    eval :: expr role a -> a

instance Eval Empty
  where
    eval _ = undefined

class ExprShow expr
  where
    exprShow :: expr role a -> String

instance ExprShow Empty
  where
    exprShow _ = undefined

printExpr :: ExprShow expr => expr role a -> IO ()
printExpr = putStrLn . exprShow

-- | Type-safe cast for expressions
exprCast :: forall expr ra a rb b
    .  (Typeable ra, Typeable a, Typeable rb, Typeable b)
    => expr ra a -> Maybe (expr rb b)
exprCast e = do
    cast (undefined :: ra) :: Maybe rb  -- Check that ra and rb are the same
    cast (undefined :: a)  :: Maybe b   -- Check that a and b are the same
    return (unsafeCoerce e)