The while-language

In this section, we introduce a simple while-language composed from the syntactic elements: expressions (Exp) and commands ( Com). In this simple language expressions are composed of integer constants, variables, and operators. A simple algebraic datatype to describe the abstract syntax of expressions is given in METAML below:

datatype Exp =
  Constant of int               (*   5     *)
| Variable of string            (*   x     *)
| Minus of (Exp * Exp)          (*  x - 5  *)
| Greater of (Exp * Exp)        (*  x > 1  *)
| Times of (Exp * Exp) ;        (*  x * 4  *)

Commands include assignment, sequencing of commands, a conditional (if command), while loops, a print command, and a declaration which introduces new statically scoped variables. A declaration introduces a variable, provides an expression that defines its initial value, and limits its scope to the enclosing command. A simple algebraic datatype to describe the abstract syntax of commands is:

datatype Com =
  Assign  of (string * Exp)     
| Seq     of (Com * Com)  
| Cond    of (Exp * Com * Com)    
| While   of (Exp * Com)   
| Declare of (string * Exp * Com)   
| Print   of Exp;    

(* ****** Example Concrete Syntax ******* *)
(* Assign    x := 1                       *)
(* Seq       { x :=1; y:= 2 }             *)
(* Cond      if x then x := 1 else y := 1 *)
(* While     while x>0 do x := x - 1      *)
(* Declare   declare x = 1 in x := x - 1  *)
(* Print     print x                      *)

A simple while-program in concrete syntax, such as

declare x = 150 in
   declare y = 200 in 
      { while x > 0 do { x := x - 1; y := y - 1 };
        print y }

is encoded abstractly in these datatypes as follows:

val S1 =
Declare("x",Constant 150,
  Declare("y",Constant 200,
    Seq(While(Greater(Variable "x",Constant 0),
              Seq(Assign("x",Minus(Variable "x",
                                   Constant 1)),
                  Assign("y",Minus(Variable "y",
                                   Constant 1)))),
        Print(Variable "y"))));