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.
  • Loading branch information
@agureev
agureev committed Aug 3, 2023
1 parent 2fe9994 commit 96f799c
Show file tree
Hide file tree
Showing 3 changed files with 81 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
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.trans:to-seqn geb-bool:and) (list 1 0 1 0)))
(is obj-equalp (list 0 0) (gapply (geb.trans:to-seqn geb-bool:and) (list 1 0 0 0)))
(is obj-equalp (list 0 0) (gapply (geb.trans:to-seqn geb-bool:and) (list 0 0 1 0)))
(is obj-equalp (list 0 0) (gapply (geb.trans: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 (geb.seqn.spec:seqn-decompose 3) (list 4)))
(is obj-equalp (list 4) (gapply (geb.seqn.spec:seqn-concat 1 2) (list 1 0)))
(is obj-equalp (list 4) (gapply (geb.seqn.spec:composition (geb.seqn.spec:seqn-concat 1 2)
(geb.seqn.spec:seqn-decompose 3))
(list 4)))
(is obj-equalp (list 1 0) (gapply (geb.seqn.spec:composition (geb.seqn.spec:seqn-decompose 3)
(geb.seqn.spec:seqn-concat 1 2))
(list 1 0))))


0 comments on commit 96f799c

Please sign in to comment.