import CHR

----------------------------------------------------------------------------------
-- CHR definition of less-than-or-equal constraint

leq    = C_a_a "leq"

reflexivity  = leq x y <=> x .=. y |> true        where x,y free
antisymmetry = leq x y /\ leq y x <=> x .=. y     where x,y free
idempotence  = leq x y \\ leq x y <=> true        where x,y free
transitivity = leq x y /\ leq y z ==> leq x z     where x,y,z free

leqint       = leq x y <=> x .<=. y |> true       where x,y free

-- Compile the "classical" rules:
main = compileCHR "Leq" [reflexivity,antisymmetry,idempotence,transitivity]

-- If one compiles these rules (including rule leqint), then a CHR solver
-- for the leq constraint over integers is generated:
maini = compileCHR "Leq" [reflexivity,antisymmetry,idempotence,transitivity,leqint]