add refinement types, linear expr objs, and ineq props (#510)

This PR adds about half of the needed primitives and logic for
reasoning about linear integer arithmetic in programs with interesting
dependent types. Things have been added in a way s.t. programs will
still continue to typecheck as they did, but if you want integer literals
and certain operations (e.g. *,+,<,<=,=,>=,>) to include linear inequality
information by default, you need to include the
'#:with-linear-integer-arithmetic' keyword at the top of your module.

The other features needed to get TR to be able to check things like
verified vector operations will be to ajust function types so
dependencies can exist between arguments and a minor tweak to get
type inference to consider the symbolic objects of functions arguments.
These features should be coming shortly in a future pull request.
This commit is contained in:
Andrew Kent 2017-03-27 14:32:29 -04:00 committed by GitHub
parent 2804bd4a93
commit 81b134cbb9
63 changed files with 4717 additions and 811 deletions

View File

@ -717,13 +717,6 @@ functions and continuation mark functions.
contract combinator, but with types instead of contracts.
}
@deftogether[(
@defidform[Top]
@defidform[Bot])]{ These are propositions that can be used with @racket[->].
@racket[Top] is the propositions with no information.
@racket[Bot] is the propositions which means the result cannot happen.
}
@defidform[Procedure]{is the supertype of all function types. The @racket[Procedure]
type corresponds to values that satisfy the @racket[procedure?] predicate.
@ -823,12 +816,85 @@ this top type.
#s((salad food 1) "quinoa" "EVOO" salad))]
}
@defalias[Union U]
@defalias[Intersection ∩]
@defalias[→ ->]
@defalias[case→ case->]
@defalias[∀ All]
@section{Logical Refinements and Propositions}
@defform[#:literals (Refine : Top Bot ! and or when
unless if < <= = > >= car cdr
vector-length + *)
(Refine [id : type] proposition)
#:grammar
([proposition Top
Bot
(: symbolic-object type)
(! symbolic-object type)
(and proposition ...)
(or proposition ...)
(when proposition proposition)
(unless proposition proposition)
(if proposition proposition proposition)
(linear-comp symbolic-object symbolic-object)]
[linear-comp < <= = >= >]
[symbolic-object exact-integer
linear-term
(+ linear-term linear-term ...)]
[linear-term symbolic-path
(* exact-integer symbolic-path)]
[symbolic-path id
(path-elem symbolic-path)]
[path-elem car
cdr
vector-length])]{@racket[(Refine [v : t] p)] is a
refinement of type @racket[t] with logical proposition
@racket[p], or in other words it describes any value
@racket[v] of type @racket[t] for which the logical
proposition @racket[p] holds.
@ex[(ann 42 (Refine [n : Integer] (= n 42)))]
Note: The identifier in a refinement type is in scope
inside the proposition, but not the type.
}
@deftogether[(
@defidform[Top]
@defidform[Bot])]{ These are propositions that can be used with
@racket[->] and @racket[Refine].
@racket[Top] is the proposition with no information (i.e. the trivially true
proposition).
@racket[Bot] is the propositions which means the result cannot happen
(i.e. the impossible proposition).
}
@racket[(: o t)] used as a proposition holds when symbolic object @racket[o]
is of type @racket[t.]
@defform[(! sym-obj type)]{This is the dual of @racket[(: o t)], holding
when @racket[o] is not of type @racket[t].}
Propositions can also describe linear inequalities (e.g. @racket[(<= x 42)]
holds when @racket[x] is less than or equal to @racket[42]), using any
of the following relations: @racket[<=], @racket[<], @racket[=],
@racket[>=], @racket[>].
The following logical combinators hold as one would expect
depending on which of their subcomponents hold hold:
@racket[and], @racket[or], @racket[if], @racket[not].
@racket[(when p q)] is equivalent to @racket[(or (not p) (and p q))].
@racket[(unless p q)] is equivalent to @racket[(or p q)].
@section{Other Types}
@defform[(Option t)]{Either @racket[t] or @racket[#f]}

View File

@ -10,11 +10,21 @@
...
(provide nm) ...)]))
(define-syntax (define-other-props stx)
(syntax-case stx ()
[(_ nm ...)
#'(begin (define-syntax nm prop-name-error)
...
(provide nm) ...)]))
;; special type names that are not bound to particular types
(define-other-types
-> ->* case-> U Union Intersection Rec All Opaque Vector
Parameterof List List* Class Object Row Unit Values AnyValues Instance Refinement
pred Struct Struct-Type Prefab Top Bot Distinction Sequenceof)
pred Struct Struct-Type Prefab Distinction Sequenceof Refine)
(define-other-props
Top Bot !)
(provide (rename-out [All ]
[U Un]

View File

@ -4,7 +4,8 @@
(require syntax/stx)
(provide type-name-error)
(provide type-name-error
prop-name-error)
(define (type-name-error stx)
(raise-syntax-error
@ -14,3 +15,12 @@
(syntax->datum stx))
stx
(and (stx-pair? stx) (stx-car stx))))
(define (prop-name-error stx)
(raise-syntax-error
'type-check
(format "proposition name used out of context\n proposition: ~a\n in: ~a"
(syntax->datum (if (stx-pair? stx) (stx-car stx) stx))
(syntax->datum stx))
stx
(and (stx-pair? stx) (stx-car stx))))

View File

@ -19,12 +19,18 @@
(define (mb-core stx)
(syntax-parse stx
[(mb (~optional (~or (~and #:optimize (~bind [opt? #'#t])) ; kept for backward compatibility
(~and #:no-optimize (~bind [opt? #'#f]))))
[(mb (~or (~optional
(~or (~and #:optimize (~bind [opt? #'#t])); kept for backward compatibility
(~and #:no-optimize (~bind [opt? #'#f]))))
(~optional
(~and #:with-linear-integer-arithmetic linear-reasoning?)))
...
forms ...)
(let ([pmb-form (syntax/loc stx (#%plain-module-begin forms ...))])
(parameterize ([optimize? (or (and (not (attribute opt?)) (optimize?))
(and (attribute opt?) (syntax-e (attribute opt?))))])
(and (attribute opt?) (syntax-e (attribute opt?))))]
[with-linear-integer-arithmetic? (or (attribute linear-reasoning?)
(with-linear-integer-arithmetic?))])
(tc-module/full stx pmb-form
(λ (new-mod pre-before-code pre-after-code)
(with-syntax*

View File

@ -215,8 +215,11 @@
[(BaseUnion: bbits nbits) `(make-BaseUnion ,bbits ,nbits)]
[(Union: base elems) `(Un . ,(append (if (Bottom? base) '() (list (type->sexp base)))
(map type->sexp elems)))]
[(Intersection: elems)
`(make-Intersection (list ,@(map type->sexp elems)))]
[(Intersection: elems raw-prop)
(if (not (TrueProp? raw-prop))
`(-refine (make-Intersection (list ,@(map type->sexp elems)))
,(prop->sexp raw-prop))
`(make-Intersection (list ,@(map type->sexp elems))))]
[(Name: stx 0 #t)
`(-struct-name (quote-syntax ,stx))]
[(Name: stx args struct?)
@ -332,6 +335,7 @@
`(make-AndProp (list ,@(map prop->sexp fs)))]
[(OrProp: fs)
`(make-OrProp (list ,@(map prop->sexp fs)))]
[(LeqProp: lhs rhs) `(-leq ,(object->sexp lhs) ,(object->sexp rhs))]
[(PropSet: thn els)
`(make-PropSet ,(prop->sexp thn) ,(prop->sexp els))]))
@ -348,7 +352,9 @@
`(make-Path (list ,@(map path-elem->sexp pes))
,(if (identifier? i)
`(quote-syntax ,i)
`(cons ,(car i) ,(cdr i))))]))
`(cons ,(car i) ,(cdr i))))]
[(LExp: const terms) `(-lexp ,@(for/list ([(o c) (in-terms terms)])
`(list ,c ,(object->sexp o))))]))
;; Path-Element -> SExp
;; Convert a path element in an object to an s-expression

View File

@ -9,8 +9,11 @@
(require "../utils/utils.rkt"
racket/keyword-transform racket/list
(for-syntax syntax/parse racket/base)
(contract-req)
(contract-req)
racket/match
(env type-env-structs global-env)
(types numeric-tower path-type)
(rep object-rep)
(utils tc-utils)
(only-in (rep type-rep) Type?)
(typecheck renamer)
@ -18,21 +21,23 @@
(require-for-cond-contract (rep object-rep core-rep))
(provide lexical-env
with-lexical-env
with-extended-lexical-env)
(provide lexical-env
add-props-to-current-lexical!
with-lexical-env
with-extended-lexical-env
with-naively-extended-lexical-env)
(provide/cond-contract
[lookup-type/lexical ((identifier?) (env? #:fail (or/c #f Type? (-> any/c (or/c Type? #f))))
. ->* .
(or/c Type? #f))]
[lookup-id-type/lexical ((identifier?) (env? #:fail (or/c #f Type? (-> any/c (or/c Type? #f))))
. ->* .
(or/c Type? #f))]
[lookup-obj-type/lexical ((Object?) (env? #:fail (or/c #f Type? (-> any/c (or/c Type? #f))))
. ->* .
(or/c Type? #f))]
[lookup-alias/lexical ((identifier?) (env?) . ->* . (or/c Path? Empty?))])
;; the current lexical environment
(define lexical-env (make-parameter empty-env))
;; run code in a new env
(define-syntax-rule (with-lexical-env e . b)
(parameterize ([lexical-env e]) . b))
(define (add-props-to-current-lexical! ps)
(lexical-env (env-replace-props (lexical-env) (append ps (env-props (lexical-env))))))
;; run code in an extended env
(define-syntax (with-extended-lexical-env stx)
@ -43,38 +48,61 @@
#:defaults ([objs #'#f]))]
. body)
(syntax/loc stx
(with-lexical-env (env-extend/bindings (lexical-env) ids tys objs) . body))]))
(let ([idents ids]
[types tys])
(let ([ps (apply append
(for*/list ([(id ty) (in-parallel (in-list idents) (in-list types))]
[props (in-value (extract-props (-id-path id) ty))]
#:unless (null? props))
props))])
(with-lexical-env (env-replace-props (env-extend/bindings (lexical-env) ids tys objs)
(append ps (env-props (lexical-env))))
. body))))]))
;; find the type of identifier i, looking first in the lexical env, then in the top-level env
;; identifier -> Type
(define (lookup-type/lexical i [env (lexical-env)] #:fail [fail #f])
(env-lookup env i (λ (i) (lookup-type i (λ ()
(cond
[(syntax-property i 'constructor-for)
=> (λ (prop)
(define orig (un-rename prop))
(define t (lookup-type/lexical orig env))
(register-type i t)
t)]
[(syntax-procedure-alias-property i)
=> (λ (prop)
(define orig (car (flatten prop)))
(define t (lookup-type/lexical orig env))
(register-type i t)
t)]
[(syntax-procedure-converted-arguments-property i)
=> (λ (prop)
(define orig (car (flatten prop)))
(define pre-t
(lookup-type/lexical
orig env #:fail (lambda (i) (lookup-fail i) #f)))
(define t (if pre-t
(kw-convert pre-t #f)
Err))
(register-type i t)
t)]
[else ((or fail lookup-fail) i)]))))))
(define (lookup-id-type/lexical i [env (lexical-env)] #:fail [fail #f])
(env-lookup-id
env i
(λ (i) (lookup-type i (λ ()
(cond
[(syntax-property i 'constructor-for)
=> (λ (prop)
(define orig (un-rename prop))
(define t (lookup-id-type/lexical orig env))
(register-type i t)
t)]
[(syntax-procedure-alias-property i)
=> (λ (prop)
(define orig (car (flatten prop)))
(define t (lookup-id-type/lexical orig env))
(register-type i t)
t)]
[(syntax-procedure-converted-arguments-property i)
=> (λ (prop)
(define orig (car (flatten prop)))
(define pre-t
(lookup-id-type/lexical
orig env #:fail (lambda (i) (lookup-fail i) #f)))
(define t (if pre-t
(kw-convert pre-t #f)
Err))
(register-type i t)
t)]
[else ((or fail lookup-fail) i)]))))))
(define (lookup-obj-type/lexical obj [env (lexical-env)] #:fail [fail #f])
(match obj
[(Path: pes (? identifier? x))
(or (path-type pes (lookup-id-type/lexical x env #:fail fail))
Univ)]
[(Path: '() _)
(env-lookup-obj env obj (λ (_) Univ))]
[(Path: pes nm)
(define nm-ty (env-lookup-obj env (-id-path nm) (λ (_) Univ)))
(or (path-type pes nm-ty)
Univ)]
[_ (env-lookup-obj env obj (λ (obj) (if (LExp? obj) -Int Univ)))]))
;; looks up the representative object for an id (i.e. itself or an alias if one exists)
(define (lookup-alias/lexical i [env (lexical-env)])

View File

@ -58,7 +58,7 @@
(define (check-type-alias-contractive id type)
(define/match (check type)
[((Union: _ ts)) (andmap check ts)]
[((Intersection: elems)) (andmap check elems)]
[((Intersection: elems _)) (andmap check elems)]
[((Name/simple: name-id))
(and (not (free-identifier=? name-id id))
(check (resolve-once type)))]

View File

@ -4,59 +4,98 @@
syntax/id-table
(except-in "../utils/utils.rkt" env)
(contract-req)
(rep core-rep object-rep))
;; dict ops only used for convenient printing
;; (e.g. performance is irrelevant)
(only-in racket/dict dict->list dict-map)
(rep core-rep object-rep)
(for-syntax racket/base syntax/parse))
(require-for-cond-contract (rep type-rep prop-rep))
;; types is a free-id-table of identifiers to types
;; props is a list of known propositions
(define-struct/cond-contract env ([types immutable-free-id-table?]
(define-struct/cond-contract env ([types immutable-free-id-table?]
[obj-types (hash/c Object? Type? #:immutable #t)]
[props (listof Prop?)]
[aliases immutable-free-id-table?])
#:transparent
#:property prop:custom-write
(lambda (e prt mode)
(fprintf prt "(env ~a ~a ~a)"
(free-id-table-map (env-types e)
(λ (id ty) (format "[~a ∈ ~a]" id ty)))
(dict-map (append (dict->list (env-types e))
(hash->list (env-obj-types e)))
(λ (id ty) (format "[~a ∈ ~a]" id ty)))
(env-props e)
(free-id-table-map (env-aliases e)
(λ (id ty) (format "[~a ≡ ~a]" id ty))))))
(provide/cond-contract
[env? predicate/c]
[env-set-type (env? identifier? Type? . -> . env?)]
[env-set-id-type (env? identifier? Type? . -> . env?)]
[env-set-obj-type (env? Object? Type? . -> . env?)]
[env-extend/bindings (env? (listof identifier?)
(listof Type?)
(or/c (listof OptObject?) #f)
. -> .
env?)]
[env-lookup (env? identifier? (identifier? . -> . any) . -> . any)]
[env-lookup-id (env? identifier? (identifier? . -> . any) . -> . any)]
[env-lookup-obj (env? Object? (Object? . -> . any) . -> . any)]
[env-props (env? . -> . (listof Prop?))]
[env-replace-props (env? (listof Prop?) . -> . env?)]
[empty-env env?]
[env-lookup-alias (env? identifier? (identifier? . -> . (or/c OptObject? #f)) . -> . (or/c OptObject? #f))])
(provide lexical-env
with-lexical-env
with-naively-extended-lexical-env)
(define empty-env
(env
(make-immutable-free-id-table)
(hash)
null
(make-immutable-free-id-table)))
(define lexical-env (make-parameter empty-env))
;; run code in a new env
(define-syntax-rule (with-lexical-env e . b)
(parameterize ([lexical-env e]) . b))
;; "naively" extends the environment by simply adding the props
;; to the environments prop list (i.e. it doesn't do any logical
;; simplifications like env+ in tc-envops.rkt)
(define-syntax (with-naively-extended-lexical-env stx)
(syntax-parse stx
[(_ [#:props ps:expr]
. body)
(syntax/loc stx
(with-lexical-env (env-replace-props (lexical-env) (append ps (env-props (lexical-env)))) . body))]))
(define (env-replace-props e props)
(match-let ([(env tys _ als) e])
(env tys props als)))
(match-let ([(env tys otys _ als) e])
(env tys otys props als)))
(define (env-lookup e key fail)
(match-let ([(env tys _ _) e])
(define (env-lookup-id e key fail)
(match-let ([(env tys _ _ _) e])
(free-id-table-ref tys key (λ () (fail key)))))
(define (env-lookup-obj e key fail)
(match-let ([(env _ otys _ _) e])
(hash-ref otys key (λ () (fail key)))))
;; like hash-set, but for the type of an ident in the lexical environment
(define (env-set-type e ident type)
(match-let ([(env tys ps als) e])
(env (free-id-table-set tys ident type) ps als)))
(define (env-set-id-type e ident type)
(match-let ([(env tys otys ps als) e])
(env (free-id-table-set tys ident type) otys ps als)))
;; like hash-set, but for the type of an object in the lexical environment
(define (env-set-obj-type e obj type)
(match-let ([(env tys otys ps als) e])
(env tys (hash-set otys obj type) ps als)))
;; extends an environment with types and aliases
;; e : the 'env' struct to be updated
@ -67,11 +106,13 @@
;; there are no aliases, you can pass #f
;; for 'aliased-objs' to simplify the computation.
(define (env-extend/bindings e idents types maybe-aliased-objs)
(match-define (env tys ps als) e)
(match-define (env tys otys ps als) e)
;; NOTE: we mutate the identifiers 'tys' and 'als' for convenience,
;; but the free-id-tables themselves are immutable.
(define (update/type! id t)
(set! tys (free-id-table-set tys id t)))
(define (update/obj-type! lexp t)
(set! otys (hash-set otys lexp t)))
(define (update/alias! id o)
(set! als (free-id-table-set als id o)))
(define (update/type+alias! id t o)
@ -82,16 +123,18 @@
;; record the alias relation 'id ≡ id*' *and* that 'id* ∈ t'
[(Path: '() id*) (update/type! id* t)
(update/alias! id o)]
;; id is aliased to an object which is not a simple identifier;
;; just record the alias. (NOTE: if we move to supporting more
;; complicated objects, we _may_ want to add o ∈ t to Γ as well)
[o (update/alias! id o)]))
;; id is aliased to a Path w/ a non-empty path element list;
;; just record the alias.
[(? Path? p) (update/alias! id p)]
;; for ids that alias non-Path objs, we record the type and alias
[o (update/obj-type! o t)
(update/alias! id o)]))
(if maybe-aliased-objs
(for-each update/type+alias! idents types maybe-aliased-objs)
(for-each update/type! idents types))
(env tys ps als))
(env tys otys ps als))
(define (env-lookup-alias e key fail)
(match-let ([(env _ _ als) e])
(match-let ([(env _ _ _ als) e])
(free-id-table-ref als key (λ () (fail key)))))

View File

@ -15,7 +15,8 @@
values-rep rep-utils type-mask)
(types utils abbrev numeric-tower subtype resolve
substitute generalize prefab)
(env index-env tvar-env))
(env lexical-env index-env tvar-env)
(logic proves))
make-env -> ->* one-of/c)
"constraint-structs.rkt"
"signatures.rkt" "fail.rkt"
@ -524,7 +525,7 @@
[(s (? Mu? t)) (cg s (unfold t))]
;; find *an* element of elems which can be made a subtype of T
[((Intersection: ts) T)
[((Intersection: ts raw-prop) T)
(cset-join
(for*/list ([t (in-list ts)]
[v (in-value (cg t T))]
@ -532,9 +533,14 @@
v))]
;; constrain S to be below *each* element of elems, and then combine the constraints
[(S (Intersection: ts))
[(S (Intersection: ts raw-prop))
(define cs (for/list/fail ([ts (in-list ts)]) (cg S ts)))
(and cs (cset-meet* (cons empty cs)))]
(let ([obj (-id-path (genid))])
(and cs
(implies-in-env? (lexical-env)
(-is-type obj S)
(instantiate-rep/obj raw-prop obj S))
(cset-meet* (cons empty cs))))]
;; constrain *each* element of es to be below T, and then combine the constraints
[((BaseUnion-bases: es) T)

View File

@ -11,14 +11,14 @@
(export intersect^)
(define ((intersect-types additive?) t1 t2)
(define ((intersect-types additive?) t1 t2 #:obj [obj -empty-obj])
(cond
;; we dispatch w/ Error first, because it behaves in
;; strange ways (e.g. it is and ⊥ w.r.t subtyping) and
;; mucks up what might otherwise be commutative behavior
[(or (Error? t1) (Error? t2)) Err]
[else
(let intersect ([t1 t1] [t2 t2] [seen '()])
(let intersect ([t1 t1] [t2 t2] [seen '()] [obj obj])
;; t1 : Type?
;; t2 : Type?
;; seen : (listof (cons/c (cons/c Type? Type?) symbol?))
@ -26,14 +26,14 @@
;; recursive types in order to prevent infinite looping
;; and build a recursive type when appropriate. See the 'resolvable?'
;; cases below.
(define (rec t1 t2) (intersect t1 t2 seen))
(define (rec t1 t2 [obj -empty-obj]) (intersect t1 t2 seen obj))
(match* (t1 t2)
;; quick overlap check
[(_ _) #:when (not (overlap? t1 t2)) -Bottom]
;; already a subtype
[(_ _) #:when (subtype t1 t2) t1]
[(_ _) #:when (subtype t2 t1) t2]
[(_ _) #:when (subtype t1 t2 #:obj obj) t1]
[(_ _) #:when (subtype t2 t1 #:obj obj) t2]
;; polymorphic intersect
@ -46,7 +46,7 @@
;; structural recursion on types
[((Pair: a1 d1) (Pair: a2 d2))
(rebuild -pair (rec a1 a2) (rec d1 d2))]
(rebuild -pair (rec a1 a2 (-car-of obj)) (rec d1 d2 (-cdr-of obj)))]
;; FIXME: support structural updating for structs when structs are updated to
;; contain not only *if* they are polymorphic, but *which* fields are too
;;[((Struct: _ _ _ _ _ _)
@ -66,16 +66,18 @@
(let ([t1s (if (Bottom? base1) t1s (cons base1 t1s))])
(apply Un (for*/list ([t1 (in-list t1s)]
[t2 (in-list t2s)]
[t* (in-value (rec t1 t2))]
[t* (in-value (rec t1 t2 obj))]
#:unless (Bottom? t*))
t*)))]
[_ (Union-fmap (λ (t1) (rec t1 t2)) base1 t1s)])]
[(t1 (Union: base2 t2s)) (Union-fmap (λ (t2) (rec t1 t2)) base2 t2s)]
[_ (Union-fmap (λ (t1) (rec t1 t2 obj)) base1 t1s)])]
[(t1 (Union: base2 t2s)) (Union-fmap (λ (t2) (rec t1 t2 obj)) base2 t2s)]
[((Intersection: t1s) t2)
(apply -unsafe-intersect (map (λ (t1) (rec t1 t2)) t1s))]
[(t1 (Intersection: t2s))
(apply -unsafe-intersect (map (λ (t2) (rec t1 t2)) t2s))]
[((Intersection: t1s raw-prop) t2)
(-refine (apply -unsafe-intersect (map (λ (t1) (rec t1 t2 obj)) t1s))
raw-prop)]
[(t1 (Intersection: t2s raw-prop))
(-refine (apply -unsafe-intersect (map (λ (t2) (rec t1 t2 obj)) t2s))
raw-prop)]
;; For resolvable types, we record the occurrence and save a back pointer
;; in 'seen'. Then, if this pair of types emerges again, we know that we are
@ -106,7 +108,8 @@
(resolve t2)
(list* (cons (cons t1 t2) record)
(cons (cons t2 t1) record)
seen)))
seen)
obj))
(cond
;; check if we used the backpointer, if so,
;; make a recursive type using that name
@ -137,10 +140,10 @@
-Bottom)])]
[((BaseUnion-bases: bases1) t2)
(apply Un (for/list ([b (in-list bases1)])
(rec b t2)))]
(rec b t2 obj)))]
[(t1 (BaseUnion-bases: bases2))
(apply Un (for/list ([b (in-list bases2)])
(rec t1 b)))]
(rec t1 b obj)))]
;; t2 and t1 have a complex relationship, so we build an intersection
;; if additive, otherwise t1 remains unchanged

View File

@ -21,8 +21,8 @@
[cond-contracted c-meet ((c? c?) (symbol?) . ->* . (or/c #f c?))]))
(define-signature intersect^
([cond-contracted intersect (Type? Type? . -> . Type?)]
[cond-contracted restrict (Type? Type? . -> . Type?)]))
([cond-contracted intersect ((Type? Type?) (#:obj OptObject?) . ->* . Type?)]
[cond-contracted restrict ((Type? Type?) (#:obj OptObject?) . ->* . Type?)]))
(define-signature infer^
([cond-contracted infer ((;; variables from the forall

View File

@ -0,0 +1,919 @@
#lang racket/base
(require "../utils/utils.rkt"
(rep object-rep prop-rep fme-utils)
(contract-req)
racket/format
racket/list
(for-syntax racket/base syntax/parse)
racket/match)
;; public API for reasoning about LeqProps
(provide/cond-contract
[contradictory-Leqs?
(-> LeqProp? LeqProp? boolean?)]
[complementary-Leqs?
(-> LeqProp? LeqProp? boolean?)]
[Leq-implies-Leq?
(-> LeqProp? LeqProp? boolean?)]
[satisfiable-Leqs?
(-> (listof LeqProp?) boolean?)]
[Leqs-imply-Leq-or-not-Leq?
(-> (listof LeqProp?) LeqProp? (or/c boolean? 'neither))]
[Leqs-imply-Leq?
(-> (listof LeqProp?) LeqProp? boolean?)]
[Leqs-imply-not-Leq?
(-> (listof LeqProp?) LeqProp? boolean?)]
[Leqs-imply-Leqs?
(-> (listof LeqProp?) (listof LeqProp?) boolean?)])
;; some internal contracts
(define-for-cond-contract lexp?
(cons/c exact-integer?
(and/c (hash/c any/c (and/c exact-integer?
(not/c (=/c 0)))
#:immutable #t)
hash-eq?)))
(define-for-cond-contract leq? (cons/c lexp? lexp?))
(define-for-cond-contract sli? (listof leq?))
;; *****************************************************
;; public API functions
(define (contradictory-Leqs? l1 l2)
(contradictory-leqs? (Leq->leq l1)
(Leq->leq l2)))
(define (complementary-Leqs? l1 l2)
(contradictory-leqs? (leq-negate (Leq->leq l1))
(leq-negate (Leq->leq l2))))
(define (Leq-implies-Leq? l1 l2)
(leq-imp-leq? (Leq->leq l1)
(Leq->leq l2)))
(define (satisfiable-Leqs? leqs)
(fme-sat? (Leqs->sli leqs)))
;; Leqs-imply-Leq-or-not-Leq?
;;
;; Determins if the Leqs in 'ls' either prove
;; or disprove 'l'
(define (Leqs-imply-Leq-or-not-Leq? ls l)
(define leqs (Leqs->sli ls))
(define ineq (Leq->leq l))
(cond
[(fme-imp-leq? leqs ineq) #t]
[(fme-imp-leq? leqs (leq-negate ineq)) #f]
[else 'neither]))
(define (Leqs-imply-Leq? ls l)
(fme-imp-leq? (Leqs->sli ls) (Leq->leq l)))
(define (Leqs-imply-not-Leq? ls l)
(fme-imp-leq? (Leqs->sli ls) (leq-negate (Leq->leq l))))
(define (Leqs-imply-Leqs? assumptions goals)
(fme-imp? (Leqs->sli assumptions)
(Leqs->sli goals)))
;; *****************************************************
;; helper functions
;; turns a list of Leqs into a sli (system of linear equations)
;; which is just a list of leqs (the internal version)
(define/cond-contract (Leqs->sli Leqs)
(-> (listof LeqProp?) sli?)
(map Leq->leq Leqs))
;; Leq to the internal leq rep
(define (Leq->leq l)
(match l
[(LeqProp: (LExp: c1 ts1) (LExp: c2 ts2))
(leq (lexp c1 ts1) (lexp c2 ts2))]))
;; *****************************************************************************
;; Fourier-Motzkin elimination implementation
;; http://en.wikipedia.org/wiki/Fourier-Motzkin_elimination
;;
;; Uses non-matrix representations of data
;;
;; Decides satisfiability, implication, etc... of/between systems of linear inequalities
;; of the form ([(a_1x_1 + a_2x_2 + ... + a_c) <= (b_1x_1 + b_2x_2 + ... + b_c)] ...)
;; *****************************************************************************
(define-match-expander lexp:
(lambda (stx)
(syntax-case stx ()
[(_ const exp)
#'(cons const exp)])))
(define-match-expander leq:
(lambda (stx)
(syntax-case stx ()
[(_ lhs rhs)
#'(cons lhs rhs)])))
(define/cond-contract (lexp const terms)
(-> exact-integer?
(and/c (hash/c any/c (and/c exact-integer?
(not/c (=/c 0)))
#:immutable #t)
hash-eq?)
lexp?)
(cons const terms))
(define lexp-const car)
(define lexp-terms cdr)
(define-syntax-rule (lexp* t ...)
(list->lexp (list t ...)))
(define/cond-contract (list->lexp terms)
(-> (listof (or/c exact-integer? (list/c exact-integer? any/c))) lexp?)
(let loop ([c 0]
[h (make-terms)]
[zxs terms])
(match zxs
[(list) (lexp c h)]
[(cons (list coeff var) zxs-rst)
(loop c (terms-set h var (+ coeff (terms-ref h var))) zxs-rst)]
[(cons constant zxs-rst)
(loop (+ constant c) h zxs-rst)])))
;; what is the coefficient of 'x' in 'l'
(define/cond-contract (lexp-coeff l x)
(-> lexp? any/c exact-integer?)
(terms-ref (lexp-terms l) x))
(module+ test
(define-syntax (check-true stx)
(syntax-case stx ()
[(_ exp) (syntax/loc stx (unless (eq? #t exp) (error 'check-true "test failed!")))]))
(define-syntax (check-false stx)
(syntax-case stx ()
[(_ exp) (syntax/loc stx (when (not (eq? #f exp)) (error 'check-false "test failed!")))]))
(define-syntax (check-not-false stx)
(syntax-case stx ()
[(_ exp) (syntax/loc stx (unless exp (error 'check-not-false "test failed!")))]))
(define-syntax (check-equal? stx)
(syntax-case stx ()
[(_ val exp)
(syntax/loc stx (unless (equal? val exp)
(error 'check-equal? "not equal!")))]))
(check-equal? (lexp* 1 '(1 x) '(42 y) 1) (lexp* '(42 y) 2 '(1 x)))
(check-equal? (lexp* 0) (lexp* 0 '(0 x) '(0 y) '(0 z)))
(check-equal? (lexp-coeff (lexp* 1 '(1 x) '(42 y)) 'y) 42)
(check-equal? (lexp-const (lexp* 1 '(1 x) '(42 y))) 1)
(check-equal? (lexp-coeff (lexp* '(1 x) '(42 y)) 'q) 0))
;; what variables are in this lexp
(define/cond-contract (lexp-vars exp)
(-> lexp? list?)
(terms-vars (lexp-terms exp)))
;; what scalars are in this lexp
(define/cond-contract (lexp-scalars exp)
(-> lexp? (listof exact-integer?))
(match exp
[(lexp: c ts)
(define coeffs (terms-coeffs ts))
(if (zero? c) coeffs (cons c coeffs))]
[_ (error 'lexp-scalars "given invalid lexp ~a" exp)]))
(module+ test
(check-true (and (equal? (sort (lexp-vars (lexp* 17 '(42 x) '(2 z))) symbol<?)
(sort '(x z) symbol<?))
(= 2 (length (lexp-vars (lexp* 17 '(42 x) '(2 z)))))))
(check-true (and (equal? (sort (lexp-scalars (lexp* 17 '(42 x) '(2 z))) <)
'(2 17 42))
(= 3 (length (lexp-scalars (lexp* 17 '(42 x) '(2 z))))))))
; lexp-scale
;; if multiplying any scalar by a results
;; in a non integer, error is thrown if
;; contracts are active
(define/cond-contract (lexp-scale exp a)
(-> lexp? rational? lexp?)
(cond
[(eqv? a 0) (lexp 0 (make-terms))]
[(= a 1) exp]
[else
(match exp
[(lexp: c h)
(lexp (* c a)
(terms-scale h a))])]))
(module+ test
(check-equal? (lexp-set (lexp* 17 '(42 x)) 'x 0)
(lexp* 17)))
; lexp-set
; excludes items set to 0
(define/cond-contract (lexp-set exp x i)
(-> lexp? any/c exact-integer? lexp?)
(match exp
[(lexp: c h)
(lexp c
(terms-set h x i))]))
; lexp-set-const
; sets the constant in an lexp
(define/cond-contract (lexp-set-const exp i)
(-> lexp? exact-integer? lexp?)
(lexp i
(lexp-terms exp)))
(module+ test
(check-equal? (lexp-set (lexp* 17) 'x 42)
(lexp* 17 '(42 x)))
(check-equal? (lexp-set (lexp* 17 '(2 x)) 'x 42)
(lexp* 17 '(42 x)))
(check-equal? (lexp-set-const (lexp* 17 '(2 x)) 42)
(lexp* 42 '(2 x))))
; lexp-zero?
;; is this lexp equiv to 0?
(define/cond-contract (lexp-zero? exp)
(-> lexp? boolean?)
(match exp
[(lexp: c h)
(and (= 0 c) (terms-empty? h))]))
(module+ test
(check-false (lexp-zero? (lexp* 17 '(42 x))))
(check-false (lexp-zero? (lexp* 17)))
(check-not-false (lexp-zero? (lexp* 0))))
; l1 - l2
(define/cond-contract (lexp-subtract l1 l2)
(-> lexp? lexp? lexp?)
(match* (l1 l2)
[((lexp: c1 h1) (lexp: c2 h2))
(lexp (- c1 c2)
(terms-subtract h1 h2))]))
;; l1 + l2
(define/cond-contract (lexp-plus l1 l2)
(-> lexp? lexp? lexp?)
(match* (l1 l2)
[((lexp: c1 h1) (lexp: c2 h2))
(lexp (+ c1 c2)
(terms-add h1 h2))]))
(module+ test
(check-equal? (lexp-subtract (lexp* -1 '(2 x) '(3 y))
(lexp* -1 '(2 x) '(42 z)))
(lexp* 0 '(3 y) '(-42 z)))
(check-equal? (lexp-subtract (lexp* 0)
(lexp* -1 '(2 x) '(42 z)))
(lexp* 1 '(-2 x) '(-42 z))))
; lexp-has-var?
; is 'x' a non-zero term in 'l'
(define/cond-contract (lexp-has-var? l x)
(-> lexp? any/c boolean?)
(not (zero? (lexp-coeff l x))))
(module+ test
(check-false (lexp-has-var? (lexp* 17 '(42 x)) 'y))
(check-not-false (lexp-has-var? (lexp* 17 '(42 x)) 'x)))
(define/cond-contract (lexp-add1 l)
(-> lexp? lexp?)
(match l
[(lexp: c h)
(lexp (add1 c) h)]))
(module+ test
(check-equal? (lexp-add1 (lexp* 0)) (lexp* 1))
(check-equal? (lexp-add1 (lexp* 1 '(5 x)))
(lexp* 2 '(5 x))))
;; is this lexp just a constant? (i.e. no terms)
(define/cond-contract (constant-lexp? l)
(-> lexp? (or/c exact-integer? #f))
(match l
[(lexp: const terms)
(and (terms-empty? terms)
const)]))
;; if this lexp is 1*x, return x
(define/cond-contract (simple-lexp? exp)
(-> lexp? any/c)
(match exp
[(lexp: c terms)
(and
;; ps is length 1? (i.e. only 1 variable)
(and (zero? c)
(= 1 (terms-count terms))
(let ([pair (car (terms->list terms))])
(and (= 1 (cdr pair))
(car pair)))))]))
(define/cond-contract (lexp->string e [pp #f])
(-> lexp? (-> any/c any/c) string?)
(define vars (terms-vars (lexp-vars e)))
(define const (lexp-const e))
(define term->string
(λ (x) (string-append (if (= 1 (lexp-coeff e x))
""
(number->string (lexp-coeff e x)))
"(" (if pp
(pp x)
(~a x)) ")")))
(cond
[(terms-empty? vars) (number->string const)]
[(zero? const)
(for/fold ([str (term->string (car vars))])
([var (in-list (cdr vars))])
(string-append str " + " (term->string var)))]
[else
(for/fold ([str (number->string const)])
([var (in-list vars)])
(string-append str " + " (term->string var)))]))
;; ********** ********** L E Q s ********* **********
(define/cond-contract (leq lhs rhs)
(-> lexp? lexp? leq?)
(cons lhs rhs))
(define leq-lhs car)
(define leq-rhs cdr)
(define/cond-contract (leq-lexps ineq)
(-> leq? (values lexp? lexp?))
(match ineq
[(leq: lhs rhs)
(values lhs rhs)]))
(define/cond-contract (leq-contains-var? ineq x)
(-> leq? any/c boolean?)
(match ineq
[(leq: lhs rhs)
(or (lexp-has-var? lhs x)
(lexp-has-var? rhs x))]))
(define/cond-contract (leq-vars ineq)
(-> leq? list)
(let-values ([(l r) (leq-lexps ineq)])
(remove-duplicates (append (lexp-vars l) (lexp-vars r)))))
; leq-negate
; ~ (l1 <= l2) ->
; l2 <= 1 + l1
; (obviously this is valid for integers only)
(define/cond-contract (leq-negate ineq)
(-> leq? leq?)
(match ineq
[(leq: (lexp: c-l terms-l) (lexp: c-r terms-r))
(define c-r* (add1 c-r))
(cond
[(eqv? c-l c-r*)
(leq (lexp 0 terms-r) (lexp 0 terms-l))]
[(< c-l c-r*)
(leq (lexp (- c-r* c-l) terms-r) (lexp 0 terms-l))]
[else
(leq (lexp 0 terms-r) (lexp (- c-l c-r*) terms-l))])]))
(module+ test
(check-equal? (leq-negate (leq (lexp* 0 '(1 x))
(lexp* 0 '(1 y))))
(leq (lexp* 1 '(1 y))
(lexp* 0 '(1 x)))))
;; leq-isolate-var
;; converts leq with x into either:
;; 1) ax <= by + cz + ...
;; or
;; 2) by + cz + ... <= ax
;; where a is a positive integer and x is on at most
;; one side of the inequality
(define/cond-contract (leq-isolate-var ineq x)
(-> leq? any/c leq?)
(match ineq
[(leq: (lexp: lhs-c lhs-ts) (lexp: rhs-c rhs-ts))
(define x-lhs-coeff (terms-ref lhs-ts x))
(define x-rhs-coeff (terms-ref rhs-ts x))
(cond
;; ...1 + ax + ...2 <= ...3 + ax + ...4
;; remove x
;; --> ;; ...1 + ...2 <= ...3 + ...4
[(eqv? x-lhs-coeff x-rhs-coeff)
(define lhs* (lexp lhs-c (terms-remove lhs-ts x)))
(define rhs* (lexp rhs-c (terms-remove rhs-ts x)))
(leq lhs* rhs*)]
;; ...1 + ax + ...2 <= ...3 + bx + ...4 where a < b
;; isolate x so it is on the rhs
;; --> ...1 + ...2 - ...3 - ...4 <= (bx - ax)
[(< x-lhs-coeff x-rhs-coeff)
(define lhs* ;; lhs - rhs (w/ x removed from the result)
(let ([lhs-c* (- lhs-c rhs-c)]
[lhs-h* (terms-subtract lhs-ts rhs-ts)])
(lexp lhs-c* (terms-remove lhs-h* x))))
(define rhs* (lexp 0 (make-terms x (- x-rhs-coeff x-lhs-coeff))))
(leq lhs* rhs*)]
;; ...1 + ax + ...2 <= ...3 + bx + ...4 where a > b
;; isolate x so it is on the lhs
;; --> (ax - bx) <= ...3 + ...4 - ...1 - ...2
[else
(define lhs* (lexp 0 (make-terms x (- x-lhs-coeff x-rhs-coeff))))
(define rhs*
(let ([rhs-c* (- rhs-c lhs-c)]
[rhs-h* (terms-subtract rhs-ts lhs-ts)])
(lexp rhs-c* (terms-remove rhs-h* x))))
(leq lhs* rhs*)])]))
; x lhs
(module+ test
(check-equal? (leq-isolate-var (leq (lexp* '(3 x) '(2 z) '(5 y))
(lexp* '(1 x) '(1 z)))
'x)
(leq (lexp* '(2 x)) (lexp* '(-5 y) '(-1 z))))
;; x rhs
(check-equal? (leq-isolate-var (leq (lexp* '(3 x) '(2 z) '(5 y))
(lexp* '(1 z) '(33 x)))
'x)
(leq (lexp* '(1 z) '(5 y)) (lexp* '(30 x))))
;; x eq
(check-equal? (leq-isolate-var (leq (lexp* '(42 x) '(2 z) '(5 y))
(lexp* '(42 x) '(1 z)))
'x)
(leq (lexp* '(2 z) '(5 y))
(lexp* '(1 z))))
;; no x
(check-equal? (leq-isolate-var (leq (lexp* '(2 z) '(5 y))
(lexp* '(1 z)))
'x)
(leq (lexp* '(2 z) '(5 y))
(lexp* '(1 z))))
; x mix
(check-equal? (leq-isolate-var (leq (lexp* '(2 x) '(4 y) 1)
(lexp* '(2 y))) 'x)
(leq (lexp* '(2 x))
(lexp* '-1 '(-2 y)))))
;; leq-join
;; takes a pair a1x <= l1 and l2 <= a2x
;; and returns a2l1 <= a1l2
(define/cond-contract (leq-join leq1 leq2 x)
(-> leq? leq? any/c leq?)
;; leq1: ... + ax + .... <= ... + bx + ...
;; leq2: ... + cx + .... <= ... + dx + ...
(let-values ([(l1 r1) (leq-lexps leq1)]
[(l2 r2) (leq-lexps leq2)])
(let ([a (lexp-coeff l1 x)] [b (lexp-coeff r1 x)]
[c (lexp-coeff l2 x)] [d (lexp-coeff r2 x)])
(cond
;; leq1: ax <= lexp1
;; leq2: lexp2 <= dx
[(and (eqv? 0 b) (eqv? 0 c))
(leq (lexp-scale l2 a)
(lexp-scale r1 d))]
;; leq1: lexp1 <= bx
;; leq2: cx <= lexp2
[(and (eqv? 0 a) (eqv? 0 d))
(leq (lexp-scale l1 c)
(lexp-scale r2 b))]
[else
(error 'leq-join "cannot join ~a and ~a by ~a" leq1 leq2 x)]))))
(module+ test
(check-equal? (leq-join (leq (lexp* '(2 x))
(lexp* '(4 y) 10))
(leq (lexp* '(4 z) 2)
(lexp* '(4 x)))
'x)
(leq (lexp* '(8 z) 4)
(lexp* '(16 y) 40))))
(define/cond-contract (leq-trivially-valid? ineq)
(-> leq? boolean?)
(let-values ([(l r) (leq-lexps ineq)])
(or (and (constant-lexp? l)
(constant-lexp? r)
(<= (lexp-const l) (lexp-const r)))
(equal? l r))))
(define/cond-contract (leq-trivially-invalid? ineq)
(-> leq? boolean?)
(let-values ([(l r) (leq-lexps ineq)])
(and (constant-lexp? l)
(constant-lexp? r)
(< (lexp-const r) (lexp-const l)))))
(define/cond-contract (leq->string ineq [pp #f])
(-> leq? (-> any/c any/c) string?)
(define-values (lhs rhs) (leq-lexps ineq))
(string-append (lexp->string lhs pp) "" (lexp->string rhs pp)))
;; ******** ******** SLIs ******** ********
;; (i.e. system of linear inequalities)
(define/cond-contract (sli->string sli)
(-> sli? string?)
(string-append
(cond
[(null? sli) "("]
[else
(for/fold ([str (leq->string (car sli))])
([ineq (cdr sli)])
(string-append str ""(leq->string ineq)))])
")"))
(define/cond-contract (sli-trivially-valid? s)
(-> sli? boolean?)
(for/and ([ineq (in-list s)])
(leq-trivially-valid? ineq)))
(define/cond-contract (sli-vars sli)
(-> sli? list?)
(remove-duplicates (append-map leq-vars sli)))
(module+ test
(check-equal? (sort (sli-vars (list (leq (lexp* '(1 x))
(lexp* '(1 y)))
(leq (lexp* '(1 x) '(1 z))
(lexp* '(1 q)))
(leq (lexp* '(1 r) '(3 z))
(lexp* '(1 x)))))
symbol<?)
(sort (list 'r 'q 'z 'y 'x) symbol<?))
(check-equal? (length (sli-vars (list (leq (lexp* '(1 x))
(lexp* '(1 y)))
(leq (lexp* '(1 x) '(1 z))
(lexp* '(1 q)))
(leq (lexp* '(1 r) '(3 z))
(lexp* '(1 x))))))
5))
;; sli-partition
;; partitions leq expressions into
;; 3 lists of x-normalized inequalities:
;; value 1) set of (ax <= by + cz + ...) leqs
;; value 2) set of form (by + cz + ... <= ax) leqs
;; value 3) leqs w/o x
(define/cond-contract (sli-partition leqs x)
(-> sli? any/c (values (listof leq?)
(listof leq?)
(listof leq?)))
(for/fold ([xlhs '()]
[xrhs '()]
[nox '()])
([ineq (in-list leqs)])
(let ([ineq (leq-isolate-var ineq x)])
(cond
[(lexp-has-var? (leq-lhs ineq) x)
(values (cons ineq xlhs) xrhs nox)]
[(lexp-has-var? (leq-rhs ineq) x)
(values xlhs (cons ineq xrhs) nox)]
[else
(values xlhs xrhs (cons ineq nox))]))))
(module+ test
(check-equal? (let-values ([(lt gt no)
(sli-partition (list (leq (lexp* '(2 x) '(4 y) 1)
(lexp* '(2 y))))
'x)])
(list lt gt no))
(list (list (leq (lexp* '(2 x))
(lexp* '(-2 y) -1)))
(list)
(list)))
(check-equal? (let-values ([(lt gt no)
(sli-partition (list (leq (lexp* '(2 x) '(4 y) 1)
(lexp* '(2 y)))
(leq (lexp* '(2 x) '(4 y))
(lexp* '(2 y) '(42 x))))
'x)])
(list lt gt no))
(list (list (leq (lexp* '(2 x))
(lexp* '(-2 y) -1)))
(list (leq (lexp* '(2 y))
(lexp* '(40 x))))
(list)))
(check-equal? (let-values ([(lt gt no)
(sli-partition (list (leq (lexp* '(2 x) '(4 y) -1)
(lexp* '(2 y)))
(leq (lexp* '(2 x) '(4 y))
(lexp* '(2 y) '(42 x)))
(leq (lexp* '(2 z) '(4 y))
(lexp* '(2 y) '(42 q))))
'x)])
(list lt gt no))
(list (list (leq (lexp* '(2 x))
(lexp* '(-2 y) 1)))
(list (leq (lexp* '(2 y))
(lexp* '(40 x))))
(list (leq (lexp* '(2 z) '(4 y))
(lexp* '(2 y) '(42 q)))))))
;; fme-elim
;; reduces the system of linear inequalties, eliminating x
;; (does so while preventing duplicate leqs)
(define/cond-contract (fme-elim sli x)
(-> sli? any/c sli?)
(define-values (xltleqs xgtleqs noxleqs) (sli-partition sli x))
(define leqs (make-hash))
(for ([l (in-list noxleqs)])
(hash-set! leqs l #t))
(for* ([l1 (in-list xltleqs)]
[l2 (in-list xgtleqs)])
(hash-set! leqs (leq-join l1 l2 x) #t))
(hash-keys leqs))
;; sli-satisfiable?
(define/cond-contract (fme-sat? sli)
(-> sli? boolean?)
(let* ([vars (sli-vars sli)]
[simple-system (for/fold ([s sli])
([x (in-list vars)])
(fme-elim s x))])
(for/and ([ineq (in-list simple-system)])
(leq-trivially-valid? ineq))))
(module+ test
; 3x + 2y <= 7; 6x + 4y <= 15; -x <= 1; 0 <= 2y has integer solutions
(check-true (fme-sat? (list (leq (lexp* '(3 x) '(2 y))
(lexp* 7))
(leq (lexp* '(6 x) '(4 y))
(lexp* 15))
(leq (lexp* '(-1 x))
(lexp* 1))
(leq (lexp* 0)
(lexp* '(2 y))))))
; 3x + 2y <= 4; 1 <= x; 1 <= y no solutions
(check-false (fme-sat? (list (leq (lexp* '(3 x) '(2 y))
(lexp* 4))
(leq (lexp* 1)
(lexp* '(1 x)))
(leq (lexp* 1)
(lexp* '(1 y)))))))
;;**********************************************************************
;; Logical Implication for Integer Linear Inequalities
;; using Fourier-Motzkin elimination
;;**********************************************************************
(define/cond-contract (fme-imp-leq? s ineq)
(-> sli? leq? boolean?)
(or (and (member ineq s) #t)
(not (fme-sat? (cons (leq-negate ineq) s)))))
(module+ test
; transitivity! x <= y /\ y <= z --> x <= z
(check-true (fme-imp-leq? (list (leq (lexp* '(1 x))
(lexp* '(1 y)))
(leq (lexp* '(1 y))
(lexp* '(1 z))))
(leq (lexp* '(1 x))
(lexp* '(1 z)))))
; x <= x;
(check-true (fme-imp-leq? (list)
(leq (lexp* '(1 x))
(lexp* '(1 x)))))
; x - 1 <= x + 1;
(check-true (fme-imp-leq? (list)
(leq (lexp* '(1 x) -1)
(lexp* '(1 x) 1))))
; x + y <= z; 1 <= y; 0 <= x --> x + 1 <= z
(check-true (fme-imp-leq? (list (leq (lexp* '(1 x) '(1 y))
(lexp* '(1 z)))
(leq (lexp* 1)
(lexp* '(1 y)))
(leq (lexp*)
(lexp* '(1 x))))
(leq (lexp* '(1 x) 1)
(lexp* '(1 z))))))
;;**********************************************************************
;; Simple Inequality Implication (does P imply Q)
;;**********************************************************************
(define/cond-contract (leq-imp-leq? P Q)
(-> leq? leq? boolean?)
(or (equal? P Q)
;; (P -> Q) == (~P or Q) == ~(P and ~Q)
(not (fme-sat? (list P (leq-negate Q))))))
(module+ test
(check-true (leq-imp-leq? (leq (lexp* '(1 x))
(lexp* '(1 y)))
(leq (lexp* '(1 x))
(lexp* '(1 y)))))
(check-true (leq-imp-leq? (leq (lexp* '(1 x))
(lexp* 14))
(leq (lexp* '(1 x))
(lexp* 15))))
(check-true (leq-imp-leq? (leq (lexp* '(1 x) '(1 y))
(lexp* 14))
(leq (lexp* '(1 x) '(1 y))
(lexp* 20))))
(check-false (leq-imp-leq? (leq (lexp* '(1 x) '(1 y))
(lexp* 14))
(leq (lexp* '(1 x))
(lexp* 14)))))
;;**********************************************************************
;; Contradictory leqs? ~(P and Q)
;;**********************************************************************
(define/cond-contract (contradictory-leqs? P Q)
(-> leq? leq? boolean?)
;; (P -> Q) == (~P or Q) == ~(P and ~Q)
(not (fme-sat? (list P Q))))
(module+ test
(check-true (contradictory-leqs? (leq (lexp* 2)
(lexp* 1))
(leq (lexp* '(1 y))
(lexp* '(1 x)))))
(check-true (contradictory-leqs? (leq (lexp* '(1 x))
(lexp* '(1 y)))
(leq (lexp* 1 '(1 y))
(lexp* '(1 x)))))
(check-false (contradictory-leqs? (leq (lexp* '(1 x))
(lexp* '(1 y)))
(leq (lexp* '(1 x))
(lexp* '(1 y)))))
(check-false (contradictory-leqs? (leq (lexp* 1)
(lexp* 2))
(leq (lexp* 2)
(lexp* 3)))))
;;**********************************************************************
;; Logical Implication for Systems of Integer Linear Inequalities
;; using Fourier-Motzkin elimination
;;**********************************************************************
(define/cond-contract (fme-imp? axioms goals)
(-> sli? sli? boolean?)
(for/and ([ineq (in-list goals)])
(fme-imp-leq? axioms ineq)))
(module+ test
;; 4 <= 3 is false
(check-false (fme-imp? (list)
(list (leq (lexp* 4)
(lexp* 3)))))
;; P and ~P --> false
(check-true (fme-imp? (list (leq (lexp*) (lexp* '(1 y)))
(leq-negate (leq (lexp*) (lexp* '(1 y)))))
(list (leq (lexp* 4)
(lexp* 3)))))
;; x + y <= z; 0 <= y; 0 <= x --> x <= z /\ y <= z
(check-true (fme-imp? (list (leq (lexp* '(1 x) '(1 y))
(lexp* '(1 z)))
(leq (lexp*)
(lexp* '(1 y)))
(leq (lexp*)
(lexp* '(1 x))))
(list (leq (lexp* '(1 x))
(lexp* '(1 z)))
(leq (lexp* '(1 y))
(lexp* '(1 z))))))
;; x + y <= z; 0 <= y; 0 <= x -/-> x <= z /\ y <= q
(check-false (fme-imp? (list (leq (lexp* '(1 x) '(1 y))
(lexp* '(1 z)))
(leq (lexp*)
(lexp* '(1 y)))
(leq (lexp*)
(lexp* '(1 x))))
(list (leq (lexp* '(1 x))
(lexp* '(1 z)))
(leq (lexp* '(1 y))
(lexp* '(1 q))))))
;; 7x <= 29 --> x <= 4
(check-true (fme-imp? (list (leq (lexp* '(7 x))
(lexp* 29)))
(list (leq (lexp* '(1 x))
(lexp* 4)))))
;; 7x <= 28 --> x <= 4
(check-true (fme-imp? (list (leq (lexp* '(7 x))
(lexp* 28)))
(list (leq (lexp* '(1 x))
(lexp* 4)))))
;; 7x <= 28 does not --> x <= 3
(check-false (fme-imp? (list (leq (lexp* '(7 x))
(lexp* 28)))
(list (leq (lexp* '(1 x))
(lexp* 3)))))
;; 7x <= 27 --> x <= 3
(check-true (fme-imp? (list (leq (lexp* '(7 x))
(lexp* 27)))
(list (leq (lexp* '(1 x))
(lexp* 3)))))
;; 4x+3y+9z+20q-100r + 42 <= 4x+3y+9z+20q+100r;
;; x <= y + z;
;; 29r <= x + y + z + q;
;; 0 <= x;
;; 0 <= x + y + z;
;; 0 <= x + z;
;; x <= z
;; z + 1 <= t
;; 0 <= x + y;
;; 0 <= x + r;
;; 0 <= x + r + q;
;; -->
;; 0 <= t
(check-true (fme-imp? (list (leq (lexp* '(4 x) '(3 y) '(9 z) '(20 q) '(-100 r) 42)
(lexp* '(4 x) '(3 y) '(9 z) '(20 q) '(100 r)))
(leq (lexp* '(1 x))
(lexp* '(1 y) '(1 z)))
(leq (lexp* '(29 r))
(lexp* '(1 x) '(1 y) '(1 z) '(1 q)))
(leq (lexp*)
(lexp* '(1 x)))
(leq (lexp*)
(lexp* '(1 x) '(1 y) '(1 z)))
(leq (lexp*)
(lexp* '(1 x) '(1 z)))
(leq (lexp* '(1 x))
(lexp* '(1 z)))
(leq (lexp* '(1 z) 1)
(lexp* '(1 t)))
(leq (lexp*)
(lexp* '(1 x) '(1 y)))
(leq (lexp*)
(lexp* '(1 x) '(1 r)))
(leq (lexp*)
(lexp* '(1 x) '(1 r) '(1 q))))
(list (leq (lexp*)
(lexp* '(1 t))))))
;; 4x+3y+9z+20q-100r + 42 <= 4x+3y+9z+20q+100r;
;; x <= y + z;
;; 29r <= x + y + z + q;
;; 0 <= x;
;; 0 <= x + y + z;
;; 0 <= x + z;
;; x <= z
;; z + 1 <= t
;; 0 <= x + y;
;; 0 <= x + r;
;; 0 <= x + r + q;
;; -/->
;; t <= 0
(check-false (fme-imp? (list (leq (lexp* '(4 x) '(3 y) '(9 z) '(20 q) '(-100 r) 42)
(lexp* '(4 x) '(3 y) '(9 z) '(20 q) '(100 r)))
(leq (lexp* '(1 x))
(lexp* '(1 y) '(1 z)))
(leq (lexp* '(29 r))
(lexp* '(1 x) '(1 y) '(1 z) '(1 q)))
(leq (lexp*)
(lexp* '(1 x)))
(leq (lexp*)
(lexp* '(1 x) '(1 y) '(1 z)))
(leq (lexp*)
(lexp* '(1 x) '(1 z)))
(leq (lexp* '(1 x))
(lexp* '(1 z)))
(leq (lexp* '(1 z) 1)
(lexp* '(1 t)))
(leq (lexp*)
(lexp* '(1 x) '(1 y)))
(leq (lexp*)
(lexp* '(1 x) '(1 r)))
(leq (lexp*)
(lexp* '(1 x) '(1 r) '(1 q))))
(list (leq (lexp* '(1 t))
(lexp*))))))

View File

@ -0,0 +1,20 @@
#lang racket/base
(require racket/lazy-require)
(lazy-require
("../typecheck/tc-envops.rkt" (implies-in-env?))
("../typecheck/tc-subst.rkt" (instantiate-rep/obj)))
(provide (rename-out [implies-in-env?-for-stupid-infer-unit
implies-in-env?]
[instantiate-rep/obj-for-stupid-infer-unit
instantiate-rep/obj]))
;; the units for infer currently make it impossible to do
;; lazy requires
(define (implies-in-env?-for-stupid-infer-unit env p q)
(implies-in-env? env p q))
(define (instantiate-rep/obj-for-stupid-infer-unit rep obj type)
(instantiate-rep/obj rep obj type))

View File

@ -3,9 +3,10 @@
;; This module provides functions for parsing types written by the user
(require (rename-in "../utils/utils.rkt" [infer infer-in])
(except-in (rep core-rep type-rep object-rep) make-arr)
(except-in (rep core-rep type-rep object-rep rep-utils) make-arr)
(rename-in (types abbrev utils prop-ops resolve
classes prefab signatures)
classes prefab signatures
subtype path-type numeric-tower)
[make-arr* make-arr])
(only-in (infer-in infer) intersect)
(utils tc-utils stxclass-util literal-syntax-class)
@ -45,6 +46,12 @@
current-referenced-class-parents
current-type-alias-name)
;; current-term-names : Parameter<(Listof Id)>
;; names currently "bound" by a type we are parsing
;; e.g. (Refine [x : τ] ψ) -- x would be added to
;; current-term-names when parsing ψ
(define current-term-names (make-parameter '()))
;; current-type-alias-name : Parameter<(Option Id)>
;; This parameter stores the name of the type alias that is
;; being parsed (set in type-alias-helper.rkt), #f if the
@ -79,6 +86,7 @@
(define-literal-syntax-class #:for-label car)
(define-literal-syntax-class #:for-label cdr)
(define-literal-syntax-class #:for-label vector-length)
(define-literal-syntax-class #:for-label colon^ (:))
(define-literal-syntax-class #:for-label quote)
(define-literal-syntax-class #:for-label cons)
@ -116,6 +124,22 @@
(define-literal-syntax-class #:for-label Sequenceof)
(define-literal-syntax-class #:for-label )
(define-literal-syntax-class #:for-label Intersection)
(define-literal-syntax-class #:for-label Refine)
(define-literal-syntax-class #:for-label not)
(define-literal-syntax-class #:for-label and)
(define-literal-syntax-class #:for-label or)
(define-literal-syntax-class #:for-label unless)
(define-literal-syntax-class #:for-label when)
(define-literal-syntax-class #:for-label if)
(define-literal-syntax-class #:for-label <)
(define-literal-syntax-class #:for-label <=)
(define-literal-syntax-class #:for-label >)
(define-literal-syntax-class #:for-label >=)
(define-literal-syntax-class #:for-label =)
(define-literal-syntax-class #:for-label *)
(define-literal-syntax-class #:for-label +)
;; (Syntax -> Type) -> Syntax Any -> Syntax
;; See `parse-type/id`. This is a curried generalization.
@ -238,9 +262,9 @@
(define-syntax-class path-elem
#:description "path element"
(pattern :car^
#:attr pe -car)
#:attr val -car)
(pattern :cdr^
#:attr pe -cdr))
#:attr val -cdr))
(define-syntax-class @
@ -255,11 +279,152 @@
#:description "latent prop"
(pattern (~seq t:expr :@ pe:path-elem ...)
#:attr type (parse-type #'t)
#:attr path (attribute pe.pe))
#:attr path (attribute pe.val))
(pattern t:expr
#:attr type (parse-type #'t)
#:attr path '()))
;; old + deprecated
(define-syntax-class proposition
#:description "proposition"
#:attributes (val)
(pattern :Top^ #:attr val -tt)
(pattern :Bot^ #:attr val -ff)
(pattern (:colon^ o:symbolic-object t:expr)
#:attr val (-is-type (attribute o.val) (parse-type #'t)))
(pattern (:! o:symbolic-object t:expr)
#:attr val (-not-type (attribute o.val) (parse-type #'t)))
(pattern (:and^ p:proposition ...)
#:attr val (apply -and (attribute p.val)))
(pattern (:or^ p:proposition ...)
#:attr val (apply -or (attribute p.val)))
(pattern (:unless^ p1:proposition p2:proposition)
#:attr val (-or (attribute p1.val) (attribute p2.val)))
(pattern (:when^ p1:proposition p2:proposition)
#:attr val (-or (negate-prop (attribute p1.val))
(-and (attribute p1.val) (attribute p2.val))))
(pattern (:if^ p1:proposition p2:proposition p3:proposition)
#:attr val (let ([tst (attribute p1.val)]
[thn (attribute p2.val)]
[els (attribute p3.val)])
(-or (-and tst thn)
(-and (negate-prop tst) els))))
(pattern (:not^ p:proposition)
#:attr val (negate-prop (attribute p.val)))
(pattern (:<=^ lhs:inequality-symbolic-object
rhs:inequality-symbolic-object)
#:attr val (-leq (attribute lhs.val)
(attribute rhs.val)))
(pattern (:<^ lhs:inequality-symbolic-object
rhs:inequality-symbolic-object)
#:attr val (-lt (attribute lhs.val)
(attribute rhs.val)))
(pattern (:>=^ lhs:inequality-symbolic-object
rhs:inequality-symbolic-object)
#:attr val (-geq (attribute lhs.val)
(attribute rhs.val)))
(pattern (:>^ lhs:inequality-symbolic-object
rhs:inequality-symbolic-object)
#:attr val (-gt (attribute lhs.val)
(attribute rhs.val)))
(pattern (:=^ lhs:inequality-symbolic-object
rhs:inequality-symbolic-object)
#:attr val (-eq (attribute lhs.val)
(attribute rhs.val))))
(define-syntax-class inequality-symbolic-object
#:description "symbolic object in an inequality"
#:attributes (val)
(pattern o:symbolic-object
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty -Int)
(format "terms in linear constraints must be integers, got ~a for ~a"
obj-ty obj)
#:attr val (attribute o.val)))
(define-syntax-class symbolic-object
#:description "symbolic object"
#:attributes (val)
(pattern (:+^ ~! . l:linear-expression-body)
#:attr val (attribute l.val))
(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-unless (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 o:symbolic-object-w/o-lexp
#:attr val (attribute o.val))
)
(define-syntax-class symbolic-object-w/o-lexp
#:description "symbolic object"
#:attributes (val)
(pattern i:id
#:fail-unless (or (identifier-binding #'i)
(assoc #'i (current-term-names) free-identifier=?))
"Propositions may not reference identifiers that are unbound"
#:fail-when (is-var-mutated? #'i)
"Propositions may not reference identifiers that are mutated"
#:attr val (match (assoc #'i (current-term-names) free-identifier=?)
[(cons _ local-name) (-id-path local-name)]
[_ (-id-path #'i)]))
(pattern (:car^ ~! o:symbolic-object-w/o-lexp)
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty (-pair Univ Univ))
(format "car expects a pair, but got ~a for ~a"
obj-ty obj)
#:attr val (-car-of (attribute o.val)))
(pattern (:cdr^ ~! o:symbolic-object-w/o-lexp)
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty (-pair Univ Univ))
(format "cdr expects a pair, but got ~a for ~a"
obj-ty obj)
#:attr val (-cdr-of (attribute o.val)))
(pattern (:vector-length^ ~! o:symbolic-object-w/o-lexp)
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty -VectorTop)
(format "vector-length expects a vector, but got ~a for ~a"
obj-ty obj)
#:attr val (-vec-len-of (attribute o.val))))
(define-syntax-class linear-expression-body
#:description "symbolic object"
#:attributes (val)
(pattern (t:linear-expression-term ts:linear-expression-term ...)
#:attr val (apply -lexp (attribute t.val) (attribute ts.val)))
)
(define-syntax-class linear-expression-term
#:description "symbolic object"
#: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-unless (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 o:symbolic-object-w/o-lexp
#:do [(define obj (attribute o.val))
(define obj-ty (lookup-obj-type/lexical obj))]
#:fail-unless (subtype obj-ty -Int)
(format "terms in linear expressions must be integers, got ~a for ~a"
obj-ty obj)
#:attr val (attribute o.val))
)
;; old + deprecated
(define-syntax-class (prop doms)
#:description "proposition"
#:attributes (prop)
@ -267,10 +432,10 @@
(pattern :Bot^ #:attr prop -ff)
;; Here is wrong check
(pattern (t:expr :@ ~! pe:path-elem ... (~var o (prop-object doms)))
#:attr prop (-is-type (-acc-path (attribute pe.pe) (attribute o.obj)) (parse-type #'t)))
#:attr prop (-is-type (-acc-path (attribute pe.val) (attribute o.obj)) (parse-type #'t)))
;; Here is wrong check
(pattern (:! t:expr :@ ~! pe:path-elem ... (~var o (prop-object doms)))
#:attr prop (-not-type (-acc-path (attribute pe.pe) (attribute o.obj)) (parse-type #'t)))
#:attr prop (-not-type (-acc-path (attribute pe.val) (attribute o.obj)) (parse-type #'t)))
(pattern (:! t:expr)
#:attr prop (-not-type 0 (parse-type #'t)))
(pattern ((~datum and) (~var p (prop doms)) ...)
@ -352,7 +517,7 @@
[(:Object^ e ...)
(parse-object-type stx)]
[(:Refinement^ p?:id)
(match (lookup-type/lexical #'p?)
(match (lookup-id-type/lexical #'p?)
[(and t (Function: (list (arr: (list dom) _ #f #f '()))))
(make-Refinement dom #'p?)]
[t (parse-error "expected a predicate for argument to Refinement"
@ -382,6 +547,17 @@
"key" (prefab-key->field-count new-key)
"fields" num-fields))
(make-Prefab new-key (parse-types #'(ts ...)))]
[(:Refine^ [x:id :colon^ type:expr] prop:expr)
(define local-name (gen-pretty-id (syntax->datum #'x)))
(define t (parse-type #'type))
(define p (with-extended-lexical-env
[#:identifiers (list local-name)
#:types (list t)]
(parameterize ([current-term-names (cons (cons #'x local-name) (current-term-names))])
(syntax-parse #'prop [p:proposition (attribute p.val)]))))
(define refinement-type (-refine local-name t p))
(save-term-var-names! refinement-type (list local-name))
refinement-type]
[(:Instance^ t)
(let ([v (parse-type #'t)])
(if (not (or (F? v) (Mu? v) (Name? v) (Class? v) (Error? v)))
@ -453,18 +629,24 @@
(let ([t* (parse-type #'t)])
;; is t in a productive position?
(define productive
(let loop ([ty t*])
(match ty
[(Union: _ elems) (andmap loop elems)]
[(Intersection: elems) (andmap loop elems)]
[(F: _) (not (equal? ty tvar))]
[(App: rator rands)
(loop (resolve-app rator rands stx))]
[(Mu: _ body) (loop body)]
[(Poly: names body) (loop body)]
[(PolyDots: names body) (loop body)]
[(PolyRow: _ _ body) (loop body)]
[else #t])))
(let/ec return
(let check ([ty t*])
(match ty
[(== tvar) (return #f)]
[(Union: _ elems) (for-each check elems)]
[(Intersection: elems prop)
(for-each check elems)
(check prop)]
[(App: rator rands)
(check (resolve-app rator rands stx))]
[(Mu: _ body) (check body)]
[(Poly: names body) (check body)]
[(PolyDots: names body) (check body)]
[(PolyRow: _ _ body) (check body)]
[(? Type?) (void)]
[(? Rep?) (Rep-for-each check ty)]
[_ (void)]))
#t))
(unless productive
(parse-error
#:stx stx

View File

@ -5,7 +5,7 @@
(require
"../utils/utils.rkt"
syntax/parse
(rep type-rep prop-rep object-rep)
(rep type-rep prop-rep object-rep fme-utils)
(utils tc-utils)
(env type-name-env row-constraint-env)
(rep core-rep rep-utils type-mask values-rep base-types numeric-base-types)
@ -346,7 +346,40 @@
(loop t 'both recursive-values))
(define (t->sc/fun t) (t->sc/function t fail typed-side recursive-values loop #f))
(define (t->sc/meth t) (t->sc/method t fail typed-side recursive-values loop))
(define (prop->sc p)
(match p
[(TypeProp: o (app t->sc tc))
(cond
[(not (equal? flat-sym (get-max-contract-kind tc)))
(fail #:reason "proposition contract generation not supported for non-flat types")]
[else (is-flat-type/sc (obj->sc o) tc)])]
[(NotTypeProp: o (app t->sc tc))
(cond
[(not (equal? flat-sym (get-max-contract-kind tc)))
(fail #:reason "proposition contract generation not supported for non-flat types")]
[else (not-flat-type/sc (obj->sc o) tc)])]
[(LeqProp: (app obj->sc lhs) (app obj->sc rhs))
(leq/sc lhs rhs)]
;; TODO: check for (<= x y) and (<= y x)
;; and generate and = instead of two <=
[(AndProp: ps)
(and-prop/sc (map prop->sc ps))]
[(OrProp: ps)
(or-prop/sc (map prop->sc ps))]))
(define (obj->sc o)
(match o
[(Path: pes (? identifier? x))
(for/fold ([obj (id/sc x)])
([pe (in-list (reverse pes))])
(match pe
[(CarPE:) (acc-obj/sc #'car obj)]
[(CdrPE:) (acc-obj/sc #'cdr obj)]
[(VecLenPE:) (acc-obj/sc #'vector-length obj)]))]
[(LExp: const terms)
(linear-exp/sc const
(for/hash ([(obj coeff) (in-terms terms)])
(values (obj->sc obj) coeff)))]))
(define (only-untyped sc)
(if (from-typed? typed-side)
(and/sc sc any-wrap/sc)
@ -375,7 +408,7 @@
(recursive-sc-use name*))])]
;; Implicit recursive aliases
[(Name: name-id args #f)
(cond [ ;; recursive references are looked up in a special table
(cond [;; recursive references are looked up in a special table
;; that's handled differently by sc instantiation
(lookup-name-sc type typed-side)]
[else
@ -420,21 +453,39 @@
[(Union: (? Bottom?) elems) (apply or/sc (map t->sc elems))]
[(Union: base elems) (apply or/sc (t->sc base) (map t->sc elems))]
[t (t->sc t)])]
[(Intersection: ts)
(define-values (chaperones/impersonators others)
(for/fold ([cs/is null] [others null])
[(Intersection: ts raw-prop)
(define-values (impersonators chaperones others)
(for/fold ([imps null]
[chaps null]
[flats null])
([elem (in-list ts)])
(define c (t->sc elem))
(if (equal? flat-sym (get-max-contract-kind c))
(values cs/is (cons c others))
(values (cons c cs/is) others))))
(match (get-max-contract-kind c)
[(== flat-sym) (values imps chaps (cons c flats))]
[(== chaperone-sym) (values imps (cons c chaps) flats)]
[(== impersonator-sym) (values (cons c imps) chaps flats)])))
(define prop
(cond
[(TrueProp? raw-prop) #f]
[else (define x (gen-pretty-id))
(define prop (Intersection-prop (-id-path x) type))
(define name (format "~a" `(λ (,(syntax->datum x)) ,prop)))
(flat-named-lambda/sc name
(id/sc x)
(prop->sc prop))]))
(cond
[(> (length chaperones/impersonators) 1)
[(> (+ (length impersonators) (length chaperones)) 1)
(fail #:reason (~a "Intersection type contract contains"
" more than 1 non-flat contract: "
type))]
[(and prop (not (null? impersonators)))
(fail #:reason (~a "Cannot logically refine an impersonated value: "
type))]
[else
(apply and/sc (append others chaperones/impersonators))])]
(apply and/sc (append others
chaperones
(if prop (list prop) '())
impersonators))])]
[(and t (Function: arrs))
#:when (any->bool? arrs)
;; Avoid putting (-> any T) contracts on struct predicates (where Boolean <: T)
@ -647,8 +698,13 @@
(channel/sc (t->sc t))]
[(Evt: t)
(evt/sc (t->sc t))]
[else
(fail #:reason "contract generation not supported for this type")]))))
[rep
(cond
[(Prop? rep)
(fail #:reason "contract generation not supported for this proposition")]
[else
(fail #:reason "contract generation not supported for this type")])]))))
(define (t->sc/function f fail typed-side recursive-values loop method?)
(define (t->sc t #:recursive-values (recursive-values recursive-values))
@ -789,7 +845,7 @@
(match (resolve ty)
[(Function: _) #t]
[(Union: _ elems) (andmap loop elems)]
[(Intersection: elems) (ormap loop elems)]
[(Intersection: elems _) (ormap loop elems)]
[(Poly: _ body) (loop body)]
[(PolyDots: _ body) (loop body)]
[_ #f])))
@ -828,7 +884,7 @@
(match (resolve ty)
[(Function: _) #t]
[(Union: _ elems) (andmap loop elems)]
[(Intersection: elems) (ormap loop elems)]
[(Intersection: elems _) (ormap loop elems)]
[(Poly: _ body) (loop body)]
[(PolyDots: _ body) (loop body)]
[_ #f])))

View File

@ -1,11 +1,13 @@
#lang racket/base
(require "rep-utils.rkt"
(require "../utils/utils.rkt"
"rep-utils.rkt"
"type-mask.rkt"
"core-rep.rkt"
"base-types.rkt"
"numeric-base-types.rkt"
racket/match
(contract-req)
(for-syntax racket/base))
(provide BaseUnion-bases:
@ -31,7 +33,10 @@
[(eqv? #b0 bbits) mask:number]
[(eqv? #b0 nbits) mask:base]
[else mask:base+number])])]
[#:custom-constructor
[#:custom-constructor/contract
(-> exact-nonnegative-integer?
exact-nonnegative-integer?
Type?)
;; make sure we do not build BaseUnions equivalent to
;; Bottom or a *single* Base type
(cond

View File

@ -29,7 +29,7 @@
def-values
def-prop
def-object
def-pathelem)
def-path-elem)
;;************************************************************
@ -136,7 +136,7 @@
;;--------------
;; e.g. car, cdr, etc
(def-rep-class PathElem #:printer print-pathelem #:define-form def-pathelem)
(def-rep-class PathElem #:printer print-pathelem #:define-form def-path-elem)
;;----------

View File

@ -0,0 +1,57 @@
#lang racket/base
(require "../utils/utils.rkt"
"core-rep.rkt"
(for-syntax racket/base)
(contract-req))
(provide (all-defined-out))
(define-for-cond-contract terms/c (hash/c Object? (and/c exact-integer?
(not zero?))))
(define-syntax terms-count (make-rename-transformer #'hash-count))
(define-syntax terms-vars (make-rename-transformer #'hash-keys))
(define-syntax terms-coeffs (make-rename-transformer #'hash-values))
(define-syntax terms-empty? (make-rename-transformer #'hash-empty?))
(define-syntax in-terms (make-rename-transformer #'in-immutable-hash))
(define-syntax in-terms-vars (make-rename-transformer #'in-immutable-hash-keys))
(define-syntax in-terms-coeffs (make-rename-transformer #'in-immutable-hash-values))
(define-syntax terms-remove (make-rename-transformer #'hash-remove))
(define-syntax make-terms (make-rename-transformer #'hasheq))
(define-syntax terms->list (make-rename-transformer #'hash->list))
(define-syntax-rule (terms-ref ts x)
(hash-ref ts x 0))
(define/cond-contract (terms-set h x i)
(-> (hash/c any/c exact-integer? #:immutable #t)
any/c
exact-integer?
(hash/c any/c exact-integer? #:immutable #t))
(if (= 0 i)
(hash-remove h x)
(hash-set h x i)))
(define/cond-contract (terms-scale ts a)
(-> (and/c hash? hash-eq?) rational? (and/c hash? hash-eq?))
(cond
[(zero? a) (hasheq)]
[(= a 1) ts]
[else
(for/hasheq ([(x coeff) (in-hash ts)])
(values x (* coeff a)))]))
(define/cond-contract (terms-subtract l1-terms l2-terms)
(-> (and/c hash? hash-eq?) (and/c hash? hash-eq?) (and/c hash? hash-eq?))
(for/fold ([h l1-terms])
([(x coeff) (in-hash l2-terms)])
(terms-set h x (- (hash-ref l1-terms x 0) coeff))))
(define/cond-contract (terms-add l1-terms l2-terms)
(-> (and/c hash? hash-eq?) (and/c hash? hash-eq?) (and/c hash? hash-eq?))
(for/fold ([h l1-terms])
([(x coeff) (in-hash l2-terms)])
(terms-set h x (+ (hash-ref l1-terms x 0) coeff))))

View File

@ -6,6 +6,7 @@
;; See "Logical Types for Untyped Languages" pg.3
(require "../utils/utils.rkt"
"fme-utils.rkt"
racket/match
"rep-utils.rkt"
"core-rep.rkt"
@ -13,19 +14,53 @@
(env mvar-env)
(contract-req))
(provide -id-path name-ref=?)
(provide -id-path
name-ref=?
-path-elem-of
-lexp-add1
-lexp-sub1
LExp-const
constant-LExp?
-lexp
-obj+
-obj*
LExp?
LExp-const
LExp-terms
LExp:
genobj
make-obj-seq
obj-seq-next
(rename-out [make-LExp* make-LExp]
[make-LExp raw-make-LExp])
(all-from-out "fme-utils.rkt"))
(def-pathelem CarPE () [#:singleton -car])
(def-pathelem CdrPE () [#:singleton -cdr])
(def-pathelem SyntaxPE () [#:singleton -syntax-e])
(def-pathelem ForcePE () [#:singleton -force])
(def-pathelem FieldPE () [#:singleton -field])
(def-pathelem StructPE ([t Type?] [idx natural-number/c])
(def-path-elem CarPE () [#:singleton -car])
(def-path-elem CdrPE () [#:singleton -cdr])
(def-path-elem SyntaxPE () [#:singleton -syntax-e])
(def-path-elem ForcePE () [#:singleton -force])
(def-path-elem FieldPE () [#:singleton -field])
(def-path-elem VecLenPE () [#:singleton -vec-len])
(def-path-elem StructPE ([t Type?] [idx natural-number/c])
[#:frees (f) (f t)]
[#:fmap (f) (make-StructPE (f t) idx)]
[#:for-each (f) (f t)])
(define/match (-path-elem-of pe o)
[(pe (Path: pes x)) (make-Path (cons pe pes) x)]
[(_ _) -empty-obj])
(define/provide (-car-of o) (-path-elem-of -car o))
(define/provide (-cdr-of o) (-path-elem-of -cdr o))
(define/provide (-syntax-of o) (-path-elem-of -syntax-e o))
(define/provide (-force-of o) (-path-elem-of -force o))
(define/provide (-vec-len-of o) (-path-elem-of -vec-len o))
(define/provide (-struct-idx-of t idx o)
(if (Empty? o) ;; lets not make the pe if we don't need to
o
(-path-elem-of (make-StructPE t idx) o)))
(def-object Path ([elems (listof PathElem?)] [name name-ref/c])
[#:frees (f) (combine-frees (map f elems))]
[#:fmap (f) (make-Path (map f elems) name)]
@ -33,16 +68,257 @@
[#:custom-constructor
(cond
[(identifier? name)
(if (is-var-mutated? name)
;; we don't want objects for visibly mutated or top level variables
(if (or (is-var-mutated? name)
(and (not (identifier-binding name))
(not (local-tr-identifier? name))))
-empty-obj
(let ([name (normalize-id name)])
(intern-double-ref!
path-intern-table
Path-intern-table
name elems #:construct (make-Path elems name))))]
[else (intern-double-ref!
path-intern-table
Path-intern-table
name elems #:construct (make-Path elems name))])])
(define path-intern-table (make-weak-hash))
(define Path-intern-table (make-weak-hash))
(define (-id-path name) (make-Path null name))
;; generates a fresh id object
;; NOTE: use this wisely -- calling this function
;; all the time will consume memory leading to GC
;; time that may add up during typechecking
(define (genobj) (-id-path (genid)))
;; creates an "object sequence" -- use 'obj-seq-next'
;; to iterate through the sequence.
;; For an example use case, see subtype.rkt,
;; which uses a seq to reuse fresh objects for subtype
;; checking
(define (make-obj-seq)
(for/fold ([seq (cons (genobj) (box #f))])
([_ (in-range 9)])
(cons (genobj) seq)))
;; obj-seq-next
;;
;; returns 2 values
;; val 1 - the next object
;; val 2 - the rest of the sequence
(define (obj-seq-next s)
(match s
[(cons val vals)
(values val vals)]
[(box (cons val vals))
(values val vals)]
[(box #f)
(define more (make-obj-seq))
(if (box-cas! s #f more)
(obj-seq-next more)
(obj-seq-next s))]))
(def-object LExp ([const exact-integer?]
[terms (hash/c Path? (and/c exact-integer?
(not/c zero?)))])
#:no-provide
[#:frees (f) (combine-frees (for/list ([x (in-terms-vars terms)]) (f x)))]
[#:fmap (f)
;; applies f to each object p in the terms
;; + if, for any p, (f p) returns Empty for any p, Empty is returned
;; + for any p where (f p) returns a LExp, it is multiplied by the
;; original coefficient of p and added to the LExp
;; + for p's where (f p) = some Path, we just swap p and (f p) basically
(define-values (new-const new-terms)
(for*/fold ([c const]
[ts (make-terms)])
([orig-x (in-terms-vars terms)]
#:break (not c)
[x (in-value (f orig-x))])
(match x
;; empty, this linear expression is kaputt
[(Empty:) (values #f #f)]
[(? Path? x) (values c (terms-set ts x (terms-ref terms orig-x)))]
;; a linear expression -- scale it by
;; the old path's coeff and add it
[(LExp: new-const new-terms)
(define old-coeff (terms-ref terms orig-x))
(values (+ c (* old-coeff new-const))
(terms-add ts (terms-scale new-terms old-coeff)))])))
(if new-const
(make-LExp* new-const new-terms)
;; if const is #f then some term(s) became Empty
-empty-obj)]
[#:for-each (f) (for ([p (in-terms-vars terms)]) (f p))]
[#:custom-constructor
(intern-double-ref!
LExp-intern-table
terms const #:construct (make-LExp const terms))])
(define LExp-intern-table (make-weak-hash))
;; make-LExp* (provided as make-LExp)
;;
; IF the lexp (exp) contains only 1 variable,
;; and that variables its coefficient is 1,
; and the constant is 0
; THEN that lone variable is returned
; ELSE it returns the LExp
;; NOTE 1: We do this so there is a 'canonical form'
;; for linear expressions which are actually just
;; the underlying object, e.g. insteaf of
;; the LExp '0 + 1*x' we just want to return 'x'
;; NOTE 2: we will also provide 'make-LExp'
;; as 'raw-make-LExp' so that LeqProps can
;; have both the lhs and rhs be LExps regardless
;; if they are equivalent to a simpler object
(define/cond-contract (make-LExp* const terms)
(-> exact-integer? hash? (or/c LExp? Path?))
(cond
[(and (eqv? 0 const)
(eqv? 1 (terms-count terms))
(for/fold ([res #f])
([(obj coeff) (in-terms terms)])
(and (eqv? 1 coeff) obj)))]
[else (make-LExp const terms)]))
;; *****************************************************************************
;; Operations for Linear Expressions
;; constructor for LExps
(define/cond-contract (-lexp . raw-terms)
(->* () () #:rest (listof (or/c exact-integer?
name-ref/c
Path?
(list/c exact-integer? (or/c name-ref/c Path?))))
(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))
;; LExp-add1
(define/cond-contract (-lexp-add1 l)
(-> LExp? LExp?)
(match l
[(LExp: c terms)
(make-LExp* (add1 c) terms)]
[(? Object? p) (-lexp 1 p)]
[(? Empty?) -empty-obj]))
;; LExp-add1
(define/cond-contract (-lexp-sub1 l)
(-> LExp? LExp?)
(match l
[(LExp: c terms)
(make-LExp* (sub1 c) terms)]
[(? Object? p) (-lexp -1 p)]
[(? Empty?) -empty-obj]))
;; constant-LExp?
;; returns #f if this LExp contains non-zero variables
;; else returns the constant value of the LExp
(define/cond-contract (constant-LExp? l)
(-> LExp? (or/c #f exact-integer?))
(match l
[(LExp: c terms)
(if (hash-empty? terms)
c
#f)]))
(define/cond-contract (in-LExp? obj l)
(-> Path? LExp? boolean?)
(match l
[(LExp: _ terms) (hash-has-key? terms obj)]))
;;******************************************************************************
;; Mathematical operations for Objects
(define/cond-contract (-obj* . objs)
(->* () () #:rest (listof OptObject?) OptObject?)
(match objs
[(list) -empty-obj]
[(list o) o]
[(list o1 o2) (multiply-OptObjects o1 o2)]
[(list o1 o2 os ...)
(apply -obj* (multiply-OptObjects o1 o2) os)]))
;; multiply-Objects
;; 1. if either is empty, the result is empty
;; 2. if one is an object the other a constant-LExp?, then
;; the result is the object scaled by the constant
;; 3. if two non-constant objects are multiplied, the
;; result is empty (since we do not represent non-linear
;; expressions currently)
(define/cond-contract (multiply-OptObjects o1 o2)
(-> OptObject? OptObject? OptObject?)
(cond
[(or (Empty? o1) (Empty? o2)) -empty-obj]
[(and (LExp? o1) (constant-LExp? o1))
=> (scale-obj o2)]
[(and (LExp? o2) (constant-LExp? o2))
=> (scale-obj o1)]
[else -empty-obj]))
(define ((scale-obj o) c)
(match o
[(? Path?) (-lexp (list c o))]
[(LExp: const terms)
;; scaling doesn't modify which objects are in the LExp! =)
;; just constants & coefficients
(make-LExp* (* c const) (terms-scale terms c))]))
(define/cond-contract (-obj+ . objs)
(->* () () #:rest (listof OptObject?) OptObject?)
(match objs
[(list) -empty-obj]
[(list o) o]
[(list o1 o2) (add-OptObjects o1 o2)]
[(list o1 o2 os ...)
(apply -obj+ (add-OptObjects o1 o2) os)]))
(define (add-OptObjects o1 o2)
(match* (o1 o2)
[(_ _) #:when (or (Empty? o1) (Empty? o2))
-empty-obj]
[((? Path?) (? Path?))
(-lexp (list 1 o1) (list 1 o2))]
[((? LExp? l) (? Path? p))
(add-path-to-lexp p l)]
[((? Path? p) (? LExp? l))
(add-path-to-lexp p l)]
[((LExp: c1 terms1) (LExp: c2 terms2))
(make-LExp* (+ c1 c2) (terms-add terms1 terms2))]))
(define (add-path-to-lexp p l)
(match l
[(LExp: const terms)
(make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))

View File

@ -2,6 +2,7 @@
(require "../utils/utils.rkt"
(contract-req)
"fme-utils.rkt"
"rep-utils.rkt"
"free-variance.rkt"
"core-rep.rkt"
@ -11,25 +12,32 @@
(only-in racket/unsafe/ops unsafe-fx<=))
(lazy-require
["../types/prop-ops.rkt" (-and -or)])
["../types/prop-ops.rkt" (-and -or negate-prop)])
(provide -is-type
-not-type)
(provide/cond-contract
[-leq (-> OptObject? OptObject? Prop?)]
[-lt (-> OptObject? OptObject? Prop?)]
[-gt (-> OptObject? OptObject? Prop?)]
[-geq (-> OptObject? OptObject? Prop?)]
[-eq (-> OptObject? OptObject? Prop?)])
(def-prop TypeProp ([obj Object?] [type (and/c Type? (not/c Univ?) (not/c Bottom?))])
[#:frees (f) (combine-frees (list (f obj) (f type)))]
[#:fmap (f) (make-TypeProp (f obj) (f type))]
[#:for-each (f) (begin (f obj) (f type))]
[#:custom-constructor
(cond
[(Empty? obj) -tt]
[(Univ? type) -tt]
[(Bottom? type) -ff]
[else
(intern-double-ref!
tprop-intern-table
obj type #:construct (make-TypeProp obj type))])])
[#:custom-constructor/contract
(-> OptObject? Type? Prop?)
(match* (obj type)
[((Empty:) _) -tt]
[(_ (Univ:)) -tt]
[(_ (Bottom:)) -ff]
[(_ _) (intern-double-ref!
tprop-intern-table
obj type #:construct (make-TypeProp obj type))])])
(define tprop-intern-table (make-weak-hash))
@ -50,15 +58,15 @@
[#:frees (f) (combine-frees (list (f obj) (f type)))]
[#:fmap (f) (-not-type (f obj) (f type))]
[#:for-each (f) (begin (f obj) (f type))]
[#:custom-constructor
(cond
[(Empty? obj) -tt]
[(Univ? type) -ff]
[(Bottom? type) -tt]
[else
(intern-double-ref!
ntprop-intern-table
obj type #:construct (make-NotTypeProp obj type))])])
[#:custom-constructor/contract
(-> OptObject? Type? Prop?)
(match* (obj type)
[((Empty:) _) -tt]
[(_ (Univ:)) -ff]
[(_ (Bottom:)) -tt]
[(_ _) (intern-double-ref!
ntprop-intern-table
obj type #:construct (make-NotTypeProp obj type))])])
(define ntprop-intern-table (make-weak-hash))
@ -75,11 +83,66 @@
[else (-id-path i)]))
(make-NotTypeProp o t))
(def-prop OrProp ([ps (listof (or/c TypeProp? NotTypeProp?))])
;; an inequality between two linear inequalities
(def-prop LeqProp ([lhs LExp?] [rhs LExp?])
[#:frees (f) (combine-frees (list (f lhs) (f rhs)))]
[#:fmap (f) (make-LeqProp (f lhs) (f rhs))]
[#:for-each (f) (f lhs) (f rhs)]
;; a custom constructor which reduces trivially valid/invalid
[#:custom-constructor/contract
(-> OptObject? OptObject? (or/c LeqProp? TrueProp?))
(let-values
([(lhs rhs)
(match lhs
[(? LExp?)
(match rhs
[(? LExp?) (values lhs rhs)]
[(? Path?) (values lhs (raw-make-LExp 0 (make-terms rhs 1)))]
[(? Empty?) (values #f #f)])]
[(? Path?)
(let ([lhs (raw-make-LExp 0 (make-terms lhs 1))])
(match rhs
[(? LExp?) (values lhs rhs)]
[(? Path?) (values lhs (raw-make-LExp 0 (make-terms rhs 1)))]
[(? Empty?) (values #f #f)]))]
[(? Empty?) (values #f #f)])])
(match* (lhs rhs)
[((? LExp?) (? LExp?))
(cond
;; if the inequality is trivially true or false,
;; return the appropriate base prop (tt or ff)
[(eq? lhs rhs) -tt]
[(constant-LExp? lhs)
=> (λ (l-const)
(cond
[(constant-LExp? rhs)
=> (λ (r-const) (if (<= l-const r-const) -tt -ff))]
[else
(intern-double-ref!
Leq-intern-table
lhs rhs #:construct (make-LeqProp lhs rhs))]))]
[else
(intern-double-ref!
Leq-intern-table
lhs rhs #:construct (make-LeqProp lhs rhs))])]
[(#f _) -tt]
[(_ #f) -tt]))])
(define Leq-intern-table (make-weak-hash))
(define -leq make-LeqProp)
(define (-lt lhs rhs) (make-LeqProp (-lexp-add1 lhs) rhs))
(define (-gt lhs rhs) (-lt rhs lhs))
(define (-geq lhs rhs) (-leq rhs lhs))
(define (-eq l1 l2) (-and (-leq l1 l2) (-leq l2 l1)))
(def-prop OrProp ([ps (listof (or/c TypeProp? NotTypeProp? LeqProp?))])
[#:frees (f) (combine-frees (map f ps))]
[#:fmap (f) (apply -or (map f ps))]
[#:for-each (f) (for-each f ps)]
[#:custom-constructor
[#:custom-constructor/contract
(-> (listof (or/c TypeProp? NotTypeProp? LeqProp?)) OrProp?)
(let ([ps (sort ps (λ (p q) (unsafe-fx<= (eq-hash-code p)
(eq-hash-code q))))])
(intern-single-ref!
@ -89,7 +152,7 @@
(define orprop-intern-table (make-weak-hash))
(def-prop AndProp ([ps (listof (or/c OrProp? TypeProp? NotTypeProp?))])
(def-prop AndProp ([ps (listof (or/c OrProp? TypeProp? NotTypeProp? LeqProp?))])
[#:frees (f) (combine-frees (map f ps))]
[#:fmap (f) (apply -and (map f ps))]
[#:for-each (f) (for-each f ps)])

View File

@ -8,7 +8,7 @@
racket/list
racket/syntax))
(provide define-switch)
(provide define-rep-switch)
;; a macro for defining a switch function of the form:
@ -17,21 +17,22 @@
;; This allows us to dispatch on the first arguments Rep-uid,
;; which can be more efficient than long match statements with a case
;; for large numbers of Reps (e.g. subtype)
(define-syntax (define-switch stx)
(define-syntax-class (switch-clause arg other-args)
(define-syntax (define-rep-switch stx)
(define-syntax-class (switch-clause pre-args arg post-args)
(pattern (((~datum case:) rep-name:id pattern:expr) . body)
#:with name #'rep-name
#:with idx (format-id #'rep-name "uid:~a" (syntax->datum #'rep-name))
#:with function
(with-syntax ([arg arg]
[other-args other-args])
(with-syntax ([(pre-args ...) pre-args]
[arg arg]
[(post-args ...) post-args])
(syntax/loc #'body
(λ (arg . other-args)
(λ (pre-args ... arg post-args ...)
(match arg
[pattern . body]))))))
(syntax-parse stx
[(_ (name:id arg:id args:id ...)
(~var clause (switch-clause #'arg #'(args ...))) ...
[(_ (name:id pre-args:id ... (#:switch arg:id) post-args:id ...)
(~var clause (switch-clause #'(pre-args ...) #'arg #'(post-args ...))) ...
[(~datum else:) . default])
(define name-symbols (map syntax->datum (syntax->list #'(clause.name ...))))
(unless (not (null? name-symbols))
@ -61,8 +62,9 @@
cur-stx)))
(syntax/loc stx
(define name
(let* ([default-fun (λ (arg args ...) . default)]
(let* ([default-fun (λ (pre-args ... arg post-args ...) . default)]
[switch-table (make-vector (get-uid-count) default-fun)])
(vector-set! switch-table clause.idx clause.function)
...
(λ (arg args ...) ((unsafe-vector-ref switch-table (Rep-uid arg)) arg args ...)))))]))
(λ (pre-args ... arg post-args ...)
((unsafe-vector-ref switch-table (Rep-uid arg)) pre-args ... arg post-args ...)))))]))

View File

@ -17,7 +17,6 @@
racket/list
(except-in syntax/parse id identifier keyword)
racket/base
syntax/struct
syntax/id-table
(contract-req)
racket/syntax))
@ -36,9 +35,11 @@
(and (list? l)
(>= (length l) len)))
(define-for-cond-contract name-ref/c
(or/c identifier?
(cons/c exact-integer? exact-integer?)))
(define (name-ref/c x)
(or (identifier? x)
(and (pair? x)
(exact-integer? (car x))
(exact-integer? (cdr x)))))
(define (name-ref=? x y)
(cond
@ -46,9 +47,41 @@
(and (identifier? y) (free-identifier=? x y))]
[else (equal? x y)]))
(define id-table (make-free-id-table))
;; normal-id-table
;;
;; id table to map all free-identifier=? ids from
;; the users program to the same id for typechecking
;; purposes (this gives us equal?, which is really nice.
;; the alternative is implementing gen:equal-hash for all
;; the structs that carry identifiers, but this was noticably
;; slower when I tried it out in late 2016 -amk)
;; Note: we use a free-id-table, which could _potentially_
;; leak memory if we're encountering lots of identifiers
;; that shouldn't stay in memory for the entirety of typechecking,
;; HOWEVER, we don't put our gensymed identifiers into this table
;; (they are 'normal' from the get-go -- see utils/utils.rkt),
;; so this shouldnt be an issue, we should just be putting
;; identifiers from the program itself in here, and those
;; will be in memory for typechecking anyway.
(define normal-id-table (make-free-id-table))
;; gets the "canonical" representative for this id.
;; if one does not exist yet, the id is marked
(define (normalize-id id)
(free-id-table-ref! id-table id id))
(cond
;; if it's alread normal, just return it
[(normalized-id? id) id]
;; otherwise check if id-table has the normal
;; version already and if so, return that
[(free-id-table-ref normal-id-table id #f)]
[else
;; otherwise mark this id as normal, put it
;; in the table, and return it (this is now
;; the canonical id for all other ids
;; free-identifier=? to this one
(let ([id (mark-id-as-normalized id)])
(free-id-table-set! normal-id-table id id)
id)]))
(define (hash-id id)
(eq-hash-code (identifier-binding-symbol id)))
@ -214,16 +247,27 @@
. body)
#:with free-vars (fixed-rep-transform #'self #'f #'free-vars* struct-fields #'body)
#:with free-idxs (fixed-rep-transform #'self #'f #'free-idxs* struct-fields #'body)))
(define-syntax-class (constructor-spec constructor-name raw-constructor-name struct-fields)
(define-syntax-class (constructor-spec constructor-name
constructor-contract
internal-constructor-name
raw-constructor-name
raw-constructor-contract
struct-fields)
#:attributes (def)
(pattern body
#:with def
(with-syntax ([constructor-name constructor-name]
[constructor-contract constructor-contract]
[internal-constructor-name internal-constructor-name]
[raw-constructor-name raw-constructor-name]
[raw-constructor-contract raw-constructor-contract]
[(struct-fields ...) struct-fields])
#'(define (constructor-name struct-fields ...)
(let ([constructor-name raw-constructor-name])
. body)))))
#'(define/cond-contract (constructor-name struct-fields ...)
constructor-contract
(define/cond-contract constructor-name
raw-constructor-contract
raw-constructor-name)
. body))))
;; definer parser for functions who operate on Reps. Fields are automatically bound
;; to the struct-field id names in the body. An optional self argument can be specified.
(define-syntax-class (generic-transformer struct-fields)
@ -236,8 +280,7 @@
(define-syntax-class var-name
#:attributes (name constructor raw-constructor match-expander predicate)
(pattern name:id
#:with constructor
(format-id #'name "make-~a" (syntax-e #'name))
#:with constructor (format-id #'name "make-~a" (syntax-e #'name))
;; hidden constructor for use inside custom constructor defs
#:with raw-constructor (format-id #'name "raw-make-~a" (syntax-e #'name))
#:with match-expander
@ -288,10 +331,23 @@
;; #:no-provide option (i.e. don't provide anything automatically)
(~optional (~and #:no-provide no-provide?-kw))
(~optional [#:singleton singleton:id])
(~optional [#:custom-constructor . (~var constr-def
(constructor-spec #'var.constructor
#'var.raw-constructor
#'(flds.ids ...)))])
(~optional (~or [#:custom-constructor
. (~var constr-def
(constructor-spec #'var.constructor
#'(-> flds.contracts ... any)
#'var.internal-constructor
#'var.raw-constructor
#'(-> flds.contracts ... any)
#'(flds.ids ...)))]
[#:custom-constructor/contract
custom-constructor-contract
. (~var constr-def
(constructor-spec #'var.constructor
#'custom-constructor-contract
#'var.internal-constructor
#'var.raw-constructor
#'(-> flds.contracts ... any)
#'(flds.ids ...)))]))
(~optional (~and #:non-transparent non-transparent-kw))
;; #:extras to specify other struct properties in a per-definition manner
(~optional [#:extras . extras]))
@ -336,7 +392,9 @@
([uid-id (format-id #'var.name "uid:~a" (syntax->datum #'var.name))]
[(parent ...) (if (attribute parent) #'(parent) #'())]
;; contract for constructor
[constructor-contract #'(-> flds.contracts ... any)]
[constructor-contract (if (attribute custom-constructor-contract)
#'custom-constructor-contract
#'(-> flds.contracts ... any))]
[constructor-name (if (attribute constr-def)
#'var.raw-constructor
#'var.constructor)]

View File

@ -21,8 +21,8 @@
;;************************************************************
(require (for-syntax racket/base syntax/parse)
racket/unsafe/ops
racket/fixnum)
;racket/fixnum
racket/unsafe/ops)
(provide type-mask?
mask-union

View File

@ -9,6 +9,8 @@
(require (utils tc-utils)
"rep-utils.rkt"
"core-rep.rkt"
"object-rep.rkt"
"prop-rep.rkt"
"values-rep.rkt"
"type-mask.rkt"
"free-variance.rkt"
@ -19,7 +21,6 @@
racket/match racket/list
syntax/id-table
racket/contract
racket/set
racket/lazy-require
(for-syntax racket/base
racket/syntax
@ -53,6 +54,15 @@
Union-all-flat:
Union/set:
Intersection?
subst-names
inc-lvl
abstract-names
-refine
Refine:
Refine-obj:
Refine-name:
save-term-var-names!
extract-props
(rename-out [instantiate instantiate-raw-type]
[Union:* Union:]
[Intersection:* Intersection:]
@ -72,7 +82,9 @@
[Mu-body Mu-body-unsafe]
[Poly-body* Poly-body]
[PolyDots-body* PolyDots-body]
[PolyRow-body* PolyRow-body]))
[PolyRow-body* PolyRow-body]
[Intersection-prop* Intersection-prop]
[Intersection:* Intersection:]))
(define (resolvable? x)
(or (Mu? x)
@ -81,9 +93,15 @@
(lazy-require
("../types/overlap.rkt" (overlap?))
("../types/resolve.rkt" (resolve-app)))
("../types/prop-ops.rkt" (-and))
("../types/resolve.rkt" (resolve-app))
("../infer/infer.rkt" (intersect)))
(define var-name-table (make-hash))
;; tables that save variables from parsed types
;; so that later printing/checking can use the
;; the same variables
(define type-var-name-table (make-hash))
(define term-var-name-table (make-hash))
;; Name = Symbol
@ -448,8 +466,7 @@
(def-type Opaque ([pred identifier?])
#:base
[#:custom-constructor
(make-Opaque (normalize-id pred))])
[#:custom-constructor (make-Opaque (normalize-id pred))])
@ -526,8 +543,7 @@
[#:frees (f) (if mutable? (make-invariant (f t)) (f t))]
[#:fmap (f) (make-fld (f t) acc mutable?)]
[#:for-each (f) (f t)]
[#:custom-constructor
(make-fld t (normalize-id acc) mutable?)])
[#:custom-constructor (make-fld t (normalize-id acc) mutable?)])
;; poly? : is this type polymorphically variant
;; If not, then the predicate is enough for higher order checks
@ -554,12 +570,9 @@
;; This should eventually be based on understanding of struct properties.
[#:mask (mask-union mask:struct mask:procedure)]
[#:custom-constructor
(make-Struct (normalize-id name)
parent
flds
proc
poly?
(normalize-id pred-id))])
(let ([name (normalize-id name)]
[pred-id (normalize-id pred-id)])
(make-Struct name parent flds proc poly? pred-id))])
;; Represents prefab structs
;; key : prefab key encoding mutability, auto-fields, etc.
@ -632,24 +645,28 @@
;; is used to remove overlapping types from unions.
(def-type Union ([mask type-mask?]
[base (or/c Bottom? Base? BaseUnion?)]
[ts (cons/c Type? (cons/c Type? (listof Type?)))]
[elems (and/c (set/c Type?)
(λ (h) (> (set-count h) 1)))])
[ts (cons/c Type? (listof Type?))]
[elems (hash/c Type? #t #:immutable #t #:flat? #t)])
#:no-provide
#:non-transparent
[#:frees (f) (combine-frees (map f ts))]
[#:fmap (f) (Union-fmap f base ts)]
[#:for-each (f) (for-each f ts)]
[#:mask (λ (t) (Union-mask t))]
[#:custom-constructor
[#:custom-constructor/contract
(-> type-mask?
(or/c Bottom? Base? BaseUnion?)
(listof Type?)
(hash/c Type? #t #:immutable #t #:flat? #t)
Type?)
;; make sure we do not build Unions equivalent to
;; Bottom, a single BaseUnion, or a single type
(cond
[(set-member? elems Univ) Univ]
[(hash-has-key? elems Univ) Univ]
[else
(match (set-count elems)
(match (hash-count elems)
[0 base]
[1 #:when (Bottom? base) (set-first elems)]
[1 #:when (Bottom? base) (hash-iterate-key elems (hash-iterate-first elems))]
[_ (intern-double-ref!
union-intern-table
elems
@ -713,7 +730,7 @@
(define bbits #b0)
(define nbits #b0)
(define ts '())
(define elems (mutable-set))
(define elems (hash))
;; add a Base element to the union
(define (add-base! numeric? bits)
(cond
@ -740,10 +757,10 @@
(add-any-base! b*)
(set! ts (append ts* ts))
(for ([t* (in-list ts*)])
(set-add! elems t*))]
(set! elems (hash-set elems t* #t)))]
[t (set! m (mask-union m (mask t)))
(set! ts (cons t ts))
(set-add! elems t)]))
(set! elems (hash-set elems t #t))]))
;; process the input arguments
(process! base-arg)
(for-each process! args)
@ -759,29 +776,35 @@
(define (Un . args)
(Union-fmap (λ (x) x) -Bottom args))
;; Intersection
;; ts - the list of types (gives deterministic behavior)
;; elems - the set equivalent of 'ts', useful for equality tests
(def-type Intersection ([ts (cons/c Type? (cons/c Type? (listof Type?)))]
[elems (set/c Type?)])
(def-type Intersection ([ts (cons/c Type? (listof Type?))]
[prop (and/c Prop? (not/c FalseProp?))]
[elems (hash/c Type? #t #:immutable #t #:flat? #t)])
#:non-transparent
#:no-provide
[#:frees (f) (combine-frees (map f ts))]
[#:fmap (f) (apply -unsafe-intersect (map f ts))]
[#:for-each (f) (for-each f ts)]
[#:frees (f) (combine-frees (cons (f prop) (map f ts)))]
[#:fmap (f) (-refine
(for*/fold ([res Univ])
([t (in-list ts)]
[t (in-value (f t))])
(intersect res t))
(f prop))]
[#:for-each (f) (for-each f ts) (f prop)]
[#:mask (λ (t) (for/fold ([m mask:unknown])
([elem (in-list (Intersection-ts t))])
(mask-intersect m (mask elem))))]
[#:custom-constructor
(intern-single-ref! intersection-table
elems
#:construct (make-Intersection ts elems))])
(intern-double-ref!
intersection-table
elems
prop
#:construct (make-Intersection ts prop elems))])
(define intersection-table (make-weak-hash))
(define-match-expander Intersection:*
(syntax-rules () [(_ ts) (Intersection: ts _)]))
(define (make-Intersection* ts)
(apply -unsafe-intersect ts))
@ -789,27 +812,116 @@
;; in general, intersections should be built
;; using the 'intersect' operator, which worries
;; about actual subtyping, etc...
(define (-unsafe-intersect . ts)
(let loop ([elems (set)]
[ts ts])
(match ts
[(list)
(let ([ts (set->list elems)])
(cond
[(null? ts) Univ]
;; size = 1 ?
[(null? (cdr ts)) (car ts)]
;; size > 1, build an intersection
[else (make-Intersection ts elems)]))]
[(cons t ts)
(match t
[(Univ:) (loop elems ts)]
[(Intersection: ts* _) (loop elems (append ts* ts))]
[_ #:when (for/or ([elem (in-immutable-set elems)]) (not (overlap? elem t)))
-Bottom]
[_ (loop (set-add elems t) ts)])])))
(define -unsafe-intersect
(case-lambda
[() Univ]
[(t) t]
[args
(let loop ([ts '()]
[elems (hash)]
[prop -tt]
[args args])
(match args
[(list)
(match ts
[(list) (-refine Univ prop)]
[(list t) (-refine (car ts) prop)]
[_ (let ([t (make-Intersection ts -tt elems)])
(-refine t prop))])]
[(cons arg args)
(match arg
[(Univ:) (loop ts elems prop args)]
[(Intersection: ts* (TrueProp:) _) (loop ts elems prop (append ts* args))]
[(Intersection: ts* prop* _)
(loop ts
elems
(-and prop* prop)
(append ts* args))]
[_ #:when (for/or ([elem (in-list args)])
(not (overlap? elem arg)))
-Bottom]
[t (let ([count (hash-count elems)]
[elems (hash-set elems t #t)])
(if (eqv? count (hash-count elems))
(loop ts elems prop args)
(loop (cons t ts) elems prop args)))])]))]))
(define/provide (Intersection-w/o-prop t)
(match t
[(Intersection: _ (TrueProp:) _) t]
[(Intersection: (list t) prop _) t]
[(Intersection: ts prop tset) (make-Intersection ts -tt tset)]))
;; -refine
;;
;; Constructor for refinements
;;
;; (-refine t p) constructs a refinement type
;; and assumes 'p' is already in the locally nameless form
;;
;; (-refine x t p) constructs a refinement type
;; after abstracting the identifier 'x' from 'p'
(define/provide -refine
(case-lambda
[(t prop)
(match* (t prop)
[(_ (TrueProp:)) t]
[(_ (FalseProp:)) -Bottom]
[(_ (TypeProp: (Path: '() (cons 0 0)) t*)) (intersect t t*)]
[((Intersection: ts (TrueProp:) tset) _) (make-Intersection ts prop tset)]
[((Intersection: ts prop* tset) _)
(-refine (make-Intersection ts -tt tset) (-and prop prop*))]
[(_ _) (make-Intersection (list t) prop (hash t #t))])]
[(nm t prop) (-refine t (abstract-names prop (list nm)))]))
(define-match-expander Intersection:*
(λ (stx) (syntax-case stx ()
[(_ ts prop) (syntax/loc stx (Intersection ts prop _))]
[(_ x ts prop) (syntax/loc stx (and (Intersection ts _ _)
(app (λ (i)
(define x (genid))
(cons x (Intersection-prop* (-id-path x) i)))
(cons x prop))))])))
(define-match-expander Refine:
(λ (stx) (syntax-case stx ()
[(_ t prop)
(syntax/loc stx
(and (Intersection: _ (and (not (TrueProp:)) prop) _)
(app Intersection-w/o-prop t)))]
[(_ x t prop)
(syntax/loc stx
(and (Intersection _ (not (TrueProp:)) _)
(app Intersection-w/o-prop t)
(app (λ (i)
(define x (genid))
(cons x (Intersection-prop* (-id-path x) i)))
(cons x prop))))])))
(define-match-expander Refine-name:
(lambda (stx)
(syntax-case stx ()
[(_ x t prop)
(syntax/loc stx
(and (Intersection _ (not (TrueProp:)) _)
(app Intersection-w/o-prop t)
(app (λ (i)
(match-define (list x) (hash-ref term-var-name-table i (list (gen-pretty-id))))
(cons x (Intersection-prop* (-id-path x) i)))
(cons x prop))))])))
(define (save-term-var-names! t xs)
(hash-set! term-var-name-table t (map (λ (id) (gen-pretty-id (syntax->datum id))) xs)))
(define-match-expander Refine-obj:
(λ (stx) (syntax-case stx ()
[(_ obj t prop)
(syntax/loc stx
(and (Intersection _ (not (TrueProp:)) _)
(app Intersection-w/o-prop t)
(app (λ (i) (Intersection-prop* obj i)) prop)))])))
;; refinement based on some predicate function 'pred'
(def-type Refinement ([parent Type?] [pred identifier?])
[#:frees (f) (f parent)]
[#:fmap (f) (make-Refinement (f parent) pred)]
@ -1055,7 +1167,7 @@
;; the 'smart' constructor
(define (Mu* name body)
(let ([v (make-Mu (abstract name body))])
(hash-set! var-name-table v name)
(hash-set! type-var-name-table v name)
v))
;; the 'smart' destructor
@ -1079,7 +1191,7 @@
(define (Poly* names body #:original-names [orig names])
(if (null? names) body
(let ([v (make-Poly (length names) (abstract-many names body))])
(hash-set! var-name-table v orig)
(hash-set! type-var-name-table v orig)
v)))
;; the 'smart' destructor
@ -1094,7 +1206,7 @@
(define (PolyDots* names body)
(if (null? names) body
(let ([v (make-PolyDots (length names) (abstract-many names body))])
(hash-set! var-name-table v names)
(hash-set! type-var-name-table v names)
v)))
;; the 'smart' destructor
@ -1113,7 +1225,7 @@
;;
(define (PolyRow* names constraints body #:original-names [orig names])
(let ([v (make-PolyRow constraints (abstract-many names body))])
(hash-set! var-name-table v orig)
(hash-set! type-var-name-table v orig)
v))
(define (PolyRow-body* names t)
@ -1152,7 +1264,7 @@
(syntax-case stx ()
[(_ np bp)
#'(? Mu?
(app (lambda (t) (let ([sym (hash-ref var-name-table t (lambda _ (gensym)))])
(app (lambda (t) (let ([sym (hash-ref type-var-name-table t (lambda _ (gensym)))])
(list sym (Mu-body* sym t))))
(list np bp)))])))
@ -1182,7 +1294,7 @@
#'(? Poly?
(app (lambda (t)
(let* ([n (Poly-n t)]
[syms (hash-ref var-name-table t (lambda _ (build-list n (lambda _ (gensym)))))])
[syms (hash-ref type-var-name-table t (lambda _ (build-list n (lambda _ (gensym)))))])
(list syms (Poly-body* syms t))))
(list nps bp)))])))
@ -1201,7 +1313,7 @@
#'(? Poly?
(app (lambda (t)
(let* ([n (Poly-n t)]
[syms (hash-ref var-name-table t (lambda _ (build-list n (lambda _ (gensym)))))]
[syms (hash-ref type-var-name-table t (lambda _ (build-list n (lambda _ (gensym)))))]
[fresh-syms (map fresh-name syms)])
(list syms fresh-syms (Poly-body* fresh-syms t))))
(list nps freshp bp)))])))
@ -1227,7 +1339,7 @@
#'(? PolyDots?
(app (lambda (t)
(let* ([n (PolyDots-n t)]
[syms (hash-ref var-name-table t (lambda _ (build-list n (lambda _ (gensym)))))])
[syms (hash-ref type-var-name-table t (lambda _ (build-list n (lambda _ (gensym)))))])
(list syms (PolyDots-body* syms t))))
(list nps bp)))])))
@ -1249,7 +1361,7 @@
[(_ nps constrp bp)
#'(? PolyRow?
(app (lambda (t)
(define syms (hash-ref var-name-table t (λ _ (list (gensym)))))
(define syms (hash-ref type-var-name-table t (λ _ (list (gensym)))))
(list syms
(PolyRow-constraints t)
(PolyRow-body* syms t)))
@ -1261,7 +1373,7 @@
[(_ nps freshp constrp bp)
#'(? PolyRow?
(app (lambda (t)
(define syms (hash-ref var-name-table t (λ _ (list (gensym)))))
(define syms (hash-ref type-var-name-table t (λ _ (list (gensym)))))
(define fresh-syms (list (gensym (car syms))))
(list syms fresh-syms
(PolyRow-constraints t)
@ -1363,3 +1475,95 @@
(match t
[(Mu-unsafe: body) (instantiate t body)]
[t (error 'unfold "not a mu! ~a" t)]))
;; inc-lvl
;; (cons nat nat) -> (cons nat nat)
;; DeBruijn indexes are represented as a pair of naturals.
;; This function increments the 'lvl' field of such an index.
(define (inc-lvl x)
(match x
[(cons lvl arg) (cons (add1 lvl) arg)]
[_ x]))
;; inc-lvls
;; This function increments the 'lvl' field in all of the targets
;; and objects of substitution (see 'inc-lvl' above)
;; (side note: there is a similar but _different_ version
;; of this function in tc-subst.rkt)
(define (inc-lvls targets)
(for/list ([tgt (in-list targets)])
(match tgt
[(cons nm1 (Path: flds nm2))
(cons (inc-lvl nm1) (make-Path flds (inc-lvl nm2)))]
[(cons nm1 rst)
(cons (inc-lvl nm1) rst)])))
;; name substitution -- like subst-rep in
;; tc-subst but much simpler
(define/cond-contract (subst-names rep targets)
(-> Rep? (listof (cons/c name-ref/c OptObject?)) Rep?)
(define (rec/inc-lvl rep)
(subst-names rep (inc-lvls targets)))
(let rec ([rep rep])
(match rep
;; Functions
;; increment the level of the substituted object
[(arr: dom rng rest drest kws)
(make-arr (map rec dom)
(rec/inc-lvl rng)
(and rest (rec rest))
(and drest (cons (rec (car drest)) (cdr drest)))
(map rec kws))]
;; Refinement types e.g. {x ∈ τ | ψ(x)}
;; increment the level of the substituted object
[(Intersection: ts p _) (-refine
(for/fold ([res Univ])
([t (in-list ts)])
(intersect res t))
(rec/inc-lvl p))]
[(Path: flds nm)
(let ([flds (map rec flds)])
(cond
[(assoc nm targets name-ref=?)
=> (match-lambda
[(cons _ (Path: flds* nm*)) (make-Path (append flds flds*) nm*)]
[(cons _ (Empty:)) -empty-obj]
[(cons _ (? LExp? l)) #:when (null? flds) l]
[_ -empty-obj])]
[else (make-Path flds nm)]))]
[_ (Rep-fmap rep rec)])))
(define (abstract-names rep ids)
(define sub (for/list ([id (in-list ids)]
[idx (in-range (length ids))])
(cons id (-id-path (cons 0 idx)))))
(subst-names rep sub))
(define (Intersection-prop* obj t)
(define p (Intersection-prop t))
(and p (subst-names p (list (cons (cons 0 0) obj)))))
;; given the fact that 'obj' is of type 'type',
;; look inside of type trying to learn
;; more info about obj
(define (extract-props obj type)
(cond
[(Empty? obj) '()]
[else
(define props '())
(let extract! ([rep type]
[obj obj])
(match rep
[(Pair: t1 t2) (extract! t1 (-car-of obj))
(extract! t2 (-cdr-of obj))]
[(Refine-obj: obj t prop)
(set! props (cons prop props))
(extract! t obj)]
[(Intersection: ts _ _) (for ([t (in-list ts)])
(extract! t obj))]
[_ (void)]))
props]))

View File

@ -0,0 +1,202 @@
#lang racket/base
;; Static contracts that are terminal and have no sub parts.
;; Unlike contracts defined with define-terminal-contract, equality of these contracts is based solely
;; on identity. Thus they are most useful for contracts which have no meaningful structure.
;; Ex: (flat/sc #'number?)
(require
"../../utils/utils.rkt"
"../structures.rkt"
"../constraints.rkt"
"symbolic-object.rkt"
racket/match
racket/generic
(for-template racket/base racket/contract/base)
(contract-req))
(struct proposition-contract static-contract () #:transparent)
(define/match (flat-lambda-write v port mode)
[((flat-named-lambda/sc _ arg body) port mode)
(define recur
(case mode
[(#t) write]
[(#f) display]
[else (lambda (p port) (print p port mode))]))
(define-values (open close)
(if (equal? mode 0)
(values "(" ")")
(values "#<" ">")))
(display open port)
(fprintf port "λ")
(display " (" port)
(recur arg port)
(display ") " port)
(recur body port)
(display close port)])
;; flat-named-lambda/sc
;;
;; represents a contract of the following form:
;; (λ (arg) body) which is printed as "name".
;;
;; These are used to represent the relatively arbitrary logical
;; predicates that can occur in areas like refinement types.
;; For example, (Refine [x : τ] ψ) can generate τ/c for the
;; τ-type as we always have for simple types, and the refining
;; proposition can we written as a contract ψ/c where 'x' might be
;; free in ψ/c, then we can generate the following compound contract:
;; (and/c τ/c (flat-named-lambda/sc x ψ/c))
;;
;; (where the name is ommitted for simplicity)
;;
;; Note: the contents of 'body' may count on 'arg' being bound
;; in the contract syntax they generate.
(struct flat-named-lambda/sc static-contract (name arg body)
#:transparent
#:methods gen:sc
[(define/match (sc-map v f)
[((flat-named-lambda/sc name arg body) f)
(flat-named-lambda/sc name (f arg 'covariant) (f body 'covariant))])
(define/match (sc-traverse v f)
[((flat-named-lambda/sc _ arg body) f)
(f arg 'covariant)
(f body 'covariant)])
(define/generic sc->c sc->contract)
(define/match (sc->contract v f)
[((flat-named-lambda/sc name arg body) f)
#`(flat-named-contract
#,name
(λ (#,(sc->c arg f)) #,(sc->c body f)))])
(define/match (sc->constraints v f)
[((flat-named-lambda/sc _ arg body) f)
(merge-restricts 'flat (f arg) (f body))])
(define (sc-terminal-kind _) 'flat)]
#:methods gen:custom-write
[(define write-proc flat-lambda-write)])
;; is-flat-type/sc
;;
;; Allows us to generate a contract that will check
;; if 'obj' is of type 'type'
;;
;; For this to be valid, these often need to appear in
;; a flat-named-lambda/sc to ensure all identifiers in
;; the generated contract syntax are bound.
;;
;; type -- needs to be a type w/ a flat contract
;; so we can use it directly as a predicate.
(struct is-flat-type/sc proposition-contract (obj type)
#:transparent
#:methods gen:sc
[(define/match (sc-map v f)
[((is-flat-type/sc obj type) f)
(is-flat-type/sc (f obj 'covariant) (f type 'covariant))])
(define/match (sc-traverse v f)
[((is-flat-type/sc obj type) f)
(f obj 'covariant)
(f type 'covariant)])
(define/generic sc->c sc->contract)
(define/match (sc->contract v f)
[((is-flat-type/sc obj type) f)
#`(#,(f type) #,(sc->c obj f))])
(define/match (sc->constraints v f)
[((is-flat-type/sc obj type) f)
(merge-restricts 'flat (f obj) (f type))])])
;; not-flat-type/sc
;;
;; Allows us to generate a contract that will check
;; if 'obj' is not of type 'type'.
;;
;; See is-flat-type/sc for more details.
(struct not-flat-type/sc proposition-contract (obj type)
#:transparent
#:methods gen:sc
[(define/match (sc-map v f)
[((not-flat-type/sc obj type) f)
(not-flat-type/sc (f obj 'covariant) (f type 'covariant))])
(define/match (sc-traverse v f)
[((not-flat-type/sc obj type) f)
(f obj 'covariant)
(f type 'covariant)])
(define/generic sc->c sc->contract)
(define/match (sc->contract v f)
[((not-flat-type/sc obj type) f) #`(not (#,(f type) #,(sc->c obj f)))])
(define/match (sc->constraints v f)
[((not-flat-type/sc obj type) f)
(merge-restricts 'flat (f obj) (f type))])])
;; used to generate contracts specifying that
;; lhs is <= rhs
;;
;; These can contain references to variables that
;; might be free if they are not contained in a
;; flat-named-lambda/sc.
(struct leq/sc proposition-contract (lhs rhs)
#:transparent
#:methods gen:sc
[(define/match (sc-map v f)
[((leq/sc lhs rhs) f)
(leq/sc (f lhs 'covariant) (f rhs 'covariant))])
(define/match (sc-traverse v f)
[((leq/sc lhs rhs) f)
(f lhs 'covariant)
(f rhs 'covariant)])
(define/generic sc->c sc->contract)
(define/match (sc->contract v f)
[((leq/sc lhs rhs) f) #`(<= #,(sc->c lhs f) #,(sc->c rhs f))])
(define/match (sc->constraints v f)
[((leq/sc lhs rhs) f)
(merge-restricts 'flat (f lhs) (f rhs))])])
(struct and-prop/sc proposition-contract (args)
#:transparent
#:methods gen:sc
[(define/match (sc-map v f)
[((and-prop/sc args) f)
(and-prop/sc (for/list ([arg (in-list args)])
(f arg 'covariant)))])
(define/match (sc-traverse v f)
[((and-prop/sc args) f)
(for ([arg (in-list args)])
(f arg 'covariant))])
(define/generic sc->c sc->contract)
(define/match (sc->contract v f)
[((and-prop/sc args) f)
#`(and #,@(for/list ([arg (in-list args)])
(sc->c arg f)))])
(define/match (sc->constraints v f)
[((and-prop/sc args) f)
(merge-restricts* 'flat (map f args))])])
(struct or-prop/sc proposition-contract (args)
#:transparent
#:methods gen:sc
[(define/match (sc-map v f)
[((or-prop/sc args) f)
(or-prop/sc (for/list ([arg (in-list args)])
(f arg 'covariant)))])
(define/match (sc-traverse v f)
[((or-prop/sc args) f)
(for ([arg (in-list args)])
(f arg 'covariant))])
(define/generic sc->c sc->contract)
(define/match (sc->contract v f)
[((or-prop/sc args) f)
#`(or #,@(for/list ([arg (in-list args)])
(sc->c arg f)))])
(define/match (sc->constraints v f)
[((or-prop/sc args) f)
(merge-restricts* 'flat (map f args))])])
(provide/cond-contract
[struct flat-named-lambda/sc ([name string?] [arg id/sc?] [body proposition-contract?])]
[struct is-flat-type/sc ([obj symbolic-object-contract?] [type static-contract?])]
[struct not-flat-type/sc ([obj symbolic-object-contract?] [type static-contract?])]
[struct leq/sc ([lhs symbolic-object-contract?] [rhs symbolic-object-contract?])]
[struct and-prop/sc ([args (listof proposition-contract?)])]
[struct or-prop/sc ([args (listof proposition-contract?)])])

View File

@ -0,0 +1,95 @@
#lang racket/base
(require
"../../utils/utils.rkt"
"../structures.rkt"
"../constraints.rkt"
racket/match
racket/generic
(for-template racket/base)
(contract-req))
(provide-for-cond-contract symbolic-object-contract?)
(struct symbolic-object-contract static-contract () #:transparent)
;; an identifier symbolic object e.g. x
(struct id/sc symbolic-object-contract (syntax)
#:transparent
#:methods gen:equal+hash
[(define/match (equal-proc a b rec)
[((id/sc id1) (id/sc id2) rec)
(free-identifier=? id1 id2)])
(define/match (hc sc hash-code)
[((id/sc id) rec)
(hash-code (identifier-binding-symbol id))])
(define hash-proc hc)
(define hash2-proc hc)]
#:methods gen:sc
[(define (sc-map v f) v)
(define (sc-traverse v f) (void))
(define (sc->contract v f) (id/sc-syntax v))
(define (sc->constraints v f) (simple-contract-restrict 'flat))])
;; a path element access into a symbolic object e.g. (car o)
(struct acc-obj/sc symbolic-object-contract (acc-stx obj)
#:transparent
#:methods gen:equal+hash
[(define/match (equal-proc a b recur)
[((acc-obj/sc acc1 obj1) (acc-obj/sc acc2 obj2) rec)
(and (free-identifier=? acc1 acc2)
(rec obj1 obj2))])
(define/match (hc sc hash-code)
[((acc-obj/sc acc obj) rec)
(bitwise-ior (rec (identifier-binding-symbol (acc-obj/sc-acc-stx sc)))
(rec (acc-obj/sc-obj sc)))])
(define hash-proc hc)
(define hash2-proc hc)]
#:methods gen:sc
[(define (sc-map v f) (acc-obj/sc (acc-obj/sc-acc-stx v)
(f (acc-obj/sc-obj v) 'covariant)))
(define (sc-traverse v f) (f (acc-obj/sc-obj v) 'covariant))
(define/generic sc->c sc->contract)
(define (sc->contract v f) #`(#,(acc-obj/sc-acc-stx v) #,(sc->c (acc-obj/sc-obj v) f)))
(define (sc->constraints v f) (f (acc-obj/sc-obj v)))])
;; a linear expression symbolic obj, e.g. 42, or x, or (+ 1 (* 2 y)), etc...
(struct linear-exp/sc symbolic-object-contract (const terms)
#:transparent
#:methods gen:sc
[(define/match (sc-map v f)
[((linear-exp/sc c ts) f)
(linear-exp/sc c (for/hash ([(o coeff) (in-hash ts)])
(values (f o 'covariant) coeff)))])
(define/match (sc-traverse v f)
[((linear-exp/sc c ts) f)
(for ([o (in-hash-keys ts)])
(f o 'covariant))])
(define/generic sc->c sc->contract)
(define/match (sc->contract v f)
[((linear-exp/sc c ts) f)
(define terms-list (for/list ([(o coeff) (in-hash ts)])
(if (= 1 coeff)
(sc->c o f)
#`(* #,coeff #,(sc->c o f)))))
(cond
[(null? terms-list) #`#,c]
[else
(match terms-list
[(list) #`#,c]
[(list t) #:when (zero? c) t]
[ts #`(+ #,c #,@ts)])])])
(define/match (sc->constraints v f)
[((linear-exp/sc c ts) f)
(merge-restricts* 'flat (for/list ([k (in-hash-keys ts)])
(f k)))])])
(provide/cond-contract
[struct id/sc ([syntax identifier?])]
[struct acc-obj/sc ([acc-stx identifier?] [obj static-contract?])]
[struct linear-exp/sc ([const exact-integer?] [terms (hash/c static-contract? exact-integer?)])])

View File

@ -13,7 +13,7 @@
;; referenced by the variable.
;;
;; merge-restricts: kind? contract-restrict? ... -> contract-restrict?
;; merge-restricts*: kind? (listof contracct-restrict?) -> contract-restrict?
;; merge-restricts*: kind? (listof contract-restrict?) -> contract-restrict?
;; This means that the generated contract will be the max of kind and all of the other contract
;; restricts.
;;

View File

@ -59,15 +59,11 @@
(define positive-implies?
(or (TrueProp? p2+)
(FalseProp? p1+)
(let ([p1-and-not-p2 (-and p1+ (negate-prop p2+))])
(or (FalseProp? p1-and-not-p2)
(impossible-in-lexical-env? p1-and-not-p2)))))
(implies-in-env? (lexical-env) p1+ p2+)))
(and positive-implies?
(or (TrueProp? p2-)
(FalseProp? p1-)
(let ([p1-and-not-p2 (-and p1- (negate-prop p2-))])
(or (FalseProp? p1-and-not-p2)
(impossible-in-lexical-env? p1-and-not-p2)))))]
(implies-in-env? (lexical-env) p1- p2-)))]
[(_ _) #f]))
(define (object-better? o1 o2)
(match* (o1 o2)

View File

@ -1134,7 +1134,7 @@
;; Determine the field type based on its private setter name
;; (assumption: the type environment maps this name already)
(define (setter->type id)
(define f-type (lookup-type/lexical id))
(define f-type (lookup-id-type/lexical id))
(match f-type
[(Function: (list (arr: (list _ type) _ _ _ _)))
type]

View File

@ -488,7 +488,7 @@
(define types (map cdr (Signature-mapping sig)))
(for ([type (in-list types)]
[id (in-list ids)])
(define lexical-type (lookup-type/lexical id))
(define lexical-type (lookup-id-type/lexical id))
(unless (subtype lexical-type type)
(tc-error/fields "type mismatch in unit-from-context export"
"expected" type
@ -597,7 +597,7 @@
(define types (map cdr (Signature-mapping sig)))
(for ([type (in-list types)]
[id (in-list ids)])
(define lexical-type (lookup-type/lexical id))
(define lexical-type (lookup-id-type/lexical id))
(unless (subtype lexical-type type)
(tc-error/fields "type mismatch in invoke-unit import"
"expected" type
@ -663,7 +663,7 @@
[sig (in-value (car sig-mapping))]
[mapping (in-value (cdr sig-mapping))]
[(id expected-type) (in-dict mapping)])
(define id-lexical-type (lookup-type/lexical id))
(define id-lexical-type (lookup-id-type/lexical id))
(unless (subtype id-lexical-type expected-type)
(tc-error/fields "type mismatch in unit export"
"expected" expected-type

View File

@ -58,12 +58,12 @@
#:with n:id #'c.e
#:with (v) #'(c.v ...)
#:fail-unless (free-identifier=? name #'n) #f
(or (type-annotation #'v) (lookup-type/lexical #'v #:fail (lambda _ #f)))]
(or (type-annotation #'v) (lookup-id-type/lexical #'v #:fail (lambda _ #f)))]
[c:lv-clause
#:with (#%plain-app reverse n:id) #'c.e
#:with (v) #'(c.v ...)
#:fail-unless (free-identifier=? name #'n) #f
(or (type-annotation #'v) (lookup-type/lexical #'v #:fail (lambda _ #f)))]
(or (type-annotation #'v) (lookup-id-type/lexical #'v #:fail (lambda _ #f)))]
[_ #f]))
(syntax-parse stx
#:literal-sets (kernel-literals)

View File

@ -7,19 +7,21 @@
(rep type-rep prop-rep object-rep rep-utils)
(utils tc-utils)
racket/set
(types tc-result resolve subtype update prop-ops)
(types tc-result resolve update prop-ops subtract)
(env type-env-structs lexical-env mvar-env)
(only-in (infer infer) intersect)
(rename-in (types abbrev)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
(typecheck tc-metafunctions))
(typecheck tc-metafunctions tc-subst))
(provide with-lexical-env+props
impossible-in-lexical-env?)
implies-in-env?
env+)
(define (impossible-in-lexical-env? p)
(not (env+ (lexical-env) (list p))))
(define (implies-in-env? env p1 p2)
(not (env+ env (list p1 (negate-prop p2)))))
;; Returns #f if anything becomes (U)
(define (env+ env ps)
@ -31,33 +33,84 @@
[props
(let loop ([ps atoms]
[negs '()]
[new '()]
[Γ (env-replace-props env props)])
(match ps
[(cons p ps)
(match p
[(TypeProp: (Path: lo x) pt)
#:when (and (not (is-var-mutated? x))
(identifier-binding x))
(let* ([t (lookup-type/lexical x Γ #:fail (λ (_) Univ))]
[new-t (update t pt #t lo)])
(and (not (Bottom? new-t))
(loop ps negs (env-set-type Γ x new-t))))]
;; process negative info _after_ positive info so we don't miss anything
[(NotTypeProp: (Path: _ x) _)
#:when (and (not (is-var-mutated? x))
(identifier-binding x))
(loop ps (cons p negs) Γ)]
[_ (loop ps negs Γ)])]
[_ (let ([Γ (let loop ([negs negs]
[Γ Γ])
(match negs
[(cons (NotTypeProp: (Path: lo x) pt) rst)
(let* ([t (lookup-type/lexical x Γ #:fail (λ (_) Univ))]
[new-t (update t pt #f lo)])
(and (not (Bottom? new-t))
(loop rst (env-set-type Γ x new-t))))]
[_ Γ]))])
(and Γ (env-replace-props Γ (append atoms (env-props Γ)))))]))]
[(TypeProp: (Path: pes (? identifier? x)) pt)
(let ([t (lookup-id-type/lexical x Γ #:fail (λ (_) Univ))])
(define new-t (update t pt #t pes))
(cond
[(Bottom? new-t) #f]
[(equal? t new-t) (loop ps negs new Γ)]
[else
;; it's a new type! check if there are any logical propositions that can
;; be extracted from new-t
(define new-props (extract-props (-id-path x) new-t))
(loop ps negs (append new-props new) (env-set-id-type Γ x new-t))]))]
[(TypeProp: obj pt)
(let ([t (lookup-obj-type/lexical obj Γ #:fail (λ (_) Univ))])
(define new-t (intersect t pt #:obj obj))
(cond
[(Bottom? new-t) #f]
[(equal? t new-t) (loop ps negs new Γ)]
[else
;; it's a new type! check if there are any logical propositions that can
;; be extracted from new-t
(define new-props (extract-props obj new-t))
(loop ps negs (append new-props new) (env-set-obj-type Γ obj new-t))]))]
;; process negative info _after_ positive info so we don't miss anything!
;; (overly simple example: if we started with x ∈ Any, updating it's type in Γ
;; with x ∉ String and then x ∈ String just produces a Γ with x ∈ String,
;; but updating with x ∈ String _and then_ x ∉ String derives a contradiction)
[(? NotTypeProp?)
(loop ps (cons p negs) new Γ)]
[_ (loop ps negs new Γ)])]
[_ (let loop ([negs negs]
[new new]
[Γ Γ])
(match negs
[(cons (NotTypeProp: (Path: pes (? identifier? x)) pt) negs)
(let ([t (lookup-id-type/lexical x Γ #:fail (λ (_) Univ))])
(define new-t (update t pt #f pes))
(cond
[(Bottom? new-t) #f]
[(equal? t new-t) (loop negs new Γ)]
[else
;; it's a new type! check if there are any logical propositions that can
;; be extracted from new-t
(define new-props (extract-props (-id-path x) new-t))
(loop negs (append new-props new) (env-set-id-type Γ x new-t))]))]
[(cons (NotTypeProp: obj pt) rst)
(let ([t (lookup-obj-type/lexical obj Γ #:fail (λ (_) Univ))])
(define new-t (subtract t pt))
(cond
[(Bottom? new-t) #f]
[(equal? t new-t) (loop rst new Γ)]
[else
;; it's a new type! check if there are any logical propositions that can
;; be extracted from new-t
(define new-props (extract-props obj new-t))
(loop rst (append new-props new) (env-set-obj-type Γ obj new-t))]))]
[_
(cond
;; there was a contradiction, return #f
[(not Γ) #f]
;; we're done updating types and nothing additional appeared, return the new Γ
[(null? new) (env-replace-props Γ (append atoms (env-props Γ)))]
;; Q: What if 'new' is not null?
;; A: as we're updating types, it's possible a new type had some refinements in it
;; that we have now extracted. For example, say we updated x's type from
;; (U String (Refine [n : Int] (<= n 42)))
;; to
;; (Refine [n : Int] (<= n 42))
;; now we _know_ not only that x has a more specific type, we know the logical
;; proposition (<= x 42).
;; So in cases like this where we have a new type and 'extract-props' found
;; something, we go back and logically add those extracted props to the environment
;; in case it further refines our logical view of the program.
[else (env+ (env-replace-props Γ (append atoms (env-props Γ))) new)])]))]))]
[else #f])]))

View File

@ -6,7 +6,8 @@
"signatures.rkt"
"check-below.rkt" "../types/kw-types.rkt"
(types utils abbrev subtype type-table path-type
prop-ops overlap resolve generalize tc-result)
prop-ops overlap resolve generalize tc-result
numeric-tower)
(private-in syntax-properties parse-type)
(rep type-rep prop-rep object-rep)
(only-in (infer infer) intersect)
@ -15,13 +16,12 @@
racket/list
racket/private/class-internal
syntax/parse
(only-in racket/list split-at)
(typecheck internal-forms tc-envops)
racket/sequence
racket/extflonum
;; Needed for current implementation of typechecking letrec-syntax+values
(for-template (only-in racket/base letrec-values)
(only-in racket/base list)
(for-template (only-in racket/base list letrec-values
+ * < <= = >= >)
;; see tc-app-contracts.rkt
racket/contract/private/provide)
@ -46,13 +46,10 @@
;; see if id* is an alias for an object
;; if not (-id-path id*) is returned
(define obj (lookup-alias/lexical id*))
(define-values (alias-path alias-id)
(define ty
(match obj
[(Path: p x) (values p x)]
[(Empty:) (values (list) id*)]))
;; calculate the type, resolving aliasing and paths if necessary
(define ty (or (path-type alias-path (lookup-type/lexical alias-id))
Univ))
[(Empty:) (lookup-id-type/lexical id*)]
[_ (lookup-obj-type/lexical obj)]))
(ret ty
(if (overlap? ty (-val #f))
@ -110,7 +107,7 @@
[#f #f]))
(define (explicit-fail stx msg var)
(cond [(and (identifier? var) (lookup-type/lexical var #:fail (λ _ #f)))
(cond [(and (identifier? var) (lookup-id-type/lexical var #:fail (λ _ #f)))
=>
(λ (t)
(tc-error/expr #:stx stx
@ -149,11 +146,17 @@
[(quote #f) (ret (-val #f) -false-propset)]
[(quote #t) (ret (-val #t) -true-propset)]
[(quote val)
(match expected
[(tc-result1: t)
(ret (tc-literal #'val t) -true-propset)]
[_
(ret (tc-literal #'val) -true-propset)])]
(ret (match expected
[(tc-result1: t) (tc-literal #'val t)]
[_ (tc-literal #'val)])
-true-propset
;; sometimes we want integer's symbolic objects
;; to be themselves
(let ([v (syntax-e #'val)])
(if (and (exact-integer? v)
(with-linear-integer-arithmetic?))
(-lexp v)
-empty-obj)))]
;; syntax
[(quote-syntax datum . _)
(define expected-type
@ -195,7 +198,12 @@
;(tc-expr/check #'e3 expected)
(tc-error/expr "with-continuation-mark requires a continuation-mark-key, but got ~a" key-t)])]
;; application
[(#%plain-app . _) (tc/app form expected)]
[(#%plain-app . _)
(define result (tc/app form expected))
(cond
[(with-linear-integer-arithmetic?)
(add-applicable-linear-info form result)]
[else result])]
;; #%expression
[(#%expression e) (tc/#%expression form expected)]
;; begin
@ -412,3 +420,86 @@
;; FIXME is there a type for prefab structs?
Univ]
[_ Univ]))
;; adds linear info for the following operations:
;; + * < <= = >= >
;; when the arguments are integers w/ objects
(define (add-applicable-linear-info form result)
;; class to recognize expressions that typecheck at a subtype of -Int
;; and whose object is non-empty
(define-syntax-class int/obj
#:attributes (obj)
(pattern e:expr
#:do [(define o
(match (type-of #'e)
[(tc-result1: t _ (? Object? o))
#:when (subtype t -Int)
o]
[_ #f]))]
#:fail-unless o "not an integer with a non-empty object"
#:attr obj o))
;; class to recognize int comparisons and associate their
;; internal TR prop constructors
(define-syntax-class int-comparison
#:attributes (constructor)
(pattern (~literal <) #:attr constructor -lt)
(pattern (~literal <=) #:attr constructor -leq)
(pattern (~literal >=) #:attr constructor -geq)
(pattern (~literal >) #:attr constructor -gt)
(pattern (~literal =) #:attr constructor -eq))
;; takes a result and adds p to the then proposition
;; and (not p) to the else proposition
(define (add-p/not-p result p)
(match result
[(tc-result1: t (PropSet: p+ p-) o)
(ret t
(-PS (-and p p+) (-and (negate-prop p) p-))
o)]
[_ result]))
;; takes a list of arguments to a comparison function
;; and returns the list of atomic facts that would hold
;; if returned #t
(define (comparison-props comp obj1 obj2 obj-rest)
(define-values (props _)
(for/fold ([atoms (list (comp obj1 obj2))]
[prev-obj obj2])
([obj (in-list obj-rest)])
(values (cons (-lt prev-obj obj) atoms)
obj)))
props)
;; inspect the function appplication to see if it is a linear
;; integer compatible form we want to enrich with info when
;; #:with-linear-integer-arithmetic is specified by the user
(syntax-parse form
[(#%plain-app (~literal *) e1:int/obj e2:int/obj)
(match result
[(tc-result1: t ps _)
(define o1*o2 (-obj* (attribute e1.obj) (attribute e2.obj)))
(cond
[(Object? o1*o2)
(ret (-refine/fresh x t (-eq (-lexp x) o1*o2))
ps
o1*o2)]
[else result])]
[_ result])]
[(#%plain-app (~literal +) e:int/obj es:int/obj ...)
(match result
[(tc-result1: t ps _)
(define l (apply -lexp (attribute e.obj) (attribute es.obj)))
(ret (-refine/fresh x t (-eq (-lexp x) l))
ps
l)])]
[(#%plain-app comp:int-comparison
e1:int/obj
e2:int/obj
es:int/obj ...)
(define p (apply -and (comparison-props (attribute comp.constructor)
(attribute e1.obj)
(attribute e2.obj)
(attribute es.obj))))
(add-p/not-p result p)]
[_ result]))

View File

@ -9,34 +9,50 @@
(only-in (infer infer) intersect)
(utils stxclass-util)
syntax/parse
racket/function
racket/sequence
racket/extflonum)
(import)
(export tc-literal^)
;; racket/function's conjoin is very general and therefore slow
;; and it's trivial to just define the specific version we need:
(define-syntax-rule (conjoin f ...)
(λ (x) (and (f x) ...)))
(define (maybe-add-linear-integer-info int t)
(if (with-linear-integer-arithmetic?)
(-refine/fresh x t (-eq (-lexp x) (-lexp int)))
t))
;; return the type of a literal value
;; tc-literal: racket-value-syntax [type] -> type
(define (tc-literal v-stx [expected #f])
(define-syntax-class exp
(pattern (~and i (~or :number :str :bytes))
#:fail-unless expected #f
#:fail-unless (subtype (-val (syntax-e #'i)) expected) #f))
#:fail-unless (let ([n (syntax-e #'i)])
(subtype (-val n) expected #:obj (if (exact-integer? n) (-lexp n) -empty-obj))) #f))
(syntax-parse v-stx
[i:exp expected]
[i:boolean (-val (syntax-e #'i))]
[i:identifier (-val (syntax-e #'i))]
;; Numbers
[0 -Zero]
[1 -One]
[(~var i (3d (conjoin byte? positive?))) -PosByte]
[(~var i (3d byte?)) -Byte]
[(~var i (3d (conjoin portable-index? positive?))) -PosIndex]
[(~var i (3d (conjoin portable-fixnum? positive?))) -PosFixnum]
[(~var i (3d (conjoin portable-fixnum? negative?))) -NegFixnum]
[(~var i (3d exact-positive-integer?)) -PosInt]
[(~var i (3d (conjoin exact-integer? negative?))) -NegInt]
[0 (maybe-add-linear-integer-info 0 -Zero)]
[1 (maybe-add-linear-integer-info 1 -One)]
[(~var i (3d (conjoin byte? positive?)))
(maybe-add-linear-integer-info (syntax-e #'i) -PosByte)]
[(~var i (3d byte?))
(maybe-add-linear-integer-info (syntax-e #'i) -Byte)]
[(~var i (3d (conjoin portable-index? positive?)))
(maybe-add-linear-integer-info (syntax-e #'i) -PosIndex)]
[(~var i (3d (conjoin portable-fixnum? positive?)))
(maybe-add-linear-integer-info (syntax-e #'i) -PosFixnum)]
[(~var i (3d (conjoin portable-fixnum? negative?)))
(maybe-add-linear-integer-info (syntax-e #'i) -NegFixnum)]
[(~var i (3d exact-positive-integer?))
(maybe-add-linear-integer-info (syntax-e #'i) -PosInt)]
[(~var i (3d (conjoin exact-integer? negative?)))
(maybe-add-linear-integer-info (syntax-e #'i) -NegInt)]
[(~var i (3d (conjoin number? exact? rational? positive?))) -PosRat]
[(~var i (3d (conjoin number? exact? rational? negative?))) -NegRat]
[(~var i (3d (lambda (x) (eqv? x 0.0)))) -FlonumPosZero]

View File

@ -6,6 +6,7 @@
-> ->* one-of/c)
(rep type-rep prop-rep object-rep values-rep rep-utils)
(typecheck tc-subst)
(logic ineq)
(contract-req))
(provide abstract-results
@ -36,24 +37,6 @@
[(tc-results: ts fs os dty dbound)
(make-ValuesDots (map -result ts fs os) dty dbound)]))
(define/cond-contract (resolve atoms prop)
((listof Prop?)
Prop?
. -> .
Prop?)
(for/fold ([prop prop])
([a (in-list atoms)])
(match prop
[(AndProp: ps)
(let loop ([ps ps] [result null])
(match ps
[(cons p ps)
(cond [(contradictory? a p) -ff]
[(implies-atomic? a p) (loop ps result)]
[else (loop ps (cons p result))])]
[_ (apply -and result)]))]
[_ prop])))
(define (flatten-props ps)
(let loop ([ps ps])
(match ps
@ -64,41 +47,83 @@
(define/cond-contract (combine-props new-props old-props)
((listof Prop?) (listof Prop?)
. -> .
(values (or/c #f (listof OrProp?))
(values (or/c #f (listof (or/c OrProp? LeqProp?)))
(or/c #f (listof (or/c TypeProp? NotTypeProp?)))))
(define (atomic-prop? p) (or (TypeProp? p) (NotTypeProp? p)))
(define-values (new-atoms new-formulas) (partition atomic-prop? (flatten-props new-props)))
(let loop ([derived-ors null]
[derived-atoms new-atoms]
[worklist (append old-props new-formulas)])
(match worklist
[(cons (app (λ (p) (resolve derived-atoms p)) p)
worklist)
(match p
[(OrProp: qs)
(let or-loop ([qs qs] [result null])
(match qs
[(cons q qs)
(let check-loop ([atoms derived-atoms])
(match atoms
[(cons a atoms)
(cond
[(contradictory? q a) (or-loop qs result)]
[(implies-atomic? a q) (loop derived-ors derived-atoms worklist)]
[else (check-loop atoms)])]
[_ (or-loop qs (cons q result))]))]
[_ (define new-or (apply -or result))
(if (OrProp? new-or)
(loop (cons new-or derived-ors) derived-atoms worklist)
(loop derived-ors derived-atoms (cons new-or worklist)))]))]
[(or (? TypeProp?)
(? NotTypeProp?))
(loop derived-ors (cons p derived-atoms) worklist)]
[(AndProp: qs) (loop derived-ors derived-atoms (append qs worklist))]
[(TrueProp:) (loop derived-ors derived-atoms worklist)]
[(FalseProp:) (values #f #f)])]
[_ (values derived-ors derived-atoms)])))
(define-values (atoms leqs ors)
(let ([atoms '()]
[leqs '()]
[ds '()])
(let partition! ([args (append old-props new-props)])
(match args
[(list) (void)]
[(cons p rst)
(match p
[(TrueProp:) (partition! rst)]
[(TypeProp: obj (Refine: t p))
(partition! (list (-is-type obj t)
(instantiate-rep/obj p obj t)))
(partition! rst)]
[(? TypeProp? p)
(set! atoms (cons p atoms))
(partition! rst)]
[(NotTypeProp: obj (Refine: t p))
(partition! (list (-or (-not-type obj t)
(negate-prop (instantiate-rep/obj p obj t)))))
(when atoms (partition! rst))]
[(? NotTypeProp? p)
(set! atoms (cons p atoms))
(partition! rst)]
[(? LeqProp? p) (set! leqs (cons p leqs))
(partition! rst)]
[(? OrProp? p) (set! ds (cons p ds))
(partition! rst)]
[(AndProp: ps) (partition! ps)
(when atoms
(partition! rst))]
[(FalseProp:) (set! atoms #f)
(set! leqs #f)
(set! ds #f)])]))
(values atoms leqs ds)))
(cond
[(not atoms) (values #f #f)]
[else
(let loop ([worklist ors]
[atoms atoms]
[leqs leqs]
[ors null])
(match worklist
[(cons cur rst)
(match cur
[(OrProp: qs)
(let or-loop ([qs qs] [result null])
(match qs
[(cons (? LeqProp? ineq) qs)
(match (Leqs-imply-Leq-or-not-Leq? leqs ineq)
[#t (loop rst atoms leqs ors)]
[#f (or-loop qs result)]
[_ (or-loop qs (cons ineq result))])]
[(cons q qs)
(let check-loop ([ps atoms])
(match ps
[(cons p ps)
(cond
[(contradiction? q p) (or-loop qs result)]
[(atomic-implies? p q) (loop rst atoms leqs ors)]
[else (check-loop ps)])]
[_ (or-loop qs (cons q result))]))]
[_ (define new-or (apply -or result))
(if (OrProp? new-or)
(loop rst atoms leqs (cons new-or ors))
(loop (cons new-or rst) atoms leqs ors))]))]
[(or (? TypeProp?)
(? NotTypeProp?))
(loop rst (cons cur atoms) leqs ors)]
[(AndProp: qs) (loop (append qs rst) atoms leqs ors)]
[(TrueProp:) (loop rst atoms leqs ors)]
[(FalseProp:) (values #f #f)]
[(? LeqProp?) (loop rst atoms (cons cur leqs) ors)])]
[_ #:when (not (satisfiable-Leqs? leqs)) (values #f #f)]
[_ (values (append leqs ors) atoms)]))]))
(define (unconditional-prop res)

View File

@ -27,7 +27,13 @@
tc-results/c
tc-results/c)])
(provide subst-rep)
(provide subst-rep
instantiate-rep/obj)
(define (instantiate-rep/obj rep obj [t Univ])
(subst-rep rep (list (list (cons 0 0) obj t))))
;; Substitutes the given objects into the values and turns it into a
;; tc-result. This matches up to the substitutions in the T-App rule
@ -114,15 +120,6 @@
(subst-rep r-o targets)))
;; inc-lvl
;; (cons nat nat) -> (cons nat nat)
;; DeBruijn indexes are represented as a pair of naturals.
;; This function increments the 'lvl' field of such an index.
(define (inc-lvl x)
(match x
[(cons lvl arg) (cons (add1 lvl) arg)]
[_ x]))
;; inc-lvls
;; This function increments the 'lvl' field in all of the targets
;; and objects of substitution (see 'inc-lvl' above)
@ -144,7 +141,7 @@
(define/cond-contract (subst-rep rep targets)
(-> any/c (listof (list/c name-ref/c OptObject? Type?))
any/c)
(define (sub/inc rep)
(define (subst/inc rep)
(subst-rep rep (inc-lvls targets)))
;; substitution loop
(let subst ([rep rep])
@ -153,53 +150,66 @@
;; increment the level of the substituted object
[(arr: dom rng rest drest kws)
(make-arr (map subst dom)
(sub/inc rng)
(subst/inc rng)
(and rest (subst rest))
(and drest (cons (subst (car drest)) (cdr drest)))
(map subst kws))]
[(Intersection: ts raw-prop)
(-refine (make-Intersection (map subst ts))
(subst/inc raw-prop))]
[(Path: flds nm)
(let ([flds (map subst flds)])
(cond
[(assoc nm targets name-ref=?) =>
[(assoc nm targets name-ref=?)
=>
(λ (l) (match (second l)
[(Empty:) -empty-obj]
[(Path: flds* nm*)
(make-Path (append flds flds*) nm*)]))]
(make-Path (append flds flds*) nm*)]
[(? LExp? l) #:when (null? flds) l]
[_ -empty-obj]))]
[else (make-Path flds nm)]))]
;; restrict with the type for results and props
[(TypeProp: (Path: flds nm) ty-at-flds)
[(TypeProp: (and obj (Path: flds nm)) obj-ty)
(let ([flds (map subst flds)])
(cond
[(assoc nm targets name-ref=?) =>
(match-lambda
[(list _ new-obj new-obj-ty)
(define arg-ty-at-flds (or (path-type flds new-obj-ty) Univ))
(define new-ty-at-flds (intersect ty-at-flds arg-ty-at-flds))
(match new-obj
[_ #:when (Bottom? new-ty-at-flds) -ff]
[_ #:when (subtype arg-ty-at-flds ty-at-flds) -tt]
[(list _ inner-obj inner-obj-ty)
(define inner-obj-ty-at-flds (or (path-type flds inner-obj-ty) Univ))
(define new-obj-ty (intersect obj-ty inner-obj-ty-at-flds #:obj obj))
(match inner-obj
[_ #:when (Bottom? new-obj-ty) -ff]
[_ #:when (subtype inner-obj-ty-at-flds obj-ty) -tt]
[(Empty:) -tt]
[(Path: flds* nm*)
(define resulting-obj (make-Path (append flds flds*) nm*))
(-is-type resulting-obj new-ty-at-flds)])])]
[else (-is-type (make-Path flds nm) (subst ty-at-flds))]))]
[(NotTypeProp: (Path: flds nm) not-ty-at-flds)
(-is-type resulting-obj new-obj-ty)]
[(? LExp? l) (if (null? flds)
(-is-type l new-obj-ty)
-ff)])])]
[else (-is-type (make-Path flds nm) (subst obj-ty))]))]
[(NotTypeProp: (and obj (Path: flds nm)) neg-obj-ty)
(let ([flds (map subst flds)])
(cond
[(assoc nm targets name-ref=?) =>
[(assoc nm targets name-ref=?)
=>
(match-lambda
[(list _ new-obj new-obj-ty)
(define arg-ty-at-flds (or (path-type flds new-obj-ty) Univ))
(define new-ty-at-flds (subtract arg-ty-at-flds not-ty-at-flds))
(define new-not-ty-at-flds (restrict not-ty-at-flds arg-ty-at-flds))
(match new-obj
[_ #:when (Bottom? new-ty-at-flds) -ff]
[_ #:when (Bottom? new-not-ty-at-flds) -tt]
[(list _ inner-obj inner-obj-ty)
(define inner-obj-ty-at-flds (or (path-type flds inner-obj-ty) Univ))
(define new-obj-ty (subtract inner-obj-ty-at-flds neg-obj-ty #:obj obj))
(define new-neg-obj-ty (restrict neg-obj-ty inner-obj-ty-at-flds #:obj obj))
(match inner-obj
[_ #:when (Bottom? new-obj-ty) -ff]
[_ #:when (Bottom? new-neg-obj-ty) -tt]
[(Empty:) -tt]
[(Path: flds* nm*)
(define resulting-obj (make-Path (append flds flds*) nm*))
(-not-type resulting-obj new-not-ty-at-flds)])])]
(-not-type resulting-obj new-neg-obj-ty)]
[(? LExp? l) (if (null? flds)
(-not-type l new-neg-obj-ty)
-ff)])])]
[else
(-not-type (make-Path flds nm) (subst not-ty-at-flds))]))]
(-not-type (make-Path flds nm) (subst neg-obj-ty))]))]
;; else default fold over subfields
[_ (Rep-fmap rep subst)])))

View File

@ -32,6 +32,15 @@
(define unann-defs (make-free-id-table))
;; adds any latent propositions inside of types to
;; the initial lexical environment that is used
;; for typechecking the rest of the program
(define (add-extracted-props-to-lexical-env obj t)
(when (Object? obj)
(define props (extract-props obj t))
(unless (null? props)
(add-props-to-current-lexical! props))))
(define (parse-typed-struct form)
(parameterize ([current-orig-stx form])
(syntax-parse form
@ -80,7 +89,7 @@
;; declare-refinement
;; FIXME - this sucks and should die
[t:type-refinement
(match (lookup-type/lexical #'t.predicate)
(match (lookup-id-type/lexical #'t.predicate)
[(and t (Function: (list (arr: (list dom) (Values: (list (Result: rng _ _))) #f #f '()))))
(let ([new-t (make-pred-ty (list dom)
rng
@ -93,6 +102,7 @@
[r:typed-require
(let ([t (parse-type #'r.type)])
(register-type #'r.name t)
(add-extracted-props-to-lexical-env (-id-path #'r.name) t)
(list (make-def-binding #'r.name t)))]
[r:typed-require/struct
@ -119,6 +129,7 @@
;; top-level type annotation
[t:type-declaration
(register-type/undefined #'t.id (parse-type #'t.type))
(add-extracted-props-to-lexical-env (-id-path #'r.name) (parse-type #'t.type))
(register-scoped-tvars #'t.id (parse-literal-alls #'t.type))
(list)]
@ -144,7 +155,10 @@
;; if all the variables have types, we stick them into the environment
[(v:type-label^ ...)
(let ([ts (map (λ (x) (get-type x #:infer #f)) vars)])
(for-each register-type-if-undefined vars ts)
(for ([var (in-list vars)]
[t (in-list ts)])
(register-type-if-undefined var t)
(add-extracted-props-to-lexical-env (-id-path var) t))
(map make-def-binding vars ts))]
;; if this already had an annotation, we just construct the binding reps
[(v:typed-id^ ...)
@ -153,7 +167,10 @@
(when (free-id-table-ref unann-defs var #f)
(free-id-table-remove! unann-defs var))
(finish-register-type var top-level?))
(stx-map make-def-binding #'(v ...) (attribute v.type))]
(for/list ([var (in-syntax #'(v ...))]
[t (in-list (attribute v.type))])
(add-extracted-props-to-lexical-env (-id-path var) t)
(make-def-binding var t))]
;; defer to pass1.5
[_ (list)])]
@ -206,6 +223,7 @@
[(list (tc-result: ts) ...)
(for/list ([i (in-list vars)] [t (in-list ts)])
(register-type i t)
(add-extracted-props-to-lexical-env (-id-path i) t)
(free-id-table-set! unann-defs i #t)
(make-def-binding i t))])])]
@ -243,7 +261,7 @@
[import-ids (in-list (syntax->list #'(dviu.import.members ...)))])
(for ([member (in-list (syntax->list import-ids))]
[expected-type (in-list (map cdr (signature->bindings import-sig)))])
(define lexical-type (lookup-type/lexical member))
(define lexical-type (lookup-id-type/lexical member))
(check-below lexical-type expected-type)))
(register-ignored! #'dviu)
'no-type]

View File

@ -7,10 +7,6 @@
(require "../utils/utils.rkt"
racket/list
racket/match
racket/function
racket/undefined
racket/function
(prefix-in c: (contract-req))
(rep rep-utils type-rep prop-rep object-rep values-rep)
(types numeric-tower prefab)
@ -23,30 +19,7 @@
;; from references generated by init-envs
(env signature-env)
(for-syntax racket/base syntax/parse)
;; for base type contracts and predicates
;; use '#%place to avoid the other dependencies of `racket/place`
(for-template
racket/base
racket/contract/base
racket/undefined
(only-in racket/pretty pretty-print-style-table?)
(only-in racket/udp udp?)
(only-in racket/tcp tcp-listener?)
(only-in racket/flonum flvector?)
(only-in racket/extflonum extflvector?)
(only-in racket/fixnum fxvector?)
(only-in racket/future fsemaphore?)
(only-in '#%place place? place-channel?))
(only-in racket/pretty pretty-print-style-table?)
(only-in racket/udp udp?)
(only-in racket/tcp tcp-listener?)
(only-in racket/flonum flvector?)
(only-in racket/extflonum extflvector?)
(only-in racket/fixnum fxvector?)
(only-in racket/future fsemaphore?)
(only-in '#%place place? place-channel?))
(for-syntax racket/base syntax/parse))
(provide (all-defined-out)
(except-out (all-from-out "base-abbrev.rkt" "match-expanders.rkt") make-arr))
@ -264,3 +237,10 @@
(define-syntax-rule (-object . ?clauses)
(make-Instance (-class . ?clauses)))
(define-syntax (-refine/fresh stx)
(syntax-parse stx
[(_ x:id t p)
(syntax/loc stx
(let ([x (genid (syntax->datum #'x))])
(-refine t (abstract-names p (list x)))))]))

View File

@ -7,9 +7,11 @@
(require "../utils/utils.rkt"
"../rep/type-rep.rkt"
"../rep/prop-rep.rkt"
"../rep/object-rep.rkt"
"../rep/base-types.rkt"
"../rep/numeric-base-types.rkt"
(rep prop-rep object-rep values-rep rep-utils)
(rep values-rep rep-utils)
(env mvar-env)
racket/match racket/list (prefix-in c: (contract-req))
(for-syntax racket/base syntax/parse racket/list)
@ -17,11 +19,10 @@
(for-template racket/base))
(provide (all-defined-out)
-is-type
-not-type
-id-path
(all-from-out "../rep/type-rep.rkt"
"../rep/object-rep.rkt"
"../rep/base-types.rkt"
"../rep/prop-rep.rkt"
"../rep/numeric-base-types.rkt")
(rename-out [make-Listof -lst]
[make-MListof -mlst]))

View File

@ -45,4 +45,5 @@
[(ListDots: t bound) (-lst (substitute Univ bound t))]
[(? (lambda (t) (subtype t -Symbol))) -Symbol]
[(== -True) -Boolean]
[(Refine: t _) (loop t)]
[_ t*]))))

View File

@ -33,7 +33,9 @@
[(_ pat)
(syntax/loc stx
(or (Value: pat)
(app Base->val? (box pat))))])))
(app Base->val? (box pat))
(Intersection: (list (or (Value: pat)
(app Base->val? (box pat)))) _)))])))
(define-match-expander Listof:
(lambda (stx)

View File

@ -4,7 +4,6 @@
(rep type-rep rep-utils type-mask)
(prefix-in c: (contract-req))
(types abbrev subtype resolve utils)
racket/set
racket/match)
@ -80,10 +79,11 @@
#t]
[((Union/set: base1 ts1 elems1) t2)
#:no-order
(or (set-member? elems1 t2)
(or (hash-ref elems1 t2 #f)
(overlap? base1 t2)
(for/or ([t1 (in-list ts1)]) (overlap? t1 t2)))]
[((Intersection: ts) s)
;; we ignore the possible refining prop for simplicities sake
[((Intersection: ts _) s)
#:no-order
(for/and ([t (in-list ts)]) (overlap? t s))]
[((or (Poly-unsafe: _ t1)

View File

@ -6,7 +6,7 @@
(rep object-rep type-rep values-rep)
(utils tc-utils)
(typecheck renamer)
(types subtype resolve)
(types subtype resolve numeric-tower)
(except-in (types utils abbrev kw-types) -> ->* one-of/c))
(require-for-cond-contract (rep rep-utils))
@ -54,7 +54,12 @@
(match-let ([(fld: ft _ _) (list-ref flds idx)])
(path-type rst ft (hash)))]
[((Intersection: ts) _)
;; vector length
[(vec-t (list (VecLenPE:)))
#:when (subtype vec-t -VectorTop)
-Int]
[((Intersection: ts _) _)
(apply -unsafe-intersect (for*/list ([t (in-list ts)]
[t (in-value (path-type path t resolved))]
#:when t)

View File

@ -8,7 +8,7 @@
racket/list
racket/set
(path-up "rep/type-rep.rkt" "rep/prop-rep.rkt" "rep/object-rep.rkt"
"rep/core-rep.rkt" "rep/values-rep.rkt"
"rep/core-rep.rkt" "rep/values-rep.rkt" "rep/fme-utils.rkt"
"rep/rep-utils.rkt" "types/subtype.rkt" "types/overlap.rkt"
"types/match-expanders.rkt"
"types/kw-types.rkt"
@ -17,7 +17,6 @@
"types/resolve.rkt"
"types/prefab.rkt"
"utils/utils.rkt"
"utils/primitive-comparison.rkt"
"utils/tc-utils.rkt")
(for-syntax racket/base syntax/parse))
@ -71,6 +70,14 @@
(and (pair? candidates)
(sort candidates string>? #:key symbol->string #:cache-keys? #t)))
;; primitive<=?
;;
;; provides a consistent ordering when printing things like
;; unions, intersections, etc
(define (primitive<=? s1 s2)
(string<=? (format "~a" s1)
(format "~a" s2)))
;; print-<thing> : <thing> Output-Port Boolean -> Void
;; print-type also takes an optional (Listof Symbol)
;;
@ -126,19 +133,41 @@
;; prop->sexp : Prop -> S-expression
;; Print a Prop (see prop-rep.rkt) to the given port
(define (prop->sexp prop)
(define (path->sexps path)
(if (null? path)
'()
(list (map pathelem->sexp path))))
(match prop
[(NotTypeProp: (Path: path nm) type)
`(! ,(type->sexp type) @ ,@(path->sexps path) ,(name-ref->sexp nm))]
[(TypeProp: (Path: path nm) type)
`(,(type->sexp type) @ ,@(path->sexps path) ,(name-ref->sexp nm))]
[(NotTypeProp: o type)
`(! ,(object->sexp o) ,(type->sexp type))]
[(TypeProp: o type)
`(: ,(object->sexp o) ,(type->sexp type))]
[(TrueProp:) 'Top]
[(FalseProp:) 'Bot]
[(AndProp: a) `(AndProp ,@(map prop->sexp a))]
[(OrProp: a) `(OrProp ,@(map prop->sexp a))]
[(AndProp: ps)
;; We do a little bit of work here to print equalities
;; instead of (<= x y) (<= y x) when we have both inequalities
(define-values (leqs others) (partition LeqProp? ps))
(define-values (eqs simple-leqs)
(for/fold ([eqs '()] [simple-leqs '()])
([leq (in-list leqs)])
(match leq
[(LeqProp: lhs rhs)
(define flip (-leq rhs lhs))
(cond
[(not (member flip leqs))
(values eqs (cons leq simple-leqs))]
[(member flip eqs) (values eqs simple-leqs)]
[else (values (cons leq eqs) simple-leqs)])])))
(let ([simple-leqs (map prop->sexp simple-leqs)]
[eqs (for/list ([leq (in-list eqs)])
(match leq
[(LeqProp: lhs rhs) `(= ,(object->sexp lhs) ,(object->sexp rhs))]))]
[others (map prop->sexp others)])
(match (append eqs simple-leqs others)
[(list sexp) sexp]
[sexps `(and ,@sexps)]))]
[(OrProp: ps) `(or ,@(map prop->sexp ps))]
[(LeqProp: (and lhs (LExp: 1 _))
(and rhs (LExp: 0 _)))
`(< ,(object->sexp (-lexp-sub1 lhs)) ,(object->sexp rhs))]
[(LeqProp: lhs rhs) `(<= ,(object->sexp lhs) ,(object->sexp rhs))]
[else `(Unknown Prop: ,(struct->vector prop))]))
;; pathelem->sexp : PathElem -> S-expression
@ -149,6 +178,7 @@
[(CdrPE:) 'cdr]
[(ForcePE:) 'force]
[(StructPE: t i) `(,(type->sexp t)-,i)]
[(VecLenPE:) 'vector-length]
[(SyntaxPE:) 'syntax]
[else `(Invalid Path-Element: ,(struct->vector pathelem))]))
@ -157,7 +187,24 @@
(define (object->sexp object)
(match object
[(Empty:) '-]
[(Path: pes n) (append (map pathelem->sexp pes) (list (name-ref->sexp n)))]
[(Path: pes n)
(let ([pes (map pathelem->sexp pes)])
(cond
[(null? pes) (name-ref->sexp n)]
[else (append pes (list (name-ref->sexp n)))]))]
[(LExp: c terms)
(cond
[(terms-empty? terms) c]
[else
(define term-list
(let ([terms (for/list ([(obj coeff) (in-terms terms)])
(if (= 1 coeff)
(object->sexp obj)
`(* ,coeff ,(object->sexp obj))))])
(if (zero? c) terms (cons c terms))))
(cond
[(null? (cdr term-list)) (car term-list)]
[else (cons '+ term-list)])])]
[else `(Unknown Object: ,(struct->vector object))]))
;; cover-union : Type LSet<Type> -> Listof<Symbol> Listof<Type>
@ -534,7 +581,9 @@
[(BaseUnion-bases: bs)
(define-values (covered remaining) (cover-union type bs ignored-names))
(cons 'U (sort (append covered (map t->s remaining)) primitive<=?))]
[(Intersection: elems)
[(Refine-name: x ty prop)
`(Refine [,(name-ref->sexp x) : ,ty] ,(prop->sexp prop))]
[(Intersection: elems _)
(cons ' (sort (map t->s elems) primitive<=?))]
[(Pair: l r) `(Pairof ,(t->s l) ,(t->s r))]
[(ListDots: dty dbound) `(List ,(t->s dty) ... ,dbound)]

View File

@ -4,18 +4,20 @@
racket/list racket/match
(prefix-in c: (contract-req))
(rep type-rep prop-rep object-rep values-rep rep-utils)
(logic ineq)
(only-in (infer infer) intersect)
(types subtype overlap subtract abbrev tc-result union))
(types subtype overlap subtract abbrev tc-result union path-type update))
(provide/cond-contract
[-and (c:->* () #:rest (c:listof Prop?) Prop?)]
[-or (c:->* () #:rest (c:listof Prop?) Prop?)]
[implies-atomic? (c:-> Prop? Prop? boolean?)]
[atomic-implies? (c:-> Prop? Prop? boolean?)]
[implies? (c:-> Prop? Prop? boolean?)]
[prop-equiv? (c:-> Prop? Prop? boolean?)]
[negate-prop (c:-> Prop? Prop?)]
[complementary? (c:-> Prop? Prop? boolean?)]
[contradictory? (c:-> Prop? Prop? boolean?)]
[atomic-complement? (c:-> Prop? Prop? boolean?)]
[atomic-contradiction? (c:-> Prop? Prop? boolean?)]
[contradiction? (c:-> Prop? Prop? boolean?)]
[add-unconditional-prop-all-args (c:-> Function? Type? Function?)]
[add-unconditional-prop (c:-> tc-results/c Prop? tc-results/c)]
[erase-props (c:-> tc-results/c tc-results/c)]
@ -60,32 +62,104 @@
[(tc-results: ts pss os)
(tc-results (map update-ps ts pss os) #f)]
[(tc-results: ts pss os dt db)
(tc-results (map update-ps ts pss os) (cons dt db))]
[_ (error 'reduce-tc-results/subsumption
"invalid res in subst-tc-results: ~a"
res)]))
(tc-results (map update-ps ts pss os) (cons dt db))]))
;; contradictory: Prop? Prop? -> boolean?
;; atomic-contradiction?: Prop? Prop? -> boolean?
;; Returns true if the AND of the two props is equivalent to FalseProp
(define (contradictory? p1 p2)
(define (atomic-contradiction? p1 p2)
(match* (p1 p2)
[((TypeProp: o1 t1) (NotTypeProp: o2 t2))
(and (eq? o1 o2) (subtype t1 t2))]
(and (eq? o1 o2) (subtype t1 t2 #:obj o1))]
[((NotTypeProp: o2 t2) (TypeProp: o1 t1))
(and (eq? o1 o2) (subtype t1 t2))]
(and (eq? o1 o2) (subtype t1 t2 #:obj o1))]
[((? LeqProp?) (? LeqProp?)) (contradictory-Leqs? p1 p2)]
[((FalseProp:) _) #t]
[(_ (FalseProp:)) #t]
[(_ _) #f]))
;; complementary: Prop? Prop? -> boolean?
;; do pes1 and pes2 share a common suffix and,
;; if so, does updating the shorter w/ the longer
;; result in bottom?
;; e.g. For the following args:
;; pes1 = (car (cdr x))
;; t1 = String
;; pes2 = (cdr x)
;; t2 = (Pairof Symbol Symbol)
;; it would see that both sets are talking
;; about (cdr x), and the first path actually
;; talks about a structural subcomponent of that
;; so it would update the 'car' of (Pairof Symbol Symbol)
;; with String and see that that is Bottom,
;; so it would return #t
(define (updates/pos-to-bot? pes1 t1 pes2 t2)
(define (check pes1 t1 pes2 t2 prefix-len)
(and (equal? pes1 (drop pes2 prefix-len))
(let ([prefix (take pes2 prefix-len)])
(Bottom? (update t1 t2 #t prefix)))))
(let ([len1 (length pes1)]
[len2 (length pes2)])
(cond
[(<= len1 len2)
(check pes1 t1 pes2 t2 (- len2 len1))]
[else
(check pes2 t2 pes1 t1 (- len1 len2))])))
;; does pes2 refer to the same or a subcomponent of
;; pes1 and if so, does updating the t1+ w/ the t2-
;; alond the difference result in bottom?
;; e.g. For the following args:
;; pes1 = (cdr x)
;; t1+ = (Pairof Symbol Symbol)
;; pes2 = (car (cdr x))
;; t2- = Symbol
;; would basically see that the path elements
;; are compatible and would update the car
;; field of (Pairof Symbol Symbol) to be _not_
;; Symbol, and so it would return #t
(define (updates/neg-to-bot? pes1 t1+ pes2 t2-)
(define len1 (length pes1))
(define len2 (length pes2))
(and (<= len1 len2)
(let ([prefix-len (- len2 len1)])
(and (equal? pes1 (drop pes2 prefix-len))
(let ([prefix (take pes2 prefix-len)])
(Bottom? (update t1+ t2- #f prefix)))))))
;; like atomic-contradiction? but it tries a little
;; harder, reasoning about how paths overlap
(define (contradiction? p1 p2)
(match* (p1 p2)
[((FalseProp:) _) #t]
[(_ (FalseProp:)) #t]
[((TypeProp: o t1) (NotTypeProp: o t2)) (subtype t1 t2 #:obj o)]
[((NotTypeProp: o t2) (TypeProp: o t1)) (subtype t1 t2 #:obj o)]
[((? LeqProp?) (? LeqProp?)) (contradictory-Leqs? p1 p2)]
[((TypeProp: (Path: pes1 x1) t1)
(TypeProp: (Path: pes2 x2) t2))
#:when (name-ref=? x1 x2)
(updates/pos-to-bot? pes1 t1 pes2 t2)]
[((TypeProp: (Path: pes1 x1) t1)
(NotTypeProp: (Path: pes2 x2) t2))
#:when (name-ref=? x1 x2)
(updates/neg-to-bot? pes1 t1 pes2 t2)]
[((NotTypeProp: (Path: pes2 x2) t2)
(TypeProp: (Path: pes1 x1) t1))
#:when (name-ref=? x1 x2)
(updates/neg-to-bot? pes1 t1 pes2 t2)]
[(_ _) #f]))
;; atomic-complement?: Prop? Prop? -> boolean?
;; Returns true if the OR of the two props is equivalent to Top
(define (complementary? p1 p2)
(define (atomic-complement? p1 p2)
(match* (p1 p2)
[((TypeProp: o1 t1) (NotTypeProp: o2 t2))
(and (eq? o1 o2) (subtype t2 t1))]
(and (eq? o1 o2) (subtype t2 t1 #:obj o1))]
[((NotTypeProp: o2 t2) (TypeProp: o1 t1))
(and (eq? o1 o2) (subtype t2 t1))]
(and (eq? o1 o2) (subtype t2 t1 #:obj o1))]
[((? LeqProp?) (? LeqProp?)) (complementary-Leqs? p1 p2)]
[((TrueProp:) _) #t]
[(_ (TrueProp:)) #t]
[(_ _) #f]))
@ -93,7 +167,7 @@
;; does p imply q? (but only directly/simply)
;; NOTE: because Ors and Atomic props are
;; interned, we use eq? and memq
(define (implies-atomic? p q)
(define (atomic-implies? p q)
(match* (p q)
;; reflexivity
[(_ _) #:when (or (eq? p q)
@ -111,15 +185,17 @@
;; t1 <: t2 ?
[((TypeProp: o1 t1)
(TypeProp: o2 t2))
(and (eq? o1 o2) (subtype t1 t2))]
(and (eq? o1 o2) (subtype t1 t2 #:obj o1))]
;; t2 <: t1 ?
[((NotTypeProp: o1 t1)
(NotTypeProp: o2 t2))
(and (eq? o1 o2) (subtype t2 t1))]
(and (eq? o1 o2) (subtype t2 t1 #:obj o1))]
;; t1 ∩ t2 = ∅ ?
[((TypeProp: o1 t1)
(NotTypeProp: o2 t2))
(and (eq? o1 o2) (not (overlap? t1 t2)))]
[((? LeqProp? p) (? LeqProp? q))
(Leq-implies-Leq? p q)]
;; otherwise we give up
[(_ _) #f]))
@ -155,32 +231,39 @@
(define ntf-map (make-hash))
;; consolidate type info and separate out other props
(define others
(for/fold ([others '()])
(define-values (leqs others)
(for/fold ([leqs '()]
[others '()])
([prop (in-list props)])
(match prop
[(TypeProp: o t1)
((if or? union-update! intersect-update!) tf-map t1 o)
others]
(values leqs others)]
[(NotTypeProp: o t1)
((if or? intersect-update! union-update!) ntf-map t1 o)
others]
[_ (cons prop others)])))
(values leqs others)]
[(? LeqProp? p) (values (cons p leqs) others)]
[_ (values leqs (cons prop others))])))
;; convert consolidated types into props and gather everything
(define raw-results
(append (for/list ([(k v) (in-hash tf-map)])
(-is-type k v))
(for/list([(k v) (in-hash ntf-map)])
(-not-type k v))
leqs
others))
;; check for abort condition and remove trivial props
(if or?
(if (member -tt raw-results)
(list -tt)
(filter-not FalseProp? raw-results))
(if (member -ff raw-results)
(list -ff)
(filter-not TrueProp? raw-results)))]))
(cond
[or?
(if (member -tt raw-results)
(list -tt)
(filter-not FalseProp? raw-results))]
[else
(cond
[(or (member -ff raw-results)
(not (satisfiable-Leqs? leqs)))
(list -ff)]
[else (filter-not TrueProp? raw-results)])])]))
@ -193,7 +276,9 @@
[(TypeProp: o t) (-not-type o t)]
[(NotTypeProp: o t) (-is-type o t)]
[(AndProp: ps) (apply -or (map negate-prop ps))]
[(OrProp: ps) (apply -and (map negate-prop ps))]))
[(OrProp: ps) (apply -and (map negate-prop ps))]
[(LeqProp: lhs rhs)
(-leq (-lexp-add1 rhs) lhs)]))
;; -or
;; (listof Prop?) -> Prop?
@ -231,12 +316,12 @@
[(TrueProp? cur) -tt]
[(FalseProp? cur) (loop rst result)]
;; is there a complementary case e.g. (ϕ ¬ϕ)? if so abort
[(for/or ([p (in-list rst)]) (complementary? p cur)) -tt]
[(for/or ([p (in-list result)]) (complementary? p cur)) -tt]
[(for/or ([p (in-list rst)]) (atomic-complement? p cur)) -tt]
[(for/or ([p (in-list result)]) (atomic-complement? p cur)) -tt]
;; don't include 'cur' if its covered by another prop
[(for/or ([p (in-list rst)]) (implies-atomic? cur p))
[(for/or ([p (in-list rst)]) (atomic-implies? cur p))
(loop rst result)]
[(for/or ([p (in-list result)]) (implies-atomic? cur p))
[(for/or ([p (in-list result)]) (atomic-implies? cur p))
(loop rst result)]
;; otherwise keep 'cur' in this disjunction
[else (loop rst (cons cur result))])]
@ -283,11 +368,11 @@
[(FalseProp? cur) -ff]
[(TrueProp? cur) (loop rst result)]
;; is there a contradition e.g. (ϕ ∧ ¬ϕ), if so abort
[(for/or ([p (in-list rst)]) (contradictory? p cur)) -ff]
[(for/or ([p (in-list result)]) (contradictory? p cur)) -ff]
[(for/or ([p (in-list rst)]) (atomic-contradiction? p cur)) -ff]
[(for/or ([p (in-list result)]) (atomic-contradiction? p cur)) -ff]
;; don't include 'cur' if its implied by another prop
;; already in our result (this is why we order the props!)
[(for/or ([p (in-list result)]) (implies-atomic? p cur))
[(for/or ([p (in-list result)]) (atomic-implies? p cur))
(loop rst result)]
;; otherwise keep 'cur' in this conjunction
[else (loop rst (cons cur result))])]

View File

@ -12,13 +12,14 @@
;; Type Type -> Type
;; conservatively calculates set subtraction
;; between the types (i.e. t - s)
(define (subtract t s)
(define (subtract t s #:obj [obj -empty-obj])
(define s-mask (mask s))
(define result
(let sub ([t t])
(let recurse ([t t] [obj obj])
(define (sub t [obj -empty-obj]) (recurse t obj))
(match t
[_ #:when (disjoint-masks? (mask t) s-mask) t]
[_ #:when (subtype t s) -Bottom]
[_ #:when (subtype t s #:obj obj) -Bottom]
[(or (App: _ _) (? Name?))
;; must be different, since they're not subtypes
;; and n must refer to a distinct struct type
@ -33,13 +34,14 @@
(make-BaseUnion (bbits-subtract bbits bbits*)
(nbits-subtract nbits nbits*))]
[_ (apply Un (for/list ([b (in-list (BaseUnion-bases t))])
(sub b)))])]
[(Union: base elems) (Union-fmap sub base elems)]
[(Intersection: ts)
(apply -unsafe-intersect (map sub ts))]
[(? Mu?) (sub (unfold t))]
[(Poly: vs b) (make-Poly vs (sub b))]
(sub b obj)))])]
[(Union: base elems) (Union-fmap (λ (t) (sub t obj)) base elems)]
[(Intersection: ts raw-prop)
(-refine (apply -unsafe-intersect (map (λ (t) (sub t obj)) ts))
raw-prop)]
[(? Mu?) (sub (unfold t) obj)]
[(Poly: vs b) (make-Poly vs (sub b) obj)]
[_ t])))
(cond
[(subtype t result) t]
[(subtype t result #:obj obj) t]
[else result]))

View File

@ -1,12 +1,14 @@
#lang racket/base
(require (except-in "../utils/utils.rkt" infer)
racket/match racket/function racket/lazy-require
racket/list racket/set
racket/list
(contract-req)
(rep type-rep prop-rep object-rep
core-rep type-mask values-rep rep-utils
free-variance rep-switch)
(utils tc-utils)
(only-in (env type-env-structs)
with-lexical-env with-naively-extended-lexical-env lexical-env)
(types utils resolve match-expanders current-seen
numeric-tower substitute prefab signatures)
(for-syntax racket/base syntax/parse racket/sequence)
@ -17,12 +19,14 @@
(lazy-require
("../infer/infer.rkt" (infer))
("../typecheck/tc-subst.rkt" (restrict-values)))
("../typecheck/tc-subst.rkt" (restrict-values instantiate-rep/obj))
("../typecheck/tc-envops.rkt" (env+ implies-in-env?)))
(provide NameStruct:)
(provide/cond-contract
[subtype (-> Type? Type? boolean?)]
[subtype (->* (Type? Type?) (#:obj OptObject?) boolean?)]
[subresult (-> Result? Result? boolean?)]
[subval (-> SomeValues? SomeValues? boolean?)]
[type-equiv? (-> Type? Type? boolean?)]
@ -35,10 +39,25 @@
;; Public Interface to Subtyping
;;************************************************************
;; When subtype is called w/ no object, we
;; us a temporary object to name the arguments.
;; This parameter gives us plenty of fresh, temporary names
;; to use and this way we don't have to be constantly allocating
;; fresh identifiers.
(define temp-objs
(make-parameter (make-obj-seq)))
;; is t1 a subtype of t2?
;; type type -> boolean
(define (subtype t1 t2)
(and (subtype* (seen) t1 t2) #t))
(define (subtype t1 t2 #:obj [obj #f])
(and
(cond
[obj (subtype* (seen) t1 t2 obj)]
[else
(define-values (o os) (obj-seq-next (temp-objs)))
(parameterize ([temp-objs os])
(subtype* (seen) t1 t2 o))])
#t))
;; is v1 a subval of v2?
@ -279,19 +298,6 @@
(app resolve-once (Poly: _ (? Struct? i))))
_))])))
(define (subtype/flds* A flds flds*)
(for/fold ([A A])
([f (in-list flds)] [f* (in-list flds*)]
#:break (not A))
(match* (f f*)
[((fld: t _ #t) (fld: t* _ #t))
(subtype-seq A
(subtype* t* t)
(subtype* t t*))]
[((fld: t _ #f) (fld: t* _ #f))
(subtype* A t t*)]
[(_ _) #f])))
(define (unrelated-structs s1 s2)
(define (in-hierarchy? s par)
(define s-name
@ -360,7 +366,7 @@
(Result: t2 (PropSet: p2+ p2-) o2))
(and (or (equal? o1 o2) (Empty? o2) (not o2))
(subtype-seq A
(subtype* t1 t2)
(subtype* t1 t2 o1)
(prop-subtype* p1+ p2+)
(prop-subtype* p1- p2-)))]))
@ -382,62 +388,72 @@
;; types as they are encountered:
;; needs-resolved? types (Mus, Names, Apps),
;; Instances, and Structs (Prefabs?)
(define/cond-contract (subtype* A t1 t2)
(-> (listof (cons/c Type? Type?)) Type? Type? (or/c #f list?))
(cond
[(Univ? t2) A]
[(Bottom? t1) A]
;; error is top and bot
[(or (Error? t1) (Error? t2)) A]
[(disjoint-masks? (mask t1) (mask t2)) #f]
[(equal? t1 t2) A]
[(seen? t1 t2 A) A]
[else
;; first we check on a few t2 cases
;; that need to come early during checking
(match t2
[(Intersection: t2s)
(for/fold ([A A])
([t2 (in-list t2s)]
#:break (not A))
(subtype* A t1 t2))]
[(? resolvable?)
(let ([A (remember t1 t2 A)])
(with-updated-seen A
(let ([t2 (resolve-once t2)])
;; check needed for if a name that hasn't been resolved yet
(and (Type? t2) (subtype* A t1 t2)))))]
[_
;; then we try a switch on t1
(subtype-switch
t1 t2 A
;; if we're still not certain after the switch,
;; check the cases that need to come at the end
(λ (A t1 t2)
(match* (t1 t2)
[(t1 (Union/set: base2 ts2 elems2))
(cond
[(set-member? elems2 t1) A]
[(subtype* A t1 base2)]
[else (for/or ([elem2 (in-list ts2)])
(subtype* A t1 elem2))])]
[((Intersection: t1s) _)
(for/or ([t1 (in-list t1s)])
(subtype* A t1 t2))]
[(_ (Instance: (? resolvable? t2*)))
(let ([A (remember t1 t2 A)])
(with-updated-seen A
(let ([t2* (resolve-once t2*)])
(and (Type? t2*)
(subtype* A t1 (make-Instance t2*))))))]
[(_ (Poly: vs2 b2))
#:when (null? (fv b2))
(subtype* A t1 b2)]
[(_ (PolyDots: vs2 b2))
#:when (and (null? (fv b2))
(null? (fi b2)))
(subtype* A t1 b2)]
[(_ _) #f])))])]))
(define subtype*
(case-lambda
[(A t1 t2)
(define-values (o os) (obj-seq-next (temp-objs)))
(parameterize ([temp-objs os])
(subtype* A t1 t2 o))]
[(A t1 t2 obj)
(cond
[(Univ? t2) A]
[(Bottom? t1) A]
;; error is top and bot
[(or (Error? t1) (Error? t2)) A]
[(disjoint-masks? (mask t1) (mask t2)) #f]
[(equal? t1 t2) A]
[(seen? t1 t2 A) A]
[else
;; first we check on a few t2 cases
;; that need to come early during checking
(match t2
[(Intersection: t2s raw-prop)
(let ([A (for/fold ([A A])
([t2 (in-list t2s)]
#:break (not A))
(subtype* A t1 t2 obj))])
(and A
(or (TrueProp? raw-prop)
(let* ([obj (if (Empty? obj) (-id-path (genid)) obj)]
[prop (instantiate-rep/obj raw-prop obj t1)])
(implies-in-env? (lexical-env)
(-is-type obj t1)
prop)))
A))]
[(? resolvable?)
(let ([A (remember t1 t2 A)])
(with-updated-seen A
(let ([t2 (resolve-once t2)])
;; check needed for if a name that hasn't been resolved yet
(and (Type? t2) (subtype* A t1 t2 obj)))))]
[_
;; otherwise we case on t1
(subtype-cases
A t1 t2 obj
;; if we're still not certain after the switch,
;; check the cases that need to come at the end
(λ (A t1 t2 obj)
(match* (t1 t2)
[(t1 (Union/set: base2 ts2 elems2))
(cond
[(hash-has-key? elems2 t1) A]
[(subtype* A t1 base2 obj)]
[else (for/or ([elem2 (in-list ts2)])
(subtype* A t1 elem2 obj))])]
[(_ (Instance: (? resolvable? t2*)))
(let ([A (remember t1 t2 A)])
(with-updated-seen A
(let ([t2* (resolve-once t2*)])
(and (Type? t2*)
(subtype* A t1 (make-Instance t2*) obj)))))]
[(_ (Poly: vs2 b2))
#:when (null? (fv b2))
(subtype* A t1 b2 obj)]
[(_ (PolyDots: vs2 b2))
#:when (and (null? (fv b2))
(null? (fi b2)))
(subtype* A t1 b2 obj)]
[(_ _) #f])))])])]))
;; these data structures are allocated once and
@ -473,7 +489,7 @@
(cons portable-fixnum? -NonNegFixnum)
(cons values -Nat)))
(define-switch (subtype-switch t1 t2 A continue)
(define-rep-switch (subtype-cases A (#:switch t1) t2 obj continue)
;; NOTE: keep these in alphabetical order
;; or ease of finding cases
[(case: App _)
@ -487,7 +503,7 @@
[(? Async-ChannelTop?) A]
[(Async-Channel: elem2) (type≡? A elem1 elem2)]
[(Evt: evt-t) (subtype* A elem1 evt-t)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Base (Base-bits: num? bits))
(match t2
[(BaseUnion: bbits nbits)
@ -519,7 +535,7 @@
[(Base:Log-Receiver? t1)
(subtype* A log-vect-type evt-t)]
[else #f])]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: BaseUnion (BaseUnion: bbits1 nbits1))
(match t2
[(? Base?) #f]
@ -534,18 +550,18 @@
[_ (for/fold ([A A])
([b (in-list (BaseUnion-bases t1))]
#:break (not A))
(subtype* A b t2))])]
(subtype* A b t2 obj))])]
[(case: Box (Box: elem1))
(match t2
[(? BoxTop?) A]
[(Box: elem2) (type≡? A elem1 elem2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Channel (Channel: elem1))
(match t2
[(? ChannelTop?) A]
[(Channel: elem2) (type≡? A elem1 elem2)]
[(Evt: evt-t) (subtype* A elem1 evt-t)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Class (Class: row inits fields methods augments init-rest))
(match t2
[(? ClassTop?) A]
@ -585,13 +601,13 @@
(sub init-rest init-rest*))
(and (not init-rest) (not init-rest*)
A)))]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Continuation-Mark-Keyof (Continuation-Mark-Keyof: val1))
(match t2
[(? Continuation-Mark-KeyTop?) A]
[(Continuation-Mark-Keyof: val2)
(type≡? A val1 val2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: CustodianBox (CustodianBox: elem1))
(match t2
[(CustodianBox: elem2) (subtype* A elem1 elem2)]
@ -599,28 +615,28 @@
;; Note that it's the whole box type that's being
;; compared against evt-t here
(subtype* A t1 evt-t)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Distinction (Distinction: nm1 id1 t1*))
(match t2
[(app resolve (Distinction: nm2 id2 t2*))
#:when (and (equal? nm1 nm2) (equal? id1 id2))
(subtype* A t1* t2*)]
[_ (cond
[(subtype* A t1* t2)]
[else (continue A t1 t2)])])]
[(subtype* A t1* t2 obj)]
[else (continue A t1 t2 obj)])])]
[(case: Ephemeron (Ephemeron: elem1))
(match t2
[(Ephemeron: elem2) (subtype* A elem1 elem2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Evt (Evt: result1))
(match t2
[(Evt: result2) (subtype* A result1 result2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: F (F: var1))
(match t2
;; tvars are equal if they are the same variable
[(F: var2) (eq? var1 var2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Function (Function: arrs1))
(match t2
;; special-case for case-lambda/union with only one argument
@ -640,11 +656,11 @@
[(supertype-of-one/arr A (car arrs2) arrs1)
=> (λ (A) (loop-arities A (cdr arrs2)))]
[else #f])))]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Future (Future: elem1))
(match t2
[(Future: elem2) (subtype* A elem1 elem2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Hashtable (Hashtable: key1 val1))
(match t2
[(? HashtableTop?) A]
@ -655,7 +671,7 @@
(subtype-seq A
(subtype* key1 key2)
(subtype* val1 val2))]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: HeterogeneousVector (HeterogeneousVector: elems1))
(match t2
[(VectorTop:) A]
@ -677,7 +693,7 @@
([elem1 (in-list elems1)]
#:break (not A))
(subtype* A elem1 seq-t))]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Instance (Instance: inst-t1))
(cond
[(resolvable? inst-t1)
@ -707,12 +723,30 @@
(and ;; Note that init & augment clauses don't matter for objects
(subtype-clause? method-map method-map*)
(subtype-clause? field-map field-map*))]
[(_ _) (continue A t1 t2)])])]
[(case: Intersection (Intersection: t1s))
(cond
[(for/or ([t1 (in-list t1s)])
(subtype* A t1 t2))]
[else (continue A t1 t2)])]
[(_ _) (continue A t1 t2 obj)])])]
[(case: Intersection (Intersection: t1s _))
(match t1
[(Refine: t1* raw-prop)
(cond
[(Object? obj)
(define prop (instantiate-rep/obj raw-prop obj t1*))
(define env (env+ (lexical-env) (list prop)))
(cond
[(not env) A]
[else (with-lexical-env env
(subtype* A t1* t2 obj))])]
[else
(define id (genid))
(define obj (-id-path id))
(define prop (instantiate-rep/obj raw-prop obj t1*))
;; since this is a fresh object, we will do a simpler environment extension
(with-naively-extended-lexical-env [#:props (list prop)]
(subtype* A t1* t2 obj))])]
[_
(cond
[(for/or ([t1 (in-list t1s)])
(subtype* A t1 t2 obj))]
[else (continue A t1 t2 obj)])])]
[(case: ListDots (ListDots: dty1 dbound1))
(match t2
;; recur structurally on dotted lists, assuming same bounds
@ -726,7 +760,7 @@
;; variance issues.
[(Listof: elem2)
(subtype* A (-poly (dbound1) dty1) elem2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: MPair (MPair: t11 t12))
(match t2
[(? MPairTop?) A]
@ -741,7 +775,7 @@
(subtype* t11 seq-t)
(subtype* t12 null-or-mpair-top)
(subtype* t12 (make-Sequence (list seq-t))))]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Mu _)
(let ([A (remember t1 t2 A)])
(with-updated-seen A
@ -765,27 +799,27 @@
(match t2
[(Pair: t21 t22)
(subtype-seq A
(subtype* t11 t21)
(subtype* t12 t22))]
(subtype* t11 t21 (-car-of obj))
(subtype* t12 t22 (-cdr-of obj)))]
[(Sequence: (list seq-t))
(subtype-seq A
(subtype* t11 seq-t)
(subtype* t12 (-lst seq-t)))]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Param (Param: in1 out1))
(match t2
[(Param: in2 out2) (subtype-seq A
(subtype* in2 in1)
(subtype* out1 out2))]
[_ (subtype* A (cl->* (t-> out1) (t-> in1 -Void)) t2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Poly (Poly: names b1))
(match t2
[(? Poly?) #:when (= (length names) (Poly-n t2))
(subtype* A b1 (Poly-body names t2))]
;; use local inference to see if we can use the polytype here
[_ #:when (infer names null (list b1) (list t2) Univ) A]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: PolyDots (PolyDots: (list ns ... n-dotted) b1))
(match t2
[(PolyDots: (list ms ... m-dotted) b2)
@ -813,7 +847,7 @@
(subtype* A (subst-all subst b1) b2)]
[_ #:when (infer ns (list n-dotted) (list b1) (list t2) Univ)
A]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Prefab (Prefab: k1 ss))
(match t2
[(Prefab: k2 ts)
@ -832,11 +866,11 @@
(subtype* t s)
(subtype* s t))
(subtype* A s t))))))))]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Promise (Promise: elem1))
(match t2
[(Promise: elem2) (subtype* A elem1 elem2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Prompt-Tagof (Prompt-Tagof: body1 handler1))
(match t2
[(? Prompt-TagTop?) A]
@ -844,7 +878,7 @@
(subtype-seq A
(type≡? body1 body2)
(type≡? handler1 handler2))]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Refinement (Refinement: t1-parent id1))
(match t2
[(Refinement: t2-parent id2)
@ -852,17 +886,17 @@
(subtype* A t1-parent t2-parent)]
[_ (cond
[(subtype* A t1-parent t2)]
[else (continue A t1 t2)])])]
[else (continue A t1 t2 obj)])])]
;; sequences are covariant
[(case: Sequence (Sequence: ts1))
(match t2
[(Sequence: ts2) (subtypes* A ts1 ts2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Set (Set: elem1))
(match t2
[(Set: elem2) (subtype* A elem1 elem2)]
[(Sequence: (list seq-t)) (subtype* A elem1 seq-t)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Struct (Struct: nm1 parent1 flds1 proc1 _ _))
(match t2
;; Avoid resolving things that refer to different structs.
@ -878,7 +912,18 @@
(let ([A (cond [(and proc1 proc2) (subtype* A proc1 proc2)]
[proc2 #f]
[else A])])
(and A (subtype/flds* A flds1 flds2)))))]
(for/fold ([A A])
([f1 (in-list flds1)]
[f2 (in-list flds2)]
[idx (in-naturals)]
#:break (not A))
(match* (f1 f2)
[((fld: fty1 _ mutable1?) (fld: fty2 _ mutable2?))
#:when (eq? mutable1? mutable2?)
(cond
[mutable1? (type≡? A fty1 fty2)]
[else (subtype* A fty1 fty2 (-struct-idx-of t1 idx obj))])]
[(_ _) #f])))))]
[(StructTop: (Struct: nm2 _ _ _ _ _))
#:when (free-identifier=? nm1 nm2)
A]
@ -889,23 +934,23 @@
(let ([A (remember t1 t2 A)])
(with-updated-seen A
(subtype* A parent1 t2))))]
[else (continue A t1 t2)])]
[_ (continue A t1 t2)])]
[else (continue A t1 t2 obj)])]
[_ (continue A t1 t2 obj)])]
[(case: StructType (StructType: t1*))
(match t2
[(StructTypeTop:) A]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Syntax (Syntax: elem1))
(match t2
[(Syntax: elem2) (subtype* A elem1 elem2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: ThreadCell (ThreadCell: elem1))
(match t2
[(? ThreadCellTop?) A]
[(ThreadCell: elem2) (type≡? A elem1 elem2)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Union (Union/set: base1 ts1 elems1))
(let ([A (subtype* A base1 t2)])
(let ([A (subtype* A base1 t2 obj)])
(and A
(match t2
[(Union/set: base2 ts2 elems2)
@ -913,13 +958,13 @@
([elem1 (in-list ts1)]
#:break (not A))
(cond
[(set-member? elems2 elem1) A]
[(subtype* A elem1 base2)]
[else (subtype* A elem1 t2)]))]
[(hash-has-key? elems2 elem1) A]
[(subtype* A elem1 base2 obj)]
[else (subtype* A elem1 t2 obj)]))]
[_ (for/fold ([A A])
([elem1 (in-list ts1)]
#:break (not A))
(subtype* A elem1 t2))])))]
(subtype* A elem1 t2 obj))])))]
;; For Unit types invoke-types are covariant
;; imports and init-depends are covariant in that importing fewer
;; signatures results in a subtype
@ -932,7 +977,7 @@
(check-sub-signatures? exports1 exports2)
(check-sub-signatures? init-depends2 init-depends1)
(subval* A t1* t2*))]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Value (Value: val1))
(match t2
[(Base-predicate: pred) (and (pred val1) A)]
@ -953,16 +998,24 @@
[(or (? Struct? s1) (NameStruct: s1))
#:when (not (struct? val1))
#f]
[_ (continue A t1 t2)])]
[(Refine: t2* p*)
#:when (and (exact-integer? val1)
(let ([obj (-lexp val1)])
(and (subtype* A t1 t2*)
(implies-in-env? (lexical-env)
(-is-type obj t1)
(instantiate-rep/obj p* obj t1)))))
A]
[_ (continue A t1 t2 obj)])]
[(case: Vector (Vector: elem1))
(match t2
[(? VectorTop?) A]
[(Vector: elem2) (type≡? A elem1 elem2)]
[(Sequence: (list seq-t)) (subtype* A elem1 seq-t)]
[_ (continue A t1 t2)])]
[_ (continue A t1 t2 obj)])]
[(case: Weak-Box (Weak-Box: elem1))
(match t2
[(? Weak-BoxTop?) A]
[(Weak-Box: elem2) (type≡? A elem1 elem2)]
[_ (continue A t1 t2)])]
[else: (continue A t1 t2)])
[_ (continue A t1 t2 obj)])]
[else: (continue A t1 t2 obj)])

View File

@ -12,7 +12,6 @@
[->* -->*]
[one-of/c -one-of/c]))
(provide update)
;; update
@ -47,23 +46,17 @@
;; struct ops
[((Struct: nm par flds proc poly pred)
(StructPE: (? (λ (s) (subtype t s))) idx))
(StructPE: s idx))
#:when (subtype t s)
;; Note: this updates fields even if they are not polymorphic.
;; Because subtyping is nominal and accessor functions do not
;; reflect this, this behavior is unobservable except when a
;; variable aliases the field in a let binding
(define-values (lhs rhs) (split-at flds idx))
(define-values (ty* acc-id)
(match rhs
[(cons (fld: ty acc-id #f) _)
(values (update ty rst) acc-id)]
[_ (int-err "update on mutable struct field")]))
(cond
[(Bottom? ty*) ty*]
[else
(define flds*
(append lhs (cons (make-fld ty* acc-id #f) (cdr rhs))))
(make-Struct nm par flds* proc poly pred)])]
(match-define-values (lhs (cons (fld: ty acc-id #f) rhs)) (split-at flds idx))
(match (update ty rst)
[(Bottom:) -Bottom]
[ty (let ([flds (append lhs (cons (make-fld ty acc-id #f) rhs))])
(make-Struct nm par flds proc poly pred))])]
;; class field ops
;;
@ -84,10 +77,11 @@
;; bases from the union
(Union-fmap (λ (t) (update t path)) -Bottom ts)]
[((Intersection: ts) _)
(for/fold ([t Univ])
([elem (in-list ts)])
(intersect t (update elem path)))]
[((Intersection: ts raw-prop) _)
(-refine (for/fold ([t Univ])
([elem (in-list ts)])
(intersect t (update elem path)))
raw-prop)]
[(_ _)
(match path-elem

View File

@ -1,55 +0,0 @@
#lang racket/base
(require racket/unsafe/ops
racket/format)
(provide primitive<=?)
;; vector of predicates for primitives paired with
;; functions which compair primitives of the same type
(define prims
(vector (cons (λ (v) (eq? v #t)) (λ _ #t))
(cons (λ (v) (eq? v #f)) (λ _ #t))
(cons (λ (v) (eq? v '())) (λ _ #t))
(cons real? <=)
(cons complex? (λ (x y) (and (<= (real-part x)
(real-part y))
(<= (imag-part x)
(imag-part y)))))
(cons char? char<=?)
(cons string? string<=?)
(cons bytes? (λ (b1 b2) (or (bytes<? b1 b2)
(bytes=? b1 b2))))
(cons symbol? (λ (s1 s2) (or (symbol<? s1 s2)
(eq? s1 s2))))
(cons keyword? (λ (k1 k2) (or (keyword<? k1 k2)
(eq? k1 k2))))
(cons pair? (λ (p1 p2) (and (primitive<=? (car p1) (car p2))
(primitive<=? (cdr p1) (cdr p2)))))
(cons vector? (λ (v1 v2) (and (< (vector-length v1) (vector-length v2))
(and (= (vector-length v1) (vector-length v2))
(for/and ([val1 (in-vector v1)]
[val2 (in-vector v2)])
(primitive<=? val1 val2))))))
(cons box? (λ (b1 b2) (primitive<=? (unbox b1) (unbox b2))))))
;; finds which index into prims 's' belongs
(define (index-of s)
(let loop ([i 0])
(cond
[(unsafe-fx<= i (vector-length prims))
(if ((unsafe-car (unsafe-vector-ref prims i)) s)
i
(loop (unsafe-fx+ i 1)))]
[else (error 'index-of "impossible!")])))
;; compares two primitives (i.e. sexps) based on the ordering
;; implied by the 'prims' predicates and, if they are equal types of
;; primitives, on the functions contained in prims
(define (primitive<=? s1 s2)
(define idx1 (index-of s1))
(define idx2 (index-of s2))
(cond
[(unsafe-fx< idx1 idx2) #t]
[(unsafe-fx> idx1 idx2) #f]
[else ((unsafe-cdr (vector-ref prims idx1)) s1 s2)]))

View File

@ -8,26 +8,36 @@ at least theoretically.
(require (for-syntax racket/base racket/string)
racket/require-syntax racket/provide-syntax
racket/match
racket/list
syntax/parse/define
racket/struct-info "timing.rkt")
(provide
;; optimization
optimize?
;; parameter to toggle linear integer reasoning
with-linear-integer-arithmetic?
;; timing
start-timing do-time
;; provide macros
rep utils typecheck infer env private types static-contracts
;; misc
list-extend
ends-with?
filter-multiple
syntax-length
in-pair
in-sequence-forever
match*/no-order
bind)
bind
genid
gen-pretty-id
local-tr-identifier?
mark-id-as-normalized
normalized-id?)
(define optimize? (make-parameter #t))
(define with-linear-integer-arithmetic? (make-parameter #f))
(define-for-syntax enable-contracts? (and (getenv "PLT_TR_CONTRACTS") #t))
(define-syntax do-contract-req
@ -91,6 +101,7 @@ at least theoretically.
(define-requirer env env-out)
(define-requirer private private-out)
(define-requirer types types-out)
(define-requirer logic logic-out)
(define-requirer optimizer optimizer-out)
(define-requirer base-env base-env-out)
(define-requirer static-contracts static-contracts-out)
@ -230,6 +241,14 @@ at least theoretically.
(define (list-extend s t extra)
(append t (build-list (max 0 (- (length s) (length t))) (lambda _ extra))))
;; does l1 end with l2?
;; e.g. (list 1 2 3) ends with (list 2 3)
(define (ends-with? l1 l2)
(define len1 (length l1))
(define len2 (length l2))
(and (<= len2 len1)
(equal? l2 (drop l1 (- len1 len2)))))
(define (filter-multiple l . fs)
(apply values
(map (lambda (f) (filter f l)) fs)))
@ -282,3 +301,46 @@ at least theoretically.
(define-syntax-rule (in-pair p)
(in-parallel (in-value (car p)) (in-value (cdr p))))
(module local-ids racket
(provide local-tr-identifier?
genid
gen-pretty-id
mark-id-as-normalized
normalized-id?)
;; we use this syntax location to recognized gensymed identifiers
(define-for-syntax loc #'x)
(define dummy-id (datum->syntax #'loc (gensym 'x)))
;; tools for marking identifiers as normalized and recognizing normalized
;; identifiers (we normalize ids so free-identifier=? ids are represented
;; with the same syntax object and are thus equal?)
(define-values (mark-id-as-normalized
normalized-id?)
(let ([normalized-identifier-sym (gensym 'normal-id)])
(values (λ (id) (syntax-property id normalized-identifier-sym #t))
(λ (id) (syntax-property id normalized-identifier-sym)))))
;; generates fresh identifiers for use while typechecking
(define (genid [sym (gensym 'local)])
(mark-id-as-normalized (datum->syntax #'loc sym)))
(define letters '("x" "y" "z" "a" "b" "c" "d" "e" "f" "g" "h" "i" "j" "k"
"l" "m" "n" "o" "p" "q" "r" "s" "t" "u" "v" "w"))
;; this is just a silly helper function that gives us a letter from
;; the latin alphabet in a cyclic manner
(define next-letter
(let ([i 0])
(λ ()
(define letter (string->uninterned-symbol (list-ref letters i)))
(set! i (modulo (add1 i) (length letters)))
letter)))
;; generates a fresh identifier w/ a "pretty" printable representation
(define (gen-pretty-id [sym (next-letter)])
(mark-id-as-normalized (datum->syntax #'loc sym)))
;; allows us to recognize and distinguish gensym'd identifiers
;; from ones that came from the program we're typechecking
(define (local-tr-identifier? id)
(and (identifier? id)
(eq? (syntax-source-module dummy-id)
(syntax-source-module id)))))
(require 'local-ids)

View File

@ -0,0 +1,24 @@
#lang typed/racket #:with-linear-integer-arithmetic
(define n-1 : (Refine [x : Integer] (= x -1)) -1)
(define n0 : (Refine [x : Integer] (= x 0)) 0)
(define n0* : (Refine [x : Zero] (= x 0)) 0)
(define n1 : (Refine [x : Integer] (= x 1)) 1)
(define n2 : (Refine [x : Integer] (= x 2)) 2)
(define n2* : (Refine [x : Byte] (= x 2)) 2)
(define n3 : (Refine [x : Integer] (= x 3)) 3)
(define n42 : (Refine [x : Integer] (= x 42)) 42)
(define n42* : (Refine [x : Byte] (= x 42)) 42)
(define n42** : (Refine [x : Fixnum] (= x 42)) 42)
(define x 1)
(ann x One)
(ann x (Refine [x : One] (= x 1)))
(define y : Integer 1)
(define z : (Refine [v : Integer] (= v (* 2 y)))
(* 2 y))

View File

@ -0,0 +1,224 @@
#lang typed/racket #:with-linear-integer-arithmetic
(provide add-to-one)
(: add-to-one (-> (Refine [o : Integer] (= o 1))
Integer
Integer))
(define (add-to-one one n)
(+ one n))
(ann 42 (Refine [n : Integer] (= n 42)))
;; constant comparisons
(if (< 5 4)
(+ "Luke," "I am your father")
"that's impossible!")
(if (<= 5 4)
(+ "Luke," "I am your father")
"that's impossible!")
(if (= 5 4)
(+ "Luke," "I am your father")
"that's impossible!")
(if (>= 4 5)
(+ "Luke," "I am your father")
"that's impossible!")
(if (> 4 5)
(+ "Luke," "I am your father")
"that's impossible!")
;; arithmetic op comparisons
(if (< (+ 2 3) 4)
(+ "Luke," "I am your father")
"that's impossible!")
(if (<= (+ 2 3) (* 2 2))
(+ "Luke," "I am your father")
"that's impossible!")
(if (= (+ 2 3) 4)
(+ "Luke," "I am your father")
"that's impossible!")
(if (>= 4 (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
(if (> (* 2 2) (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
;; module level bound to integers
(define four 4)
(if (< (+ 2 3) four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (<= (+ 2 3) four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (= (+ 2 3) four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (>= four (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
(if (> four (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
;; module level bound to expr
(define two+two (+ 2 2))
(if (< (+ 2 3) two+two)
(+ "Luke," "I am your father")
"that's impossible!")
(if (<= (+ 2 3) two+two)
(+ "Luke," "I am your father")
"that's impossible!")
(if (= (+ 2 3) two+two)
(+ "Luke," "I am your father")
"that's impossible!")
(if (>= two+two (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
(if (> two+two (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
;; let binding bound to integers
(let ([four four]
[other-four 4]
[two+two (+ 2 2)])
(if (< (+ 2 3) four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (<= (+ 2 3) four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (= (+ 2 3) four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (>= four (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
(if (> four (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
(if (< (+ 2 3) other-four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (<= (+ 2 3) other-four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (= (+ 2 3) other-four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (>= other-four (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
(if (> other-four (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
(if (< (+ 2 3) two+two)
(+ "Luke," "I am your father")
"that's impossible!")
(if (<= (+ 2 3) two+two)
(+ "Luke," "I am your father")
"that's impossible!")
(if (= (+ 2 3) two+two)
(+ "Luke," "I am your father")
"that's impossible!")
(if (>= two+two (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
(if (> two+two (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!"))
(define (foo [four : (Refine [val : Integer] (= val 4))])
(if (< (+ 2 3) four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (<= (+ 2 3) four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (= (+ 2 3) four)
(+ "Luke," "I am your father")
"that's impossible!")
(if (>= four (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!")
(if (> four (+ 2 3))
(+ "Luke," "I am your father")
"that's impossible!"))

View File

@ -12,6 +12,8 @@
(provide tests)
(gen-test-main)
(define x #'x)
;; Ensure that we never return a prop or object of #f.
(define (check-prop f)
(match f

View File

@ -6,7 +6,7 @@
(for-template racket/base)
(private type-contract)
(rep type-rep values-rep)
(types abbrev numeric-tower)
(types abbrev numeric-tower prop-ops)
(static-contracts combinators optimize)
(submod typed-racket/private/type-contract numeric-contracts)
(submod typed-racket/private/type-contract test-exports)
@ -115,17 +115,18 @@
(define namespace (ctc-namespace))
(define val (eval (quote val-expr) namespace))
(define fun-val (eval (quote fun-expr) namespace))
(check (λ ()
(define ctced-val
(eval #`(let ()
#,@(map (λ (stx) (syntax-shift-phase-level stx 1))
extra-stxs)
(contract #,(syntax-shift-phase-level ctc-stx 1)
#,val
#,(quote (quote #,pos))
#,(quote (quote #,neg))))
namespace))
(fun-val ctced-val))))))]))
#,(quasisyntax/loc stx
(check (λ ()
(define ctced-val
(eval #`(let ()
#,@(map (λ (stx) (syntax-shift-phase-level stx 1))
extra-stxs)
(contract #,(syntax-shift-phase-level ctc-stx 1)
#,val
#,(quote (quote #,pos))
#,(quote (quote #,neg))))
namespace))
(fun-val ctced-val)))))))]))
(define tests
(test-suite
@ -387,4 +388,218 @@
"more than 1 non-flat contract")
(t/fail (-unsafe-intersect (-box -Symbol) (-box Univ))
"more than 1 non-flat contract")
))
;; logical refinements
(let ([int<=42 (-refine/fresh x -Int (-leq (-lexp x) (-lexp 42)))])
(t int<=42)
(t-int (-> int<=42 int<=42)
(λ (c) (c 1))
(λ (_) 1)
#:typed)
(t-int/fail (-> int<=42 int<=42)
(λ (c) (c "bad"))
(λ (_) 1)
#:typed
#:msg #rx"expected: Integer.*given: \"bad\"")
(t-int/fail (-> int<=42 int<=42)
(λ (c) (c 43))
(λ (_) 1)
#:typed
#:msg #rx"expected: .*given: 43")
(t-int/fail (-> int<=42 int<=42)
(λ (c) (c 1))
(λ (_) "bad")
#:untyped
#:msg #rx"promised: .*produced: \"bad\"")
(t-int/fail (-> int<=42 int<=42)
(λ (c) (c 1))
(λ (_) 43)
#:untyped
#:msg #rx"promised: .*produced: 43")
;; make sure we optimize away the trusted side (e.g. if the type
;; system is unsound, we can return an incorrect value)
(t-int (-> int<=42 int<=42)
(λ (c) (c 1))
(λ (_) 43)
#:typed))
;; logical refinements w/ car/cdr
(let ([ord-pair (-refine/fresh p (-pair -Int -Int) (-leq (-lexp (-car-of (-id-path p)))
(-lexp (-cdr-of (-id-path p)))))])
(t ord-pair)
(t-int (-> ord-pair ord-pair)
(λ (c) (cons 1 2))
(λ (_) 1)
#:typed)
(t-int/fail (-> ord-pair ord-pair)
(λ (c) (c "bad"))
(λ (_) (cons 1 2))
#:typed
#:msg #rx"expected: .*given: \"bad\"")
(t-int/fail (-> ord-pair ord-pair)
(λ (c) (c (cons "a" 0)))
(λ (_) (cons 1 2))
#:typed
#:msg #rx"expected: .*given: \"a\"")
(t-int/fail (-> ord-pair ord-pair)
(λ (c) (c (cons 0 "d")))
(λ (_) (cons 1 2))
#:typed
#:msg #rx"expected: .*given: \"d\"")
(t-int/fail (-> ord-pair ord-pair)
(λ (c) (c (cons 1 0)))
(λ (_) (cons 1 2))
#:typed
#:msg #rx"expected: .*given: .*(1 . 0)")
(t-int/fail (-> ord-pair ord-pair)
(λ (c) (c (cons 3 4)))
(λ (_) "bad")
#:untyped
#:msg #rx"promised: .*produced: \"bad\"")
(t-int/fail (-> ord-pair ord-pair)
(λ (c) (c (cons 3 4)))
(λ (_) (cons 4 3))
#:untyped
#:msg #rx"promised: .*produced: .*(4 . 3)")
;; make sure we optimize away the trusted side (e.g. if the type
;; system is unsound, we can return an incorrect value)
(t-int (-> ord-pair ord-pair)
(λ (c) (cons 3 4))
(λ (_) 43)
#:typed))
;; refinements w/ vector length refinements
(let ([vec-w/len<=10
(-refine/fresh p (-vec Univ) (-leq (-lexp (-vec-len-of (-id-path p)))
(-lexp 10)))])
(t vec-w/len<=10)
(t-int (-> vec-w/len<=10 vec-w/len<=10)
(λ (c) (c (vector 0)))
(λ (_) (vector 0))
#:typed)
(t-int/fail (-> vec-w/len<=10 vec-w/len<=10)
(λ (c) (c (for/vector ([n (in-range 11)]) n)))
(λ (_) (vector 0))
#:typed
#:msg #rx"expected: .*given: .*(0 1 2 3 4 5 6 7 8 9 10)")
(t-int/fail (-> vec-w/len<=10 vec-w/len<=10)
(λ (c) (c (vector 0)))
(λ (_) (for/vector ([n (in-range 11)]) n))
#:untyped
#:msg #rx"promised: .*produced: .*(0 1 2 3 4 5 6 7 8 9 10)")
;; typed can be unsound
(t-int (-> vec-w/len<=10 vec-w/len<=10)
(λ (c) (c (vector 0)))
(λ (_) (for/vector ([n (in-range 11)]) n))
#:typed))
;; logical propositions about types
(let ([pair-car-is-int (-refine/fresh p (-pair Univ Univ) (-is-type (-car-of (-id-path p)) -Int))])
(t pair-car-is-int)
(t-int (-> pair-car-is-int pair-car-is-int)
(λ (c) (c (cons 42 "any")))
(λ (_) (cons 42 "any"))
#:typed)
(t-int/fail (-> pair-car-is-int pair-car-is-int)
(λ (c) (c (cons "any" "any")))
(λ (_) (cons 42 "any"))
#:typed
#:msg #rx"given: .*(\"any\" . \"any\")")
(t-int/fail (-> pair-car-is-int pair-car-is-int)
(λ (c) (c (cons "any" "any")))
(λ (_) (cons "any" "any"))
#:untyped
#:msg #rx"produced: .*(\"any\" . \"any\")")
;; check range is not checked
(t-int (-> pair-car-is-int pair-car-is-int)
(λ (c) (c (cons 42 "any")))
(λ (_) (cons "any" "any"))
#:typed))
(let ([pair-car-not-int (-refine/fresh p (-pair Univ Univ) (-not-type (-car-of (-id-path p)) -Int))])
(t pair-car-not-int)
(t-int (-> pair-car-not-int pair-car-not-int)
(λ (c) (c (cons "any" 42)))
(λ (_) (cons "any" 42))
#:typed)
(t-int/fail (-> pair-car-not-int pair-car-not-int)
(λ (c) (c (cons 42 "any")))
(λ (_) (cons "any" "any"))
#:typed
#:msg #rx"given: .*(42 . \"any\")")
(t-int/fail (-> pair-car-not-int pair-car-not-int)
(λ (c) (c (cons "any" "any")))
(λ (_) (cons 42 "any"))
#:untyped
#:msg #rx"produced: .*(42 . \"any\")")
;; check range is not checked
(t-int (-> pair-car-not-int pair-car-not-int)
(λ (c) (c (cons "any" "any")))
(λ (_) (cons 42 "any"))
#:typed))
(let ([int=42 (-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 42))
(-leq (-lexp 42) (-lexp x))))])
(t int=42)
(t-int (-> int=42 int=42)
(λ (c) (c 42))
(λ (_) 42)
#:typed)
(t-int/fail (-> int=42 int=42)
(λ (c) (c "foo"))
(λ (_) 42)
#:typed
#:msg #rx"expected: Integer.*given: .*\"foo\"")
(t-int/fail (-> int=42 int=42)
(λ (c) (c 41))
(λ (_) 42)
#:typed
#:msg #rx"expected: .*given: .*41")
(t-int/fail (-> int=42 int=42)
(λ (c) (c 43))
(λ (_) 42)
#:typed
#:msg #rx"expected: .*given: .*43")
;; range is skipped
(t-int (-> int=42 int=42)
(λ (c) (c 42))
(λ (_) 41)
#:typed))
(let ([int<=0or>=100 (-refine/fresh x -Int (-or (-leq (-lexp x) (-lexp 0))
(-leq (-lexp 100) (-lexp x))))])
(t int<=0or>=100)
(t-int (-> int<=0or>=100 int<=0or>=100)
(λ (c) (c -1))
(λ (_) -1)
#:typed)
(t-int (-> int<=0or>=100 int<=0or>=100)
(λ (c) (c 0))
(λ (_) 0)
#:typed)
(t-int (-> int<=0or>=100 int<=0or>=100)
(λ (c) (c 100))
(λ (_) 100)
#:typed)
(t-int (-> int<=0or>=100 int<=0or>=100)
(λ (c) (c 101))
(λ (_) 101)
#:typed)
(t-int/fail (-> int<=0or>=100 int<=0or>=100)
(λ (c) (c "foo"))
(λ (_) -1)
#:typed
#:msg #rx"expected: Integer.*given: .*\"foo\"")
(t-int/fail (-> int<=0or>=100 int<=0or>=100)
(λ (c) (c 42))
(λ (_) -1)
#:typed
#:msg #rx"expected: .*given: .*42")
;; range is skipped
(t-int (-> int<=0or>=100 int<=0or>=100)
(λ (c) (c 120))
(λ (_) 50)
#:typed))
(t/fail (-refine/fresh p (-pair Univ Univ) (-is-type (-car-of (-id-path p)) (-vec Univ)))
"proposition contract generation not supported for non-flat types")
(t/fail (-refine/fresh p (-pair Univ Univ) (-not-type (-car-of (-id-path p)) (-vec Univ)))
"proposition contract generation not supported for non-flat types")))

View File

@ -0,0 +1,284 @@
#lang racket/base
(require "test-utils.rkt"
rackunit racket/format
(rep prop-rep)
(types abbrev prop-ops)
(logic ineq)
(for-syntax racket/base syntax/parse))
(provide tests)
(gen-test-main)
;; binding these means props that mention #'x, #'y, and #'z
;; will be referring to identifiers w/ variable bindings
;; (and props about things w/o variable bindings are erased
;; since top level ids are mutable)
(define q 42)
(define r 42)
(define t 42)
(define x 42)
(define y 42)
(define z 42)
(define tests
(let ([q (-id-path #'q)]
[r (-id-path #'r)]
[t (-id-path #'t)]
[x (-id-path #'x)]
[y (-id-path #'y)]
[z (-id-path #'z)])
(test-suite
"LExps and Inequalities"
(test-suite
"LExp Basics"
;; some sanity checks on the construction of LExps
;; and basic properties about them
(check-equal? (-lexp (list 1 x))
(-lexp x))
(check-equal? (-lexp (list 1 x))
(-lexp 0 x))
(check-equal? (-lexp 0
(list 1 x)
(list 1 x))
(-lexp 0 x x))
(check-equal? (-lexp 0
(list 1 x)
(list 1 x))
(-lexp (list 2 x)))
(check-equal? (constant-LExp? (-lexp 0
(list 1 x)
(list 1 x)))
#f)
(check-equal? (constant-LExp? (-lexp 0
(list 1 x)
(list -1 x)))
0)
(check-equal? (constant-LExp? (-lexp 42))
42)
(check-equal? (constant-LExp? (-lexp -42))
-42))
(test-suite
"Leq Constructor Simplifications"
;; do obviously valid leqs get erased? do
;; others get turned into actual LeqProps, etc
(check-equal? (-leq (-lexp 1) (-lexp 2)) -tt)
(check-equal? (-leq (-lexp 2) (-lexp 1)) -ff)
(check-equal? (-leq x
x)
-tt)
(check-true (LeqProp? (-leq x
(-id-path #'y))))
(check-true (LeqProp? (-leq (-lexp (list 2 x))
x)))
(check-true (LeqProp? (-leq (-lexp 42 x)
x)))
(check-true (LeqProp? (-leq x
(-lexp (list 2 x)))))
(check-true (LeqProp? (-leq x
(-lexp 42 x))))
(check-true (LeqProp? (-leq (-lexp (list 2 x))
x)))
(check-true (LeqProp? (negate-prop
(-leq (-lexp (list 2 x))
x))))
(check-equal? (negate-prop
(-leq (-lexp (list 2 x))
x))
(-leq (-lexp 1 x)
(-lexp (list 2 x)))))
(test-suite
"Simple Satisfiability"
(check-true (satisfiable-Leqs?
(list (-leq (-lexp (list 2 x))
x))))
(check-false (satisfiable-Leqs?
(list (-leq (-lexp (list 2 x)) x)
(negate-prop
(-leq (-lexp (list 2 x)) x)))))
(check-false (satisfiable-Leqs?
(list (-leq (-lexp 0) (-lexp (list 1 y)))
(negate-prop (-leq (-lexp 0) (-lexp (list 1 y)))))))
)
(test-suite
"Leq binary relations"
;; contradictory-Leqs?
(check-false (contradictory-Leqs?
(-leq (-lexp (list 2 x)) x)
(-leq (-lexp (list 2 x)) x)))
(check-false (contradictory-Leqs?
(-leq (-lexp (list 2 x)) x)
(-leq (-lexp (list 2 y)) x)))
(check-false (contradictory-Leqs?
(-leq (-lexp (list 2 x)) x)
(-leq x (-lexp (list 2 x)))))
(check-true (contradictory-Leqs?
(-leq (-lexp (list 2 x)) x)
(negate-prop
(-leq (-lexp (list 2 x)) x))))
(check-false (contradictory-Leqs?
(-leq (-lexp (list 2 x)) x)
(negate-prop
(-leq (-lexp (list 2 y)) y))))
;; complementary-Leqs?
(check-false (complementary-Leqs?
(-leq (-lexp (list 2 x)) x)
(-leq (-lexp (list 2 x)) x)))
(check-true (complementary-Leqs?
(-leq (-lexp (list 2 x)) x)
(-leq x (-lexp (list 2 x)))))
(check-true (complementary-Leqs?
(-leq (-lexp (list 2 x)) x)
(negate-prop (-leq (-lexp (list 2 x)) x))))
(check-false (complementary-Leqs?
(-leq (-lexp (list 2 x)) x)
(negate-prop (-leq (-lexp (list 2 y)) y))))
)
(test-suite
"Leq implication"
;; x + y <= z; 0 <= y; 0 <= x --> x <= z /\ y <= z
(check-true
(Leqs-imply-Leqs?
(list (-leq (-lexp (list 1 x) (list 1 y))
(-lexp (list 1 z)))
(-leq (-lexp 0)
(-lexp (list 1 y)))
(-leq (-lexp 0)
(-lexp (list 1 x))))
(list (-leq (-lexp (list 1 x))
(-lexp (list 1 z)))
(-leq (-lexp (list 1 y))
(-lexp (list 1 z))))))
;; x + y <= z; 0 <= y; 0 <= x -/-> x <= z /\ y <= q
(check-false
(Leqs-imply-Leqs?
(list (-leq (-lexp (list 1 x) (list 1 y))
(-lexp (list 1 z)))
(-leq (-lexp 0)
(-lexp (list 1 y)))
(-leq (-lexp 0)
(-lexp (list 1 x))))
(list (-leq (-lexp (list 1 x))
(-lexp (list 1 z)))
(-leq (-lexp (list 1 y))
(-lexp (list 1 q))))))
;; 7x <= 29 --> x <= 4
(check-true
(Leqs-imply-Leqs?
(list (-leq (-lexp (list 7 x))
(-lexp 29)))
(list (-leq (-lexp (list 1 x))
(-lexp 4)))))
;; 7x <= 28 --> x <= 4
(check-true
(Leqs-imply-Leqs?
(list (-leq (-lexp (list 7 x))
(-lexp 28)))
(list (-leq (-lexp (list 1 x))
(-lexp 4)))))
;; 7x <= 28 does not --> x <= 3
(check-false
(Leqs-imply-Leqs?
(list (-leq (-lexp (list 7 x))
(-lexp 28)))
(list (-leq (-lexp (list 1 x))
(-lexp 3)))))
;; 7x <= 27 --> x <= 3
(check-true
(Leqs-imply-Leqs?
(list (-leq (-lexp (list 7 x))
(-lexp 27)))
(list (-leq (-lexp (list 1 x))
(-lexp 3)))))
;; 4x+3y+9z+20q-100r + 42 <= 4x+3y+9z+20q+100r;
;; x <= y + z;
;; 29r <= x + y + z + q;
;; 0 <= x;
;; 0 <= x + y + z;
;; 0 <= x + z;
;; x <= z
;; z + 1 <= t
;; 0 <= x + y;
;; 0 <= x + r;
;; 0 <= x + r + q;
;; -->
;; 0 <= t
(check-true
(Leqs-imply-Leqs?
(list (-leq (-lexp (list 4 x) (list 3 y) (list 9 z) (list 20 q) (list -100 r) 42)
(-lexp (list 4 x) (list 3 y) (list 9 z) (list 20 q) (list 100 r)))
(-leq (-lexp (list 1 x))
(-lexp (list 1 y) (list 1 z)))
(-leq (-lexp (list 29 r))
(-lexp (list 1 x) (list 1 y) (list 1 z) (list 1 q)))
(-leq (-lexp 0)
(-lexp (list 1 x)))
(-leq (-lexp 0)
(-lexp (list 1 x) (list 1 y) (list 1 z)))
(-leq (-lexp 0)
(-lexp (list 1 x) (list 1 z)))
(-leq (-lexp (list 1 x))
(-lexp (list 1 z)))
(-leq (-lexp (list 1 z) 1)
(-lexp (list 1 t)))
(-leq (-lexp 0)
(-lexp (list 1 x) (list 1 y)))
(-leq (-lexp 0)
(-lexp (list 1 x) (list 1 r)))
(-leq (-lexp 0)
(-lexp (list 1 x) (list 1 r) (list 1 q))))
(list (-leq (-lexp 0)
(-lexp (list 1 t))))))
;; 4x+3y+9z+20q-100r + 42 <= 4x+3y+9z+20q+100r;
;; x <= y + z;
;; 29r <= x + y + z + q;
;; 0 <= x;
;; 0 <= x + y + z;
;; 0 <= x + z;
;; x <= z
;; z + 1 <= t
;; 0 <= x + y;
;; 0 <= x + r;
;; 0 <= x + r + q;
;; -/->
;; t <= 0
(check-false
(Leqs-imply-Leqs?
(list (-leq (-lexp (list 4 x) (list 3 y) (list 9 z) (list 20 q) (list -100 r) 42)
(-lexp (list 4 x) (list 3 y) (list 9 z) (list 20 q) (list 100 r)))
(-leq (-lexp (list 1 x))
(-lexp (list 1 y) (list 1 z)))
(-leq (-lexp (list 29 r))
(-lexp (list 1 x) (list 1 y) (list 1 z) (list 1 q)))
(-leq (-lexp 0)
(-lexp (list 1 x)))
(-leq (-lexp 0)
(-lexp (list 1 x) (list 1 y) (list 1 z)))
(-leq (-lexp 0)
(-lexp (list 1 x) (list 1 z)))
(-leq (-lexp (list 1 x))
(-lexp (list 1 z)))
(-leq (-lexp (list 1 z) 1)
(-lexp (list 1 t)))
(-leq (-lexp 0)
(-lexp (list 1 x) (list 1 y)))
(-leq (-lexp 0)
(-lexp (list 1 x) (list 1 r)))
(-leq (-lexp 0)
(-lexp (list 1 x) (list 1 r) (list 1 q))))
(list (-leq (-lexp (list 1 t))
(-lexp 0))))))
))
)

View File

@ -23,6 +23,11 @@
#t))
#,(syntax/loc stx (check-equal? success box-v))))]))
;; we create some bindings so that syntax for the unit tests
;; refers to identifiers that produce #t for identifier-binding
(define x 42)
(define y 42)
(define z 42)
(define tests
(test-suite "Metafunctions"
@ -37,11 +42,37 @@
#t)
(test-combine-props
(list (-or (-is-type #'x -String) (-is-type #'y -String)))
(list (-is-type #'x (Un -String -Symbol)) (-is-type #'y (Un -String -Symbol)))
(list (-or (-is-type #'y -String) (-is-type #'x -String))
(-is-type #'y (Un -String -Symbol)) (-is-type #'x (Un -String -Symbol)))
#t)
(list (-or (-is-type #'x -String) (-is-type #'y -String)))
(list (-is-type #'x (Un -String -Symbol)) (-is-type #'y (Un -String -Symbol)))
(list (-or (-is-type #'y -String) (-is-type #'x -String))
(-is-type #'y (Un -String -Symbol)) (-is-type #'x (Un -String -Symbol)))
#t)
(test-combine-props
(list (-is-type (-car-of (-id-path #'y)) -Int))
(list (-or (-is-type #'x (-pair -Int -Int))
(-is-type #'y (-pair -String -String))))
(list (-is-type #'x (-pair -Int -Int))
(-is-type (-car-of (-id-path #'y)) -Int))
#t)
(test-combine-props
(list (-is-type (-car-of (-id-path #'y)) -Int)
(-is-type (-car-of (-id-path #'x)) -String))
(list (-or (-is-type #'x (-pair -Int -Int))
(-is-type #'y (-pair -String -String))))
#f
#t)
(test-combine-props
(list (-leq (-lexp 1 (-id-path #'x))
(-lexp (-id-path #'y)))
(-is-type (-car-of (-id-path #'x)) -String))
(list (-or (-is-type #'x (-pair -Int -Int))
(-leq (-lexp 1 (-id-path #'y))
(-lexp (-id-path #'x)))))
#f
#t)
)
(test-suite "merge-tc-results"
@ -171,5 +202,22 @@
(replace-names (list #'x) (list (make-Path null '(0 . 0)))
(ret (-> Univ Univ : -tt-propset : (make-Path null #'x))))
(ret (-> Univ Univ : -tt-propset : (make-Path null '(1 . 0)))))
(check-equal?
(replace-names (list #'x) (list (make-Path null '(0 . 0)))
(ret (-refine y -Int (-leq (-lexp y) (-lexp #'x)))
-tt-propset
(make-Path null #'x)))
(ret (-refine y -Int (-leq (-lexp y) (-lexp (make-Path null '(1 . 0)))))
-tt-propset
(make-Path null '(0 . 0))))
(check-equal?
(replace-names (list #'x) (list -empty-obj)
(ret (-refine y -Int (-leq (-lexp y) (-lexp #'x)))
-tt-propset
(make-Path null #'x)))
(ret -Int
-tt-propset
-empty-obj))
)
))

View File

@ -13,7 +13,7 @@
(rep type-rep values-rep)
(submod typed-racket/base-env/base-types initialize)
(rename-in (types abbrev numeric-tower resolve)
(rename-in (types abbrev numeric-tower resolve prop-ops)
[Un t:Un] [-> t:->] [->* t:->*]))
(only-in typed-racket/typed-racket do-standard-inits)
(base-env base-types base-types-extra colon)
@ -32,6 +32,10 @@
(define mutated-var #f)
(define not-mutated-var #f)
(define x #'x)
(define y #'y)
(define z #'z)
(begin-for-syntax
(do-standard-inits)
(register-mutated-var #'mutated-var))
@ -416,6 +420,128 @@
[( (-> Number Number) (-> String String))
(-unsafe-intersect (t:-> -String -String)
(t:-> -Number -Number))]
;; refinements
;; top/bot
[(Refine [x : Number] Top) -Number]
[(Refine [x : Number] Bot) -Bottom]
;; simplify props about subject
[(Refine [x : Any] (: x String)) -String]
[(Refine [x : Integer] (: x Integer)) -Int]
[(Refine [x : Integer] (: x Symbol)) -Bottom]
;; refinements w/ inequalities
[(Refine [val : Integer] (<= val 42))
(-refine/fresh x -Int (-leq (-lexp x)
(-lexp 42)))]
[(Refine [vec : (Vectorof Any)] (<= (vector-length vec) 42))
(-refine/fresh x (-vec Univ) (-leq (-lexp (-vec-len-of (-id-path x)))
(-lexp 42)))]
[(Refine [p : (Pairof Integer Integer)] (<= (car p) (cdr p)))
(-refine/fresh p (-pair -Int -Int) (-leq (-lexp (-car-of (-id-path p)))
(-lexp (-cdr-of (-id-path p)))))]
[(Refine [x : Integer] (<= (* 2 x) 42))
(-refine/fresh x -Int (-leq (-lexp (list 2 x))
(-lexp 42)))]
[(Refine [x : Integer] (<= (+ 1 x) 42))
(-refine/fresh x -Int (-leq (-lexp 1 x)
(-lexp 42)))]
[(Refine [x : Integer] (<= (+ 1 (* 3 x)) 42))
(-refine/fresh x -Int (-leq (-lexp 1 (list 3 x))
(-lexp 42)))]
[(Refine [x : Integer] (<= (+ 1 (* 3 x) (* 2 x)) 42))
(-refine/fresh x -Int (-leq (-lexp 1 (list 5 x))
(-lexp 42)))]
[(Refine [x : Integer] (<= 42 (+ 1 (* 3 x) (* 2 x))))
(-refine/fresh x -Int (-leq (-lexp 42)
(-lexp 1 (list 5 x))))]
[(Refine [x : Integer] (<= 42 (* 2 x)))
(-refine/fresh x -Int (-leq (-lexp 42)
(-lexp (list 2 x))))]
[(Refine [x : Integer] (<= 42 (+ 1 x)))
(-refine/fresh x -Int (-leq (-lexp 42)
(-lexp 1 x)))]
[(Refine [x : Integer] (<= x 42))
(-refine/fresh x -Int (-leq (-lexp x)
(-lexp 42)))]
[(Refine [x : Integer] (< x 42))
(-refine/fresh x -Int (-leq (-lexp 1 (list 1 x))
(-lexp 42)))]
[(Refine [x : Integer] (>= x 42))
(-refine/fresh x -Int (-leq (-lexp 42)
(-lexp x)))]
[(Refine [x : Integer] (>= x 42))
(-refine/fresh x -Int (-leq (-lexp 42)
(-lexp x)))]
[(Refine [x : Integer] (> x 42))
(-refine/fresh x -Int (-leq (-lexp 43)
(-lexp x)))]
;; refinements w/ equality
[(Refine [x : Integer] (= x 42))
(-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 42))
(-leq (-lexp 42) (-lexp x))))]
;; other abritrary propositions in refinements
[(Refine [x : Integer] (and (<= x 42)
(<= 0 x)))
(-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 42))
(-leq (-lexp 0) (-lexp x))))]
[(Refine [x : String] (and (: z Symbol)
(! y String)))
(-refine/fresh x -String (-and (-is-type #'z -Symbol)
(-not-type #'y -String)))]
[(Refine [x : String] (or (: z Symbol)
(: y String)))
(-refine/fresh x -String (-or (-is-type #'z -Symbol)
(-is-type #'y -String)))]
[(Refine [x : String] (unless (: z Symbol)
(: y String)))
(-refine/fresh x -String (-or (-is-type #'z -Symbol)
(-is-type #'y -String)))]
[(Refine [x : String] (or (not (: y String))
(: z Symbol)))
(-refine/fresh x -String (-or (-not-type #'y -String)
(-is-type #'z -Symbol)))]
[(Refine [x : Any] (if (: x String) (! y String) (: z Symbol)))
(-refine/fresh x Univ (-or (-and (-is-type x -String) (-not-type #'y -String))
(-and (-not-type x -String) (-is-type #'z -Symbol))))]
[(Refine [x : String] (when (: z Symbol) (: y String)))
(-refine/fresh x -String (-or (-not-type #'z -Symbol)
(-is-type #'y -String)))]
[(Refine [x : String] (when (not (not (: z Symbol)))
(: y String)))
(-refine/fresh x -String (-or (-not-type #'z -Symbol)
(-is-type #'y -String)))]
[(Refine [x : (Refine [x : Integer] (<= 42 x))] (<= x 42))
(-refine/fresh z -Int (-and (-leq (-lexp 42) (-lexp z))
(-leq (-lexp z) (-lexp 42))))]
;; fail for unbound identifiers
[FAIL (Refine [x : String] (: r Symbol))]
[FAIL (Refine [x String] (: x Symbol))]
[FAIL (Refine [x y : String] (: x Symbol))]
[FAIL (Refine [x : String] (: r Symbol) (: r Symbol))]
;; fail for bad path element usage
[FAIL (Refine [p : Integer] (<= (car p) 42))]
[FAIL (Refine [p : Integer] (<= (cdr p) 42))]
[FAIL (Refine [p : (Pairof Integer Integer)] (<= (car (car p)) 42))]
[FAIL (Refine [p : (Pairof Integer Integer)] (<= (car (cdr p)) 42))]
[FAIL (Refine [p : (Pairof Integer Integer)] (<= (cdr (car p)) 42))]
[FAIL (Refine [p : (Pairof Integer Integer)] (<= (cdr (cdr p)) 42))]
[FAIL (Refine [vec : Any] (<= (vector-length vec) 42))]
;; fail for bad linear expression (i.e. not an integer)
[FAIL (Refine [q : Any] (<= q 42))]
[FAIL (Refine [q : Any] (<= 42 q))]
[FAIL (Refine [q : Any] (< q 42))]
[FAIL (Refine [q : Any] (< 42 q))]
[FAIL (Refine [q : Any] (>= 42 q))]
[FAIL (Refine [q : Any] (>= q 42))]
[FAIL (Refine [q : Any] (> q 42))]
[FAIL (Refine [q : Any] (> 42 q))]
[FAIL (Refine [q : Any] (= 42 q))]
[FAIL (Refine [q : Any] (= q 42))]
[FAIL (Refine [q : Any] (<= (+ 1 q) 42))]
[FAIL (Refine [q : Any] (<= 42 (+ 1 q)))]
[FAIL (Refine [q : Any] (<= (* 2 q) 42))]
[FAIL (Refine [q : Any] (<= 42 (* 2 q)))]
[FAIL (Refine [q : Any] (<= (+ 1 (* 2 q)) 42))]
[FAIL (Refine [q : Any] (<= 42 (+ 1 (* 2 q))))]
))
;; FIXME - add tests for parse-values-type, parse-tc-results

View File

@ -9,7 +9,37 @@
(provide tests)
(gen-test-main)
(define (not-implies-atomic? y x) (not (implies-atomic? y x)))
(define (not-atomic-implies? y x) (not (atomic-implies? y x)))
(define (not-implies? y x) (not (implies? y x)))
;; binding these means props that mention #'x, #'y, and #'z
;; will be referring to identifiers w/ variable bindings
;; (and props about things w/o variable bindings are erased
;; since top level ids are mutable)
(define x 42)
(define y 42)
(define z 42)
(define-syntax (implies-atomic-tests stx)
(define-syntax-class imp-test
(pattern (~and tst [#:not a:expr c:expr])
#:with check #`(test-case
(~a '(not (implies-atomic? a c)))
#,(syntax/loc #'tst (check-false (atomic-implies? a c)))
#,(syntax/loc #'tst (check-false (implies? a c)))))
(pattern (~and tst [a:expr c:expr])
#:with check #`(test-case
(~a '(implies-atomic? a c))
#,(syntax/loc #'tst (check-true (atomic-implies? a c)))
#,(syntax/loc #'tst (check-true (implies? a c))))))
(syntax-parse stx
[(_ tst:imp-test ...)
#'(test-suite
"Implies Atomic"
tst.check ...)]))
(define-syntax (test-opposite stx)
(define-syntax-class complementary
@ -20,12 +50,15 @@
(pattern #:not-contradictory #:with check #'check-false))
(syntax-parse stx
[(_ comp:complementary contr:contradictory p1* p2*)
(syntax/loc stx
(test-case (~a '(opposite p1* p2*))
(define p1 p1*)
(define p2 p2*)
(comp.check (complementary? p1 p2) "Complementary")
(contr.check (contradictory? p1 p2) "Contradictory")))]))
#`(test-case
(~a '(opposite p1* p2*))
(define p1 p1*)
(define p2 p2*)
#,(syntax/loc stx (comp.check (atomic-complement? p1 p2) "Complementary"))
#,(syntax/loc stx (contr.check (atomic-contradiction? p1 p2) "Contradictory"))
;; 'contradiction' should be strictly stronger than 'atomic-contradiction'
;; and so we'll test both here
#,(syntax/loc stx (contr.check (contradiction? p1 p2) "Contradictory")))]))
(define tests
@ -67,49 +100,87 @@
-tt
-tt)
(test-opposite #:not-complementary #:not-contradictory
(-leq (-lexp (list 2 (-id-path #'x))) (-id-path #'x))
(-leq (-lexp (list 2 (-id-path #'x))) (-id-path #'x)))
(test-opposite #:complementary #:not-contradictory
(-leq (-lexp (list 2 (-id-path #'x))) (-id-path #'x))
(-leq (-id-path #'x) (-lexp (list 2 (-id-path #'x)))))
(test-opposite #:not-complementary #:contradictory
(-leq (-id-path #'x) (-lexp 42))
(-leq (-lexp 100) (-id-path #'x)))
(test-opposite #:complementary #:contradictory
(-leq (-lexp (list 2 (-id-path #'x))) (-id-path #'x))
(negate-prop (-leq (-lexp (list 2 (-id-path #'x))) (-id-path #'x))))
)
(test-suite "Implies Atomic"
(check implies-atomic?
-tt -tt)
(check implies-atomic?
-ff -ff)
(check implies-atomic?
-ff -tt)
(check not-implies-atomic?
-tt -ff)
(check implies-atomic?
(-is-type 0 -Symbol) -tt)
(check implies-atomic?
-ff (-is-type 0 -Symbol))
(check implies-atomic?
(-is-type 0 -Symbol)
(-is-type 0 (Un -String -Symbol)))
(check not-implies-atomic?
(-is-type 0 (Un -String -Symbol))
(-is-type 0 -Symbol))
(check implies-atomic?
(-not-type 0 (Un -String -Symbol))
(-not-type 0 -Symbol))
(check not-implies-atomic?
(-not-type 0 -Symbol)
(-not-type 0 (Un -String -Symbol)))
(check not-implies-atomic?
(-is-type 0 -Symbol)
(-is-type 1 -Symbol))
(check implies-atomic?
(-is-type #'x -Symbol)
(-is-type #'x -Symbol))
(check implies-atomic?
(-is-type #'x -Symbol)
(-or (-is-type 1 -Symbol) (-is-type #'x -Symbol)))
(check implies-atomic?
(-and (-is-type 1 -Symbol) (-is-type #'x -Symbol))
(-is-type #'x -Symbol))
(check implies-atomic?
(-is-type #'x -Symbol)
(-not-type #'x (-val #f)))
)
(test-suite
"Contradiction"
(check contradiction?
(-is-type #'x (-pair -String -String))
(-is-type (-car-of (-id-path #'x)) -Symbol))
(check contradiction?
(-is-type (-car-of (-id-path #'x)) (-pair -String -String))
(-is-type (-cdr-of (-car-of (-id-path #'x))) -Symbol))
(check contradiction?
(-is-type (-car-of (-id-path #'x)) -Symbol)
(-is-type #'x (-pair -String -String)))
(check contradiction?
(-is-type (-cdr-of (-car-of (-id-path #'x))) -Symbol)
(-is-type (-car-of (-id-path #'x)) (-pair -String -String)))
(check contradiction?
(-not-type (-car-of (-id-path #'x)) -String)
(-is-type #'x (-pair -String -String)))
(check contradiction?
(-is-type #'x (-pair -String -String))
(-not-type (-car-of (-id-path #'x)) -String))
(check contradiction?
(-not-type (-car-of (-cdr-of (-id-path #'x))) -String)
(-is-type (-cdr-of (-id-path #'x)) (-pair -String -String)))
(check contradiction?
(-is-type (-cdr-of (-id-path #'x)) (-pair -String -String))
(-not-type (-car-of (-cdr-of (-id-path #'x))) -String))
(check contradiction?
(-leq (-id-path #'x) (-lexp 0))
(-leq (-lexp 1) (-id-path #'x))))
(implies-atomic-tests
[-tt -tt]
[-ff -ff]
[#:not -tt -ff]
[(-is-type 0 -Symbol) -tt]
[-ff (-is-type 0 -Symbol)]
[(-is-type 0 -Symbol)
(-is-type 0 (Un -String -Symbol))]
[#:not
(-is-type 0 (Un -String -Symbol))
(-is-type 0 -Symbol)]
[(-not-type 0 (Un -String -Symbol))
(-not-type 0 -Symbol)]
[#:not
(-not-type 0 -Symbol)
(-not-type 0 (Un -String -Symbol))]
[#:not
(-is-type 0 -Symbol)
(-is-type 1 -Symbol)]
[(-is-type #'x -Symbol)
(-is-type #'x -Symbol)]
[(-is-type #'x -Symbol)
(-or (-is-type 1 -Symbol) (-is-type #'x -Symbol))]
[(-and (-is-type 1 -Symbol) (-is-type #'x -Symbol))
(-is-type #'x -Symbol)]
[(-is-type #'x -Symbol)
(-not-type #'x (-val #f))]
[(-leq (-id-path #'x) (-lexp 42))
(-leq (-id-path #'x) (-lexp 50))]
[#:not
(-leq (-id-path #'x) (-lexp 50))
(-leq (-id-path #'x) (-lexp 42))])
(test-suite "Simplification"
(check-equal?
@ -129,6 +200,20 @@
(-and (-not-type #'y (-val #f))
(-or (-not-type #'y (-val #f))
(-not-type #'x (-val #f))))
(-not-type #'y (-val #f))))
(-not-type #'y (-val #f)))
(check-equal?
(-or (-not-type #'y (-val #f))
(-leq (-id-path #'x) (-lexp 42))
(-leq (-id-path #'x) (-lexp 50)))
(-or (-not-type #'y (-val #f))
(-leq (-id-path #'x) (-lexp 50))))
(check-equal?
(-and (-is-type (-id-path #'z) (-val #f))
(-or (-not-type #'y (-val #f))
(-leq (-lexp 50) (-id-path #'x))
(-leq (-id-path #'x) (-lexp 50))))
(-is-type (-id-path #'z) (-val #f))))
))

View File

@ -24,7 +24,7 @@
result))
(define tests
(test-suite "Tests for substitution"
(test-suite "Tests for type substitution"
(s -Number a (-v a) -Number)
(s -Number a (-pair (-v a) -String) (-pair -Number -String))
(s -Number a (-pair -String (-v a)) (-pair -String -Number))

View File

@ -1,9 +1,9 @@
#lang racket/base
(require "test-utils.rkt"
(types subtype numeric-tower utils abbrev)
(types subtype numeric-tower utils abbrev prop-ops)
(rep type-rep values-rep)
(env init-envs type-env-structs)
(env lexical-env init-envs type-env-structs)
rackunit
(for-syntax racket/base))
@ -11,8 +11,14 @@
(gen-test-main)
(define-for-syntax (single-subtype-test stx)
(syntax-case stx (FAIL)
[(FAIL t s) (syntax/loc stx (test-check (format "FAIL ~a" '(t s)) (lambda (a b) (not (subtype a b))) t s))]
(syntax-case stx (FAIL ENV ENV/FAIL)
[(FAIL t s) (syntax/loc stx (test-check (format "FAIL ~a" '(t s))
(λ (a b) (not (subtype a b))) t s))]
[(ENV ps t s) (syntax/loc stx (with-naively-extended-lexical-env [#:props ps]
(test-check (format "ENV ~a" '(ps t s)) subtype t s)))]
[(ENV/FAIL ps t s) (syntax/loc stx (with-naively-extended-lexical-env [#:props ps]
(test-check (format "ENV/FAIL ~a" '(ps t s))
(λ (a b) (not (subtype a b))) t s)))]
[(t s) (syntax/loc stx (test-check (format "~a" '(t s)) subtype t s))]))
(define-syntax (subtyping-tests stx)
@ -25,6 +31,9 @@
(define x1 #'x)
(define x2 #'x)
(define x #'x)
(define y #'y)
(define z #'z)
(define A (make-F (gensym 'A)))
(define B (make-F (gensym 'B)))
(define AorB (Un A B))
@ -584,6 +593,114 @@
))
(define refinement-tests
(subtyping-tests
"Refinement Subtyping"
;; weakening
[(-refine/fresh x -Int (-leq (-lexp x) (-lexp 42)))
-Int]
;; τ not a subtype of refined τ
[FAIL -Int
(-refine/fresh x -Int (-leq (-lexp x) (-lexp 42)))]
;; prop implies w/ leqs
[(-refine/fresh x -Int (-leq (-lexp x) (-lexp 99)))
(-refine/fresh x -Int (-leq (-lexp x) (-lexp 100)))]
;; prop doesn't imply
[FAIL
(-refine/fresh x -Int (-leq (-lexp x) (-lexp 99)))
(-refine/fresh x -Nat (-leq (-lexp x) (-lexp 100)))]
[FAIL
(-refine/fresh x -Int (-is-type y -String))
(-refine/fresh x -Nat (-is-type y -String))]
;; logical implication w/ types
[(-refine/fresh x -Int (-is-type y -Int))
(-refine/fresh x -Int (-is-type y -Number))]
[(-refine/fresh x -Int (-and (-is-type y -Nat)
(-is-type z -Nat)))
(-refine/fresh x -Int (-or (-is-type y -Int)
(-is-type z -Int)))]
[(-refine/fresh x -Int (-or (-is-type y -Nat)
(-is-type z -Nat)))
(-refine/fresh x -Int (-or (-is-type y -Int)
(-is-type z -Int)))]
[FAIL
(-refine/fresh x -Int (-or (-is-type y -Nat)
(-is-type z -String)))
(-refine/fresh x -Int (-or (-is-type y -Int)
(-is-type z -Int)))]
[(-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 99))
(-leq (-lexp 1) (-lexp x))))
(-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 100))
(-leq (-lexp 0) (-lexp x))))]
[FAIL
(-refine/fresh x -Int (-or (-leq (-lexp x) (-lexp 99))
(-leq (-lexp 1) (-lexp x))))
(-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 100))
(-leq (-lexp 0) (-lexp x))))]
;; refinements in unions
[(Un -String (-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 99))
(-leq (-lexp 1) (-lexp x)))))
(Un -String (-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 100))
(-leq (-lexp 0) (-lexp x)))))]
[(Un (-refine/fresh x -String (-and (-is-type y -Nat)
(-is-type z -Nat)))
(-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 99))
(-leq (-lexp 1) (-lexp x)))))
(Un (-refine/fresh x -String (-or (-is-type y -Int)
(-is-type z -Int)))
(-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 100))
(-leq (-lexp 0) (-lexp x)))))]
[FAIL
(Un (-refine/fresh x -String (-or (-is-type y -Int)
(-is-type z -Int)))
(-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 99))
(-leq (-lexp 1) (-lexp x)))))
(Un (-refine/fresh x -String (-and (-is-type y -Nat)
(-is-type z -Nat)))
(-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 100))
(-leq (-lexp 0) (-lexp x)))))]
;; refinements with "structural" types
[(-pair -String (-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 99))
(-leq (-lexp 1) (-lexp x)))))
(-pair -String (-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 100))
(-leq (-lexp 0) (-lexp x)))))]
[(-pair (-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 99))
(-leq (-lexp 1) (-lexp x))))
-String)
(-pair (-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 100))
(-leq (-lexp 0) (-lexp x))))
-String)]
[(-refine/fresh x (-pair -Int -Int)
(-and (-leq (-lexp (-car-of (-id-path x))) (-lexp 99))
(-leq (-lexp 1) (-lexp (-car-of (-id-path x))))))
(-pair (-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 100))
(-leq (-lexp 0) (-lexp x))))
-Number)]
[(-refine/fresh x (-pair -Int -Int)
(-and (-leq (-lexp (-cdr-of (-id-path x))) (-lexp 99))
(-leq (-lexp 1) (-lexp (-cdr-of (-id-path x))))))
(-pair -Number
(-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 100))
(-leq (-lexp 0) (-lexp x)))))]
[FAIL
(-refine/fresh x -Int (-leq (-lexp x) (-lexp y)))
(-refine/fresh x -Int (-leq (-lexp x) (-lexp z)))]
;; some tests w/ environments
[ENV
(list (-leq (-lexp y) (-lexp z)))
(-refine/fresh x -Int (-leq (-lexp x) (-lexp y)))
(-refine/fresh x -Int (-leq (-lexp x) (-lexp z)))]
[ENV
(list (-not-type z -String))
(-refine/fresh x -Int (-or (-is-type y -Nat)
(-is-type z -String)))
(-refine/fresh x -Int (-or (-is-type y -Int)
(-is-type z -Int)))]
[ENV/FAIL
(list (-leq (-lexp z) (-lexp y)))
(-refine/fresh x -Int (-leq (-lexp x) (-lexp y)))
(-refine/fresh x -Int (-leq (-lexp x) (-lexp z)))]))
(define tests
(test-suite
@ -596,4 +713,5 @@
function-tests
oo-tests
values-tests
other-tests))
other-tests
refinement-tests))

View File

@ -11,7 +11,9 @@
(rep type-rep)
rackunit rackunit/text-ui)
(provide private typecheck (rename-out [infer r:infer]) utils env rep types base-env static-contracts
(provide private typecheck (rename-out [infer r:infer])
utils env rep types base-env static-contracts
logic
(all-defined-out))
(define (tc-result-equal/test? res1 res2)

View File

@ -4,11 +4,13 @@
(require "test-utils.rkt"
rackunit
racket/match
typed-racket/standard-inits
typed-racket/tc-setup
typed-racket/rep/type-rep
typed-racket/rep/values-rep
typed-racket/types/abbrev
typed-racket/types/prop-ops
typed-racket/types/numeric-tower
typed-racket/types/printer
typed-racket/utils/tc-utils
@ -17,8 +19,14 @@
(provide tests)
(gen-test-main)
(define (prints-as? thing str)
(string=? (format "~a" thing) str))
(define y #'y)
(define z #'z)
(define (prints-as? thing expected)
(cond
[(string? expected) (string=? (format "~a" thing) expected)]
[(procedure? expected) (expected (format "~a" thing))]
[else (error 'prints-as? "unsupported expected ~a" expected)]))
(define (pretty-prints-as? thing str)
(string=? (pretty-format-rep thing) str))
@ -50,11 +58,11 @@
;; next three cases for PR 14552
(check-prints-as? (-mu x (Un (-pair x x) -Null))
"(Rec x (U Null (Pairof x x)))")
"(Rec x (U (Pairof x x) Null))")
(check-prints-as? (-mu x (Un (-pair (-box x) x) -Null))
"(Rec x (U Null (Pairof (Boxof x) x)))")
"(Rec x (U (Pairof (Boxof x) x) Null))")
(check-prints-as? (-mu x (Un (-mpair x x) -Null))
"(Rec x (U Null (MPairof x x)))")
"(Rec x (U (MPairof x x) Null))")
(check-prints-as? -Custodian "Custodian")
(check-prints-as? (make-Opaque #'integer?) "(Opaque integer?)")
@ -119,10 +127,10 @@
" 'binary 'text)] Void)"))
(check-prints-as? (-> Univ (-AnyValues -tt)) "(-> Any AnyValues)")
(check-prints-as? (-> Univ (-AnyValues (-is-type '(0 . 0) -String)))
"(-> Any AnyValues : (String @ (0 0)))")
"(-> Any AnyValues : (: (0 0) String))")
(check-prints-as? (-AnyValues -tt) "AnyValues")
(check-prints-as? (-AnyValues (-is-type '(0 . 0) -String))
"(AnyValues : (String @ (0 0)))")
"(AnyValues : (: (0 0) String))")
(check-prints-as? (->opt Univ [] -Void) "(-> Any Void)")
(check-prints-as? (->opt [-String] -Void) "(->* () (String) Void)")
@ -171,7 +179,50 @@
"(Unit (import a^ b^) (export c^ d^) (init-depend b^) String)")
(check-prints-as? (make-Unit (list a^ b^) (list c^ d^) (list b^ a^) (-values (list -String)))
"(Unit (import a^ b^) (export c^ d^) (init-depend b^ a^) String)"))
(check-prints-as? -UnitTop "UnitTop"))
(check-prints-as? -UnitTop "UnitTop")
(check-prints-as? (-refine/fresh x -Int (-leq (-lexp x) (-lexp 42)))
(λ (str) (match (read (open-input-string str))
[`(Refine [,x : Integer] (<= ,x 42)) #t]
[_ #f])))
(check-prints-as? (-refine/fresh x (-pair -Int -Int) (-leq (-lexp (-car-of (-id-path x)))
(-lexp (-cdr-of (-id-path x)))))
(λ (str) (match (read (open-input-string str))
[`(Refine [,x : (Pairof Integer Integer)] (<= (car ,x) (cdr ,x))) #t]
[_ #f])))
(check-prints-as? (-refine/fresh x (-vec Univ) (-leq (-lexp (-vec-len-of (-id-path x)))
(-lexp 42)))
(λ (str) (match (read (open-input-string str))
[`(Refine [,x : (Vectorof Any)] (<= (vector-length ,x) 42)) #t]
[_ #f])))
(check-prints-as? (-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 42))
(-leq (-lexp 42) (-lexp x))
(-leq (-lexp 1 x) (-lexp #'y))))
(λ (str) (match (read (open-input-string str))
[`(Refine [,x : Integer] (and (= ,x 42) (< ,x y))) #t]
[`(Refine [,x : Integer] (and (= 42 ,x) (< ,x y))) #t]
[`(Refine [,x : Integer] (and (< ,x y) (= ,x 42))) #t]
[`(Refine [,x : Integer] (and (< ,x y) (= ,x 42))) #t]
[_ #f])))
(check-prints-as? (-refine/fresh x -Int (-and (-leq (-lexp x) (-lexp 42))
(-leq (-lexp 42) (-lexp x))))
(λ (str) (match (read (open-input-string str))
[`(Refine [,x : Integer] (= ,x 42)) #t]
[`(Refine [,x : Integer] (= 42 ,x)) #t]
[_ #f])))
(check-prints-as? (-refine/fresh x -Int (-is-type #'y -Int))
(λ (str) (match (read (open-input-string str))
[`(Refine [,x : Integer] (: y Integer)) #t]
[_ #f])))
(check-prints-as? (-refine/fresh x -Int (-not-type #'y -Int))
(λ (str) (match (read (open-input-string str))
[`(Refine [,x : Integer] (! y Integer)) #t]
[_ #f])))
(check-prints-as? (-refine/fresh x -Int (-or (-is-type #'y -Int)
(-is-type #'z -String)))
(λ (str) (match (read (open-input-string str))
[`(Refine [,x : Integer] (or (: y Integer) (: z String))) #t]
[`(Refine [,x : Integer] (or (: z String) (: y Integer))) #t]
[_ #f]))))
(test-suite
"Pretty printing tests"
(check-pretty-prints-as? (-val 3) "3")

View File

@ -3906,6 +3906,28 @@
(-seq Univ)]
[tc-e (ann (in-hash-pairs (hash)) (Sequenceof (Pairof Any Any)))
(-seq (-pair Univ Univ))]
;; integer literals w/ refinements
[tc-e (ann -1 (Refine [x : Integer] (= x -1)))
(-refine/fresh x -Int (-eq (-lexp x) (-lexp -1)))]
[tc-e (ann 0 (Refine [x : Zero] (= x 0)))
(-refine/fresh x -Zero (-eq (-lexp x) (-lexp 0)))]
[tc-e (ann 0 (Refine [x : Integer] (= x 0)))
(-refine/fresh x -Int (-eq (-lexp x) (-lexp 0)))]
[tc-e (ann 1 (Refine [x : One] (= x 1)))
(-refine/fresh x -One (-eq (-lexp x) (-lexp 1)))]
[tc-e (ann 1 (Refine [x : Integer] (= x 1)))
(-refine/fresh x -Int (-eq (-lexp x) (-lexp 1)))]
[tc-e (ann 2 (Refine [x : Byte] (= x 2)))
(-refine/fresh x -Byte (-eq (-lexp x) (-lexp 2)))]
[tc-e (ann 2 (Refine [x : Integer] (= x 2)))
(-refine/fresh x -Int (-eq (-lexp x) (-lexp 2)))]
[tc-e (ann 123456 (Refine [x : Index] (= x 123456)))
(-refine/fresh x -Index (-eq (-lexp x) (-lexp 123456)))]
[tc-e (ann 123456 (Refine [x : Fixnum] (= x 123456)))
(-refine/fresh x -Fixnum (-eq (-lexp x) (-lexp 123456)))]
[tc-e (ann 123456 (Refine [x : Integer] (= x 123456)))
(-refine/fresh x -Int (-eq (-lexp x) (-lexp 123456)))]
)
(test-suite