commit efb01eb662d9a565684dbf491831944cef40b11a
parent 4372fef6073fc716340fb770fec83f6a6974fad8
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Mon, 21 Aug 2017 22:19:07 +0200
Used different fonts and capitalization for ctor and record when used as an expression, value and type
Diffstat:
16 files changed, 283 insertions(+), 250 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -701,6 +701,8 @@ The @update operator can then apply @restrict to perform the intersection of
the type indicated by the @|ifop|'s condition and the currently-known type for
the subpart of the considered variable.
+@todo{How do @restrict and @remove behave on intersections?}
+
@include-equation["trules.rkt" restrict]
The @update operator can also apply
diff --git a/from-dissertation-tobin-hochstadt/subtyping.rkt b/from-dissertation-tobin-hochstadt/subtyping.rkt
@@ -192,14 +192,14 @@
@$inferrule[
@${∃ i . @<:[τ @${σᵢ}]}
- @${@<:[τ @${⋃ @repeated{σᵢ}}]}
+ @${@<:[τ @un[@repeated{σᵢ}]]}
@${@textsc{S-UnionSuper}}]
#:S-UnionSub
@$inferrule[
@${@repeated[@<:[τᵢ @${σ}]]}
- @${@<:[@${⋃ @repeated{τᵢ}} σ]}
+ @${@<:[@un[@repeated{τᵢ}] σ]}
@${@textsc{S-UnionSub}}]
#:S-Pair
diff --git a/from-dissertation-tobin-hochstadt/trules.rkt b/from-dissertation-tobin-hochstadt/trules.rkt
@@ -289,7 +289,7 @@
@aligned{
@restrict(τ, σ) &= ⊥ &@textif @no-overlap(τ,σ)\\
- @restrict((⋃ @repeatset{τ}), σ) &= (⋃ @repeatset{@restrict(τ,σ)}) &\\
+ @restrict(@un[@repeatset{τ}], σ) &= @un[@repeatset{@restrict(τ,σ)}] &\\
@restrict(τ, σ) &= τ &@textif @<:[τ σ]\\
@restrict(τ, σ) &= σ &@otherwise
}
@@ -298,7 +298,7 @@
@aligned{
@remove(τ, σ) &= ⊥ &@textif @<:[τ σ] \\
- @remove((⋃ @repeatset{τ}), σ) &= (⋃ @repeatset{@remove(τ,σ)}) &\\
+ @remove(@un[@repeatset{τ}], σ) &= @un[@repeatset{@remove(τ,σ)}] &\\
@remove(τ, σ) &= τ &@otherwise
}
@@ -306,11 +306,11 @@
@aligned{
@no-overlap(τ, τ′) &= @metatrue
- &&@textif ∄ σ .
- \quad @<:[σ τ]\quad
- ∧ \quad@<:[σ τ′]\quad
- ∧ \quadΔ ⊢ σ\quad
- ∧ \quad@≠:[σ ⊥]\\
+ &&@textif ∄ σ .\begin{aligned}[t]
+ &@<:[σ τ]\\
+ {}\mathbin{∧}{} &@<:[σ τ′]\\
+ {}\mathbin{∧}{} &Δ ⊢ σ\\
+ {}\mathbin{∧}{} &@≠:[σ ⊥]\end{aligned}\\
@no-overlap(τ, σ) &= @metafalse
&&@otherwise
}
diff --git a/scribblings/adt-row-Ectx.scrbl b/scribblings/adt-row-Ectx.scrbl
@@ -11,12 +11,12 @@
@$${
@cases["E" #:first-sep "⩴"
@acase{…}
- @acase{@ctor[@κ E]@tag*{constructor instance}}
+ @acase{@ctore[@κ E]@tag*{constructor instance}}
@acase{(@ctor-pred[@κ]\ E)@tag*{constructor predicate}}
@acase{(@ctor-val[@κ]\ E)@tag*{constructor value access}}
- @acase{@record[@repeated{@|ɐ|ᵢ = vᵢ}
- @${@|ɐ|ⱼ = E}
- @repeated{@|ɐ|ₖ = eₖ}]@tag*{record instance}}
+ @acase{@recorde[@repeated{@|ɐ|ᵢ = vᵢ}
+ @${@|ɐ|ⱼ = E}
+ @repeated{@|ɐ|ₖ = eₖ}]@tag*{record instance}}
@acase{(@record-pred[@repeatset{@|ɐ|ᵢ}]\ E)@tag*{record predicate}}
@acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ E)
@tag*{row-polymorphic record predicate}}
diff --git a/scribblings/adt-row-e.scrbl b/scribblings/adt-row-e.scrbl
@@ -22,7 +22,7 @@ the value stored in an instance of a constructor.
@cases*[
"e" #:first-sep "⩴"
@acase{…}
- @acase{@ctor[@κ e]@tag*{constructor instance}}
+ @acase{@ctore[@κ e]@tag*{constructor instance}}
@acase{(@ctor-pred[@κ]\ e)@tag*{constructor predicate}}
@acase{(@ctor-val[@κ]\ e)@tag*{constructor value access}}
@interpar{
@@ -39,11 +39,11 @@ the value stored in an instance of a constructor.
the @ɐ field.
}
@acase{…}
- @acase{@record[@repeated{@↦e[@${@|ɐ|ᵢ} eᵢ]}]@tag*{record instance}}
+ @acase{@recorde[@repeated{@↦e[@${@|ɐ|ᵢ} eᵢ]}]@tag*{record instance}}
@acase{(@record-pred[@repeatset{@|ɐ|ᵢ}]\ e)@tag*{record predicate}}
@acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ e)
@tag*{row-record predicate}}@;added
- @acase{e.@|ɐ|@tag*{record field access}}
+ @acase{@record-gete[e @|ɐ|]@tag*{record field access}}
@acase{@opwith[e @|ɐ| e]@tag*{record update (new/change field)}}
@acase{@opwithout[e @|ɐ|]@tag*{record update (remove field)}}
@interpar{
diff --git a/scribblings/adt-row-opsem.scrbl b/scribblings/adt-row-opsem.scrbl
@@ -26,21 +26,13 @@
@todo{Does this need any change when adding row typing (they don't add any
rules in @~cite["tobin-hochstadt_typed_2010"])?}
-@$${
- @$inferrule[
- @${\phantom{x}}
- @${@ctor[@κ v] ↪ @ctor[@κ v]}
- @${@textsc{E-Ctor-Build}}
- ]
-}
+@$inferrule[-
+ @${@ctore[@κ v] ↪ @ctorv[@κ v]}
+ @${@textsc{E-Ctor-Build}}]
-@$${
- @$inferrule[
- @${\phantom{x}}
- @${(@ctor-pred[@κ] v) ↪ δ(@ctor-pred[@κ], v)}
- @${@textsc{E-Ctor-Pred}}
- ]
-}
+@$inferrule[-
+ @${(@ctor-pred[@κ] v) ↪ δ(@ctor-pred[@κ], v)}
+ @${@textsc{E-Ctor-Pred}}]
We extend the @${δ} relation to accept in its first position not only constant
functions (members of @${c}), but also members of families of operators
@@ -49,94 +41,69 @@ indexed by a constructor label or a field label, like @${@ctor-pred[@κ]},
@$${
@aligned{
- δ(@ctor-pred[@κ], v) &= \#t &@textif v = @ctor[@κ @${v'}] \\
- δ(@ctor-pred[@κ], v) &= \#f & @text[" otherwise"] \\
+ δ(@ctor-pred[@κ], v) &= \#t &@textif v = @ctorv[@κ @${v'}] \\
+ δ(@ctor-pred[@κ], v) &= \#f &@otherwise \\
}
}
@todo{Is it really necessary to use a δ-rule for E-Ctor-GetVal ?}
-@$${
- @$inferrule[
- @${\phantom{x}}
- @${(@ctor-val[@κ] v) ↪ δ(@ctor-val[@κ], v)}
- @${@textsc{E-Ctor-GetVal}}
- ]
-}
+@$inferrule[-
+ @${(@ctor-val[@κ] v) ↪ δ(@ctor-val[@κ], v)}
+ @${@textsc{E-Ctor-GetVal}}]
@$${
@aligned{
- δ(@ctor-val[@κ], @ctor[@κ @${v'}]) & = @${v'}
+ δ(@ctor-val[@κ], @ctorv[@κ @${v'}]) & = @${v'}
}
}
-@$${
- @$inferrule[
- @${\phantom{x}}
- @${@record[@repeated{@|ɐ|ᵢ = vᵢ}] ↪ @record[@repeated{@|ɐ|ᵢ = vᵢ}]}
- @${@textsc{E-Record-Build}}
- ]
-}
+@$inferrule[-
+ @${@recorde[@repeated{@|ɐ|ᵢ = vᵢ}]
+ ↪ @recordv[@repeated{@|ɐ|ᵢ = vᵢ}]}
+ @${@textsc{E-Record-Build}}]
-@$${
- @$inferrule[
- @${\phantom{x}}
- @${(@record-pred[@repeated{@|ɐ|ᵢ}] v) ↪ δ(@record-pred[@repeated{@|ɐ|ᵢ}], v)}
- @${@textsc{E-Record-Pred}}
- ]
-}
+@$inferrule[-
+ @${(@record-pred[@repeated{@|ɐ|ᵢ}] v)
+ ↪ δ(@record-pred[@repeated{@|ɐ|ᵢ}], v)}
+ @${@textsc{E-Record-Pred}}]
@$${
@aligned{
δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#t
- @textif v = @record[@repeated{@|ɐ|ⱼ = vⱼ}] ∧ @repeatset{@|ɐ|ⱼ} = @repeatset{@|ɐ|ᵢ}
+ @textif v = @recordv[@repeated{@|ɐ|ⱼ = vⱼ}]
+ ∧ @repeatset{@|ɐ|ⱼ} = @repeatset{@|ɐ|ᵢ}
\\
- δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#f @text[" otherwise"]
+ δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#f @otherwise
}
}
-@$${
- @$inferrule[
- @${@|ɐ|' ∈ @repeatset{@|ɐ|ᵢ} \\ @|ɐ|' = @|ɐ|ⱼ}
- @${@record[@repeated{@|ɐ|ᵢ = vᵢ}].@|ɐ|' ↪ vⱼ}
- @${@textsc{E-Record-GetField}}
- ]
-}
+@$inferrule[@${@|ɐ|' ∈ @repeatset{@|ɐ|ᵢ} \\ @|ɐ|' = @|ɐ|ⱼ}
+ @${@recordv[@repeated{@|ɐ|ᵢ = vᵢ}].@|ɐ|' ↪ vⱼ}
+ @${@textsc{E-Record-GetField}}]
@todo{This ∖ does not make sense because we remove the label @|ɐ|' from a set of
label+value tuples. We must define a separate mathematical operator for removal
of a label+value tuple from a set based on the label.}
-@$${
- @$inferrule[
- @${@|ɐ|ⱼ ∈ @repeatset{@|ɐ|ᵢ}}
- @${@opwith[@record[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ} @${v'}]
- ↪ @record[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}}
- @${\quad @|ɐ|ⱼ = v'}] \\
- (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}}
- @${@textsc{E-Record-With}_1}
- ]
-}
+@$inferrule[@${@|ɐ|ⱼ ∈ @repeatset{@|ɐ|ᵢ}}
+ @${@opwith[@recordv[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ} @${v'}]
+ ↪ @recordv[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}}
+ @${\quad @|ɐ|ⱼ = v'}] \\
+ (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}}
+ @${@textsc{E-Record-With}_1}]
@todo{what to do with the = sign? The a = v sign is syntactical, but could
easily be understood as a meta comparison, instead of indicating the
association between the field and the value.}
-@$${
- @$inferrule[
- @${@|ɐ|' ∉ @repeatset{@|ɐ|ᵢ}}
- @${@opwith[@record[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|'} @${v'}]
- ↪ @record[@repeatset{@|ɐ|ᵢ = vᵢ} @${\quad @${@|ɐ|'} = v'}]}
- @${@textsc{E-Record-With}_2}
- ]
-}
+@$inferrule[@${@|ɐ|' ∉ @repeatset{@|ɐ|ᵢ}}
+ @${@opwith[@recordv[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|'} @${v'}]
+ ↪ @recordv[@repeatset{@|ɐ|ᵢ = vᵢ} @${\quad @${@|ɐ|'} = v'}]}
+ @${@textsc{E-Record-With}_2}]
-@$${
- @$inferrule[
- @${@|ɐ|ⱼ ∈ @repeatset{@|ɐ|ᵢ}}
- @${@opwithout[@record[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ}]
- ↪ @record[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}}] \\
- (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}}
- @${@textsc{E-Record-Without}}
- ]
-}
-\ No newline at end of file
+@$inferrule[@${@|ɐ|ⱼ ∈ @repeatset{@|ɐ|ᵢ}}
+ @${@opwithout[@recordv[@repeated{@|ɐ|ᵢ = vᵢ}] @${@|ɐ|ⱼ}]
+ ↪ @recordv[@${@repeatset{@|ɐ|ᵢ = vᵢ} ∖ \{@|ɐ|ⱼ = vⱼ\}}] \\
+ (@|ɐ|ⱼ = vⱼ) ∈ @repeatset{@|ɐ|ᵢ = vᵢ}}
+ @${@textsc{E-Record-Without}}]
diff --git a/scribblings/adt-row-pe.scrbl b/scribblings/adt-row-pe.scrbl
@@ -12,8 +12,8 @@
@cases[@pe #:first-sep "⩴"
@acase{…}
- @acase{@πctor-val @tag*{value of the constructor}}
- @acase{@|ɐ| @tag*{field value}}]
+ @acase{@πctor-val @tag*{value of constructor}}
+ @acase{@|ɐ| @tag*{value of field @|ɐ|}}]
We extend the metafunctions for paths given
in@~cite[#:precision "pp. 65 and 75" "tobin-hochstadt_typed_2010"]. The @${
@@ -27,11 +27,60 @@ a conditional.
@todo{How should I note cleanly these removals / replacements which refer to
an @|ɐ| and its τ or @${v} inside the set of @${@|ɐ|ᵢ}?}
+@todo{Also write down the simple "update" cases for row polymorphism}
+
@aligned{
- @update(@record[@repeated{@|ɐ|ᵢ : τᵢ}ⁿ], υ_{π∷@|ɐ|ⱼ})
- &= @record[@${@repeated{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}}
- @${@|ɐ|ⱼ : @${@update(τⱼ, υ_π)}}]
+ @update(@recordτ[@repeatset{@|ɐ|ᵢ : τᵢ}], σ_{π∷@|ɐ|ⱼ})
+ &= @recordτ[@${@repeatset{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}}
+ @${@|ɐ|ⱼ : @${@update(τⱼ, σ_π)}}]
+ \\
+ @update(@recordτ[@repeatset{@|ɐ|ᵢ : τᵢ}], @!{σ}_{π∷@|ɐ|ⱼ})
+ &= @recordτ[@${@repeatset{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}}
+ @${@|ɐ|ⱼ : @${@update(τⱼ, @!{σ}_π)}}]
\\
&\quad @where @|ɐ|ⱼ : τⱼ ∈ @repeatset{@|ɐ|ᵢ : τᵢ}\\
- @update(@ctor[@κ τ], υ_{π∷@πctor-val})
- &= @ctor[@κ @${@update(τ, υ_π)}]}
-\ No newline at end of file
+ @update(@ctorτ[@κ τ], σ_{π∷@πctor-val})
+ &= @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{+@|ɐ|ₙ : σₙ}]\\
+ @where @disjoint-sets(
+ @repeatSet{@|ɐ|ᵢ},
+ @repeatSet{@|ɐ|ⱼ},
+ @repeatSet{@|ɐ|ₖ},
+ @repeatSet{@|ɐ|ₗ},
+ @repeatSet{@|ɐ|ₘ},
+ @repeatSet{@|ɐ|ₙ})
+}
+
+where
+
+@aligned{
+ @disjoint-sets(@repeated{s})
+ &= @metatrue @textif ∀ sᵢ, sⱼ ∈ s . i ≠ j ⇒ sᵢ ∩ sⱼ = ∅\\
+ @disjoint-sets(@repeated{s})
+ &= @metafalse @otherwise
+}
+
+@aligned{
+ @remove(@variantτ[@repeatset{τ}], σ) &= @variantτ[@repeatset{@remove(τ,σ)}]
+}
diff --git a/scribblings/adt-row-shorthands.scrbl b/scribblings/adt-row-shorthands.scrbl
@@ -9,20 +9,20 @@
#:version (version-text)]{Shorthands (with ρ)}
The polymorphic builder function for the @κ constructor which
-intuitively corresponds to @ctor[κ] can be written as the η-expansion of the
-@ctor[κ e] operator:
+intuitively corresponds to @ctore[κ] can be written as the η-expansion of the
+@ctore[κ e] operator:
-@$${(Λ (α) (λ ([x : α]) @ctor[κ x]))}
+@$${@Λe[(α) @λe[(@${x : α}) @ctore[κ x]]]}
The same applies to the predicate form of constructors:
-@$${(λ ([x : ⊤]) (@ctor-pred[κ] x))}
+@$${@λe[(@${x : ⊤}) @app[@ctor-pred[κ] x]]}
The same applies to the accessor for a constructor's encapsulated value:
-@$${(Λ (α) (λ ([x : @ctor[κ α]]) (@ctor-val[κ] α))}
+@$${@Λe[(α) @λe[(@${x : @ctorτ[κ α]}) @app[@ctor-val[κ] x]]]}
-As a convenience, we will write @ctor[κ], @ctor-pred[κ] and @ctor-val[κ] as a
+As a convenience, we will write @ctore[κ], @ctor-pred[κ] and @ctor-val[κ] as a
shorthand for the above lambda functions.
As per the typing rules given in @secref{adt-row-trules}, these functions have
@@ -31,25 +31,21 @@ the following types:
@htodo{The rules below are the same??? Probably an unfinished copy-paste}
@$inferrule[-
- @${Γ ⊢ @ctor[κ] : (∀ (α) (α → @ctor[κ α])) ; ϵ|⊥ ; ∅}
- @${@textsc{T-Abs}}]
-
-@$inferrule[-
- @${Γ ⊢ @ctor[κ] : (∀ (α) (α → @ctor[κ α])) ; ϵ|⊥ ; ∅}
- @${…}]
+ @${Γ ⊢ @ctorτ[κ] : @∀r[(α) @f→[(α) @R[@ctorτ[κ α] ϵ ⊥ ∅]]]}
+ @${@textsc{T-Shorthand-Ctor}}]
@todo{Write their types here too.}
The polymorphic builder function for a record which
-intuitively corresponds to @record[@repeated{@ɐ}] can be written as the
-η-expansion of the @record[@repeated{@ɐ = e}] operator:
+intuitively corresponds to @recorde[@repeated{@ɐ}] can be written as the
+η-expansion of the @recorde[@repeated{@ɐ = e}] operator:
@$${
- (Λ (@repeated{αᵢ}) (λ (@repeated{[xᵢ : αᵢ]}) @record[@repeated{@|ɐ|ᵢ = xᵢ}]))
+ @Λe[(@repeated{αᵢ}) @λe[(@repeated{xᵢ : αᵢ}) @recorde[@repeated{@|ɐ|ᵢ = xᵢ}]]]
}
-The same applies to the predicate form of records:
+The same applies to the predicate forms of record types:
@;{
@$${
@@ -57,22 +53,25 @@ The same applies to the predicate form of records:
&(λ ([x : ⊤])\\
&\quad(Λ (@repeated{αᵢ})\\
&\qquad(λ (@repeated{[pᵢ : (⊤ \xrightarrow[∅]{αᵢ|\overline{αᵢ}} Boolean)]})\\
- &\qquad\quad(@record-pred[@repeated{@|ɐ|ᵢ ? pᵢ}] x))}\\
+ &\qquad\quad(@record-pred[@repeatset{@|ɐ|ᵢ ? pᵢ}] x))}\\
}
}
@$${
- @aligned{
- &(λ ([x : ⊤])\\
- &\quad(@record-pred[@repeated{@|ɐ|ᵢ}] x))}\\
+ \begin{gathered}
+ @λe[(@${x : ⊤}) @app[@record-pred[@repeatset{@|ɐ|ᵢ}] x]] \\
+ @λe[(@${x : ⊤}) @app[@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}] x]]
+ \end{gathered}
}
-The same applies to the accessor for a constructor's encapsulated value:
+The same applies to the accessor for a field of a record:
-@$${(Λ (α) (λ ([x : @ctor[κ α]]) (@ctor-val[κ] α))}
+@$${@Λe[(α) @Λfe[(@ρf) @λe[(@${x : @recorde[@ρf @${+@|ɐ|:τ}]})
+ @record-gete[x @ɐ]]]]}
@todo{Write their types here too.}
-As a convenience, we will write @ctor[κ], @ctor-pred[κ] and @ctor-val[κ] as a
-shorthand for the above lambda functions.
-
+As a convenience, we will write @recorde[@repeated{@ɐ}],
+@record-pred[@repeatset{@|ɐ|ᵢ}],
+@record-pred[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}] and @record-gete[ɐ] as
+shorthands for the above lambda functions.
diff --git a/scribblings/adt-row-sub.scrbl b/scribblings/adt-row-sub.scrbl
@@ -8,51 +8,72 @@
@title[#:style (with-html5 manual-doc-style)
#:version (version-text)]{Subtyping (with ρ)}
-@;{
- @$${
- @$inferrule[
- @${\phantom{x}}
- @${⊢ @ctor[@κ τ] <: @ctorTop[τ]}
- @${@textsc{S-CtorTop}}
- ]
- }
-}
+@$inferrule[@${∃ i . @<:[τ @${σᵢ}]}
+ @${@<:[τ @variantτ[@repeated{σᵢ}]]}
+ @${@textsc{S-VariantSuper}}]
-@$${
- @$inferrule[
- @${⊢ τ <: τ'}
- @${⊢ @ctor[@κ τ] <: @ctor[@κ @${τ'}]}
- @${@textsc{S-Ctor}}
- ]
-}
+@$inferrule[@${@repeated[@<:[τᵢ @${σ}]]}
+ @${@<:[@variantτ[@repeated{τᵢ}] σ]}
+ @${@textsc{S-VariantSub}}]
-@$${
- @$inferrule[
- @${@repeated{⊢ τᵢ <: τ'ᵢ}}
- @${⊢ @record[@repeated{@${@|ɐ|ᵢ : τᵢ}}] <: @record[@repeated{@${@|ɐ|ᵢ : τ'ᵢ}}]}
- @${@textsc{S-Record}}
- ]
-}
+
+@;{@$inferrule[-
+ @<:[@ctorτ[@κof[τ]] @ctorTop[τ]]
+ @${@textsc{S-CtorTop}}]}
+
+@$inferrule[
+ @${@<:[τ τ′]}
+ @<:[@ctorτ[@κof[τ]] @ctorτ[@κof[τ′]]]
+ @${@textsc{S-Ctor}}]
+
+@$inferrule[
+ @${@repeated{@<:[τᵢ τ′ᵢ]}}
+ @<:[@recordτ[@repeated{@${@|ɐ|ᵢ : τᵢ}}] @recordτ[@repeated{@${@|ɐ|ᵢ : τ'ᵢ}}]]
+ @${@textsc{S-Record}}]
+
+@$inferrule[
+ @${@repeated{@<:[τⱼ τ′ⱼ]}}
+ @<:[@recordτ[@repeated{@${@|ɐ|ⱼ : τⱼ}}]
+ @recordτ[@|ρf| @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τ'ⱼ}]]
+ @${@textsc{S-RecordF}}]
+
+@$inferrule[
+ @${@repeated{@<:[τₖ τ′ₖ]}}
+ @<:[@recordτ[@|ρf| @repeatset{-@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ} @repeatset{+@|ɐ|ₖ:τₖ}]
+ @recordτ[@|ρf| @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ₖ:τ'ₖ}]]
+ @${@textsc{S-FRecordF}}]
+
+@$inferrule[@${@<:[@${τ[@repeated{@|ρf|ᵢ ↦ @|ρf|′ᵢ}]} σ]}
+ @${@<:[@∀f[(@repeated{@|ρf|ᵢ}) τ]
+ @∀f[(@repeated{@|ρf|′ᵢ}) σ]]}
+ @${@textsc{S-PolyF-}α@textsc{-Equiv}}]
+
+@$inferrule[@${@<:[@${τ[@repeated{@|ρc|ᵢ ↦ @|ρc|′ᵢ}]} σ]}
+ @${@<:[@∀c[(@repeated{@|ρc|ᵢ}) τ]
+ @∀c[(@repeated{@|ρc|′ᵢ}) σ]]}
+ @${@textsc{S-PolyC-}α@textsc{-Equiv}}]
+
+@$inferrule[-
+ @=:[@variantτ[] ⊥]
+ @${@textsc{S-Variant-Empty}}]
+
+@; TODO: can these rules be used to combine a record type and a record*?
+@; predicate to make sure some fields are absent, without checking anything
+@; for the other fields?
@; TODO: instantiation rules. ∀ rules. Etc.
-@$${
- @$inferrule[
- @${@repeated{⊢ τⱼ <: τ'ⱼ}}
- @${⊢ @record[@repeated{@ρf @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τⱼ}}]
- <: @record[@repeated{@ρf @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τ'ⱼ}}]}
- @${@textsc{S-Record-Row}}
- ]
-}
-Permutation of the fields of a record type produces an equivalent type:
+@;{
+ Permutation of the fields of a record type produces an equivalent type:
-@$${
- @$inferrule[
+ @$${
+ @$inferrule[
@${\phantom{x}}
- @${⊢ @record[@repeated{@${@|ɐ|ᵢ : τᵢ}} @repeated{@${@|ɐ|ⱼ : τⱼ}}]
- <: @record[@repeated{@${@|ɐ|ⱼ : τⱼ}} @repeated{@${@|ɐ|ᵢ : τᵢ}}]}
+ @<:[@recordτ[@repeated{@${@|ɐ|ᵢ : τᵢ}} @repeated{@${@|ɐ|ⱼ : τⱼ}}]
+ @recordτ[@repeated{@${@|ɐ|ⱼ : τⱼ}} @repeated{@${@|ɐ|ᵢ : τᵢ}}]]
@${@textsc{S-Record-Permuation}}
]
+ }
}
@todo{propagate our types up/down unions like the primitive ones (I think
diff --git a/scribblings/adt-row-tausigma.scrbl b/scribblings/adt-row-tausigma.scrbl
@@ -24,8 +24,8 @@ constructors or fields.
@cases["σ,τ" #:first-sep "⩴"
@acase{…}
- @acase{@ctor[@κof[τ]]@tag*{constructor}} @; same
- @acase{@record[@ςf]@tag*{possibly row-polymorphic record}} @; changed
+ @acase{@ctorτ[@κof[τ]]@tag*{constructor}} @; same
+ @acase{@recordτ[@ςf]@tag*{possibly row-polymorphic record}} @; changed
@acase{@∀c[(@repeated{@ρc}) τ]
@tag*{row-polymorphic abstraction (constructors)}} @; new
@acase{@∀f[(@repeated{@ρf}) τ]
@@ -44,7 +44,7 @@ constructors in the row type can be specified on variants.
@cases["σ,τ" #:first-sep "⩴"
@acase{…}
- @acase{@variant[@ςf]
+ @acase{@variantτ[@ςf]
@tag*{possibly row-polymorphic variant}}] @; new/changed
A variant acts as the union of multiple constructor types. The variant type
diff --git a/scribblings/adt-row-te.scrbl b/scribblings/adt-row-te.scrbl
@@ -17,13 +17,12 @@
@${@textsc{TE-FAll}}]
-@$inferrule[
- @${@ρc ∈ Δ \\
- \{@repeated{@|ɐ|ᵢ}\} ∩ \{@repeated{@|ɐ|ⱼ}\} = ∅ \\
- @alldifferent(@repeated{@|ɐ|ᵢ}) \\
- @alldifferent(@repeated{@|ɐ|ⱼ})}
- @${Δ ⊢ @record[@ρf @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τⱼ}]}
- @${@textsc{TE-FAllDifferent}}]
+@$inferrule[@${@ρc ∈ Δ \\
+ \{@repeated{@|κ|ᵢ}\} ∩ \{@repeated{@|κ|ⱼ}\} = ∅ \\
+ @alldifferent(@repeated{@|κ|ᵢ}) \\
+ @alldifferent(@repeated{@|κ|ⱼ})}
+ @${Δ ⊢ @variantτ[@ρc @repeatset{-@|κ|ᵢ} @repeatset{+@κof[ⱼ τⱼ]}]}
+ @${@textsc{TE-CVariant}}]
where
@@ -34,47 +33,24 @@ where
\end{aligned}
}
-@$inferrule[
- @${@ρf ∈ Δ \\
- \{@repeated{@|ɐ|ᵢ}\} ∩ \{@repeated{@|ɐ|ⱼ}\} = ∅ \\
- @alldifferent(@repeated{@|ɐ|ᵢ}) \\
- @alldifferent(@repeated{@|ɐ|ⱼ})}
- @${Δ ⊢ @record[@ρf @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τⱼ}]}
- @${@textsc{TE-FAllDifferent}}]
-
-@;{TODO: if we extend rows with subtraction, we may need to allow it either in
- function types or within bodies too.
-
- @$${
- @$inferrule[
- @${Δ ∪ \{ @ρc \} ⊢ τ}
- @${Δ ⊢ ???}
- @${@textsc{TE-CFun}}
- ]
- }
-
- @$${
- @$inferrule[
- @${Δ ∪ \{ @ρf \} ⊢ τ}
- @${Δ ⊢ ???}
- @${@textsc{TE-FFun}}
- ]
- }
-}
-
-@$${
- @$inferrule[
- @${@ρc ∈ Δ \\ @repeated{Δ ⊢ τᵢ}}
- @${Δ ⊢ @variant[@repeated{@ctor[@|κ|ᵢ τᵢ]} @ρc]}
- @${@textsc{TE-CVariant}}
- ]
-}
-
-@$${
- @$inferrule[
- @${@ρf ∈ Δ \\ @repeated{Δ ⊢ τᵢ}}
- @${Δ ⊢ @record[@repeated{@|ɐ|ᵢ : τᵢ} @ρf]}
- @${@textsc{TE-FRecord}}
- ]
-}
-
+@$inferrule[@${@ρf ∈ Δ \\
+ \{@repeated{@|ɐ|ᵢ}\} ∩ \{@repeated{@|ɐ|ⱼ}\} = ∅ \\
+ @alldifferent(@repeated{@|ɐ|ᵢ}) \\
+ @alldifferent(@repeated{@|ɐ|ⱼ}) \\
+ @repeated{Δ ⊢ τⱼ}}
+ @${Δ ⊢ @recordτ[@ρf @repeatset{-@|ɐ|ᵢ} @repeatset{+@|ɐ|ⱼ:τⱼ}]}
+ @${@textsc{TE-FRecord}}]
+
+@$inferrule[@${@alldifferent(@repeated{@|κ|ᵢ}) \\
+ @repeated{Δ ⊢ τᵢ}}
+ @${Δ ⊢ @variantτ[@repeated{@ctorτ[@κof[ᵢ τᵢ]]}]}
+ @${@textsc{TE-Variant}}]
+
+@$inferrule[@${@alldifferent(@repeated{@|ɐ|ᵢ}) \\
+ @repeated{Δ ⊢ τᵢ}}
+ @${Δ ⊢ @recordτ[@repeated{@|ɐ|ᵢ : τᵢ}]}
+ @${@textsc{TE-Record}}]
+
+@$inferrule[@${@repeated{Δ ⊢ τ}}
+ @${Δ ⊢ @ctorτ[@κof[τ]]}
+ @${@textsc{TE-Ctor}}]
+\ No newline at end of file
diff --git a/scribblings/adt-row-trules.scrbl b/scribblings/adt-row-trules.scrbl
@@ -15,7 +15,7 @@
@$inferrule[
@${@Γ[⊢ e @R[τ φ⁺ φ⁻ o]]}
- @${@Γ[⊢ @ctor[@κe[e]] @R[@ctor[@κof[τ]] ϵ ⊥ ∅]]}
+ @${@Γ[⊢ @ctore[@κe[e]] @R[@ctorτ[@κof[τ]] ϵ ⊥ ∅]]}
@${@textsc{T-Ctor-Build}}]
@${@applyfilter} is defined
@@ -29,13 +29,11 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@todo{Copy the definition of applyfilter.}
-@$inferrule[
- @${@Γ[⊢ e @R[τ φ⁺ φ⁻ o]] \\
- φ⁺_r / φ⁻_r
- = @applyfilter(@ctor[@κof[⊤]]/\overline{@ctor[@κof[⊤]]}, τ, o)}
- @${@Γ[⊢ @${(@ctor-pred[@κ]\ e)} @R[Boolean φ⁺_r φ⁻_r ∅]]}
- @${@textsc{T-Ctor-Pred}}
- ]
+@$inferrule[@${@Γ[⊢ e @R[τ φ⁺ φ⁻ o]] \\
+ φ⁺_r / φ⁻_r
+ = @applyfilter(@ctorτ[@κof[⊤]]/\overline{@ctorτ[@κof[⊤]]}, τ, o)}
+ @${@Γ[⊢ @${(@ctor-pred[@κ]\ e)} @R[Boolean φ⁺_r φ⁻_r ∅]]}
+ @${@textsc{T-Ctor-Pred}}]
@(define & @cond-element[[latex "\\savedamp"] [else "&"]])
@(define nl @cond-element[[latex "\\csname @arraycr\\endcsname"] [else "\\\\"]])
@@ -43,7 +41,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@cond-element[[latex @list{\let\savedamp&}] [else ""]]
@$inferrule[
- @${Γ ⊢ e : τ ; φ ; o \\ τ <: @ctor[@κ @${τ'}] \\
+ @${Γ ⊢ e : τ ; φ ; o \\ τ <: @ctorτ[@κ @${τ'}] \\
o_r = @"\\left\\{" \begin{array}{rl}
@πctor-val(π(x)) @& @textif o = π(x) @nl
∅ @& @otherwise
@@ -59,8 +57,8 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@$inferrule[
@${@repeated{Γ ⊢ eᵢ : τᵢ ; φᵢ ; oᵢ}}
- @${Γ ⊢ @record[@repeated{@|ɐ|ᵢ = eᵢ}]
- : @record[@repeated{@|ɐ|ᵢ = τᵢ}]; ϵ|⊥ ; ∅}
+ @${Γ ⊢ @recorde[@repeated{@|ɐ|ᵢ = eᵢ}]
+ : @recordτ[@repeated{@|ɐ|ᵢ : τᵢ}]; ϵ|⊥ ; ∅}
@${@textsc{T-Record-Build}}
]
}
@@ -68,8 +66,8 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@$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}}
]
@@ -78,7 +76,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@cond-element[[latex @list{\let\savedamp&}] [else ""]]
@$inferrule[
- @${Γ ⊢ e : τ ; φ ; o \\ τ <: @record[@repeated{@|ɐ|ᵢ : τᵢ} @ρf] \\ @; changed
+ @${Γ ⊢ e : τ ; φ ; o \\ τ <: @recordτ[@repeated{@|ɐ|ᵢ : τᵢ} @ρf] \\ @; changed
o_r = @"\\left\\{" \begin{array}{rl}
@πɐ{@|ɐ|ⱼ}(π(x)) @& @textif o = π(x) @nl
∅ @& @otherwise
@@ -95,15 +93,16 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$inferrule[
@${
Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
- τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ} @${@ρf - \{@repeated{@|ɐ|'ⱼ}\}}]\\@;c
+ τ_{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}
]
@@ -117,14 +116,14 @@ are in the main part).
@$inferrule[
@${
Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
- τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\@;changed
+ τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\@;changed
Γ ⊢ e_{v} : τ_{v} ; φ_{v} ; o_{v} \\
@|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ}
}
@${Γ ⊢ @opwith[@${e_{r}} @${@|ɐ|ⱼ} @${e_{v}}]
- : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}
- @${@|ɐ|ⱼ : τ_{v}}
- @ρf]@;changed
+ : @recordτ[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}
+ @${@|ɐ|ⱼ : τ_{v}}
+ @ρf]@;changed
; ϵ|⊥ ; ∅}
@${@textsc{T-Record-With}_2}
]
@@ -134,12 +133,12 @@ are in the main part).
@$inferrule[
@${
Γ ⊢ e_{r} : τ_{r} ; φ_{r} ; o_{r} \\
- τ_{r} <: @record[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\
+ τ_{r} <: @recordτ[@repeated{@|ɐ|ᵢ : τ'ᵢ} @ρf] \\
@|ɐ|ⱼ : τ'ⱼ ∈ @repeatset{@|ɐ|ᵢ : τ'ᵢ}
}
@${Γ ⊢ @opwithout[@${e_{r}} @|ɐ|]
- : @record[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}
- @${@ρf - @|ɐ|}]
+ : @recordτ[@${@repeatset{@|ɐ|ᵢ : τ'ᵢ} ∖ \{@|ɐ|ⱼ : τ'ⱼ\}}
+ @${@ρf - @|ɐ|}]
; ϵ|⊥ ; ∅}
@${@textsc{T-Record-Without}}
]
diff --git a/scribblings/adt-row-v.scrbl b/scribblings/adt-row-v.scrbl
@@ -10,5 +10,5 @@
@cases["v" #:first-sep "⩴"
@acase{…}
- @acase{@ctor[@κ v]@tag*{constructor instance}}
- @acase{@record[@repeated{@|ɐ|ᵢ = vᵢ}]@tag*{record instance}}]
+ @acase{@ctorv[@κ v]@tag*{constructor instance}}
+ @acase{@recordv[@repeated{@|ɐ|ᵢ = vᵢ}]@tag*{record instance}}]
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -57,7 +57,9 @@
(define (spaces . l)
(add-between l "\\ "))
-(define-syntax ctor (defop "ctor"))
+(define-syntax ctorτ (defop "Ctor"))
+(define-syntax ctorv (defvop "ctor"))
+(define-syntax ctore (defop "ctor"))
(define κ @${κ})
(define-syntax κof
(syntax-rules ()
@@ -75,8 +77,10 @@
(define-syntax ctorTop (defop "CtorTop"))
(define-syntax-rule (ctor-val κ)
@${\mathbf{getval}_@κ})
-(define-syntax record (defop "record"))
-(define-syntax variant (defop "V"))
+(define-syntax recordτ (defop "Record"))
+(define-syntax recordv (defvop "record"))
+(define-syntax recorde (defop "record"))
+(define-syntax variantτ (defop "V"))
(define-syntax ifop (defop "if"))
(define-syntax mapop (defop "map"))
(define-syntax-rule (λv (arg ...) expr)
@@ -103,7 +107,7 @@
@${\{@(apply repeatset l)\}})
(define |P| @${\ |\ })
(define ρc @${ρ_{c}})
-(define ρf @${ρ_{f}})
+(define ρf @${ϱ_{f}})
(define ςc @${ς_{c}})
(define ςf @${ς_{f}})
(define-syntax at (defop "@"))
@@ -130,6 +134,10 @@
(∀f* @${(@(add-between (list (stringify ρ) ...) "\\ "))} τ))
(define-syntax-rule (ctor-pred c)
@${@(stringify c)@textbf{?}})
+(define-syntax record-gete
+ (syntax-rules ()
+ [(_ e ɐ) @${@(stringify e).@(stringify ɐ)}]
+ [(_ ɐ) @${.@(stringify ɐ)}]))
(define-syntax-rule (record-pred . f*)
@${(@textbf{record?}\ @(stringify . f*))})
(define-syntax-rule (record-pred* . f*)
@@ -185,9 +193,9 @@
(define-syntax (R stx)
(syntax-case stx ()
[(_ to φ⁺ φ⁻ o)
- #'@${\mathbf{❲}@(stringify to)
- \;\mathbf{;}\; @(stringify φ⁺) \mathbf{{/}} @(stringify φ⁻)
- \;\mathbf{;}\; @(stringify o)❳}]
+ #'@${@mathbm{❲}@(stringify to)
+ \;@mathbm{;}\; @(stringify φ⁺) @mathbm{{/}} @(stringify φ⁻)
+ \;@mathbm{;}\; @(stringify o)@mathbm{❳}}]
[self (identifier? #'self)
#'@${\mathrm{R}}]))
@@ -316,4 +324,5 @@
tmp)]))
(define δe @${δ_{\mathrm{e}}})
-(define alldifferent @${\operatorname{alldifferent}})
+(define alldifferent @${\operatorname{AllDifferent}})
+(define disjoint-sets @${\operatorname{DisjointSets}})
+\ No newline at end of file
diff --git a/scribblings/adt.scrbl b/scribblings/adt.scrbl
@@ -14,6 +14,17 @@ from@~cite[#:precision "pp. 62, 72 and 92" "tobin-hochstadt_typed_2010"].
@require["adt-utils.rkt"]
+@subsubsub*section{Notations}
+
+We use the same notations as in
+@secref["from-dissertation-tobin-hochstadt"
+ #:doc '(lib "phc-thesis/scribblings/phc-thesis.scrbl")]. Additionally,
+we use @ρc to denote a row type variable abstracting over a set of constructors,
+and we use @ρf to denote a row type variable abstracting over a set of fields.
+The occurrences of @${c} and @${f} in this context are purely syntactical, and
+only serve the purpose of distinguishing between the two notations — the one for
+constructors, and the one for fields.
+
We define the universe of constructor names @${𝒞} as being equivalent to the
set of strings of unicode characters@htodo{Check in the implementation that
this is not equivalent to the set of symbols, as these cannot be serialised.},
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -694,7 +694,7 @@ EOCSS
[else ($ "\\bm{\\mathit{" l "}}")]))
(define (mathbm . l)
(cond-element
- [html ($ "{\\mathbf " l "}")]
+ [html ($ "{\\mathbf{" l "}}")]
[else ($ "\\bm{\\mathrm{" l "}}")]))
(define (textit . l) ($ (mathtext "\\textit{" l "}")))
(define (textrm . l) ($ (mathtext "\\textrm{" l "}")))
