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

-- |
-- Module      : Jikka.Core.Convert.ShortCutFusion
-- Description : does short cut fusion. / short cut fusion を行います。
-- Copyright   : (c) Kimiyuki Onaka, 2021
-- License     : Apache License 2.0
-- Maintainer  : kimiyuki95@gmail.com
-- Stability   : experimental
-- Portability : portable
--
-- \[
--     \newcommand\int{\mathbf{int}}
--     \newcommand\bool{\mathbf{bool}}
--     \newcommand\list{\mathbf{list}}
-- \]
module Jikka.Core.Convert.ShortCutFusion
  ( run,

    -- * internal rules
    rule,
    reduceBuild,
    reduceMapBuild,
    reduceMap,
    reduceMapMap,
    reduceFoldMap,
    reduceFold,
    reduceFoldBuild,
  )
where

import Jikka.Common.Alpha
import Jikka.Common.Error
import Jikka.Core.Format (formatExpr)
import Jikka.Core.Language.BuiltinPatterns
import Jikka.Core.Language.Expr
import Jikka.Core.Language.FreeVars
import Jikka.Core.Language.Lint
import Jikka.Core.Language.RewriteRules
import Jikka.Core.Language.Util

-- |
-- * `Range1` remains.
-- * `Range2` is removed.
-- * `Range3` is removed.
-- * `Nil` and `Cons` are kept as is.
reduceBuild :: MonadAlpha m => RewriteRule m
reduceBuild :: RewriteRule m
reduceBuild =
  let return' :: a -> m (Maybe a)
return' = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> (a -> Maybe a) -> a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just
   in ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
RewriteRule (([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \[(VarName, Type)]
_ -> \case
        Range2' Expr
l Expr
r -> do
          let n :: Expr
n = Expr -> Expr -> Expr
Minus' Expr
r Expr
l
          VarName
x <- m VarName
forall (m :: * -> *). MonadAlpha m => m VarName
genVarName'
          let f :: Expr
f = VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy (Expr -> Expr -> Expr
Plus' Expr
l (VarName -> Expr
Var VarName
x))
          Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Expr -> Expr -> Expr
Map' Type
IntTy Type
IntTy Expr
f (Expr -> Expr
Range1' Expr
n)
        Range3' Expr
l Expr
r Expr
step -> do
          let n :: Expr
n = Expr -> Expr -> Expr
CeilDiv' (Expr -> Expr -> Expr
Minus' Expr
r Expr
l) Expr
step
          VarName
x <- m VarName
forall (m :: * -> *). MonadAlpha m => m VarName
genVarName'
          let f :: Expr
f = VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy (Expr -> Expr -> Expr
Plus' Expr
l (Expr -> Expr -> Expr
Mult' Expr
step (VarName -> Expr
Var VarName
x)))
          Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Expr -> Expr -> Expr
Map' Type
IntTy Type
IntTy Expr
f (Expr -> Expr
Range1' Expr
n)
        Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing

reduceMapBuild :: MonadAlpha m => RewriteRule m
reduceMapBuild :: RewriteRule m
reduceMapBuild =
  let return' :: a -> m (Maybe a)
return' = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> (a -> Maybe a) -> a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just
   in ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
RewriteRule (([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \[(VarName, Type)]
_ -> \case
        -- reduce `Sorted`
        Sorted' Type
_ (Nil' Type
t) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr
Nil' Type
t
        Sorted' Type
_ (Range1' Expr
n) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Range1' Expr
n
        -- reduce `Reversed`
        Reversed' Type
_ (Nil' Type
t) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr
Nil' Type
t
        Reversed' Type
_ (Range1' Expr
n) -> do
          VarName
x <- m VarName
forall (m :: * -> *). MonadAlpha m => m VarName
genVarName'
          let f :: Expr
f = VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy (Expr -> Expr -> Expr
Minus' (Expr -> Expr -> Expr
Minus' Expr
n (VarName -> Expr
Var VarName
x)) (Integer -> Expr
LitInt' Integer
1))
          Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Expr -> Expr -> Expr
Map' Type
IntTy Type
IntTy Expr
f Expr
n
        -- reduce `Filter`
        Filter' Type
_ Expr
_ (Nil' Type
t) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr
Nil' Type
t
        -- reduce `Map`
        Map' Type
_ Type
_ Expr
_ (Nil' Type
t) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr
Nil' Type
t
        Map' Type
t1 Type
t2 Expr
f (Cons' Type
_ Expr
x Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr -> Expr
Cons' Type
t2 (Expr -> Expr -> Expr
App Expr
f Expr
x) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 Expr
f Expr
xs)
        -- others
        Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing

reduceMap :: Monad m => RewriteRule m
reduceMap :: RewriteRule m
reduceMap =
  let return' :: a -> m (Maybe a)
return' = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> (a -> Maybe a) -> a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just
   in ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
RewriteRule (([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \[(VarName, Type)]
_ -> \case
        -- reduce `Map`
        Map' Type
_ Type
_ (LamId VarName
_ Type
_) Expr
xs -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
xs
        -- reduce `Filter`
        Filter' Type
t (Lam VarName
_ Type
_ Expr
LitFalse) Expr
_ -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Type -> Expr
Nil' Type
t)
        Filter' Type
_ (Lam VarName
_ Type
_ Expr
LitTrue) Expr
xs -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
xs
        -- others
        Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing

-- |
-- * Functions are reordered as:
--   * `Sort` and `Reversed` (functions to reorder) are lastly applied to lists
--   * `Map` (functions to modify lists)
--   * `Filter` (funcitons to reduce lengths) is firstly applied to lists
reduceMapMap :: MonadAlpha m => RewriteRule m
reduceMapMap :: RewriteRule m
reduceMapMap =
  let return' :: a -> m (Maybe a)
return' = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> (a -> Maybe a) -> a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just
   in ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
RewriteRule (([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \[(VarName, Type)]
_ -> \case
        -- reduce `Map`
        Map' Type
_ Type
_ (LamId VarName
_ Type
_) Expr
xs -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
xs
        Map' Type
_ Type
t3 Expr
g (Map' Type
t1 Type
_ Expr
f Expr
xs) -> do
          VarName
x <- m VarName
forall (m :: * -> *). MonadAlpha m => m VarName
genVarName'
          let h :: Expr
h = VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 (Expr -> Expr -> Expr
App Expr
g (Expr -> Expr -> Expr
App Expr
f (VarName -> Expr
Var VarName
x)))
          Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t3 Expr
h Expr
xs
        Map' Type
t1 Type
t2 Expr
f (Reversed' Type
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr
Reversed' Type
t2 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 Expr
f Expr
xs)
        -- reduce `Filter`
        Filter' Type
t2 Expr
g (Map' Type
t1 Type
_ Expr
f Expr
xs) -> do
          VarName
x <- m VarName
forall (m :: * -> *). MonadAlpha m => m VarName
genVarName'
          let h :: Expr
h = VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 (Expr -> Expr -> Expr
App Expr
g (Expr -> Expr -> Expr
App Expr
f (VarName -> Expr
Var VarName
x)))
          Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 Expr
f (Type -> Expr -> Expr -> Expr
Filter' Type
t1 Expr
h Expr
xs)
        Filter' Type
t Expr
g (Filter' Type
_ Expr
f Expr
xs) -> do
          VarName
x <- m VarName
forall (m :: * -> *). MonadAlpha m => m VarName
genVarName'
          let h :: Expr
h = VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t (Expr -> Expr -> Expr
And' (Expr -> Expr -> Expr
App Expr
g (VarName -> Expr
Var VarName
x)) (Expr -> Expr -> Expr
App Expr
f (VarName -> Expr
Var VarName
x)))
          Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr -> Expr
Filter' Type
t Expr
h Expr
xs
        Filter' Type
t Expr
f (Sorted' Type
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr
Sorted' Type
t (Type -> Expr -> Expr -> Expr
Filter' Type
t Expr
f Expr
xs)
        Filter' Type
t Expr
f (Reversed' Type
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr
Reversed' Type
t (Type -> Expr -> Expr -> Expr
Filter' Type
t Expr
f Expr
xs)
        -- reduce `Reversed`
        Reversed' Type
_ (Reversed' Type
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
xs
        Reversed' Type
_ (Map' Type
t1 Type
t2 Expr
f Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 Expr
f (Type -> Expr -> Expr
Reversed' Type
t1 Expr
xs)
        -- reduce `Sorted`
        Sorted' Type
t (Reversed' Type
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr
Sorted' Type
t Expr
xs
        Sorted' Type
t (Sorted' Type
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr
Sorted' Type
t Expr
xs
        -- others
        Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing

reduceFoldMap :: MonadAlpha m => RewriteRule m
reduceFoldMap :: RewriteRule m
reduceFoldMap =
  let return' :: a -> m (Maybe a)
return' = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> (a -> Maybe a) -> a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just
   in ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
RewriteRule (([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \[(VarName, Type)]
_ -> \case
        -- reduce `Reversed`
        Len' Type
t (Reversed' Type
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr
Len' Type
t Expr
xs
        Elem' Type
t Expr
x (Reversed' Type
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr -> Expr
Elem' Type
t Expr
x Expr
xs
        At' Type
t (Reversed' Type
_ Expr
xs) Expr
i -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr -> Expr
At' Type
t Expr
xs (Expr -> Expr -> Expr
Minus' (Expr -> Expr -> Expr
Minus' (Type -> Expr -> Expr
Len' Type
t Expr
xs) Expr
i) Expr
Lit1)
        -- reduce `Sorted`
        Len' Type
t (Sorted' Type
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr
Len' Type
t Expr
xs
        Elem' Type
t Expr
x (Sorted' Type
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr -> Expr
Elem' Type
t Expr
x Expr
xs
        -- reduce `Map`
        Len' Type
_ (Map' Type
t1 Type
_ Expr
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr
Len' Type
t1 Expr
xs
        At' Type
_ (Map' Type
t1 Type
_ Expr
f Expr
xs) Expr
i -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
App Expr
f (Type -> Expr -> Expr -> Expr
At' Type
t1 Expr
xs Expr
i)
        Foldl' Type
_ Type
t3 Expr
g Expr
init (Map' Type
t1 Type
_ Expr
f Expr
xs) -> do
          VarName
x3 <- m VarName
forall (m :: * -> *). MonadAlpha m => m VarName
genVarName'
          VarName
x1 <- m VarName
forall (m :: * -> *). MonadAlpha m => m VarName
genVarName'
          Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Expr -> Expr -> Expr -> Expr
Foldl' Type
t1 Type
t3 (VarName -> Type -> VarName -> Type -> Expr -> Expr
Lam2 VarName
x3 Type
t3 VarName
x1 Type
t1 (Expr -> Expr -> Expr -> Expr
App2 Expr
g (VarName -> Expr
Var VarName
x3) (Expr -> Expr -> Expr
App Expr
f (VarName -> Expr
Var VarName
x1)))) Expr
init Expr
xs
        -- others
        Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing

reduceFold :: Monad m => RewriteRule m
reduceFold :: RewriteRule m
reduceFold = (Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
(Expr -> Maybe Expr) -> RewriteRule m
simpleRewriteRule ((Expr -> Maybe Expr) -> RewriteRule m)
-> (Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \case
  Foldl' Type
t1 Type
t2 (Lam2 VarName
x2 Type
_ VarName
x1 Type
_ Expr
body) Expr
init Expr
xs | VarName
x1 VarName -> Expr -> Bool
`isUnusedVar` Expr
body -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr -> Expr -> Expr
Iterate' Type
t2 (Type -> Expr -> Expr
Len' Type
t1 Expr
xs) (VarName -> Type -> Expr -> Expr
Lam VarName
x2 Type
t2 Expr
body) Expr
init
  Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

reduceFoldBuild :: MonadAlpha m => RewriteRule m
reduceFoldBuild :: RewriteRule m
reduceFoldBuild =
  let return' :: a -> m (Maybe a)
return' = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> (a -> Maybe a) -> a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just
   in ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
RewriteRule (([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> ([(VarName, Type)] -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \[(VarName, Type)]
_ -> \case
        -- reduce `Foldl`
        Foldl' Type
_ Type
_ Expr
_ Expr
init (Nil' Type
_) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
init
        Foldl' Type
t1 Type
t2 Expr
g Expr
init (Cons' Type
_ Expr
x Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Expr -> Expr -> Expr -> Expr
Foldl' Type
t1 Type
t2 Expr
g (Expr -> Expr -> Expr -> Expr
App2 Expr
g Expr
init Expr
x) Expr
xs
        -- reduce `Len`
        Len' Type
_ (Nil' Type
_) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
Lit0
        Len' Type
t (Cons' Type
_ Expr
_ Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Plus' Expr
Lit1 (Type -> Expr -> Expr
Len' Type
t Expr
xs)
        Len' Type
_ (Range1' Expr
n) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
n
        -- reduce `At`
        At' Type
t (Nil' Type
_) Expr
i -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> String -> Expr
Bottom' Type
t (String -> Expr) -> String -> Expr
forall a b. (a -> b) -> a -> b
$ String
"cannot subscript empty list: index = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
formatExpr Expr
i
        At' Type
t (Cons' Type
_ Expr
x Expr
xs) Expr
i -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr -> Expr -> Expr
If' Type
t (Type -> Expr -> Expr -> Expr
Equal' Type
IntTy Expr
i Expr
Lit0) Expr
x (Type -> Expr -> Expr -> Expr
At' Type
t Expr
xs (Expr -> Expr -> Expr
Minus' Expr
i Expr
Lit1))
        At' Type
_ (Range1' Expr
_) Expr
i -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
i
        -- reduce `Elem`
        Elem' Type
_ Expr
_ (Nil' Type
_) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
LitFalse
        Elem' Type
t Expr
y (Cons' Type
_ Expr
x Expr
xs) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
And' (Type -> Expr -> Expr -> Expr
Equal' Type
t Expr
x Expr
y) (Type -> Expr -> Expr -> Expr
Elem' Type
t Expr
y Expr
xs)
        Elem' Type
_ Expr
x (Range1' Expr
n) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
And' (Type -> Expr -> Expr -> Expr
LessEqual' Type
IntTy Expr
Lit0 Expr
x) (Type -> Expr -> Expr -> Expr
LessThan' Type
IntTy Expr
x Expr
n)
        -- others
        Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing

rule :: MonadAlpha m => RewriteRule m
rule :: RewriteRule m
rule =
  [RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
    [ RewriteRule m
forall (m :: * -> *). MonadAlpha m => RewriteRule m
reduceFoldMap,
      RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
reduceMap,
      RewriteRule m
forall (m :: * -> *). MonadAlpha m => RewriteRule m
reduceMapMap,
      RewriteRule m
forall (m :: * -> *). MonadAlpha m => RewriteRule m
reduceFoldBuild,
      RewriteRule m
forall (m :: * -> *). MonadAlpha m => RewriteRule m
reduceMapBuild,
      RewriteRule m
forall (m :: * -> *). MonadAlpha m => RewriteRule m
reduceBuild,
      RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
reduceFold
    ]

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 => RewriteRule m
rule

-- | `run` does short cut fusion.
--
-- * This function is mainly for polymorphic reductions. This dosn't do much about concrete things, e.g., arithmetical operations.
-- * This doesn't do nothing about `Scanl` or `SetAt`.
--
-- == Example
--
-- Before:
--
-- > length (map f (cons (-1) (range n)))
--
-- After:
--
-- > n + 1
--
-- == List of builtin functions which are reduced
--
-- === Build functions
--
-- * `Nil` \(: \forall \alpha. \list(\alpha)\)
-- * `Cons` \(: \forall \alpha. \alpha \to \list(\alpha) \to \list(\alpha)\)
-- * `Range1` \(: \int \to \list(\int)\)
-- * `Range2` \(: \int \to \int \to \list(\int)\)
-- * `Range3` \(: \int \to \int \to \int \to \list(\int)\)
--
-- === Map functions
--
-- * `Map` \(: \forall \alpha \beta. (\alpha \to \beta) \to \list(\alpha) \to \list(\beta)\)
-- * `Filter` \(: \forall \alpha \beta. (\alpha \to \bool) \to \list(\alpha) \to \list(\beta)\)
-- * `Reversed` \(: \forall \alpha. \list(\alpha) \to \list(\alpha)\)
-- * `Sorted` \(: \forall \alpha. \list(\alpha) \to \list(\alpha)\)
--
-- === Fold functions
--
-- * `Foldl` \(: \forall \alpha \beta. (\beta \to \alpha \to \beta) \to \beta \to \list(\alpha) \to \beta\)
-- * `Len` \(: \forall \alpha. \list(\alpha) \to \int\)
-- * `At` \(: \forall \alpha. \list(\alpha) \to \int \to \alpha\)
-- * `Elem` \(: \forall \alpha. \alpha \to \list(\alpha) \to \bool\)
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.ShortCutFusion" (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 ()
ensureWellTyped 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 ()
ensureWellTyped Program
prog
  Program -> m Program
forall (m :: * -> *) a. Monad m => a -> m a
return Program
prog