Model of CPP tokens

CommaSep.hs

{-# LANGUAGE PolyKinds, TypeOperators, TypeFamilies, KindSignatures, DataKinds, GADTs #-}
{-# OPTIONS_GHC -Wall #-}
module CommaSep where

-- classify tokens as either the empty token, or not 
data P = Empty | NonEmpty

-- space-separated token values 'a' with a kind index tracking whether they're populated
data Token a :: P -> * where
  -- the empty token
  EmptyT :: Token a 'Empty
  NET :: NonEmptyToken a -> Token a 'NonEmpty

-- one or more non-empty tokens
data NonEmptyToken a = OneT !a | !(NonEmptyToken a) :*: !(NonEmptyToken a)

infixl 7 :*:

-- classify groups by whether at lest one comma occurs in them or not
data Comma = NoComma | Comma

-- comma separated groups of 'a' tokens with kind indices tracking
-- whether the leading and trailing tokens are empty, and whether the
-- group has at least one comma.
data Group a :: P -> Comma -> P -> * where
  -- the empty group
  EmptyG :: Group a 'Empty 'NoComma 'Empty
  -- singleton group of a non-empty token
  OneG :: !(Token a 'NonEmpty) -> Group a 'NonEmpty 'NoComma 'NonEmpty
  -- (possibly empty) token comma separated from a comma-separated token group
  (:+:) :: !(Token a l) -> !(Group a m c r) -> Group a l 'Comma r

infixl 6 :+:

-- join in the "is populated" lattice
type family (x :: P) \/ (y :: P) :: P where
  'Empty \/ a = a
  'NonEmpty \/ b = 'NonEmpty
  a \/ 'NonEmpty = 'NonEmpty
  a \/ 'Empty = a

-- when adjoining a token to a group, what happens at the far end of the group
-- depends on whether the group has a comma - the comma absorbs any modifications
--   T <| [empty group] = T
--   T <| left , ...rest... end =  T * left , ... rest ... end
type family Absorb c old new where
  Absorb 'Comma old new = old
  Absorb 'NoComma old new = new
  Absorb c x x = x

-- existential quantification over the rightmost index of a type constructor 
data ExR (f :: k -> *) :: * where
  SomeR :: f r -> ExR f


-- place a token next to a group with a space between them
(<|) :: Token a l -> Group a m c r -> Group a (l \/ m) c (Absorb c r (l \/ r))
EmptyT   <| g             = g
t@NET {} <| EmptyG        = OneG t
NET t1   <| (NET t2 :+: g) = NET (t1 :*: t2) :+: g
NET t1   <| OneG (NET t2) = OneG (NET (t1 :*: t2))
t@NET {}   <| (EmptyT :+: g) = t :+: g

(|>) :: Group a l c m -> Token a r -> Group a (Absorb c l (r \/ l)) c (r \/ m)
g |> EmptyT = g
EmptyG |> t@NET {} = OneG t
OneG (NET t1) |> NET t2 = OneG (NET (t1 :*: t2))
(tl :+: g2) |> t = tl :+: g2 |> t

infixl 6 |>
infixr 6 <|

type family JoinC c1 c2 where
  JoinC 'NoComma c2 = c2
  JoinC 'Comma c2 = 'Comma
  JoinC c1 'NoComma = c1

(|><|) :: Group a l c1 m1 -> Group a m2 c2 r -> Group a (Absorb c1 l (m2 \/ l)) (JoinC c1 c2) (Absorb c2 r (m1 \/ r))
EmptyG |><| g = g
g |><| EmptyG = g
OneG (t@NET{}) |><| g = t <| g
(tl :+: gl) |><| gr = tl :+: (gl |><| gr)


data SomeGroup a where
  SomeGroup :: Group a l c r -> SomeGroup a

foreach :: (ExR (Token a) -> SomeGroup b) -> Group a l c r -> SomeGroup b
foreach _f EmptyG = SomeGroup EmptyG
foreach f (OneG t) = f (SomeR t)
foreach f (tl :+: gr) = case f (SomeR tl) of
   SomeGroup gl' -> case foreach f gr of
     SomeGroup gr' -> SomeGroup (gl' |><| gr')