commit 0344b94bfd882486a134bb091026167f4e5266c3
parent 92f25bef04476e1eaa7801f51beea8d345f88eff
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Tue, 11 Jul 2017 02:58:21 +0200
More on formalisation, some typography fixes.
Diffstat:
10 files changed, 329 insertions(+), 162 deletions(-)
diff --git a/scribblings/adt-row-e.scrbl b/scribblings/adt-row-e.scrbl
@@ -8,22 +8,60 @@
@title[#:style (with-html5 manual-doc-style)
#:version (version-text)]{Expressions (with ρ)}
-@$${
- @cases["e" #:first-sep "⩴"
- @acase{…}
- @acase{@ctor[@κ e]}
- @acase{(@ctor-pred[@κ] e)}
- @acase{(@ctor-val[@κ] e)}
- @acase{@record[@repeated{@|ɐ|ᵢ = eᵢ}]}
- @acase{(@record-pred[@repeated{@|ɐ|ᵢ}] e)}
- @acase{e.@|ɐ|}
- @acase{@opwith[e @|ɐ| e]}
- @acase{@opwithout[e @|ɐ|]}
- @acase{@Λc[@${(@repeated{@ρc})} e]}@; new
- @acase{@Λf[@${(@repeated{@ρf})} e]}@; new
- @acase{@atc[e @repeated{@ρc}]}@; new
- @acase{@atf[e @repeated{@ρf}]}]@; new
-}
+We extend the syntax of expressions in typed racket as defined
+by@~cite[#:precision "pp. 62, 72 and 92" "tobin-hochstadt_typed_2010"] by
+adding expressions related to constructors. The first syntax builds an
+instance of the constructor with label @|κ| and the value of @${e}. The
+expression @${(@ctor-pred[@κ] e)} determines whether @${e} is an instance of
+the constructor with label @|κ|. The expression @${(@ctor-val[@κ] e)} extracts
+the value stored in an instance of a constructor.
+
+@cases*[
+ "e" #:first-sep "⩴"
+ @acase{…}
+ @acase{@ctor[@κ e]}
+ @acase{(@ctor-pred[@κ] e)}
+ @acase{(@ctor-val[@κ] e)}
+ @intertext{@list[]
+
+ We also introduce expressions related to records. The first builds an instance
+ of a record with the given fields. We note that the order in which the fields
+ appear affects the order in which the sub-expressions will be evaluated.
+ However, in the resulting value and in its type, the order of the fields is
+ irrelevant. The second expression tests whether @${e} is an instance of a
+ record with the given fields present. The third expression is similar, but
+ allows any number of extra fields to be present, while checking that the @${
+ -@|ɐ|ⱼ} fields are absent. The fourth expression accesses the value of the @ɐ
+ field stored in the given instance. The fifth expression updates an existing
+ record instance by adding (or replacing) the field @ɐ, while the sixth removes
+ the @ɐ field.
+
+ @list[]}
+
+ @acase{…}
+ @acase{@record[@repeated{@|ɐ|ᵢ = eᵢ}]}
+ @acase{(@record-pred[@repeated{@|ɐ|ᵢ}] e)}
+ @acase{(@record-pred*[@repeated{@|ɐ|ᵢ} @repeated{-@|ɐ|ⱼ}] e)}@;added
+ @acase{e.@|ɐ|}
+ @acase{@opwith[e @|ɐ| e]}
+ @acase{@opwithout[e @|ɐ|]}
+
+ @intertext{@list[]
+
+ Finally, we define the row-polymorphic abstractions
+ @Λc[@${(@repeated{@ρc})} e] and @Λf[@${(@repeated{@ρf})} e] which bind row
+ type variables hiding constructors and fields respectively. The corresponding
+ instantiation operators are @atc[e @repeated{@ρc}] and @atf[e @repeated{@ρf}].
+
+ @list[]}
+
+ @acase{…}
+ @acase{@Λc[@${(@repeated{@ρc})} e]}@; new
+ @acase{@Λf[@${(@repeated{@ρf})} e]}@; new
+ @acase{@atc[e @repeated{@ρc}]}@; new
+ @acase{@atf[e @repeated{@ρf}]}@; new
+ ]
+
@;{
Note: In the @${@record[@repeated{@|ɐ|ᵢ = eᵢ}]} expression, which builds a
diff --git a/scribblings/adt-row-opsem.scrbl b/scribblings/adt-row-opsem.scrbl
@@ -35,7 +35,7 @@ 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) &= \#f & @text[" otherwise"] \\
}
}
@@ -76,7 +76,7 @@ indexed by a constructor label or a field label, like @${@ctor-pred[@κ]},
δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#t
@textif v = @record[@repeated{@|ɐ|ⱼ = vⱼ}] ∧ @repeatset{@|ɐ|ⱼ} = @repeatset{@|ɐ|ᵢ}
\\
- δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#f \text{ otherwise}
+ δ(@record-pred[@repeated{@|ɐ|ᵢ}], v) &= \#f @text[" otherwise"]
}
}
diff --git a/scribblings/adt-row-shorthands.scrbl b/scribblings/adt-row-shorthands.scrbl
@@ -0,0 +1,80 @@
+#lang scribble/manual
+
+@require["util.rkt"
+ "adt-utils.rkt"
+ (for-label (only-meta-in 0 typed/racket))]
+@(use-mathjax)
+
+@title[#:style (with-html5 manual-doc-style)
+ #: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:
+
+@$${(Λ (α) (λ ([x : α]) @ctor[κ x]))}
+
+The same applies to the predicate form of constructors:
+
+@$${(λ ([x : ⊤]) (@ctor-pred[κ] x))}
+
+The same applies to the accessor for a constructor's encapsulated value:
+
+@$${(Λ (α) (λ ([x : @ctor[κ α]]) (@ctor-val[κ] α))}
+
+As a convenience, we will write @ctor[κ], @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
+the following types:
+
+@$${
+ @$inferrule[
+ @${@textsc{T-Abs}}
+ @${Γ ⊢ @ctor[κ] : (∀ (α) (α → @ctor[κ α])) ; ϵ|⊥ ; ∅}
+ ]
+}
+
+@$${
+ @$inferrule[
+ @${…}
+ @${Γ ⊢ @ctor[κ] : (∀ (α) (α → @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:
+
+@$${(Λ (@repeated{αᵢ}) (λ (@repeated{[xᵢ : αᵢ]}) @record[@repeated{ɐᵢ = xᵢ}]))}
+
+The same applies to the predicate form of records:
+
+@;{
+ @$${
+ @aligned{
+ &(λ ([x : ⊤])\\
+ &\quad(Λ (@repeated{αᵢ})\\
+ &\qquad(λ (@repeated{[pᵢ : (⊤ \xrightarrow[∅]{αᵢ|\overline{αᵢ}} Boolean)]})\\
+ &\qquad\quad(@record-pred[@repeated{@|ɐ|ᵢ ? pᵢ}] x))}\\
+ }
+}
+
+@$${
+ @aligned{
+ &(λ ([x : ⊤])\\
+ &\quad(@record-pred[@repeated{@|ɐ|ᵢ}] x))}\\
+}
+
+The same applies to the accessor for a constructor's encapsulated value:
+
+@$${(Λ (α) (λ ([x : @ctor[κ α]]) (@ctor-val[κ] α))}
+
+@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.
+
diff --git a/scribblings/adt-row-trules.scrbl b/scribblings/adt-row-trules.scrbl
@@ -7,6 +7,7 @@
@(use-mathjax)
@title[#:style (with-html5 manual-doc-style)
+ #:tag "adt-row-trules"
#:version (version-text)]{Typing rules (with ρ)}
@todo{Should the filter be something else than @${ϵ|ϵ} or is the filter inferred
@@ -20,7 +21,7 @@
]
}
-@${\mathop{\textit{applyfilter}}} is defined
+@${\mathop{@textit{applyfilter}}} is defined
in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@htodo{their second (p. 75) definition of applyfilter does not clearly state
@@ -33,7 +34,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
φ_r
- = \mathop{\textit{applyfilter}}(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)}
+ = \mathop{@textit{applyfilter}}(@ctor[@κ ⊤]|\overline{@ctor[@κ ⊤]}, τ, o)}
@${Γ ⊢ (@ctor-pred[@κ] e) : Boolean ; φ_r ; ∅}
@${@textsc{T-Ctor-Pred}}
]
@@ -51,7 +52,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
∅ @& @otherwise
\end{array}\right. \\
φ_r
- = \mathop{\textit{applyfilter}}(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
+ = \mathop{@textit{applyfilter}}(\overline{\#f}_{@πctor-val}|\#f_{@πctor-val},
τ, o)}
@${Γ ⊢ (@ctor-val[@κ]\ e) : τ' ; φ_r ; o_r}
@${@textsc{T-Ctor-Val}}
@@ -70,7 +71,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
@$${
@$inferrule[
@${Γ ⊢ e : τ ; φ ; o \\
- φ_r = \mathop{\textit{applyfilter}}(@record[@repeated{@|ɐ|ᵢ : ⊤}]
+ φ_r = \mathop{@textit{applyfilter}}(@record[@repeated{@|ɐ|ᵢ : ⊤}]
|\overline{@record[@repeated{@|ɐ|ᵢ : ⊤}]}, τ, o)}
@${Γ ⊢ (@record-pred[@repeated{@|ɐ|ᵢ}] e) : Boolean ; φ_r ; ∅}
@${@textsc{T-Record-Pred}}
@@ -86,7 +87,7 @@ in@~cite[#:precision "p. 75" "tobin-hochstadt_typed_2010"].
∅ @& @otherwise
\end{array}\right. \\
φ_r
- = \mathop{\textit{applyfilter}}(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
+ = \mathop{@textit{applyfilter}}(\overline{\#f}_{@πɐ{@|ɐ|ⱼ}}|\#f_{@πɐ{@|ɐ|ⱼ}},
τ, o)}
@${Γ ⊢ e.@|ɐ|ⱼ : τ' ; φ_r ; o_r}
@${@textsc{T-Record-GetField}}
diff --git a/scribblings/adt-row-ty.scrbl b/scribblings/adt-row-ty.scrbl
@@ -9,7 +9,7 @@
#:version (version-text)]{Types (with ρ)}
@$${σ,τ ⩴ …
- @P @ctor[@κ τ] @; same
+ @|P| @ctor[@κ τ] @; same
@P @variant[@repeated{@ctor[@|κ|ᵢ τᵢ]} @ρc] @; new/changed
@P @record[@repeated{@|ɐ|ᵢ : τᵢ} @repeatset{-@|ɐ|ᵢ} @${@ρf - @repeatset{@|ɐ|ⱼ}}] @; changed
@P (∀_c (@repeated{@ρc}) τ) @; new
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -17,13 +17,15 @@
@(define-for-syntax (defop op)
(syntax-parser
[(_ :stringify ...)
- #`@${(@(add-between (list (string-append "\\textbf{" #,op "}")
+ #`@${(@(add-between (list @textbf{@#,op}
#,@(syntax->list #'(→str ...)))
"\\ "))}]))
@(define-syntax stringify
(syntax-parser
[(_ :stringify)
- #'→str]))
+ #'→str]
+ [(_ :stringify ...)
+ #'(add-between (list →str ...) "\\ ")]))
@(define-syntax ctor (defop "ctor"))
@(define κ @${κ})
@@ -38,17 +40,19 @@
@(define |P| @${\ |\ })
@(define ρc @${\rho_{c}})
@(define ρf @${\rho_{f}})
-@(define-syntax atc (defop "@${}_{\\textbf{c}}$"))
+@(define-syntax atc (defop "@${}_{\\textbf{c}}$"));; TODO text vs math!!!
@(define-syntax atf (defop "@${}_{\\textbf{f}}$"))
@(define-syntax Λc (defop "Λ${}_{\\textbf{c}}$"))
@(define-syntax Λf (defop "Λ${}_{\\textbf{f}}$"))
@(define-syntax-rule (ctor-pred c)
@${@(stringify c)\mathbf{?}})
-@(define-syntax-rule (record-pred f*)
- @${(\textbf{record?}\ @(stringify f*))})
+@(define-syntax-rule (record-pred . f*)
+ @${(@textbf{record?}\ @(stringify . f*))})
+@(define-syntax-rule (record-pred* . f*)
+ @${(@textbf{record$\mathbf{*}$?}\ @(stringify . f*))});; TODO text vs math!!!
@(define-syntax-rule (opwith rec a v)
- @list{@(stringify rec) \textbf{ with } @(stringify a) = @(stringify v)})
+ @list{@(stringify rec) @textbf[" with "] @(stringify a) = @(stringify v)})
@(define-syntax-rule (opwithout rec a)
- @list{@(stringify rec) \textbf{ without } @(stringify a)})
-@(define πctor-val @${\textbf{getval}})
+ @list{@(stringify rec) @textbf[" without "] @(stringify a)})
+@(define πctor-val @${@textbf{getval}})
@(define (πɐ . ɐ) @${\mathbf{@ɐ}})
\ No newline at end of file
diff --git a/scribblings/adt.scrbl b/scribblings/adt.scrbl
@@ -36,7 +36,7 @@ constants, i.e. they are written literally in the program source.
@;{
Primitive operations:
- @$${c ⩴ … @P \textit{ctor-val}}
+ @$${c ⩴ … @P @textit{ctor-val}}
}
We further define variants as a subset of the unions allowed by @|typedracket|
@@ -57,59 +57,6 @@ values of two function types present in the same union).
\end{gathered}
}
-Notes: the polymorphic builder function for the @κ constructor which
-intuitively corresponds to @ctor[κ] can be written as the η-expansion of the
-@ctor[κ e] operator:
-
-@$${(Λ (α) (λ ([x : α]) @ctor[κ x]))}
-
-The same applies to the predicate form of constructors:
-
-@$${(λ ([x : ⊤]) (@ctor-pred[κ] x))}
-
-The same applies to the accessor for a constructor's encapsulated value:
-
-@$${(Λ (α) (λ ([x : @ctor[κ α]]) (@ctor-val[κ] α))}
-
-@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.
-
-
-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:
-
-@$${(Λ (@repeated{αᵢ}) (λ (@repeated{[xᵢ : αᵢ]}) @record[@repeated{ɐᵢ = xᵢ}]))}
-
-The same applies to the predicate form of records:
-
-@;{
- @$${
- @aligned{
- &(λ ([x : ⊤])\\
- &\quad(Λ (@repeated{αᵢ})\\
- &\qquad(λ (@repeated{[pᵢ : (⊤ \xrightarrow[∅]{αᵢ|\overline{αᵢ}} Boolean)]})\\
- &\qquad\quad(@record-pred[@repeated{@|ɐ|ᵢ ? pᵢ}] x))}\\
- }
-}
-
-@$${
- @aligned{
- &(λ ([x : ⊤])\\
- &\quad(@record-pred[@repeated{@|ɐ|ᵢ}] x))}\\
-}
-
-The same applies to the accessor for a constructor's encapsulated value:
-
-@$${(Λ (α) (λ ([x : @ctor[κ α]]) (@ctor-val[κ] α))}
-
-@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.
-
@asection{
@atitle{With row polymorphism}
@include-asection["adt-row-e.scrbl"]
@@ -120,4 +67,5 @@ shorthand for the above lambda functions.
@include-asection["adt-row-pe.scrbl"]
@include-asection["adt-row-trules.scrbl"]
@include-asection["adt-row-opsem.scrbl"]
-}
-\ No newline at end of file
+ @include-asection["adt-row-shorthands.scrbl"]
+}
diff --git a/scribblings/phc-thesis.scrbl b/scribblings/phc-thesis.scrbl
@@ -64,7 +64,6 @@
(add1 a)))
1))
-@;{
@aappendix{
@include-asection[(lib "phc-graph/scribblings/phc-graph-implementation.scrbl")]
@include-asection[(lib "phc-adt/scribblings/phc-adt-implementation.scrbl")]
@@ -73,7 +72,6 @@
@include-asection[
(lib "type-expander/scribblings/type-expander-implementation.scrbl")]
}
-}
@;{
Notes concerning tikz → SVG conversion:
@@ -119,4 +117,4 @@
We might want to create a special scribble command to typeset "normal" text
(rendered using scribble's HTML font), and another to typeset math (possibly
with MathJax).
-}
-\ No newline at end of file
+}
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -14,8 +14,9 @@
(rename-out [note* note])
define-footnote ;; TODO: does not use the (superscript …)
(all-from-out "abbreviations.rkt")
- (except-out (all-from-out scribble-math) $ $$)
- (rename-out [$* $] [$$* $$])
+ (all-from-out scribble-math)
+ $
+ $$
version-text
aappendix
tex-header
@@ -36,11 +37,18 @@
aligned
acase
cases
+ intertext
+ cases*
frac
where
textif
otherwise
- quad)
+ quad
+ mathtext
+ textbf
+ textit
+ textrm
+ text)
(require racket/stxparam
racket/splicing
@@ -53,13 +61,13 @@
scribble-enhanced/math
scribble/latex-properties
scribble/decode
- scribble-math
+ (except-in scribble-math $ $$)
phc-toolkit/untyped/meta-struct
"abbreviations.rkt"
+ "util0.rkt"
(for-syntax syntax/parse)
scribble/html-properties
- scribble/latex-properties
- scribble-math)
+ scribble/latex-properties)
(use-mathjax)
@@ -458,48 +466,24 @@ EOTEX
(define lastname list)
-;; Math stuff
-(define (clean-$ e)
- (cond [(pair? e) (cons (clean-$ (car e)) (clean-$ (cdr e)))]
- [(traverse-element? e)
- (traverse-element (λ (a b)
- (clean-$ ((traverse-element-traverse e) a b))))]
- [(match e
- [(element (style (or "math" "texMathInline" "texMathDisplay")
- _)
- content)
- #t]
- [_ #f])
- (clean-$ (element-content e))]
- [(element? e)
- (element (element-style e)
- (clean-$ (element-content e)))]
- [else e]))
-
-(define ($* . elts)
- (apply $ (clean-$ elts)))
-
-(define ($$* . elts)
- (apply $$ (clean-$ elts)))
-
-(define tr<: ($* "\\mathrel{<:_\\mathit{tr}}"))
-(define tr≤: ($* "\\mathrel{≤:_\\mathit{tr}}"))
-(define $ooo ($* "\\textit{ooo}"))
+(define tr<: ($ "\\mathrel{<:_\\mathit{tr}}"))
+(define tr≤: ($ "\\mathrel{≤:_\\mathit{tr}}"))
+(define $ooo ($ (mathtext "\\textit{ooo}")))
(define ($inferrule from* to* [label '()])
(elem #:style
(style #f (list (tex-addition
(string->bytes/utf-8
"\\usepackage{mathpartir}"))))
- ($* (cond-element [html "\\frac{\\begin{gathered}"]
- [else "\\inferrule{"])
- from*
- (cond-element [html "\\end{gathered}}{\\begin{gathered}"]
- [else "}{"])
- to*
- (cond-element [html "\\end{gathered}}"]
- [else "}"])
- label)))
+ ($ (cond-element [html "\\frac{\\begin{gathered}"]
+ [else "\\inferrule{"])
+ from*
+ (cond-element [html "\\end{gathered}}{\\begin{gathered}"]
+ [else "}{"])
+ to*
+ (cond-element [html "\\end{gathered}}"]
+ [else "}"])
+ label)))
(define htmldiff-css-experiment #<<EOCSS
.version:after {
@@ -532,19 +516,19 @@ EOCSS
)
(define (textsc str)
- ($* (cond-element
- [html (list "{\\rm "
- (for/list ([c (in-string str)])
- (cond
- [(char=? c #\-)
- "\\text{-}"]
- [(char-upper-case? c)
- (string c)]
- [else (list "{\\small "
- (string (char-upcase c))
- "}")]))
- "}")]
- [else (list "\\text{\\textsc{" str "}}")])))
+ ($ (cond-element
+ [html (list "{\\rm "
+ (for/list ([c (in-string str)])
+ (cond
+ [(char=? c #\-)
+ (mathtext "\\text{-}")]
+ [(char-upper-case? c)
+ (string c)]
+ [else (list "{\\small "
+ (string (char-upcase c))
+ "}")]))
+ "}")]
+ [else (list (mathtext "\\text{\\textsc{" str "}}"))])))
(define (aligned #:valign [valign 'mid] . lines)
(define valign-letter (case valign [(top) "t"] [(mid) "m"] [(bot) "b"]))
@@ -558,21 +542,75 @@ EOCSS
(define acase list)
(define cases
(λ (#:first-sep [first-sep "\\vphantom{x}\\mathbin{:=}\\vphantom{x}"]
- #:then-sep [then-sep "|\\;\\ "] term
+ #:then-sep [then-sep "|\\;\\ "]
+ term
. the-cases)
- (list
- term
- (aligned #:valign 'top @; cl
- @(for/list ([c (in-list the-cases)]
- [i (in-naturals)])
- (list (if (= i 0) first-sep then-sep)
- " & "
- c
- (if (= i (sub1 (length the-cases))) "" "\\\\\n")))
- ))))
+ ($$ (list
+ term
+ (aligned #:valign 'top @; cl
+ @(for/list ([c (in-list the-cases)]
+ [i (in-naturals)])
+ (list (if (= i 0) first-sep then-sep)
+ " & "
+ c
+ (if (= i (sub1 (length the-cases))) "" "\\\\\n")))
+ )))))
+(require (for-syntax racket/base
+ racket/contract/base
+ syntax/parse
+ syntax/parse/experimental/template))
+(define (intertext . l) (list (mathtext "\\text{" l "}")))
+(define-syntax cases*
+ (syntax-parser
+ #:literals (acase intertext)
+ [(_ term
+ {~optional {~seq #:first-sep first-sep}}
+ {~optional {~seq #:then-sep then-sep}}
+ {~optional (intertext . intertext₀)}
+ (~seq {~and acaseᵢ₀ [acase . _]}
+ {~and acaseᵢⱼ [acase . _]} ...
+ [intertext . intertextᵢ])
+ ...
+ {~and acaseₙ₀ [acase . _]}
+ {~and acaseₙⱼ [acase . _]} ...)
+ #:with (tmpᵢ ...) (generate-temporaries #'((acaseᵢⱼ ...) ...))
+ (quasitemplate
+ (#,(if ((or/c 'expression list?) (syntax-local-context)) #'list #'begin)
+ (define (vcenter lst)
+ @cond-element[[html (list "\\vcenter{" lst "}")]
+ [else (list "\\begin{array}{l}" lst "\\end{array}")]])
+ (define phantom
+ @$${\hphantom{@vcenter{@(list (?@ acaseᵢ₀ "\\\\"
+ (?@ acaseᵢⱼ "\\\\") ...)
+ ...
+ (?? (?@ acaseₙ₀
+ (?@ acaseₙⱼ "\\\\") ...)))}}})
+ (define tmpᵢ @cases[term
+ (?? (?@ #:first-sep first-sep))
+ (?? (?@ #:then-sep then-sep))
+ (list "\\rlap{" acaseᵢ₀ "}" phantom)
+ acaseᵢⱼ
+ ...])
+ ...
+ (?? (define tmpₙ @cases[term
+ (?? (?@ #:first-sep first-sep))
+ (?? (?@ #:then-sep then-sep))
+ (list "\\rlap{" acaseₙ₀ "}" phantom)
+ acaseₙⱼ
+ ...]))
+ (?? (?@ . intertext₀))
+ (?@ tmpᵢ . intertextᵢ)
+ ...
+ tmpₙ
+ ))]))
+
(define (frac x . y)
@list{\frac{@x}{@y}})
-(define where @${\text{ where }})
-(define textif @${\text{ if }})
-(define otherwise @${\text{ otherwise }})
-(define quad @${\quad})
+(define where (mathtext @${\text{ where }}))
+(define textif (mathtext @${\text{ if }}))
+(define otherwise (mathtext @${\text{ otherwise }}))
+(define quad (mathtext @${\quad}))
+(define (textbf . l) (mathtext "\\textbf{" l "}"))
+(define (textit . l) (mathtext "\\textit{" l "}"))
+(define (textrm . l) (mathtext "\\textrm{" l "}"))
+(define (text . l) (mathtext "\\text{" l "}"))
+\ No newline at end of file
diff --git a/scribblings/util0.rkt b/scribblings/util0.rkt
@@ -0,0 +1,61 @@
+#lang racket
+
+(require scribble/manual
+ scribble/core
+ scribble/latex-properties
+ scribble-math
+ scribble-math/katex-convert-unicode)
+
+(provide mathtext
+ clean-$
+ (rename-out [$* $]
+ [$$* $$]))
+
+(define (mathtext . l)
+ ;; TODO: (clean-$ l), but wrap converted stuff with $…$
+ (apply elem #:style (style "mathText"
+ (list (tex-addition #"\\def\\mathText#1{#1}")
+ 'exact-chars))
+ l))
+
+;; Math stuff
+(define (clean-$ e)
+ (cond [(pair? e) (cons (clean-$ (car e)) (clean-$ (cdr e)))]
+ [(traverse-element? e)
+ (traverse-element (λ (a b)
+ (clean-$ ((traverse-element-traverse e) a b))))]
+ [(match e
+ [(element (style (or "math" "texMathInline" "texMathDisplay")
+ _)
+ content)
+ #t]
+ [_ #f])
+ ;; No need to go down recursively, as the contents should already have
+ ;; been cleaned when the e was created. Plus we risk re-escaping
+ ;; things within \text{…}.
+ #;(clean-$ (element-content e))
+ (element-content e)]
+ [(match e
+ [(element (style "mathText" _)
+ content)
+ #t]
+ [_ #f])
+ ;; No need to go down recursively, as the contents should already have
+ ;; been cleaned when the e was created. Plus we risk re-escaping
+ ;; things within \text{…}.
+ ;; TODO: when a "math" "texMathInline" "texMathDisplay" is encountered
+ ;; within a "mathText", we should wrap it with $…$.
+ (element-content e)]
+ [(element? e)
+ (element (element-style e)
+ (clean-$ (element-content e)))]
+ [(string? e)
+ ;; TODO: do this only when compiling to HTML.
+ (katex-convert-unicode e)]
+ [else e]))
+
+(define ($* . elts)
+ (apply $ (clean-$ elts)))
+
+(define ($$* . elts)
+ (apply $$ (clean-$ elts)))
