www

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

stlc+rec-iso.rkt (803B)

      1 #lang s-exp macrotypes/typecheck
      2 (extends "stlc+tup.rkt")
      3 (reuse ∨ var case #:from "stlc+reco+var.rkt")
      4 
      5 ;; stlc + (iso) recursive types
      6 ;; Types:
      7 ;; - types from stlc+tup.rkt
      8 ;; - also ∨ from stlc+reco+var
      9 ;; - μ
     10 ;; Terms:
     11 ;; - terms from stlc+tup.rkt
     12 ;; - also var and case from stlc+reco+var
     13 ;; - fld, unfld
     14 
     15 (provide μ unfld fld)
     16 
     17 (define-binding-type μ #:bvs = 1)
     18 
     19 (define-typed-syntax unfld
     20   [(_ τ:type-ann e)
     21    #:with (~μ (tv) τ_body) #'τ.norm
     22    #:with [e- τ_e] (infer+erase #'e)
     23    #:when (typecheck? #'τ_e #'τ.norm)
     24    (⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))])
     25 (define-typed-syntax fld
     26   [(_ τ:type-ann e)
     27    #:with (~μ (tv) τ_body) #'τ.norm
     28    #:with [e- τ_e] (infer+erase #'e)
     29    #:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body))
     30    (⊢ e- : τ.norm)])