module Facts.Utility.Templates ( list_to_bijection
                               , list_to_injection
                               , list_to_injection_via_pushout
                               , list_to_injection_via_pullback
                               ) where

import Control.Monad
import Data.Data
import Language.Haskell.TH
import Language.Haskell.TH.Quote


-- The list must be the list encoding of the extension of a bijective function
list_to_bijection :: (Data a, Data b) => String -> String -> [(a,b)] -> Q [Dec]
list_to_bijection left_name right_name xs = do 
        m1 <- list_to_injection left_name  xs
        m2 <- list_to_injection right_name (adjoint xs)
        return $ m1 ++ m2

-- The list must be the list encoding of the extension of an injective function.
list_to_injection:: (Data a, Data b) => String -> [(a,b)] -> Q [Dec]
list_to_injection name xs = liftM (\x -> [x]) $ liftM (FunD $ mkName name) (mapM mkClause xs)
    where
      mkClause (a,b) = do
        a_pat <- dataToPatQ (const Nothing) a
        b_exp <- dataToExpQ (const Nothing) b
        return $ Clause [a_pat] (NormalB b_exp) []


-- | Use precomposition to access projections on values in the co-domain.  The list must be the extension
--   of an injective function.
list_to_injection_via_pushout :: (Data a, Data b, Data c) => String -> (b -> c) -> [(a,b)] -> Q [Dec]
list_to_injection_via_pushout name f xs = (list_to_injection name) (fmap (apply_right f) xs)

-- | Use precomposition to access injections on values in the domain.  The list must be the extension
--   of an injective function.  The function by which we pull back must be an injection into the domain.
list_to_injection_via_pullback :: (Data a, Data b, Data c) => String -> (b -> c) -> [(a, b)] -> Q [Dec]
list_to_injection_via_pullback name f xs = (list_to_injection name (adjoint $ fmap (apply_right f) xs)) 

                                                
flip_pair :: (a, b) -> (b, a)
flip_pair = \(a, b) -> (b, a)


adjoint :: [(a,b)] -> [(b,a)]
adjoint = fmap flip_pair

apply_left :: (a -> c) -> (a, b) -> (c, b)
apply_left f (a, b) = (f a, b)

apply_right :: (b -> c) -> (a, b) -> (a, c)
apply_right f (a, b) = (a, f b)