{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ViewPatterns #-}
module Jikka.Core.Convert.CloseMin
( run,
rule,
reduceMin,
reduceMax,
reduceArgMin,
reduceArgMax,
)
where
import Jikka.Common.Alpha
import Jikka.Common.Error
import Jikka.Core.Language.AssertedHint
import Jikka.Core.Language.BuiltinPatterns
import Jikka.Core.Language.Expr
import Jikka.Core.Language.FreeVars
import Jikka.Core.Language.LambdaPatterns
import Jikka.Core.Language.Lint
import Jikka.Core.Language.QuasiRules
import Jikka.Core.Language.RewriteRules
reduceMin :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceMin :: RewriteRule m
reduceMin =
[RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
[
String
-> (RewriteEnvironment -> Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> Maybe Expr) -> RewriteRule m
pureRewriteRule String
"minimum/cons" ((RewriteEnvironment -> Expr -> Maybe Expr) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
env -> \case
Min1' Type
t (Cons' Type
_ Expr
x Expr
xs) | [(VarName, AssertedHint)] -> Expr -> Maybe Bool
nullWithHints (RewriteEnvironment -> [(VarName, AssertedHint)]
assertedHints RewriteEnvironment
env) Expr
xs Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False -> 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
x (Type -> Expr -> Expr
Min1' Type
t Expr
xs)
Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing,
[r| "minimum/nil" minimum nil = bottom<"no minimum in empty list"> |],
[r| "minimum/cons/cons" forall x y zs. minimum (cons x (cons y zs)) = min x (minimum (cons y zs)) |],
[r| "minimum/range" forall n. minimum (range n) = 0 |],
[r| "minimum/reversed" forall xs. minimum (reversed xs) = minimum xs |],
[r| "minimum/cons/reversed" forall x xs. minimum (cons x (reversed xs)) = minimum (cons x xs) |],
[r| "minimum/sorted" forall xs. minimum (sorted xs) = minimum xs |],
[r| "minimum/cons/sorted" forall x xs. minimum (cons x (sorted xs)) = minimum (cons x xs) |],
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"minimum/map/const" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Min1' Type
_ (Map' Type
_ Type
_ (LamConst Type
_ Expr
e) Expr
_) -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr)) -> Maybe Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
[r| "minimum/map/min" forall e1 e2 xs. minimum (map (fun x -> min e1 e2) xs) = min (minimum (map (fun x -> e1) xs)) (minimum (map (fun x -> e2) xs)) |],
[r| "minimum/map/negate" forall e xs. minimum (map (fun x -> - e) xs) = - (maximum (map (fun x -> e) xs)) |],
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"minimum/map/plus" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Min1' Type
_ (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Plus' Expr
k Expr
e)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Plus' Expr
k (Type -> Expr -> Expr
Min1' Type
IntTy (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"minimum/map/plus'" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Min1' Type
_ (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Plus' Expr
e Expr
k)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Plus' Expr
k (Type -> Expr -> Expr
Min1' Type
IntTy (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"minimum/map/minus" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Min1' Type
_ (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Minus' Expr
k Expr
e)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Minus' Expr
k (Type -> Expr -> Expr
Max1' Type
IntTy (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"minimum/map/minus'" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Min1' Type
_ (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Minus' Expr
e Expr
k)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Minus' Expr
k (Type -> Expr -> Expr
Min1' Type
IntTy (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"minimum/cons/map/const" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Min1' Type
t (Cons' Type
_ Expr
x (Map' Type
_ Type
_ (LamConst Type
_ Expr
e) Expr
_)) -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr -> Expr
Min2' Type
t Expr
x Expr
e
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
[r| "minimum/cons/map/min" forall e0 e1 e2 xs. minimum (cons e0 (map (fun x -> min e1 e2) xs)) = min (minimum (cons e0 (map (fun x -> e1) xs))) (minimum (cons x (map (fun x -> e2) xs))) |],
[r| "minimum/cons/map/negate" forall e0 e xs. minimum (cons e0 (map (fun x -> - e) xs)) = - (maximum (cons (- e0) (map (fun x -> e) xs))) |],
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"minimum/cons/map/plus" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Min1' Type
_ (Cons' Type
_ Expr
e0 (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Plus' Expr
k Expr
e)) Expr
xs)) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Plus' Expr
k (Type -> Expr -> Expr
Min1' Type
IntTy (Type -> Expr -> Expr -> Expr
Cons' Type
IntTy (Expr -> Expr -> Expr
Minus' Expr
e0 Expr
k) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs)))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"minimum/cons/map/plus'" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Min1' Type
_ (Cons' Type
_ Expr
e0 (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Plus' Expr
e Expr
k)) Expr
xs)) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Plus' Expr
k (Type -> Expr -> Expr
Min1' Type
IntTy (Type -> Expr -> Expr -> Expr
Cons' Type
IntTy (Expr -> Expr -> Expr
Minus' Expr
e0 Expr
k) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs)))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"minimum/cons/map/minus" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Min1' Type
_ (Cons' Type
_ Expr
e0 (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Minus' Expr
k Expr
e)) Expr
xs)) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Minus' Expr
k (Type -> Expr -> Expr
Max1' Type
IntTy (Type -> Expr -> Expr -> Expr
Cons' Type
IntTy (Expr -> Expr -> Expr
Minus' Expr
k Expr
e0) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs)))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"minimum/cons/map/minus'" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Min1' Type
_ (Cons' Type
_ Expr
e0 (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Minus' Expr
e Expr
k)) Expr
xs)) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Minus' (Type -> Expr -> Expr
Min1' Type
IntTy (Type -> Expr -> Expr -> Expr
Cons' Type
IntTy (Expr -> Expr -> Expr
Plus' Expr
e0 Expr
k) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs))) Expr
k
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing
]
reduceMax :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceMax :: RewriteRule m
reduceMax =
[RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
[
String
-> (RewriteEnvironment -> Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> Maybe Expr) -> RewriteRule m
pureRewriteRule String
"maximum/cons" ((RewriteEnvironment -> Expr -> Maybe Expr) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
env -> \case
Max1' Type
t (Cons' Type
_ Expr
x Expr
xs) | [(VarName, AssertedHint)] -> Expr -> Maybe Bool
nullWithHints (RewriteEnvironment -> [(VarName, AssertedHint)]
assertedHints RewriteEnvironment
env) Expr
xs Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False -> 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
x (Type -> Expr -> Expr
Max1' Type
t Expr
xs)
Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing,
[r| "maximum/nil" maximum nil = bottom<"no maximum in empty list"> |],
[r| "maximum/cons/cons" forall x y zs. maximum (cons x (cons y zs)) = max x (maximum (cons y zs)) |],
[r| "maximum/range" forall n. maximum (range n) = n - 1 |],
[r| "maximum/reversed" forall xs. maximum (reversed xs) = maximum xs |],
[r| "maximum/cons/reversed" forall x xs. maximum (cons x (reversed xs)) = maximum (cons x xs) |],
[r| "maximum/sorted" forall xs. maximum (sorted xs) = maximum xs |],
[r| "maximum/cons/sorted" forall x xs. maximum (cons x (sorted xs)) = maximum (cons x xs) |],
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"maximum/map/const" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Max1' Type
_ (Map' Type
_ Type
_ (LamConst Type
_ Expr
e) Expr
_) -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr)) -> Maybe Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
[r| "maximum/map/max" forall e1 e2 xs. maximum (map (fun x -> max e1 e2) xs) = max (maximum (map (fun x -> e1) xs)) (maximum (map (fun x -> e2) xs)) |],
[r| "maximum/map/negate" forall e xs. maximum (map (fun x -> - e) xs) = - (maximum (map (fun x -> e) xs)) |],
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"maximum/map/plus" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Max1' Type
_ (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Plus' Expr
k Expr
e)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Plus' Expr
k (Type -> Expr -> Expr
Max1' Type
IntTy (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"maximum/map/plus'" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Max1' Type
_ (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Plus' Expr
e Expr
k)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Plus' Expr
k (Type -> Expr -> Expr
Max1' Type
IntTy (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"maximum/map/minus" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Max1' Type
_ (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Minus' Expr
k Expr
e)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Minus' Expr
k (Type -> Expr -> Expr
Min1' Type
IntTy (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"maximum/map/minus'" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Max1' Type
_ (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Minus' Expr
e Expr
k)) Expr
xs) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Minus' Expr
k (Type -> Expr -> Expr
Max1' Type
IntTy (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"maximum/cons/map/const" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Max1' Type
t (Cons' Type
_ Expr
x (Map' Type
_ Type
_ (LamConst Type
_ Expr
e) Expr
_)) -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Type -> Expr -> Expr -> Expr
Max2' Type
t Expr
x Expr
e
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
[r| "maximum/cons/map/max" forall e0 e1 e2 xs. maximum (cons e0 (map (fun x -> max e1 e2) xs)) = max (maximum (cons e0 (map (fun x -> e1) xs))) (maximum (cons e0 (map (fun x -> e2) xs))) |],
[r| "maximum/cons/map/negate" forall e0 e xs. maximum (cons e0 (map (fun x -> - e) xs)) = - (minimum (cons e0 (map (fun x -> e) xs))) |],
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"maximum/cons/map/plus" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Max1' Type
_ (Cons' Type
_ Expr
e0 (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Plus' Expr
k Expr
e)) Expr
xs)) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Plus' Expr
k (Type -> Expr -> Expr
Max1' Type
IntTy (Type -> Expr -> Expr -> Expr
Cons' Type
IntTy (Expr -> Expr -> Expr
Minus' Expr
e0 Expr
k) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs)))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"maximum/cons/map/plus'" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Max1' Type
_ (Cons' Type
_ Expr
e0 (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Plus' Expr
e Expr
k)) Expr
xs)) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Plus' Expr
k (Type -> Expr -> Expr
Max1' Type
IntTy (Type -> Expr -> Expr -> Expr
Cons' Type
IntTy (Expr -> Expr -> Expr
Minus' Expr
e0 Expr
k) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs)))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"maximum/cons/map/minus" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Max1' Type
_ (Cons' Type
_ Expr
e0 (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Minus' Expr
k Expr
e)) Expr
xs)) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Minus' Expr
k (Type -> Expr -> Expr
Min1' Type
IntTy (Type -> Expr -> Expr -> Expr
Cons' Type
IntTy (Expr -> Expr -> Expr
Minus' Expr
k Expr
e0) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs)))
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule String
"maximum/cons/map/minus'" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Max1' Type
_ (Cons' Type
_ Expr
e0 (Map' Type
t1 Type
_ (Lam VarName
x Type
_ (Minus' Expr
e Expr
k)) Expr
xs)) | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> m (Maybe Expr))
-> (Expr -> Maybe Expr) -> Expr -> m (Maybe Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> m (Maybe Expr)) -> Expr -> m (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
Minus' (Type -> Expr -> Expr
Max1' Type
IntTy (Type -> Expr -> Expr -> Expr
Cons' Type
IntTy (Expr -> Expr -> Expr
Plus' Expr
e0 Expr
k) (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
IntTy (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t1 Expr
e) Expr
xs))) Expr
k
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing
]
reduceArgMin :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceArgMin :: RewriteRule m
reduceArgMin = String -> (Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String -> (Expr -> Maybe Expr) -> RewriteRule m
simpleRewriteRule String
"reduceArgMin" ((Expr -> Maybe Expr) -> RewriteRule m)
-> (Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \case
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
reduceArgMax :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceArgMax :: RewriteRule m
reduceArgMax = String -> (Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
String -> (Expr -> Maybe Expr) -> RewriteRule m
simpleRewriteRule String
"reduceArgMax" ((Expr -> Maybe Expr) -> RewriteRule m)
-> (Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \case
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 :: (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
reduceMin,
RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceMax,
RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceArgMin,
RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error 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 :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
rule
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 ()
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