commit efa7621c16fd19bb7a74ee58874dcff0801efabd
parent 0a356299287fc18076a03264d573a63dde103669
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Thu, 24 Aug 2017 22:10:48 +0200
Added the detail for some derived rules.
Diffstat:
7 files changed, 130 insertions(+), 58 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -445,7 +445,10 @@ their inclusion in the following semantics would needlessly complicate things.
indicates that @${τ} and @${σ} are not mutually subtypes of each other (but
one can be a strict subtype of the other).
- @$p[@include-equation["subtyping.rkt" S-Reflexive]
+ @$p[@include-equation["subtyping.rkt" S-Eq₁]
+ @include-equation["subtyping.rkt" S-Eq₂]
+ @include-equation["subtyping.rkt" S-Eq₃]
+ @include-equation["subtyping.rkt" S-Reflexive]
@include-equation["subtyping.rkt" S-Transitive]]
The @${⊥} type is a shorthand for the empty union @${(∪)}. It is a subtype of
diff --git a/from-dissertation-tobin-hochstadt/subtyping.rkt b/from-dissertation-tobin-hochstadt/subtyping.rkt
@@ -5,6 +5,27 @@
@; permission to copy these rules, but did not ask for a relicensing under the
@; CC0 license.
+#:S-Eq₁
+
+@$inferrule[
+ @=:[τ σ]
+ @<:[τ σ]
+ @${@textsc{S-Eq}_1}]
+
+#:S-Eq₂
+
+@$inferrule[
+ @=:[τ σ]
+ @<:[σ τ]
+ @${@textsc{S-Eq}_2}]
+
+#:S-Eq₃
+
+@$inferrule[
+ @${@<:[τ σ] \\ @<:[σ τ]}
+ @=:[τ σ]
+ @${@textsc{S-Eq}_3}]
+
#:S-Reflexive
@$inferrule[
@@ -33,8 +54,11 @@
#:S-Bot-Sub
-@$inferrule[@${@refrule[@textsc{S-Bot}] \\
- @refrule[@textsc{S-UnionSub}]}
+@$infertree[((@refrule[@textsc{S-Bot}] ⇒ @refrule[@textsc{S-Eq₁}])
+ @refrule[@textsc{S-UnionSub}]
+ ⇒
+ @refrule[@textsc{S-Transitive}])
+ ⇒
@${@<:[⊥ τ]}
@${@textsc{S-Bot-Sub}}]
diff --git a/scribblings/adt-row-sub.scrbl b/scribblings/adt-row-sub.scrbl
@@ -17,22 +17,38 @@ present in the union, as specified by the type validity rule
@=:[@variantτ[@repeated{τ}] @un[@repeated{τ}]]
@${@textsc{S-Variant-Union}}]
-From @refrule[@textsc{S-Variant-Union}], we can derive that the empty variant is
-equivalent to the bottom type.
-
-@$inferrule[@${@textsc{S-Variant-Union} \\
- @textsc{S-Bot}}
- @=:[@variantτ[] ⊥]
- @${@textsc{S-Variant-Empty}}]
-
-
-@$inferrule[@${∃ i . @<:[τ @${σᵢ}]}
- @${@<:[τ @variantτ[@repeated{σᵢ}]]}
- @${@textsc{S-VariantSuper}}]
-
-@$inferrule[@${@repeated[@<:[τᵢ @${σ}]]}
- @${@<:[@variantτ[@repeated{τᵢ}] σ]}
- @${@textsc{S-VariantSub}}]
+From @refrule[@textsc{S-Variant-Union}], we can derive that the empty variant
+is equivalent to the bottom type.
+
+@$p[@$infertree[(@refrule[@textsc{S-Variant-Union}]
+ @refrule[@textsc{S-Bot}]
+ ⇒
+ @refrule[@textsc{S-Eq-Transitive}])
+ ⇒
+ @=:[@variantτ[] ⊥]
+ @${@textsc{S-Variant-Empty}}]
+ @$infertree[(((@${@=:[τ τ′]} ⇒ @refrule[@${@textsc{S-Eq}_1}])
+ (@${@=:[τ′ τ″]} ⇒ @refrule[@${@textsc{S-Eq}_1}])
+ ⇒
+ @refrule[@textsc{S-Eq-Transitive}])
+ ((@${@=:[τ′ τ″]} ⇒ @refrule[@${@textsc{S-Eq}_2}])
+ (@${@=:[τ τ′]} ⇒ @refrule[@${@textsc{S-Eq}_2}])
+ ⇒
+ @refrule[@textsc{S-Eq-Transitive}])
+ ⇒
+ @refrule[@${@textsc{S-Eq}_3}])
+ ⇒
+ @=:[τ τ″]
+ @${@textsc{S-Eq-Transitive}}]]
+
+
+@$p[@$inferrule[@${∃ i . @<:[τ @${σᵢ}]}
+ @${@<:[τ @variantτ[@repeated{σᵢ}]]}
+ @${@textsc{S-VariantSuper}}]
+
+ @$inferrule[@${@repeated[@<:[τᵢ @${σ}]]}
+ @${@<:[@variantτ[@repeated{τᵢ}] σ]}
+ @${@textsc{S-VariantSub}}]]
diff --git a/scribblings/adt-row-trules.scrbl b/scribblings/adt-row-trules.scrbl
@@ -38,21 +38,18 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@(define & @cond-element[[latex "\\savedamp"] [else "&"]])
@(define nl @cond-element[[latex "\\csname @arraycr\\endcsname"] [else "\\\\"]])
-@$${
- @cond-element[[latex @list{\let\savedamp&}] [else ""]]
- @$inferrule[
+@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\ τ <: @ctorτ[@κ @${τ'}] \\
- o_r = @"\\left\\{" \begin{array}{rl}
- @πctor-val(π(x)) @& @textif o = π(x) @nl
- ∅ @& @otherwise
- \end{array}\right. \\
- φ_r
- = @applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
- τ, o)}
+ o_r = @"\\left\\{" \begin{array}{rl}
+ @πctor-val(π(x)) @& @textif o = π(x) @nl
+ ∅ @& @otherwise
+ \end{array}\right. \\
+ φ_r
+ = @applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
+ τ, o)}
@${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r}
#:wide 'latex
@${@textsc{T-Ctor-Val}}]
-}
@$inferrule[
@${@repeated{Γ ⊢ eᵢ : τᵢ ; φᵢ ; oᵢ}}
@@ -68,21 +65,18 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
#:wide 'latex
@${@textsc{T-Record-Pred}}]
-@$${
- @cond-element[[latex @list{\let\savedamp&}] [else ""]]
- @$inferrule[
+@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\ τ <: @recordτ[@repeated{@|ɐ|ᵢ : τᵢ} @ρf] \\ @; changed
- o_r = @"\\left\\{" \begin{array}{rl}
- @πɐ{@|ɐ|ⱼ}(π(x)) @& @textif o = π(x) @nl
- ∅ @& @otherwise
- \end{array}\right. \\
- φ_r
- = @applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
- τ, o)}
+ o_r = @"\\left\\{" \begin{array}{rl}
+ @πɐ{@|ɐ|ⱼ}(π(x)) @& @textif o = π(x) @nl
+ ∅ @& @otherwise
+ \end{array}\right. \\
+ φ_r
+ = @applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
+ τ, o)}
@${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r}
#:wide 'latex
@${@textsc{T-Record-GetField}}]
-}
@$inferrule[
@${
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -325,7 +325,4 @@
(define δe @${δ_{\mathrm{e}}})
(define alldifferent @${\operatorname{AllDifferent}})
-(define disjoint-sets @${\operatorname{DisjointSets}})
-
-;; Temporary placeholder, will add linking and propper names later.
-(define-syntax-rule (refrule name) name)
-\ No newline at end of file
+(define disjoint-sets @${\operatorname{DisjointSets}})
+\ No newline at end of file
diff --git a/scribblings/phc-thesis.scrbl b/scribblings/phc-thesis.scrbl
@@ -10,8 +10,8 @@
@;@tex-header{\usepackage{morewrites}}
@tex-header{
- \let\realtableofcontents\tableofcontents
- \def\tableofcontents{\realtableofcontents\let\tableofcontents\relax}
+ \let\realtableofcontents\tableofcontents
+ \def\tableofcontents{\realtableofcontents\let\tableofcontents\relax}
}
@title[#:style (struct-update style
@@ -96,7 +96,7 @@
@include-asection[(submod (lib "multi-id/multi-id.hl.rkt") doc)]
@include-asection[
(lib "type-expander/scribblings/type-expander-implementation.scrbl")]
- }]
+ }]
@;{
Notes concerning tikz → SVG conversion:
@@ -118,7 +118,7 @@
See also:
http://tex.stackexchange.com/questions/51757/
- how-can-i-use-tikz-to-make-standalone-svg-graphics
+ how-can-i-use-tikz-to-make-standalone-svg-graphics
To get real, selectable text (must not contain formatting, otherwise some
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -35,6 +35,8 @@
tr≤:
$ooo
$inferrule
+ $infertree
+ refrule
textsc
aligned
acase
@@ -511,7 +513,7 @@ EOTEX
(define tr≤: ($ "\\mathrel{≤:_\\mathit{tr}}"))
(define $ooo ($ (mathtext "\\textit{ooo}")))
-(define ($inferrule #:wide [wide? #f] from* to* [label '()])
+(define ($inferrule from* to* #:wide [wide? #f] [label '()] #:* [*? #f])
(define-syntax-rule (if-wide wide not-wide)
(cond
[(eq? wide? #t)
@@ -526,16 +528,14 @@ EOTEX
(elem #:style
(style #f (list (tex-addition
(string->bytes/utf-8
- "\\usepackage{mathpartir}"))))
- ($ (cond-element
- [html ""]
- [else (string-append "\\ifcsname savedamp\\endcsname"
- "\\else\\global\\let\\savedamp&\\fi")])
- (if-wide
+ (string-append
+ "\\usepackage{mathpartir}"
+ "\\AtBeginDocument{\\global\\let\\savedamp&}")))))
+ ($ (if-wide
@${\begin{aligned}\vphantom{x}&@|label|\\ \vphantom{x}&}
'())
(cond-element [html "\\frac{\\begin{gathered}"]
- [else "\\inferrule{"])
+ [else (list "\\inferrule" (if *? "*" "") "{")])
(if (eq? from* -) "\\vphantom{x}" from*)
(cond-element [html "\\end{gathered}}{\\begin{gathered}"]
[else "}{"])
@@ -546,6 +546,44 @@ EOTEX
"\\end{aligned}"
(list @${\ } label))))])
+;; Temporary placeholder, will add linking and propper names later.
+(define-syntax-rule (refrule name) name)
+
+(begin-for-syntax
+ (define-syntax-class inferimpl
+ #:attributes (x)
+ (pattern {~and x ({~literal refrule} _rule)})
+ (pattern {~and x ({~literal $} . _)})
+ (pattern (from:inferimpl ...
+ {~literal ⇒}
+ to:expr
+ {~optional label:expr})
+ #:with x #`(cond-element
+ [html
+ @${\begin{array}[b]{c}
+ @(add-between (list from.x ...) "\\quad{}")
+ \\\hline
+ @to
+ \end{array}
+ @#,@(if (attribute label)
+ #'{@list{\ \smash{
+ \begin{array}[c]{c}
+ @label
+ \\[1ex]
+ \vphantom{@to}
+ \end{array}}}}
+ #'{})}]
+ [else @$inferrule[(add-between (list from.x ...) "\\ ")
+ to
+ #,@(if (attribute label)
+ #'{@list{\ @label}}
+ #'{})
+ #:* #t]]))))
+(define-syntax $infertree
+ (syntax-parser
+ [(_ . :inferimpl)
+ #'@$${@x}]))
+
(define htmldiff-css-experiment #<<EOCSS
.version:after {
display:block;
