Skip to content

Commit

Permalink
Update Tests
Browse files Browse the repository at this point in the history 
Updates test files to include interpretations of compiled STLC code in
SeqN and other individual tests for interpreters in Geb and SeqN.
  • Loading branch information
@agureev @mariari
agureev authored and mariari committed Aug 29, 2023
1 parent dda4070 commit 3b52547
Show file tree
Hide file tree
Showing 4 changed files with 82 additions and 3 deletions.
11 changes: 11 additions & 0 deletions test/geb.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,3 +128,14 @@
(is obj-equalp (gapply bool:not (left so1)) (right so1))

(is obj-equalp (gapply bool:not (right so1)) (left so1)))

(define-test geb-de-concat
:parent geb-interpreter
(is obj-equalp (list 1 0) (gapply (geb.extension.spec:nat-decompose 3) 4))
(is obj-equalp 4 (gapply (geb.extension.spec:nat-concat 1 2) (list 1 0)))
(is obj-equalp 4 (gapply (comp (geb.extension.spec:nat-concat 1 2)
(geb.extension.spec:nat-decompose 3))
4))
(is obj-equalp (list 1 0) (gapply (comp (geb.extension.spec:nat-decompose 3)
(geb.extension.spec:nat-concat 1 2))
(list 1 0))))
51 changes: 48 additions & 3 deletions test/lambda-trans.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,27 @@
(lambda:err so1)
(lambda:unit)))

(def one-bit
(lambda:bit-choice #*0000000000000001))

(def plus-one
(lambda:lamb (list (nat-width 16)) (lambda:plus (lambda:index 0)
one-bit)))
(def minus-one
(lambda:lamb (list (nat-width 16)) (lambda:minus (lambda:index 0)
one-bit)))

(def less-than-1 (lambda:lamb (list (nat-width 16))
(lambda:case-on (lambda:lamb-lt (lambda:index 0)
one-bit)
(lambda:bit-choice #*0)
(lambda:bit-choice #*1))))
(def is-1 (lambda:lamb (list (nat-width 16))
(lambda:case-on (lambda:lamb-eq (lambda:index 0)
one-bit)
(lambda:bit-choice #*0)
(lambda:bit-choice #*1))))

(def issue-58-circuit
(to-circuit
(lambda:case-on
Expand Down Expand Up @@ -92,7 +113,13 @@
(gapply (to-bitc lambda-not-with-lambda) #*0))
(is equalp
(gapply (to-bitc lambda-not-without-lambda) #*1)
(gapply (to-bitc lambda-not-with-lambda) #*1)))
(gapply (to-bitc lambda-not-with-lambda) #*1))
(is equalp (list 0 0) (gapply (to-seqn lambda-not-with-lambda) (list 1 0 0)))
(is equalp (list 1 0) (gapply (to-seqn lambda-not-with-lambda) (list 0 0 0)))
(is equalp (gapply (to-seqn lambda-not-without-lambda) (list 0 0 0))
(gapply (to-seqn lambda-not-with-lambda) (list 0 0 0)))
(is equalp (gapply (to-seqn lambda-not-without-lambda) (list 1 0 0))
(gapply (to-seqn lambda-not-with-lambda) (list 1 0 0))))

(define-test lambda.preserves-pair :parent lambda.trans-eval
(is obj-equalp
Expand All @@ -113,15 +140,19 @@
(to-cat nil bool-id)
(list (left so1) so1)))
(is obj-equalp #*0 (gapply (to-bitc bool-id) #*0))
(is obj-equalp #*1 (gapply (to-bitc bool-id) #*1)))
(is obj-equalp #*1 (gapply (to-bitc bool-id) #*1))
(is obj-equalp (list 0 0) (gapply (to-seqn bool-id) (list 0 0 0)))
(is obj-equalp (list 1 0) (gapply (to-seqn bool-id) (list 1 0 0))))

(define-test lambda.not-works :parent lambda.trans-eval
(is obj-equalp (left so1) (gapply (to-cat nil proper-not)
(list (geb:right so1) so1)))
(is obj-equalp (right so1) (gapply (to-cat nil proper-not)
(list (geb:left so1) so1)))
(is equalp #*0 (gapply (to-bitc proper-not) #*1))
(is equalp #*1 (gapply (to-bitc proper-not) #*0)))
(is equalp #*1 (gapply (to-bitc proper-not) #*0))
(is equalp (list 0 0) (gapply (to-seqn proper-not) (list 1 0 0)))
(is equalp (list 1 0) (gapply (to-seqn proper-not) (list 0 0 0))))

(define-test error-handling-case :parent lambda.trans-eval
(is obj-equalp (left so1) (gapply (to-cat nil case-error-left)
Expand All @@ -143,6 +174,20 @@
(right so1)))
so1))))

(define-test arithmetic-compilation :parent lambda.trans-eval
(is obj-equalp 1 (gapply (to-cat nil plus-one) (list 0 so1)))
(is obj-equalp 2 (gapply (to-cat nil plus-one) (list 1 so1)))
(is obj-equalp (list 1) (gapply (to-seqn plus-one) (list 0 0)))
(is obj-equalp (list 2) (gapply (to-seqn plus-one) (list 1 0)))
(is obj-equalp 0 (gapply (to-cat nil less-than-1) (list 0 so1)))
(is obj-equalp 1 (gapply (to-cat nil less-than-1) (list 1 so1)))
(is obj-equalp (list 0) (gapply (to-seqn less-than-1) (list 0 so1)))
(is obj-equalp (list 1) (gapply (to-seqn less-than-1) (list 1 so1)))
(is obj-equalp 0 (gapply (to-cat nil is-1) (list 1 so1)))
(is obj-equalp 1 (gapply (to-cat nil is-1) (list 0 so1)))
(is obj-equalp (list 0) (gapply (to-seqn is-1) (list 1 so1)))
(is obj-equalp (list 1) (gapply (to-seqn is-1) (list 0 so1))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Compile checked term tests ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Expand Down
1 change: 1 addition & 0 deletions test/package.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
(#:list #:geb-list)
(#:bool #:geb-bool)
(#:bitc #:geb.bitc)
(#:seqn #:geb.seqn.spec)
(#:lambda #:geb.lambda))
(:use #:geb.common #:parachute))

Expand Down
22 changes: 22 additions & 0 deletions test/seqn.lisp
View file
Original file line number Diff line number Diff line change
@@ -1 +1,23 @@
(in-package :geb-test)

(define-test geb-seqn :parent geb-test-suite)

(define-test seqn-evaluates-and-correctly
:parent geb-seqn
(is obj-equalp (list 1 0) (gapply (geb.common:to-seqn geb-bool:and) (list 1 0 1 0)))
(is obj-equalp (list 0 0) (gapply (geb.common:to-seqn geb-bool:and) (list 1 0 0 0)))
(is obj-equalp (list 0 0) (gapply (geb.common:to-seqn geb-bool:and) (list 0 0 1 0)))
(is obj-equalp (list 0 0) (gapply (geb.common:to-seqn geb-bool:and) (list 0 0 0 0))))

(define-test seqn-de-compose
:parent geb-seqn
(is obj-equalp (list 1 0) (gapply (seqn:seqn-decompose 3) (list 4)))
(is obj-equalp (list 4) (gapply (seqn:seqn-concat 1 2) (list 1 0)))
(is obj-equalp (list 4) (gapply (seqn:composition (seqn:seqn-concat 1 2)
(seqn:seqn-decompose 3))
(list 4)))
(is obj-equalp (list 1 0) (gapply (seqn:composition (seqn:seqn-decompose 3)
(seqn:seqn-concat 1 2))
(list 1 0))))


0 comments on commit 3b52547

Please sign in to comment.