Added single step evaluation abilities. Closes #27

* Added single step meta-function to core
* Expose step/syn in redex-lang
* Added macro to sugar for convenience use
* Updated relevant docs (also fixed bug in reflection docs)

curnel/redex-core.rkt

@@ -355,11 +355,20 @@
          (where Θ_r (elim-recur x_D U e_P Θ_m Θ_m Θ_i (x_c* ...)))
          -->elim)))
 
+(define-metafunction cic-redL
+  step : Σ e -> e
+  [(step Σ e)
+   e_r
+   (where (_ e_r) ,(car (apply-reduction-relation cic--> (term (Σ e)))))])
+
 (define-metafunction cic-redL
   reduce : Σ e -> e
   [(reduce Σ e)
    e_r
-   (where (_ e_r) ,(car (apply-reduction-relation* cic--> (term (Σ e)))))])
+   (where (_ e_r) ,(let ([r (apply-reduction-relation* cic--> (term (Σ e)))])
+                     (unless (null? (cdr r))
+                       (error "Church-rosser broken" r))
+                     (car r)))])
 ;; TODO: Move equivalence up here, and use in these tests.
 (module+ test
   (check-equal? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
@@ -393,7 +402,37 @@
                      (s (s zero)))
                     (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
                    (s (s zero)))))
-    (term (s (s (s (s zero)))))))
+    (term (s (s (s (s zero))))))
+  (check-equal?
+    (term (step ,Σ
+                  ((((((elim nat) Type) (λ (x : nat) nat))
+                     (s (s zero)))
+                    (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                   (s (s zero)))))
+    (term
+      (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+        (s zero))
+       ((((((elim nat) Type) (λ (x : nat) nat))
+          (s (s zero)))
+         (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+        (s zero)))))
+  (check-equal?
+    (term (step ,Σ (step ,Σ
+                 (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+                   (s zero))
+                  ((((((elim nat) Type) (λ (x : nat) nat))
+                     (s (s zero)))
+                    (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                   (s zero))))))
+    (term
+      ;; TODO: Should be checking equivalence, not equal with DYI alpha equivalence
+      ((λ (ih-x1 : nat) (s ih-x1))
+       (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+         zero)
+        ((((((elim nat) Type) (λ (x : nat) nat))
+           (s (s zero)))
+          (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+         zero))))))
 
 (define-judgment-form cic-redL
   #:mode (equivalent I I I)

curnel/redex-lang.rkt

@@ -65,6 +65,7 @@
     type-infer/syn
     type-check/syn?
     normalize/syn
+    step/syn
     cur-equal?))
 
 (begin-for-syntax
@@ -229,6 +230,10 @@
       syn
       (eval-cur syn)))
 
+  (define (step/syn syn)
+    (datum->cur
+      syn
+      (term (step ,(sigma) (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst)))))))
 
   ;; Are these two terms equivalent in type-systems internal equational reasoning?
   (define (cur-equal? e1 e2)

scribblings/reflection.scrbl

@@ -41,9 +41,9 @@ Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could b
 
 @examples[
 (eval:alts (type-infer/syn #'(lambda (x : Type) x))
-           (eval:result @racket[#'(Π (x : (Unv 0)) (Unv 0))] "" ""))
+           (eval:result @racket[#'(forall (x : (Type 0)) (Type 0))] "" ""))
 (eval:alts (type-infer/syn #'Type)
-           (eval:result @racket[#'(Unv 1)] "" ""))
+           (eval:result @racket[#'(Type 1)] "" ""))
 ]
 }
 
@@ -52,10 +52,12 @@ Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could b
 Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise.
 
 @examples[
-(eval:alts (type-infer/syn #'(lambda (x : Type) x))
-           (eval:result @racket[#'(Π (x : (Unv 0)) (Unv 0))] "" ""))
-(eval:alts (type-infer/syn #'Type)
-           (eval:result @racket[#'(Unv 1)] "" ""))
+(eval:alts (type-check/syn? #'(lambda (x : Type) x))
+           (eval:result @racket[#t] "" ""))
+(eval:alts (type-check/syn? #'Type)
+           (eval:result @racket[#t] "" ""))
+(eval:alts (type-check/syn? #'x)
+           (eval:result @racket[#f] "" ""))
 ]
 }
 
@@ -71,6 +73,21 @@ Runs the Cur term @racket[syn] to a value.
 ]
 }
 
+@defproc[(step/syn [syn syntax?])
+         syntax?]{
+Runs the Cur term @racket[syn] for one step.
+
+@examples[
+(eval:alts (step/syn #'((lambda (x : Type) x) Bool))
+           (eval:result @racket[#'Bool] "" ""))
+(eval:alts (step/syn #'(sub1 (s (s z))))
+           (eval:result @racket[#'(((((elim Nat (Type 0))
+                                      (lambda (x2 : Nat) Nat)) z)
+                                    (lambda (x2 : Nat) (lambda (ih-n2 : Nat) x2)))
+                                   (s (s z)))] "" ""))
+]
+}
+
 @defproc[(cur-equal? [e1 syntax?] [e2 syntax?])
          boolean?]{
 Returns @racket[#t] if the Cur terms @racket[e1] and @racket[e2] and equivalent according to
@@ -87,3 +104,14 @@ equal modulo α and β-equivalence.
 ]
 }
 
+
+@defproc[(cur->datum [s syntax?])
+         (or/c symbol? list?)]{
+Converts @racket[s] to a datum representation of the @tech{curnel form}, after expansion.
+@examples[
+
+
+(eval:alts (cur-?datum #'(lambda (a : Type) a))
+           (eval:result @racket['(λ (a : (Unv 0) a))] "" ""))
+]
+}

scribblings/stdlib/sugar.scrbl

@@ -154,6 +154,23 @@ computing part of the term from another Cur term.
 
 }
 
+@defform[(step syn)]{
+Like @racket[run], but uses @racket[step/syn] to evaluate only one step and prints intermediate
+results before returning the result of evaluation.
+
+@examples[#:eval curnel-eval
+          (step (plus z z))]
+
+}
+
+@defform[(step-n natural syn)]{
+Like @racket[step], but expands to @racket[natural] calls to @racket[step].
+
+@examples[#:eval curnel-eval
+          (step-n 3 (plus z z))]
+
+}
+
 @defform[(query-type expr)]{
 Print the type of @racket[expr], at compile-time. Similar to Coq's @racketfont{Check}.
 

stdlib/sugar.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../curnel/redex-lang.rkt"
+#lang s-exp "../cur.rkt"
 (provide
   ->
   ->*
@@ -16,6 +16,8 @@
   case
   case*
   run
+  step
+  step-n
   query-type
 
   ;; don't use these
@@ -123,6 +125,21 @@
   (syntax-case syn ()
     [(_ expr) (normalize/syn #'expr)]))
 
+(define-syntax (step syn)
+  (syntax-case syn ()
+    [(_ expr)
+     (let ([t (step/syn #'expr)])
+       (displayln (cur->datum t))
+       t)]))
+
+(define-syntax (step-n syn)
+  (syntax-case syn ()
+    [(_ n expr)
+     (for/fold
+       ([expr #'expr])
+       ([i (in-range (syntax->datum #'n))])
+       #`(step #,expr))]))
+
 (define-syntax (query-type syn)
   (syntax-case syn ()
     [(_ term)