Skip to content

Commit

Permalink
24-bit Changes
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@agureev
agureev committed Oct 10, 2023
1 parent 5bcfc00 commit 6269858
Show file tree
Hide file tree
Showing 5 changed files with 62 additions and 63 deletions.
34 changes: 20 additions & 14 deletions src/lambda/lambda.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down Expand Up @@ -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)
Expand Down
38 changes: 21 additions & 17 deletions src/lambda/trans.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 <stlc>))
"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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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"))
Expand Down
32 changes: 12 additions & 20 deletions src/seqn/trans.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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))
Expand All @@ -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))
Expand All @@ -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))
Expand Down
3 changes: 0 additions & 3 deletions src/vampir/vampir.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -597,9 +597,6 @@
*tl*
*n-th*
*negative*
*plus-range*
*mult-range*
*minus-range*
*isZero*
*combine-aux*
*combine*
Expand Down
18 changes: 9 additions & 9 deletions test/lambda-trans.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 6269858

Please sign in to comment.