www

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

stlc+rec-iso.rkt (715B)

      1 #lang turnstile/lang
      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 τ:type-ann e) ≫
     20   #:with (~μ (tv) τ_body) #'τ.norm
     21   [⊢ e ≫ e- ⇐ τ.norm]
     22   --------
     23   [⊢ e- ⇒ #,(subst #'τ.norm #'tv #'τ_body)])
     24 (define-typed-syntax (fld τ:type-ann e) ≫
     25   #:with (~μ (tv) τ_body) #'τ.norm
     26   [⊢ e ≫ e- ⇐ #,(subst #'τ.norm #'tv #'τ_body)]
     27   --------
     28   [⊢ e- ⇒ τ.norm])