{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns #-}
module Symantic.Parser.Haskell.Optimize where

import Data.Bool (Bool(..))
import Data.Functor.Identity (Identity(..))
import Data.String (String)
import Prelude (undefined)
import Text.Show (Show(..))
import qualified Data.Eq as Eq
import qualified Data.Function as Fun
import qualified Language.Haskell.TH as TH
import qualified Language.Haskell.TH.Syntax as TH

import Symantic.Univariant.Trans
import Symantic.Parser.Haskell.Term

-- * Type 'Term'
-- | Initial encoding of some 'Termable' symantics,
-- useful for some optimizations in 'optimizeTerm'.
data Term repr a where
  -- | Black-box for all terms neither interpreted nor pattern-matched.
  Term :: { unTerm :: repr a } -> Term repr a

  -- Terms useful for 'optimizeTerm'.
  (:@) :: Term repr (a->b) -> Term repr a -> Term repr b
  Lam :: (Term repr a -> Term repr b) -> Term repr (a->b)
  Lam1 :: (Term repr a -> Term repr b) -> Term repr (a->b)
  Var :: String -> Term repr a

  -- Terms useful for prettier dumps.
  Char :: (TH.Lift tok, Show tok) => tok -> Term repr tok
  Cons :: Term repr (a -> [a] -> [a])
  Eq :: Eq.Eq a => Term repr (a -> a -> Bool)
  {-
  Const :: Term repr (a -> b -> a)
  Flip :: Term repr ((a -> b -> c) -> b -> a -> c)
  Id :: Term repr (a->a)
  (:$) :: Term repr ((a->b) -> a -> b)
  -- (:.) :: Term repr ((b->c) -> (a->b) -> a -> c)
-- infixr 0 :$
-- infixr 9 :.
  -}
infixl 9 :@

type instance Output (Term repr) = repr
instance Trans repr (Term repr) where
  trans = Term

instance Termable repr => Termable (Term repr) where
  lam     = Lam
  lam1    = Lam1
  (.@)    = (:@)
  cons    = Cons
  eq      = Eq
  unit    = Term unit
  bool b  = Term (bool b)
  char    = Char
  nil     = Term nil
  left    = Term left
  right   = Term right
  nothing = Term nothing
  just    = Term just
  const   = Lam1 (\x -> Lam1 (\_y -> x))
  flip    = Lam1 (\f -> Lam1 (\x -> Lam1 (\y -> f .@ y .@ x)))
  id      = Lam1 (\x -> x)
  ($)     = Lam1 (\f -> Lam1 (\x -> f .@ x))
  (.)     = Lam1 (\f -> Lam1 (\g -> Lam1 (\x -> f .@ (g .@ x))))

-- | Beta-reduce the left-most outer-most lambda abstraction (aka. normal-order reduction),
-- but to avoid duplication of work, only those manually marked
-- as using their variable at most once.
-- This is mainly to get prettier splices.
-- 
-- DOC: Demonstrating Lambda Calculus Reduction, Peter Sestoft, 2001,
-- https://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf
optimizeTerm :: Term repr a -> Term repr a
optimizeTerm = nor
  where
  -- | normal-order reduction
  nor :: Term repr a -> Term repr a
  nor = \case
    Lam f -> Lam (nor Fun.. f)
    Lam1 f -> Lam1 (nor Fun.. f)
    x :@ y -> case whnf x of
      Lam1 f -> nor (f y)
      x' -> nor x' :@ nor y
    x -> x
  -- | weak-head normal-form
  whnf :: Term repr a -> Term repr a
  whnf = \case
    x :@ y -> case whnf x of
      Lam1 f -> whnf (f y)
      x' -> x' :@ y
    x -> x