LayeredTerms.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Module defining 'layered terms'.
-- At each layer, an operator from `SubSig l i` is applied
module Control.Monad.IMSOS.LayeredTerms where
import Control.Monad.IMSOS.Signatures (HasSubSig(..), TermL, Sig)
import Data.Comp.Multi ((:<:), inj, proj, HFunctor (hfmap), inject)
import qualified Data.Comp.Multi as Multi

data Term l i where 
  Term ::
   ( HasSubSig l i ) => 
      SubSig l i (Term l) i -> Term l i

unTerm :: Term l i -> SubSig l i (Term l) i
unTerm (Term l) = l

inject :: (f :<: SubSig l i, HasSubSig l i) 
  => f (Term l) i -> Term l i
inject = Term . inj

project :: (f :<: SubSig l i) => Term l i -> Maybe (f (Term l) i)
project = proj . unTerm

fixL :: forall l i. Term l i -> TermL l i
fixL = go
  where
    go :: forall j. Term l j -> TermL l j
    go (Term layer) =
      Data.Comp.Multi.inject (hfmap go layer)

-- TODO: instances below might cause significant overhead due to fixing
instance 
  (Show (Multi.Term (Sig l) i)) 
  => Show (Term l i) where 
  show = show . fixL

instance 
  (Ord (Multi.Term (Sig l) i))
  => Ord (Term l i) where 
    compare l r = compare (fixL l) (fixL r)

instance 
  (Eq (Multi.Term (Sig l) i))
  => Eq (Term l i) where 
    l == r = fixL l == fixL r