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

-- |
-- Module      : Jikka.Core.Convert.StrengthReduction
-- Description : does strength reduction. / 演算子強度低減を行います。
-- Copyright   : (c) Kimiyuki Onaka, 2020
-- License     : Apache License 2.0
-- Maintainer  : kimiyuki95@gmail.com
-- Stability   : experimental
-- Portability : portable
module Jikka.Core.Convert.StrengthReduction
  ( run,
  )
where

import Jikka.Common.Alpha
import Jikka.Common.Error
import Jikka.Core.Language.BuiltinPatterns
import Jikka.Core.Language.Expr
import Jikka.Core.Language.Lint
import Jikka.Core.Language.RewriteRules

-- | `eliminateSomeBuiltins` removes some `Builtin` from `Expr` at all.
eliminateSomeBuiltins :: Monad m => RewriteRule m
eliminateSomeBuiltins :: RewriteRule m
eliminateSomeBuiltins = (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
  -- advanced arithmetical functions
  Abs' Expr
e -> 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
Max2' Type
IntTy Expr
e (Expr -> Expr
Negate' Expr
e)
  Lcm' Expr
e1 Expr
e2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
FloorDiv' (Expr -> Expr -> Expr
Gcd' Expr
e1 Expr
e2) (Expr -> Expr -> Expr
Mult' Expr
e1 Expr
e2)
  -- logical functions
  Implies' Expr
e1 Expr
e2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Or' (Expr -> Expr
Not' Expr
e1) Expr
e2
  -- comparison
  GreaterThan' Type
t Expr
e1 Expr
e2 -> 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
LessThan' Type
t Expr
e2 Expr
e1
  GreaterEqual' Type
t Expr
e1 Expr
e2 -> 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
LessEqual' Type
t Expr
e2 Expr
e1
  NotEqual' Type
t Expr
e1 Expr
e2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Not' (Type -> Expr -> Expr -> Expr
Equal' Type
t Expr
e1 Expr
e2)
  Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

-- | `reduceNegate` brings `Negate` to the root.
reduceNegate :: Monad m => RewriteRule m
reduceNegate :: RewriteRule m
reduceNegate = (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
  Negate' (Negate' Expr
e) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
  Plus' (Negate' Expr
e1) (Negate' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Negate' (Expr -> Expr -> Expr
Plus' Expr
e1 Expr
e2)
  Minus' Expr
e1 (Negate' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Plus' Expr
e1 Expr
e2
  Minus' (Negate' Expr
e1) Expr
e2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Negate' (Expr -> Expr -> Expr
Minus' Expr
e1 Expr
e2)
  -- `Minus` is already removed.
  Mult' (Negate' Expr
e1) Expr
e2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Negate' (Expr -> Expr -> Expr
Mult' Expr
e1 Expr
e2)
  Mult' Expr
e1 (Negate' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Negate' (Expr -> Expr -> Expr
Mult' Expr
e1 Expr
e2)
  -- `Abs` is already removed.
  Min2' Type
IntTy (Negate' Expr
e1) (Negate' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Negate' (Type -> Expr -> Expr -> Expr
Max2' Type
IntTy Expr
e1 Expr
e2)
  Max2' Type
IntTy (Negate' Expr
e1) (Negate' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Negate' (Type -> Expr -> Expr -> Expr
Min2' Type
IntTy Expr
e1 Expr
e2)
  Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

-- | `reduceNot` brings `Not` to the root.
reduceNot :: Monad m => RewriteRule m
reduceNot :: RewriteRule m
reduceNot = (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
  Not' (Not' Expr
e) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
  And' (Not' Expr
e1) (Not' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Not' (Expr -> Expr -> Expr
Or' Expr
e1 Expr
e2)
  Or' (Not' Expr
e1) (Not' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Not' (Expr -> Expr -> Expr
And' Expr
e1 Expr
e2)
  -- `Implies` is already removed.
  Mult' (Negate' Expr
e1) Expr
e2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Negate' (Expr -> Expr -> Expr
Mult' Expr
e1 Expr
e2)
  Mult' Expr
e1 (Negate' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Negate' (Expr -> Expr -> Expr
Mult' Expr
e1 Expr
e2)
  If' Type
t (Not' Expr
e1) Expr
e2 Expr
e3 -> 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
If' Type
t Expr
e1 Expr
e3 Expr
e2
  Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

-- | `reduceBitNot` brings `BitNot` to the root.
reduceBitNot :: Monad m => RewriteRule m
reduceBitNot :: RewriteRule m
reduceBitNot = (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
  BitNot' (BitNot' Expr
e) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
  BitAnd' (BitNot' Expr
e1) (BitNot' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
BitNot' (Expr -> Expr -> Expr
BitOr' Expr
e1 Expr
e2)
  BitOr' (BitNot' Expr
e1) (BitNot' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
BitNot' (Expr -> Expr -> Expr
BitAnd' Expr
e1 Expr
e2)
  BitXor' (BitNot' Expr
e1) Expr
e2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
BitNot' (Expr -> Expr -> Expr
BitXor' Expr
e1 Expr
e2)
  BitXor' Expr
e1 (BitNot' Expr
e2) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
BitNot' (Expr -> Expr -> Expr
BitXor' Expr
e1 Expr
e2)
  Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

misc :: Monad m => RewriteRule m
misc :: RewriteRule m
misc = (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
  -- arithmetical functions
  Pow' (Pow' Expr
e1 Expr
e2) Expr
e3 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Pow' Expr
e1 (Expr -> Expr -> Expr
Plus' Expr
e2 Expr
e3)
  -- advanced arithmetical functions
  Gcd' (Mult' Expr
k1 Expr
e1) (Mult' Expr
k2 Expr
e2) | Expr
k1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
k2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Mult' Expr
k1 (Expr -> Expr -> Expr
Gcd' Expr
e1 Expr
e2)
  Gcd' (Mult' Expr
k1 Expr
e1) (Mult' Expr
e2 Expr
k2) | Expr
k1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
k2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Mult' Expr
k1 (Expr -> Expr -> Expr
Gcd' Expr
e1 Expr
e2)
  Gcd' (Mult' Expr
e1 Expr
k1) (Mult' Expr
e2 Expr
k2) | Expr
k1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
k2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Mult' Expr
k1 (Expr -> Expr -> Expr
Gcd' Expr
e1 Expr
e2)
  Gcd' (Mult' Expr
e1 Expr
k1) (Mult' Expr
k2 Expr
e2) | Expr
k1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
k2 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Mult' Expr
k1 (Expr -> Expr -> Expr
Gcd' Expr
e1 Expr
e2)
  Expr
_ -> 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 :: * -> *). Monad m => RewriteRule m
eliminateSomeBuiltins,
      RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
reduceNegate,
      RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
reduceNot,
      RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
reduceBitNot,
      RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
misc
    ]

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

-- | TODO: Split and remove this module.
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.StrengthReduction" (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