content: {-# LANGUAGE ImplicitParams #-}
  {-|
  Module      : Parsley.Internal.Core.Lam
  Description : Generic defunctionalised abstraction.
  License     : BSD-3-Clause
  Maintainer  : Jamie Willis
  Stability   : experimental
  
  This module contains `Lam`, which is a defunctionalised lambda calculus.
  This serves as a more easy to work with form of defunctionalisation moving
  into the backend and machine where it is no longer necessary to inspect function
  values. It permits for the generation of efficient terms, with some inspection
  of values.
  
  @since 1.0.1.0
  -}
  module Parsley.Internal.Core.Lam (normaliseGen, normalise, Lam(..), andLam, orLam, notLam) where
  
  import Parsley.Internal.Common.Utils   (Code)
  import Parsley.Internal.Common.THUtils (eta)
  
  import qualified Parsley.Internal.Opt   as Opt
  
  {-|
  Defunctionalised lambda calculus in HOAS form. Supports basic inspection
  of values, but not functions.
  
  @since 1.0.1.0
  -}
  data Lam a where
      -- | Function abstraction.
      Abs :: (Lam a -> Lam b) -> Lam (a -> b)
      -- | Function application.
      App :: Lam (a -> b) -> Lam a -> Lam b
      -- | Variable. The boolean represents whether it is "simple" or "complex", i.e. the size of the term.
      Var :: Bool {- Simple -} -> Code a -> Lam a
      -- | Conditional expression.
      If  :: Lam Bool -> Lam a -> Lam a -> Lam a
      -- | Let-binding.
      Let :: Lam a -> (Lam a -> Lam b) -> Lam b
      -- | Value representing true.
      T   :: Lam Bool
      -- | Value representing false.
      F   :: Lam Bool
  
  andLam :: Lam Bool -> Lam Bool -> Lam Bool
  andLam x y = If x y F
  
  orLam :: Lam Bool -> Lam Bool -> Lam Bool
  orLam x = If x T
  
  notLam :: Lam Bool -> Lam Bool
  notLam x = If x F T
  
  {-|
  Optimises a `Lam` expression, reducing it until the outmost lambda, let, or if statement.
  
  @since 1.0.1.0
  -}
  normalise :: (?flags :: Opt.Flags) => Lam a -> Lam a
  normalise x = if normal x || not (Opt.termNormalisation ?flags) then x else reduce x
    where
      reduce :: Lam a -> Lam a
      reduce (App (Abs f) x) = normalise (f x)
      reduce (App f x) = case reduce f of
        f@Abs{} -> reduce (App f x)
        f       -> App f x
      reduce (If T t _) = normalise t
      reduce (If F _ f) = normalise f
      reduce (If _ T T) = T
      reduce (If _ F F) = F
      reduce (If c T F) = normalise c
      -- one of them must be not in normal form
      reduce (If c t f) = normalise (If (normalise c) (normalise t) (normalise f))
      -- Reduction rule found courtesy of David Davies, forever immortalised
      reduce (Let v@(Var True _) f) = normalise (f v)
      reduce x = x
  
      normal :: Lam a -> Bool
      normal (App (Abs _) _) = False
      normal (App f _) = normal f
      normal (If T _ _) = False
      normal (If F _ _) = False
      normal (If _ T T) = False
      normal (If _ F F) = False
      normal (If _ T F) = False
      normal (If c t f) = normal c && normal t && normal f
      normal (Let (Var True _) _) = False
      normal _ = True
  
  generate :: (?flags :: Opt.Flags) => Lam a -> Code a
  generate (Abs f)    = [|| \x -> $$(normaliseGen (f (Var True [||x||]))) ||]
  -- f has already been reduced, since we only expose `normaliseGen`
  generate (App f x)  = [|| $$(generate f) $$(normaliseGen x) ||]
  generate (Var _ x)  = x
  -- all parts are reduced
  generate (If c T e) = [|| $$(generate c) || $$(generate e) ||]
  generate (If c t F) = [|| $$(generate c) && $$(generate t) ||]
  generate (If c F T) = [|| not $$(generate c) ||]
  generate (If c t e) = [|| if $$(generate c) then $$(generate t) else $$(generate e) ||]
  generate (Let b i)  = [|| let x = $$(normaliseGen b) in $$(normaliseGen (i (Var True [||x||]))) ||]
  generate T          = [|| True ||]
  generate F          = [|| False ||]
  
  {-|
  Generates Haskell code that represents a `Lam` value, but normalising it first to ensure the
  term is minimal.
  
  @since 1.0.1.0
  -}
  normaliseGen :: (?flags :: Opt.Flags) => Lam a -> Code a
  normaliseGen = eta . generate . normalise
  
  instance Show (Lam a) where
    show = let ?flags = Opt.none { Opt.termNormalisation = True } in show' . normalise
  
  show' :: Lam a -> String
  show' (Abs f) = concat ["(\\x -> ", show (f (Var True undefined)), ")"]
  show' (App f x) = concat ["(", show' f, " ", show' x, ")"]
  show' (Var True _) = "x"
  show' (Var False _) = "complex"
  show' (If c t e) = concat ["if ", show' c, " then ", show t, " else ", show e]
  show' (Let x f) = concat ["let x = ", show x, " in ", show' (f (Var True undefined))]
  show' T = "True"
  show' F = "False"
  