diff --git a/info.rkt b/info.rkt index 7c2fc19..8c3f0da 100644 --- a/info.rkt +++ b/info.rkt @@ -3,7 +3,8 @@ (define deps '("base" "rackunit-lib" "typed-racket-lib" - "typed-racket-more")) + "typed-racket-more" + "typed-map")) (define build-deps '("scribble-lib" "racket-doc" "typed-racket-doc")) diff --git a/typed-syntax.rkt b/typed-syntax.rkt new file mode 100644 index 0000000..a6cefe7 --- /dev/null +++ b/typed-syntax.rkt @@ -0,0 +1,32 @@ +#lang typed/racket + +(provide isexp? + Sexp/Non + try-any->isexp + any->isexp/non + CoreSexp + isyntax? + isyntax-e? + ISyntax + ISyntax-E + ISyntaxOf + ISyntaxOf-E + ISyntax/Non + ISyntax/Non-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 + pairof?) + +(require "typed-syntax/typed-syntax-convert.rkt" + "typed-syntax/typed-syntax-convert2.rkt" + "typed-syntax/typed-syntax-predicate.rkt" + "typed-syntax/typed-prefab-declarations.rkt" + "typed-syntax/typed-pairof-predicate.rkt") + diff --git a/typed-syntax/typed-pairof-predicate.rkt b/typed-syntax/typed-pairof-predicate.rkt new file mode 100644 index 0000000..6ca7489 --- /dev/null +++ b/typed-syntax/typed-pairof-predicate.rkt @@ -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)))))) \ No newline at end of file diff --git a/typed-syntax/typed-prefab-declarations.rkt b/typed-syntax/typed-prefab-declarations.rkt new file mode 100644 index 0000000..439ad14 --- /dev/null +++ b/typed-syntax/typed-prefab-declarations.rkt @@ -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)))) \ No newline at end of file diff --git a/typed-syntax/typed-syntax-convert.rkt b/typed-syntax/typed-syntax-convert.rkt new file mode 100644 index 0000000..a6f13d1 --- /dev/null +++ b/typed-syntax/typed-syntax-convert.rkt @@ -0,0 +1,133 @@ +#lang typed/racket + +(require typed-map + typed/racket/unsafe + "typed-prefab-declarations.rkt") + +(provide try-any->isexp* + try-any->isexp + any->isexp/non + Sexp/Non) + +(define-type Sexp/Non (Sexpof (NonSexpOf Any))) + +(unsafe-require/typed racket/function + [[identity unsafe-cast-function] (∀ (A) (→ Any A))]) +(unsafe-require/typed racket/base + [[datum->syntax datum->syntax*] + (∀ (A) (→ (Syntaxof Any) + A + (Syntaxof Any) + (Syntaxof Any) + (Syntaxof A)))]) + +(define-syntax-rule (unsafe-cast v t) + ((inst unsafe-cast-function t) v)) + +(define-type (non-sexp-handler A) + (→ Any + (Values (U (Sexpof A) #f) + (U 'unmodified 'modified #f)))) + +(: try-listof-any->isexp* (∀ (A) (→ (Listof Any) + (non-sexp-handler A) + (U (Pairof (Listof (Sexpof A)) + (U 'unmodified 'modified)) + (Pairof #f #f))))) + +(define (try-listof-any->isexp* e non-sexp) + (define e+status* + (map (λ ([eᵢ : Any]) + (let-values ([(eᵢ* status) (try-any->isexp* eᵢ non-sexp)]) + (cons eᵢ* status))) + e)) + (define e* (map car e+status*)) + (define status* (map cdr e+status*)) + (cond + [(andmap (curry eq? 'unmodified) status*) + (cons (unsafe-cast e (Listof (Sexpof A))) 'unmodified)] + [(ormap (curry eq? #f) status*) + (cons #f #f)] + [else + (cons e* 'modified)])) + +(: try-any->isexp* (∀ (A) (→ Any + (non-sexp-handler A) + (Values (U (Sexpof A) #f) + (U 'unmodified 'modified #f))))) +(define (try-any->isexp* e non-sexp) + (cond + [(boolean? e) (values e 'unmodified)] + [(char? e) (values e 'unmodified)] + [(number? e) (values e 'unmodified)] + [(keyword? e) (values e 'unmodified)] + [(null? e) (values e 'unmodified)] + [(string? e) (if (immutable? e) + (values e 'unmodified) + (values (string->immutable-string e) 'modified))] + [(symbol? e) (values e 'unmodified)] + [(box? e) (let*-values ([(u) (unbox e)] + [(u* status) (try-any->isexp* e non-sexp)]) + (case status + [(unmodified) + (if (immutable? e) + (values (unsafe-cast e (Sexpof A)) 'unmodified) + (values (box-immutable u*) 'modified))] + [(modified) + (values (box-immutable u*) 'modified)] + [(#f) + (values #f #f)]))] + [(pair? e) (let*-values ([(car* status-car) + (try-any->isexp* (car e) non-sexp)] + [(cdr* status-cdr) + (try-any->isexp* (cdr e) non-sexp)]) + (cond + [(and (eq? status-car 'unmodified) + (eq? status-cdr 'unmodified)) + (values (unsafe-cast e (Sexpof A)) 'unmodified)] + [(or (eq? status-car #f) + (eq? status-cdr #f)) + (values #f #f)] + [else + (values (cons car* cdr*) 'modified)]))] + [(vector? e) (match-let ([(cons vs* status) + (try-listof-any->isexp* (vector->list e) non-sexp)]) + (case status + [(unmodified) + (if (immutable? e) + (values (unsafe-cast e (Sexpof A)) 'unmodified) + (values (apply vector-immutable vs*) 'modified))] + [(modified) + (values (apply vector-immutable vs*) 'modified)] + [(#f) + (values #f #f)]))] + [else + (non-sexp e)])) + + +(: any->isexp/non (→ Any (Sexpof (NonSexpOf Any)))) +(define (any->isexp/non e) + (let*-values ([(e* status) (try-any->isexp* + e + (λ (non-sexp-e) + (values (NonSexp non-sexp-e) + 'modified)))]) + (case status + [(unmodified) (unsafe-cast e (Sexpof (NonSexpOf Any)))] + [(modified) e*] + [(#f) + (error + (string-append "Got #f from try->any-isexp* using non-sexp which does" + " not return #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) (Some (unsafe-cast e Sexp))] + [(modified) (Some e*)] + [(#f) #f]))) diff --git a/typed-syntax/typed-syntax-convert2.rkt b/typed-syntax/typed-syntax-convert2.rkt new file mode 100644 index 0000000..9568fb8 --- /dev/null +++ b/typed-syntax/typed-syntax-convert2.rkt @@ -0,0 +1,328 @@ +#lang typed/racket + +(require typed-map + typed/racket/unsafe + "typed-prefab-declarations.rkt") + +(unsafe-require/typed racket/base + [[datum->syntax datum->syntax*] + (∀ (A) (→ (Syntaxof Any) + A + (Syntaxof Any) + (Syntaxof Any) + (Syntaxof A)))]) + +(provide ISyntaxOf + ISyntaxOf-E + ISyntax + ISyntax-E + ISyntax/Non + ISyntax/Non-E + any->isyntax/non + syntax->isyntax/non + any->isyntax/non-e + try-any->isyntax + try-syntax->isyntax + try-any->isyntax-e + isyntax? + isyntax-e?) + +(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)) + +(define-type (ISyntaxOf A B) + (Rec + stx + (U A + (Syntaxof + (U B + Boolean + Char + Complex + Keyword + String + Symbol + (Boxof stx) + Null + (Pairof stx (Rec L (U Null + stx + (Pairof stx L)))) + (Vectorof stx)))))) + +(define-type (ISyntaxOf-E A B) + (U B + Boolean + Char + Complex + Keyword + String + Symbol + (Boxof (ISyntaxOf A B)) + Null + (Pairof (ISyntaxOf A B) (Rec L (U Null + (ISyntaxOf A B) + (Pairof (ISyntaxOf A B) L)))) + (Vectorof (ISyntaxOf A B)))) + +(define-type ISyntax/Non (ISyntaxOf (NonSyntaxOf Any) (NonSexpOf Any))) +(define-type ISyntax/Non-E (ISyntaxOf-E (NonSyntaxOf Any) (NonSexpOf Any))) + +(define-type ISyntax (ISyntaxOf Nothing Nothing)) +(define-type ISyntax-E (ISyntaxOf-E Nothing Nothing)) + +(define-type (Result A) (U (Pairof A (U 'modified 'unmodified)) + (Pairof #f #f))) +(define Result#f (cons #f #f)) + +(: syntax->isyntax* (∀ (A B) (→ (Syntaxof Any) + (→ Any (Result A)) + (→ Any (Result B)) + (U (Result (Syntaxof (ISyntaxOf-E A B))))))) +(define (syntax->isyntax* stx nstx nsexp) + (define e (syntax-e stx)) + (match-define (cons e* status) (any->isyntax-e* e nstx nsexp)) + (case status + [(unmodified) + (cons (unsafe-cast e (Syntaxof (ISyntaxOf-E A B))) 'unmodified)] + [(modified) + (cons (datum->syntax* stx e* stx stx) 'modified)] + [(#f) + Result#f])) + +(: any->isyntax* (∀ (A B) (→ Any + (→ Any (Result A)) + (→ Any (Result B)) + (Result (ISyntaxOf A B))))) +(define (any->isyntax* e nstx nsexp) + (if (syntax? e) + (syntax->isyntax* e nstx nsexp) + (nstx e))) + +(: listof-any->listof-isyntax + (∀ (A B) (→ (Listof Any) + (→ Any (Result A)) + (→ Any (Result B)) + (Result (Listof (ISyntaxOf A B)))))) +(define (listof-any->listof-isyntax e nstx nsexp) + (define e*+status + (foldr (λ ([eᵢ : Any] [acc : (Result (Listof (ISyntaxOf A B)))]) + (match-let ([(cons eᵢ* status) (any->isyntax* eᵢ nstx nsexp)]) + (cond + [(and (eq? status 'unmodified) + (eq? (cdr acc) 'unmodified)) + (cons (cons eᵢ* (car acc)) 'unmodified)] + [(or (eq? status #f) + (eq? (cdr acc) #f)) + Result#f] + [else + (cons (cons eᵢ* (car acc)) 'modified)]))) + (cons '() 'unmodified) + e)) + (define e* (car e*+status)) + (define status (cdr e*+status)) + (case status + [(unmodified) (cons (unsafe-cast e (Listof (ISyntaxOf A B))) 'unmodified)] + [(modified) (cons e* 'modified)] + [(#f) Result#f])) + +#;(: handle-pair (case→ (→ (Listof Any) + (Values (Listof Syntax-E) + (U 'unmodified 'modified))) + (→ (Pairof Any (Rec L (U Any (Pairof Any L)))) + (Values (Pairof Syntax-E + (Rec L (U Syntax-E + (Pairof Syntax-E L)))) + (U 'unmodified 'modified))) + (→ Any + (Values ISyntax + (U 'unmodified 'modified))))) +#;(: handle-pair (case→ (→ (Pairof Any (Listof Any)) + (Values (Listof Syntax-E) + (U 'unmodified 'modified))) + (→ (Pairof Any (Rec L (U Any (Pairof Any L)))) + (Values (Pairof Syntax-E + (Rec L (U Syntax-E + (Pairof Syntax-E L)))) + (U 'unmodified 'modified))))) +(: handle-pair (∀ (A B) (→ (U (Pairof Any (Listof Any)) + (Pairof Any (Rec L (U Any (Pairof Any L))))) + (→ Any (Result A)) + (→ Any (Result B)) + (Result (Pairof (ISyntaxOf A B) + (Rec L (U (ISyntaxOf A B) + Null + (Pairof (ISyntaxOf A B) + L)))))))) +(define (handle-pair e nstx nsexp) + (define car*+status (any->isyntax* (car e) nstx nsexp)) + (define car* (car car*+status)) + (define status-car (cdr car*+status)) + (cond + [(pair? (cdr e)) + (match-let ([(cons cdr* status-cdr) + (handle-pair (cdr e) nstx nsexp)]) + (cond + #;[(and (eq? status-car 'unmodified) + (eq? status-cdr 'unmodified)) + (cons (unsafe-cast e (Pairof ISyntax + (Rec L (U ISyntax + Null + (Pairof ISyntax L))))) + 'unmodified)] + [(or (eq? status-car #f) + (eq? status-cdr #f)) + Result#f] + [else + (cons (cons car* cdr*) 'modified)]))] + [(null? (cdr e)) + (cond + #;[(eq? status-car 'unmodified) + (cons (unsafe-cast e (Pairof ISyntax Null)) 'unmodified)] + [(eq? status-car #f) + Result#f] + [else + (cons (ann (cons car* (cdr e)) + (Pairof (ISyntaxOf A B) + (Rec L (U (ISyntaxOf A B) + Null + (Pairof (ISyntaxOf A B) + L))))) + 'modified)])] + [else + (match-let ([(cons cdr* status-cdr) (any->isyntax* (cdr e) nstx nsexp)]) + (cond + #;[(and (eq? status-car 'unmodified) + (eq? status-cdr 'unmodified)) + (cons (unsafe-cast e (Pairof ISyntax + (Rec L (U ISyntax + Null + (Pairof ISyntax L))))) + 'unmodified)] + [(or (eq? status-car #f) + (eq? status-cdr #f)) + Result#f] + [else + (cons (cons car* cdr*) 'modified)]))])) + +(: any->isyntax-e* (∀ (A B) (→ Any + (→ Any (Result A)) + (→ Any (Result B)) + (Result (ISyntaxOf-E A B))))) +(define (any->isyntax-e* e nstx nsexp) + (cond + [(boolean? e) (cons e 'unmodified)] + [(char? e) (cons e 'unmodified)] + [(number? e) (cons e 'unmodified)] + [(keyword? e) (cons e 'unmodified)] + [(null? e) (cons e 'unmodified)] + [(string? e) (if (immutable? e) + (cons e 'unmodified) + (cons (string->immutable-string e) 'modified))] + [(symbol? e) (cons e 'unmodified)] + [(box? e) (match-let ([(cons u* status) (any->isyntax* (unbox e) nstx nsexp)]) + (case status + [(unmodified) + ;(if (immutable? e) + ;(values (unsafe-cast e (Sexpof A)) 'unmodified) + (cons (box-immutable u*) 'modified);) + ] + [(modified) + (cons (box-immutable u*) 'modified)] + [(#f) + Result#f]))] + [(pair? e) (handle-pair e nstx nsexp)] + [(vector? e) (match-let ([(cons vs* status) + (listof-any->listof-isyntax (vector->list e) nstx nsexp)]) + (case status + [(unmodified) + (if (immutable? e) + (cons (unsafe-cast e (ISyntaxOf-E A B)) + 'unmodified) + (cons (apply vector-immutable vs*) + 'modified))] + [(modified) + (cons (apply vector-immutable vs*) 'modified)] + [(#f) + Result#f]))] + [else + (nsexp e)])) + +(: any->isyntax/non (→ Any ISyntax/Non)) +(define (any->isyntax/non e) + (define e*+status + (any->isyntax* e + (λ (n) (cons (NonSyntax n) 'modified)) + (λ (n) (cons (NonSexp n) 'modified)))) + (if (cdr e*+status) + (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) + (define e*+status + (syntax->isyntax* stx + (λ (n) (cons (NonSyntax n) 'modified)) + (λ (n) (cons (NonSexp n) 'modified)))) + (if (cdr e*+status) + (car e*+status) + (error "Got #f from any->isyntax* with handlers not returning #f"))) + +(: 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)) + (λ (n) (cons (NonSexp n) 'modified)))) + (if (cdr e*+status) + (car e*+status) + (error "Got #f from any->isyntax* with handlers not returning #f"))) + +(: try-any->isyntax (→ Any (Maybe ISyntax))) +(define (try-any->isyntax e) + (define e*+status + ((inst any->isyntax* Nothing Nothing) e + (λ (n) Result#f) + (λ (n) Result#f))) + (if (cdr e*+status) + (Some (car e*+status)) + #f)) + +(: try-syntax->isyntax (→ (Syntaxof Any) (Maybe (Syntaxof ISyntax-E)))) +(define (try-syntax->isyntax stx) + (define e*+status + ((inst syntax->isyntax* Nothing Nothing) stx + (λ (n) Result#f) + (λ (n) Result#f))) + (if (cdr e*+status) + (Some (car e*+status)) + #f)) + +(: try-any->isyntax-e (→ Any (Maybe ISyntax-E))) +(define (try-any->isyntax-e e) + (define e*+status + ((inst any->isyntax-e* Nothing Nothing) e + (λ (n) Result#f) + (λ (n) Result#f))) + (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))) \ No newline at end of file diff --git a/typed-syntax/typed-syntax-predicate.rkt b/typed-syntax/typed-syntax-predicate.rkt new file mode 100644 index 0000000..132fd5b --- /dev/null +++ b/typed-syntax/typed-syntax-predicate.rkt @@ -0,0 +1,52 @@ +#lang typed/racket + +(provide isexp? + CoreSexp) + +(module unsafe racket + (provide isexp?) + + (define isexp/c + (flat-rec-contract isexp + (or/c boolean? + char? + number? + keyword? + null? + (and/c string? immutable?) + symbol? + (box/c isexp #:immutable #t) + (cons/c isexp isexp) + (vectorof isexp #:immutable #t)))) + + (define sexp/c + (recursive-contract + (or/c boolean? + char? + number? + keyword? + null? + string? + symbol? + (box/c sexp/c) + (cons/c sexp/c sexp/c) + (vectorof sexp/c)))) + + (define isexp? + (flat-contract-predicate isexp/c))) + +(define-type CoreSexp (Rec core-sexp + (U Boolean + Char + Number + Keyword + Null + String + Symbol + #|(Boxof sexp)|# + (Pairof core-sexp core-sexp) + #|(Vectorof sexp)|#))) + +(require typed/racket/unsafe) +(unsafe-require/typed 'unsafe + [isexp? (→ Any Boolean : #:+ Sexp #:- (! CoreSexp))]) \ No newline at end of file