Num.metta

;; Collection of functions operating on numbers

;; Define max
(: max (-> $a $a $a))
(= (max $x $y) (if (> $x $y) $x $y))

;; Define min
(: min (-> $a $a $a))
(= (min $x $y) (if (< $x $y) $x $y))

;; Clamp a number to be within a certain range
(: clamp (-> $a $a $a $a))
(= (clamp $x $l $u) (max $l (min $u $x)))

;; Define abs
(: abs (-> $a $a))
(= (abs $x) (if (< $x 0) (* -1 $x) $x))

;; Define <=
(: <= (-> $a $a Bool))
(= (<= $x $y) (or (< $x $y) (== $x $y)))

;; Define >=
(: >= (-> $a $a Bool))
(= (>= $x $y) (or (> $x $y) (== $x $y)))

;; Define approximately equal
(: approxEq (-> $a $a $a Bool))
(= (approxEq $x $y $epsilon) (<= (abs (- $x $y)) $epsilon))

;; 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)))

;; Define a generic less than operator, ⩻, for Nat.  < cannot be used
;; because it is a built-in, its type is hardwired and cannot be
;; overloaded.
(: ⩻ (-> Nat Nat Bool))
(= (⩻ $_ Z) False)
(= (⩻ Z (S $_)) True)
(= (⩻ (S $x) (S $y)) (⩻ $x $y))

;; Overload ⩻ for Number.
(: ⩻ (-> Number Number Bool))
(= (⩻ $x $y) (< $x $y))

;; Return the ceiling of a non negative number.  If the number is
;; negative it returns 1.
(: ceil (-> Number Number))
(= (ceil $n) (fromNat (fromNumber $n)))

;; Convert Number to Bool.  Anything above 0 converts to True.
(: number->bool (-> Number Bool))
(= (number->bool $x) (< 0 $x))

;; Convert Bool to Number.  False converts to 0, True converts to 1.
(: bool->number (-> Bool Number))
(= (bool->number False) 0)
(= (bool->number True) 1)

;; Define a less than type.  Note that it is purposefully different
;; than ⩻ as it is a type, not an operator.  Inhabitants of (⍃ x y)
;; are proofs that x ⩻ y == True.  For now ⍃ is only axiomatized for
;; Nat.
(: ⍃ (-> $t $t Type))

;; Zero is always less than the successor of something
(: (zero-lt-succ-axiom) (-> Atom))
(= (zero-lt-succ-axiom)
   (: ZeroLTSucc (⍃ Z (S $k))))

;; If x ⍃ y then (S x) ⍃ (S y)
(: (succ-monotonicity-rule) (-> Atom))
(= (succ-monotonicity-rule)
   (: SuccMonotonicity (-> (⍃ $x $y)
                           (⍃ (S $x) (S $y)))))