{\small\sf class} $GroupPhase$
\par
\kValues
\val{secondRoundWinners}{\seq{\const{A},\const{B},\const{C},\const{D},\const{E},\const{F},\const{G},\const{H}};}
\val{secondRoundRunnersUp}{\seq{\const{B},\const{A},\const{D},\const{C},\const{F},\const{E},\const{H},\const{G}}}
\kTypes
\type{\kw{ }Team}{\const{Brazil} | \const{Norway} | \const{Morocco} | \const{Scotland} |  \\
\const{Italy} | \const{Chile} | \const{Austria} | \const{Cameroon} |  \\
\const{France} | \const{Denmark} | \const{SouthAfrica} | \const{SaudiArabia} |  \\
\const{Nigeria} | \const{Paraguay} | \const{Spain} | \const{Bulgaria} |  \\
\const{Holland} | \const{Mexico} | \const{Belgium} | \const{SouthKorea} |  \\
\const{Germany} | \const{Yugoslavia} | \const{Iran} | \const{UnitedStates} |  \\
\const{Rumania} | \const{England} | \const{Colombia} | \const{Tunisia} |  \\
\const{Argentina} | \const{Croatia} | \const{Jamaica} | \const{Japan};}
\type{\kw{ }GroupName}{\const{A} | \const{B} | \const{C} | \const{D} | \const{E} | \const{F} | \const{G} | \const{H};}
\begin{record}{Score}team :{Team} \\
won :{\Nat } \\
drawn :{\Nat } \\
lost :{\Nat } \\
points :{\Nat } \\
\end{record}
\begin{invfn}{sc}sc.points = 3 \X sc.won + sc.drawn
\end{invfn}
\kInstanceVarDef
\parlinebr
\begin{insvar}
\assdef{gps}{GroupName \Gmap \setof{Score}}[{\map{\const{A} \Mapsto \fnapply{sc-init}{\set{\const{Brazil},\const{Norway},\const{Morocco},\const{Scotland}}}, \\
\const{B} \Mapsto \fnapply{sc-init}{\set{\const{Italy},\const{Chile},\const{Austria},\const{Cameroon}}}, \\
\const{C} \Mapsto \fnapply{sc-init}{\set{\const{France},\const{Denmark},\const{SouthAfrica},\const{SaudiArabia}}}, \\
\const{D} \Mapsto \fnapply{sc-init}{\set{\const{Nigeria},\const{Paraguay},\const{Spain},\const{Bulgaria}}}, \\
\const{E} \Mapsto \fnapply{sc-init}{\set{\const{Holland},\const{Mexico},\const{Belgium},\const{SouthKorea}}}, \\
\const{F} \Mapsto \fnapply{sc-init}{\set{\const{Germany},\const{Yugoslavia},\const{Iran},\const{UnitedStates}}}, \\
\const{G} \Mapsto \fnapply{sc-init}{\set{\const{Rumania},\const{England},\const{Colombia},\const{Tunisia}}}, \\
\const{H} \Mapsto \fnapply{sc-init}{\set{\const{Argentina},\const{Croatia},\const{Jamaica},\const{Japan}}}}}]
\end{insvar}
\begin{instinvfn}
\all{gp \In  \Rng gps} \\
{\pex{ \Card gp = 4 \And  \\
\all{sc \In gp}{sc.won + sc.lost + sc.drawn \Le 3}}}\end{instinvfn}
\par
\kFunctions
\begin{fn}[e]{sc-init}%
\signature{\setof{Team} \To \setof{Score}}
\parms*{\Lp ts\Rp }
\annlab[o]{GroupPhase`sc-init}
\setcomp{\reccons{\kw{mk-} Score}{t,0,0,0,0}}{t \In ts};
\end{fn}
\begin{fn}[e]{clear-winner}%
\signature{\setof{Score} \To \Bool }
\parms*{\Lp scs\Rp }
\annlab[o]{GroupPhase`clear-winner}
\exists{sc \In scs} \\
{\all{sc' \In scs \Setdiff \set{sc}}{sc.points > sc'.points}};
\end{fn}
\begin{fn}[e]{winner-by-more-wins}%
\signature{\setof{Score} \To \Bool }
\parms*{\Lp scs\Rp }
\annlab[o]{GroupPhase`winner-by-more-wins}
\exists{sc \In scs} \\
{\all{sc' \In scs \Setdiff \set{sc}} \\
{\pex{sc.points > sc'.points} \Or  \\
\pex{sc.points = sc'.points \And sc.won > sc'.won}}}
\end{fn}
\kOperations
\begin{op}[e]{Win}%
\signature{Team \X Team \Oto ()}
\parms{wt,lt}
\annlab[o]{GroupPhase`Win}
\Letbe\kw{ }gp \In  \Dom gps \Best\kw{ }\set{wt,lt} \Subset \setcomp{sc.team}{sc \In \fnapply{gps}{gp}} \Lin \\
\ass{gps}{gps \Override \map{gp \Mapsto  \\
\setcomp{\If sc.team = wt
\Then \\
\recmod{sc}{won \Mapsto sc.won + 1, \\
points \Mapsto sc.points + 3}
\Else \\
\If sc.team = lt
\Then \\
\recmod{sc}{lost \Mapsto sc.lost + 1}
\Else \\
sc
\Fi
\Fi} \\
{sc \In \fnapply{gps}{gp}}}}
\begin{precond}
\exists{gp \In  \Dom gps}{\set{wt,lt} \Subset \setcomp{sc.team}{sc \In \fnapply{gps}{gp}}}
\end{precond};
\end{op}
\begin{op}[i]{Win2}%
\parms{wt,lt : Team}\annlab[o]{GroupPhase`Win2}
\begin{externals}
\Wr gps : {GroupName \Gmap \setof{Score}}  \\
\end{externals}
\begin{precond}
\exists{gp \In  \Dom gps} \\
{\set{wt,lt} \Subset \setcomp{sc.team}{sc \In \fnapply{gps}{gp}}}
\end{precond}
\post{\exists{gp \In  \Dom gps} \\
{\set{wt,lt} \Subset \setcomp{sc.team}{sc \In \fnapply{gps}{gp}} \And  \\
gps = \old{gps} \Override  \\
\map{gp \Mapsto  \\
\setcomp{\If sc.team = wt
\Then \\
\recmod{sc}{won \Mapsto sc.won + 1, \\
points \Mapsto sc.points + 3}
\Else \\
\If sc.team = lt
\Then \\
\recmod{sc}{lost \Mapsto sc.lost + 1}
\Else \\
sc
\Fi
\Fi} \\
{sc \In \fnapply{gps}{gp}}}}};
\end{op}
\begin{op}[i]{GroupWinner}%
\parms{gp : GroupName}[t : Team]\annlab[o]{GroupPhase`GroupWinner}
\begin{externals}
\Rd gps : {GroupName \Gmap \setof{Score}}  \\
\end{externals}
\begin{precond}
gp \In  \Dom gps
\end{precond}
\post{t \In \setcomp{sc.team}{sc \In \fnapply{gps}{gp}} \And  \\
\begin{letexpr}
\patdef{sct}{\iota{sc \In \fnapply{gps}{gp}}{sc.team = t}}
\end{letexpr} \\
\all{sc \In \fnapply{gps}{gp}} \\
{sc.team \Neq t \Implies sct.points > sc.points \Or  \\
sct.points = sc.points \And sct.won > sc.won}};
\end{op}
\begin{op}[i]{GroupRunnerUp}%
\parms{gp : GroupName}[t : Team]\annlab[o]{GroupPhase`GroupRunnerUp}
\begin{externals}
\Rd gps : {GroupName \Gmap \setof{Score}}  \\
\end{externals}
\begin{precond}
gp \In  \Dom gps
\end{precond}
\post{\Letbe* sc' \In \fnapply{gps}{gp} \Lin \\
t \In \setcomp{sc.team}{sc \In \fnapply{gps}{gp} \Setdiff \set{sc'}} \And  \\
\begin{letexpr}
\patdef{sct}{\iota{sc \In \fnapply{gps}{gp} \Setdiff \set{sc'}}{sc.team = t}}
\end{letexpr} \\
\all{sc \In \fnapply{gps}{gp} \Setdiff \set{sc'}} \\
{sc.team \Neq t \Implies sct.points > sc.points \Or  \\
sct.points = sc.points \And sct.won > sc.won}};
\end{op}
\begin{op}[e]{GroupWinner-expl}%
\signature{GroupName \Oto Team}
\parms{gp}
\annlab[o]{GroupPhase`GroupWinner-expl}
\Letbe\kw{ }sc \In \fnapply{gps}{gp} \Best \\
\kw{ }\all{sc' \In \fnapply{gps}{gp} \Setdiff \set{sc}} \\
{\pex{sc.points > sc'.points} \Or  \\
\pex{sc.points = sc'.points \And sc.won > sc'.won}} \Lin \\
\return{sc.team}
\begin{precond}
gp \In  \Dom gps
\end{precond};
\end{op}
\begin{op}[e]{GroupRunnerUp-expl}%
\signature{GroupName \Oto Team}
\parms{gp}
\annlab[o]{GroupPhase`GroupRunnerUp-expl}
\begin{defstmt}
\eqdef{t}{\fnapply{GroupWinner}{gp}}
\end{defstmt} \\
\begin{letstmt}
\patdef{sct}{\iota{sc \In \fnapply{gps}{gp}}{sc.team = t}}
\end{letstmt} \\
\Letbe\kw{ }sc \In \fnapply{gps}{gp} \Setdiff \set{sct} \Best \\
\kw{ }\all{sc' \In \fnapply{gps}{gp} \Setdiff \set{sc,sct}} \\
{\pex{sc.points > sc'.points} \Or  \\
\pex{sc.points = sc'.points \And sc.won > sc'.won}} \Lin \\
\return{sc.team}
\begin{precond}
gp \In  \Dom gps
\end{precond};
\end{op}
\begin{op}[e]{SecondRound-expl}%
\signature{() \Oto \seqof*{\Lp Team \X Team \Rp }}
\parms{}
\annlab[o]{GroupPhase`SecondRound-expl}
\begin{defstmt}
\eqdef{winners}{\mapcomp{gp \Mapsto \fnapply{GroupWinner-expl}{gp}}{gp \In  \Dom gps}}
\eqdef{runners-up}{\mapcomp{gp \Mapsto \fnapply{GroupRunnerUp-expl}{gp}}{gp \In  \Dom gps}}
\end{defstmt} \\
\return{\pex{\seqcomp{\reccons{\kw{mk-}}{\fnapply{winners}{\fnapply{secondRoundWinners}{i}}, \\
\fnapply{runners-up}{\fnapply{secondRoundRunnersUp}{i}}}} \\
{i \In \setrange{1}{8}}}};
\end{op}
\begin{op}[e]{Win-sd}%
\signature{Team \X Team \Oto ()}
\parms{wt,lt}
\annlab[o]{GroupPhase`Win-sd}
\Letbe\kw{ }gp \In  \Dom gps \Best\kw{ }\set{wt,lt} \Subset \setcomp{sc.team}{sc \In \fnapply{gps}{gp}} \Lin \\
\ass{gps\pex{gp}}{\setcomp{\If sc.team = wt
\Then \\
\recmod{sc}{won \Mapsto sc.won + 1, \\
points \Mapsto sc.points + 3}
\Else \\
\If sc.team = lt
\Then \\
\recmod{sc}{lost \Mapsto sc.lost + 1}
\Else \\
sc
\Fi
\Fi} \\
{sc \In \fnapply{gps}{gp}}}
\begin{precond}
\exists{gp \In  \Dom gps}{\set{wt,lt} \Subset \setcomp{sc.team}{sc \In \fnapply{gps}{gp}}}
\end{precond};
\end{op}
\begin{op}[e]{GroupWinner-if}%
\signature{GroupName \Oto Team}
\parms{gp}
\annlab[o]{GroupPhase`GroupWinner-if}
\If \fnapply{clear-winner}{\fnapply{gps}{gp}}
\Then \\
\return{\pex{\pex{\iota{sc \In \fnapply{gps}{gp}} \\
{\all{sc' \In \fnapply{gps}{gp} \Setdiff \set{sc}} \\
{sc.points > sc'.points}}}.team}}
\Else \\
\If \fnapply{winner-by-more-wins}{\fnapply{gps}{gp}}
\Then \\
\return{\pex{\pex{\iota{sc \In \fnapply{gps}{gp}} \\
{\all{sc' \In \fnapply{gps}{gp} \Setdiff \set{sc}} \\
{\pex{sc.points > sc'.points} \Or  \\
\pex{sc.points = sc'.points \And sc.won > sc'.won}}}}.team}}
\Else \\
\call{RandomElement}{\setcomp{sc.team}{sc \In \fnapply{gps}{gp}} \\
[\all{sc' \In \fnapply{gps}{gp}} \\
{sc'.points \Le sc.points}]}
\Fi
\Fi
\begin{precond}
gp \In  \Dom gps
\end{precond};
\end{op}
\begin{op}[e]{RandomElement}%
\signature{\setof{Team} \Oto Team}
\parms{ts}
\annlab[o]{GroupPhase`RandomElement}
\begin{blockstmt}
\begin{dclstmt}
\assdef{t}{Team}[{\Letbe* t' \In ts \Lin \\
t'}]
\end{dclstmt}
\return{\pex{t}}
\end{blockstmt};
\end{op}
\begin{op}[e]{GroupWinner-cases}%
\signature{GroupName \Oto Team}
\parms{gp}
\annlab[o]{GroupPhase`GroupWinner-cases}
\begin{Cases}{\True }
\alt{\pex{\fnapply{clear-winner}{\fnapply{gps}{gp}}}} \\
{\return{\pex{\pex{\iota{sc \In \fnapply{gps}{gp}} \\
{\all{sc' \In \fnapply{gps}{gp} \Setdiff \set{sc}} \\
{sc.points > sc'.points}}}.team}}}
\alt{\pex{\fnapply{winner-by-more-wins}{\fnapply{gps}{gp}}}} \\
{\return{\pex{\pex{\iota{sc \In \fnapply{gps}{gp}} \\
{\all{sc' \In \fnapply{gps}{gp} \Setdiff \set{sc}} \\
{\pex{sc.points > sc'.points} \Or  \\
\pex{sc.points = sc'.points \And sc.won > sc'.won}}}}.team}}}
\others{\call{RandomElement}{\setcomp{sc.team}{sc \In \fnapply{gps}{gp}} \\
[\all{sc' \In \fnapply{gps}{gp}} \\
{sc'.points \Le sc.points}]}}
\end{Cases}
\begin{precond}
gp \In  \Dom gps
\end{precond};
\end{op}
\begin{op}[e]{GroupWinners}%
\signature{() \Oto \setof{Team}}
\parms{}
\annlab[o]{GroupPhase`GroupWinners}
\begin{blockstmt}
\begin{dclstmt}
\assdef{winners}{\setof{Team}}[{\set{}}]
\end{dclstmt}
\begin{setfor}{gp}{ \Dom gps}
\begin{blockstmt}
\begin{dclstmt}
\assdef{winner}{Team}[{\fnapply{GroupWinner}{gp}}]
\end{dclstmt}
\ass{winners}{winners \Union \set{winner}}
\end{blockstmt}
\end{setfor} ; \\
\return{winners}
\end{blockstmt}
\end{op}
{\small\sf end} {\it GroupPhase}

