From ca30c7c6423183219fc221820c1fda9f35952059 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Wed, 16 May 2018 19:26:55 -0400 Subject: [PATCH 1/3] =?UTF-8?q?Add=20`=E2=8B=AE`=20declarations=20for=20va?= =?UTF-8?q?l=20definitions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- hackett-lib/hackett/private/base.rkt | 115 ++++++++++++++++++++----- hackett-lib/hackett/private/kernel.rkt | 2 +- hackett-lib/info.rkt | 3 +- 3 files changed, 98 insertions(+), 22 deletions(-) diff --git a/hackett-lib/hackett/private/base.rkt b/hackett-lib/hackett/private/base.rkt index 2f78c2e..35a3645 100644 --- a/hackett-lib/hackett/private/base.rkt +++ b/hackett-lib/hackett/private/base.rkt @@ -6,7 +6,9 @@ syntax/parse/experimental/template syntax/intdef syntax/srcloc - threading) + syntax/parse/class/local-value + threading + serialize-syntax-introducer) (postfix-in - (combine-in racket/base racket/promise)) racket/stxparam @@ -26,7 +28,7 @@ @%superclasses-key @%dictionary-placeholder @%with-dictionary #%defer-expansion define-primop define-base-type -> Integer Double String - : λ1 def let letrec todo!) + : ⋮ λ1 def let letrec todo!) (define-base-type Integer) (define-base-type Double) @@ -324,6 +326,37 @@ ;; --------------------------------------------------------------------------------------------------- +(begin-for-syntax + ; Instances of this struct are created by `⋮` when declaring the types of bindings + ; seperately from their definitions. When a binding is defined (with `def` or related + ; forms), it searches for a `binding-declaration` and fills in `internal-id` with the + ; actual definition. The `type` field is used as the expected type of the definition. + ; fixity : [Maybe Fixity] + (struct binding-declaration [internal-id type scoped-binding-introducer fixity] + #:property prop:procedure + (λ (this stx) + (match-define (binding-declaration x- type _ _) this) + ((make-typed-var-transformer x- type) stx)) + #:property prop:infix-operator + (λ (this) (binding-declaration-fixity this))) + + (define-syntax-class id/binding-declaration + #:attributes [internal-id type scoped-binding-introducer fixity] + [pattern (~var x (local-value binding-declaration?)) + #:do [(match-define (binding-declaration x-* type* sbi* fixity*) + (attribute x.local-value))] + #:attr internal-id (syntax-local-introduce x-*) + #:with type (syntax-local-introduce type*) + #:attr scoped-binding-introducer (deserialize-syntax-introducer sbi*) + #:attr fixity fixity*])) + +(define-syntax-parser define/binding-declaration + [(_ x:id/binding-declaration rhs) + #:with x- #'x.internal-id + #'(define- x- rhs)]) + +;; --------------------------------------------------------------------------------------------------- + (define-syntax-parser @%module-begin [(_ form ...) (~> (local-expand (value-namespace-introduce @@ -343,6 +376,7 @@ [(_ . x) (raise-syntax-error #f "literal not supported" #'x)]) +;; The `:` form annotates an expression with an expected type. (define-syntax-parser : ; The #:exact option prevents : from performing context reduction. This is not normally important, ; but it is required for forms that use : to ensure an expression has a particular shape in order to @@ -358,6 +392,36 @@ #,(τ⇐! ((attribute t.scoped-binding-introducer) #'e) #'t_reduced)) #'t_reduced)]) +;; The `⋮` form declares that an id will be defined with an expected type. +;; For example: +;; (⋮ x τ) +;; (def x e) +;; Defines `x` with type `τ` to be equal to the value produced by `e`, +;; which must produce +(define-syntax ⋮ + (λ (stx) + (syntax-parse stx + [(_ x:id {~type t:type} + {~alt {~optional {~and #:exact exact?}} + {~optional f:fixity-annotation}} + ...) + #:with x- (generate-temporary #'x) + #:with exct? (and (attribute exact?) #true) + #:with fixity (attribute f.fixity) + #:with t_reduced (if (attribute exact?) + #'t.expansion + (type-reduce-context #'t.expansion)) + #:with sbi (serialize-syntax-introducer + (attribute t.scoped-binding-introducer)) + #`(begin- + (define-values- [] t.residual) + (define-syntax- x + (binding-declaration + (quote-syntax x-) + (quote-syntax t_reduced) + (quote-syntax sbi) + 'fixity)))]))) + (define-syntax-parser λ1 [(_ x:id e:expr) #:do [(define t (get-expected this-syntax))] @@ -383,31 +447,42 @@ (define-syntax-parser def #:literals [:] - [(_ id:id - {~or {~once {~seq {~and : {~var :/use}} {~type t:type} - {~optional {~and #:exact exact?}}}} - {~optional fixity:fixity-annotation}} - ... + [(_ x:id/binding-declaration e:expr) + #:with x- #'x.internal-id + (syntax-property + #`(define- x- + (: #,((attribute x.scoped-binding-introducer) #'e) + x.type + #:exact)) + 'disappeared-use + (syntax-local-introduce #'x))] + + [(_ x:id : type:expr + {~and {~seq stuff ...} + {~seq {~alt {~optional {~and #:exact exact?}} + {~optional f:fixity-annotation}} + ...}} e:expr) - #:with id- (generate-temporary #'id) - #:with t_reduced (if (attribute exact?) #'t.expansion (type-reduce-context #'t.expansion)) - #`(begin- - #,(indirect-infix-definition - #'(define-syntax- id (make-typed-var-transformer #'id- (quote-syntax t_reduced))) - (attribute fixity.fixity)) - (define- id- (:/use #,((attribute t.scoped-binding-introducer) #'e) t_reduced #:exact)))] + #'(begin- + (⋮ x type stuff ...) + (def x e))] + [(_ id:id - {~optional fixity:fixity-annotation} + {~and {~seq fixity-stuff ...} + {~optional fixity:fixity-annotation}} e:expr) - #:with x^ (generate-temporary) + #:with x^ (generate-temporary #'z) #:with t_e #'(#%type:wobbly-var x^) #:do [(match-define-values [(list id-) e-] (τ⇐/λ! #'e #'t_e (list (cons #'id #'t_e))))] #:with t_gen (type-reduce-context (generalize (apply-current-subst #'t_e))) + #:with id-/gen (attach-type id- #'t_gen) #`(begin- - #,(indirect-infix-definition - #`(define-syntax- id (make-typed-var-transformer (quote-syntax #,id-) (quote-syntax t_gen))) - (attribute fixity.fixity)) - (define- #,id- #,e-))]) + (⋮ id t_gen fixity-stuff ... #:exact) + (define/binding-declaration id + (let-syntax ([id-/gen + (make-rename-transformer (quote-syntax id))]) + #,e-)))]) + (begin-for-syntax (struct todo-item (full summary) #:prefab)) diff --git a/hackett-lib/hackett/private/kernel.rkt b/hackett-lib/hackett/private/kernel.rkt index c81ee58..4a5e8a7 100644 --- a/hackett-lib/hackett/private/kernel.rkt +++ b/hackett-lib/hackett/private/kernel.rkt @@ -20,7 +20,7 @@ [λ lambda]) #%require/only-types combine-in except-in only-in prefix-in rename-in provide combine-out except-out prefix-out rename-out for-type module+ - : def λ let letrec todo! + : ⋮ def λ let letrec todo! (for-type #:no-introduce ∀ -> => Integer Double String (rename-out [@%top #%top] [#%type:app #%app] diff --git a/hackett-lib/info.rkt b/hackett-lib/info.rkt index e1fc9f0..7db8abc 100644 --- a/hackett-lib/info.rkt +++ b/hackett-lib/info.rkt @@ -7,6 +7,7 @@ "curly-fn-lib" "data-lib" "syntax-classes-lib" - "threading-lib")) + "threading-lib" + "serialize-syntax-introducer")) (define build-deps '()) From dc8a269341853ba77bf856936d3f5e02e1e7e96f Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 17 May 2018 17:23:22 -0400 Subject: [PATCH 2/3] =?UTF-8?q?Add=20tests=20for=20`=E2=8B=AE`=20declarati?= =?UTF-8?q?ons?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../tests/hackett/integration/id-decl.rkt | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 hackett-test/tests/hackett/integration/id-decl.rkt diff --git a/hackett-test/tests/hackett/integration/id-decl.rkt b/hackett-test/tests/hackett/integration/id-decl.rkt new file mode 100644 index 0000000..686e170 --- /dev/null +++ b/hackett-test/tests/hackett/integration/id-decl.rkt @@ -0,0 +1,22 @@ +#lang hackett + +(require hackett/private/test) + +(⋮ f {Integer -> Integer}) +(def f (λ [x] (id x))) + +(⋮ fact {Integer -> Integer}) +(defn fact + [[0] 1] + [[n] {n * (fact {n - 1})}]) + +(⋮ id (forall [a] {a -> a})) +(defn id + [[x] (: x a)]) + +(⋮ rmt (forall [a b] (Monoid b) => (Either a b))) +(def rmt (Right (: mempty b))) + +(test {rmt ==! (: (Right "") (Either Unit String))}) +(test {rmt ==! (: (Right Nil) (Either Bool (List Integer)))}) + From 543f0e60a0c6deafd656c34b3e32589f6aa648e9 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 28 Jun 2018 10:40:21 -0400 Subject: [PATCH 3/3] id-decl: if x- is already defined, it's a new definition --- hackett-lib/hackett/private/base.rkt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/hackett-lib/hackett/private/base.rkt b/hackett-lib/hackett/private/base.rkt index 4d95e64..be44e85 100644 --- a/hackett-lib/hackett/private/base.rkt +++ b/hackett-lib/hackett/private/base.rkt @@ -483,6 +483,9 @@ #:literals [:] [(_ x:id/binding-declaration e:expr) #:with x- #'x.internal-id + ;; if x- is already defined, move on to the case where + ;; this is treated as a new definition + #:when (not (identifier-binding #'x-)) (syntax-property #`(define- x- (: #,((attribute x.scoped-binding-introducer) #'e)