so close
original commit: d935b63290b1aae41b61c772f9a3a728350a1b11
This commit is contained in:
Sam Tobin-Hochstadt
parent
6ae59dc036
commit
1505c7c3de
|
|
@ -5,4 +5,7 @@
|
|||
|
||||
;(let ([tmp (number? x)]) (if tmp tmp (string? x)))
|
||||
|
||||
(if (let ([tmp (number? x)]) (if tmp tmp (string? x))) (f x) 0)
|
||||
(if (let ([tmp (number? x)])
|
||||
(if tmp tmp (string? x)))
|
||||
(f x)
|
||||
0)
|
||||
|
|
@ -65,8 +65,8 @@
|
|||
;; sets the flag box to #f if anything becomes (U)
|
||||
(d/c (env+ env fs flag)
|
||||
(env? (listof Filter/c) (box/c #t). -> . env?)
|
||||
(define-values (imps atoms) (combine-props fs (env-props env) flag))
|
||||
(for/fold ([Γ (replace-props env imps)]) ([f atoms])
|
||||
(define-values (props atoms) (combine-props fs (env-props env) flag))
|
||||
(for/fold ([Γ (replace-props env (append atoms props))]) ([f atoms])
|
||||
(match f
|
||||
[(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)]
|
||||
[(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x))
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
(require (rename-in "../utils/utils.ss" [private private-in]))
|
||||
(require syntax/kerncase mzlib/trace
|
||||
scheme/match (prefix-in - scheme/contract)
|
||||
"signatures.ss" "tc-envops.ss" "tc-metafunctions.ss"
|
||||
"signatures.ss" "tc-envops.ss" "tc-metafunctions.ss" "tc-subst.ss"
|
||||
(types utils convenience union subtype remove-intersect type-table)
|
||||
(private-in parse-type type-annotation)
|
||||
(rep type-rep)
|
||||
|
|
@ -12,7 +12,7 @@
|
|||
(except-in (utils tc-utils stxclass-util))
|
||||
(env lexical-env)
|
||||
(only-in (env type-environments) lookup current-tvars extend-env)
|
||||
racket/private/class-internal
|
||||
racket/private/class-internal unstable/debug
|
||||
(except-in syntax/parse id)
|
||||
(only-in srfi/1 split-at))
|
||||
|
||||
|
|
@ -158,65 +158,83 @@
|
|||
;; (Results Results -> Result)
|
||||
;; (Type Results -> Type)
|
||||
;; (Type Type -> Type))
|
||||
(define (check-below tr1 expected)
|
||||
(match* (tr1 expected)
|
||||
;; these two have to be first so that errors can be allowed in cases where multiple values are expected
|
||||
[((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:)))
|
||||
(ret ts2)]
|
||||
[((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
|
||||
expected]
|
||||
|
||||
[((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
|
||||
(unless (= (length ts) (length ts2))
|
||||
(tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts)))
|
||||
(unless (for/and ([t ts] [s ts2]) (subtype t s))
|
||||
(tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts)))
|
||||
(if (= (length ts) (length ts2))
|
||||
(ret ts2 fs os)
|
||||
(ret ts2))]
|
||||
[((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
|
||||
(cond
|
||||
[(not (subtype t1 t2))
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1)])
|
||||
expected]
|
||||
[((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
|
||||
(cond
|
||||
[(not (subtype t1 t2))
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1)]
|
||||
[(and (not (filter-equal? f1 f2))
|
||||
(object-equal? o1 o2))
|
||||
(tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
|
||||
[(not (and (equal? f1 f2) (equal? o1 o2)))
|
||||
(tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))])
|
||||
expected]
|
||||
[((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
|
||||
(unless (andmap subtype t1 t2)
|
||||
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
|
||||
expected]
|
||||
[((tc-results: t1 fs os) (tc-results: t2 fs os))
|
||||
(unless (= (length t1) (length t2))
|
||||
(tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1)))
|
||||
(unless (for/and ([t t1] [s t2]) (subtype t s))
|
||||
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
|
||||
expected]
|
||||
[((tc-result1: t1 f o) (? Type? t2))
|
||||
(unless (subtype t1 t2)
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
|
||||
(ret t2 f o)]
|
||||
[((? Type? t1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:)))
|
||||
(unless (subtype t1 t2)
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
|
||||
t1]
|
||||
[((? Type? t1) (tc-result1: t2 f o))
|
||||
(if (subtype t1 t2)
|
||||
(tc-error/expr "Expected result with filter ~a and ~a, got ~a" f (print-object o) t1)
|
||||
(define (check-below tr1 expected)
|
||||
(define (maybe-abstract r)
|
||||
(define l (hash-ref to-be-abstr expected #f))
|
||||
(define (sub-one proc i)
|
||||
(for/fold ([s i])
|
||||
([nm (in-list l)])
|
||||
(proc s nm (make-Empty) #t)))
|
||||
(define (subber proc lst)
|
||||
(for/list ([i (in-list lst)])
|
||||
(sub-one proc i)))
|
||||
(if l
|
||||
(match r
|
||||
[(tc-results: ts fs os)
|
||||
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
|
||||
[(tc-results: ts fs os dt db)
|
||||
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)]
|
||||
[t (sub-one subst-type t)])
|
||||
r))
|
||||
(let ([tr1 (debug maybe-abstract tr1)])
|
||||
(match* (tr1 expected)
|
||||
;; these two have to be first so that errors can be allowed in cases where multiple values are expected
|
||||
[((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:)))
|
||||
(ret ts2)]
|
||||
[((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
|
||||
expected]
|
||||
|
||||
[((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
|
||||
(unless (= (length ts) (length ts2))
|
||||
(tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts)))
|
||||
(unless (for/and ([t ts] [s ts2]) (subtype t s))
|
||||
(tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts)))
|
||||
(if (= (length ts) (length ts2))
|
||||
(ret ts2 fs os)
|
||||
(ret ts2))]
|
||||
[((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
|
||||
(cond
|
||||
[(not (subtype t1 t2))
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1)])
|
||||
expected]
|
||||
[((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
|
||||
(cond
|
||||
[(not (subtype t1 t2))
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1)]
|
||||
[(and (not (filter-equal? f1 f2))
|
||||
(object-equal? o1 o2))
|
||||
(tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
|
||||
[(not (and (equal? f1 f2) (equal? o1 o2)))
|
||||
(tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))])
|
||||
expected]
|
||||
[((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
|
||||
(unless (andmap subtype t1 t2)
|
||||
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
|
||||
expected]
|
||||
[((tc-results: t1 fs os) (tc-results: t2 fs os))
|
||||
(unless (= (length t1) (length t2))
|
||||
(tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1)))
|
||||
(unless (for/and ([t t1] [s t2]) (subtype t s))
|
||||
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
|
||||
expected]
|
||||
[((tc-result1: t1 f o) (? Type? t2))
|
||||
(unless (subtype t1 t2)
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
|
||||
t1]
|
||||
[((? Type? t1) (? Type? t2))
|
||||
(unless (subtype t1 t2)
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
|
||||
expected]
|
||||
[(a b) (int-err "unexpected input for check-below: ~a ~a" a b)]))
|
||||
(ret t2 f o)]
|
||||
[((? Type? t1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:)))
|
||||
(unless (subtype t1 t2)
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
|
||||
t1]
|
||||
[((? Type? t1) (tc-result1: t2 f o))
|
||||
(if (subtype t1 t2)
|
||||
(tc-error/expr "Expected result with filter ~a and ~a, got ~a" f (print-object o) t1)
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
|
||||
t1]
|
||||
[((? Type? t1) (? Type? t2))
|
||||
(unless (subtype t1 t2)
|
||||
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
|
||||
expected]
|
||||
[(a b) (int-err "unexpected input for check-below: ~a ~a" a b)])))
|
||||
|
||||
(define (tc-expr/check/type form expected)
|
||||
#;(syntax? Type/c . -> . tc-results?)
|
||||
|
|
|
|||
|
|
@ -44,10 +44,16 @@
|
|||
(let*-values ([(flag+ flag-) (values (box #t) (box #t))])
|
||||
(match-let* ([env-thn (env+ (lexical-env) (list fs+) flag+)]
|
||||
[env-els (env+ (lexical-env) (list fs-) flag-)]
|
||||
[new-thn-props (env-props env-thn)]
|
||||
[new-els-props (env-props env-els)]
|
||||
[new-thn-props (filter (λ (e) (and (atomic-filter? e) (not (memq e (env-props (lexical-env))))))
|
||||
(env-props env-thn))]
|
||||
[new-els-props (filter (λ (e) (and (atomic-filter? e) (not (memq e (env-props (lexical-env))))))
|
||||
(env-props env-els))]
|
||||
[(tc-results: ts fs2 os2) (with-lexical-env env-thn (tc thn (unbox flag+)))]
|
||||
[(tc-results: us fs3 os3) (with-lexical-env env-els (tc els (unbox flag-)))])
|
||||
;(printf "old thn-props: ~a\n" (env-props (lexical-env)))
|
||||
;(printf "fs+: ~a~n" fs+)
|
||||
;(printf "thn-props: ~a~n" (env-props env-thn))
|
||||
;(printf "new-thn-props: ~a~n" new-thn-props)
|
||||
;; if we have the same number of values in both cases
|
||||
(cond [(= (length ts) (length us))
|
||||
(let ([r (combine-results
|
||||
|
|
@ -59,12 +65,12 @@
|
|||
[(_ (NoFilter:))
|
||||
(-FS -top -top)]
|
||||
[((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
|
||||
(-FS (-or (-and fs+ f2+) (-and fs- f3+))
|
||||
(-or (-and fs+ f2-) (-and fs- f3-)))])]
|
||||
(-FS (-or (apply -and fs+ f2+ new-thn-props) (-and fs- f3+))
|
||||
(-or (apply -and fs+ f2- new-thn-props) (-and fs- f3-)))])]
|
||||
[type (Un t2 t3)]
|
||||
[object (if (object-equal? o2 o3) o2 (make-Empty))])
|
||||
;(printf "result filter is: ~a\n" filter)
|
||||
(debug ret type filter object))))])
|
||||
(ret type filter object))))])
|
||||
(if expected (check-below r expected) r))]
|
||||
;; special case if one of the branches is unreachable
|
||||
[(and (= 1 (length us)) (type-equal? (car us) (Un)))
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
#lang scheme/unit
|
||||
|
||||
(require (rename-in "../utils/utils.ss" [infer r:infer]))
|
||||
(require "signatures.ss" "tc-metafunctions.ss"
|
||||
(require "signatures.ss" "tc-metafunctions.ss" "tc-subst.ss"
|
||||
(types utils convenience)
|
||||
(private type-annotation parse-type)
|
||||
(env lexical-env type-alias-env type-env type-environments)
|
||||
|
|
@ -36,11 +36,12 @@
|
|||
(match r
|
||||
[(tc-results: ts (FilterSet: fs+ fs-) os)
|
||||
(values ts
|
||||
(for/list ([n names]
|
||||
[f+ fs+]
|
||||
[f- fs-])
|
||||
(-and (make-ImpFilter (make-NotTypeFilter (-val #f) null n) f+)
|
||||
(make-ImpFilter (make-TypeFilter (-val #f) null n) f-))))]))))
|
||||
(apply append
|
||||
(for/list ([n names]
|
||||
[f+ fs+]
|
||||
[f- fs-])
|
||||
(list (make-ImpFilter (make-NotTypeFilter (-val #f) null n) f+)
|
||||
(make-ImpFilter (make-TypeFilter (-val #f) null n) f-)))))]))))
|
||||
;; extend the lexical environment for checking the body
|
||||
(with-lexical-env/extend/props
|
||||
;; the list of lists of name
|
||||
|
|
@ -49,14 +50,29 @@
|
|||
types
|
||||
(w/c append-region
|
||||
#:result (listof Filter?)
|
||||
(append (apply append props) (env-props (lexical-env))))
|
||||
(define-values (p1 p2)
|
||||
(combine-props (apply append props) (env-props (lexical-env)) (box #t)))
|
||||
(append p1 p2))
|
||||
(for-each expr->type
|
||||
clauses
|
||||
exprs
|
||||
results)
|
||||
(if expected
|
||||
(tc-exprs/check (syntax->list body) expected)
|
||||
(tc-exprs (syntax->list body)))))
|
||||
(let ([subber (lambda (proc lst)
|
||||
(for/list ([i (in-list lst)])
|
||||
(for/fold ([s i])
|
||||
([nm (in-list (apply append namess))])
|
||||
(proc s nm (make-Empty) #t))))])
|
||||
(if expected
|
||||
(begin
|
||||
(hash-update! to-be-abstr expected
|
||||
(lambda (old-l) (apply append old-l namess))
|
||||
null)
|
||||
(tc-exprs/check (syntax->list body) expected))
|
||||
(match (tc-exprs (syntax->list body))
|
||||
[(tc-results: ts fs os)
|
||||
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
|
||||
[(tc-results: ts fs os dt db)
|
||||
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)])))))
|
||||
|
||||
(define (tc/letrec-values/check namess exprs body form expected)
|
||||
(tc/letrec-values/internal namess exprs body form expected))
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@
|
|||
[one-of/c -one-of/c])
|
||||
(rep type-rep filter-rep rep-utils) scheme/list
|
||||
scheme/contract scheme/match unstable/match scheme/trace
|
||||
unstable/debug
|
||||
(for-syntax scheme/base))
|
||||
|
||||
;(provide (all-defined-out))
|
||||
|
|
@ -125,6 +126,7 @@
|
|||
(match p
|
||||
[(AndFilter: ps) (loop derived-props derived-atoms (append ps (cdr worklist)))]
|
||||
[(ImpFilter: a c)
|
||||
;(printf "combining ~a with ~a\n" p (append derived-props derived-atoms))
|
||||
(if (for/or ([p (append derived-props derived-atoms)])
|
||||
(implied-atomic? a p))
|
||||
(loop derived-props derived-atoms (cons c (cdr worklist)))
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
[->* -->*]
|
||||
[one-of/c -one-of/c])
|
||||
(rep type-rep filter-rep rep-utils) scheme/list
|
||||
scheme/contract scheme/match unstable/match
|
||||
scheme/contract scheme/match unstable/match unstable/debug
|
||||
(for-syntax scheme/base)
|
||||
"tc-metafunctions.ss")
|
||||
|
||||
|
|
@ -16,6 +16,12 @@
|
|||
(begin (d/c (name . args) c . body)
|
||||
(p/c [name c])))
|
||||
|
||||
(define (name-ref=? a b)
|
||||
(or (eq? a b)
|
||||
(and (identifier? a)
|
||||
(identifier? b)
|
||||
(free-identifier=? a b))))
|
||||
|
||||
(d/c/p (open-Result r objs)
|
||||
(-> Result? (listof Object?) (values Type/c FilterSet? Object?))
|
||||
(match r
|
||||
|
|
@ -27,14 +33,14 @@
|
|||
(subst-object old-obj k o #t)))]))
|
||||
|
||||
(d/c/p (subst-filter-set fs k o polarity)
|
||||
(-> FilterSet? integer? Object? boolean? FilterSet?)
|
||||
(-> FilterSet? name-ref/c Object? boolean? FilterSet?)
|
||||
(match fs
|
||||
[(FilterSet: f+ f-)
|
||||
(combine (subst-filter f+ k o polarity)
|
||||
(subst-filter f- k o polarity))]))
|
||||
|
||||
(d/c (subst-type t k o polarity)
|
||||
(-> Type/c integer? Object? boolean? Type/c)
|
||||
(d/c/p (subst-type t k o polarity)
|
||||
(-> Type/c name-ref/c Object? boolean? Type/c)
|
||||
(define (st t) (subst-type t k o polarity))
|
||||
(d/c (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs k o polarity))
|
||||
(type-case (#:Type st
|
||||
|
|
@ -44,20 +50,22 @@
|
|||
[#:arr dom rng rest drest kws
|
||||
;; here we have to increment the count for the domain, where the new bindings are in scope
|
||||
(let* ([arg-count (+ (length dom) (if rest 1 0) (if drest 1 0) (length kws))]
|
||||
[st* (lambda (t) (subst-type t (+ arg-count k) o polarity))])
|
||||
[st* (if (integer? k)
|
||||
(λ (t) (subst-type t (+ arg-count k) o polarity))
|
||||
st)])
|
||||
(make-arr (map st dom)
|
||||
(st* rng)
|
||||
(and rest (st rest))
|
||||
(and drest (cons (st (car drest)) (cdr drest)))
|
||||
(map st kws)))]))
|
||||
|
||||
(d/c (subst-object t k o polarity)
|
||||
(-> Object? integer? Object? boolean? Object?)
|
||||
(d/c/p (subst-object t k o polarity)
|
||||
(-> Object? name-ref/c Object? boolean? Object?)
|
||||
(match t
|
||||
[(NoObject:) t]
|
||||
[(Empty:) t]
|
||||
[(Path: p i)
|
||||
(if (eq? i k)
|
||||
(if (name-ref=? i k)
|
||||
(match o
|
||||
[(Empty:) (make-Empty)]
|
||||
;; the result is not from an annotation, so it isn't a NoObject
|
||||
|
|
@ -67,13 +75,17 @@
|
|||
|
||||
;; this is the substitution metafunction
|
||||
(d/c/p (subst-filter f k o polarity)
|
||||
(-> Filter/c integer? Object? boolean? Filter/c)
|
||||
(define (ap f) (subst-filter f o polarity))
|
||||
(-> Filter/c name-ref/c Object? boolean? Filter/c)
|
||||
(define (ap f) (subst-filter f k o polarity))
|
||||
(define (tf-matcher t p i k o polarity maker)
|
||||
(match o
|
||||
[(or (Empty:) (NoObject:)) (if polarity -top -bot)]
|
||||
[(or (Empty:) (NoObject:))
|
||||
(cond [(name-ref=? i k)
|
||||
(if polarity -top -bot)]
|
||||
[(index-free-in? k t) (if polarity -top -bot)]
|
||||
[else f])]
|
||||
[(Path: p* i*)
|
||||
(cond [(eq? i k)
|
||||
(cond [(name-ref=? i k)
|
||||
(maker
|
||||
(subst-type t k o polarity)
|
||||
(append p p*)
|
||||
|
|
@ -83,8 +95,8 @@
|
|||
(match f
|
||||
[(ImpFilter: ant consq)
|
||||
(make-ImpFilter (subst-filter ant k o (not polarity)) (ap consq))]
|
||||
[(AndFilter: fs) (make-AndFilter (map ap fs))]
|
||||
[(OrFilter: fs) (make-OrFilter (map ap fs))]
|
||||
[(AndFilter: fs) (apply -and (map ap fs))]
|
||||
[(OrFilter: fs) (apply -or (map ap fs))]
|
||||
[(Bot:) -bot]
|
||||
[(Top:) -top]
|
||||
[(TypeFilter: t p i)
|
||||
|
|
@ -99,7 +111,7 @@
|
|||
(object-case (#:Type for-type)
|
||||
o
|
||||
[#:Path p i
|
||||
(if (eq? i k)
|
||||
(if (name-ref=? i k)
|
||||
(return #t)
|
||||
o)]))
|
||||
(define (for-filter o)
|
||||
|
|
@ -107,11 +119,11 @@
|
|||
#:Filter for-filter)
|
||||
o
|
||||
[#:NotTypeFilter t p i
|
||||
(if (eq? i k)
|
||||
(if (name-ref=? i k)
|
||||
(return #t)
|
||||
o)]
|
||||
[#:TypeFilter t p i
|
||||
(if (eq? i k)
|
||||
(if (name-ref=? i k)
|
||||
(return #t)
|
||||
o)]))
|
||||
(define (for-type t)
|
||||
|
|
@ -128,7 +140,8 @@
|
|||
(and rest (for-type rest))
|
||||
(and drest (cons (for-type (car drest)) (cdr drest)))
|
||||
(map for-type kws)))]))
|
||||
(for-type type)))
|
||||
(for-type type)
|
||||
#f))
|
||||
|
||||
;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
|
||||
(d/c/p (values->tc-results tc formals)
|
||||
|
|
|
|||
|
|
@ -71,6 +71,9 @@
|
|||
|
||||
(define Ident (-Syntax -Symbol))
|
||||
|
||||
(define (atomic-filter? e)
|
||||
(or (TypeFilter? e) (NotTypeFilter? e)))
|
||||
|
||||
(define (opposite? f1 f2)
|
||||
(match* (f1 f2)
|
||||
[((TypeFilter: t1 p1 i1)
|
||||
|
|
@ -124,11 +127,15 @@
|
|||
(loop (cdr props) others)]
|
||||
[p (loop (cdr props) (cons p others))]))))
|
||||
|
||||
(define (-or . args)
|
||||
(define (-or . args)
|
||||
(define mk
|
||||
(case-lambda [() -bot]
|
||||
[(f) f]
|
||||
[fs (make-OrFilter fs)]))
|
||||
(define (distribute args)
|
||||
(define-values (ands others) (partition AndFilter? args))
|
||||
(if (null? ands)
|
||||
(make-OrFilter others)
|
||||
(apply mk others)
|
||||
(match-let ([(AndFilter: elems) (car ands)])
|
||||
(apply -and (for/list ([a (in-list elems)])
|
||||
(apply -or a (append (cdr ands) others)))))))
|
||||
|
|
@ -152,7 +159,7 @@
|
|||
(loop (cdr fs) (cons t result))])]))))
|
||||
|
||||
(define (-and . args)
|
||||
(let loop ([fs args] [result null])
|
||||
(let loop ([fs (remove-duplicates args filter-equal?)] [result null])
|
||||
(if (null? fs)
|
||||
(match result
|
||||
[(list) -top]
|
||||
|
|
|
|||
|
|
@ -310,3 +310,10 @@
|
|||
;; a parameter for the current polymorphic structure being defined
|
||||
;; to allow us to prevent non-regular datatypes
|
||||
(define current-poly-struct (make-parameter #f))
|
||||
|
||||
;; a table indicating what variables should be abstracted away before using this expected type
|
||||
;; keyed on the numeric Rep sequence
|
||||
(define to-be-abstr
|
||||
(make-weak-hash))
|
||||
|
||||
(provide to-be-abstr)
|
||||
Loading…
Reference in New Issue
Block a user