{-# 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 :: Lam Bool -> Lam Bool -> Lam Bool
andLam Lam Bool
x Lam Bool
y = forall a. Lam Bool -> Lam a -> Lam a -> Lam a
If Lam Bool
x Lam Bool
y Lam Bool
F

orLam :: Lam Bool -> Lam Bool -> Lam Bool
orLam :: Lam Bool -> Lam Bool -> Lam Bool
orLam Lam Bool
x = forall a. Lam Bool -> Lam a -> Lam a -> Lam a
If Lam Bool
x Lam Bool
T

notLam :: Lam Bool -> Lam Bool
notLam :: Lam Bool -> Lam Bool
notLam Lam Bool
x = forall a. Lam Bool -> Lam a -> Lam a -> Lam a
If Lam Bool
x Lam Bool
F Lam Bool
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 :: forall a. (?flags::Flags) => Lam a -> Lam a
normalise Lam a
x = if forall a. Lam a -> Bool
normal Lam a
x Bool -> Bool -> Bool
|| Bool -> Bool
not (Flags -> Bool
Opt.termNormalisation ?flags::Flags
?flags) then Lam a
x else forall a. Lam a -> Lam a
reduce Lam a
x
  where
    reduce :: Lam a -> Lam a
    reduce :: forall a. Lam a -> Lam a
reduce (App (Abs Lam a -> Lam b
f) Lam a
x) = forall a. (?flags::Flags) => Lam a -> Lam a
normalise (Lam a -> Lam b
f Lam a
x)
    reduce (App Lam (a -> a)
f Lam a
x) = case forall a. Lam a -> Lam a
reduce Lam (a -> a)
f of
      f :: Lam (a -> a)
f@Abs{} -> forall a. Lam a -> Lam a
reduce (forall a b. Lam (a -> b) -> Lam a -> Lam b
App Lam (a -> a)
f Lam a
x)
      Lam (a -> a)
f       -> forall a b. Lam (a -> b) -> Lam a -> Lam b
App Lam (a -> a)
f Lam a
x
    reduce (If Lam Bool
T Lam a
t Lam a
_) = forall a. (?flags::Flags) => Lam a -> Lam a
normalise Lam a
t
    reduce (If Lam Bool
F Lam a
_ Lam a
f) = forall a. (?flags::Flags) => Lam a -> Lam a
normalise Lam a
f
    reduce (If Lam Bool
_ Lam a
T Lam a
T) = Lam Bool
T
    reduce (If Lam Bool
_ Lam a
F Lam a
F) = Lam Bool
F
    reduce (If Lam Bool
c Lam a
T Lam a
F) = forall a. (?flags::Flags) => Lam a -> Lam a
normalise Lam Bool
c
    -- one of them must be not in normal form
    reduce (If Lam Bool
c Lam a
t Lam a
f) = forall a. (?flags::Flags) => Lam a -> Lam a
normalise (forall a. Lam Bool -> Lam a -> Lam a -> Lam a
If (forall a. (?flags::Flags) => Lam a -> Lam a
normalise Lam Bool
c) (forall a. (?flags::Flags) => Lam a -> Lam a
normalise Lam a
t) (forall a. (?flags::Flags) => Lam a -> Lam a
normalise Lam a
f))
    -- Reduction rule found courtesy of David Davies, forever immortalised
    reduce (Let v :: Lam a
v@(Var Bool
True Code a
_) Lam a -> Lam a
f) = forall a. (?flags::Flags) => Lam a -> Lam a
normalise (Lam a -> Lam a
f Lam a
v)
    reduce Lam a
x = Lam a
x

    normal :: Lam a -> Bool
    normal :: forall a. Lam a -> Bool
normal (App (Abs Lam a -> Lam b
_) Lam a
_) = Bool
False
    normal (App Lam (a -> a)
f Lam a
_) = forall a. Lam a -> Bool
normal Lam (a -> a)
f
    normal (If Lam Bool
T Lam a
_ Lam a
_) = Bool
False
    normal (If Lam Bool
F Lam a
_ Lam a
_) = Bool
False
    normal (If Lam Bool
_ Lam a
T Lam a
T) = Bool
False
    normal (If Lam Bool
_ Lam a
F Lam a
F) = Bool
False
    normal (If Lam Bool
_ Lam a
T Lam a
F) = Bool
False
    normal (If Lam Bool
c Lam a
t Lam a
f) = forall a. Lam a -> Bool
normal Lam Bool
c Bool -> Bool -> Bool
&& forall a. Lam a -> Bool
normal Lam a
t Bool -> Bool -> Bool
&& forall a. Lam a -> Bool
normal Lam a
f
    normal (Let (Var Bool
True Code a
_) Lam a -> Lam a
_) = Bool
False
    normal Lam a
_ = Bool
True

generate :: (?flags :: Opt.Flags) => Lam a -> Code a
generate :: forall a. (?flags::Flags) => Lam a -> Code a
generate (Abs Lam a -> Lam b
f)    = [|| \x -> $$(normaliseGen (f (Var True [||x||]))) ||]
-- f has already been reduced, since we only expose `normaliseGen`
generate (App Lam (a -> a)
f Lam a
x)  = [|| $$(generate f) $$(normaliseGen x) ||]
generate (Var Bool
_ Code a
x)  = Code a
x
-- all parts are reduced
generate (If Lam Bool
c Lam a
T Lam a
e) = [|| $$(generate c) || $$(generate e) ||]
generate (If Lam Bool
c Lam a
t Lam a
F) = [|| $$(generate c) && $$(generate t) ||]
generate (If Lam Bool
c Lam a
F Lam a
T) = [|| not $$(generate c) ||]
generate (If Lam Bool
c Lam a
t Lam a
e) = [|| if $$(generate c) then $$(generate t) else $$(generate e) ||]
generate (Let Lam a
b Lam a -> Lam a
i)  = [|| let x = $$(normaliseGen b) in $$(normaliseGen (i (Var True [||x||]))) ||]
generate Lam a
T          = [|| True ||]
generate Lam a
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 :: forall a. (?flags::Flags) => Lam a -> Code a
normaliseGen = forall a. Code a -> Code a
eta forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (?flags::Flags) => Lam a -> Code a
generate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (?flags::Flags) => Lam a -> Lam a
normalise

instance Show (Lam a) where
  show :: Lam a -> String
show = let ?flags = Flags
Opt.none { termNormalisation :: Bool
Opt.termNormalisation = Bool
True } in forall a. Lam a -> String
show' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (?flags::Flags) => Lam a -> Lam a
normalise

show' :: Lam a -> String
show' :: forall a. Lam a -> String
show' (Abs Lam a -> Lam b
f) = forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [String
"(\\x -> ", forall a. Show a => a -> String
show (Lam a -> Lam b
f (forall a. Bool -> Code a -> Lam a
Var Bool
True forall a. HasCallStack => a
undefined)), String
")"]
show' (App Lam (a -> a)
f Lam a
x) = forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [String
"(", forall a. Lam a -> String
show' Lam (a -> a)
f, String
" ", forall a. Lam a -> String
show' Lam a
x, String
")"]
show' (Var Bool
True Code a
_) = String
"x"
show' (Var Bool
False Code a
_) = String
"complex"
show' (If Lam Bool
c Lam a
t Lam a
e) = forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [String
"if ", forall a. Lam a -> String
show' Lam Bool
c, String
" then ", forall a. Show a => a -> String
show Lam a
t, String
" else ", forall a. Show a => a -> String
show Lam a
e]
show' (Let Lam a
x Lam a -> Lam a
f) = forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [String
"let x = ", forall a. Show a => a -> String
show Lam a
x, String
" in ", forall a. Lam a -> String
show' (Lam a -> Lam a
f (forall a. Bool -> Code a -> Lam a
Var Bool
True forall a. HasCallStack => a
undefined))]
show' Lam a
T = String
"True"
show' Lam a
F = String
"False"