{-|
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(..)) where

import Parsley.Internal.Common.Utils (Code)

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

{-|
Optimises a `Lam` expression, reducing it until the outmost lambda, let, or if statement.

@since 1.0.1.0
-}
normalise :: Lam a -> Lam a
normalise :: Lam a -> Lam a
normalise Lam a
x = if Lam a -> Bool
forall a. Lam a -> Bool
normal Lam a
x then Lam a
x else Lam a -> Lam a
forall a. Lam a -> Lam a
reduce Lam a
x
  where
    reduce :: Lam a -> Lam a
    reduce :: Lam a -> Lam a
reduce (App (Abs Lam a -> Lam b
f) Lam a
x) = case Lam a -> Lam b
f Lam a
Lam a
x of
      Lam b
x | Lam b -> Bool
forall a. Lam a -> Bool
normal Lam b
x -> Lam a
Lam b
x
      Lam b
x            -> Lam b -> Lam b
forall a. Lam a -> Lam a
reduce Lam b
x
    reduce (App Lam (a -> a)
f Lam a
x) = case Lam (a -> a) -> Lam (a -> a)
forall a. Lam a -> Lam a
reduce Lam (a -> a)
f of
      f :: Lam (a -> a)
f@(Abs Lam a -> Lam b
_) -> Lam a -> Lam a
forall a. Lam a -> Lam a
reduce (Lam (a -> a) -> Lam a -> Lam a
forall a b. Lam (a -> b) -> Lam a -> Lam b
App Lam (a -> a)
f Lam a
x)
      Lam (a -> a)
f         -> Lam (a -> a) -> Lam a -> Lam a
forall a b. Lam (a -> b) -> Lam a -> Lam b
App Lam (a -> a)
f Lam a
x
    reduce (If Lam Bool
c Lam a
x Lam a
y) = case Lam Bool -> Lam Bool
forall a. Lam a -> Lam a
reduce Lam Bool
c of
      Lam Bool
T -> Lam a
x
      Lam Bool
F -> Lam a
y
      Lam Bool
c -> Lam Bool -> Lam a -> Lam a -> Lam a
forall a. Lam Bool -> Lam a -> Lam a -> Lam a
If Lam Bool
c Lam a
x Lam a
y
    reduce Lam a
x = Lam a
x

    normal :: Lam a -> Bool
    normal :: Lam a -> Bool
normal (App (Abs Lam a -> Lam b
_) Lam a
_) = Bool
False
    normal (App Lam (a -> a)
f Lam a
_) = Lam (a -> a) -> Bool
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
x Lam a
_ Lam a
_) = Lam Bool -> Bool
forall a. Lam a -> Bool
normal Lam Bool
x
    normal Lam a
_ = Bool
True

generate :: Lam a -> Code a
generate :: 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
-- c has already been reduced, since we only expose `normaliseGen`
generate (If Lam Bool
c Lam a
t Lam a
e) = [||if $$(generate c) then $$(normaliseGen t) else $$(normaliseGen 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 :: Lam a -> Code a
normaliseGen :: Lam a -> Code a
normaliseGen = Lam a -> Code a
forall a. Lam a -> Code a
generate (Lam a -> Code a) -> (Lam a -> Lam a) -> Lam a -> Code a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lam a -> Lam a
forall a. Lam a -> Lam a
normalise

instance Show (Lam a) where
  show :: Lam a -> String
show = Lam a -> String
forall a. Lam a -> String
show' (Lam a -> String) -> (Lam a -> Lam a) -> Lam a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lam a -> Lam a
forall a. Lam a -> Lam a
normalise

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