{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      : Jikka.Core.Convert.ConstantFolding
-- Description : folds constants. / 定数畳み込みをします。
-- 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.ConstantFolding
  ( run,

    -- * internal rules
    rule,
    reduceConstArithmeticExpr,
    reduceConstMaxExpr,
    reduceIdempotentBooleanExpr,
    reduceUnitBooleanExpr,
    reduceConstBooleanExpr,
    reduceUnitBitExpr,
    reduceConstBitExpr,
    reduceConstIntComparison,
    reduceUnitBooleanComparison,
  )
where

import Data.Bits
import Data.Either
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.QuasiRules
import Jikka.Core.Language.RewriteRules
import Jikka.Core.Language.Runtime

-- |
-- == List of functions which are reduced
--
-- === Basic arithmetical functions
--
-- * `Negate` \(: \int \to \int\)
-- * `Plus` \(: \int \to \int \to \int\)
-- * `Minus` \(: \int \to \int \to \int\)
-- * `Mult` \(: \int \to \int \to \int\)
-- * `FloorDiv` \(: \int \to \int \to \int\)
-- * `FloorMod` \(: \int \to \int \to \int\)
-- * `CeilDiv` \(: \int \to \int \to \int\)
-- * `CeilMod` \(: \int \to \int \to \int\)
-- * `Pow` \(: \int \to \int \to \int\)
--
-- === Advanced arithmetical functions
--
-- * `Abs` \(: \int \to \int\)
-- * `Gcd` \(: \int \to \int \to \int\)
-- * `Lcm` \(: \int \to \int \to \int\)
reduceConstArithmeticExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceConstArithmeticExpr :: RewriteRule m
reduceConstArithmeticExpr =
  let return' :: Integer -> Maybe Expr
return' = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> (Integer -> Expr) -> Integer -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Expr
LitInt'
   in String -> (Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String -> (Expr -> Maybe Expr) -> RewriteRule m
simpleRewriteRule String
"reduceConstArithmeticExpr" ((Expr -> Maybe Expr) -> RewriteRule m)
-> (Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \case
        Negate' (LitInt' Integer
a) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ - Integer
a
        Plus' Expr
a (LitInt' Integer
0) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
a
        Plus' (LitInt' Integer
0) Expr
b -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
b
        Plus' (LitInt' Integer
a) (LitInt' Integer
b) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b
        Minus' Expr
a (LitInt' Integer
0) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
a
        Minus' (LitInt' Integer
0) Expr
b -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Expr
Negate' Expr
b)
        Minus' (LitInt' Integer
a) (LitInt' Integer
b) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b
        Mult' Expr
_ (LitInt' Integer
0) -> Integer -> Maybe Expr
return' Integer
0
        Mult' Expr
a (LitInt' Integer
1) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
a
        Mult' (LitInt' Integer
0) Expr
_ -> Integer -> Maybe Expr
return' Integer
0
        Mult' (LitInt' Integer
1) Expr
b -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
b
        Mult' (LitInt' Integer
a) (LitInt' Integer
b) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
b
        FloorDiv' Expr
a (LitInt' Integer
1) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
a
        FloorDiv' (LitInt' Integer
a) (LitInt' Integer
b) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr)
-> (Either Error Integer -> Expr)
-> Either Error Integer
-> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Either Error Expr -> Expr
forall b a. b -> Either a b -> b
fromRight (Type -> String -> Expr
Bottom' Type
IntTy String
"division by zero") (Either Error Expr -> Expr)
-> (Either Error Integer -> Either Error Expr)
-> Either Error Integer
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Expr
LitInt' (Integer -> Expr) -> Either Error Integer -> Either Error Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Either Error Integer -> Maybe Expr)
-> Either Error Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Either Error Integer
forall (m :: * -> *).
MonadError Error m =>
Integer -> Integer -> m Integer
floorDiv Integer
a Integer
b
        FloorMod' Expr
_ (LitInt' Integer
1) -> Integer -> Maybe Expr
return' Integer
0
        FloorMod' (LitInt' Integer
a) (LitInt' Integer
b) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr)
-> (Either Error Integer -> Expr)
-> Either Error Integer
-> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Either Error Expr -> Expr
forall b a. b -> Either a b -> b
fromRight (Type -> String -> Expr
Bottom' Type
IntTy String
"modulo by zero") (Either Error Expr -> Expr)
-> (Either Error Integer -> Either Error Expr)
-> Either Error Integer
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Expr
LitInt' (Integer -> Expr) -> Either Error Integer -> Either Error Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Either Error Integer -> Maybe Expr)
-> Either Error Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Either Error Integer
forall (m :: * -> *).
MonadError Error m =>
Integer -> Integer -> m Integer
floorMod Integer
a Integer
b
        CeilDiv' Expr
a (LitInt' Integer
1) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
a
        CeilDiv' (LitInt' Integer
a) (LitInt' Integer
b) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr)
-> (Either Error Integer -> Expr)
-> Either Error Integer
-> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Either Error Expr -> Expr
forall b a. b -> Either a b -> b
fromRight (Type -> String -> Expr
Bottom' Type
IntTy String
"division by zero") (Either Error Expr -> Expr)
-> (Either Error Integer -> Either Error Expr)
-> Either Error Integer
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Expr
LitInt' (Integer -> Expr) -> Either Error Integer -> Either Error Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Either Error Integer -> Maybe Expr)
-> Either Error Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Either Error Integer
forall (m :: * -> *).
MonadError Error m =>
Integer -> Integer -> m Integer
ceilDiv Integer
a Integer
b
        CeilMod' Expr
_ (LitInt' Integer
1) -> Integer -> Maybe Expr
return' Integer
0
        CeilMod' (LitInt' Integer
a) (LitInt' Integer
b) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr)
-> (Either Error Integer -> Expr)
-> Either Error Integer
-> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Either Error Expr -> Expr
forall b a. b -> Either a b -> b
fromRight (Type -> String -> Expr
Bottom' Type
IntTy String
"modulo by zero") (Either Error Expr -> Expr)
-> (Either Error Integer -> Either Error Expr)
-> Either Error Integer
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Expr
LitInt' (Integer -> Expr) -> Either Error Integer -> Either Error Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Either Error Integer -> Maybe Expr)
-> Either Error Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Either Error Integer
forall (m :: * -> *).
MonadError Error m =>
Integer -> Integer -> m Integer
ceilMod Integer
a Integer
b
        Pow' Expr
_ (LitInt' Integer
0) -> Integer -> Maybe Expr
return' Integer
1
        Pow' Expr
a (LitInt' Integer
1) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
a
        Pow' (LitInt' Integer
a) (LitInt' Integer
b) | Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&& Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
b Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double -> Double
forall a. Floating a => a -> a
log (Double -> Double
forall a. Num a => a -> a
abs (Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
a)) Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
100 -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
b
        Abs' (LitInt' Integer
a) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
abs Integer
a
        Gcd' Expr
a (LitInt' Integer
0) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
a
        Gcd' Expr
_ (LitInt' Integer
1) -> Integer -> Maybe Expr
return' Integer
1
        Gcd' (LitInt' Integer
0) Expr
b -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
b
        Gcd' (LitInt' Integer
1) Expr
_ -> Integer -> Maybe Expr
return' Integer
1
        Gcd' (LitInt' Integer
a) (LitInt' Integer
b) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd Integer
a Integer
b
        Lcm' Expr
_ (LitInt' Integer
0) -> Integer -> Maybe Expr
return' Integer
0
        Lcm' Expr
a (LitInt' Integer
1) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
a
        Lcm' (LitInt' Integer
0) Expr
_ -> Integer -> Maybe Expr
return' Integer
0
        Lcm' (LitInt' Integer
1) Expr
b -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
b
        Lcm' (LitInt' Integer
a) (LitInt' Integer
b) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
lcm Integer
a Integer
b
        Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

-- |
-- == List of functions which are reduced
--
-- === Max functions
--
-- * `Min2` \(: \forall \alpha. \alpha \to \alpha \to \alpha\) (specialized to \(\alpha = \lbrace \bool, \int \rbrace\))
-- * `Max2` \(: \forall \alpha. \alpha \to \alpha \to \alpha\) (specialized to \(\alpha = \lbrace \bool, \int \rbrace\))
reduceConstMaxExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceConstMaxExpr :: RewriteRule m
reduceConstMaxExpr = String -> (Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String -> (Expr -> Maybe Expr) -> RewriteRule m
simpleRewriteRule String
"reduceConstMaxExpr" ((Expr -> Maybe Expr) -> RewriteRule m)
-> (Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \case
  Min2' Type
_ (LitInt' Integer
a) (LitInt' Integer
b) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> (Integer -> Expr) -> Integer -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Expr
LitInt' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
a Integer
b
  Min2' Type
_ (LitBool' Bool
a) (LitBool' Bool
b) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> (Bool -> Expr) -> Bool -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Expr
LitBool' (Bool -> Maybe Expr) -> Bool -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
min Bool
a Bool
b
  Max2' Type
_ (LitInt' Integer
a) (LitInt' Integer
b) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> (Integer -> Expr) -> Integer -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Expr
LitInt' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
a Integer
b
  Max2' Type
_ (LitBool' Bool
a) (LitBool' Bool
b) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> (Bool -> Expr) -> Bool -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Expr
LitBool' (Bool -> Maybe Expr) -> Bool -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max Bool
a Bool
b
  Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

-- |
-- == List of functions which are reduced
--
-- === Boolean functions
--
-- * `And` \(: \bool \to \bool \to \bool\)
-- * `Or` \(: \bool \to \bool \to \bool\)
-- * `Implies` \(: \bool \to \bool \to \bool\)
reduceIdempotentBooleanExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceIdempotentBooleanExpr :: RewriteRule m
reduceIdempotentBooleanExpr =
  [RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
    [ [r| "join/and" forall x. x && x = x|],
      [r| "join/or" forall x. x || x = x|],
      [r| "join/implies" forall x. implies (not x) x = x|],
      [r| "join/implies'" forall x. implies x (not x) = not x|]
    ]

-- |
-- == List of functions which are reduced
--
-- === Boolean functions
--
-- * `Not` \(: \bool \to \bool\)
-- * `And` \(: \bool \to \bool \to \bool\)
-- * `Or` \(: \bool \to \bool \to \bool\)
-- * `Implies` \(: \bool \to \bool \to \bool\)
reduceUnitBooleanExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceUnitBooleanExpr :: RewriteRule m
reduceUnitBooleanExpr =
  [RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
    [ [r| "not/true" not true = false|],
      [r| "not/false" not false = false|],
      [r| "and/false" forall x. false && x = false|],
      [r| "and/false'" forall x. x && false = false|],
      [r| "and/true" forall x. true && x = x|],
      [r| "and/true'" forall x. x && true = x|],
      [r| "or/false" forall x. false || x = x|],
      [r| "or/false'" forall x. x || false = x|],
      [r| "or/true" forall x. true || x = true|],
      [r| "or/true'" forall x. x || true = true|],
      [r| "implies/false" forall x. implies false x = true|],
      [r| "implies/false'" forall x. implies x false = not x|],
      [r| "implies/true" forall x. implies true x = x|],
      [r| "implies/true'" forall x. implies x true = true|]
    ]

-- |
-- == List of functions which are reduced
--
-- === Boolean functions
--
-- * `If` \(: \forall \alpha. \bool \to \alpha \to \alpha \to \alpha\)
reduceConstBooleanExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceConstBooleanExpr :: RewriteRule m
reduceConstBooleanExpr =
  [RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
    [ [r| "if/true" forall e1 e2. if true then e1 else e2 = e1|],
      [r| "if/false" forall e1 e2. if false then e1 else e2 = e2|]
    ]

-- |
-- == List of functions which are reduced
--
-- === Bitwise boolean functions
--
-- * `BitNot` \(: \int \to \int\)
-- * `BitAnd` \(: \int \to \int \to \int\)
-- * `BitOr` \(: \int \to \int \to \int\)
-- * `BitXor` \(: \int \to \int \to \int\)
-- * `BitLeftShift` \(: \int \to \int \to \int\)
-- * `BitRightShift` \(: \int \to \int \to \int\)
reduceUnitBitExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceUnitBitExpr :: RewriteRule m
reduceUnitBitExpr =
  [RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
    [ [r| "bitand/0" forall x. 0 & x = 0 |],
      [r| "bitand/0'" forall x. x & 0 = 0 |],
      [r| "bitand/-1" forall x. (-1) & x = x |],
      [r| "bitand/-1'" forall x. x & (-1) = x |],
      [r| "bitor/0" forall x. 0 | x = x |],
      [r| "bitor/0'" forall x. x | 0 = x |],
      [r| "bitor/-1" forall x. (-1) | x = -1 |],
      [r| "bitor/-1'" forall x. x | (-1) = -1 |],
      [r| "bitxor/0" forall x. 0 ^ x = x |],
      [r| "bitxor/0'" forall x. x ^ 0 = x |],
      [r| "bitxor/-1" forall x. (-1) ^ x = ~ x |],
      [r| "bitxor/-1'" forall x. x ^ (-1) = ~ x |],
      [r| "bitleftshift/0" forall x. 0 << x = 0 |],
      [r| "bitleftshift/0'" forall x. x << 0 = x |],
      [r| "bitrightshift/0" forall x. 0 >> x = 0 |],
      [r| "bitrightshift/0'" forall x. x >> 0 = x |]
    ]

-- |
-- == List of functions which are reduced
--
-- === Bitwise boolean functions
--
-- * `BitNot` \(: \int \to \int\)
-- * `BitAnd` \(: \int \to \int \to \int\)
-- * `BitOr` \(: \int \to \int \to \int\)
-- * `BitXor` \(: \int \to \int \to \int\)
-- * `BitLeftShift` \(: \int \to \int \to \int\)
-- * `BitRightShift` \(: \int \to \int \to \int\)
reduceConstBitExpr :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceConstBitExpr :: RewriteRule m
reduceConstBitExpr =
  let return' :: Integer -> Maybe Expr
return' = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> (Integer -> Expr) -> Integer -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Expr
LitInt'
   in String -> (Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String -> (Expr -> Maybe Expr) -> RewriteRule m
simpleRewriteRule String
"reduceConstBitExpr" ((Expr -> Maybe Expr) -> RewriteRule m)
-> (Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \case
        BitNot' (LitInt' Integer
a) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Bits a => a -> a
complement Integer
a
        BitAnd' (LitInt' Integer
a) (LitInt' Integer
b) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
b
        BitOr' (LitInt' Integer
a) (LitInt' Integer
b) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b
        BitXor' (LitInt' Integer
a) (LitInt' Integer
b) -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b
        BitLeftShift' (LitInt' Integer
a) (LitInt' Integer
b) | - Integer
100 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b Bool -> Bool -> Bool
&& Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
100 -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shift` Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
b
        BitRightShift' (LitInt' Integer
a) (LitInt' Integer
b) | - Integer
100 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b Bool -> Bool -> Bool
&& Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
100 -> Integer -> Maybe Expr
return' (Integer -> Maybe Expr) -> Integer -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shift` Integer -> Int
forall a. Num a => Integer -> a
fromInteger (- Integer
b)
        Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

-- |
-- == List of functions which are reduced
--
-- === Comparison functions
--
-- * `LessThan` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
-- * `LessEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
-- * `GreaterThan` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
-- * `GreaterEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
-- * `Equal` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
-- * `NotEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
reduceConstIntComparison :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceConstIntComparison :: RewriteRule m
reduceConstIntComparison =
  String -> (Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String -> (Expr -> Maybe Expr) -> RewriteRule m
simpleRewriteRule String
"comparison/const/int" ((Expr -> Maybe Expr) -> RewriteRule m)
-> (Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$
    (Bool -> Expr
LitBool' (Bool -> Expr) -> Maybe Bool -> Maybe Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe Bool -> Maybe Expr)
-> (Expr -> Maybe Bool) -> Expr -> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      LessThan' Type
_ (LitInt' Integer
a) (LitInt' Integer
b) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b
      LessEqual' Type
_ (LitInt' Integer
a) (LitInt' Integer
b) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
b
      GreaterThan' Type
_ (LitInt' Integer
a) (LitInt' Integer
b) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
b
      GreaterEqual' Type
_ (LitInt' Integer
a) (LitInt' Integer
b) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
b
      Equal' Type
_ (LitInt' Integer
a) (LitInt' Integer
b) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
b
      NotEqual' Type
_ (LitInt' Integer
a) (LitInt' Integer
b) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
b
      Expr
_ -> Maybe Bool
forall a. Maybe a
Nothing

-- |
-- == List of functions which are reduced
--
-- === Comparison functions
--
-- * `LessThan` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
-- * `LessEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
-- * `GreaterThan` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
-- * `GreaterEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
-- * `Equal` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
-- * `NotEqual` \(: \forall \alpha. \alpha \to \alpha \to \bool\) (specialized to \(\alpha \in \lbrace \bool, \int \rbrace\))
reduceUnitBooleanComparison :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceUnitBooleanComparison :: RewriteRule m
reduceUnitBooleanComparison =
  [RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
    [ -- TODO: implement lessthan and lessequal
      -- NOTE: We can ignore greaterthan and greaterequal because EqualitySolving swaps inequalities.
      [r| "equal/true" forall x. true == x = x |],
      [r| "equal/true'" forall x. x == true = x |],
      [r| "equal/false" forall x. false == x = not x |],
      [r| "equal/false'" forall x. x == false = not x |],
      [r| "notequal/true" forall x. true /= x = not x |],
      [r| "notequal/true'" forall x. x /= true = not x |],
      [r| "notequal/false" forall x. false /= x = x |],
      [r| "notequal/false'" forall x. x /= false = x |]
    ]

rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m
rule :: RewriteRule m
rule =
  [RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
    [ RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceConstArithmeticExpr,
      RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceConstMaxExpr,
      RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceIdempotentBooleanExpr,
      RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceUnitBooleanExpr,
      RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceConstBooleanExpr,
      RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceUnitBitExpr,
      RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceConstBitExpr,
      RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceConstIntComparison,
      RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceUnitBooleanComparison
    ]

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` folds constants in given programs.
-- For example, this converts the following:
--
-- > 3 x + 2 + 1
--
-- to the follwoing:
--
-- > 3 x + 3
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.ConstantFolding" (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