Skip to content

Commit

Permalink
Introduce Test Flag For Binary
Browse files Browse the repository at this point in the history
Introduces `--test` flag using `-t` for binary usage. When used with
`-p`, given a compiled VampIR function of form `def foo x1 ... xn =
{body};` produces a test equality `foo x1 ... xn = y;` printed after
the entry function.
  • Loading branch information
agureev committed Nov 22, 2023
1 parent f057960 commit 1425aa6
Show file tree
Hide file tree
Showing 4 changed files with 38 additions and 4 deletions.
23 changes: 20 additions & 3 deletions src/entry/entry.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@
:type boolean :optional t :documentation "Prints the current version of the compiler")
(("vampir" #\p)
:type string :optional t :documentation "Return a vamp-ir expression")
(("test" #\t)
:type boolean :optional t :documentation "Prints a test equality with public parameters")
(("help" #\h #\?)
:type boolean :optional t :documentation "The current help message")))

Expand All @@ -26,7 +28,7 @@
(defparameter *no-input-text*
"Please provide an input file with -p or see the help command with -h")

(defun argument-handlers (&key help stlc output input entry-point vampir version)
(defun argument-handlers (&key help stlc output input entry-point vampir test version)
(flet ((run (stream)
(cond (help
(command-line-arguments:show-option-help +command-line-spec+
Expand All @@ -40,6 +42,7 @@
(compile-down :vampir vampir
:stlc stlc
:entry entry-point
:test test
:stream stream)))))
(if output
(with-open-file (file output :direction :output
Expand All @@ -49,12 +52,26 @@
(run *standard-output*))))

;; this code is very bad please abstract out many of the components
(defun compile-down (&key vampir stlc entry (stream *standard-output*))
(defun compile-down (&key vampir stlc entry test (stream *standard-output*))
(let* ((name (read-from-string entry))
(eval (eval name))
(vampir-name (renaming-scheme (intern (symbol-name name) 'keyword))))
(cond ((and vampir stlc)
(cond ((and vampir stlc test)
(let ((circuit (to-circuit eval vampir-name)))
(geb.vampir:extract (append circuit
(geb.seqn.trans:test-call
(car circuit)))
stream)
(format stream ";")))
((and vampir stlc)
(geb.vampir:extract (to-circuit eval vampir-name) stream))
((and vampir test)
(let ((circuit (to-circuit eval vampir-name)))
(geb.vampir:extract (append circuit
(geb.seqn.trans:test-call
(car circuit)))
stream)
(format stream ";")))
(stlc
(format stream "~A" (to-cat nil eval)))
(vampir
Expand Down
7 changes: 6 additions & 1 deletion src/entry/package.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -82,5 +82,10 @@ expects a symbol.
the -l flag means that we are not expecting a geb term, but rather a
lambda frontend term, this is to simply notify us to compile it as a
lambda term rather than a geb term. In time this will go away"
lambda term rather than a geb term. In time this will go away
The flag -t after -p signals that the user wants to make an
automatically generated test equality. Given a compiled VampIR
function with name foo and arguments x1...xn prints an equality as
foo x1 ... xn = y"
(compile-down function))
1 change: 1 addition & 0 deletions src/seqn/package.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@
(pax:defsection @seqb-trans (:title "Seqn Transformations")
"This covers transformation functions from"
(to-circuit (method () (<seqn> t)))
(test-call function)
(to-vampir (method () (id t t)))
(to-vampir (method () (composition t t)))
(to-vampir (method () (parallel-seq t t)))
Expand Down
11 changes: 11 additions & 0 deletions src/seqn/trans.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,17 @@ and skip 0es, making non-zero entries into wires"
(prod-list (cod morphism)
(to-vampir morphism wires nil)))))))))))

(defun test-call (circuit)
"Given a compiled VampIR function with name foo and arguments x1...xn prints
an equality as foo x1 ... xn = y"
(let ((inputs (vamp:inputs circuit))
(name (vamp:name circuit)))
(list (vamp:make-equality
:lhs (if (zerop (length inputs))
(vamp:make-wire :var name)
(vamp:make-application :func name :arguments inputs))
:rhs (vamp:make-wire :var :y)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; SeqN to Vamp-IR Compilation
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Expand Down

0 comments on commit 1425aa6

Please sign in to comment.