commit 61c290d1ecd1737d8c0dee9a965f817880396bfc
parent 6ad729b1ef8e17afc22544f3c2e12dd2ec9a1a55
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Sat, 9 Sep 2017 12:20:23 +0200
Added record types where the order of fields is irrelevant.
Diffstat:
10 files changed, 319 insertions(+), 42 deletions(-)
diff --git a/aliases.rkt b/aliases.rkt
@@ -0,0 +1,8 @@
+#lang racket
+(provide … ∘)
+
+(require (only-in (only-meta-in 0 racket/base)
+ [... …]
+ [compose ∘])
+ racket/syntax)
+
diff --git a/info.rkt b/info.rkt
@@ -1,9 +1,15 @@
#lang info
(define collection "phc-ts")
(define deps '("base" ;; ("base" "6.4")
- "rackunit-lib"))
+ "rackunit-lib"
+ "reprovide-lang"
+ "dotlambda"
+ "hyper-literate"
+ "phc-toolkit"
+ "turnstile"))
(define build-deps '("scribble-lib"
- "racket-doc"))
+ "racket-doc"
+ "scribble-enhanced"))
(define scribblings '(("scribblings/phc-ts.scrbl" ())))
(define pkg-desc "")
(define version "0.0")
diff --git a/main.rkt b/main.rkt
@@ -1,14 +1,129 @@
-#lang hyper-literate #:no-auto-require(dotlambda/unhygienic . typed/racket/base)
+#lang hyper-literate #:no-auto-require (dotlambda/unhygienic . turnstile/lang)
-@(require (for-label typed/racket/base))
+@(define (turnstile) @racketmodname[turnstile])
-@section{Conclusion}
+@(require racket/require
+ (for-label (prefix-in host: (only-meta-in 0 turnstile/lang))
+ (prefix-in host:
+ (subtract-in (only-meta-in 1 turnstile/lang)
+ (only-meta-in 0 turnstile/lang)))
+ turnstile/examples/mlish))
+
+@section{Introduction}
+
+We define our type system as an extension to another language. We could extend
+one of the many sufficiently capable languages built with @turnstile[]. Here,
+we will base ourselves on @racketmodname[mlish], a ml-like language
+implemented with @turnstile[], and provided as part of @turnstile[]'s suite of
+examples.
@chunk[<*>
- (provide
- ;; description
- #;id)
+ (extends turnstile/examples/mlish)]
+
+Since @racketmodname[turnstile/examples/mlish] provides some identifiers which
+conflict with some racket utilities, we import those with a prefix.
+
+@chunk[<*>
+ (require racket/require
+ (prefix-in host: turnstile/lang)
+ (for-syntax "aliases.rkt")
+ (for-syntax "stx-sort.rkt")
+ (for-meta 2 syntax/stx)
+ (for-meta 2 "stx-sort.rkt")
+ (for-meta 2 "aliases.rkt"))]
+
+We define a @racket[Record] type, in which the order of fields is irrelevant.
+
+@CHUNK[<*>
+ ;;(host:provide (type-out Record))
+ (host:provide Record (for-syntax ~Record))
+
+ (define-type-constructor Record* #:arity >= 0
+ #:arg-variances λstx.(make-list (sub1 (stx-length stx)) covariant))
+
+ (define-type-constructor Field* #:arity = 2
+ #:arg-variances λstx.(make-list (sub1 (stx-length stx)) covariant))
+
+ (define-syntax (Field stx)
+ (syntax-case stx ()
+ [(_ ℓ τ) #`(Field* #,(mk-type #'(quote ℓ)) τ)]))
- (require (for-syntax racket/base))
+ (define-syntax Record
+ (syntax-parser
+ [(_ {~sort-seq [{~key ℓ:id} {~literal :} τ] …})
+ #'(Record* [Field ℓ τ] …)]))
+
+ (begin-for-syntax
+ (define-syntax ~Field
+ (pattern-expander
+ (λ (stx)
+ (syntax-case stx ()
+ [(_ ℓ τ)
+ #'[~Field* ({~literal quote} ℓ) τ]]))))
+
+ (define-syntax ~Record
+ (pattern-expander
+ (syntax-parser
+ [(_ [ℓ {~literal :} τ] {~datum ⊤ρ}) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+ #'(~Record* _ (… …) [~Field ℓ τ] _ (… …))]
+ [(_ {~sort-seq [{~key ℓ} {~literal :} τ] …})
+ #'(~Record* [~Field ℓ τ] …)]))))]
+
+The builder form for the @racket[Record] type is @racket[record].
- #;(define id …)]
+@chunk[<*>
+ (host:provide record)
+ (define-typed-syntax
+ (record [ℓ:id {~literal =} e] …) ≫
+ [⊢ e ≫ e- ⇒ τ] …
+ #:with (tmp …) (generate-temporaries #'(e …))
+ #:with (~sort [{~key sorted-ℓ} sorted-τ sorted-tmp] …) #'([ℓ τ tmp] …)
+ --------
+ [⊢ (let ([tmp e] …)
+ (list- (list- 'sorted-ℓ sorted-tmp) …))
+ ⇒ (Record [sorted-ℓ : sorted-τ] …)])]
+
+Fields can be accessed via the @racket[getfield] operator. The @racket[i.ℓ]
+notation will later be introduced, and will reduce to @racket[(getfield i ℓ)].
+
+@chunk[<*>
+ (host:provide getfield)
+ (require (for-syntax "same-id-pattern.rkt"))
+ (define-typed-syntax
+ (getfield ℓ:id e) ≫
+ [⊢ e ≫ e- ⇒ {~or {~Record [{~same-free-id ℓ} : τ] ⊤ρ} <record-err-ℓ>}]
+ --------
+ [⊢ (car- (assoc- 'ℓ e-)) ⇒ τ])]
+
+@chunk[<record-err-ℓ>
+ {~and
+ other
+ {~do (type-error
+ #:src #'other
+ #:msg "expected record type containing the field ~a, got: ~a"
+ #'ℓ #'other)}}]
+
+@chunk[<*>
+ (host:provide :)
+ (define-syntax (: stx)
+ (raise-syntax-error ': "Invalid use of token" stx))]
+
+We define a quick and dirty @racket[:type] operator, which can be used to
+print the type of an expression. For now, we simply trigger an error message
+which should contain the inferred type, unless the type of @racket[e] is an
+@racket[Int].
+
+@chunk[<*>
+ (host:provide :type)
+ (require syntax/macro-testing)
+ (define ann/:type-regexp
+ #px"ann: type mismatch: expected Int, given (.*)\n expression:")
+ (define-syntax-rule (:type e)
+ (with-handlers ([(λ (exn) #true)
+ (λ (exn)
+ (displayln
+ (cadr (regexp-match ann/:type-regexp
+ (exn-message exn)))))])
+ (convert-compile-time-error (ann e : Int))))]
+
+@section{Conclusion}
diff --git a/same-id-pattern.rkt b/same-id-pattern.rkt
@@ -0,0 +1,15 @@
+#lang racket
+(provide ~same-free-id)
+
+(require syntax/parse)
+
+(define-splicing-syntax-class (same-free-id f)
+ #:description (format "the identifier ~a"
+ (syntax-e f))
+ (pattern x #:when (and (identifier? #'x) (free-identifier=? #'x f))))
+
+(define-syntax ~same-free-id
+ (pattern-expander
+ (λ (stx)
+ (syntax-case stx ()
+ [(_ pvar) (identifier? #'pvar) #'{~var || (same-free-id #'pvar)}]))))
diff --git a/scribblings/phc-ts.scrbl b/scribblings/phc-ts.scrbl
@@ -0,0 +1,33 @@
+#lang scribble/manual
+@require[@for-label[phc-ts]
+ (for-syntax racket/base)]
+
+@title{phc-ts}
+@author[@author+email["Georges Dupéron" "georges.duperon@gmail.com"]]
+
+@defmodule[phc-ts]
+
+There is no documentation for this package yet.
+
+@(define-syntax (show-ids stx)
+ (syntax-case stx ()
+ [(_ b)
+ (boolean? (syntax-e #'b))
+ (let-values ([(vars stx-vars) (module->exports 'phc-ts)])
+ #`(itemlist
+ #,@(for*/list ([phase+ids (in-list (if (syntax-e #'b)
+ vars
+ stx-vars))]
+ [phase (in-value (car phase+ids))]
+ [id (in-list (cdr phase+ids))])
+ #`(item (racketid #,id)
+ "at phase"
+ #,(number->string phase)))))]))
+
+The following variables are provided:
+
+@(show-ids #t)
+
+The following syntaxes are provided:
+
+@(show-ids #f)
+\ No newline at end of file
diff --git a/scribblings/travis-skeleton.scrbl b/scribblings/travis-skeleton.scrbl
@@ -1,31 +0,0 @@
-#lang scribble/manual
-@require[@for-label[phc-ts
- racket/base]]
-
-@title{phc-ts}
-@author[@author+email["Georges Dupéron" "georges.duperon@gmail.com"]]
-
-@defmodule[phc-ts]
-
-There is no documentation for this package yet.
-
-@(define-syntax (show-ids _stx)
- (syntax-case stx ()
- [(_ b)
- (boolean? (syntax-e #'b))
- (let-values ([(vars stx-vars) (module->exports phc-ts)])
- #`(itemlist
- #,(for*/list ([phase+ids (in-list (if (syntax-e #'b) vars stx-vars))]
- [phase (in-value (car phase+ids))]
- [id (in-list (cdr phase+ids))])
- #`(item (racketit #,id)
- "at phase"
- #,(number->string phase)))))]))
-
-The following variables are provided:
-
-@(show-ids #t)
-
-The following syntaxes are provided:
-
-@(show-ids #f)
-\ No newline at end of file
diff --git a/stx-sort.rkt b/stx-sort.rkt
@@ -0,0 +1,84 @@
+#lang racket
+
+(provide ~sort
+ ~sort-seq
+ ~key)
+
+;; Note: when using nested ~sort, the inner sort is not performed during the
+;; first pass for the outer ~sort. Once the values for the outer ~sort have been
+;; gathered and sorted, then the innder ~sort is applied. This means that the
+;; comparison operator for the outer ~sort should work with unsorted
+;; sub-sequences.s
+
+(require syntax/parse
+ "aliases.rkt"
+ syntax/stx
+ racket/stxparam
+ (for-syntax racket/syntax))
+
+(define-for-syntax sort-scope (make-syntax-introducer))
+(define-syntax-parameter current-key-id #f)
+
+(define-for-syntax (~sort-ish op*)
+ (pattern-expander
+ (λ (stx)
+ (syntax-case stx (…)
+ [(self pat …)
+ (if (syntax-parameter-value #'current-key-id)
+ #`(#,@op* _ …)
+ #`(~and (#,@op* tmp …)
+ (~parse (pat …)
+ (sort/stx self #'(tmp …) pat))))]))))
+(define-syntax ~sort (~sort-ish #'{}))
+
+(define-syntax ~sort-seq (~sort-ish #'{~seq}))
+
+(define-syntax (sort/stx stx)
+ (syntax-case stx ()
+ [(_ ctx stxlist pat)
+ #'(syntax-parameterize
+ ([current-key-id (generate-temporary #'key)])
+ (def-cls tmpcls pat)
+ (and (syntax-parse stxlist [({~var || tmpcls} …) #t] [_ (displayln (format "Failed to parse ~a as ~a." stxlist 'pat)) #f])
+ (sort (syntax->list stxlist)
+ (λ (a b)
+ (cond
+ [(and (symbol? a) (symbol? b)) (symbol<? a b)]
+ [(and (number? a) (number? b)) (< a b)]
+ [else (number? a)])) ; numbers come first in the order
+ #:key (do-parse tmpcls))))]))
+
+(define-syntax (def-cls stx)
+ (syntax-case stx ()
+ [(_ tmpcls pat)
+ (with-syntax ([key (syntax-parameter-value
+ #'current-key-id)])
+ #'(define-syntax-class tmpcls
+ ;; I can't seem to manage to establish reliable communication between
+ ;; the ~sort and the ~key. So here we're relying on the fact that
+ ;; #:attributes is actually unhygienic, in order to get a handle on
+ ;; the key as defined by ~key.
+ #:attributes (key)
+ (pattern pat)))]))
+
+(define-syntax (do-parse stx)
+ (syntax-case stx ()
+ [(_ tmpcls)
+ (with-syntax ([x.key (format-id #'x "x.~a" (syntax-parameter-value
+ #'current-key-id))])
+ #'(syntax-parser
+ [(~var x tmpcls) (syntax-e #'x.key)]))]))
+
+(define-syntax ~key
+ (pattern-expander
+ (λ (stx)
+ (syntax-case stx ()
+ [(self pat)
+ (if (syntax-parameter-value #'current-key-id)
+ (with-syntax ([key (syntax-parameter-value #'current-key-id)])
+ #`(~and pat key))
+ #'(~and pat _))]))))
+
+#;(syntax-parse #'([a 3] [c 1] [b 2])
+ [{~sort [{~key k} v] …}
+ #'([k . v] …)])
diff --git a/test/same-id-pattern-test.rkt b/test/same-id-pattern-test.rkt
@@ -0,0 +1,12 @@
+#lang racket
+(require syntax/parse
+ phc-ts/same-id-pattern
+ rackunit)
+
+(check-true (syntax-parse #'(a 1 2 a 4)
+ [(y _ ... {~same-free-id y} _ ...) #t]
+ [_ #f]))
+
+(check-false (syntax-parse #'(a 1 2 b 4)
+ [(y _ ... {~same-free-id y} _ ...) #t]
+ [_ #f]))
+\ No newline at end of file
diff --git a/test/stx-sort-test.rkt b/test/stx-sort-test.rkt
@@ -0,0 +1,20 @@
+#lang racket
+(require phc-ts/stx-sort
+ syntax/parse
+ phc-toolkit/untyped/aliases
+ rackunit)
+
+(check-equal? (syntax-parse #'([a 3] [c 2] [b 1])
+ [{~sort [{~key k} v] …}
+ (syntax->datum #'([k . v] …))])
+ '([a . 3] [b . 1] [c . 2]))
+
+(check-equal? (syntax-parse #'([a z y] [c x] [b w])
+ [{~sort [{~key k} . {~sort {~key v} …}] …}
+ (syntax->datum #'([k v …] …))])
+ '([a y z] [b w] [c x]))
+
+(check-equal? (syntax-parse #'([a 5 4] [c 3 1 2] [b 0])
+ [{~sort [{~key k} . {~sort {~key v} …}] …}
+ (syntax->datum #'([k v …] …))])
+ '([a 4 5] [b 0] [c 1 2 3]))
+\ No newline at end of file
diff --git a/test/test1.rkt b/test/test1.rkt
@@ -0,0 +1,12 @@
+#lang s-exp phc-ts
+(require turnstile/examples/tests/rackunit-typechecking)
+
+(check-type (λ ([x : X]) (ann x : X)) : (→/test A A))
+(check-type (λ ([x : y]) (ann x : y)) : (→/test A A))
+(check-type (λ ([x : y]) x) : (→/test A A))
+(check-type (record [b = 1] [a = 2]) : (Record [a : Int] [b : Int]))
+(check-type (record [a = 2] [b = 1]) : (Record [a : Int] [b : Int]))
+(typecheck-fail
+ (getfield c (record [b = 1] [a = 2]))
+ #:with-msg (string-append "expected record type containing the field c, got:"
+ " \\(Record \\(a : Int\\) \\(b : Int\\)\\)"))
+\ No newline at end of file
