From 68bf43440ca6d407c6107243a019726be02365c9 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Wed, 16 May 2018 19:26:55 -0400 Subject: [PATCH 1/2] Add `:` declarations for val definitions --- hackett-lib/hackett/private/base.rkt | 144 +++++++++++++++++++++------ hackett-lib/info.rkt | 3 +- 2 files changed, 113 insertions(+), 34 deletions(-) diff --git a/hackett-lib/hackett/private/base.rkt b/hackett-lib/hackett/private/base.rkt index 2f78c2e..4351492 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 @@ -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,20 +376,54 @@ [(_ . x) (raise-syntax-error #f "literal not supported" #'x)]) -(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 - ; interface with untyped (i.e. Racket) code, and therefore the resulting type is ignored. For - ; example, the def form wraps an expression in its expansion with :, but it binds the actual - ; identifier to a syntax transformer that attaches the type directly. Therefore, it needs to perform - ; context reduction itself prior to expanding to :, and it must use #:exact. - [(_ e {~type t:type} {~optional {~and #:exact exact?}}) - #:with t_reduced (if (attribute exact?) - #'t.expansion - (type-reduce-context #'t.expansion)) - (attach-type #`(let-values- ([() t.residual]) - #,(τ⇐! ((attribute t.scoped-binding-introducer) #'e) #'t_reduced)) - #'t_reduced)]) +;; The `:` form behaves differently in an expression context vs. a +;; module context by dispatching on (syntax-local-context). +(define-syntax : + (λ (stx) + (match (syntax-local-context) + ; In an expression context, `:` annotates an expression with + ; an expected type. + ['expression + (syntax-parse stx + ; 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 + ; interface with untyped (i.e. Racket) code, and therefore the resulting type is ignored. For + ; example, the def form wraps an expression in its expansion with :, but it binds the actual + ; identifier to a syntax transformer that attaches the type directly. Therefore, it needs to perform + ; context reduction itself prior to expanding to :, and it must use #:exact. + [(_ e {~type t:type} {~optional {~and #:exact exact?}}) + #:with t_reduced (if (attribute exact?) + #'t.expansion + (type-reduce-context #'t.expansion)) + (attach-type #`(let-values- ([() t.residual]) + #,(τ⇐! ((attribute t.scoped-binding-introducer) #'e) #'t_reduced)) + #'t_reduced)])] + + ; In other contexts, such as module-level bindings or + ; in the REPL, : is a type declaration for `x`, and + ; will be understood by `def`. + [_ + (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) @@ -383,31 +450,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 {~and : {~var :/use}} 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- + (:/use 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/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 854853b525acae29454c3915588aa69c4051f5e8 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 17 May 2018 17:23:22 -0400 Subject: [PATCH 2/2] Add tests for `:` declarations --- .../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..362431b --- /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)))}) +