From 626985888158535814156ae0b9378c783036ea45 Mon Sep 17 00:00:00 2001 From: Artem Gureev Date: Tue, 10 Oct 2023 16:44:46 +0600 Subject: [PATCH] 24-bit Changes Assumes that all the numbers fed into the pipeline are of 24-bitwidth. Removes all range checks and replaces bits with natural numbers for the sake of Juvix test compilation efficientcy. --- src/lambda/lambda.lisp | 34 ++++++++++++++++++++-------------- src/lambda/trans.lisp | 38 +++++++++++++++++++++----------------- src/seqn/trans.lisp | 32 ++++++++++++-------------------- src/vampir/vampir.lisp | 3 --- test/lambda-trans.lisp | 18 +++++++++--------- 5 files changed, 62 insertions(+), 63 deletions(-) diff --git a/src/lambda/lambda.lisp b/src/lambda/lambda.lisp index c054159d0..d0afb4759 100644 --- a/src/lambda/lambda.lisp +++ b/src/lambda/lambda.lisp @@ -171,23 +171,23 @@ the context on the left as well. For more info check [LAMB][class]")) ((times ltm rtm) (let ((ant (ann-term1 ctx ltm))) (times ant (ann-term1 ctx rtm) - :ttype (ttype ant)))) + :ttype (nat-width 24)))) ((minus ltm rtm) (let ((ant (ann-term1 ctx ltm))) (minus ant (ann-term1 ctx rtm) - :ttype (ttype ant)))) + :ttype (nat-width 24)))) ((divide ltm rtm) (let ((ant (ann-term1 ctx ltm))) (divide ant (ann-term1 ctx rtm) - :ttype (ttype ant)))) + :ttype (nat-width 24)))) ((bit-choice bitv) (bit-choice bitv - :ttype (nat-width (array-total-size bitv)))) + :ttype (nat-width 24))) ((lamb-eq ltm rtm) (lamb-eq (ann-term1 ctx ltm) (ann-term1 ctx rtm) :ttype (coprod so1 so1))) ((lamb-lt ltm rtm) (lamb-lt (ann-term1 ctx ltm) - (ann-term1 ctx rtm) - :ttype (coprod so1 so1))) + (ann-term1 ctx rtm) + :ttype (coprod so1 so1))) ((case-on on ltm rtm) (let* ((ann-on (ann-term1 ctx on)) (type-of-on (ttype ann-on)) @@ -340,14 +340,20 @@ nil")) (obj-equalp (mcadr lambda-type) (ttype term))))) ((app fun term) (and (check fun) - (check (reduce #'pair term)))) - ((or (plus ltm rtm) - (minus ltm rtm) - (times ltm rtm) - (divide ltm rtm) - (lamb-eq ltm rtm) - (lamb-lt ltm rtm)) - (obj-equalp (ttype ltm) (ttype rtm))) + (check (reduce #'pair term :from-end t)) + (typep (ttype fun) 'fun-type) + (obj-equalp (ttype fun) + (fun-type (reduce #'prod + (mapcar #'ttype term) + :from-end t) + (ttype tterm))))) + ((or plus + minus + times + divide + lamb-eq + lamb-lt) + t) (index t) (unit t) (err t) diff --git a/src/lambda/trans.lisp b/src/lambda/trans.lisp index 7bc48f2cf..fc5fe7e99 100644 --- a/src/lambda/trans.lisp +++ b/src/lambda/trans.lisp @@ -85,6 +85,12 @@ error node" (lamb-eq #'nat-eq) (lamb-lt #'nat-lt))) +(defparameter *int* (nat-width 24) + "A Juvix stand-in for a type of integers of their bit-choice. +In this version, the choice is that of 24-bits.") + +(def int *int*) + (defmethod to-cat-err (context (tterm )) "Compiles a checked term with an error term in an appropriate context into the morphism of the GEB category using a Maybe monad wrapper, that is, given a @@ -261,19 +267,19 @@ This follows from the fact that bool arapped in maybe is 1 + (bool + bool)" (let ((tyltm (ttype (ltm tterm)))) (labels ((arith (op) (comp (mcase (terminal (prod (maybe tyltm) - so1)) - (commutes-left (comp - (mcase (terminal (prod tyltm - so1)) - (funcall op tyltm)) - (distribute tyltm - so1 - tyltm)))) - (comp (distribute (maybe tyltm) - so1 - tyltm) - (geb:pair (rec context (ltm tterm)) - (rec context (rtm tterm))))))) + so1)) + (commutes-left (comp + (mcase (terminal (prod tyltm + so1)) + (funcall op tyltm)) + (distribute tyltm + so1 + tyltm)))) + (comp (distribute (maybe tyltm) + so1 + tyltm) + (geb:pair (rec context (ltm tterm)) + (rec context (rtm tterm))))))) (arith (dispatch tterm)))))))) (if (not (well-defp context tterm)) (error "not a well-defined ~A in said ~A" tterm context) @@ -380,10 +386,8 @@ iterated, so is the uncurrying." ((index pos) (stlc-ctx-proj context pos)) ((bit-choice bitv) - (comp (nat-const (num (ttype tterm)) - (reduce - (lambda (a b) (+ (ash a 1) b)) - bitv)) + (comp (nat-const 24 + bitv) (terminal (stlc-ctx-to-mu context)))) (err (error "Not meant for the compiler")) diff --git a/src/seqn/trans.lisp b/src/seqn/trans.lisp index 92bc4f82f..c474f1f01 100644 --- a/src/seqn/trans.lisp +++ b/src/seqn/trans.lisp @@ -31,17 +31,15 @@ and skip 0es, making non-zero entries into wires" :name name :inputs wires :body - (append - (range-constraints-dom (dom morphism)) - (list - (vamp:make-tuples - :wires - (remove nil - (filter-map (lambda (x) - (unless (zerop (car x)) - (cadr x))) - (prod-list (cod morphism) - (to-vampir morphism wires nil))))))))))) + (list + (vamp:make-tuples + :wires + (remove nil + (filter-map (lambda (x) + (unless (zerop (car x)) + (cadr x))) + (prod-list (cod morphism) + (to-vampir morphism wires nil)))))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; SeqN to Vamp-IR Compilation @@ -186,9 +184,7 @@ removed already and hence we cannot count as usual" (if (> (expt 2 mcar) plus) (vamp:make-constant :const plus) (error "Range Exceeded"))) - (list (geb.vampir:plus-range (vamp:make-constant :const mcar) - car - cadr))))) + (list (make-opt-plus car cadr))))) (defmethod to-vampir ((obj seqn-subtract) inputs constraints) (declare (ignore constraints)) @@ -199,9 +195,7 @@ removed already and hence we cannot count as usual" (if (<= 0 minus) (vamp:make-constant :const minus) (error "Subtraction Produces Negative Numbers"))) - (list (geb.vampir:minus-range (vamp:make-constant :const (mcar obj)) - car - cadr))))) + (list (make-opt-minus car cadr))))) (defmethod to-vampir ((obj seqn-multiply) inputs constraints) (declare (ignore constraints)) @@ -213,9 +207,7 @@ removed already and hence we cannot count as usual" (if (> (expt 2 mcar) mult) (vamp:make-constant :const mult) (error "Range Exceeded"))) - (list (geb.vampir:mult-range (vamp:make-constant :const mcar) - car - cadr))))) + (list (make-opt-times car cadr))))) (defmethod to-vampir ((obj seqn-divide) inputs constraints) (declare (ignore constraints)) diff --git a/src/vampir/vampir.lisp b/src/vampir/vampir.lisp index 139b27d3b..8c31068f8 100644 --- a/src/vampir/vampir.lisp +++ b/src/vampir/vampir.lisp @@ -597,9 +597,6 @@ *tl* *n-th* *negative* - *plus-range* - *mult-range* - *minus-range* *isZero* *combine-aux* *combine* diff --git a/test/lambda-trans.lisp b/test/lambda-trans.lisp index a9ec301c0..6b7d05a62 100644 --- a/test/lambda-trans.lisp +++ b/test/lambda-trans.lisp @@ -58,25 +58,25 @@ (lambda:unit))) (def one-bit - (lambda:bit-choice #*0000000000000001)) + (lambda:bit-choice 1)) (def plus-one - (lambda:lamb (list (nat-width 16)) (lambda:plus (lambda:index 0) + (lambda:lamb (list (nat-width 24)) (lambda:plus (lambda:index 0) one-bit))) (def minus-one - (lambda:lamb (list (nat-width 16)) (lambda:minus (lambda:index 0) + (lambda:lamb (list (nat-width 24)) (lambda:minus (lambda:index 0) one-bit))) -(def less-than-1 (lambda:lamb (list (nat-width 16)) +(def less-than-1 (lambda:lamb (list (nat-width 24)) (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:bit-choice 0) + (lambda:bit-choice 1)))) +(def is-1 (lambda:lamb (list (nat-width 24)) (lambda:case-on (lambda:lamb-eq (lambda:index 0) one-bit) - (lambda:bit-choice #*0) - (lambda:bit-choice #*1)))) + (lambda:bit-choice 0) + (lambda:bit-choice 1)))) (def issue-58-circuit (to-circuit