Assignment 3

Implement the function

val lex : string -> string list

so that lex input is the result of removing the whitespace from input and separating it into its constituent parts (formally called lexemes). These parts consist of: (, ), +, -, *, /, =, nonnegative integers (i.e. contiguous groups of digits) and variables (i.e., contiguous groups of upper-case letters), e.g.,

let _ = assert (lex "VAR = 2 + 3" = ["VAR"; "="; "2"; "+"; "3"])

The behavior of the function is undefined if the input is not a well-formed statement as described above.

Evaluation is roughly the same as in assignment 2, except that now it's possible that the given expression contains variables. We'll be using association lists to represent variable bindings that we create during a calculator interaction. An association list is a list of key-value pairs (('k * 'v) list). See the textbook chapter and the stdlib320 section for more information. For the above sample interaction the final assocation list we should get up to reordering is:

[("X", 4); ("Y", 12); ("ADDXY", 16)]

Implement the function

val eval : (string * int) list -> string list -> int

so that eval env expr is the result of evaluating an arithmetic expression expr in infix notation with variables (i.e., the right-hand side of the "=" after lexing) relative to the variable bindings in env, e.g.,

let _ = assert (eval [("X", 4); ("Y", 12)] ["X"; "+"; "Y"] = 16)

The behavior of the function is undefined if expr is not a valid arithmetic expression in infix notation with variables post-lexing.

After evaluating an expression, we'll need to add it to the variable bindings maintained by the calculator. Implement the function

val insert_uniq : 'k -> 'v -> ('k * 'v) list -> ('k * 'v) list

so that insert_uniq k v l is the result of inserting (k, v) into l. Furthermore, your implementation must maintain the invariant that a key appears at most once in the resulting list. Furthermore furthermore, your implementation must be tail recursive. Note: The order of key-value pairs does not need to be maintained in the resulting list.

let l = [("X", 4); ("Y", 12); ("ADDXY", 16)]
let _ = assert (List.assoc "X" l = 4)
let _ = assert (List.assoc "X" (insert_uniq "X" 7 l) = 7)

1. Determine a type \(\tau\) such that the following typing judgment is derivable. Also provide the derivation.

   \[ \{ \texttt{f} : \texttt{int -> bool} \} \vdash \texttt{let x = let y = 3 in y + y in f x} : \tau \]

2. Determine a type \(\tau\) such that the following typing judgment is derivable. Also provide the derivation.

   \[ \{\} \vdash \texttt{(fun x -> fun y -> y x) (fun x -> x) (fun f -> f 1)} : \tau \]

1. Determine a value \(v\) such that the following semantic judgment is derivable. Also provide the derivation.

   \[ \texttt{let x = 3 in if x = 4 then x + 1 else x + 2} \Downarrow v \]

2. Determine a value \(v\) such that the following semantic judgment is derivable. Also provide the derivation.

   \[ \texttt{let x = let y = 3 + 3 in y in x} \Downarrow v \]

One rule not included in the 320Caml specification is the typing rule for recursive let expressions, which have the following syntax:

<expr> ::= let rec <var> = <expr> in <expr>

The only difference between the let rule and the recursive let rule is that, given an expression of form:

\[ \texttt{let} \ \texttt{rec}\ f \ \texttt{=} \ e_1 \ \texttt{in} \ e_2 \]

determining the type of \(e_1\) requires that \(f\) appears in the context, since the definition of a recursive function can depend on the function itself.

Provide the typing rule for recursive let statements (we'll call it LetRec), and use this to give a derivation of the following typing judgment.¹

\[ \{\} \vdash \texttt{let rec f = fun x -> f (x + 1) = }\textcolor{red}{\texttt{false}}\texttt{ in f} : \texttt{int -> bool} \]