Knocked off a bunch of TODOs

* Removed some TODOs that were already completed
* Added cur-match, to abstract the common (syntax-parse (cur-expand syn) ...)
  pattern

cur.rkt

@@ -1,4 +1,28 @@
 #lang racket/base
 
-(require (rename-in "curnel/redex-lang.rkt" [provide real-provide]))
-(provide (rename-out [real-provide provide]) (all-from-out "curnel/redex-lang.rkt"))
+(module extra racket
+  (require
+    racket/syntax
+    syntax/parse
+    (for-template
+      (only-in "curnel/redex-lang.rkt"
+       cur-expand)))
+
+  (provide cur-match)
+
+  (define-syntax (cur-match syn)
+    (syntax-case syn ()
+      [(_ syn [pattern body] ...)
+       #'(syntax-parse (cur-expand syn)
+           [pattern body] ...)])))
+
+(require
+  (rename-in "curnel/redex-lang.rkt" [provide real-provide])
+  (for-syntax 'extra)
+  'extra)
+(provide
+  (rename-out [real-provide provide])
+  (for-syntax (all-from-out 'extra))
+  (all-from-out
+    'extra
+    "curnel/redex-lang.rkt"))

curnel/redex-lang.rkt

@@ -1,17 +1,13 @@
 #lang racket/base
 ;; This module just provide module language sugar over the redex model.
 
-;; TODO: Strip to racket/base as much as possible.
-;; TODO: Remove trace,pretty, debugging stuff
 (require
-  racket/pretty
   "redex-core.rkt"
   redex/reduction-semantics
   racket/provide-syntax
   (for-syntax
     (except-in racket import)
     syntax/parse
-    racket/pretty
     racket/syntax
     (except-in racket/provide-transform export)
     racket/require-transform
@@ -133,8 +129,7 @@
       (term (reduce #,(sigma) (subst-all #,(datum->syntax syn t) #,(first (bind-subst)) #,(second (bind-subst)))))))
 
   ;; TODO: Blanket disarming is probably a bad idea.
-  (define orig-insp (variable-reference->module-declaration-inspector
-                      (#%variable-reference)))
+  (define orig-insp (variable-reference->module-declaration-inspector (#%variable-reference)))
   (define (disarm syn) (syntax-disarm syn orig-insp))
 
   ;; Locally expand everything down to core forms.
@@ -225,7 +220,7 @@
         (append (syntax-e #'(Type dep-inductive dep-lambda dep-app dep-elim dep-forall dep-var))
                 ls)))))
 
-;; TODO: OOps, run doesn't return a cur term but a redex term
+;; TODO: Oops, run doesn't return a cur term but a redex term
 ;; wrapped in syntax bla. This is bad.
 (define-syntax (run syn)
   (syntax-case syn ()

oll.rkt

@@ -1,17 +1,22 @@
 #lang s-exp "cur.rkt"
 ;; OLL: The OTT-Like Library
-;; TODO: Add latex extraction
 ;; TODO: Automagically create a parser from bnf grammar
-(require "stdlib/sugar.rkt" "stdlib/nat.rkt" racket/trace)
+(require "stdlib/sugar.rkt" "stdlib/nat.rkt")
 
-(provide define-relation define-language var avar var-equal?
-         generate-coq #;(rename-out [oll-define-theorem define-theorem]))
+(provide
+  define-relation
+  define-language
+  var
+  avar
+  var-equal?
+  generate-coq
+  #;(rename-out [oll-define-theorem define-theorem]))
 
 (begin-for-syntax
   (define-syntax-class dash
     (pattern x:id
-           #:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x)))
-           "Invalid dash"))
+             #:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x)))
+             "Invalid dash"))
 
   (define-syntax-class decl (pattern (x:id (~datum :) t:id)))
 
@@ -58,7 +63,7 @@
                        (string-trim
                          (for/fold ([str ""])
                                    ([rule (attribute rules.latex)])
-                                   (format "~a~a\\and~n" str rule))
+                           (format "~a~a\\and~n" str rule))
                          "\\and"
                          #:left? #f))))
             #:exists 'append))
@@ -73,8 +78,8 @@
   (require racket/syntax)
   (define (new-name name . id*)
     (apply format-id name (for/fold ([str "~a"])
-                                  ([_ id*])
-                          (string-append str "-~a")) name (map syntax->datum id*)))
+                                    ([_ id*])
+                            (string-append str "-~a")) name (map syntax->datum id*)))
 
   (define (fresh-name id)
     (datum->syntax id (gensym (syntax->datum id)))))

stdlib/tactics/standard.rkt

@@ -18,8 +18,7 @@
  | state unmodified, or raise exception, or ...
  |#
 (define-tactic (intro name ps)
-  ;; TODO: Provide cur-match, which wraps syntax-parse and uses cur-expand.
-  (syntax-parse (cur-expand (proof-state-current-goal-ref ps))
+  (cur-match (proof-state-current-goal-ref ps)
     [(forall (x:id : P:expr) body:expr)
      (let* ([ps (proof-state-extend-env ps name #'P)]
             [ps (proof-state-current-goal-set ps #'body)]
@@ -44,7 +43,7 @@
 
 ;; Do the obvious thing
 (define-tactic (obvious ps)
-  (syntax-parse (cur-expand (proof-state-current-goal-ref ps))
+  (cur-match (proof-state-current-goal-ref ps)
     [(forall (x : P) t)
      (obvious (intro #'x ps))]
     [t:expr