Jikka.Core.Convert.CloseAll

Documentation

run :: (MonadAlpha m, MonadError Error m) => Program -> m Program

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)\)

internal rules

rule :: (MonadAlpha m, MonadError Error m) => RewriteRule m

reduceAll :: (MonadAlpha m, MonadError Error m) => RewriteRule m

reduceAny :: (MonadAlpha m, MonadError Error m) => RewriteRule m