cs: reimplement the predicate lattice in cptypes

Clean up the implementation. For example predicate-union was
calling predicate-implies? like 20 times. With the new
implementation this can be done in a single pass.

Also, this changes the results of the functions for 'bottom and
#f so they behave like sets. So this removes some special cases
and makes the functions more consistent.
This commit is contained in:
Gustavo Massaccesi 2021-01-20 16:24:47 -03:00
parent ad6bbe9809
commit 0ff8d18be5
5 changed files with 739 additions and 166 deletions

View File

@ -558,11 +558,14 @@
(mat cptypes-type-implies?
(test-chain '((lambda (x) (eq? x 0)) fixnum? #;exact-integer? real? number?))
(test-chain* '((lambda (x) (or (eq? x 0) (eq? x 10))) fixnum? #;exact-integer? real? number?))
(test-chain* '(fixnum? integer? real?))
(test-chain* '(fixnum? exact? number?)) ; exact? may raise an error
(test-chain* '(bignum? exact? number?)) ; exact? may raise an error
(test-chain* '((lambda (x) (eq? x (expt 256 100))) bignum? real? number?))
(test-chain '((lambda (x) (eqv? 0.0 x)) flonum? real? number?))
(test-chain* '((lambda (x) (or (eqv? x 0.0) (eqv? x 3.14))) flonum? real? number?))
(test-chain* '((lambda (x) (or (eq? x 0) (eqv? x 3.14))) real? number?))
(test-chain '(gensym? symbol?))
(test-chain '(not boolean?))
(test-chain '((lambda (x) (eq? x #t)) boolean?))

View File

@ -169,7 +169,7 @@ macroobj =\
allsrc =\
${basesrc} ${compilersrc} cmacros.ss ${archincludes} setup.ss debug.ss priminfo.ss primdata.ss layout.ss\
base-lang.ss expand-lang.ss primref.ss types.ss io-types.ss fasl-helpers.ss hashtable-types.ss\
np-languages.ss fxmap.ss strip-types.ss
np-languages.ss fxmap.ss cptypes-lattice.ss strip-types.ss
# doit uses a different Scheme process to compile each target
doit: ${PetiteBoot} ${SchemeBoot} ${Cheader} ${Cequates} ${Cgcocd} ${Cgcoce} ${Cgcpar} ${Cheapcheck} ${Revision}
@ -595,9 +595,9 @@ setup.so: debug.ss
strip.so: strip-types.ss
vfasl.so: strip-types.ss
${patchobj}: ${macroobj} nanopass.so base-lang.ss expand-lang.ss primref.ss types.ss io-types.ss fasl-helpers.ss hashtable-types.ss strip-types.ss env.ss
cpnanopass.$m cpnanopass.patch: nanopass.so np-languages.ss fxmap.ss ${archincludes}
cptypes.$m: fxmap.ss
${patchobj}: ${macroobj} nanopass.so base-lang.ss expand-lang.ss primref.ss types.ss io-types.ss fasl-helpers.ss hashtable-types.ss strip-types.ss env.ss fxmap.ss cptypes-lattice.ss
cpnanopass.$m cpnanopass.patch: nanopass.so np-languages.ss ${archincludes}
cptypes.$m: fxmap.ss cptypes-lattice.ss
5_4.$m: ../unicode/unicode-char-cases.ss ../unicode/unicode-charinfo.ss
strip.$m: strip-types.ss
vfasl.$m: strip-types.ss

View File

@ -0,0 +1,699 @@
;;; cptypes-lattice.ss
;;; Copyright 1984-2020 Cisco Systems, Inc.
;;;
;;; Licensed under the Apache License, Version 2.0 (the "License");
;;; you may not use this file except in compliance with the License.
;;; You may obtain a copy of the License at
;;;
;;; http://www.apache.org/licenses/LICENSE-2.0
;;;
;;; Unless required by applicable law or agreed to in writing, software
;;; distributed under the License is distributed on an "AS IS" BASIS,
;;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
;;; See the License for the specific language governing permissions and
;;; limitations under the License.
; bottom -> empty set / the expression raised an error
; <something> -> some other set
; ptr -> all single values expressions
; #f -> a result that may be single or multiple valued.
; bottom => <something> => ptr => #f
; properties of bottom:
; (implies? x bottom): only for x=bottom
; (implies? bottom y): always
; (disjoint? x bottom): always
; (disjoint? bottom y): always
; remember to check (implies? x bottom) before (implies? x something)
(module cptypes-lattice
(predicate-implies?
predicate-disjoint?
predicate-intersect
predicate-union
make-pred-$record/rtd
make-pred-$record/ref)
(include "base-lang.ss")
(with-output-language (Lsrc Expr)
(define true-rec `(quote #t)))
; don't use rtd-* as defined in record.ss in case we're building a patch
; file for cross compilation, because the offsets may be incorrect
(define rtd-ancestors (csv7:record-field-accessor #!base-rtd 'ancestors))
(define (rtd-parent x) (vector-ref (rtd-ancestors x) 0))
;(define (rtd-ancestry x) ($object-ref 'scheme-object x (constant record-type-ancestry-disp)))
;(define (rtd-parent x) (vector-ref (rtd-ancestry x) 0))
(define-record-type pred-$record/rtd
(fields rtd)
(nongenerative #{pred-$record/rtd wnquzwrp8wl515lhz2url8sjc-0})
(sealed #t))
(define-record-type pred-$record/ref
(fields ref)
(nongenerative #{pred-$record/ref zc0e8e4cs8scbwhdj7qpad6k3-0})
(sealed #t))
(define (check-constant-is? x pred?)
(and (Lsrc? x)
(nanopass-case (Lsrc Expr) x
[(quote ,d) (pred? d)]
[else #f])))
(define (check-constant-eqv? x v)
(and (Lsrc? x)
(nanopass-case (Lsrc Expr) x
[(quote ,d) (eqv? d v)]
[else #f])))
;only false-rec, boolean and ptr may be '#f
;use when the other argument is truthy bur not exactly '#t
(define (union/true x)
(cond
[(or (eq? x 'boolean)
(check-constant-eqv? x #f))
'ptr]
[else
'true]))
(define (union/simple x pred? y)
(cond
[(or (check-constant-is? x pred?)
(eq? x y))
y]
[else
(union/true x)]))
(define (union/symbol x pred? y)
(cond
[(or (check-constant-is? x pred?)
(eq? x y))
y]
[(or (eq? x 'gensym)
(eq? x 'interned-symbol)
(eq? x 'uninterned-symbol)
(eq? x 'symbol)
(check-constant-is? x symbol?))
'symbol]
[else
(union/true x)]))
(define (union/record x)
(cond
[(or (pred-$record/rtd? x)
(pred-$record/ref? x)
(eq? x '$record))
'$record]
[else
(union/true x)]))
(define (union/fixnum x)
(cond
[(check-constant-is? x target-fixnum?)
'fixnum]
[(or (eq? x 'bignum)
(eq? x 'exact-integer)
(check-constant-is? x exact-integer?))
'exact-integer]
[(or (eq? x 'flonum)
(eq? x 'real)
(check-constant-is? x real?))
'real]
[(or (eq? x 'number)
(check-constant-is? x number?))
'number]
[else
(union/true x)]))
(define (union/bignum x)
(cond
[(check-constant-is? x target-bignum?)
'bignum]
[(or (eq? x 'fixnum)
(eq? x 'exact-integer)
(check-constant-is? x exact-integer?))
'exact-integer]
[(or (eq? x 'flonum)
(eq? x 'real)
(check-constant-is? x real?))
'real]
[(or (eq? x 'number)
(check-constant-is? x number?))
'number]
[else
(union/true x)]))
(define (union/exact-integer x)
(cond
[(or (eq? x 'fixnum)
(eq? x 'bignum)
(check-constant-is? x exact-integer?))
'exact-integer]
[(or (eq? x 'flonum)
(eq? x 'real)
(check-constant-is? x real?))
'real]
[(or (eq? x 'number)
(check-constant-is? x number?))
'number]
[else
(union/true x)]))
(define (union/flonum x)
(cond
[(or (check-constant-is? x flonum?))
'flonum]
[(or (eq? x 'real)
(check-constant-is? x real?))
'real]
[(or (eq? x 'number)
(check-constant-is? x number?))
'number]
[else
(union/true x)]))
(define (union/real x)
(cond
[(or (eq? x 'fixnum)
(eq? x 'bignum)
(eq? x 'exact-integer)
(eq? x 'flonum)
(check-constant-is? x real?))
'real]
[(or (eq? x 'number)
(check-constant-is? x number?))
'number]
[else
(union/true x)]))
(define (union/number x)
(cond
[(or (eq? x 'fixnum)
(eq? x 'bignum)
(eq? x 'exact-integer)
(eq? x 'flonum)
(eq? x 'real)
(check-constant-is? x number?))
'number]
[else
(union/true x)]))
;true when x is an ancestor of y
;includes the case when the are the same
(define (rtd-ancestor*? x y)
(or (eq? x y)
(let ()
(define ax (rtd-ancestors x))
(define lx (vector-length ax))
(define ay (rtd-ancestors y))
(define ly (vector-length ay))
(let ([pos (fx- ly lx 1)])
(and (fx>= pos 0)
(eq? x (vector-ref ay pos)))))))
;includes the case when the are the same
;or when one is the ancester of the other
(define (rdt-last-common-ancestor* x y)
(cond
[(eq? x y) x]
[else
(let ()
(define ax (rtd-ancestors x))
(define lx (vector-length ax))
(define ay (rtd-ancestors y))
(define ly (vector-length ay))
(cond
[(let ([pos (fx- ly lx 1)])
(and (fx>= pos 0)
(eq? x (vector-ref ay pos))))
x]
[(let ([pos (fx- lx ly 1)])
(and (fx>= pos 0)
(eq? y (vector-ref ax pos))))
y]
[(fx= lx 1) #f]
[(fx= ly 1) #f]
[else
(let ()
(define offset (fx- lx ly))
(define f (if (fx< lx ly) (fx- offset) 0))
(define l (fx- ly 1))
(cond
[(eq? (vector-ref ay f)
(vector-ref ax (fx+ f offset)))
(vector-ref ay f)]
[else
(let loop ([f f] [l l])
(cond
[(fx= (fx- l f) 1) (vector-ref ay l)]
[else
(let ()
(define m (fxquotient (fx+ f l) 2))
(if (eq? (vector-ref ay m)
(vector-ref ax (fx+ m offset)))
(loop f m)
(loop m l)))]))]))]))]))
(define (exact-integer? x)
(and (integer? x) (exact? x)))
(define (interned-symbol? x)
(and (symbol? x)
(not (gensym? x))
(not (uninterned-symbol? x))))
;If x and y are equivalent, they result must be eq? to y
;so it's easy to test in predicate-implies?.
;The result may be bigger than the actual union.
(define (predicate-union x y)
(cond
[(eq? x y) y]
[(not x) #f] ;possible a multivalued expression
[(not y) #f] ;possible a multivalued expression
[(eq? x 'bottom) y]
[(eq? y 'bottom) x]
[(eq? y 'ptr) y]
[(eq? x 'ptr) x]
[(Lsrc? y)
(nanopass-case (Lsrc Expr) y
[(quote ,d1)
(define dy d1)
(cond
[(check-constant-eqv? x dy)
y]
[(not dy)
(cond
[(or (eq? x 'boolean)
(check-constant-eqv? x #t))
'boolean]
[else
'ptr])]
[(eq? dy #t)
(cond
[(or (eq? x 'boolean)
(check-constant-eqv? x #f))
'boolean]
[else
'true])]
[(null? dy)
(cond
[(or (eq? x 'null-or-pair)
(eq? x 'pair))
'null-or-pair]
[else
(union/true x)])]
[(fixnum? dy)
(union/fixnum x)]
[(bignum? dy)
(union/bignum x)]
[(exact-integer? dy)
(union/exact-integer x)]
[(flonum? dy)
(union/flonum x)]
[(real? dy)
(union/real x)]
[(number? dy)
(union/number x)]
[(gensym? dy) (union/symbol x gensym? 'gensym)]
[(uninterned-symbol? dy) (union/symbol x uninterned-symbol? 'uninterned-symbol)]
[(interned-symbol? dy) (union/symbol x interned-symbol? 'interned-symbol)]
[(char? dy) (union/simple x char? 'char)]
[(vector? dy) (union/simple x vector? 'vector)]; i.e. #()
[(string? dy) (union/simple x string? 'string)]; i.e. ""
[(bytevector? dy) (union/simple x bytevector? 'bytevector)] ; i.e. '#vu8()
[(fxvector? dy) (union/simple x fxvector? 'fxvector)] ; i.e. '#vfx()
[(flvector? dy) (union/simple x flvector? 'flvector)] ; i.e. '#vfl()
[else
(union/true x)])])]
[(pred-$record/rtd? y)
(cond
[(pred-$record/rtd? x)
(let ([x-rtd (pred-$record/rtd-rtd x)]
[y-rtd (pred-$record/rtd-rtd y)])
(cond
[(eqv? x-rtd y-rtd)
y]
[(record-type-sealed? x-rtd)
(if (rtd-ancestor*? y-rtd x-rtd) y '$record)]
[(record-type-sealed? y-rtd)
(if (rtd-ancestor*? x-rtd y-rtd) x '$record)]
[else
(let ([lca-rtd (rdt-last-common-ancestor* x-rtd y-rtd)])
(cond
[(not lca-rtd) '$record]
[(eqv? lca-rtd y-rtd) y]
[(eqv? lca-rtd x-rtd) x]
[else (make-pred-$record/rtd lca-rtd)]))]))]
[else (union/record x)])]
[(pred-$record/ref? y)
(cond
[(pred-$record/ref? x)
(if (eq? (pred-$record/ref-ref x)
(pred-$record/ref-ref y))
y
'$record)]
[else (union/record x)])]
[else
(case y
[($record)
(union/record x)] ; y must be the symbol '$record
[(null-or-pair)
(cond
[(or (eq? x 'pair)
(check-constant-eqv? x '()))
y]
[else (union/true x)])]
[(pair)
(cond
[(or (eq? x 'null-or-pair)
(check-constant-eqv? x '()))
'null-or-pair]
[else
(union/true x)])]
[(fixnum)
(union/fixnum x)]
[(bignum)
(union/bignum x)]
[(exact-integer)
(union/exact-integer x)]
[(flonum)
(union/flonum x)]
[(real)
(union/real x)]
[(number)
(union/number x)]
[(gensym)
(union/symbol x gensym? 'gensym)]
[(uninterned-symbol)
(union/symbol x uninterned-symbol? 'uninterned-symbol)]
[(interned-symbol)
(union/symbol x interned-symbol? 'interned-symbol)]
[(symbol)
(union/symbol x symbol? 'symbol)]
[(boolean)
(cond
[(check-constant-is? x boolean?)
y]
[else
'ptr])]
[(char) (union/simple x char? y)]
[(vector) (union/simple x vector? y)]; i.e. #()
[(string) (union/simple x string? y)]; i.e. ""
[(bytevector) (union/simple x bytevector? y)] ; i.e. '#vu8()
[(fxvector) (union/simple x fxvector? y)] ; i.e. '#vfx()
[(flvector) (union/simple x flvector? y)] ; i.e. '#vfl()
[else (union/true x)])]))
(define (intersect/simple x pred? qpred y)
(cond
[(and pred? (check-constant-is? x pred?))
x]
[(or (eq? x qpred)
(eq? x 'true))
y]
[else
'bottom]))
(define (intersect/record x y)
(cond
[(or (pred-$record/ref? x)
(pred-$record/rtd? x))
x]
[(or (eq? x '$record)
(eq? x 'true))
y]
[else
'bottom]))
(define (intersect/symbol x pred? qpred y)
(cond
[(and pred? (check-constant-is? x pred?))
x]
[(or (eq? x qpred)
(eq? x 'symbol)
(eq? x 'true))
y]
[else
'bottom]))
(define (intersect/fixnum x check? y)
(cond
[(and check? (check-constant-is? x fixnum?))
x]
[(or (eq? x 'fixnum)
(eq? x 'exact-integer)
(eq? x 'real)
(eq? x 'number)
(eq? x 'true))
y]
[else
'bottom]))
(define (intersect/bignum x check? y)
(cond
[(and check? (check-constant-is? x bignum?))
x]
[(or (eq? x 'bignum)
(eq? x 'exact-integer)
(eq? x 'real)
(eq? x 'number)
(eq? x 'true))
y]
[else
'bottom]))
(define (intersect/exact-integer x check? y)
(cond
[(and check? (or (check-constant-is? x exact-integer?)
(eq? x 'fixnum)
(eq? x 'bignum)))
x]
[(or (eq? x 'exact-integer)
(eq? x 'real)
(eq? x 'number)
(eq? x 'true))
y]
[else
'bottom]))
(define (intersect/flonum x check? y)
(cond
[(and check? (check-constant-is? x flonum?))
x]
[(or (eq? x 'flonum)
(eq? x 'real)
(eq? x 'number)
(eq? x 'true))
y]
[else
'bottom]))
(define (intersect/real x check? y)
(cond
[(and check? (or (check-constant-is? x real?)
(eq? x 'fixnum)
(eq? x 'bignum)
(eq? x 'exact-integer)
(eq? x 'flonum)))
x]
[(or (eq? x 'real)
(eq? x 'number)
(eq? x 'true))
y]
[else
'bottom]))
(define (intersect/number x check? y)
(cond
[(and check? (eq? x 'fixnum))
x]
[(and check? (or (check-constant-is? x number?)
(eq? x 'fixnum)
(eq? x 'bignum)
(eq? x 'exact-integer)
(eq? x 'flonum)
(eq? x 'real)))
x]
[(or (eq? x 'number)
(eq? x 'true))
y]
[else
'bottom]))
;The result may be bigger than the actual intersection
;if there is no exact result, it must be at least included in x
;so it's possible to make decreasing sequences.
;Anyway, for now the result is exact.
(define (predicate-intersect x y)
(cond
[(eq? x y) x]
[(not y) x]
[(not x) y]
[(eq? y 'bottom) 'bottom]
[(eq? x 'bottom) 'bottom]
[(eq? y 'ptr) x]
[(eq? x 'ptr) y]
[(Lsrc? y)
(nanopass-case (Lsrc Expr) y
[(quote ,d1)
(define dy d1)
(cond
[(check-constant-eqv? x dy)
x]
[(not dy)
(cond
[(eq? x 'boolean)
y]
[else
'bottom])]
[(eq? dy #t)
(cond
[(or (eq? x 'boolean)
(eq? x 'true))
y]
[else
'bottom])]
[(null? dy)
(cond
[(or (eq? x 'null-or-pair)
(eq? x 'true))
y]
[else
'bottom])]
[(fixnum? dy)
(intersect/fixnum x #f y)]
[(bignum? dy)
(intersect/bignum x #f y)]
[(exact-integer? dy)
(intersect/exact-integer x #f y)]
[(flonum? dy)
(intersect/flonum x #f y)]
[(real? dy)
(intersect/real x #f y)]
[(number? dy)
(intersect/number x #f y)]
[(gensym? dy) (intersect/symbol x #f 'gensym y)]
[(uninterned-symbol? dy) (intersect/symbol x #f 'uninterned-symbol y)]
[(interned-symbol? dy) (intersect/symbol x #f 'interned-symbol y)]
[(char? dy) (intersect/simple x #f 'char y)]
[(vector? dy) (intersect/simple x #f 'vector y)]; i.e. #()
[(string? dy) (intersect/simple x #f 'string y)]; i.e. ""
[(bytevector? dy) (intersect/simple x bytevector? 'bytevector y)] ; i.e. '#vu8()
[(fxvector? dy) (intersect/simple x #f 'fxvector y)] ; i.e. '#vfx()
[(flvector? dy) (intersect/simple x #f 'flvector y)] ; i.e. '#vfl()
[else
(cond
[(eq? x 'true)
y]
[else
'bottom])])])]
[(pred-$record/rtd? y)
(cond
[(pred-$record/rtd? x)
(let ([x-rtd (pred-$record/rtd-rtd x)]
[y-rtd (pred-$record/rtd-rtd y)])
(cond
[(eqv? x-rtd y-rtd)
x]
[(record-type-sealed? x-rtd)
(if (rtd-ancestor*? y-rtd x-rtd) x 'bottom)]
[(record-type-sealed? y-rtd)
(if (rtd-ancestor*? x-rtd y-rtd) y 'bottom)]
[else
(cond
[(rtd-ancestor*? y-rtd x-rtd) x]
[(rtd-ancestor*? x-rtd y-rtd) y]
[else 'bottom])]))]
[else
(intersect/record x y)])]
[(pred-$record/ref? y)
(intersect/record x y)]
[else
(case y
[($record)
(intersect/record x y)]
[(null-or-pair)
(cond
[(eq? x 'pair)
'pair]
[(check-constant-eqv? x '())
x]
[(eq? x 'true)
'null-or-pair]
[else 'bottom])]
[(pair)
(cond
[(or (eq? x 'null-or-pair)
(eq? x 'true))
'pair]
[else
'bottom])]
[(fixnum)
(intersect/fixnum x #t y)]
[(bignum)
(intersect/bignum x #t y)]
[(exact-integer)
(intersect/exact-integer x #t y)]
[(flonum)
(intersect/flonum x #t y)]
[(real)
(intersect/real x #t y)]
[(number)
(intersect/number x #t y)]
[(gensym)
(intersect/symbol x gensym? 'gensym y)]
[(uninterned-symbol)
(intersect/symbol x uninterned-symbol? 'uninterned-symbol y)]
[(interned-symbol)
(intersect/symbol x interned-symbol? 'interned-symbol y)]
[(symbol)
(cond
[(or (eq? x 'gensym)
(eq? x 'uninterned-symbol)
(eq? x 'interned-symbol)
(eq? x 'symbol)
(eq? x 'true)
(check-constant-is? x symbol?))
x]
[else
'bottom])]
[(boolean)
(cond
[(eq? x 'true)
true-rec]
[(check-constant-is? x boolean?)
x]
[else
'bottom])]
[(true)
(cond
[(eq? x 'boolean)
true-rec]
[(check-constant-eqv? x #f)
'bottom]
[else
x])]
[(char) (intersect/simple x char? 'char y)]
[(vector) (intersect/simple x vector? 'vector y)]; i.e. #()
[(string) (intersect/simple x string? 'string y)]; i.e. ""
[(bytevector) (intersect/simple x bytevector? 'bytevector y)] ; i.e. '#vu8()
[(fxvector) (intersect/simple x fxvector? 'fxvector y)] ; i.e. '#vfx()
[(flvector) (intersect/simple x flvector? 'flvector y)] ; i.e. '#vfl()
[else
(cond
[(eq? x 'true)
y]
[else
'bottom])])]))
(define (predicate-implies? x y)
(eq? (predicate-union x y) y))
(define (predicate-disjoint? x y)
(eq? (predicate-intersect x y) 'bottom))
)

View File

@ -61,6 +61,11 @@ Notes:
- Most of the time I'm using eq? and eqv? as if they were equivalent.
I assume that the differences are hidden by unspecified behavior.
- The result of predicate-union may be bigger than the actual union.
- The result of predicate-intersect is exact for now, but it may change in the future.
In that case it's necesary to ensure that the order of the arguments is correct
to make decreasing sequences of predicates.
|#
@ -69,6 +74,8 @@ Notes:
(import (nanopass))
(include "base-lang.ss")
(include "fxmap.ss")
(include "cptypes-lattice.ss")
(import cptypes-lattice)
(define (prelex-counter x plxc)
(or (prelex-operand x)
@ -287,22 +294,13 @@ Notes:
(loop (car e*) (cdr e*)))))]))
)
(define-record-type pred-$record/rtd
(fields rtd)
(nongenerative #{pred-$record/rtd wnquzwrp8wl515lhz2url8sjc-0})
(sealed #t))
(define-record-type pred-$record/ref
(fields ref)
(nongenerative #{pred-$record/ref zc0e8e4cs8scbwhdj7qpad6k3-0})
(sealed #t))
(module (pred-env-empty pred-env-bottom
pred-env-add pred-env-remove/base pred-env-lookup
pred-env-intersect/base pred-env-union/super-base
pred-env-rebase
pred-intersect pred-union)
predicate-intersect predicate-union)
(import fxmap)
(import cptypes-lattice)
; a fake fxmap that is full of 'bottom
(define-record-type $bottom
@ -324,7 +322,7 @@ Notes:
(cond
[(not old)
(fxmap-set types key pred)]
[else (let ([new (pred-intersect old pred)])
[else (let ([new (predicate-intersect old pred)])
(cond
[(eq? new old) types]
[(eq? new 'bottom) bottom-fxmap]
@ -366,6 +364,7 @@ Notes:
(eq? from bottom-fxmap))
bottom-fxmap]
[(fx> (fxmap-changes from) (fxmap-changes types))
;TODO: don't swap the order in case the result of predicate-intersect is not exact.
(pred-env-intersect/base from types base)]
[else
(let ([ret types])
@ -374,7 +373,7 @@ Notes:
;x-> from
;y-> base
;z-> types
(set! ret (pred-env-add/key ret key (pred-intersect x z)))))
(set! ret (pred-env-add/key ret key (predicate-intersect x z)))))
(lambda (key x)
(set! ret (pred-env-add/key ret key x)))
(lambda (key x)
@ -383,18 +382,6 @@ Notes:
base)
ret)]))
(define (pred-intersect x y)
(cond
[(predicate-implies? x y) x]
[(predicate-implies? y x) y]
[(or (predicate-implies-not? x y)
(predicate-implies-not? y x))
'bottom]
[(or (and (eq? x 'boolean) (eq? y 'true))
(and (eq? y 'boolean) (eq? x 'true)))
true-rec]
[else (or x y)])) ; if there is no exact option, at least keep the old value
; This is conceptually the union of the types in `types` and `from`
; but since 'ptr is not stored to save space and time, the implementation
; looks like an intersection of the fxmaps.
@ -411,12 +398,12 @@ Notes:
;x-> from
;y-> base
;z-> types
(set! ret (pred-env-add/key ret key (pred-union x z)))))
(set! ret (pred-env-add/key ret key (predicate-union x z)))))
(lambda (key x)
(let ([z (fxmap-ref types key #f)])
;x-> from
;z-> types
(set! ret (pred-env-add/key ret key (pred-union x z)))))
(set! ret (pred-env-add/key ret key (predicate-union x z)))))
(lambda (key x)
($impoops 'pred-env-union/from "unexpected value ~s in base environment ~s" x base))
from
@ -453,19 +440,6 @@ Notes:
; temp is never bottom-fxmap here
($pred-env-union/from types types/b from temp))]))]))
(define (pred-union x y)
(cond
[(predicate-implies? y x) x]
[(predicate-implies? x y) y]
[(find (lambda (t)
(and (predicate-implies? x t)
(predicate-implies? y t)))
'(char null-or-pair $record
gensym uninterned-symbol interned-symbol symbol
fixnum bignum exact-integer flonum real number
boolean true ptr))] ; ensure they are order from more restrictive to less restrictive
[else #f]))
(define (pred-env-rebase types base new-base)
(cond
[(or (eq? types bottom-fxmap)
@ -679,108 +653,6 @@ Notes:
[(quote ,d) (pred? d)]
[else #f]))
; strange properties of bottom here:
; (implies? x bottom): only for x=bottom
; (implies? bottom y): always
; (implies-not? x bottom): never
; (implies-not? bottom y): never
; check (implies? x bottom) before (implies? x something)
(define (predicate-implies? x y)
(and x
y
(or (eq? x y)
(eq? x 'bottom)
(cond
[(Lsrc? y)
(and (Lsrc? x)
(nanopass-case (Lsrc Expr) y
[(quote ,d1)
(nanopass-case (Lsrc Expr) x
[(quote ,d2) (eqv? d1 d2)]
[else #f])]
[else #f]))]
[(pred-$record/rtd? y)
(and (pred-$record/rtd? x)
(let ([x-rtd (pred-$record/rtd-rtd x)]
[y-rtd (pred-$record/rtd-rtd y)])
(cond
[(record-type-sealed? y-rtd)
(eqv? x-rtd y-rtd)]
[else
(let loop ([x-rtd x-rtd])
(or (eqv? x-rtd y-rtd)
(let ([xp-rtd (record-type-parent x-rtd)])
(and xp-rtd (loop xp-rtd)))))])))]
[(pred-$record/ref? y)
(and (pred-$record/ref? x)
(eq? (pred-$record/ref-ref x)
(pred-$record/ref-ref y)))]
[(case y
[(null-or-pair) (or (eq? x 'pair)
(check-constant-is? x null?))]
[(fixnum) (check-constant-is? x target-fixnum?)]
[(bignum) (check-constant-is? x target-bignum?)]
[(exact-integer)
(or (eq? x 'fixnum)
(eq? x 'bignum)
(check-constant-is? x (lambda (x) (and (integer? x)
(exact? x)))))]
[(flonum) (check-constant-is? x flonum?)]
[(real) (or (eq? x 'fixnum)
(eq? x 'bignum)
(eq? x 'exact-integer)
(eq? x 'flonum)
(check-constant-is? x real?))]
[(number) (or (eq? x 'fixnum)
(eq? x 'bignum)
(eq? x 'exact-integer)
(eq? x 'flonum)
(eq? x 'real)
(check-constant-is? x number?))]
[(gensym) (check-constant-is? x gensym?)]
[(uninterned-symbol) (check-constant-is? x uninterned-symbol?)]
[(interned-symbol) (check-constant-is? x (lambda (x)
(and (symbol? x)
(not (gensym? x))
(not (uninterned-symbol? x)))))]
[(symbol) (or (eq? x 'gensym)
(eq? x 'uninterned-symbol)
(eq? x 'interned-symbol)
(check-constant-is? x symbol?))]
[(char) (check-constant-is? x char?)]
[(boolean) (check-constant-is? x boolean?)]
[(true) (and (not (check-constant-is? x not))
(not (eq? x 'boolean))
(not (eq? x 'ptr)))] ; only false-rec, boolean and ptr may be `#f
[($record) (or (pred-$record/rtd? x)
(pred-$record/ref? x)
(check-constant-is? x #3%$record?))]
[(vector) (check-constant-is? x vector?)] ; i.e. '#()
[(string) (check-constant-is? x string?)] ; i.e. ""
[(bytevector) (check-constant-is? x bytevector?)] ; i.e. '#vu8()
[(fxvector) (check-constant-is? x fxvector?)] ; i.e. '#vfx()
[(flvector) (check-constant-is? x flvector?)] ; i.e. '#vfl()
[(ptr) #t]
[else #f])]
[else #f]))))
(define (predicate-implies-not? x y)
(and x
y
; a pred-$record/ref may be any other kind or record
(not (and (pred-$record/ref? x)
(predicate-implies? y '$record)))
(not (and (pred-$record/ref? y)
(predicate-implies? x '$record)))
; boolean and true may be a #t
(not (and (eq? x 'boolean)
(eq? y 'true)))
(not (and (eq? y 'boolean)
(eq? x 'true)))
; the other types are included or disjoint
(not (predicate-implies? x y))
(not (predicate-implies? y x))))
(define (primref->result-predicate pr arity)
(define parameterlike? box?)
(define parameterlike-type unbox)
@ -790,8 +662,8 @@ Notes:
[(parameterlike? type)
(cond
[(not arity) ; unknown
(pred-union void-rec
(primref-name/nqm->predicate (parameterlike-type type) #t))]
(predicate-union void-rec
(primref-name/nqm->predicate (parameterlike-type type) #t))]
[(fx= arity 0)
(primref-name/nqm->predicate (parameterlike-type type) #t)]
[else
@ -1000,8 +872,7 @@ Notes:
[(e1 e2) (let ([r1 (get-type e1)]
[r2 (get-type e2)])
(cond
[(or (predicate-implies-not? r1 r2)
(predicate-implies-not? r2 r1))
[(predicate-disjoint? r2 r1)
(values (make-seq ctxt e1 e2 false-rec)
false-rec ntypes #f #f)]
[else
@ -1033,7 +904,7 @@ Notes:
[(predicate-implies? val-type (rtd->record-predicate rtd #f))
(values (make-seq ctxt val rtd true-rec)
true-rec ntypes #f #f)]
[(predicate-implies-not? val-type (rtd->record-predicate rtd #t))
[(predicate-disjoint? val-type (rtd->record-predicate rtd #t))
(cond
[(fx= level 3)
(let ([rtd (ensure-single-value rtd (get-type rtd))]) ; ensure that rtd is a single valued expression
@ -1111,7 +982,7 @@ Notes:
(define-specialize 2 atan
[(n) (let ([r (get-type n)])
(cond
[(predicate-implies-not? r 'number)
[(predicate-disjoint? r 'number)
(values `(call ,preinfo ,pr ,n)
'bottom pred-env-bottom #f #f)]
[else
@ -1120,8 +991,8 @@ Notes:
[(x y) (let ([rx (get-type x)]
[ry (get-type y)])
(cond
[(or (predicate-implies-not? rx 'real)
(predicate-implies-not? ry 'real))
[(or (predicate-disjoint? rx 'real)
(predicate-disjoint? ry 'real))
(values `(call ,preinfo ,pr ,x ,y)
'bottom pred-env-bottom #f #f)]
[else
@ -1139,8 +1010,8 @@ Notes:
(values ir 'ptr ntypes #f #f)] ; should be maybe-symbol
[(predicate-implies? r 'symbol)
(values ir 'ptr ntypes #f #f)] ; should be maybe-char
[(and (predicate-implies-not? r 'char)
(predicate-implies-not? r 'symbol))
[(and (predicate-disjoint? r 'char)
(predicate-disjoint? r 'symbol))
(values ir 'bottom pred-env-bottom #f #f)]
[else
(values ir 'ptr ; should be maybe-(union 'char 'symbol)
@ -1149,8 +1020,8 @@ Notes:
[rc (get-type c)]
[ir `(call ,preinfo ,pr ,n ,c)])
(cond
[(or (predicate-implies-not? rn 'symbol)
(predicate-implies-not? rc 'ptr)) ; should be maybe-char
[(or (predicate-disjoint? rn 'symbol)
(predicate-disjoint? rc 'ptr)) ; should be maybe-char
(values ir 'bottom pred-env-bottom #f #f)]
[else
(values ir void-rec
@ -1185,12 +1056,12 @@ Notes:
[(args rargs targs t-targs f-targs)
(Expr/main args 'value oldtypes plxc)])
(let* ([predn (primref->argument-predicate pr 1 3 #t)]
[tn (if (predicate-implies-not? rn predn)
[tn (if (predicate-disjoint? rn predn)
'bottom
tn)]
[tn (pred-env-add/ref tn n predn plxc)]
[predargs (primref->argument-predicate pr 2 3 #t)]
[targs (if (predicate-implies-not? rargs predargs)
[targs (if (predicate-disjoint? rargs predargs)
'bottom
targs)]
[targs (pred-env-add/ref targs args predargs plxc)]
@ -1250,7 +1121,7 @@ Notes:
[(predicate-implies? val-type (primref->predicate pr #f))
(values (make-seq ctxt val true-rec)
true-rec ntypes #f #f)]
[(predicate-implies-not? val-type (primref->predicate pr #t))
[(predicate-disjoint? val-type (primref->predicate pr #t))
(values (make-seq ctxt val false-rec)
false-rec ntypes #f #f)]
[else
@ -1294,7 +1165,7 @@ Notes:
(loop (cdr e*)
(cdr r*)
(fx+ n 1)
(if (predicate-implies-not? (car r*) pred)
(if (predicate-disjoint? (car r*) pred)
'bottom
ret)
(pred-env-add/ref t (car e*) pred plxc)))))])
@ -1497,7 +1368,7 @@ Notes:
types)])
(loop (cdr cl*)
(cons cl2 rev-rcl*)
(pred-union rret ret2)
(predicate-union rret ret2)
ntypes
(cond
[(not (eq? ctxt 'test))
@ -1525,7 +1396,7 @@ Notes:
(let-values ([(ir ret n-types t-types f-types)
(Expr/main ir 'value outtypes plxc)])
(values ir
(if (predicate-implies-not? ret 'procedure)
(if (predicate-disjoint? ret 'procedure)
'bottom
#f)
(pred-env-add/ref (pred-env-intersect/base n-types types outtypes)
@ -1604,7 +1475,7 @@ Notes:
types1
types1)])
(values ir
(pred-union ret2 ret3)
(predicate-union ret2 ret3)
new-types
(cond
[(not (eq? ctxt 'test))

View File

@ -799,7 +799,7 @@
(free-identifier=? [sig [(identifier identifier) -> (boolean)]] [flags pure mifoldable discard cp03])
(syntax->datum [sig [(ptr) -> (ptr)]] [flags pure unrestricted mifoldable discard])
(datum->syntax [sig [(identifier ptr) -> (syntax)]] [flags pure mifoldable discard true])
(generate-temporaries [sig [(list) -> (list)]] [flags alloc])
(generate-temporaries [sig [(ptr) -> (list)]] [flags alloc]) ; the argument can be a list or a syntax with a list or an annotation
(syntax-violation [sig [(maybe-who string ptr) (maybe-who string ptr ptr) -> (bottom)]] [flags abort-op])
)