Test.Speculate.Expr.Ground

This module is part of Speculate.

Generate and evaluate ground values of expressions.

Documentation

grounds :: (Expr -> [[Expr]]) -> Expr -> [Expr]

List all possible valuations of an expression (potentially infinite). In pseudo-Haskell:

take 3 $ grounds (lookupTiers preludeInstances) ((x + x) + y)
  == [(0 + 0) + 0, (0 + 0) + 1, (1 + 1) + 0]

Note this function will return an empty list when a Listable instance is not found in the Instances list.

groundBinds :: (Expr -> [[Expr]]) -> Expr -> [Binds]

List all possible variable bindings to an expression

take 3 $ groundBinds (lookupTiers preludeInstances) ((x + x) + y)
  == [ [("x",0),("y",0)]
     , [("x",0),("y",1)]
     , [("x",1),("y",0)] ]

equal :: Instances -> Int -> Expr -> Expr -> Bool

Are two expressions equal for a given number of tests?

lessOrEqual :: Instances -> Int -> Expr -> Expr -> Bool

Are two expressions less-than-or-equal for a given number of tests?

less :: Instances -> Int -> Expr -> Expr -> Bool

Are two expressions less-than for a given number of tests?

inequal :: Instances -> Int -> Expr -> Expr -> Bool

Are two expressions inequal for *all* variable assignments? Note this is different than not . equal.

isTrue :: (Expr -> [Expr]) -> Expr -> Bool

Is a boolean expression true for all variable assignments?

isFalse :: (Expr -> [Expr]) -> Expr -> Bool

Is an expression ALWAYS false? This is *NOT* the same as not true.

condEqual :: Instances -> Int -> Expr -> Expr -> Expr -> Bool

Are two expressions equal under a given condition for a given number of tests?

condEqualM :: Instances -> Int -> Int -> Expr -> Expr -> Expr -> Bool

Are two expressions equal under a given condition for a given number of tests and a minimum amount of tests

trueRatio :: Instances -> Int -> Expr -> Ratio Int

Under a maximum number of tests, returns the ratio for which an expression holds true.

constify :: Expr -> Expr

O(n). Turn all variables in an expression into fake constants.

> vars (xx -+- yy)
[x :: Int, y :: Int]

> constify (xx -+- yy)
x + y :: Int

> vars (constify (xx -+- yy))
[]

constifications :: Expr -> [Expr]

O(n). Returns a list with all possible permutations of variables in the given expression, all constifyed into fake constants.

> constifications (xx -+- yy)
[ x + y :: Int
, y + x :: Int ]

> constifications (xx -:- xxs)
[ x:xs :: [Int] ]

Types are respected.

This is useful for checking ground-joinability in term rewriting.