diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt index f0c425c..aa1141f 100644 --- a/curnel/redex-core.rkt +++ b/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) diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt index 094a713..b8ca1e7 100644 --- a/curnel/redex-lang.rkt +++ b/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) diff --git a/scribblings/reflection.scrbl b/scribblings/reflection.scrbl index b49b206..3bfef87 100644 --- a/scribblings/reflection.scrbl +++ b/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))] "" "")) +] +} diff --git a/scribblings/stdlib/sugar.scrbl b/scribblings/stdlib/sugar.scrbl index 251d678..4955957 100644 --- a/scribblings/stdlib/sugar.scrbl +++ b/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}. diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt index 54ad6c6..23c1eb2 100644 --- a/stdlib/sugar.rkt +++ b/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)