From f0579600d5a160269eb0f6a98d2035c51fb18270 Mon Sep 17 00:00:00 2001 From: Artem Gureev Date: Fri, 3 Nov 2023 18:34:50 +0600 Subject: [PATCH 1/4] Fix to-circuit Variable Printing Previously a Lambda function taking natural number arguments `A1` to `An` would be compiled to a circuit with arguments `x1` to `x(n+1)` where argument `xi` in the circuit for i<(n+1) stands for argument `A(n-i)` and `x(n+1)` stands as an unused variable. Current channge omits the final variable and renames the rest, so that the compiled circuit will have appropriate argument order and type corresponding to the relevant STLC term. Note that this changes how to input coproduct type circuit variables. A --- src/seqn/trans.lisp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/seqn/trans.lisp b/src/seqn/trans.lisp index 2663dc69b..0d9467f68 100644 --- a/src/seqn/trans.lisp +++ b/src/seqn/trans.lisp @@ -24,12 +24,14 @@ Note that what is happening is that we look at the domain of the morphism and skip 0es, making non-zero entries into wires" (let* ((wire-count (length (dom morphism))) (wires (loop for i from 1 to wire-count - collect (vamp:make-wire :var (intern (format nil "X~a" i) - :keyword))))) + collect (vamp:make-wire + :var (intern + (format nil "X~a" (- wire-count i)) + :keyword))))) (list (vamp:make-alias :name name - :inputs wires + :inputs (cdr (reverse wires)) :body (list (vamp:make-tuples From cb83981d23075e1db728557e3b61c25e0a55c9e0 Mon Sep 17 00:00:00 2001 From: Artem Gureev Date: Tue, 21 Nov 2023 18:28:32 +0600 Subject: [PATCH 2/4] Add Standard Library Flag for Entry Adds a `library` flag which can be included while using Geb as a binary to print the standard library alongside the compiled STLC or Geb term. --- src/entry/entry.lisp | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/src/entry/entry.lisp b/src/entry/entry.lisp index e6463a3b6..cf6453e42 100644 --- a/src/entry/entry.lisp +++ b/src/entry/entry.lisp @@ -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") + (("library" #\s) + :type boolean :optional t :documentation "Prints standard library") (("help" #\h #\?) :type boolean :optional t :documentation "The current help message"))) @@ -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 library version) (flet ((run (stream) (cond (help (command-line-arguments:show-option-help +command-line-spec+ @@ -39,6 +41,7 @@ (load input) (compile-down :vampir vampir :stlc stlc + :library library :entry entry-point :stream stream))))) (if output @@ -49,16 +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*)) - (let* ((name (read-from-string entry)) - (eval (eval name)) - (vampir-name (renaming-scheme (intern (symbol-name name) 'keyword)))) - (cond ((and vampir stlc) +(defun compile-down (&key vampir stlc entry library (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 library) + (geb.vampir:extract + (append geb.vampir::*standard-library* + (to-circuit eval vampir-name)))) + ((and vampir stlc) (geb.vampir:extract (to-circuit eval vampir-name) stream)) (stlc (format stream "~A" (to-cat nil eval))) + ((and vampir library) + (geb.vampir:extract + (append geb.vampir::*standard-library* + (to-circuit eval vampir-name)))) (vampir (geb.vampir:extract (to-circuit eval vampir-name) stream)) + (library + (geb.vampir:extract geb.vampir::*standard-library*)) (t (format stream eval))))) From 3c7e9eb13dc8c162d4283900bcca2de8e48b85c4 Mon Sep 17 00:00:00 2001 From: Artem Gureev Date: Thu, 2 Nov 2023 17:42:58 +0600 Subject: [PATCH 3/4] Add New Flag Documentation Adds documentation for the new standard library flag. --- src/entry/package.lisp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/entry/package.lisp b/src/entry/package.lisp index 99ba7ea53..978b7cad1 100644 --- a/src/entry/package.lisp +++ b/src/entry/package.lisp @@ -45,6 +45,7 @@ mariari@Gensokyo % ./geb.image -h -o --output string Save the output to a file rather than printing -v --version boolean Prints the current version of the compiler -p --vampir string Return a vamp-ir expression + -s --library boolean Print standard library -h -? --help boolean The current help message mariari@Gensokyo % ./geb.image -v @@ -82,5 +83,9 @@ 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 -s prints the standard library the compiler uses. If -p is +used alongside it, the standard library gets printed before the +compiled circuit." (compile-down function)) From 1425aa6d757c62b6f383083a215e6cc8a0117f85 Mon Sep 17 00:00:00 2001 From: Artem Gureev Date: Fri, 3 Nov 2023 21:18:22 +0600 Subject: [PATCH 4/4] Introduce Test Flag For Binary 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. --- src/entry/entry.lisp | 23 ++++++++++++++++++++--- src/entry/package.lisp | 7 ++++++- src/seqn/package.lisp | 1 + src/seqn/trans.lisp | 11 +++++++++++ 4 files changed, 38 insertions(+), 4 deletions(-) diff --git a/src/entry/entry.lisp b/src/entry/entry.lisp index e6463a3b6..cd97fc5e7 100644 --- a/src/entry/entry.lisp +++ b/src/entry/entry.lisp @@ -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"))) @@ -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+ @@ -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 @@ -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 diff --git a/src/entry/package.lisp b/src/entry/package.lisp index 99ba7ea53..67849d038 100644 --- a/src/entry/package.lisp +++ b/src/entry/package.lisp @@ -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)) diff --git a/src/seqn/package.lisp b/src/seqn/package.lisp index 28a98b962..37e48ae48 100644 --- a/src/seqn/package.lisp +++ b/src/seqn/package.lisp @@ -41,6 +41,7 @@ (pax:defsection @seqb-trans (:title "Seqn Transformations") "This covers transformation functions from" (to-circuit (method () ( t))) + (test-call function) (to-vampir (method () (id t t))) (to-vampir (method () (composition t t))) (to-vampir (method () (parallel-seq t t))) diff --git a/src/seqn/trans.lisp b/src/seqn/trans.lisp index 0d9467f68..de6afdd0d 100644 --- a/src/seqn/trans.lisp +++ b/src/seqn/trans.lisp @@ -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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;