{-# LANGUAGE ImplicitParams #-}
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
data Lam a where
Abs :: (Lam a -> Lam b) -> Lam (a -> b)
App :: Lam (a -> b) -> Lam a -> Lam b
Var :: Bool -> 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
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
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
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))
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||]))) ||]
generate (App Lam (a -> a)
f Lam a
x) = [|| $$(generate f) $$(normaliseGen x) ||]
generate (Var Bool
_ Code a
x) = Code a
x
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 ||]
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"