Redex 1.6 enables caching of judgment forms!

* Judgment form caching enables running test suite in seconds instead of
  days.
* Fixed numerous bugs after properly exercising the oll/stlc examples.

README.md

@@ -16,7 +16,8 @@ cur (plural curs)
 Getting started
 ===============
 
-Don't actually try to run anything. The type-checker may be exponential,
+Requires redex-lib version 1.6 if you want answer in a reasonable amount
+of time. Otherwise, the type-checker may require exponential time
 or worse.
 
 Open up `stlc.rkt` to see an example of what advanced meta-programming can let you do.

oll.rkt

@@ -54,10 +54,11 @@
           (with-output-to-file (syntax->datum #'latex-file)
             (thunk
               (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\end{mathpar}$$"
+                      (syntax->datum #'(n types* ...))
                       (string-trim
                         (for/fold ([str ""])
-                                  ([rule (syntax->datum #'(rules.latex ...))])
-                          (format "~a~a\\and~n" rule))
+                                  ([rule (attribute rules.latex)])
+                          (format "~a~a\\and~n" str rule))
                         "\\and"
                         #:left? #f)))
             #:exists 'append))
@@ -311,7 +312,7 @@
         (begin
           (coq-lift-top-level
             (format "Inductive ~a : ~a :=~a."
-                   (syntax-e #'n)
+                   (sanitize-id (format "~a" (syntax-e #'n)))
                    (output-coq #'t)
                    (for/fold ([strs ""])
                              ([clause (syntax->list #'((x* : t*) ...))])

redex-curnel.rkt

@@ -47,7 +47,7 @@
     (check-true (t? (term (λ (x_0 : (Unv 0)) x_0)))))
 
   ;; 'A'
-  ;; Universes
+  ;; (Unv 0)s of Universes
   ;; Replace with sub-typing
   (define-judgment-form cicL
     #:mode (unv-ok I O)

stlc.rkt

@@ -15,17 +15,16 @@
 ;; TODO: Abstract this over stlc-type, and provide from in OLL
 (data gamma : Type
   (emp-gamma : gamma)
-  (ext-gamma : (->* gamma var stlc-type gamma)))
+  (extend-gamma : (->* gamma var stlc-type gamma)))
 
 (define-rec (lookup-gamma (g : gamma) (x : var) : (maybe stlc-type))
   (case* g
     [emp-gamma (none stlc-type)]
-    [(ext-gamma (g1 : gamma) (v1 : var) (t1 : stlc-type))
+    [(extend-gamma (g1 : gamma) (v1 : var) (t1 : stlc-type))
      (if (var-equal? v1 x)
          (some stlc-type t1)
          (lookup-gamma g1 x))]))
 
-
 (define-relation (has-type gamma stlc-term stlc-type)
   #:output-coq "stlc.v"
   #:output-latex "stlc.tex"
@@ -41,7 +40,7 @@
    ------------------------ T-False
    (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
 
-  [(g : gamma) (x : var) (t : style-type)
+  [(g : gamma) (x : var) (t : stlc-type)
    (== (maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
    ------------------------ T-Var
    (has-type g (var-->-stlc-term x) t)]
@@ -55,9 +54,11 @@
 
   [(g : gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
+               (t : stlc-type)
+               (x : var) (y : var)
    (has-type g e1 (stlc-* t1 t2))
-   (has-type (extend-gamma (extend-gamma g x t1) t y2) e2 t)
-   ---------------------- T-Pair
+   (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
+   ---------------------- T-Let
    (has-type g (stlc-let x y e1 e2) t)]
 
   [(g : gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : var)