{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}

-- |
-- Module      : Jikka.Core.Convert.Eta
-- Description : does eta-reductions and makes exprs pointful. / eta 簡約を行って式を pointful にします。
-- Copyright   : (c) Kimiyuki Onaka, 2021
-- License     : Apache License 2.0
-- Maintainer  : kimiyuki95@gmail.com
-- Stability   : experimental
-- Portability : portable
module Jikka.Core.Convert.Eta
  ( run,

    -- * internal rules
    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` does eta-reductions in some locations.
-- This aims to:

-- * simplify other rewrite-rules

-- * convert to C++

-- TODO: expand in toplevel-let too.
--
-- == Examples
--
-- Before:
--
-- > foldl (+) 0 xs
--
-- After:
--
-- > foldl (fun y x -> y + x) 0 xs
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