Jikka.Core.Convert.EqualitySolving

\[ \newcommand\int{\mathbf{int}} \newcommand\bool{\mathbf{bool}} \newcommand\list{\mathbf{list}} \]

Documentation

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

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

internal rules

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

moveLiteralToRight moves literals to lhs of (==) or (/=), using symmetricity.

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

convertGreaterToLess erases (>) and (>=).

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

reduceReflexivity uses reflexivity.

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

makeRightZero makes RHS of integer equality/inequality zero with subtracting RHS from both sides.

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

reduceIntInjective removes injective functions from equalities of integers.

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

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

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