{-# LANGUAGE CPP
, DataKinds
, EmptyCase
, ExistentialQuantification
, FlexibleContexts
, GADTs
, GeneralizedNewtypeDeriving
, KindSignatures
, MultiParamTypeClasses
, OverloadedStrings
, PolyKinds
, ScopedTypeVariables
, TypeFamilies
, TypeOperators
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.CSE (cse) where
import Control.Monad.Reader
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.AST.Eq
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Syntax.TypeOf
import Language.Hakaru.Types.DataKind
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
data EAssoc (abt :: [Hakaru] -> Hakaru -> *)
= forall a . EAssoc !(abt '[] a) !(abt '[] a)
newtype Env (abt :: [Hakaru] -> Hakaru -> *) = Env [EAssoc abt]
emptyEnv :: Env a
emptyEnv :: Env a
emptyEnv = [EAssoc a] -> Env a
forall (abt :: [Hakaru] -> Hakaru -> *). [EAssoc abt] -> Env abt
Env []
trivial :: (ABT Term abt) => abt '[] a -> Bool
trivial :: abt '[] a -> Bool
trivial abt '[] a
abt = case abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] a
abt of
Var Variable a
_ -> Bool
True
Syn (Literal_ _) -> Bool
True
View (Term abt) '[] a
_ -> Bool
False
lookupEnv
:: forall abt a . (ABT Term abt)
=> abt '[] a
-> Env abt
-> abt '[] a
lookupEnv :: abt '[] a -> Env abt -> abt '[] a
lookupEnv abt '[] a
start (Env [EAssoc abt]
env) = abt '[] a -> [EAssoc abt] -> abt '[] a
go abt '[] a
start [EAssoc abt]
env
where
go :: abt '[] a -> [EAssoc abt] -> abt '[] a
go :: abt '[] a -> [EAssoc abt] -> abt '[] a
go abt '[] a
ast [] = abt '[] a
ast
go abt '[] a
ast (EAssoc abt '[] a
a abt '[] a
b : [EAssoc abt]
xs) =
case Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
ast) (abt '[] a -> Sing a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] a
a) of
Just TypeEq a a
Refl | abt '[] a -> abt '[] a -> Bool
forall (abt :: [Hakaru] -> Hakaru -> *) (d :: Hakaru).
ABT Term abt =>
abt '[] d -> abt '[] d -> Bool
alphaEq abt '[] a
ast abt '[] a
abt '[] a
a -> abt '[] a -> [EAssoc abt] -> abt '[] a
go abt '[] a
abt '[] a
b [EAssoc abt]
env
Maybe (TypeEq a a)
_ -> abt '[] a -> [EAssoc abt] -> abt '[] a
go abt '[] a
ast [EAssoc abt]
xs
insertEnv
:: forall abt a . (ABT Term abt)
=> abt '[] a
-> abt '[] a
-> Env abt
-> Env abt
insertEnv :: abt '[] a -> abt '[] a -> Env abt -> Env abt
insertEnv abt '[] a
ast1 abt '[] a
ast2 (Env [EAssoc abt]
env)
| abt '[] a -> Bool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Bool
trivial abt '[] a
ast1 = [EAssoc abt] -> Env abt
forall (abt :: [Hakaru] -> Hakaru -> *). [EAssoc abt] -> Env abt
Env (abt '[] a -> abt '[] a -> EAssoc abt
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> abt '[] a -> EAssoc abt
EAssoc abt '[] a
ast2 abt '[] a
ast1 EAssoc abt -> [EAssoc abt] -> [EAssoc abt]
forall a. a -> [a] -> [a]
: [EAssoc abt]
env)
| Bool
otherwise = [EAssoc abt] -> Env abt
forall (abt :: [Hakaru] -> Hakaru -> *). [EAssoc abt] -> Env abt
Env (abt '[] a -> abt '[] a -> EAssoc abt
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> abt '[] a -> EAssoc abt
EAssoc abt '[] a
ast1 abt '[] a
ast2 EAssoc abt -> [EAssoc abt] -> [EAssoc abt]
forall a. a -> [a] -> [a]
: [EAssoc abt]
env)
newtype CSE (abt :: [Hakaru] -> Hakaru -> *) a = CSE { CSE abt a -> Reader (Env abt) a
runCSE :: Reader (Env abt) a }
deriving (a -> CSE abt b -> CSE abt a
(a -> b) -> CSE abt a -> CSE abt b
(forall a b. (a -> b) -> CSE abt a -> CSE abt b)
-> (forall a b. a -> CSE abt b -> CSE abt a) -> Functor (CSE abt)
forall a b. a -> CSE abt b -> CSE abt a
forall a b. (a -> b) -> CSE abt a -> CSE abt b
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
a -> CSE abt b -> CSE abt a
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
(a -> b) -> CSE abt a -> CSE abt b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> CSE abt b -> CSE abt a
$c<$ :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
a -> CSE abt b -> CSE abt a
fmap :: (a -> b) -> CSE abt a -> CSE abt b
$cfmap :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
(a -> b) -> CSE abt a -> CSE abt b
Functor, Functor (CSE abt)
a -> CSE abt a
Functor (CSE abt)
-> (forall a. a -> CSE abt a)
-> (forall a b. CSE abt (a -> b) -> CSE abt a -> CSE abt b)
-> (forall a b c.
(a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c)
-> (forall a b. CSE abt a -> CSE abt b -> CSE abt b)
-> (forall a b. CSE abt a -> CSE abt b -> CSE abt a)
-> Applicative (CSE abt)
CSE abt a -> CSE abt b -> CSE abt b
CSE abt a -> CSE abt b -> CSE abt a
CSE abt (a -> b) -> CSE abt a -> CSE abt b
(a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c
forall a. a -> CSE abt a
forall a b. CSE abt a -> CSE abt b -> CSE abt a
forall a b. CSE abt a -> CSE abt b -> CSE abt b
forall a b. CSE abt (a -> b) -> CSE abt a -> CSE abt b
forall a b c. (a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c
forall (abt :: [Hakaru] -> Hakaru -> *). Functor (CSE abt)
forall (abt :: [Hakaru] -> Hakaru -> *) a. a -> CSE abt a
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt a
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt b
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt (a -> b) -> CSE abt a -> CSE abt b
forall (abt :: [Hakaru] -> Hakaru -> *) a b c.
(a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: CSE abt a -> CSE abt b -> CSE abt a
$c<* :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt a
*> :: CSE abt a -> CSE abt b -> CSE abt b
$c*> :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt b
liftA2 :: (a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c
$cliftA2 :: forall (abt :: [Hakaru] -> Hakaru -> *) a b c.
(a -> b -> c) -> CSE abt a -> CSE abt b -> CSE abt c
<*> :: CSE abt (a -> b) -> CSE abt a -> CSE abt b
$c<*> :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt (a -> b) -> CSE abt a -> CSE abt b
pure :: a -> CSE abt a
$cpure :: forall (abt :: [Hakaru] -> Hakaru -> *) a. a -> CSE abt a
$cp1Applicative :: forall (abt :: [Hakaru] -> Hakaru -> *). Functor (CSE abt)
Applicative, Applicative (CSE abt)
a -> CSE abt a
Applicative (CSE abt)
-> (forall a b. CSE abt a -> (a -> CSE abt b) -> CSE abt b)
-> (forall a b. CSE abt a -> CSE abt b -> CSE abt b)
-> (forall a. a -> CSE abt a)
-> Monad (CSE abt)
CSE abt a -> (a -> CSE abt b) -> CSE abt b
CSE abt a -> CSE abt b -> CSE abt b
forall a. a -> CSE abt a
forall a b. CSE abt a -> CSE abt b -> CSE abt b
forall a b. CSE abt a -> (a -> CSE abt b) -> CSE abt b
forall (abt :: [Hakaru] -> Hakaru -> *). Applicative (CSE abt)
forall (abt :: [Hakaru] -> Hakaru -> *) a. a -> CSE abt a
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt b
forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> (a -> CSE abt b) -> CSE abt b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> CSE abt a
$creturn :: forall (abt :: [Hakaru] -> Hakaru -> *) a. a -> CSE abt a
>> :: CSE abt a -> CSE abt b -> CSE abt b
$c>> :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> CSE abt b -> CSE abt b
>>= :: CSE abt a -> (a -> CSE abt b) -> CSE abt b
$c>>= :: forall (abt :: [Hakaru] -> Hakaru -> *) a b.
CSE abt a -> (a -> CSE abt b) -> CSE abt b
$cp1Monad :: forall (abt :: [Hakaru] -> Hakaru -> *). Applicative (CSE abt)
Monad, MonadReader (Env abt))
replaceCSE
:: (ABT Term abt)
=> abt '[] a
-> CSE abt (abt '[] a)
replaceCSE :: abt '[] a -> CSE abt (abt '[] a)
replaceCSE abt '[] a
abt = abt '[] a -> Env abt -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Env abt -> abt '[] a
lookupEnv abt '[] a
abt (Env abt -> abt '[] a) -> CSE abt (Env abt) -> CSE abt (abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` CSE abt (Env abt)
forall r (m :: * -> *). MonadReader r m => m r
ask
cse :: forall abt a . (ABT Term abt) => abt '[] a -> abt '[] a
cse :: abt '[] a -> abt '[] a
cse abt '[] a
abt = Reader (Env abt) (abt '[] a) -> Env abt -> abt '[] a
forall r a. Reader r a -> r -> a
runReader (CSE abt (abt '[] a) -> Reader (Env abt) (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) a.
CSE abt a -> Reader (Env abt) a
runCSE (abt '[] a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
ABT Term abt =>
abt xs a -> CSE abt (abt xs a)
cse' abt '[] a
abt)) Env abt
forall (a :: [Hakaru] -> Hakaru -> *). Env a
emptyEnv
cse' :: forall abt xs a . (ABT Term abt) => abt xs a -> CSE abt (abt xs a)
cse' :: abt xs a -> CSE abt (abt xs a)
cse' = View (Term abt) xs a -> CSE abt (abt xs a)
forall (ys :: [Hakaru]). View (Term abt) ys a -> CSE abt (abt ys a)
loop (View (Term abt) xs a -> CSE abt (abt xs a))
-> (abt xs a -> View (Term abt) xs a)
-> abt xs a
-> CSE abt (abt xs a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt xs a -> View (Term abt) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
where
loop :: View (Term abt) ys a -> CSE abt (abt ys a)
loop :: View (Term abt) ys a -> CSE abt (abt ys a)
loop (Var Variable a
v) = Variable a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Variable a -> CSE abt (abt '[] a)
cseVar Variable a
v
loop (Syn Term abt a
s) = Term abt a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Term abt a -> CSE abt (abt '[] a)
cseTerm Term abt a
s
loop (Bind Variable a
v View (Term abt) xs a
b) = (abt xs a -> abt (a : xs) a)
-> CSE abt (abt xs a) -> CSE abt (abt (a : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Variable a -> abt xs a -> abt (a : xs) a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
v) (View (Term abt) xs a -> CSE abt (abt xs a)
forall (ys :: [Hakaru]). View (Term abt) ys a -> CSE abt (abt ys a)
loop View (Term abt) xs a
b)
cseVar
:: (ABT Term abt)
=> Variable a
-> CSE abt (abt '[] a)
cseVar :: Variable a -> CSE abt (abt '[] a)
cseVar = abt '[] a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> CSE abt (abt '[] a)
replaceCSE (abt '[] a -> CSE abt (abt '[] a))
-> (Variable a -> abt '[] a) -> Variable a -> CSE abt (abt '[] a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var
mklet :: ABT Term abt => Variable b -> abt '[] b -> abt '[] a -> abt '[] a
mklet :: Variable b -> abt '[] b -> abt '[] a -> abt '[] a
mklet Variable b
v abt '[] b
rhs abt '[] a
body = Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon '[LC b, '( '[b], a)] a
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC b, '( '[b], a)] a
-> SArgs abt '[LC b, '( '[b], a)] -> Term abt a
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
(abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] b
rhs abt '[] b
-> SArgs abt '[ '( '[b], a)] -> SArgs abt '[LC b, '( '[b], a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* Variable b -> abt '[] a -> abt '[b] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable b
v abt '[] a
body abt '[b] a -> SArgs abt '[] -> SArgs abt '[ '( '[b], a)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End)
cseTerm
:: (ABT Term abt)
=> Term abt a
-> CSE abt (abt '[] a)
cseTerm :: Term abt a -> CSE abt (abt '[] a)
cseTerm (SCon args a
Let_ :$ abt vars a
rhs :* abt vars a
body :* SArgs abt args
End) = do
abt vars a
rhs' <- abt vars a -> CSE abt (abt vars a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
ABT Term abt =>
abt xs a -> CSE abt (abt xs a)
cse' abt vars a
rhs
abt '[a] a
-> (Variable a -> abt '[] a -> CSE abt (abt '[] a))
-> CSE abt (abt '[] a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
body ((Variable a -> abt '[] a -> CSE abt (abt '[] a))
-> CSE abt (abt '[] a))
-> (Variable a -> abt '[] a -> CSE abt (abt '[] a))
-> CSE abt (abt '[] a)
forall a b. (a -> b) -> a -> b
$ \Variable a
v abt '[] a
body' ->
(Env abt -> Env abt) -> CSE abt (abt '[] a) -> CSE abt (abt '[] a)
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (abt '[] a -> abt '[] a -> Env abt -> Env abt
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a -> Env abt -> Env abt
insertEnv abt vars a
abt '[] a
rhs' (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
v)) (CSE abt (abt '[] a) -> CSE abt (abt '[] a))
-> CSE abt (abt '[] a) -> CSE abt (abt '[] a)
forall a b. (a -> b) -> a -> b
$
if abt '[] a -> Bool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Bool
trivial abt vars a
abt '[] a
rhs'
then abt '[] a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
ABT Term abt =>
abt xs a -> CSE abt (abt xs a)
cse' abt '[] a
body'
else (abt '[] a -> abt '[] a)
-> CSE abt (abt '[] a) -> CSE abt (abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Variable a -> abt '[] a -> abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru)
(a :: Hakaru).
ABT Term abt =>
Variable b -> abt '[] b -> abt '[] a -> abt '[] a
mklet Variable a
v abt vars a
abt '[] a
rhs') (abt '[] a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
ABT Term abt =>
abt xs a -> CSE abt (abt xs a)
cse' abt '[] a
body')
cseTerm Term abt a
term = (forall (h :: [Hakaru]) (i :: Hakaru).
abt h i -> CSE abt (abt h i))
-> Term abt a -> CSE abt (Term abt a)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru). abt h i -> CSE abt (abt h i)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
(a :: Hakaru).
ABT Term abt =>
abt xs a -> CSE abt (abt xs a)
cse' Term abt a
term CSE abt (Term abt a)
-> (Term abt a -> CSE abt (abt '[] a)) -> CSE abt (abt '[] a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= abt '[] a -> CSE abt (abt '[] a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> CSE abt (abt '[] a)
replaceCSE (abt '[] a -> CSE abt (abt '[] a))
-> (Term abt a -> abt '[] a) -> Term abt a -> CSE abt (abt '[] a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn