content: {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE QuasiQuotes #-}
  {-# LANGUAGE ViewPatterns #-}
  
  -- |
  -- Module      : Jikka.Core.Convert.EqualitySolving
  -- Description : equality solving. / 等式を解きます
  -- Copyright   : (c) Kimiyuki Onaka, 2021
  -- License     : Apache License 2.0
  -- Maintainer  : hotman78@gmail.com
  -- Stability   : experimental
  -- Portability : portable
  --
  -- \[
  --     \newcommand\int{\mathbf{int}}
  --     \newcommand\bool{\mathbf{bool}}
  --     \newcommand\list{\mathbf{list}}
  -- \]
  module Jikka.Core.Convert.EqualitySolving
    ( run,
      rule,
  
      -- * internal rules
      moveLiteralToRight,
      convertGreaterToLess,
      reduceReflexivity,
      makeRightZero,
      reduceIntInjective,
      reduceNot,
      reduceListCtor,
      reduceListInjective,
    )
  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.QuasiRules
  import Jikka.Core.Language.RewriteRules
  import Jikka.Core.Language.Util
  
  -- | `moveLiteralToRight` moves literals to lhs of `(==)` or `(/=)`, using symmetricity.
  moveLiteralToRight :: (MonadAlpha m, MonadError Error m) => RewriteRule m
  moveLiteralToRight =
    mconcat
      [ simpleRewriteRule "equal/symmetricity/literal" $ \case
          Equal' t x y | isLiteral x && not (isLiteral y) -> Just $ Equal' t y x
          _ -> Nothing,
        simpleRewriteRule "notequal/symmetricity/literal" $ \case
          Equal' t x y | isLiteral x && not (isLiteral y) -> Just $ Equal' t y x
          _ -> Nothing
      ]
  
  -- | `convertGreaterToLess` erases `(>)` and `(>=)`.
  convertGreaterToLess :: (MonadAlpha m, MonadError Error m) => RewriteRule m
  convertGreaterToLess =
    mconcat
      [ [r| "greaterthan->lessthan" forall x y. x > y = y < x |],
        [r| "greaterequal->lessequal" forall x y. x >= y = y <= x |]
      ]
  
  -- | `reduceReflexivity` uses reflexivity.
  reduceReflexivity :: (MonadAlpha m, MonadError Error m) => RewriteRule m
  reduceReflexivity =
    mconcat
      [ [r| "lessthan/reflexivity" forall x. x == x = false |],
        [r| "lessequal/reflexivity" forall x. x == x = true |],
        [r| "equal/reflexivity" forall x. x == x = true |],
        [r| "notequal/reflexivity" forall x. x == x = false |]
      ]
  
  -- | `makeRightZero` makes RHS of integer equality/inequality zero with subtracting RHS from both sides.
  makeRightZero :: (MonadAlpha m, MonadError Error m) => RewriteRule m
  makeRightZero =
    mconcat
      [ simpleRewriteRule "lessthan/right-zero" $ \case
          LessThan' IntTy x y | y /= LitInt' 0 -> Just $ LessThan' IntTy (Minus' x y) (LitInt' 0)
          _ -> Nothing,
        simpleRewriteRule "lessequal/right-zero" $ \case
          LessEqual' IntTy x y | y /= LitInt' 0 -> Just $ LessEqual' IntTy (Minus' x y) (LitInt' 0)
          _ -> Nothing,
        simpleRewriteRule "equal/right-zero" $ \case
          Equal' IntTy x y | y /= LitInt' 0 -> Just $ Equal' IntTy (Minus' x y) (LitInt' 0)
          _ -> Nothing,
        simpleRewriteRule "notequal/right-zero" $ \case
          NotEqual' IntTy x y | y /= LitInt' 0 -> Just $ NotEqual' IntTy (Minus' x y) (LitInt' 0)
          _ -> Nothing
      ]
  
  -- | `reduceIntInjective` removes injective functions from equalities of integers.
  reduceIntInjective :: (MonadAlpha m, MonadError Error m) => RewriteRule m
  reduceIntInjective =
    mconcat
      [ [r| "equal/negate" forall x y k. - x == 0 = x == 0  |],
        [r| "equal/fact" forall x y. fact x - fact y == 0 = x == y  |],
        [r| "equal/fact'" forall x y. - fact x + fact y == 0 = x == y  |]
      ]
  
  reduceNot :: (MonadAlpha m, MonadError Error m) => RewriteRule m
  reduceNot =
    mconcat
      [ [r| "equal/not" forall x y. not x == y = x /= y |],
        [r| "equal/not'" forall x y. x == not y = x /= y |],
        [r| "notequal/not" forall x y. not x /= y = x == y |],
        [r| "notequal/not'" forall x y. x /= not y = x == y |]
      ]
  
  reduceListCtor :: (MonadAlpha m, MonadError Error m) => RewriteRule m
  reduceListCtor =
    mconcat
      [ [r| "equal/nil/nil" forall x xs. nil == nil = true |],
        [r| "equal/cons/nil" forall x xs. cons x xs == nil = false |],
        [r| "equal/nil/cons" forall x xs. nil == cons x xs = false |],
        [r| "equal/cons/cons" forall x xs y ys. cons x xs == cons y ys = x == y && xs == ys |]
      ]
  
  reduceListInjective :: (MonadAlpha m, MonadError Error m) => RewriteRule m
  reduceListInjective =
    mconcat
      [ [r| "equal/range/range" forall n1 n2. range n1 == range n2 = n1 == n2 |]
      ]
  
  rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m
  rule =
    mconcat
      [ moveLiteralToRight,
        convertGreaterToLess,
        reduceReflexivity,
        makeRightZero,
        reduceIntInjective,
        reduceNot,
        reduceListCtor,
        reduceListInjective
      ]
  
  runProgram :: (MonadAlpha m, MonadError Error m) => Program -> m Program
  runProgram = applyRewriteRuleProgram' rule
  
  run :: (MonadAlpha m, MonadError Error m) => Program -> m Program
  run prog = wrapError' "Jikka.Core.Convert.EqualitySolving" $ do
    precondition $ do
      lint prog
    prog <- runProgram prog
    postcondition $ do
      lint prog
    return prog
  