From bf867bca7ff6aa4f9ce5e0629e41acfa658b7c11 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Fri, 25 Sep 2015 13:36:44 -0400
Subject: [PATCH] Moved some features out of curnel

* run is user-definable through the existing reflection features; moved
  to sugar.
* define need not have special function support in curnel; moved to
  sugar.
* fixed relevant documentation
---
 curnel/redex-lang.rkt          | 17 +++++------------
 scribblings/reflection.scrbl   | 13 -------------
 scribblings/stdlib/sugar.scrbl | 11 +++++++++++
 stdlib/sugar.rkt               |  6 +++++-
 4 files changed, 21 insertions(+), 26 deletions(-)

diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt
index 7485aa9..13987f8 100644
--- a/curnel/redex-lang.rkt
+++ b/curnel/redex-lang.rkt
@@ -63,8 +63,7 @@
     type-infer/syn
     type-check/syn?
     normalize/syn
-    cur-equal?)
-  run)
+    cur-equal?))
 
 (begin-for-syntax
   ;; TODO: Gamma and Sigma seem to get reset inside a module+
@@ -194,7 +193,10 @@
     reified-term)
 
   ;; Reflection tools
-  ;; TODO: Why is this not just (define (normalize/syn syn) (denote syn syn))
+  #| TODO:
+   | Why is this not just (define (normalize/syn syn) (denote syn syn))?
+   | Well, because that has a very different meaning. Apparently.
+   |#
   (define (normalize/syn syn)
     (denote
       syn
@@ -227,13 +229,6 @@
         (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
-;; wrapped in syntax bla. This is bad.
-;; TODO: Should be provided by user-land code.
-(define-syntax (run syn)
-  (syntax-case syn ()
-    [(_ expr) (normalize/syn #'expr)]))
-
 ;; -----------------------------------------------------------------
 ;; Require/provide macros
 
@@ -456,8 +451,6 @@
 
 (define-syntax (dep-define syn)
   (syntax-parse syn
-    [(_ (name:id (x:id : t)) e)
-     #'(dep-define name (dep-lambda (x : t) e))]
     [(_ id:id e)
      (let ([e (cur->datum #'e)]
            [id (syntax->datum #'id)])
diff --git a/scribblings/reflection.scrbl b/scribblings/reflection.scrbl
index 332d527..b49b206 100644
--- a/scribblings/reflection.scrbl
+++ b/scribblings/reflection.scrbl
@@ -71,19 +71,6 @@ Runs the Cur term @racket[syn] to a value.
 ]
 }
 
-
-@defform[(run syn)]{
-Like @racket[normalize/syn], but is a syntactic form which allows a Cur term to be written by
-computing part of the term from another Cur term.
-
-@margin-note{This one is a real working example, assuming the @racketmodname[cur/stdlib/bool] and
-@racketmodname[cur/stdlib/nat] are loaded. Also, could be moved outside the privileged code.}
-
-@examples[#:eval curnel-eval
-          (lambda (x : (run (if true Bool Nat))) x)]
-
-}
-
 @defproc[(cur-equal? [e1 syntax?] [e2 syntax?])
          boolean?]{
 Returns @racket[#t] if the Cur terms @racket[e1] and @racket[e2] and equivalent according to
diff --git a/scribblings/stdlib/sugar.scrbl b/scribblings/stdlib/sugar.scrbl
index 55eb301..4b1a932 100644
--- a/scribblings/stdlib/sugar.scrbl
+++ b/scribblings/stdlib/sugar.scrbl
@@ -104,3 +104,14 @@ defined.
              IH: ((_ : Bool))
              false])]
 }
+@defform[(run syn)]{
+Like @racket[normalize/syn], but is a syntactic form which allows a Cur term to be written by
+computing part of the term from another Cur term.
+
+@margin-note{This one is a real working example, assuming the @racketmodname[cur/stdlib/bool] and
+@racketmodname[cur/stdlib/nat] are loaded. Also, could be moved outside the privileged code.}
+
+@examples[#:eval curnel-eval
+          (lambda (x : (run (if true Bool Nat))) x)]
+
+}
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index cd0d35b..c0f189c 100644
--- a/stdlib/sugar.rkt
+++ b/stdlib/sugar.rkt
@@ -7,7 +7,8 @@
   #%app
   define
   case
-  define-type)
+  define-type
+  run)
 
 (require
   (only-in "../cur.rkt"
@@ -99,3 +100,6 @@
            #'pf #'t))
        #'pf)]))
 
+(define-syntax (run syn)
+  (syntax-case syn ()
+    [(_ expr) (normalize/syn #'expr)]))