diff --git a/src/entry/entry.lisp b/src/entry/entry.lisp index e6463a3b6..172e8012b 100644 --- a/src/entry/entry.lisp +++ b/src/entry/entry.lisp @@ -13,6 +13,10 @@ :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") + (("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 +30,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 test version) (flet ((run (stream) (cond (help (command-line-arguments:show-option-help +command-line-spec+ @@ -39,7 +43,9 @@ (load input) (compile-down :vampir vampir :stlc stlc + :library library :entry entry-point + :test test :stream stream))))) (if output (with-open-file (file output :direction :output @@ -49,16 +55,46 @@ (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 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 library test) + (let ((circuit (to-circuit eval vampir-name))) + (geb.vampir:extract + (append geb.vampir::*standard-library* + circuit (geb.seqn.trans:test-call (car circuit))) + stream) + (format stream ";"))) + ((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 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)) + ((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))) + ((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))))) diff --git a/src/entry/package.lisp b/src/entry/package.lisp index 99ba7ea53..13a51839e 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,14 @@ 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. + +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 3de8c110b..51e6547fe 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 @@ -42,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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/src/vampir/vampir.lisp b/src/vampir/vampir.lisp index e3f920d57..b5a2e6ca7 100644 --- a/src/vampir/vampir.lisp +++ b/src/vampir/vampir.lisp @@ -217,7 +217,7 @@ (make-wire :var :lst)))))))) (defun n-th (lst n) - (make-application :func :nth + (make-application :func :n_th :arguments (list lst n))) (defparameter *negative* @@ -227,7 +227,7 @@ :inputs (list :n :a) :body (list (make-application - :func :nth + :func :n_th :arguments (list (range-n (make-infix :op :+ @@ -267,7 +267,7 @@ (b-wire (make-wire :var :b)) (q-wire (make-wire :var :q)) (r-wire (make-wire :var :r))) - (make-alias :name :mod32 + (make-alias :name :mod_n :inputs (list :n :a :b) :body (list (make-equality @@ -278,7 +278,7 @@ :names (list q-wire) :value (make-application :func :fresh - :arguments (list (make-infix :op :/ + :arguments (list (make-infix :op :\\ :lhs a-wire :rhs b-wire)))) (make-bind @@ -298,7 +298,7 @@ :lhs (make-infix :op :* :lhs b-wire :rhs q-wire) - :rhs q-wire)) + :rhs r-wire)) (make-equality :lhs (make-application :func :negative :arguments @@ -310,7 +310,7 @@ r-wire)))) (defun mod-n (n a b) - (make-application :func :mod-n + (make-application :func :mod_n :arguments (list n a b))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -413,7 +413,7 @@ (defparameter *combine-aux* (make-alias - :name :combine-aux + :name :combine_aux :inputs (list :x :y) :body (list (make-infix :op :+ :lhs (make-wire :var :x) @@ -462,7 +462,7 @@ (defparameter *drop-ith-rec* (make-alias :name :drop_ith_rec - :inputs (list (cons-deconstruct :h :t)) + :inputs (list :take (cons-deconstruct :h :t)) :body (list (make-infix :lhs (make-wire :var :h) :rhs (make-application :func :take @@ -470,7 +470,7 @@ :op :|:|)))) (defparameter *drop-ith* - (let ((one (make-constant :const 1))) + (let ((l-wire (make-wire :var :l))) (make-alias :name :drop_ith :inputs (list :n) @@ -482,9 +482,9 @@ :func :fun :arguments (list (make-infix :lhs (make-wire :var :h) - :rhs one + :rhs l-wire :op :|:|) - (make-curly :value one))))))))) + (make-curly :value l-wire))))))))) (defun drop-ith (n) (make-application :func :drop_ith