module Data.Reify.TGraph
( ShowF(..), Id, V(..), Bind(..), bindEnv, Graph(..)
) where
import Data.IsTy
import Data.Proof.EQ
import qualified Data.IntMap as I
type Id = Int
data V ty a = V Id (ty a)
instance Eq (V ty a) where V i _ == V j _ = i == j
class ShowF f where
showF :: f a -> String
instance ShowF (V ty) where
showF (V i _) = 'x' : show i
instance Show (V ty a) where show = showF
data Bind ty n = forall a. IsTyConstraint ty a => Bind (V ty a) (n (V ty) a)
instance ShowF (n (V ty)) => Show (Bind ty n) where
show (Bind v n) = showF v ++" = "++ showF n
bindEnv :: forall ty n. [Bind ty n] ->
forall a. (IsTy ty, IsTyConstraint ty a) =>
(V ty a -> n (V ty) a)
bindEnv binds = \ (V i' a') -> extract a' (I.lookup i' m)
where
m :: I.IntMap (Bind ty n)
m = I.fromList [(i,b) | b@(Bind (V i _) _) <- binds]
extract :: IsTyConstraint ty a =>
ty a -> Maybe (Bind ty n) -> n (V ty) a
extract _ Nothing = error "bindEnv: variable not found"
extract a' (Just (Bind (V _ a) n))
| Just Refl <- a `tyEq` a' = n
| otherwise = error "bindEnv: wrong type"
data Graph ty n a = Graph [Bind ty n] (V ty a)
instance (ShowF (n (V ty)), Show (V ty a)) => Show (Graph ty n a) where
show (Graph netlist start) = "let " ++ show netlist ++ " in " ++ show start