con.scrbl

#lang scribble/manual

@(require (for-label (except-in racket compile ...) a86/printer a86/ast))
@(require redex/pict
          racket/runtime-path
          scribble/examples
	  #;(except-in "con/semantics.rkt" ext lookup)
	  #;(prefix-in sem: (only-in "con/semantics.rkt" ext lookup))
	  "utils.rkt"
	  "ev.rkt"
	  con/semantics
	  "../utils.rkt")



@(define codeblock-include (make-codeblock-include #'h))


@(ev '(require rackunit a86))
@(for-each (λ (f) (ev `(require (file ,(path->string (build-path langs "con" f))))))
	   '("main.rkt" "random.rkt" "correct.rkt"))


@title[#:tag "Con"]{Con: branching with conditionals}

@src-code["con"]

@emph{When you come to a fork in the road, take it.}

@table-of-contents[]

@section{Conditional execution}

Let's now consider adding a notion of @bold{conditionals} to our target
language.

We'll call it @bold{Con}.

We will use the following concrete syntax: @racket[(if (zero? _e0) _e1 _e2)].

This leads to the following grammar for concrete Con:

@centered{@render-language[C-concrete]}

And abstract grammar:

@codeblock-include["con/ast.rkt"]

@;{
 We will also need a predicate for well-formed Con expressions, but
let's return to this after considering the semantics and interpreter.
}

The parser is similar to what we've seen before:

@codeblock-include["con/parse.rkt"]

@ex[
(parse '(if (zero? 42) 1 2))
(parse '(if (zero? (sub1 1)) (add1 2) (sub1 7)))
(parse '(if (zero? 0) (if (zero? 1) 2 3) 4))]


@section{Meaning of Con programs}

The meaning of Con programs depends on the form of the expression and
the new form is an if-expression.

@itemlist[

@item{the meaning of a if expression @racket[(IfZero _e0 _e1 _e2)] is
the meaning of @racket[_e1] if the meaning of @racket[_e0] is 0 and is
the meaning of @racket[_e2] otherwise.}

]

Let's consider some examples (using concrete notation):

@itemlist[

@item{@racket[(if (zero? 0) (add1 2) 4)] means @racket[3].}
@item{@racket[(if (zero? 1) (add1 2) 4)] means @racket[4].}
@item{@racket[(if (zero? (if (zero? (sub1 1)) 1 0)) (add1 2) 4)] means @racket[4].}
@item{@racket[(if (zero? (add1 0)) (add1 2) (if (zero? (sub1 1)) 1 0))] means @racket[1].}

]


@;{The semantics is inductively defined as before.  There are @emph{two}
new rules added for handling if-expressions: one for when the test
expression means @racket[0] and one for when it doesn't.

@(define ((rewrite s) lws)
   (define lhs (list-ref lws 2))
   (define rhs (list-ref lws 3))
   (list "" lhs (string-append " " (symbol->string s) " ") rhs ""))

@(require (only-in racket add-between))
@(define-syntax-rule (show-judgment name i j)
   (with-unquote-rewriter
      (lambda (lw)
        (build-lw (lw-e lw) (lw-line lw) (lw-line-span lw) (lw-column lw) (lw-column-span lw)))
      (with-compound-rewriters (['+ (rewrite '+)]
                                ['- (rewrite '–)]
                                ['= (rewrite '=)]
				['!= (rewrite '≠)])
        (apply centered
	   (add-between 
             (build-list (- j i)
	                 (λ (n) (begin (judgment-form-cases (list (+ n i)))
	                               (render-judgment-form name))))
             (hspace 4))))))

@(show-judgment 𝑪 0 3)
@(show-judgment 𝑪 3 5)


@;{
The heart of the semantics is an auxiliary relation, @render-term[C
𝑪𝒓], which relates an expression and an environement to the integer
the expression evaluates to (in the given environment):

@(define ((rewrite s) lws)
   (define lhs (list-ref lws 2))
   (define rhs (list-ref lws 3))
   (list "" lhs (string-append " " (symbol->string s) " ") rhs ""))

@(require (only-in racket add-between))
@(define-syntax-rule (show-judgment name i j)
   (with-unquote-rewriter
      (lambda (lw)
        (build-lw (lw-e lw) (lw-line lw) (lw-line-span lw) (lw-column lw) (lw-column-span lw)))
      (with-compound-rewriters (['+ (rewrite '+)]
                                ['- (rewrite '–)])
        (apply centered
	   (add-between 
             (build-list (- j i)
	                 (λ (n) (begin (judgment-form-cases (list (+ n i)))
	                               (render-judgment-form name))))
             (hspace 4))))))

@(show-judgment 𝑪𝒓 0 3)
@(show-judgment 𝑪𝒓 3 5)

It relies on two functions: one for extending an environment with a
variable binding and one for lookup up a variable binding in an
environment:

@centered{
@render-metafunction[sem:ext #:contract? #t]

@(with-atomic-rewriter
  'undefined
  "⊥"
  (render-metafunction sem:lookup #:contract? #t))}

The operational semantics for Con is then defined as a binary relation
@render-term[C 𝑪], which says that @math{(e,i)} in @render-term[C 𝑪],
only when @math{e} evaluates to @math{i} in the empty environment
according to @render-term[C 𝑪𝒓]:

@(show-judgment 𝑪 0 1)
}
}

The semantics is defined by extending the interpreter to add a case
for if-expressions, which recursively evaluates the test expression
and branches based on its value.

@codeblock-include["con/interp.rkt"]

We can confirm the interpreter computes the right result for the
examples given earlier (using @racket[parse] to state the examples
with concrete notation):

@ex[
(interp (parse '(if (zero? 0) (add1 2) 4)))
(interp (parse '(if (zero? 1) (add1 2) 4)))
(interp (parse '(if (zero? (if (zero? (sub1 1)) 1 0)) (add1 2) 4)))
(interp (parse '(if (zero? (add1 0)) (add1 2) (if (zero? (sub1 1)) 1 0))))
]


@section{An Example of Con compilation}

Suppose we want to compile @racket[(if (zero? 8) 2 3)]...

We already know how to compile the @racket[8], @racket[2], and
@racket[3] part.

What needs to happen?

@itemlist[
@item{Execute the code for @racket[8] leaving the result in @racket['rax],}
@item{check whether @racket['rax] holds zero,}
@item{if it does, execute the code for @racket[2],}
@item{if it doesn't, execute the code for @racket[3].}
]

We can determine whether @racket[8] evaluates to @racket[0] using a
comparison instruction: @racket[(Cmp rax 0)].  To do the conditional
execution, we will need to jump to different parts of the code to
either execute the code for @racket[2] or @racket[3].  There are
several ways we could accomplish this, but we take the following
approach: immediately after the comparison, do a conditional jump to
the code for the then branch when zero. Should the jump not occur,
the next instructions will carry out the evaluation of the else
branch, then (unconditionally) jump over the then branch code.

To accomplish this, we will need two new labels: one for the then
branch code and one for the end of the then branch code.  The
@racket[gensym] function can be used to generate symbols that have not
appeared before. @margin-note{Q: Why should we generate label names
here?  What would go wrong if simply used labels like @racket['l0] and
@racket['l1]?}

In total, the code for this example would look like:

@racketblock[
(let ((l0 (gensym))
      (l1 (gensym)))
  (list (Mov 'rax 8)
        (Cmp 'rax 0)
        (Je l0)
        (Mov 'rax 3)
        (Jmp l1)
        (Label l0)
        (Mov rax 2)
        (Label l1)))
]


@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
this, we arrive at the following code for the compiler:

@racketblock[
(let ((l0 (gensym 'if))
      (l1 (gensym 'if)))
  (seq (compile-e e1)
       (Cmp 'rax 0)
       (Je l0)
       (compile-e e3)
       (Jmp l1)
       (Label l0)
       (compile-e e2)
       (Label l1)))
]


This will require extending our use of a86 instructions; in
particular, we add @racket[Jmp], @racket[Je], and @racket[Cmp]
instructions.

The complete compiler code is:

@codeblock-include["con/compile.rkt"]

Let's take a look at a few examples:
@ex[
(define (show s)
  (compile-e (parse s)))
    
(show '(if (zero? 8) 2 3))
(show '(if (zero? 0) 1 2))
(show '(if (zero? 0) (if (zero? 0) 8 9) 2))
(show '(if (zero? (if (zero? 2) 1 0)) 4 5))
]

And confirm they are running as expected:
@ex[
(exec (parse '(if (zero? 8) 2 3)))
(exec (parse '(if (zero? 0) 1 2)))
(exec (parse '(if (zero? 0) (if (zero? 0) 8 9) 2)))
(exec (parse '(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 @racket[e] @math{∈} @tt{Expr},
@racket[(interp e)] equals @racket[(exec e)].}

Again, we formulate correctness as a property that can be tested:

@codeblock-include["con/correct.rkt"]

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)))
]

This compiler has continues to have the issues identified in
@secref{broken}, but appears correct in its implementation of
conditional expressions.