www

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

stlc+lit.rkt (537B)

      1 #lang turnstile/lang
      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) ≫
     21    --------
     22    [⊢ (#%datum- . n) ⇒ Int]]
     23   [(_ . x) ≫
     24    --------
     25    [#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])