From 2ecab812f47c9ed18254b17b77c92f5a29af83f9 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 15 Dec 2023 14:48:38 +0100 Subject: [PATCH] Use replaceable modules to ensure that the notarget interface is the same as the language specific ones --- Source/DafnyCore/AST/Grammar/Printer.cs | 7 ++++++- .../binaries/DafnyStandardLibraries-cs.doo | Bin 1332 -> 1340 bytes .../binaries/DafnyStandardLibraries-go.doo | Bin 1357 -> 1360 bytes .../binaries/DafnyStandardLibraries-java.doo | Bin 1319 -> 1321 bytes .../binaries/DafnyStandardLibraries-js.doo | Bin 1867 -> 1867 bytes .../DafnyStandardLibraries-notarget.doo | Bin 1305 -> 1314 bytes .../binaries/DafnyStandardLibraries-py.doo | Bin 1327 -> 1331 bytes .../src/Std/Concurrent/AtomicBox.java | 8 +++++--- .../src/Std/Concurrent/Concurrent.cs | 12 ++++++++++-- .../src/Std/Concurrent/Lock.java | 2 ++ .../src/Std/Concurrent/MutableMap.java | 2 ++ .../src/Std/FileIOInternalExterns/FileIO.js | 6 +++--- .../src/Std/TargetSpecific/Concurrent-go.dfy | 3 --- .../Std/TargetSpecific/Concurrent-java.dfy | 3 --- .../src/Std/TargetSpecific/Concurrent-js.dfy | 3 --- .../TargetSpecific/Concurrent-notarget-cs.dfy | 3 --- ... Concurrent-notarget-java-cs-js-go-py.dfy} | 7 +++++++ .../src/Std/TargetSpecific/Concurrent-py.dfy | 3 --- .../FileIOInternalExterns-go.dfy | 2 +- .../src/Std_Concurrent.py | 12 +++++++++++- .../src/Std_Concurrent/Std_Concurrent.go | 6 +++--- .../Std_FileIOInternalExterns.go | 13 +++++++++---- 22 files changed, 59 insertions(+), 33 deletions(-) rename Source/DafnyStandardLibraries/src/Std/TargetSpecific/{ConcurrentInterface-notarget-java-cs-js-go-py.dfy => Concurrent-notarget-java-cs-js-go-py.dfy} (93%) diff --git a/Source/DafnyCore/AST/Grammar/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer.cs index 640d0b02db..b40650701e 100644 --- a/Source/DafnyCore/AST/Grammar/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer.cs @@ -583,7 +583,12 @@ public void PrintModuleDefinition(CompilationData compilation, ModuleDefinition } wr.Write("{0} ", module.Name); if (module.Implements != null) { - wr.Write("refines {0} ", module.Implements.Target); + var kindString = module.Implements.Kind switch { + ImplementationKind.Refinement => "refines", + ImplementationKind.Replacement => "replaces", + _ => throw new ArgumentOutOfRangeException() + }; + wr.Write($"{kindString} {module.Implements.Target} "); } if (!module.TopLevelDecls.Any()) { wr.WriteLine("{ }"); diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index d5ef3edcaa9135b6735fd3408b8ec635e1a5b51c..289bb463082c11873669bdb1817f8801e62797da 100644 GIT binary patch delta 1073 zcmV-11kU@k3cLyoP)h>@6aWAK2mniUkqps)OLdP|dte2Zz5@UNr4IlA2LJ#7aB^>F za$#-7SMP7rJP`igzvA9+iPSe65+6`#i(uMdbOW@G@ez5+b+wwr!FHmK(f=LWX%;8V zj}8P(s+QV!_dNI9*_R$2K}eR#Jv{fGd&l1K=;#RaN3QT|%Gn(!@n|%PS(rr#4?b>x zB=Tgdo&px9RIM#ZBybB08G0v+72)X#OM;AZOeAnjBNCthYwckK5JW@>E81ly$!&y} zB%REi>C_#=js7bLH>C|1-E{EOJN2 zzt~SXhBP1&;f6#sbX>DnAONWNXdbtJg-?uf#lkkYIo=D$Rr$$`Cjy+c`tE~3IhoJg zA?J5QD1T?|!`upy2@HLkad!a4J;NG)ZdM8gH^U6hCB`*>suv3PLcQS_pE7Au7=x1h zX3+dC%4WvghmWbGEIEYo6~-*bBE*pGf__IkyTFHpNL_1F*k<>=mMo^h8@8E$T>oOn zU6;)^2C2UNk(Sc}S~*!b{WU5KJ5s-3!TJd)4+83V!&aY@sIb$l6tCSip|1eg-8AMp zu`dl}OXHMr2`t3~L-@i;nj#mES(#iOEah{;feO7`o~+Scmb-EQU?MWEZmR!Ek6IEJ zC13r=@moggw&ey1g}OPZ*e$4kWayG&ZLI`q#j%vBA^i@J&C+UuTG!jM8F?Cg-6C9H z`#0Gqxg(oGYo?ysf$3Bm)MRMwbvyNkZBxwx!VY3Le>WW~o+VD_KD0qqLD54fR13dr@d)@7}(^SX?~)2bI(8>(D?W(Ob*kF`Tm z%vFlHPO)&dl3aH~A2bjTL6-_$*BMNJ5>R@_>S%b+_8Zimpe=1$Fl_)gPfG7t?Iq2< z1&i^Osm~6Mdq%f9)7tQD&}^@359RLZymubEXTzC#^*sN0p6JO!qEjkuKmqFzY93c8vPe#R!N?yf4d%zJEX)D(r;z7WAa-fIBu1F z$D3!h(@IkB<3{fr8tT_{PD6F{_9`~s({*ftC%>*b7OLdP|dte2Zz5@UNrIP{$EC#j&000002W9Az delta 1073 zcmV-11kU@s3bYCgP)h>@6aWAK2mlgtkqps)5^|4Mx}RSrwgUhFNDlx22LJ#7aB^>F za$#-7S6y$@Fcf|7ueiJ=QptwI0}5>sOdE`D1Fd6woV?_AwVK$$cA}2b|Bmf6#A(x} z0|_3gCeHmh=iKY-XxM5*mA@>vA1HXGeRvDt%H^Gak2r8RL`md`({E zf=Te^`aT4SYA_!8UCy6~)c)Q)gs~GMml%g@J{AG%Me|*6Z!*Pc2Nk7C{t^HTiDIs ze6M&)qYr#BxcS3=ys28T4@%!v4Jq(@PEAK@BTxN@HZ`Iu>_+1LvWkgc8Q0$Z*&xt4pz4dS-u?)~M&bD-}$fOgPm9x)9V`-lHtQd2HS zlE55(>K|obTpU$4xw0oXo`iQSUNi- z=etuMbS@o|UFqzmkYEE;2~}{c2XydiyQ|!TtfjX~q#KDh+k5ZnwimPrCOpM=wm$20 zBCxtOkv7i24Vdk9-2-{|A-T1Qc8}XL{d#!*<(!#eO_EbPw58orRYk9EPOq=tU)*2o zfFGU|$}_=JO z$$KYs3)sXrd@Joba2>P@$9Bq9%bT-N<})eCiTo_v6{_BvJN2uB{x2n45d1q$>mGAO z=}^Ggg9gVn$~;knnr&%jah1crJoGInN1z%Rgv0hq1sz54-}Y*M=0K-a7W3)F;Ed2j z?|-jK;{)pNESTg`gi?CHf!HW3rzFqRzg-W{?^5C!^ji_Fk^Geio?o-y@h(?CX$5JX z%!z2 diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo index 3f73a8610c5cdca8c2994f28450c527cfc7a2402..b0c70f357426f92454ed6b36e3fde76b25e97aae 100644 GIT binary patch delta 1077 zcmV-51j_r(3eXA+P)h>@6aWAK2mnrXkqps)PIZr0ZIphE(gOeh><<6{2LJ#7aB^>F za$#-7S50r*I1s)2SIqV#0j`n)JuFn)i*z?>11D{fWYc3nOLRh55>=8CoVxz+9a2_A z$@*|M*fxL>nVgyT=FN~JA00tRmdPW$_1=2N-tp+@2=qri(7ROddqLvSXcY4>izsY= z{D8+P!>1*QB;Dddn8oqqd7N^gE@`}=0$%;2m+tOfjX{YFjjmPbec*rdB*=uIi2^~> zhy+xEwYC`n1QC%EW74&vBH6-arpO|qmn5Cco$1sa!>#@|1JCn}1G?};B1)jRupBo& zSu-AQ!MT6nQUObHADlV*yYPAj3(g~dcVzsF{Z!D91w>J}B@qi9*X$JtV6rfe+rlTN z>Vb!CaC7=79T)RcnMfo!EBx+*q-rvsxkJt$i9~;A<-^Y!Nns2q`R$I+f?C(xvKe_Aecd8lU;8)NC%L1VLTjcT?!a`a4Qev9_PU+=X4_P= zfUtwu&EHMOif4(_IgmPps*jw0wVLDUa9R4NPOm;oE=Ux?3Vz^+C7@k@!S{i#nN$*T z{j7Ca;dNe@ad=ww0&7FeWp)74@K`$}#T--2b&7?vmE@`$`k;Y$2)aUaU1u->N^G=AL0j6iVA=p~o|N9P+Dlq^*F2_wnfmPDglBZCGp!BZ2F>=m_E7Gg&U@#v zdp4ZmyXpDo^F&V;5}lfV2_wzvEGzoy=Je{*$;I6j27Ldhs5}!q)^1Kp)B~1Q36|Vf zuw~)psSsTFyZdaRJ#`4(3*RP-{Lk4KsJ6J2_f?P<+^+&#zyROyJ=k5~D(Dc8eaLO! z%X&3(4}NWLSM=!(eo*iV^mj?$!r<2xp=wH7lmP{-L#ugQQJF=5YEorem>FKh;3-~d z3@J;XiW&IR_DXpJMRDJas?32cOBDU{Fo83|BD^r162=9JjRx0QfUO~&Cn6@w)+)&} z^>5e1afg(6M*6Lcc1&I*g5y@%cf6@qJFO)3K3(g5Lj!-5=Pbmdw^y<8o~~mH1R4AU vP)h*<6ay3h000OB08Vw2)dV>WPIZr0ZIphE(gOeh?2{V>EC$L100000!aoit delta 1073 zcmV-11kU@=3e5@(P)h>@6aWAK2mlpwkqps)6>^VPw@%|r&jSDejt>9;2LJ#7aB^>F za$#-7SKn{jHV}UIUvce|1b9jY^r6sf5B-sJfs=Mfvh*>arE^SJ5>=8ioO%A=cciR} zl4Z+Tf%U<#Ox@l0eRszreRc*hn`h7PCU_H^2j_#cGcX^$z{gyQC&|*mV33NqNDwxE zVI?;q^ze^!WIC2wE0obf@FsllUOAsE`sf4HD-( zLj}&#W&jW+OeqS9YmGA7!cC#sEWsO=kEY&u><{6=d`%z-0_#97B2xqsX(1iQO~}?< zq+9Tw7D8#@*(wBYO8!3lGJ%;8iErJ10WedABr1BrRX}zy9vkz4eO-Fz5@Q}Qjqtz{ z9($$hW*5Lnw2#};Cq=ywaTl2>J}b{B@w$+i0&hvbLr|zk(}~~b{0CFy?=3@^Iw1;$ zak$gd6M(oE*uY=em6E|jKZ7fcX~UnJh0?vuZGVhE3vDF~feP}_YyJs!Td@p(;Y+T$ z$WEbri>X*)8KTejj{l9Wx+sKZxh$O~XzUa>Z8klvz0e@p*@-T(&9<$z+%s+v zw>1y%FDITu{ony~Kt}V3Y0x-6{Ev#73(1lMmhcaKcm~E5!VqxHl~%BSGS5cLlBQ}? zd;g(v6xbNjpqZS2)PK61B5_3$S4Lv#?1)?*hCb`yl+-~oqr`u7|GPn~d{%-5DgOh>HTa#(y3~bTtuImxXhY!iUO>}tNUef*X z>dRGThBZqr?9f(rOH~zr{d|9M`}y7V<1Gbz|Ey76N|72jFK2o|rPY#WPc>{+cy%GA zkm2rBof%IP!t}zo(QNg0G6XahH|nVl(t-O`QVUq%d$9+*3tR{7(JE7GjyEol6^VPw@%|r&jSDej*}h*EC$B}00000c&ho9 diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index ac45478e52f94ed015fee9507660e2d652a2b57c..45727f4816a11b92b0eacf5580e2e1a6c64f4604 100644 GIT binary patch delta 1037 zcmV+o1oHc*3aJVVP)h>@6aWAK2mnlVkqps)Om&Y}pmm}ms{;T4r4IlA2LJ#7aB^>F za$#-7S5a@He?YhT7wb@pPEqRh`q|4>MpCsF{ zoH$jwVRr$7I1Yq!MMt^gbltLg=unGbInipIs-~}>F;j17;fkNtyBqLJ72c9gnAn4ECJ(mh9 zB7jP>jA;xvoM(aEO*oTEl!@X3!jWA9KqgCp68>m4YS|psJx{Ieji|uyCGE?$8zhxF zHY%G19Spst*jsCX264WyY!K;JfLt$s*TIIa*NW#fdBc~Jt67gWOAk<1#c&1BXZwh& zh5KS-Q2O7l_pA!lHqpk@NbkUOY6N;TyhRm`w7x0@lMwcen$TD4Z8mEN*U0Bmg?@J& zdk#70r83ocPKwDqoK8n$xHdm~i3;ahVssc=ec7kbGRFt$^0LtXW00sO^O=W#pIa_S zmcau4(O=5Is6reAE~!)!D)Vf3S&X6T)A)`^jTIvjdQ>NmgPn zz{;-FAzmLCVx>c@Oo+9z6Xaq)^qIoEhfK{v4P58zKy;4ioMSe??;b;gSyIN zW4lQ_;@*Dn==Un!BfGzlok`N_!L!Z4eYWlo-=C_!otgU^%5QKCACRwh>JHLi?jo82 zds{m^axZRkL-R;E_bYq4?74ZK(hSc&oiU?LvJ-1XT2I?~@$u^9;^XTN-!AlV_2xmL zJQX}QYGFaty)JPjD7))_4z;!cVTLvbv6sNk>iToT@6aWAK2mljukqps)6LODNEKx3BsRIB2NDlx22LJ#7aB^>F za$#-7S5a@p=hjvJ|)J;1iS^8Ko(m5e4kt#_E&OHD3k(6Xf zHXXVv&;>B;kazce_Z{yjot;5Omh2f`$FJk__&hi}1M^W&__-APQIH}C0)b^tQX~(5 zIYPm+N`Kv|EdGtNv=RcDf=v(r(4yo*0WXnZ2A>2eOB7OXq&bli-t%;&4MG1sK5?m_ zCIYB5%a|qbzy@&3dVYn@_kQf!3cK_*Y?yf>Tb-dTscRaGr%lL#EcS$&{b`_9@C^HFyTHf;qN-Xy=UQKV(sT|gi1E^a=&dH?xF&%d|N z3gxBXg>ef@qMmeHC_&kOV_(UxY2<|vTqJF^AB?97VfyIH^r8NFJ^?fq*YdFs;=uhR zbpKi4JAMG$2JVCUcpO5$ILhTa=~k$l>|Xu)p#PVW4hG*()BcPNMe!&wn1Y7K4azE4 z(>~kA%<^h_s(DATqy_@@%pjS$D;0Z+68#eNnFC#RDCX6R!6l(txt>sA2NMD2Qs-Qy zDM}gch}bCGK}o(+f43fCFE?=nw002mn_XI2kp#%T` F008C~=F0#8 diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo index beab34ae3bc8cb74c05613984e64c0c11a7a475d..8510c9484f638ab9e5991aefc55ddae568ac8b9b 100644 GIT binary patch delta 1581 zcmV+|2GaS<4$BS@6aWAK2mnrXkqps)PIZr0CLKh9%>@7e#T)F za$#-7S>IFRHV}T#U$MOh#+l{}owkvz&iiu$liJr%_G_N*OFiBY=33VZs1sC`B{)Lc%OVgz|wX2`Pn7IGS@o z;D2}bm@+6r0x=b@(JX))jFXWZjc`gC$s>jdcw_kr0Hri1h{AXEj7oNa*gc*}-Hj+g z4|#0L)&t>;a^GUAUT|mP+ZY+|YC~3kJHMxi)zUVGbd=?&q3bQfi#U3R9}h0425pia zh|?l~OL#r)Bd!uQ#U{Y`(<=J3@K~2tnx%p3FhEGH=i&r~X0UzS}q zD-*hs-*V=;;b{6aa!zw5qVY7$4oJ#78et-U*i&4`a)e-Gr7C^h9-kUgrEc z0E*bb$<)EmEhb@-z#N|Wf1HAt3PAwqF{X?{A-)S<<`XDP8h;Hbx9iOVIMGb!wBAz= z!$OezG96&)Dok=@I9SLxm5WycT`ahZg>bQ&tT{RFH~oR3g<&}sFDk>;dJVMBxOK74 zAQjXGnZL)khX2EAfC^eUnt)q>u!U)bv}3rtQ#wmS0{EP<7^iN^h<||>=qI^8${g_} zZzj@nw7>6icczcXT73l zmq+JkZ$Dk1bA|7o7^24nFT^x23)wwiT1MjZt~FaPJUt==lR%wkH)5uLP$6RB;ozqD zaXJAcBu?pFtHfgW3*jLk4PW9Fvr2KR)P-Z!B3Uf^-7&dS|@sQitqa>ujnbGowy9b z#~3flwOK^VOBq44I0_km5+`arQ`N*$k-_yN`PJN&7IW*|DI%NBgQLTfrjMt5?VsKfmj$Nq|vK>_s zjI;0|M=Qb4SC54;UnI{gXN1N-YKW8Su`#YcR|c(~`4Z^CVY@=Gv(uGPfNLpDUFqJg zD}7}Rp=lm?iKkwFLDfc>;CLC?3`1QE)*@f$-^MLs@z-Umd_l9LicovN=(yXir`wFk zWot;i0yKKxAh=-VlyAGMT3L=A#eT!GayQ#IFS-Yx#!V#&MJF>dEHgAS^Y(v(m zbwagnnuFRJYT>`JdquOMJ6p!)-9}B}5C@rXLhBCewySM_4~>mqb&wiV3CM9b88AdpHk zwtT(z&UWp&qY=<_3<9$>)pugJsoXU9y99QEW1F8B8UmHLup+M&Y~Bs~tzpnl3w^d5 zWj6Z*e}fqMlfys+W|!1n@#$Amj{7Gq`H2$b9ML>~VF&G9Qza&|;j-Di>Pkqvo@(!f z1W@ZeneVs~Q>RXaN2E$+rOJ=TVVrQ9yxNS)j~96qAxgalh}2SQ7h)UUe%bl(#x5o{ zaNmkZA=!!qZ`^v{)Bd(2R*+&GJ&JJ&BO|zoXFN7nR&27u>qIlc5&R8MO928D0~7!N f00;mAPIZ&h200B*b&ppj9Ylf61polWlNkpxee~@6aWAK2mlmvkqps)6mpMOFfWC?%>@7eXdD0l2LJ#7aB^>F za$#-7S>JElHV}UIUvcY0AY-nQ0eu)0+e6zWTk9qrk}Q2FicFE|M6fI>B&9iX^uLd! zevpzWQ%;61KwwKe-uK<{$h)Ht4`J>v;zxMnzHyJ-qru@Jh<|pEZW4m;h`$;P1_UL4 zksl!cHbSt%^OS#Fvbp;n$3aR6iWzJM1AuUqV8Q?=C`NPmLi{8_gz|wP@+pN+I9PH) z;D2}bm@>$G0wEQz(cFVujH7`Z4RA~uNdtxnI79gg0L3&Vh{6xmj6!yW*gc+0-L)t| z4{6wxtp@x#<+g>ie8G(g7a?lAtALDuIDf{G5$PpBI?H@eyX!5(t1x(n*W;^c!)?+% z5XPAYSMYkOIj$u68)D9ob6_cnDL9PF4I9KZdE3@FbJ(z<%&avRnEz>Srkv zv2x}oQ3OkP;{RcP3}PyH z9-wtd8HG%I7sf0{kTq@p-KQMaS$Z(jpi^3fsRdXF!elb-fpqOhDQXy)$v1_G*F8%xX&(jegA#q0UloA8(7s5k-KmuRkE!a}A zQflL|4at2|`eWlEX@4#~^U=@z_w*w*dx)S#81q%L`cEnSzdUJR@I8GR;8nsQVBtp; zDc4>GButo=?JJKq3V`bHS2lE}0oQfQRG_DNHF4wl>kzMUaEer6ND}R`K;%`I%kh0J z#0OfUNeG&UfzOaQZNqtgnY=fp0*;R4*XE8jklCGzER*di#iGETDJ%+lo%a?U?c>`b zZat|j^BZTdMYj8h)d~|euTfn+D<13Gi>Enjo%9{U)L8xXSl7x3qq}77-rr4Dz_MPq zNNLq}ZaDnm6+fYF)FJdLZ?z@A%GRb&Z}P&5Rmq5+W*OtZn zxvRTuxL1-|m`(t8k75v7oW{0Cyd;Nn93vBXOIzJOp*p(lU6)j*nnX_+imQ0a>fF)D z59;AZ*evsgjLH-GBbUo+xvrSZdpGVKj@Z@D@9Pv^O(0%q7*!tca2&kWUDD4~+qHth zYWw~!4KR#<1cL8VMfj;=^nzPUF)XT{Tf7#h_f=P^^Q>BX{|ZRb5Js|{rO!+10Krtk znDX_`i`$*&j^=>6V-TDrRM&}Ncjdmp-*#XtI9~D#K<&U%T%gE%3X^sHeh%n$``?9K zD>LEu{F$KduL3<8G`l2qWvJhASuV7+g|dRUsy`;ilfboo4ojGqibP z5A%(TN+vIIf-_XsceKB1#7I(%qqP{9G!lZdaL!|MYsE%eejRBboWZ|PO928D0~7!N f00;mA6mpZ(200BBa*tOqFNM6#1pokOlNkpxv;+B5 diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo index 27523da94c44127f81bc1c4784a454ddb8906dcb..b904a93dfeec4ef5019478f4adcc1e2d79a1a77f 100644 GIT binary patch delta 1031 zcmV+i1o-=z3Ze=OP)h>@6aWAK2mnfTkqps)N_CG{5_jz!qyqo|P!0e92LJ#7aB^>F za$#+?S50r*I1s)2SIpidz^i0|9tzd=qAil$z)4%g+4NX2(l{n8kt#_EPE-H)B`GVS zWPLbWYycxNIWzCgn<2+KJA;_4*%Q18-UR2t`Q+>j%tvkTTPFCUAn9Z>NqL+n2+tvZ z?i32P*G~~oGpg6tB$2p>m5PIps|^v^N6w;L2xJNbW(kQd)#oTfU+V4Z>jx#_5OM#-4BYN(2BMAMN9RzVt~^ZFt-Tx5Ovu`8q$93nsza>hB>)RI}y6 zA9MbjNbT=!Ls&W?a*1*1GVTwcx#!rxFYHRm;C`IJmBO^)Pt8K84=d&N^4ec-!)+1-Ea zxVx&^rl9n<|E1-OfKE;h&Tx%N!=BWyd9-~+%A9_9X&>2GXwpxh$O~Xmq_Ro0X^4*B!zQ zwSSvED?HT}+At0D4$SAqpdmwNue+%~@7rpY5N;5+`TOZO@f>k_2U3qv&5<*#R(m|1 zF3a%L8PsRZ1xXUv!cYC742&y;A>fWmC803SMwhL=&YLohPpd&-W2kd~S)710KGsf2 zvCt_NCdJa(Npjl{ebPWY1zl-$Q)jRNDnJ#S>!T6;aonKp1np?kl4%RLeNqO;>L6(m ztayrl+WH*eL|}DmGHnds7R~Ou4p8o&&PV65e>Pm|pPpBrub7!EB)PB?M%vR^RrJ%{ z#qFo}*WYe+zzKJ#!&Zft7ea6m9`3UT<7q;eUidzHDBdon zfX3oRKGs1xaK8%O0v7m=AHg01*Fnd497FD3ewEjHxB`si?evS`af>of)U3|2G_$3dRRi)bAUx$|L<=A-xwO zHp<>9#4Gjh*2DA1lz2t@os14len|w+ue0y@kyP(=k~I6cGy9f?e(@`4tPl55#imEP zP8|@<;9pQn0Rj{Q6aWAK2mnfTlc5AT4oY>8R}y#a9HavP08kE-=maYUoCE*>001sP B?=1iT delta 1022 zcmV@6aWAK2mldskqps)5ps`LO#tIGn*#s<^bG(22LJ#7aB^>F za$#-7S5a@9Fc5yvueiN|l+jMw!^DzITh(q=+I4EW_OWu|(pUkT*#@P{^518hP)tHX zx<2e73Yfe5zVGgQhNB~h$&@|8``~?W931zKj==oX4DU0+9|cK!y#!nK@bGiLA!7!mB=H-MS}%dP@b;9dz^8pfU+V4Z>;@&csqgz&J*9d10a*R z&{Win%0Sz}aA?eX_HpT*35;n(6v8ckNoeequFG`*jgIzmRr;i;W;|{qGsY+B`C7cn z1(V>-^?e8u)nGjGyPUrfsr|iq2xBKiE-?<*dO8AV?m0H_3%gP>xb0?et}t!*Q?pRI zm$~hZ@grAOLLYQNZadAtqS{m}Lb%ElAG%Me|*6Z#unbx{b6C{t^HTiDIs z{H%CNqc40hxcSF^ys28T4@%!v4Jq(fPEAK@BTxN@HZ@6i@=$U+pstmO)^uI)X#RpU zbpo1r-Bv$YQra0-nwP*VArYFP0_)Lb=aV~zv@K0DE)?(#8OCrYNS2|H&#J7JrIY!B z2%yp|SG%#drPAB1yKc;@fD2+O~Q?;<6Xk3t9}FQf#bMK&?1VW|~d+3LuxI z(*%v3;-<}}XJaokNVayOOKiE?)LQNtH;CJsyZ4t9&!N8a0NNp=dBikm>>vJnMNPRN zNdj~DqkoivafL7hTu`Yb6z1B9nd_;*Q4deDpxK>r#fMQJ&{$l`$2v$0 z?w!yrV1aM=7VJ839kh$bHstF0&AHBpn}818PQMr)*C_Ku4Qh?0ndMaus`7xcq@1+W z%pe>>YgK}dQurTxwQ``-3dMXTFgPPL(Y@+bFg~FECV)vEMJT09_e{h_SviGxVgB3m z;rU&ec!B&@Mr$UoN`mLt>UX?%)K6MTn&-GM&n*r8aaPb+Z|<#%^|$iccR)0Qzfem7 s0u%!j00008015ps`LO#tIGn*#s<^bM2o1S@6aWAK2mnuYkqps)Pj!!1*S0M6wF3YEst*7F2LJ#7aB^>F za$#-7SKn{jHV}UIUvYbr0Z++*J`9@ep&gPoaMKn^mOd7YbWR9Mq)JkP)71ZakNROz zwj4Suwiz%ilgInM`*^&gPEH_UOYsP=!dKyGcse>c0sA!%_$62JUa@R68Y#?E79+cV zOA#`e6!dd#lJGAn;zB7D2A)PE0G{Pi8IU;&OyIL(d5%icM4U3M;k}GkWC--Re~{Wh z$rNyHhcSuZPRevt&Bjt_ql(x_1;Mx)0zjb)g&KZoSJbu{ng^LwzPF|dzZSf2+fJ}V zQ*2x}0~8Eja_o(@K!Z4ci*yj_XMkLPmYdO5uGdCpJbokB)0=ruwn`r0qKx1Mew`l@ zt~TzQO~BBLS&WZUt8e=fSr+)HU0qi6KLU+rx|n-^^jS*9 z(iB$koxWUvT?$bIxaQhuDDAV=Wi^4aFXKC=2{%|puyCLY-JU5Aur;Ju=0_mivb4Zn zfMqpOhj@Erh$V$s+7Ro-PLQj^&=&@?9x}HBHE_LON1_`-xBCp0gBH+)r*t&J-}V#K z%1Ue^LKsTZn&}Sk?n&9%8Wq8R$J}r!{F15gT4wlXwLcA<3M<|EOs_DLCDuT@G>7-~ z8OqoE8@f`*5ePPX9%*6I51t}i8&qOLPqEB$PGd`!YTQ(<;?pC!7Uwj2@$o`fLzbRZ z3n<9CyJ#4mwkNt_)`47nxH-G}@cR9iE28t}(V#w8GP4eXoS6qo45PSzxbH}}X`|1S zk}7Jd;hkM+UD!k>diDCh zRQfNq+2-HDtaGj@+f?gaUD~G7ZSKML5{6;ZV%+ZGCO=zqnQfkJC{ByY6(&4p25oWW zNprDyYJ?#FSUvU+=m6Y*^PR`D*xx}s4*ZS5)Bz?UtGeYq2G&Ui|9 zjG%=X15(|D>msK5sDmw$%FD(n?k}wA!+Hc`pAs(!e~?kb3a<(bP)h>@6aWAK2mlsxkqps)7IKeQboV@Pu>$}AO%DJ72LJ#7aB^>F za$#-7SHW)EI1s(-D`syJ;8jwfhlSSmqAil$z)f2u+4NX2(l{Y3kt#_EPE-GTNlLOP zTMpe8Xbl*a$>F^BhQk@^-%_$WwOqL6wb&54xomZvLi2>NsXz@>tk z2%ypoW0t@j=XqdfQ_iFkRjRmvFtS4c$Ydo@!XMp=#;Q(!6bxA+eHInPn%t>tPWK)aPpy2J1aY>jqRR4hx%ouOs-s#a=Hj-vuFah z=I5Y{aG@=tQ7sF6l&+YS{-1zEHC@a-qLy5cJckv0)nCfMEQKTiTvMqe)aKcLh*?db z9%}!ONR1n=5?DCUmF&{g18fXoHk%)TbW8FI2Lfw5(n!2LQev$o)<$Bp*b%up41J-n z7$8$K&;U0ZawNLa=w>6qI_LmZd^!OYzu3lFBRp? zA2JbN^8){|`_saS*v4(h^a=}qUSk8aOLKf*pP_tBzn~lHGyz7&50PHjme{8R*9ryO z=%igkQyJqKl^y2*mGlnETvkSCHTvDcqj?bD?*b?h8F5caoUA=qt z_S2PS^ZHStJQut$4#JYC2b~v6Pm<@9Mwi6F_5e zDerqH&ocNZbS7B}H++vk3(>pxG1>>;9PDV`c>S&@{mR&E)9+x?IgP)|w834V>jVAX z9_$El9JgJ;?fP!&lQreV2EwLmjP#4$8-i)Ev9{Ak+?WSW&nX3FG$jg6;iXyI$DdjU z8XfK9@bHe1dA=)o7W=z@i^qY#X?PqQRr)j&l7V|%#TI(L+Q-Qc42 zL;1M9hUt#yy)ym6G#$MN9nBYMoF4^T$_1I zL%;RbG}GsEZ^tHkah*6In!z_vO928D0~7!N00;mUa+A9RISm$ak5_c}JaDlC002#s N0R=1usRRH3000XA@PPmT diff --git a/Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java b/Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java index 33d38947d7..81fd9e48d1 100644 --- a/Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java +++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java @@ -7,11 +7,13 @@ public class AtomicBox { private volatile T val; public AtomicBox(T t) { - val = t; } - public AtomicBox(dafny.TypeDescriptor td, T t) { - this(t); + public AtomicBox(dafny.TypeDescriptor td) { + } + + public void __ctor(T t) { + val = t; } public void Put(T t) { diff --git a/Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs b/Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs index becbb8d78c..19444a5c1a 100644 --- a/Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs +++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs @@ -10,6 +10,8 @@ public MutableMap() { map = new ConcurrentDictionary(); } + public void __ctor() { } + public Dafny.ISet Keys() { return Dafny.Set.FromCollection(map.Keys); } @@ -58,11 +60,14 @@ public class AtomicBox { private T val; private Lock l; - public AtomicBox(T t) { - val = t; + public AtomicBox() { l = new Lock(); } + public void __ctor(T t) { + val = t; + } + public void Put(T t) { l.__Lock(); val = t; @@ -81,6 +86,9 @@ public class Lock { private static System.Threading.Mutex mut = new System.Threading.Mutex(); + public void __ctor() { + } + public void __Lock() { mut.WaitOne(); } diff --git a/Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java b/Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java index a07168500c..7b35aa7b14 100644 --- a/Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java +++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java @@ -6,6 +6,8 @@ public class Lock { private final ReentrantLock lock = new ReentrantLock(); + public void __ctor() {} + public void __Lock() { lock.lock(); } diff --git a/Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java b/Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java index 1fc171ec63..27b718ab42 100644 --- a/Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java +++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java @@ -19,6 +19,8 @@ public MutableMap(dafny.TypeDescriptor td_K, dafny.TypeDescriptor td_V) { this.td_V = td_V; map = new ConcurrentHashMap(); } + + public void __ctor() { } public dafny.DafnySet Keys() { return new dafny.DafnySet(Collections.list(map.keys())); diff --git a/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js b/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js index b327d81031..188e5e0f70 100644 --- a/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js +++ b/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js @@ -3,9 +3,9 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -var Std_ConcurrentInterface = Std_ConcurrentInterface || {}; -var FileIOInternalExterns = FileIOInternalExterns || {}; -FileIOInternalExterns.__default = (function() { +var Std_Concurrent = Std_Concurrent || {}; +var Std_FileIOInternalExterns = Std_FileIOInternalExterns || {}; +Std_FileIOInternalExterns.__default = (function() { const buffer = require("buffer"); const fs = require("fs"); const nodePath = require("path"); diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy index 0296e711b5..4370198604 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy @@ -6,7 +6,6 @@ Std.GoConcurrent replaces Concurrent { class {:extern} MutableMap ... { constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool) - ensures this.inv == inv ghost predicate Valid() { @@ -34,8 +33,6 @@ Std.GoConcurrent replaces Concurrent { class {:extern} AtomicBox ... { constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T) - requires inv(t) - ensures this.inv == inv ghost predicate Valid() { true } diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy index 5e7f5c6f1a..b5b2f17e75 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy @@ -3,7 +3,6 @@ module {:extern} Std.JavaConcurrent replaces Concurrent { class {:extern} MutableMap ... { constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool) - ensures this.inv == inv ghost predicate Valid() { @@ -31,8 +30,6 @@ module {:extern} Std.JavaConcurrent replaces Concurrent { class {:extern "AtomicBox"} AtomicBox ... { constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T) - requires inv(t) - ensures this.inv == inv ghost predicate Valid() { true } diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy index ca0355b00d..08d7ddbc9c 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy @@ -4,7 +4,6 @@ module {:compile false} Std.JavaScriptConcurrent replaces Concurrent { class {:extern} MutableMap ... { constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool) - ensures this.inv == inv ghost predicate Valid() { @@ -32,8 +31,6 @@ module {:compile false} Std.JavaScriptConcurrent replaces Concurrent { class {:extern} AtomicBox ... { constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T) - requires inv(t) - ensures this.inv == inv ghost predicate Valid() { true } diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy index 1079d09ffe..ac29b7f360 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy @@ -3,7 +3,6 @@ module {:extern} {:compile false} Std.CSharpConcurrent replaces Concurrent { class {:extern} MutableMap ... { constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool) - ensures this.inv == inv ghost predicate Valid() { @@ -31,8 +30,6 @@ module {:extern} {:compile false} Std.CSharpConcurrent replaces Concurrent { class {:extern} AtomicBox ... { constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T) - requires inv(t) - ensures this.inv == inv ghost predicate Valid() { true } diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/ConcurrentInterface-notarget-java-cs-js-go-py.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-java-cs-js-go-py.dfy similarity index 93% rename from Source/DafnyStandardLibraries/src/Std/TargetSpecific/ConcurrentInterface-notarget-java-cs-js-go-py.dfy rename to Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-java-cs-js-go-py.dfy index c7f69bd07d..332adb69ce 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/ConcurrentInterface-notarget-java-cs-js-go-py.dfy +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-java-cs-js-go-py.dfy @@ -47,6 +47,10 @@ replaceable module Std.Concurrent { // Invariant on values this box may hold ghost const inv: T -> bool + constructor (ghost inv: T -> bool, t: T) + requires inv(t) + ensures this.inv == inv + method Get() returns (t: T) reads {} ensures inv(t) @@ -68,6 +72,9 @@ replaceable module Std.Concurrent { // Invariant on key-value pairs this map may hold ghost const inv: (K, V) -> bool + constructor (ghost inv: (K, V) -> bool) + ensures this.inv == inv + method Keys() returns (keys: set) reads {} ensures forall k <- keys :: exists v :: inv(k, v) diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy index 3b61ab9195..4843b72d50 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy @@ -3,7 +3,6 @@ module {:compile false} Std.PythonConcurrent replaces Concurrent { class {:extern} MutableMap ... { constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool) - ensures this.inv == inv ghost predicate Valid() { @@ -31,8 +30,6 @@ module {:compile false} Std.PythonConcurrent replaces Concurrent { class {:extern} AtomicBox ... { constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T) - requires inv(t) - ensures this.inv == inv ghost predicate Valid() { true } diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy index 7f87ee27fe..77680d67aa 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy +++ b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy @@ -13,7 +13,7 @@ module // But it makes debugging the translated output a little clearer. {:compile false} {:extern} -{:dummyImportMember "Dummy_", true} +{:dummyImportMember "Dummy__", true} Std.GoFileIOInternalExterns replaces FileIOInternalExterns { method {:extern} diff --git a/Source/DafnyStandardLibraries/src/Std_Concurrent.py b/Source/DafnyStandardLibraries/src/Std_Concurrent.py index 2da109f619..9983f12281 100644 --- a/Source/DafnyStandardLibraries/src/Std_Concurrent.py +++ b/Source/DafnyStandardLibraries/src/Std_Concurrent.py @@ -10,6 +10,9 @@ class MutableMap: + def ctor__(self): + pass + def __init__(self) -> None: self.map = dict() self.lock = Lock() @@ -66,8 +69,12 @@ def Size(self): class AtomicBox: - def __init__(self, t) -> None: + def __init__(self) -> None: + pass + + def ctor__(self, t): self.boxed = t + pass def Get(self): return self.boxed @@ -76,6 +83,9 @@ def Put(self, t): self.boxed = t class Lock: + def ctor__(self): + pass + def __init__(self) -> None: self.lock = threading.Lock() diff --git a/Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go b/Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go index 7bea051e2d..4fe317dba8 100644 --- a/Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go +++ b/Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go @@ -1,4 +1,4 @@ -package DafnyStdLibs_Concurrent +package Std_Concurrent import ( _dafny "dafny" @@ -56,7 +56,7 @@ func (_this *MutableMap) ParentTraits_() []*_dafny.TraitID { } var _ _dafny.TraitOffspring = &MutableMap{} -func (_this *MutableMap) Ctor__(inv func (interface{}, interface{}) bool) { +func (_this *MutableMap) Ctor__() { { } } @@ -188,7 +188,7 @@ func (_this *AtomicBox) ParentTraits_() []*_dafny.TraitID { } var _ _dafny.TraitOffspring = &AtomicBox{} -func (_this *AtomicBox) Ctor__(inv func (interface{}) bool, t interface{}) { +func (_this *AtomicBox) Ctor__(t interface{}) { { _this.mu.Lock() _this.Boxed = t diff --git a/Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go b/Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go index a5c1e88b9e..83ec9a86b5 100644 --- a/Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go +++ b/Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go @@ -1,4 +1,4 @@ -package DafnyStdLibs_FileIOInternalExterns +package Std_FileIOInternalExterns import ( _dafny "dafny" @@ -8,7 +8,12 @@ import ( type Dummy__ struct{} -func INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) { +type CompanionStruct_Default___ struct { +} +var Companion_Default___ = CompanionStruct_Default___ { +} + +func (_static *CompanionStruct_Default___) INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) { p := _dafny.SequenceVerbatimString(path, false) dat, err := os.ReadFile(p) if err != nil { @@ -19,7 +24,7 @@ func INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead return false, datAsSequence, _dafny.EmptySeq } -func INTERNAL__WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) { +func (_static *CompanionStruct_Default___) INTERNAL__WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) { p := _dafny.SequenceVerbatimString(path, false) // Create directories @@ -32,4 +37,4 @@ func INTERNAL__WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (is return true, errAsSequence } return false, _dafny.EmptySeq -} +} \ No newline at end of file