speculate-0.4.20: discovery of properties about Haskell functions
Copyright(c) 2016-2024 Rudy Matela
License3-Clause BSD (see the file LICENSE)
MaintainerRudy Matela <rudy@matela.com.br>
Safe HaskellSafe-Inferred
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

This is not a simplification order on funny Exprs.

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

funny :: Expr -> Bool Source #

Returns True when an Expression has either a functional type or functional variables.

funny xx        =  False
funny one       =  False
funny idE       =  True
funny (ff one)  =  True

serious :: Expr -> Bool Source #

Returns True when an Expression has no functional return type and no functional variables.

serious xx        =  True
serious one       =  True
serious idE       =  False
serious (ff one)  =  False