simplify.hs

{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE GADTs                 #-}

module Main (main) where

import Data.Comp.Multi
import Data.Comp.Multi.Show ()
import Data.Comp.Multi.Equality ()
import Data.Comp.Multi.Ordering ()
import Data.Comp.Multi.Derive
import Data.Comp.Multi.Ops

data Value e l where
  Const ::        Int -> Value e Int
  Pair  :: e i -> e j -> Value e (i,j)

data Op e l where
  Add, Mult :: e Int -> e Int   -> Op e Int
  Fst       ::          e (i,j) -> Op e i
  Snd       ::          e (i,j) -> Op e j

type Sig = Op :+: Value

$(derive [makeHFunctor, makeHFoldable, makeHTraversable, makeShowHF, makeEqHF,
          makeOrdHF, smartConstructors, smartAConstructors] 
          [''Value, ''Op])

simplify :: Term Sig :-> Term Sig
simplify = transform simplifyTf
  where simplifyTf :: Term Sig :-> Term Sig
        simplifyTf t = case unTerm t of
          Inl t' -> op t'
          Inr _  -> t

        op :: Op (Term Sig) :-> Term Sig
        op t@(Add t' t'') | t' == t'' = iMult (iConst 2) t'
                          | otherwise = inject t
        op t                          = inject t

class Simplify f where
  simplifyCoa :: CVCoalg f (Term f)

simplify' :: (HFunctor f, Simplify f) => Term f :-> Term f
simplify' = futu simplifyCoa

instance Simplify Sig where
  simplifyCoa = simplifyCoa'
    where simplifyCoa' :: CVCoalg Sig (Term Sig)
          simplifyCoa' t = case unTerm t of
            Inl t'     -> op t'
            t'@(Inr _) -> hfmap Hole t'

          op :: forall l. Op (Term Sig) l -> Sig (Context Sig (Term Sig)) l
          op t@(Add t' t'') | t' == t'' = Inl (Mult (iConst 2) (Hole t'))
                            | otherwise = Inl (hfmap Hole t)
          op t                          = Inl (hfmap Hole t)

exs :: [E (Term Sig)]
exs = [E (iAdd (iConst 1) (iConst 1)),
       E (iAdd (iConst 1) (iAdd (iConst 1) (iConst 1))),
       E (iAdd (iAdd (iConst 1) (iConst 1)) (iAdd (iConst 1) (iConst 1)))]

main :: IO ()
main = do
  putStrLn "transform:"
  demo simplify  exs
  putStrLn "futu:"
  demo simplify' exs
    where demo :: (Term Sig :-> Term Sig) -> [E (Term Sig)] -> IO ()
          demo f xs = mapM_ putStrLn $ runE (show . f) <$> xs