DIRECTORY Rope, Atom, TypeCheck, Unparser;

TypeCheckImpl: PROGRAM 
IMPORTS Atom, Unparser
EXPORTS TypeCheck = BEGIN

OPEN TypeCheck;

arrow : ATOM = Atom.MakeAtom [ "=>" ];
asgn : ATOM = Atom.MakeAtom[ "_" ];
box : ATOM = Atom.MakeAtom[ "||" ];
colon : ATOM = Atom.MakeAtom [ ":" ];
comma : ATOM = Atom.MakeAtom[ "," ];
dblEq : ATOM = Atom.MakeAtom[ "==" ];
eq : ATOM = Atom.MakeAtom[ "=" ];
ge : ATOM = Atom.MakeAtom[ ">=" ];
gt : ATOM = Atom.MakeAtom[ ">" ];
lbrace : ATOM = Atom.MakeAtom[ "{" ];
lbracket : ATOM = Atom.MakeAtom[ "[" ];
le : ATOM = Atom.MakeAtom[ "<=" ];
lparen : ATOM = Atom.MakeAtom [ "(" ];
lt : ATOM = Atom.MakeAtom[ "<" ];
minus : ATOM = Atom.MakeAtom[ "-" ];
ne : ATOM = Atom.MakeAtom[ "#" ];
not : ATOM = Atom.MakeAtom[ "~" ];
plus : ATOM = Atom.MakeAtom[ "+" ];
rbrace : ATOM = Atom.MakeAtom[ "}" ];
rbracket : ATOM = Atom.MakeAtom[ "]" ];
rparen : ATOM = Atom.MakeAtom[ ")" ];
semicolon : ATOM = Atom.MakeAtom[";"];
star : ATOM = Atom.MakeAtom[ "*" ];
up : ATOM = Atom.MakeAtom[ "^" ];

Wlp: PUBLIC PROCEDURE [ s : Stmt, p : Predicate ]  RETURNS [ q : Predicate ] =
{
IF s = NIL THEN ERROR;

SELECT Optr [ s ] FROM

asgn => q _ Substitute  [ VarOfAsgn [ s ], Arg2 [ s ], p ];
semicolon => q _ Wlp [ Arg1 [ s ], Wlp [ Arg2 [ s ], p ] ];
$if => q _ WlpIfCmdList [ GcmdsOfIf [ s ], p ];
$do => q _ WlpDo [ s, p ];

ENDCASE => ERROR;
};

Substitute:
  PRIVATE PROCEDURE [ v : Term, t : Term, p : ParseTree ] RETURNS [ q : ParseTree ] =
{
IF p = NIL THEN RETURN [ p ];

WITH p SELECT FROM

a : ATOM => q _ SubstituteForVar [ v, t, a ];

n : REF INT => q _ n;

l : List =>
q _ CONS
[ Substitute [ v, t, l.first ], NARROW [ Substitute [ v, t, l.rest ], List ] ]

ENDCASE => ERROR;
};

SubstituteForVar:
  PRIVATE PROCEDURE [ v : Term, t : Term, a : ATOM ] RETURNS [ q : ParseTree ] =
{
IF v = NIL THEN RETURN [ a ];

IF ISTYPE [ v, ATOM ] THEN
IF NARROW [ v, ATOM ] = a THEN RETURN [ t ] ELSE RETURN [ a ];

IF ( a = NARROW [ Arg1 [ v ], ATOM ] ) THEN
q _ Arg1 [ t ]
ELSE
q _ SubstituteForVar [ Arg2 [ v ], Arg2 [ t ], a ];
};

WlpIfCmdList:
  PRIVATE PROCEDURE [ gcs : ParseTree, p : Predicate ] RETURNS [ q : Predicate ] =
{
moreThanOne : BOOL;  -- TRUE if there is more than one guard in the list.
wlpFirst, wlpRest : ParseTree;  -- wlp's of first and other guards of the list.
IF gcs = NIL THEN RETURN [ $true ];

IF ( moreThanOne _ ( Optr [ gcs ] = box ) ) THEN
{
wlpFirst _ WlpIfCmd [ Arg1 [ gcs ], p ];
wlpRest _ WlpIfCmdList [ Arg2 [ gcs ], p ];

q _ Binary [ $and, Parenthesize [ wlpFirst ], wlpRest ]
}
ELSE
q _ Parenthesize [ WlpIfCmd [ gcs, p ] ];
};

WlpIfCmd:
  PRIVATE PROCEDURE [ gc : Stmt, p : Predicate ] RETURNS [ q : Predicate ] =
{
x, R, S : ParseTree;  -- as above.
impl : ParseTree;  -- the tree ( R impl wlp(S,P)).
IF gc = NIL OR Optr [ gc ] # arrow THEN ERROR;

[ x, R, S ] _ SplitGcmd [ gc ];

impl _ PBinary [ $impl, R, Wlp [ S, p ] ];

IF x = NIL THEN
q _ PUnary [ $all, PBinary [ colon, x, impl ] ]
ELSE
q _ impl;
};

WlpDo:
  PRIVATE PROCEDURE [ s : ParseTree, p : Predicate ] RETURNS [ F1 : Predicate ] =
{

F2, F3, F4, F5, F6, F7, F8, F9 : Predicate;
u : Term;  -- the free variables of s that are assigned to in s.
inv : ParseTree _ InvOfDo [ s ];
gcs : ParseTree _ GcmdsOfDo [ s ];

[ F7, F9 ] _ WlpDoGcmds [ gcs, inv ];

F6 _ PUnary [ not, F7 ];
F5 _ PBinary [ $and, p, F6 ];
F8 _ PBinary [ $or, F5, F9 ];

IF ( u _ FreeAsgVars [ s ] ) = NIL THEN
F1 _ PBinary [ $and, inv, F8 ]
ELSE
{
F4 _ PBinary [ $impl, inv, F8 ];
F3 _ PBinary [ colon, u, F4 ];
F2 _ PUnary [ $all, F3 ];
F1 _ PBinary [ $and, inv, F2 ]
};
};

WlpDoGcmds:
  PRIVATE PROCEDURE [ gcs : ParseTree, inv : Predicate ] RETURNS [ F7, F9 : Predicate ] =
{
moreThanOne : BOOL;  -- TRUE if there is more than one guard in the list.
x, R, S : ParseTree;  -- the current guard, broken into its parts, x : R => S.

IF gcs = NIL THEN RETURN [ F7 : $false, F9 : $true ];

IF ( moreThanOne _ ( Optr [ gcs ] = box ) ) THEN
{
[ F7, F9 ] _ WlpDoGcmds [ Arg2 [ gcs ], inv ];
[ x, R, S ] _ SplitGcmd [ Arg1 [ gcs ] ];
F7 _ Binary [ $or, Parenthesize [ R ], F7 ];
F9 _ PBinary [ $and, PBinary [ $impl, R, Wlp [ S, inv ] ], F9 ]
}
ELSE
{
[ x, R, S ] _ SplitGcmd [ gcs ];
F7 _ Parenthesize [ R ];
F9 _ Parenthesize [ PBinary [ $impl, R, Wlp [ S, inv ] ] ]
};
};

FreeAsgVars:
  PRIVATE PROCEDURE [ s : Stmt ] RETURNS [ v : ParseTree ] =
{
IF s = NIL THEN RETURN [ NIL ];

SELECT Optr [ s ] FROM

asgn => v _ VarOfAsgn [ s ];
semicolon => v _ Add [ FreeAsgVars [ Arg1 [ s ] ], FreeAsgVars [ Arg2 [ s ] ] ];
$if => v _ FreeAsgVarsOfGcmds [ GcmdsOfIf [ s ] ];
$do => v _ FreeAsgVarsOfGcmds [ GcmdsOfDo [ s ] ];

ENDCASE => ERROR;
};

FreeAsgVarsOfGcmds:
  PRIVATE PROCEDURE [ gcs : ParseTree ] RETURNS [ v : Term ] =
{
moreThanOne : BOOL;  -- TRUE if there is more than one guard in the list.

IF gcs = NIL THEN RETURN [ NIL ];

IF ( moreThanOne _ ( Optr [ gcs ] = box ) ) THEN

v _ Add
[ FreeAsgVarsOfGcmd [ Arg1 [ gcs ] ]
, FreeAsgVarsOfGcmds [ Arg2 [ gcs ] ]
]

ELSE
v _ FreeAsgVarsOfGcmd [ gcs ]
};

FreeAsgVarsOfGcmd:
  PRIVATE PROCEDURE [ gc : Stmt ] RETURNS [ v : Term ] =
{
x, R, S : ParseTree;
IF gc = NIL OR Optr [ gc ] # arrow THEN ERROR;

[ x, R, S ] _ SplitGcmd [ gc ];

IF x = NIL THEN
v _ FreeAsgVars [ S ]
ELSE
v _ Subtract [ FreeAsgVars [ S ], x ];
};

Add:
  PRIVATE PROCEDURE [ x, y : Term ] RETURNS [ z : Term ] =
{
IF x = NIL THEN RETURN [ y ];
IF y = NIL THEN RETURN [ x ];

WITH x SELECT FROM  a : ATOM => RETURN [ AddVar [ a, y ] ]  ENDCASE;

IF Optr [ x ] # comma THEN ERROR;

z _  AddVar [ NARROW [ Arg1 [ x ], ATOM ], Add [ Arg2 [ x ], y ] ]
};

AddVar:
  PRIVATE PROCEDURE [ v : ATOM, y : Term ] RETURNS [ t : Term ] =
{
a : ATOM;  -- the first variable of y.
IF y = NIL THEN RETURN [ v ];

WITH y SELECT FROM
a : ATOM => RETURN [ IF a = v THEN a ELSE CommaTogether [ v, a ] ]
ENDCASE;

IF Optr [ y ] # comma THEN ERROR;

IF v = ( a _ NARROW [ Arg1 [ y ], ATOM ] ) THEN
t _ y
ELSE
t _ CommaTogether [ a, AddVar [ v, Arg2 [ y ] ] ]
};

Subtract:
  PRIVATE PROCEDURE [ x, y : Term ] RETURNS [ z : Term ] =
{
IF x = NIL THEN RETURN [ NIL ];
IF y = NIL THEN RETURN [ x ];

WITH y SELECT FROM  a : ATOM => RETURN [ SubtractVar [ a, x ] ]  ENDCASE;

IF Optr [ y ] # comma THEN ERROR;

z _  SubtractVar [ NARROW [ Arg1 [ y], ATOM ], Subtract [ x, Arg2 [ y ] ] ]
};

SubtractVar:
  PRIVATE PROCEDURE [ v : ATOM, y : Term ] RETURNS [ t : Term ] =
{
a : ATOM;  -- the first variable of y.
IF y = NIL THEN RETURN [ NIL ];

WITH y SELECT FROM a : ATOM => RETURN [ IF a = v THEN NIL ELSE a ] ENDCASE;

IF Optr [ y ] # comma THEN ERROR;

IF v = ( a _ NARROW [ Arg1 [ y ], ATOM ] ) THEN
t _ Arg2 [ y ]
ELSE
t _ CommaTogether [ a, SubtractVar [ v, Arg2 [ y ] ] ]
};

CommaTogether:
  PRIVATE PROCEDURE [ v : ATOM, y : Term ] RETURNS [ t : Term ] =
{
t _ IF y = NIL THEN v ELSE Binary [ comma, v, y ]
};


PBinary:
  PRIVATE PROCEDURE [ op : ATOM, lhs, rhs : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN
[ CONS [ op, CONS [ Parenthesize [ lhs ], CONS [ Parenthesize [ rhs ], NIL ] ] ] ]
};

PUnary:
  PRIVATE PROCEDURE [ op : ATOM, opnd : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN [ CONS [ op, CONS [ Parenthesize [ opnd ], NIL ] ] ]
};

Binary:
  PRIVATE PROCEDURE [ op : ATOM, lhs, rhs : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN [ CONS [ op, CONS [ lhs, CONS [ rhs, NIL ] ] ] ]
};

Unary:
  PRIVATE PROCEDURE [ op : ATOM, opnd : ParseTree ] RETURNS [ t : ParseTree ] =
{
RETURN [ CONS [ op, CONS [ opnd, NIL ] ] ]
};

Parenthesize:
  PRIVATE PROCEDURE [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
IF NotLeaf [ p ] AND Optr [ p ] = lparen THEN RETURN [ p ];

RETURN [ Unary [ lparen, p ] ]
};

ArgsOf:
  PRIVATE PROCEDURE [ p : ParseTree ] RETURNS [ ParseTree, ParseTree ] =
{
RETURN [ Arg1 [ p ], Arg2 [ p ] ]
};

Optr: PROC [ r : ParseTree ] RETURNS [ a : ATOM ] = { a _ NARROW [ Car[r] ] };
Arg1: PROC [ r : ParseTree ] RETURNS [ ParseTree ] = Cadr;
Arg2: PROC [ r : ParseTree ] RETURNS [ ParseTree ] = Caddr;
SplitGcmd: PROC [ gc : Stmt ] RETURNS [ x, R, S : ParseTree _ NIL ] =
{
G : ParseTree;  -- x : R or R, as appropriate

[ G, S ] _ ArgsOf [ gc ];

IF NotLeaf [ G ] AND Optr [ G ] = colon THEN
[ x, R ] _ ArgsOf [ G ]
ELSE
R _ G;
};

VarOfAsgn: PROC [ p : ParseTree ] RETURNS [ v : ParseTree ] =
{
v _ Arg1 [ p ]  -- The variables of an assignment
};

GcmdsOfIf: PROC [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
q _ Arg1 [ p ] -- the guarded commands of if G => S ... fi
};

GcmdsOfDo: PROC [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
q _ Arg2 [ Arg1 [ p ] ] -- the guarded commands of do I inv G => S ... od
};

InvOfDo: PROC [ p : ParseTree ] RETURNS [ q : ParseTree ] =
{
q _ Arg1 [ Arg1 [ p ] ] -- the invariant of do I inv G => S ... od
};

Car: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[NARROW[NARROW[r, List].first]]};
Cdr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[NARROW[r, List].rest]};
Cadr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[Car[Cdr[r]]]};
Cddr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[Cdr[Cdr[r]]]};
Caddr: PROC [r: ParseTree] RETURNS [ParseTree] = {RETURN[Car[Cdr[Cdr[r]]]]};

NotLeaf: PROC [ p : ParseTree ] RETURNS [ b : BOOL ] =
{
RETURN [ p # NIL AND ISTYPE [ p, List ] ]
};

Unparse:
  PRIVATE PROCEDURE [ p : ParseTree ] RETURNS [ r : ROPE ] =
{
r _ Unparser.Unparse
[ f : CONS [ p, NIL ], culprit : NIL, margin : 60, p : NIL, openCount : 0 ]
};

END. 

–-- TypeCheckImpl.mesa
-- Last edited by Jim Sasaki on August 24, 1983 10:34 am
-- Some Atoms used as operators.

-- We calculate the weakest liberal precondition (wlp) of a statement S and a predicate P; it is the weakest predicate Q such that if you start S in state Q and S halts (i.e., doesn't abort or run forever) then P is true afterwards.

-- Substitute terms t for variables v in parse tree p.  Note that t and v are either individual terms or lists separated by commas.

-- If the atom a is among the variables v, then substitute the corresponding term from t for it.  Note that t and v are either individual terms or lists separated by commas.

-- We take the guarded commands of an if ... fi and return the and of their wlp's.


-- We have a guarded command of the form G => S where G is a guard.  If G is R, return ( R impl wlp(S,P) ).  If G is of the form x : R, return all x : ( R impl wlp(S,P) ).


-- Wlp ( do I inv G1 => S1 || ... Gn => Sn od, P ) =

I and all u : I impl ((P and not OR(i) Ri) or AND(i) (Ri => Wlp(Si,I)))
    1   2    3     4       5   6    7        8  9         10

where
OR(i) Ri means (R1 or R2 or ... Rn)
AND(i) R1 means (R1 and R2 and ... Rn)
u is the list of free variables of the loop that are assigned to (in the loop).

and the numbers under the operators indicate which formula is which.  (That is, F1 is (I and F2), F2 is (all F3), and so on.)

If u is empty, return
    I and ((P and not OR(i) Ri) or AND(i) (Ri => Wlp(Si,I)))
       1       5  6    7        8   9         10
-- Calculate formulas F7 and F9 as defined in WlpDo.

-- We return the free variables of s that are assigned to (in s).

-- We return an identifier list containing the free variables of gcs that are assigned to in gcs, where gcs is a list of guarded commands, G1 => S1 || ... Gn => Sn.

-- The guarded command gc has of the form G => S.  If G is a predicate R then fav(gc) is fav(s).  If G is a binding x : R, then fav(gc) = fav(s) minus the variables x.


-- Add together the two identifier lists x and y.  Eliminate duplications.

-- Add the variable v to the term y = var1,var2,...varN.


-- Take x and subtract off the identifiers of y, where both x and y are identifier lists.

-- Remove the variable v from the term y = var1,var2,...varN.


-- If y is nonNIL, we return (v,y) otherwise we return v.

-- Tree building routines: build binary and unary trees (with and without parenthesizing the arguments), parenthesize a tree.
-- Selector routines: get various args of a tree.


--  Split up the guarded command, x : R => S or R => S.  (Return x = NIL in the latter case.)

-- Inspection routines: check for nonleaves.

-- Some testing routines; not normally used otherwise.

Κ˜Jš
œN™NJ˜JšΟk	œ!˜*J˜šœœ
˜Jšœ˜Jšœ
˜J˜Jšœ˜J˜™ J™Jšœœ˜&Jšœœ˜#Jšœœ˜#Jšœœ˜%Jšœœ˜$Jšœœ˜%Jšœœ˜!Jšœœ˜"Jšœœ˜!Jšœ	œ˜%Jšœœ˜'Jšœœ˜"Jšœ	œ˜&Jšœœ˜!Jšœœ˜$Jšœœ˜!Jšœœ˜"Jšœœ˜#Jšœ	œ˜%Jšœœ˜'Jšœ	œ˜%Jšœœ˜&Jšœœ˜#Jšœœ˜!—J˜JšΟnœœ
	œœ˜Nš
œ
˜
š
œθ
™θ
J™Jšœœ
œ
œ
˜J˜šœ˜J˜Jš
œ;˜;J˜;J˜/J˜J˜—Jšœœ
˜——J˜J˜Jšž
œœ
	œ'œ˜a˜
Jš
œƒ
™ƒ
™Jšœœ
œ
œ˜J˜šœœ
˜J˜Jšœœ%˜-J˜Jšœœ
œ
˜J˜š
œ˜šœ˜Jšœ œ(˜N——J˜—Jšœœ
˜——J˜J˜Jš
žœœ
	œœœ˜b˜
Jš
œ­
™­
™Jšœœ
œ
œ˜J˜šœ
œœ˜Jšœ
œœœ
œœ
œ˜>—J˜šœœœ˜+J˜—š
˜J˜3———J˜J˜Jšžœœ
	œ$œ˜`˜
Jšœ&ž	œžœ™R™JšœœΟc4˜IJšœ Ÿ/˜OJ™Jšœœ
œ
œ˜#J˜Jšœ*˜0˜
Jš
œ(˜(Jš
œ+˜+J˜Jš
œ7˜7—J˜
š
˜J˜)———J˜J˜Jšžœœ
	œœ˜V˜
Jšœ)žœž
œž
œž
œ	žœ
ž
œž
œžœ	žœ
™«
™Jšœ
œ
œŸ˜"JšœŸΠcnŸ
˜2J™Jš
œœ
œœ
œ
˜.J˜Jšœ
œ
œ˜J˜Jšœ
œ
œ˜*J˜šœœ
˜J˜/—š
˜J˜	———J˜J˜Jšžœœ
	œ"œ˜X˜
Jš
œ4™4J™Jš
ΟfG™Gšœ‘8™<J™™J™#J™&J™O—J™Jš
œ}™}J™J™Jš
‘<™<Jš
‘0™0J˜J˜+JšœŸ5˜@J˜ J˜"J˜J˜%J˜J˜J˜J˜J˜šœœ
˜'J˜—Jš
˜˜
J˜ J˜J˜J˜—J˜——J˜J˜Jšž
œœ
	œ&œ˜e˜
šœ.žœ
™4J™JšœœŸ4˜IJš	œ
œ
œŸΠce*Ρcen
Ÿ
˜NJ˜Jšœœ
œ
œ˜5J˜Jšœ*˜0˜
J˜.Jšœ
œ
œ ˜)Jšœ"
œ	˜,Jšœ&
œ
œ˜?—J˜
Jš
˜˜
Jšœ
œ
œ˜ Jšœ
œ˜Jšœ%
œ
œ˜:—J˜——J˜J˜Jšžœœ
	œœ˜I˜
š
œA™AJ™Jš
œœ
œ
œœ˜J˜šœ˜J˜J˜J˜PJ˜2J˜2J˜—Jšœœ
˜——J˜J˜Jšžœœ
	œœ˜R˜
šœ‹
žœ
™€
J™JšœœŸ4˜IJ˜Jš
œœ
œ
œœ˜!J˜šœ*˜0J˜˜J˜$J˜%J˜
—J˜š
˜J˜————J˜J˜Jšžœœ
	œœ˜K˜
š
œ*žœž
œž
œž
œ
žœ,ž
œ
™§
J™Jšœ
œ
œ
˜J™Jš
œœ
œœ
œ
˜.J˜Jšœ
œ
œ˜J˜šœœ
˜Jšœ
œ˜—š
˜Jšœ
œ˜&———J˜J˜Jšžœœ
	œœ˜?˜
š
œJ™JJ™Jšœœ
œ
œ˜Jšœœ
œ
œ˜J˜Jšœœ
œœœœ
˜DJ˜Jšœœ
œ
˜!J˜Jšœœœ˜B——J˜J˜Jš
žœœ
	œœ
œ˜I˜
šœ&ž™8J™JšœœŸ˜&J™Jšœœ
œ
œ˜J˜šœœ
˜Jšœœœœœœ˜B—Jšœ
˜J˜Jšœœ
œ
˜!J˜šœœœ˜/Jš
œ˜—š
˜Jš
œ1˜1———J˜J˜Jšžœœ
	œœ˜D˜
š
œY™YJ™Jš
œœ
œ
œœ˜Jšœœ
œ
œ˜J˜Jšœœ
œœœœ
˜IJ˜Jšœœ
œ
˜!J˜Jšœœœ ˜K——J˜J˜Jš
žœœ
	œœ
œ˜N˜
šœ+ž™=J™JšœœŸ˜&J™Jš
œœ
œ
œœ˜J˜Jšœœ
œœœœœ
œ
œœ
˜KJ˜Jšœœ
œ
˜!J˜šœœœ˜/Jš
œ˜—š
˜Jš
œ6˜6———J˜J˜Jš
ž
œœ
	œœ
œ˜P˜
šœžœ™9J™Jš	œœœ
œœ˜1——J˜J˜™}J˜Jš
žœœ
	œœœ˜\˜
Jš
˜Jš	œœœœœ˜R—J˜J˜Jš
žœœ
	œœœ˜W˜
Jšœœœœ˜;—J˜J˜Jš
žœœ
	œœœ˜[˜
Jš
œœœœœ˜7—J˜J˜Jš
žœœ
	œœœ˜V˜
Jšœœœ	œ˜*—J˜J˜Jšžœœ
	œœ˜O˜
Jšœœœ
œ˜;J˜Jšœ˜—J˜—J˜™1J™Jšžœœ
	œœ˜P˜
Jšœ˜!—J˜J˜Jš
žœœœœœ˜NJšžœœœ˜:Jšžœœœ˜;J™Jšž	œœœ
œ
œœ˜Eš
œ
˜
Jšœ"žœžœ'™]™Jš
œŸ œ Ÿ˜-J˜Jšœ
œ
œ˜J˜š	œ
œœ
œ˜,Jšœ
œ
œ˜—š
˜Jš
œ
œ
˜———Jš
œ˜J˜Jšž	œœœ˜=š
œ
˜
JšœŸ!˜1—Jš
œ˜J˜Jšž	œœœ˜=š
œ
˜
JšœŸ ˜:—Jš
œ˜J˜Jšž	œœœ˜=š
œ
˜
JšœŸ ˜I—Jš
œ˜J˜Jšžœœœ˜;š
œ
˜
JšœŸ ˜B—Jš
œ˜J˜Jšžœœœœ
œ
œ˜WJš
žœœœœ
œ˜NJšžœœœœ˜FJšžœœœœ˜FJšžœœœœ˜L—J˜™,J™Jšžœœœœ˜6š
œ
˜
Jšœœ
œ
œ˜)—Jš
œ˜—J˜™6J™Jš
žœœ
	œœœ˜Eš
œ
˜
š
œ˜Jš	œœœœœ˜K——Jš
œ˜—J˜Jšœ˜——…—$˜>?