{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ViewPatterns #-}
module Jikka.Core.Convert.CloseSum
( run,
rule,
reduceSum,
reduceProduct,
reduceModSum,
reduceModProduct,
)
where
import Jikka.Common.Alpha
import Jikka.Common.Error
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
reduceSum :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceSum :: RewriteRule m
reduceSum =
[RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
[
[r| "sum/nil" sum nil = 0 |],
[r| "sum/cons" forall x xs. sum (cons x xs) = x + sum xs |],
[r| "sum/range" forall n. sum (range n) = n * (n - 1) /! 2 |],
[r| "sum/reversed" forall xs. sum (reversed xs) = sum xs |],
[r| "sum/sorted" forall xs. sum (sorted xs) = sum xs |],
[r| "sum/filter/map" forall g f xs. sum (filter g (map f xs)) = sum (map (fun x -> if g (f x) then f x else 0) xs) |],
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule [Char]
"sum/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
Sum' (Map' Type
_ Type
_ (LamConst Type
t Expr
e) Expr
xs) -> 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
Mult' (Type -> Expr -> Expr
Len' Type
t Expr
xs) 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| "sum/map/id" forall n. sum (map (fun x -> x) (range n)) = n * (n - 1) /! 2 |],
[r| "sum/map/pow/2" forall n. sum (map (fun x -> x ** 2) (range n)) = n * (n - 1) * (2 * n - 1) /! 6 |],
[r| "sum/map/pow/2'" forall n. sum (map (fun x -> x * x) (range n)) = n * (n - 1) * (2 * n - 1) /! 6 |],
[r| "sum/map/negate" forall e xs. sum (map (fun x -> - e) xs) = - sum (map (fun x -> e) xs) |],
[r| "sum/map/plus" forall e1 e2 xs. sum (map (fun x -> e1 + e2) xs) = sum (map (fun x -> e1) xs) + sum (map (fun x -> e2) xs) |],
[r| "sum/map/minus" forall e1 e2 xs. sum (map (fun x -> e1 - e2) xs) = sum (map (fun x -> e1) xs) - sum (map (fun x -> e2) xs) |],
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule [Char]
"sum/map/mult" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Sum' (Map' Type
t1 Type
t2 (Lam VarName
x Type
t (Mult' 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
Mult' Expr
k (Expr -> Expr
Sum' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t 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,
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule [Char]
"sum/map/mult'" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
Sum' (Map' Type
t1 Type
t2 (Lam VarName
x Type
t (Mult' 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
Mult' Expr
k (Expr -> Expr
Sum' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t 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
]
reduceProduct :: Monad m => RewriteRule m
reduceProduct :: RewriteRule m
reduceProduct = [Char] -> (Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
[Char] -> (Expr -> Maybe Expr) -> RewriteRule m
simpleRewriteRule [Char]
"reduceProduct" ((Expr -> Maybe Expr) -> RewriteRule m)
-> (Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \case
Product' Expr
xs -> case Expr
xs of
Nil' Type
_ -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
Lit1
Cons' Type
_ Expr
x 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
Mult' Expr
x (Expr -> Expr
Product' Expr
xs)
Range1' Expr
n -> 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
IntTy (Type -> Expr -> Expr -> Expr
Equal' Type
IntTy Expr
n Expr
Lit0) Expr
Lit1 Expr
Lit0
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
Product' Expr
xs
Sorted' 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
Product' Expr
xs
Map' Type
t1 Type
_ (Lam VarName
x Type
_ 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
Pow' Expr
e (Type -> Expr -> Expr
Len' Type
t1 Expr
xs)
Map' Type
t1 Type
t2 (Lam VarName
x Type
t (Negate' Expr
e)) 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
Mult' (Expr -> Expr -> Expr
Pow' (Expr -> Expr
Negate' Expr
Lit0) (Type -> Expr -> Expr
Len' Type
t1 Expr
xs)) (Expr -> Expr
Product' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e) Expr
xs))
Map' Type
t1 Type
t2 (Lam VarName
x Type
t (Mult' Expr
e1 Expr
e2)) 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
Mult' (Expr -> Expr
Product' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e1) Expr
xs)) (Expr -> Expr
Product' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e2) Expr
xs))
Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing
Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing
reduceModSum :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceModSum :: RewriteRule m
reduceModSum =
[RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
[
[r| "modsum/1" forall xs. modsum xs 1 = 0 |],
[r| "modsum/nil" forall m. modsum nil m = 0 |],
[r| "modsum/cons" forall m x xs. modsum (cons x xs) m = modplus x (sum xs) m |],
[r| "modsum/range" forall m n. modsum (range n) m = (n * (n - 1) /! 2) % m |],
[r| "modsum/reversed" forall m xs. modsum (reversed xs) m = modsum xs m |],
[r| "modsum/sorted" forall m xs. modsum (sorted xs) m = modsum xs m |],
[r| "modsum/filter/map" forall m g f xs. modsum (filter g (map f xs)) m = modsum (map (fun x -> if g (f x) then f x else 0) xs) m |],
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule [Char]
"modsum/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
ModSum' (Map' Type
_ Type
_ (LamConst Type
t Expr
e) Expr
xs) Expr
m -> 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 -> Expr
ModMult' (Type -> Expr -> Expr
Len' Type
t Expr
xs) Expr
e Expr
m
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule [Char]
"modsum/map/floormod/const" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
ModSum' (Map' Type
_ Type
_ (LamConst Type
t (FloorMod' Expr
e Expr
m')) Expr
xs) Expr
m | Expr
m' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
m -> 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 -> Expr
ModMult' (Type -> Expr -> Expr
Len' Type
t Expr
xs) Expr
e Expr
m
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
[r| "modsum/map/id" forall m n. modsum (map (fun x -> x) (range n)) m = n * (n - 1) /! 2 % m |],
[r| "modsum/map/floormod/id" forall m n. modsum (map (fun x -> x % m) (range n)) m = n * (n - 1) /! 2 % m |],
[r| "modsum/map/modpow/2" forall m n. modsum (map (fun x -> modpow x 2 m) (range n)) m = n * (n - 1) * (2 * n - 1) /! 6 % m |],
[r| "modsum/map/modpow/2'" forall m n. modsum (map (fun x -> modmult x x m) (range n)) m = n * (n - 1) * (2 * n - 1) /! 6 % m |],
[r| "modsum/map/modnegate" forall m e xs. modsum (map (fun x -> modnegate e m) xs) m = modnegate (modsum (map (fun x -> e) xs) m) m |],
[r| "modsum/map/modplus" forall m e1 e2 xs. modsum (map (fun x -> modplus e1 e2 m) xs) m = modplus (modsum (map (fun x -> e1) xs) m) (modsum (map (fun x -> e2) xs) m) m |],
[r| "modsum/map/modminus" forall m e1 e2 xs. modsum (map (fun x -> modminus e1 e2 m) xs) m = modminus (modsum (map (fun x -> e1) xs) m) (modsum (map (fun x -> e2) xs) m) m |],
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule [Char]
"modsum/map/modmult" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
ModSum' (Map' Type
t1 Type
t2 (Lam VarName
x Type
t (ModMult' Expr
k Expr
e Expr
m')) Expr
xs) Expr
m | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k Bool -> Bool -> Bool
&& Expr
m' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
m -> 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 -> Expr
ModMult' Expr
k (Expr -> Expr -> Expr
ModSum' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e) Expr
xs) Expr
m) Expr
m
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing,
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
[Char]
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
makeRewriteRule [Char]
"modsum/map/modmult'" ((RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m)
-> (RewriteEnvironment -> Expr -> m (Maybe Expr)) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \RewriteEnvironment
_ -> \case
ModSum' (Map' Type
t1 Type
t2 (Lam VarName
x Type
t (ModMult' Expr
e Expr
k Expr
m')) Expr
xs) Expr
m | VarName
x VarName -> Expr -> Bool
`isUnusedVar` Expr
k Bool -> Bool -> Bool
&& Expr
m' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
m -> 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 -> Expr
ModMult' Expr
k (Expr -> Expr -> Expr
ModSum' (Type -> Type -> Expr -> Expr -> Expr
Map' Type
t1 Type
t2 (VarName -> Type -> Expr -> Expr
Lam VarName
x Type
t Expr
e) Expr
xs) Expr
m) Expr
m
Expr
_ -> Maybe Expr -> m (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing
]
reduceModProduct :: Monad m => RewriteRule m
reduceModProduct :: RewriteRule m
reduceModProduct = [Char] -> (Expr -> Maybe Expr) -> RewriteRule m
forall (m :: * -> *).
Monad m =>
[Char] -> (Expr -> Maybe Expr) -> RewriteRule m
simpleRewriteRule [Char]
"reduceModProduct" ((Expr -> Maybe Expr) -> RewriteRule m)
-> (Expr -> Maybe Expr) -> RewriteRule m
forall a b. (a -> b) -> a -> b
$ \case
ModProduct' Expr
xs Expr
m -> case Expr
xs of
Expr
_ | Expr
m Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
Lit1 -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
Lit0
Nil' Type
_ -> 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
FloorMod' Expr
Lit1 Expr
m
Cons' Type
_ Expr
x 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 -> Expr
ModMult' Expr
x (Expr -> Expr -> Expr
ModProduct' Expr
xs Expr
m) Expr
m
Range1' Expr
n -> 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
IntTy (Type -> Expr -> Expr -> Expr
Equal' Type
IntTy Expr
n Expr
Lit0) (Expr -> Expr -> Expr
FloorMod' Expr
Lit1 Expr
m) Expr
Lit0
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
ModProduct' Expr
xs Expr
m
Sorted' 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
ModProduct' Expr
xs Expr
m
Expr
_ -> Maybe Expr
forall a. Maybe a
Nothing
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
reduceSum,
RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
reduceProduct,
RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error m) =>
RewriteRule m
reduceModSum,
RewriteRule m
forall (m :: * -> *). Monad m => RewriteRule m
reduceModProduct
]
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 = [Char] -> m Program -> m Program
forall (m :: * -> *) a. MonadError Error m => [Char] -> m a -> m a
wrapError' [Char]
"Jikka.Core.Convert.CloseSum" (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