From 22404dfe9814f0e7804a4bc259f7a3710fe8c01f Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Mon, 18 Jan 2016 15:13:09 -0500
Subject: [PATCH] Fixed up inferrence rules

---
 cur-lib/cur/olly.rkt | 23 ++++++++++-------------
 1 file changed, 10 insertions(+), 13 deletions(-)

diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt
index 4d615d8..7ad17ac 100644
--- a/cur-lib/cur/olly.rkt
+++ b/cur-lib/cur/olly.rkt
@@ -151,13 +151,11 @@
      x:id
      #:when (regexp-match? #rx"-+" (symbol->string (syntax-e #'x)))))
 
-  (define-syntax-class declaration
-    (pattern (x:id (~datum :) t)))
-
-  ;; Alias syntax-classes with names for better error messages
   (define-syntax-class hypothesis
+    (pattern (x:id (~datum :) t))
     (pattern (~not e:horizontal-line)))
 
+  ;; Alias syntax-classes with names for better error messages
   (define-syntax-class rule-name
     (pattern x:id))
 
@@ -186,26 +184,25 @@
              (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.
+  ;; TODO: Automatically infer hypotheses that are merely declarations by binding all free identifiers?
+  ;; TODO: Automatically infer hypotheses as above for meta-variables that are the
+  ;; same as bnf grammar, as a simple first case
   (define-syntax-class (inferrence-rule name indices)
-    (pattern (d:declaration ...
-              (~peek (~not declaration))
+    (pattern (h:hypothesis ...
+              #;line:horizontal-line
+              (~optional line:horizontal-line)
               ~!
-              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 ...)))
+             #'(lab : (-> 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 ""])
+                         ;; TODO: Perhaps omit hypotheses that are merely delcarations of free variables
                          ([hyp (syntax->datum #'(h ...))])
                  (format "~a~a \\+" str hyp))
                " \\+"