Merge remote-tracking branch 'origin/artem/modulo-func' into artem/la…

…mbda-reducer

src/geb/geb.lisp

@@ -97,7 +97,8 @@
          nat-sub
          nat-mult
          nat-div
-         nat-const)
+         nat-const
+         nat-mod)
      (nat-width (num x)))
     (otherwise
      (subclass-responsibility x))))
@@ -492,6 +493,7 @@ GEB> (gapply geb-bool:and
     (nat-sub   (- (car object) (cadr object)))
     (nat-div   (multiple-value-bind (q)
                    (floor (car object) (cadr object)) q))
+    (nat-mod   (mod (car object) (cadr object)))
     (nat-const  (pos morph))
     (nat-inj    object)
     (nat-concat  (+ (* (expt 2 (num-right morph)) (car object)) (cadr object)))

src/geb/trans.lisp

@@ -328,6 +328,10 @@ get ((A x B) + (A x C)) as times appends sequences"
   "Division is interpreted as divition"
   (seqn-divide (geb.extension.spec:num obj)))
 
+(defmethod to-seqn ((obj geb.extension.spec:nat-mod))
+  "Division is interpreted as divition"
+  (seqn-mod (geb.extension.spec:num obj)))
+
 (defmethod to-seqn ((obj geb.extension.spec:nat-const))
   "A choice of a natural number is the same exact choice in SeqN"
   (seqn-nat (geb.extension.spec:num obj) (geb.extension.spec:pos obj)))

src/lambda/lambda.lisp

@@ -158,8 +158,12 @@ the context on the left as well. For more info check [LAMB][class]"))
                                             (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)))
+        ((modulo ltm rtm)          (let ((ant (ann-term1 ctx ltm)))
+                                     (modulo ant
                                              (ann-term1 ctx rtm)
-                                             :ttype (coprod so1 so1)))
+                                             :ttype (ttype ant))))
         ((case-on on ltm rtm)
          (let* ((ann-on     (ann-term1 ctx on))
                 (type-of-on (ttype ann-on))
@@ -231,6 +235,7 @@ occurences - re-annotates the term and its subterms with actual
          times
          minus
          divide
+         modulo
          bit-choice
          lamb-eq
          lamb-lt)
@@ -322,7 +327,8 @@ nil"))
                ((or plus
                     minus
                     divide
-                    times)
+                    times
+                    modulo)
                 (obj-equalp (ttype (ltm tterm))
                             (ttype (rtm tterm))))
                ((or lamb-eq
@@ -358,7 +364,8 @@ nil"))
              (typep tterm 'times)
              (typep tterm 'divide)
              (typep tterm 'lamb-eq)
-             (typep tterm 'lamb-lt))
+             (typep tterm 'lamb-lt)
+             (typep tterm 'modulo))
          (or (errorp (ltm tterm))
              (errorp (rtm tterm))))
         (t                        (errorp (term tterm)))))

src/lambda/trans.lisp

@@ -83,7 +83,8 @@ error node"
     (times #'nat-mult)
     (divide #'nat-div)
     (lamb-eq #'nat-eq)
-    (lamb-lt #'nat-lt)))
+    (lamb-lt #'nat-lt)
+    (modulo #'nat-mod)))
 
 (defmethod to-cat-err (context (tterm <stlc>))
   "Compiles a checked term with an error term in an appropriate context into the
@@ -257,7 +258,8 @@ This follows from the fact that bool arapped in maybe is 1 + (bool + bool)"
                     times
                     divide
                     lamb-eq
-                    lamb-lt)
+                    lamb-lt
+                    modulo)
                 (let ((tyltm (ttype (ltm tterm))))
                   (labels ((arith (op)
                              (comp (mcase (terminal (prod (maybe tyltm)
@@ -392,7 +394,8 @@ iterated, so is the uncurrying."
                     times
                     divide
                     lamb-eq
-                    lamb-lt)
+                    lamb-lt
+                    modulo)
                 (let ((ltm (ltm tterm)))
                   (labels ((arith (op)
                              (comp (funcall op (num (ttype ltm)))

src/seqn/seqn.lisp

@@ -84,6 +84,7 @@ For a less formal desription consult the specs file"
     (seqn-subtract    (list (mcar x) (mcar x)))
     (seqn-multiply    (list (mcar x) (mcar x)))
     (seqn-divide      (list (mcar x) (mcar x)))
+    (seqn-mod         (list (mcar x) (mcar x)))
     (seqn-nat         (list 0))
     (seqn-concat      (list (mcar x) (mcadr x)))
     (seqn-decompose   (list (mcar x)))
@@ -119,6 +120,7 @@ For a less formal description consult the specs file"
     (seqn-multiply    (list (mcar x)))
     (seqn-divide      (list (mcar x)))
     (seqn-nat         (list (mcar x)))
+    (seqn-mod         (list (mcar x)))
     (seqn-concat      (list (+ (mcar x) (mcadr x))))
     (seqn-decompose   (list 1 (1- (mcar x))))
     (seqn-eq          (list 1 0))
@@ -167,6 +169,7 @@ is capable of succesfully evaluating all compiled terms"
     (seqn-multiply    (list (* (car vector) (cadr vector))))
     (seqn-divide      (list (multiple-value-bind (q)
                                 (floor (car vector) (cadr vector)) q)))
+    (seqn-mod         (list (mod (car vector) (cadr vector))))
     (seqn-nat         (list (mcadr morphism)))
     (seqn-concat      (list (+ (* (expt 2 (mcadr morphism)) (car vector))
                                (cadr vector))))
@@ -236,6 +239,7 @@ is capable of succesfully evaluating all compiled terms"
          seqn-multiply
          seqn-divide
          seqn-subtract
+         seqn-mod
          seqn-nat
          seqn-concat
          seqn-decompose

src/seqn/trans.lisp

@@ -322,6 +322,15 @@ removed already and hence we cannot count as usual"
                                                     :rhs cadr))
               zero))))
 
+(defmethod to-vampir ((obj seqn-mod) inputs constraints)
+  (declare (ignore constraints))
+  (let ((car (car inputs))
+        (cadr (cadr inputs)))
+    (if (const-check inputs)
+        (list (vamp:make-constant :const (mod (vamp:const car) (vamp:const cadr))))
+        (list (geb.vampir:mod-n (vamp:make-constant :const (mcar obj))
+                                car cadr)))))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Helpers
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

src/specs/extension.lisp

@@ -69,7 +69,7 @@ of natural numbers"))
 
 (deftype natmorph ()
   '(or nat-add nat-inj nat-mult nat-sub nat-div nat-const nat-concat
-       one-bit-to-bool nat-decompose nat-eq nat-lt))
+       one-bit-to-bool nat-decompose nat-eq nat-lt nat-mod))
 
 (defclass nat-width (<natobj>)
   ((num :initarg :num
@@ -233,6 +233,14 @@ which evaluated to true iff both inputs are the same"))
   (:documentation "Morphism nat-width n x nat-width n -> bool
 which evaluated to true iff the first input is less than the second"))
 
+(defclass nat-mod (<natmorph>)
+  ((num :initarg :num
+        :accessor num
+        :documentation ""))
+  (:documentation "Morphism nat-width n x nat-width n -> nat-width n
+which takes a modulo of the left projection of a pair by the second
+projection of a pari"))
+
 (defun nat-add (num)
   (values
    (make-instance 'nat-add :num num)))
@@ -284,6 +292,9 @@ which evaluated to true iff the first input is less than the second"))
 (defun nat-lt (num)
   (make-instance 'nat-lt :num num))
 
+(defun nat-mod (num)
+  (make-instance 'nat-mod :num num))
+
 
 
 

src/specs/lambda-printer.lisp

@@ -25,3 +25,4 @@
 (easy-printer bit-choice)
 (easy-printer lamb-eq)
 (easy-printer lamb-lt)
+(easy-printer modulo)

src/specs/lambda.lisp

@@ -11,7 +11,7 @@ unit types as well as coproduct, product, and function types."))
 which can be filled by auxillary functions or by user. Types are
 represented as [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]."
   '(or absurd unit left right case-on pair fst snd lamb app index err
-    plus times minus divide bit-choice lamb-eq lamb-lt))
+    plus times minus divide bit-choice lamb-eq lamb-lt modulo))
 
 ;; New defgenerics
 
@@ -744,3 +744,33 @@ will be associated with the 0 input and teh second branch with 1."))
 (defun lamb-lt (ltm rtm &key (ttype nil))
   (values
    (make-instance 'lamb-lt :ltm ltm :rtm rtm :ttype ttype)))
+
+(defclass modulo (<stlc>)
+  ((ltm :initarg :ltm
+        :accessor ltm
+        :documentation "")
+   (rtm :initarg :rtm
+        :accessor rtm
+        :documentation "")
+   (ttype :initarg :ttype
+          :initform nil
+          :accessor ttype
+          :documentation ""))
+  (:documentation "A term representing syntactic modulus of the first number
+by the second number. The formal grammar of [MODULO] is
+
+```lisp
+(modulo ltm rtm)
+```
+
+where we can possibly supply typing info by
+
+```lisp
+(modulo ltm rtm :ttype ttype)
+```
+
+meaning that we take ltm mod rtm"))
+
+(defun modulo (ltm rtm &key (ttype nil))
+  (values
+   (make-instance 'modulo :ltm ltm :rtm rtm :ttype ttype)))

src/specs/package.lisp

@@ -176,7 +176,8 @@ constructors"
   (seqn-concat      pax:class)
   (seqn-decompose   pax:class)
   (seqn-eq          pax:class)
-  (seqn-lt          pax:class))
+  (seqn-lt          pax:class)
+  (seqn-mod         pax:class))
 
 (pax:defsection @seqn-constructors (:title "Seqn Constructors")
   "Every accessor for each of the classes making up seqn"
@@ -203,7 +204,8 @@ constructors"
   (seqn-concat      pax:function)
   (seqn-decompose   pax:function)
   (seqn-eq          pax:function)
-  (seqn-lt          pax:function))
+  (seqn-lt          pax:function)
+  (seqn-mod         pax:function))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Geb lambda Package Documentation
@@ -237,6 +239,7 @@ constructors"
   (bit-choice pax:class)
   (lamb-eq pax:class)
   (lamb-lt pax:class)
+  (modulo  pax:class)
 
   (absurd pax:function)
   (unit pax:function)
@@ -257,6 +260,7 @@ constructors"
   (bit-choice pax:function)
   (lamb-eq    pax:function)
   (lamb-lt    pax:function)
+  (absurd     pax:function)
 
 
   "Accessors of [ABSURD][class]"
@@ -348,6 +352,11 @@ constructors"
   (rtm   (pax:method () (lamb-lt)))
   (ttype (pax:method () (lamb-lt)))
 
+  "Accessors of [MODULO][class]"
+  (ltm   (pax:method () (modulo)))
+  (rtm   (pax:method () (modulo)))
+  (ttype (pax:method () (modulo)))
+
   (tcod pax:generic-function)
   (tdom pax:generic-function)
   (term pax:generic-function)
@@ -579,6 +588,7 @@ throughout any piece of code"
   (nat-decompose   pax:class)
   (nat-eq          pax:class)
   (nat-lt          pax:class)
+  (nat-mod         pax:class)
 
   (num       (pax:method () (nat-add)))
   (num       (pax:method () (nat-mult)))
@@ -592,6 +602,7 @@ throughout any piece of code"
   (num       (pax:method () (nat-decompose)))
   (num       (pax:method () (nat-eq)))
   (num       (pax:method () (nat-lt)))
+  (num       (pax:method () (nat-mod)))
 
   (nat-add         pax:function)
   (nat-mult        pax:function)
@@ -604,6 +615,7 @@ throughout any piece of code"
   (nat-decompose   pax:function)
   (nat-eq          pax:function)
   (nat-lt          pax:function)
+  (nat-mod         pax:function)
 
   (num          pax:generic-function)
   (pos          pax:generic-function)

src/specs/seqn-printer.lisp

@@ -30,3 +30,4 @@
 (easy-printer seqn-decompose)
 (easy-printer seqn-eq)
 (easy-printer seqn-lt)
+(easy-printer seqn-mod)

src/specs/seqn.lisp

@@ -4,7 +4,7 @@
   '(or composition id fork-seq drop-nil remove-right remove-left drop-width
     inj-length-left inj-length-right inj-size branch-seq shift-front zero-bit
     one-bit parallel-seq seqn-add seqn-subtract seqn-multiply seqn-divide
-    seqn-nat seqn-concat seqn-decompose seqn-lt seqn-eq))
+    seqn-nat seqn-concat seqn-decompose seqn-lt seqn-eq seqn-mod))
 
 (defclass <seqn> (geb.mixins:direct-pointwise-mixin cat-morph) ()
   (:documentation "Seqn is a category whose objects are finite sequences of natural numbers.
@@ -262,6 +262,15 @@ seqn-eq n : (n, n) -> (1, 0) with the intended semantics being
 that the morphism takes two n-bit integers and produces 1 iff the first
 one is less than the second"))
 
+(defclass seqn-mod (<seqn>)
+  ((mcar :initarg :mcar
+         :accessor mcar
+         :documentation ""))
+  (:documentation " The type signature of the morphism is
+seqn-mod n : (n, n) -> (n) with the intended semantics being
+that the morphism takes two n-bit integers and produces the
+modulo of the first integer by the second"))
+
 (serapeum:-> composition (<seqn> <seqn>) composition)
 (defun composition (mcar mcadr)
   (values
@@ -378,6 +387,11 @@ one is less than the second"))
   (values
    (make-instance 'seqn-lt :mcar mcar)))
 
+(serapeum:-> seqn-mod (fixnum) seqn-mod)
+(defun seqn-mod (mcar)
+  (values
+   (make-instance 'seqn-mod :mcar mcar)))
+
 (make-pattern composition mcar mcadr)
 (make-pattern id mcar)
 (make-pattern fork-seq mcar)
@@ -402,4 +416,5 @@ one is less than the second"))
 (make-pattern seqn-decompose)
 (make-pattern seqn-eq)
 (make-pattern seqn-lt)
+(make-pattern seqn-mod)
 

src/vampir/package.lisp

@@ -103,5 +103,8 @@
     :pwmod32
 
     :*range-n*
-    :range-n)))
+    :range-n
+
+    :*mod-n*
+    :mod-n)))