Term.hs

{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
-- | Haskell terms which are interesting
-- to pattern-match when optimizing.
module Symantic.Parser.Haskell.Term where

import Data.Bool (Bool(..))
import Data.Either (Either(..))
import Data.Eq (Eq)
import Data.Maybe (Maybe(..))
import Data.Functor.Identity (Identity(..))
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 qualified Symantic.Univariant.Trans as Sym

-- * Class 'Termable'
-- | Single-out some Haskell terms in order to 
class Termable repr where
  -- | Application, aka. unabstract.
  (.@) :: repr (a->b) -> repr a -> repr b
  -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  lam :: (repr a -> repr b) -> repr (a->b)
  -- | Like 'lam' but whose argument is used only once,
  -- hence safe to beta-reduce (inline) without duplicating work.
  lam1 :: (repr a -> repr b) -> repr (a->b)

  -- Singled-out terms
  bool :: Bool -> repr Bool
  char :: (TH.Lift tok, Show tok) => tok -> repr tok
  cons :: repr (a -> [a] -> [a])
  nil :: repr [a]
  eq :: Eq a => repr (a -> a -> Bool)
  unit :: repr ()
  left :: repr (l -> Either l r)
  right :: repr (r -> Either l r)
  nothing :: repr (Maybe a)
  just :: repr (a -> Maybe a)
  const :: repr (a -> b -> a)
  flip :: repr ((a -> b -> c) -> b -> a -> c)
  id :: repr (a->a)
  (.) :: repr ((b->c) -> (a->b) -> a -> c)
  ($) :: repr ((a->b) -> a -> b)

  default (.@) ::
    Sym.Liftable2 repr => Termable (Sym.Output repr) =>
    repr (a->b) -> repr a -> repr b
  default lam ::
    Sym.Liftable repr => Sym.Unliftable repr => Termable (Sym.Output repr) =>
    (repr a -> repr b) -> repr (a->b)
  default lam1 ::
    Sym.Liftable repr => Sym.Unliftable repr => Termable (Sym.Output repr) =>
    (repr a -> repr b) -> repr (a->b)
  default bool ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    Bool -> repr Bool
  default char ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    TH.Lift tok => Show tok =>
    tok -> repr tok
  default cons ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr (a -> [a] -> [a])
  default nil ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr [a]
  default eq ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    Eq a => repr (a -> a -> Bool)
  default unit ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr ()
  default left ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr (l -> Either l r)
  default right ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr (r -> Either l r)
  default nothing ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr (Maybe a)
  default just ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr (a -> Maybe a)
  default const ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr (a -> b -> a)
  default flip ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr ((a -> b -> c) -> b -> a -> c)
  default id ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr (a->a)
  default (.) ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr ((b->c) -> (a->b) -> a -> c)
  default ($) ::
    Sym.Liftable repr => Termable (Sym.Output repr) =>
    repr ((a->b) -> a -> b)

  (.@) = Sym.lift2 (.@)
  lam f = Sym.lift (lam (Sym.trans Fun.. f Fun.. Sym.trans))
  lam1 f = Sym.lift (lam1 (Sym.trans Fun.. f Fun.. Sym.trans))
  bool = Sym.lift Fun.. bool
  char = Sym.lift Fun.. char
  cons = Sym.lift cons
  nil = Sym.lift nil
  eq = Sym.lift eq
  unit = Sym.lift unit
  left = Sym.lift left
  right = Sym.lift right
  nothing = Sym.lift nothing
  just = Sym.lift just
  const = Sym.lift const
  flip = Sym.lift flip
  id = Sym.lift id
  (.) = Sym.lift (.)
  ($) = Sym.lift ($)
infixr 0 $
infixr 9 .
infixl 9 .@

-- * Type 'ValueCode'
data ValueCode a = ValueCode
  { value :: a
  , code :: TH.CodeQ a
  }
instance Termable ValueCode where
  f .@ x = ValueCode
    { value = runIdentity (Identity (value f) .@ (Identity (value x)))
    , code = code f .@ code x
    }
  lam f = ValueCode
    { value = runIdentity (lam (Identity Fun.. value Fun.. f Fun.. (`ValueCode` undefined) Fun.. runIdentity))
    , code  = lam (code Fun.. f Fun.. ValueCode undefined)
    }
  lam1     = lam
  bool b   = ValueCode (runIdentity (bool b)) (bool b)
  char c   = ValueCode (runIdentity (char c)) (char c)
  cons     = ValueCode (runIdentity cons) cons
  nil      = ValueCode (runIdentity nil) nil
  eq       = ValueCode (runIdentity eq) eq
  unit     = ValueCode (runIdentity unit) unit
  left     = ValueCode (runIdentity left) left
  right    = ValueCode (runIdentity right) right
  nothing  = ValueCode (runIdentity nothing) nothing
  just     = ValueCode (runIdentity just) just
  const    = ValueCode (runIdentity const) const
  flip     = ValueCode (runIdentity flip) flip
  id       = ValueCode (runIdentity id) id
  ($)      = ValueCode (runIdentity ($)) ($)
  (.)      = ValueCode (runIdentity (.)) (.)
instance Termable Identity where
  f .@ x   = Identity (runIdentity f (runIdentity x))
  lam f    = Identity (runIdentity Fun.. f Fun.. Identity)
  lam1     = lam
  bool     = Identity
  char     = Identity
  cons     = Identity (:)
  nil      = Identity []
  eq       = Identity (Eq.==)
  unit     = Identity ()
  left     = Identity Left
  right    = Identity Right
  nothing  = Identity Nothing
  just     = Identity Just
  const    = Identity Fun.const
  flip     = Identity Fun.flip
  id       = Identity Fun.id
  ($)      = Identity (Fun.$)
  (.)      = Identity (Fun..)
instance Termable TH.CodeQ where
  (.@) f x = [|| $$f $$x ||]
  lam f    = [|| \x -> $$(f [||x||]) ||]
  lam1     = lam
  bool b   = [|| b ||]
  char c   = [|| c ||]
  cons     = [|| (:) ||]
  nil      = [|| [] ||]
  eq       = [|| (Eq.==) ||]
  unit     = [|| () ||]
  left     = [|| Left ||]
  right    = [|| Right ||]
  nothing  = [|| Nothing ||]
  just     = [|| Just ||]
  const    = [|| Fun.const ||]
  id       = [|| \x -> x ||]
  flip     = [|| \f x y -> f y x ||]
  ($)      = [|| (Fun.$) ||]
  (.)      = [|| (Fun..) ||]