more general linear exp stx for props

Author: Andrew Kent

typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl

@@ -72,11 +72,10 @@ on the values of terms.
            (linear-comp symbolic-object symbolic-object)]
           [linear-comp < <= = >= >]
           [symbolic-object exact-integer
-           linear-term
-           (+ linear-term linear-term ...)
-           (- linear-term linear-term ...)]
-          [linear-term symbolic-path
-           (* exact-integer symbolic-path)]
+           symbolic-path
+           (+ symbolic-object ...)
+           (- symbolic-object ...)
+           (* exact-integer symbolic-object)]
           [symbolic-path id
            (path-elem symbolic-path)]
           [path-elem car

typed-racket-lib/typed-racket/private/parse-type.rkt

@@ -401,20 +401,14 @@
 (define-syntax-class symbolic-object
   #:description "symbolic object"
   #:attributes (val)
-  (pattern (:+^ . body)
-           #:attr val (parse-linear-expression-body #'body #t))
-  (pattern (:-^ . body)
-           #:attr val (parse-linear-expression-body #'body #f))
-  (pattern (:*^ ~! n:exact-integer o:symbolic-object-w/o-lexp)
-           #:do [(define obj (attribute o.val))
-                 (define obj-ty (lookup-obj-type/lexical obj))]
-           #:fail-when (and (check-type-invariants-while-parsing?)
-                            (not (subtype obj-ty -Int)))
-           (format "terms in linear constraints must be integers, got ~a for ~a"
-                   obj-ty obj)
-           #:attr val (-lexp (list (syntax->datum #'n) (attribute o.val))))
   (pattern n:exact-integer
            #:attr val (-lexp (syntax->datum #'n)))
+  (pattern (:+^ ls:linear-expression ...)
+           #:attr val (combine-linear-expressions (attribute ls.val) #t))
+  (pattern (:-^ ls:linear-expression ...)
+           #:attr val (combine-linear-expressions (attribute ls.val) #f))
+  (pattern (:*^ ~! n:exact-integer o:linear-expression)
+           #:attr val (-lexp (list (syntax->datum #'n) (attribute o.val))))
   (pattern o:symbolic-object-w/o-lexp
            #:attr val (attribute o.val))
   )
@@ -457,31 +451,17 @@
                    obj-ty obj)
            #:attr val (-vec-len-of (attribute o.val))))
 
-(define (parse-linear-expression-body body plus?)
-  (syntax-parse body
-    [(t:linear-expression-term ts:linear-expression-term ...)
-     (cond
-       [plus?
-        (apply -lexp (attribute t.val) (attribute ts.val))]
-       [else
-        (apply -lexp
-               (attribute t.val)
-               (for/list ([term (in-list (attribute ts.val))])
-                 (scale-obj -1 term)))])]))
-
-(define-syntax-class linear-expression-term
-  #:description "symbolic object"
+(define-syntax-class linear-expression
+  #:description "linear expression"
   #:attributes (val)
-  (pattern (:*^ ~! coeff:exact-integer o:symbolic-object-w/o-lexp)
-           #:do [(define obj (attribute o.val))
-                 (define obj-ty (lookup-obj-type/lexical obj))]
-           #:fail-when (and (check-type-invariants-while-parsing?)
-                            (not (subtype obj-ty -Int)))
-           (format "terms in linear expressions must be integers, got ~a for ~a"
-                   obj-ty obj)
-           #:attr val (-lexp (list (syntax->datum #'coeff) (attribute o.val))))
   (pattern n:exact-integer
            #:attr val (-lexp (syntax-e (attribute n))))
+  (pattern (:+^ ls:linear-expression ...)
+           #:attr val (combine-linear-expressions (attribute ls.val) #t))
+  (pattern (:-^ ls:linear-expression ...)
+           #:attr val (combine-linear-expressions (attribute ls.val) #f))
+  (pattern (:*^ ~! coeff:exact-integer l:linear-expression)
+           #:attr val (-lexp (list (syntax->datum #'coeff) (attribute l.val))))
   (pattern o:symbolic-object-w/o-lexp
            #:do [(define obj (attribute o.val))
                  (define obj-ty (lookup-obj-type/lexical obj))]
@@ -492,6 +472,20 @@
            #:attr val (attribute o.val))
   )
 
+;; [Listof Object?] boolean? -> Object?
+;; create (+ linear-exps ...) or (- linear-exps ...)
+(define (combine-linear-expressions linear-exps plus?)
+  (cond
+    [(null? linear-exps) (-lexp 0)]
+    [plus?
+     (apply -lexp linear-exps)]
+    [else
+     (apply -lexp
+            (car linear-exps)
+            (for/list ([term (in-list (cdr linear-exps))])
+              (scale-obj -1 term)))]))
+
+
 ;; old + deprecated
 (define-syntax-class (legacy-prop doms)
   #:description "proposition"

typed-racket-lib/typed-racket/rep/object-rep.rkt

@@ -242,39 +242,46 @@
 ;; *****************************************************************************
 ;; Operations for Linear Expressions
 
+;; adds two sets of terms -- used in a few cases
+;; for -lexp below
+(define-syntax-rule (add-terms ts ts*)
+  (for/fold ([ts ts])
+            ([(p coeff) (in-terms ts*)])
+    (terms-set ts p (+ coeff (terms-ref ts p)))))
 
 ;; constructor for LExps
 (define/cond-contract (-lexp . raw-terms)
   (->* () () #:rest (listof (or/c exact-integer?
                                   name-ref/c
                                   Path?
                                   LExp?
-                                  (list/c exact-integer? (or/c name-ref/c Path?))))
+                                  (list/c exact-integer? (or/c name-ref/c Path? LExp?))))
        (or/c LExp? Path?))
-  (define-values (const terms)
-    (for/fold ([c 0] [ts (make-terms)])
-              ([term (in-list raw-terms)])
-      (match term
-        [(list (? exact-integer? coeff) (? Path? p))
-         (values c (terms-set ts p (+ coeff (terms-ref ts p))))]
-        [(list (? exact-integer? coeff) (? name-ref/c nm))
-         (let ([p (-id-path nm)])
-           (if (Empty? nm)
-               (values c ts)
-               (values c (terms-set ts p (+ coeff (terms-ref ts p))))))]
-        [(? exact-integer? new-const)
-         (values (+ new-const c) ts)]
-        [(LExp: c* ts*)
-         (values (+ c c*)
-                 (for/fold ([ts ts])
-                           ([(p coeff) (in-terms ts*)])
-                   (terms-set ts p (+ coeff (terms-ref ts p)))))]
-        [(? Object? p)
-         (values c (terms-set ts p (add1 (terms-ref ts p))))]
-        [(? name-ref/c var)
-         (define p (-id-path var))
-         (values c (terms-set ts p (add1 (terms-ref ts p))))])))
-  (make-LExp* const terms))
+  (for/fold ([c 0]
+             [ts (make-terms)]
+             #:result (make-LExp* c ts))
+            ([term (in-list raw-terms)])
+    (match term
+      [(list (? exact-integer? coeff) (? Path? p))
+       (values c (terms-set ts p (+ coeff (terms-ref ts p))))]
+      [(list (? exact-integer? coeff) (? name-ref/c nm))
+       (let ([p (-id-path nm)])
+         (if (Empty? nm)
+             (values c ts)
+             (values c (terms-set ts p (+ coeff (terms-ref ts p))))))]
+      [(? exact-integer? new-const)
+       (values (+ new-const c) ts)]
+      [(LExp: c* ts*)
+       (values (+ c c*) (add-terms ts ts*))]
+      [(list (? exact-integer? l-coeff) (? LExp? l))
+       (match (scale-obj l-coeff l)
+         [(LExp: c* ts*)
+          (values (+ c c*) (add-terms ts ts*))])]
+      [(? Object? p)
+       (values c (terms-set ts p (add1 (terms-ref ts p))))]
+      [(? name-ref/c var)
+       (define p (-id-path var))
+       (values c (terms-set ts p (add1 (terms-ref ts p))))])))
 
 
 ;; LExp-add1

typed-racket-test/unit-tests/parse-type-tests.rkt

@@ -497,6 +497,10 @@
    [(Refine [x : Integer] (> x 42))
     (-refine/fresh x -Int (-leq (-lexp 43)
                                 (-lexp x)))]
+   [(Refine [n : Integer] (<= (- (+ n n) (* 1 (+ n)))
+                              (+ 2 (- 80 (* 2 (+ 9 9 (+) (-) 2))))))
+    (-refine/fresh x -Int (-leq (-lexp x)
+                                (-lexp 42)))]
    ;; id shadowing
    [(Refine [x : Any] (: x (Refine [x : Integer] (<= x 42))))
     (-refine/fresh x -Int (-leq (-lexp x)