adt-trules.scrbl.old (3660B)
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 #:version (version-text)]{Typing rules} 11 12 @todo{Should the filter be something else than @${ϵ|ϵ} or is the filter inferred 13 via other rules when the ``function'' does not do anything special?} 14 15 16 @$${ 17 @$inferrule[ 18 @${Γ ⊢ e : τ ; φ ; o} 19 @${Γ ⊢ @ctor[@κ e] : @ctor[@κ τ] ; ϵ|⊥ ; ∅} 20 @${@textsc{T-Ctor-Build}} 21 ] 22 } 23 24 @${@applyfilter} is defined 25 in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"]. 26 27 @htodo{their second (p. 75) definition of applyfilter does not clearly state 28 that ϵ in τ_ϵ means the empty path (actually, ϵ means an emtpy 29 \overrightarrow{?} for any such sequence. Also, τ_π matches τ, with π = ϵ (and 30 therefore τ_ϵ matches τ). So that's how Number|\overline{Number} gets processed 31 with the updated applyfilter.} 32 33 @$${ 34 @$inferrule[ 35 @${Γ ⊢ e : τ ; φ ; o \\ 36 φ_r 37 = @applyfilter(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)} 38 @${Γ ⊢ (@ctor-pred[@κ] e) : Boolean ; φ_r ; ∅} 39 @${@textsc{T-Ctor-Pred}} 40 ] 41 } 42 43 @$${ 44 @$inferrule[ 45 @${Γ ⊢ e : τ ; φ ; o \\ τ <: @ctor[@κ @${τ'}] \\ 46 o_r = @"\\left\\{" \begin{array}{rl} 47 @πctor-val(π(x)) @& @textif o = π(x) @nl 48 ∅ @& @otherwise 49 \end{array}\right. \\ 50 φ_r 51 = @applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val}, 52 τ, o)} 53 @${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r} 54 @${@textsc{T-Ctor-Val}} 55 ] 56 } 57 58 @$${ 59 @$inferrule[ 60 @${@repeated{Γ ⊢ eᵢ : τᵢ ; φᵢ ; oᵢ}} 61 @${Γ ⊢ @record[@repeated{@|ɐ|ᵢ = eᵢ}] 62 : @record[@repeated{@|ɐ|ᵢ = τᵢ}]; ϵ|⊥ ; ∅} 63 @${@textsc{T-Record-Build}} 64 ] 65 } 66 67 @$${ 68 @$inferrule[ 69 @${Γ ⊢ e : τ ; φ ; o \\ 70 φ_r = @applyfilter(@record[@repeated{@|ɐ|ᵢ : ⊤}] 71 |\overline{@record[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)} 72 @${Γ ⊢ (@record-pred[@repeated{@|ɐ|ᵢ}] e) : Boolean ; φ_r ; ∅} 73 @${@textsc{T-Record-Pred}} 74 ] 75 } 76 77 @$${ 78 @cond-element[[latex @list{\let\savedamp&}] [else ""]] 79 @$inferrule[ 80 @${Γ ⊢ e : τ ; φ ; o \\ τ <: @record[@repeated{@|ɐ|ᵢ : τᵢ}] \\ 81 o_r = @"\\left\\{" \begin{array}{rl} 82 @πɐ{@|ɐ|ⱼ}(π(x)) @& @textif o = π(x) @nl 83 ∅ @& @otherwise 84 \end{array}\right. \\ 85 φ_r 86 = @applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}}, 87 τ, o)} 88 @${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r} 89 @${@textsc{T-Record-GetField}} 90 ] 91 } 92 93 @$${ 94 @$inferrule[ 95 @${ 96 Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\ 97 τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ}] \\ 98 Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\ 99 @|ɐ| ∉ \{@|ɐ|ᵢ\} 100 } 101 @${Γ ⊢ @opwith[@${e_{r}} @|ɐ| @${e_{v}}] 102 : @record[@repeated{@|ɐ|ᵢ : τ'ᵢ} @${@|ɐ| : τ_{v}}] 103 ; ϵ|⊥ ; ∅} 104 @${@textsc{T-Record-With}_1} 105 ] 106 } 107 108 @$${ 109 @$inferrule[ 110 @${ 111 Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\ 112 τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ}] \\ 113 Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\ 114 @|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ} 115 } 116 @${Γ ⊢ @opwith[@${e_{r}} @${@|ɐ|ⱼ} @${e_{v}}] 117 : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}} @${@|ɐ|ⱼ : τ_{v}}] 118 ; ϵ|⊥ ; ∅} 119 @${@textsc{T-Record-With}_2} 120 ] 121 } 122 123 @$${ 124 @$inferrule[ 125 @${ 126 Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\ 127 τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ}] \\ 128 @|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ} 129 } 130 @${Γ ⊢ @opwithout[@${e_{r}} @|ɐ|] 131 : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}] 132 ; ϵ|⊥ ; ∅} 133 @${@textsc{T-Record-Without}} 134 ] 135 }