1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170

------------------------------------------------------------------------------
--- Library for constraint programming with arithmetic constraints over reals.
---
--- @author Michael Hanus
--- @version July 2023
------------------------------------------------------------------------------

module CLP.R(CFloat, minimumFor, minimize, maximumFor, maximize) where

-- The operator declarations are similar to the standard arithmetic operators.

infixl 7 *., /.
infixl 6 +., -.
infix  4 <., >., <=., >=.

--- Abstract type to represent floats used in constraints.
data CFloat = CF Float

instance Eq CFloat where
  (CF f1) == (CF f2) = f1 == f2

instance Ord CFloat where
  compare (CF f1) (CF f2) = compare f1 f2
  x < y = x <. y
  x > y = x >. y
  x <= y = x <=. y
  x >= y = x >=. y

instance Show CFloat where
  show (CF f) = show f

instance Num CFloat where
  x + y = x +. y
  x - y = x -. y
  x * y = x *. y

  negate (CF x) = CF (negate x)

  abs x | x >= 0 = x
        | otherwise = negate x


  signum x | x > 0     = 1
           | x == 0    = 0
           | otherwise = -1

  fromInt x = i2f x

instance Fractional CFloat where
  x / y = x /. y

  fromFloat x = CF x

--- The `Real` instance of `CFloat` provides the conversion operation `toFloat`.
instance Real CFloat where
  toFloat (CF x) = x

--- Addition on floats in arithmetic constraints.

(+.)   :: CFloat -> CFloat -> CFloat
(CF x) +. (CF y) = CF ((prim_CLPR_plus $! y) $! x)

prim_CLPR_plus :: Float -> Float -> Float
prim_CLPR_plus external

--- Subtraction on floats in arithmetic constraints.

(-.)   :: CFloat -> CFloat -> CFloat
(CF x) -. (CF y) = CF ((prim_CLPR_minus $! y) $! x)

prim_CLPR_minus :: Float -> Float -> Float
prim_CLPR_minus external

--- Multiplication on floats in arithmetic constraints.

(*.)   :: CFloat -> CFloat -> CFloat
(CF x) *. (CF y) = CF ((prim_CLPR_times $! y) $! x)

prim_CLPR_times :: Float -> Float -> Float
prim_CLPR_times external

--- Division on floats in arithmetic constraints.

(/.)   :: CFloat -> CFloat -> CFloat
(CF x) /. (CF y)  = CF ((prim_CLPR_div $! y) $! x)

prim_CLPR_div :: Float -> Float -> Float
prim_CLPR_div external

--- "Less than" constraint on floats.

(<.)   :: CFloat -> CFloat -> Bool
(CF x) <. (CF y) = (prim_CLPR_le $! y) $! x

prim_CLPR_le :: Float -> Float -> Bool
prim_CLPR_le external

--- "Greater than" constraint on floats.

(>.)   :: CFloat -> CFloat -> Bool
(CF x) >. (CF y) = (prim_CLPR_ge $! y) $! x

prim_CLPR_ge :: Float -> Float -> Bool
prim_CLPR_ge external

--- "Less than or equal" constraint on floats.

(<=.)  :: CFloat -> CFloat -> Bool
(CF x) <=. (CF y) = (prim_CLPR_leq $! y) $! x

prim_CLPR_leq :: Float -> Float -> Bool
prim_CLPR_leq external

--- "Greater than or equal" constraint on floats.

(>=.)  :: CFloat -> CFloat -> Bool
(CF x) >=. (CF y) = (prim_CLPR_geq $! y) $! x

prim_CLPR_geq :: Float -> Float -> Bool
prim_CLPR_geq external

--- Conversion function from integers to floats.
--- Rigid in the first argument, i.e., suspends until the first argument
--- is ground.

i2f    :: Int -> CFloat
i2f x = CF (prim_CLPR_i2f $# x)

prim_CLPR_i2f :: Int -> Float
prim_CLPR_i2f external


--- Computes the minimum with respect to a given constraint.
--- (minimumFor g f) evaluates to x if (g x) is satisfied and
--- (f x) is minimal. The evaluation fails if such a minimal value
--- does not exist. The evaluation suspends if it contains
--- unbound non-local variables.
minimumFor :: (a -> Bool) -> (a -> CFloat) -> a
minimumFor g f = prim_minimumFor g (toFloat . f)

prim_minimumFor :: (a -> Bool) -> (a -> Float) -> a
prim_minimumFor external

--- Minimization constraint.
--- (minimize g f x) is satisfied if (g x) is satisfied and
--- (f x) is minimal. The evaluation suspends if it contains
--- unbound non-local variables.
minimize :: Data a => (a -> Bool) -> (a -> CFloat) -> a -> Bool
minimize g f x = minimumFor g f =:= x

--- Computes the maximum with respect to a given constraint.
--- (maximumFor g f) evaluates to x if (g x) is satisfied and
--- (f x) is maximal. The evaluation fails if such a maximal value
--- does not exist. The evaluation suspends if it contains
--- unbound non-local variables.
maximumFor :: (a -> Bool) -> (a -> CFloat) -> a
maximumFor g f = prim_maximumFor g (toFloat . f)

prim_maximumFor :: (a -> Bool) -> (a -> Float) -> a
prim_maximumFor external

--- Maximization constraint.
--- (maximize g f x) is satisfied if (g x) is satisfied and
--- (f x) is maximal. The evaluation suspends if it contains
--- unbound non-local variables.
maximize :: Data a => (a -> Bool) -> (a -> CFloat) -> a -> Bool
maximize g f x = maximumFor g f =:= x


-- end of CLP.R