module Language.Syntactic.Features.Literal where
import Data.Typeable
import Data.Hash
import Data.Proxy
import Language.Syntactic
data Literal ctx a
where
Literal :: (Eq a, Show a, Typeable a, Sat ctx a) =>
a -> Literal ctx (Full a)
instance WitnessCons (Literal ctx)
where
witnessCons (Literal _) = ConsWit
instance WitnessSat (Literal ctx)
where
type Context (Literal ctx) = ctx
witnessSat (Literal _) = Witness'
instance ExprEq (Literal ctx)
where
Literal a `exprEq` Literal b = case cast a of
Just a' -> a'==b
Nothing -> False
exprHash (Literal a) = hash (show a)
instance Render (Literal ctx)
where
render (Literal a) = show a
instance ToTree (Literal ctx)
instance Eval (Literal ctx)
where
evaluate (Literal a) = fromEval a
litCtx :: (Eq a, Show a, Typeable a, Sat ctx a, Literal ctx :<: dom) =>
Proxy ctx -> a -> ASTF dom a
litCtx ctx = inject . (`withContext` ctx) . Literal
lit :: (Eq a, Show a, Typeable a, Literal Poly :<: dom) => a -> ASTF dom a
lit = litCtx poly
prjLiteral :: (Literal ctx :<: sup) =>
Proxy ctx -> sup a -> Maybe (Literal ctx a)
prjLiteral _ = project