www

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

te.rkt (3513B)

      1 #lang at-exp s-exp phc-thesis/scribblings/equations-lang
      2 
      3 @; This file is NOT under the CC0 license, as it contains rules and definitions
      4 @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the
      5 @; permission to copy these rules, but did not ask for a relicensing under the
      6 @; CC0 license.
      7 
      8 #:TE-Var
      9 
     10 @$inferrule[@${α ∈ Δ}
     11             @${Δ ⊢ α}
     12             @${@textsc{TE-Var}}]
     13 
     14 #:TE-DList
     15 
     16 @$inferrule[@${@polydotα[α] ∈ Δ \\ Δ ∪ \{α\} ⊢ τ}
     17             @${Δ ⊢ @List…τ[τ α]}
     18             @${@textsc{TE-DList}}]
     19 
     20 #:TE-All
     21 
     22 @$inferrule[@${Δ ∪ \{@repeated{αᵢ}\} ⊢ τ}
     23             @${Δ ⊢ @∀r[(@repeated{αᵢ}) τ]}
     24             @${@textsc{TE-All}}]
     25 
     26 #:TE-DFun
     27 
     28 @$inferrule[@${Δ ▷ @polydot[τ_r α] \\ @repeated{Δ ⊢ τᵢ} \\ Δ ⊢ τ}
     29             @${Δ ⊢ @f…[(@repeated{τᵢ} @polydot[τ_r α]) @R[τ φ⁺ φ⁻ o]]}
     30             @${@textsc{TE-DFun}}]
     31 
     32 #:TE-DAll
     33 
     34 @$inferrule[@${Δ ∪ \{@repeated{αᵢ}\ @polydotα[β]\} ⊢ τ}
     35             @${Δ ⊢ @∀r[(@repeated{αᵢ} @polydotα[β]) τ]}
     36             @${@textsc{TE-DAll}}]
     37 
     38 #:TE-DPretype
     39 
     40 @$inferrule[@${@polydotα[α] ∈ Δ \\ Δ ∪ \{α\} ⊢ τ}
     41             @${Δ ▷ @polydot[τ α]}
     42             @${@textsc{TE-DPretype}}]
     43 
     44 #:TE-Rec
     45 
     46 @$inferrule[@${Δ ∪ \{r\} ⊢ τ}
     47             @${Δ ⊢ @recτ[r τ]}
     48             @${@textsc{TE-Rec}}]
     49 
     50 #:TE-Trivial
     51 
     52 @$p[
     53  @$inferrule[-
     54              @${Δ ⊢ ⊤}
     55              @${@textsc{TE-Top}}]
     56 
     57  @$inferrule[-
     58              @${Δ ⊢ @num-τ[n]}
     59              @${@textsc{TE-Num}}]
     60        
     61  @$inferrule[-
     62              @${Δ ⊢ @Numberτ}
     63              @${@textsc{TE-Number}}]
     64 
     65  @$inferrule[-
     66              @${Δ ⊢ @true-τ}
     67              @${@textsc{TE-True}}]
     68 
     69  @$inferrule[-
     70              @${Δ ⊢ @false-τ}
     71              @${@textsc{TE-False}}]
     72 
     73  @$inferrule[-
     74              @${Δ ⊢ @symτ[s]}
     75              @${@textsc{TE-Sym}}]
     76 
     77  @$inferrule[-
     78              @${Δ ⊢ @Symbolτ}
     79              @${@textsc{TE-Symbol}}]
     80 
     81  @; function/poly × 5
     82 
     83  @$inferrule[@${@repeated{Δ ⊢ τᵢ}}
     84              @${Δ ⊢ @un[@repeatset{τᵢ}]}
     85              @${@textsc{TE-Union}}]
     86 
     87  @$inferrule[@${@repeated{Δ ⊢ τᵢ}}
     88              @${Δ ⊢ @∩τ[@repeatset{τᵢ}]}
     89              @${@textsc{TE-Intersection}}]
     90 
     91  @$inferrule[@${Δ ⊢ τ \\ Δ ⊢ σ}
     92              @${Δ ⊢ @consτ[τ σ]}
     93              @${@textsc{TE-Pair}}]
     94 
     95  @$inferrule[-
     96              @${Δ ⊢ @null-τ}
     97              @${@textsc{TE-Null}}]
     98 
     99  @$inferrule[@${Δ ⊢_R R}
    100              @${Δ ⊢ @promiseτ[R]}
    101              @${@textsc{TE-Promise}}]
    102  ]
    103 
    104 #:TE-R
    105 
    106 ;; No particular restrictions on the object at this point (should we put some to
    107 ;; make sure that it exists?)
    108 @$inferrule[@${Δ ⊢ τ \\ Δ ⊢_{\mathrm{φ}} φ⁺ \\ Δ ⊢_{\mathrm{φ}} φ⁻}
    109             @${Δ ⊢_R @R[τ φ⁺ φ⁻ o]}
    110             @${@textsc{TE-R}}]
    111 
    112 #:TE-Phi
    113 
    114 @$inferrule[@${@repeated{Δ ⊢_{\mathrm{ψ}} ψ}}
    115             @${Δ ⊢_{\mathrm{φ}} @repeatset{ψ}}
    116             @${@textsc{TE-Phi}}]
    117 
    118 #:TE-Psi
    119 
    120 ;; TODO? should we impose that the @loc is within scope, and that the π is
    121 ;; valid? (same thing for the o in TE-R?)
    122 @$inferrule[@${@repeated{Δ ⊢ τ}}
    123             @${Δ ⊢_{\mathrm{ψ}} τ_{π(@loc)}}
    124             @${@textsc{TE-Psi}}]
    125 
    126 #:TE-Psi-Not
    127 
    128 @$inferrule[@${@repeated{Δ ⊢ τ}}
    129             @${Δ ⊢_{\mathrm{ψ}} @!{τ}_{π(@loc)}}
    130             @${@textsc{TE-Psi-Not}}]
    131 
    132 #:TE-Psi-Bot
    133 
    134 @$inferrule[-
    135             @${Δ ⊢_{\mathrm{ψ}} ⊥}
    136             @${@textsc{TE-Psi-Bot}}]