\documentclass{article}
\input camila.mac
\begin{document}

\INCLUDE{io.cam}
\INCLUDE{sets.cam}
\INCLUDE{ffs.cam}
\INCLUDE{txt.cam}
\INCLUDE{sql.cam}
\SORTS

$\begin{array}{lcll}
BAMS & \cong & AccId \pfunc{Account}  \\
Account & \cong & 
\PROD H \TYPE {\set{AccHolder}} \NEXT B \TYPE Amount \DORP
  \\
AccId & \cong & str  \\
AccHolder & \cong & str  \\
Amount & \cong & int  \\
\end{array}$

\OPERS

\STATE{bams}{BAMS}
$\begin{array}{l}
Init: \tfunc{Void} \\ Init() \deff \\ \rule{3ex}{0pt}  bams' = \left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"0636024550431"}}} \\ 
Account(\{\!\!\mattt{
\mbox{\texttt{"J N Oliveira"}}},\!\!\mattt{
\mbox{\texttt{"L.S. Barbosa"}}}\},3000) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"0636024000999"}}} \\ 
Account(\{\!\!\mattt{
\mbox{\texttt{"Neves,  Fernando L."}}},\!\!\mattt{
\mbox{\texttt{"J N Oliveira"}}}\},9000) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"0636099999000"}}} \\ 
Account(\{\!\!\mattt{
\mbox{\texttt{"J.J.A."}}}\},9500) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"0636055566677"}}} \\ 
Account(\emptyset,10) 
\end{array}\!\! \right) \right)
\end{array}$

\traco

$\begin{array}{l}
OpenAccount:AccId \times {\set{AccHolder}} \times Amount \tfunc{Void} \\ OpenAccount(n,h,m) \deff \\ \rule{3ex}{0pt}  bams' = \left( \left(\!\! \begin{array}{c}
 n \\ 
Account(h,m) 
\end{array}\!\! \right) \right) \plus bams
\end{array}$

\traco

$\begin{array}{l}
RemoAccount:AccId \tfunc{Void} \\ RemoAccount(n) \deff \\ \rule{3ex}{0pt}  bams' = 
bams \mapds \{n\}
\end{array}$

\traco

$\begin{array}{l}
AddAccHolders:AccId \times {\set{AccHolder}} \tfunc{Void} \\ AddAccHolders(n,h) \deff \\ \rule{3ex}{0pt}  bams' = bams \plus 
\LET 
addh = 
\LAMBDA{x}
Account(
H(x) \cup h,
B(x)) 
\IN  
\star\hookrightarrow addh (
bams \mapdr \{n\}) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
Credit:AccId \times Amount \tfunc{Void} \\ Credit(n,m) \deff \\ \rule{3ex}{0pt}  bams' = bams \plus 
\LET 
addm = 
\LAMBDA{x}
Account(
H(x),

B(x) + m) 
\IN  
\star\hookrightarrow addm (
bams \mapdr \{n\}) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
Withdraw:AccId \times Amount \tfunc{Void} \\ Withdraw(n,m) \deff \\ \rule{3ex}{0pt}  bams' = bams \plus 
\LET 
subm = 
\LAMBDA{x}
\LET 
b = 
B(x)\\
c = 
\COND{
b \geq m}{
b - m}{b} 
\IN 
Account(
H(x),c) 
\TEL 
\IN  
\star\hookrightarrow subm (
bams \mapdr \{n\}) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
GoodCostumers:Amount \tfunc{{\set{AccHolder}}} \\ GoodCostumers(m) \deff \\ \rule{3ex}{0pt}  
\bigcup (\{
H( bams(k)) \asor k \in 
dom(bams) \wedge 

B( bams(k)) \geq m\})
\end{array}$

\traco

$\begin{array}{l}
abs0' = 
\star\hookrightarrow 
\LAMBDA{x}
Account(
\pi_1(x),
\pi_2(x)) 
\end{array}$\\


$\begin{array}{l}
rep0' = 
\star\hookrightarrow 
const(
\LAMBDA{x}
H(x),
\LAMBDA{x}
B(x)) 
\end{array}$\\


$\begin{array}{l}
abs1' = 
\star\hookrightarrow 
const(p2,p1) 
\end{array}$\\


$\begin{array}{l}
rep1' = 
\star\hookrightarrow 
const(p2,p1) 
\end{array}$\\


$\begin{array}{l}
abs2' = 
\star\hookrightarrow 
prod(id,dom) 
\end{array}$\\


$\begin{array}{l}
rep2' = 
\star\hookrightarrow 
prod(id,ffAset) 
\end{array}$\\


$\begin{array}{l}
abs3' = nJoin
\end{array}$\\


$\begin{array}{l}
rep3' = nJoinInv
\end{array}$\\


$\begin{array}{l}
abs4' = 
prod(id,ffAset)
\end{array}$\\


$\begin{array}{l}
rep4' = 
prod(id,dom)
\end{array}$\\


$\begin{array}{l}
abs5' = 
prod(mkf,id)
\end{array}$\\


$\begin{array}{l}
rep5' = 
prod(mkr,id)
\end{array}$\\


$\begin{array}{l}
abs6' = 
prod(
ff2pair\hbox{-set} ,
ff2pair\hbox{-set} )
\end{array}$\\


$\begin{array}{l}
rep6' = 
prod(
seq2ff\hbox{-set} ,
seq2ff\hbox{-set} )
\end{array}$\\


$\begin{array}{l}
abs7() \deff \\ \rule{3ex}{0pt} 
\LET 
ss = 
abs7\_2()\\
\_ = 
nload(\!\!\mattt{
\mbox{\texttt{"\_bamsAmsTable"}}}) 
\IN \enlist{\_bamsAmsTable,ss} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
abs7\_2() \deff \\ \rule{3ex}{0pt} 
ioAwk2afs(\!\!\mattt{
\mbox{\texttt{"\_bamsAccHolTable"}}},\!\!\mattt{
\mbox{\texttt{"\%"}}})
\end{array}$

\traco

$\begin{array}{l}
rep7(r) \deff \\ \rule{3ex}{0pt} 
do(\_bamsAmsTable' = 
\pi_1(r),
ioObjSave('\_bamsAmsTable,
\pi_1(r)),
ioAfs2awk(\!\!\mattt{
\mbox{\texttt{"\_bamsAccHolTable"}}},
\pi_2(r),\!\!\mattt{
\mbox{\texttt{"\%"}}}))
\end{array}$

\traco

$\begin{array}{l}
abs6to0(r) \deff \\ \rule{3ex}{0pt} 
abs0(
abs1(
abs2(
abs3(
abs4(
abs5(
abs6(r)))))))
\end{array}$

\traco

$\begin{array}{l}
rep0to6(a) \deff \\ \rule{3ex}{0pt} 
rep6(
rep5(
rep4(
rep3(
rep2(
rep1(
rep0(a)))))))
\end{array}$

\traco

$\begin{array}{l}
a() \deff \\ \rule{3ex}{0pt} 
abs6to0(
abs7())
\end{array}$

\traco

$\begin{array}{l}
r() \deff \\ \rule{3ex}{0pt} 
rep7(
rep0to6(bams))
\end{array}$

\traco

$\begin{array}{l}
Init7: \tfunc{Void} \\ Init7() \deff \\ \rule{3ex}{0pt}  
rep7(
rep0to6(\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"0636024550431"}}} \\ 
Account(\{\!\!\mattt{
\mbox{\texttt{"J N Oliveira"}}},\!\!\mattt{
\mbox{\texttt{"L.S. Barbosa"}}}\},3000) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"0636024000999"}}} \\ 
Account(\{\!\!\mattt{
\mbox{\texttt{"Neves,  Fernando L."}}},\!\!\mattt{
\mbox{\texttt{"J N Oliveira"}}}\},9000) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"0636099999000"}}} \\ 
Account(\{\!\!\mattt{
\mbox{\texttt{"J.J.A."}}}\},9500) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"0636055566677"}}} \\ 
Account(\emptyset,10) 
\end{array}\!\! \right) \right)))
\end{array}$

\traco

$\begin{array}{l}
OpenAccount7:AccId \times {\set{AccHolder}} \times Amount \tfunc{Void} \\ OpenAccount7(n,h,m) \deff \\ \rule{3ex}{0pt}  
do(
ioObjLoad('\_bamsAmsTable),
\COND{

card(
sqlSelect(\_bamsAmsTable,\{1,2\},1,
\LAMBDA{x}
x = n)) = 0}{
\LET 
a = \_bamsAmsTable \cup \{\left( \left(\!\! \begin{array}{c}
 1 \\ n 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 2 \\ m 
\end{array}\!\! \right) \right)\}\\
b = \{\left( \left(\!\! \begin{array}{c}
 1 \\ n 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 2 \\ i 
\end{array}\!\! \right) \right) \asor i \in h\} 
\IN 
do(\_bamsAmsTable' = a,
ioObjSave('\_bamsAmsTable,a),
ioAfs2awk(\!\!\mattt{
\mbox{\texttt{"\_tmp0"}}},b,\!\!\mattt{
\mbox{\texttt{"\%"}}}),
sh(\!\!\mattt{
\mbox{\texttt{"cat \_tmp0 \_bamsAccHolTable > \_tmp1"}}}),
sh(\!\!\mattt{
\mbox{\texttt{"cp  \_tmp1 \_bamsAccHolTable "}}}),
sh(\!\!\mattt{
\mbox{\texttt{"ls -l     \_bamsAccHolTable "}}})) 
\TEL}{\!\!\mattt{
\mbox{\texttt{"(cr)Sorry, account exists"}}}})
\end{array}$

\traco

$\begin{array}{l}
RemoAccount7:AccId \tfunc{Void} \\ RemoAccount7(n) \deff \\ \rule{3ex}{0pt}  
do(
ioObjLoad('\_bamsAmsTable),\_bamsAmsTable' = 
sqlDelete(\_bamsAmsTable,1,
\LAMBDA{x}
n = x),
ioObjSave('\_bamsAmsTable,\_bamsAmsTable),
sh(\!\!\mattt{
\mbox{\texttt{"awk '\{ FS=$\backslash$"\%$\backslash$"; if (\$1!="}}} \conc n \conc \!\!\mattt{
\mbox{\texttt{") print \}' \_bamsAccHolTable > \_tmp"}}}),
sh(\!\!\mattt{
\mbox{\texttt{"cp \_tmp \_bamsAccHolTable"}}}),\!\!\mattt{
\mbox{\texttt{"(cr)[ successful awk call ]"}}})
\end{array}$

\traco

$\begin{array}{l}
Withdraw7:AccId \times Amount \tfunc{Void} \\ Withdraw7(n,m) \deff \\ \rule{3ex}{0pt}  
do(
ioObjLoad('\_bamsAmsTable),
\COND{

card(
sqlSelect(
sqlSelect(\_bamsAmsTable,\{1,2\},1,
\LAMBDA{x}
x = n),\{1,2\},2,
\LAMBDA{x}
x \geq m)) = 0}{\!\!\mattt{
\mbox{\texttt{"(cr)Non-existing account or insufficient balance"}}}}{
do(\_bamsAmsTable' = 
sqlUpdate(\_bamsAmsTable,2,
\LAMBDA{x}
x - m,1,
\LAMBDA{x}
n = x),
ioObjSave('\_bamsAmsTable,\_bamsAmsTable))})
\end{array}$

\traco

$\begin{array}{l}
AddAccHolders7:AccId \times {\set{AccHolder}} \tfunc{Void} \\ AddAccHolders7(n,h) \deff \\ \rule{3ex}{0pt}  
\LET 
a = 
sqlSelect(\_bamsAmsTable,\{1\},1,
\LAMBDA{x}
x = n)\\
b = \{\left( \left(\!\! \begin{array}{c}
 1 \\ n 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 2 \\ i 
\end{array}\!\! \right) \right) \asor i \in h\}\\
c = 
ffsJoin(a,b) 
\IN 
do(
ioAfs2awk(\!\!\mattt{
\mbox{\texttt{"\_tmp0"}}},c,\!\!\mattt{
\mbox{\texttt{"\%"}}}),
sh(\!\!\mattt{
\mbox{\texttt{"cat \_tmp0 \_bamsAccHolTable | sort -u > \_tmp1"}}}),
sh(\!\!\mattt{
\mbox{\texttt{"cp  \_tmp1 \_bamsAccHolTable "}}}),
sh(\!\!\mattt{
\mbox{\texttt{"ls -l     \_bamsAccHolTable "}}}),\!\!\mattt{
\mbox{\texttt{"(cr)[ ffsJoin performed at CAMILA level ]"}}}) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
Credit7:AccId \times Amount \tfunc{Void} \\ Credit7(n,m) \deff \\ \rule{3ex}{0pt}  
do(
ioObjLoad('\_bamsAmsTable),\_bamsAmsTable' = 
sqlUpdate(\_bamsAmsTable,2,
\LAMBDA{x}
m + x,1,
\LAMBDA{x}
n = x),
ioObjSave('\_bamsAmsTable,\_bamsAmsTable))
\end{array}$

\traco

$\begin{array}{l}
GoodCostumers7:Amount \tfunc{{\set{AccHolder}}} \\ GoodCostumers7(m) \deff \\ \rule{3ex}{0pt}  
\LET 
a = 
sqlSelect(\_bamsAmsTable,\{1\},2,
\LAMBDA{x}
x \geq m)\\
\_ = 
do(
ioAfs2awk(\!\!\mattt{
\mbox{\texttt{"\_tmp"}}},a,\!\!\mattt{
\mbox{\texttt{"\%"}}}),
sh(\!\!\mattt{
\mbox{\texttt{"sort \_tmp > \_tmp0"}}}),
sh(\!\!\mattt{
\mbox{\texttt{"sort \_bamsAccHolTable > \_tmp1"}}}),
sh(\!\!\mattt{
\mbox{\texttt{"ls -l \_tmp0 \_tmp1 "}}}),
sh(\!\!\mattt{
\mbox{\texttt{"join -t \% \_tmp0 \_tmp1 > \_tmp"}}}),
princ(\!\!\mattt{
\mbox{\texttt{"[ join performed at UNIX level ](cr)(cr)"}}}))\\
b = 
ioAwk2afs(\!\!\mattt{
\mbox{\texttt{"\_tmp"}}},\!\!\mattt{
\mbox{\texttt{"\%"}}}) 
\IN 
ffsPro(2,b) 
\TEL
\end{array}$

\traco

$\begin{array}{l}
ROLLBACK2REP() \deff \\ \rule{3ex}{0pt} bams' = 
abs6to0(
abs7())
\end{array}$

\traco

$\begin{array}{l}
ROLLBACK2ABS() \deff \\ \rule{3ex}{0pt} 
rep7(
rep0to6(bams))
\end{array}$

\traco

$\begin{array}{l}
view0(x) \deff \\ \rule{3ex}{0pt} 
ioAfsPrint(
show0(
rep0(x)))
\end{array}$

\traco

$\begin{array}{l}
tex0(x) \deff \\ \rule{3ex}{0pt} 
ioTxtPrint(
ffs2TeXtxt(
show0(
rep0(x))))
\end{array}$

\traco

$\begin{array}{l}
show0(x) \deff \\ \rule{3ex}{0pt} 
\LET 
f = 
\LAMBDA{x}
strCAT(
seqAddSep(\enlist{a \asor a \in x},\!\!\mattt{
\mbox{\texttt{" + "}}}))\\
y =  
\star\hookrightarrow 
prod(f,itoa) (x)\\
z = \{\left( \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"AccId"}}} \\ a 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"AccHolders"}}} \\ 
\pi_1( y(a)) 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 \!\!\mattt{
\mbox{\texttt{"Balance"}}} \\ 
\pi_2( y(a)) 
\end{array}\!\! \right) \right) \asor a \in 
dom(y)\} 
\IN z 
\TEL
\end{array}$

\traco

$\begin{array}{l}
tex6(x) \deff \\ \rule{3ex}{0pt} 
\LET 
a = 
show6(x)\\
f = 
\LAMBDA{x}
ioTxtPrint(
ffs2TeXtxt(x)) 
\IN \enlist{
f(
\pi_1(a)),
princ(\!\!\mattt{
\mbox{\texttt{" \~{ }\~{ }\~{ }\~{ }\~{ }(cr) "}}}),
f(
\pi_2(a))} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
view6(x) \deff \\ \rule{3ex}{0pt} 
\LET 
\_ =  
prod(ioAfsPrint,ioAfsPrint)(
show6(x)) 
\IN \!\!\mattt{
""} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
show6' = 
prod(
\LAMBDA{x}
ffsRename(\left( \left(\!\! \begin{array}{c}
 1 \\ \!\!\mattt{
\mbox{\texttt{"AccId"}}} 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 2 \\ \!\!\mattt{
\mbox{\texttt{"Balance"}}} 
\end{array}\!\! \right) \right),x),
\LAMBDA{x}
ffsRename(\left( \left(\!\! \begin{array}{c}
 1 \\ \!\!\mattt{
\mbox{\texttt{"AccId"}}} 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 2 \\ \!\!\mattt{
\mbox{\texttt{"AccHolder"}}} 
\end{array}\!\! \right) \right),x))
\end{array}$\\

\end{document}
