Add ⋮ declarations for val definitions

Author: AlexKnauth

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))

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]

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
   '())