take out work on paths, now compiles
svn: r13431 original commit: f867eea8c313ff53bdfa4edd9f4e5af0d89ef657
This commit is contained in:
parent
cfab8a698f
commit
bb5298992b
|
@ -100,9 +100,9 @@
|
|||
(define (cgen/eff V X t s)
|
||||
(match* (t s)
|
||||
[(e e) (empty-cset X)]
|
||||
[((Latent-Restrict-Effect: t k) (Latent-Restrict-Effect: s k))
|
||||
[((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: s))
|
||||
(cset-meet (cgen V X t s) (cgen V X s t))]
|
||||
[((Latent-Remove-Effect: t k) (Latent-Remove-Effect: s k))
|
||||
[((Latent-Remove-Effect: t) (Latent-Remove-Effect: s))
|
||||
(cset-meet (cgen V X t s) (cgen V X s t))]
|
||||
[(_ _) (fail! t s)]))
|
||||
|
||||
|
|
|
@ -108,8 +108,8 @@
|
|||
[filter (-poly (a b) (cl->*
|
||||
((a . -> . B
|
||||
:
|
||||
(list (make-Latent-Restrict-Effect b 0))
|
||||
(list (make-Latent-Remove-Effect b 0)))
|
||||
(list (make-Latent-Restrict-Effect b))
|
||||
(list (make-Latent-Remove-Effect b)))
|
||||
(-lst a)
|
||||
. -> .
|
||||
(-lst b))
|
||||
|
|
|
@ -83,10 +83,10 @@
|
|||
(define (sub-eff e1 e2)
|
||||
(match* (e1 e2)
|
||||
[(e e) #t]
|
||||
[((Latent-Restrict-Effect: t k) (Latent-Restrict-Effect: t* k))
|
||||
[((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: t*))
|
||||
(and (subtype t t*)
|
||||
(subtype t* t))]
|
||||
[((Latent-Remove-Effect: t k) (Latent-Remove-Effect: t* k))
|
||||
[((Latent-Remove-Effect: t) (Latent-Remove-Effect: t*))
|
||||
(and (subtype t t*)
|
||||
(subtype t* t))]
|
||||
[(_ _) #f]))
|
||||
|
|
|
@ -38,10 +38,10 @@
|
|||
|
||||
(define ((add-var v) eff)
|
||||
(match eff
|
||||
[(Latent-Var-True-Effect: k) (-vet v)]
|
||||
[(Latent-Var-False-Effect: k) (-vef v)]
|
||||
[(Latent-Restrict-Effect: t k) (make-Restrict-Effect t v)]
|
||||
[(Latent-Remove-Effect: t k) (make-Remove-Effect t v)]
|
||||
[(Latent-Var-True-Effect:) (-vet v)]
|
||||
[(Latent-Var-False-Effect:) (-vef v)]
|
||||
[(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
|
||||
[(Latent-Remove-Effect: t) (make-Remove-Effect t v)]
|
||||
[(True-Effect:) eff]
|
||||
[(False-Effect:) eff]
|
||||
[_ (int-err "can't add var ~a to effect ~a" v eff)]))
|
||||
|
@ -208,7 +208,7 @@
|
|||
(define make-pred-ty
|
||||
(case-lambda
|
||||
[(in out t)
|
||||
(->* in out : (list (make-Latent-Restrict-Effect t 0)) (list (make-Latent-Remove-Effect t 0)))]
|
||||
(->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))]
|
||||
[(t) (make-pred-ty (list Univ) B t)]))
|
||||
|
||||
(define -Pathlike (*Un -Path -String))
|
||||
|
|
|
@ -32,10 +32,10 @@
|
|||
(match c
|
||||
[(Restrict-Effect: t v) (fp "(restrict ~a ~a)" t (syntax-e v))]
|
||||
[(Remove-Effect: t v) (fp "(remove ~a ~a)" t (syntax-e v))]
|
||||
[(Latent-Restrict-Effect: t k) (fp "(restrict ~a ~a)" t k)]
|
||||
[(Latent-Remove-Effect: t k) (fp "(remove ~a ~a)" t k)]
|
||||
[(Latent-Var-True-Effect: k) (fp "(var #t ~a)" k)]
|
||||
[(Latent-Var-False-Effect: k) (fp "(var #f ~a)" k)]
|
||||
[(Latent-Restrict-Effect: t) (fp "(restrict ~a)" t)]
|
||||
[(Latent-Remove-Effect: t) (fp "(remove ~a)" t)]
|
||||
[(Latent-Var-True-Effect:) (fp "(var #t)")]
|
||||
[(Latent-Var-False-Effect:) (fp "(var #f)")]
|
||||
[(True-Effect:) (fp "T")]
|
||||
[(False-Effect:) (fp "F")]
|
||||
[(Var-True-Effect: v) (fp "(var #t ~a)" (syntax-e v))]
|
||||
|
@ -66,8 +66,8 @@
|
|||
(fp "-> ~a" rng)
|
||||
(match* (thn-eff els-eff)
|
||||
[((list) (list)) (void)]
|
||||
[((list (Latent-Restrict-Effect: t 0)) (list (Latent-Remove-Effect: t 0))) (fp " : ~a" t)]
|
||||
[((list (Latent-Restrict-Effect: t k)) (list (Latent-Remove-Effect: t k))) (fp " : ~a_~a" t k)]
|
||||
[((list (Latent-Restrict-Effect: t)) (list (Latent-Remove-Effect: t))) (fp " : ~a" t)]
|
||||
[((list (Latent-Restrict-Effect: t)) (list (Latent-Remove-Effect: t))) (fp " : ~a" t)]
|
||||
[(_ _) (fp " : ~a ~a" thn-eff els-eff)])
|
||||
(fp ")")]))
|
||||
(define (tuple? t)
|
||||
|
|
|
@ -27,19 +27,15 @@
|
|||
[#:fold-rhs (*Remove-Effect (type-rec-id t) v)])
|
||||
|
||||
;; t is a Type
|
||||
;; k is a nat
|
||||
(de Latent-Restrict-Effect (t k) [#:frees (free-vars* t) (free-idxs* t)]
|
||||
[#:fold-rhs (*Latent-Restrict-Effect (type-rec-id t) k)])
|
||||
(de Latent-Restrict-Effect (t) [#:frees (free-vars* t) (free-idxs* t)]
|
||||
[#:fold-rhs (*Latent-Restrict-Effect (type-rec-id t))])
|
||||
|
||||
;; t is a Type
|
||||
;; k is a nat
|
||||
(de Latent-Remove-Effect (t k) [#:frees (free-vars* t) (free-idxs* t)]
|
||||
[#:fold-rhs (*Latent-Remove-Effect (type-rec-id t) k)])
|
||||
(de Latent-Remove-Effect (t) [#:frees (free-vars* t) (free-idxs* t)]
|
||||
[#:fold-rhs (*Latent-Remove-Effect (type-rec-id t))])
|
||||
|
||||
;; k is a nat
|
||||
(de Latent-Var-True-Effect (k) [#:frees #f] [#:fold-rhs #:base])
|
||||
(de Latent-Var-True-Effect () [#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
;; k is a nat
|
||||
(de Latent-Var-False-Effect (k) [#:frees #f] [#:fold-rhs #:base])
|
||||
(de Latent-Var-False-Effect () [#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
;; could also have latent true/false effects, but seems pointless
|
||||
|
|
|
@ -11,7 +11,7 @@
|
|||
scheme/base
|
||||
syntax/struct
|
||||
syntax/stx
|
||||
(except-in (utils utils))))
|
||||
(utils utils)))
|
||||
|
||||
(provide == dt de print-type* print-effect* Type Type? Effect Effect? defintern hash-id Type-seq Effect-seq)
|
||||
|
||||
|
|
Loading…
Reference in New Issue
Block a user