{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module TFHOE.Expr.Common where

import Data.Proxy (Proxy(..))
import GHC.Prim (Constraint)

import TFHOE.Type

-- * Class 'Expr_from'

class Expr_from raw (ty:: {-h-}* -> *) (ty_end:: {-h-}* -> *) where
	expr_from
	 :: forall hs ret
	 .  Proxy ty
	 -> Proxy ty_end
	 -> Context (Var ty_end) hs
	 -> raw
	 -> (forall h. ty_end h -> Forall_Repr_with_Context ty_end hs h
	                        -> Either Error_Type ret)
	 -> Either Error_Type ret

-- ** Type 'Expr_from_Type'

-- | A type family recursively accumulating the expressions
-- an interpreter will have to support.
type family   Expr_from_Type (ty:: * -> *) (repr:: * -> *) :: Constraint
type instance Expr_from_Type Type_End repr = ()

-- ** Type 'Forall_Repr_with_Context'

-- | A data type embedding a universal quantification over @repr@
-- to construct an expression polymorphic enough to stay
-- interpretable by different interpreters;
-- moreover the expression is abstracted by a 'Context'
-- built at parsing time.
data Forall_Repr_with_Context ty hs h
 =   Forall_Repr_with_Context
 (   forall repr. Expr_from_Type ty repr =>
                  Context repr hs -> repr h )

-- ** Type 'Forall_Repr'

data Forall_Repr ty h
 =   Forall_Repr
 { unForall_Repr :: forall repr
                 .  Expr_from_Type ty repr
                 => repr h }