From f372bdda3e97ce02134c7069a2508da56a743eb8 Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Sun, 5 Nov 2017 19:20:03 -0500 Subject: [PATCH] more general linear exp stx for props --- .../scribblings/reference/experimental.scrbl | 9 ++- .../typed-racket/private/parse-type.rkt | 62 +++++++++---------- .../typed-racket/rep/object-rep.rkt | 57 +++++++++-------- .../unit-tests/parse-type-tests.rkt | 4 ++ 4 files changed, 68 insertions(+), 64 deletions(-) diff --git a/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl index c589a617..85ca0a85 100644 --- a/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl +++ b/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 diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt index 160952dc..c68196cb 100644 --- a/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/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" diff --git a/typed-racket-lib/typed-racket/rep/object-rep.rkt b/typed-racket-lib/typed-racket/rep/object-rep.rkt index 8cfb4d17..1ef94a08 100644 --- a/typed-racket-lib/typed-racket/rep/object-rep.rkt +++ b/typed-racket-lib/typed-racket/rep/object-rep.rkt @@ -242,6 +242,12 @@ ;; ***************************************************************************** ;; 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) @@ -249,32 +255,33 @@ 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 diff --git a/typed-racket-test/unit-tests/parse-type-tests.rkt b/typed-racket-test/unit-tests/parse-type-tests.rkt index 343153f6..01477a17 100644 --- a/typed-racket-test/unit-tests/parse-type-tests.rkt +++ b/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)