adt-row-opsem.scrbl (3844B)
1 #lang scribble/manual 2 3 @require["util.rkt" 4 "adt-utils.rkt" 5 (for-label (only-meta-in 0 typed/racket))] 6 @(use-mathjax) 7 8 @title[#:style (with-html5 manual-doc-style) 9 #:version (version-text)]{Operational Semantics (with ρ)} 10 11 @list{ 12 Instantiation of the new sorts of polymorphic abstractions is a no-op at 13 run-time, similarly to those of @|typedracket|. 14 15 @;; New: 16 @$p[@$inferrule[- 17 @${@atc[@Λcv[(@repeated{@ρc}) e] @repeated{@ςc}] ↪ e} 18 @${@textsc{E-Inst-C}}] 19 20 @$inferrule[- 21 @${@atf[@Λfv[(@repeated{@ρc}) e] @repeated{@ςf}] ↪ e} 22 @${@textsc{E-Inst-F}}]] 23 } 24 25 26 @todo{Does this need any change when adding row typing (they don't add any 27 rules in @~cite["tobin-hochstadt_typed_2010"])?} 28 29 @$inferrule[- 30 @${@ctore[@κ v] ↪ @ctorv[@κ v]} 31 @${@textsc{E-Ctor-Build}}] 32 33 @$inferrule[- 34 @${(@ctor-pred[@κ] v) ↪ δ(@ctor-pred[@κ], v)} 35 @${@textsc{E-Ctor-Pred}}] 36 37 We extend the @${δ} relation to accept in its first position not only constant 38 functions (members of @${c}), but also members of families of operators 39 indexed by a constructor label or a field label, like @${@ctor-pred[@κ]}, 40 @${@ctor-val[@κ]} and @record-pred[@repeated{@|ɐ|ᵢ}] 41 42 @$${ 43 @aligned{ 44 δ(@ctor-pred[@κ], v) &= \#t &@textif v = @ctorv[@κ @${v'}] \\ 45 δ(@ctor-pred[@κ], v) &= \#f &@otherwise \\ 46 } 47 } 48 49 @todo{Is it really necessary to use a δ-rule for E-Ctor-GetVal ?} 50 51 @$inferrule[- 52 @${(@ctor-val[@κ] v) ↪ δ(@ctor-val[@κ], v)} 53 @${@textsc{E-Ctor-GetVal}}] 54 55 @$${ 56 @aligned{ 57 δ(@ctor-val[@κ], @ctorv[@κ @${v'}]) & = @${v'} 58 } 59 } 60 61 @$inferrule[- 62 @${@recorde[@repeated{@|ɐ|ᵢ = vᵢ}] 63 ↪ @recordv[@repeated{@|ɐ|ᵢ = vᵢ}]} 64 @${@textsc{E-Record-Build}}] 65 66 @$inferrule[- 67 @${(@record-pred[@repeated{@|ɐ|ᵢ}] v) 68 ↪ δ(@record-pred[@repeated{@|ɐ|ᵢ}], v)} 69 @${@textsc{E-Record-Pred}}] 70 71 @$${ 72 @aligned{ 73 δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#t 74 @textif v = @recordv[@repeated{@|ɐ|ⱼ = vⱼ}] 75 ∧ @repeatset{@|ɐ|ⱼ} = @repeatset{@|ɐ|ᵢ} 76 \\ 77 δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#f @otherwise 78 } 79 } 80 81 @$inferrule[@${@|ɐ|' ∈ @repeatset{@|ɐ|ᵢ} \\ @|ɐ|' = @|ɐ|ⱼ} 82 @${@recordv[@repeated{@|ɐ|ᵢ = vᵢ}].@|ɐ|' ↪ vⱼ} 83 @${@textsc{E-Record-GetField}}] 84 85 86 @todo{This ∖ does not make sense because we remove the label @|ɐ|' from a set of 87 label+value tuples. We must define a separate mathematical operator for removal 88 of a label+value tuple from a set based on the label.} 89 @$inferrule[@${@|ɐ|ⱼ ∈ @repeatset{@|ɐ|ᵢ}} 90 @${@opwith[@recordv[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ} @${v'}] 91 ↪ @recordv[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}} 92 @${\quad @|ɐ|ⱼ = v'}] \\ 93 (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}} 94 #:wide #t 95 @${@textsc{E-Record-With}_1}] 96 97 @todo{what to do with the = sign? The a = v sign is syntactical, but could 98 easily be understood as a meta comparison, instead of indicating the 99 association between the field and the value.} 100 101 @$inferrule[@${@|ɐ|' ∉ @repeatset{@|ɐ|ᵢ}} 102 @${@opwith[@recordv[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|'} @${v'}] 103 ↪ @recordv[@repeatset{@|ɐ|ᵢ = vᵢ} @${\quad @${@|ɐ|'} = v'}]} 104 @${@textsc{E-Record-With}_2}] 105 106 @$inferrule[@${@|ɐ|ⱼ ∈ @repeatset{@|ɐ|ᵢ}} 107 @${@opwithout[@recordv[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ}] 108 ↪ @recordv[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}}] \\ 109 (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}} 110 #:wide #t 111 @${@textsc{E-Record-Without}}]