Jikka.Core.Language.ArithmeticExpr

Basic functions

data ArithmeticExpr

Instances

Eq ArithmeticExpr

Defined in Jikka.Core.Language.ArithmeticExpr

Methods

(==) :: ArithmeticExpr -> ArithmeticExpr -> Bool

(/=) :: ArithmeticExpr -> ArithmeticExpr -> Bool

Ord ArithmeticExpr

Defined in Jikka.Core.Language.ArithmeticExpr

Methods

compare :: ArithmeticExpr -> ArithmeticExpr -> Ordering

(<) :: ArithmeticExpr -> ArithmeticExpr -> Bool

(<=) :: ArithmeticExpr -> ArithmeticExpr -> Bool

(>) :: ArithmeticExpr -> ArithmeticExpr -> Bool

(>=) :: ArithmeticExpr -> ArithmeticExpr -> Bool

max :: ArithmeticExpr -> ArithmeticExpr -> ArithmeticExpr

min :: ArithmeticExpr -> ArithmeticExpr -> ArithmeticExpr

Show ArithmeticExpr

Defined in Jikka.Core.Language.ArithmeticExpr

Methods

showsPrec :: Int -> ArithmeticExpr -> ShowS

show :: ArithmeticExpr -> String

showList :: [ArithmeticExpr] -> ShowS

parseArithmeticExpr :: Expr -> ArithmeticExpr

parseArithmeticExpr converts a given expr to a normal form \(\sum_i \prod_j e _ {i,j})\). This assumes given exprs have the type \(\mathbf{int}\).

formatArithmeticExpr :: ArithmeticExpr -> Expr

integerArithmeticExpr :: Integer -> ArithmeticExpr

negateArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr

plusArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr -> ArithmeticExpr

minusArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr -> ArithmeticExpr

multArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr -> ArithmeticExpr

incrArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr

decrArithmeticExpr :: ArithmeticExpr -> ArithmeticExpr

sumArithmeticExpr :: [ArithmeticExpr] -> ArithmeticExpr

isZeroArithmeticExpr :: ArithmeticExpr -> Bool

isOneArithmeticExpr :: ArithmeticExpr -> Bool

isIntegerArithmeticExpr :: ArithmeticExpr -> Bool

integerFromArithmeticExpr :: ArithmeticExpr -> Maybe Integer

Advanced functions

unNPlusKPattern :: ArithmeticExpr -> Maybe (VarName, Integer)

unNPlusKPattern recognizes a pattern of \(x + k\) for a variable \(x\) and an integer constant \(k \in \mathbb{Z}\).

makeVectorFromArithmeticExpr :: Vector VarName -> ArithmeticExpr -> Maybe (Vector ArithmeticExpr, ArithmeticExpr)

makeVectorFromArithmeticExpr makes a vector \(f\) and a expr \(c\) from a given vector of variables \(x_0, x_1, \dots, x _ {n - 1}\) and a given expr \(e\) s.t. \(f\) and \(c\) don't have \(x_0, x_1, \dots, x _ {n - 1}\) as free variables and \(e = c + f \cdot (x_0, x_1, \dots, x _ {n - 1})\) holds. This assumes given variables and exprs have the type \(\mathbf{int}\).

• The returned exprs are normalized with normalizeArithmeticExpr.

makeAffineFunctionFromArithmeticExpr :: VarName -> ArithmeticExpr -> Maybe (ArithmeticExpr, ArithmeticExpr)

makeAffineFunctionFromArithmeticExpr is a specialized version of makeVectorFromArithmeticExpr. This function returns \(a, b\) for a given variable \(x\) and a given expr \(e = a x + b\) where \(a, b\) which doesn't use \(x\) free.

splitConstantFactorArithmeticExpr :: ArithmeticExpr -> (Integer, ArithmeticExpr)

splitConstantFactorArithmeticExpr finds \(k\) and \(e'\) for given \(e\) s.t. \(e = k e'\).

splitToSumArithmeticExpr :: ArithmeticExpr -> [ArithmeticExpr]