{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
module Jikka.Core.Convert.Eta
( run,
rule,
)
where
import Jikka.Common.Alpha
import Jikka.Common.Error
import Jikka.Core.Language.BuiltinPatterns
import Jikka.Core.Language.Eta
import Jikka.Core.Language.Expr
import Jikka.Core.Language.Lint
import Jikka.Core.Language.RewriteRules
rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m
rule :: RewriteRule m
rule =
let go :: (MonadAlpha m, MonadError Error m) => RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
go :: RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
go RewriteEnvironment
env Expr
e Expr -> Expr
f = (Expr -> Expr
f (Expr -> Expr) -> Maybe Expr -> Maybe Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe Expr -> Maybe Expr) -> m (Maybe Expr) -> m (Maybe Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(VarName, Type)] -> Expr -> m (Maybe Expr)
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
[(VarName, Type)] -> Expr -> m (Maybe Expr)
etaExpand' (RewriteEnvironment -> [(VarName, Type)]
typeEnv RewriteEnvironment
env) Expr
e
in String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"eta-expansion" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
env -> \case
Let VarName
x Type
t Expr
e1 Expr
e2 -> RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
go RewriteEnvironment
env Expr
e1 (\Expr
e1 -> VarName -> Type -> Expr -> Expr -> Expr
Let VarName
x Type
t Expr
e1 Expr
e2)
Iterate' Type
t Expr
k Expr
f Expr
x -> RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
go RewriteEnvironment
env Expr
f (\Expr
f -> Type -> Expr -> Expr -> Expr -> Expr
Iterate' Type
t Expr
k Expr
f Expr
x)
Foldl' Type
t1 Type
t2 Expr
f Expr
init Expr
xs -> RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
go RewriteEnvironment
env Expr
f (\Expr
f -> Type -> Type -> Expr -> Expr -> Expr -> Expr
Foldl' Type
t1 Type
t2 Expr
f Expr
init Expr
xs)
Scanl' Type
t1 Type
t2 Expr
f Expr
init Expr
xs -> RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
go RewriteEnvironment
env Expr
f (\Expr
f -> Type -> Type -> Expr -> Expr -> Expr -> Expr
Scanl' Type
t1 Type
t2 Expr
f Expr
init Expr
xs)
Build' Type
t Expr
f Expr
xs Expr
n -> RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
go RewriteEnvironment
env Expr
f (\Expr
f -> Type -> Expr -> Expr -> Expr -> Expr
Build' Type
t Expr
f Expr
xs Expr
n)
Map' Type
t1 Type
t2 Expr
f Expr
xs -> RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
go RewriteEnvironment
env Expr
f (\Expr
f -> Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 Expr
f Expr
xs)
Filter' Type
t Expr
f Expr
xs -> RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteEnvironment -> Expr -> (Expr -> Expr) -> m (Maybe Expr)
go RewriteEnvironment
env Expr
f (\Expr
f -> Type -> Expr -> Expr -> Expr
Filter' Type
t Expr
f Expr
xs)
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing
runProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Program
runProgram :: Program -> m Program
runProgram = RewriteRule m -> Program -> m Program
forall (m :: * -> *).
MonadError Error m =>
RewriteRule m -> Program -> m Program
applyRewriteRuleProgram' RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
rule
run :: (MonadAlpha m, MonadError Error m) => Program -> m Program
run :: Program -> m Program
run Program
prog = String -> m Program -> m Program
forall (m :: * -> *) a. MonadError Error m => String -> m a -> m a
wrapError' String
"Jikka.Core.Convert.Eta" (m Program -> m Program) -> m Program -> m Program
forall a b. (a -> b) -> a -> b
$ do
m () -> m ()
forall (m :: * -> *) a. MonadError Error m => m a -> m a
precondition (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
Program -> m ()
forall (m :: * -> *). MonadError Error m => Program -> m ()
lint Program
prog
Program
prog <- Program -> m Program
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
Program -> m Program
runProgram Program
prog
m () -> m ()
forall (m :: * -> *) a. MonadError Error m => m a -> m a
postcondition (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
Program -> m ()
forall (m :: * -> *). MonadError Error m => Program -> m ()
lint Program
prog
Program -> m Program
forall (m :: * -> *) a. Monad m => a -> m a
return Program
prog