parameterize-example.rkt

#lang turnstile
;; this is a silly language that allows the literal #t to be an Int.
;; you can decide lexically which expressions obey this property using (true=>int <expression>)
;; this is a test that the turnstile syntax works, because I don't yet have a "serious" language
;; to test the behavior with
(provide #%datum #%top-interaction true=>int
         (type-out Int Bool))

(define-base-type Int)
(define-base-type Bool)

(define-for-syntax true-is-an-int
  (make-parameter #f))


(define-typed-syntax #%datum
  [(_ . n:integer) ≫
   --------
   [⊢ 'n ⇒ Int]]

  [(_ . b:boolean) ≫
   #:with τ (if (and (syntax-e #'b)
                     (true-is-an-int))
                #'Int
                #'Bool)
   --------
   [⊢ 'b ⇒ τ]])


(define-typed-syntax true=>int
  [(_ e) ≫
   [⊢ [e ≫ e- ⇒ τ] #:with-param true-is-an-int #t]
   --------
   [⊢ e- ⇒ τ]])


(define-typed-syntax #%top-interaction
  [(_ . e) ≫
   [⊢ e ≫ e- ⇒ τ]
   --------
   [≻ (#%app- printf- '"~v : ~a\n"
              e-
              '#,(type->str #'τ))]])


(require "tests/rackunit-typechecking.rkt")

(check-type #t : Bool)
(check-type #f : Bool)
(check-type 123 : Int)

(check-type (true=>int #t) : Int)
(check-type (true=>int #f) : Bool)
(check-type #t : Bool)