Make initial version of structural type recursion, and use it.
This commit is contained in:
parent
cadc2dcb8f
commit
9efa4af051
|
@ -2,7 +2,7 @@
|
||||||
|
|
||||||
(require "../utils/utils.rkt"
|
(require "../utils/utils.rkt"
|
||||||
(rep type-rep rep-utils)
|
(rep type-rep rep-utils)
|
||||||
(types abbrev union utils)
|
(types abbrev union utils structural)
|
||||||
racket/list racket/match)
|
racket/list racket/match)
|
||||||
|
|
||||||
(provide/cond-contract
|
(provide/cond-contract
|
||||||
|
@ -24,36 +24,40 @@
|
||||||
(define-values (var-promote var-demote)
|
(define-values (var-promote var-demote)
|
||||||
(let ()
|
(let ()
|
||||||
(define (var-change V T change)
|
(define (var-change V T change)
|
||||||
(define (co t) (var-change V t change))
|
(define (structural-recur t sym)
|
||||||
(define (contra t) (var-change V t (not change)))
|
(case sym
|
||||||
(define (inv t)
|
[(co) (var-change V t change)]
|
||||||
(if (V-in? V t)
|
[(contra) (var-change V t (not change))]
|
||||||
(if change Univ -Bottom)
|
[(inv)
|
||||||
t))
|
(if (V-in? V t)
|
||||||
(type-case (#:Type co #:Filter (sub-f co)) T
|
(if change Univ -Bottom)
|
||||||
[#:F name (if (memq name V) (if change Univ -Bottom) T)]
|
t)]))
|
||||||
[#:Vector t (make-Vector (inv t))]
|
(define (co t) (structural-recur t 'co))
|
||||||
[#:Box t (make-Box (inv t))]
|
(define (contra t) (structural-recur t 'contra))
|
||||||
[#:Channel t (make-Channel (inv t))]
|
|
||||||
[#:ThreadCell t (make-ThreadCell (inv t))]
|
(match T
|
||||||
[#:Hashtable k v (make-Hashtable (inv k) (inv v))]
|
[(? structural?) (structural-map T structural-recur)]
|
||||||
[#:Param in out (make-Param (contra in) (co out))]
|
[(F: name) (if (memq name V) (if change Univ -Bottom) T)]
|
||||||
[#:arr dom rng rest drest kws
|
[(arr: dom rng rest drest kws)
|
||||||
(cond
|
(cond
|
||||||
[(apply V-in? V (get-filters rng))
|
[(apply V-in? V (get-filters rng))
|
||||||
(make-top-arr)]
|
(make-top-arr)]
|
||||||
[(and drest (memq (cdr drest) V))
|
[(and drest (memq (cdr drest) V))
|
||||||
(make-arr (map contra dom)
|
(make-arr (map contra dom)
|
||||||
(co rng)
|
(co rng)
|
||||||
(contra (car drest))
|
(contra (car drest))
|
||||||
#f
|
#f
|
||||||
(map contra kws))]
|
(map contra kws))]
|
||||||
[else
|
[else
|
||||||
(make-arr (map contra dom)
|
(make-arr (map contra dom)
|
||||||
(co rng)
|
(co rng)
|
||||||
(and rest (contra rest))
|
(and rest (contra rest))
|
||||||
(and drest (cons (contra (car drest)) (cdr drest)))
|
(and drest (cons (contra (car drest)) (cdr drest)))
|
||||||
(map contra kws))])]))
|
(map contra kws))])]
|
||||||
|
[(? Filter?) ((sub-f co) T)]
|
||||||
|
[(? Object?) ((sub-o co) T)]
|
||||||
|
[(? Type?) ((sub-t co) T)]))
|
||||||
|
|
||||||
(values
|
(values
|
||||||
(lambda (T V) (var-change V T #t))
|
(lambda (T V) (var-change V T #t))
|
||||||
(lambda (T V) (var-change V T #f)))))
|
(lambda (T V) (var-change V T #f)))))
|
||||||
|
|
|
@ -31,7 +31,7 @@
|
||||||
free-vars*
|
free-vars*
|
||||||
type-compare type<?
|
type-compare type<?
|
||||||
remove-dups
|
remove-dups
|
||||||
sub-f sub-o sub-pe
|
sub-t sub-f sub-o sub-pe
|
||||||
(rename-out [Class:* Class:]
|
(rename-out [Class:* Class:]
|
||||||
[Class* make-Class]
|
[Class* make-Class]
|
||||||
[Row* make-Row]
|
[Row* make-Row]
|
||||||
|
@ -618,6 +618,12 @@
|
||||||
#:PathElem (sub-pe st))
|
#:PathElem (sub-pe st))
|
||||||
e))
|
e))
|
||||||
|
|
||||||
|
(define ((sub-t st) e)
|
||||||
|
(type-case (#:Type st
|
||||||
|
#:Filter (sub-f st))
|
||||||
|
e))
|
||||||
|
|
||||||
|
|
||||||
;; abstract-many : Names Type -> Scope^n
|
;; abstract-many : Names Type -> Scope^n
|
||||||
;; where n is the length of names
|
;; where n is the length of names
|
||||||
(define (abstract-many names ty)
|
(define (abstract-many names ty)
|
||||||
|
|
|
@ -0,0 +1,135 @@
|
||||||
|
#lang racket/base
|
||||||
|
|
||||||
|
;; Module for providing recursive operations over types when the operation doesn't care about the
|
||||||
|
;; type constructor.
|
||||||
|
|
||||||
|
;; This file is meant to implement more general versions of type-case.
|
||||||
|
;; Currently supported
|
||||||
|
;; * Trivial type constructors (only have Rep? or (listof Rep?) fields)
|
||||||
|
;; * A variance aware traversal of a Rep? with the return value having the same type constructor as
|
||||||
|
;; the input.
|
||||||
|
;; To be added
|
||||||
|
;; * Support for type constructors with non Rep? fields
|
||||||
|
;; * Support for objects and filters
|
||||||
|
;; * Support for smart constructors for the return value
|
||||||
|
;; * Support for return values that are not Rep?
|
||||||
|
;; * Parallel traversal of two types
|
||||||
|
|
||||||
|
(require
|
||||||
|
"../utils/utils.rkt"
|
||||||
|
racket/match
|
||||||
|
(rep type-rep)
|
||||||
|
(for-syntax
|
||||||
|
racket/base
|
||||||
|
syntax/parse
|
||||||
|
racket/syntax
|
||||||
|
unstable/sequence))
|
||||||
|
(provide
|
||||||
|
structural?
|
||||||
|
structural-map)
|
||||||
|
|
||||||
|
|
||||||
|
(define-for-syntax structural-reps
|
||||||
|
#'([BoxTop ()]
|
||||||
|
[ChannelTop ()]
|
||||||
|
[ClassTop ()]
|
||||||
|
[Continuation-Mark-KeyTop ()]
|
||||||
|
[Error ()]
|
||||||
|
[HashtableTop ()]
|
||||||
|
[MPairTop ()]
|
||||||
|
[Prompt-TagTop ()]
|
||||||
|
[StructTypeTop ()]
|
||||||
|
[ThreadCellTop ()]
|
||||||
|
[Univ ()]
|
||||||
|
[VectorTop ()]
|
||||||
|
|
||||||
|
[CustodianBox (#:co)]
|
||||||
|
[Ephemeron (#:co)]
|
||||||
|
[Evt (#:co)]
|
||||||
|
[Future (#:co)]
|
||||||
|
[Instance (#:co)]
|
||||||
|
[Promise (#:co)]
|
||||||
|
[Set (#:co)]
|
||||||
|
[StructTop (#:co)]
|
||||||
|
[StructType (#:co)]
|
||||||
|
[Syntax (#:co)]
|
||||||
|
[Pair (#:co #:co)]
|
||||||
|
[Sequence ((#:listof #:co))]
|
||||||
|
[Function ((#:listof #:co))]
|
||||||
|
|
||||||
|
[Param (#:contra #:co)]
|
||||||
|
|
||||||
|
[Continuation-Mark-Keyof (#:inv)]
|
||||||
|
[Box (#:inv)]
|
||||||
|
[Channel (#:inv)]
|
||||||
|
[ThreadCell (#:inv)]
|
||||||
|
[Vector (#:inv)]
|
||||||
|
[Hashtable (#:inv #:inv)]
|
||||||
|
[MPair (#:inv #:inv)]
|
||||||
|
[Prompt-Tagof (#:inv #:inv)]
|
||||||
|
[HeterogeneousVector ((#:listof #:inv))]
|
||||||
|
|
||||||
|
;; Non Types
|
||||||
|
[Result (#:co #:co #:co)]
|
||||||
|
[Values ((#:listof #:co))]
|
||||||
|
[AnyValues ()]
|
||||||
|
[top-arr ()]))
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
(define-syntax-class type-name
|
||||||
|
#:attributes (pred? matcher: maker)
|
||||||
|
(pattern t:id
|
||||||
|
#:with pred? (format-id #'t "~a?" #'t)
|
||||||
|
#:with matcher: (format-id #'t "~a:" #'t)
|
||||||
|
#:with maker (format-id #'t "make-~a" #'t))))
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
(define-syntax-class type-variance
|
||||||
|
#:attributes (sym)
|
||||||
|
(pattern #:co #:with sym 'co)
|
||||||
|
(pattern #:inv #:with sym 'inv)
|
||||||
|
(pattern #:contra #:with sym 'contra))
|
||||||
|
|
||||||
|
(define-syntax-class type-field
|
||||||
|
(pattern var:type-variance)
|
||||||
|
(pattern (#:listof var:type-variance))))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
(define-syntax (gen-structural? stx)
|
||||||
|
(syntax-parse structural-reps
|
||||||
|
[([type:type-name (field:type-field ...)] ...)
|
||||||
|
#'(lambda (t)
|
||||||
|
(or (type.pred? t) ...))]))
|
||||||
|
|
||||||
|
;; Returns true if the type/filter/object supports structural operations.
|
||||||
|
(define structural? (gen-structural?))
|
||||||
|
|
||||||
|
|
||||||
|
(define-syntax (gen-structural-map stx)
|
||||||
|
(syntax-parse stx
|
||||||
|
[(_ input-type:id recur-f:id)
|
||||||
|
(define-syntax-class type-field*
|
||||||
|
#:attributes (recur)
|
||||||
|
(pattern var:type-variance
|
||||||
|
#:with recur #'(λ (t) (recur-f t 'var.sym)))
|
||||||
|
(pattern (#:listof var:type-variance)
|
||||||
|
#:with recur #'(λ (ts) (for/list ([t (in-list ts)]) (recur-f t 'var.sym)))))
|
||||||
|
|
||||||
|
(define-syntax-class type-clause
|
||||||
|
#:attributes (match-clause)
|
||||||
|
(pattern [type:type-name (field:type-field* ...)]
|
||||||
|
#:with (field-pat ...) (generate-temporaries #'(field ...))
|
||||||
|
#:with match-clause
|
||||||
|
#'[(type.matcher: field-pat ...)
|
||||||
|
(type.maker (field.recur field-pat) ...)]))
|
||||||
|
|
||||||
|
(syntax-parse structural-reps
|
||||||
|
[(:type-clause ...)
|
||||||
|
#'(match input-type match-clause ...)])]))
|
||||||
|
|
||||||
|
;; Rep? (-> Rep? (or/c 'co 'contra 'inv) Rep?) -> Rep?
|
||||||
|
;; Calls `f` on each sub-type with the corresponding variance of the sub-type and combines the results
|
||||||
|
;; using the type constructor of the input type
|
||||||
|
(define (structural-map t f)
|
||||||
|
(gen-structural-map t f))
|
Loading…
Reference in New Issue
Block a user