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" "MyRules" [rule1,rule2]' :q

Author: Michael Hanus

Version: July 2021

Summary of exported operations:

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

Simplification rule.

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

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

Propagation rule.

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

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

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  Deterministic 

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  Deterministic 

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  Deterministic 

The always satisfiable CHR constraint.

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

false :: Goal a b  Deterministic 

The always unsatisfiable constraint.

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

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

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

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

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

chrsToGoal :: [a] -> Goal b a  Deterministic 

Transforms a list of CHR constraints into a CHR goal.

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

Transform unary CHR constraint into a CHR goal.

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

Transforms binary CHR constraint into a CHR goal.

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

Transforms a ternary CHR constraint into a CHR goal.

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

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  Deterministic 

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  Deterministic 

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

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

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  Deterministic 

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

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

Primitive less-or-equal constraint.

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

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

Primitive greater-or-equal constraint.

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

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

Primitive less-than constraint.

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

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

Primitive greater-than constraint.

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

ground :: a -> Goal a b  Deterministic 

Primitive groundness constraint (useful for guards).

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

nonvar :: a -> Goal a b  Deterministic 

Primitive nonvar constraint (useful for guards).

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

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

Embed user-defined primitive constraint.

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

solveCHR :: (Data a, Eq a, Data b, Show b) => [[a] -> CHR a b] -> Goal a b -> Bool  Non-deterministic 

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 :: (Data a, Eq a, Data b) => [[a] -> CHR a b] -> Goal a b -> [b]  Non-deterministic 

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

runCHRwithTrace :: (Data a, Eq a, Data b) => [[a] -> CHR a b] -> Goal a b -> [b]  Non-deterministic 

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 -> String -> [[a] -> CHR a b] -> IO ()  Non-deterministic 

Compile a list of CHR(Curry) rules into CHR(Prolog) and store its interface in a Curry program (name given as first argument). The second argument is the name of the module containing the CHR(Curry) rules.

chr2curry :: (Data a, Eq a) => Goal a b -> Bool  Non-deterministic 

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