Skip to content

Commit

Permalink
Unify cast and coerce in preparation for adding uninterpreted functio…
Browse files Browse the repository at this point in the history 
…ns: coerce -> type-cast everywhere.
  • Loading branch information
@emina
emina committed Mar 1, 2016
1 parent b87450d commit 93e760a
Show file tree
Hide file tree
Showing 12 changed files with 49 additions and 233 deletions.
6 changes: 3 additions & 3 deletions rosette/base/adt/box.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
(require (for-syntax racket/syntax "../core/lift.rkt") racket/provide
"../core/safe.rkt" "generic.rkt"
(only-in "../core/effects.rkt" apply!)
(only-in "../core/type.rkt" define-lifted-type)
(only-in "../core/type.rkt" define-lifted-type type-cast)
(only-in "../core/equality.rkt" @eq? @equal?)
(only-in "../core/bool.rkt" instance-of? && ||)
(only-in "../core/union.rkt" union)
Expand Down Expand Up @@ -36,12 +36,12 @@
(box (apply merge* (for/list ([p ps]) (cons (car p) (unbox (cdr p)))))))]))

(define (@unbox b)
(match (coerce b @box? 'unbox)
(match (type-cast @box? b 'unbox)
[(box v) v]
[(union vs) (apply merge* (for/list ([gv vs]) (cons (car gv) (unbox (cdr gv)))))]))

(define (@set-box! b v)
(match (coerce b @box? 'set-box!)
(match (type-cast @box? b 'set-box!)
[(? box? x)
(apply! set-box! unbox x v)]
[(union vs)
Expand Down
19 changes: 10 additions & 9 deletions rosette/base/adt/list.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
(only-in "../core/real.rkt" @integer? @<= @< @= @> @+)
(only-in "../core/union.rkt" union union?)
(only-in "../core/merge.rkt" merge merge*)
(only-in "../core/type.rkt" subtype?))
(only-in "../core/type.rkt" subtype? type-cast))

(provide (filtered-out with@ (all-defined-out))
(rename-out [list @list] [null @null]))
Expand Down Expand Up @@ -123,7 +123,8 @@
[(proc init ... xs . rest)
(assert-arity-includes proc (+ (length (list init ...)) 1 (length rest)) (quote iterator))
(define name (quote iterator))
(let ([vs (cons (coerce xs @list? name) (map (curryr coerce @list? name) rest))])
(let ([vs (cons (type-cast @list? xs name)
(for/list ([r rest]) (type-cast @list? r name)))])
(if (andmap list? vs)
(apply iterator proc init ... vs)
(match (apply set-intersect (map lengths vs))
Expand Down Expand Up @@ -238,7 +239,7 @@
[(equal? (car l-rest) first-r) (rloop (cdr r))]
[else (loop (cdr l-rest))])))])))
(define (@do-remove* name equal? l r)
(match* ((coerce l @list? name) (coerce r @list? name))
(match* ((type-cast @list? l name) (type-cast @list? r name))
[((? list? vs) (? list? ws)) (do-remove* equal? vs ws)]
[((? list? vs) (union ws))
(higher-order/for [ws] #:lift (do-remove* equal? vs) #:enforce @list? #:name name)]
Expand Down Expand Up @@ -389,7 +390,7 @@
[(_ proc)
#`(define (#,(lift-id #'proc) xs pos)
(define name (object-name proc))
(match* (xs (coerce pos @integer? name))
(match* (xs (type-cast @integer? pos name))
[((union vs) (? number? idx))
(assert-bound [0 <= idx] name)
(apply merge* (assert-some
Expand Down Expand Up @@ -433,7 +434,7 @@
(define (@add-between l x #:splice? [sp? #f] #:before-first [bf '()] #:before-last [bl x] #:after-last [al '()])
(if (list? l)
(add-between l x #:splice? sp? #:before-first bf #:before-last bl #:after-last al)
(match (coerce l @list? 'add-between)
(match (type-cast @list? l 'add-between)
[(? list? vs) (add-between vs x #:splice? sp? #:before-first bf #:before-last bl #:after-last al)]
[(union vs) (merge** vs (add-between _ x #:splice? sp? #:before-first bf #:before-last bl #:after-last al))])))

Expand Down Expand Up @@ -478,13 +479,13 @@
(assert-arity-includes f 1 name)
(assert (@pair? xs) (argument-error name "(and/c list? (not/c empty?))" xs))

(let ([init-min-var (coerce (f (car xs)) @integer? name)])
(let ([init-min-var (type-cast @integer? (f (car xs)) name)])
(let loop ([min (car xs)]
[min-var init-min-var]
[xs (cdr xs)])
(@if (null? xs)
min
(let ([new-min (coerce (f (car xs)) @integer? name)])
(let ([new-min (type-cast @integer? (f (car xs)) name)])
(@if (cmp new-min min-var)
(loop (car xs) new-min (cdr xs))
(loop min min-var (cdr xs))))))))
Expand All @@ -503,7 +504,7 @@
(cons (@= i idx) (insert xs idx v)))))]
(define (@insert xs i v)
(or (and (list? xs) (number? i) (insert xs i v))
(match* ((coerce xs @list? 'insert) (coerce i @integer? 'insert))
(match* ((type-cast @list? xs 'insert) (type-cast @integer? i 'insert))
[((? list? xs) (? number? i)) (insert xs i v)]
[((? list? xs) i)
(assert-bound [0 @<= i @<= (length xs)] 'insert)
Expand All @@ -528,7 +529,7 @@
(cons (@= i idx) (replace xs idx v)))))]
(define (@replace xs i v)
(or (and (list? xs) (number? i) (replace xs i v))
(match* ((coerce xs @list? 'replace) (coerce i @integer? 'replace))
(match* ((type-cast @list? xs 'replace) (type-cast @integer? i 'replace))
[((? list? xs) (? number? i)) (replace xs i v)]
[((? list? xs) i)
(assert-bound [0 @<= i @< (length xs)] 'replace)
Expand Down
16 changes: 9 additions & 7 deletions rosette/base/adt/seq.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
racket/splicing racket/stxparam
(only-in racket/unsafe/ops [unsafe-car car] [unsafe-cdr cdr])
"../core/safe.rkt" "../core/lift.rkt"
(only-in "../core/type.rkt" type-cast)
(only-in "../core/bool.rkt" && or-|| ||)
(only-in "../core/real.rkt" @integer? @= @< @<=)
(only-in "../core/union.rkt" union union?)
Expand All @@ -21,7 +22,7 @@
(define-syntax lift/apply/higher-order
(syntax-rules (: ->)
[(_ applicator proc arg ... seq : name : racket-contract? -> rosette-contract?)
(match (coerce seq rosette-contract? name)
(match (type-cast rosette-contract? seq name)
[(? racket-contract? vs) (applicator proc arg ... vs)]
[(union vs) (higher-order/for (vs) #:lift (applicator proc arg ...) #:enforce rosette-contract? #:name name)])]
[(_ applicator proc arg ... seq : racket-contract? -> rosette-contract?)
Expand All @@ -38,7 +39,8 @@
#`(define (#,(lift-id #'proc) xs idx)
(if (and (racket-contract? xs) (number? idx))
(proc xs idx)
(match* ((coerce xs rosette-contract? (quote proc)) (coerce idx @integer? (quote proc)))
(match* ((type-cast rosette-contract? xs (quote proc))
(type-cast @integer? idx (quote proc)))
[((? racket-contract? vs) (? number? idx))
(proc vs idx)]
[((? racket-contract? vs) idx)
Expand Down Expand Up @@ -77,11 +79,11 @@
(define #,(lift-id #'proc)
(case-lambda
[() (racket-constructor)]
[(xs) (coerce xs rosette-contract? (quote proc))]
[(xs ys) (unsafe/append (coerce xs rosette-contract? (quote proc))
(coerce ys rosette-contract? (quote proc)))]
[(xs) (type-cast rosette-contract? xs (quote proc))]
[(xs ys) (unsafe/append (type-cast rosette-contract? xs (quote proc))
(type-cast rosette-contract? ys (quote proc)))]
[xss (for/fold ([out (racket-constructor)])
([xs (map (curryr coerce rosette-contract? (quote proc)) xss)])
([xs (for/list ([ys xss]) (type-cast rosette-contract? ys (quote proc)))])
(unsafe/append out xs))])))]))

(define-syntax (define/lift/split stx)
Expand All @@ -90,7 +92,7 @@
#`(define (#,(lift-id #'proc) xs idx)
(if (and (not (union? xs)) (number? idx))
(proc xs idx)
(match* (xs (coerce idx @integer? (quote proc)))
(match* (xs (type-cast @integer? idx (quote proc)))
[((not (? union?)) (? number? idx)) (proc xs idx)]
[(_ idx) (values (left xs idx) (right xs idx))])))]))

Expand Down
24 changes: 12 additions & 12 deletions rosette/base/adt/vector.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
(only-in "list.rkt" @list?)
(only-in "../form/control.rkt" @when)
(only-in "../core/effects.rkt" apply!)
(only-in "../core/term.rkt" define-lifted-type @any/c)
(only-in "../core/term.rkt" define-lifted-type @any/c type-cast)
(only-in "../core/equality.rkt" @eq? @equal?)
(only-in "../core/bool.rkt" instance-of? && ||)
(only-in "../core/real.rkt" @integer? @= @<= @< @- @+)
Expand Down Expand Up @@ -65,7 +65,7 @@
;(printf "vector-set! ~a ~a ~a\n" (eq-hash-code vec) idx val)
(if (and (vector? vec) (number? idx))
(apply! vector-set! vector-ref vec idx val)
(match* ((coerce vec @vector? 'vector-set!) (coerce idx @integer? 'vector-set!))
(match* ((type-cast @vector? vec 'vector-set!) (type-cast @integer? idx 'vector-set!))
[((? vector? vs) (? number? idx))
(apply! vector-set! vector-ref vs idx val)]
[((? vector? vs) idx)
Expand All @@ -87,7 +87,7 @@
(and (merge-set! (cdr v) idx val (car v)) (car v)))])))

(define (@vector-fill! vec val)
(match (coerce vec @vector? 'vector-fill!)
(match (type-cast @vector? vec 'vector-fill!)
[(? vector? vs)
(for ([i (in-range (vector-length vs))])
(apply! vector-set! vector-ref vs i val))]
Expand All @@ -114,18 +114,18 @@
[(dest dest-start src)
(@vector-copy! dest dest-start src 0)]
[(dest dest-start src src-start)
(let ([dest (coerce dest @vector? 'vector-copy!)]
[dest-start (coerce dest-start @integer? 'vector-copy!)]
[src (coerce src @vector? 'vector-copy!)]
[src-start (coerce src-start @integer? 'vector-copy!)])
(let ([dest (type-cast @vector? dest 'vector-copy!)]
[dest-start (type-cast @integer? dest-start 'vector-copy!)]
[src (type-cast @vector? src 'vector-copy!)]
[src-start (type-cast @integer? src-start 'vector-copy!)])
(for*/all ([d dest] [s src])
(@vector-copy! d dest-start s src-start (vector-length s))))]
[(dest dest-start src src-start src-end)
(let ([dest (coerce dest @vector? 'vector-copy!)]
[dest-start (coerce dest-start @integer? 'vector-copy!)]
[src (coerce src @vector? 'vector-copy!)]
[src-start (coerce src-start @integer? 'vector-copy!)]
[src-end (coerce src-end @integer? 'vector-copy!)])
(let ([dest (type-cast @vector? dest 'vector-copy!)]
[dest-start (type-cast @integer? dest-start 'vector-copy!)]
[src (type-cast @vector? src 'vector-copy!)]
[src-start (type-cast @integer? src-start 'vector-copy!)]
[src-end (type-cast @integer? src-end 'vector-copy!)])
(assert-bound [0 @<= dest-start] 'vector-copy)
(assert-bound [0 @<= src-start @<= src-end] 'vector-copy!)
(define len (@- src-end src-start))
Expand Down
2 changes: 1 addition & 1 deletion rosette/base/base.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@
; core/finitize.rkt
finitize current-bitwidth
; core/reflect.rkt
symbolics type? type-of coerce for/all for*/all
symbolics type? type-of type-cast for/all for*/all
term? constant? expression?
term expression constant term-type
term=? term->datum clear-terms! term-cache
Expand Down
5 changes: 3 additions & 2 deletions rosette/base/core/lift.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
(only-in racket/unsafe/ops [unsafe-car car] [unsafe-cdr cdr])
(only-in "merge.rkt" merge* unsafe-merge*)
(only-in "union.rkt" union)
(only-in "type.rkt" type-cast)
"safe.rkt")

(provide define/lift (for-syntax lift-id) merge+ merge** unsafe-merge** flat-pattern-contract
Expand Down Expand Up @@ -60,7 +61,7 @@
#`(define (#,(lift-id #'id) val)
(if (contracted? val)
(id val)
(match (coerce val rosette-type? (quote id))
(match (type-cast rosette-type? val (quote id))
[(? contracted? v) (id v)]
[(union vs) (apply merge* (assert-some
(for/list ([v vs] #:when (contracted? (cdr v)))
Expand All @@ -76,7 +77,7 @@
#`(define (#,(lift-id #'id) val)
(if (contracted? val)
(id val)
(match (coerce val rosette-type? (quote id))
(match (type-cast rosette-type? val (quote id))
[(? contracted? v) (id v)]
[(union vs) (apply merge* (assert-some
(for/list ([v vs] #:when (contracted? (cdr v)))
Expand Down
Loading

0 comments on commit 93e760a

Please sign in to comment.