Added top-interactive support/fixed top-level eval

Also fixed some random stylistic things

cur.rkt

@@ -17,14 +17,15 @@
            [pattern body] ...)])))
 
 (require
-  (rename-in "curnel/redex-lang.rkt" [provide real-provide])
+  (rename-in "curnel/redex-lang.rkt" [provide -provide])
   (only-in racket/base eof)
   (for-syntax 'extra)
   'extra)
 (provide
-  eof
-  (rename-out [real-provide provide])
+  (rename-out [-provide provide])
   (for-syntax (all-from-out 'extra))
-  (all-from-out
-    'extra
-    "curnel/redex-lang.rkt"))
+  (except-out
+    (all-from-out
+     'extra
+     "curnel/redex-lang.rkt")
+    -provide))

curnel/redex-core.rkt

@@ -303,8 +303,9 @@
 
 (define-metafunction cic-redL
   reduce : Σ e -> e
-  [(reduce Σ e) e_r
-                (where (_ e_r) ,(car (apply-reduction-relation* cic--> (term (Σ e)))))])
+  [(reduce Σ e)
+   e_r
+   (where (_ e_r) ,(car (apply-reduction-relation* cic--> (term (Σ e)))))])
 (module+ test
   (check-equal? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
   (check-equal? (term (reduce ∅ ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))

curnel/redex-lang.rkt

@@ -39,7 +39,8 @@
 
     [dep-elim elim]
 
-    [dep-var #%top]
+    [dep-top #%top]
+    [dep-top #%top-interaction]
 
     ;      [dep-datum #%datum]
     [dep-define define])
@@ -138,7 +139,7 @@
       (local-expand
         syn
         'expression
-        (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π elim Unv #%datum))))))
+        (append (syntax-e #'(term reduce subst-all dep-top #%app λ Π elim Unv #%datum))))))
 
   ;; Only type-check at the top-level, to prevent exponential
   ;; type-checking. Redex is expensive enough.
@@ -188,6 +189,7 @@
     reified-term)
 
   ;; Reflection tools
+  ;; TODO: Why is this not just (define (normalize/syn syn) (denote syn syn))
   (define (normalize/syn syn)
     (denote
       syn
@@ -217,7 +219,7 @@
       (local-expand
         syn
         'expression
-        (append (syntax-e #'(Type dep-inductive dep-lambda dep-app dep-elim dep-forall dep-var))
+        (append (syntax-e #'(Type dep-inductive dep-lambda dep-app dep-elim dep-forall dep-top))
                 ls)))))
 
 ;; TODO: Oops, run doesn't return a cur term but a redex term
@@ -415,9 +417,9 @@
        (quasisyntax/loc syn (elim D e P method ...)))]))
 
 ;; TODO: Not sure if this is the correct behavior for #%top
-(define-syntax (dep-var syn)
+(define-syntax (dep-top syn)
   (syntax-case syn ()
-    [(_ . id) #`(term (reduce #,(sigma) id))]))
+    [(_ . id) (denote syn #'id)]))
 
 ;; TODO: Syntax-parse
 (define-syntax (dep-define syn)