module Parsley.Internal.Core.Lam (normaliseGen, normalise, Lam(..)) where

import Parsley.Internal.Common.Utils (Code)

data Lam a where
    Abs :: (Lam a -> Lam b) -> Lam (a -> b)
    App :: Lam (a -> b) -> Lam a -> Lam b
    Var :: Bool {- Simple -} -> Code a -> Lam a
    If  :: Lam Bool -> Lam a -> Lam a -> Lam a
    Let :: Lam a -> (Lam a -> Lam b) -> Lam b
    T   :: Lam Bool
    F   :: Lam Bool

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

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"