From 05e49ba8cecbbb7276d12ac9e103fa2134552eba Mon Sep 17 00:00:00 2001 From: David Van Horn Date: Tue, 17 Sep 2019 22:10:58 -0400 Subject: [PATCH 1/4] Polishing Dupe notes. --- www/notes/dupe.scrbl | 350 ++++++++++++++++++++++++++++++++++--------- 1 file changed, 278 insertions(+), 72 deletions(-) diff --git a/www/notes/dupe.scrbl b/www/notes/dupe.scrbl index 2b5c9f7b..8563dda8 100644 --- a/www/notes/dupe.scrbl +++ b/www/notes/dupe.scrbl @@ -207,7 +207,7 @@ From a pragmatic point of view, this is a concern because it complicates testing. If the interpreter is correct and every expression has a meaning (as in all of our previous languages), it follows that the interpreter can't crash on any @tt{Expr} input. That -makes testing easy: think of an expression, run the interpeter to +makes testing easy: think of an expression, run the interpreter to compute its meaning. But now the interpreter may break if the expression is undefined. We can only safely run the interpreter on expressions that have a meaning. @@ -332,12 +332,30 @@ We can also write the inverse: ) -The interpreter operates at the level of Values. The compiler will -have to work at the level of Bits. Of course, we could, as an -intermediate step, define an interpreter that works on bits, which may -help us think about how to implement the compiler. +The interpreter operates at the level of @tt{Value}s. The compiler +will have to work at the level of @tt{Bits}. Of course, we could, +as an intermediate step, define an interpreter that works on bits, +which may help us think about how to implement the compiler. -Let's design @racket[interp-bits] by derivation. First, let's cheat: +We want a function +@#reader scribble/comment-reader +(racketblock +;; interp-bits : Expr -> Bits +) +such that +@#reader scribble/comment-reader +(racketblock +;; ∀ e : Expr . (interp-bits e) = (value->bits (interp e)) +) + +Let's design @racket[interp-bits] by derivation. This is a common +functional programming technique whereby we start from a specification +program and through a series of algebraic transformations, arrive an +correct implementation. + +First, let's state the specification of @racket[interp-bits] as a +function that ``cheats,'' it uses @racket[interp] to carry out +evaluation and then finally converts to bits. @#reader scribble/comment-reader (ex @@ -346,102 +364,290 @@ Let's design @racket[interp-bits] by derivation. First, let's cheat: (value->bits (interp e))) ) -Now let's ``push'' the @racket[value->bits] inward: +It's clearly correct with respect to the spec for @racket[interp-bits] +that we started with because @emph{the code is just the specification +itself}. + +We can even do some property-based random testing (which obviously +succeeds): + +@ex[#:no-prompt +(define (interp-bits-correct e) + (with-handlers ([exn:fail? (λ (x) 'ok)]) + (interp e) + (check-equal? (interp-bits e) + (value->bits (interp e))))) + +(define es + (for/list ([i 100]) + (random-expr))) + +(for-each interp-bits-correct es) +] + +The one wrinkle is we really only need the spec to hold when +@racket[_e] is defined according to the semantics. Since we know +@racket[interp] crashes (by raising an exception) whenever @racket[_e] +is undefined, we use an exception handler to avoid testing when +@racket[_e] is undefined. + +Now let us inline the defintion of @racket[interp]: @#reader scribble/comment-reader -(ex +(ex #:no-prompt +;; Expr -> Bits +(define (interp-bits e) + (value->bits + (match e + [(? integer? i) i] + [(? boolean? b) b] + [`(add1 ,e0) + (add1 (interp e0))] + [`(sub1 ,e0) + (sub1 (interp e0))] + [`(zero? ,e0) + (zero? (interp e0))] + [`(if ,e0 ,e1 ,e2) + (if (interp e0) + (interp e1) + (interp e2))]))) +) + +It's still correct: +@ex[ +(for-each interp-bits-correct es)] + +Now let's ``push'' the @racket[value->bits] inward by using the following equation: +@racketblock[ +(_f (match _m [_p _e] ...)) = (match _m [_p (_f _e)] ...) +] + +So we get: + +@#reader scribble/comment-reader +(ex #:no-prompt ;; Expr -> Bits (define (interp-bits e) (match e [(? integer? i) (value->bits i)] [(? boolean? b) (value->bits b)] [`(add1 ,e0) - (value->bits (add1 (bits->value (interp-bits e0))))] + (value->bits (add1 (interp- e0)))] [`(sub1 ,e0) - (value->bits (sub1 (bits->value (interp-bits e0))))] + (value->bits (sub1 (interp e0)))] [`(zero? ,e0) - (value->bits (zero? (bits->value (interp-bits e0))))] + (value->bits (zero? (interp e0)))] [`(if ,e0 ,e1 ,e2) - (if (bits->value (interp-bits e0)) - (interp-bits e1) - (interp-bits e2))])) + (value->bits + (if (interp e0) + (interp e1) + (interp e2)))])) ) -Unfolding @racket[value->bits] in the first two cases: + +Still correct: +@ex[ +(for-each interp-bits-correct es)] + +In the first two cases, we know that @racket[i] and @racket[b] are +integers and booleans, respectively. So we know @racket[(values->bits +i) = (* 2 i)] and @racket[(values->bits b) = (if b #b01 #b11)]. We can +rewrite the code as: @#reader scribble/comment-reader -(ex +(ex #:no-prompt ;; Expr -> Bits -(define (interp-bits e) - (match e - [(? integer? i) (* 2 i)] - [(? boolean? b) (if b 3 1)] - [`(add1 ,e0) - (value->bits (add1 (bits->value (interp-bits e0))))] - [`(sub1 ,e0) - (value->bits (sub1 (bits->value (interp-bits e0))))] - [`(zero? ,e0) - (value->bits (zero? (bits->value (interp-bits e0))))] - [`(if ,e0 ,e1 ,e2) - (if (bits->value (interp-bits e0)) - (interp-bits e1) - (interp-bits e2))])) + (define (interp-bits e) + (match e + [(? integer? i) (* 2 i)] + [(? boolean? b) (if b 3 1)] + [`(add1 ,e0) + (value->bits (add1 (interp e0)))] + [`(sub1 ,e0) + (value->bits (sub1 (interp e0)))] + [`(zero? ,e0) + (value->bits (zero? (interp e0)))] + [`(if ,e0 ,e1 ,e2) + (value->bits + (if (interp e0) + (interp e1) + (interp e2)))])) ) -We can simplify the conditional case as follows: +Still correct: +@ex[ +(for-each interp-bits-correct es)] + + +We can rewrite the last case by the following equation: +@racketblock[ +(_f (if _e0 _e1 _e2)) = (if _e0 (_f _e1) (_f _e2)) +] @#reader scribble/comment-reader -(ex +(ex #:no-prompt ;; Expr -> Bits -(define (interp-bits e) - (match e - [(? integer? i) (* 2 i)] - [(? boolean? b) (if b 3 1)] - [`(add1 ,e0) - (value->bits (add1 (bits->value (interp-bits e0))))] - [`(sub1 ,e0) - (value->bits (sub1 (bits->value (interp-bits e0))))] - [`(zero? ,e0) - (value->bits (zero? (bits->value (interp-bits e0))))] - [`(if ,e0 ,e1 ,e2) - (match (interp-bits e0) - [1 (interp-bits e2)] - [_ (interp-bits e1)])])) + (define (interp-bits e) + (match e + [(? integer? i) (* 2 i)] + [(? boolean? b) (if b 3 1)] + [`(add1 ,e0) + (value->bits (add1 (interp e0)))] + [`(sub1 ,e0) + (value->bits (sub1 (interp e0)))] + [`(zero? ,e0) + (value->bits (zero? (interp e0)))] + [`(if ,e0 ,e1 ,e2) + (if (interp e0) + (value->bits (interp e1)) + (value->bits (interp e2)))])) ) -We can also push around the @racket[add1], @racket[sub1], and -@racket[zero?] operations to avoid the conversions. Note that -whenever @racket[_bs] are bits representing an integer, then +Still correct: +@ex[ +(for-each interp-bits-correct es)] + + +Let's now re-write by the following equations: + +@racketblock[ +(add1 _e) = (+ _e 1) +(sub1 _e) = (- _e 1) +(f (+ _e0 _e1)) = (+ (f _e0) (f _e1)) +(f (- _e0 _e1)) = (- (f _e0) (f _e1)) +] + +to get: + +@#reader scribble/comment-reader +(ex #:no-prompt +;; Expr -> Bits + (define (interp-bits e) + (match e + [(? integer? i) (* 2 i)] + [(? boolean? b) (if b 3 1)] + [`(add1 ,e0) + (+ (value->bits (interp e0)) (value->bits 1))] + [`(sub1 ,e0) + (- (value->bits (interp e0)) (value->bits 1))] + [`(zero? ,e0) + (value->bits (zero? (interp e0)))] + [`(if ,e0 ,e1 ,e2) + (if (interp e0) + (value->bits (interp e1)) + (value->bits (interp e2)))])) +) + +Still correct: +@ex[ +(for-each interp-bits-correct es)] + +By computation, @racket[(value->bits 1) = 2]. + +We can now rewrite by the equation of our specification: + +@racketblock[ +(value->bits (interp _e)) = (interp-bits _e)] + + +@#reader scribble/comment-reader +(ex #:no-prompt +;; Expr -> Bits + (define (interp-bits e) + (match e + [(? integer? i) (* 2 i)] + [(? boolean? b) (if b 3 1)] + [`(add1 ,e0) + (+ (interp-bits e0) 2)] + [`(sub1 ,e0) + (- (interp-bits e0) 2)] + [`(zero? ,e0) + (value->bits (zero? (interp e0)))] + [`(if ,e0 ,e1 ,e2) + (if (interp e0) + (interp-bits e1) + (interp-bits e2))])) +) + +Still correct: +@ex[ +(for-each interp-bits-correct es)] + +We can rewrite by the equation +@racketblock[(zero? (interp _e0)) = (zero? (interp-bits _e0))] +and inline @racket[value->bits] specialized to a boolean argument: + +@#reader scribble/comment-reader +(ex #:no-prompt +;; Expr -> Bits + (define (interp-bits e) + (match e + [(? integer? i) (* 2 i)] + [(? boolean? b) (if b 3 1)] + [`(add1 ,e0) + (+ (interp-bits e0) 2)] + [`(sub1 ,e0) + (- (interp-bits e0) 2)] + [`(zero? ,e0) + (match (zero? (interp-bits e0)) + [#t #b11] + [#f #b01])] + [`(if ,e0 ,e1 ,e2) + (if (interp e0) + (interp-bits e1) + (interp-bits e2))])) + ) + +Still correct: +@ex[ +(for-each interp-bits-correct es)] + +Finally, in the last case, all that matters in @racket[(if (interp e0) +...)] is whether @racket[(interp e0)] returns @racket[#f] or something +else. So we can rewrite in terms of whether @racket[(interp-bits e0)] +produces the representation of @racket[#f] (@code[#:lang +"racket"]{#b01}): + +@#reader scribble/comment-reader +(ex #:no-prompt +;; Expr -> Bits + (define (interp-bits e) + (match e + [(? integer? i) (* 2 i)] + [(? boolean? b) (if b 3 1)] + [`(add1 ,e0) + (+ (interp-bits e0) 2)] + [`(sub1 ,e0) + (- (interp-bits e0) 2)] + [`(zero? ,e0) + (match (zero? (interp-bits e0)) + [#t #b11] + [#f #b01])] + [`(if ,e0 ,e1 ,e2) + (match (interp-bits e0) + [#b01 (interp-bits e2)] + [_ (interp-bits e1)])])) + ) + + +Still correct: +@ex[ +(for-each interp-bits-correct es)] + + +Note that whenever @racket[_bs] are bits representing an integer, then @racket[(value->bits (add1 (bits->value _bs)))] is equal to @racket[(+ _bs 2)], i.e. adding @code[#:lang "racket"]{#b10}. When @racket[_bs] represents a boolean, then @racket[(value->bits (add1 (bits->value _bs)))] would crash, while @racket[(+ _bs 2)] doesn't, but this is an undefined program, so changing the behavior is fine. -We do something similar for @racket[sub1] and arrive at: - -@#reader scribble/comment-reader -(ex -;; Expr -> Bits -(define (interp-bits e) - (match e - [(? integer? i) (* 2 i)] - [(? boolean? b) (if b 3 1)] - [`(add1 ,e0) - (+ (interp-bits e0) 2)] - [`(sub1 ,e0) - (- (interp-bits e0) 2)] - [`(zero? ,e0) - (match (interp-bits e0) - [0 #b11] - [_ #b01])] - [`(if ,e0 ,e1 ,e2) - (match (interp-bits e0) - [#b01 (interp-bits e2)] ; if #f, interp e2 - [_ (interp-bits e1)])])) -) +Looking back: starting from the spec, we've arrived at a definition of +@racket[interp-bits] that is completely self-contained: it doesn't use +@racket[interp] at all. It also only uses the @tt{Bits} +representation and does no conversions to or from @tt{Value}s. -And we can recover the original interpreter by wrapping the bit +We can recover the original interpreter by wrapping the bit interpreter in a final conversion: @#reader scribble/comment-reader From e8f76d556836dece31c9934788dc1d15b2190925 Mon Sep 17 00:00:00 2001 From: David Van Horn Date: Thu, 19 Sep 2019 08:14:11 -0400 Subject: [PATCH 2/4] Assignment 4. --- www/assignments.scrbl | 2 +- www/assignments/4.scrbl | 354 ++++++++++++++++++++++++++++++++++++++++ www/schedule.scrbl | 2 +- 3 files changed, 356 insertions(+), 2 deletions(-) create mode 100644 www/assignments/4.scrbl diff --git a/www/assignments.scrbl b/www/assignments.scrbl index 0803d638..bc04e236 100644 --- a/www/assignments.scrbl +++ b/www/assignments.scrbl @@ -6,4 +6,4 @@ @include-section{assignments/1.scrbl} @include-section{assignments/2.scrbl} @include-section{assignments/3.scrbl} - +@include-section{assignments/4.scrbl} diff --git a/www/assignments/4.scrbl b/www/assignments/4.scrbl new file mode 100644 index 00000000..335c0e42 --- /dev/null +++ b/www/assignments/4.scrbl @@ -0,0 +1,354 @@ +#lang scribble/manual +@title[#:tag "Assignment 4" #:style 'unnumbered]{Assignment 4: Let there be Variables, Characters} + +@(require (for-label (except-in racket ...))) +@(require "../notes/fraud-plus/semantics.rkt") +@(require redex/pict) + +@(require "../notes/ev.rkt") + +@bold{Due: Thurs, Sept 26, 11:59PM} + +@(define repo "https://classroom.github.com/a/HuBPd1o9") + +The goal of this assignment is to extend a compiler with binding forms +and a character data type. + +Assignment repository: +@centered{@link[repo repo]} + +You are given a repository with a starter compiler similar to the +@seclink["Fraud"]{Fraud} language we studied in class. You are tasked +with: + +@itemlist[ + +@item{incorporating the Con+ features you added in +@seclink["Assignment 3"]{Assignment 3},} + +@item{extending the language to include a character data type,} + +@item{extending the @racket[let]-binding form of the language to bind +any number of variables, and} + +@item{updating the parser to work for Fraud+.} + +] + +@section[#:tag-prefix "a4-" #:style 'unnumbered]{From Con+ to Fraud+} + +Implement the @racket[abs] and unary @racket[-] operations and the +@racket[cond] form from @seclink["Assignment 3"]{Con+}. You can start +from your previous code, but you will need to update it to work for +Fraud+. + +In particular, functions should signal an error when applied to the +wrong type of argument and your @racket[cond] form should work with +@emph{arbitrary} question expressions. In other words, @racket[cond] +should work like @racket[if] in @seclink["Dupe"]{Dupe}. + +The formal semantics of @racket[cond] are defined as: + +@(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 1) +@(show-judgment 𝑭-𝒆𝒏𝒗 1 2) +@(show-judgment 𝑭-𝒆𝒏𝒗 2 3) + + +The following files have already been updated for you: +@itemlist[ +@item{@tt{ast.rkt}} +@item{@tt{syntax.rkt}} +@item{@tt{interp.rkt}} +] + +You will need to modify @tt{compile.rkt} to correctly implement these +features. + + +@section[#:tag-prefix "a4-" #:style 'unnumbered]{Adding a Bit of Character} + +Racket has a Character data type for representing single letters. A +Racket character can represent any of the 1,114,112 Unicode +@link["http://unicode.org/glossary/#code_point"]{code points}. + +The way a character is most often written is an octothorp, followed by +a backslash, followed by the character itself. So for example the +character @tt{a} is written @racket[#\a]. The character @tt{λ} is +written @racket[#\λ]. The character @tt{文} is written @racket[#\文]. + +A character can be converted to an integer and @emph{vice versa}: + +@ex[ +(char->integer #\a) +(char->integer #\λ) +(char->integer #\文) +(integer->char 97) +(integer->char 955) +(integer->char 25991) +] + +However, integers in the range of valid code points are acceptable to +@racket[integer->char] and using any other integer will produce an +error: + +@ex[ +(eval:error (integer->char -1)) +(eval:error (integer->char 55296)) +] + +There are a few other ways to write characters (see the Racket +@link["https://docs.racket-lang.org/reference/reader.html#%28part._parse-character%29"]{Reference} +for the details), but you don't have to worry much about this since +the lexer takes care of reading characters in all their different +forms and the run-time system given to you takes care of printing +them. + +Your job is extend the compiler to handle the compilation of +characters and implement the operations @racket[integer->char], +@racket[char->integer], and @racket[char?]. The operations should +work as in Racket and should signal an error (i.e. @racket['err]) +whenever Racket produces an error. While you're at it, implement +the predicates @racket[integer?] and @racket[boolean?], too. + +The following files have already been updated for you: + +@itemlist[ + +@item{@tt{ast.rkt}} + +@item{@tt{syntax.rkt}} + +@item{@tt{interp.rkt}} + +@item{@tt{main.c}} + +] + +You will need to modify @tt{compile.rkt} to correctly implement these +features. Note that you must use the same representation of +characters as used in the run-time system and should not change +@tt{main.c}. + +@section[#:tag-prefix "a4-" #:style 'unnumbererd]{Generalizing Let} + +The Fraud language has a let form that binds a single variable in the +scope of some expression. This is a restriction of the more general +form of @racket[let] that binds any number of expressions. So for +example, + +@racketblock[ +(let ((x 1) (y 2) (z 3)) + _e) +] + +simultaneously binds @racket[x], @racket[y], and @racket[z] in the +scope of @racket[_e]. + +The syntax of a @racket[let] expression allows any number of binders +to occur, so @racket[(let () _e)] is valid syntax and is equivalent to +@racket[_e]. + +The binding of each variable is only in scope in the body, @bold{not} +in the right-hand-sides of any of the @racket[let]. + +For example, @racketblock[(let ((x 1) (y x)) 0)] is a syntax error +because the occurrence of @racket[x] is not bound. + +The following files have already been updated for you: + +@itemlist[ + +@item{@tt{ast.rkt}} + +@item{@tt{interp.rkt}} + +] + +Update @tt{syntax.rkt} to define two functions: + +@itemize[ + +@item{@code[#:lang "racket"]{expr? ; Any -> Boolean}, which consumes +anything and determines if it is a well-formed expression, i.e. it +must be an instance of an @tt{Expr} @emph{and} each @racket[let] +expression must bind a distinct set of variables.} + +@item{@code[#:lang "racket"]{closed? ; Expr -> Boolean}, which consumes +an @tt{Expr} and determines if it is closed, i.e. every variable +occurrence is bound.} + +] + +Update @tt{compile.rkt} to correctly compile the generalized form of +@racket[let]. The compiler may assume the input is a closed +expression. + +@section[#:tag-prefix "a4-" #:style 'unnumbered]{Extending your Parser} + + +Extend your Con+ parser for the Fraud+ language based on the following +grammar: + +@verbatim{ + ::= integer + | character + | variable + | ( ) + | [ ] + + ::= + | if + | cond * + | let + + ::= add1 | sub1 | abs | - | zero? | integer->char | char->integer + | char? | integer? | boolean? + + ::= ( ) + | [ ] + + ::= ( else ) + | [ else ] + + ::= ( * ) + | [ * ] + + ::= ( variable ) + | [ variable ] +} + +There is a lexer given to you in @tt{lex.rkt}, which provides two +functions: @racket[lex-string] and @racket[lex-port], which consume a +string or an input port, respectively, and produce a list of tokens, +which are defined as follows: + +@margin-note{Note that the @tt{Token} type has changed slightly from +@secref{Assignment 3}: @racket['add1] is now @racket['(prim add1)], +@racket['cond] is now @racket['(keyword cond)], etc.} + +@#reader scribble/comment-reader +(racketblock +;; type Token = +;; | Integer +;; | Char +;; | Boolean +;; | `(variable ,Variable) +;; | `(keyword ,Keyword) +;; | `(prim ,Prim) +;; | 'lparen ;; ( +;; | 'rparen ;; ) +;; | 'lsquare ;; [ +;; | 'rsquare ;; ] +;; | 'eof ;; end of file + +;; type Variable = Symbol (other than 'let, 'cond, etc.) + +;; type Keyword = +;; | 'let +;; | 'cond +;; | 'else +;; | 'if + +;; type Prim = +;; | 'add1 +;; | 'sub1 +;; | 'zero? +;; | 'abs +;; | '- +;; | 'integer->char +;; | 'char->integer +;; | 'char? +;; | 'boolean? +;; | 'integer? +) + +The lexer will take care of reading the @tt{#lang racket} header and +remove any whitespace. + +You must complete the code in @tt{parse.rkt} to implement the parser +which constructs an s-expression representing a valid Fraud+ +expression, if possible, from a list of tokens. The @racket[parse] +function should have the following signature and must be provided by +the module: + +@#reader scribble/comment-reader +(racketblock +;; parse : [Listof Token] -> Expr +) + +As an example, @racket[parse] should produce @racket['(add1 (sub1 7))] +if given + +@racketblock['(lparen (prim add1) lparen (prim sub1) 7 rparen rparen eof)] + + +You should not need to make any changes to @tt{lex.rkt}. + +The given @tt{interp-file.rkt} and @tt{compile-file.rkt} code no +longer use @racket[read], but instead use the parser. This means you +neither will work until the parser is complete. + + +@bold{The code you are given includes two(!) implementations of the +Con+ parser.} One implementation follows the imperative approach; the +other follows the functional approach. + +You may extend either, or you may throw out the given code and start +from the code you wrote previously. + + +@section[#:tag-prefix "a4-" #:style 'unnumbered]{Testing} + +You can test your code in several ways: + +@itemlist[ + + @item{Using the command line @tt{raco test .} from + the directory containing the repository to test everything.} + + @item{Using the command line @tt{raco test } to + test only @tt{}.} + + @item{Pushing to github. You can + see test reports at: + @centered{@link["https://travis-ci.com/cmsc430/"]{ + https://travis-ci.com/cmsc430/}} + + (You will need to be signed in in order see results for your private repo.)}] + +Note that only a small number of tests are given to you, so you should +write additional test cases. + +@bold{We have removed @tt{random.rkt}} and instead provide a +@tt{random-exprs.rkt} module which provides @racket[exprs], a list +of 500 closed expressions. It is used in the +@tt{test/compile-rand.rkt} file to randomly test compiler correctness. +This should help speed up the testing process since the random +generation is slow. + +@section[#:tag-prefix "a4-" #:style 'unnumbered]{Submitting} + +Pushing your local repository to github ``submits'' your work. We +will grade the latest submission that occurs before the deadline. + diff --git a/www/schedule.scrbl b/www/schedule.scrbl index a3fa0b56..d600e18e 100644 --- a/www/schedule.scrbl +++ b/www/schedule.scrbl @@ -34,7 +34,7 @@ @secref["Fraud"]) (list @wk{9/24} - "A4" @;seclink["Assignment 4"]{A4} + @seclink["Assignment 4"]{A4} @secref["Grift"] @secref["Hustle"]) From a587d3e26fde688450a03271449428513479a962 Mon Sep 17 00:00:00 2001 From: David Van Horn Date: Thu, 19 Sep 2019 08:14:22 -0400 Subject: [PATCH 3/4] Add missing token. --- www/assignments/3.scrbl | 1 + 1 file changed, 1 insertion(+) diff --git a/www/assignments/3.scrbl b/www/assignments/3.scrbl index c3174492..314c58ef 100644 --- a/www/assignments/3.scrbl +++ b/www/assignments/3.scrbl @@ -173,6 +173,7 @@ which are defined as: ;; | 'add1 ;; | 'sub1 ;; | 'zero? +;; | 'if ;; | 'cond ;; | 'else ;; | 'abs From d6920e23e058028029b1fc55276d2f5dc01c95d9 Mon Sep 17 00:00:00 2001 From: David Van Horn Date: Thu, 19 Sep 2019 08:18:44 -0400 Subject: [PATCH 4/4] Add missing Fraud+ semantics. --- www/notes/fraud-plus/semantics.rkt | 57 ++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 www/notes/fraud-plus/semantics.rkt diff --git a/www/notes/fraud-plus/semantics.rkt b/www/notes/fraud-plus/semantics.rkt new file mode 100644 index 00000000..e96186bb --- /dev/null +++ b/www/notes/fraud-plus/semantics.rkt @@ -0,0 +1,57 @@ +#lang racket +(provide F 𝑭-𝒆𝒏𝒗) + +(require redex/reduction-semantics + (rename-in (only-in "../fraud/semantics.rkt" F 𝑭-𝒆𝒏𝒗) [F F-] [𝑭-𝒆𝒏𝒗 𝑭--𝒆𝒏𝒗])) + +; for use in presentations (informally noting x can't be let, etc.) +(define-extended-language F F- + (e ::= .... (cond [e_p0 e_a0] ... [else e_an]))) + + +(define-extended-judgment-form F 𝑭--𝒆𝒏𝒗 + #:contract (𝑭-𝒆𝒏𝒗 e r a) + #:mode (𝑭-𝒆𝒏𝒗 I I O) + + [(𝑭-𝒆𝒏𝒗 e_p0 r v_p0) ... (is-false v_p0) ... (𝑭-𝒆𝒏𝒗 e_pk r v) (is-true v) (𝑭-𝒆𝒏𝒗 e_ak r a) + -------- + (𝑭-𝒆𝒏𝒗 (cond [e_p0 e_a0] ... [e_pk e_ak] [e_pk+1 e_ak+1] ... [else e_an]) r a)] + + [(𝑭-𝒆𝒏𝒗 e_p0 r v_p0) ... (is-false v_p0) ... (𝑭-𝒆𝒏𝒗 e_an r a) + -------- + (𝑭-𝒆𝒏𝒗 (cond [e_p0 e_a0] ... [else e_an]) r a)] + + [(𝑭-𝒆𝒏𝒗 e_p0 r v_p0) ... (is-false v_p0) ... (𝑭-𝒆𝒏𝒗 e_pk r err) + -------- + (𝑭-𝒆𝒏𝒗 (cond [e_p0 e_a0] ... [e_pk e_ak] [e_pk+1 e_ak+1] ... [else e_an]) r err)] + +#| + + [(𝑭-𝒆𝒏𝒗 e_0 r v_0) (𝑭-𝒆𝒏𝒗 e_1 (ext r x v_0) a) + ----- "let" + (𝑭-𝒆𝒏𝒗 (let ((x e_0)) e_1) r a)] + + [(𝑭-𝒆𝒏𝒗 e_0 r err) + ----------- "let-err" + (𝑭-𝒆𝒏𝒗 (let ((x e_0)) e_1) r err)] + + ;; Primitive application + [(𝑭-𝒆𝒏𝒗 e_0 r a_0) + ----------- "prim" + (𝑭-𝒆𝒏𝒗 (p e_0) r (𝑭-𝒑𝒓𝒊𝒎 (p a_0)))]) + |# + ) + +(define-judgment-form F + #:mode (is-true I) + #:contract (is-true v) + [---- + (is-true #t)] + [----- + (is-true i)]) + +(define-judgment-form F + #:mode (is-false I) + #:contract (is-false v) + [---- + (is-false #f)])