-
Notifications
You must be signed in to change notification settings - Fork 0
/
order.dats
34 lines (26 loc) · 1.22 KB
/
order.dats
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
#define ATS_DYNLOADFLAG 0
#include "share/atspre_staload.hats"
staload "symintr.sats"
staload "order.sats"
implement {a} order_compare (x, y) = gcompare_val_val<a> (x, y)
typedef nat = intGte 0
implement order_compare<nat> (x, y) = g0ofg1 x - g0ofg1 y
implement {a} order_compare_addr (x, y) = ($UNSAFE.cast{int} x) - ($UNSAFE.cast{int} y)
implement (a:t@ype,b:t@ype) order_compare<@(a,b)> (x, y) =
if cmp<a> (x.0, y.0) != 0
then cmp<a> (x.0, y.0)
else cmp<b> (x.1, y.1)
implement (a:t@ype,b:t@ype,c:t@ype) order_compare<@(a,b,c)> (x, y) =
if cmp<a> (x.0, y.0) != 0
then cmp<a> (x.0, y.0)
else if cmp<b> (x.1, y.1) != 0
then cmp<b> (x.1, y.1)
else cmp<c> (x.2, y.2)
implement {a} order_eq (x, y) = order_compare<a> (x, y) = 0
implement {a} order_neq (x, y) = order_compare<a> (x, y) != 0
implement {a} order_gt (x, y) = order_compare<a> (x, y) > 0
implement {a} order_lt (x, y) = order_compare<a> (x, y) < 0
implement {a} order_gte (x, y) = order_compare<a> (x, y) >= 0
implement {a} order_lte (x, y) = order_compare<a> (x, y) <= 0
implement {a} order_min (x, y) = if x \order_lte<a> y then x else y
implement {a} order_max (x, y) = if x \order_gte<a> y then x else y