adt-row-trules.scrbl (4608B)
1 #lang scribble/manual 2 3 @require["util.rkt" 4 "adt-utils.rkt" 5 scriblib/render-cond 6 (for-label (only-meta-in 0 typed/racket))] 7 @(use-mathjax) 8 9 @title[#:style (with-html5 manual-doc-style) 10 #:tag "adt-row-trules" 11 #:version (version-text)]{Typing rules (with ρ)} 12 13 @todo{Should the filter be something else than @${ϵ|ϵ} or is the filter inferred 14 via other rules when the ``function'' does not do anything special?} 15 16 @$inferrule[ 17 @${@Γ[⊢ e @R[τ φ⁺ φ⁻ o]]} 18 @${@Γ[⊢ @ctore[@κe[e]] @R[@ctorτ[@κof[τ]] ϵ ⊥ ∅]]} 19 @${@textsc{T-Ctor-Build}}] 20 21 @${@applyfilter} is defined 22 in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"]. 23 24 @htodo{their second (p. 75) definition of applyfilter does not clearly state 25 that ϵ in τ_ϵ means the empty path (actually, ϵ means an emtpy 26 \overrightarrow{?} for any such sequence. Also, τ_π matches τ, with π = ϵ (and 27 therefore τ_ϵ matches τ). So that's how Number|\overline{Number} gets processed 28 with the updated applyfilter.} 29 30 @todo{Copy the definition of applyfilter.} 31 32 @$inferrule[@${@Γ[⊢ e @R[τ φ⁺ φ⁻ o]] \\ 33 φ⁺_r / φ⁻_r 34 = @applyfilter(@ctorτ[@κof[⊤]]/\overline{@ctorτ[@κof[⊤]]}, τ, o)} 35 @${@Γ[⊢ @${(@ctor-pred[@κ]\ e)} @R[Boolean φ⁺_r φ⁻_r ∅]]} 36 @${@textsc{T-Ctor-Pred}}] 37 38 @(define & @cond-element[[latex "\\savedamp"] [else "&"]]) 39 @(define nl @cond-element[[latex "\\csname @arraycr\\endcsname"] [else "\\\\"]]) 40 41 @$inferrule[ 42 @${Γ ⊢ e : τ ; φ ; o \\ τ <: @ctorτ[@κ @${τ'}] \\ 43 o_r = @"\\left\\{" \begin{array}{rl} 44 @πctor-val(π(x)) @& @textif o = π(x) @nl 45 ∅ @& @otherwise 46 \end{array}\right. \\ 47 φ_r 48 = @applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val}, 49 τ, o)} 50 @${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r} 51 #:wide 'latex 52 @${@textsc{T-Ctor-Val}}] 53 54 @$inferrule[ 55 @${@repeated{Γ ⊢ eᵢ : τᵢ ; φᵢ ; oᵢ}} 56 @${Γ ⊢ @recorde[@repeated{@|ɐ|ᵢ = eᵢ}] 57 : @recordτ[@repeated{@|ɐ|ᵢ : τᵢ}]; ϵ|⊥ ; ∅} 58 @${@textsc{T-Record-Build}}] 59 60 @$inferrule[ 61 @${Γ ⊢ e : τ ; φ ; o \\ 62 φ_r = @applyfilter(@recordτ[@repeated{@|ɐ|ᵢ : ⊤}] 63 |\overline{@recordτ[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)} 64 @${Γ ⊢ (@record-pred[@repeated{@|ɐ|ᵢ}] e) : Boolean ; φ_r ; ∅} 65 #:wide 'latex 66 @${@textsc{T-Record-Pred}}] 67 68 @$inferrule[ 69 @${Γ ⊢ e : τ ; φ ; o \\ τ <: @recordτ[@repeated{@|ɐ|ᵢ : τᵢ} @ρf] \\ @; changed 70 o_r = @"\\left\\{" \begin{array}{rl} 71 @πɐ{@|ɐ|ⱼ}(π(x)) @& @textif o = π(x) @nl 72 ∅ @& @otherwise 73 \end{array}\right. \\ 74 φ_r 75 = @applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}}, 76 τ, o)} 77 @${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r} 78 #:wide 'latex 79 @${@textsc{T-Record-GetField}}] 80 81 @$inferrule[ 82 @${ 83 Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\ 84 τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ} 85 @${@ρf - \{@repeated{@|ɐ|'ⱼ}\}}]\\@;c 86 Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\ 87 @|ɐ| ∉ \{@|ɐ|ᵢ\} \\ 88 @|ɐ| ∈ \{@repeated{@|ɐ|'ⱼ}\} 89 } 90 @${Γ ⊢ @opwith[@${e_{r}} @|ɐ| @${e_{v}}] 91 : @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ} 92 @${@|ɐ| : τ_{v}} 93 @${@ρf - \{@repeated{@|ɐ|'ⱼ}\}}]@;changed 94 ; ϵ|⊥ ; ∅} 95 #:wide 'latex 96 @${@textsc{T-Record-With}_1} 97 ] 98 99 TODO: removing fields on the ρ should not matter if the fields are present in 100 the main part of the record (as they are implicitly not in the ρ, because they 101 are in the main part). 102 103 @$inferrule[@${ 104 Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\ 105 τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\@;changed 106 Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\ 107 @|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ} 108 } 109 @${Γ ⊢ @opwith[@${e_{r}} @${@|ɐ|ⱼ} @${e_{v}}] 110 : @recordτ[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}} 111 @${@|ɐ|ⱼ : τ_{v}} 112 @ρf]@;changed 113 ; ϵ|⊥ ; ∅} 114 #:wide #t 115 @${@textsc{T-Record-With}_2}] 116 117 @$inferrule[@${ 118 Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\ 119 τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\ 120 @|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ} 121 } 122 @${Γ ⊢ @opwithout[@${e_{r}} @|ɐ|] 123 : @recordτ[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}} 124 @${@ρf - @|ɐ|}] 125 ; ϵ|⊥ ; ∅} 126 #:wide #t 127 @${@textsc{T-Record-Without}}]