Module CHR

A representation of CHR rules in Curry, an interpreter for CHR rules based on the refined operational semantics of Duck et al. (ICLP 2004), and a compiler into CHR(Prolog).

To use CHR(Curry), specify the CHR(Curry) rules in a Curry program, load it, add module CHR and interpret or compile the rules with runCHR or compileCHR, respectively. This can be done in one shot with

> pakcs :l MyRules :add CHR :eval 'compileCHR "MyCHR" [rule1,rule2]' :q

Author: Michael Hanus

Version: May 2017

Summary of exported operations:

(<=>) :: Goal a b -> Goal a b -> CHR a b   
Simplification rule.
(==>) :: Goal a b -> Goal a b -> CHR a b   
Propagation rule.
(\\) :: Goal a b -> CHR a b -> CHR a b   
Simpagation rule: if rule is applicable, the first constraint is kept and the second constraint is deleted.
(|>) :: CHR a b -> Goal a b -> CHR a b   
A rule with a guard.
(/\) :: Goal a b -> Goal a b -> Goal a b   
Conjunction of CHR goals.
true :: Goal a b   
The always satisfiable CHR constraint.
fail :: Goal a b   
The always failing constraint.
andCHR :: [Goal a b] -> Goal a b   
Join a list of CHR goals into a single CHR goal (by conjunction).
allCHR :: (a -> Goal b c) -> [a] -> Goal b c   
Is a given constraint abstraction satisfied by all elements in a list?
chrsToGoal :: [a] -> Goal b a   
Transforms a list of CHR constraints into a CHR goal.
toGoal1 :: (a -> b) -> a -> Goal c b   
Transform unary CHR constraint into a CHR goal.
toGoal2 :: (a -> b -> c) -> a -> b -> Goal d c   
Transforms binary CHR constraint into a CHR goal.
toGoal3 :: (a -> b -> c -> d) -> a -> b -> c -> Goal e d   
Transforms a ternary CHR constraint into a CHR goal.
toGoal4 :: (a -> b -> c -> d -> e) -> a -> b -> c -> d -> Goal f e   
Transforms a CHR constraint of arity 4 into a CHR goal.
toGoal5 :: (a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> Goal g f   
Transforms a CHR constraint of arity 5 into a CHR goal.
toGoal6 :: (a -> b -> c -> d -> e -> f -> g) -> a -> b -> c -> d -> e -> f -> Goal h g   
Transforms a CHR constraint of arity 6 into a CHR goal.
(.=.) :: a -> a -> Goal a b   
Primitive syntactic equality on arbitrary terms.
(./=.) :: a -> a -> Goal a b   
Primitive syntactic disequality on ground(!) terms.
(.<=.) :: a -> a -> Goal a b   
Primitive less-or-equal constraint.
(.>=.) :: a -> a -> Goal a b   
Primitive greater-or-equal constraint.
(.<.) :: a -> a -> Goal a b   
Primitive less-than constraint.
(.>.) :: a -> a -> Goal a b   
Primitive greater-than constraint.
ground :: a -> Goal a b   
Primitive groundness constraint (useful for guards).
nonvar :: a -> Goal a b   
Primitive nonvar constraint (useful for guards).
anyPrim :: (() -> Bool) -> Goal a b   
Embed user-defined primitive constraint.
solveCHR :: [[a] -> CHR a b] -> Goal a b -> Bool   
Interpret CHR rules (parameterized over domain variables) for a given CHR goal (second argument) and embed this as a constraint solver in Curry.
runCHR :: [[a] -> CHR a b] -> Goal a b -> [b]   
Interpret CHR rules (parameterized over domain variables) for a given CHR goal (second argument) and return the remaining CHR constraints.
runCHRwithTrace :: [[a] -> CHR a b] -> Goal a b -> [b]   
Interpret CHR rules (parameterized over domain variables) for a given CHR goal (second argument) and return the remaining CHR constraints.
compileCHR :: String -> [[a] -> CHR a b] -> IO ()   
Compile a list of CHR(Curry) rules into CHR(Prolog) and store its interface in a Curry program (name given as first argument).
chr2curry :: Goal a b -> Bool   
Transforms a primitive CHR constraint into a Curry constraint.

Exported datatypes:


CHR

The basic data type of Constraint Handling Rules.

Constructors:


Goal

A CHR goal is a list of CHR constraints (primitive or user-defined).

Constructors:


Exported operations:

(<=>) :: Goal a b -> Goal a b -> CHR a b   

Simplification rule.

Further infos:
  • defined as non-associative infix operator with precedence 3

(==>) :: Goal a b -> Goal a b -> CHR a b   

Propagation rule.

Further infos:
  • defined as non-associative infix operator with precedence 3

(\\) :: Goal a b -> CHR a b -> CHR a b   

Simpagation rule: if rule is applicable, the first constraint is kept and the second constraint is deleted.

Further infos:
  • defined as non-associative infix operator with precedence 2
  • partially defined

(|>) :: CHR a b -> Goal a b -> CHR a b   

A rule with a guard.

Further infos:
  • defined as non-associative infix operator with precedence 1

(/\) :: Goal a b -> Goal a b -> Goal a b   

Conjunction of CHR goals.

Further infos:
  • defined as right-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

true :: Goal a b   

The always satisfiable CHR constraint.

Further infos:
  • solution complete, i.e., able to compute all solutions

fail :: Goal a b   

The always failing constraint.

Further infos:
  • solution complete, i.e., able to compute all solutions

andCHR :: [Goal a b] -> Goal a b   

Join a list of CHR goals into a single CHR goal (by conjunction).

allCHR :: (a -> Goal b c) -> [a] -> Goal b c   

Is a given constraint abstraction satisfied by all elements in a list?

chrsToGoal :: [a] -> Goal b a   

Transforms a list of CHR constraints into a CHR goal.

toGoal1 :: (a -> b) -> a -> Goal c b   

Transform unary CHR constraint into a CHR goal.

toGoal2 :: (a -> b -> c) -> a -> b -> Goal d c   

Transforms binary CHR constraint into a CHR goal.

toGoal3 :: (a -> b -> c -> d) -> a -> b -> c -> Goal e d   

Transforms a ternary CHR constraint into a CHR goal.

toGoal4 :: (a -> b -> c -> d -> e) -> a -> b -> c -> d -> Goal f e   

Transforms a CHR constraint of arity 4 into a CHR goal.

toGoal5 :: (a -> b -> c -> d -> e -> f) -> a -> b -> c -> d -> e -> Goal g f   

Transforms a CHR constraint of arity 5 into a CHR goal.

toGoal6 :: (a -> b -> c -> d -> e -> f -> g) -> a -> b -> c -> d -> e -> f -> Goal h g   

Transforms a CHR constraint of arity 6 into a CHR goal.

(.=.) :: a -> a -> Goal a b   

Primitive syntactic equality on arbitrary terms.

Further infos:
  • defined as non-associative infix operator with precedence 5
  • solution complete, i.e., able to compute all solutions

(./=.) :: a -> a -> Goal a b   

Primitive syntactic disequality on ground(!) terms.

Further infos:
  • defined as non-associative infix operator with precedence 5
  • solution complete, i.e., able to compute all solutions

(.<=.) :: a -> a -> Goal a b   

Primitive less-or-equal constraint.

Further infos:
  • defined as non-associative infix operator with precedence 5

(.>=.) :: a -> a -> Goal a b   

Primitive greater-or-equal constraint.

Further infos:
  • defined as non-associative infix operator with precedence 5

(.<.) :: a -> a -> Goal a b   

Primitive less-than constraint.

Further infos:
  • defined as non-associative infix operator with precedence 5

(.>.) :: a -> a -> Goal a b   

Primitive greater-than constraint.

Further infos:
  • defined as non-associative infix operator with precedence 5

ground :: a -> Goal a b   

Primitive groundness constraint (useful for guards).

Further infos:
  • solution complete, i.e., able to compute all solutions

nonvar :: a -> Goal a b   

Primitive nonvar constraint (useful for guards).

Further infos:
  • solution complete, i.e., able to compute all solutions

anyPrim :: (() -> Bool) -> Goal a b   

Embed user-defined primitive constraint.

Further infos:
  • solution complete, i.e., able to compute all solutions

solveCHR :: [[a] -> CHR a b] -> Goal a b -> Bool   

Interpret CHR rules (parameterized over domain variables) for a given CHR goal (second argument) and embed this as a constraint solver in Curry. If user-defined CHR constraints remain after applying all CHR rules, a warning showing the residual constraints is issued.

runCHR :: [[a] -> CHR a b] -> Goal a b -> [b]   

Interpret CHR rules (parameterized over domain variables) for a given CHR goal (second argument) and return the remaining CHR constraints.

runCHRwithTrace :: [[a] -> CHR a b] -> Goal a b -> [b]   

Interpret CHR rules (parameterized over domain variables) for a given CHR goal (second argument) and return the remaining CHR constraints. Trace also the active and passive constraints as well as the applied rule number during computation.

compileCHR :: String -> [[a] -> CHR a b] -> IO ()   

Compile a list of CHR(Curry) rules into CHR(Prolog) and store its interface in a Curry program (name given as first argument).

chr2curry :: Goal a b -> Bool   

Transforms a primitive CHR constraint into a Curry constraint. Used in the generated CHR(Prolog) code to evaluated primitive constraints.