Skip to content

Commit

Permalink
simple functionality from exetend_compat that need to be in baseline_…
Browse files Browse the repository at this point in the history
…compat
  • Loading branch information
TeamSPoon committed Nov 26, 2024
1 parent 563a37f commit 25b5584
Show file tree
Hide file tree
Showing 4 changed files with 220 additions and 0 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
;; define some-value returning Number and String
(= (some-value) 1)
(= (some-value) "a")
(= (some-value) 'a')
(= (some-value) ())
(= (some-value) (1 2 3))
(= (some-value) (println! "did it"))
(= (some-value) S)
(= (some-value) Z)
(= (some-value) (S Z))
(= (some-value) (S (S Z)))
(= (some-value) &self)


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



;; Test elementary functions
!(assertEqual (fromNumber 1) (S Z))
!(assertEqual (fromNat (S (S Z))) 2)
!(assertEqual (ceil 2.4) 3)
!(assertEqual (abs -10) 10)
!(assertEqual (approxEq 10 10.0001 1e-3) True)
!(assertEqual (approxEq 10 10.0001 1e-9) False)
!(assertEqual (⩻ Z (S Z)) True)

Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@

!(pragma! source-macros True)

(==> a b)
a

!(assertEqual (match &self b b) b)
; !(assertEqualToResult (match &self $x $x) (a b &corelib &stdlib))
82 changes: 82 additions & 0 deletions tests/baseline_compat/hyperon-mettalog_sanity/sorting_tests.metta
Original file line number Diff line number Diff line change
@@ -0,0 +1,82 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Definition of a List data structure with various methods for it. ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Declaration of List data type and constructors
(: List (-> $a Type))
(: Nil (List $a))
(: Cons (-> $a (List $a) (List $a)))

;; Insert an element to a presumably sorted list, remains sorted.
(: insert (-> $a (List $a) (List $a)))
(= (insert $x Nil) (Cons $x Nil))
(= (insert $x (Cons $head $tail))
(if (< $x $head)
(Cons $x (Cons $head $tail))
(Cons $head (insert $x $tail))))

;; Sort a list
(: sort (-> (List $a) (List $a)))
(= (sort Nil) Nil)
(= (sort (Cons $head $tail)) (insert $head (sort $tail)))

;; Check if an element is in a list (sorted or not)
(: elem (-> $a (List $a) Bool))
(= (elem $x Nil) False)
(= (elem $x (Cons $head $tail)) (if (== $x $head) True (elem $x $tail)))

;; Remove duplicates from a list
(: uniq_ (-> (List $a) (List $a) (List $a)))
(= (uniq_ $acc Nil) Nil)
(= (uniq_ $acc (Cons $head $tail))
(if (elem $head $acc)
(uniq_ $acc $tail)
(Cons $head (uniq_ (Cons $head $acc) $tail))))
(: uniq (-> (List $a) (List $a)))
(= (uniq $l) (uniq_ Nil $l))

;; Insert an element in a presumably sorted list without duplicate.
;; Only insert if the element is not already in the list as to produce
;; a sorted list without duplicate.
(: insert_uniq (-> $a (List $a) (List $a)))
(= (insert_uniq $x Nil) (Cons $x Nil))
(= (insert_uniq $x (Cons $head $tail))
(if (== $x $head)
(Cons $head $tail)
(if (< $x $head)
(Cons $x (Cons $head $tail))
(Cons $head (insert_uniq $x $tail)))))


;; Import List
!(import! &self List.metta)

;; Test insert
!("============ Test insert ============")
!(insert 1 Nil)
!(insert 2 (insert 1 Nil))
!(insert 3 (insert 2 (insert 1 Nil)))
!(== (Cons 1 Nil) (Cons 1 Nil))

;; Test sort
!("============ Test sort ============")
!(sort (Cons 1 Nil))
!(sort (Cons 2 (Cons 1 Nil)))
!(sort (Cons 3 (Cons 1 (Cons 2 Nil))))

;; Test elem
!("============ Test elem ============")
!(elem 1 (Cons 3 (Cons 1 (Cons 2 Nil))))
!(elem 5 (Cons 3 (Cons 1 (Cons 2 Nil))))

;; Test uniq
!("============ Test uniq ============")
!(uniq (Cons 2 (Cons 3 (Cons 1 (Cons 2 Nil)))))
!(uniq (Cons 2 (Cons 3 (Cons 3 (Cons 2 Nil)))))

;; Test insert_uniq
!("============ Test insert_uniq ============")
!(insert_uniq 2 (insert_uniq 1 Nil))
!(insert_uniq 3 (insert_uniq 2 (insert_uniq 1 Nil)))
!(insert_uniq 2 (insert_uniq 3 (insert_uniq 2 (insert_uniq 1 Nil))))

Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
;; define some-value returning Number and String
(= (some-value) 1)
(= (some-value) "a")
(= (some-value) 'a')
(= (some-value) ())
(= (some-value) (1 2 3))
(= (some-value) (println! "did it"))
(= (some-value) a-symbol)
(= (some-value) &self)

(: Filter-String (-> String $t))
(: Filter-Number (-> Number $t))

;; returns of appropriate type
!(assertEqualToResult (Filter-Number (some-value)) (1))
!(assertEqualToResult (Filter-String (some-value)) ("a"))


;; Checks if the above would oif worked had there been a specific implemenation other than default
(: Impl-Filter-String (-> String $t))
(= (Impl-Filter-String $a) $a)

(: Impl-Filter-Number (-> Number $t))
(= (Impl-Filter-Number $a) $a)

;; returns of appropriate type
!(assertEqualToResult (Impl-Filter-Number (some-value)) (1))
!(assertEqualToResult (Impl-Filter-String (some-value)) ("a"))



0 comments on commit 25b5584

Please sign in to comment.