Update Con notes.

Author: dvanhorn

www/notes/con.scrbl

@@ -16,17 +16,23 @@
 @(define codeblock-include (make-codeblock-include #'h))
 
 @(for-each (λ (f) (ev `(require (file ,(path->string (build-path notes "con" f))))))
-	   '("interp.rkt" "compile.rkt" "asm/interp.rkt" "asm/printer.rkt"))
+	   '("interp.rkt" "compile.rkt" "asm/interp.rkt" "asm/printer.rkt" "random.rkt"))
 
 
 @title[#:tag "Con"]{Con: branching with conditionals}
 
+@emph{When you come to a fork in the road, take it.}
+
+@table-of-contents[]
+
+@section{Conditional execution}
+
 Let's now consider add a notion of @bold{conditionals} to our target
 language.
 
 We'll call it @bold{Con}.
 
-We will use the following syntax...
+We will use the following syntax: @racket[(if (zero? _e0) _e1 _e2)].
 
 Together this leads to the following grammar for Con:
 
@@ -46,9 +52,9 @@ the new form is an if-expression.
 
 @itemlist[
 
-@item{the meaning of a if expression @tt{(if (zero? e0) e1 e2)} is the
-meaning of @math{e1} if the meaning of @tt{e1} if the meaning of
-@tt{e0} is 0 and is the meaning of @math{e2} otherwise.}
+@item{the meaning of a if expression @racket[(if (zero? _e0) _e1 _e2)] is the
+meaning of @racket[_e1] if the meaning of @racket[_e1] if the meaning of
+@racket[_e0] is 0 and is the meaning of @racket[_e2] otherwise.}
 
 ]
 
@@ -204,6 +210,9 @@ In total, the code for this example would look like:
   if-else-end)
 ]
 
+
+@section{A Compiler for Con}
+
 Notice that the @racket['(mov rax 8)], @racket['(mov rax 3)] and
 @racket['(mov rax 2)] parts are just the instructions generated by
 compiling @racket[8], @racket[2] and @racket[3].  Generalizing from
@@ -213,9 +222,9 @@ this, we arrive at the following code for the compiler:
 (let ((c0 (compile-e e0))
       (c1 (compile-e e1))
       (c2 (compile-e e2))
-      (l0 (gensym "if-else-begin"))
-      (l1 (gensym "if-else-end")))
-  '(,@c0
+      (l0 (gensym "if"))
+      (l1 (gensym "if")))
+  `(,@c0
     (cmp rax 0)
     (jne ,l0)
     ,@c1
@@ -226,22 +235,65 @@ this, we arrive at the following code for the compiler:
 ]
 
 
-@ex[
-(asm-display (compile '(if (zero? 8) 2 3)))
-]
-
+This will require extending our representation of x86 instructions; in
+particular, we add @racket['jmp], @racket['jne], and @racket['cmp]
+instructions:
 
 @codeblock-include["con/asm/ast.rkt"]
 
 We omit the printer code, which is mundane.  See
 @link["con/asm/printer.rkt"]{@tt{asm/printer.rkt}} for details.
 
+The complete compiler code is:
+
 @codeblock-include["con/compile.rkt"]
 
+Let's take a look at a few examples:
+@ex[
+(asm-display (compile '(if (zero? 8) 2 3)))
+(asm-display (compile '(if (zero? 0) 1 2)))
+(asm-display (compile '(if (zero? 0) (if (zero? 0) 8 9) 2)))
+(asm-display (compile '(if (zero? (if (zero? 2) 1 0)) 4 5)))
+]
 
+And confirm they are running as expected:
 @ex[
+(asm-interp (compile '(if (zero? 8) 2 3)))
 (asm-interp (compile '(if (zero? 0) 1 2)))
-(asm-interp (compile '(if (zero? 3) 1 2)))
 (asm-interp (compile '(if (zero? 0) (if (zero? 0) 8 9) 2)))
 (asm-interp (compile '(if (zero? (if (zero? 2) 1 0)) 4 5)))
 ]
+
+
+@section[#:tag-prefix "con"]{Correctness and random testing}
+
+The statement of correctness follows the same outline as before:
+
+@bold{Compiler Correctness}: @emph{For all expressions @racket[e] and
+integers @racket[i], if (@racket[e],@racket[i]) in @render-term[C 𝑪],
+then @racket[(asm-interp (compile e))] equals @racket[i].}
+
+Again, we formulate correctness as a property that can be tested:
+
+@ex[
+(define (check-compiler e)
+  (check-equal? (asm-interp (compile e))
+                (interp e)
+                e))]
+
+Generating random Con programs is essentially the same as Blackmail
+programs, and are provided in a @link["con/random.rkt"]{random.rkt}
+module.
+
+@ex[
+(eval:alts (require "random.rkt") (void))
+(random-expr)
+(random-expr)
+(random-expr)
+(random-expr)
+(for ([i (in-range 10)])
+  (check-compiler (random-expr)))
+]
+
+
+