{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ViewPatterns #-}
module Jikka.Core.Convert.CloseAll
( run,
rule,
reduceAll,
reduceAny,
)
where
import Jikka.Common.Alpha
import Jikka.Common.Error
import Jikka.Core.Language.Expr
import Jikka.Core.Language.Lint
import Jikka.Core.Language.QuasiRules
import Jikka.Core.Language.RewriteRules
reduceAll :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceAll :: RewriteRule m
reduceAll =
[RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
[
[r| "all/nil" all nil = true |],
[r| "all/cons" forall x xs. all (cons x xs) = x && all xs |],
[r| "all/reversed" forall xs. all (reversed xs) = all xs |],
[r| "all/sorted" forall xs. all (sorted xs) = all xs |],
[r| "all/filter" forall f xs. all (filter f xs) = all (map (fun x -> implies (f x) x) xs) |],
[r| "all/map/not" forall e xs. all (map (fun x -> not e) xs) = not (any (map (fun x -> e) xs)) |],
[r| "all/map/and" forall e1 e2 xs. all (map (fun x -> e1 && e2) xs) = all (map (fun x -> e1) xs) && all (map (fun x -> e2) xs) |]
]
reduceAny :: (MonadAlpha m, MonadError Error m) => RewriteRule m
reduceAny :: RewriteRule m
reduceAny =
[RewriteRule m] -> RewriteRule m
forall a. Monoid a => [a] -> a
mconcat
[
[r| "any/nil" any nil = false |],
[r| "any/cons" forall x xs. any (cons x xs) = x || any xs |],
[r| "any/reversed" forall xs. any (reversed xs) = any xs |],
[r| "any/sorted" forall xs. any (sorted xs) = any xs |],
[r| "any/filter" forall f xs. any (filter f xs) = any (map (fun x -> f x && x) xs) |],
[r| "any/map/not" forall e xs. any (map (fun x -> not e) xs) = not (all (map (fun x -> e) xs)) |],
[r| "any/map/or" forall e1 e2 xs. any (map (fun x -> e1 || e2) xs) = any (map (fun x -> e1) xs) || any (map (fun x -> e2) xs) |],
[r| "any/map/implies" forall e1 e2 xs. any (map (fun x -> implies e1 e2) xs) = any (map (fun x -> not e1) xs) || any (map (fun x -> e2) xs) |]
]
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
reduceAll,
RewriteRule m
forall (m :: * -> *).
(MonadAlpha m, MonadError Error 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, 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.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 ()
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