type/satisfies - Maple Programming Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : Programming : Data Types : Type Checking : Types : type/satisfies

type/satisfies

embed a predicate as a structured type

 

Calling Sequence

Parameters

Description

Examples

Calling Sequence

type(expr, 'satisfies'(P1, P2, ... ))

Parameters

expr

-

Maple expression

P1, P2, ...

-

predicates

Description

• 

The type satisfies provides a mechanism for embedding arbitrary predicates in Maple's type system. It enables you to define a structured type corresponding to an arbitrary predicate without having to pollute the type namespace. This is helpful when used in conjunction with the few Maple facilities (such as the two-argument form of indets) that accept types, but not arbitrary predicates.

• 

An expression expr is of type satisfies(P1, P2, ...) if all Pk(expr) evaluate to true, or to And, Or, Xor, Implies, Not constructions that, when converted to their corresponding boolean operators (and, or, xor, implies, not; see convert/boolean_operator), evaluate to true. Also all Pk(expr) are expected to evaluate to either true or false, or to And, Or, Xor, Implies, Not constructions with those meanings.

• 

Type satisfies is always used as a structured type with at least one parameter. The function type(expr, 'satisfies'(P)) evaluates to true if the expression expr satisfies the predicate P. More than one predicate P1, P2, ... can be supplied, in which case the expression expr must satisfy all of the predicates P1, P2, ....

• 

Type satisfies evaluates the Pk(expr) in the order supplied until an expression evaluates to false. Then the type(expr, 'satisfies'(P1, P2, ...) call returns false. If no predicate returns false, then the value true is returned.

• 

Predicates are expected to return normally, without raising exceptions. You can use the ordered evaluation of the predicates to test that any preconditions for error-free evaluations are met. See Example 3.

Examples

Example 1

  

Use this type to filter conditions when computing objects of certain type:

  

All the functions

indetsFGx,y,zHx,'function'

FGx,y,z,Gx,y,Hx

(1)
  

Only the functions having y

indetsFGx,y,zHx,'Andfunction,satisfiesf→hasf,y'

FGx,y,z,Gx,y

(2)
  

Only the functions having y and not having z

indetsFGx,y,zHx,'Andfunction,satisfiesf→hasf,yandnothasf,z'

Gx,y

(3)

Example 2

  

Use this mechanism to introduce local types within module or procedure bodies. Note that NumberTheory[IsSquareFree] returns true or false when applied to some arguments

mmoduleexportsqrfree;sqrfree'satisfies'x→typex,'odd',NumberTheory['IsSquareFree']end module:

  

Observe that, unlike global type names, which should always be quoted to protect against unwanted evaluation, a local type defined in this way must not be quoted.

  

For example, the following example cannot have quotes, that is, 'm:sqrfree'.

type7,m:-sqrfree

true

(4)
  

The global space of names (including the global name sqrfree) remains distinct and so the definition of type m:-sqrfree does not imply the existence of a sqrfree type

type7,sqrfree

Error, type `sqrfree` does not exist

Example 3

  

Giving predicates in certain order, they are evaluated in that order

maptype,0,1,2,'And''integer','satisfies's→evalbs0,s→type1s,'integer'

false,true,false

(5)
  

While constructing predicates (the procedures testing whether a condition is satisfied), the condition being tester may lead to an error, for example, because the test produces a division by zero.

maptype,0,1,2,'And''integer','satisfies's→type1s,'integer'

Error, (in unknown) numeric exception: division by zero

  

You can prevent these situations adding more predicates, taking care of the exceptional cases before the predicate which returns an error is considered

maptype,0,1,2,'And''integer','satisfies's→iss0,s→type1s,'integer'

false,true,false

(6)
  

You can use And, Or, Xor, Implies, Not constructions to make them more readable or to have full control of the evaluation rules when constructing your types - these constructions do not automatically evaluate to true or false.

conditionf→Andtypef,function,Nothastypefⅇ,function

conditionftypef,function¬hastypefⅇ,function

(7)

typeⅇ2,satisfiescondition

false

(8)

typeⅇ,satisfiescondition

true

(9)

See Also

convert/boolean_operator

evalb

export

has

indets

map

module

NumberTheory[IsSquareFree]

rcurry

sqrfree

type

type/structure