suzanne.soy/hyper-literate
1
0
Fork 0
Code Issues 4 Pull Requests 1 Actions Packages Projects Releases Wiki Activity

Finally managed to get syntax-properties-typed.rkt to typecheck, without relying on (Syntaxof Any) in the First-Comments and Comments-After types. The predicates are horrible to write, though :-(

Browse Source
This commit is contained in:
Georges Dupéron 2017-01-12 05:03:10 +01:00
parent a110b20df1
commit deca84c956
10 changed files with 156 additions and 170 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
comments/maybe.rkt
View File

@ -1,7 +0,0 @@
#lang typed/racket
(provide (struct-out Some)
Maybe)
(struct (A) Some ([v : A]) #:prefab)
(define-type (Maybe A)
(U (Some A) #f))

43
comments/syntax-properties-typed.rkt
View File

@ -7,7 +7,9 @@
extract-first-comments
extract-comments-after)
(require "typed-syntax.rkt")
(require "typed-syntax.rkt"
"typed-pairof-predicate.rkt"
typed-map)
(define-type First-Comments
(Rec R (Pairof (U #f (Pairof (Syntaxof 'saved-props+srcloc)
@ -17,6 +19,37 @@
(define-type Comments-After
(Listof ISyntax))
(: first-comments? (→ Any Boolean : (Pairof (U #f (Pairof (Syntaxof 'saved-props+srcloc)
First-Comments))
(Listof ISyntax))))
(define (first-comments? v)
(define p? (inst pairof?
(U #f (Pairof (Syntaxof 'saved-props+srcloc)
First-Comments))
(Listof ISyntax)))
(p? v first-comments1? first-comments2?))
(: first-comments1? (→ Any Boolean : (U #f (Pairof (Syntaxof 'saved-props+srcloc)
First-Comments))))
(define (first-comments1? v)
(or (false? v)
(first-comments11? v)))
(: first-comments11? (→ Any Boolean : (Pairof (Syntaxof 'saved-props+srcloc)
First-Comments)))
(define (first-comments11? v)
(define p? (inst pairof?
(Syntaxof 'saved-props+srcloc)
First-Comments))
(p? v
(make-predicate (Syntaxof 'saved-props+srcloc))
first-comments?))
(: first-comments2? (→ Any Boolean : (Listof ISyntax)))
(define (first-comments2? v)
(and (list? v)
(andmap isyntax? v)))
(: with-first-comments (∀ (A) (→ ISyntax
(U #f First-Comments)
ISyntax)))
@ -37,13 +70,13 @@
(: extract-first-comments (-> (Syntaxof Any) (U #f First-Comments)))
(define (extract-first-comments stx)
(define c (syntax-property stx 'first-comments))
(if ((make-predicate First-Comments) c)
(if (first-comments? c)
c
#f))
(: extract-comments-after (-> (Syntaxof Any) (U #f Comments-After)))
(define (extract-comments-after stx)
(define c (syntax-property stx 'comments-after))
(if ((make-predicate Comments-After) c)
c
#f))
(and (list? c)
(andmap isyntax? c)
c))

27
comments/typed-cross-phase-structs-wrappers.rkt
View File

@ -1,27 +0,0 @@
#lang typed/racket
(require typed/racket/unsafe)
(require "untyped-cross-phase-structs-wrappers.rkt")
(unsafe-require/typed "untyped-cross-phase-structs-wrappers.rkt"
[#:struct (A) NonSexp ([v : A]) #:type-name NonSexpOf]
[#:struct (A) NonSyntax ([v : A]) #:type-name NonSyntaxOf]
[#:struct (A) Some ([v : A])])
;(require typed-racket/base-env/prims-struct)
;(dtsi* (A) NonSexp NonSexpOf ([v : A]) #:maker make-NonSexp)
(provide (struct-out NonSexp))
;(struct (A) NonSexp ([v : A]) #:type-name NonSexpOf #:constructor-name make-NonSexp)
#;(module* test typed/racket
(require (submod ".."))
(require typed/rackunit)
(check-pred procedure? NonSexp)
(check-pred NonSexp? (ann (ann (NonSexp 1) (NonSexpOf Number)) Any))
(check-not-exn
(λ ()
(ann (let ([n : (NonSexpOf Any) (NonSexp 1)])
(if (number? (NonSexp-v n))
(NonSexp-v n)
0))
Number))))

47
comments/typed-cross-phase-structs.rkt
View File

@ -1,47 +0,0 @@
(module typed-cross-phase-structs '#%kernel
(#%declare #:cross-phase-persistent)
(#%provide struct:NonSexp make-NonSexp NonSexp? NonSexp-ref)
(define-values (struct:NonSexp make-NonSexp NonSexp? NonSexp-ref NonSexp-set!)
(make-struct-type 'NonSexp ;; name
#f ;; parent
1 ;; arguments to the constructor
0 ;; auto-fields
#f ;; auto-v
'() ;; props
#f ;; inspector
#f ;; proc-spec
(list 0) ;; immutables
#f ;; guard
'NonSexp ;; constructor-name
))
(#%provide struct:NonSyntax make-NonSyntax NonSyntax? NonSyntax-ref)
(define-values (struct:NonSyntax make-NonSyntax NonSyntax? NonSyntax-ref NonSyntax-set!)
(make-struct-type 'NonSyntax ;; name
#f ;; parent
1 ;; arguments to the constructor
0 ;; auto-fields
#f ;; auto-v
'() ;; props
#f ;; inspector
#f ;; proc-spec
(list 0) ;; immutables
#f ;; guard
'NonSyntax ;; constructor-name
))
(#%provide struct:Some make-Some Some? Some-ref)
(define-values (struct:Some make-Some Some? Some-ref Some-set!)
(make-struct-type 'Some ;; name
#f ;; parent
1 ;; arguments to the constructor
0 ;; auto-fields
#f ;; auto-v
'() ;; props
#f ;; inspector
#f ;; proc-spec
(list 0) ;; immutables
#f ;; guard
'Some ;; constructor-name
)))

31
comments/typed-pairof-predicate.rkt Normal file
View File

@ -0,0 +1,31 @@
#lang typed/racket
(provide pairof?)
(require typed/racket/unsafe)
(unsafe-require/typed racket/function
[[identity unsafe-cast-function] (∀ (A) (→ Any A))])
(define-syntax-rule (unsafe-cast v t)
((inst unsafe-cast-function t) v))
(: pairof?* (∀ (A D) (→ Any
(→ Any Boolean : A)
(→ Any Boolean : D)
Boolean)))
(define (pairof?* v a? d?)
(and (pair? v)
(a? (car v))
(d? (cdr v))))
(define pairof?
;; Circumvent https://github.com/racket/typed-racket/issues/429
(unsafe-cast pairof?*
(∀ (A D) (→ Any
(→ Any Boolean : A)
(→ Any Boolean : D)
Boolean
:
;; Circumvent
;; https://github.com/racket/typed-racket/issues/488
#:+ (Pairof A D)
#:- (! (Pairof A D))))))

35
comments/typed-prefab-declarations.rkt Normal file
View File

@ -0,0 +1,35 @@
#lang typed/racket
(struct (A) NonSexp ([v : A]) #:type-name NonSexpOf)
(struct (A) NonSyntax ([v : A]) #:type-name NonSyntaxOf)
(struct (A) Some ([v : A]))
(define-type (Maybe A)
(U (Some A) #f))
(provide (struct-out NonSexp) NonSexpOf
(struct-out NonSyntax) NonSyntaxOf
(struct-out Some)
Maybe)
(module* test typed/racket
(require (submod ".."))
(require typed/rackunit)
(check-pred procedure? NonSexp)
(check-pred NonSexp? (ann (ann (NonSexp 1) (NonSexpOf Number)) Any))
(check-not-exn
(λ ()
(ann (let ([n : (NonSexpOf Any) (NonSexp 1)])
(if (number? (NonSexp-v n))
(NonSexp-v n)
0))
Number)))
(check-not-exn
(λ ()
(ann (let ([n : Any (NonSexp 1)])
(if (NonSexp? n)
(if (number? (NonSexp-v n))
(NonSexp-v n)
2)
0))
Number))))

16
comments/typed-syntax-convert.rkt
View File

@ -1,12 +1,12 @@
#lang typed/racket
(require typed-map
typed/racket/unsafe)
typed/racket/unsafe
"typed-prefab-declarations.rkt")
(provide try-any->isexp*
try-any->isexp
any->isexp+non-sexp
(struct-out NonSexp))
any->isexp+non-sexp)
(unsafe-require/typed racket/function
[[identity unsafe-cast-function] (∀ (A) (→ Any A))])
@ -102,10 +102,6 @@
(non-sexp e)]))
;; Sexp:
(struct (A) NonSexp ([value : A]) #:type-name NonSexpOf)
(: any->isexp+non-sexp (→ Any (Sexpof (NonSexpOf Any))))
(define (any->isexp+non-sexp e)
(let*-values ([(e* status) (try-any->isexp*
@ -122,13 +118,13 @@
" not return #f."))])))
(: try-any->isexp (→ Any (U (List Any) #f)))
(: try-any->isexp (→ Any (Maybe Sexp)))
(define (try-any->isexp e)
(let*-values ([(e* status) (try-any->isexp*
e
(λ (non-sexp-e)
(values #f #f)))])
(case status
[(unmodified) (list e)]
[(modified) (list e*)]
[(unmodified) (Some (unsafe-cast e Sexp))]
[(modified) (Some e*)]
[(#f) #f])))

51
comments/typed-syntax-convert2.rkt
View File

@ -2,8 +2,8 @@
(require typed-map
typed/racket/unsafe
"typed-syntax-convert.rkt"
"maybe.rkt")
"typed-prefab-declarations.rkt")
(unsafe-require/typed racket/base
[[datum->syntax datum->syntax*]
(∀ (A) (→ (Syntaxof Any)
@ -18,16 +18,14 @@
ISyntax-E
ISyntax/Non
ISyntax/Non-E
(struct-out NonSyntax)
;(struct-out NonSexp) ; already exported in typed-syntax-convert.rkt
NonSyntaxOf
NonSexpOf
any->isyntax+non
syntax->isyntax+non
any->isyntax-e+non
any->isyntax/non
syntax->isyntax/non
any->isyntax/non-e
try-any->isyntax
try-syntax->isyntax
try-any->isyntax-e)
try-any->isyntax-e
isyntax?
isyntax-e?)
(unsafe-require/typed racket/function
[[identity unsafe-cast-function] (∀ (A) (→ Any A))])
@ -68,9 +66,6 @@
(Pairof (ISyntaxOf A B) L))))
(Vectorof (ISyntaxOf A B))))
(struct (A) NonSyntax ([value : A]) #:type-name NonSyntaxOf)
(struct (A) NonSexp ([value : A]) #:type-name NonSexpOf)
(define-type ISyntax/Non (ISyntaxOf (NonSyntaxOf Any) (NonSexpOf Any)))
(define-type ISyntax/Non-E (ISyntaxOf-E (NonSyntaxOf Any) (NonSexpOf Any)))
@ -254,8 +249,8 @@
[else
(nsexp e)]))
(: any->isyntax+non (→ Any ISyntax/Non))
(define (any->isyntax+non e)
(: any->isyntax/non (→ Any ISyntax/Non))
(define (any->isyntax/non e)
(define e*+status
(any->isyntax* e
(λ (n) (cons (NonSyntax n) 'modified))
@ -264,8 +259,8 @@
(car e*+status)
(error "Got #f from any->isyntax* with handlers not returning #f")))
(: syntax->isyntax+non (→ (Syntaxof Any) (Syntaxof ISyntax/Non-E)))
(define (syntax->isyntax+non stx)
(: syntax->isyntax/non (→ (Syntaxof Any) (Syntaxof ISyntax/Non-E)))
(define (syntax->isyntax/non stx)
(define e*+status
(syntax->isyntax* stx
(λ (n) (cons (NonSyntax n) 'modified))
@ -274,8 +269,8 @@
(car e*+status)
(error "Got #f from any->isyntax* with handlers not returning #f")))
(: any->isyntax-e+non (→ Any ISyntax/Non-E))
(define (any->isyntax-e+non e)
(: any->isyntax/non-e (→ Any ISyntax/Non-E))
(define (any->isyntax/non-e e)
(define e*+status
(any->isyntax-e* e
(λ (n) (cons (NonSyntax n) 'modified))
@ -313,3 +308,21 @@
(if (cdr e*+status)
(Some (car e*+status))
#f))
(define isyntax?
(unsafe-cast (λ ([e : Any]) : Boolean
(define e*+status
((inst any->isyntax* Nothing Nothing) e
(λ (n) Result#f)
(λ (n) Result#f)))
(eq? (cdr e*+status) 'unmodified))
(→ Any Boolean : ISyntax)))
(define isyntax-e?
(unsafe-cast (λ ([e : Any]) : Boolean
(define e*+status
((inst any->isyntax-e* Nothing Nothing) e
(λ (n) Result#f)
(λ (n) Result#f)))
(eq? (cdr e*+status) 'unmodified))
(→ Any Boolean : ISyntax-E)))

19
comments/typed-syntax.rkt
View File

@ -4,19 +4,26 @@
try-any->isexp
any->isexp+non-sexp
CoreSexp
isyntax?
isyntax-e?
ISyntax
ISyntax-E
ISyntaxOf
ISyntaxOf-E
ISyntax/Non
ISyntax/Non-E
NonSyntaxOf
NonSexpOf
any->isyntax ;; TODO: make wrappers for these, which discard the second value
syntax->isyntax
any->isyntax-e)
any->isyntax/non
syntax->isyntax/non
any->isyntax/non-e
try-any->isyntax
try-syntax->isyntax
try-any->isyntax-e
NonSexp NonSexp? NonSexp-v NonSexpOf
NonSyntax NonSyntax? NonSyntax-v NonSyntaxOf
Some Some? Some-v)
(require "typed-syntax-convert.rkt"
"typed-syntax-convert2.rkt"
"typed-syntax-predicate.rkt")
"typed-syntax-predicate.rkt"
"typed-prefab-declarations.rkt")

48
comments/untyped-cross-phase-structs-wrappers.rkt
View File

@ -1,48 +0,0 @@
#lang racket
(require "typed-cross-phase-structs.rkt"
(for-syntax racket/struct-info))
(define-syntax-rule (define+provide-struct-wrapper-single-field
[struct:S make-S S? S-ref S field S-field S-struct-info]
...)
(begin
(begin
(provide (struct-out S))
(define S-field
(values (make-struct-field-accessor S-ref 0 'field)))
(begin-for-syntax
(struct S-struct-info ()
#:transparent
#:property prop:struct-info
(λ (self)
(list #'struct:S
#'make-S
#'S?
(list #'S-field) ;; in reverse order
(list #f) ;; in reverse order
#t))
#:property prop:set!-transformer
(lambda (stx)
(syntax-case stx (set!)
[(set! id _)
(raise-syntax-error 'set! "Cannot mutate struct identifier" stx)]
[id
(identifier? #'id)
#'make-S]
[(id . args)
(identifier? #'id)
(syntax/loc stx
(make-S . args))]))))
(define-syntax S (S-struct-info)))
...))
(define+provide-struct-wrapper-single-field
[struct:NonSexp make-NonSexp NonSexp? NonSexp-ref
NonSexp v NonSexp-v NonSexp-struct-info]
[struct:NonSyntax make-NonSyntax NonSyntax? NonSyntax-ref
NonSyntax v NonSyntax-v NonSyntax-struct-info]
[struct:Some make-Some Some? Some-ref
Some v Some-v Some-struct-info])