commit f53fd5200d25e3b50b8eb3a5b2fe24f0045909bb
parent d00836f0b1fcb98003c0e473ef5e06487f87c419
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Sun, 13 Aug 2017 12:05:34 +0200
Small tweaks.
Diffstat:
7 files changed, 56 insertions(+), 49 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/operational-semantics.rkt b/from-dissertation-tobin-hochstadt/operational-semantics.rkt
@@ -49,7 +49,7 @@
@δe(@λe[(@repeated{x:τ} @${\ .\ } @${x_r:@polydot[σ α]}) e])
= @λv[(@repeated{x:τ} @${\ .\ } @${x_r:@polydot[σ α]}) e] \\
@δe(@Λe[(@repeated{α}) e]) = @Λv[(@repeated{α}) e] \\
- @δe(@Λe[(@repeated{α} @polydotα[β]) e]) = @Λe[(@repeated{α} @polydotα[β]) e] \\
+ @δe(@Λe[(@repeated{α} @polydotα[β]) e]) = @Λv[(@repeated{α} @polydotα[β]) e] \\
@δe(@promisee[e]) = @promisev[e] \\
@δe(@syme[s]) = @symv[s]
\end{aligned}
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -61,15 +61,15 @@ their inclusion in the following semantics would needlessly complicate things.
We note a sequence of elements with @repeated{y}. When there is more than one
sequence involved in a rule or equation, we may use the notation
@repeated[#:n "n"]{y} to indicate that there are @${n} elements in the
-sequence. Two sequences can that way be forced to have the same number of
-elements. We represent a set of elements (an “unordered” sequence) with the
-notation @repeatset{y}. The use of ellipses in @polydotα{α} does not indicate
-the repetition of @${α}. Instead, it indicates that @${α} is a @emph{variadic}
-polymorphic type variable: a placeholder for zero or more types which will be
-substituted for occurrences of @${α} when the polymorphic type is
-instantiated. These ellipses appear as such in the @typedracket source code,
-and are the reason we use the notation @repeated{y} to indicate repetition,
-instead of the ellipses commonly used for that purpose.
+sequence. Two sequences can be forced to have the same number of elements in
+that way. We represent a set of elements (an “unordered” sequence) with the
+notation @repeatset{y}. The use of ellipses in @polydotα{α} does not
+indicate the repetition of @${α}. Instead, it indicates that @${α} is a @emph{
+ variadic} polymorphic type variable: a placeholder for zero or more types
+which will be substituted for occurrences of @${α} when the polymorphic type
+is instantiated. These ellipses appear as such in the @typedracket source
+code, and are the reason we use the notation @repeated{y} to indicate
+repetition, instead of the ellipses commonly used for that purpose.
We indicate the syntactical substitution of @${y} with @${z} in @${w} using
the notation @${w@subst[y ↦ z]}. When given several elements to replace, the
diff --git a/scribblings/adt-row-e.scrbl b/scribblings/adt-row-e.scrbl
@@ -22,8 +22,7 @@ the value stored in an instance of a constructor.
@acase{@ctor[@κ e]}
@acase{(@ctor-pred[@κ]\ e)}
@acase{(@ctor-val[@κ]\ e)}
- @intertext{@list[]
-
+ @interpar{
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.
@@ -35,32 +34,25 @@ the value stored in an instance of a constructor.
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[@${@|ɐ|ᵢ} eᵢ]}]}
- @acase{(@record-pred[@repeated{@|ɐ|ᵢ}]\ e)}
- @acase{(@record-pred*[@repeated{@|ɐ|ᵢ} @repeated{-@|ɐ|ⱼ}]\ e)}@;added
+ @acase{(@record-pred[@repeatset{@|ɐ|ᵢ}]\ e)}
+ @acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ e)}@;added
@acase{e.@|ɐ|}
@acase{@opwith[e @|ɐ| e]}
@acase{@opwithout[e @|ɐ|]}
-
- @intertext{@list[]
-
+ @interpar{
Finally, we define the row-polymorphic abstractions
- @Λc[@${(@repeated{@ρc})} e] and @Λf[@${(@repeated{@ρf})} e] which bind row
+ @Λce[(@repeated{@ρc}) e] and @Λfe[(@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{@Λce[(@repeated{@ρc}) e]}@; new
+ @acase{@Λfe[(@repeated{@ρf}) e]}@; new
@acase{@atc[e @repeated{@ρc}]}@; new
- @acase{@atf[e @repeated{@ρf}]}@; new
- ]
+ @acase{@atf[e @repeated{@ρf}]}]@; new
@;{
diff --git a/scribblings/adt-row-ectx.scrbl b/scribblings/adt-row-ectx.scrbl
@@ -8,8 +8,6 @@
@title[#:style (with-html5 manual-doc-style)
#:version (version-text)]{Evaluation contexts (with ρ)}
-@todo{Does this need any change when adding row typing?}
-
@$${
@cases["E" #:first-sep "⩴"
@acase{…}
@@ -19,8 +17,8 @@
@acase{@record[@repeated{@|ɐ|ᵢ = vᵢ}
@${@|ɐ|ⱼ = E}
@repeated{@|ɐ|ₖ = eₖ}]}
- @acase{(@record-pred[@repeated{@|ɐ|ᵢ}]\ E)}
- @acase{(@record-pred*[@repeated{@|ɐ|ᵢ} @repeated{-@|ɐ|ⱼ}]\ E)}
+ @acase{(@record-pred[@repeatset{@|ɐ|ᵢ}]\ E)}
+ @acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ E)}
@acase{E.@|ɐ|}
@acase{@opwith[E @|ɐ| e]}
@acase{@opwith[v @|ɐ| E]}
diff --git a/scribblings/adt-row-opsem.scrbl b/scribblings/adt-row-opsem.scrbl
@@ -15,11 +15,11 @@
@;; New:
@$p[@$inferrule[-
- @${@atc[e @repeated{@ρc}] ↪ e}
+ @${@atc[@Λcv[(@repeated{@ρc}) e] @repeated{@ρc}] ↪ e}
@${@textsc{E-Inst-C}}]
@$inferrule[-
- @${@atf[e @repeated{@ρf}] ↪ e}
+ @${@atf[@Λfv[(@repeated{@ρc}) e] @repeated{@ρf}] ↪ e}
@${@textsc{E-Inst-F}}]]
}
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -2,7 +2,9 @@
@(provide (except-out (all-defined-out)
num-e*
num-τ*
- List…τ*))
+ List…τ*
+ Λc*
+ Λf*))
@require["util.rkt"
(only-in scribble/base emph)
scriblib/render-cond
@@ -71,12 +73,12 @@
@${\overrightarrow{@l}}))
(define (repeatset #:w [wide? #f] . l)
(define w (if wide? "\\!" ""))
- (cond-element
- [html
- @${\def\overrightbracedarrow#1{\overset{\scriptscriptstyle{\raise1mu{\{}}}{\vphantom{#1}}\overrightarrow{@|w|#1@|w|}\overset{\scriptscriptstyle{\raise1mu{\}}}}{\vphantom{#1}}}\overrightbracedarrow{@l}}]
- [else
- ;; Defined in util.rkt
- @${\overrightbracedarrow{@|w|@|l|@|w|}}]))
+ ($ (cond-element
+ [html
+ @${\def\overrightbracedarrow#1{\overset{\scriptscriptstyle{\raise1mu{\{}}}{\vphantom{#1}}\overrightarrow{@|w|#1@|w|}\overset{\scriptscriptstyle{\raise1mu{\}}}}{\vphantom{#1}}}\overrightbracedarrow{@l}}]
+ [else
+ ;; Defined in util.rkt
+ @${\overrightbracedarrow{@|w|@|l|@|w|}}])))
(define (repeatSet . l)
@${\{@(apply repeatset l)\}})
(define |P| @${\ |\ })
@@ -85,8 +87,16 @@
(define-syntax at (defop "@"))
(define-syntax atc (defop (list "@" @${{}_{@textbf{c}}})))
(define-syntax atf (defop (list "@" @${{}_{@textbf{f}}})))
-(define-syntax Λc (defop (list "Λ" @${{}_{@textbf{c}}})))
-(define-syntax Λf (defop (list "Λ" @${{}_{@textbf{f}}})))
+(define-syntax Λc* (defop (list "Λ" @${{}_{@textbf{c}}})))
+(define-syntax Λf* (defop (list "Λ" @${{}_{@textbf{f}}})))
+(define-syntax-rule (Λce (ρ ...) e)
+ (Λc* @${(@(add-between (list ρ ...) "\\ "))} e))
+(define-syntax-rule (Λcv (ρ ...) e)
+ (Λc* @${(@(add-between (list ρ ...) "\\ "))} e))
+(define-syntax-rule (Λfe (ρ ...) e)
+ (Λf* @${(@(add-between (list ρ ...) "\\ "))} e))
+(define-syntax-rule (Λfv (ρ ...) e)
+ (Λf* @${(@(add-between (list ρ ...) "\\ "))} e))
(define-syntax ∀r* (defop @${\mathbf{∀}}))
(define-syntax-rule (∀r (α ...) τ)
(∀r* @${(@(add-between (list (stringify α) ...) "\\ "))} τ))
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -39,6 +39,7 @@
acase
cases
intertext
+ interpar
cases*
frac
where
@@ -600,7 +601,13 @@ EOCSS
racket/contract/base
syntax/parse
syntax/parse/experimental/template))
-(define (intertext . l) (list (mathtext "\\text{" l "}")))
+(define-syntax (intertext stx)
+ (syntax-case stx ()
+ [(_ . l) (eq? (syntax-local-context) 'module)
+ #'(begin . l)]
+ [(_ . l)
+ #'(list (mathtext "\\text{" l "}"))]))
+(define-syntax-rule (interpar l ...) (intertext "\n" "\n" l ... "\n" "\n"))
(define (array<l>-no-extra-h-space lst)
(list "\\!\\begin{array}{l}"
(add-between lst "\\\\")
@@ -610,14 +617,14 @@ EOCSS
@$${\hphantom{@array<l>-no-extra-h-space[phantoms]}}))
(define-syntax cases*
(syntax-parser
- #:literals (acase intertext)
+ #:literals (acase intertext interpar)
[(_ term
{~optional {~seq #:first-sep first-sep}}
{~optional {~seq #:then-sep then-sep}}
- {~optional (intertext . intertext₀)}
+ {~optional {~and inter₀ ({~or intertext interpar} . _)}}
(~seq {~and acaseᵢ₀ [acase . _]}
{~and acaseᵢⱼ [acase . _]} ...
- [intertext . intertextᵢ])
+ {~and interᵢ [{~or intertext interpar} . _]})
...
{~and acaseₙ₀ [acase . _]}
{~and acaseₙⱼ [acase . _]} ...)
@@ -641,8 +648,8 @@ EOCSS
(minwidth phantoms acaseₙ₀)
acaseₙⱼ
...]))
- (?? (?@ . intertext₀))
- (?@ tmpᵢ . intertextᵢ)
+ (?? inter₀)
+ (?@ tmpᵢ interᵢ)
...
tmpₙ
))]))
