commit 59cbe9bf97f34d4fd481362e0e77caa1d40fcb2d
parent 8221bebb559abd3137f85d4cbe75fdcdf754b6dd
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Wed, 7 Jun 2017 15:00:23 +0200
Moved more from refs.tex
Diffstat:
3 files changed, 310 insertions(+), 186 deletions(-)
diff --git a/scribblings/introduction.scrbl b/scribblings/introduction.scrbl
@@ -22,8 +22,8 @@
concerned with logical errors in their own code, and should not fear that the
compiler introduces erroneous behaviour on its own; extensible because the
language is likely to evolve over time; and fast because the programmer's
- edit-build-test cycle should be as frequent as possible@todo{@~cite{
- smalltalk-programmer-efficiency-cycle}}.
+ edit-build-test cycle should be as frequent as
+ possible@todo{@~cite["smalltalk-programmer-efficiency-cycle"]}.
Given their broad role, the complexity of the transformations involved, and
the stringent requirements, writing compilers is a difficult task. Multiple
@@ -33,15 +33,8 @@
closer to correctness, and easier to maintain.
@require[scribble/core scribble/html-properties scribble/latex-properties]
- @elem[#:style (style "hrStyle"
- (list (alt-tag "hr")
- (css-addition
- #".hrStyle { margin-bottom: 1em; }")
- (tex-addition
- (string->bytes/utf-8 #<<EOTEX
-\def\hrStyle#1{\noindent{\centerline{\rule[0.5ex]{0.5\linewidth}{0.5pt}}}}
-EOTEX
- ))))]{}
+
+ @hr
The overall structure of a compiler will usually include a lexer and parser,
which turn the the program's source into an in-memory representation. This
@@ -59,8 +52,8 @@ EOTEX
@itemlist[
@item{It is easy to reuse excessively a single @usetech{intermediate
- representation}, instead of properly distinguishing the features of the input
- and output of each pass;}
+ representation}, instead of properly distinguishing the features of the
+ input and output of each pass;}
@item{There is a high risk
associated with the definition of large, monolithic passes, which are hard to
test, debug, and extend;}
@@ -199,15 +192,25 @@ EOTEX
(thereby really representing the program as an ``Abstract Syntax Graph''),
using mutation to patch nodes after they are initially created.
- @todo{Mutation: verification (two phases for invariants), generally frowned
- upon, reference some of Roland's and others' work on freezing objects. (as
- long as it is ensured that no improper manipulation of the objects is done
- before freezing).}}
+ In order to prevent undesired mutation of the graph after it is created, it
+ is possible to ``freeze'' the objects contained within@todo{references}.
+ This intuitively gives the guarantees similar to those obtained from a
+ purely immutable representation. However, the use of mutation could obstruct
+ formal verification efforts, as some invariants will need to take into
+ account the two phases of an object's lifetime (during the creation of the
+ containing graph, and after freezing it). More generally speaking, it is
+ necessary to ensure that no mutation of objects happens during the graph
+ construction, with the exception of the mutation required to patch cycles.}
@item{The compiler could also manipulate lazy data structures, where the
actual value of a node in the graph is computed on the fly when that node is
accessed.
- @todo{Lazy: harder to debug}}
+ Lazy programs are however harder to debug@~cite["nilsson1993lazy"
+ "wadler1998functional"
+ "morris1982real"],
+ as the computation of the various parts of the data manipulated do not occur
+ in an intuitive order. Among other things, accidental infinite recursion
+ could be triggered by an access to a value by totally unrelated code.}
@item{Finally, Higher-Order Abstract Syntax, or HOAS for short, is a
technique which encodes variable bindings as anonymous functions in the host
language (whose parameters reify bindings at the level of the host
@@ -287,4 +290,103 @@ EOTEX
different input and output type.
}
-}
-\ No newline at end of file
+}
+
+@asection{
+ @atitle{Summary}
+
+ @asection{ @atitle{Extensible type system} We implemented a different type
+ system on top of @|typedracket|, using macros. Macros have been used not only
+ to extend a language's syntax (control structures, contract annotations, and
+ so on), but also to reduce the amount of ``boilerplate'' code and obtain
+ clearer syntax for common or occasional tasks. Macros have further been used
+ to extend the language with new paradigms, like adding an object system
+ (CLOS@~cite["bobrow_common_1988"]@todo{is it really implemented using
+ macros?}, Racket classes@~cite["flatt_scheme_classes_2006"]) or supporting
+ logic programming (Racket
+ Datalog@note{@url{http://docs.racket-lang.org/datalog/}} and
+ Racklog@note{@url{http://docs.racket-lang.org/racklog/}},
+ Rosette@~cite["torlak_growing_rosette_2013"]). In the past,
+ @|typedracket|@~cite["tobin-hochstadt_design_2008"] has proved that a type
+ system can be successfully fitted onto an existing ``untyped'' language, using
+ macros. We implemented the @racketmodname[type-expander] library atop
+ @|typedracket|, without altering @|typedracket| itself. Our
+ @racketmodname[type-expander] library allows macros to be used in contexts
+ where a type is expected.
+
+ This shows that an existing type system can be made extensible using macros,
+ without altering the core implementation of the type system. We further use
+ these type expanders to build new kinds of types which were not initially
+ supported by @|typedracket|: non-nominal algebraic types, with row
+ polymorphism. @|Typedracket| has successfully been extended in the past (for
+ example by adding type primitives for Racket's class system, which
+ incidentally also support row polymorphism), but these extensions required
+ modifications to the trusted core of @|typedracket|. Aside from a small hack
+ (needed to obtain non-nominal algebraic types which remain equivalent across
+ multiple files), our extension integrates seamlessly with other built-in
+ types, and code using these types can use idiomatic @|typedracket| features.
+
+ @Typedracket was not initially designed with this extension in mind, nor,
+ that we know of, was it designed with the goal of being extensible. We
+ therefore argue that a better choice of primitive types supported by the
+ core implementation could enable many extensions without the need to resort
+ to hacks the like of which was needed in our case. In other words, a better
+ design of the core types with extensibility in mind would have made our job
+ easier.
+
+ In particular, Types in Typed
+ Clojure@~cite["practical_types_for_clojure_2016"] support fine-grained typing
+ of heterogeneous hash tables, this would likely allow us to build much more
+ easily the ``strong duck typing'' primitives on which our algebraic data types
+ are based, and without the need to resort to hacks.
+
+ In languages making heavy uses of macros, it would be beneficial to design
+ type systems with a well-chosen set of primitive type, on top of which more
+ complex types can be built using macros.
+
+ Building the type system via macros atop a small kernel is an approach that
+ has been pursued by Cur, a dependently-typed language developed with Racket,
+ in which the tactics language is entirely built using macros, and does not
+ depend on Cur's trusted type-checking core.}
+
+ @asection{
+ @atitle{Compiler-writing framework}
+
+ Our goal was to introduce a compiler-writing framework, which:
+ @itemlist[
+ @item{Supports writing a compiler using many small passes (in the spirit of
+ Nanopass)}
+ @item{Allows writing the compiler in a strongly-typed language}
+ @item{Uses immutable data structures for the Intermediate Representations
+ (ASTs)}
+ @item{Supports transversal and backwards branches in the AST, making it
+ rather an Abstract Syntax Graph (this is challenging due to the use of
+ immutable data structures).}
+ @item{Provides easy manipulation of the Intermediate Representations: local
+ navigation from node to node, global higher-order operations over many
+ nodes, easy construction, easy serialization, with the guarantee that at
+ no point an incomplete representation can be manipulated. These operations
+ should handle seamlessly transversal and backwards arcs.}
+ @item{Enforces structural invariants (either at compile-time or at
+ run-time), and ensures via the type system that unchecked values cannot be
+ used where a value respecting the invariant is expected.}
+ @item{Has extensive support for testing the compiler, by allowing the
+ generation of random ASTs @todo{(note that the user guides the random
+ generation, it's not fully automatic like quickcheck)}, making it
+ possible to read and write ASTs from files and compare them, and allows
+ compiler passes to consume ASTs containing only the relevant fields (using
+ row polymorphism).}]}
+
+ @htodo{
+ testing (random stuff)
+
+ TODO:@~cite{quickcheck} and other things related to test generation
+ (I have something in Zotero)
+
+ TODO: and the l-sets (find something about that)
+
+ TODO: Problems with ``mocks'' and strong typing (null values everywhere,
+ bleargh).
+ }
+
+}
diff --git a/scribblings/state-of-the-art.scrbl b/scribblings/state-of-the-art.scrbl
@@ -14,8 +14,8 @@
Our work explores one interesting use of macros: their use to extend a
programming language's type system.
- Chang, Knauth and Greenman@~cite{chang2017type-systems-as-macros} took
- the decision to depart from Typed Racket, and implemented a new approach,
+ Chang, Knauth and Greenman@~cite["chang2017type-systems-as-macros"] took
+ the decision to depart from @|typedracket|, and implemented a new approach,
which allows type systems to be implemented as macros. Typing information
about identifiers is threaded across the program at compile-time, and macros
can decide whether a term is well-typed or not.
@@ -24,56 +24,56 @@
dependent type system implemented using Racket macros.
Bracha suggests that pluggable type systems should be
- used@~cite{bracha2004pluggable-types}. Such a system, JavaCOP is presented by
+ used@~cite["bracha2004pluggable-types"]. Such a system, JavaCOP is presented by
Andreae, Noble, Markstrum and
- Shane@~cite{pluggable-types-andreae2006framework} as a tool which ``enforces
+ Shane@~cite["pluggable-types-andreae2006framework"] as a tool which ``enforces
user-defined typing constraints written in a declarative and expressive rule
language''.
- In contrast, Typed Racket@~cite{tobin-hochstadt_design_2008} was
+ In contrast, @|typedracket|@~cite["tobin-hochstadt_design_2008"] was
implemented using macros on top of ``untyped'' Racket, but was not
designed as an extensible system: new rules in the type system must be
added to the core implementation, a system which is complex to approach.
Following work by Asumu
Takikawa@note{@url{https://github.com/racket/racket/pull/604}}, we
- extended Typed Racket with support for macros in the type declarations and
+ extended @|typedracket| with support for macros in the type declarations and
annotations. We call this sort of macro ``type expanders'', following the
commonly-used naming convention (e.g. ``match expanders'' are macros which
operate within patterns in pattern-matching forms). These type expanders
allow users to easily extend the type system with new kinds of types, as
long as these can be translated back to the types offered natively by
- Typed Racket.
+ @|typedracket|.
While the Type Systems as Macros by Chang, Knauth and
- Greenman@~cite{chang2017type-systems-as-macros} allows greater flexibility
+ Greenman@~cite["chang2017type-systems-as-macros"] allows greater flexibility
by not relying on a fixed set of core types, it also places on the
programmer the burden of ensuring that the type checking macros are
- sound. In contrast, our type expanders rely on Typed Racket's type
+ sound. In contrast, our type expanders rely on @|typedracket|'s type
checker, which will still catch type errors in the fully-expanded
types. In other words, writing type expanders is safe, because they do not
- require any specific trust, and translate down to plain Typed Racket
+ require any specific trust, and translate down to plain @|typedracket|
types, where any type error would be caught at that level.
An interesting aspect of our work is that the support for type expanders
- was implemented without any change to the core of Typed Racket. Instead,
+ was implemented without any change to the core of @|typedracket|. Instead,
the support for type expanders itself is available as a library, which
overrides special forms like @tt{define}, @tt{lambda} or
@tt{cast}, enhancing them by pre-processing type expanders, and
- translating back to the ``official'' forms from Typed Racket. It is worth
- noting that Typed Racket itself is implemented in a similar way: special
+ translating back to the ``official'' forms from @|typedracket|. It is worth
+ noting that @|typedracket| itself is implemented in a similar way: special
forms like @tt{define} and @tt{lambda} support plain type
annotations, and translate back to the ``official'' forms from so-called
``untyped'' Racket. In both cases, this approach goes with the Racket
spirit of implementing languages as
- libraries@~cite{tobin-hochstadt_languages_as_libraries_2011}}
+ libraries@~cite["tobin-hochstadt_languages_as_libraries_2011"]}
@asection{
@atitle{Algebraic datatypes for compilers (phc-adt)}
The @tt{phc-adt} library implements algebraic datatypes (variants and
structures) which are adapted to compiler-writing.
- There is an existing ``simple'' datatype library for Typed/Racket (source
+ There is an existing ``simple'' datatype library for @|typedracket| (source
code available at @url{https://github.com/pnwamk/datatype}). It differs
from our library on several points:
@itemlist[
@@ -134,17 +134,17 @@
@subsubsub*section{Subtyping, polymorphism and alternatives}
@|~|@(linebreak)
- @~cite{ducournau-cours-lots}. @htodo{The course includes a couple of
+ @~cite["ducournau-cours-lots"]. @htodo{The course includes a couple of
other kinds of polymorphism and subtyping (or makes finer distinctions
than in the list below). Refine and augment the list below using
Roland's classification.} @htodo{Probably also cite:}
- @~cite{cardelli1985understanding} @htodo{(apparently does not cover
+ @~cite["cardelli1985understanding"] @htodo{(apparently does not cover
``Higher-Kinded Polymorphism'', ``Structural Polymorphism'' and ``Row
Polymorphism'')}
@itemlist[
@item{Subtyping (also called inclusion polymorphism, subtype
polymorphism, or nominal subtyping ?): Subclasses and interfaces in
- @csharp and Java, sub-structs and union types in Typed Racket,
+ @csharp and Java, sub-structs and union types in @|typedracket|,
polymorphic variants in @CAML @~cite[#:precision @list{chap. 6, sec. Polymorphic Variants}]{minsky2013real}}
@; https://realworldocaml.org/v1/en/html/variants.html
@@ -269,7 +269,7 @@
the interface has to be explicitly implemented by the class (i.e. at
the definition site, not at the use-site).
- Palmer et al. present TinyBang@~cite{types-for-flexible-objects}, a
+ Palmer et al. present TinyBang@~cite["types-for-flexible-objects"], a
typed language in which flexible manipulation of objects is possible,
including adding and removing fields, as well as changing the type of
a field. They implement in this way a sound, decidable form of static
@@ -328,7 +328,7 @@
@; phc/reading/CITE/Object-Oriented Programming_ What is a concise definition of polymorphism_ - Quora.html
@; TODO: fix the footnote here!
See also post on Quora@superscript{\ref{quora-url-footnote}},
- which links to @~cite{cardelli1985understanding}, and to a blog post by Sam
+ which links to @~cite["cardelli1985understanding"], and to a blog post by Sam
Tobin-Hochstadt@note{@url|{https://medium.com/@samth/on-typed-untyped-and-uni-typed-languages-8a3b4bedf68c}|}
The blog post by Sam Tobin-Hochstadt explains how @typedracket tries to
explore and understand how programmers think about programs written in
@@ -422,139 +422,136 @@
}
@asection{
- @atitle{Representation and transformation of graphs}
+ @atitle{Cycles in intermediate representations of programs}
@todo{There already were a few references in my proposal for JFLA.}
@todo{Look for articles about graph rewriting systems.}
- @asection{
- @atitle{Cycles in intermediate representations of programs}
- The following sections present the many ways in which cycles within the
- AST, CFG and other intermediate representations can be represented.
+ The following sections present the many ways in which cycles within the
+ AST, CFG and other intermediate representations can be represented.
- @asection{
- @atitle{Mutable data structures}
+ @asection{
+ @atitle{Mutable data structures}
- @itemlist[
+ @itemlist[
@item{Hard to debug}
@item{When e.g. using lazy-loading, it is easy to mistakenly load a
- class or method after the Intermediate Representation was
- frozen. Furthermore, unless a @tt{.freeze()} method actually
- enforces this conceptual change from a mutable to an immutable
- representation, it can be unclear at which point the IR (or parts of
- it) is guaranteed to be complete and its state frozen. This is another
- factor making maintenance of such code difficult.}]
- Quote from@~cite{ramsey_applicative_2006}:
-
- @quotation{
- We are using ML to build a compiler that does low-level optimization. To
- support optimizations in classic imperative style, we built a control-flow
- graph using mutable pointers and other mutable state in the nodes. This
- decision proved unfortunate: the mutable flow graph was big and complex,
- and it led to many bugs. We have replaced it by a smaller, simpler,
- applicative flow graph based on Huet’s (1997) zipper. The new flow graph
- is a success; this paper presents its design and shows how it leads to a
- gratifyingly simple implementation of the dataflow framework developed by
- Lerner, Grove, and Chambers (2002).}
- }
+ class or method after the Intermediate Representation was
+ frozen. Furthermore, unless a @tt{.freeze()} method actually
+ enforces this conceptual change from a mutable to an immutable
+ representation, it can be unclear at which point the IR (or parts of
+ it) is guaranteed to be complete and its state frozen. This is another
+ factor making maintenance of such code difficult.}]
+ Quote from@~cite["ramsey_applicative_2006"]:
- @asection{
- @atitle{Unique identifiers used as a replacement for pointers}
+ @quotation{
+ We are using ML to build a compiler that does low-level optimization. To
+ support optimizations in classic imperative style, we built a control-flow
+ graph using mutable pointers and other mutable state in the nodes. This
+ decision proved unfortunate: the mutable flow graph was big and complex,
+ and it led to many bugs. We have replaced it by a smaller, simpler,
+ applicative flow graph based on Huet’s (1997) zipper. The new flow graph
+ is a success; this paper presents its design and shows how it leads to a
+ gratifyingly simple implementation of the dataflow framework developed by
+ Lerner, Grove, and Chambers (2002).}
+ }
+
+ @asection{
+ @atitle{Unique identifiers used as a replacement for pointers}
- @htodo{Check that the multi-reference worked correctly here}
- Mono uses that@~cite["mono-cecil-website" "mono-cecil-source"], it is very
- easy to use an identifier which is supposed to reference a missing
- object, or an object from another version of the AST. It is also very
- easy to get things wrong when duplicating nodes (e.g. while specializing
- methods based on their caller), or when merging or removing nodes.
+ @htodo{Check that the multi-reference worked correctly here}
+ Mono uses that@~cite["mono-cecil-website" "mono-cecil-source"], it is very
+ easy to use an identifier which is supposed to reference a missing
+ object, or an object from another version of the AST. It is also very
+ easy to get things wrong when duplicating nodes (e.g. while specializing
+ methods based on their caller), or when merging or removing nodes.
- }
+ }
- @asection{
- @atitle{Explicit use of other common graph representations}
+ @asection{
+ @atitle{Explicit use of other common graph representations}
- Adjacency lists, @DeBruijn indices.
+ Adjacency lists, @DeBruijn indices.
- @itemlist[
+ @itemlist[
@item{ Error prone when updating the graph (moving nodes around, adding,
- duplicating or removing nodes).}
+ duplicating or removing nodes).}
@item{Needs manual @htodo{caretaking}}]
- }
+ }
- @asection{
- @atitle{Using lazy programming languages}
+ @asection{
+ @atitle{Using lazy programming languages}
- @itemlist[
+ @itemlist[
@item{Lazy programming is harder to debug.
- @(linebreak)
- Quote@~cite{nilsson1993lazy}:
- @aquote{
- Traditional debugging techniques are, however, not suited for lazy
- functional languages since computations generally do not take place in the
- order one might expect.
- }
-
- Quote@~cite{nilsson1993lazy}:
- @aquote{
- Within the field of lazy functional programming, the lack of suitable
- debugging tools has been apparent for quite some time. We feel that
- traditional debugging techniques (e.g. breakpoints, tracing, variable
- watching etc.) are not particularly well suited for the class of lazy
- languages since computations in a program generally do not take place in the
- order one might expect from reading the source code.
- }
-
- Quote@~cite{wadler1998functional}:
- @aquote{
- To be usable, a language system must be accompanied by a debugger and a
- profiler. Just as with interlanguage working, designing such tools is
- straightforward for strict languages, but trickier for lazy languages.
- }
-
- Quote@~cite{wadler1998functional}:
- @aquote{
- Constructing debuggers and profilers for lazy languages is recognized as
- difficult. Fortunately, there have been great strides in profiler research,
- and most implementations of Haskell are now accompanied by usable time and
- space profiling tools. But the slow rate of progress on debuggers for lazy
- languages makes us researchers look, well, lazy.
- }
-
- Quote@~cite{morris1982real}:
- @aquote{
- How does one debug a program with a surprising evaluation order? Our
- attempts to debug programs submitted to the lazy implementation have been
- quite entertaining. The only thing in our experience to resemble it was
- debugging a multi-programming system, but in this case virtually every
- parameter to a procedure represents a new process. It was difficult to
- predict when something was going to happen; the best strategy seems to be
- to print out well-defined intermediate results, clearly labelled.
- }}
+ @(linebreak)
+ Quote@~cite["nilsson1993lazy"]:
+ @aquote{
+ Traditional debugging techniques are, however, not suited for lazy
+ functional languages since computations generally do not take place in the
+ order one might expect.
+ }
+
+ Quote@~cite["nilsson1993lazy"]:
+ @aquote{
+ Within the field of lazy functional programming, the lack of suitable
+ debugging tools has been apparent for quite some time. We feel that
+ traditional debugging techniques (e.g. breakpoints, tracing, variable
+ watching etc.) are not particularly well suited for the class of lazy
+ languages since computations in a program generally do not take place in
+ the order one might expect from reading the source code.
+ }
+
+ Quote@~cite["wadler1998functional"]:
+ @aquote{
+ To be usable, a language system must be accompanied by a debugger and a
+ profiler. Just as with interlanguage working, designing such tools is
+ straightforward for strict languages, but trickier for lazy languages.
+ }
+
+ Quote@~cite["wadler1998functional"]:
+ @aquote{
+ Constructing debuggers and profilers for lazy languages is recognized as
+ difficult. Fortunately, there have been great strides in profiler research,
+ and most implementations of Haskell are now accompanied by usable time and
+ space profiling tools. But the slow rate of progress on debuggers for lazy
+ languages makes us researchers look, well, lazy.
+ }
+
+ Quote@~cite["morris1982real"]:
+ @aquote{
+ How does one debug a program with a surprising evaluation order? Our
+ attempts to debug programs submitted to the lazy implementation have been
+ quite entertaining. The only thing in our experience to resemble it was
+ debugging a multi-programming system, but in this case virtually every
+ parameter to a procedure represents a new process. It was difficult to
+ predict when something was going to happen; the best strategy seems to be
+ to print out well-defined intermediate results, clearly labelled.
+ }}
@item{So-called ``infinite'' data structures constructed lazily have
- problems with equality and serialization. The latter is especially
- important for serializing and de-serializing Intermediate
- Representations for the purpose of testing, and is also very important
- for code generation: the backend effectively needs to turn the
- infinite data structure into a finite one. The Revised$^6$ Report on
- Scheme requires the @racket{equal?} predicate to correctly handle
- cyclic data structures, but efficient algorithms implementing this
- requirement are nontrivial@~cite{adams2008efficient}. Although any
- representation of cyclic data structures will have at some point to
- deal with equality and serialization, it is best if these concerns are
- abstracted away as much as possible.}]
- }
+ problems with equality and serialization. The latter is especially
+ important for serializing and de-serializing Intermediate
+ Representations for the purpose of testing, and is also very important
+ for code generation: the backend effectively needs to turn the
+ infinite data structure into a finite one. The Revised$^6$ Report on
+ Scheme requires the @racket{equal?} predicate to correctly handle
+ cyclic data structures, but efficient algorithms implementing this
+ requirement are nontrivial@~cite["adams2008efficient"]. Although any
+ representation of cyclic data structures will have at some point to
+ deal with equality and serialization, it is best if these concerns are
+ abstracted away as much as possible.}]
+ }
- @asection{
- @atitle{True graph representations using immutable data structures}
- @itemlist[
- @item{Roslyn@~cite{overbey2013immutable} : immutable trees with ``up'' pointers}
- @item{The huet zipper@~cite{huet1997zipper}. Implementation in untyped Racket,
- but not Typed
- Racket@note{
- @url{http://docs.racket-lang.org/zippers/}
- @(linebreak)
- @url{https://github.com/david-christiansen/racket-zippers}}}]
- }
+ @asection{
+ @atitle{True graph representations using immutable data structures}
+ @itemlist[
+ @item{Roslyn@~cite["overbey2013immutable"] : immutable trees with ``up''
+ pointers}
+ @item{The huet zipper@~cite["huet1997zipper"]. Implementation in untyped
+ Racket, but not @|typedracket|@note{
+ @url{http://docs.racket-lang.org/zippers/}
+ @(linebreak)
+ @url{https://github.com/david-christiansen/racket-zippers}}}]
}
}
\ No newline at end of file
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -24,7 +24,8 @@
struct-update
part-style-update
epigraph
- usetech)
+ usetech
+ hr)
(require racket/stxparam
racket/splicing
@@ -263,39 +264,24 @@
args
(coloured-elem "gray" "]" (superscript "Todo"))))
-(define (aquote . content)
- (apply nested
- #:style (style "quote"
- (list (css-addition
- (string->bytes/utf-8 #<<EOCSS
-.quote {
- background: #eee;
- padding: 0.5em 1em;
- margin-left: 2em;
- margin-right: 2em;
-}
-EOCSS
- ))))
- content #;(list (paragraph content))))
-
-(define (quotation . content)
- (apply nested
- #:style (style "quotation"
- (list (css-addition
- (string->bytes/utf-8 #<<EOCSS
+(define quote-quotation-css (string->bytes/utf-8 #<<EOCSS
+.quote,
.quotation {
background: #eee;
- padding: 0.75em 1em;
- margin-left: 2em;
- margin-right: 2em;
+ padding: 0.885rem 1.18em; /* 0.75 and 1 ×main font-size */
+ margin-left: 2.36rem; /* 2×main font-size */
+ margin-right: 2.36rem; /* 2×main font-size */
+ margin-top: 1.77rem; /* 1.5×main font-size */
quotes: "“" "”" "‘" "’";
}
+.quote > p:last-child,
.quotation > p:last-child {
margin-bottom: 0;
}
-.quotation:before {
+.quote-old:before,
+.quotation-old:before {
content: open-quote;
color:gray;
font-size: 200%;
@@ -303,18 +289,47 @@ EOCSS
margin-left: -0.45em;
margin-top: -0.25em;
}
+
+.quote:before,
+.quotation:before {
+ content: open-quote;
+ color: gray;
+ font-size: 2.36rem; /* 2×outer font-size */
+ float: left;
+ background: #eee;
+ border-radius: 1.77rem; /* 1.5×outer font-size */
+ width: 3.54rem; /* 3×outer font-size */
+ height: 2.36rem; /* 2×outer font-size */
+ text-align: center;
+ padding: 0.826rem 0 0.354rem; /* 0.7, 0 and 0.3 ×outer font-size */
+ display: inline-block;
+ margin-left: -2.95rem; /* -2.5×outer font-size */
+ margin-top: -2.36rem; /* -2×outer font-size */
+ margin-right: -2.95rem; /* -2.5×outer font-size */
+}
+
+.quote:after,
.quotation:after {
content: close-quote;
- color:gray;
- font-size: 200%;
+ color: gray;
+ font-size: 2.36rem; /* 2×outer font-size */
float: right;
- margin-right: -0.25em;
- margin-top: -0.75em;
+ margin-right: -0.295rem; /* -0.25×outer font-size */
+ margin-top: -1.18rem; /* -1×outer font-size */
}
+
EOCSS
- ))))
- content #;(list (paragraph (style #f '())
- content))))
+ ))
+
+(define (aquote . content)
+ (apply nested
+ #:style (style "quote" (list (css-addition quote-quotation-css)))
+ content #;(list (paragraph content))))
+
+(define (quotation . content)
+ (apply nested
+ #:style (style "quotation" (list (css-addition quote-quotation-css)))
+ content))
(define (~cite* #:precision [precision #f] . rest)
(if precision
@@ -402,4 +417,15 @@ EOTEX
;; For now, do not perform any check. Later on, we may verify automatically that
;; a usetech always happens after the corresponding deftech.
-(define usetech list)
-\ No newline at end of file
+(define usetech list)
+
+(define hr
+ (elem #:style (style "hrStyle"
+ (list (alt-tag "hr")
+ (css-addition
+ #".hrStyle { margin-bottom: 1em; }")
+ (tex-addition
+ (string->bytes/utf-8 #<<EOTEX
+\def\hrStyle#1{\noindent{\centerline{\rule[0.5ex]{0.5\linewidth}{0.5pt}}}}
+EOTEX
+ ))))))
+\ No newline at end of file
