Implementation of Natural Numbers

[agureev]

1. Introduces SeqN category of finite natural number sequences

2. Introduces a new pipeline compiling STLC terms through SeqN instead of BITC

3. Implements for each n an object of natural numbers of n-bit length alongside appropriate floored operations alongside new API. Propagated the implementation to STLC and SeqN.

4. Implements is-less-than and is-equal-to predicates on natural numbers in Geb, propagates the change to STLC and SeqN.

5. Upgrades the pipeline now supporting compilation of STLC+Natural numbers+Natural Number Predicates to Vamp-IR

[mariari]

Yeah see all my comments, they are fairly through.

In the future take the generic work into their own topics so I can merge them faster and be done more properly.

When changes are in big prs like this I get less stringent and works worse with a bigger team size.

Also the docs won't build this isn't your fault (I don't think besides warnings you produced), but by other issues I've posted in #140

[mariari]

Let's start with a general formatting note

     :body (list (make-bind :names (list wire-ai)
                            :value (make-application
                                    :func :fresh
                                    :arguments (list (make-infix :op :\|
                                                                 :lhs one
                                                                 :rhs wire-a))))

For code like this try to make it look nice and around 80, here is an example of what you can do around code here in general that gets big. Notice we don't compromise the formatting too much to do this, so it read fine.

[mariari]

note symbols are case insensitive, so this will be the same as *ISZERO* or *iszero* but I don't mind it

[mariari]

minor formatting nit, you can 1 line the list here fine

[mariari]

same fam

[mariari]

- :body (list (make-wire :var :|h:(take t)|))))
+  :body (list (make-infix :lhs (make-wire :var :h)
+                           :rhs (make-application :func :take
+                                                  :arguments (list (make-wire :var :t)))
+                           :op :|:|))

Notice that we can use application here, and it is much more proper against any syntax changes that vampir might get.

I want all of these changes. Infix places parens for you already properly

VAMPIR> (make-infix :lhs (make-wire :var :h) 
                    :op :+
                    :rhs
                    (make-infix :lhs (make-wire :var :h)
                                :rhs (make-application :func :take :arguments (list (make-wire :var :t)))
                                :op :|:|))
h + (h : (take t))

if you need an extra set for whatever reason, then you should add that as a construct

[mariari]

I see lambda is still horrible as ever.

Let us attept to clean it up.

Please fix the formatting by newlining after (bit-choice bitv), so the code it maps to is on the next line, given just how big they are.

[mariari]

sbcl will yell at you for unused x. just use the make-list I used in my previous comments for these. would read much better. Or in this case use the pad-with-zeros I mentioned before.

Maybe make the API of pad-with-zeros take a keyword for prepend or postpend, doing the more useful one by default.

[mariari]

Yeah just newline the code after the case.

(defmethod well-defp-cat ((morph <substmorph>))
  (etypecase-of substmorph morph
    (comp
     (let ((mcar (mcar morph))
           (mcadr (mcadr morph)))
       (if (and (well-defp-cat mcar)
                (well-defp-cat mcadr)
                (obj-equalp (dom mcar)
                            (codom mcadr)))
           t
           (error "(Co)Domains do not match for ~A" morph))))
    (case
        (let ((mcar (mcar morph))
              (mcadr (mcadr morph)))
          (if (and (well-defp-cat mcar)
                   (well-defp-cat mcadr)
                   (obj-equalp (codom mcar)
                               (codom mcadr)))
              t
              (error "Casing ill-defined for ~A" morph))))
    (pair
     (let ((mcar (mcar morph))
           (mcdr (mcdr morph)))
       (if (and (well-defp-cat mcar)
                (well-defp-cat mcdr)
                (obj-equalp (dom mcar)
                            (dom mcdr)))
           t
           (error "Pairing ill-defined for ~A" morph))))
    ((or substobj
         init
         terminal
         project-left
         project-right
         inject-left
         inject-right
         distribute)
     t)))

[mariari]

In the future, make such generic functions be a separate topic. Thus this should be apart of some other topic, and merged into your topic.

For this PR I'll let you keep it here, but note for the future, will make your work diverge less in a real setting of X engineers hacking on a project and if I was an active dev I could merge this patch into my own code

[mariari]

Same formatting comment as I mentioned earlier

[mariari]

alias your seqn so this is just seqn: and remove the seqn words on your functions they only make the API ugly

[mariari]

Yeah see all my comments, they are fairly through.

In the future take the generic work into their own topics so I can merge them faster and be done more properly.

When changes are in big prs like this I get less stringent and works worse with a bigger team size.

Also the docs won't build this isn't your fault (I don't think besides warnings you produced), but by other issues I've posted in #140