Skip to content

Commit 06574e5

Browse files
committed
Get the notes building with ziggy.
1 parent 7a5a4a5 commit 06574e5

11 files changed

Lines changed: 194 additions & 195 deletions

File tree

www/notes/abscond.scrbl

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -150,10 +150,10 @@ parse the concrete expression as an s-expression.
150150
While not terribly useful for a language as overly simplistic as Abscond, we use
151151
an AST datatype for representing expressions and another syntactic categories.
152152
For each category, we will have an appropriate constructor. In the case of Abscond
153-
all expressions are integers, so we have a single constructor, @racket[Int].
153+
all expressions are integers, so we have a single constructor, @racket[Lit].
154154

155155
@(define-language A-concrete
156-
(e ::= (Int i))
156+
(e ::= (Lit i))
157157
(i ::= integer))
158158

159159
@centered{@render-language[A-concrete]}
@@ -171,7 +171,7 @@ it is, otherwise it signals an error:
171171
@section{Meaning of Abscond programs}
172172

173173
The meaning of an Abscond program is simply the number itself. So
174-
@racket[(Int 42)] evaluates to @racket[42].
174+
@racket[(Lit 42)] evaluates to @racket[42].
175175

176176
We can write an ``interpreter'' that consumes an expression and
177177
produces it's meaning:
@@ -180,8 +180,8 @@ produces it's meaning:
180180

181181
@#reader scribble/comment-reader
182182
(examples #:eval ev
183-
(interp (Int 42))
184-
(interp (Int -8))
183+
(interp (Lit 42))
184+
(interp (Lit -8))
185185
)
186186

187187
We can add a command line wrapper program for interpreting Abscond
@@ -213,15 +213,15 @@ language, just a single inference rule suffices:
213213
#:mode (𝑨 I O)
214214
#:contract (𝑨 e i)
215215
[----------
216-
(𝑨 (Int i) i)])
216+
(𝑨 (Lit i) i)])
217217

218218
@(centered (render-judgment-form 𝑨))
219219

220220
Here, we are defining a binary relation, called
221221
@render-term[A 𝑨], and saying every integer literal
222222
expression is paired with the integer itself in the
223-
relation. So @math{((Int 2),2)} is in @render-term[A 𝑨],
224-
@math{((Int 5),5)} is in @render-term[A 𝑨], and so on.
223+
relation. So @math{((Lit 2),2)} is in @render-term[A 𝑨],
224+
@math{((Lit 5),5)} is in @render-term[A 𝑨], and so on.
225225

226226
The inference rules define the binary relation by defining the
227227
@emph{evidence} for being in the relation. The rule makes use of
@@ -419,8 +419,8 @@ Writing the @racket[compile] function is easy:
419419

420420
@#reader scribble/comment-reader
421421
(examples #:eval ev
422-
(compile (Int 42))
423-
(compile (Int 38))
422+
(compile (Lit 42))
423+
(compile (Lit 38))
424424
)
425425

426426
To convert back to the concrete NASM syntax, we use
@@ -432,7 +432,7 @@ appropriately.}
432432

433433
@#reader scribble/comment-reader
434434
(examples #:eval ev
435-
(asm-display (compile (Int 42))))
435+
(asm-display (compile (Lit 42))))
436436

437437
Putting it all together, we can write a command line compiler much
438438
like the command line interpreter before, except now we emit assembly
@@ -533,17 +533,17 @@ compilation within Racket:
533533

534534

535535
@examples[#:eval ev
536-
(asm-interp (compile (Int 42)))
537-
(asm-interp (compile (Int 37)))
538-
(asm-interp (compile (Int -8)))
536+
(asm-interp (compile (Lit 42)))
537+
(asm-interp (compile (Lit 37)))
538+
(asm-interp (compile (Lit -8)))
539539
]
540540

541541
This of course agrees with what we will get from the interpreter:
542542

543543
@examples[#:eval ev
544-
(interp (Int 42))
545-
(interp (Int 37))
546-
(interp (Int -8))
544+
(interp (Lit 42))
545+
(interp (Lit 37))
546+
(interp (Lit -8))
547547
]
548548

549549
We can turn this in a @bold{property-based test}, i.e. a function that
@@ -554,9 +554,9 @@ correctness claim:
554554
(check-eqv? (interp e)
555555
(asm-interp (compile e))))
556556

557-
(check-compiler (Int 42))
558-
(check-compiler (Int 37))
559-
(check-compiler (Int -8))
557+
(check-compiler (Lit 42))
558+
(check-compiler (Lit 37))
559+
(check-compiler (Lit -8))
560560
]
561561

562562
This is a powerful testing technique when combined with random
@@ -565,11 +565,11 @@ Abscond programs, we can randomly generate @emph{any} Abscond program
565565
and check that it holds.
566566

567567
@examples[#:eval ev
568-
(check-compiler (Int (random 100)))
568+
(check-compiler (Lit (random 100)))
569569

570570
; test 10 random programs
571571
(for ([i (in-range 10)])
572-
(check-compiler (Int (random 10000))))
572+
(check-compiler (Lit (random 10000))))
573573
]
574574

575575
The last expression is taking 10 samples from the space of Abscond

www/notes/blackmail.scrbl

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -77,10 +77,10 @@ The grammar of abstract Backmail expressions is:
7777

7878
@centered{@render-language[B]}
7979

80-
So, @racket[(Int 0)], @racket[(Int 120)], and
81-
@racket[(Int -42)] are Blackmail AST expressions, but so are
82-
@racket[(Prim1 'add1 (Int 0))], @racket[(Sub1 (Int 120))],
83-
@racket[(Prim1 'add1 (Prim1 'add1 (Prim1 'add1 (Int -42))))].
80+
So, @racket[(Lit 0)], @racket[(Lit 120)], and
81+
@racket[(Lit -42)] are Blackmail AST expressions, but so are
82+
@racket[(Prim1 'add1 (Lit 0))], @racket[(Sub1 (Lit 120))],
83+
@racket[(Prim1 'add1 (Prim1 'add1 (Prim1 'add1 (Lit -42))))].
8484

8585
A datatype for representing expressions can be defined as:
8686

@@ -129,7 +129,7 @@ contrast to the first rule, which applies unconditionally.
129129

130130
We can understand these rules as saying the following:
131131
@itemlist[
132-
@item{For all integers @math{i}, @math{((Int i),i)} is in @render-term[B 𝑩].}
132+
@item{For all integers @math{i}, @math{((Lit i),i)} is in @render-term[B 𝑩].}
133133

134134
@item{For expressions @math{e_0} and all integers @math{i_0} and
135135
@math{i_1}, if @math{(e_0,i_0)} is in @render-term[B 𝑩] and @math{i_1
@@ -157,11 +157,11 @@ interpreter, one for each form of expression:
157157
@codeblock-include["blackmail/interp.rkt"]
158158

159159
@examples[#:eval ev
160-
(interp (Int 42))
161-
(interp (Int -7))
162-
(interp (Prim1 'add1 (Int 42)))
163-
(interp (Prim1 'sub1 (Int 8)))
164-
(interp (Prim1 'add1 (Prim1 'add1 (Prim1 'add1 (Int 8)))))
160+
(interp (Lit 42))
161+
(interp (Lit -7))
162+
(interp (Prim1 'add1 (Lit 42)))
163+
(interp (Prim1 'sub1 (Lit 8)))
164+
(interp (Prim1 'add1 (Prim1 'add1 (Prim1 'add1 (Lit 8)))))
165165
]
166166

167167
Here's how to connect the dots between the semantics and interpreter:
@@ -172,7 +172,7 @@ expression, which determines which rule of the semantics applies.
172172

173173
@itemlist[
174174

175-
@item{if @math{e} is an integer @math{(Int i)}, then we're done: this is the
175+
@item{if @math{e} is an integer @math{(Lit i)}, then we're done: this is the
176176
right-hand-side of the pair @math{(e,i)} in @render-term[B 𝑩].}
177177

178178
@item{if @math{e} is an expression @RACKET[(Prim1 'add1 (UNSYNTAX
@@ -241,9 +241,9 @@ recursion, much like the interpreter.
241241
We can now try out a few examples:
242242

243243
@ex[
244-
(compile (Prim1 'add1 (Prim1 'add1 (Int 40))))
245-
(compile (Prim1 'sub1 (Int 8)))
246-
(compile (Prim1 'add1 (Prim1 'add1 (Prim1 'sub1 (Prim1 'add1 (Int -8))))))
244+
(compile (Prim1 'add1 (Prim1 'add1 (Lit 40))))
245+
(compile (Prim1 'sub1 (Lit 8)))
246+
(compile (Prim1 'add1 (Prim1 'add1 (Prim1 'sub1 (Prim1 'add1 (Lit -8))))))
247247
]
248248

249249
And give a command line wrapper for parsing, checking, and compiling
@@ -264,9 +264,9 @@ the same @racket[asm-interp] function to encapsulate running
264264
assembly code:
265265

266266
@ex[
267-
(asm-interp (compile (Prim1 'add1 (Prim1 'add1 (Int 40)))))
268-
(asm-interp (compile (Prim1 'sub1 (Int 8))))
269-
(asm-interp (compile (Prim1 'add1 (Prim1 'add1 (Prim1 'add1 (Prim1 'add1 (Int -8)))))))
267+
(asm-interp (compile (Prim1 'add1 (Prim1 'add1 (Lit 40)))))
268+
(asm-interp (compile (Prim1 'sub1 (Lit 8))))
269+
(asm-interp (compile (Prim1 'add1 (Prim1 'add1 (Prim1 'add1 (Prim1 'add1 (Lit -8)))))))
270270
]
271271

272272
@section{Correctness and random testing}
@@ -332,10 +332,10 @@ x86 does. Let's see:
332332
@ex[
333333
(define max-int (sub1 (expt 2 63)))
334334
(define min-int (- (expt 2 63)))
335-
(asm-interp (compile (Int max-int)))
336-
(asm-interp (compile (Prim1 'add1 (Int max-int))))
337-
(asm-interp (compile (Int min-int)))
338-
(asm-interp (compile (Prim1 'sub1 (Int min-int))))]
335+
(asm-interp (compile (Lit max-int)))
336+
(asm-interp (compile (Prim1 'add1 (Lit max-int))))
337+
(asm-interp (compile (Lit min-int)))
338+
(asm-interp (compile (Prim1 'sub1 (Lit min-int))))]
339339

340340
Now there's a fact you didn't learn in grade school: in the
341341
first example, adding 1 to a number made it smaller; in the
@@ -344,18 +344,18 @@ second, subtracting 1 made it bigger!
344344
This problem doesn't exist in the interpreter:
345345

346346
@ex[
347-
(interp (Int max-int))
348-
(interp (Prim1 'add1 (Int max-int)))
349-
(interp (Int min-int))
350-
(interp (Prim1 'sub1 (Int min-int)))
347+
(interp (Lit max-int))
348+
(interp (Prim1 'add1 (Lit max-int)))
349+
(interp (Lit min-int))
350+
(interp (Prim1 'sub1 (Lit min-int)))
351351
]
352352

353353
So we have found a counter-example to the claim of compiler
354354
correctness:
355355

356356
@ex[
357-
(check-compiler (Prim1 'add1 (Int max-int)))
358-
(check-compiler (Prim1 'sub1 (Int min-int)))
357+
(check-compiler (Prim1 'add1 (Lit max-int)))
358+
(check-compiler (Prim1 'sub1 (Lit min-int)))
359359
]
360360

361361
What can we do? This is the basic problem of a program not

www/notes/con.scrbl

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -269,7 +269,7 @@ The complete compiler code is:
269269
Mirroring the change we made to the interpreter, we separate out a
270270
module for compiling primitives:
271271

272-
@codeblock-include["con/compile-prim.rkt"]
272+
@codeblock-include["con/compile-ops.rkt"]
273273

274274
Let's take a look at a few examples:
275275
@ex[

www/notes/dodger.scrbl

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -114,27 +114,27 @@ The meaning of characters and their operations are just lifted from Racket.
114114
We can try out some examples:
115115

116116
@ex[
117-
(interp (Char #\a))
118-
(interp (Char #\b))
119-
(interp (Prim1 'char? (Char #\a)))
120-
(interp (Prim1 'char? (Bool #t)))
121-
(interp (Prim1 'char->integer (Char #\a)))
122-
(interp (Prim1 'integer->char (Prim1 'char->integer (Char #\a))))
117+
(interp (Lit #\a))
118+
(interp (Lit #\b))
119+
(interp (Prim1 'char? (Lit #\a)))
120+
(interp (Prim1 'char? (Lit #t)))
121+
(interp (Prim1 'char->integer (Lit #\a)))
122+
(interp (Prim1 'integer->char (Prim1 'char->integer (Lit #\a))))
123123
]
124124

125125
Just as in Dupe, type errors result in the interpreter crashing:
126126

127127

128128
@ex[
129-
(eval:error (interp (Prim1 'char->integer (Bool #f))))
129+
(eval:error (interp (Prim1 'char->integer (Lit #f))))
130130
]
131131

132132
Also, not every integer corresponds to a character, so when
133133
@racket[integer->char] is given an invalid input, it crashes
134134
(more on this in a minute):
135135

136136
@ex[
137-
(eval:error (interp (Prim1 'integer->char (Int -1))))
137+
(eval:error (interp (Prim1 'integer->char (Lit -1))))
138138
]
139139

140140
@section{Ex uno plures iterum: Out of One, Many... Again}

0 commit comments

Comments
 (0)