commit 4b247149b2cab12e334c2c108114344fb80b94af
parent efb01eb662d9a565684dbf491831944cef40b11a
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Wed, 23 Aug 2017 00:05:31 +0200
Some changes to the row formalisation. Fixed some math layout.
Diffstat:
10 files changed, 138 insertions(+), 122 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -774,7 +774,7 @@ Finally, the type and semantics of primitive functions are expressed using the
@include-equation["deltarules.rkt"]
-@subsubsub*section{Soundness proof}
+@subsubsub*section{Soundness}
Since @typedracket is an existing language which we use for our
implementation, and not a new language, we do not provide here a full proof of
diff --git a/from-dissertation-tobin-hochstadt/simplify.rkt b/from-dissertation-tobin-hochstadt/simplify.rkt
@@ -14,12 +14,12 @@
@simplify[@∩τ[@un[@repeatset{τ}] @repeatset{σ}]]
&= @propagate⊥(@un[@repeatset{@simplify[@∩τ[τ @repeatset{σ}]]}])\\
@simplify[@∩τ[@consτ[τ τ′] @consτ[σ σ′]]]
- &= @(∩τ @${@propagate⊥(@(consτ @simplify[@∩τ[τ σ]]
- @simplify[@∩τ[τ′ σ′]]))})\\
+ &= @${@propagate⊥(@(consτ @simplify[@∩τ[τ σ]]
+ @simplify[@∩τ[τ′ σ′]]))}\\
@simplify[@∩τ[@repeatset{σ}]]
&= \begin{cases}
- ⊥ & @textif ∃ τ, τ′ ∈ \{@repeatset{σ}\} . @no-overlap(τ, τ′) \\
- @∩τ[@repeatset{@simplify[σ]}] &@otherwise
+ ⊥ & \hspace{-1.5em}@textif ∃ τ, τ′ ∈ \{@repeatset{σ}\} . @no-overlap(τ, τ′) \\
+ @∩τ[@repeatset{@simplify[σ]}] &\hspace{-1em}@otherwise
\end{cases}
\end{aligned}
}
diff --git a/from-dissertation-tobin-hochstadt/trules.rkt b/from-dissertation-tobin-hochstadt/trules.rkt
@@ -80,9 +80,9 @@
φ⁻_f
o_f]]}
@${@Γ[⊢ @mapop[e_f e_r] @R[@polydot[@${τ@subst[β ↦ α]} α]
- ϵ
- ⊥
- ∅]]}
+ ϵ
+ ⊥
+ ∅]]}
@${@textsc{T-DMap}}]
#:T-AbsPred
@@ -136,6 +136,7 @@
ϵ
∅])
ϵ ⊥ ∅]]}
+ #:wide #t
@${@textsc{T-DAbs}}]
#:T-TAbs
@@ -221,7 +222,7 @@
@$inferrule[@${@repeated[#:n "n"]{Δ ⊢ τⱼ} \\
@repeated[#:n "m"]{Δ ⊢ τₖ} \\
@Γ[⊢ @${e@_op} @R[@∀r[(@repeated[#:n "n"]{αⱼ} @polydotα[β]) τ]
- φ⁺ φ⁻ o]]}
+ φ⁺ φ⁻ o]]}
@Γ[⊢ @at[@${e@_op} @repeated[#:n "n"]{τⱼ} @repeated[#:n "m"]{τₖ}]
@R[@transdots[@${τ@subst[@repeated[#:n "n"]{aⱼ ↦ τⱼ}]}
@${β}
@@ -234,7 +235,7 @@
@$inferrule[@${@repeated{Δ ⊢ τₖ} \\
Δ ▷ @polydot[τ_r β] \\
@Γ[⊢ @${e@_op} @R[@∀r[(@repeated{αₖ} @polydotα[α_r]) τ]
- φ⁺ φ⁻ o]]}
+ φ⁺ φ⁻ o]]}
@Γ[⊢ @at[@${e@_op} @repeated{τₖ} @polydot[τ_r β]]
@R[@substdots[@${τ@subst[@repeated{aₖ ↦ τₖ}]}
@${α_r}
@@ -307,10 +308,10 @@
@aligned{
@no-overlap(τ, τ′) &= @metatrue
&&@textif ∄ σ .\begin{aligned}[t]
- &@<:[σ τ]\\
- {}\mathbin{∧}{} &@<:[σ τ′]\\
- {}\mathbin{∧}{} &Δ ⊢ σ\\
- {}\mathbin{∧}{} &@≠:[σ ⊥]\end{aligned}\\
+ &@<:[σ τ]\\
+ {}\mathbin{∧}{} &@<:[σ τ′]\\
+ {}\mathbin{∧}{} &Δ ⊢ σ\\
+ {}\mathbin{∧}{} &@≠:[σ ⊥]\end{aligned}\\
@no-overlap(τ, σ) &= @metafalse
&&@otherwise
}
diff --git a/scribblings/adt-row-opsem.scrbl b/scribblings/adt-row-opsem.scrbl
@@ -91,6 +91,7 @@ indexed by a constructor label or a field label, like @${@ctor-pred[@κ]},
↪ @recordv[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}}
@${\quad @|ɐ|ⱼ = v'}] \\
(@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}}
+ #:wide #t
@${@textsc{E-Record-With}_1}]
@todo{what to do with the = sign? The a = v sign is syntactical, but could
@@ -106,4 +107,5 @@ indexed by a constructor label or a field label, like @${@ctor-pred[@κ]},
@${@opwithout[@recordv[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ}]
↪ @recordv[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}}] \\
(@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}}
+ #:wide #t
@${@textsc{E-Record-Without}}]
diff --git a/scribblings/adt-row-pe.scrbl b/scribblings/adt-row-pe.scrbl
@@ -2,6 +2,7 @@
@require["util.rkt"
"adt-utils.rkt"
+ scriblib/render-cond
(for-label (only-meta-in 0 typed/racket))]
@(use-mathjax)
@@ -43,26 +44,39 @@ a conditional.
&= @ctorτ[@κ @${@update(τ, σ_π)}]\\@;TODO: update rule when the π is ɐ or getval
}
-@aligned{
+@$${
@restrict(@variantτ[@repeatset{τ}], σ)
- &= @variantτ[@repeatset{@restrict(τ,σ)}]\\
- @restrict(
- @recordτ[@ρf
- @repeatset{-@|ɐ|ᵢ}
- @repeatset{-@|ɐ|ⱼ}
- @repeatset{+@|ɐ|ₗ : τₗ}
- @repeatset{+@|ɐ|ₘ : τₘ}],@; TODO: this does not handle the regular per-field update like above?
- @recordτ[@ρf
- @repeatset{-@|ɐ|ᵢ}
- @repeatset{-@|ɐ|ₖ}
- @repeatset{+@|ɐ|ₗ : σₗ}
- @repeatset{+@|ɐ|ₙ : σₙ}])
- &= @recordτ[@repeatset{-@|ɐ|ᵢ}
- @repeatset{-@|ɐ|ⱼ}
- @repeatset{-@|ɐ|ₖ}
- @repeatset{+@|ɐ|ₗ : @update(τₗ, σₗ)}
- @repeatset{+@|ɐ|ₘ : τₘ}
- @repeatset{+@|ɐ|ₙ : σₙ}]\\
+ = @variantτ[@repeatset{@restrict(τ,σ)}]
+}
+@$${
+ @cond-element[
+ [html @${\begin{multline}}]
+ [else @${\begin{multlined}}]]
+ @|restrict|\left(\begin{aligned}
+ &@recordτ[@ρf
+ @repeatset{-@|ɐ|ᵢ}
+ @repeatset{-@|ɐ|ⱼ}
+ @repeatset{+@|ɐ|ₗ : τₗ}
+ @repeatset{+@|ɐ|ₘ : τₘ}],
+ \\@; TODO: this does not handle the regular per-field update like above?
+ &@recordτ[@ρf
+ @repeatset{-@|ɐ|ᵢ}
+ @repeatset{-@|ɐ|ₖ}
+ @repeatset{+@|ɐ|ₗ : σₗ}
+ @repeatset{+@|ɐ|ₙ : σₙ}]\end{aligned}\right)
+ \\
+ = @recordτ[@repeatset{-@|ɐ|ᵢ}
+ @repeatset{-@|ɐ|ⱼ}
+ @repeatset{-@|ɐ|ₖ}
+ @repeatset{+@|ɐ|ₗ : @update(τₗ, σₗ)}
+ @repeatset{+@|ɐ|ₘ : τₘ}
+ @repeatset{+@|ɐ|ₙ : σₙ}]
+ @cond-element[
+ [html @${\end{multline}}]
+ [else @${\end{multlined}}]]
+}
+
+@$${
@where @disjoint-sets(
@repeatSet{@|ɐ|ᵢ},
@repeatSet{@|ɐ|ⱼ},
diff --git a/scribblings/adt-row-sub.scrbl b/scribblings/adt-row-sub.scrbl
@@ -37,11 +37,17 @@
@recordτ[@|ρf| @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τ'ⱼ}]]
@${@textsc{S-RecordF}}]
-@$inferrule[
- @${@repeated{@<:[τₖ τ′ₖ]}}
- @<:[@recordτ[@|ρf| @repeatset{-@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ} @repeatset{+@|ɐ|ₖ:τₖ}]
- @recordτ[@|ρf| @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ₖ:τ'ₖ}]]
- @${@textsc{S-FRecordF}}]
+@$inferrule[@${@repeated{@<:[τₖ τ′ₖ]}}
+ @<:[@recordτ[@|ρf|
+ @repeatset{-@|ɐ|ᵢ}
+ @repeatset{-@|ɐ|ⱼ}
+ @repeatset{+@|ɐ|ₖ:τₖ}
+ @repeatset{+@|ɐ|ₗ:τₗ}]
+ @recordτ[@|ρf|
+ @repeatset{-@|ɐ|ᵢ}
+ @repeatset{+@|ɐ|ₖ:τ'ₖ}]]
+ #:wide #t
+ @${@textsc{S-FRecordF}}]
@$inferrule[@${@<:[@${τ[@repeated{@|ρf|ᵢ ↦ @|ρf|′ᵢ}]} σ]}
@${@<:[@∀f[(@repeated{@|ρf|ᵢ}) τ]
diff --git a/scribblings/adt-row-te.scrbl b/scribblings/adt-row-te.scrbl
@@ -17,12 +17,20 @@
@${@textsc{TE-FAll}}]
-@$inferrule[@${@ρc ∈ Δ \\
- \{@repeated{@|κ|ᵢ}\} ∩ \{@repeated{@|κ|ⱼ}\} = ∅ \\
- @alldifferent(@repeated{@|κ|ᵢ}) \\
- @alldifferent(@repeated{@|κ|ⱼ})}
- @${Δ ⊢ @variantτ[@ρc @repeatset{-@|κ|ᵢ} @repeatset{+@κof[ⱼ τⱼ]}]}
- @${@textsc{TE-CVariant}}]
+@$p[
+ @$inferrule[@${@ρc ∈ Δ \\
+ \{@repeated{@|κ|ᵢ}\} ∩ \{@repeated{@|κ|ⱼ}\} = ∅ \\
+ @alldifferent(@repeated{@|κ|ᵢ}) \\
+ @alldifferent(@repeated{@|κ|ⱼ})}
+ @${Δ ⊢ @variantτ[@ρc @repeatset{-@ctorτ[@|κ|ᵢ]}
+ @repeatset{+@ctorτ[@κof[ⱼ τⱼ]]}]}
+ @${@textsc{TE-CVariant}}]
+
+ @$inferrule[@${@ρf ∈ Δ \\
+ @alldifferent(@repeated{@|ɐ|ᵢ} @repeated{@|ɐ|ⱼ}) \\
+ @repeated{Δ ⊢ τⱼ}}
+ @${Δ ⊢ @recordτ[@ρf @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τⱼ}]}
+ @${@textsc{TE-FRecord}}]]
where
@@ -33,13 +41,7 @@ where
\end{aligned}
}
-@$inferrule[@${@ρf ∈ Δ \\
- \{@repeated{@|ɐ|ᵢ}\} ∩ \{@repeated{@|ɐ|ⱼ}\} = ∅ \\
- @alldifferent(@repeated{@|ɐ|ᵢ}) \\
- @alldifferent(@repeated{@|ɐ|ⱼ}) \\
- @repeated{Δ ⊢ τⱼ}}
- @${Δ ⊢ @recordτ[@ρf @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τⱼ}]}
- @${@textsc{TE-FRecord}}]
+
@$inferrule[@${@alldifferent(@repeated{@|κ|ᵢ}) \\
@repeated{Δ ⊢ τᵢ}}
diff --git a/scribblings/adt-row-trules.scrbl b/scribblings/adt-row-trules.scrbl
@@ -50,28 +50,21 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
= @applyfilter(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
τ, o)}
@${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r}
- @${@textsc{T-Ctor-Val}}
- ]
+ @${@textsc{T-Ctor-Val}}]
}
-@$${
- @$inferrule[
+@$inferrule[
@${@repeated{Γ ⊢ eᵢ : τᵢ ; φᵢ ; oᵢ}}
@${Γ ⊢ @recorde[@repeated{@|ɐ|ᵢ = eᵢ}]
- : @recordτ[@repeated{@|ɐ|ᵢ : τᵢ}]; ϵ|⊥ ; ∅}
- @${@textsc{T-Record-Build}}
- ]
-}
+ : @recordτ[@repeated{@|ɐ|ᵢ : τᵢ}]; ϵ|⊥ ; ∅}
+ @${@textsc{T-Record-Build}}]
-@$${
- @$inferrule[
+@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
- φ_r = @applyfilter(@recordτ[@repeated{@|ɐ|ᵢ : ⊤}]
- |\overline{@recordτ[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)}
+ φ_r = @applyfilter(@recordτ[@repeated{@|ɐ|ᵢ : ⊤}]
+ |\overline{@recordτ[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)}
@${Γ ⊢ (@record-pred[@repeated{@|ɐ|ᵢ}] e) : Boolean ; φ_r ; ∅}
- @${@textsc{T-Record-Pred}}
- ]
-}
+ @${@textsc{T-Record-Pred}}]
@$${
@cond-element[[latex @list{\let\savedamp&}] [else ""]]
@@ -85,61 +78,52 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
= @applyfilter(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
τ, o)}
@${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r}
- @${@textsc{T-Record-GetField}}
- ]
+ @${@textsc{T-Record-GetField}}]
}
-@$${
- @$inferrule[
+@$inferrule[
@${
- Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
- τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ}
- @${@ρf - \{@repeated{@|ɐ|'ⱼ}\}}]\\@;c
- Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\
- @|ɐ| ∉ \{@|ɐ|ᵢ\} \\
- @|ɐ| ∈ \{@repeated{@|ɐ|'ⱼ}\}
- }
+ Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
+ τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ}
+ @${@ρf - \{@repeated{@|ɐ|'ⱼ}\}}]\\@;c
+ Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\
+ @|ɐ| ∉ \{@|ɐ|ᵢ\} \\
+ @|ɐ| ∈ \{@repeated{@|ɐ|'ⱼ}\}
+ }
@${Γ ⊢ @opwith[@${e_{r}} @|ɐ| @${e_{v}}]
- : @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ}
- @${@|ɐ| : τ_{v}}
- @${@ρf - \{@repeated{@|ɐ|'ⱼ}\}}]@;changed
- ; ϵ|⊥ ; ∅}
+ : @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ}
+ @${@|ɐ| : τ_{v}}
+ @${@ρf - \{@repeated{@|ɐ|'ⱼ}\}}]@;changed
+ ; ϵ|⊥ ; ∅}
@${@textsc{T-Record-With}_1}
]
-}
TODO: removing fields on the ρ should not matter if the fields are present in
the main part of the record (as they are implicitly not in the ρ, because they
are in the main part).
-@$${
- @$inferrule[
- @${
- Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
- τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\@;changed
- Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\
- @|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ}
- }
- @${Γ ⊢ @opwith[@${e_{r}} @${@|ɐ|ⱼ} @${e_{v}}]
- : @recordτ[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}
- @${@|ɐ|ⱼ : τ_{v}}
- @ρf]@;changed
- ; ϵ|⊥ ; ∅}
- @${@textsc{T-Record-With}_2}
- ]
-}
-
-@$${
- @$inferrule[
- @${
- Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
- τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\
- @|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ}
- }
- @${Γ ⊢ @opwithout[@${e_{r}} @|ɐ|]
- : @recordτ[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}
- @${@ρf - @|ɐ|}]
- ; ϵ|⊥ ; ∅}
- @${@textsc{T-Record-Without}}
- ]
-}
+@$inferrule[@${
+ Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
+ τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\@;changed
+ Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\
+ @|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ}
+ }
+ @${Γ ⊢ @opwith[@${e_{r}} @${@|ɐ|ⱼ} @${e_{v}}]
+ : @recordτ[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}
+ @${@|ɐ|ⱼ : τ_{v}}
+ @ρf]@;changed
+ ; ϵ|⊥ ; ∅}
+ #:wide #t
+ @${@textsc{T-Record-With}_2}]
+
+@$inferrule[@${
+ Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
+ τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\
+ @|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ}
+ }
+ @${Γ ⊢ @opwithout[@${e_{r}} @|ɐ|]
+ : @recordτ[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}
+ @${@ρf - @|ɐ|}]
+ ; ϵ|⊥ ; ∅}
+ #:wide #t
+ @${@textsc{T-Record-Without}}]
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -123,11 +123,11 @@
(Λf* @${(@(add-between (list ρ ...) "\\ "))} e))
(define-syntax-rule (Λfv (ρ ...) e)
(Λf* @${(@(add-between (list ρ ...) "\\ "))} e))
-(define-syntax ∀r* (defop @${\mathbf{∀}}))
+(define-syntax ∀r* (defop @${@mathbm{∀}}))
(define-syntax-rule (∀r (α ...) τ)
(∀r* @${(@(add-between (list (stringify α) ...) "\\ "))} τ))
-(define-syntax ∀c* (defop @${\mathbf{∀}_{@textbf{c}}}))
-(define-syntax ∀f* (defop @${\mathbf{∀}_{@textbf{f}}}))
+(define-syntax ∀c* (defop @${@mathbm{∀}_{@textbf{c}}}))
+(define-syntax ∀f* (defop @${@mathbm{∀}_{@textbf{f}}}))
(define-syntax-rule (∀c (ρ ...) τ)
(∀c* @${(@(add-between (list (stringify ρ) ...) "\\ "))} τ))
(define-syntax-rule (∀f (ρ ...) τ)
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -507,23 +507,30 @@ EOTEX
(define tr≤: ($ "\\mathrel{≤:_\\mathit{tr}}"))
(define $ooo ($ (mathtext "\\textit{ooo}")))
-(define ($inferrule from* to* [label '()])
+(define ($inferrule #:wide [wide? #f] from* to* [label '()])
@$$[
(elem #:style
(style #f (list (tex-addition
(string->bytes/utf-8
"\\usepackage{mathpartir}"))))
- ($ (cond-element [html "\\frac{\\begin{gathered}"]
- [else (string-append "\\ifcsname savedamp\\endcsname"
- "\\else\\let\\savedamp&\\fi"
- "\\inferrule{")])
+ ($ (cond-element
+ [html ""]
+ [else (string-append "\\ifcsname savedamp\\endcsname"
+ "\\else\\global\\let\\savedamp&\\fi")])
+ (if wide?
+ @${\begin{aligned}\vphantom{x}&@|label|\\ \vphantom{x}&}
+ '())
+ (cond-element [html "\\frac{\\begin{gathered}"]
+ [else "\\inferrule{"])
(if (eq? from* -) "\\vphantom{x}" from*)
(cond-element [html "\\end{gathered}}{\\begin{gathered}"]
[else "}{"])
(if (eq? to* -) "\\vphantom{x}" to*)
(cond-element [html "\\end{gathered}}"]
[else "}"])
- "\\ " label))])
+ (if wide?
+ "\\end{aligned}"
+ (list @${\ } label))))])
(define htmldiff-css-experiment #<<EOCSS
.version:after {
