From f2e424944eee5fbdb639c6a3f4f75e3b68881ff3 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 13 Nov 2024 19:57:08 -0800 Subject: [PATCH] Start working on the control flow graphs post Signed-off-by: Danila Fedorin --- content/blog/00_spa_agda_intro.md | 4 +- content/blog/05_spa_agda_semantics/index.md | 1 + content/blog/06_spa_agda_cfg/if-cfg.dot | 15 ++ content/blog/06_spa_agda_cfg/if-cfg.png | Bin 0 -> 21067 bytes content/blog/06_spa_agda_cfg/index.md | 179 ++++++++++++++++++++ content/blog/06_spa_agda_cfg/while-cfg.dot | 15 ++ content/blog/06_spa_agda_cfg/while-cfg.png | Bin 0 -> 13927 bytes 7 files changed, 212 insertions(+), 2 deletions(-) create mode 100644 content/blog/06_spa_agda_cfg/if-cfg.dot create mode 100644 content/blog/06_spa_agda_cfg/if-cfg.png create mode 100644 content/blog/06_spa_agda_cfg/index.md create mode 100644 content/blog/06_spa_agda_cfg/while-cfg.dot create mode 100644 content/blog/06_spa_agda_cfg/while-cfg.png diff --git a/content/blog/00_spa_agda_intro.md b/content/blog/00_spa_agda_intro.md index 1b9ff0e..175f258 100644 --- a/content/blog/00_spa_agda_intro.md +++ b/content/blog/00_spa_agda_intro.md @@ -104,5 +104,5 @@ Here are the posts that I’ve written so far for this series: * {{< draftlink "Lattices of Finite Height" "03_spa_agda_fixed_height" >}} * {{< draftlink "The Fixed-Point Algorithm" "04_spa_agda_fixedpoint" >}} * {{< draftlink "Our Programming Language" "05_spa_agda_semantics" >}} -* {{< draftlink "Control Flow Graphs" "06_spa_agda_cfg" >}}. -* {{< draftlink "Connecting Semantics and Control Flow Graphs" "07_spa_agda_semantics_and_cfg" >}}. +* {{< draftlink "Control Flow Graphs" "06_spa_agda_cfg" >}} +* {{< draftlink "Connecting Semantics and Control Flow Graphs" "07_spa_agda_semantics_and_cfg" >}} diff --git a/content/blog/05_spa_agda_semantics/index.md b/content/blog/05_spa_agda_semantics/index.md index cf0fdfc..b08ee5e 100644 --- a/content/blog/05_spa_agda_semantics/index.md +++ b/content/blog/05_spa_agda_semantics/index.md @@ -171,6 +171,7 @@ will be guaranteed to always execute without any decisions or jumps. The reason for this will become clearer in subsequent posts; I will foreshadow a bit by saying that consecutive simple statements can be placed into a single [basic block](https://en.wikipedia.org/wiki/Basic_block). +{#introduce-simple-statements} The following is a group of three simple statements: diff --git a/content/blog/06_spa_agda_cfg/if-cfg.dot b/content/blog/06_spa_agda_cfg/if-cfg.dot new file mode 100644 index 0000000..5a45973 --- /dev/null +++ b/content/blog/06_spa_agda_cfg/if-cfg.dot @@ -0,0 +1,15 @@ +digraph G { + graph[dpi=300 fontsize=14 fontname="Courier New"]; + node[shape=rectangle style="filled" fillcolor="#fafafa" penwidth=0.5 color="#aaaaaa"]; + edge[arrowsize=0.3 color="#444444"] + + node_begin [label="x = ...;\lx\l"] + node_then [label="x = 1\l"] + node_else [label="x = 0\l"] + node_end [label="y = x\l"] + + node_begin -> node_then + node_begin -> node_else + node_then -> node_end + node_else -> node_end +} diff --git a/content/blog/06_spa_agda_cfg/if-cfg.png b/content/blog/06_spa_agda_cfg/if-cfg.png new file mode 100644 index 0000000000000000000000000000000000000000..526320879886eeec52391e8a97376212fce10227 GIT binary patch literal 21067 zcmeAS@N?(olHy`uVBq!ia0y~yVA5k?U{>K^VqjnpIARmUz`($k|H*Y zfkA=6)5S5QV$Pepl`&IG|NZ~}dcz4lJHiKgN&)hYugVe?Q)eRi|C6Nay;xSnGlZ4JBL)n0TelmUPK*g+A%H zbLY;hD=U@fGHD#XySqI9?k?52Ow-&%Ef-mpzG`V}^IFbuYQog1r9VC-z7*MD;up=p zz_GZCf#J{!C58rrRU8ZoJz7jdPbg*y^8q_iQPI0Q3Kt)0|M~N$BoCWwpqH1|y4c-e z&ypd55`6e)LI0#llYV}FzCLQ}swGQOPE1f-zyDv=+NiBdoDT*DxEgdfv-5v@b93{d z_NPytR8&@Kc1@Z(_3Eb7(?;^f1rH8PnKDHy#iIC`PiAJO=)R3k@7}#TJImDgxWCw! zW77FGzg{k1_I9$m|2+HpfA8!6@6J)N;A_5^G36Y?>62&9*c3cy*uTF%BV)zR|7+sw zex@Gpla)5lyR$X>`ri1tw$&cTR1v#17k4Tpo?5_O$EOuv6>ep9SU(LI8 z>5^{rHXcbMm+vQ@JW08H%w4|LB=gdetbaSJzrE4a)Li+DUvu*E<;yMW)-2dn`g&XT z^>;5WE`Bxd+1c6lpH3(@O?(irLMh_Vp;m5wS*wy?UouP2Us)Oa``g>sZ{MzcXIb{< z#-UbjQCCUZs*lDZdTLIi)Z)qFI~R;{0u{7JG*-sCVum5cGmy@*YuIW zV_{c9AR{B==Vxaxznf`aUsqOEc70v!^D{G*r*bvuoLkVm^yu;9`8PHsetvfLm7KWv z^d(DF#HUOByMAM1^6@=;_RRV_Q!V%Qw%FZeYc1=H9?V#w#NpxLk#T?D-m1$xA3b_> z<;s=txXPtz|EHWe<70d`_u;~JIiutKtTJMuER6sD{rmj*QLhQ#JF9Sx0+?rv{y@6`u)J6=Cgx`{!j;j);5 zf}&#L-Cd=;QYIBY9=2bdd%RD!`uE%Itig;EoJ0>^>XWfFDt#5wd~m{y89OpAD!sj% z`t0oN^z`yQYypxXf;w8}=H*XLOk`zc1!d5Ph=}v^Y}Nhdtf{p`%l#eXmCIdkTWX7DnOrOXP=T1`)D{{4Kua^*^1 zDU*nOH9I$N-kiC-z5V#3quo~n1E(zYp8m=&iy`6u3Z;k>3!U4S`OZ$Wa=Ef1Q2Fh2 zCnu+6zO$FzHBLO#a(cRcw3z~f;hZzP-aG34{`&CnFgG`MeC^k(8#ZjHmN%&V_2uj9 z>&urfpM7j~`1(F+^Sr}tyx;y#w5BWl|Yu2oJ@ZiDkx$EA(diCq5c>I@FS66S@ za%D^U?QOa8^?yEISsAQ5T?K%0nABk611lIq)eg9o;O-02IZ~eVf=FY8sKfS29SX?*C zB;~|}mKK)cqf^}=4a9Nyu1JI|NmX@=l684iOK87|NlI<|NZON zvL#D2x-RXn|DQg;)=Wd=MZf*O9hINcrv7JcJY_7=>-Lgo!<;i`&M>p{{rLU6y{*kF zy)l%Vhv(1V@At2-jsAY8_VvK-kLrAV#b>*D}x;z8cM`0SXOZysMplenq^nJ>tMo#DtW0im$k3S_yxnC_KO*F%yMrnpI>KH_ow1=>&b@H4O&bK zG`cpGzrUA0zxG>x{qNiD@^w2B4l;?0$1Oip^y50411CTK|9`*VFJ8R3U(WW{s!;8h z76ld|f(%Q;*T;EJ*IWBRt+8QdfGdN@U3YONv11ztUyGx7A|J!=kdTm)$H#iPOaw4;K{`?b)+O#P#H< zQ&~4RrOxb^v?xgM^6~{77Ei%c! z_vdqMe1i_T1awE_v&}-1p?k6O+nM zPuh5;v&z}fD{T#Vd3o<6tP1T~O*hZZHqZa@;o&XYrAwDaZ_C;Fed5WJCztj1+x^P; z^yK6;4)z0F0j?WbTDisTzTHT^WgEQQ@9gQ*mr*L+FH1Zp>&)VB&{)MW?ZM;6n~R>F zirSjBvijUyYxCM)C8auAT2j_!Ie~$J9v&y2&#%{;DA*uDWEIL_86v2Yerk&5-QDHk z?u#$}c+{;gCMx>&&d%a{dn(zQ6E7}u^_^`d>cio{63TMAu&5|%PsPUV+qdshx3#T3 z)+71x<43o}g`b|B{QLX6cn`Y+S13z27YD}-^Za>b=l}ftym|BH-DPjB($C4P3}HwK zbltG!$B!TB^J~L)A3u6jRa5ii(bnpE2EHz>riPZ5mUg)+583YS?%?2H*3S$RTtyul z_V54y=jZ3G)oEvDOq@4QZz_9(&MFQgvz!|XWVyMx9zA-*#m&9+6N7+@sH20E)1h6Z zucb^fK72ULzuLNA*81DG+xgtfm=s#InwH917NxwpvXZS?(a^B);v&~&=e3Pyn&-zw zMa@buV^CV56cLh__wK|*Wo|C6xca|eH*DB2&$ilcjz!?#tjx^Jni^1b!79wO!DbbQ zm}%XgADh$9e|vE;`PrG7%WR9Eow-<-5to+sY>H-Z%O%DMj-m&P?Ee4xeC5g&HeM;6 z_ZS}E@*MxX z<=wGZd@=#0ihL^CCB=y}i5p`kS8&9*esY;@Xuon>TNsKR^B_|GO(I zCzt8y>B-qte7LyS{p<|>2GIpw33{2CnHx85+?;mSs8>~0HThUizApCJ^tAKy{yv+X|Ei3Ql{GabWy*hJ`yUUO^(;44M@B}r^ULSm*pS#S zXS-zcfubKR5;IzN@BYnv_x6cSl@8|D7-7hft-MziL)6dU) zcXxMnWu<5OMvcW6E1sMX)Yo4>O*h&reWl^{yt|Y77#Kq)D(@^W|k^bfj0N z{rvI6!@a>Z(6w)A-rZfLudhw@3!FSnH+tIq`T4iZBzW}qd~kAbXvk3V&bYkn?7G<9 z=jPdFOMQQHQ&?Cy*+3#Cm@)KNCijL!P}?gjYn9cvH#aW}R(S-9G#?a@m0jC6bLPzZ z_5b%K$Ss()Lg~haD_5@U*<*8g+rb10)2t~ua^9~lEdk>1n#gQoT);4X+k- zC9HmTXXodu;qfaU2m9Mz-BVe7&_=B6{h^Ha_x8e61O*4@-`|&et89zvM9+RX+bwTr zPnmM$5QkZpR+I0p>hJ5mX-s@~SBrh2_5ot&!2;Xg05_g-k!&|L&fN#Zjax5yT6C|?Kz$?u4>b2dh6-y zdsVMf=7Yw>u=R0!w{R=_Ep66a)RmB2;=M?HevOfVL4ZNOMe{*}q$3=qHnqRL{QLWx z^)o}LgXqCyYvT9E#R_S5J$m4+H2L1%YV+)CKC+P#2cHGFZczRC^XKbpYlDxg&#(F9 zU;k@zf}HllCr_5x7Ah+%KR(dN+*H}X?kak4TF#9P51*Z#{p!RdkEPKPs%mPR44QZs zb|n~dadBN+7rVMIc6Zs<&AWTT+b2(+{B7D3Nl8g|emRjd%r*k6ILwkCAM3rP8tCKG zlOUn}<&5!pliXV&vXduGVmZvf-=fu&tD&QFMNakArKQ~7O0stky?8#qJ}r?Y+EMhN zS)c*RCd1*Wt%AmX?;8 z>kWVXd_JFF)=Fgt`wEp+9A*iZm-*gO6;wYrb+P|^yIv{NAa^mh4V)o@Yv$&8URfEu ze8B>RgEnF3jvjTbKJwzp$;s}0GJ@3rjybm-6_DYKjv zecsdcM0vmpR)>XzY)LySRr=<}#>c|`Hi|QjtGy6&d-?LEd%v9M8Rn1IOSifk|qN}UJS0}gg$==$MsXXI&+m0POc;xM3WG`R7 z+%IphH-lY6K9uG4*3{F}R)?=&rF>n;b^>Uy;P>y<%I5J6ri;50mUeY_Z*}jywKeFKAZr(a1(OKVFUb8BsH-)zw2yPzwf7ow@Dx%u|C zTh&d&X8W9GVb>uxE#we!oTC9-I{h#q|P=XL!5T_rCkSsgoi^knKr z_P@Ws*S}cUex>kemuORBgHfRC2EC(4k7|dn3pu`E!Gf~4w>Y0|WQH2UC;RK=^7$;E z8NM&-N{HQ-e}7%9P_Lx1n?cXrif=d5w{kCj@+9S;!GXOilp+N0PFhj=`r6yu+r`f$ zn`d2JB`PYqw2z%n#>3xV{0#Gp0M`vl)@5%_oI4kG{NiGF?zWA_%xpX>;`i^f+GNla zy09xj*UQ^Gd~MXyzJB|E703HzSwG*H8MQUb)y-|y<9_>pKThlK=Xl1rWrb2ix2$zp z%#H#_*+`+QJD$(0_S_T_`To4>cb0Dtbp*dm;9a4_p{=WX z^vD#-c9*|jzyF`s4EBH(N*%ZNR&Ou!G^zTMG0o+fn4sXp z*RNOi>GUY{X*H=VzPQ5H>&uPg{?eD1Tn+l03(Cvotx8r{y}P^HTv^%KfZsvX@zT4y zyN!*FuTE5*c$7!ZCL&fsve!+_4b+6{d1s!`EvCDx?5);};|pJixn*W%rk|fDdWMQZp{UMAqJq&aWi zJm)r^z~i>n-!kIm8N{4L9S?lJU%$RqzeD&r3$L8bjoY_xZ#jF2BWQ(E#H@=MSMIeM zD<~|e{{F71QfAKd>C?Y;Onet3bifEC{cca9-yC7{k{1DBj~!f8vj3%A<&%kWwpAR@ z8W(BA#lXm<%~KlsuRDij@|vO_`L1%zWa5*-~Rmkob~g8LQv};G>kAkzAo_ijT;f^ z>FEb;cFbR~LPN|A)X~WyCp#)WJTHATg+@c z0mo&n%Tm(Qxt}#EFX&2$W9OIi@%Ilu{^CW(G?#0j5iL16xn*x3Jxc16ICy7;(v0cf zj_f?vD{cSzjB!(9fakt_`_9|_USpMaf8XCrOTC*a6TYudnsITVb9>#dm+GZ5rdcB1 zO3{WnHw?_p%`cmAE6|paH-JY=Zak{hF%X+k$c4n+s{q*@WH#fI1PqWsF@b&Y)bzHo* zHd;S^pUw=hibxsTswt`yWhLxtEVz{;7(!V#U(oIR_3f>;1Y0PmLjL#n_v**fbfY6A z4$7=hy0Rzvc%Q6&U5u=IpUlZgC(3#y44rlxL~Ty%&5^sIx{AZpf4553g#`!y|2hAk zqs`Iu>gw?I@%!su?SPc>T+bR~7j*?3zI6F=zpVALzQu06MWv;pXPRG0n`TYfWuT>{ zm6X^b5H_m&jzHX`SpKYGMuk7ut1i2gXt2j(GZEgR8#$qj!j&MwK z`R4dL{Ny1H(>^UH->7XlGk2}6*5sXiZGj{6TR~+pw-u2gf>~!yPFClaw_DS9idYRmInve!kv%(?t=53jV@ogIbF2K;Z> zLR+LJOq{qdRwy$+hRu5M-nk0g%2z~IahNI?8eYsWnYFESdvV*`i+59M54Z7}=id`K z!~EMpbm1-|BO^W;iv@kR_;)tOUefE~;^MNH%6HXWbm6XPda?Mi7l@dcLnH5N=n-Q`?1(+lS+{QC{WAF%yOSUe_niq8KA1cmZpC%$JyEay0 z>5?TUo;CU|?g}Wqr5gD5)>cceCjnCCd4IlK_Fw(@dVKxaLmZ)Qq6@pu&9VG^nBRWI z;|+<2ZES5>KOgv%l$3O(_2S*#<@FK=WZ1#i-H9?auIQlkM&l6 zeYLc2<;s;hJpra6f~%B_jf>yk+xtpFRP^Yi6NX2R9m^7TTe))OrpkoHE0jW7zeO#& zwKd!R`<>!Vl?qEeC#&shz4-R__NR{ygax`*B+Q&SGcz;um4u|^$w?xv=(%IIIzXNbI;zrmR?UD%reQmv^m|s)W_HN?CI0OXPBd1L?0eZNlUBy zezzQC#LKsDb!V_&Q&3YomS8Yr+y5Vr`THauItIE{7~E2wIDLA!i%Uz6Ttsubd|kwD z120d{#KabMC((zDfByY`uhSWzcK6VW*X#FBJIj0f9Jz>oce%}DrP-zOw$yu|@;MD2U(fjN6=E&U;Sj91QX|xcp zq>+mm{~BKh2Z!(P?p`gtyQ@^EC%`jAQ0wWTR_7atsKjud(rx7fY^nqH4t-W`qE z?Aw~OoR+Gns!p9YZPqqhTiZyXg+7dojCXgH1|KhdeeLefVs``n9M;g5uGl>lh2P)Z zePvPcAwgbVey7ETtmI=of#Po4^X}f-kl36fcY|dWhp4xgmzJicVQzIr1*q0E<6jf$ z;Ba8Fzun5d?Ca}N6I-|fT~{19+AUuG_SVwAW;WhWU%!f;VSc^bcIvxpYolchomy8Y zg(Up^^z_xF6L;^{zPPY(Q)R;6s4W>6w`PZfQZ-kgtHybd0q^dt>}zJ{PxEX!bzz>@ z^x3m_XI@sjX|tgyMDWz+q@!HZTvjw4m#bdmJzekBjunDLB;9mOEI_E=K0gkGH1JqKHN8H^5m`Fi%y*IxM{ONx3RHtu623XantN; zA|fIj&l*h^cLi)aJzf9(jg8K-^Q+(Ov?_hY@vKqzQe5(s$&(KYD&OG`ZP~OoV&kG6 zJ8o=w`|O#RsHo~}_H7!F){1PT#KXE3N>d)5nyP(!dw%%wMrQU+Do$6A96h>{d$F{6 zUd`vT=9?-L=B`kh;<#I7Rp@Fl_s)RS#>Pfj>#~sJp{v6-8XVfYLg_{9&Z4LB|9?%l z;*+reO{FzeCcJj*ms^{+*}!S$3Z)loV|E7ZR(Yf$xa#G{gt;f zn#4j|{ue(!#`|{Ci<{~5YhNsEXZd_!-U~6eTlJX?p)LP6CmroNbja!Qw$-a&Z%90x z^7+6#7FO1++1LGKLCwr{`x#ep{9jnT@YeqN`e`mJA`1%(Uu}E0LPbU)q&Z4Ei zzU^JT`t^s0hf_Zv_{RcnW3NswD%w=FPEAH8l*Ki0inMuN&dp7(vWLOVa)lY}-?Yrk z!tU;?`l_}3(!mz3rbU0gFO}2N)00tcn#sb>zCHJLnCw>ZjRz+Nx?YH9ke8Et_x`>9 z4EArnyA3Ygy~WJet<|&%G>Sf{W3h|D>aw@Dwq{;-lig}=({gxGm(00^&h0&Ji>;nL zd6Hotw>f@)ola*$-mcb(-^@OAEt+Fp{_fONZ83gU&yb19ntFP5k9*CJ^~>+C{aqHU zm}&3SrYfkjxc2wARK1=}n>IZ=H`hAv&W3)g9DAXR0HqttCcp((U9QpQ?|1D_4RtZd2al^n#!}YOrM{ddwXYbdS>RzMHCbE zFJ4^z_0`iSN3=z+Y%oqgr=qI*_U`WOf5L5+HP2#eKA3b+q5HmR-%=xev(1|}?fd=C z`trr(1!;3Fi_`A!s})_hhnt(bxTr`+nDbhLR*}xsm5c7}t=|9jTC|?tni+wge|>vv zoqNk9J^eYC{7KIezE-Uwg`-E0USAih{ok|+`04b)Aao-OFm?ar(7Yp|9)s7l2nHIGn1?^M;v;M(W3cg2YW1D_cNibh63R)Pz@-$?GS z{d7|O>#M8Ay=%H;jyK0Xnl*WH@w+>g#;%Q#e}BDR-?d1Br|n=f`}T~BkA8f7e5v!y ziQ~tYSAKqWN%PDh!FkR9fA9bQ`>1&Qon57`pPZch?Jxh;KHC??9}ce4FgO2xWo0nG z1ZUX8>G5@j5+j3p2Xu|V^ii#i4&dxqR-~K(v|BYoY9p^WP z?)=!le0ln0HQ!YqdId_py}9}DaC`Zi8-Z3Gm3McQo))}!wXo$ms5iFn*Q?bB4miA2 zs4xhv<_lZeRZ~;b)YJsh2AcEys#{?_ZR*sg9HCDX&L6zCHro1-eUx?Z*5?Y#buGB& zUD{yzXK|@ah#&)b3tEP@M$mE`z3FBg?r=+Cpt@^rTGXtNBzW)0sCnqoWoBQeO zSJ0Y*fPe{;h4p`FJBZ#~$Stl{^W~y@x48bf^XK1RTPq#P5^?Oj{r^ALqVscaZ8@1? zvdVh4c|NH4u>b$_{JVGWnr^O<2~7z%GB&pV^Wkvn>1m>3VqWQtG9I3uC$-n_`P5(k zXYrOTSI(YY8@)Ymu66mjlP7QPEKYZGI|iE5t@-)s$&)9?0a_^nD|8G z%kEZ!4^~q)+=59 z?#|6Eu|Ywfp3TmmWj<%^!mc;IZ*Of~s?5Nb`0LBdSKHRF&%eDb_jG;Da=*D(-p;iy zPfJUir8z@)QP&$^(ApzqhHv_|wtuh3*M}a@ySpp2!kaZ$RI>Njks~g~sheFxChjdP zEuGrOaAW`4=35wcj<`wQG@1?5>dNU^aGl(VNm=FK94)zPT-Tc3IA?Et#$N zFD-KIwkmzK;&Cgt__;Zj!Jkj&OrHAhmX?;*uENJ|t^A)qe>Rrj=~^^p%9NPhWoyqI z2aPWM|HT->cK%?|oqe^|y1Kr*mm8H=nMm+3GBUdN%Y}ZIu_}47@wnXTpEYJDyjH(> zaIpF5{Jx|~lP5oZ`gEy=S6Eos>1n#BYt9^KWcC$zvR`4Ges0RNX<-kgwV%9ucW+Ik zaq*v&1wB*Hwg%1z6hg-JUZoH($#mj43_vc5S zthHI*ogLZN*Hz0KRDXN(e184CFERllODjJ=+yC#^>+1J=m)i$B!4w^2^)BJmo1nR@E=MHS22Dqa&TS zx8+v9TsplZzNn~ZmQ7{R;Wpl_*33*yYCba-^c6op7rVPGHzZ`ryZ3Sqsvl+c%zu4- z{p)X6)<$nPy8q(!>(#RQF*^d1XXebAx~^->v$M0ypPrfu8o90Z^7h`IbJHm0guq?p z$&)AhO3T-Nxwyo0@~WTDLBl^wmMocNzr<(Wym`-lY;2hMLFUTNs;{fcN{WhBJvnG_ zSGr_--rZGxJk?3ep-VJQ5w%KcK6BS17FO2K|LqLl8lNwiwyx{dwYAYF&u3m;+m&~3 zPvqo{IWxcRb6o!PF=#s1>+R9m&(F=h9QP_FB*dib&5cEi7EPEi;k^C-7$xO|^A&tq zFVBgt`NOXIdYyy5me#K7?|HpPH>GY1bnRNi!p?qvo^AAQbw$O*`}=B_y^Y+QCTm}} zr|$2s)#2;Qii?F$u-~wr*Q^yQ8v1Dtt7~A%^Shc|K>+~)#xrx~oDG?{NF#We&&zvz zcUwvI9utqR*|=gw#`AM?KR-KbEWy()rn~A)YZ}9_xCsVG3GaN=N*M(?}q(b{GlW? zWPP0NW!6I*mTCows46HV+}l%m%l7m0^XJcp7OiOM)2tnx8KyI`6*m$&)7` zpQJy3{=7B$DZkN8+uIh+e%f|+b%)z{XPf7Tec!QThl;A|)gODWTa~@ZSk~{Hdwbj4 zTU)cwew@t6{lGHfsn#XiPYc`SRu!>XCs&6q(eQF|a{B%4?N#OWqeqXfT)Fc5Z;ks} zr_Y=*xjgmWpWn@Ei$6SHu&zt1-f!ExiBs+GAAEN+MfB(I-{oeV+)NSG?Anxg znC)#uK!AX_`1EPh!kXn}!j-STVElG!;{4|C^HgU{p8WXv^YDk}Y3b?N$4}iUxaN4{ zMkco!Cnx9YYiqMFEI4?W-+s+Io3b}IZs+gUoxxQg!}m|-&*l05mRL9LHfrzY;^y8O z`sB?U&?Z}ZMuH9mp{;hM&^X1C-u$}3BzF_w3+Z}?+ zTdMoy?c*Mnr>3T6+J9D3QCadyT;-;%^y)=-?%bKE>@FrEvghBg*NKUVw$87|T9qS@1#T&;O&xk7pk@vUhiWer09wEkhlhHEqT>jigsE`uOpnz-#)v?jq->k1 zZ#ON~`t|4Y`QYGSX_Jf%H9w2e)6*~e@$>f|?G|6Xc#($pbiJ#x0jvSa6?|EsSiHU5 zfBwFTk4ZoKuZLZ{>~DW}Ww5$2>tDDWixnD#`$SC)g$=i9H z!fG-5YHn^~T-*ANdB)iF0w$b$zDezy+2a`o!hZvA~1 z>Z-18%e`&)??K3J4T93rOtgxHc{QdLv{ePB*t`1xFw)FM2mwM7cQ>RVSi`#Q! z%iDMF{++XaAE7b-?S@9JD&(pBQ#-5HWnW)6apJ^Vwwu$=-r8Nh{^sY%ncU)f8OOQq z?`P9GQv9Lr&fUAybt02?{fu*TY<%~5PRQo;^LAx#W-QXk%gcLxZ7nwk$A$#A+X-(& zzx@0CzW&$Cv6`@Fhg!LRe}8}dou{AQvjV|Y z&Ce5lT9v)ok#p1Na%}xHoybWOCM>8vVE^x9|IXs)T3wHxJ=<3H_SU}I-&{+!RGs_2 z`lHd^J(Zsy9qqn%?;dDLZ}gJ?9^T%w?P`BDv2yz?zL;TC@nJ!K|M|oG_BHQcZ(6fv zP3Y>d+AkN~cm4kH?D_Nck(-}wzh4&&Zc$C$={e=>$@8G%<=@}$_dzv4-JgoPt2C6A zA1|L@_vzCoBPr0@gj@czHhS;ex%1}DoA>VB>$myTQ6jeafn`Q()b_l)D}$GReSKYA zR1`Ez2h#QNqo$tTz0K+8r)UQI{AZRn&DxT4b5q^lU!LuzyI0w=^YWL(7$UD-;Gg$_ z@yYY&*Vo1FKBIqjp6&0m=J&6><>BHwb>f7^|Ma>K2ieOicOGV!uUQcHFmU0VIWqeC z`kS9koC;nZ{;-W#`rC_(&Q{%#A7r*frJtKK(>VRys?gOX@13u#i~W5yJbtc8=A`Az zmxq{nuew!y!7IQ0)w_599G2HDUA}y_e$UkEzhAG%*Z(bjDYC)bhFw0STTFMFPUNR+ z(fMz0Zhj6L^*nbj@8+h|f`WpK3=Q)iD<@116J)rtNK6+rh~;F}`gY^D%VG=+W&J~O zMLOB*>0?%Xu-y(`q_O^^#)h8D%l)4}e{TQri0~!HGmoyVjlLwPbFgoIvw8kKAAkS% zmzH*SdxzFpJH}j{*Btuu^gi%P4L8w!f}7UG>@0e4ppjc#ucE5T%G&yK$oAN>KQebV zr=Qo~|7TP3@jgg)e|+xTxl5f1oc!NTpSXT~d+Obj z-F&^X9i@#oJq^!AGAxeF|EpbNck^`2BU476yp&|B^A0=yfx8 zZQNS<`K&p=j77q&Z(qO0Zp)dueEISm6^HD1cXnEry)nq$y?eKQ^tLs5cXw@?m>@Z4 z+XIJ3k00~0HD_9zo0tFn^>tGv!`jc!&%eL5)mv6sN$G{+aYs?h2?q`wxNsq$G-h*} zZ(Q8G1UUz7L&J?rmK@pg_TfW8@Cf2G7g0;Gw}&+J_4QR%UCsCtCe56=GyS|=sf<<0 ziuLQ)C&)!egg%L2Vq%(C^-8nU$J6uV*|VZ&m}lrjZgR2Bd;9jSZOMy(n>HH^R-JeV z8g5iSac^%mc!6$ZLr+gn?eA|ZK?C%A_U;7@(63Nxzq}>$^1Z#)tHIL&MMW&18M?*w z!=}6J+qX|pP;gUaLS@KA<*x4T;Pv@u&!3Nn%#m&S^5si2JO8T39fHa`jvZhObnQEF z|Nj2``}oE?W7fjkB=oLCN@1qN}Ux%J6Nk z>l_)(}Rn#bPvDD&Q)%6>Upmd^*I0$c;y z_++D&`^kbQ`DVXkk$iji(ZdZZlr-ez_-aS}|9_L!{kfhs%3h8&6OfR&u{AsV zpv?xM5J3^wKsH{fko|SFr7^ooRwhW?FuZ&83aE$ct)vkm=yT`Joi={?b$#vp^4IS5 zv91u@745^y%3AvBil+hp8urkZ{}KiX4$W-5R|2aido6Iwxwj{>`tjW#KPnCyY|si3 z{CD{3)zT{~0$;7zU1}fT%gV~SI(&WDaXwiq7SMu-#?XabAL@U7eSLjJpmOPzx&@K} zzVY>czkYpv{c7Qv8HP=X3Arnj{>Y1qPoFVEqV&v(6F(ld%d>nwkoUrF*FMlf+UV_K zXPC2{MIY|}^78WX$jxc5cBGsX5_4OzZ_1P@ckaZ1)-iST_D($uQDk9hnOX1q=iBZ4 z>ThoZ&oEn0m_B{_q)ChVKpTW^Zd#fk2O8C`+FSLt>dQsE~%irEooxyIV3(2XkZtO14f6FaY>>+&Ob1gckaQ2%cIHEdiP*`Tgx}Q)R;9ygNHK7Cv?> z<>BVOJWqsq#R{b>eg{ayC<*2=}-MD+p`-+Ju| zTN|b9-Zuq2f3eU8GPYh@zd&ZXe*87L_$zmF#4jxD3YfQG!GZ}B1WK>W<7J(qY-kv0 z`})$|yS1Pp!pelFE0jVUepjB~mF?1C^m3hRcSpyH=afov8@bK{RhPuC< z`q^RTmhu-LK78ot>Y8+x`L(;~!lYZR6W`S(HTb2aE&H~w)w!MT>sQd6&TI$Kg-MKz zjQ+M?r&wjZ-^BAGV+t{ryJLVd}(*8}skmmCBgq%-Ftt zdxG2zu2mdUFQFGg2dpyfe_p?S-CRk@$qYOF!%ZM=j)@kdVwavs;Yh+ zY-Yb&c%(yc-n@BDl?l!(ltQNM-(P=!U+vYx%gcPj*T;#TVa}dBW5$ZS>#M`_9~@{b zicCmep=8s5UJ^z0qnAVnwgtFWFx1u6{r&wt{P^1F?P=+tx&N;oUS2`l|Ni-N=aco}Nzq><|_eb!%nt@+*dB zW?{CMg;uDn;^04X{d)O@1&*&kV+xzo&vQL%RJc3Iqx`QVX#Q`Nl9ra&-mbXsr#bji zzrVYCOI+#W$B(aKEgMcP?g|jyRo(sa-lE244PD)<`?wILQCXntibV^Z+pnz*KECDb zp%aEL{h}`3J1ASB5F)th#NorrMn*xh-{0S_|MbN3pv?w@yDR@RHa5oYE)zY&Jljol z;VabAC}PGtrsvP+*UwWGT-BrHbam&>oxGq$U!b}7y}r3RfYuLA*NHrI z=tSJoB}<+>dp2tuFPn2t&YB##8|G@mx<@Wn^w>PKvC&gj1sl?mo6l&88c=?1O+M0V1KqD?d&Y*BFzi?47o$tLtADo ztX}`@&(F`h%iao|X_f*_ZPxv*Dt&Wz_x5i`*#l%l1hag$=iQCknzgjg)6?_l(W6b3 z0h`0tMwLE4CwqC@>zCahSSoH`rD2@zJ-pw^=_gV7t4c5VR=qm4uksGTT7b z6>6(EOjn{8NRGaq=mpZ;gB*3=ZGg4qC5f zU3z8TthU}u>+-U%t}-op0-8Xz4-w3Yi;0=DYpwM$hS|kGKc&7kw7<(+&?x07y6_n* zD{E^@%ZkO{&S>A5bL5E2S09h^^6!GmZYRLYK@!Anou76swx3CQ(QZ2(C8b4qcXu^a zCahnfG{ZF^At57Ug;m!2OYOWD@0lJxd{|ja%gc=ajc6!K@kPC!lJ9!Wz9-I{xpL3j zz{u#*_3PmV{BI;eS&BJ1I4WMPTz)06+CBXS%UjuNd-v{b=aE!`ER2yndi1EJwe{?6 zrSprKwWm)+FOtkxaim>AFOn8~+A{yx>({TP1qBsnvw!Q=YN|YX^ytnVJ7#SA{P}bE z+9=i8>{BPsn^*VYfn%wRVN%QT<;xS~ZrHBkc=q)D`}^DT<4f;s$-I1ZbvWzi1x7-` z!dKr`eSO6%V-cXoEyEPbvbnpjudKAxG*?_qOif+=^fSkweKM9sUtR>3_Vo3E#-z?L zyE}*;e1qONYW}3Es=D%aU0vP7hYy<)L2H{L4y_1Wd?oza(W6JT!`4hV+x+|H{`&u& z!s=HH)zsW#FETxI7Ck6ba$I^_{{6alcPtOuXiUDCaYe6F$~;d-OiXPCdtb9wQ)|Zg zLt47JvHNOv=E&XAMzoGr&-=?ULo}3y`{UQIvL+c5tUx1CZ*FdGs$8%*TIl6EPUbUR zT1`(~K+U5!uj@WK-g$R-_f~zrM~@$0wN7Pt<|cZuXwTlgpgmQ6yS6tgtk|+8xnMa;iU(dRwzYGX>WH=Nm*j`?*9J&Pfkv5s$6iV zxT-cGA>sPESk}*=w&;c}j?HXW*T=`pPS=aol3+V!D=usQ|IcTg&Vy5`$Q9K){BouUVyUE-Z8|DAFI&0h8Ytlemo3X3|;83tH0v?rKR4ludQYMd|+artH9;u{`1q$ z&RY3+lB#!vL}ZYcmseiiy3E@N21kw^JN2wld2yG*F;Ic@`aQfrYM+GOI#WAVs z>#MIX7Wc18PD)Dh^z2NKJH8RQJc{IskPBt;-1WWn+RR}|iMfl5V4+h|6B>jp7M+o*yq>&Vm7 z)3+XfSYp1El_k)1gP5bEqoShXs};7VxlNToZ6oW8u(lCsC9C$LzcSf(x9YD@yK5RP zC@5I^`kLq&=8Qns4N8rTjSCkpe6?b)GQ%p*YISaY{{9s!G;Z27h=sDeUKA_w^4;V% zt;=`s>%&T+1OI}!ix=)kL^G%jgFTsUA|o2rXoPry+`8V%a@un*foShS+YTk$52Y6 z8|#i7aVgy$x3`L!oo~u%raR)HEZU;7vTt9#%DSbeqvPY}H|=b4H%4i6hd-1>`|0!N z*Z0@gm)_Y`nq5}5EkQ0CrK`qx%2D)S6}Yb^8V~EMZA<?5$Pxw>1fJvlm1QndaWwQvUv4Q)L5JpzDUR zz`(#)cNt6ervxs$ySqG_+uF`9Zf`X!Xe~~Jb$tBbl4m~Cuql$4dP2A0n<3fUEWkC~ZyH)!E7 zc$NOP#0v`?zrMa6?(Vl#d-6M{2axtr4pS)0?FY}EnbrI#D7C5ivEkb^vw(LyZ9%gP z%l+oEd}f&HE_yJHN5Wu%V>8>U6?-qLi@4qd6-LW8f(xStb|=w;X*+i9>XS0{k}Z|5 zU!ZYHfB&CH7V~qyJnpxjHf73+WJkw?udc4Xy3x6v@8H3MLOUB)E$B+{h80gC_9A-5 z#-Hbw->dxjbo%)@mdex5ExK3x{jOp1v7CE*c5c}c5;z6cpb9_UBdILTTaj>wn`PS( zaFgoU;(j}$UP(zwY4f~4KcCOv|My#TuzKvCia?VEt#|fRem*zXy8PXppI1n#Ul58vNR&i{5^6TsC z`L*97otzH+m3yEN8ggzq$2^e)x^a$9L@55wjqxXgo{C)?(f;__a0O4INbK3U({?_`1-iKyu9~&KA-#B z*JM#4YWw@m=E-Wln|=$MC!|+2^KDZ%G5PZM`~B}4#ds;>k zJdclq_7~6bkX!Hzv=8aHTy@UBKR<8zmz!>U-#YQ#{&NWid;WYn9T*rGRN3%qaaY1^ zxw;<@{q24(Nj%(kYi?PLD=RCjdET7>_w@AVnU|OGN*Fj82nE!J2Y8Pi`|9CC#kq%iK%2#Weo6(MZL;cw;LjgFX7sIOxTdD9 z-K|yRFlQSB=|`{(?G-Cja{W#Z_J-P1XV0EJe_sE;;k|qJ;^N|_{*MzEpAISqee4un zU0u!d?yUHbSXWoa*6bKKWzwWcpq1f2CCtsYTa~`LQefx65z4ap$LIO~_oSVjRV0^S zAdz-<*4JmV^TYmC&#!pYdAOZF-0tv9<8&`?Z|(m-P8FAz=U-bBDY_3d&tqHtZOw;7 zOH0dTlg^=SvKBRB2s@ErBDK``K#`HLF~5w(gZJ;{rKGa1*=v}agT`&S#dItxKP`FZ zy>H*X`8A(B@9(Sq`{&Q8KXHpMR(ySRwUt|Z-}igf%WO+uU;BIe{=aM6^Y8B}eH~`! z3_WmV>z}9GoSdHC-m7nY|M%&%zIEA~8#@XguZ!LN?(eHNH#g6(|M#ok+Jdp z>i2t(9C0c2cX2tgA@T69udkm!ejL1&=bDbT_UjK15A#Z!y}7u!y+ka6FZ4--PME8j zrKP29^|wDyr^j!xj<0^Z)w1|m$dA1@Z{7sW2rbf>H*enky5G6S`()+6_-{X_6}0!) ztJU*szs)S`pFBC(&#$k&z5U%p_dc1ImzH*CR=>NmbF#Ysx@YpaXICg4KO$XXuy|ML z>vgfawe2%KVD{cXyWDIuVR8ZTc){*^b% zzqdy_d>v?{;BIhK)UMRi(-fWCUdYXyGbiWPj~9#k)qH1#{I!?bU=|{HW_9Z6X~E0= zYQNttziM0k?M>y=so`3Gj>*^m2?Xu8G)O$uvg+?eM@Prd-)`NJI|?2ybZ+;XZ@2c{ zOsmqY`}=D5?%jLU_IRIc^p1jsi!>Iy_b+QtSZ^^?I?X)y)|O+v(%{__dU1Oq9+ra^ z>jq8%Em_=nT+TSzBGAsx4&=_z)zfx8zq7OW@^b(1`la5#YOu2{}`#OFQ0S#|6}?8 z0U}ES7rQaD@fcKFWa3}hkacUz$^@qacUCAxG)G zX`H&TF*!Eo&HsXBlP6z(bhLZx@%BrXFQ=cGAt*1OZz84cKkv@|`uc+v;0;9+#N%rM zt7XqLv2wpFU-tFVQg3cF2e&jOzaU$of|}bLPynT}QS~n(k)1qNSzf+uPf#&F5G}Eku07NF zzG3a+t^~_}|Na#g7IJcOF8g?Ds&==S?j;Lawq;Yn(IX^e|>Syxi#m~+( zH8o}Zn_!fA-gmtt<}o(c>KjD@d_x3vUR@23|NGqje`HKdj@0wBv(4-NRD3-&>&=@t zzO&6VyNvSgSg0?5C3j-WQEn%5#D4!vmo9C&F30$-{jyj>V86|$6CHxeS3VwU<@WUS z1dYH?di3Z~)K<{?0M3@l(a?e}dY7i-yPdS2q8d-s2#o3l`r{70}-EmOuIY^V+p*o2(Tk@Gjvn ziqV^X_@Rev)~sbyK2_L=ii#FFr`|qxtnK(?PZgoPd-t;2xtkgoO!yaY@z<}a>S}9i z{l_m9T?Hn8oErc1CNFn&b#>hO^2*Ac`}X}S-=01D>@#)$c}wh*OwG-wN7-;%7SD=RB6AMPb8CKeVN`uFGAvfZ|S4QBf6y8EvD{XIzw`3bR0 zI3}%&*%=fZym*RL;iH!0k0;8hOULc4D*gQI?7@SMe+%;S-(OoBefjcbc0Hwid-m9v znwpxKO)LC&dwc%bvuEw*zkhmqy0x`+8$Yi^kBDQCqhsT~H4WEa>uPFFlsjIqd-v|= z=jUISf9V?;6SJr8ZPn|j{9eS7kx=h7>0Z*RXT&Ud1C35SuI zn%cg)zfn<9vo! z>ZGi!?CtIC>gvkN%d4xat2h1i*Voq3@gfsPaeo!;jGT92*C#K58KI;a#yO#H$iuwm;~(e9&5mNW2u`1`y3rJzEC z$kWAh=g#eyxA*dAWT;nk{ke3}qC;6*z5E&f^nUtO^ips_=(4|mYhOw-FjV&57Gq#I eM2QFgvX~f!waf@Hh-YA6VDNPHb6Mw<&;$Vf18}} + +Here, the initialization of `x` with `...`, as well as the `if` condition (just `x`), +are guaranteed to execute one after another, so they occupy a single node. From there, +depending on the condition, the control flow can jump to one of the +branches of the `if` statement: the "then" branch if the condition is true, +and the "else" branch if the condition is false. As a result, there are two +arrows coming out of the initial node. Once either branch is executed, control +always jumps to the code right after the `if` statement (the `y = x`). Thus, +both the `x = 1` and `x = 0` nodes have a single arrow to the `y = x` node. + +As another example, if you had a loop: + +``` +x = ...; +while x { + x = x - 1; +} +y = x; +``` + +The CFG would look like this: + +{{< figure src="while-cfg.png" label="CFG for simple `while` code." class="small" >}} + +Here, condition of the loop (`x`) is not always guaranteed to execute together +with the code that initializes `x`. That's because the condition of the loop +is checked after every iteration, whereas the code before the loop is executed +only once. As a result, `x = ...` and `x` occupy distinct CFG nodes. From there, +the control flow can proceed in two different ways, depending on the value +of `x`. If `x` is truthy, the program will proceed to the loop body (decrementing `x`). +If `x` is falsy, the program will skip the loop body altogether, and go to the +code right after the loop (`y = x`). This is indicated by the two arrows +going out of the `x` node. After executing the body, we return to the condition +of the loop to see if we need to run another iteration. Because of this, the +decrementing node has an arrow back to the loop condition. + +Now, let's be a bit more precise. Control Flow Graphs are defined as follows: + +* __The nodes__ are [_basic blocks_](https://en.wikipedia.org/wiki/Basic_block). + Paraphrasing Wikipedia's definition, a basic block is a piece of code that + has only one entry point and one exit point. + + The one-entry-point rule means that it's not possible to jump into the middle + of the basic block, executing only half of its instructions. The execution of + a basic block always begins at the top. Symmetrically, the one-exit-point + rule means that you can't jump away to other code (even within the same block), + skipping some instructions. The execution of a basic block always ends at + the bottom. + + As a result of these constraints, when running a basic block, you are + guaranteed to execute every instruction in exactly the order they occur in, + and execute each instruction exactly once. +* __The edges__ are jumps between basic blocks. We've already seen how + `if` and `while` statements introduce these jumps. + +Basic blocks can only be made of code that doen't jump (otherwise, +we violate the single-exit-point policy). In the previous post, +we defined exactly this kind of code as [simple statements]({{< relref "05_spa_agda_semantics#introduce-simple-statements" >}}). +So, in our control flow graph, nodes will be sequences of simple statements. +{#list-basic-stmts} + +### Control Flow Graphs in Agda + +#### Basic Definition +At an abstract level, it's easy to say "it's just a graph where X is Y" about +anything. It's much harder to give a precise definition of such a graph, +particularly if you want to rule out invalid graphs (e.g., ones with edges +pointing nowhere). In Agda, I chose the represent a two lists: one of nodes, +and one of edges. Each node is simply a list of `BasicStmt`s, as +I described in a preceding paragraph. An edge is simply a pair of numbers, +each number encoding the index of the node connected by the edge. + +Here's where it gets a little complicated. I don't want to use plain natural +numbers for indices, because that means you can easily introduce "broken" edge. +For example, what if you have 4 nodes, and you have an edge `(5, 5)`? Therefore, +I picked the finite natural numbers represented by [`Fin`](https://agda.github.io/agda-stdlib/v2.0/Data.Fin.Base.html#1154). + +```Agda +data Fin : ℕ → Set where + zero : Fin (suc n) + suc : (i : Fin n) → Fin (suc n) +``` + +Specifically, `Fin n` is the type of natural numbers less than `n`. Following +this definition, `Fin 3` represents the numbers `0`, `1` and `2`. These are +represented using the same constructors as `Nat`: `zero` and `suc`. The type +of `zero` is `Fin (suc n)` for any `n`; this makes sense because zero is less +than any number plus one. For `suc,` the bound `n` of the input `i` is incremented +by one, leading to another `suc n` in the final type. This makes sense because if +`i < n`, then `i + 1 < n + 1`. I've previously explained this data type +[in another post on this site]({{< relref "01_aoc_coq#aside-vectors-and-finite-mathbbn" >}}). + +Here's my definition of `Graph`s written using `Fin`: + +{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 24 39 >}} + +I explicitly used a `size` field, which determines how many nodes are in the +graph, and serves both as the upper bound the edge indices as well as the +size `nodes` field. From there, an index `Index` into the node list is +{{< sidenote "right" "size-note" "just a natural number less than `size`," >}} +Ther are size natural numbers less than size:
+0, 1, ..., size - 1. +{{< /sidenote >}} +and an edge is just a pair of indices. The graph then contains a vector +(exact-length list) `nodes` of all the basic blocks, and then a list of +edges `edges`. + +There are two fields here that I have not yet said anything about: `inputs` +and `outputs`. When we have a complete CFG for our programs, these fields are +totally unnecessary. However, as we are _building_ the CFG, these will come +in handy, by telling us how to stitch together smaller sub-graphs that we've +already built. Let's talk about that next. + +#### Combining Graphs +Suppose you're building a CFG for a program in the following form: + +``` +code1; +code2; +``` + +Where `code1` and `code2` are arbitrary pieces of code, which could include +statements, loops, and pretty much anything else. Besides the fact that they +occur one after another, these pieces of code are unrelated, and we can +build CFGs for each one them independently. However, the fact that `code1` and +`code2` are in sequence means that the full control flow graph for the above +program should have edges going from the nodes in `code1` to the nodes in `code2`. +Of course, not _every_ node in `code1` should have such edges: that would +mean that after executing any "basic" sequence of instructions, you could suddenly +decide to skip the rest of `code1` and move on to executing `code2`. + +Thus, we need to be more precise about what edges we need to insert; we want +to insert edges between the "final" nodes in `code1` (where control ends up +after `code1` is finished executing) and the "initial" nodes in `code2` (where +control would begin once we started executing `code2`). Those are the `outputs` +and `inputs`, respectively. When stitching together sequenced control graphs, +we will connect each of the outputs of one to each of the inputs of the other. + +This is defined by the operation `_↦_`: + +{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 72 83 >}} diff --git a/content/blog/06_spa_agda_cfg/while-cfg.dot b/content/blog/06_spa_agda_cfg/while-cfg.dot new file mode 100644 index 0000000..ef37a6c --- /dev/null +++ b/content/blog/06_spa_agda_cfg/while-cfg.dot @@ -0,0 +1,15 @@ +digraph G { + graph[dpi=300 fontsize=14 fontname="Courier New"]; + node[shape=rectangle style="filled" fillcolor="#fafafa" penwidth=0.5 color="#aaaaaa"]; + edge[arrowsize=0.3 color="#444444"] + + node_begin [label="x = ...;\l"] + node_cond [label="x\l"] + node_body [label="x = x - 1\l"] + node_end [label="y = x\l"] + + node_begin -> node_cond + node_cond -> node_body + node_cond -> node_end + node_body -> node_cond +} diff --git a/content/blog/06_spa_agda_cfg/while-cfg.png b/content/blog/06_spa_agda_cfg/while-cfg.png new file mode 100644 index 0000000000000000000000000000000000000000..278ce6022d5fd5b827d2cbf18c2098c78a72fd33 GIT binary patch literal 13927 zcmeAS@N?(olHy`uVBq!ia0y~yV2WU1VCLswVqjos`(abSz`($k|H*Y zfkA=6)5S5QV$R#U)fFLM=l=Nk{)y8&l{-uw8kt)Y7B6VasL*1&aV#{ZG|}gr0;wFsdE3nQmK@zR4t*)-F zVg8H`+IrI%89LlJ7#S7`Ix#e4v$)C?zzrS+*dcTZi(YH4@Wvxm!RB13M z?J#Kh{r$bazkmL>wA9p8LqkKam6Ik-+E@GAtZH_j`=9M*OAsyJ=XPU#{Qi}}%irDES$u0tX5D=* zPR^Nz$!$BEyjI%P{_>e;bMr>c$D`ur`S)z9zPvCC7g!q<8Tm5YacM|oe!tx=Z&h;Q#^fneN*?!`M_C9lSjNaXExq#U>S}%&i-I>d z43p2FnQ8of_xpV}ZbT&e*VX-db#?XBpycCyydJDmgAUsLeQlJ#_v}j2F*M2PD`&eFfxnjL?qmsJbU);^7nD~ zuSZ5kva+(q?kc&tB{SH?rG@pgqvp~OA0Hn#w_|_5-@m^x*?o07qe4fAfYwqYW8?Qb zpUWj*e*M*NrqR-E+sdx5i@kaCrd)se*;%I7(>cjwSY28OVSLQYFV=G)b7+PwK}bx~1~-(0Jy)2409xTv&x z852Xq>A&HwbTG`+oobeH+zvbaMXw`kI*7ST7S46r`oC&HOKWYS7=`-|z3K zEHCc3|J(e3e}0CqpC%-5J+?g7piYC>mYgO~f6?z?^Af4$bIx5aF$-MOO@o{#3Ih*=_HTUPa zc8krlpR|3)4hv)B%ZpwzFkG7;bSQLnSnlm@YooX4?(czM{g-3!;aY<0&*4w3D?#{?wih5{q0TWzp$*VS8F0SpQ%>!pBEDqwW{2Kp&|9o z|8Jee&(HNr8ZTS6?Aguq`Dag@*zt?4`1!fN{r`XTA3Ef8|JlvW>FR!ScGUhZyIwDM zZ>jh6ZFzUAetmiA*v!T&XJfHpd;VMf^($6Xyxn@8Pu}j%a{u}4auo`?x@(vImt?qL zr^laITl@EMzkOU#kWs>chU~qLN;Wosu7=0U8l`wRJ2&T_KR4GpzV7GKna1f^b3(RX zUhcnq`SSX|U$5^wd*;lUrQXxoUVU5p_v!uG?{{s#-}!vj{QeKK>3Xrh{(L@f|NqbD zb^o_>FjyD-TzS#5_}QCVTfH^67Ck+sc29r)v}tBpS2RA)TeD_Ozx_Xp7oQ{3|NZ&t zwqi<sPPbdL#;8Tv(`ZE`234JDmU~Z>!Gw0u*pL=Gr zHn6?pc{tCuy6)%c__Wm2pJuOLzn)+5s8ct3o5`<20aaDi^?SeF`t+*e7>6w`?_tpNM^+S_^gG0P+!>UzT zFD@*cZI)~F{?C)i{{NoF|4TjEB^rMJUn9HR471!@D}$G>`xjPO`E!J0w*Bv$=cV>eT9FHK_k4@Oq{YAc{!*zqB0=7|$0X3d&4 z?f$(TaUoN#T)ARf{q4z2pC>#XeT>Rw-4 z>$URX;dc8U51LP&JULx2c2~her`i9R85gwL#H|m%Jy%pjM8>k{$+Ow{d_U6V4yNYq z`}s^*-7n|nrl$|v<*!xlM=AQx{bo&26rU&6dO0*CWXhB&8cXwbzcpK(&iJ6NMPS?K zhwbuJd+#+evwwSe`S`0yh8^;XEqkwAyLN7__4UUeb>jEUF~7omp+VqKoS1G@$&(Wk z)#p__dbj)iwkk0Or5ztu1zJqG{(7!y_BHMGdyFzKsoeMCU|7KD-m;;!-~Qi^gY5D# z8+juC^z_sQgMXcD4#M;D685soRXkYSZ&&r_<8gjjt1Ii{?N=XXRNz)@`P#-K zxhe1NuC(jTtPKeYEgRC&1%qGjucy9x^@>l%A|Yqlk|iyzkss=X8Rq!C4o;7WiRqWKExEV2J9b}< zrM>5I+1Il;MEp!Vn?#)#UTS6);E9>g^ZLIwHDfM&t_jh-tWo2`7_#_Mz z?Cj$17ce}CkXwH}`zuez#8snC>r$y%ldd2Q2czCFlJM8=; zxsM+|&b2DtRK>+GD}(pp$;s;dGM0-z%f+tGzP?VbKmGo`+A#h{TD8BwskSu8L^;0@ zmX(zi7hnFrE>=@f(NR-WP%!bUf?i-?VBybCsjHVWESSow_~z>B>4iI$6SN`K&}iqD zqCR~qk)2zH1AZ|QhyMQlzI^#|^Xko;Hf@?QLt<%&r>E!reYMhi&pPwlZYh0zjo~~y z!v*0!qT&W^%ow{1S1P_F-R zSpL(ePfga^37|86r;oRqW~R zzP+O`xt&k8$5!2c-W==lbsHn2qpcGUwcNUO>&lfYp{v6p4V4)V7`@|P7?gFOfstEG z$Kd_RvuE$_E?@ut^_n$nnwpyQVt3`-+M=nXbg1bk1H&~zL8ql5X=%@Fzu!sDsoHx_ zGkDpRYuDc0+Ny1Bef#mpHIbX2{d&EAdw~-}gX)qN0~M8&x3{)#+_>@ByhDc$RepZf zD{p`A_1AMV43mF+cqrD#&ak0tih$PAUteBMo;x@9-sH)Xi(g$?xn;{1*KV;$Q&ENk zQB6)OrbyY>{b}a6%eW^jCbq5a@2?F8;_EgrGh}c^Du#GHefF&E?X9af)~sHAdt2`8 z*3S$KYgF}G?(Qx>fAXZ^`;N+_|3=G_z+=+R4@22TS?<##= zc9_>(!us>)&*FM984p7k7*?O)dU&vzJ^kFAmme!Wefo55P2}U>Hcs>3ym@0={Vl>m zn&E&@lT$=o+`k*i{h{IE=jYj4D=RD8+Sb0hvhrBDw3O7be);&oz{H0w3=Dr+S_>{M z@jTuyFK<)v;m^;{wbf#}Q7QjC?mc?+=*$_P?q$pj5zby5;cKI|=HA|xcX!v`zu#^z zT)1%G+`zy

0xTYS8OzYd`Ov!p86*Psyp`!GXre&1pa5q~6@zy!>bM%9SfOr=2x= zKhvhNC^K{AJw`@`X@&J1=jU3Rr=6KGYu2nYXU_EW^sLS|D1Ue7$&-}i&u?yS7FPHB zQngnqorNLd*i*$d>(|%+`FPyh%ZrUiqF}ALM@xJA{$H$;ik^N=mwHE@x4&pmOuNb$LfR1l##!xgOOpFi01qb9{eu^YiKWe@5Ecr?*GO z$NxVf?4NUU)6z|wKE0BjK4r?DZ@02fPuKr`J3cII+Qf;5m7kt`zgPYK)6>(A@=^>5 zto`R!J8^Mw^~qQkeLibGTi=g!$EsDU`ed!meywHY7PI+&r?}2~^5n_gU0t*O&GnwH z_f)q{NJLCbOjPvi+uPgg|Njd+&*UI1UdI=ol9IAI?839f>I@D><@2Oi85Xn>KP+lO z?s)28(s;;IN=j;t9Am@nmY4facZ=&!n=<9a{&zkK=f@9*#5 zzg5X2ZI&ZpnicYaZ`-ZMFD@>Yul+Ld{cGd&b8l{JeEjja{QDallPA2>)6>)Q*e}_@ zn~7-oZ&|1ty-gzie%efm@c z9-1)EyR#$ZuW%6lgKLbKoe|*48%O_wLTl&8?GXJbnILd#RVV zcdzk;vf{_R=6dn_?$mHZ1O^&be|vM@?)RBPD?x3xE3ZC1J$?1+)nm(Q`#5S9L%jC> zez*IY-=&s!cX$8)wtc^^pP$*ckkHVx^X==OpPMV@$9mu;$HK5@haFRA3&icK*|}oH ziSJ)8E_UbU;#xCzIcH&Eq4#vXy|35p?y>#)_3O=>H_P6cGt5?QiJBR&(9_q~*U_<| zK;p1?d`)6qX2IuYXT|s~uQ_qzME(Eo_51(-``v3BxBh#t`Mrp}Ra>vW-dbS5z~{=b zb<=b1mUcc_qx`yGFPE$P&DoGOV;To9@7XhFYQ9`_KWn``_x84&o11p+vRb{2=|MnC zfOauQZc$vw%s7QFAFK98Z_nGBHAC!Eg^j=6&nHtfgKgycH-6s#@AZB$y_k$TQ87@n zZ|kN+4*l3&C2wvR?w>1P^P%yl&br)Q3B#mkXJ#fQ+V7G5Hre0q=hyZ1XT35RqWT1~ zQV*L8%GuTYcr|rRc6Rpm{QG$)ZPremIC0|Csi}2azph@t@6?$yHr3zOv<5R42so{n z%G=NJ_guHsw*32Xp`lAFXKeHI_OAZiYlZ{QoO9KC?G|;b|~aZi%}2_DV)->e7u&Kd$ENeiXGhqKeJowt&-G zy_g*dHFGCSNO-7X$I8m;TXW^@%gf8Zzqz@%cwSl3OG$=Y2ac~hi=KMr=C0kC*)9h zM~)uVjoNa;Lg0(8?dFt|LZ5&0F?P6ed^MC8y!Fs)CM&nt40CR7?p}dwSFS`D1YGzr zZC>TSpU+R9K3!W~<9%Kya?_DN`}aAj$SfmSl1}DV$q$Z83Y-yLiE>Ud4om9>f? zAR(=m0D1PkZZ94QXib~P_+dN8LOU~irINqdEonNo%m*AmZcMxRAxYBGy~PeB(k}4o z@KGbPBbSUBI2Nj1y?XUo`O4cLIxff@(hgr|^3k$YZ!$QQfjR+iKI+;Qe|r1H@^F3`}^(gCE@Zz}j-#l(c}9C_DM}&f55eM}bB0$`L`uCs$rv zji_QPuytC&saT>nZ64#DUV*G6zJ!k%~ad)h37$7 zOMtL@%Y@*?zR52o4@?C~awsl$n|<_>al>x`Ctn$Hr#_DLtxMAxrYpA0vUrpv>DRkW z!23Kyo)d?uVfoRT2dUa~q;f5%&0~yd7RXBaS5f8OGC}!J+Qu(D5BORFCf~Xh^*H3V;+D693oAGL`c=iP zUMMqd9^;&Dfvlu=UAg@nXBD4x^Db^HFM{ zWs8j9HeT=Z41LZVrVmY>EJ1-G=CqwV7`IF)FHusi2ZW0b4=ddbX zS-5ZCy&9Q>cfD(8uxDpvJh-uRE=Vnl(~9Q%f(^=ky;^)+%q>gPL1nVlkJby@mb?9B zd(0CD%Hs*?EdlJyWdwiC-Tbt}pdq4)ZG*1Uiss-xj=xSP1QQcBe&I>*hbZ|ZmAC=K zb%t<-oOnU1rJYtdJ3BX5Uf!nooJ_bp|h27(OV6fo}k3d070Q=`uzApYfuD?P22oPUzVbG~<`Ana+ zx7@$6fq&XOMy3vdR}acvGHwg};(carmeaa4y}?1T#meI86%EA_F_4NTfma6v6`NX? zrZ;?3Zn3g3X?ghYVVG}ISmH~`1-2Xu`Rc;w-uQMUBR6+#$Mpe!~{TV z0bWWjILon+&u?ee6`L8yA3t0bm=4mG3(^+25u7Jw_^brI&x0xoP?p%X-0f`hN2Z0& z8^7>?>IdOIj)kC9xfYURwkewMyK%_&E=_Nkrra{iLa9YYa2Kcdc~D7jT6kn-U>`>; zC`hI$K=Rw?$;#rVcQAXOXE>|WGHZtOi|_kNe;c$!RcM(tWBQ*JD_3qTn50(V z@*+vcmN|x7@yd}uEG17*iE^uFGKrtwA?jZQ8s>P~jM- z+!DOu3(pd8@nh=b#34UzUZX}!fbj46QeUg~K64UwdKgi~RwUr$dnR_}%9R@*wqF5F zE?*aZXzH}#3r~we%d8_uj?6IEkKL7WRpt7l@;Rpj6-B(yJFq#e@XX0sQ@MH5rc0|l z*ByQTxan;8cL$?s^BP|ZI{7LoDV>oo%|0wJ%bkmtSGC0;`K9Cz3B@bNYXUMp3miLk zY}Wsu{2J5dHC78c)#k_@>gwWp{CdX@3vTts+>Kv&Vmbw0C4Ux}<*wASLu}f-#@_-U zRZe{z7oBu$nWrnZ{Ibw!sk^>|sV<_5EzgPLtKs#dZSR%8?2b5g$nyb*jxF^>xDEcl-mzxQo44EVo0-X1JYdvj`y;)_t)uMJ zi4z^&-O*bzCVq6kyZy_VNvhsw-dnT0X$xNLIAzL|E&2EN>F@uuY0H)^FNzPDLkqIMEx5p^xToM@(?`?m zKNJl*_! zOaJ|;eEiyPu2rN3XN;PTPR_SCH|xC5|EPT2YaTI)S4^qJibv8&#n5o$#r(TPAJ@$vGvx0dG09pG2IqNt195@%_K=%6;!YTf6<U6UM4jfyhOtYqZoS7@ve_YMIB{enmS@(5LMW%J-@9zaK^SQaB@Nuxe zZRy?8>#?uXOifK+UtfRSQepwe!ZiC|7yEleuUCD4mpl2%jCchee*XT>&W!~UJ0fy& z-mC~*{OQxDxSEegtKaW6S6MRg`TV)oq=+m^kFSnfAB zr-tm^x>t9~}{+@fE%*Lt-|C9g8 z%$YSy>Yw=b;H<1w(asfLUR=Dq+@JmZ_vK5L+$lP(8(;S`H8Jtwv$L}&Pny(J9$&EW z+CSNxSdLoA!lhdunhknnEHBx~*Ug?as|pn0dnz_ATJ*@>{#W4lcX!v$JF!wPW=BA5 zZ0=VP$LkxDkFQv<;=$j4OO`C@>FEhx?)TAMaP8G?`K8WTuoe8AQs(D(7_^mx61h0 z-{0T&i%#oKojO&lkL7@@g;I-h>HB-Os;Wm{X)^3!RBQ?U`s(WGSAr0B>6;rD;p`U| z4#L>2?d{RFObq4z_M)+Bom?3FUs9UoRGazh7T}J8j47b-T5+v~GRd?Cb68dv|lXzjWONK7MY2 zoYi4#rHoQeoSLfr|I_sSKWeq@?CO4gdiwotd3;h*(qjAFb$@@&nKS3=>TvzIJvX*5 z4_@x49kyo2`+dKotl7>p6y5l4dZ_O2FWVAJd9OnQ1_4V`bYnRWfdL_R9 z$I-1?E2ey^u<7jV^tb&wCEwV}>eu=Df1hU%h5;@Xo`bbhiBB#nFW7^!gwa?DX z^qp-cSuG_cRrcnFVbK$h{n2?hHXQtZbW`f-W&ZQ;o%?-vZ*}hB*X9ouboteMo>elS*)BfZnCN6y6%_*$5rIJ-?9^;b&2ac&htHamZ6+Aew zG5L6pt#SIfJ@5DZPD)PhMV^{5Q~1Am^5n_4|9dx`n$*sEVOjqDea7kMY96+V_t@?( ze_!`(X8NqZ2hZF6_R)O$vEmH7^V*}v4Km+sO|!(r#kUtecKa;7!hfEPW%;|9)x9m(0&Wp94G+x>pl-<7@6=2}bJc%{oO z`noD}l@u;IX6HJ=#?b(tTwUXRn(*3N$PEq~9)wxCt%=jZ+Z!2e(1%fp<8 z^oDQ6K^)FbPS@7OX50OZ#k&4)4cKj+oinXUS8a?847_;6@!`$Q>DzN}FPk#UAhBt} z*7gdv414v~0L`n*{pY`Vlk<7roH=uXm-{VUx)d}JwQ8l#@xx5zvyD=_eir?osvREp zS{Ag#X!XjKoV>hq4HBEyy_y2!(b~f{G>#eprcCN0jARG34yjy<%EYr=5{+5;&P>OvzJ^ownw5d~{ zK6`dsenpEbW9;>9a(x96{X_(|ginZBByqT=HBJ09~T^X}cXYgg{=ZCjr# zdKIRrr^k0`mym9aen|Gq%7_{<{kT8v_J0<(n%h-=O8NfoZnGiVlNolkzfMin?k#nx z|9$(u-&`wGEv-{Ev;Y5l|KG0e&yJw1OG`Z8?so^J*%Xf5dGyQ(e=d-(ZS=~=7EBm&@b8?UU?d5)RtKRSZJ|#$4-H(Tp^T1Vp8|D)aH*}}g z6crb5&$)SNZS;0f{d;5P{Q3I}9y)O^-z3A&edp~l>HI&>>;I)Ef4-f+KX!lJ-i<%6 zMdx3=dbRY$g~U5M3dMNRnQfT2%>3+B@!`S2na1f=HuLuE*<+f0?T202X?1Js-MQJj zb~ik0PrbS-G(CDvr|P7}u%FxOf17`v|8{y@)yeHL8P3j!XPIVC2~u|Jd2wy+?9|VZ z?dr$A6-02HK7Crg`pw2yuU_5UoSvSNvSj)4+3_kF85t7xbu|;>?r$^x%kN!MQc}}B z^S>X{+l%Yt_q)qg9=Y-7*X#AQtNq^J*!cL#$;ny{(@$FP`S-kivO&OamdVQ>A0Icf z^Ut%d-Czu#_mc6P3{Uc6`#C=2CiExooj`uX>+jk`Z?aF{Y> z%9Q#4|2#kTEIht;Ytqp!S?e;5rSob&dA@$OiRV1S+vhXjOFNAp*j9ftsn<3&z4~6h zbF#XB-p|{6Wqm&#zI5S2!abf#?#Bd2=la7hQjS)nYMgi@i?W`;SKTHQIM{ zZEbCJbqXZY*8KQzJ8$>d8$O;Ou(3eyZv`8N!tVBhlao}} z@A=dfq-A2V<>vOqyfPLS_C$tsX-uqM6fpXtc@99-vUrn7b zVZr}E7z=fb93`@*|^@<*Vo^-e!nL;ENt3@2_K%#&bNBnUuf-F$ClB#?XT>Y zEw5THKYH}2_V>5a_xEZqEO1;qe}m|%RjaJZ-rRVxT}&t9!=2*uKi~TJ`RQqCW&JAG zi`{kQ<@+Uq|2F8v?z&PjJ7n{zQ>T)WlA5f}U;Xy(Zgf=CtXZ>eE%%o{TfX)L#jmziPRsH<*G^~Gd^M~|?X&JZgJI>bIB`Ya;b5%D3 zH#c{)c~31zeMH*%dA8Nxa#k;Ih<$Tw>+2gElf5og20lE`a4`A%bq>Y_f$R5vn-!Gx z;laV}cZ#~NZa#36Ly_URp(#LAA#mftDAU;Faq%lUP`UQSZ= z&dSc-UGnnLvhw{0qgn(S-iCySpPy;`{Lao|ua&!Y?W+C#?d|RD?_0&=KGd44sH7b2 z61`rPZFwPTjudNx_59jzGuJouMr}+w`r_i^(sRt^$}J2z&#y)2=ay`}@!`XV)YH>G z-g9ITQ)Ef7o@-Tl>h$T)*$+1)9_Ev=FsS`ivU*ul^hYU02J5OH58Ju9x&Qw-Za>ea za#Q~OeV~=c^$dyv4lM!=zF*(m{QPqH{B2cSJLH$U4bie^J*lJN4*&dpbq8O~I{*Lx literal 0 HcmV?d00001