commit 481e4f8fd00149714d462142086f463a45f25a43
parent 1e745d6159e6965975cb86713ac387720a30d3ce
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Wed, 16 Aug 2017 17:00:38 +0200
Description for the terms of the ctor + variant + records + row extension
Diffstat:
9 files changed, 83 insertions(+), 66 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/Ectx.rkt b/from-dissertation-tobin-hochstadt/Ectx.rkt
@@ -12,5 +12,5 @@
@acase{@ifop[E e e]@tag*{conditional}}
@acase{@eq?op[E e]@tag*{symbol equality}}
@acase{@eq?op[v E]}
- @acase{@mapop[E e]}
+ @acase{@mapop[E e]@tag*{map function over list}}
@acase{@mapop[v E]}]
\ No newline at end of file
diff --git a/scribblings/adt-Ectx.scrbl b/scribblings/adt-Ectx.scrbl
@@ -11,15 +11,15 @@
@$${
@cases["E" #:first-sep "⩴"
@acase{…}
- @acase{@ctor[@κ E]}
- @acase{(@ctor-pred[@κ] E)}
- @acase{(@ctor-val[@κ] E)}
+ @acase{@ctor[@κ 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ₖ}]}
- @acase{(@record-pred[@repeated{@|ɐ|ᵢ}] E)}
- @acase{E.@|ɐ|}
- @acase{@opwith[E @|ɐ| e]}
+ @repeated{@|ɐ|ₖ = eₖ}]@tag*{record instance}}
+ @acase{(@record-pred[@repeated{@|ɐ|ᵢ}] E)@tag*{record predicate}}
+ @acase{E.@|ɐ|@tag*{record field access}}
+ @acase{@opwith[E @|ɐ| e]@tag*{record update (new/change)}}
@acase{@opwith[v @|ɐ| E]}
- @acase{@opwithout[E @|ɐ|]}]
+ @acase{@opwithout[E @|ɐ|]@tag*{record update (remove)}}]
}
diff --git a/scribblings/adt-row-Ectx.scrbl b/scribblings/adt-row-Ectx.scrbl
@@ -11,16 +11,16 @@
@$${
@cases["E" #:first-sep "⩴"
@acase{…}
- @acase{@ctor[@κ E]}
- @acase{(@ctor-pred[@κ]\ E)}
- @acase{(@ctor-val[@κ]\ E)}
+ @acase{@ctor[@κ 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ₖ}]}
- @acase{(@record-pred[@repeatset{@|ɐ|ᵢ}]\ E)}
- @acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ E)}
- @acase{E.@|ɐ|}
- @acase{@opwith[E @|ɐ| 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}}
+ @acase{E.@|ɐ|@tag*{record field access}}
+ @acase{@opwith[E @|ɐ| e]@tag*{record update (new/change)}}
@acase{@opwith[v @|ɐ| E]}
- @acase{@opwithout[E @|ɐ|]}]
+ @acase{@opwithout[E @|ɐ|]@tag*{record update (remove)}}]
}
diff --git a/scribblings/adt-row-e.scrbl b/scribblings/adt-row-e.scrbl
@@ -44,8 +44,8 @@ the value stored in an instance of a constructor.
@acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ e)
@tag*{row-record predicate}}@;added
@acase{e.@|ɐ|@tag*{record field access}}
- @acase{@opwith[e @|ɐ| e]@tag*{record update (new/changed field)}}
- @acase{@opwithout[e @|ɐ|]@tag*{record update (removed field)}}
+ @acase{@opwith[e @|ɐ| e]@tag*{record update (new/change field)}}
+ @acase{@opwithout[e @|ɐ|]@tag*{record update (remove field)}}
@interpar{
Finally, we define the row-polymorphic abstractions
@Λce[(@repeated{@ρc}) e] and @Λfe[(@repeated{@ρf}) e] which bind row
diff --git a/scribblings/adt-row-pe.scrbl b/scribblings/adt-row-pe.scrbl
@@ -10,7 +10,10 @@
@todo{Does this need any change when adding row typing?}
-@$${pe ⩴ … @P @πctor-val @P @|ɐ|}
+@cases[@pe #:first-sep "⩴"
+ @acase{…}
+ @acase{@πctor-val @tag*{value of the constructor}}
+ @acase{@|ɐ| @tag*{field value}}]
We extend the metafunctions for paths given
in@~cite[#:precision "pp. 65 and 75" "tobin-hochstadt_typed_2010"]. The @${
@@ -24,14 +27,11 @@ a conditional.
@todo{How should I note cleanly these removals / replacements which refer to
an @|ɐ| and its τ or @${v} inside the set of @${@|ɐ|ᵢ}?}
-@$${
- @aligned{
- @update(@record[@repeated{@|ɐ|ᵢ : τᵢ}ⁿ], υ_{π∷@|ɐ|ⱼ})
- &= @record[@${@repeated{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}}
+@aligned{
+ @update(@record[@repeated{@|ɐ|ᵢ : τᵢ}ⁿ], υ_{π∷@|ɐ|ⱼ})
+ &= @record[@${@repeated{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}}
@${@|ɐ|ⱼ : @${@update(τⱼ, υ_π)}}]
- \\
- &\quad @where @|ɐ|ⱼ : τⱼ ∈ @repeatset{@|ɐ|ᵢ : τᵢ}\\
- @update(@ctor[@κ τ], υ_{π∷@πctor-val})
- &= @ctor[@κ @${@update(τ, υ_π)}]
- }
-}
-\ No newline at end of file
+ \\
+ &\quad @where @|ɐ|ⱼ : τⱼ ∈ @repeatset{@|ɐ|ᵢ : τᵢ}\\
+ @update(@ctor[@κ τ], υ_{π∷@πctor-val})
+ &= @ctor[@κ @${@update(τ, υ_π)}]}
+\ No newline at end of file
diff --git a/scribblings/adt-row-tausigma.scrbl b/scribblings/adt-row-tausigma.scrbl
@@ -10,10 +10,10 @@
@cases["σ,τ" #:first-sep "⩴"
@acase{…}
- @acase{@ctor[@κof[τ]]} @; same
- @acase{@record[@ςf]} @; changed
- @acase{@∀c[(@repeated{@ρc}) τ]} @; new
- @acase{@∀f[(@repeated{@ρf}) τ]}] @; new
+ @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}) τ]@tag*{row-polymorphic abstraction (fields)}}] @; new
@; new↓
@@ -28,14 +28,12 @@ constructors in the row type can be specified on variants.
@cases["σ,τ" #:first-sep "⩴"
@acase{…}
- @acase{@variant[@ςf]}] @; new/changed
+ @acase{@variant[@ςf]@tag*{possibly row-polymorphic variant}}] @; new/changed
-@; TODO: what about adding some fields to the ρ used to instantiate another function?
-@; new
@cases[@ςc #:first-sep "⩴"
- @acase{@repeatset{@κof[τ]}}
- @acase{@|ρc|\ @repeatset{-@|κ|ᵢ}\ @repeatset{+@κof[ⱼ τⱼ]}}]
+ @acase{@repeatset{@κof[τ]}@tag*{fixed constructors}}
+ @acase{@|ρc|\ @repeatset{-@|κ|ᵢ}\ @repeatset{+@κof[ⱼ τⱼ]} @tag*{row without some ctors, with extra ctors}}]
@cases[@ςf #:first-sep "⩴"
- @acase{@repeatset{@|ɐ|:τ}}
- @acase{@|ρf|\ @repeatset{-@|ɐ|ᵢ}\ @repeatset{+@|ɐ|ⱼ:τⱼ}}]
+ @acase{@repeatset{@|ɐ|:τ}@tag*{fixed fields}}
+ @acase{@|ρf|\ @repeatset{-@|ɐ|ᵢ}\ @repeatset{+@|ɐ|ⱼ:τⱼ}@tag*{row without some fields, with extra fields}}]
diff --git a/scribblings/adt-row-v.scrbl b/scribblings/adt-row-v.scrbl
@@ -8,6 +8,7 @@
@title[#:style (with-html5 manual-doc-style)
#:version (version-text)]{Values (with ρ)}
-@$${v ⩴ …
- @P @ctor[@κ v]
- @P @record[@repeated{@|ɐ|ᵢ = vᵢ}]}
+@cases["v" #:first-sep "⩴"
+ @acase{…}
+ @acase{@ctor[@κ v]@tag*{constructor instance}}
+ @acase{@record[@repeated{@|ɐ|ᵢ = vᵢ}]@tag*{record instance}}]
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -138,6 +138,7 @@
@list{@(stringify rec) @textbf[" with "] @(stringify a) = @(stringify v)})
(define-syntax-rule (opwithout rec a)
@list{@(stringify rec) @textbf[" without "] @(stringify a)})
+(define pe @${\mathit{pe}})
(define πctor-val @${@textbf{getval}})
(define (πɐ . ɐ) @${\mathbf{@ɐ}})
;; Associates a variable name or record field name with a value, type or
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -627,26 +627,37 @@ EOCSS
(define (minwidth phantoms realcontent)
(list "\\rlap{" realcontent "}"
@$${\hphantom{@array<l>-no-extra-h-space[phantoms]}}))
+(begin-for-syntax
+ (define-syntax-class acase-cls
+ (pattern ({~and self {~literal acase}}
+ {~and arg {~not ({~or {~literal tag} {~literal tag*}} . _)}} ...
+ {~optional ({~and tag-id {~or {~literal tag} {~literal tag*}}}
+ . tag-args)})
+ #:with phantom-tag
+ #`(self arg ...
+ . #,(if (attribute tag-id)
+ #'{(tag-id #:phantom? #t . tag-args)}
+ #'())))))
(define-syntax cases*
(syntax-parser
- #:literals (acase intertext interpar)
+ #:literals (intertext interpar)
[(_ term
{~optional {~seq #:first-sep first-sep}}
{~optional {~seq #:then-sep then-sep}}
{~optional {~and inter₀ ({~or intertext interpar} . _)}}
- (~seq {~and acaseᵢ₀ [acase . _]}
- {~and acaseᵢⱼ [acase . _]} ...
+ (~seq acaseᵢ₀:acase-cls
+ acaseᵢⱼ:acase-cls ...
{~and interᵢ [{~or intertext interpar} . _]})
...
- {~and acaseₙ₀ [acase . _]}
- {~and acaseₙⱼ [acase . _]} ...)
+ acaseₙ₀:acase-cls
+ acaseₙⱼ:acase-cls ...)
#:with (tmpᵢ ...) (generate-temporaries #'((acaseᵢⱼ ...) ...))
(quasitemplate
(#,(if ((or/c 'expression list?) (syntax-local-context)) #'list #'begin)
(define phantoms
- (list (?@ acaseᵢ₀ acaseᵢⱼ ...)
+ (list (?@ acaseᵢ₀.phantom-tag acaseᵢⱼ.phantom-tag ...)
...
- (?? (?@ acaseₙ₀ acaseₙⱼ ...))))
+ (?? (?@ acaseₙ₀.phantom-tag acaseₙⱼ.phantom-tag ...))))
(define tmpᵢ @cases[term
(?? (?@ #:first-sep first-sep))
(?? (?@ #:then-sep then-sep))
@@ -696,21 +707,23 @@ EOCSS
(define nl @cond-element[[latex "\\csname @arraycr\\endcsname"] [else "\\\\"]])
(define-runtime-path tikztag.sty "../tikztag.sty")
-(define ((tag** starred?) . txt)
+(define ((tag** starred?) #:phantom? [phantom? #f] . txt)
(cond-element
- [html (list "\\hphantom{"
+ [html (list* "\\hphantom{"
(text (if starred? "" "(")
txt
(if starred? "" ")"))
"}"
- "\\tag*{"
- (mathtext
- ($ "\\llap{"
- (text (if starred? "" "(")
- txt
- (if starred? "" ")"))
- "}"))
- "}")]
+ (if phantom?
+ '()
+ (list "\\tag*{"
+ (mathtext
+ ($ "\\llap{"
+ (text (if starred? "" "(")
+ txt
+ (if starred? "" ")"))
+ "}"))
+ "}")))]
[latex (elem #:style (style #f (list (tex-addition
;; The \n are important in case the
;; file does not end with a newline
@@ -720,9 +733,13 @@ EOCSS
(bytes-append #"\n\\makeatletter\n"
(file->bytes tikztag.sty)
#"\n\\makeatother\n"))))
- (list "\\hphantom{\\text{" @mathtext[txt] "}}"
- "\\tikztag" (if starred? "*" "") "{" @mathtext[txt] "}"))]
- [else (list " (" txt ")")]))
+ (list* "\\hphantom{\\text{" @mathtext[txt] "}}"
+ (if phantom?
+ '()
+ (list "\\tikztag" (if starred? "*" "") "{"
+ @mathtext[txt]
+ "}"))))]
+ [else (if phantom? '() (list " (" txt ")"))]))
(define tag (tag** #f))
(define tag* (tag** #t))
