{-# LANGUAGE
  TypeOperators
, MultiParamTypeClasses
, FlexibleInstances
, OverlappingInstances
, FlexibleContexts #-}

module Calculus.Expr where

{-
  This module generalizes expressions.
-}  

import Auxiliary.List
import Auxiliary.NameSource

import Data.Functor
import Control.Monad.State

-- Coproduct type definition
data (f :+: g) a = Inl (f a) | Inr (g a)
  deriving Show

-- Making it to be right-assoc in order
-- to get linear search on it later
infixr 6 :+:

-- Making it to be functor in order to fold it later
instance (Functor f, Functor g) => Functor (f :+: g) where
  fmap f (Inl x) = Inl $ fmap f x
  fmap f (Inr x) = Inr $ fmap f x
  
-- Expr is a data type, which generates a recursive
-- Expr over whatever constructors are present in its
-- functor argument f. This argument must be a coproduct
-- type made of subExprs which can be found in subtrees
-- of Expr.
newtype Expr f = In { out :: f (Expr f) }

{-
    In  :: f (Expr f) -> Expr f
    out :: Expr f -> f (Expr f)
    
    `In` rolls one layer of Expr
    `out` unrolls one layer of Expr
    
    These functions allows to operate on
    outermost constructor
-}

-- To fold Expr
foldExpr :: Functor f => (f a -> a) -> Expr f -> a
foldExpr f = f . fmap (foldExpr f) . out

{-
  Here `f` is an algebra which tells us how to fold
  a Expr's layer
-}

{-
  Consider types
  
    data A a = A a a
    data B b = B b
    data C c = C
    
  And suppose that we want to make a Expr of type
    
    Expr (A :+: B :+: C)
    
  (:+:) is right-associative, so this type may be rewritten as
  
    Expr (A :+: (B :+: C))
    
  Signature of this type may be considered as list,
  where `A` is a head and `B :+: C` is a tail. To get
  head, we can use `Inl`; to get tail - `Inr`.
  
  Having that in mind, we can write correct expression
  `A (B (C)) C` to suit this type definition:
  
  abcExpr :: Expr (A :+: B :+: C)
  abcExpr = In (Inl (A
                         (In (Inr (Inl (B
                                         (In (Inr (Inr C)))))))
                         (In (Inr (Inr C))))) 
  
  Using (:+:) to construct Expr in modular fashion
  comes with overhead on constructors. It's not
  wise to turn types from signature into a signature
  each time by hands. It can be automated.
  
-}

class (Functor sub, Functor sup) => sub :<: sup where
  inj :: sub a -> sup a
  prj :: sup a -> Maybe (sub a)
  
instance Functor f => f :<: f where
  inj = id
  prj = Just . id
  
instance (Functor f, Functor g) => f :<: (f :+: g) where
  inj = Inl
  prj (Inl f) = Just f
  prj _       = Nothing

instance (Functor f, Functor g, Functor h, f :<: g) => f :<: (h :+: g) where
  inj = Inr . inj
  prj (Inr g) = prj g
  prj _       = Nothing  
  
-- rolls next layer
inject :: (g :<: f) => g (Expr f) -> Expr f
inject = In . inj

-- unrolls layer
match :: (g :<: f) => Expr f -> Maybe (g (Expr f))
match (In f) = prj f

{- Rendering -}

class Render f where
  render :: (NameState ns m, Render g) => f (Expr g) -> m String

instance (Render f, Render g) => Render (f :+: g) where
  render (Inl f) = render f
  render (Inr f) = render f

pretty :: (NameSource ns, Render f) => ns -> Expr f -> String
pretty ns f = evalState (render $ out f) ns

prettyPair ::
  (NameSource ns, Render f, Render g) => ns -> (Expr f, Expr g) -> (String, String)
prettyPair ns (a, b) =
  let
    (aSrc, bSrc) = splitSrc ns
    aString = pretty aSrc a
    bString = pretty bSrc b
  in (aString, bString)
  
renderPair ::
  (NameState ns m, Render f) => (Expr f, Expr f) -> m (String, String)
renderPair (a, b) = get >>= return . flip prettyPair (a, b)

renderBinOp ::
  (NameState ns m, Render f) => String -> (Expr f, Expr f) -> m String
renderBinOp op pair =
  do (a, b) <- renderPair pair
     return $ between "(" ")" $ between a b $ between " " " " op
     
showExprs :: (NameSource ns, Render f) => ns -> [Expr f] -> String
showExprs ns = showColumn . map (pretty ns) 
