-
Notifications
You must be signed in to change notification settings - Fork 5
/
auto_coerce_mw.metta
125 lines (97 loc) · 4.77 KB
/
auto_coerce_mw.metta
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
;; Collection of functions operating on numbers
;; Define max
(: max (-> Number Number Number))
(= (max $x $y) (if (> $x $y) $x $y))
;; Define min
(: min (-> Number Number Number))
(= (min $x $y) (if (< $x $y) $x $y))
;; Clamp a number to be within a certain range
(: clamp (-> Number Number Number Number))
(= (clamp $x $l $u) (max $l (min $u $x)))
;; Define abs
(: abs (-> Number Number))
(= (abs $x) (if (< $x 0) (* -1 $x) $x))
;; Define lte
(: lte (-> Number Number Bool))
(= (lte $x $y) (or (< $x $y) (== $x $y)))
;; Define gte
(: gte (-> Number Number Bool))
(= (gte $x $y) (or (> $x $y) (== $x $y)))
;; Define approximately equal
(: approxEq (-> Number Number Number Bool))
(= (approxEq $x $y $epsilon) (lte (abs (- $x $y)) $epsilon))
;; Tests for max
!(assertEqual (max 3 5) 5) ;; Test when the second number is larger
!(assertEqual (max 7 2) 7) ;; Test when the first number is larger
!(assertEqual (max 4 4) 4) ;; Test when both numbers are equal
;; Tests for min
!(assertEqual (min 3 5) 3) ;; Test when the first number is smaller
!(assertEqual (min 7 2) 2) ;; Test when the second number is smaller
!(assertEqual (min 4 4) 4) ;; Test when both numbers are equal
;; Tests for clamp
!(assertEqual (clamp 5 0 10) 5) ;; Test when value is within the range
!(assertEqual (clamp -1 0 10) 0) ;; Test when value is below the lower bound
!(assertEqual (clamp 15 0 10) 10) ;; Test when value is above the upper bound
!(assertEqual (clamp 0 0 10) 0) ;; Test edge case at the lower bound
!(assertEqual (clamp 10 0 10) 10) ;; Test edge case at the upper bound
;; Tests for abs
!(assertEqual (abs 5) 5) ;; Test positive number
!(assertEqual (abs -5) 5) ;; Test negative number
!(assertEqual (abs 0) 0) ;; Test zero
;; Tests for lte
!(assertEqual (lte 3 5) True) ;; Test when first number is less
!(assertEqual (lte 5 5) True) ;; Test when numbers are equal
!(assertEqual (lte 7 5) False) ;; Test when first number is greater
;; Tests for gte
!(assertEqual (gte 7 5) True) ;; Test when first number is greater
!(assertEqual (gte 5 5) True) ;; Test when numbers are equal
!(assertEqual (gte 3 5) False) ;; Test when first number is less
;; Tests for approxEq
!(assertEqual (approxEq 3.0 3.1 0.1) False) ;; Test when difference exceeds epsilon
!(assertEqual (approxEq 3.0 3.05 0.1) True) ;; Test when difference is within epsilon
!(assertEqual (approxEq 3.0 3.0 0.1) True) ;; Test when numbers are exactly equal
!(assertEqual (approxEq 3.0 2.9 0.1) True) ;; Test when difference is just within epsilon
!(assertEqual (approxEq 3.0 2.8 0.1) False) ;; Test when difference is slightly beyond epsilon
;; Combined test cases
!(assertEqual (clamp (max 3 7) 0 5) 5) ;; Clamp the maximum of two numbers
!(assertEqual (clamp (min -3 2) -5 5) -3) ;; Clamp the minimum of two numbers
!(assertEqual (abs (min -3 2)) 3) ;; Absolute value of the minimum
!(assertEqual (approxEq (abs -5) 5 0) True) ;; Absolute value and approximate equality
;; Define Nat
(: Nat Type)
(: Z Nat)
(: S (-> Nat Nat))
;; Define cast functions between Nat and Number
(: fromNumber (-> Number Nat))
(= (fromNumber $n) (if (<= $n 0) Z (S (fromNumber (- $n 1)))))
(: fromNat (-> Nat Number))
(= (fromNat Z) 0)
(= (fromNat (S $k)) (+ 1 (fromNat $k)))
!(pragma! coerce auto)
;; Tests for max
!(assertEqual (max (S Z) (S (S Z))) (S (S Z))) ;; max(1, 2) = 2
!(assertEqual (max (S (S Z)) Z) (S (S Z))) ;; max(2, 0) = 2
!(assertEqual (max (S Z) (S Z)) (S Z)) ;; max(1, 1) = 1
;; Tests for min
!(assertEqual (min (S Z) (S (S Z))) (S Z)) ;; min(1, 2) = 1
!(assertEqual (min (S (S Z)) Z) Z) ;; min(2, 0) = 0
!(assertEqual (min (S Z) (S Z)) (S Z)) ;; min(1, 1) = 1
;; Tests for clamp
!(assertEqual (clamp (S Z) Z (S (S (S Z)))) (S Z)) ;; clamp(1, 0, 3) = 1
!(assertEqual (clamp Z (S Z) (S (S Z))) (S Z)) ;; clamp(0, 1, 2) = 1
!(assertEqual (clamp (S (S (S Z))) Z (S (S Z))) (S (S Z))) ;; clamp(3, 0, 2) = 2
;; Tests for lte
!(assertEqual (lte (S Z) (S (S Z))) True) ;; lte(1, 2) = True
!(assertEqual (lte (S (S Z)) (S (S Z))) True) ;; lte(2, 2) = True
!(assertEqual (lte (S (S Z)) Z) False) ;; lte(2, 0) = False
;; Tests for gte
!(assertEqual (gte (S (S Z)) (S Z)) True) ;; gte(2, 1) = True
!(assertEqual (gte (S Z) (S Z)) True) ;; gte(1, 1) = True
!(assertEqual (gte Z (S Z)) False) ;; gte(0, 1) = False
;; Tests for approxEq
!(assertEqual (approxEq (S Z) (S Z) Z) True) ;; approxEq(1, 1, 0) = True
!(assertEqual (approxEq (S Z) (S (S Z)) Z) False) ;; approxEq(1, 2, 0) = False
;; Combined test cases
!(assertEqual (clamp (max (S Z) (S (S Z))) Z (S (S (S Z)))) (S (S Z))) ;; max(1, 2) clamped to [0, 3] = 2
!(assertEqual (clamp (min (S (S Z)) (S (S Z))) (S Z) (S (S (S Z)))) (S (S Z))) ;; min(2, 2) clamped to [1, 3] = 2
!(assertEqual (approxEq (max Z (min (S (S Z)) (S Z))) (S Z) Z) True) ;; approxEq(max(0, min(2, 1)), 1, 0) = True