speculate-0.2.9: discovery of properties about Haskell functions

Copyright(c) 2016-2017 Rudy Matela
License3-Clause BSD (see the file LICENSE)
MaintainerRudy Matela <rudy@matela.com.br>
Safe HaskellNone
LanguageHaskell2010

Test.Speculate.Reason.Order

Description

This module is part o Speculate.

Orders for term rewriting and completion.

Synopsis

Documentation

(|>|) :: Expr -> Expr -> Bool infix 4 Source #

Strict order between expressions as defined in TRAAT p103.

s > t iff |s| > |t| and , for all x in V, |s|_x > |t|_x

This is perhaps the simplest order that can be used with KBC.

(>|) :: Expr -> Expr -> Bool infix 4 Source #

Strict order between expressions loosely as defined in TRAAT p124 (KBO)

Reversed K >| for Knuth, sorry Bendix.

(|>) :: Expr -> Expr -> Bool infix 4 Source #

kboBy :: (Expr -> Int) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool Source #

dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool Source #

Dershowitz reduction order as defined in TRAAT

|> a D for Dershowitz

weight :: Expr -> Int Source #

Weight function for kboBy:

  • Variables weigh 1
  • Nullary functions weigh 1 (a.k.a. constants)
  • N-ary functions weigh 0
  • Unary functions weigh 1

This is the weight when using >|.

weightExcept :: Expr -> Expr -> Int Source #

Weight function for kboBy:

  • Variables weigh 1
  • Nullary functions weigh 1 (a.k.a. constants)
  • N-ary functions weigh 0
  • Unary functions weigh 1 except for the one given as argument

gtExcept :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool Source #

To be used alongside weightExcept