From e54c7e5bb53f682bcf40053d6406eabbee8f944e Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Fri, 25 Sep 2015 20:08:07 -0400
Subject: [PATCH] Added query-type command to sugar

---
 curnel/redex-lang.rkt          |  7 +++++--
 scribblings/stdlib/sugar.scrbl | 11 ++++++++---
 stdlib/sugar.rkt               | 11 ++++++++++-
 3 files changed, 23 insertions(+), 6 deletions(-)

diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt
index 07fe348..0926082 100644
--- a/curnel/redex-lang.rkt
+++ b/curnel/redex-lang.rkt
@@ -17,6 +17,7 @@
   ;; Basic syntax
   for-syntax
   only-in
+  except-in
   all-defined-out
   rename-in
   rename-out
@@ -44,9 +45,9 @@
     [dep-top-interaction #%top-interaction]
 
     ;      [dep-datum #%datum]
-    [dep-define define])
+    [dep-define define]
+    [dep-void void])
   begin
-  void
   Type
   ;; DYI syntax extension
   define-syntax
@@ -415,6 +416,8 @@
      (syntax->curnel-syntax
        (quasisyntax/loc syn (elim D T)))]))
 
+(define-syntax-rule (dep-void) (void))
+
 ;; TODO: Not sure if this is the correct behavior for #%top
 (define-syntax (dep-top syn)
   (syntax-case syn ()
diff --git a/scribblings/stdlib/sugar.scrbl b/scribblings/stdlib/sugar.scrbl
index 62b33db..251d678 100644
--- a/scribblings/stdlib/sugar.scrbl
+++ b/scribblings/stdlib/sugar.scrbl
@@ -149,10 +149,15 @@ Necessary for more advanced types, like @racket[And], because @racket[case] is n
 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)]
 
 }
+
+@defform[(query-type expr)]{
+Print the type of @racket[expr], at compile-time. Similar to Coq's @racketfont{Check}.
+
+@examples[#:eval curnel-eval
+          (query-type Bool)]
+
+}
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index 3a11ce8..54ad6c6 100644
--- a/stdlib/sugar.rkt
+++ b/stdlib/sugar.rkt
@@ -1,4 +1,4 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../curnel/redex-lang.rkt"
 (provide
   ->
   ->*
@@ -16,6 +16,7 @@
   case
   case*
   run
+  query-type
 
   ;; don't use these
   define-theorem
@@ -122,6 +123,14 @@
   (syntax-case syn ()
     [(_ expr) (normalize/syn #'expr)]))
 
+(define-syntax (query-type syn)
+  (syntax-case syn ()
+    [(_ term)
+     (begin
+       (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (type-infer/syn #'term)))
+       ;; Void is undocumented and a hack, but sort of works
+       #'(void))]))
+
 (module+ test
   (require rackunit (submod ".."))