suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

more general linear exp stx for props

Browse Source
This commit is contained in:
Andrew Kent 2017-11-05 19:20:03 -05:00 committed by GitHub
parent 1a042f8520
commit f372bdda3e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 68 additions and 64 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl
View File

@ -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

62
typed-racket-lib/typed-racket/private/parse-type.rkt
View File

@ -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"

57
typed-racket-lib/typed-racket/rep/object-rep.rkt
View File

@ -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

4
typed-racket-test/unit-tests/parse-type-tests.rkt
View File

@ -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)