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

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

    -- * internal rules
    rule,
    reduceMin,
    reduceMax,
    reduceArgMin,
    reduceArgMax,
  )
where

import Jikka.Common.Alpha
import Jikka.Common.Error
import qualified Jikka.Core.Convert.Alpha as Alpha
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

reduceMin :: Monad m => RewriteRule m
reduceMin :: RewriteRule m
reduceMin = (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
  -- list build functions
  Min1' Type
t (Nil' Type
_) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Type -> String -> Expr
Bottom' Type
t String
"no minimum in empty list"
  Min1' Type
_ (Cons' Type
_ Expr
e (Nil' Type
_)) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
  Min1' Type
t (Cons' Type
_ Expr
e (Cons' Type
_ Expr
e' Expr
es)) -> 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
Min2' Type
t Expr
e (Type -> Expr -> Expr
Min1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t Expr
e' Expr
es))
  -- list map functions
  Min1' Type
t (Reversed' Type
_ Expr
es) -> 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
Min1' Type
t Expr
es
  Min1' Type
t (Cons' Type
_ Expr
e (Reversed' Type
_ Expr
es)) -> 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
Min1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t Expr
e Expr
es)
  Min1' Type
t (Sorted' Type
_ Expr
es) -> 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
Min1' Type
t Expr
es
  Min1' Type
t (Cons' Type
_ Expr
e (Sorted' Type
_ Expr
es)) -> 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
Min1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t Expr
e Expr
es)
  Min1' Type
t (Map' Type
t1 Type
t2 Expr
f Expr
es) -> case Expr
f of
    Lam VarName
x Type
_ Expr
e | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
e -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
    Lam VarName
x Type
_ (Min2' Type
_ 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
Min2' Type
t (Type -> Expr -> Expr
Min1' Type
t (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e1) Expr
es)) (Type -> Expr -> Expr
Min1' Type
t (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e2) Expr
es))
    Lam VarName
x Type
_ (Negate' Expr
e) -> 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
Max1' Type
t (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e) Expr
es))
    Lam VarName
x Type
_ (Plus' Expr
e1 Expr
e2) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
e1 -> 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 (Type -> Expr -> Expr
Min1' Type
t (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e2) Expr
es))
    Lam VarName
x Type
_ (Plus' Expr
e1 Expr
e2) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` 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' (Type -> Expr -> Expr
Min1' Type
t (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e1) Expr
es)) Expr
e2
    Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing
  Min1' Type
t (Cons' Type
_ Expr
e0 (Map' Type
t1 Type
t2 Expr
f Expr
xs)) -> case Expr
f of
    Lam VarName
x Type
_ Expr
e | VarName
x VarName -> Expr -> Bool
`isUnusedVar` 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 -> Expr
If' Type
t (Type -> Expr -> Expr -> Expr
Equal' Type
IntTy (Type -> Expr -> Expr
Len' Type
t Expr
xs) Expr
Lit0) Expr
e0 (Type -> Expr -> Expr -> Expr
Min2' Type
t Expr
e0 Expr
e)
    Lam VarName
x Type
_ (Min2' Type
_ 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
Min2' Type
t (Type -> Expr -> Expr
Min1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t Expr
e0 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e1) Expr
xs))) (Type -> Expr -> Expr
Min1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t Expr
e0 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e2) Expr
xs)))
    Lam VarName
x Type
_ (Negate' Expr
e) -> 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
Max1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t (Expr -> Expr
Negate' Expr
e0) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e) Expr
xs)))
    Lam VarName
x Type
_ (Plus' Expr
e1 Expr
e2) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
e1 -> 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 (Type -> Expr -> Expr
Min1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t (Expr -> Expr -> Expr
Minus' Expr
e0 Expr
e1) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e2) Expr
xs)))
    Lam VarName
x Type
_ (Plus' Expr
e1 Expr
e2) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` 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' (Type -> Expr -> Expr
Min1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t (Expr -> Expr -> Expr
Minus' Expr
e0 Expr
e1) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e1) Expr
xs))) Expr
e2
    Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing
  Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

reduceMax :: Monad m => RewriteRule m
reduceMax :: RewriteRule m
reduceMax = (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
  -- list build functions
  Max1' Type
t (Nil' Type
_) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Type -> String -> Expr
Bottom' Type
t String
"no maximum in empty list"
  Max1' Type
_ (Cons' Type
_ Expr
e (Nil' Type
_)) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
  Max1' Type
t (Cons' Type
_ Expr
e (Cons' Type
_ Expr
e' Expr
es)) -> 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
t Expr
e (Type -> Expr -> Expr
Max1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t Expr
e' Expr
es))
  -- list map functions
  Max1' Type
t (Reversed' Type
_ Expr
es) -> 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
Max1' Type
t Expr
es
  Max1' Type
t (Cons' Type
_ Expr
e (Reversed' Type
_ Expr
es)) -> 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
Max1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t Expr
e Expr
es)
  Max1' Type
t (Sorted' Type
_ Expr
es) -> 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
Max1' Type
t Expr
es
  Max1' Type
t (Cons' Type
_ Expr
e (Sorted' Type
_ Expr
es)) -> 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
Max1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t Expr
e Expr
es)
  Max1' Type
t (Map' Type
t1 Type
t2 Expr
f Expr
es) -> case Expr
f of
    Lam VarName
x Type
_ Expr
e | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
e -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
    Lam VarName
x Type
_ (Max2' Type
_ 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
Max2' Type
t (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e1) Expr
es) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e2) Expr
es)
    Lam VarName
x Type
_ (Negate' Expr
e) -> 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
Min1' Type
t2 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e) Expr
es))
    Lam VarName
x Type
_ (Plus' Expr
e1 Expr
e2) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
e1 -> 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 (Type -> Expr -> Expr
Max1' Type
t2 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e2) Expr
es))
    Lam VarName
x Type
_ (Plus' Expr
e1 Expr
e2) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` 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' (Type -> Expr -> Expr
Max1' Type
t2 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e1) Expr
es)) Expr
e2
    Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing
  Max1' Type
t (Cons' Type
_ Expr
e0 (Map' Type
t1 Type
t2 Expr
f Expr
xs)) -> case Expr
f of
    Lam VarName
x Type
_ Expr
e | VarName
x VarName -> Expr -> Bool
`isUnusedVar` 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 -> Expr
If' Type
t (Type -> Expr -> Expr -> Expr
Equal' Type
IntTy (Type -> Expr -> Expr
Len' Type
t Expr
xs) Expr
Lit0) Expr
e0 (Type -> Expr -> Expr -> Expr
Max2' Type
t Expr
e0 Expr
e)
    Lam VarName
x Type
_ (Max2' Type
_ 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
Max2' Type
t (Type -> Expr -> Expr
Max1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t Expr
e0 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e1) Expr
xs))) (Type -> Expr -> Expr
Max1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t Expr
e0 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e2) Expr
xs)))
    Lam VarName
x Type
_ (Negate' Expr
e) -> 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
Min1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t (Expr -> Expr
Negate' Expr
e0) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e) Expr
xs)))
    Lam VarName
x Type
_ (Plus' Expr
e1 Expr
e2) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
e1 -> 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 (Type -> Expr -> Expr
Max1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t (Expr -> Expr -> Expr
Minus' Expr
e0 Expr
e1) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e2) Expr
xs)))
    Lam VarName
x Type
_ (Plus' Expr
e1 Expr
e2) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` 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' (Type -> Expr -> Expr
Max1' Type
t (Type -> Expr -> Expr -> Expr
Cons' Type
t (Expr -> Expr -> Expr
Minus' Expr
e0 Expr
e1) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
IntTy Expr
e1) Expr
xs))) Expr
e2
    Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing
  Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

-- | TODO: implement this
reduceArgMin :: Monad m => RewriteRule m
reduceArgMin :: RewriteRule m
reduceArgMin = (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
  -- list map functions
  ArgMin' Type
t (Reversed' Type
_ Expr
xs) -> 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
Minus' (Expr -> Expr -> Expr
Minus' (Type -> Expr -> Expr
Len' Type
t Expr
xs) (Type -> Expr -> Expr
ArgMin' Type
t Expr
xs)) Expr
Lit1
  ArgMin' Type
_ (Map' Type
_ Type
_ (Lam VarName
x Type
_ Expr
e) Expr
_) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
e -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
Lit0
  ArgMin' Type
_ (Map' Type
t1 Type
t2 (Lam VarName
x Type
t (Plus' Expr
e1 Expr
e2)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
e1 -> 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
ArgMin' Type
t2 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e2) Expr
xs)
  ArgMin' Type
_ (Map' Type
t1 Type
t2 (Lam VarName
x Type
t (Plus' Expr
e1 Expr
e2)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` 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
ArgMin' Type
t2 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e1) Expr
xs)
  Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

-- | TODO: implement this
reduceArgMax :: Monad m => RewriteRule m
reduceArgMax :: RewriteRule m
reduceArgMax = (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
  -- list map functions
  ArgMax' Type
t (Reversed' Type
_ Expr
xs) -> 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
Minus' (Expr -> Expr -> Expr
Minus' (Type -> Expr -> Expr
Len' Type
t Expr
xs) (Type -> Expr -> Expr
ArgMax' Type
t Expr
xs)) Expr
Lit1
  ArgMax' Type
_ (Map' Type
_ Type
_ (Lam VarName
x Type
t Expr
e) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
e -> 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
Minus' (Type -> Expr -> Expr
Len' Type
t Expr
xs) Expr
Lit1
  ArgMax' Type
_ (Map' Type
t1 Type
t2 (Lam VarName
x Type
t (Plus' Expr
e1 Expr
e2)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
e1 -> 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
ArgMax' Type
t2 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e2) Expr
xs)
  ArgMax' Type
_ (Map' Type
t1 Type
t2 (Lam VarName
x Type
t (Plus' Expr
e1 Expr
e2)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` 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
ArgMax' Type
t2 (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e1) Expr
xs)
  Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing

rule :: Monad 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
reduceMin,
      RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
reduceMax,
      RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
reduceArgMin,
      RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
reduceArgMax
    ]

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 :: * -> *). Monad m => RewriteRule m
rule

-- | `run` reduces maximums and minimums.
--
-- == Examples
--
-- Before:
--
-- > max (map (fun x -> 3 + f x) xs)
--
-- After:
--
-- > 3 + max (map f xs)
--
-- == List of builtin functions which are reduced
--
-- \[
--     \newcommand\int{\mathbf{int}}
--     \newcommand\bool{\mathbf{bool}}
--     \newcommand\list{\mathbf{list}}
-- \]
--
-- === Target functions
--
-- * `Max1` \(: \forall \alpha. \list(\alpha) \to \alpha\)
-- * `Min1` \(: \forall \alpha. \list(\alpha) \to \alpha\)
-- * `ArgMax` \(: \forall \alpha. \list(\alpha) \to \int\)
-- * `ArgMin` \(: \forall \alpha. \list(\alpha) \to \int\)
--
-- === Related functions
--
-- * `Max2` \(: \forall \alpha. \alpha \to \alpha \to \alpha\)
-- * `Min2` \(: \forall \alpha. \alpha \to \alpha \to \alpha\)
--
-- === List Build functions
--
-- * `Nil` \(: \forall \alpha. \list(\alpha)\)
-- * `Cons` \(: \forall \alpha. \alpha \to \list(\alpha) \to \list(\alpha)\)
-- * `Range1` \(: \int \to \list(\int)\)
--
-- === 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.CloseMin" (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
  Program
prog <- Program -> m Program
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
Program -> m Program
Alpha.run 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