Added query-type command to sugar

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 ()

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)]
+
+}

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 ".."))