
module DDC.Type.Transform.AnonymizeT
        ( anonymizeT
        , AnonymizeT(..)
        , pushAnonymizeBindT)
where
import DDC.Type.Exp.Simple
import Data.List
import qualified DDC.Type.Sum           as T


-- | Rewrite all binders in a thing to be of anonymous form.
anonymizeT :: (Ord n, AnonymizeT c) => c n -> c n
anonymizeT xx
        = anonymizeWithT [] xx


-------------------------------------------------------------------------------
class AnonymizeT (c :: * -> *) where

 -- | Rewrite all binders in a thing to be of anonymous form.
 --
 --   The stack contains existing anonymous binders that we have entered into,
 --   and named binders that we have rewritten. All bound occurrences of variables
 --   will be replaced by references into this stack.
 anonymizeWithT :: forall n. Ord n => [Bind n] -> c n -> c n


instance AnonymizeT Type where
 anonymizeWithT kstack tt
  = case tt of
        TVar u  -> TVar $ anonymizeWithT kstack u
        TCon{}  -> tt

        TAbs b t
         -> let (kstack', b') = pushAnonymizeBindT kstack b
            in  TAbs b' (anonymizeWithT kstack' t)

        TApp t1 t2 -> TApp (anonymizeWithT kstack t1) (anonymizeWithT kstack t2)

        TForall b t
         -> let (kstack', b') = pushAnonymizeBindT kstack b
            in  TForall b' (anonymizeWithT kstack' t)

        TSum ss -> TSum (anonymizeWithT kstack ss)
        TRow r  -> TRow [ (l, anonymizeWithT kstack t) | (l, t) <- r ]


instance AnonymizeT TypeSum where
 anonymizeWithT kstack ss
        = T.fromList (anonymizeWithT kstack $ T.kindOfSum ss)
        $ map (anonymizeWithT kstack)
        $ T.toList ss


instance AnonymizeT Bound where
 anonymizeWithT kstack bb
  = case bb of
        UName _
         | Just ix      <- findIndex (boundMatchesBind bb) kstack
         -> UIx ix

        _ -> bb


-- Push ----------------------------------------------------------------------
-- | Push a binding occurrence of a level-1 variable on the stack,
--   returning the anonyized binding occurrence and the new stack.
pushAnonymizeBindT
  ^ Stack for Spec binders ( level-1 )
        -> Bind n
        -> ([Bind n], Bind n)

pushAnonymizeBindT kstack b
 = let  t'      = typeOfBind b
        kstack' = b : kstack
   in   (kstack', BAnon t')


 | Rewrite all binders in a thing to be of anonymous form.
-----------------------------------------------------------------------------
 | Rewrite all binders in a thing to be of anonymous form.

   The stack contains existing anonymous binders that we have entered into,
   and named binders that we have rewritten. All bound occurrences of variables
   will be replaced by references into this stack.
 Push ----------------------------------------------------------------------
 | Push a binding occurrence of a level-1 variable on the stack,
   returning the anonyized binding occurrence and the new stack.

module DDC.Type.Transform.AnonymizeT
        ( anonymizeT
        , AnonymizeT(..)
        , pushAnonymizeBindT)
where
import DDC.Type.Exp.Simple
import Data.List
import qualified DDC.Type.Sum           as T


anonymizeT :: (Ord n, AnonymizeT c) => c n -> c n
anonymizeT xx
        = anonymizeWithT [] xx


class AnonymizeT (c :: * -> *) where

 anonymizeWithT :: forall n. Ord n => [Bind n] -> c n -> c n


instance AnonymizeT Type where
 anonymizeWithT kstack tt
  = case tt of
        TVar u  -> TVar $ anonymizeWithT kstack u
        TCon{}  -> tt

        TAbs b t
         -> let (kstack', b') = pushAnonymizeBindT kstack b
            in  TAbs b' (anonymizeWithT kstack' t)

        TApp t1 t2 -> TApp (anonymizeWithT kstack t1) (anonymizeWithT kstack t2)

        TForall b t
         -> let (kstack', b') = pushAnonymizeBindT kstack b
            in  TForall b' (anonymizeWithT kstack' t)

        TSum ss -> TSum (anonymizeWithT kstack ss)
        TRow r  -> TRow [ (l, anonymizeWithT kstack t) | (l, t) <- r ]


instance AnonymizeT TypeSum where
 anonymizeWithT kstack ss
        = T.fromList (anonymizeWithT kstack $ T.kindOfSum ss)
        $ map (anonymizeWithT kstack)
        $ T.toList ss


instance AnonymizeT Bound where
 anonymizeWithT kstack bb
  = case bb of
        UName _
         | Just ix      <- findIndex (boundMatchesBind bb) kstack
         -> UIx ix

        _ -> bb


pushAnonymizeBindT
  ^ Stack for Spec binders ( level-1 )
        -> Bind n
        -> ([Bind n], Bind n)

pushAnonymizeBindT kstack b
 = let  t'      = typeOfBind b
        kstack' = b : kstack
   in   (kstack', BAnon t')

