From 0e46da74abf3706b24e62e7db3df67074d85d6da Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Thu, 14 Jan 2016 18:32:16 -0500
Subject: [PATCH] [Broken] rewriting the rest of olly

Rewriting the rest of olly, including the latex and coq generators, and
the define-relation form.
Unfortunately, managed to break parsing somehow.
---
 cur-lib/cur/olly.rkt        | 465 +++++++++++++++++++++---------------
 cur-test/cur/tests/olly.rkt |  42 ++--
 2 files changed, 293 insertions(+), 214 deletions(-)

diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt
index e22cd9e..4d615d8 100644
--- a/cur-lib/cur/olly.rkt
+++ b/cur-lib/cur/olly.rkt
@@ -14,105 +14,240 @@
 
   ;; private; exported for testing only
   (for-syntax
-   coq-defns
-   output-latex-bnf
-   output-coq))
+   typeset-relation
+   typeset-bnf
+   cur->coq))
+
+;; Generate Coq from Cur:
 
 (begin-for-syntax
-  (define-syntax-class dash
+  (define coq-defns (make-parameter ""))
+
+  (define (coq-lift-top-level str)
+    (coq-defns (format "~a~a~n" (coq-defns) str)))
+
+  ;; TODO: OOps, type-infer doesn't return a cur term but a redex syntax bla
+  ;; TODO: Think the above TODO was fixed; consult git log
+  (define (constructor-args syn)
+    (syntax-parse (type-infer/syn syn)
+      #:datum-literals (Π :)
+      [(Π (x:id : t) body)
+       (cons #'x (constructor-args #'body))]
+      [_ null]))
+
+  (define (sanitize-id str)
+    (let ([replace-by `((: _) (- _))])
+      (for/fold ([str str])
+                ([p replace-by])
+        (string-replace str (symbol->string (first p))
+                        (symbol->string (second p))))))
+
+  (define (cur->coq syn)
+    (parameterize ([coq-defns ""])
+      (define output
+        (let cur->coq ([syn syn])
+          (syntax-parse (cur-expand syn #'define #'begin)
+            ;; TODO: Need to add these to a literal set and export it
+            ;; Or, maybe overwrite syntax-parse
+            #:literals (real-lambda real-forall data real-app real-elim define begin Type)
+            [(begin e ...)
+             (for/fold ([str ""])
+                       ([e (syntax->list #'(e ...))])
+               (format "~a~n" (cur->coq e)))]
+            [(define name:id body)
+             (begin
+               (coq-lift-top-level
+                (format "Definition ~a := ~a.~n"
+                        (cur->coq #'name)
+                        (cur->coq #'body)))
+               "")]
+            [(define (name:id (x:id : t) ...) body)
+             (begin
+               (coq-lift-top-level
+                (format "Function ~a ~a := ~a.~n"
+                        (cur->coq #'name)
+                        (for/fold ([str ""])
+                                  ([n (syntax->list #'(x ...))]
+                                   [t (syntax->list #'(t ...))])
+                          (format "~a(~a : ~a) " str (cur->coq n) (cur->coq t)))
+                        (cur->coq #'body)))
+               "")]
+            [(real-lambda ~! (x:id (~datum :) t) body:expr)
+             (format "(fun ~a : ~a => ~a)" (cur->coq #'x) (cur->coq #'t)
+                     (cur->coq #'body))]
+            [(real-forall ~! (x:id (~datum :) t) body:expr)
+             (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t)
+                     (cur->coq #'body))]
+            [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
+             (begin
+               (coq-lift-top-level
+                (format "Inductive ~a : ~a :=~a."
+                        (sanitize-id (format "~a" (syntax-e #'n)))
+                        (cur->coq #'t)
+                        (for/fold ([strs ""])
+                                  ([clause (syntax->list #'((x* : t*) ...))])
+                          (syntax-parse clause
+                            [(x (~datum :) t)
+                             (format "~a~n| ~a : ~a" strs (syntax-e #'x)
+                                     (cur->coq #'t))]))))
+               "")]
+            [(Type i) "Type"]
+            [(real-elim var t)
+             (format "~a_rect" (cur->coq #'var))]
+            [(real-app e1 e2)
+             (format "(~a ~a)" (cur->coq #'e1) (cur->coq #'e2))]
+            [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
+      (format
+       "~a~a"
+       (coq-defns)
+       (if (regexp-match "^\\s*$" output)
+           ""
+           (format "Eval compute in ~a." output))))))
+
+(define-syntax (generate-coq syn)
+  (syntax-parse syn
+    [(_ (~optional (~seq #:file file))
+        (~optional (~seq #:exists flag))
+        body:expr)
+     (parameterize ([current-output-port
+                     (if (attribute file)
+                         (open-output-file
+                          (syntax->datum #'file)
+                          #:exists
+                          (if (attribute flag)
+                              ;; TODO: AHH WHAT?
+                              (eval (syntax->datum #'flag))
+                              'error))
+                         (current-output-port))])
+       (displayln (cur->coq #'body))
+       #'(begin))]))
+
+;; TODO: Should these display or return a string?
+(begin-for-syntax
+  (define (display-mathpartir)
+    (displayln
+     "%% Requires mathpartir, http://pauillac.inria.fr/~remy/latex/mathpartir.html")
+    (displayln
+     "%% or mttex, https://github.com/wilbowma/mttex")
+    (displayln
+     "\\usepackage{mathpartir}"))
+
+  (define (display-bnf)
+    (displayln
+     "%% Some auxillary defs. These should deleted if using mttex, https://github.com/wilbowma/mttex")
+    (displayln
+     "\\newcommand{\\bnfdef}{{\\bf ::=}}")
+    (displayln
+     "\\newcommand{\\bnfalt}{{\\bf \\mid}}"))
+
+  )
+
+;; ------------------------------------
+;; define-relation
+
+(begin-for-syntax
+  (define-syntax-class horizontal-line
     (pattern
      x:id
-     #:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x))) "Invalid dash"))
+     #:when (regexp-match? #rx"-+" (symbol->string (syntax-e #'x)))))
 
-  (define-syntax-class decl (pattern (x:id (~datum :) t)))
+  (define-syntax-class declaration
+    (pattern (x:id (~datum :) t)))
+
+  ;; Alias syntax-classes with names for better error messages
+  (define-syntax-class hypothesis
+    (pattern (~not e:horizontal-line)))
+
+  (define-syntax-class rule-name
+    (pattern x:id))
+
+  (define-syntax-class relation-name
+    (pattern x:id))
+
+  (define-syntax-class relation-index
+    (pattern e:expr))
+
+  (define-syntax-class (conclusion n args lab)
+    (pattern
+     (name:id arg:expr ...)
+     #:attr rule-label-symbol (syntax-e lab)
+     #:attr rule-name-symbol (syntax-e #'name)
+     #:attr relation-name-symbol (syntax-e n)
+     #:fail-unless (eq? (attribute rule-name-symbol) (attribute relation-name-symbol))
+     (format "In rule ~a, name of conclusion ~a did not match name of relation ~a"
+             (attribute rule-label-symbol)
+             (attribute rule-name-symbol)
+             (attribute relation-name-symbol))
+     #:attr rule-arg-count (length (attribute arg))
+     #:attr relation-arg-count (length args)
+     #:fail-unless (= (attribute rule-arg-count) (attribute relation-arg-count))
+     (format "In rule ~a, conclusion applied to ~a arguments, while relation declared to have ~a arguments"
+             (attribute rule-label-symbol)
+             (attribute rule-arg-count)
+             (attribute relation-arg-count))))
 
   ;; TODO: Automatically infer decl ... by binding all free identifiers?
   ;; TODO: Automatically infer decl ... for meta-variables that are the
   ;; same as bnf grammar.
-  (define-syntax-class inferrence-rule
-    (pattern (d:decl ...
-              x*:expr ...
-              line:dash lab:id
-              (name:id y* ...))
-              #:with rule #'(lab : (-> d ... x* ... (name y* ...)))
-              ;; TODO: convert meta-vars such as e1 to e_1
-              #:attr latex (format "\\inferrule~n{~a}~n{~a}"
-                             (string-trim
-                               (for/fold ([str ""])
-                                        ([hyp (syntax->datum #'(x* ...))])
-                                 (format "~a~a \\+" str hyp))
-                               " \\+"
-                               #:left? #f)
-                             (format "~a" (syntax->datum #'(name y* ...)))))))
+  (define-syntax-class (inferrence-rule name indices)
+    (pattern (d:declaration ...
+              (~peek (~not declaration))
+              ~!
+              h:hypothesis ...
+              line:horizontal-line
+              #;(~optional line:horizontal-line)
+              lab:rule-name
+              (~var t (conclusion name indices (attribute lab))))
+             #:with constr-decl
+             #'(lab : (-> d ... h ... (t.name t.arg ...)))
+             ;; TODO: convert meta-vars such as e1 to e_1
+             #:attr latex
+             (format
+              "\\inferrule~n{~a}~n{~a}"
+              (string-trim
+               (for/fold ([str ""])
+                         ([hyp (syntax->datum #'(h ...))])
+                 (format "~a~a \\+" str hyp))
+               " \\+"
+               #:left? #f)
+              (format "~a" (syntax->datum #'(t.name t.arg ...))))))
+
+  ;; TODO: Should this display or return a string?
+  (define (typeset-relation form rules-latex)
+    (display-mathpartir)
+    (printf
+     "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}"
+     form
+     (string-trim
+      (for/fold ([str ""])
+                ([rule rules-latex])
+        (format "~a~a\\and~n" str rule))
+      "\\and"
+      #:left? #f))))
+
 (define-syntax (define-relation syn)
   (syntax-parse syn
-    [(_ (n:id types* ...)
+    [(_ (name:relation-name index:relation-index ...)
         (~optional (~seq #:output-coq coq-file:str))
         (~optional (~seq #:output-latex latex-file:str))
-        rules:inferrence-rule ...)
-     #:fail-unless (andmap (curry equal? (length (syntax->datum #'(types* ...))))
-                           (map length (syntax->datum #'((rules.y* ...)
-                                                          ...))))
-     "Mismatch between relation declared and relation definition"
-     #:fail-unless (andmap (curry equal? (syntax->datum #'n))
-                           (syntax->datum #'(rules.name ...)))
-     "Mismatch between relation declared name and result of inference rule"
-      (let ([output #`(data n : (-> types* ... Type) rules.rule ...)])
-        ;; TODO: Pull this out into a separate function and test. Except
-        ;; that might make using attritbutes more difficult.
+        (~var rule (inferrence-rule (attribute name) (attribute index))) ...)
+      (let ([output #`(data name : (-> index ... Type) rule.constr-decl ...)])
         (when (attribute latex-file)
           (with-output-to-file (syntax->datum #'latex-file)
             (thunk
-              (printf (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}$$"
-                       (syntax->datum #'(n types* ...))
-                       (string-trim
-                         (for/fold ([str ""])
-                                   ([rule (attribute rules.latex)])
-                           (format "~a~a\\and~n" str rule))
-                         "\\and"
-                         #:left? #f))))
+             (typeset-relation
+              (syntax->datum #'(name index ...))
+              (attribute rule.latex)))
             #:exists 'append))
-        #`(begin
-            #,@(if (attribute coq-file)
-                   #`((generate-coq #:file coq-file #:exists
-                                    'append #,output))
-                   #'())
-               #,output))]))
+        (when (attribute coq-file)
+          (with-output-to-file (syntax->datum #'coq-file)
+            (thunk (displayln (cur->coq output)))
+            #:exists 'append))
+        output)]))
 
 ;; ------------------------------------
 ;; define-language
 
-(begin-for-syntax
-  ;; TODO: More clever use of syntax-parse would enable something akin to what
-  ;; define-relation is doing---having attributes that contain the latex
-  ;; code for each clause.
-  ;; TODO: convert meta-vars such as e1 to e_1
-  (define (output-latex-bnf clauses)
-    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
-      (for/fold ([str ""])
-                ([clause (syntax->list clauses)])
-        (syntax-parse clause
-          #:datum-literals (::=)
-          [(type:id (nonterminal:id ...) ::= exprs ...)
-           (format "\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
-                   (symbol->string (syntax->datum #'type))
-                   (string-trim
-                     (for/fold ([str ""])
-                               ([nt (syntax->datum #'(nonterminal ...))])
-                       (format "~a~a," str nt))
-                     ","
-                     #:left? #f)
-                   (string-trim
-                     (for/fold ([str ""])
-                               ([expr (syntax->datum #'(exprs ...))])
-                       (format "~a~a \\bnfalt " str expr))
-                     " \\bnfalt "
-                     #:left? #f))]))))
-  (define (generate-latex-bnf file-name clauses)
-    (with-output-to-file file-name
-      (thunk (printf (output-latex-bnf clauses)))
-      #:exists 'append)))
-
 (begin-for-syntax
   ;; A mutable dictionary from non-terminal meta-variables names to their types.
   (define mv-map (make-parameter #f))
@@ -157,25 +292,33 @@
     (pattern
      e:meta-variable
      #:attr args
-     (list #'e.type))
+     (list #'e.type)
+     #:attr latex
+     (format "~a" (syntax-e #'e)))
 
     ;; An identifier is a terminal-args, but is treated as syntax
     (pattern
      x:id
      #:attr args
-     '())
+     '()
+     #:attr latex
+     (format "~a" (syntax-e #'x)))
 
     ;; So is an empty list
     (pattern
      ()
      #:attr args
-     '())
-    
+     '()
+     #:attr latex
+     "")
+
     ;; We use De-Bruijn indices, so binding positions are removed.
     (pattern
      (#:bind x:var-meta-variable . (~var t (terminal-args non-terminal-type)))
      #:attr args
-     (attribute t.args))
+     (attribute t.args)
+     #:attr latex
+     (format "~a ~a" (syntax-e #'x) (attribute t.latex)))
 
     ;; A terminal-args applied to other nested expressions is a terminal-args
     (pattern
@@ -184,7 +327,9 @@
      #:attr args
      (for/fold ([ls (attribute h.args)])
                ([args (attribute t.args)])
-       (append ls args))))
+       (append ls args))
+     #:attr latex
+     (format "~a ~a" (attribute h.latex) (apply string-append (attribute t.latex)))))
 
   ;; a expression is parameterized by the name of the non-terminal to
   ;; which is belongs,
@@ -198,19 +343,25 @@
      #:attr constructor-name
      (format-id #'e "~a->~a" #'e.type non-terminal-type)
      #:attr constr-decl
-     #`(constructor-name : (-> e.type #,non-terminal-type)))
+     #`(constructor-name : (-> e.type #,non-terminal-type))
+     #:attr latex
+     (format "~a" (syntax-e #'e)))
 
     ;; An identifier is a valid expression, generating a base constructor.
     (pattern
      x:terminal
      #:attr constr-decl
-     #`(x.constructor-name : #,non-terminal-type))
+     #`(x.constructor-name : #,non-terminal-type)
+     #:attr latex
+     (format "~a" (syntax-e #'x)))
 
     ;; A terminal applied to a terminal-args is a valid expression.
     (pattern
      (x:terminal . (~var c (terminal-args non-terminal-type)))
      #:attr constr-decl
-     #`(x.constructor-name : (-> #,@(attribute c.args) #,non-terminal-type))))
+     #`(x.constructor-name : (-> #,@(attribute c.args) #,non-terminal-type))
+     #:attr latex
+     (format "(~a ~a)" (syntax-e #'x) (attribute c.latex))))
 
   (define-syntax-class non-terminal-def
     (pattern
@@ -228,7 +379,31 @@
       (~var c (expression (attribute nt-type))) ...)
      ;; Generates the inductive data type for this non-terminal definition.
      #:attr def
-     #`(data nt-type : Type c.constr-decl ...))))
+     #`(data nt-type : Type c.constr-decl ...)
+     #:attr latex
+     (format
+      "\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
+      (symbol->string (syntax->datum #'name))
+      (string-trim
+       (for/fold ([str ""])
+                 ([nt (syntax->datum #'(meta-var ...))])
+         (format "~a~a," str nt))
+       ","
+       #:left? #f)
+      (string-trim
+       (for/fold ([str ""])
+                 ([expr (attribute c.latex)])
+         (format "~a~a \\bnfalt " str expr))
+       " \\bnfalt "
+       #:left? #f))))
+
+  ;; TODO: Should this display or return a string?
+  (define (typeset-bnf nt-latex)
+    (display-mathpartir)
+    (display-bnf)
+    (printf
+     "\begin{displaymath}~n\\begin{array}{lrrl}~n~a~n\\end{array}~n\end{displaymath}"
+     (apply string-append nt-latex))))
 
 ;; TODO: For better error messages, add context
 ;; TODO: Extend define-language with syntax such as ....
@@ -251,110 +426,16 @@
          (for ([x xls])
            (dict-set! (mv-map) (syntax-e x) #'Nat)))])
     (syntax-parse #'non-terminal-defs
-      [((~var defs non-terminal-def) ...)
-       (let ([output #`(begin defs.def ...)])
-         ;; TODO: Should do this via attributes
+      [(def:non-terminal-def ...)
+       (let ([output #`(begin def.def ...)])
          (when (attribute latex-file)
-           (generate-latex-bnf (syntax->datum #'latex-file) #'(defs ...)))
-         #`(begin
-             ;; TODO: generate-coq should also export a compile-time function.
-             #,@(if (attribute coq-file)
-                    #`((generate-coq #:file coq-file #:exists 'append #,output))
-                    #'())
-             #,output))])))
+           (with-output-to-file (syntax-e #'latex-file)
+             (thunk (typeset-bnf (attribute def.latex)))
+             #:exists 'append))
+         (when (attribute coq-file)
+           (with-output-to-file (syntax-e #'coq-file)
+             (thunk (displayln (cur->coq output)))
+             #:exists 'append))
+         output)])))
 
 ;; See stlc.rkt for examples
-
-;; Generate Coq from Cur:
-
-(begin-for-syntax
-  (define coq-defns (make-parameter ""))
-  (define (coq-lift-top-level str)
-    (coq-defns (format "~a~a~n" (coq-defns) str)))
-  ;; TODO: OOps, type-infer doesn't return a cur term but a redex syntax bla
-  ;; TODO: Think the above TODO was fixed; consult git log
-  (define (constructor-args syn)
-    (syntax-parse (type-infer/syn syn)
-      #:datum-literals (Π :)
-      [(Π (x:id : t) body)
-       (cons #'x (constructor-args #'body))]
-      [_ null]))
-  (define (sanitize-id str)
-    (let ([replace-by `((: _) (- _))])
-      (for/fold ([str str])
-                ([p replace-by])
-        (string-replace str (symbol->string (first p))
-                        (symbol->string (second p))))))
-  (define (output-coq syn)
-    (syntax-parse (cur-expand syn #'define #'begin)
-       ;; TODO: Need to add these to a literal set and export it
-       ;; Or, maybe overwrite syntax-parse
-       #:literals (real-lambda real-forall data real-app real-elim define begin Type)
-       [(begin e ...)
-        (for/fold ([str ""])
-                  ([e (syntax->list #'(e ...))])
-          (format "~a~n" (output-coq e)))]
-       [(define name:id body)
-        (begin
-          (coq-lift-top-level
-            (format "Definition ~a := ~a.~n"
-                    (output-coq #'name)
-                    (output-coq #'body)))
-          "")]
-       [(define (name:id (x:id : t) ...) body)
-        (begin
-          (coq-lift-top-level
-            (format "Function ~a ~a := ~a.~n"
-                    (output-coq #'name)
-                    (for/fold ([str ""])
-                              ([n (syntax->list #'(x ...))]
-                               [t (syntax->list #'(t ...))])
-                      (format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
-                    (output-coq #'body)))
-          "")]
-       [(real-lambda ~! (x:id (~datum :) t) body:expr)
-        (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
-                (output-coq #'body))]
-       [(real-forall ~! (x:id (~datum :) t) body:expr)
-        (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
-                (output-coq #'body))]
-       [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
-        (begin
-          (coq-lift-top-level
-            (format "Inductive ~a : ~a :=~a."
-                   (sanitize-id (format "~a" (syntax-e #'n)))
-                   (output-coq #'t)
-                   (for/fold ([strs ""])
-                             ([clause (syntax->list #'((x* : t*) ...))])
-                     (syntax-parse clause
-                       [(x (~datum :) t)
-                        (format "~a~n| ~a : ~a" strs (syntax-e #'x)
-                          (output-coq #'t))]))))
-          "")]
-       [(Type i) "Type"]
-       [(real-elim var t)
-        (format "~a_rect" (output-coq #'var))]
-       [(real-app e1 e2)
-        (format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))]
-       [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
-
-(define-syntax (generate-coq syn)
-  (syntax-parse syn
-    [(_ (~optional (~seq #:file file))
-        (~optional (~seq #:exists flag)) body:expr)
-     (parameterize ([current-output-port (if (attribute file)
-                                             (open-output-file (syntax->datum #'file)
-                                                               #:exists
-                                                               (if (attribute flag)
-                                                                   ;; TODO: AHH WHAT?
-                                                                   (eval (syntax->datum #'flag))
-                                                                   'error))
-                                             (current-output-port))]
-                    [coq-defns ""])
-       (define output
-         (let ([body (output-coq #'body)])
-           (if (regexp-match "^\\s*$" body)
-               ""
-               (format "Eval compute in ~a." body))))
-       (displayln (format "~a~a" (coq-defns) output))
-       #'(begin))]))
diff --git a/cur-test/cur/tests/olly.rkt b/cur-test/cur/tests/olly.rkt
index 3eb4c9a..a2cda7b 100644
--- a/cur-test/cur/tests/olly.rkt
+++ b/cur-test/cur/tests/olly.rkt
@@ -11,49 +11,47 @@
 (begin-for-syntax
   (require rackunit))
 
-(begin-for-syntax
+;; Can't test this way anymore.
+#;(begin-for-syntax
   (check-equal?
    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
            (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
-   (output-latex-bnf #'((term (e) ::= (e1 e2) (lambda (x) e)))))
+   (typeset-bnf #'((term (e) ::= (e1 e2) (lambda (x) e)))))
   (check-equal?
    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
            (format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
-   (output-latex-bnf #'((type (A B C) ::= unit (* A B) (+ A C))))))
+   (typeset-bnf #'((type (A B C) ::= unit (* A B) (+ A C))))))
 
 (begin-for-syntax
   (check-equal?
-   (parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
-   (format "Inductive nat : Type :=~n| z : nat.~n"))
+   (format "Inductive nat : Type :=~n| z : nat.~n")
+   (cur->coq #'(data nat : Type (z : nat))))
   (check-regexp-match
    "(forall .+ : Type, Type)"
-   (output-coq #'(-> Type Type)))
-  (let ([t (parameterize ([coq-defns ""])
-             (output-coq #'(define-relation (meow gamma term type)
-                             [(g : gamma) (e : term) (t : type)
-                              --------------- T-Bla
-                              (meow g e t)]))
-             (coq-defns))])
+   (cur->coq #'(-> Type Type)))
+  (let ([t (cur->coq
+            #'(define-relation (meow gamma term type)
+                [(g : gamma) (e : term) (t : type)
+                 --------------- T-Bla
+                 (meow g e t)]))])
     (check-regexp-match
      "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
      (first (string-split t "\n")))
     (check-regexp-match
      "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
      (second (string-split t "\n"))))
-  (let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
-                               (lambda (x : nat) (ih-x : nat) ih-x)
-                               e))])
+  (let ([t (cur->coq
+            #'(elim nat Type (lambda (x : nat) nat) z
+                    (lambda (x : nat) (ih-x : nat) ih-x)
+                    e))])
     (check-regexp-match
      "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
      t))
   (check-regexp-match
    "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
-   (parameterize ([coq-defns ""])
-     (output-coq #'(define thm:plus-commutes (forall (n : nat) (m : nat)
-                                                      (== nat (plus n m) (plus m n)))))
-     (coq-defns)))
+   (cur->coq
+    #'(define thm:plus-commutes (forall (n : nat) (m : nat)
+                                        (== nat (plus n m) (plus m n))))))
   (check-regexp-match
    "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
-   (parameterize ([coq-defns ""])
-     (output-coq #'(define (add1 (n : nat)) (s n)))
-     (coq-defns))))
+   (cur->coq #'(define (add1 (n : nat)) (s n)))))