commit e1986a96cb88d308de443c04c0188feff225b032
parent a93aadcedefe60619877f961a9ca9555f54604d6
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Fri, 21 Jul 2017 19:02:18 +0200
Description for the grammar.
Diffstat:
5 files changed, 81 insertions(+), 70 deletions(-)
diff --git a/from-dissertation-tobin-hochstadt/rules.scrbl b/from-dissertation-tobin-hochstadt/rules.scrbl
@@ -59,7 +59,7 @@ Expressions:
@acase{@true-e @tag*{booleans}}
@acase{@false-e}
@acase{@null-e @tag*{null constant}}
- @acase{@primop @tag*{primitive operations}}
+ @acase{@primop @tag*{primitive functions}}
@acase{@app[e @repeated{e}] @tag*{function application}}
@acase{@ifop[e e e] @tag*{conditional}}
@acase{@λe[(@repeated{x:τ}) e] @tag*{lambda function}}
@@ -87,31 +87,35 @@ Primitive operations:
Values:
@cases["v" #:first-sep "⩴"
- @acase{c}
- @acase{@num-v}
- @acase{@true-v}
+ @acase{@primop @tag*{primitive function}}
+ @acase{@num-v @tag*{number}}
+ @acase{@true-v @tag*{booleans}}
@acase{@false-v}
- @acase{@primop}
- @acase{@λv[ℰ (@repeated{x:τ}) e]}
- @acase{@λv[ℰ (@repeated{x:τ} @${\ .\ } @${x:τ*}) e]}
- @acase{@λv[ℰ (@repeated{x:τ} @${\ .\ } @${x:@polydot[τ α]}) e]}
- @acase{@Λv[ℰ (@repeated{α}) e]}
- @acase{@Λv[ℰ (@repeated{α} @polydotα[α]) e]}
- @acase{@consv[v v]}]
+ @acase{@λv[ℰ (@repeated{x:τ}) e] @tag*{lambda function}}
+ @acase{@λv[ℰ (@repeated{x:τ} @${\ .\ } @${x:τ*}) e]
+ @tag*{variadic function}}
+ @acase{@λv[ℰ (@repeated{x:τ} @${\ .\ } @${x:@polydot[τ α]}) e]
+ @tag*{variadic polymorphic function}}
+ @acase{@Λv[ℰ (@repeated{α}) e]
+ @tag*{polymorphic abstraction}}
+ @acase{@Λv[ℰ (@repeated{α} @polydotα[α]) e]
+ @tag*{variadic polymorphic abstraction}}
+ @acase{@consv[v v] @tag*{pair}}]
Execution environment:
@cases["ℰ" #:first-sep "⩴"
- @acase{@repeated{@↦v[x v]}\ @repeated{@↦v[α τ]}}]
+ @acase{@repeated{@↦v[x v]}\ @repeated{@↦v[α τ]}
+ @tag*{bound variables \& types}}]
Evaluation context:
@cases["E" #:first-sep "⩴"
- @acase{[]}
- @acase{@app[E @repeated{e}]}
+ @acase{[] @tag*{program entry point}}
+ @acase{@app[E @repeated{e}]@tag*{function application}}
@acase{@app[v @repeated{v} E @repeated{e}]}
- @acase{@ifop[E e e]}
- @acase{@conse[E e]} @; TODO: shouldn't it be a primop?
+ @acase{@ifop[E e e]@tag*{conditional}}
+ @acase{@conse[E e]@tag*{pair}} @; TODO: shouldn't it be a primop?
@acase{@conse[v E]}] @; TODO: shouldn't it be a primop?
@; TODO: are other cases needed?
@@ -127,18 +131,20 @@ Typing judgement:
Types:
@cases["τ,σ" #:first-sep "⩴"
- @acase{⊤}
- @acase{@num-τ}
- @acase{@true-τ}
+ @acase{⊤@tag*{top}}
+ @acase{@num-τ @tag*{number singleton}}
+ @acase{@true-τ @tag*{boolean singleton}}
@acase{@false-τ}
- @acase{@f→[(@repeated{τ}) R]}
- @acase{@f→[(@repeated{τ} @${\ .\ } @${τ*}) R]}
- @acase{@f→[(@repeated{τ} @${\ .\ } @polydot[τ α]) R]}
- @acase{@∀r[@${(@repeated{α})} @repeated{τ}]}
- @acase{@∀r[@${(@repeated{α} @polydotα[α])} @repeated{τ}]}
- @acase{@un[@repeated{τ}]}
- @acase{@consτ[τ τ]}
- @acase{@null-τ}]
+ @acase{@f→[(@repeated{τ}) R] @tag*{function}}
+ @acase{@f→[(@repeated{τ} @${\ .\ } @${τ*}) R] @tag*{variadic function}}
+ @acase{@f→[(@repeated{τ} @${\ .\ } @polydot[τ α]) R]
+ @tag*{variadic polymorphic function}}
+ @acase{@∀r[@${(@repeated{α})} @repeated{τ}]@tag*{polymorphic type}}
+ @acase{@∀r[@${(@repeated{α} @polydotα[α])} @repeated{τ}]
+ @tag*{variadic polymorphic type}}
+ @acase{@un[@repeated{τ}]@tag*{union}}
+ @acase{@consτ[τ τ]@tag*{pair}}
+ @acase{@null-τ @tag*{null (end of lists)}}]
@htodo{Add the rec types}
@@ -151,28 +157,30 @@ Types:
Filters (conditional typing information):
-@cases[@${φ} #:first-sep "⩴" @acase{@repeatset{ψ}}]
+@cases[@${φ} #:first-sep "⩴" @acase{@repeatset{ψ}}@tag*{filter set}]
@cases["ψ" #:first-sep "⩴"
- @acase{τ_{@loc}}
- @acase{@!{τ}_{@loc}}
- @acase{⊥}]
+ @acase{τ_{@loc}
+ @tag*{@${ℰ[v] = \mathbf{?} ⇒ ℰ[@loc]@text{ is of type @${τ}}}}}
+ @acase{@!{τ}_{@loc}
+ @tag*{@${ℰ[v] = \mathbf{?} ⇒ ℰ[@loc]@text{ is not of type @${τ}}}}}
+ @acase{⊥@tag*{contradiction}}]
@cases[@loc #:first-sep "⩴"
- @acase{•\qquad\qquad@text{function's first argument}}
- @acase{x}]
+ @acase{•@tag*{function's first argument}}
+ @acase{x@tag*{variable}}]
Objects (aliasing information):
@cases[@textrm{o} #:first-sep "⩴"
- @acase{π(@loc)}
- @acase{∅}]
+ @acase{π(@loc)@tag*{@${e} is an alias for @${π(@loc)}}}
+ @acase{∅@tag*{no aliasing information}}]
Paths:
@cases[@textit{π} #:first-sep "⩴"
- @acase{pe∷π}
- @acase{@emptypath \qquad\qquad\text{empty path}}]
+ @acase{pe∷π@tag*{path concatenation}}
+ @acase{@emptypath @tag*{empty path}}]
The path concatenation operator @${∷} is associative. @htodo{Actually, we
define it for pe∷π above, not for π∷π}. The @${@emptypath} is omitted from
@@ -182,8 +190,8 @@ paths with one or more elements, so we write @${car∷cdr} instead of @${
Path elements (aliasing information):
@cases[@textit{pe} #:first-sep "⩴"
- @acase{car}
- @acase{cdr}]
+ @acase{car@tag*{first element of pair}}
+ @acase{cdr@tag*{second element of pair}}]
Subtyping:
diff --git a/scribblings/adt-utils.rkt b/scribblings/adt-utils.rkt
@@ -182,13 +182,13 @@
[(_ from {~literal ↦} to)
#'@$["{|}_{{" (stringify from) "}↦{" (stringify to) "}}"]]))
-(define update "\\operatorname{update}")
-(define applyfilter "\\operatorname{applyfilter}")
-(define combinefilter "\\operatorname{combinefilter}")
-(define no-overlap "\\operatorname{no-overlap}")
-(define restrict "\\operatorname{restrict}")
-(define remove "\\operatorname{remove}")
-(define loc "\\mathit{loc}")
-(define (! . rest) (list "\\overline{" rest "}"))
-(define metatrue "\\mathrm{true}")
-(define metafalse "\\mathrm{false}")
-\ No newline at end of file
+(define update @${\operatorname{update}})
+(define applyfilter @${\operatorname{applyfilter}})
+(define combinefilter @${\operatorname{combinefilter}})
+(define no-overlap @${\operatorname{no-overlap}})
+(define restrict @${\operatorname{restrict}})
+(define remove @${\operatorname{remove}})
+(define loc @${\mathit{loc}})
+(define (! . rest) @${\overline{@rest}})
+(define metatrue @${\mathrm{true}})
+(define metafalse @${\mathrm{false}})
+\ No newline at end of file
diff --git a/scribblings/phc-thesis.scrbl b/scribblings/phc-thesis.scrbl
@@ -72,6 +72,7 @@
(add1 a)))
1))
+@;{
@aappendix{
@include-asection[(lib "phc-graph/scribblings/phc-graph-implementation.scrbl")]
@include-asection[(lib "phc-adt/scribblings/phc-adt-implementation.scrbl")]
@@ -80,6 +81,7 @@
@include-asection[
(lib "type-expander/scribblings/type-expander-implementation.scrbl")]
}
+}
@;{
Notes concerning tikz → SVG conversion:
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -652,10 +652,10 @@ EOCSS
(define textif @mathtext{\text{ if }})
(define otherwise @mathtext{\text{ otherwise }})
(define quad @${\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 "}"))
+(define (textbf . l) ($ (mathtext "\\textbf{" l "}")))
+(define (textit . l) ($ (mathtext "\\textit{" l "}")))
+(define (textrm . l) ($ (mathtext "\\textrm{" l "}")))
+(define (text . l) ($ (mathtext "\\text{" l "}")))
;; In some cases, LaTeX doesn't like the use of the regular & and \\ because
;; they were redefined (mostly when placing arrays or cases within an inferrule.
@@ -688,7 +688,7 @@ EOCSS
(bytes-append #"\n\\makeatletter\n"
(file->bytes tikztag.sty)
#"\n\\makeatother\n"))))
- (list "\\hphantom{\text{" @mathtext[txt] "}}"
+ (list "\\hphantom{\\text{" @mathtext[txt] "}}"
"\\tikztag" (if starred? "*" "") "{" @mathtext[txt] "}"))]
[else (list " (" txt ")")]))
diff --git a/tikztag.sty b/tikztag.sty
@@ -40,28 +40,29 @@
\xdef\tikztagnumber{\tikztagnumber}%
\tikz[remember picture]\coordinate(tikztagmarker\tikztagnumber){};%
% dispatch given the options
+ \expandafter\gdef\csname @tikztag@tag@\tikztagnumber\endcsname{#1}%
\if@tikztag@label@%
\if@tikztag@labeltext@%
\if@tikztag@star@%
- \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\expandafter\noexpand\@tikztag@labeltext}{\noexpand#1}{\tikztagnumber}{\noexpand\@firstoftwo}}%
+ \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\expandafter\noexpand\@tikztag@labeltext}{\expandafter\noexpand\csname @tikztag@tag@\tikztagnumber\endcsname}{\tikztagnumber}{\noexpand\@firstoftwo}}%
\else%
- \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\expandafter\noexpand\@tikztag@labeltext}{(\noexpand#1)}{\tikztagnumber}{\noexpand\@firstoftwo}}%
+ \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\expandafter\noexpand\@tikztag@labeltext}{(\expandafter\noexpand\csname @tikztag@tag@\tikztagnumber\endcsname)}{\tikztagnumber}{\noexpand\@firstoftwo}}%
\fi%
\else%
\if@tikztag@star@%
- \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\noexpand#1}{\noexpand#1}{\tikztagnumber}{\noexpand\@firstoftwo}}
- \else
- \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\noexpand#1}{(\noexpand#1)}{\tikztagnumber}{\noexpand\@firstoftwo}}
- \fi
- \fi
- \else
- \if@tikztag@star@
- \edef\@@tikztag{\noexpand\@@@tikztag{no label}{no label text}{\noexpand#1}{\tikztagnumber}{\noexpand\@secondoftwo}}
- \else
- \edef\@@tikztag{\noexpand\@@@tikztag{no label}{no label text}{(\noexpand#1)}{\tikztagnumber}{\noexpand\@secondoftwo}}
- \fi
- \fi
- \@@tikztag
+ \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\expandafter\noexpand\csname @tikztag@tag@\tikztagnumber\endcsname}{\expandafter\noexpand\csname @tikztag@tag@\tikztagnumber\endcsname}{\tikztagnumber}{\noexpand\@firstoftwo}}%
+ \else%
+ \edef\@@tikztag{\noexpand\@@@tikztag{\expandafter\noexpand\@tikztag@label}{\expandafter\noexpand\csname @tikztag@tag@\tikztagnumber\endcsname}{(\expandafter\noexpand\csname @tikztag@tag@\tikztagnumber\endcsname)}{\tikztagnumber}{\noexpand\@firstoftwo}}%
+ \fi%
+ \fi%
+ \else%
+ \if@tikztag@star@%
+ \edef\@@tikztag{\noexpand\@@@tikztag{no label}{no label text}{\expandafter\noexpand\csname @tikztag@tag@\tikztagnumber\endcsname}{\tikztagnumber}{\noexpand\@secondoftwo}}%
+ \else%
+ \edef\@@tikztag{\noexpand\@@@tikztag{no label}{no label text}{(\expandafter\noexpand\csname @tikztag@tag@\tikztagnumber\endcsname)}{\tikztagnumber}{\noexpand\@secondoftwo}}%
+ \fi%
+ \fi%
+ \@@tikztag%
}
\newcommand{\@@@tikztag}[5]{%
\g@addto@macro\accumulatetikztag{\@@@@tikztag{#1}{#2}{#3}{#4}{#5}}%
