Implemented control constructs

doc/03.tex

@@ -0,0 +1,289 @@
+\documentclass{article}
+
+\usepackage{amssymb, amsmath}
+\usepackage{alltt}
+\usepackage{pslatex}
+\usepackage{epigraph}
+\usepackage{verbatim}
+\usepackage{latexsym}
+\usepackage{array}
+\usepackage{comment}
+\usepackage{makeidx}
+\usepackage{listings}
+\usepackage{indentfirst}
+\usepackage{verbatim}
+\usepackage{color}
+\usepackage{url}
+\usepackage{xspace}
+\usepackage{hyperref}
+\usepackage{stmaryrd}
+\usepackage{amsmath, amsthm, amssymb}
+\usepackage{graphicx}
+\usepackage{euscript}
+\usepackage{mathtools}
+\usepackage{mathrsfs}
+\usepackage{multirow,bigdelim}
+\usepackage{subcaption}
+\usepackage{placeins}
+
+\makeatletter
+
+\makeatother
+
+\definecolor{shadecolor}{gray}{1.00}
+\definecolor{darkgray}{gray}{0.30}
+
+\def\transarrow{\xrightarrow}
+\newcommand{\setarrow}[1]{\def\transarrow{#1}}
+
+\def\padding{\phantom{X}}
+\newcommand{\setpadding}[1]{\def\padding{#1}}
+
+\newcommand{\trule}[2]{\frac{#1}{#2}}
+\newcommand{\crule}[3]{\frac{#1}{#2},\;{#3}}
+\newcommand{\withenv}[2]{{#1}\vdash{#2}}
+\newcommand{\trans}[3]{{#1}\transarrow{\padding#2\padding}{#3}}
+\newcommand{\ctrans}[4]{{#1}\transarrow{\padding#2\padding}{#3},\;{#4}}
+\newcommand{\llang}[1]{\mbox{\lstinline[mathescape]|#1|}}
+\newcommand{\pair}[2]{\inbr{{#1}\mid{#2}}}
+\newcommand{\inbr}[1]{\left<{#1}\right>}
+\newcommand{\highlight}[1]{\color{red}{#1}}
+\newcommand{\ruleno}[1]{\eqno[\scriptsize\textsc{#1}]}
+\newcommand{\rulename}[1]{\textsc{#1}}
+\newcommand{\inmath}[1]{\mbox{$#1$}}
+\newcommand{\lfp}[1]{fix_{#1}}
+\newcommand{\gfp}[1]{Fix_{#1}}
+\newcommand{\vsep}{\vspace{-2mm}}
+\newcommand{\supp}[1]{\scriptsize{#1}}
+\newcommand{\sembr}[1]{\llbracket{#1}\rrbracket}
+\newcommand{\cd}[1]{\texttt{#1}}
+\newcommand{\free}[1]{\boxed{#1}}
+\newcommand{\binds}{\;\mapsto\;}
+\newcommand{\dbi}[1]{\mbox{\bf{#1}}}
+\newcommand{\sv}[1]{\mbox{\textbf{#1}}}
+\newcommand{\bnd}[2]{{#1}\mkern-9mu\binds\mkern-9mu{#2}}
+\newtheorem{lemma}{Lemma}
+\newtheorem{theorem}{Theorem}
+\newcommand{\meta}[1]{{\mathcal{#1}}}
+\renewcommand{\emptyset}{\varnothing}
+
+\definecolor{light-gray}{gray}{0.90}
+\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}}
+
+\lstdefinelanguage{ocaml}{
+keywords={let, begin, end, in, match, type, and, fun, 
+function, try, with, class, object, method, of, rec, repeat, until,
+while, not, do, done, as, val, inherit, module, sig, @type, struct, 
+if, then, else, open, virtual, new, fresh},
+sensitive=true,
+%basicstyle=\small,
+commentstyle=\scriptsize\rmfamily,
+keywordstyle=\ttfamily\bfseries,
+identifierstyle=\ttfamily,
+basewidth={0.5em,0.5em},
+columns=fixed,
+fontadjust=true,
+literate={fun}{{$\lambda$}}1 {->}{{$\to$}}3 {===}{{$\equiv$}}1 {=/=}{{$\not\equiv$}}1 {|>}{{$\triangleright$}}3 {\&\&\&}{{$\wedge$}}2 {|||}{{$\vee$}}2 {^}{{$\uparrow$}}1,
+morecomment=[s]{(*}{*)}
+}
+
+\lstset{
+mathescape=true,
+%basicstyle=\small,
+identifierstyle=\ttfamily,
+keywordstyle=\bfseries,
+commentstyle=\scriptsize\rmfamily,
+basewidth={0.5em,0.5em},
+fontadjust=true,
+escapechar=!,
+language=ocaml
+}
+
+\sloppy
+
+\newcommand{\ocaml}{\texttt{OCaml}\xspace}
+
+\theoremstyle{definition}
+
+\title{Structural Induction\\
+  (the first draft)
+}
+
+\author{Dmitry Boulytchev}
+
+\begin{document}
+
+\maketitle
+
+%\section{Structural Induction}
+
+
+\begin{figure}
+\begin{subfigure}{\textwidth}
+\[
+\begin{array}{rclr}
+  \sembr{n}          & = & \lambda \sigma . n & \mbox{\scriptsize\rulename{[Const]}}\\
+  \sembr{x}          & = & \lambda \sigma . \sigma x & \mbox{\scriptsize\rulename{[Var]}} \\
+  \sembr{A\otimes B} & = & \lambda \sigma . (\sembr{A}\sigma \oplus \sembr{B}\sigma) & \mbox{\scriptsize\rulename{[Binop]}}
+\end{array}
+\]
+\caption{Denotational semantics for expressions}
+\end{subfigure}
+\vskip5mm
+\begin{subfigure}{\textwidth}
+  \[\trans{c}{\epsilon}{c}\ruleno{Stop$_{SM}$}\]
+  \[\trule{\trans{\inbr{(x\oplus y)\llang{::}st, s}}{p}{c^\prime}}{\trans{\inbr{y\llang{::}x\llang{::}st, s}}{(\llang{BINOP $\;\otimes$})p}{c^\prime}}\ruleno{Binop$_{SM}$}\]
+  \[\trule{\trans{\inbr{z\llang{::}st, s}}{p}{c^\prime}}{\trans{\inbr{st, s}}{(\llang{CONST $\;z$})p}{c^\prime}}\ruleno{Const$_{SM}$}\]
+  \[\trule{\trans{\inbr{(s\;x)\llang{::}st, s}}{p}{c^\prime}}{\trans{\inbr{st, s}}{(\llang{LD $\;x$})p}{c^\prime}}\ruleno{LD$_{SM}$}\]
+  \caption{Big-step operational semantics for stack machine}
+\end{subfigure}
+\vskip5mm
+\begin{subfigure}{\textwidth}
+\[
+\begin{array}{rclr}
+  \sembr{x}^{\mathscr E}_{comp}&=&\llang{[LD $\;x$]} & \mbox{\scriptsize\rulename{[Var$_{comp}$]}} \\
+  \sembr{n}^{\mathscr E}_{comp}&=&\llang{[CONST $\;n$]} & \mbox{\scriptsize\rulename{[Const$_{comp}$]}}\\
+  \sembr{A\otimes B}^{\mathscr E}_{comp}&=&\sembr{A}^{\mathscr E}_{comp}\llang{@}\sembr{B}^{\mathscr E}_{comp}\llang{@[BINOP $\otimes$]}) & \mbox{\scriptsize\rulename{[Binop$_{comp}$]}}
+\end{array}
+\]
+\caption{Compilation}
+\end{subfigure}
+\caption{All relevant definitions}
+\label{definitions}
+\end{figure}
+
+
+We have considered two languages (a language of expressions $\mathscr E$ and a language of stack machine programs $\mathscr P$), and a compiler from the former to the latter.
+It can be formally proven, that the compiler is (fully) correct in the sense, given in the lecture 1. Due to the simplicity of the languages, the proof technique~---
+\emph{structural induction}~--- is simple as well.
+
+First, we collect all needed definitions in one place (see Fig.~\ref{definitions}). We simplified the description of stack machine semantics a little bit: first,
+we dropped off all instructions, which cannot be generated by the expression compiler, and then, we removed the input and output streams from the stack machine
+configurations, since they are never affected by the remaining instructions.
+
+\begin{lemma}(Determinism)
+  Let $p$ be an arbitrary stack machine program, and let $c$, $c_1$ and $c_2$ be arbitrary configurations. Then
+
+  \[
+    \trans{c}{p}{c_1} \wedge \trans{c}{p}{c_2} \Rightarrow c_1= c_2
+  \]
+\end{lemma}
+\begin{proof}
+  Induction on the structure of $p$.
+
+  \textbf{Base case}. If $p=\epsilon$, then, by the rule \rulename{Stop$_{SM}$}, $c_1=c$ and $c_2=c$. Since no other rule can be
+  applied, we're done.
+
+  \textbf{Induction step}. If $p=\iota p^\prime$, then, by condition, we have
+
+    \[
+      \trule{\trans{c^\prime}{p^\prime}{c_1}}{\trans{c}{\iota p^\prime}{c_1}}
+    \]
+
+    and
+
+    \[
+      \trule{\trans{c^{\prime\prime}}{p^\prime}{c_2}}{\trans{c}{\iota p^\prime}{c_2}}
+    \]
+
+    where $c^\prime$ and $c^{\prime\prime}$ depend only on $c$ and $\iota$. By the case analysis on $\iota$ we conclude, that
+    $c^\prime=c^{\prime\prime}$. Since $p^\prime$ is shorter, than $p$, we can apply the induction hypothesis, which gives us
+    $c_1=c_2$.
+\end{proof}
+
+\FloatBarrier
+
+\begin{lemma} (Compositionality)
+  Let $p=p_1p_2$ be an arbitrary stack machine program, subdivided into arbitrary subprograms $p_1$ and $p_2$. Then,
+
+  \[
+  \forall c_1, c_2:\;\trans{c_1}{p}{c_2}\;\Leftrightarrow\;\exists c^\prime:\; \trans{c_1}{p_1}{c^\prime} \wedge \trans{c^\prime}{p_2}{c_2}
+  \]
+\end{lemma}
+\begin{proof}
+  Induction on the structure of $p$.
+  
+  \textbf{Base case}. The base case $p=\epsilon$ is trivial: use the rule \rulename{Stop$_{SM}$} and get $c^\prime=c_2=c_1$.
+  
+  \textbf{Induction step}. When $p=\iota p^\prime$, then there are two cases:
+
+  \begin{itemize}
+    \item Either $p_1=\epsilon$, then $c^\prime=c_1$ trivially by the rule \rulename{Stop$_{SM}$}, and we're done.
+    \item Otherwise $p_1=\iota p_1^\prime$, and, thus, $p=\iota p_1^\prime p_2$. In order to prove the lemma, we need to prove two implications:
+      \begin{enumerate}
+      \item Let $\trans{c_1}{p=\iota p_1^\prime p_2}{c_2}$. Technically, we need here to consider three cases (one for each type of the instruction
+        $\iota$), but in all cases the outcome would be the same: we have the picture
+
+        \[
+        \trule{\trans{c^{\prime\prime}}{p_1^\prime p_2}{c_2}}{\trans{c_1}{p=\iota p_1^\prime p_2}{c_2}}
+        \]
+
+        where $c^{\prime\prime}$ depends only on $\iota$ and $c_1$. Since $p_1^\prime p_2$ is shorter, than $p$, we can apply the induction hypothesis, which gives us a
+        configuration $c^\prime$, such, that $\trans{c^{\prime\prime}}{p_1^\prime}{c^\prime}$ and $\trans{c^\prime}{p_2}{c_2}$. The observation $\trans{c_1}{\iota p_1^\prime}{c^\prime}$
+        concludes the proof (note, we implicitly use determinism here).
+      \item Let there exists $c^\prime$, such that $\trans{c_1}{\iota p_1^\prime}{c^\prime}$ and $\trans{c^\prime}{p_2}{c_2}$. From the first relation we have
+
+        \[
+          \trule{\trans{c^{\prime\prime}}{p_1^\prime}{c^\prime}}{\trans{c_1}{\iota p_1^\prime}{c^\prime}}
+        \]
+
+        where $c^{\prime\prime}$ depends only on $\iota$ and $c_1$. Since $p_1^\prime p_2$ is shorter, than $p$, we can apply the induction hypothesis, which
+        gives us $\trans{c^{\prime\prime}}{p_1^\prime p_2}{c_2}$, and, thus, $\trans{c_1}{\iota p_1^\prime p_2}{c_2}$ (again, we implicitly use determinism here).
+      \end{enumerate}
+  \end{itemize}
+\end{proof}
+
+\begin{theorem}(Correctness of compilation)
+  Let $e\in\mathscr E$ be arbitrary expression, $s$~--- arbitrary state, and $st$~--- arbitrary stack. Then
+
+  \[
+    \trans{\inbr{st, s}}{\sembr{e}^{\mathscr E}_{comp}}{\inbr{(\sembr{e}\,s)::st, s}}\; \mbox{iff} \; (\sembr{e}\,s)\; \mbox{is defined}
+  \]
+\end{theorem}
+\begin{proof}
+  Induction on the structure of $e$.
+
+  \textbf{Base case}. There are two subcases:
+
+  \begin{enumerate}
+  \item $e$ is a constant $z$. Then:
+     \begin{itemize}
+       \item $\sembr{e}\,s=z$ for each state $s$;
+       \item \mbox{$\sembr{e}^{\mathscr E}_{comp}=[\llang{CONST z}]$};
+       \item $\trans{\inbr{st, s}}{[\llang{CONST z}]}{\inbr{z::st, s}}$ for arbitrary $st$ and $s$.
+     \end{itemize}
+
+     This concludes the first base case.
+
+   \item $e$ is a variable $x$. Then:
+     \begin{itemize}
+       \item $\sembr{s}\,s=s\,x$ for each state $s$, such that $s\,x$ is defined;
+       \item \mbox{$\sembr{e}^{\mathscr E}_{comp}=[\llang{LD x}]$};
+       \item $\trans{\inbr{st, s}}{[\llang{CONST z}]}{\inbr{(s\,x)::st, s}}$ for arbitrary $st$ and arbitrary $s$, such that $s\, x$ is defined.
+     \end{itemize}
+
+     This concludes the second base case.     
+  \end{enumerate}
+
+  \textbf{Induction step}. Let $e$ be $A\otimes B$. Then:
+
+  \begin{itemize}
+    \item $\sembr{A\otimes B}s=\sembr{A}s\oplus\sembr{B}s$ for each state $s$, such that both $\sembr{A}s$ and $\sembr{B}s$ are defined;
+    \item $\sembr{A\otimes B}^{\mathscr E}_{comp}=\sembr{A}^{\mathscr E}_{comp}\llang{@}\sembr{B}^{\mathscr E}_{comp}\llang{@[BINOP $\oplus$]}$;
+    \item by the inductive hypothesis, for arbitrary $st$ and $s$
+
+      \[
+        \trans{\inbr{st, s}}{\sembr{A}^{\mathscr E}_{comp}}{\inbr{(\sembr{A}s)::st, s}} \mbox{iff} \; (\sembr{A}\,s)\; \mbox{is defined}
+      \]
+
+      and
+
+      \[
+        \trans{\inbr{(\sembr{A}s)::st, s}}{\sembr{B}^{\mathscr E}_{comp}}{\inbr{(\sembr{B}s)::(\sembr{A}s)::st, s}} \mbox{iff} \; (\sembr{A}\,s) \;\mbox{and}\; (\sembr{A}\,s) \; \mbox{are defined}
+      \]
+
+      Taking into account the semantics of \llang{BINOP $\otimes$} and applying the compositionality lemma, the theorem follows.
+  \end{itemize}
+\end{proof}
+
+\end{document}

regression/Makefile

@@ -1,4 +1,4 @@
-TESTS=test001 test002 test003 test004 test005 test006 test007 test008 test009 test010 test011 test012
+TESTS=test001 test002 test003 test004 test005 test006 test007 test008 test009 test010 test011 test012 test015 test017 test018 test019 test020 test021 test022 test023
 
 RC=../src/rc.opt
 

regression/test012.expr

@@ -0,0 +1,12 @@
+read (n);
+while n >= 0 do
+  if n > 1
+  then
+    write (0);
+    if n == 3 then write (0) else write (1) fi
+  else
+    write (1);
+    if n > 0 then write (0) else write (1) fi
+  fi;
+  n := n - 1
+od

regression/test012.input

@@ -0,0 +1 @@
+3

regression/test015.expr

@@ -0,0 +1,20 @@
+s := 0;
+read (n);
+p := 2;
+
+while n > 0 do
+    c := 2;
+    f := 1;
+
+    while c*c <= p && f do
+      f := (p % c) != 0;
+      c := c + 1
+    od;
+
+    if f != 0 then
+      if n == 1 then write (p) else skip fi;
+      n := n - 1
+    else skip fi;
+
+    p := p + 1
+od

regression/test015.input

@@ -0,0 +1 @@
+1000

regression/test017.expr

@@ -0,0 +1,15 @@
+read (n);
+
+i     := 2;
+fib_1 := 1;
+fib_2 := 1;
+fib   := 1;
+
+while i < n do
+      fib   := fib_1 + fib_2;
+      fib_2 := fib_1;
+      fib_1 := fib;
+      i     := i+1
+od;
+
+write (fib)

regression/test017.input

@@ -0,0 +1 @@
+20

regression/test018.expr

@@ -0,0 +1,43 @@
+read (n);
+
+c := 1;
+p := 2;
+
+while c do
+
+  cc := 1;
+
+  while cc do
+    q := 2;
+
+    while q * q <= p && cc do
+      cc := p % q != 0;
+      q := q + 1
+    od;
+
+    if cc then cc := 0 else p := p + 1; cc := 1 fi
+   
+  od;
+
+  d := p;
+  i := 0;
+
+  q := n / d;
+  m := n % d;
+
+  while q > 0 && m == 0 do
+    i := i + 1;
+    d := d * p;
+    m := n % d;
+    if m == 0 then q := n / d else skip fi
+  od;
+
+  write (p);
+  write (i);
+
+  n := n / (d / p);
+  p := p + 1;
+  c := n != 1
+
+od
+

regression/test018.input

@@ -0,0 +1 @@
+23409

regression/test019.expr

@@ -0,0 +1,13 @@
+i := 0;
+s := 0; 
+
+for i := 0, i < 100, i := i+1
+do
+    for j := 0, j < 100, j := j+1
+    do   
+      s := s + j
+    od;
+    s := s + i
+od;
+
+write (s)

regression/test020.expr

@@ -0,0 +1,20 @@
+s := 0;
+read (n);
+p := 2;
+
+while n > 0 do
+    c := 2;
+    f := 1;
+
+    for c := 2, c*c <= p && f, c := c+1
+    do  
+      f := p % c != 0
+    od;
+
+    if f != 0 then
+      if n == 1 then write (p) fi;
+      n := n - 1
+    fi;
+
+    p := p + 1
+od

regression/test020.input

@@ -0,0 +1 @@
+1000

regression/test021.expr

@@ -0,0 +1,9 @@
+read (n);
+f := 1;
+
+for skip, n >= 1, n := n-1
+do
+  f := f * n
+od;
+
+write (f)

regression/test021.input

@@ -0,0 +1 @@
+10

regression/test022.expr

@@ -0,0 +1,14 @@
+read (n);
+
+fib_1 := 1;
+fib_2 := 1;
+fib   := 1;
+
+for i := 2, i < n, i := i+1
+do
+      fib   := fib_1 + fib_2;
+      fib_2 := fib_1;
+      fib_1 := fib
+od;
+
+write (fib)

regression/test022.input

@@ -0,0 +1 @@
+20

regression/test023.expr

@@ -0,0 +1,8 @@
+s := 0;
+
+repeat
+  read (n);
+  s := s + n
+until n == 0;
+
+write (s)  

regression/test023.input

@@ -0,0 +1,6 @@
+5
+6
+7
+8
+9
+0

src/Driver.ml

@@ -6,7 +6,7 @@ let parse infile =
     (object
        inherit Matcher.t s
        inherit Util.Lexers.decimal s
-       inherit Util.Lexers.ident ["read"; "write"; "skip"; "if"; "then"; "else"; "fi"; "while"; "do"; "od"] s
+       inherit Util.Lexers.ident ["read"; "write"; "skip"; "if"; "then"; "else"; "elif"; "fi"; "while"; "do"; "od"; "repeat"; "until"; "for"] s
        inherit Util.Lexers.skip [
 	 Matcher.Skip.whitespaces " \t\n";
 	 Matcher.Skip.lineComment "--";

src/Language.ml

@@ -113,7 +113,8 @@ module Stmt =
     (* composition                      *) | Seq    of t * t 
     (* empty statement                  *) | Skip
     (* conditional                      *) | If     of Expr.t * t * t
-    (* loop                             *) | While  of Expr.t * t with show
+    (* loop with a pre-condition        *) | While  of Expr.t * t
+    (* loop with a post-condition       *) | Repeat of t * Expr.t with show
                                                                     
     (* The type of configuration: a state, an input stream, an output stream *)
     type config = Expr.state * int list * int list 
@@ -133,6 +134,7 @@ module Stmt =
       | Skip               -> conf
       | If     (e, s1, s2) -> eval conf (if Expr.eval st e <> 0 then s1 else s2)
       | While  (e, s)      -> if Expr.eval st e = 0 then conf else eval (eval conf s) stmt
+      | Repeat (s, e)      -> let (st, _, _) as conf' = eval conf s in if Expr.eval st e = 0 then eval conf' stmt else conf'
                                 
     (* Statement parser *)
     ostap (
@@ -140,12 +142,27 @@ module Stmt =
         s:stmt ";" ss:parse {Seq (s, ss)}
       | stmt;
       stmt:
-        %"read"  "(" x:IDENT ")"                                      {Read x}
+        %"read"  "(" x:IDENT ")"         {Read x}
-      | %"write" "(" e:!(Expr.parse) ")"                              {Write e}
+      | %"write" "(" e:!(Expr.parse) ")" {Write e}
-      | %"skip"                                                       {Skip}
+      | %"skip"                          {Skip}
-      | %"if" e:!(Expr.parse) %"then" s1:parse %"else" s2:parse %"fi" {If (e, s1, s2)}
+      | %"if" e:!(Expr.parse)
-      | %"while" e:!(Expr.parse) %"do" s:parse %"od"                  {While (e, s)}
+	  %"then" the:parse 
-      | x:IDENT ":=" e:!(Expr.parse)                                  {Assign (x, e)}            
+          elif:(%"elif" !(Expr.parse) %"then" parse)*
+	  els:(%"else" parse)? 
+        %"fi" {
+          If (e, the, 
+	         List.fold_right 
+		   (fun (e, t) elif -> If (e, t, elif)) 
+		   elif
+		   (match els with None -> Skip | Some s -> s)
+          )
+        }
+      | %"while" e:!(Expr.parse) %"do" s:parse %"od"{While (e, s)}
+      | %"for" i:parse "," c:!(Expr.parse) "," s:parse %"do" b:parse %"od" {
+	  Seq (i, While (c, Seq (b, s)))
+        }
+      | %"repeat" s:parse %"until" e:!(Expr.parse)  {Repeat (s, e)}
+      | x:IDENT ":=" e:!(Expr.parse)                {Assign (x, e)}            
     )
       
   end

src/SM.ml

@@ -92,6 +92,11 @@ let compile p =
                                let cond, env = env#get_label in
                                let env, _, s = compile' cond env s in
                                env, false, [JMP cond; LABEL loop] @ s @ [LABEL cond] @ expr c @ [CJMP ("nz", loop)]
+                                                                                                  
+  | Stmt.Repeat (s, c)      -> let loop , env = env#get_label in
+                               let check, env = env#get_label in
+                               let env  , flag, body = compile' check env s in
+                               env, false, [LABEL loop] @ body @ (if flag then [LABEL check] else []) @ (expr c) @ [CJMP ("z", loop)]
   in
   let env =
     object