From 61c290d1ecd1737d8c0dee9a965f817880396bfc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= <georges.duperon@gmail.com>
Date: Sat, 9 Sep 2017 12:20:23 +0200
Subject: [PATCH] Added record types where the order of fields is irrelevant.

---
 aliases.rkt                       |   8 ++
 info.rkt                          |  10 ++-
 main.rkt                          | 133 ++++++++++++++++++++++++++++--
 same-id-pattern.rkt               |  15 ++++
 scribblings/phc-ts.scrbl          |  33 ++++++++
 scribblings/travis-skeleton.scrbl |  31 -------
 stx-sort.rkt                      |  84 +++++++++++++++++++
 test/same-id-pattern-test.rkt     |  12 +++
 test/stx-sort-test.rkt            |  20 +++++
 test/test1.rkt                    |  12 +++
 10 files changed, 316 insertions(+), 42 deletions(-)
 create mode 100644 aliases.rkt
 create mode 100644 same-id-pattern.rkt
 create mode 100644 scribblings/phc-ts.scrbl
 delete mode 100644 scribblings/travis-skeleton.scrbl
 create mode 100644 stx-sort.rkt
 create mode 100644 test/same-id-pattern-test.rkt
 create mode 100644 test/stx-sort-test.rkt
 create mode 100644 test/test1.rkt

diff --git a/aliases.rkt b/aliases.rkt
new file mode 100644
index 0000000..0568541
--- /dev/null
+++ 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
index 8ecaa66..ffdb7c6 100644
--- 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
index a68874f..7dcb625 100644
--- 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)
-       
-       (require (for-syntax racket/base))
+       (extends turnstile/examples/mlish)]
 
-       #;(define id …)]
+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 ℓ)) τ)]))
+       
+       (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].
+
+@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
new file mode 100644
index 0000000..24b4ff8
--- /dev/null
+++ 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
new file mode 100644
index 0000000..668e179
--- /dev/null
+++ 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
deleted file mode 100644
index ba73c95..0000000
--- a/scribblings/travis-skeleton.scrbl
+++ /dev/null
@@ -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
new file mode 100644
index 0000000..8ca6717
--- /dev/null
+++ 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
new file mode 100644
index 0000000..83fefd6
--- /dev/null
+++ 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
new file mode 100644
index 0000000..5c8659c
--- /dev/null
+++ 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
new file mode 100644
index 0000000..d1d5aa3
--- /dev/null
+++ 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