From baa793edd80dd1e1302e0f1860d8ef8378893ab8 Mon Sep 17 00:00:00 2001 From: MartinWho2 Date: Wed, 21 Aug 2024 15:24:02 +0200 Subject: [PATCH] Added auto checker in the CI --- .github/pip-requirements.txt | 3 +- .github/workflows/ci.yml | 5 + .../__pycache__/coq_parser.cpython-310.pyc | Bin 0 -> 10798 bytes .../__pycache__/ecma_parser.cpython-310.pyc | Bin 0 -> 7385 bytes specification_check/coq_parser.py | 344 ++++++++++++++++++ specification_check/ecma_parser.py | 201 ++++++++++ specification_check/expected_text_output.txt | 225 ++++++++++++ specification_check/main.py | 24 ++ 8 files changed, 801 insertions(+), 1 deletion(-) create mode 100644 specification_check/__pycache__/coq_parser.cpython-310.pyc create mode 100644 specification_check/__pycache__/ecma_parser.cpython-310.pyc create mode 100644 specification_check/coq_parser.py create mode 100644 specification_check/ecma_parser.py create mode 100644 specification_check/expected_text_output.txt create mode 100644 specification_check/main.py diff --git a/.github/pip-requirements.txt b/.github/pip-requirements.txt index 880ccd6..444e8cc 100644 --- a/.github/pip-requirements.txt +++ b/.github/pip-requirements.txt @@ -1 +1,2 @@ -alectryon == 1.4.0 \ No newline at end of file +alectryon == 1.4.0 +git+https://github.com/epfl-systemf/SpecMerger \ No newline at end of file diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bebec97..1c4b175 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -106,4 +106,9 @@ jobs: echo "::group::Uninstall Warblre" opam remove --confirm-level=unsafe-yes . echo "::endgroup::" + - name: Run auto checker + run: | + cd specification_check + python3 main.py > actual_text_output.txt + diff -u expected_text_output.txt actual_text_output.txt \ No newline at end of file diff --git a/specification_check/__pycache__/coq_parser.cpython-310.pyc b/specification_check/__pycache__/coq_parser.cpython-310.pyc new file mode 100644 index 0000000000000000000000000000000000000000..58a4d67f1686c01c0404cecd417128e90aace863 GIT binary patch literal 10798 zcmbVSTWlQHd7k^uUbrNe6mO#BjV;Su$|5Z#wOy5=BTc1kCyU8?s+i(Dy_PPfxs6OQgSTDlt7nVZ zdVjIMK2RK}4;BZR&Z*_BgG>ecWWc{(c&n_leMw>cyV0Ud_$x}`rG=; zn#hR0_cYPBW9;a~36b@Wt{S3W47_I*C&i$D%s=WM@yB1%R*i8@E73Cj7x2vzQn9qE!36psS=Pg{5+> z6a)oRS=TE;sI1GCa;WU3t&N(G%)WAS)7vP?uo7094VAdmtk?ZUs8WletTfi%toU~e zma<+eh3hK)T1f`JTntO0uTq>4ua(w(<-`T((0#2La7&1%s3$a9lJ}8v;s%N4tx8Q? zDoL?K*{ia-?KjFa;@+Q$#05OT^9X#cs0*!VyrKD~ZwY-)^KHD1IjnWj@e_z!9CtZx zBkq6?37XF4^-9B6$<<2D_Zp?TuhKPSc#W<4iZ8FKY$fpghVaVmd8gZHqF*Q^mFsaW z&r>PSt2f0Kn(?+;u)fr@Hk%@4gUSG~KHaJ{(|Vk?E~W7N8VAgjx#iPkQc z0zXi0&0h_@+x~r(l$EvhIBMT1)wcYy1-j0U;`Hz+uOmXEjA)eFmM)KWQX$ei`fWqz z1jZhj5opG>su9t?Ku%~1EixjrqVE_~7UzDbFJMEP7`-IcsRVYrtoVT>b`&gm5-<4- z1yd9hDCn+PJaxAuuwgKzNfa{gvwBXq@QfJpH1f)L4*YDSF5n5~5FFgi*vXFXkPM*5 zPtfibhHpVun8L#8cZDsS_q1YCB(OrRN@GuVPMON`3T(6wT_E#l|B)4^-kFyZhzK1k zj<(+eSF8H2v8P=I7xzeRSPR?6v-tznX&Gp91@xRl@C{VEHMVTDbUa3jSgd~!jfQyd zPz>xxXhtSN>j%jyosrHY*J|%iUE%zaD&ugAn+& z)x$lyopxxe1P+3f?wan;w}&6s*#YhzIF1?A1Q)ekeGdz=s7abY!BEzEDOi^;A|Xi@ zKGMDC5rOB?Q2Eql^n+b@2o?${IZ7?i`IO@n(DF*!6_WOdr2Q<9Qo!BOdiQk4r-07B zoI&t3p1?(r(#DLek#RWpk)1yXiVH;g5+>W(`AI!#B+aCiw3CiFD-tBtp#$CaJL%gZ zg(r6_vEHNa8-?N|-)7{e4sugQcGN}Q%hSt+6A$uJH%q6tFP<)< z;_}VqTenUX^5@P?p|O~-@Zbw?Bhmf8c?KPDFVlsHs@{rjR_@%Zl~HkdrVuSp7xFXH zCmx)9`)2<1t?BdB5|f`o>8UtYKpu$BM}-s0rt=@DRM_yJ-|MMVPGa+QeiZL2mIe}#UYZw&P$q~Q971{_Zbdpm z8!ANeoG`KLM%EtXBsuPeiE3((%F>*+xh%tRhvR)5PjEa-3MoF({VEsu42%MA<$fE8 zD7Otj0@YWl)mX6-x`5Iom0xaxF&1UWmoRKe(p(wRR|!hJbpA6aB;=9d za68xCqBEUJDh){sKWHq&b2$Yl7(j$FW7XT+n8GEKMN3|C8OPou2 zc+5S@HEFG?CWHt9f~O+TzDT)H|EtEL_Mx?)^pqrd`!NMjCVBu^(%b^nHCOyKd6skK zB3`P$33yUzlvq1p%qqo@F;+S*#~-74j(Z+KA}S7ORXrfvIzj8wnk;Rs(+UJ6;~isI zAJMbAi@)uuUQT^h^+)su32f#T;Y!RMdgCCcu-}$YR50aRc*);(Ip>}(0Cv4VaNE+K+B4(U2{)s*%1!m``VoL7LKZgza3N88txe_IC)ps0Wfs! zD|jMv*Lq*uLk=A_pqT?aGte*bi~t1h-ZgOTmfO6e6ZN*hRsf)gKN?)j_KJ+WKqtFfScy;DwG(!GY}%A7CG?Um6c@xot!$IG$^C9I^E-Yq!qeu$fg|J{KBQ zior?~#6pmKH-973!{i9G{iQjc)R0T+*M4sS9QwbRW_ zP>c>Utdy&;N)lmngTN%j8c8(ez;Y86sf=czth=S!ZMj0(!(Ml8`%{xAs3=id3D~qD ziB@o9#(ov?n5Pyo6Wnh$VKt-WAeNjYoqoaL>4@rEAPMMPT3~YuvT*{eeo{9c8V_?8 zPW>YXs#Ea*%Sl@ier1;b6cMnSq#Uuk%8Um?#v$cGNVy%Ijtfe@)Urb}vO{afkjtR9 zccHr?yXq3ir<~m+rS|le6Q(*PyJ^Cls67r;pJ?Gw?q(vQaU&NJ)s$a?%ww=J{|D%b*`BI9KTvX^OcJv7Y&G&ZPU>M)fZkrCo7D2)ZR zd=gV$x>^|E)sU|sB}tN~R3)f1a5x)fUnVG*)SR;GrLertU{>jO)L8GbcLXcTtfUXg z zv0hOY^>ujj48@YS4FF;VQbCi!Nd&ZiU{Bz05(jpI<72wfKrE|cLXeiDmEQ&N#v1cz~)3Q z#a^OA5wwy~5_#>?I~u3j6nB8!EiJFf?;eMz4vx>0hx-7>{? zjL?33{;ClrqU4;`cwUE2Ld!pDxBMftoIuMz;+Fp$nu*8B?Z!2Z=|ulgoBpHrNIv3P zf8WzvObriaQVSh{BmA5CW)XZzfo~XFHNjjk_T$WldMh25M`-{e_)I>~0HNx!tE*nSHt_({1~ygSk;EO3!H@=$oniKC20$-!Iwx$$p*o2rupD z#B`wPj=7T)x?wU(?C1dKmPn0ikv*z~E!+^a`niLpY%LNa=N@(a(?|tPyHEKpR4b%gJb2!i1V5WeDFoPX6mq zTMi+MDllM_Ac?f6TUyJNC71%S0Q0k7&V<_(do=2Tua{1O7K)4>BycoMMrQ zlbt$TPPviOvKnr?-5ZfDZ%|I;?!r?Cl?l_an%qr=Y1*gU7ZB{`Kx7A-acf~F9(Sit zZj+Fb+e(IgP>6(tAXhenSRt0^sw0)(|Gn&oK|Wmf^OXkhwjbo1tDJ1hd@3u2d2E=l zRB3PtpN1}7$NbDs9jw6`be}%9s0+P4pNoCU=kgcx=(+9O&l5!6uhtn&yO(?^$YT@c zOAWy^zwDTMyX|R;y~W)!c@MjT5BAjsNk_Yog*P6qUE0!;HS{%#5nz?45U7b>HGgmq zs>$B67y<-aEA7sey(XJm8?mA71b#`j(FV%{_9a6$kb$lGV*f*XrfTpm?mNo3@9;W| z$F0kjlyE$ID{wvDR$1K8wBvLcp~l;U9^4`;z6a+!aIROnTe?s8HGDw>TU_|}*#77H z8W;(|S(Rv4JbdJb4}yYtJNyyG%068Sc03_f@?a0+2xoQ6Ap11+Y05Hm_n`x^KsaQW zk2xJ^7Y7Upj_AKv)e*3|U;Jly1S(}itkYI-`4 zRPyGluUuPNx^npzoY)EJZ`4Y_$v;GYxDkpcZ^Vt#&p_S+@DHfvD=2YLGQ}khO5T8<;d7iyAhnFt1ZZ5u??eN_gkcl{tr4XR zA@idF$p4|p*iA=6?1!LHC1Cl|DBhtlZ=Q%=cQF{C(tQ>49Fz zM#IoPm=GO=?=>X#3ScEt*@n|#}*NFyq2L)V?@_(R{5;RuyKDe6` zF6|?#!T33e5&w-ywfY(-dHkmQZyrCHd}AUVjos1YPopu^OCx7I90L9t=f20Ojc{0y z$HoFboH&m1F=(t)5v>{V=aV*H9z+Atpvdr<9YDEOJ+eCz4ek*p{W55YJ89x1(uHu8 z_!5pq{X05t?ex|}l)>pAY#rqh9OV%llg!&<`LQx%)frRKWoPf#Jc^p zCZo*mL^QdJ`tUW-yKhflW7Cs%6}XY4@ppCw#`87o3#~fY9q*mT_0XOJ&k?vg^MM|0 zQBOG0X54y%5XK;6mIYecU+bOyg+Bi5P#=H#OZM?6hx%~fBO4Sh^Vx2^K%=^Cp#A?m zz>Dr&g1?TE80kOrc>m#GTXfcmIM6 zA^Wg~W=scL;{UUjpM=L^Jl{GN9z$zc*p}nSfkT7eHg0o|iEJC|_b=?@dKQXTS?DWw zvF&5W=LXlVU%qtl#^nckUJbl<@y6n{g_pgn*REgjt}I+$!d2tBbFobQ9TJGYi=c2k z#tsBTRo{&(7cWzlrE5#quc*vRSFXN#BhC!mae_J zuwVDm#lwo*bS*>oPh^gzIK}{hab}#suJG`%dd+pz>prghConnqF9ah% zT^8S`#8|8oy1-dkJ!2T`uq6YHzVe_Ha2WrQhlr>N#TooKxRC`sF&&s~knCcgC8;xR|lM;Oh|e0Kj1+r?M^jE@PC#rOX=5K|dC!j*E}$G1E}lFMKI6$SKNfSNiyNoD|fHV@r& z$%x3|F~@giaCic9N@|2qfBeD0zfdek!M{?#Jo!Gw6aqEc+YfW3ElR#lB;TXp2NW<< z|BYh%tmN1el=o{0K9483fWXz@gXsQ^eL@}y!!SNIOylQi0)8@MKv%u<5*JXe(~)u4mq z{bpkZ-%+v0nH|`%)0(;aDiLo`8-ske%?7EQ*@6@dBrguBpm?eoA{*}|E7dA%a3^~) zIr(ta$=-7E0FaT%9{~En%)ZIaJXcSC7BQI$m=h@yb>g!KJF+oWN4%^PH0Y-(_z4B9 ytVlaCA0M||%AJe9t(&JKADlqoY8hOV4nt_T`WWo3_|G*5^lW0ra+5Gs`~DB*RBPz~ literal 0 HcmV?d00001 diff --git a/specification_check/__pycache__/ecma_parser.cpython-310.pyc b/specification_check/__pycache__/ecma_parser.cpython-310.pyc new file mode 100644 index 0000000000000000000000000000000000000000..bd4e74babd332982eb29efd357be54d74a747503 GIT binary patch literal 7385 zcma)BO>7)TcJ8YFnVz2E@K+)!%Q9ECERWWr5_|umFtTKccI4PxLzH)c3GCkHRFRx< zPtUNrM=MQc5GSOOO%N}8@6iIOPqS)wc}yY?=t&58**C(p@XlP_ALBF`gTHt9)u zZqpM}VtUW1&7lwt~eM_MV01 zb}$`Rmp*v#?x#k7;kc=Ibu%^-Vt=f-xsC2zDMl{JzZN^Z%=VZFU`>#Zp4m{nQsJkkDk){4V4Q`0mu4so9K=1$CId8Dvb z^|T*`Nz{^IsDm(UwM93kbU6%nx=}nVvC){G48tf%+E{k0A3&pC4e8x=hXWnP7|f)(0}1 z3^}~9W!Actabe~8T&KZyu?2memsahyuW7Fo3E;=xl9?_5Z>k|vRWKjb1yXp9#6=Rc z6}g}ZX+IJoq(PrU&djR9FR)8oEg@gWGxjSYcNL1O3n>SeQ{pQ@42-J zv4E0Xe^FdOTNUw~oZRH%qIe#;DRIe^Ps?dpShP%^FNh_S%!qGE7kZb)i^$E2m%sup z7~qOLhxU9}{>$PjO3ouU54~4J6}bh$0q|FKuzL5sJGu2~htg|x2Xi0&C`~XlmU0V; zKDH;c`ZhM!Qh{JwY+(0oe8aXvqIBOrz*dJ2Hr5K=ZP?V`Q3(hT9olQXE2*qsH`dXi zS2vE-b@{lXWSRn<*V`LSSyTKHcGh-8hcVNqw8`3oQ`tT%f+jOCH`812xM=rM~)V9l(3A|BXD(;l$QAsg7`1Ky{-;cLATS^IK6 zG?1FF4wfN0;3`i?$hwMeo8$$E# z-^B`cq6GX$PEmVU2cYOMAY9^87x|N(g=~dvhPdaqw8dMnf)9fMtfOg`MF2a&V!=ubCtPp0I=5a&$#1Efi&k%WY_kkb!r?|O zuf*+o6sNb47*+lHDSmIkZ55TQcU9VW^z6Z_n@1z~eM+s67$22-1K)l?-)}=y1LG(R zDh)ohv)M?5b~5=m)6=l;M~!wj4b#R(jL0C>&yShyaPZxY;rO*rwZkZm^@Xz(a|Y0U zeY+70C6lV3Tk~r)9>S;gJHx<3yICWPrJmYss5A@H<35V$HQG{9XIqyN`P0$bN^l%wO1&8kHmcvv=~)4UmapL zJv&_D^q3M;T^OxaieNPhyVhe0!N44uy!H$Oi0BV8Dd2?({P zWY$&5n9+~{kmnIdm_6yB zU#!SxHSHt*bBX_mO$DE~zHgyb2TbRH3$a?1N1JE?-(16y?g2ZgO{G{vZ_P}|Eacc$ z5Ikw{g!}X)f1xq(7Y2*w4o>nH4h9Qj26}Sk=Eh2LBkDYpOWs4LhD&JpMdPPMiey0 z6NDmqjD0L1k&(Y+@Q8@2!5G8~z>tXLRBqcu2E78g z*LEk^z&DpFORZ&-`Io|?hbXhUdVG^QGq3`dm_qXi6G!Ftb~0j`n0o~0CA zLJP;ZGdH7*7Rj{p&A@08y1={JCU80Z)@7u%ST3*~c;B zfT>HuOPDAOyuQ=4DA2*7o(~HB0_xWWK7v7imt}6#L!ABkP8GFFF2er4_kCc2&bxzR z-*1xk@*seAaHRdt&h36+O3n{T{Zi8xWi0nc{i2uvREqr)5dx^9xbt2gxhBzuNn=}V z6+_RPw=g#JfR>7)g2RM|7XAcjTr7Nw0}uKhji;E82P3rigFa@4aI4s-ONGg`UWN7% z?m~1;z-~yV=g~(*thCd*SZ~L1)Jdf{WJ`vR^37M<>09beXsG8QdgdHJ8>$leb_b$b zQh!M4dn5=LI6X&c7-cx{I)<6;jr2QuaxHq)*orn{xo$jA4x}rj|J)hma0CP|>U3lx zs^uJQ9jZ{IQkqVxB;_4SYddRobTO5nf+%Y%J*663+gZ3BA$~DlM%$Q;_Of<}!>Hy- zrb}rHkqzzuD0n%A;n|ZI9wIS9Z|Q3gflJQTAI2L#t8k7qF-`^G4)8a}%KSW@GWe%V z5&flSz&lWBvc*P(@yrfrbO6Au)CK&NSw&d#Jc0QtF-IxG=h zhNC^Smu}wthR1R-%#W|RM*qM)r@CYam!Sw(NBA0=KDAvW>Lj=dRI4%eZ8P0+O-$b_m4eBU1`4BEw z0T)EN`!>Eg1|T+c-GQI{8X7hLbq^Xo)u-><{E?;Z<{F4{s2-gIixiRwCy$4ce?(1} z=!$AO@Hrl+R4u&E2#iirK?^?04-sRHN(;kMFZomS zMx}qxs3#w@gce8^V?u4u(D^h78r0YiL~+r|N&vdI%Qrdl!J@Tm1CoC|zFx^gv|2)| z|90G}U?AsT{Xg6L2Wk)FDAPCwh2&MVM^50^$$6wEkoxyz8mS6W|B;lDnndb1Nnu#} zUkOgl=9w&7*@T#)J%cGt(>}qFaGQmZRsNjq%=8PReg4?~oT&vf!kIzI%(!%F#--7W zKW95`1~bn}xF)i9^S6WdB=YVq7c+l@uQ1cuVWj$9piL2ym4eW`8zaE~36ed2Z7Fvd z2%n54=Z3vUx^$@O5o=%1$OH7uvAxmiv=t(|?bl$z4<7vR!Of))5@PFEilr>tT52Rq zbO>4+9*LH2F7^1UO9({XMRU4@b3+{`2)cnXmygvc6;Q#%gVj6t?ytQaKD__%-PQb5 zPsE)&r`b{Iz18)*5AMJJ@cs|iOaQ9HSmnES)>qfhJoA$Cp*b#5n`C+FFR7;6!A*On zgC9k4SFS46R{727&~bf6ie$WI^y+g;QIx97xB|ezIWxDTdiG>4GzaEXmrZnwIEXIn z4NvKrZ|doQ?pO0Vr=8i%h=q=s z_%;4C;B?XEgS;Gk&FfJKuHl|K@OVE!4UW1FiJHVfg=uU>~Dk|UQ2CfYE^7-|{sguXiNjSeO*Rt4zJZkMOWa8{@tPG zNxVwpDhZmcvPsbC!oVlLJNOb=-2Kr%4(ctLZMQ{!a3aX6Uy`5!sh^T)k|0Fps3tF& z-w3@;DKp`}rPQ%=J({cf778fNGe=I}3b-F!aQz8hm}3|1nM%dGP^etKP?`Cz(X1}Q z2uJ^?!aoA&oPqG_NeA~z`7})D#?4-*F3tRCr21w0CrsFqYD=o+;nitquJ&ZQEROzz zWtKo+{=byzn2YYn4)x+m#VBrUB@(v;StCvr9ToKS$@2U=F-E>9ULt8n>sDdS*xb~6-31Nr_U`ytnu(=3$W)D9+u7D9P{lN_Htp)|6e>#<0k+B literal 0 HcmV?d00001 diff --git a/specification_check/coq_parser.py b/specification_check/coq_parser.py new file mode 100644 index 0000000..9cb33fc --- /dev/null +++ b/specification_check/coq_parser.py @@ -0,0 +1,344 @@ +import json + +from dataclasses import dataclass +from typing import List, Dict, Tuple +from alectryon.literate import coq_partition, Comment, StringView +import re +import os + +from spec_merger.utils import Path, ParserState, ParsedPage, Parser +from spec_merger.aligner_utils import Position +from spec_merger.content_classes.dictionary import Dictionary +from spec_merger.content_classes.string import String +from spec_merger.content_classes.wildcard import WildCard + + +@dataclass(frozen=True) +class CoqLine: + file_name: str + line_number: int + is_end_comment: bool = False + is_end_file: bool = False + + +def get_file_name_without_path(path) -> str: + return path.split("/")[-1] + + +def add_case(cases: dict[str, Dictionary | WildCard], left_key: str, right_key: str, value: String | WildCard) -> None: + if cases.get(left_key) is not None: + if cases.get(left_key) == WildCard(None): + return + cases[left_key].entries[right_key] = value + else: + cases[left_key] = Dictionary(None, {right_key: value}) + + +@dataclass(frozen=True) +class CoqPosition(Position): + file_positions: Dict[str, Tuple[int, int]] + + def html_str(self) -> str: + return ", ".join( + f"{get_file_name_without_path(file_name)}: {start} - {end}" + for file_name, (start, end) + in self.file_positions.items()) + + def __hash__(self): + return hash(self.html_str()) + + +class COQParser(Parser): + def __init__(self, files: List[Path], to_exclude: List[Path], parser_name: str = "COQ", + title_regex: str = r"(22\.2(?:\.[0-9]{0,2}){1,3})", + spec_regex: str = r"^\(\*(\* )?>?>(.|\n)*?<<\*\)$", + case_regex: str = r"([a-zA-Z0-9\[\]]+) ::((?:.|\n)*)", + algo_regex: str = r"^(?:(?:(?:(?:[1-9][0-9]*)|[a-z]|[ivxlc]+)\.)|\*) .*$", + any_title_regex: str = r"^[ -]*?((?:[0-9]+\.)+[0-9]+)(?: .*?|)$"): + self.sections_by_number = None + self.comments: list[tuple[str, CoqLine]] = None + self.all_filenames = None + self.coq_code = None + + self.name = parser_name + self.files = files + self.to_exclude = to_exclude + self.title_regex = re.compile(title_regex) + self.any_title_regex = re.compile(any_title_regex, re.MULTILINE) + self.spec_regex = re.compile(spec_regex) + self.case_regex = re.compile(case_regex) + self.algo_regex = re.compile(algo_regex) + + @staticmethod + def __get_lines_num_from_paragraph(string_view: StringView) -> tuple[int, int]: + original_string: str = string_view.s + line_start = original_string.count("\n", 0, string_view.beg) + 1 + line_end = line_start + original_string.count("\n", string_view.beg, string_view.end) + if original_string[string_view.end] == "\n": + line_end -= 1 + return line_start, line_end + + @staticmethod + def __get_line_num(string_view: StringView) -> int: + return string_view.s.count("\n", 0, string_view.beg) + 1 + + def __add_file(self, filename: str, files_dic: dict, all_filenames: list): + if any([filename.startswith(excluded.uri) for excluded in self.to_exclude]): + return + with open(filename, "r") as f: + coq_file = f.read() + files_dic[filename] = coq_file + all_filenames.append(filename) + + def __get_coq_code(self) -> Tuple[Dict[str, str], List[str]]: + files_dic: dict[str, str] = {} + all_filenames: list[str] = [] + for file in self.files: + if file.is_dir: + for root, dirs, files in os.walk(file.uri, topdown=False): + for name in files: + self.__add_file(os.path.abspath(os.path.join(root, name)), files_dic, all_filenames) + else: + self.__add_file(file.uri, files_dic, all_filenames) + return files_dic, all_filenames + + def __get_comment_lines(self) -> list[tuple[str, CoqLine]]: + comments = [] + for filename in self.all_filenames: + file = self.coq_code[filename] + partition = coq_partition(file) + for field in partition: + if isinstance(field, Comment) and self.spec_regex.match(str(field.v)): + start_line_num = self.__get_line_num(field.v) + for i, line in enumerate(str(field.v).splitlines()): + line = self.__parse_comment(line) + if line != "": + comments.append((line, CoqLine(filename, start_line_num + i))) + # avoid -1 at start, would have made no sense + if len(comments) > 0: + comments.append(("", CoqLine(filename, -1, True))) + if len(comments) > 0: + comments.append(("", CoqLine(filename, -1, False, True))) + return comments + + # Completely arbitrary in our case + def __merge_comments(self, section1: Dictionary, section2: Dictionary) -> Dictionary: + #print("[WARNING] Merge called for ", section1, section2) + title = section1["title"] if len(section1["title"]) > len(section2["title"]) else section2["title"] + description_first = section1["description"] if len(section1["description"]) > len( + section2["description"]) else section2["description"] + description_second = section1["description"] if len(section1["description"]) <= len( + section2["description"]) else section2["description"] + pos: tuple[CoqPosition, CoqPosition] = section1.position, section2.position + new_files = {} + old_files = (pos[0].file_positions, pos[1].file_positions) + for filename in old_files[0].keys() | old_files[1].keys(): + match (filename in old_files[0].keys(), filename in old_files[1].keys()): + case (True, True): + new_files[filename] = (min(old_files[0][filename], old_files[1][filename]), + max(old_files[0][filename], old_files[1][filename])) + case (False, True): + new_files[filename] = old_files[1][filename] + case (True, False): + new_files[filename] = old_files[0][filename] + case _: + raise Exception("This should never happen") + new_cases = {} + for case in section1["cases"].entries.keys() | section2["cases"].entries.keys(): + if section1["cases"][case] is not None and section2["cases"][case] is not None: + section1["cases"][case]: Dictionary[String] + for key in section1["cases"][case].entries.keys() | section2["cases"][case].entries.keys(): + if section1["cases"][case][key] is not None: + new_cases[case] = section1["cases"][case][key] + else: + new_cases[case] = section2["cases"][case].entries[key] + elif section1["cases"][case] is not None: + new_cases[case] = section1["cases"][case] + else: + new_cases[case] = section2["cases"][case] + return Dictionary(CoqPosition(new_files), {"title": title, "description": description_first + "\n" + + description_second, + "cases": Dictionary(None, new_cases)}) + + + def __get_comment_titles(self) -> Dict[str, Dictionary]: + """ + Gets the indices of the comments that contain the titles of the sections (comments that match the title_regex) + :return: A dictionary with the title of the section as key and the indices of the comments that contain the + section as value + """ + title_indices = {} + wildcard_sections = set() + current_block = "" + last_block_end = 0 + section_to_be_thrown_away = False + for comment_index, comment in enumerate(self.comments): + if res2 := self.any_title_regex.match(comment[0]): + if current_block != "" and not section_to_be_thrown_away: + if title_indices.get(current_block) is not None: + # This means the section was split + title_indices[current_block] = self.__merge_comments( + self.__parse_subsection((last_block_end, comment_index), wildcard_sections), + title_indices.get(current_block)) + else: + title_indices[current_block] = self.__parse_subsection((last_block_end, comment_index), + wildcard_sections) + last_block_end = comment_index + elif current_block != "" and section_to_be_thrown_away: + last_block_end = comment_index + current_block = res2.group(1) + section_to_be_thrown_away = self.title_regex.search(str(comment)) is None + if not section_to_be_thrown_away: + title_indices[current_block] = self.__parse_subsection((last_block_end, len(self.comments)), + wildcard_sections) + for section in wildcard_sections: + title_indices[section] = WildCard(None) + return title_indices + + def __parse_title(self, title: str) -> str: + + lines = title.splitlines(keepends=False) + title = lines[1].lstrip() + for line in lines[3:-1]: + title += "\n" + line.lstrip() + return title + "\n" + + def __parse_comment(self, comment: str) -> str: + return (comment.replace("\n", "").replace("(*>>", "").replace("<<*)", "") + .replace("(** >>", "").replace("[OMITTED]","").lstrip().rstrip()) + + def __parse_subsection(self, comment_indices, wildcard_indices: set) -> Dictionary: + comment_lines = self.comments[comment_indices[0]:comment_indices[1]] + + title = "" + description = "" + parser_state = ParserState.READING_TITLE + saved_state = ParserState.BEFORE_START + wildcard_state = "" + in_case_title = False + cases: dict[str, Dictionary| WildCard] = {} + current_case = "" + current_case_titles = [] + skip_until_end_file = False + filenames = {} + case_line_indices = [-1, -1] + wildcard_comment = "" + for parsed_comment, coq_line in comment_lines: + # We are at the end of a comment + if coq_line.is_end_comment or coq_line.is_end_file: + match parser_state: + case ParserState.BEFORE_START: + parser_state = ParserState.READING_TITLE + case ParserState.READING_TITLE: + if coq_line.is_end_comment: + parser_state = ParserState.READING_DESCRIPTION + case ParserState.READING_DESCRIPTION: + pass + case ParserState.READING_CASES: + pass + case ParserState.READING_WILDCARD: + if wildcard_comment != "": + if wildcard_state == "Sections": + sections = json.loads(wildcard_comment) + wildcard_indices.update(sections) + wildcard_comment = "" + parser_state = saved_state + if coq_line.is_end_file: + skip_until_end_file = False + continue + if skip_until_end_file: + continue + # Get file name + filename = coq_line.file_name + # If not already in, add it and add its current line + if filenames.get(filename) is None: + filenames[filename] = (coq_line.line_number, coq_line.line_number) + # Otherwise update last line + else: + before_indices = filenames[filename] + added_index = coq_line.line_number + new_indices = (min(before_indices[0], added_index), max(before_indices[1], added_index)) + filenames[filename] = new_indices + if parsed_comment.startswith("WILDCARD"): + saved_state = parser_state + parser_state = ParserState.READING_WILDCARD + wildcard_state = parsed_comment.split(" ", 1)[1] + if wildcard_state == "PARSING_FILE_END": + skip_until_end_file = True + elif wildcard_state != "Sections": + case_wildcarded = json.loads(wildcard_state) + if " ::" in case_wildcarded: + parts = case_wildcarded.split(" ::") + add_case(cases, parts[0], parts[1], WildCard(None)) + else: + cases[case_wildcarded] = WildCard(None) + continue + if parser_state == ParserState.READING_WILDCARD: + if wildcard_state == "Sections": + wildcard_comment += parsed_comment + "\n" + continue + if self.case_regex.match(parsed_comment): + parser_state = ParserState.READING_CASES + if current_case != "": + case_pos = CoqPosition({coq_line.file_name: tuple(case_line_indices)}) + for case_title in current_case_titles: + add_case(cases, case_title[0], case_title[1], String(case_pos, current_case)) + current_case_titles = [] + case_line_indices[0] = coq_line.line_number + case_line_indices[1] = coq_line.line_number + match = self.case_regex.match(parsed_comment) + current_case_titles.append([match.group(1), match.group(2)]) + current_case = "" + in_case_title = True + + else: + match parser_state: + case ParserState.READING_TITLE: + if self.algo_regex.match(parsed_comment): + # If there is a start of an algorithm, but we are still building title, it means that there + # is only one case in the subsection, and therefore we set its title to "" + case_line_indices[0] = coq_line.line_number + case_line_indices[1] = coq_line.line_number + parser_state = ParserState.READING_CASES + current_case = parsed_comment + "\n" + if not current_case_titles: + current_case_titles.append(["", ""]) + else: + title += parsed_comment + parser_state = ParserState.READING_DESCRIPTION + case ParserState.READING_DESCRIPTION: + if self.algo_regex.match(parsed_comment): + # If there is a start of an algorithm, but we are still building description, it means that + # there is only one case in the subsection, and therefore we set its title to "" + case_line_indices[0] = coq_line.line_number + case_line_indices[1] = coq_line.line_number + parser_state = ParserState.READING_CASES + current_case = parsed_comment + "\n" + if not current_case_titles: + current_case_titles.append(["", ""]) + else: + description += parsed_comment + " " + case ParserState.READING_CASES: + case_line_indices[1] = coq_line.line_number + if self.algo_regex.match(parsed_comment) or not in_case_title: + if not current_case_titles: + current_case_titles.append(["", ""]) + in_case_title = False + current_case += parsed_comment + "\n" + elif in_case_title: + current_case_titles[-1][1] += "\n" + parsed_comment + if current_case != "": + case_pos = CoqPosition({comment_lines[-1][1].file_name: tuple(case_line_indices)}) + for case_title in current_case_titles: + add_case(cases, case_title[0], case_title[1], String(case_pos, current_case)) + cases_dict = Dictionary(None, cases) + return Dictionary(CoqPosition(filenames), {"title": String(None, title), + "description": String(None, description), + "cases": cases_dict}) + + def get_parsed_page(self) -> ParsedPage: + if self.sections_by_number is None: + self.coq_code, self.all_filenames = self.__get_coq_code() + self.comments = self.__get_comment_lines() + self.sections_by_number = self.__get_comment_titles() + return ParsedPage(self.name, Dictionary(None, self.sections_by_number)) diff --git a/specification_check/ecma_parser.py b/specification_check/ecma_parser.py new file mode 100644 index 0000000..6e61990 --- /dev/null +++ b/specification_check/ecma_parser.py @@ -0,0 +1,201 @@ +from dataclasses import dataclass +from typing import Dict, List + +import bs4 +import requests +from bs4 import BeautifulSoup, PageElement +from spec_merger.content_classes.dictionary import Dictionary +from spec_merger.content_classes.string import String +from spec_merger.aligner_utils import Position +from spec_merger.utils import ParserState, ParsedPage, Parser + + +@dataclass(frozen=True) +class URLPosition(Position): + url: str + + def html_str(self): + return f"{self.url}" + + +def add_case(cases: dict[str, Dictionary], case: tuple[str, String], key: str): + # lines = OrderedSeq(case[1].position, list(map(lambda x: String(None,x),case[1].value.split("\n")))) + if cases.get(key) is not None: + cases[key].entries[case[0]] = case[1] + else: + cases[key] = Dictionary(None, {case[0]: case[1]}) + + +class ECMAParser(Parser): + + def __init__(self, url, parser_name="ECMA", sections=None): + self.name = parser_name + if sections is None: + sections = ["sec-regexp-regular-expression-objects"] + self.sections = sections + self.url = url + self.page = self.__get_page() + self.sections_by_number: Dict[str, Dictionary] = None + self.avoid = {None, "emu-note", "\n"} + + def __get_page(self): + html_spec = requests.get(self.url).content + soup = BeautifulSoup(html_spec, 'html.parser') + return soup + + def __parse_section(self, section_html: BeautifulSoup, sections_by_number: Dict[str, Dictionary]): + position = URLPosition(self.url + "#" + section_html.get("id")) + title = section_html.find("h1").find("span", {"class": "secnum"}).text + first_subsection = section_html.find("emu-clause") + if first_subsection is not None: + paragraph = [x for x in first_subsection.previous_siblings if x.name not in self.avoid][::-1] + sections_by_number[title] = self.__parse_subsection(paragraph, position) + for new_section in section_html.find_all("emu-clause", recursive=False): + self.__parse_section(new_section, sections_by_number) + else: + paragraph = [x for x in section_html.children if x.name not in self.avoid] + sections_by_number[title] = self.__parse_subsection(paragraph, position) + + def __preprocess(self, sections): + sections_by_numbers = {} + for section in sections: + html_section = self.page.find("emu-clause", {"id": section}) + self.__parse_section(html_section, sections_by_numbers) + self.sections_by_number = sections_by_numbers + + @staticmethod + def __strip_sides(string: str) -> str: + return string.replace("\n", "").replace("\t", "").lstrip().rstrip() + + def __parse_list(self, ol_or_ul: BeautifulSoup, list_type: str = "ol", prefix: str = "") -> str: + result = "" + for li in ol_or_ul.children: + if li == '\n': + continue + if (sub_list := li.find(list_type)) is not None: + result += prefix + "".join( + [self.__strip_sides(self.__parse_p(x)) for x in sub_list.previous_siblings][::-1]) + "\n" + result += self.__parse_list(sub_list, list_type) + else: + result += prefix + self.__strip_sides(self.__parse_p(li)) + "\n" + + return result + + def __parse_emu_alg(self, emu_alg_section: BeautifulSoup) -> str: + # An emu-alg always contain a single
    containing a lot of
  1. elements and can also contain other
      + # elements + main_ol = list(emu_alg_section.children)[0] + return self.__parse_list(main_ol) + + def __parse_emu_mods(self, mods: PageElement): + match list(mods.children)[0]: + case "emu-opt": + return "_" + mods.text + case _: + return mods.text + + def __parse_emu_grammar(self, emu_grammar_section: BeautifulSoup) -> list[list[str]]: + # an emu-grammar always contains one or multiple emu-production which themselves contain : + # - an emu-nt + # - an emu-geq + # one or multiple emu-rhs which all contain one or more element + emu_prods = emu_grammar_section.find_all("emu-production") + result = [] + for prod in emu_prods: + tmp = ["", ""] + tmp[0] = prod.find("emu-nt").text + separator = " " if prod.has_attr("collapsed") else "\n" + right_hand_sides = prod.find_all("emu-rhs", recursive=False) + for rhs in right_hand_sides: + # hack to avoid beautiful soup to add \n for no reason ? + if type(rhs) is bs4.NavigableString: + continue + tmp[1] += separator + to_add = "" + for nt in rhs.children: + if type(nt) is bs4.NavigableString: + continue + for small_child in nt.children: + if small_child.name == "emu-mods": + to_add += "_" + self.__parse_emu_mods(small_child) + else: + to_add += small_child.text + to_add = to_add + " " if to_add != "" else "" + # remove last space + if to_add[-1] == " ": + to_add = to_add[:-1] + tmp[1] += to_add + result.append(tmp) + return result + + def __parse_p(self, p: BeautifulSoup): + res = "" + if type(p) is bs4.NavigableString: + return p.text + for child in p.children: + match child.name: + case "emu-grammar": + res += " ::".join(f"{x[0]} ::{x[1]}" for x in self.__parse_emu_grammar(child)) + case "sup": + res += "^" + child.text + case _: + res += child.text + return res + + def __parse_subsection(self, subsection: List[BeautifulSoup], position: URLPosition) -> Dictionary: + title = "" + description = "" + cases: dict[str, Dictionary] = {} + current_case = "" + current_case_titles = [["", ""]] + parser_state = ParserState.READING_TITLE + for children in subsection: + match children.name: + case "h1": + title += self.__strip_sides(children.text) + parser_state = ParserState.READING_DESCRIPTION + case "p": + if parser_state in {ParserState.READING_TITLE, ParserState.READING_DESCRIPTION}: + parser_state = ParserState.READING_DESCRIPTION + description += self.__strip_sides(self.__parse_p(children)) + " " + else: + pass + case "ul": + match parser_state: + case ParserState.READING_TITLE: + title += self.__strip_sides(children.text) + " " + case ParserState.READING_DESCRIPTION: + description += self.__parse_list(children, "ul", prefix=" ") + case ParserState.READING_CASES: + current_case += self.__parse_list(children, "ul", prefix="* ") + case "emu-alg": + parser_state = ParserState.READING_CASES + current_case += self.__parse_emu_alg(children) + for current_case_title in current_case_titles: + add_case(cases, (current_case_title[1], String(position, current_case)), current_case_title[0]) + current_case = "" + current_case_titles = [["", ""]] + case "emu-grammar": + parser_state = ParserState.READING_CASES + if current_case != "": + for current_case_title in current_case_titles: + add_case(cases, (current_case_title[1], String(position, current_case)), + current_case_title[0]) + current_case = "" + current_case_titles = self.__parse_emu_grammar(children) + case "span" | "emu-table" | "emu-import" | "h2" | "emu-table": + pass + case _: + print(f"ERROR: Unhandled tag in html section : {children.name}, {children.text}") + raise ValueError + if current_case_titles != [["", ""]]: + for case_title in current_case_titles: + add_case(cases, (case_title[1], String(position, current_case)), case_title[0]) + return Dictionary(position, {"title": String(None, title), + "description": String(None, description), + "cases": Dictionary(None, cases)}) + + def get_parsed_page(self) -> ParsedPage: + if self.sections_by_number is None: + self.__preprocess(self.sections) + return ParsedPage(self.name, Dictionary(None, self.sections_by_number)) diff --git a/specification_check/expected_text_output.txt b/specification_check/expected_text_output.txt new file mode 100644 index 0000000..6711d4d --- /dev/null +++ b/specification_check/expected_text_output.txt @@ -0,0 +1,225 @@ +DICT: OK + 22.2 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.1 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.1.1 DICT: OK + title STRING: OK + description STRING: OK + cases DICT: OK + Pattern DICT: OK + QuantifierPrefix DICT: OK + AtomEscape DICT: OK + NonemptyClassRanges DICT: OK + NonemptyClassRangesNoDash DICT: OK + RegExpIdentifierStart !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + RegExpIdentifierPart !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + UnicodePropertyValueExpression !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.1.2 DICT: OK + 22.2.1.3 DICT: OK + 22.2.1.4 DICT: OK + title STRING: OK + description STRING: OK + cases DICT: OK + DecimalEscape !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.1.5 DICT: OK + 22.2.1.6 DICT: OK + title STRING: OK + description STRING: OK + cases DICT: OK + ClassAtom !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + ClassAtomNoDash DICT: OK + ClassEscape DICT: OK + CharacterEscape DICT: OK + RegExpUnicodeEscapeSequence DICT: OK + HexLeadSurrogate DICT: OK + HexTrailSurrogate DICT: OK + HexNonSurrogate DICT: OK + 22.2.1.7 DICT: OK + 22.2.1.8 DICT: OK + 22.2.1.9 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.1.10 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.2 DICT: OK + 22.2.2.1 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.2.1.1 DICT: OK + 22.2.2.2 DICT: OK + 22.2.2.3 DICT: OK + 22.2.2.3.1 DICT: OK + 22.2.2.4 DICT: OK + 22.2.2.4.1 DICT: OK + 22.2.2.5 DICT: OK + 22.2.2.6 DICT: OK + 22.2.2.7 DICT: OK + title STRING: OK + description STRING: OK + cases DICT: OK + Atom DICT: OK + PatternCharacter STRING: OK + . STRING: OK + CharacterClass STRING: OK + ( GroupSpecifier_opt Disjunction ) STRING: OK + (?: Disjunction ) !MISALIGNMENT! Matched Wildcards + WildCard + STRING: OK + AtomEscape DICT: OK + 22.2.2.7.1 DICT: OK + 22.2.2.7.2 DICT: OK + 22.2.2.7.3 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.2.8 DICT: OK + 22.2.2.9 DICT: OK + title STRING: OK + description STRING: OK + cases DICT: OK + ClassRanges DICT: OK + NonemptyClassRanges DICT: OK + NonemptyClassRangesNoDash DICT: OK + ClassAtom !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + ClassAtomNoDash DICT: OK + ClassEscape DICT: OK + CharacterClassEscape DICT: OK + UnicodePropertyValueExpression !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.2.9.1 DICT: OK + 22.2.2.9.2 DICT: OK + 22.2.2.9.3 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.2.9.4 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.3 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.3.1 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.3.2 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.3.3 DICT: OK + 22.2.3.4 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.4 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.4.1 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.5 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.5.1 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.5.2 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.1 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.2 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.3 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.4 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.4.1 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.5 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.6 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.7 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.8 DICT: OK + 22.2.6.9 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.10 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.11 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.12 DICT: OK + 22.2.6.13 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.13.1 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.14 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.15 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.16 DICT: OK + 22.2.6.17 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.6.18 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.7 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.7.1 DICT: OK + 22.2.7.2 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.7.3 DICT: OK + 22.2.7.4 DICT: OK + 22.2.7.5 DICT: OK + 22.2.7.6 DICT: OK + 22.2.7.7 DICT: OK + 22.2.7.8 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.8 DICT: OK + 22.2.8.1 DICT: OK + 22.2.9 DICT: OK + 22.2.9.1 DICT: OK + 22.2.9.2 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.9.2.1 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK + 22.2.9.2.2 !MISALIGNMENT! Matched Wildcards + WildCard + DICT: OK diff --git a/specification_check/main.py b/specification_check/main.py new file mode 100644 index 0000000..641f207 --- /dev/null +++ b/specification_check/main.py @@ -0,0 +1,24 @@ +from spec_merger.aligner import Aligner +from coq_parser import COQParser +from ecma_parser import ECMAParser +from spec_merger.utils import Path + + +def main(): + paths = [Path("../mechanization/spec/", True)] + files_to_exclude = [Path("../mechanization/spec/Node.v", False)] + url = "https://262.ecma-international.org/14.0/" + + coq_parser = COQParser(paths, files_to_exclude) + coq_parsed_page = coq_parser.get_parsed_page() + ecma_parser_v14 = ECMAParser(url, parser_name="ECMAScript v14.0") + ecma_parsed_page_v14 = ecma_parser_v14.get_parsed_page() + + a = Aligner() + result = a.align(coq_parsed_page.entries, ecma_parsed_page_v14.entries) + text_result = result.to_text() + print(text_result) + + +if __name__ == "__main__": + main()