datatype Bop = Plus | Minus | Mult | Div | Equal | Less | Greater | And | Or datatype stat = Assign of string * exp | Sequence of stat list | Ifthen of exp * stat | Ifthenelse of exp * stat * stat | While of exp * stat | Repeat of stat list * exp | Forup of string * exp * exp * stat | Fordown of string * exp * exp * stat | Case of exp * (int * stat) list and exp = Var of string | Number of int | Boolean of bool | Binary of exp * Bop * exp | Not of expWrite an ML function that accepts an arbitrary
stat
and
eliminates from it all occurrences of Repeat, Forup, Fordown,
and Case
. For example,
- ... in SML ... (* so we can see the output clearly *) - Compiler.Control.Print.printDepth := 100; - Compiler.Control.Print.printLength := 1000; - expandstat (Repeat([Assign("x",Number(3)), Assign("z",Number(4))], Var("y"))); val it = Sequence [Assign ("x",Number 3), Assign ("z",Number 4), While (Not (Var "y"), Sequence [Assign ("x",Number 3),Assign ("z",Number 4)])] : stat (* converted repeat x=3; z=4; until y to x =3; z=4; while (not y) do x=3; z=4; *) - expandstat(Case(Var("x"), [(0,Assign("y0",Number(10))), (1,Assign("y1",Number(11))), (2,Assign("y2",Number(12)))])); val it = Sequence [Assign ("temp",Var "x"), Ifthenelse (Binary (Var "temp",Equal,Number 0),Assign ("y0",Number 10), Ifthenelse (Binary (Var "temp",Equal,Number 1),Assign ("y1",Number 11), Ifthen (Binary (Var "temp",Equal,Number 2),Assign ("y2",Number 12))))] : stat (* converted case x of 0: y0 = 10; 1: y1 = 11; 2: y2 = 12; to temp = x if temp=0 then y0=10 else if temp=1 then y1=11 else if temp=2 then y2=12 *) - expandstat (Forup("x",Number(0),Number(10),Assign("y",Number(100)))); val it = Sequence [Assign ("x",Number 0), While (Not (Binary (Var "x",Greater,Number 10)), Sequence [Assign ("y",Number 100), Assign ("x",Binary (Var "x",Plus,Number 1))])] : stat (* converted for x = 0 upto 10 do y=100 to x = 0; while (not (x > 10)) do y = 100; x = x+1; *)
P
be the predicate { x >= 0 AND y > 5 }
. Q
be the predicate { x >= 0 AND y <= 5 }
. P
holds before the following loop:
repeat x = x + y; y = y - 1; until y <= 5then
Q
will hold after the loop.
sabry@cs.uoregon.edu