www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

stlc+lit.rkt (549B)

      1 #lang s-exp macrotypes/typecheck
      2 (extends "stlc.rkt")
      3  
      4 ;; Simply-Typed Lambda Calculus, plus numeric literals and primitives
      5 ;; Types:
      6 ;; - types from stlc.rkt
      7 ;; - Int
      8 ;; Terms:
      9 ;; - terms from stlc.rkt
     10 ;; - numeric literals
     11 ;; - prim +
     12 
     13 (provide (type-out Int)
     14          (typed-out [+ : (→ Int Int Int)])
     15          #%datum)
     16 
     17 (define-base-type Int)
     18 
     19 (define-typed-syntax #%datum
     20   [(_ . n:integer) (⊢ #,(syntax/loc stx (#%datum- . n)) : Int)]
     21   [(_ . x)
     22    #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
     23    #'(#%datum- . x)])