{-# 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

instance Trans (Term Identity) Identity where
  trans = \case
    Cons -> cons
    Char t -> char t
    Eq -> eq
    Term repr -> repr
    x :@ y -> Identity (runIdentity (trans x) (runIdentity (trans y)))
    Lam  f -> Identity (runIdentity Fun.. trans Fun.. f Fun.. Term Fun.. Identity)
    Lam1 f -> trans (Lam f)
    Var{} -> undefined
    {-
    Const -> const
    Flip -> flip
    Id -> id
    (:$) -> ($)
    -}
instance Trans (Term TH.CodeQ) TH.CodeQ where
  -- Superfluous pattern-matches are only here
  -- for cosmetic concerns when reading *.dump-splices,
  -- not for optimizing, which is done in 'optimizeTerm'.
  trans = \case
    Cons :@ x :@ y -> [|| $$(trans x) : $$(trans y) ||]
    Cons :@ x -> [|| ($$(trans x) :) ||]
    Cons -> cons
    Char t -> char t
    Eq :@ x :@ y -> [|| $$(trans x) Eq.== $$(trans y) ||]
    Eq :@ x -> [|| ($$(trans x) Eq.==) ||]
    Eq -> eq
    Term repr -> repr
    -- (:$) :@ x -> [|| ($$(trans x) Fun.$) ||]
    -- (:.) :@ f :@ g -> [|| \xx -> $$(trans f) ($$(trans g) xx) ||]
    -- (:.) :@ (:.) -> [|| \f x -> (\g y -> (f x) (g y)) ||]
    -- (:.) :@ x :@ y -> [|| $$(trans x) Fun.. $$(trans y) ||]
    -- (:.) :@ x -> [|| ($$(trans x) Fun..) ||]
    -- (:.) :@ f -> [|| \g x -> $$(trans f) (g x) ||]
    -- (:.) -> (.)
    x :@ y -> [|| $$(trans x) $$(trans y) ||]
    Lam f -> [|| \x -> $$(trans (f (Term [||x||]))) ||]
    Lam1 f -> trans (Lam f)
    Var{} -> undefined
    {-
    Const -> const
    Flip -> flip
    Id -> id
    (:$) -> ($)
    -}
instance Trans (Term ValueCode) ValueCode where
  trans = \case
    Term x -> x
    Char c -> char c
    Cons -> cons
    Eq -> eq
    (:@) f x -> (.@) (trans f) (trans x)
    Lam f -> ValueCode
      { value = value Fun.. trans Fun.. f Fun.. Term Fun.. (`ValueCode` undefined)
      , code = [|| \x -> $$(code Fun.. trans Fun.. f Fun.. Term Fun.. (undefined `ValueCode`) Fun.$ [||x||]) ||]
      }
    Lam1 f -> trans (Lam f)
    Var{} -> undefined
    {-
    Const -> const
    Flip -> flip
    Id -> id
    (:$) -> ($)
    -}
instance Trans (Term ValueCode) (Term TH.CodeQ) where
  trans = \case
    Term x -> Term (code x)
    Char c -> char c
    Cons -> cons
    Eq -> eq
    (:@) f x -> (.@) (trans f) (trans x)
    Lam f -> Lam (\x -> trans (f (trans x)))
    Lam1 f -> Lam1 (\x -> trans (f (trans x)))
    Var v -> Var v
    {-
    Const -> const
    Flip -> flip
    Id -> id
    (:$) -> ($)
    -}
instance Trans (Term TH.CodeQ) (Term ValueCode) where
  trans = \case
    Term x -> Term (ValueCode undefined x)
    Char c -> char c
    Cons -> cons
    Eq -> eq
    (:@) f x -> (.@) (trans f) (trans x)
    Lam f -> Lam (\x -> trans (f (trans x)))
    Lam1 f -> Lam1 (\x -> trans (f (trans x)))
    Var v -> Var v
    {-
    Const -> const
    Flip -> flip
    Id -> id
    (:$) -> ($)
    -}