Implement dmap operations.
Remove lots of unneeded requires. Add in-list-forever and extend to utils.ss Add optional variable argument to c-meet.
This commit is contained in:
parent
49be490b51
commit
e2c0b4e642
|
@ -1,30 +1,15 @@
|
||||||
#lang scheme/unit
|
#lang scheme/unit
|
||||||
|
|
||||||
(require syntax/kerncase
|
(require syntax/kerncase
|
||||||
syntax/struct
|
|
||||||
syntax/stx
|
|
||||||
scheme/match
|
scheme/match
|
||||||
"type-contract.ss"
|
|
||||||
"signatures.ss"
|
"signatures.ss"
|
||||||
"tc-structs.ss"
|
|
||||||
"type-utils.ss"
|
"type-utils.ss"
|
||||||
"utils.ss" ;; doesn't need tests
|
|
||||||
"type-rep.ss" ;; doesn't need tests
|
"type-rep.ss" ;; doesn't need tests
|
||||||
"type-effect-convenience.ss" ;; maybe needs tests
|
"type-effect-convenience.ss" ;; maybe needs tests
|
||||||
"union.ss"
|
"union.ss"
|
||||||
"subtype.ss" ;; has tests
|
"subtype.ss" ;; has tests
|
||||||
"internal-forms.ss" ;; doesn't need tests
|
|
||||||
"planet-requires.ss" ;; doesn't need tests
|
|
||||||
"type-env.ss" ;; maybe needs tests
|
|
||||||
"parse-type.ss" ;; has tests
|
|
||||||
"tc-utils.ss" ;; doesn't need tests
|
"tc-utils.ss" ;; doesn't need tests
|
||||||
"type-environments.ss" ;; doesn't need tests
|
)
|
||||||
"lexical-env.ss" ;; maybe needs tests
|
|
||||||
"type-annotation.ss" ;; has tests
|
|
||||||
"type-name-env.ss" ;; maybe needs tests
|
|
||||||
"init-envs.ss"
|
|
||||||
"effect-rep.ss"
|
|
||||||
"mutated-vars.ss")
|
|
||||||
|
|
||||||
(import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-expr^)
|
(import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-expr^)
|
||||||
(export check-subforms^)
|
(export check-subforms^)
|
||||||
|
|
|
@ -1,15 +1,12 @@
|
||||||
#lang scheme/unit
|
#lang scheme/unit
|
||||||
|
|
||||||
(require "type-effect-convenience.ss" "type-rep.ss" "effect-rep.ss" "rep-utils.ss"
|
(require "type-effect-convenience.ss" "type-rep.ss"
|
||||||
"free-variance.ss" "type-utils.ss" "union.ss" "tc-utils.ss" "type-name-env.ss"
|
"type-utils.ss" "union.ss" "tc-utils.ss"
|
||||||
"subtype.ss" "remove-intersect.ss" "utils.ss"
|
"subtype.ss" "utils.ss"
|
||||||
"signatures.ss"
|
"signatures.ss"
|
||||||
scheme/match
|
scheme/match)
|
||||||
mzlib/etc
|
|
||||||
mzlib/trace
|
|
||||||
scheme/list)
|
|
||||||
|
|
||||||
(import restrict^)
|
(import restrict^ dmap^)
|
||||||
(export constraints^)
|
(export constraints^)
|
||||||
|
|
||||||
|
|
||||||
|
@ -68,13 +65,15 @@
|
||||||
(define (join T U) (Un T U))
|
(define (join T U) (Un T U))
|
||||||
|
|
||||||
|
|
||||||
(define c-meet
|
(define (c-meet c1 c2 [var #f])
|
||||||
(match-lambda**
|
(match* (c1 c2)
|
||||||
[((struct c (S X T)) (struct c (S* _ T*)))
|
[((struct c (S X T)) (struct c (S* X* T*)))
|
||||||
(let ([S (join S S*)] [T (meet T T*)])
|
(unless (or var (eq? X X*))
|
||||||
(unless (subtype S T)
|
(int-err "Non-matching vars in c-meet: ~a ~a" X X*))
|
||||||
(fail! S T))
|
(let ([S (join S S*)] [T (meet T T*)])
|
||||||
(make-c S X T))]))
|
(unless (subtype S T)
|
||||||
|
(fail! S T))
|
||||||
|
(make-c S (or var X) T))]))
|
||||||
|
|
||||||
(define (subst-all/c sub -c)
|
(define (subst-all/c sub -c)
|
||||||
(match -c
|
(match -c
|
||||||
|
|
|
@ -1,6 +1,50 @@
|
||||||
#lang scheme/unit
|
#lang scheme/unit
|
||||||
|
|
||||||
(import)
|
(require "signatures.ss" "utils.ss" "tc-utils.ss" scheme/match)
|
||||||
(export)
|
|
||||||
|
|
||||||
|
(import constraints^)
|
||||||
|
(export dmap^)
|
||||||
|
|
||||||
|
;; map : hash mapping variable to dcon
|
||||||
|
(define-struct dmap (map))
|
||||||
|
|
||||||
|
;; fixed : Listof[c]
|
||||||
|
;; rest : option[c]
|
||||||
|
(define-struct dcon (fixed rest))
|
||||||
|
|
||||||
|
;; dcon-meet : dcon dcon -> dcon
|
||||||
|
(define (dcon-meet dc1 dc2)
|
||||||
|
(match* (dc1 dc2)
|
||||||
|
[((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f)))
|
||||||
|
(unless (= (length fixed1) (length fixed2))
|
||||||
|
(fail! fixed1 fixed2))
|
||||||
|
(make-dcon
|
||||||
|
(for/list ([c1 fixed1]
|
||||||
|
[c2 fixed2])
|
||||||
|
(c-meet c1 c2 (c-X c1)))
|
||||||
|
#f)]
|
||||||
|
[((struct dcon (fixed1 #f)) (struct dcon (fixed2 rest)))
|
||||||
|
(unless (>= (length fixed1) (length fixed2))
|
||||||
|
(fail! fixed1 fixed2))
|
||||||
|
(make-dcon
|
||||||
|
(for/list ([c1 fixed1]
|
||||||
|
[c2 (in-list-forever fixed2 rest)])
|
||||||
|
(c-meet c1 c2 (c-X c1)))
|
||||||
|
#f)]
|
||||||
|
[((struct dcon (fixed1 rest)) (struct dcon (fixed2 #f)))
|
||||||
|
(dcon-meet dc2 dc1)]
|
||||||
|
[((struct dcon (fixed1 rest1)) (struct dcon (fixed2 rest2)))
|
||||||
|
(let-values ([(shorter longer srest lrest)
|
||||||
|
(if (< (length fixed1) (length fixed2))
|
||||||
|
(values fixed1 fixed2 rest1 rest2)
|
||||||
|
(values fixed2 fixed1 rest2 rest1))])
|
||||||
|
(make-dcon
|
||||||
|
(for/list ([c1 longer]
|
||||||
|
[c2 (in-list-forever shorter srest)])
|
||||||
|
(c-meet c1 c2 (c-X c1)))
|
||||||
|
(c-meet lrest srest (c-X lrest))))]))
|
||||||
|
|
||||||
|
(define (dmap-meet dm1 dm2)
|
||||||
|
(hash-union dm1 dm2
|
||||||
|
(lambda (k dc1 dc2) (dcon-meet dc1 dc2))))
|
||||||
|
|
||||||
|
|
|
@ -11,8 +11,6 @@
|
||||||
(import constraints^ promote-demote^)
|
(import constraints^ promote-demote^)
|
||||||
(export infer^)
|
(export infer^)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(define (empty-set) '())
|
(define (empty-set) '())
|
||||||
|
|
||||||
(define current-seen (make-parameter (empty-set)))
|
(define current-seen (make-parameter (empty-set)))
|
||||||
|
@ -25,7 +23,6 @@
|
||||||
(make-cset (for/list ([(cs vs) (in-pairs (cset-maps cset))])
|
(make-cset (for/list ([(cs vs) (in-pairs (cset-maps cset))])
|
||||||
(cons cs (hash-set vs dbound vars)))))
|
(cons cs (hash-set vs dbound vars)))))
|
||||||
|
|
||||||
|
|
||||||
;; ss and ts have the same length
|
;; ss and ts have the same length
|
||||||
(define (cgen-union V X ss ts)
|
(define (cgen-union V X ss ts)
|
||||||
;; first, we remove common elements of ss and ts
|
;; first, we remove common elements of ss and ts
|
||||||
|
@ -279,24 +276,8 @@
|
||||||
(subst-gen cs R)
|
(subst-gen cs R)
|
||||||
(cset-meet cs (cgen null X R expected))))))
|
(cset-meet cs (cgen null X R expected))))))
|
||||||
|
|
||||||
;; Listof[A] Listof[B] B -> Listof[B]
|
|
||||||
;; pads out t to be as long as s
|
|
||||||
(define (extend s t extra)
|
|
||||||
(append t (build-list (- (length s) (length t)) (lambda _ extra))))
|
|
||||||
|
|
||||||
(define (infer/simple S T R)
|
(define (infer/simple S T R)
|
||||||
(infer (fv/list T) S T R))
|
(infer (fv/list T) S T R))
|
||||||
|
|
||||||
|
|
||||||
(define (i s t r)
|
(define (i s t r)
|
||||||
(infer/simple (list s) (list t) r))
|
(infer/simple (list s) (list t) r))
|
||||||
|
|
||||||
;; this is *definitely* not yet correct
|
|
||||||
|
|
||||||
|
|
||||||
;(trace infer cgen cset-meet* subst-gen)
|
|
||||||
;(trace cgen/arr cgen/list cset-meet)
|
|
||||||
|
|
||||||
;(trace infer/dots cset-meet)
|
|
||||||
|
|
||||||
;(trace infer subst-gen cgen)
|
|
||||||
|
|
|
@ -1,11 +1,8 @@
|
||||||
#lang scheme/unit
|
#lang scheme/unit
|
||||||
|
|
||||||
(require "type-effect-convenience.ss" "type-rep.ss" "effect-rep.ss" "rep-utils.ss"
|
(require "type-effect-convenience.ss" "type-rep.ss"
|
||||||
"free-variance.ss" "type-utils.ss" "union.ss" "tc-utils.ss" "type-name-env.ss"
|
"type-utils.ss" "union.ss"
|
||||||
"subtype.ss" "remove-intersect.ss" "signatures.ss" "utils.ss"
|
"signatures.ss"
|
||||||
scheme/match
|
|
||||||
mzlib/etc
|
|
||||||
mzlib/trace
|
|
||||||
scheme/list)
|
scheme/list)
|
||||||
|
|
||||||
(import)
|
(import)
|
||||||
|
|
|
@ -1,28 +1,11 @@
|
||||||
#lang scheme/base
|
#lang scheme/base
|
||||||
|
|
||||||
(require (only-in srfi/1/list s:member)
|
(require (only-in srfi/1/list s:member)
|
||||||
syntax/kerncase syntax/struct syntax/stx
|
syntax/kerncase
|
||||||
mzlib/trace
|
mzlib/trace
|
||||||
"type-contract.ss"
|
"type-contract.ss"
|
||||||
"signatures.ss"
|
"type-rep.ss"
|
||||||
"tc-structs.ss"
|
"tc-utils.ss"
|
||||||
"utils.ss" ;; doesn't need tests
|
|
||||||
"type-rep.ss" ;; doesn't need tests
|
|
||||||
"type-effect-convenience.ss" ;; maybe needs tests
|
|
||||||
"union.ss"
|
|
||||||
"subtype.ss" ;; has tests
|
|
||||||
"internal-forms.ss" ;; doesn't need tests
|
|
||||||
"planet-requires.ss" ;; doesn't need tests
|
|
||||||
"type-env.ss" ;; maybe needs tests
|
|
||||||
"parse-type.ss" ;; has tests
|
|
||||||
"tc-utils.ss" ;; doesn't need tests
|
|
||||||
"type-environments.ss" ;; doesn't need tests
|
|
||||||
"lexical-env.ss" ;; maybe needs tests
|
|
||||||
"type-annotation.ss" ;; has tests
|
|
||||||
"type-name-env.ss" ;; maybe needs tests
|
|
||||||
"init-envs.ss"
|
|
||||||
"effect-rep.ss"
|
|
||||||
"mutated-vars.ss"
|
|
||||||
"def-binding.ss")
|
"def-binding.ss")
|
||||||
|
|
||||||
(require (for-template scheme/base
|
(require (for-template scheme/base
|
||||||
|
|
|
@ -2,6 +2,11 @@
|
||||||
(require scheme/unit)
|
(require scheme/unit)
|
||||||
(provide (all-defined-out))
|
(provide (all-defined-out))
|
||||||
|
|
||||||
|
(define-signature dmap^
|
||||||
|
((struct dmap (map))
|
||||||
|
(struct dcon (fixed rest))
|
||||||
|
dmap-meet))
|
||||||
|
|
||||||
(define-signature promote-demote^
|
(define-signature promote-demote^
|
||||||
(var-promote var-demote))
|
(var-promote var-demote))
|
||||||
|
|
||||||
|
@ -18,6 +23,7 @@
|
||||||
empty-cset
|
empty-cset
|
||||||
insert
|
insert
|
||||||
cset-combine
|
cset-combine
|
||||||
|
c-meet
|
||||||
(struct c (S X T))))
|
(struct c (S X T))))
|
||||||
|
|
||||||
(define-signature restrict^
|
(define-signature restrict^
|
||||||
|
|
|
@ -2,30 +2,19 @@
|
||||||
|
|
||||||
|
|
||||||
(require syntax/kerncase
|
(require syntax/kerncase
|
||||||
syntax/struct
|
|
||||||
syntax/stx
|
|
||||||
scheme/match
|
scheme/match
|
||||||
"type-contract.ss"
|
|
||||||
"signatures.ss"
|
"signatures.ss"
|
||||||
"tc-structs.ss"
|
|
||||||
"type-utils.ss"
|
"type-utils.ss"
|
||||||
"utils.ss" ;; doesn't need tests
|
"utils.ss" ;; doesn't need tests
|
||||||
"type-rep.ss" ;; doesn't need tests
|
"type-rep.ss" ;; doesn't need tests
|
||||||
"type-effect-convenience.ss" ;; maybe needs tests
|
"type-effect-convenience.ss" ;; maybe needs tests
|
||||||
"union.ss"
|
"union.ss"
|
||||||
"subtype.ss" ;; has tests
|
"subtype.ss" ;; has tests
|
||||||
"internal-forms.ss" ;; doesn't need tests
|
|
||||||
"planet-requires.ss" ;; doesn't need tests
|
|
||||||
"type-env.ss" ;; maybe needs tests
|
|
||||||
"parse-type.ss" ;; has tests
|
"parse-type.ss" ;; has tests
|
||||||
"tc-utils.ss" ;; doesn't need tests
|
"tc-utils.ss" ;; doesn't need tests
|
||||||
"type-environments.ss" ;; doesn't need tests
|
|
||||||
"lexical-env.ss" ;; maybe needs tests
|
"lexical-env.ss" ;; maybe needs tests
|
||||||
"type-annotation.ss" ;; has tests
|
"type-annotation.ss" ;; has tests
|
||||||
"type-name-env.ss" ;; maybe needs tests
|
|
||||||
"init-envs.ss"
|
|
||||||
"effect-rep.ss"
|
"effect-rep.ss"
|
||||||
"mutated-vars.ss"
|
|
||||||
scheme/private/class-internal)
|
scheme/private/class-internal)
|
||||||
|
|
||||||
(require (for-template scheme/base scheme/private/class-internal))
|
(require (for-template scheme/base scheme/private/class-internal))
|
||||||
|
|
|
@ -1,18 +1,17 @@
|
||||||
#lang scheme/unit
|
#lang scheme/unit
|
||||||
|
|
||||||
(require "signatures.ss"
|
(require "signatures.ss"
|
||||||
(lib "trace.ss")
|
mzlib/trace
|
||||||
(except-in "type-rep.ss" make-arr) ;; doesn't need tests
|
(except-in "type-rep.ss" make-arr) ;; doesn't need tests
|
||||||
"type-effect-convenience.ss" ;; maybe needs tests
|
"type-effect-convenience.ss" ;; maybe needs tests
|
||||||
"type-environments.ss" ;; doesn't need tests
|
"type-environments.ss" ;; doesn't need tests
|
||||||
"lexical-env.ss" ;; maybe needs tests
|
"lexical-env.ss" ;; maybe needs tests
|
||||||
"type-annotation.ss" ;; has tests
|
"type-annotation.ss" ;; has tests
|
||||||
"utils.ss"
|
(except-in "utils.ss" extend)
|
||||||
"type-utils.ss"
|
"type-utils.ss"
|
||||||
"effect-rep.ss"
|
"effect-rep.ss"
|
||||||
"tc-utils.ss"
|
"tc-utils.ss"
|
||||||
"union.ss"
|
"union.ss"
|
||||||
"resolve-type.ss"
|
|
||||||
(lib "plt-match.ss")
|
(lib "plt-match.ss")
|
||||||
(only-in "type-effect-convenience.ss" [make-arr* make-arr]))
|
(only-in "type-effect-convenience.ss" [make-arr* make-arr]))
|
||||||
(require (for-template scheme/base "internal-forms.ss"))
|
(require (for-template scheme/base "internal-forms.ss"))
|
||||||
|
|
|
@ -12,7 +12,9 @@
|
||||||
id
|
id
|
||||||
filter-multiple
|
filter-multiple
|
||||||
hash-union
|
hash-union
|
||||||
in-pairs)
|
in-pairs
|
||||||
|
in-list-forever
|
||||||
|
extend)
|
||||||
|
|
||||||
(define-syntax (with-syntax* stx)
|
(define-syntax (with-syntax* stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
|
@ -142,3 +144,19 @@
|
||||||
(lambda (_) (more?))
|
(lambda (_) (more?))
|
||||||
(lambda _ #t)
|
(lambda _ #t)
|
||||||
(lambda _ #t))))))
|
(lambda _ #t))))))
|
||||||
|
|
||||||
|
(define (in-list-forever seq val)
|
||||||
|
(make-do-sequence
|
||||||
|
(lambda ()
|
||||||
|
(let-values ([(more? gen) (sequence-generate seq)])
|
||||||
|
(values (lambda (e) (let ([e (if (more?) (gen) val)]) e))
|
||||||
|
(lambda (_) #t)
|
||||||
|
#t
|
||||||
|
(lambda (_) #t)
|
||||||
|
(lambda _ #t)
|
||||||
|
(lambda _ #t))))))
|
||||||
|
|
||||||
|
;; Listof[A] Listof[B] B -> Listof[B]
|
||||||
|
;; pads out t to be as long as s
|
||||||
|
(define (extend s t extra)
|
||||||
|
(append t (build-list (- (length s) (length t)) (lambda _ extra))))
|
|
@ -12,7 +12,7 @@
|
||||||
"private/tc-utils.ss"
|
"private/tc-utils.ss"
|
||||||
"private/type-name-env.ss"
|
"private/type-name-env.ss"
|
||||||
"private/type-alias-env.ss"
|
"private/type-alias-env.ss"
|
||||||
"private/utils.ss"
|
(except-in "private/utils.ss" extend)
|
||||||
(only-in "private/infer-dummy.ss" infer-param)
|
(only-in "private/infer-dummy.ss" infer-param)
|
||||||
"private/infer.ss"
|
"private/infer.ss"
|
||||||
"private/type-effect-convenience.ss"
|
"private/type-effect-convenience.ss"
|
||||||
|
|
Loading…
Reference in New Issue
Block a user