micros-experiments.rkt

#lang racket/base

(require
  racket/serialize
  (for-syntax
    racket/base
    syntax/parse
    racket/syntax
    racket/generic)
  (for-meta 2 racket/base))

(provide (all-defined-out))

;;------------------------------------------------------------------------
; syntax debugging
(require racket/trace)
(require (for-syntax racket/trace))
#;(begin-for-syntax
  (current-trace-print-args
    (let ([ctpa (current-trace-print-args)])
      (lambda (s l kw l2 n)
        (ctpa s (map syntax->datum l) kw l2 n))))
  (current-trace-print-results
    (let ([ctpr (current-trace-print-results)])
      (lambda (s r n)
        (ctpr s (map syntax->datum r) n)))))

;;------------------------------------------------------------------------

(define eeyore (void))

(begin-for-syntax
  ;; The Mule Pattern lets us smuggle values through the macro expander using syntax properties.
  (define mule #'eeyore)
  (define (burden-mule ir)
    (syntax-property mule 'expansion ir))
  (define (unburden-mule m)
    (syntax-property m 'expansion))

  ;; binds should be a list of pairs of an identifier and their expansion, as an IR struct.
  (define (expand-micro stx binds)
    (define idx (syntax-local-make-definition-context))
    (syntax-local-bind-syntaxes (map car binds) #f idx)
    (local-expand  #`(let-syntax #,(for/list ([bind-info binds])
                                     (define x (car bind-info))
                                     #`[#,x (lambda (stx) (burden-mule #,(cdr bind-info)))])
                       #,stx)
                   'expression '() idx)))

(define-syntax (declare-language stx)
  (syntax-parse stx
    [(_ language-name:id)
     #:with param (format-id stx "param:~a-term-pattern" #'language-name)
     #:with syntax-class (format-id stx "~a-term" #'language-name)
     #:with expand-lang (format-id stx "expand-~a" #'language-name)
     #`(begin
         (begin-for-syntax
           (define param (make-parameter (lambda (stx) (raise-syntax-error 'sytax-class "Did not match expanded term" stx))))
           (define-syntax-class syntax-class
             #:literals (#%expression let-values eeyore)
             #:attributes (body)
             #:commit
             (pattern (let-values _ (~var e syntax-class)) #:attr body #'e.body)
             (pattern (#%expression (~var e syntax-class)) #:attr body #'e.body)
             (pattern eeyore #:attr body this-syntax)
             (pattern term #:attr body (burden-mule ((param) #'term))))

           (define (expand-lang stx [binds '()])
             (syntax-parse (expand-micro stx binds)
               [(~var e syntax-class)
                (unburden-mule #'e.body)])))

         (define-syntax language-name
           (make-hasheq
             (list
               (cons 'syntax-class-param #'param)
               (cons 'expander-id #'expand-lang)))))]))

(define-syntax (define-embedding-micro stx)
  (syntax-parse stx
    [(_ kw:id language-name:id
        micro-def
        (~optional (~seq #:struct struct-info ...)))
     #:with param (hash-ref (syntax-local-value #'language-name) 'syntax-class-param)
     #`(begin
         (begin-for-syntax
           (~? (~@ (struct/derived #'#,stx kw struct-info ...)))
           (let ([super-pattern (param)])
             (param (lambda (stx)
                      (with-handlers ([exn:fail:syntax? (lambda _ (super-pattern stx))])
                        (micro-def stx)))))))]))

(define-syntax (define-micro stx)
  (syntax-parse stx
    [(_ kw:id language-name:id
        micro-def
        (~optional (~seq #:struct struct-info ...)))
     #'(begin
         (begin-for-syntax
           (~? (~@ (struct/derived #'#,stx kw struct-info ...))))
         (define-syntax (kw stx)
           (burden-mule (micro-def stx))))]))

(define-syntax (define-simple-micro stx)
  (syntax-parse stx
    [(_ kw:id language-name:id options ...)
     #:with expand-lang (hash-ref (syntax-local-value #'language-name) 'expander-id)
     #'(begin
         ;; TODO: implement a singleton struct pattern
         (define-micro kw language-name
           (lambda (stx)
             (syntax-parse stx
               [foo:id
                (kw)]))
           #:struct () options ...))]
    [(_ (kw:id args:id ...) language-name:id
        options ...)
     #:with expand-lang (hash-ref (syntax-local-value #'language-name) 'expander-id)
     #'(define-micro kw language-name
         (lambda (stx)
           (syntax-case stx ()
             [(_ args ...)
              (kw (expand-lang #'args) ...)]))
         #:struct (args ...) options ...)]))

;; Seems no reason, yet, for this to be significantly different from generics.
(define-syntax (define-judgements stx)
  (syntax-parse stx
    [(_ e ...)
     #'(begin-for-syntax
         (define-generics e ...))]))

;;------------------------------------------------------------------------

;; stlc
(module* stlc racket/base
  (require
    (submod "..")
    (for-syntax
      racket/base
      syntax/parse
      racket/generic
      syntax/id-table
      racket/match))

  (declare-language stlc-types)

  (define-judgements type-judgements
    (type-equal? type-judgements B))

  (define-simple-micro Nat stlc-types
    #:methods
    gen:type-judgements
    [(define (type-equal? A B)
      (Nat? B))])

  (define-simple-micro (-> A B) stlc-types
    #:methods
    gen:type-judgements
    [(define/generic super-equal? type-equal?)
     (define (type-equal? A B)
       (match* (A B)
         [((-> A1 B1)
           (-> A2 B2))
          (and (super-equal? A1 B1)
               (super-equal? A2 B2))]
         [(_ _) #f]))])

  (declare-language stlc)

  (define-judgements stlc-checkable
    (type-check stlc-checkable env type)
    #:defaults
    ([values
       (define (type-check term env type)
         (type-equal? (type-synth term env) type))]))

  (define-judgements stlc-synthable
    (type-synth stlc-synthable env)
    #:defaults
    ([identifier?
       (define (type-synth term env)
         (free-id-table-ref env term))]))

  (define-judgements stlc-compileable
    (stlc-compile stlc-compileable))

  (define-embedding-micro stlc-var stlc
    (lambda (stx)
      ;; NOTE: bound variables are weird and don't get written directly.
      (error 'stlc-var-transformer "unused"))
    #:struct (v type)
    #:methods
    gen:stlc-synthable
    [(define (type-synth t env)
       (stlc-var-type t))]
    #:methods
    gen:stlc-compileable
    [(define (stlc-compile e)
       (stlc-var-v e))])

  (define-embedding-micro nat stlc
    (lambda (stx)
      (syntax-parse stx
        #:literals (quote)
        [(quote n:exact-nonnegative-integer)
         (nat (syntax-e #'n))]))
    #:struct (n)
    #:methods
    gen:stlc-synthable
    [(define (type-synth term env)
       (Nat))]
    #:methods
    gen:stlc-compileable
    [(define (stlc-compile e)
       (nat-n e))])

  (define-micro stlc-lambda stlc
    (lambda (stx)
      (syntax-parse stx
        [(_ (x : A) e)
         (define A- (expand-stlc-types #'A))
         (stlc-lambda #'x A- (expand-stlc #'e (list (cons #'x (stlc-var #'x A-)))))]))
    #:struct (x type body)
    #:methods
    gen:stlc-checkable
    [(define/generic super-check type-check)
     (define (type-check t env type)
       (match* (t type)
         [((stlc-lambda x A1 body) (-> A2 B))
          (and (type-equal? A1 A2)
               (super-check body (free-id-table-set env x A1) B))]))]
    #:methods
    gen:stlc-compileable
    [(define/generic super-compile stlc-compile)
     (define (stlc-compile e)
       #`(lambda (#,(stlc-lambda-x e)) #,(super-compile (stlc-lambda-body e))))])

  (define-micro :: stlc
    (lambda (stx)
      (syntax-parse stx
        [(_ e A)
         (:: (expand-stlc #'e) (expand-stlc-types #'A))]))
    #:struct (term type)
    #:methods
    gen:stlc-synthable
    [(define (type-synth t env)
       (match t
         [(:: e A)
          (if (type-check e env A)
              A
              (error 'type-synth "Term ~a does not check against ~a" e A))]))]
    #:methods
    gen:stlc-compileable
    [(define/generic super-compile stlc-compile)
     (define (stlc-compile e)
       (super-compile (::-term e)))])

  (define-micro stlc-app stlc
    (lambda (stx)
      (syntax-parse stx
        [(_ e1 e2)
         (stlc-app (expand-stlc #'e1) (expand-stlc #'e2))]))
    #:struct (rator rand)
    #:methods
    gen:stlc-synthable
    [(define/generic super-synth type-synth)
     (define (type-synth t env)
       (match t
         [(stlc-app rator rand)
          (match (super-synth rator env)
            [(-> A B)
             (unless (type-check rand env A)
               (error 'type-synth "Argument ~a failed to check against expected type ~a" rator A))
             B])]))]
    #:methods
    gen:stlc-compileable
    [(define/generic super-compile stlc-compile)
     (define (stlc-compile e)
       #`(#%app #,(super-compile (stlc-app-rator e)) #,(super-compile (stlc-app-rand e))))])

  (define-syntax (new-module-begin stx)
    (syntax-case stx ()
      [(_ es ...)
       #`(#%module-begin
          #,@(for/list ([e (syntax->list #'(es ...))])
               (let* ([e- (expand-stlc e)]
                      [A (type-synth e- (make-immutable-free-id-table))])
                 (printf "~a has type ~a~n" (syntax->datum e) A)
                 (stlc-compile e-))))]))

  (provide
    ::
    Nat
    ->
    #%datum
    (rename-out
      [stlc-lambda lambda]
      [stlc-app #%app]
      [new-module-begin #%module-begin])))

(module* A (submod ".." stlc)
  5
  (:: 5 Nat)
  ((:: (lambda (x : Nat) x) (-> Nat Nat)) 5))