{-# LANGUAGE QuasiQuotes, TypeOperators, TypeFamilies, GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
  UndecidableInstances #-}

{- |

Module      :  Data.Yoko.Algebra
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Catamorphism for mutually-recursive datatypes.

-}
module Data.Yoko.Cata
  (Algebras, SiblingAlgs, algebras, CataU(..), catas, cata,
  module Data.Yoko.Reduce) where
    
import Type.Yoko

import Data.Yoko.Generic
import Data.Yoko.Reflect
import Data.Yoko.Reduce





type Algebras ts m = Each ts (Algebra m)
type SiblingAlgs t m = Algebras (Siblings t) m

-- | Builds an 'Each' of algebras via 'AlgebraDT'.
algebras :: forall ts m. (ts ::: All (AlgebraU m)) => [qP|m|] -> Algebras ts m
algebras _ = each [qP|AlgebraU m :: *->*|] $ \AlgebraU -> algebraDT




-- | @t@ inhabits @CataU ts m@ if
--
--   1. @t@ is an instance of 'DT' and @ts ~ Siblings t@
--
--   2. the recursive reduction can be mapped as a 'FromAt' function via
--   'RMMap' across all constructors of @t@ and
--
--   3. all of @t@'s siblings also inhabit the same universe.
data CataU ts m t where
  CataU :: (DT t, ts ~ Siblings t, ts ::: Exists ((:=:) t),
            DCs t ::: All
              (YieldsArrowTSSU
               (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),
            ts ::: All (CataU ts m)
           ) => CataU ts m t
instance (DT t, ts ~ Siblings t, ts ::: Exists ((:=:) t),
          DCs t ::: All
            (YieldsArrowTSSU
             (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),
          ts ::: All (CataU ts m)
         ) => t ::: CataU ts m where inhabits = CataU

catas :: forall m ts. (ts ::: All (CataU ts m)) =>
         Algebras ts m -> Each ts (FromAt m IdM)
catas fs = each [qP|CataU ts m :: *->*|] $ \d@CataU -> cataD d fs

cataD :: forall m t. CataU (Siblings t) m t -> SiblingAlgs t m -> t -> Med m t
cataD CataU fs =
  appNT fs (inhabits :: Uni (Siblings t) t) .
  appNTtoNP (eachArrow $ AsComp $ composeWith [qP|N :: *->*|] $
             RMMap $ catas fs) . disband

-- | Uses the @m@-mediated algebras for @t@'s siblings to reduce a @t@ to @Med
-- m t@.
cata :: (t ::: CataU (Siblings t) m) => SiblingAlgs t m -> t -> Med m t
cata = cataD inhabits