Due date: 9/28 @ at the beginning of class

Purpose: The goal of this problem set is to reinforce programming with metafunctions.

---

Problem 1:

Here are two language definitions for representing finite state machines:

  (define-language BASE
    (STATE string)
    (KEY "A" "B" "C" "D" "E" "F" "G" "H" "I" "J" "K" "L" "M" 
         "N" "O" "P" "Q" "R" "S" "T" "U" "V" "W" "X" "Y" "Z"
         "a" "b" "c" "d" "e" "f" "g" "h" "i" "j" "k" "l" "m"
         "n" "o" "p" "q" "r" "s" "t" "u" "v" "w" "x" "y" "z"
         "0" "1" "2" "3" "4" "5" "6" "7" "8" "9"))

  (define-extended-language FSM-L BASE
    (XFSM       (fsm ((initial STATE)) FINAL FINAL ... TRANSITION ...))
    (FINAL      (final ((label STATE))))
    (TRANSITION (transition ((current STATE) (next STATE)) ACTION ACTION ...))
    (ACTION     (action ((key KEY)))))

  (define-extended-language TOP FSM-L
    (FSM        (fsm STATE (STATE STATE ...) ((STATE (KEY KEY ...) STATE) ...))))
    

Clearly, there is a natural equivalence between the two variants -- XFSM and FSM -- of finite-state machine specifications that TOP introduces. That is, for each instance of an XFSM there is an equivalent instance of a FSM and vice versa.

Define three instances of an XFSM and construct three corresponding FSM instances.

Design the following three functions:

1. fsm-2-xfsm, which constructs an XFSM from a given FSM;
2. xfsm-2-fsm, which constructs an FSM from a given XFSM;
3. stuck?, which determines whether an FSM instance is stuck for a given STATE and KEY.

   Def.: A FSM is stuck if it does not contain a transition that originates from the current STATE and KEY.

Formulate a logical conjecture about the relationship between xfsm-2-fsm and fsm-2-xfsm via a metafunction.

Constraint Your solution must use the Redex programming language for all problems. The function may escape to the Racket programming language for simple tasks like consing an item onto a list.

Problem 2:

The simple-lang toy language is Algol-C-Java like except for types. Here is one way to add types to the abstract syntax tree representation:

 (define-language simple-lang 
    (s (x ..._n = e ..._n)
       (block d s ...))
    (e x
       n
       (+ e e)
       s)
    (d ((t x) ...))
    (n number)
    (x variable-not-otherwise-mentioned)
    (t int float))
   

Each identifier declaration in a block comes with a type specification. To keep the language simple, a type is either int or float.

Design the function type-of, which consumes a statement and produces its type. In contrast to the C programming language, simple-lang assigns non-void types to statements: (1) the type of an assignment statement is the type of the last variable on the left-hand side and (2) the type of a block statement is the type of the last statement in the block. In addition, type-of checks the following constraints:

1. the declared type of the ith variable on the left-hand side of an assignment statement is equal to the type of the ith expression on the right-hand side;
2. each statement inside of a block must have a type;
3. the type of a variable expression is the specified type of the closest variable declaration;
4. the type of a number is int if it is an exact-integer? and float otherwise;
5. the types of the two subexpression of an addition expression must be equal and the type of the addition expression is the same as the type of its two subexpressions.

These rules correspond to those of Algol, C, and Java except that the latter automatically convert int-typed expressions to float-typed expressions.

If any component of the given statement fails to satisfy one of the above constraints, type-of signals an error.

As a reminder, here is a function that looks up a type in a series of typed variable declarations:

  ;; lookup the type of a variable in a list of type declarations 
  (define-metafunction simple-lang 
    lookup : x d -> t
    [(lookup x ((t_1 x_1) ... (t x) (t_2 x_2) ...)) 
     t
     (side-condition (not (member (term x) (term (x_1 ...)))))]
    [(lookup x d)
     ,(error 'lookup "~s has no type in ~s" (term x) (term d))])

  (test-equal (term (lookup y ((int x) (float y) (int z)))) (term float))
  (with-handlers ((exn:fail? void)) (term (lookup y ())) 'bad-float)
   

Constraint Your program may escape to Racket for two reasons: (1) to determine the type of a number and (2) to signal an error.

Send in a single Racket file. Its name should consist of the two last names in alphabetical order separated with a hyphen; its suffix must be .rkt.

Your file must start with the following two lines:

  ;; NameOfPartner1, NameOfPartner2 
  ;; email@of.partner1.com, email@of.partner2.com

appropriately instantiated of course. Also separate problems with lines of the shape ";; " followed by 77 "="; for sub-problems use "-". Each gives you a width of 80 chars. Stick to this width for all of your code; if you also follow DrRacket's indentation rules, it ensures some readability.