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

-- |
-- Module      : Jikka.Core.Convert.CloseAll
-- Description : does reductions about @all@ and @any@, and tries to rewrite with closed-form exprs. / @all@ と @any@ についての簡約を行い、閉じた式への書き換えを目指します。
-- Copyright   : (c) Kimiyuki Onaka, 2021
-- License     : Apache License 2.0
-- Maintainer  : kimiyuki95@gmail.com
-- Stability   : experimental
-- Portability : portable
module Jikka.Core.Convert.CloseAll
  ( run,

    -- * internal rules
    rule,
    reduceAll,
    reduceAny,
  )
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
import Jikka.Core.Language.Util

reduceAll :: MonadAlpha m => RewriteRule m
reduceAll :: RewriteRule m
reduceAll =
  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
        -- list build functions
        All' (Nil' Type
_) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
LitTrue
        All' (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' Expr
x (Expr -> Expr
All' Expr
xs)
        -- list map functions
        All' (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
$ Expr -> Expr
All' Expr
xs
        All' (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
$ Expr -> Expr
All' Expr
xs
        All' (Filter' Type
_ Expr
f Expr
xs) -> do
          VarName
x <- 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
$ Expr -> Expr
All' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
BoolTy Type
BoolTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
BoolTy (Expr -> Expr -> Expr
Implies' (Expr -> Expr -> Expr
App Expr
f (VarName -> Expr
Var VarName
x)) (VarName -> Expr
Var VarName
x))) Expr
xs)
        All' (Map' Type
_ Type
_ Expr
f Expr
xs) -> case Expr
f of
          Lam VarName
x Type
_ (Not' Expr
e) -> do
            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
Not' (Expr -> Expr
Any' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
BoolTy Type
BoolTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
BoolTy Expr
e) Expr
xs))
          Lam VarName
x Type
_ (And' Expr
e1 Expr
e2) -> do
            VarName
x1 <- VarName -> m VarName
forall (m :: * -> *). MonadAlpha m => VarName -> m VarName
genVarName VarName
x
            VarName
x2 <- VarName -> m VarName
forall (m :: * -> *). MonadAlpha m => VarName -> m VarName
genVarName 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
$ Expr -> Expr -> Expr
And' (Expr -> Expr
All' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
BoolTy Type
BoolTy (VarName -> Type -> Expr -> Expr
Lam VarName
x1 Type
BoolTy Expr
e1) Expr
xs)) (Expr -> Expr
All' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
BoolTy Type
BoolTy (VarName -> Type -> Expr -> Expr
Lam VarName
x2 Type
BoolTy Expr
e2) Expr
xs))
          Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing
        -- others
        Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing

reduceAny :: MonadAlpha m => RewriteRule m
reduceAny :: RewriteRule m
reduceAny =
  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
        -- list build functions
        Any' (Nil' Type
_) -> Expr -> m (Maybe Expr)
forall a. a -> m (Maybe a)
return' Expr
LitFalse
        Any' (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
Or' Expr
x (Expr -> Expr
Any' Expr
xs)
        -- list map functions
        Any' (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
$ Expr -> Expr
Any' Expr
xs
        Any' (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
$ Expr -> Expr
Any' Expr
xs
        Any' (Filter' Type
_ Expr
f Expr
xs) -> do
          VarName
x <- 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
$ Expr -> Expr
Any' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
BoolTy Type
BoolTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
BoolTy (Expr -> Expr -> Expr
And' (Expr -> Expr -> Expr
App Expr
f (VarName -> Expr
Var VarName
x)) (VarName -> Expr
Var VarName
x))) Expr
xs)
        Any' (Map' Type
_ Type
_ Expr
f Expr
xs) -> case Expr
f of
          Lam VarName
x Type
_ (Not' Expr
e) -> do
            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
Not' (Expr -> Expr
All' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
BoolTy Type
BoolTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
BoolTy Expr
e) Expr
xs))
          Lam VarName
x Type
_ (Or' Expr
e1 Expr
e2) -> do
            VarName
x1 <- VarName -> m VarName
forall (m :: * -> *). MonadAlpha m => VarName -> m VarName
genVarName VarName
x
            VarName
x2 <- VarName -> m VarName
forall (m :: * -> *). MonadAlpha m => VarName -> m VarName
genVarName 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
$ Expr -> Expr -> Expr
Or' (Expr -> Expr
Any' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
BoolTy Type
BoolTy (VarName -> Type -> Expr -> Expr
Lam VarName
x1 Type
BoolTy Expr
e1) Expr
xs)) (Expr -> Expr
Any' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
BoolTy Type
BoolTy (VarName -> Type -> Expr -> Expr
Lam VarName
x2 Type
BoolTy Expr
e2) Expr
xs))
          Lam VarName
x Type
_ (Implies' Expr
e1 Expr
e2) -> do
            VarName
x1 <- VarName -> m VarName
forall (m :: * -> *). MonadAlpha m => VarName -> m VarName
genVarName VarName
x
            VarName
x2 <- VarName -> m VarName
forall (m :: * -> *). MonadAlpha m => VarName -> m VarName
genVarName 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
$ Expr -> Expr -> Expr
Or' (Expr -> Expr
Any' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
BoolTy Type
BoolTy (VarName -> Type -> Expr -> Expr
Lam VarName
x1 Type
BoolTy (Expr -> Expr
Negate' Expr
e1)) Expr
xs)) (Expr -> Expr
Any' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
BoolTy Type
BoolTy (VarName -> Type -> Expr -> Expr
Lam VarName
x2 Type
BoolTy Expr
e2) Expr
xs))
          Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing
        -- 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
reduceAll,
      RewriteRule m
forall (m :: * -> *). MonadAlpha m => RewriteRule m
reduceAny
    ]

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` reduces `All` and `Any`.
--
-- == Examples
--
-- Before:
--
-- > any (filter (fun x -> x || f x) xs)
--
-- After:
--
-- > any xs || any (map f xs)
--
-- == List of builtin functions which are reduced
--
-- \[
--     \newcommand\int{\mathbf{int}}
--     \newcommand\bool{\mathbf{bool}}
--     \newcommand\list{\mathbf{list}}
-- \]
--
-- === Target functions
--
-- * `All` \(: \list(\bool) \to \bool\)
-- * `Any` \(: \list(\bool) \to \bool\)
--
-- === Boolean functions
--
-- * `Not` \(: \bool \to \bool\)
-- * `And` \(: \bool \to \bool \to \bool\)
-- * `Or` \(: \bool \to \bool \to \bool\)
-- * `Implies` \(: \bool \to \bool \to \bool\)
--
-- === List Build functions
--
-- * `Nil` \(: \forall \alpha. \list(\alpha)\)
-- * `Cons` \(: \forall \alpha. \alpha \to \list(\alpha) \to \list(\alpha)\)
--
-- === List 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)\)
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.CloseAll" (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