More on Matthews-Findler lump

tests/dsls/matthews-findler/for-figures.rkt

@@ -0,0 +1,82 @@
+(syntax-spec
+  (binding-class ml-var
+    #:reference-compiler
+    (make-variable-like-reference-compiler
+      compile-RM))
+
+  (nonterminal ml-expr
+    #:binding-space ml
+
+    (~> x:ml-var
+        (syntax/loc #'x (MR x)))
+
+    x:ml-var
+    n:number
+    (app e1:ml-expr e2:ml-expr)
+    (+ e1:ml-expr e2:ml-expr)
+    (- e1:ml-expr e2:ml-expr)
+    (if0 e1:ml-expr e2:ml-expr e3:ml-expr)
+    (lambda ([x:ml-var t:ml-type]) e:ml-expr)
+    #:binding (scope (bind x) e)
+
+    (MR e:racket-expr)
+    (: e:ml-expr t:ml-type)
+
+    (~> (e1 e2)
+        #'(app e1 e2)))
+
+  (nonterminal ml-type
+    #:binding-space ml
+    Nat
+    L
+    (-> t1:ml-type t2:ml-type))
+
+  (host-interface/expression
+    (RM e:ml-expr)
+    (compile-RM #'e)))
+
+(struct ml-value [v t])
+(struct racket-value [v])
+
+;; MLVar is Identifier
+;; MLType is Syntax
+;; MLExpr is Syntax
+
+;; RM-translation : Any MLType -> Any
+(define (RM-translation v t) #| elided ... |#)
+
+;; MR-translation : Any MLType -> Any
+(define (MR-translation v t) #| elided ... |#)
+
+(begin-for-syntax
+    ;; compile-RM : MLExpr -> Syntax
+    (define (compile-RM e)
+      (define-values (e^ t) (infer-type e))
+      #`(RM-translation (ml->racket #,e^) #'#,t))
+
+    ;; assert-type-equal! : MLType MLType MLExpr -> Void
+    (define (assert-type-equal! actual expected term) #| elided ... |#)
+
+    (define-local-symbol-table type-env)
+
+    ;; type-env-ref : MLVar -> MLType
+    (define (type-env-ref x)
+      (symbol-table-ref type-env x #'Nat))
+
+    ;; type-env-extend! : MLVar MLType -> Void
+    (define (type-env-extend! x t)
+      (symbol-table-set! type-env x t))
+
+    ;; infer-type : MLExpr -> (Values MLExpr MLType)
+    (define (infer-type e) #| elided ... |#)
+
+    ;; check-type! : MLExpr MLType -> MLExpr
+    (define (check-type! e t) #| elided ... |#))
+
+(define-syntax ml->racket
+  (syntax-parser
+    #:datum-literals (app + - if0 lambda MR)
+    #| elided cases ... |#
+    [(_ (MR e t))
+     #'(MR-translation e #'t)]))
+

tests/dsls/matthews-findler/lump-inferred.rkt

@@ -57,13 +57,19 @@
 (struct ml-value [v t])
 (struct racket-value [v])
 
+;; MLVar is Identifier
+;; MLType is Syntax
+;; MLExpr is Syntax
+
+;; RM-translation : Any MLType -> Any
 (define (RM-translation v t)
   (if (equal? (syntax->datum t) 'L)
     (if (racket-value? v)
       (racket-value-v v)
       (error 'RM "not a Racket value"))
     (ml-value v t)))
 
+;; MR-translation : Any MLType -> Any
 (define (MR-translation v t)
   (if (equal? (syntax->datum t) 'L)
     (racket-value v)
@@ -76,10 +82,12 @@
       (error 'MR "not an ML value"))))
 
 (begin-for-syntax
+  ;; compile-RM : MLExpr -> Syntax
   (define (compile-RM e)
     (define-values (e^ t) (infer-type e))
     #`(RM-translation (ml->racket #,e^) #'#,t))
 
+  ;; assert-type-equal! : MLType MLType MLExpr -> Void
   ;; No type variables yet, so should just be datum equality.
   (define (assert-type-equal! actual expected term)
     (unless (equal? (syntax->datum actual) (syntax->datum expected))
@@ -93,12 +101,15 @@
 
   (define-local-symbol-table type-env)
 
+  ;; type-env-ref : MLVar -> MLType
   (define (type-env-ref x)
     (symbol-table-ref type-env x #'Nat))
 
+  ;; type-env-extend! : MLVar MLType -> Void
   (define (type-env-extend! x t)
     (symbol-table-set! type-env x t))
 
+  ;; infer-type : MLExpr -> (Values MLExpr MLType)
   (define (infer-type e)
     (syntax-parse e
       #:datum-literals (app + - if0 lambda MR)
@@ -138,6 +149,7 @@
        (define e^ (check-type! #'e #'t))
        (values e^ #'t)]))
 
+  ;; check-type! : MLExpr MLType -> MLExpr
   (define (check-type! e t)
     (syntax-parse e
       #:datum-literals (app MR)
@@ -155,7 +167,7 @@
 
 (define-syntax ml->racket
   (syntax-parser
-    #:datum-literals (app + - if0 lambda)
+    #:datum-literals (app + - if0 lambda MR)
     [(_ x:id)
      #'x]
     [(_ n:number)

tests/dsls/matthews-findler/lump.rkt

@@ -72,7 +72,7 @@
 
   (define (infer-type e)
     (syntax-parse e
-      #:datum-literals (app + - if0 lambda)
+      #:datum-literals (app + - if0 lambda MR)
       [x:id
        (type-env-ref #'x)]
       [_:number
@@ -109,7 +109,7 @@
 
 (define-syntax ml->racket
   (syntax-parser
-    #:datum-literals (app + - if0 lambda)
+    #:datum-literals (app + - if0 lambda MR)
     [(_ x:id)
      #'x]
     [(_ n:number)