diff --git a/doc/03.tex b/doc/03.tex new file mode 100644 index 000000000..cca85795c --- /dev/null +++ b/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} diff --git a/regression/Makefile b/regression/Makefile index 6c6a99356..07fdbcf81 100644 --- a/regression/Makefile +++ b/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 diff --git a/regression/test012.expr b/regression/test012.expr new file mode 100644 index 000000000..ee4f4d7f3 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/regression/test012.input b/regression/test012.input new file mode 100644 index 000000000..e440e5c84 --- /dev/null +++ b/regression/test012.input @@ -0,0 +1 @@ +3 \ No newline at end of file diff --git a/regression/test015.expr b/regression/test015.expr new file mode 100644 index 000000000..7bf37b790 --- /dev/null +++ b/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 diff --git a/regression/test015.input b/regression/test015.input new file mode 100644 index 000000000..83b33d238 --- /dev/null +++ b/regression/test015.input @@ -0,0 +1 @@ +1000 diff --git a/regression/test017.expr b/regression/test017.expr new file mode 100644 index 000000000..182b94036 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/regression/test017.input b/regression/test017.input new file mode 100644 index 000000000..209e3ef4b --- /dev/null +++ b/regression/test017.input @@ -0,0 +1 @@ +20 diff --git a/regression/test018.expr b/regression/test018.expr new file mode 100644 index 000000000..90852b822 --- /dev/null +++ b/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 + diff --git a/regression/test018.input b/regression/test018.input new file mode 100644 index 000000000..123af9e94 --- /dev/null +++ b/regression/test018.input @@ -0,0 +1 @@ +23409 diff --git a/regression/test019.expr b/regression/test019.expr new file mode 100644 index 000000000..cdf9b51f9 --- /dev/null +++ b/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) diff --git a/regression/test019.input b/regression/test019.input new file mode 100644 index 000000000..e69de29bb diff --git a/regression/test020.expr b/regression/test020.expr new file mode 100644 index 000000000..a21ba85ce --- /dev/null +++ b/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 diff --git a/regression/test020.input b/regression/test020.input new file mode 100644 index 000000000..83b33d238 --- /dev/null +++ b/regression/test020.input @@ -0,0 +1 @@ +1000 diff --git a/regression/test021.expr b/regression/test021.expr new file mode 100644 index 000000000..d5190ba67 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/regression/test021.input b/regression/test021.input new file mode 100644 index 000000000..f599e28b8 --- /dev/null +++ b/regression/test021.input @@ -0,0 +1 @@ +10 diff --git a/regression/test022.expr b/regression/test022.expr new file mode 100644 index 000000000..6ad9db93a --- /dev/null +++ b/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) \ No newline at end of file diff --git a/regression/test022.input b/regression/test022.input new file mode 100644 index 000000000..209e3ef4b --- /dev/null +++ b/regression/test022.input @@ -0,0 +1 @@ +20 diff --git a/regression/test023.expr b/regression/test023.expr new file mode 100644 index 000000000..91d4ea9d9 --- /dev/null +++ b/regression/test023.expr @@ -0,0 +1,8 @@ +s := 0; + +repeat + read (n); + s := s + n +until n == 0; + +write (s) diff --git a/regression/test023.input b/regression/test023.input new file mode 100644 index 000000000..b4ce092e4 --- /dev/null +++ b/regression/test023.input @@ -0,0 +1,6 @@ +5 +6 +7 +8 +9 +0 \ No newline at end of file diff --git a/src/Driver.ml b/src/Driver.ml index da6c5b0ac..0ea101ebd 100644 --- a/src/Driver.ml +++ b/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 "--"; diff --git a/src/Language.ml b/src/Language.ml index 23a945e93..6b56a26e9 100644 --- a/src/Language.ml +++ b/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} - | %"write" "(" e:!(Expr.parse) ")" {Write e} - | %"skip" {Skip} - | %"if" e:!(Expr.parse) %"then" s1:parse %"else" s2:parse %"fi" {If (e, s1, s2)} - | %"while" e:!(Expr.parse) %"do" s:parse %"od" {While (e, s)} - | x:IDENT ":=" e:!(Expr.parse) {Assign (x, e)} + %"read" "(" x:IDENT ")" {Read x} + | %"write" "(" e:!(Expr.parse) ")" {Write e} + | %"skip" {Skip} + | %"if" e:!(Expr.parse) + %"then" the:parse + 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 diff --git a/src/SM.ml b/src/SM.ml index e3568119d..fe12ccf23 100644 --- a/src/SM.ml +++ b/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