diff --git a/hw2/hs/WhileInterp.hs b/hw2/hs/WhileInterp.hs new file mode 100644 index 0000000..271de6c --- /dev/null +++ b/hw2/hs/WhileInterp.hs @@ -0,0 +1,80 @@ +{- + Name: + Class: CS 252 + Assigment: HW2 + Date: + Description: +-} + + +module WhileInterp ( + Expression(..), + Binop(..), + Value(..), + testProgram, + run +) where + +import Data.Map (Map) +import qualified Data.Map as Map + +-- We represent variables as strings. +type Variable = String + +-- The store is an associative map from variables to values. +-- (The store roughly corresponds with the heap in a language like Java). +type Store = Map Variable Value + +data Expression = + Var Variable -- x + | Val Value -- v + | Assign Variable Expression -- x := e + | Sequence Expression Expression -- e1; e2 + | Op Binop Expression Expression + | If Expression Expression Expression -- if e1 then e2 else e3 + | While Expression Expression -- while (e1) e2 + deriving (Show) + +data Binop = + Plus -- + :: Int -> Int -> Int + | Minus -- - :: Int -> Int -> Int + | Times -- * :: Int -> Int -> Int + | Divide -- / :: Int -> Int -> Int + | Gt -- > :: Int -> Int -> Bool + | Ge -- >= :: Int -> Int -> Bool + | Lt -- < :: Int -> Int -> Bool + | Le -- <= :: Int -> Int -> Bool + deriving (Show) + +data Value = + IntVal Int + | BoolVal Bool + deriving (Show) + + +-- This function will be useful for defining binary operations. +-- The first case is done for you. +-- Be sure to explicitly check for a divide by 0 and throw an error. +applyOp :: Binop -> Value -> Value -> Value +applyOp Plus (IntVal i) (IntVal j) = IntVal $ i + j +applyOp _ _ _ = error "TBD" + + +-- Implement this function according to the specified semantics +evaluate :: Expression -> Store -> (Value, Store) +evaluate (Op o e1 e2) s = + let (v1,s1) = evaluate e1 s + (v2,s') = evaluate e2 s1 + in (applyOp o v1 v2, s') +evaluate _ _ = error "TBD" + + +-- Evaluates a program with an initially empty state +run :: Expression -> (Value, Store) +run prog = evaluate prog Map.empty + +-- The same as run, but only returns the Store +testProgram :: Expression -> Store +testProgram prog = snd $ run prog + + diff --git a/hw2/hs/mapExample.hs b/hw2/hs/mapExample.hs new file mode 100644 index 0000000..00f02d2 --- /dev/null +++ b/hw2/hs/mapExample.hs @@ -0,0 +1,12 @@ +import Data.Map (Map) +import qualified Data.Map as Map + +m = Map.empty + +m' = Map.insert "a" 42 m + +main = do + case (Map.lookup "a" m') of + Just i -> putStrLn $ show i + _ -> error "Key is not in the map" + diff --git a/hw2/hs/test.hs b/hw2/hs/test.hs new file mode 100644 index 0000000..3d3e3ca --- /dev/null +++ b/hw2/hs/test.hs @@ -0,0 +1,36 @@ +import WhileInterp + +-- Here are a few tests that you can use to check your implementation. +w_test = (Sequence (Assign "X" (Op Plus (Op Minus (Op Plus (Val (IntVal 1)) (Val (IntVal 2))) (Val (IntVal 3))) (Op Plus (Val (IntVal 1)) (Val (IntVal 3))))) (Sequence (Assign "Y" (Val (IntVal 0))) (While (Op Gt (Var "X") (Val (IntVal 0))) (Sequence (Assign "Y" (Op Plus (Var "Y") (Var "X"))) (Assign "X" (Op Minus (Var "X") (Val (IntVal 1)))))))) + +w_fact = (Sequence (Assign "N" (Val (IntVal 2))) (Sequence (Assign "F" (Val (IntVal 1))) (While (Op Gt (Var "N") (Val (IntVal 0))) (Sequence (Assign "X" (Var "N")) (Sequence (Assign "Z" (Var "F")) (Sequence (While (Op Gt (Var "X") (Val (IntVal 1))) (Sequence (Assign "F" (Op Plus (Var "Z") (Var "F"))) (Assign "X" (Op Minus (Var "X") (Val (IntVal 1)))))) (Assign "N" (Op Minus (Var "N") (Val (IntVal 1)))))))))) + +testUnit :: IO () +testUnit = do + -- Should be: (IntVal 1,fromList []) + putStrLn $ show $ WhileInterp.run (Val (IntVal 1)) + -- Should be: (BoolVal True,fromList [("X",BoolVal True)]) + putStrLn $ show $ WhileInterp.run (Assign "X" (Val (BoolVal True))) + -- Should be: (IntVal 2,fromList []) + putStrLn $ show $ WhileInterp.run (Sequence (Val (IntVal 1)) (Val (IntVal 2))) + -- Should be: (IntVal 11,fromList []) + putStrLn $ show $ WhileInterp.run (Op Plus (Val (IntVal 9)) (Val (IntVal 2))) + -- Should be: (IntVal 1,fromList []) + putStrLn $ show $ WhileInterp.run (If (Val (BoolVal True)) (Val (IntVal 1)) (Val (IntVal 2))) + -- Should be: (IntVal 2,fromList []) + putStrLn $ show $ WhileInterp.run (If (Val (BoolVal False)) (Val (IntVal 1)) (Val (IntVal 2))) + -- Should be: (BoolVal False,fromList []) + putStrLn $ show $ WhileInterp.run (While (Val (BoolVal False)) (Val (IntVal 42))) + -- Should be: (IntVal 666,fromList [("X",IntVal 666)]) + putStrLn $ show $ WhileInterp.run (Sequence + (Assign "X" (Val (IntVal 666))) + (Var "X")) + +main :: IO () +main = do + testUnit + -- Should be: fromList [("X",IntVal 0),("Y",IntVal 10)] + putStrLn $ show $ WhileInterp.testProgram w_test + -- Should be: fromList [("F",IntVal 2),("N",IntVal 0),("X",IntVal 1),("Z",IntVal 2)] + putStrLn $ show $ WhileInterp.testProgram w_fact + diff --git a/hw2/while-semantics.pdf b/hw2/while-semantics.pdf new file mode 100644 index 0000000..ae02da6 Binary files /dev/null and b/hw2/while-semantics.pdf differ diff --git a/hw2/while-semantics.tex b/hw2/while-semantics.tex new file mode 100644 index 0000000..71038ba --- /dev/null +++ b/hw2/while-semantics.tex @@ -0,0 +1,292 @@ +\documentclass{article} + +\usepackage{fullpage} +\usepackage{listings} +\usepackage{amsmath} +\usepackage{amsthm} +\usepackage{amssymb} +%\usepackagen{url} +\usepackage{float} +\usepackage{paralist} + +\floatstyle{boxed} +\restylefloat{figure} + + + +\newcommand{\rel}[1]{ \mbox{\sc [#1]} } + +\title{Homework 2: Operational Semantics for WHILE} + +\author{ + CS 252: Advanced Programming Languages \\ + Prof. Thomas H. Austin \\ + San Jos\'{e} State University \\ + } +\date{} + +\begin{document} +\maketitle + +\section{Introduction} + +For this assignment, +you will implement the semantics for a small imperative language, named WHILE. + +% Commands for formatting figure +\newcommand{\mydefhead}[2]{\multicolumn{2}{l}{{#1}}&\mbox{\emph{#2}}\\} +\newcommand{\mydefcase}[2]{\qquad\qquad& #1 &\mbox{#2}\\} + +% Commands for language format +\newcommand{\assign}[2]{#1~{:=}~#2} +\newcommand{\ife}[3]{\mbox{\tt if}~{#1}~\mbox{\tt then}~{#2}~\mbox{\tt else}~{#3}} +\newcommand{\whilee}[2]{\mbox{\tt while}~(#1)~#2} +\newcommand{\true}{\mbox{\tt true}} +\newcommand{\false}{\mbox{\tt false}} + +\begin{figure}\label{fig:lang} +\caption{The WHILE language} +\[ +\begin{array}{llr} + \mydefhead{e ::=\qquad\qquad\qquad\qquad}{Expressions} + \mydefcase{x}{variables/addresses} + \mydefcase{v}{values} + \mydefcase{\assign x e}{assignment} + \mydefcase{e; e}{sequential expressions} + \mydefcase{e ~op~ e}{binary operations} + \mydefcase{\ife e e e}{conditional expressions} + \mydefcase{\whilee e e}{while expressions} + \\ + \mydefhead{v ::=\qquad\qquad\qquad\qquad}{Values} + \mydefcase{i}{integer values} + \mydefcase{b}{boolean values} + \\ + op ::= & + ~|~ - ~|~ * ~|~ / ~|~ > ~|~ >= ~|~ < ~|~ <= & \mbox{\emph{Binary operators}} \\ +\end{array} +\] +\end{figure} + +The language for WHILE is given in Figure~\ref{fig:lang}. +Unlike the Bool* language we discussed previously, +WHILE supports \emph{mutable references}. +The state of these references is maintained in a \emph{store}, +a mapping of references to values. +(``Store'' can be thought of as a synonym for heap.) +Once we have mutable references, other language constructs become more useful, +such as sequencing operations ($e_1;e_2$). + + + +%--------- +\section{Small-step semantics} + +\newcommand{\ssrule}[3]{ + \rel{#1} & + \frac{\strut\begin{array}{@{}c@{}} #2 \end{array}} + {\strut\begin{array}{@{}c@{}} #3 \end{array}} + \\~\\ +} +%\newcommand{\sstep}[4]{\ctxt[{#1}],{#2} \rightarrow \ctxt[{#3}],{#4}} +%\newcommand{\sstepraw}[4]{{#1},{#2} \rightarrow {#3},{#4}} +\newcommand{\sstep}[4]{{#1},{#2} \rightarrow {#3},{#4}} +\newcommand{\ctxt}{C} + +The small-step semantics for WHILE are given in Figure~\ref{fig:smallstep}. +%For the sake of brevity, these rules use \emph{evaluation contexts} ($\ctxt$), +%which specify which \emph{redex} will be evaluated next. +%The evaluation rules then apply to the ``hole'' ($\bullet$) in this context. +% +Most of these rules are fairly straightforward, but there are a couple of points +to note with the $\rel{ss-while}$ rule. +First of all, this is the only rule that makes a more complex expression +when it has finished. +(This rule is much cleaner when specified with the big-step operational semantics.) + +Secondly, note the final value of this expression once the while loop completes. +It will \emph{always} be {\false} when it completes. +We could have created a special value, such as {\tt null}, +or we could have made the while loop a statement that returns no value. +Both choices, however, would complicate our language needlessly. + + +%-------------- +\section{YOUR ASSIGNMENT} +\newcommand{\bstep}[4]{{#1},{#2} \Downarrow {#3},{#4}} + +\noindent +{\bf Part 1:} +Rewrite the operational semantic rules for WHILE in \LaTeX\ +to use big-step operational semantics instead. +Submit both your \LaTeX\ source and the generated PDF file. + +Extend your semantics with features to handle boolean values. +{\bf Do not treat these a binary operators.} +Specifically, add support for: +\begin{compactitem} + \item {\tt and} + \item {\tt or} + \item {\tt not} +\end{compactitem} + +The exact behavior of these new features is up to you, +but should seem reasonable to most programmers. + +\bigskip +\noindent +{\bf Part 2:} +Once you have your semantics defined, +download {\tt WhileInterp.hs} and implement the {\tt evaluate} function, +as well as any additional functions you need. +Your implementation must be consistent with your operational semantics, +{\it including your extensions for {\tt and}, {\tt or}, and {\tt not}}. +Also, you may not change any type signatures provided in the file. + +Finally, implement the interpreter to match your semantics. + +\bigskip +\noindent +{\bf Zip all files together into {\tt hw2.zip} and submit to Canvas.} + + + + + +%\begin{figure}[H]\label{fig:smallstep} +%\caption{Small-step semantics for WHILE} +%{\bf Runtime Syntax:} +%\[ +%\begin{array}{rclcl} +% \ctxt & \in & {Context} \quad & ::= & \quad \ctxt; e +% ~|~ \ctxt ~op~ e +% ~|~ v ~op~ \ctxt +% ~|~ \assign{x}{\ctxt} +% ~|~ \ife{\ctxt}{e_1}{e_2} +% ~|~ \bullet \\ +% \sigma & \in & {Store} \quad & = & \quad {variable} ~\rightarrow ~v \\ +% \\ +%\end{array} +%\] +%{\bf Evaluation Rules:~~~ \fbox{$\sstepraw{e}{\sigma}{e'}{\sigma'}$}} \\ +%\[ +%\begin{array}{cc} +%\begin{array}{r@{\qquad}l} +%\ssrule{ss-var}{ +% x \in domain(\sigma) \qquad \sigma(x)=v +%}{ +% \sstep{x}{\sigma}{v}{\sigma} +%} +%\ssrule{ss-assign}{ +%}{ +% \sstep{\assign{x}{v}}{\sigma}{v}{\sigma[x:=v]} +%} +%\ssrule{ss-op}{ +% v = v_1 ~op~ v_2 +%}{ +% \sstep{v_1~op~v_2}{\sigma}{v}{\sigma} +%} +%\end{array} +% & +%\begin{array}{r@{\qquad}l} +%\ssrule{ss-seq}{ +%}{ +% \sstep{v;e}{\sigma}{e}{\sigma} +%} +%\ssrule{ss-iftrue}{ +%}{ +% \sstep{\ife{\true}{e_1}{e_2}}{\sigma}{e_1}{\sigma} +%} +%\ssrule{ss-iffalse}{ +%}{ +% \sstep{\ife{\false}{e_1}{e_2}}{\sigma}{e_2}{\sigma} +%} +%\ssrule{ss-while}{ +%}{ +% \sstep{\whilee{e_1}{e_2}}{\sigma}{\ife{e_1}{e_2;\whilee{e_1}{e_2}}{\false}}{\sigma} +%} +%\end{array} +%\end{array} +%\] +%\end{figure} +% + +\begin{figure}[H]\label{fig:smallstep} +\caption{Small-step semantics for WHILE} +{\bf Runtime Syntax:} +\[ +\begin{array}{rclcl} + \sigma & \in & {Store} \quad & = & \quad {variable} ~\rightarrow ~v \\ + \\ +\end{array} +\] +{\bf Evaluation Rules:~~~ \fbox{$\sstep{e}{\sigma}{e'}{\sigma'}$}} \\ +\[ +%\begin{array}{cc} +\begin{array}{r@{\qquad}l} +\ssrule{ss-seqctx}{ + \sstep{e_1}{\sigma}{e_1'}{\sigma'} +}{ + \sstep{e_1;e_2}{\sigma}{e_1';e_2}{\sigma'} +} +\ssrule{ss-seq}{ +}{ + \sstep{v;e}{\sigma}{e}{\sigma} +} +\ssrule{ss-opctx1}{ + \sstep{e_1}{\sigma}{e_1'}{\sigma'} +}{ + \sstep{e_1~op~e_2}{\sigma}{e_1'~op~e_2}{\sigma'} +} +\ssrule{ss-opctx2}{ + \sstep{e_2}{\sigma}{e_2'}{\sigma'} +}{ + \sstep{v_1~op~e_2}{\sigma}{v_1~op~e_2'}{\sigma'} +} +\ssrule{ss-op}{ + v = v_1 ~op~ v_2 +}{ + \sstep{v_1~op~v_2}{\sigma}{v}{\sigma} +} +\end{array} +\begin{array}{r@{\qquad}l} +\ssrule{ss-var}{ + x \in domain(\sigma) \qquad \sigma(x)=v +}{ + \sstep{x}{\sigma}{v}{\sigma} +} +\ssrule{ss-assignctx}{ + \sstep{e_1}{\sigma}{e_1'}{\sigma'} +}{ + \sstep{\assign{x}{e}}{\sigma}{\assign{x}{e'}}{\sigma'} +} +\ssrule{ss-assign}{ +}{ + \sstep{\assign{x}{v}}{\sigma}{v}{\sigma[x:=v]} +} +\ssrule{ss-iftrue}{ +}{ + \sstep{\ife{\true}{e_1}{e_2}}{\sigma}{e_1}{\sigma} +} +\ssrule{ss-iffalse}{ +}{ + \sstep{\ife{\false}{e_1}{e_2}}{\sigma}{e_2}{\sigma} +} +\end{array} +\] +\[ +\begin{array}{r@{\qquad}l} +\ssrule{ss-ifctx}{ + \sstep{e_1}{\sigma}{e_1'}{\sigma'} +}{ + \sstep{\ife{e_1}{e_2}{e_3}}{\sigma}{\ife{e_1'}{e_2}{e_3}}{\sigma'} +} +\ssrule{ss-while}{ +}{ + \sstep{\whilee{e_1}{e_2}}{\sigma}{\ife{e_1}{e_2;\whilee{e_1}{e_2}}{\false}}{\sigma} +} +\end{array} +\] +\end{figure} + + +\end{document} +