From cf31ffd68bba2d3c15dc9b70ba7db3b94a2f22a9 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 28 Nov 2018 10:49:35 +0100 Subject: [PATCH 01/13] revisions of scholarly paper and report ontologies --- .../IsaDof_Manual/IsaDofManual.thy | 2 +- .../output/document.pdf | Bin 626548 -> 626413 bytes ontologies/scholarly_paper.thy | 33 +++++++++--------- ontologies/technical_report.thy | 16 +++++---- 4 files changed, 28 insertions(+), 23 deletions(-) diff --git a/examples/technical_report/IsaDof_Manual/IsaDofManual.thy b/examples/technical_report/IsaDof_Manual/IsaDofManual.thy index 226d5a0..f2efeaf 100644 --- a/examples/technical_report/IsaDof_Manual/IsaDofManual.thy +++ b/examples/technical_report/IsaDof_Manual/IsaDofManual.thy @@ -3,7 +3,7 @@ theory IsaDofManual imports "../../../ontologies/technical_report" begin -open_monitor*[this::article] +open_monitor*[this::report] (*>*) title*[tit::title]\The \isadof User and Implementation Manual\ diff --git a/examples/technical_report/TR_my_commented_isabelle/output/document.pdf b/examples/technical_report/TR_my_commented_isabelle/output/document.pdf index 782eafa9228ca6850af66b190e6b8ff732407067..0a935e7edcd5c4a8b6b65c9279b0333612b47546 100644 GIT binary patch delta 23104 zcmV(zK<2;no+j;`Ca_!q5!%xs1jOlVBxRR6`vcC-Yr2!6zZ0{70U$I1GnY{t1Sx;* zntzNG5x=L0~f&^;1bvYI|r8?#*cqp^UjUzYsHe@$!@6d<=JnZ@8FL{i9NvoD--g+no-ZM z*6e@heF6U)nU8+VK|c!k>n+)o_;CpT+L$>mRQW{hzXyL;%&GhBYe=?U`F*wCn3&JI zC#(H-ihS^ABeJ!*Z-9KC6n);sc_qFLD?DG~A@N|Vj(^B+59@jG)6wZO{%!z%`|Q`v ze4F#F!#{@D%PA2*?`d7un|~L3;Cuo6+QEN%W#Y%};1c?NE&3IT{>J6k0kvMI_?J%= zz8Coxx$kKjc~?JBoq96IhXlflJlkF*In3;^B;v@X-LWc5bsAtKkI+T zjrns0{`PD1$=a^wZ;1B)=S@8;kCH$Bp&|O2-a9xob%wm7*54KJLh{xn7W=sfM=PKW&G0?7}D$k*GyANp1uRQDM@_W0}{;xCumwOK!Z zqFR5k#3SOxDahOA{s*booUasakI8?JBKEmk>L2Q_+=O(_?>DRU`ckrg2YyT=9{S|J zzu^1@^4sN7?}P7?dJp`d)Gy%2q+Y^4ZWMlCU*~gvk9cv1*emwCl=&s>eN8lf$%Xm6 z)35N`*q_CEKG+?l)@!+#_3>9vMDgM3{SUmBLBAaKuW;UHrCtOtmU<5SN2z}=xzARf z4;f!7^)U6x?>K*+eC3eDyB0P6lJpP2uWRZDn|k9hO}q?=4_;$^_zwsDJRSZNsQ))4 z^p8IL_C^{;unns4rH<)Xxg{ zzu`E=+tOCGe>IASpWL`{%u(a;>$eHxjgNntt>H&N{kVa6>r!uY>FN>ue``Z+_~8+M zy2%f0?BQ9>`K!!7C!s&elW%XVll;-$sqRy(k$-iG504^0ANe=8W`2JVBmSEH;BW9J9{M$OAf@w@&pgQfW%Q*@XOHw7dNli&$q%lHnZE?&Z|_S! zK)>mrMql&vn+~zRMSa>9#mhfTzwRFa{k92pl0TKGFMpa+JonIt?v&z-h5S2GI$wzV zR!TlkJYE&~Lp!2?`e1)s+K z|HA)GN~muk_q+E%o%l2Ioz*`O|D84k^uG^kh4irJsBcKvU@=g?nR1;2k>_|>J6ht2c0ykEiJ zp9l7i=)bu5!{+Gc)&+OoQ$XIn^e?c#zmq=}xKF>Fk9fB(`giBe^P7#u9Z{d)-v>4M zn1z3T`Tz8OdFrLjDftH%eHuJQ{g({>=qJQ;hkW3qxbJg`m-9HUk3C)0_}~1ZV_HD} zcfE!`dGuowxWIq+4O685&-W4IIA6&7({nhVL;m@KVERQX?1cKt`;6Ch`6K@5mdL+$ zPxa>%k$-5`yJdb&-lL?FG&Ah=7TqZ zOW@5SFV1gCenmay^ZuhO{bc4>z;A*B@LRGU`M^`$C#WjiDE^W6Q7zzr`#voGi}l`S zJ)3;)T@D#9-a?*ev91iEWS?>{!rh&D)E%@ZL%M@Pws>NnkDi^A4Z@L z4)fn(+y!r!`QUfueHOS1&VzTvw4W03=kb{KT4w%+37NVii~RCm_(uo*IXR{Nx=pss0+(fY#?ENpThx3iOCEkZTUnljlg@5}nX8f{vAN0H?|106o=d~p} zPX&GaeMD1WI*Np={DTR}fZ4-m+K8Nf+0f+290*CBA1BdKB z1h?!y1v2>rF*r9km$9$|6a_IdG&VAq;THuce{*wirr)x4Y}HNnK0*iODVzjM#Ib*sL5{@C5CSJz&>c0Uv(k`DH+>RygO76ukZW?q1rq^bf7 zJ3BLgnUM{Sf)6g2=+KzpFGi7i0c&D7S~3?Of92DEnp(f}+RoB_7~P5@>O_U6|A(&WPU zj{tjjptI{=VHVB~b^rwlbrDG=MRkCLe;AXx7{J8d93U_Kx82^=h4(KTXy$D9uj%Lk zuK$f}P5v91{x|w>)!Fmk5hEN63&7mk%oSh?w6wN|WBQkGGWHe@0M38I=5CJvDg71X z@>d^#`mcvH0CS+lU$&dAt)ht?5I`;FVCU%O3Umf2IG6*S?E$I|b|&`!VVT%jf7^Qf ze|i7Ika0En>w}2Bl|C=kAxH?;Ve**NF8UM8&%>VlS6B+z3OH|as(}#hDiyOee#=-+& zVdG*3@UXLg|37lg+?<_(_OAaJ{&$xDk##B+K$T*NHZJSv zheX+qUt7Glm!dJCLd(?sL;&v5Rin&Vg%)0#3O)Z`2Mf;+-bJ{gz%{ZeEDv-%2-p4D z4h){wWbIf#6Hp<1VV~v{fA?lt0=%;DX^{*%hTeNN_@U$CYE?70)dh7Ov(<)xRq%a3 zw+`^>D8rz=nZYE?cqqx74^MxQ3cRY8?im}Qha9$HvvaD{Rs-SWkhLfG*{%uzcy}Ccn{NbT^)%9&1Io9gf4yxz2FFSPkq}Ro zp{lp&Bd#+3LAj}c4D7HxPh4Csgw*Mv>W5`d4^ZCIIqq?iGR;KlDnd-2o*2ZVxTd~j z??#<1LKZYum_n$X8oGY@%_kAx@hmQK?s}l=X~USaoLRu9=n`CmX;Eba&+_HO){+I0 zrPj;np%7;YQ4Ybze@c&PhN*i_=xYfBXad>f6<;fDKB?_G4d89e|Ir)9-P;ts?K=H*ril8hoo~0bkJBnP$r_>NgKaqK$Qzz~#Z92LZnPr}# z%u-kllt#NAfxuFAvSXI6pXHP)fkaAhfenI6gx()gpn<(!K7pD6*-?0nepX*Yn)4hs;Ba^Ill%|+Ba^SdrD$dY9{`m znZ~UqrZ+PXkE6*miCc}}Pd3XVBuYwW1&{QwVfS_rhL{>MSvOX&>;ef2+(u@xr4+*!p0jX!TY0(z#(A z1y&REU8Txu1G*crkheTqzXAW$kktakV%@S$ioP@8ebN z#|2=BFZTNjykt`}g$(@|xIuyKnoxlatyo03OY)P~dLtG~fDjHgj$umafL0mQ9qG_b z<=704e^}>~x2k2^tDr04Ci7BHy1Vp`*F4Xm7W#w8UGG1IWZj&qFbmWR^NiZxOIxjS zTz6BATz2>Adu6a*W+ia$8Yy%0PF*dAeO~oeD0s}b#KyM^r;b4)o495N2opJ+)sRG5 zHNBH3twN{W9lXx1?bOdnQ_$O`4f{uL?Hqt<0Po~SwkpTf)ir9}1e zy7Kz4f+orddag%8?(-!xa&fh{4j1GhWLbY=Rj^b38x<`vTNIawN;~um>0> zS6*L7p&%Mu)?!~g&}0QX%-)~o>80Y9t7po;N(aOw7<>E8U%TxQXD$Xc9+DNsLCL#6 zf7d;6GFd|ppPb7jfzHwfJ6F=ln-fAb*$#-0F67!+0QGs3S{Zq?r zWYadnN}Efj0X1#CtS~167n1sXfgPA`;m1CRRC;}s%p*DNl@xW0ZKXGmE-;qf(dj7{A|CN|PkCe#ip zHmB~?B6D88iCVvKE|kJdC2Mmee>YL^C%L*gCkTTv08vvrx0OAK1(oEa zWtZF`mk^;X%~(*#WC^p6Gc#GTfjUhVCa*CnENj$Yeb+{}^t-Ck+XPhae`Ya{3K)b* z=*5)FUBAs>MA>TxeM46VRF1{e*|Qu|n53x0m!(-$UW68P@%_v$|L#j8f0;`ncmql& z>Ju8=qx$E{Sj#SS`&_0-I-j9Dk!~(SqC#BW?{|2*_r~e&8im%Y%!X8@z=MRIwucfz z;`DZoL1ToOP|nL#$In~y2d|t8oVjPNm+^ubwo5sueh2zUV&^|!<+W5L?{!|1(Xu7@DLmrrHc|u}ur#!|bbw z^fWrrRJs%(HJcNtDM)Z+bgB_dBeRfsN^io`9(iNFRVX}gh5)XBvIHqZ6n&#P zG=nab#G`Z|F|GzQ2u)7NRS8mZg~e&kU>+#KU3500ym}dT(qfA=f1YJvxedkj!ryvt z>o>iw84Y9yG>U&t@FuJHdrDz3Q^TO{#=wl1jbn+@UYpZi`9Nl$WCUL9wC>m9>XN-5 zi3QO9@DWeWudU$aj09nkU+zZ?7Y7}N68Lbf_P|%uA-vuy%Y!JWQ21K>tyc(A(`7pD zUWw_u4P^vvptbgZe|_3jEE;`v~Rc-BfSbTUcCSIwb% z&qkg$EeVEH_R=CY+tMwSdxNHvLLK&Pa#s#7C1EfOL~S(d5Xcd$Les~K&k2e*@1(rG z_3m0iJalCG4KQa>FGxEqtyFiqV|T7`|1{rDJFnUkv`yVJ@+5-dnbh8DcpMwlbE_qzu*WP6H z>AdeM4vp8;e-#a{+wd|HqC$C+6uk|MJ>mLDF?`w9E~_e#x289>7Mci~V(8|^V`o_W zK*8f|CQL8+_WO&a1y%1Yf0HG-Uvw66#UhG#d?cld_s-1(cI^cC!!0|Q`g0kNaw~;=IVZp12DNA{;)v5fENGxD0LsHMS zaqIZs35zIF-TBt+IW?yB{TBFD14Cr;u)KDU`ZP1}S7Sp?c8P>)>?;NiEAJz!#4i9c z%)cKQe=dmNnEx2W@33vA*=T4BZJpM~yod44uG%yxkDRwo(g-RGMKaPZRxE<#pjT_& zuPD|#ViZ$(wfTIi^F)8MbGg`0sJ2jd2Mh|MXa-1DYAfE_CaKUyLASBbj?J zj7j3UAf!DgapL`IznG2f+zoy%pHMnxv^f{pf7J&m2R6yBGb7Y*4(^v`pvM%Cp9Lun z&+0Geztv(=D38A{mI?TN(?1LjyaEP}l&Qd)qP;rzo_?8U3??K&j~Mc0dqlmTF(EYd z$X`{9=4yi@vtSkCN=A$XFT$+W3*}n?CV9zY`&6z&{Bw42^i>yS?n4UkZGk?T>4JO|d zybas+1p2_H=n`Iro8O;kVA`d)AhMnieI2-h|%Ren^sN z899+i2e5@c7@-*HB2#feJI=gnahm&IaPa^$rp}q0p;%ACMGIG3kTKzHMoAsDGd`l~ z3+?4eRCRs#jhUk#m`$6pzv5%k<|~d8I&mrQLLaB23U+q-)M~Es40$+xjXKU+fB9AU zn5TY9v`t6YX?2e4q?zJZ1IfL2cbhg`~j$<sMNhqW_eRIAs~VORn{y$9m@%s%tuNM7)Eq^~}iV0Smioe_5@QU1fO^ zUNsXS!*E40qyQTpQi@BJ^rtm*6Qmle56t$UY=7b1$1TEj%2>mr)K#IL9c?ObY+=dw za)^NVqBsiI2aVtr1e~5g5-g*Bxk@koT`Uw_hIVvfx6H>-T%kWqWA4P7d!5&HZ*ipY z=q*cJf=OuDR$~^A^t7GG7zp-3Ui-_%fPr` zrI)ff_tbpkaQ!8+Nu{~vHrJ{Yh2adB<=Un;u@yI#!y*D~u1 zTjspOg1t3Vo=eC2x5&(fbu0&6!J$ij#17tH9<6~_PzY+|RZl}2e-8{yG$3q_Kl$tJ z2-cL+k#|vY2es6#Q%6+6+mz5O%0qPtyZF4nmm*S3Q$c}4|F&vNT~hFf?Nj!sO<2n} zf7HbOO#HzR6Rp3gXH9#baN)v-b3g|vs~4BlGLo28?3bNzR3#>Z!yKRP6voRE7PQeWoG{@JVyg`K=0 zRtGCPUHg$DgEz6oj0_z8S9f{(A!aK^N|!6{f#EDw0b&c(f6?bk>6nYnn4k)5<_GLB-5*7DZ#&^N-LHLedZF_0J%+c+r&*l!$g&6;Q>dC%p zZRnJY;NTE-f80RM|RyLUZO9CVl^#1&3EW-`eEQ9$+ z>%DNR*PfK4C35Zv$(xd!`OH7HD|OtPNOYek7z1^Sf67iVQMkkqT%f72^80?;WW@JJ zs7~lCP*#L!3de`fLEN#vlL*)=b@IV)v9}TPc-5Jzd(xp}bJXxVl%Yw$@7gQt3i*HL z*V^}`oCauDbbamE6niU2&d{)$d(1m^PA-tws|3eN7a0q~-@7d{6tuIch3hkZ*%!qv z%%yP2e+{fAtZD5d$6l73EkFiY<{@ z!Oz!(h*e|x)VhWwrrU}$`;bB)nq4IhVrPzPHm z8$boZHQs!PSv_LBdqw2%J2Sj#`-fNwOQr+1Rlok*+=72U)FyQ? z=0R>k9v_-BSJ@K*r<$a#VMq*1fD86CYXQ@X)v$V2g&(qBP99|mOiCW@7}CYD1nUto zoQO2}@!}jkQ#HAhcA%%<$|KvB&v0wMe?NHijq^7_Av!V2ueUhuo`xZ(bEfH^lfLNR zT3gUCzUjh;XU$!BSMXWk@hmTG+1 z2lzgl$80|PDYy)m@w{~YDo5zjp0hNEfD;vkH%PwnMh7MGbcXERH!zR1U1`O&e-(h( zp~%Pi8T0^h=fFgVYZwX(i?Fw<_f?`fJD677v<)kWDNnFLFMO5ur;)bs3B?+XG4=VW zcrCy;eR8$NZ1=M(k4dBBnKq*&Gbs z7n;J0S*~b~7vG^=cOkf8pRxW$V|% z$FR8K)0-JIfw3Zi-2KfTm{O}hCBtBMG}PBV@Emx!@=_{@5$$8K!sC>mZgCV%=Yn|r zF4?#cL@TS$BG%JXg_6rWlO2)Z`Z+-pX2$q+zmM>PD(}4}E(D0coWA{W9#(f2-xBl9 znZOgon2KMO&87GKnOb+mf8cQ`9RtohGQltH^6`#NP?W_3xBwRCr<@A~1=a2KGAhXutgH(@CzMQAMvXdUCJLs&a$6HRsl{f7sN-zN~M7{PY6> z1BEqbhYIZDmF4K#x1^wXtl%O}11VL9EsU#9!5dMMy^N0dQ8!4Km_kbyl8_53N^mmw zaOA+|;o&Bcb;xAf+vxsHllWXSOfZt~Q>LXDOsb0lj*W2RzQ0Z1R~<8}siCY7a0=7% zbL}F`ab#2&gfO((e^^@5A$cTMiu&Z!Ta3Cyqb`9!&T)T%?X8$J=)d@c3ZFy~l z40{_ADtUD?vRWy(7+u;5QvusEm5VC4s}$@0%a0az7Y%Q#YXXFf z3HmCInFE@BvXEd-7KlV|CUr~>Cmu(^+en@Fyhc7Jd#uN}f7zrG(e$_hCYza~1oPJy zH`yHnX0pTa^oc3V4F}z9L%6M6oDZ7T(ixx9v-6?TP11Z!Qlg%xJ}aAn2>F%GbK=$- zA7x)S((Cw4p+j3#BNt^wkddoL6SN5~`oz_zOSSjbE1%PL%FADQ@iPK50Q;Ytc~_>pRuj7fZN;Gf9TU9EuR!){J+0iI%6z2{9Mra z>kxsF47t2%xHp@M+OZ26!ExFnvipwU;m|Li1`pP`IB_*AA>ZojoVY2-6AoL|<!0ftEM@FTg0~EYmie|n z62DFxe@sXbrhnwuKwbHXS&T4HEhM}u#T{c&Dz2>D(2BY*MAAIJ$NKlFF^kVXivkIc z=3ORcEjDp)t9O!@UL)6&=Qb`>PUszCDqKAKp*geP0$iXv4c*Y^Fl{nGM;VVYMZeW_ zirH*HV<=rrHYSAAXju!HpkOHOz<( z0Y|S&?VmbncDQGo4Go*A#F$@(A z&RBq>zZ;JlLU)Gi;?^NdiMtelrUlCNu_K}A>!qmyT}iTsc^N>;;n%} znW(_d2icC=mSZ{lt0xQ#UvBZ zyv`LZisUZ5x4#L8HrRL+0$b7cf40o3D7Qq>3|nPyccjxR9%cGjl4hT`l?a^rjzW>= zTrh~6)Z+>MxJ1zl?uXFk^G)@t9g42hca*%Th4yCFlE~m@ur-j0oaZ;H9%d1P)Gs(T z>BWjp*x@ESU-6PdAMI&Pf1asu5%DnkQ;K=Bo2qJzD*=&KI zt+&$Mk+tmna_G_@ubsl_ftt4G@5$sc+zh%^ddRDw<=Oh)2tWut14j1jCQ1piir$<7 z3bV7Vd}J{li~OM=Am$vYe|_Oh4Y>zF!=2aiWtShC%R;T7mo1LFp_}AuK)-10RIj|a zgFt?4FWC2%u}M%<(3O3C2qLzqY&1VPB6!{WDiOo|tj(>VyE%bn)f^L}>>6-KdDNhq;sf6Vz#4U$cIV=}2B z$CW9OShR!V=@hXnu|U}IcSUXMZePTCroFhGEE2N>6Uiw*nkl73P;}^g@@F_{4{O2L zqaplZSa*NJiGdPC|7q#IN6f@zb^Z{a2kU7)``r>k&|YcMUa zOGMfpqtdi=zSp%+f8F#%VBB6iH`z1kIy(2x<#XEjF%IfiPDg}}JazaKZ%&?p#aR2u zzgIzL+bZP~{yIG*O2-O$pFnswATOb2*bZPlnYuO!PpNO5^kS5GOG&L%y{1iPYrK`% zIw%-fYkhX7`kE9ZO)}DxwQtPVXkeN8L0WR-E;6nS(=$qW2WFZ z-85K=BxpU4eL2BiB6TRV(G7CsgMxz$WaatHDy5-2=2xp;5tGsAQbO}&}*gkE^>+VT`Vi=I-Z>*ZD`p^?Wh)4+VzZr5L* zH2DEM49ct!M$CoTp9RPri1ChHx0weUN0+9B{FBm+f6r}x0(>wm*V~AvwnnJPxN04n zsz}D8!Gt>f592@db=zomv3z-i5x2K*AfMfxETiLe2#}Zbkx-q2?B~o*!ZcoFlfl#1 zNv9nTcOO(m&lVLMrSX0dOW4uNo<#si{X+rg3>VFBKc6j|ACq>=pGm@o($&XsM{K>0 zzl|57e^55p7TEG@ZR&_nWS~0zntf|3$7*Z~|M6R)Yt^zH&Ohqnx-ojqL%;XKd>0STd2LQ#E9W=xQMwJ$>l z`wJbb++_(}0hDusG3}UJtUNd_qIoki@_BuFe>YXhSyL1tgNhSDR_i=H4(gFwWzK6t z4@`U&+cRQL;+4EQJV%S#8oq1ySGAJ?0TdOV*Qc@guqi2Jx`Mk~jV`or6Ce=iG2bp_{c+fWbgsjY`+!@bkNuMqzM`Ou<}Fq` zM)vsPM%i#^0+ttiE6XGJn(do*wHoe=aT( za^7emNrYouzY$8J-`r|A`F-qqU98;ImO2`i0vyGSwSoD$)xpFRy^sz2T zZ`Gm7%rxxKA~C740;bIew5NHF)1wUv?)6-{jL)%u#j#xkTek@k`4gjARM(zkma+^07%?{O*5whx zBHPo5D)42CXv!vdXrPfjn1ipWvjYzq7FNrHxsVfR_Hxw8#D1Ya&^d_X$q=Wvi@W)9 z@5(dAkUKw_T@ZI)nB{VORb7`QoDnw*FB;?XE2mOocE^z_cHAc{A0t80e_ouyEXoR? zD!pZB7KrS}j^B~0i^IJ-smDCeayr!OAuVl#dm6B7Yl(JVJu<6Ci;voYQPg0JN}z|~FDTe6Qt{-SwV z!U`zk$g9@P>O7+p7Bq+Q{%jC3v+mzD}2zVbml)EufPdZXs0fb(&1t%C>Qyo=vPQ>N9R61TYj_(v^ zRH$>1&rtX)(F+Ws{`j-tP>r37U5va&klvVUIA;8uf8AX9JcALh!^==;H-<)$56q(l zHqxiNZ&e!L%pc-DLnMWof>=PnZrzH5TY?s5k_}oua+y&SHylb>(-&9PTx1>DB1k^T%lGt zkh6+8Sd<@CYY%-}Mv^A4^8tEB-aC!>M;_jC%&D<-*a$$3hI3Ixxca%cIE+3wuH==* zv0G&KRfuGDm8d|;{t;->Q{G8-jz3N_!M@eOtui-V-%%a0(^MKkKZwQ`n_yeOjr}@Q zf4RU9W7BG+B6RpzwxQ47b~e~+%$ZJav9?nr6ci-Yar{FUsA0|DyA#=&G)^?)$O3mW z*}>3YeS2%Ms`;EUXL3U!L`^|qXmTqDSAw0$odbE1wUbUQOLD@){6s|uboFV0qe~VBi zaARgQk%Hg-=Yg5}!GU*cA56teLEo5~DF^)+7R#7Uu#~17oHxuw4UJJk*SVX`a8*e} zQL)1>Jhp-J_;hY~PS4o+fjy>)knKlKB^U=NA)D^f47+>XZeb zbc#A5eEc}n4J%Rs_r!$*XuPWHiR$Mz;rcKm} zTtE;`^IO(yZ|_ui@|#e)E5^Q7JMhE5D_^Mc#!ttEeyFF3Wx;YIquASB0Y?yvTJbg2 zJvVW-SI)o^iWwS*?oRK}@h1)<=8iH#7NA@eRS3~G>|F+9g}A7O{aQd0e~mPqD4ZP* z6XWOGZ|Tm%s&h)q*UD$>kAbInsFb5?3Ch58iFOV@v=`fi0!ITvOclIX{;W+gH7y3 zcmXbVV_@q+l3AMM{2>ek)9}O}1T;F*K|CaKsMeNwQ}b-2g2msMWFcrC4y z@*s0Ew5hz2+Y28Wk%pYY;%vL-%ZHbz_ICehPkMcLf!(wGLnqV}NRou@kZM*{FkPGv zw!$X#S=?(cf1twtyaI&BG{Y!^&?rNz&0d7D6KVHp)VS-mJ4Xt^;5+IX(U2!&lR@0c zQ;?Bj@1uQ0R>P9!El_H+Dget`v9K!`s|O}iMo9wMkD z#_5s=vjCgisWF{*d3lh4rP@U)?J)9ujrbFk-)Zcze>0-emPj%&WI>`PX^&BARVlAX z+R-5tU>+RVffXGVuINs3ku}CNwM=tR1@3LIU%MYnUm^%;q1L5fOY~MOXMx{*r^;yM>x$2`I>C z)bD}&f3-V0PWdL#oD_!-fb@ zrGIhQ8|g=Bic%~jXY;W5ZG-rpNw3R8&>Hixf46;ZafT6_rE*&sBs1oy7`3lY`=rkq z(^@Z3S%bH85iYE-GX(lxGjVO}OXX6Vz$rFV}((30bYWDFRz6sB|A!#!Sd+M*6oCo($T0u5EJy%5U zcRBZihShc|ME&i3pJyDWo8hiJYYra-coGrpRy&Y^z@^87XdM95ZVZfV176%9%t!t; z=a?$YMNp`6%j2JJp21d0@?p2MX7k}=e_k~?=&GV^^Z=|Z2|;|HN&QNjPlIvm;Svv? z2{}R(qkWU;3=@w?=qU0)txm2!rKURTo|Zs0SOm7L$`rz2MTLCpA07Jlf^9shDA z%@-0`hnz1&>7OMQrj|dJt}H7Xf^mgy3>YD=keZ0gC(C!48N|C6@O2d$-P>4Se6W{uf zx*;q}Cd(~=w!Yj}vbFdk&6Ru)Xt2CTk=HD6ZiAG2PG%{;?$y1sL`Yimp0yED9tb@jeSB2Y*z%BR#IQbzUOC7`~DfFr=ikeaB&=yy0H zZ;ujB_h9#ZpKefFdz{*|adHmJ9L3gKpPcn(iT;+-Yy?{`z@9RwB9HZGB4k@Nt27N# zFH_m+G{>qT4LcfruF=|LFn6Vr;Imn;PLJ?{J9YZ|7@gLXs;Pm zCg@v=KNhTHRWuPDat@~a$%FBlBlG-W!Cb)Nu+3%e7DE8jManv04SM06uBZ_G{{RPZ z{&AP#CI}OUxM>E5xM>HsxM>J*{sK2Mlkov5e_dO18@G~v*RPnz-8vP`;0{!!PL(fG zBHOYR%XTEE{6I^z#f>fwN#!Kx*KhaNm?37UQB0ZHeK}QD4~Sc%FKBc(hP1V+YAS0@ zr5a7orc&0^(^onqdWOnte#Xk1K+jZpZz}7W$_GVHRVl4$pwpEK$?jNZDyv`iax6&!|5gQb* zl|HG)(=3)|Q%dpVk(i^5CB%`aRW4F%f3#Ezi4a8^p__*5A~VHMU7``1;Eqi+LWhRy zXoP7rVIwXnqa#s7PqLO0%IjT#Z_+mn!QXrL4p6en>(P-|MxRumL6QB9B zrjjNlG(?|njQ2Z+B&8ehE^)~dHHH*VHzZNQ$)!j-KrQr_sE=XwAtBMqiBhe2K1EW{ zismC4s4p?b@Hi@Y-|Xmy>mtvfe|T(S{Uyn0o{-i|tJ0e3(p)kuJe`wm*uXpO# z)5Xp0{A{|w=0?@w^n5mXeDg>33s<=0b~OnvTD2R~haH+}PE!C0cmL-tZ%RQ{!B@3bTE*&5~G7MqYS3X&SE^xh5Nm@x2^)6X*wr|>VozaAq zb{fH;4Alg(Jc0TLvOf&T)=*n=O&)8hR#Pvv%XZmBYP|DdsGrHue?_+ySk4&}uUzWO zvR4i9Bf7-U8(M25YUube%%@0e3soR4yDCPhcg&~8^H{RI$uYel8tSJS>C&)hqGz&# z4nWAPiN2wsp;0uM50;r1A|d25A8z#E`I)zLlv5{ewtVpJnjY+P&dMYrgGTT2Y16Re zNupFkTa*rKqJ^Q!e=@hUL>#;rm0^s`8G$gV4pIY@9*jEBF3>G37Ae@shhRZD)_c}|mIrIG z)99&KGnmJO$FhDnKri#qj^UjU;DK-#%_0fOGck#m5fv6{e*+I{usq9p;I+dNcq67L zs7w}|fhvX`sdvDFW!AD%t;3f41}qY&vGle@#&b#PVPa?_H@Rfh5HFZVx>`gW1txO|l(iV)SD{7iAJ4y{u$-Mgr$$4$h@q)dpB3aTf@W1JdzH*` zg#x0jSl(R=e;fPLYpal1d2i|rGkchIjVJ+Xy@4%eqv9PC7NX58=G{!fE9hjQB-M#P z>M%CXZai!RGd9ofgq;+Ibm(2H7b`+_mO8nhID#zMIzEytAt(IrWT%XGUdykJJVvG+k_YLece;ZDZgyZaZm&*{qsy-uM|WD|2(jVUE1KXQ_;utLdQ7YEM) zE2s~;+xZ>wqGP0p?T83bA^;}?-tRqQ@J{BnSJBGN`xN(uaB-s5`d{Eox>zRSGoJ%f zYCPt%WT%jjK$oR?ygNT)fr%7?kXiS}JLu-X21f)op}L0k(Zf=8fSmc#lq_ z4Zl`#V;qEXE0tVzw!9wF1tirLJUADXegc&Y3 z!3dw+2wljD9f&(()m+7lvz7AYjon~{ad6V07fV>Tgj&w4YTTjVc&zS2uL#Z$Tp2b}9!N2<3*T;>mu1)Za5 zVdli|Wc7{8Rd2k-%Ns-^70A5Qr5;9RgvOQ#%y`4YGPG(I|1CF2J7YjLp?+ zj)+Yg-h6>v7Mjof2x_zaH={>k&*FS#Ft9N%T_N7Q?s=a<#(#&t^SM&WR zB>9@um3W$HDENH$f??YJeJ&qfkjmiMaRdewkRrf))X7h$$r0qdA9JI-U0kc+79+Wir^E=+QBG zs>Bs!D9>~72zWsjhgEh9Qv%y;G-5XABP3a9{` zyunOaW{p|n$4~vj>mk07=8A^k%@;mVdR5S#{mb&Of^HM1rr`0ea*zZ`Rzr}$mk*rz z$GUkPs+@Ysa@ZcY)Tv`DIlnfcTRt7zODQ<{ea=-(*%M0yT0uE0YVZd_9D$kq{@>d7 z-13+&cwTLmQ3TMN7sbt8XB=>RF--)X!ECNARVQSyv6TaS!kSAKFlpu+^aj*#~aC69Of^ybHHiPQRTkRssS4TpH-`~S>HM(lfrOjB}AvJcL?tD>HHK8%_Bb6sHwMhgy#WOwB1!}E=FvV?ZmDb zk**djsYMq?kQ^fQili|*2OMDOlUlG&h26?VTIfSvv5PJHMh>@Y_}5{B#6|Rxf zw;JITbW#1?E5#{Q_WiG=jj3s`&Esew8->xwjAx3^D2DZR1o=M_3>X`oMyu$448-Ha z|M-jfi(qis`dizt>hjjdhaRdfm&S?Y!T)%wb~wl4vQ8MWGoM*BdBIQt{z8ceq+ny% zAZI{ABnzFZXe}RgYYk5NG6P0&fQ zub0_0>sEN0;#Z)5ZDuX~-L+{NQ6Q^PIw=b_nuD%DhZ*;Rz{hksh@0nfp1n}>SM{iPmG9Qv)f{t&~a8AoL$b4hQz2Xo3Q16S1#hEPRK zra?!UfFe&nbb|d0A?Fc(uzm-pl@RvX$sclDt%TkL>22VZi5il3EoG~_axrr+zCP>@s0n<(S_z z^B=s{c4|sC=Ge!ShMvFmz&?V-r#8gV@>Kywnk3p~%CO+?Q?LM2g3<)B{RnAe_Mdgp zSRYj*XpgczGl`rPT&{i?MUD&v36vTJDjVtX46mASVNMU|Qdoqw&(anT+ex%sQVYzz z48ZGuP1~vTi^|{}WPN>L!ZpN?1?Ry)vuR~VSt}K+n)3V{qr}l!=!4qrbN>UK@{|w| z4ns4HtM4HO6UM2GPRT?W7Yhc_lb=UB!J|W!wpO~C;it^l`dp;hg8RuE-)sk65E!f! z6sRU0e&}9B8J9XC`0p||$Hs%Irf{iN5(R@|g7#j#)tnJt{!`bS(h*m0HkIJA999VsZf3)SgU65hpHRI^8Q%gGE)}><^w=a+J5VW*IvV zjyKgGfsyO*)ujmA;#HSZsD{Dr38~|XAI$zDTQ$dY&7F-K$7fG2inlpHNh(LV^v_bR^V99F94t*1$kDRI*wsx%GB?=&ETSsf-QW6Ws|n<&F%9lE>nId|&Xupn zj%Q*DuW}2b7s*_kWR4J5PV0_6gCoi(H#g5GfhzXVMi0@419uk# zpt0FxDr$Fne}C(A>yO%Cky#@#*R#Sg(bMcO#k36#&s_(ef?aaLg`i#YL9|% z?u<;A!M=sqmbvA70O!34VYG~b?8JWapSyECR~I?-{VOqIse5pZSSlf*wc3B{E=|yCyL;`T<0u84WIVSs z9|TipHw$_ZcpVCbCaxdp7@AYmOTbuzQ(LEdAMVRfI$@Bfi%*h~+yhyF9H`MHN!-!76tq=EdY_7^kVImqZQFDrR@jT>9%1_JjuUR0i6eoRBw7 z=7eoVg6^r>?bF`U!BjcaIhJ0X%%X(^lCey+%5@d0Vn2`$OJbrF20yl8qnD~`!8zBn z=Yo9(P1hb1t{>+;wcE+ zBf3g~iZe++1yeg4b5M~#k=>7$e8>k?Mc^yT>cBP!c}p=T^4^8Jg>mmn{Gz1M@=+Fu zU{ku<-ZC8HQRC6zu?czQ<~KPTI^5hn*>ZLCO@`t()nw?)o0Zksuadl6y+*T_eZbrM zT#FK^@KP)VeG&tV&U>M1%;=j3d=5MFP6C=Xk-sAJ9F)r*_v9{Ic&#Ol^SQL+aCbcl)gzeL1)Oe!0&47v`&s0Q>C2GZi_+sUF6drOfuHfomf2ozj!=(ub z+wZfadiQf_2Qq)Rd((krjc?!4-K5c`!#*x|(D$2#9lw&|o%@AEAyi+#yvws{lA&gL zLwJ*feqyirG6$%w-9PgykUBfbB*BCob$Bm2Y3?{IE!Z*M)Yha8U?oki0_)AQrklB8 zVn?}uZRmABP?KYyEQaZRYEO>Aj}2n-R?DqI__#X7mQ20RW?k*K6Pr6@KYNjRP3+-K z%yeP%kmJd3kTq;+Reggv(6KUuB~~w3cpSE?G>p1LH(>bOtC0+nu^=DnKAkhqQc#(} zm^gv!PXrUB;@t^fLh_MnKuAZRApK1FNM$}JKLsz^6$MJ6T-fiCtvudl-!cccL#j5v z%QG$axTWSsre%NY=?;lCJuM|ng$ol@OzImrAwvO!$=CNp*Plcz(WF?<1VrCjl$W8s~WZwP-P!pD|aLrd1Jz7+YC#lVA_z z&%b=o#~|jya4^-E*h4I?Rd@MKb`-L*{dinpb60(12KTN7%m}u73a^jP_I;q0?Xe6? zHo#$*m`|#izbL=dzMZA;KDe|3vsUPG)d){&-wV&1t>P>U)Wn#!~7{VevSaYv1aq^JH#n7)`I@{?eHu_=GV>b z>mvK#)(?la4d3}x>U?$ZdlK&dlg@o_JdxqDuoP*Rzu-l|`jo(fysUrOapS9VYe*@Z z%>%hvLm}VdOu@El#e)9CZFW0E!ONuap%|U(sp^IA_tbhYvn~s_|E#d5u)CVD|3Cqh z87C}9;^~i0O4O`eWKs%hK}aX>6zQNMm_4g51WXWs|$HKwf)y*Y!hY{;VDl7my z;+-Hj7Z(q&AS)L)6Bic~3l67>qq+1aHw#*3X<;5NZb5Etp8pf6Hw?r+$Iz6PcrU;$ z$SceLUYdtnKtftVKths7hF4IE_q{Z)kc5C3?T7zY!~};^*}}of&6<|`J(s}Kix4xw zkYZq$EJNJ4J=9X)V&4H`Hep%3%AU~Nkz`R{Nhzu+8Vli|eJ+7TY60a!19LfhcaX-& z65(|hpFpBzPZ?URX;09#2~+d13643qImTD+@j2Ua&T?;BM+97v+uvMAL{CScOdJoX z$9*SW>ySb+S|WRtQvdh3Y?31W zDQbU6KfFpwI<%7eZM2TIz zj5WHoP~l|&>)5+7JF+?<)^Xdh99njC3u`>$$HIHeTBVr>BVR36^< zN~u=RRKC4*b!iDEo^|HfoXIj)##r5VM4dnosK(wpE7}p=-ukn(yZHg+^}HZC?4L-x zZH>))kwew75dI)pnQOj0ir?rhYsUPW>$3qlTtf4hjO~JH77)=LBBpJ77xB4g7#*?| z*mf9F5ZpN&O$ezSrbxSL1uhWnzX&0Y4sfo(RQ7Ly(4?VhLCA;vA0X5(f-fGd_p13u zD{n>H!GB`J``-lt`ui^Z!z<0h{hfeUro>ca8}QFnW|@LlhN=4 zBdVB@PwH*gj?g5Jr#t5yiXD35)4XVPK^k1>mhF_ImQfVHYU)?sm;h{L_bEk5^&Fp; zupl0GuAk27pItcni(!&vH zLM*jY)1XFzU}n@%1Y7m^g6%R4K8t4u5UPZvE;Ya%6%u=eI*CL?wd#CxTfZrg-ei(#IpZ*Z({lj3A6RmNLdVW-I;GH|~91efvTS< zV&aH9$Cjd=c3|EMJ1Ea6z9T`c~#hlt|X^4fK($ikJ!zDqf-riul(g=p^hIN!m$x#kKtz zd9`A|0NdK-O9MVuwhzVtO5|e=>pX%nXP$8=_;%ZSVjrIb>7aGDPbrT z8T_uQATsZuky>a1jC|)y$hpgwSxoTzhZ;4bc$+NFZpZ}BSO;CmpC&`2ycnQYCz*E* zl7jFC&;D1~`q+vRWXzcEi@(rx^2q1DmVl-LydblsvSVl&61djr_IV~e9NJ;P4OS=i bm3YP{r`%MfSZo>`0X{Aq1_l{5S)Bg?txkdx delta 23281 zcmV(!K;^&fohJ02Ca_!q5t`E>1jOlVBxRR6`vcClYq^sVMiaAu0U$I2GBK0!0V#i) zdyEy;9mnso4_j)Q(FS7)-OTEWk63nu7A+=W{<)xceCEw=4XLoab(Zm&HGJ+x&qxzt>+_%P82@OMT2Z3@4Md`hbnUIPD1%pWfDpRe#f#`EZlkG_?gNQ;n9Ece(-I=AMhAizf<8Rkw4?N zGwy=Niu}QMfGeE8o%8#QdyEI*aUw79oeA~fv&hCi1~%q$E5EjDsE@skh9BXN6n?i} zqfhX2XmhSAWIdwRf4n}M^$K^X^(M#mwP9)ZP=AiXH`aand=Gzgq1Xfbza=gIvG2{A z_XUgKf1`gWtilt~k0SnhZ(TBghM*h^pdMg#)U7!10lDAl$?>_9uyHDYl8#3}g*z<+)&-MZR)`jr* zs78OEoXKi@NBsW3+}*kHEcp{p8{(f)-6w`;%@5mG>%SB8W9nqvIqUuCb9)Q(@o#&Q zz5xF>jpsf1(-iY#OrOIY@B|2+Bc{*3J3gC8S^hk5efo7jJm z{C2(6``{%~?}1lH{Q`bM>Lu)BlJEn3HTw^U7c<3PvEMb!FJtdp;`vLj4Fd0eh5w2D zIjrY{{l^sUdmZcJuYMKBhuc3|{;Ewpc6fiteqWG!5xhY1`KJ|LCG{ow_dcGt7+-%Q z_3&zi7qR~W`O3#&oB4l~{sH(kP5t0fZ#OUo{anp`S>C1$;Ce$OIgnc*ke8N z^4Ncy)X(_WDH{J;K);vv%I16y{T+Xg{e<|JKg9d_Mg6wT|LgkY>1w@A3H3AN{1eVo zye-o&4dZzD{-mA#&Kieb3sc6MJo)Q*4L>64#~s95pL(NRSC8QTn;WXbkAV2oL4M$3 z4=?ECNxgnqN`F)!-`-gx`J;c2+E1ZM{?(WM9rDW~|K82HF9ZeD6GxAwd)|K~zgQst z3;UWV{+j;r5AY`e`gQ7fM*An9S;6}&=u3;n9&P#!otpPo$PdOQ%wHn%x3?r8px<;- zqpt<}O&{}qhx)W7j+YOP`re-->~~O&B&^+y{WWq+Tv4T!*}hjORrk;ctcamFU0EdSAKH(4b`707n8Gl{g2i`B|!GDbtd7}@#&RSM*Ve{c=0^?=n$_rihXjw zJ}05SsL(HaHDSE*s4x0T{)~UPQRIz$>NWX;M?dmn^gDk*-+wFlIr+qV`JR>j+I;ax z^ydbPyyr9ezK`d97Wwkll=m?%^1G)c8-DxTKSc@sMV{{=I$EkD|2+9v-zxd9 zkoYvDO6&XhmoXaq`2>lZhv` zZQHi3nb@|z-#O==bL&=p_59PldUfs9Yxk~)f<(gJ&PC0`0m#C@!pO`6P?b=TXJKb& z1~4y1({j`_*`9GgnDsC@O!b0mMa_)Ir+Wo!$w@%aDc z{U3(3i}61`2-{iw;~evUAds^J$Q@{=1akSuYI9?oe=Pbpt_l3ly~qR2KtFB&(+~W| zkAH5|%-+t%<+>pf&IFk7@1E~S-!^}d8pi?=4<{z0NW%4( z@t%vw$}N1Ww_cU=Uh2XPF28Bu+L|hSyNbARNn2kFRHB_^&&WQlmT@fMN0VfUGAeEF zgF@YoTV1%flcdq7LQmKEL z1`L|gU~OMJ<5zzsd|{vB5c6bN1iZ5FYLW~%gxtH=`(ohYYF06~)&_PSvDE}al=J$W zgZ#bPOEGD0rm+aq9*WZE!ct!(1Fov1x<`lUp@yv3Y#l4K6m73Dhk#_Lq0q0}ztJe9 zO(esRQ{jOXY`w!vwJxFZC|VPHY*%>zyt^N78*c=obu@oc8vRPQq&=&q??G;lm(gG-7$$ra810) z-VHmN1{dN)OCDwn~uYM@XRl=?z*AtXhWGZoLC?y>Ed02Xwjqv&T?f%R}%$L zB-cvmp^<-P2vH9pMoSK>hp4-c>1zo6X$A@`*baAMs|agt(RKd}UsxquWqddphaJn+ z{`Bh}B>Lcdf*btXx;s1Z=FC{3#s4ijvE<2W2^nUgo%=3UI1N2$R*9EWY8NB3F!ht~ ziVN#)Wb0m$Qs~_|X~s~p%a11Nr+mqL+ZXMbqtbs;*B2vC-tXUjLSRr0$cq!|9esS{ z5laW4ls}`ts*nHN+LxcO>Qj7ijUX!Vk7X!D@rI7q)%M=U~-8KKWT4jHR7^9>Yc-L8~uW;ekE(F?NFIah%xpb-@ zLxs}-e^;)wT!-mG%I7JI(yPZmF<>=EHD9x6m87qTqCKjuv7X^@X*JE_zU8E$1zAM>DMfUz9WAf zyr~$S#u4q9^i;8EeHCya++bepPIZ-ve9dtmY^L9j*!4WkC+p%+ft{zGpJUYWDQU6H za@kEbbl%;g?~%rSnGwgiYoN@|IdL%`@_N->rr3!u zqT!i1VHq;zYVUClvQ;}LO~PoCGU$IBxxE`VyPl@p6Bp4=|FtIbtJ5)n+%H~1(5s*g-syMaF!d0XqSg}Doe5y2e*%D zeC6?V7y_ow2@?I{h9S%2X7>CvODz$zSUFSLEa?{&XYA=Sd+oAAn!XrNe@K5+5CbRg z`do9zNoNf?cycO}06IzO?_5bGZj1}kWZEM=IziC^ zC7ZGmQruWH@vm;}VTC>BzmU-54QR*u8Fu7_M5WtH$voURcSO1pi5Txajh~n-jM5sB6?(Q#c!2rDS!cY+SQ=`|69mRZh>d^fHjpxZ(#ANV zHWJp*^Gp05(x{&vh1rEWM4foFXnnxA|7h%c0PhyRcd@pf`FkD=tlAIBdH&grfT(KG z7d7E>7rx_&;xsn?w+b7qT1ebdH*P*D4Tuj(7gyWtMECcB6ail&%gDr4cziuYd0chB zd}H!XH6rW9S_JgMF<*ZIJDI5UBe4l9U%{@T{6tV$?YGNMr+6U<1|V8;$F`C?v4Eni zl+2d^Ov1gpf!dXpkg$-){f(nM>l`%PD*rv#=R6GyS}ha$hzmY zZo}i6QD3HCy|8$kCsEnYT@ss_8WwFg8g{I73|oZu+Kl$f3o7$CE#P9OWv>QThwS}O z)SoueODr+BrksZ(0*pm&sShbk415Th|HGxq4PRB8@OrB>=UZO6{MW)C-F&d>PLna$ z3M}t!XhVM(ea+Q}?-vgWNI^TMvRJ=qJ_+j-$k6EAz3={rKkp9`&seI4O#GJiR<*DC zYb8gU@*9>^=F&VS)8c0`*E&rHg&N%3#I7t}Qv5(DnCeKz0q{qRGEFZJJ_k77oTJj( z*1Jm)@!+9}HDK1fPJnhuO0o82$M#(PzBuSYvM7Ji8s@IOM!(hR%wrzOt45O?>G{zM zy-wfnPDbh(s{@My`QWAYU2b4kY4T_F9hGZCev;?|WdqzItz;2c4<&mE0qLxOimqGh zyDO7ei%_u#z>B{xUHPs2>aKAj=BxY|81+}t=M>tTc3+=9)pXvlcz|KiIfv8p+LNp< zmFIt5*}mbLy1f2%8$nuJL@-B!qNkp*J4_Ebnl}^VyrK+sYjRU#u7S8AieY9ndWOvh z6gbLc!t#)7yT4eRSMl8PGhUS4q%)5#6jr$7B`I0BcWNTAZ6m-R+dJK_Vq`ajejM>@ z(wZ%QiYWCrjCMA!zL`)*gA?j#`Svi5)&GB`Q`4`cE*x}+-ckTHnvaKkBBSN*n~<$3 zj*tR;Lgh3;b}j`&XrGW8AmbwdjT|Rjqp+k4O&4;TFiN^O6H3|W`S59lzg^{ zUBmYwETBksG>o1u6{9 z=*{cB)nHL5jlD0F@_SqB9Rvkj0Rx6hmEla#U!8hRzRc1F;(x;o8}Mej{dzxRLTv1o zyQ&h&)`CP~!Oq8(2pQhAshF_OA6kh4GFsr) zT3((2g_)ELTDo%v=^q#(4A>{qJoF}L-!)aGW1l8&fvaSzu8Vn98dLew~;#e}9UpjO44ZerNjD)!oG zcAl)h=XQ%)nPv5XNK~AYG3X|sX&*X+(ksF{u@NQt?W?<;qpGCgoJP4PfuFPpG-Teo}rU=u0tu zr8LyEuDq1b&=1?QinR=EuqRV$($0y&V6xm8z!nWI!jYK$+>mB5*AGVEU6U}g*MgPt zR_%+`w;+L7Uud&rY1tX0ETwnO1|7Jqb$p?@q!Ne6*?WVghev<*S=d!dYaDGW%6{Wj zF#*yHmKB2Yz9T?Ma;lIPgP0qkR9U@Xw+CeU^6x%w5wDX*>mMbr@^x)#lYyi2i{6)m z1jHAGzi_?K30}b<=?Nqt((0Bfb>rSeLm;JTN5*$cy$rrIp3)*5}U6ZP9%Vtrvt zpR=F013~9Fx35`8q}Q)u+v^AnUh*Ne^K81c1YAKQs*-xz)t4=9)cf zeE&>{WQdN^+t3Bk-p5}!^WyB&LCNUG{%#&l$SCy9j6bXtmBwL?OLYw8VTtx-zM*CF z{8OeoPegxTzf}Ypp6sZWa9a`c6DAMtvw34>syH_Px@y$Nq)1v!`q5laCNaz^vm3J} z)tv_reu6}zg&tI#>kQ)}gTguLJJ{6ec~KIL9&nmc0DJLGnV-;;KC^o^Ek$J~&x_H< z&P>&Mq)6jQXf`E-#MtaAOFh79!A$CO!QD5Qp~`8iHc0cb(ZEMFgAeD-lJtF1(-g(9r4=O0Xh@opHDv7Rjv-6 zkP(0EAE1rt%Nm~>!8B_LP?hj>T_Tes@RfPd=ACZ$My@tvCrxylyLJDe#c-t;aNhw6 zM>p77@#F`ZVrG(1NsdGJ-p(h=t5~dk^(82+E3~k|?p+cf8)Nk4K4TlKt7PcUJ%av* zS-y5B9WIh{g-hHN-OQz*)-2a@Z6MQq9%Fy@*DfeIM*qSk{>BNO3@5ket3^h9e~9LY z!2)ebh%SG0@Eph$<2`}+eYsXH=q=_pd=9TFUFEM-$mlFJ!VYD~Z=jFX@|t|^>D+4D zo}^fK@eYw0lKl|0g}HaXV79h$Tdat%I}0+@PR~LW@LKx{{CZ7|{*Z95Q$pPWDVS z(P6|?H;K>C)nI&;?BR1j`7LYX$%WT-&z_167~i+w8nwAM^%wA=Z9& zd=4+V6KClY0f(xDjX`iUi@)>tDb_ru7t0~FjB;NT-K-qSBG{xH+EL_-BXQP4Vt8RG z@}q@WdZsFJN38&N-{nWPEw6u}mOekos2eA10YN%Z%CEOrt?v3k$8)Bs;t6jI>y~D8 zOluv4u#DLY&vL$u&I5<>{4q(|neZt8Z(&b({EYe87xG(>=f0kw3VNct9VO}?cK+Va zX3-nZzVgmPrQ9zan`MZdTC)~r-{3_=5cCtTJTbtD+?}9$_VmpnY?gmpaBcX%?NH?6 z6bC+l-PtqI;TnX%!6E)#(fumYm>EbZY}|$uz>*_arx&_PIc=cLe?kSJGbTSj6|VYw zr%tR?o9=#g2EWMna#m=|(-JY#4N^Kl6<)$Nh;vVd47OJNdMA%@+#_H}S3zP@?X>t! zl)Q3_?}93FhlUXY0v&(pUXvQn=awDL`~sjf7j@39y!!M(qgyTf+$0v6#du~qlPe!d zTh;Otf3pWGa0V;;ly7SEBpXeAD9GRjTmTDmlTHM@Mx*(jmGvFtcQ+h{ zvvnwn&D42yTh+WyhtR4HFi{SBSR&9;30q z9o%I;(z(Cgz+I;w?v;IgI?DDjD(mJ)P5f=OtXQXR$+~~FC^Rv)EA5>pKlwn!L}ks| zp@R5$WjVa|F3M{f&AW(IM^4se3+1ep_e7FlFQp@X)Cm+KrqGmuBIJbrB`}eFFuZT| z@NkpBI%vG@X?XvpL42+eDiFc@DcxKMA=ya*&qla@-`A?=t%jA+SYO%;IDu_0UcCr) z7#-IXC2JlG2dq(t3My_Qz};d09x=fo}5UP|8Z zq}Orjf(JHehR#X~V8d6B#^~dm^a(3Zm#XhAS6(M=l$V=1ans{bJkwCyAz`6v+~i7U zuT6jWE*~Apu6;W-Ef#;q*o2FpYz)I|BUP1{tO!~cKXQ}5LzEt?Q!{C}TXDq{>J!ffFA>mY%l zG`XBfm?xXE>X9=U!BNU1itCQR!QiG>y&LOnteC2$pm)`ER_r9y@edo7rIACw(ZfAW z{^mEmFN466g}so}yqb^nNg%r;7iI|q8>sxUwH`y?Ru8RavpF0;?=6j?d9L+TeDi;# z-k20|Dl)ek`pQ?-e3*f1KK@lP_6VC&VR`w6R>XBag68=>#;;eES#0iE1W0%|=R7`R zzJYsNwUfB`8nKo*yMCd3Om81u?(E(N!;$&s?+o2x@DpPe%PI|ggz+$4#Jaje)M_0D z8@UVW#lQfUx*P9&Om=emZwmD`4UK#<*iLQ*TQP?)jCnYE zyK!j2bZ5BEKih>UaTop3HNiPQcElCDJv7u|DhL>#6m38M7yTctGai~+z5;S`}EkuyicN7ZT=K_IT zq;5|LM@0%A@R5QW&o@;owx~LiKBzg9^KDJ6MG-+w5UXJ0SSE#2%H}Yp*Me9tJg77Zu^DODPkS= za6A%1u~S^F`h?!&_31nzfYGb5F%va!3zM(#Lu`uaJmi{r+WcW%FeLnLvY9+z8&Ac% zLy*keQpn<|$4>rKe|77#Pa?TA7lTfvF3JjcS*D&RBJdlYJ|lZ(Bc(W5c~4e9h3VN= zE{dqOdG25!5Nm&y)GmLzn%s?`{?23RveOscdA>%#!v@FI;HSi^f1gOqWRIMfJ%4UY z4}?$i=mfY4`0}3KHzKxQndrW)JceDIUDp|&cnS&ZLPKp$FZfwUI z7$gXf=a6ilboz&13V*VweB`g7q7Q=1ob>Sp0W=wE_uTpk#T$V-1x6?=i#|$Hm~D)2E__8M}sD^?H`cNYbJkSK%?05u1PXGHRE;jd2xcOa| z8gPH_Tudhln~_OcLl1HG#y`$v|4IUzGwNxq9Z`;wUju2VX{vfByfs46##y`~zk(IP5Vn*e1|4;jrd&~DcBI8^;bCJ{1qjdaT4 zVD~{qK6hyXSis3D}J_Udi=dx_Dm8wn5s64J8a`|WIcbD zk4o88lV`)HxuGpgk%s2DIrG+7hTYH_7WqfMbH$=XSlZ15u5N4~Okzt-fUiqLv2+s! z+ufvmdP)Xebb)Z5@7#_k9^eeh;wgn~V^38?JP+_fL`JL;S5RA(9u;6;=}puA{)K^E z=Ddg@56&^pm~zA=S{4)=-n0=B@w|UFwVSNyq#=TsM#X_Bqj{bh3;jr~JnJ#83n8}h z-93C({FS^aEK8FbgwVOWS>>ot08Pc~@o6MBWI{^W@bQEcdJ9H36^ZsR8{^`!=QOL% zG2EGs<4TTGcmo@gYGY&2S2K_bMf++LkRtgDXM)gbc2_EXJYgkt*3pvjRa1W|esPS~ zC|!`#YE38ux~rCo-Zt%QGkvNn`44S$Hn|5^!cn5HiSlOSG@&W}Y&uji8!A!uY- z4ig+xJa0HNYV1_vsbPWG%s%$$NtU68N>*)D;5j4a<(1jDo zo8#ZmO5B86G*0wb$xL~}F*{ISXYA)){j-^Ng{~b)R$edx>3?W@PL6-H8x|G_Ic_wO z#ltYK-v}izZf?~beLr?RE|%|VN*oMI01jeCTEN`wsvu&Dp3o=3o{{+k`WR>Ax2g~& zW}3DpI74vG8V;KE;aJ9dAV)U|&j6#MQh(6UXCz?TrkqO$rNy_lg7z>KzP1C@mf32#p! zDI=6Fpeq^Up@TXNm!7&`H?$w5I4fv)j(0zv=V<9}ao)s9L)Z8v@lK zfcvC$*W#l?i6>5{qU$=u+llc^l#><_?n)dfoPvSCy1;+8_O}@?v7D!F2$n{dDeg{u zc@uPdD9i`c0`C;C5a01L7{ew0E&GSIe(DLVWvJRo*)8>7AL$pQ6v#3HdPrPfO`C8T(#{8ve}X~-Wo*IYl}^Er!^+=Sp3IuY zh9!*tyeLJm=m+&&>QW-(hvA1>#EG*B{+waK38G~~gp1qL0LysScun|`!=H8uM zX5Ty`+5RDomqB^w_Ru>avV`x_fHh2inRSi5c^ZGdCm0>))WBkpayiX{uRUmr@E$1? zv~czZ!#veNK^0i!wx@y{NEZG=cGD4|I)mnIv_*|I^BByB)J*;H$@s{eCIeT>>uOa1 zkJsm2+jtGLH_;G5JyAhnt_4@{m9Xw=Kr$-6bQ^?W?t6n=(RaF!2hQa(^wMqpmvCkN z7^{C_C1hHNiyorJ($$KY!dq*cwdJO^BIu76uj?e*GA2THJ8g>)3mx($1pM_oxhe}t zPt92Op%udVwq7!A;6A#B)yV{MwtLC0_5F`zA43phx$6C!LD}pkV;u1P5}hu7uW2-a z`j|}qAN+f%B8%F;YgTY#kl5*32Kls^ijs7eF zSN!mGYYzQ4Qb^p$jU%R0x%Yikb6JKJ{Z!ny$@~GF5NZtmdOC*Rwp;9VBsAiQK{pVx z1xu#;jz?kR*tBc?u2@)>@wJG&W)3dC2Zk@0D7*poH~Sh18^?d1)i0V` z>Du`I8O3UQUp@9=kJ|1r?D#q)A@h=*~cL`(!I2ZM@*82=t0vZ4ZRKUXiw4MqE4m~ zResFzmZGjkooV~zF{~p0q(x(~rx!C{JC!8Dg~z@>g(RMSH2+TJ=7?)9K)nNs@{H89 zGWYT#5B&(lbW-I{774gJ!-xUh zjG%@i!5U&^waNE@4GCw?9MXTKR_N;Bnv_)aTytIbBLWo{1#FyivHj1dE;*naAztn| zk5?w1ukwSh%^IVM9O|HSf;$8Fppu(~gl4ZxiXf`avUGVOoD^Gp0h6y10OC`}gbtUV;^6aFRVm5zD=dCmCnds$!Y0hAR&y zNudzi2l&LyGVH)tEp-y}r5zS}50f94*IJ-lvcrlzcO#g+{a>m4hN?4=g_Lgt(_|($ z!j0>d(MUtO)!VY;)^?a)j&LktN0Rx>C`R6MQuYSXrGcv zk?y0@G%_yCDcXNC-I#7it{2|JpGw3x4zD@J+#*EnhWX86(J_ z9->t@dz9f*zl5lt!?BrM{fIHcqJt;(&SpQ5d){}=0}7xCdM8CAs#LrdgB46yIP9F- zZ3w!nkfJK?$JrE_z*_Hux-jNt(X0c!wK!yn7kopE95bhm9O+|ilNp(TJzE0JYazMD2OfQHL6?l*X0*F%z;lH zOx|epNs52BwqI=h&z)2lxTRzX|6;@H0TYzM?Tuj-!UF3?t| zlN9#je$unkxK!1s;K&I|pe%41)+2#aPY?n>IsU21@?$WA)-B1_ICnjPTlTvN!9zF; zqm(yOawzZ`T1ZZwpnJfp^}Wztj5s94Jj)PT+k=02nSVQ%ohX=zr3_5?UW!P_wIPk_ zF(I3qs4v?$e~crU#)dRWJ0IO&LleJf9nWbgdu;%EnLz1 zo`gxL>@4Eq_73LpWlrP@qV#n!w#@ z1rdL{%pXS}!8)WZcw@CG*~88|%zPWy!gifLJ*nfB1Dwp~Nd4T3OM$h(q2`Mkxf}xL z*h0I@^+`9;{nbn!4JmI}r)D8Cc=q^X=Emgd=CPK>VlA!?l-NNG%Qyh#-_-u#SD-AC zwbvh2MsMDg!93^!sZ-Yqy<3~&T_Pbtan*kytH5Wmh$ph<8OEH*w$!xMyCiku37&dK zQy+oOKnLSt|MU47S#||ww_!+2-;J_mxm+n*WRn@u&&)~^C`l)=O%xD zZ=IxQ29{N_d{+i~6V2xR3r2eQP=Bs+`tJM2$2X6WafjTO>hq4cQJp%ml`@DmPD2GtXkN&Eh{Qz3a!8$vt3R!kkTM4 zG@{}404eT$N%ttLg(+M{4i5x{d)|D5~qE!Q?6Q(A8Jh*Bx6U_dEBmM7A`)7(MEVDuBqE3kh@VpAUcGk8s1z7KMB{R~RtR ze8Ne4W!LHB*3>P(&$w-cpXTQdjCA#+*7m{@m5tZ6;e(%)^)iuJ7HZxmzd0JL-w!fr zzQ&-%Mm9xN;tnFeIRbxlhS?r~c*Y9vwBi}O0)gQ33zfy$Gy(yAL~TIkUA6C{%2#5N zC5#1Lp>!K=woyHaZ9t?k(=Dt*ltTb7SmGEQ3$w+O2q}jlCcmKn%kM7qXR00+odqY% zL5vOm5}M?R+ri$h1fd@9CXUbKBHPwyvE6O)bS*nyuJ8K#-JvMK_zJV{K@AF_05L+^SfE>UQ>ZV)%V zFd*aC?9Rs|D#(9npk9Mg*)h{-!wAXevKV6Z)Yvpha0X092P4$nh1Mb*M)nlnF3F%U zWkd~#h33Zfd$q9_ma+wA$Dg~wkEi=^2Rn)%qN*@zS&VG8Y*aN1{FPV~mOme2$lY^L zg&%qXG6fMamj#ODZ0ys5QB~d{jSa;kQ9n3KIjuh_jOu@HMSrB_l(xmvwSyGHvALGE z4Ak)`E%6dA0}!*}6C)0_)=Y>f*3WB(s(9p-HeUeP%jV2sr70B|u68FCB$p|_5qTwD z6OWli&ocn?`=-Tb^o2Xs_bNR!PAxEx^h`333d7s{#TMSvH23EitWLXYss(9Uvfz4y ziAa2b6tE`2a9dkq8F0!hA)P*c)&033lsJ4SdavE$g07=#DoCII52WNrahJhX1r&!f zX$FTgX$QA6X$Wur0XCDNH7b8yTXP#XvVPaEn8$N!E1JO_s7h^>Z%Slawqp4r+vNvZ zqAhN8aY!n0_SbLs*O(z@s8LLrIp<}otR4`zMqkkAZVYK_Rn=71no2dAo=v5!r>C!U zNc0Sq*Zho?H-Vn1^4?U|HI)yFo~lw>(?F*y6_VYt&Qw|_n!>qCo5p`qf#x!b`vjVl zXLXSZ(NQ5W8k)~Hm5vQf=v8G*;2K?-gc?TY!jAQ}a$0kfqXJEDy|0{Cgv--1qv6i6 z3Mxb@q$-$5h0s(X60o$~sA-ut=qfs1GoeY!x*Z#Am0X~Cf+IF4UMqc4ji*^G&8C#% z$s;jG8B2&GQL9{})@XmJ6cQndG(tBG*F|QEp}IsPG{GI4XoL<8*U<>mXu?KZQbtFj zh{h}9w5nV~BTUedN;JYGLnIOtmDQH(XoO|fIGTwBMdO@ek)_7(I9j)IN)emrPdP)Y zcf=j#9I@Cb8sU|qI!z=C6mBADmkWAbIG$riHDj5m{{_x_N)UWb5eI> zc4$&6ky=-Vc%zNg%oE-Wjug)D2wEQFpfwxj5OIu3iFsvctZleN6lklsl!yYWStn^G zZArd6KmNE=zx?ydw5ks$pQk(ZgR9Hs^m4f%p=jFIFLrBA1qG^Z(mguDOqpTP34dT(JXUR3q*+jpepyPgCP8%NJn zU0$D`e`x#e(JHDRf2`^~BMiZ)J=TV#+7AxG&mRILCm)muKt4DJp5<;DV&xBnsXm-v zog7V<)q8)U{^4F#znp$uR#?P)(&t^)^#8)G!w);}qcOXNp3bLTvc*G4Ek>tZ%RQ{! zCCjPxE*&5~G7MqYS3X&SE^s~VOlc)m)VpNK*}7=Ybw(3bA3edK4AlfWOak>M+hrK~ zn5ZqeCXcmLtErdTWxH%5HQx9z)X!w-qT32A=Zt@eS1$Es*{g>55nW>F4Xrg2HFW$K z=2N7#g(?u2T@|C$JLXg4c`Vu9x-7{LEWA%Bd4KTRwPqO%L`tXJrzRL8Ev1v}suKBvGoNElP(q(ZbMVnOj;S z4qktjSi|+kE1tO_p$1ZuKuW>uyE{}3pPUSCu66luRa10ceWnAF)-LeIt{N@^_w*jR z$}mRej6j%F2dM!{4@ONVDeI=dVv&N4dy12VOfYfj44`g34sU8K`3Dk$M9xSVnFG ztI!&3xo^NCff`G1TVyf(3`* zZi~AUT!Op1CFlY#fdmM!c#z=1-4_TR+}#4f7g!|t;&6OdcUAZA{!GnO_e@Pq&C@+I zJ^ko2)BK5o{cWhJm28IsSn1!dipII?BMcWJ33BJj7p(+XS9vUH|BPC#j?uS;suRE0 z&U#sZV|{+u-=n~7eSWXLsBEbevDz3=OQ&mJs-ye)-C$zn*1I7BuW3msdq33zHMy!c zj*?#qW5>#q3opUBqwh3pk|z`TE?X#SuC9gX`mbMnTY60LBo&J1KMp?Ly{AlTg0o2QF*60il|`X6XC~$uMZ@vQ|{hWWE4v% zkc6P@v_-zW-1L|>z&@)`TQ^T1D_g_bu?cd`haX(N->7Avc;^C|XnKTAh47kV>Kics z*s1(mb4)^*5xLGT=HzE%leF}!t|dM@9FaLf@iO}Xqk4%ix-{)I-w5{G=x_~ebzAo7 zH{1!Sn_!R`lD=YNashN3r^(Q-8d*Pw&%X6fBDHoorA{IYpyM5F8{u=B8|o)*An#|d zTs6L~qmW!2B+O$vK(WI5OxqRB;e_h+cH^2o$;3NDDB<^Wd~h& zi9?r7#(QcXK%v&emyW&Q&+CTv?ZXW=@rPLbf;N||Oup$fBR|?=PruOw6-bxr_kn3I z4QOpkxzbaV`)BEnp`)#sbnF3yp^X&cL%Rm-)rTBG>@C_Q!bGpwb{nwVA2)?=G-zz)Ypf|`2B_~)jl;i#3u8;>fZ;H1WnvC3HNlMWWD$>7hnzLJToM;@CyTC-8**7Ki@D?K^<$G zS8UoG(-Y{ZDI};1wJvB4$EJ$oDms9rpBuN<(Z-c?CgAYQ=w0p_-)k z4dT_HJ8J_axnwXdFnhO^f<|&%F>y|2mJ~T=5Sy1l(OLghXK=FiZygJrYa+T#d|ibp zAn4fV_4#+acmJ!qEbY> zZRmzg1(D?k-_zEfax9z9cQ7KU&){7p0|n6p1Zl`OIR5%gxDpMX)ya7m3CUXHMc%jt z$7k=n-1M|icC&j|hP24kd>(}chVs>EDW!I#BXBi1-^5!%Y;jx+jSGGQ*f)K zJNNbPKtnF@i@X!HQtG}!5LhIrWwIRk1*^__#HGrM^v_8S(vh}(FsMP%XO?4Cmp1WG};gTUZOxeNw5gXM##E=4L>O(Q8M^gS;os;!H)dHBvTw58UG$de zkK*%u-;eLB?Bn|YoOE(Cq3T07A6Sx6kp;^$ENat^M4w$Iw@912rW8|fytDxH3&aNG zH@3P-YPYJKp-Gqi@hz^WXe1ljAaW2d`%a=4PwJvU@(1g6QNocE0#d^n0$GOABv{kW zE^V>SPz=OvrjR{3SH*g2edd=Niq~f{AEylx_r!i43;_zj%5v{gI9mtr=5ktLJW z$14Gkb}_QcY%m-RyQ2Nih%*l7KuMK;5lR-(n;@aiQr^*^VLc+estUXRU7rR4Z|7IT zn@4yETN(9;ngG;-FhU=$z}J0`U#023wnv53OLS(2=m#`MjI!jP-$SmEgfP)iu5>DN zdA5LENkt~`;S|@iXAx$o@l)hrs2a0rLwDxDZsw4E2sS$E?RVlj03aB*2a`9K{ zZDZe>>07`v9P;+C?hHK+>7q)u^qmvVv@j>za!8%*x-;Ia9W>Vr97paF*@eE1g}1>l z7t0>-ivJ$LNoq&_#pW$aDF0f@i&H%cL#MXdeg+at?G6+xiQpMz9DmF#S!9kuVA%?b z3v;l@e*dRDr*5V+{_6mRW*dbbhL0Xr$u|DUsO+RM>J*6gUW$#jEiPf-A&}2i7M;lL z+G=-YG8o^-y!Q5_4fns|oG52@_jh}v6RE|wDSJYe^a}k-=;gy}?Q&k| z9@nJ6VUba^@A~#7Hrx^BRR$jp0jQ(&-EX`XB4+xA0ui?UpwtEP95v2n*vV!2!o=h0 z`ubF@Q^`i)nZK4H+>_dU{V~_|GE6<&eA9=W2P^OZ9Q~&4vx+R0YRA1;R*;0T-o@tx zj~?8PJdL}Np_{|)RoL!1iy#$8F-i4M=+W$eKPn5OnukF8xk}xWPL6pHke#JE&Xig_ z0$+eV4YMNb`2U2jmUjU1bM>hji0n3+G91J}3Ga`R-^*ge$7dChXG1BvHx5|82nAC< zJ>(}c{d4_S56-GZA*9gXdRmgOkx~6Uh-o-ksyETV8B-evaoI^OuodYVPuA9F-x*wgP z#G4V{@U%bG(*veqfw(|tqnMjrOA9Fr;oJM0R@y+e2Ga<Y8Q9ImOdZEWi!UJla1`KW1_*bW%|^rf z4!8I3_vy}j7K59FN)%?=i)y)!m9GY>4l zw9DZ-;JP;@hymo46{Zi{el1_nx!R1Fbqb65UB2=>-aFdkQMvD7DJN_#a_f_{+WG4v zK|NtjkvUQQDD>dBdK9{JoOBL{4K-#{Ch?Bcr*J)2nS!N%cqAuC}Wlb^ZNrJrM1f^9Q23zQv?iZ6=P~7~G4> z+jyTP0wJ$*)fD{~v?4Wbr+2h>n!l?dJ-(=X7)cdKK6VN#TMa)eQrlY^Oc56q3l6x( zxmfYS-XizCH=V)zEwIPqJJmv|GFdBbd>_DLm_0}B_{A@gdT8Yob!MDiz3{2; z@GL;<3>X8E8`kPabc(fIA*dC>S8*A$F-ttMikaPleDE)M9HvyLL92y3892!LKX{x~ z#>Fdf_h$l(%n_x32KmK*oi+PP@9@hEo_{0jgYbfe3ObX@n2x68lY^=z1~1zx zs`vfdOHwbXFLQ#71bJ26ak9lbuaX^tJSVTU0HY5*1O@rbB_K>hoEJhupm2_#p>jLt z0=_iJD=z5=J`tFCqX4H3!V3^9wXOT=ea3U?dye>TssG*e)UtIR(<4ZH+;g7uG3(+m zNq}me%jqod;Els}@ogK`X@-G(HF&!mf<3xA6@7Q7@#S6%rDqMwaCTF^4cRGx0c*;S za2JsrPP^!U0MB9Qcc^7f2SjzO_3jFRFbnDM)ahBHX1XQZH4e<_sQsi;FKl_We|H&n zYxz*JS`L%}jKY$P%Jt$wdXf>nar>#4<+t7sMH1l`iVug+5&c~qucrFB#N0%XE$eup zN7Zf!P$qfWX$S#2leDu`n$LiiXoZRWddX)1a}C`-ls|s|6uW}B^-|avB?|q)m0u-_ zQQJA!X==_<{K?4&&2gakJJe@f{ChByP4v=&0Chc9#{R+W?O8H%cvAUI!(*1q$-?c# z?b>B$@p*ZNK=as2{9X0Gc6`?wA60Uh?XU>*1&lo?kX1osj z%gy;{m95>xvEYf-JK125r_1hq+0DKw*N7Tg!I^dPyP^#j$Bh)nIms_aJ8d4dozi~J zht?_-({{|Sb18;@CT0mlZGO|XT_wayZY-Mk2^kMJ&!(pQ_dv%!y~RH5BBo>-x_g(+ z8#C)T!X6NBNbeJN)OP@k7J*bk#-8BeM`kYP<`ER_uE3R#Z%fXyshEu<^iWgzQej{w z-#q*9Seyhi#?9c-kSH-^*PM1kFc?dNhd=D~!7&XI$gS@ROl-34DMpu|VTiZJgtl=b zxI8LxEGQy!+!^@m2|?*MAz9Dc56*xvbY>Fkyp8bE4$Qo|%>ddiCU+mg$klqI24vsS zQr%CoVmH@K;nzK_PxVB&2$=s{+vEnR?P?0~X80n25tkmu?7p$!KF2&F8KDzSstgD|mH~BK`b00&f`620UNZ4r~2Q&LNxF#*M8OC|?~fJ1&6+1xT)2d(8oRpH6YPX19Ztc9=HQ2Cd^}(T{0&+{>isMIV^9=#Z zYOIwXD|F$LKiWRVCbH(Y+HN2HiLHp4SSe9ug|{R;suM2O{~l{w8yS(*WENDkq3P58 zz4se=3uumDAv(uSTJG0$f{m%4#_gSV)5j=!+1npMfnQOQ!qfKeW8QJAp(YAr`S~ z>(k*i;Ktunvpb6s#{$^32cW~+u5oIk!*Q3`pcA^^crERe!gu$S2)mDmVZP|$iw}6M zY_;HanSVz+gBZRyvfIug3xv%{EH4*)HCt9qZ(n#D=?Haj?R&I_x{(VG{OvrV+BDMv z1g#bJ5N;n=dRjMW5#B+s3OgZ2-}M;sqJkB=g~RPKFlD$~a_ zm)+v_)WQJYmT|)JCyea}l_6TMpk+Os3TDdXV~fpscSQL0LIdaZ6q*f7BNI(9;Qdj} zpf!b@6Yeup{Km-9sz`~Ml&Wy3_;+A zN40jyKhM(0z@YOd+jg}H?sO|Pw=t|{a%9ls=>^(Tz%8iw;#ZE8FJoLVuPAIg)I{pz zFPZF3+Y^nw5uH%LJs1?7L;dfIEV9|7f1v*`8{WNl$~|GGg6c+=2k8{wV;u2zI z+1H`3w=2v*KD0KQRD6Q-@d;zj%$DZ=a&4uK>7ikyGJeMV#wy6e&Ck!x!^X|S#Ldmb zg2kogZX;*;$(Dv$PK1}6M~H`q_kUEHmOf)%pld5A@X8B<1o)*DNbRAzu7#n|P8JmE9jqeSs;CNXnE zAqm#SMR2FI`vo#gZx8*w3Rgpe)GJoJ1RDJ05}sUI(ir;pf!qpes$Fu_;b}@TK0l{O z1E;!VAya!OJb2c0_*5|jeK#pw<_ov>h<}Iam(_gzr00WV){y7p;A5O;`uyT=A_ru4 zBjP_^(=UMDNw29Wz;=c2iMGIy7%waVq2aU$IMxhUiKC!ec*E!QwEI za1=0zATrAWJr~Org-q0@T>AAN1^&Ok zj5H&ln2^7Xm$^u;Y(Lzv<+f~G_#C9k3 z9}k? zj=uWVZk$}UG-Ts0#u~~)WN;Vu;za$D6}lI2!ErsvL8ud;qcgnBVY$j};Y(>3wW!{d z>>#HKhN#~tJv6cL!JEw0iWJ=uK(D?VP3x?Yls?(+mMS#SEr4dKL<`p3a_ zsQ4Dd5E5sLoio-5%D5JDaU9;`T75C9PM9b2k>_>VK*9l)2BTPPELiOF^8n9kU>h*7 z1wW@^>X<3Cv{HQKWw0>SKoRcEh9uza7$R)?wkxp;*+NbqttO`&DQ$cXsbYuh1^P#| z7sf5bA?YiuAzw|%yM(GxEJz|uDSSNBdM`uFCNWMzd#J0ZH7#-Ug-kX)zV;CPPlX&c zz|Ww^@^u7=V%{U*ITUhJ9|#nw`Z}bhB~i@Q`+_KmKElx;HPJnsIITk18%2F4K_&TV zy;^5(IcXYvA9S1#3;8sE<^gbs^L@&f-(BcGNh8Csj1oAe zUU}d4pixdzhnm#Ljb;hz&J>xWp7pMD7XQ#Yw5uUNBNz^^{s1U*^C(6NLNti^*0L#;-*_%4qTM*Pl36oTv{G-dBl=b!e)bgm#Brxd<$v}kr+rpT2kCGod-c83k(ld|C zM$2hOJWfV(MIlRh$`k6#dCFrxv+wcnA+_Q=dTM!0$w(>7F99J&(G8eR2l=CPZnz10 zZ+yc`UU=w4GB-!wNz2{HC2KqvMiROP$tk(pJuiLdtY&Y3E8I?Kr|{`5{Q}=XodB1Qp}fVSyAIU z&C=K2M3aF4mA3UDh!MTSN~KnLFH^^)!}ngUCdUS&&GROZQ&P-$C&(!^=G{KLM3%Qo za<)W=K!pjkpV<4&4l=K_IUG&qty1@Xgnd6@`@olf|NHhtF=&4a%aYzZ1<9D%f`J*y zQ4{Op*9RO{DTc`dJx~c!qg1u=vt8j2eI_|Hk}4N07{AW>IeP=%krV@YQ~h6O;b!A* f<%IR|lcm=uKQCK5ECF7AAwgj*1_pTz1+4!999#TI diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index bb7a6f0..66a773b 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -25,17 +25,20 @@ doc_class abstract = doc_class text_section = main_author :: "author option" <= None fixme_list :: "string list" <= "[]" + level :: "int option" <= "None" + (* we follow LaTeX terminology on levels + part = Some -1 + chapter = Some 0 + section = Some 1 + subsection = Some 2 + subsubsection = Some 3 + ... *) + (* for scholarly paper: invariant level > 0 *) doc_class introduction = text_section + comment :: string claims :: "thm list" -doc_class introduction_title = introduction + - fixme_list :: "string list" <= "[]" - -doc_class introduction_elem = introduction + - fixme_list :: "string list" <= "[]" - doc_class technical = text_section + definition_list :: "string list" <= "[]" formal_results :: "thm list" @@ -84,16 +87,14 @@ text \underlying idea: a monitor class automatically receives a doc_class article = style_id :: string <= "''LNCS''" version :: "(int \ int \ int)" <= "(0,0,0)" - accepts "(title ~~ - \subtitle\ ~~ - \author\\<^sup>+ ~~ - abstract ~~ - introduction_title ~~ - \introduction_elem\\<^sup>+ ~~ - \technical || example\\<^sup>+ ~~ - \introduction\ ~~ - conclusion ~~ - bibliography)" + accepts "(title ~~ + \subtitle\ ~~ + \author\\<^sup>+ ~~ + abstract ~~ + introduction ~~ + \technical || example\\<^sup>+ ~~ + conclusion ~~ + bibliography)" gen_sty_template diff --git a/ontologies/technical_report.thy b/ontologies/technical_report.thy index e64319a..b4fed9d 100644 --- a/ontologies/technical_report.thy +++ b/ontologies/technical_report.thy @@ -4,15 +4,19 @@ theory technical_report imports "scholarly_paper" begin +(* for reports paper: invariant: level \ -1 *) + doc_class table_of_contents = - depth :: int <= 3 + bookmark_depth :: int <= 3 + depth :: int <= 3 doc_class front_matter = - style :: string + front_matter_style :: string (* TODO Achim :::: *) + +doc_class index = + kind :: "doc_class" + level :: "int option" -doc_class "chapter" = text_section + - style :: string - doc_class report = style_id :: string <= "''LNCS''" version :: "(int \ int \ int)" <= "(0,0,0)" @@ -25,7 +29,7 @@ doc_class report = introduction ~~ \technical || example\\<^sup>+ ~~ conclusion ~~ - \table_of_contents\ ~~ + \index\\<^sup>+ ~~ bibliography)" end From 4da4434a2767ce2acd4883addd0e1a0da4d3e8ac Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 11:23:51 +0100 Subject: [PATCH 02/13] Small corrections in the ontologies. --- ontologies/scholarly_paper.thy | 4 ++-- ontologies/technical_report.thy | 16 ++++++++-------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index 66a773b..ed95253 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -91,9 +91,9 @@ doc_class article = \subtitle\ ~~ \author\\<^sup>+ ~~ abstract ~~ - introduction ~~ + \introduction\\<^sup>+ ~~ \technical || example\\<^sup>+ ~~ - conclusion ~~ + \conclusion\\<^sup>+ ~~ bibliography)" gen_sty_template diff --git a/ontologies/technical_report.thy b/ontologies/technical_report.thy index b4fed9d..e287593 100644 --- a/ontologies/technical_report.thy +++ b/ontologies/technical_report.thy @@ -20,15 +20,15 @@ doc_class index = doc_class report = style_id :: string <= "''LNCS''" version :: "(int \ int \ int)" <= "(0,0,0)" - accepts "(title ~~ - \subtitle\ ~~ - \author\\<^sup>+ ~~ - \front_matter\ ~~ - abstract ~~ - \table_of_contents\ ~~ - introduction ~~ + accepts "(title ~~ + \subtitle\ ~~ + \author\\<^sup>+ ~~ + \front_matter\ ~~ + abstract ~~ + \table_of_contents\ ~~ + \introduction\\<^sup>+ ~~ \technical || example\\<^sup>+ ~~ - conclusion ~~ + \conclusion\\<^sup>+ ~~ \index\\<^sup>+ ~~ bibliography)" From 23bc75d08d695ab57fe84f34b874c485f68dbb15 Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 13:19:31 +0100 Subject: [PATCH 03/13] Corrections in ontologies (revealed by examples) - identified problem: accept/reject conflicts were only detected at application time, not at declaration time :-( (leaved as "known problem" for the moment) - new functionality for declaring doc class invariants --- Isa_COL.thy | 2 +- Isa_DOF.thy | 52 ++++++++++++++++++++--------- examples/cenelec/Example.thy | 3 -- examples/conceptual/Attributes.thy | 2 +- examples/simple/Concept_Example.thy | 8 +++++ ontologies/Conceptual.thy | 11 +++++- ontologies/technical_report.thy | 3 ++ 7 files changed, 60 insertions(+), 21 deletions(-) diff --git a/Isa_COL.thy b/Isa_COL.thy index 90892ac..fb0b4bd 100644 --- a/Isa_COL.thy +++ b/Isa_COL.thy @@ -34,7 +34,7 @@ doc_class figure_group = (* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *) anchor :: "string" caption :: "string" - rejects figure, figure_group (* this forbids recursive figure-groups *) + rejects figure_group (* this forbids recursive figure-groups *) accepts "\figure\\<^sup>+" ML\@{term "side_by_side_figure"}; diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 0e91ef0..3ccad46 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -66,8 +66,9 @@ section\ A HomeGrown Document Type Management (the ''Model'') \ ML\ structure DOF_core = struct - type docclass_struct = {params : (string * sort) list, (*currently not used *) - name : binding, thy_name : string, id : serial, (* for pide *) + type docclass_struct = {params : (string * sort) list, (*currently not used *) + name : binding, + thy_name : string, id : serial, (* for pide *) inherits_from : (typ list * string) option, (* imports *) attribute_decl : (binding * typ * term option) list, (* class local *) rejectS : term list, @@ -188,7 +189,7 @@ fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab fun upd_docclass_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab, docclass_inv_tab} = {docobj_tab = docobj_tab,docclass_tab = docclass_tab, ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, - docclass_inv_tab= f docclass_inv_tab}; + docclass_inv_tab = f docclass_inv_tab}; fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids @@ -232,12 +233,19 @@ fun is_defined_cid_global cid thy = let val t = #docclass_tab(get_data_global th Symtab.defined t (name2doc_class_name thy cid) end +fun is_defined_cid_global' cid_long thy = let val t = #docclass_tab(get_data_global thy) + in cid_long=default_cid orelse Symtab.defined t cid_long end + + fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) in cid=default_cid orelse Symtab.defined t (name2doc_class_name_local ctxt cid) end +fun is_defined_cid_local' cid_long ctxt = let val t = #docclass_tab(get_data ctxt) + in cid_long=default_cid orelse Symtab.defined t cid_long end + fun is_declared_oid_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy) in Symtab.defined tab oid end @@ -272,6 +280,24 @@ fun declare_object_local oid ctxt = handle Symtab.DUP _ => error("multiple declaration of document reference")) end + +fun update_class_invariant cid_long f thy = + let val _ = if is_defined_cid_global' cid_long thy then () + else error("undefined class id : " ^cid_long) + in map_data_global (upd_docclass_inv_tab (Symtab.update (cid_long, + (fn ctxt => ((writeln("Inv check of :" ^cid_long); f ctxt )))))) + thy + end + +fun get_class_invariant cid_long thy = + let val _ = if is_defined_cid_global' cid_long thy then () + else error("undefined class id : " ^cid_long) + val {docclass_inv_tab, ...} = get_data_global thy + in case Symtab.lookup docclass_inv_tab cid_long of + NONE => K true + | SOME f => f + end + val SPY = Unsynchronized.ref(Bound 0) fun check_regexps term = @@ -464,9 +490,10 @@ fun update_value_global oid upd thy = val ISA_prefix = "Isa_DOF.ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *) -fun get_isa_global isa thy = case Symtab.lookup (#ISA_transformer_tab(get_data_global thy)) (ISA_prefix^isa) of - NONE => error("undefined inner syntax antiquotation: "^isa) - |SOME(bbb) => bbb +fun get_isa_global isa thy = + case Symtab.lookup (#ISA_transformer_tab(get_data_global thy)) (ISA_prefix^isa) of + NONE => error("undefined inner syntax antiquotation: "^isa) + | SOME(bbb) => bbb fun get_isa_local isa ctxt = case Symtab.lookup (#ISA_transformer_tab(get_data ctxt)) (ISA_prefix^isa) of @@ -894,13 +921,13 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) val _ = if Long_Name.base_name lhs = lhs orelse ln = lhs then () else error("illegal notation for attribute of "^cid_long) fun join (ttt as @{typ "int"}) - = Const (@{const_name "plus"}, ttt --> ttt --> ttt) + = Const (@{const_name "Groups.plus"}, ttt --> ttt --> ttt) |join (ttt as @{typ "string"}) - = Const (@{const_name "append"}, ttt --> ttt --> ttt) + = Const (@{const_name "List.append"}, ttt --> ttt --> ttt) |join (ttt as Type(@{type_name "set"},_)) - = Const (@{const_name "sup"}, ttt --> ttt --> ttt) + = Const (@{const_name "Lattices.sup"}, ttt --> ttt --> ttt) |join (ttt as Type(@{type_name "list"},_)) - = Const (@{const_name "append"}, ttt --> ttt --> ttt) + = Const (@{const_name "List.append"}, ttt --> ttt --> ttt) |join _ = error("implicit fusion operation not defined for attribute: "^ lhs) (* could be extended to bool, map, multisets, ... *) val rhs' = instantiate_term tyenv' (generalize_term rhs) @@ -1491,11 +1518,6 @@ ML\ section\ Testing and Validation \ -text*[sdf] {* f @{thm refl}*} -text*[sdfg] {* fg @{thm refl}*} - -text*[xxxy] {* dd @{docitem \sdfg\} @{thm refl}*} - (* the following test crashes the LaTeX generation - however, without the latter this output is instructive ML\ diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy index 34bcaeb..830eb3b 100644 --- a/examples/cenelec/Example.thy +++ b/examples/cenelec/Example.thy @@ -70,9 +70,6 @@ paragraph* [sdfk] \ just a paragraph - lexical variant \ section\ Some global inspection commands for the status of docitem and doc-class tables ... \ -print_doc_classes -print_doc_items - section\ Text Antiquotation Infrastructure ... \ diff --git a/examples/conceptual/Attributes.thy b/examples/conceptual/Attributes.thy index fe7abe6..6a6e5a9 100644 --- a/examples/conceptual/Attributes.thy +++ b/examples/conceptual/Attributes.thy @@ -10,7 +10,7 @@ print_doc_items (* this corresponds to low-level accesses : *) ML\ -val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab} +val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...} = DOF_core.get_data @{context}; Symtab.dest docitem_tab; diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy index 385f0af..476a1be 100644 --- a/examples/simple/Concept_Example.thy +++ b/examples/simple/Concept_Example.thy @@ -41,6 +41,14 @@ close_monitor*[struct] text\And the trace of the monitor is:\ ML\@{trace_attribute struct}\ +print_doc_classes +print_doc_items + +ML\ + +\ + +setup\DOF_core.update_class_invariant "Conceptual.A" (K true)\ end \ No newline at end of file diff --git a/ontologies/Conceptual.thy b/ontologies/Conceptual.thy index 9182c84..32c3a16 100644 --- a/ontologies/Conceptual.thy +++ b/ontologies/Conceptual.thy @@ -41,5 +41,14 @@ doc_class G = C + doc_class M = trace :: "(A + C + D + F) list" accepts "A ~~ \C || D\\<^sup>* ~~ \F\" - + + +section*[test::A]\ Test and Validation\ +text\Defining some document elements to be referenced in another theory: \ +text*[sdf] {* f @{thm refl}*} +text*[sdfg] {* fg @{thm refl}*} + +text*[xxxy] {* dd @{docitem \sdfg\} @{thm refl}*} + + end \ No newline at end of file diff --git a/ontologies/technical_report.thy b/ontologies/technical_report.thy index e287593..51db48b 100644 --- a/ontologies/technical_report.thy +++ b/ontologies/technical_report.thy @@ -32,5 +32,8 @@ doc_class report = \index\\<^sup>+ ~~ bibliography)" +ML\ +\ + end From 6b85bd74cd5a22119c34c76b5bef86d2d4418e34 Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 14:14:53 +0100 Subject: [PATCH 04/13] Very first example of class invariant checking ... --- Isa_DOF.thy | 7 ++++++- examples/simple/Concept_Example.thy | 7 +++++-- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 3ccad46..e2456d1 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -176,7 +176,7 @@ fun upd_docobj_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab,d {docobj_tab = f docobj_tab, docclass_tab=docclass_tab, ISA_transformer_tab=ISA_transformer_tab, monitor_tab=monitor_tab, docclass_inv_tab=docclass_inv_tab}; -fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab, docclass_inv_tab} = +fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab, docclass_inv_tab} = {docobj_tab=x,docclass_tab = f y,ISA_transformer_tab = z, monitor_tab=monitor_tab, docclass_inv_tab=docclass_inv_tab}; fun upd_ISA_transformers f{docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab, docclass_inv_tab} = @@ -1008,12 +1008,14 @@ fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy = fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults + val check_inv = (DOF_core.get_class_invariant cid_long thy) o Context.Theory in thy |> DOF_core.define_object_global (oid, {pos = pos, thy_name = Context.theory_name thy, value = value_term, id = id, cid = cid_long}) |> register_oid_cid_in_open_monitors oid pos cid_long + |> (fn thy => (check_inv thy; thy)) end @@ -1038,8 +1040,10 @@ fun update_instance_command (((oid:string,pos),cid_pos), Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs val def_trans = #1 o (calc_update_term thy cid_long assns') + val check_inv = (DOF_core.get_class_invariant cid_long thy) o Context.Theory in thy |> DOF_core.update_value_global oid (def_trans) + |> (fn thy => (check_inv thy; thy)) end @@ -1315,6 +1319,7 @@ fun docitem_value_ML_antiquotation binding = (* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*) val _ = Theory.setup((docitem_ref_antiquotation @{binding docref} DOF_core.default_cid) #> + (* deprecated syntax ^^^^^^*) (docitem_ref_antiquotation @{binding docitem_ref} DOF_core.default_cid) #> (* deprecated syntax ^^^^^^^^^^*) (docitem_ref_antiquotation @{binding docitem} DOF_core.default_cid) #> diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy index 476a1be..7a9d527 100644 --- a/examples/simple/Concept_Example.thy +++ b/examples/simple/Concept_Example.thy @@ -48,7 +48,10 @@ ML\ \ -setup\DOF_core.update_class_invariant "Conceptual.A" (K true)\ - +setup\DOF_core.update_class_invariant "Conceptual.A" (fn thy => (writeln "ZZZ"; true))\ + +section*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ + + end \ No newline at end of file From 184a17f97759407572be6312f2f93f48385b8186 Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 14:25:04 +0100 Subject: [PATCH 05/13] Refinement: class invariants now gets also the oid from its context. --- Isa_DOF.thy | 8 ++++---- examples/simple/Concept_Example.thy | 3 ++- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index e2456d1..3c57cf5 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -122,7 +122,7 @@ struct type ISA_transformer_tab = (theory -> term * typ * Position.T -> term option) Symtab.table val initial_ISA_tab:ISA_transformer_tab = Symtab.empty - type docclass_inv_tab = (Context.generic -> bool) Symtab.table + type docclass_inv_tab = (string -> Context.generic -> bool) Symtab.table val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty type open_monitor_info = {accepted_cids : string list, @@ -294,7 +294,7 @@ fun get_class_invariant cid_long thy = else error("undefined class id : " ^cid_long) val {docclass_inv_tab, ...} = get_data_global thy in case Symtab.lookup docclass_inv_tab cid_long of - NONE => K true + NONE => K(K true) | SOME f => f end @@ -1008,7 +1008,7 @@ fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy = fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults - val check_inv = (DOF_core.get_class_invariant cid_long thy) o Context.Theory + val check_inv = (DOF_core.get_class_invariant cid_long thy oid) o Context.Theory in thy |> DOF_core.define_object_global (oid, {pos = pos, thy_name = Context.theory_name thy, value = value_term, @@ -1040,7 +1040,7 @@ fun update_instance_command (((oid:string,pos),cid_pos), Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs val def_trans = #1 o (calc_update_term thy cid_long assns') - val check_inv = (DOF_core.get_class_invariant cid_long thy) o Context.Theory + val check_inv = (DOF_core.get_class_invariant cid_long thy oid) o Context.Theory in thy |> DOF_core.update_value_global oid (def_trans) |> (fn thy => (check_inv thy; thy)) diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy index 7a9d527..d4e6eed 100644 --- a/examples/simple/Concept_Example.thy +++ b/examples/simple/Concept_Example.thy @@ -48,7 +48,8 @@ ML\ \ -setup\DOF_core.update_class_invariant "Conceptual.A" (fn thy => (writeln "ZZZ"; true))\ +setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => + fn thy => (writeln ("ZZZ:"^oid); true))\ section*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ From 04f5e99e415dad6ceacba8b56a407693f30c61bd Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 16:43:27 +0100 Subject: [PATCH 06/13] First running example for class invariants. --- Isa_DOF.thy | 14 +++++++------- .../{simple => conceptual}/Concept_Example.thy | 8 -------- .../MyCommentedIsabelle.thy | 17 ++++++++++++++++- 3 files changed, 23 insertions(+), 16 deletions(-) rename examples/{simple => conceptual}/Concept_Example.thy (87%) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 3c57cf5..dfe346f 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -1333,7 +1333,7 @@ ML\ structure AttributeAccess = struct -fun calculate_attr_access ctxt proj_term term = +fun calculate_attr_access0 ctxt proj_term term = (* term assumed to be ground type, (f term) not necessarily *) let val [subterm'] = Type_Infer_Context.infer_types ctxt [proj_term $ term] val ty = type_of (subterm') @@ -1354,9 +1354,9 @@ fun calculate_attr_access ctxt proj_term term = Syntax.string_of_term ctxt subterm') end -fun calculate_attr_access_check ctxt attr oid pos = (* template *) - case DOF_core.get_value_local oid (Context.the_proof ctxt) of - SOME term => let val ctxt = Context.the_proof ctxt +fun calc_attr_access ctxt attr oid pos = (* template *) + case DOF_core.get_value_global oid (Context.theory_of ctxt) of + SOME term => let val ctxt = (Proof_Context.init_global (Context.theory_of ctxt)) val SOME{cid,pos=pos_decl,id,...} = DOF_core.get_object_local oid ctxt val markup = docref_markup false oid id pos_decl; val _ = Context_Position.report ctxt pos markup; @@ -1366,7 +1366,7 @@ fun calculate_attr_access_check ctxt attr oid pos = (* template *) SOME f => f | NONE => error ("attribute undefined for ref"^ oid) val proj_term = Const(long_name,dummyT --> ty) - in calculate_attr_access ctxt proj_term term end + in calculate_attr_access0 ctxt proj_term term end | NONE => error "identifier not a docitem reference" val _ = Theory.setup @@ -1378,7 +1378,7 @@ val _ = Theory.setup >> (fn(attr:string,(oid:string,pos)) => (ML_Syntax.atomic o ML_Syntax.print_term) - (calculate_attr_access_check ctxt attr oid pos)) + (calc_attr_access ctxt attr oid pos)) : string context_parser ) (ctxt, toks)) @@ -1387,7 +1387,7 @@ val _ = Theory.setup fun calculate_trace ctxt oid pos = (* grabs attribute, and converts its HOL-term into (textual) ML representation *) let fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) - val term = calculate_attr_access_check ctxt "trace" oid pos + val term = calc_attr_access ctxt "trace" oid pos val string_pair_list = map conv (HOLogic.dest_list term) val print_string_pair = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_string in ML_Syntax.print_list print_string_pair string_pair_list end diff --git a/examples/simple/Concept_Example.thy b/examples/conceptual/Concept_Example.thy similarity index 87% rename from examples/simple/Concept_Example.thy rename to examples/conceptual/Concept_Example.thy index d4e6eed..d8c3cdb 100644 --- a/examples/simple/Concept_Example.thy +++ b/examples/conceptual/Concept_Example.thy @@ -44,14 +44,6 @@ ML\@{trace_attribute struct}\ print_doc_classes print_doc_items -ML\ - -\ - -setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => - fn thy => (writeln ("ZZZ:"^oid); true))\ - -section*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ end diff --git a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy index faceaa5..cbe7d76 100644 --- a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy @@ -271,7 +271,14 @@ Context.certificate_theory_id : Context.certificate -> Context.theory_id; Context.theory_name : theory -> string; Context.map_theory: (theory -> theory) -> Context.generic -> Context.generic; *} - + + +text\ML structure @{ML_structure Proof_Context}:\ +ML\ + Proof_Context.init_global: theory -> Proof.context; + Context.Proof: Proof.context -> Context.generic; (* the path to a generic Context *) + Proof_Context.get_global: theory -> string -> Proof.context +\ subsection\Mechanism 2 : global arbitrary data structure that is attached to the global and @@ -783,6 +790,14 @@ Gentzen Natural Deduction (to which Isabelle/Pure is geared) reasoning and Gentzen Sequent Deduction.\ +section\The classical goal package\ + +ML\ open Goal; +Goal.prove_internal : Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm; + +Goal.prove_global : theory -> string list -> term list -> term -> + ({context: Proof.context, prems: thm list} -> tactic) -> thm +\ section\The Isar Engine\ From dd942cfb99b7dbe7b1f9f6f0e6c3e2731798b72d Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 16:46:11 +0100 Subject: [PATCH 07/13] rearrangement --- examples/simple/Concept_Example.thy | 50 ++++++++++++++++++++ examples/simple/Concept_ExampleInvariant.thy | 39 +++++++++++++++ 2 files changed, 89 insertions(+) create mode 100644 examples/simple/Concept_Example.thy create mode 100644 examples/simple/Concept_ExampleInvariant.thy diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy new file mode 100644 index 0000000..d8c3cdb --- /dev/null +++ b/examples/simple/Concept_Example.thy @@ -0,0 +1,50 @@ +chapter\Setting and modifying attributes of doc-items\ + +theory Concept_Example + imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *) +begin + +text\@{theory Conceptual} provides a monitor @{typ M} enforcing a particular document structure. + Here, we say: From now on, this structural rules are respected wrt. all doc\_classes M is + enabled for.\ +open_monitor*[struct::M] + +section*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ + +text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ + +text*[d::D, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, + ... @{docitem \c1\} @{thm "refl"}\ + + +update_instance*[d::D, a1 := X2] + +text\ ... in ut tortor ... @{docitem \a\} ... @{A \a\}\ + +text*[c2::C, x = "''delta''"] \ ... in ut tortor eleifend augue pretium consectetuer. \ + +section*[f::F] \ Lectus accumsan velit ultrices, ... }\ + +theorem some_proof : "P" sorry + +text\This is an example where we add a theorem into a kind of "result-list" of the doc-item f.\ +update_instance*[f::F,r:="[@{thm ''Concept_Example.some_proof''}]"] + +text\ ..., mauris amet, id elit aliquam aptent id, ... @{docitem \a\} \ + +text\Here we add and maintain a link that is actually modeled as m-to-n relation ...\ +update_instance*[f::F,b:="{(@{docitem ''a''}::A,@{docitem ''c1''}::C), + (@{docitem ''a''}, @{docitem ''c2''})}"] + +close_monitor*[struct] + +text\And the trace of the monitor is:\ +ML\@{trace_attribute struct}\ + +print_doc_classes +print_doc_items + + + +end + \ No newline at end of file diff --git a/examples/simple/Concept_ExampleInvariant.thy b/examples/simple/Concept_ExampleInvariant.thy new file mode 100644 index 0000000..850ac48 --- /dev/null +++ b/examples/simple/Concept_ExampleInvariant.thy @@ -0,0 +1,39 @@ +chapter\Setting and modifying attributes of doc-items\ + +theory Concept_ExampleInvariant + imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *) +begin + +print_doc_classes +print_doc_items + +ML\fun check_A_invariant oid ctxt = + let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here} + val (@{typ "int"},x_value) = HOLogic.dest_number term + in if x_value > 5 then error("class A invariant violation") else true end +\ + +text\Watch out: The current programming interface to document class invariants is pretty low-level: +\<^item> No inheritance principle +\<^item> No high-level notation in HOL +\<^item> Typing on ML level is assumed to be correct. +The implementor of an ontology must know what he does ... +\ +setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => + fn ctxt => + (writeln ("sample echo : "^oid); true))\ + +section*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ + +setup\DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\ + +(* test : should fail : +section*[c::A, x = "6"] \ Lorem ipsum dolor sit amet, ... \ +*) + +(* to test : updates *) + +(* to do: trace example *) + +end + \ No newline at end of file From 9c0bcd86c696b81e83e4dc4e235277047960306a Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 16:48:15 +0100 Subject: [PATCH 08/13] rearrangement --- examples/{simple => conceptual}/Concept_ExampleInvariant.thy | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename examples/{simple => conceptual}/Concept_ExampleInvariant.thy (100%) diff --git a/examples/simple/Concept_ExampleInvariant.thy b/examples/conceptual/Concept_ExampleInvariant.thy similarity index 100% rename from examples/simple/Concept_ExampleInvariant.thy rename to examples/conceptual/Concept_ExampleInvariant.thy From ac1180b5291b6b7a89b7c7dc282f67344406a94f Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 22:18:47 +0100 Subject: [PATCH 09/13] - checking class invariants - checking monitor class invariants --- Isa_DOF.thy | 11 ++- .../conceptual/Concept_ExampleInvariant.thy | 89 ++++++++++++++++--- ontologies/Conceptual.thy | 2 +- 3 files changed, 87 insertions(+), 15 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index dfe346f..3c27e19 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -1090,7 +1090,10 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos), SOME X => check_if_final X | NONE => error ("Not belonging to a monitor class: "^oid) val delete_monitor_entry = DOF_core.map_data_global (DOF_core.upd_monitor_tabs (Symtab.delete oid)) - in thy |> update_instance_command args + val {cid=cid_long, ...} = the(DOF_core.get_object_global oid thy) + val check_inv = (DOF_core.get_class_invariant cid_long thy oid) o Context.Theory + in thy |> update_instance_command args + |> (fn thy => (check_inv thy; thy)) |> delete_monitor_entry end @@ -1364,7 +1367,7 @@ fun calc_attr_access ctxt attr oid pos = (* template *) {long_name, typ=ty,...} = case DOF_core.get_attribute_info_local cid attr ctxt of SOME f => f - | NONE => error ("attribute undefined for ref"^ oid) + | NONE => error ("attribute undefined for reference: "^ oid) val proj_term = Const(long_name,dummyT --> ty) in calculate_attr_access0 ctxt proj_term term end | NONE => error "identifier not a docitem reference" @@ -1386,8 +1389,8 @@ val _ = Theory.setup fun calculate_trace ctxt oid pos = (* grabs attribute, and converts its HOL-term into (textual) ML representation *) - let fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) - val term = calc_attr_access ctxt "trace" oid pos + let val term = calc_attr_access ctxt "trace" oid pos + fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) val string_pair_list = map conv (HOLogic.dest_list term) val print_string_pair = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_string in ML_Syntax.print_list print_string_pair string_pair_list end diff --git a/examples/conceptual/Concept_ExampleInvariant.thy b/examples/conceptual/Concept_ExampleInvariant.thy index 850ac48..67b6297 100644 --- a/examples/conceptual/Concept_ExampleInvariant.thy +++ b/examples/conceptual/Concept_ExampleInvariant.thy @@ -4,14 +4,12 @@ theory Concept_ExampleInvariant imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *) begin +section\Example: Standard Class Invariant\ + +text\Status:\ print_doc_classes print_doc_items -ML\fun check_A_invariant oid ctxt = - let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here} - val (@{typ "int"},x_value) = HOLogic.dest_number term - in if x_value > 5 then error("class A invariant violation") else true end -\ text\Watch out: The current programming interface to document class invariants is pretty low-level: \<^item> No inheritance principle @@ -19,21 +17,92 @@ text\Watch out: The current programming interface to document class invari \<^item> Typing on ML level is assumed to be correct. The implementor of an ontology must know what he does ... \ + +text\Setting a sample invariant, which simply produces some side-effect:\ setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => fn ctxt => (writeln ("sample echo : "^oid); true))\ -section*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ +subsection*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ + + +text\Setting a sample invariant, referring to attribute value "x":\ +ML\fun check_A_invariant oid ctxt = + let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here} + val (@{typ "int"},x_value) = HOLogic.dest_number term + in if x_value > 5 then error("class A invariant violation") else true end +\ setup\DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\ -(* test : should fail : -section*[c::A, x = "6"] \ Lorem ipsum dolor sit amet, ... \ +(* test : should fail : *) +subsection*[c::A, x = "6"] \ Lorem ipsum dolor sit amet, ... \ + + +subsection*[d::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ + +(* test : update should fail : *) +update_instance*[d::A, x += "1"] + + +section\Example: Monitor Class Invariant\ + +text\Of particular interest are class invariants attached to monitor classes: since the +latter manage a trace-attribute, a class invariant on them can assure a global form of consistency. +It is possible to express: +\<^item> that attributes of a document element must satisfy particular conditions depending on the + prior document elements --- as long they have been observed in a monitor. +\<^item> non-regular properties on a trace not expressible in a regular expression + (like balanced ness of opening and closing text elements) +\<^item> etc. +\ + +text\A simple global trace-invariant is expressed in the following: it requires +that instances of class C occur more often as those of class D; note that this is meant +to take sub-classing into account: +\ + +ML\fun check_M_invariant oid ctxt = + let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here} + fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) + val string_pair_list = map conv (HOLogic.dest_list term) + val cid_list = map fst string_pair_list + val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) + fun is_C x = DOF_core.is_subclass ctxt' x "Conceptual.C" + fun is_D x = DOF_core.is_subclass ctxt' x "Conceptual.D" + val n = length (filter is_C cid_list) + val m = length (filter is_D cid_list) + in if m > n then error("class M invariant violation") else true end +\ + +setup\DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\ + +open_monitor*[struct::M] + + +section*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ + +text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ + +text*[d1::E, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, ... \ + +text*[c2::C, x = "''delta''"] \ ... in ut tortor eleifend augue pretium consectetuer... \ + +section*[f::E] \ Lectus accumsan velit ultrices, ... }\ + +(* test : close_monitor should fail : * +section*[f2::E] \ Lectus accumsan velit ultrices, ... }\ *) +ML\val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here}; + fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) + val string_pair_list = map conv (HOLogic.dest_list term) + \ +(* trace example *) +text\Setting a sample invariant, referring to attribute value "x":\ -(* to test : updates *) -(* to do: trace example *) +close_monitor*[struct] + end \ No newline at end of file diff --git a/ontologies/Conceptual.thy b/ontologies/Conceptual.thy index 32c3a16..0cbcc64 100644 --- a/ontologies/Conceptual.thy +++ b/ontologies/Conceptual.thy @@ -44,7 +44,7 @@ doc_class M = section*[test::A]\ Test and Validation\ -text\Defining some document elements to be referenced in another theory: \ +text\Defining some document elements to be referenced in later on in another theory: \ text*[sdf] {* f @{thm refl}*} text*[sdfg] {* fg @{thm refl}*} From 17c66f0fea6f0b1097bacf9707ffd9de5cb3c703 Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 22:36:08 +0100 Subject: [PATCH 10/13] Integrated is_monitor flag for monitor class invariants. Makes special treatment of monitor class invariants possible, when changes of trace are indirect... --- examples/conceptual/Concept_ExampleInvariant.thy | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/examples/conceptual/Concept_ExampleInvariant.thy b/examples/conceptual/Concept_ExampleInvariant.thy index 67b6297..aca91fc 100644 --- a/examples/conceptual/Concept_ExampleInvariant.thy +++ b/examples/conceptual/Concept_ExampleInvariant.thy @@ -20,14 +20,15 @@ The implementor of an ontology must know what he does ... text\Setting a sample invariant, which simply produces some side-effect:\ setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => - fn ctxt => - (writeln ("sample echo : "^oid); true))\ + fn {is_monitor = b} => + fn ctxt => + (writeln ("sample echo : "^oid); true))\ subsection*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ text\Setting a sample invariant, referring to attribute value "x":\ -ML\fun check_A_invariant oid ctxt = +ML\fun check_A_invariant oid {is_monitor:bool} ctxt = let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here} val (@{typ "int"},x_value) = HOLogic.dest_number term in if x_value > 5 then error("class A invariant violation") else true end @@ -62,7 +63,7 @@ that instances of class C occur more often as those of class D; note that this i to take sub-classing into account: \ -ML\fun check_M_invariant oid ctxt = +ML\fun check_M_invariant oid {is_monitor} ctxt = let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here} fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) val string_pair_list = map conv (HOLogic.dest_list term) From 5e7ac1c02ec7e4d4eb6ed48fc52e261e4e45ae89 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 4 Dec 2018 10:41:34 +0100 Subject: [PATCH 11/13] - Fixed the FrontEnd - level problem according to what we discussed: -- there are classes that do not have a level -- title, subtitle and abstract DO NOT HAVE a level -- text* has a level, but the level "None" - Tested whatever we have as examples --- Isa_COL.thy | 18 +++++-- Isa_DOF.thy | 48 +++++++++++-------- .../conceptual/Concept_ExampleInvariant.thy | 2 +- examples/math_exam/BAC2017/BAC2017.thy | 2 +- .../2018_cicm/IsaDofApplications.thy | 10 ++-- 5 files changed, 47 insertions(+), 33 deletions(-) diff --git a/Isa_COL.thy b/Isa_COL.thy index fb0b4bd..1fcedeb 100644 --- a/Isa_COL.thy +++ b/Isa_COL.thy @@ -29,7 +29,6 @@ doc_class side_by_side_figure = figure + caption2 :: "string" -ML\DOF_core.SPY;\ doc_class figure_group = (* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *) anchor :: "string" @@ -37,13 +36,22 @@ doc_class figure_group = rejects figure_group (* this forbids recursive figure-groups *) accepts "\figure\\<^sup>+" -ML\@{term "side_by_side_figure"}; -@{typ "doc_class rexp"}; -DOF_core.SPY; -\ + (* dito the future table *) (* dito the future monitor: table - block *) + + + + +section\Tests\ + +ML\@{term "side_by_side_figure"}; +@{typ "doc_class rexp"}; +DOF_core.SPY; +\ + + end diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 3c27e19..e632baf 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -122,7 +122,7 @@ struct type ISA_transformer_tab = (theory -> term * typ * Position.T -> term option) Symtab.table val initial_ISA_tab:ISA_transformer_tab = Symtab.empty - type docclass_inv_tab = (string -> Context.generic -> bool) Symtab.table + type docclass_inv_tab = (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty type open_monitor_info = {accepted_cids : string list, @@ -285,7 +285,7 @@ fun update_class_invariant cid_long f thy = let val _ = if is_defined_cid_global' cid_long thy then () else error("undefined class id : " ^cid_long) in map_data_global (upd_docclass_inv_tab (Symtab.update (cid_long, - (fn ctxt => ((writeln("Inv check of :" ^cid_long); f ctxt )))))) + (fn ctxt => ((writeln("Inv check of : " ^cid_long); f ctxt )))))) thy end @@ -294,7 +294,7 @@ fun get_class_invariant cid_long thy = else error("undefined class id : " ^cid_long) val {docclass_inv_tab, ...} = get_data_global thy in case Symtab.lookup docclass_inv_tab cid_long of - NONE => K(K true) + NONE => K(K(K true)) | SOME f => f end @@ -1008,7 +1008,8 @@ fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy = fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults - val check_inv = (DOF_core.get_class_invariant cid_long thy oid) o Context.Theory + val check_inv = (DOF_core.get_class_invariant cid_long thy oid {is_monitor=is_monitor}) + o Context.Theory in thy |> DOF_core.define_object_global (oid, {pos = pos, thy_name = Context.theory_name thy, value = value_term, @@ -1040,20 +1041,26 @@ fun update_instance_command (((oid:string,pos),cid_pos), Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs val def_trans = #1 o (calc_update_term thy cid_long assns') - val check_inv = (DOF_core.get_class_invariant cid_long thy oid) o Context.Theory + val check_inv = (DOF_core.get_class_invariant cid_long thy oid {is_monitor=false}) + o Context.Theory in thy |> DOF_core.update_value_global oid (def_trans) |> (fn thy => (check_inv thy; thy)) end -fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta_args_t, +fun enriched_document_command markdown level (((((oid,pos),cid_pos), doc_attrs) : meta_args_t, xstring_opt:(xstring * Position.T) option), toks:Input.source) : Toplevel.transition -> Toplevel.transition = let - fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy) (* as side-effect, generates markup *) + fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy) + (* generating the level-attribute syntax *) + val doc_attrs' = case level of + NONE => doc_attrs + | SOME(NONE) => (("level",@{here}),"None")::doc_attrs + | SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::doc_attrs in Toplevel.theory(create_and_check_docitem false oid pos cid_pos doc_attrs #> check_text) (* Thanks Frederic Tuong! ! ! *) @@ -1091,7 +1098,8 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos), | NONE => error ("Not belonging to a monitor class: "^oid) val delete_monitor_entry = DOF_core.map_data_global (DOF_core.upd_monitor_tabs (Symtab.delete oid)) val {cid=cid_long, ...} = the(DOF_core.get_object_global oid thy) - val check_inv = (DOF_core.get_class_invariant cid_long thy oid) o Context.Theory + val check_inv = (DOF_core.get_class_invariant cid_long thy oid) {is_monitor=true} + o Context.Theory in thy |> update_instance_command args |> (fn thy => (check_inv thy; thy)) |> delete_monitor_entry @@ -1101,59 +1109,59 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos), val _ = Outer_Syntax.command ("title*", @{here}) "section heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = false} NONE) ; val _ = Outer_Syntax.command ("subtitle*", @{here}) "section heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = false} NONE); val _ = Outer_Syntax.command ("chapter*", @{here}) "section heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = false} (SOME(SOME 0))); val _ = Outer_Syntax.command ("section*", @{here}) "section heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = false} (SOME(SOME 1))); val _ = Outer_Syntax.command ("subsection*", @{here}) "subsection heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = false} (SOME(SOME 2))); val _ = Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = false} (SOME(SOME 3))); val _ = Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = false} (SOME(SOME 4))); val _ = Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = false} (SOME(SOME 5))); val _ = Outer_Syntax.command ("figure*", @{here}) "figure" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = false} NONE); val _ = Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> enriched_document_command {markdown = false}); + >> enriched_document_command {markdown = false} NONE); val _ = Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)" (attributes -- Parse.opt_target -- Parse.document_source - >> enriched_document_command {markdown = true}); + >> enriched_document_command {markdown = true} (SOME NONE)); val _ = Outer_Syntax.command @{command_keyword "declare_reference*"} @@ -1537,6 +1545,4 @@ writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []); \ *) - - end diff --git a/examples/conceptual/Concept_ExampleInvariant.thy b/examples/conceptual/Concept_ExampleInvariant.thy index aca91fc..0a7bcaa 100644 --- a/examples/conceptual/Concept_ExampleInvariant.thy +++ b/examples/conceptual/Concept_ExampleInvariant.thy @@ -91,7 +91,7 @@ text*[c2::C, x = "''delta''"] \ ... in ut tortor eleifend augue pretium co section*[f::E] \ Lectus accumsan velit ultrices, ... }\ -(* test : close_monitor should fail : * +(* test : close_monitor should fail : section*[f2::E] \ Lectus accumsan velit ultrices, ... }\ *) ML\val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here}; diff --git a/examples/math_exam/BAC2017/BAC2017.thy b/examples/math_exam/BAC2017/BAC2017.thy index d6b0652..a4eebb5 100644 --- a/examples/math_exam/BAC2017/BAC2017.thy +++ b/examples/math_exam/BAC2017/BAC2017.thy @@ -86,7 +86,7 @@ lemma q2_b : "0 \ x \ x \ y \ y \ 1 \ h x lemma q2_c : "1 \ x \ x \ y \ h x \ h y" sorry -text*[v2::Validation, proofs="[@{thm ''q2_b''}, @{thm ''q2_c''}]"] +text*[v2::Validation, proofs="[@{thm ''BAC2017.q2_b''}, @{thm ''BAC2017.q2_c''}]"] {* See lemmas @{thm q2_b} and @{thm q2_c}. *} diff --git a/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy b/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy index ac89011..8424264 100644 --- a/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy @@ -44,8 +44,8 @@ on top of Isabelle. \isadof allows for conventional typesetting for enforcing a certain document structure, and discuss ontology-specific IDE support. \ -section*[intro::introduction_title]\ Introduction \ -text*[introtext::introduction_elem]\ +section*[intro::introduction]\ Introduction \ +text*[introtext::introduction]\ The linking of the \<^emph>\formal\ to the \<^emph>\informal\ is perhaps the most pervasive challenge in the digitization of knowledge and its propagation. This challenge incites numerous research efforts @@ -94,7 +94,7 @@ declare_reference*[ontomod::text_section] declare_reference*[ontopide::text_section] declare_reference*[conclusion::text_section] (*>*) -text*[plan::introduction_elem]\ The plan of the paper is follows: we start by introducing the underlying +text*[plan::introduction]\ The plan of the paper is follows: we start by introducing the underlying Isabelel sytem (@{docitem (unchecked) \bgrnd\}) followed by presenting the essentials of \isadof and its ontology language (@{docitem (unchecked) \isadof\}). It follows @{docitem (unchecked) \ontomod\}, where we present three application @@ -104,7 +104,7 @@ conclusions and discuss related work in @{docitem_ref (unchecked) \conclu section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"] \ Background: The Isabelle System \ -text*[background::introduction_elem]\ +text*[background::introduction]\ While Isabelle is widely perceived as an interactive theorem prover for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we would like to emphasize the view that Isabelle is far more than that: @@ -133,7 +133,7 @@ figure*[architecture::figure,relative_width="100",src="''figures/isabelle-archit asynchronous communication between the Isabelle system and the IDE (right-hand side). \ -text*[blug::introduction_elem]\ The Isabelle system architecture shown in @{docitem_ref \architecture\} +text*[blug::introduction]\ The Isabelle system architecture shown in @{docitem_ref \architecture\} comes with many layers, with Standard ML (SML) at the bottom layer as implementation language. The architecture actually foresees a \<^emph>\Nano-Kernel\ (our terminology) which resides in the SML structure \texttt{Context}. This structure provides a kind of container called From 9c8d57e573ef976f88de5ee4d1ee5d3833d9bca5 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 4 Dec 2018 14:28:59 +0100 Subject: [PATCH 12/13] Continuous checking of class invariants of enabled monitors. Regression test suite revised. --- Isa_DOF.thy | 14 ++- .../conceptual/Concept_ExampleInvariant.thy | 9 +- test/cenelec/Example.thy | 3 +- test/conceptual/Attributes.thy | 34 +++--- test/conceptual/Concept_ExampleInvariant.thy | 109 ++++++++++++++++++ test/simple/Example.thy | 3 +- 6 files changed, 142 insertions(+), 30 deletions(-) create mode 100644 test/conceptual/Concept_ExampleInvariant.thy diff --git a/Isa_DOF.thy b/Isa_DOF.thy index e632baf..eed052e 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -956,7 +956,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy = along the super-class id. The evaluation is in parallel, simulating a product semantics without expanding the subclass relationship. *) fun is_enabled_for_cid moid = - let val {accepted_cids, rejected_cids, automatas} = + let val {accepted_cids, automatas, ...} = the(Symtab.lookup monitor_tab moid) val indexS= 1 upto (length automatas) val indexed_autoS = automatas ~~ indexS @@ -981,16 +981,22 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy = val _ = if null enabled_monitors then () else writeln "registrating in monitors ..." val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors; (* check that any transition is possible : *) + fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false} + fun class_inv_checks ctxt = map (fn x => inst_class_inv x ctxt) enabled_monitors val delta_autoS = map is_enabled_for_cid enabled_monitors; fun update_info (n, aS) (tab: DOF_core.monitor_tab) = - let val {accepted_cids,rejected_cids,automatas} = the(Symtab.lookup tab n) + let val {accepted_cids,rejected_cids,...} = the(Symtab.lookup tab n) in Symtab.update(n, {accepted_cids=accepted_cids, rejected_cids=rejected_cids, automatas=aS}) tab end fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans mon_oid) val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) - in thy |> fold (update_trace) (enabled_monitors) - |> DOF_core.map_data_global(update_automatons) + in thy |> (* update traces of all enabled monitors *) + fold (update_trace) (enabled_monitors) + |> (* check class invariants of enabled monitors *) + (fn thy => (class_inv_checks (Context.Theory thy); thy)) + |> (* update the automata of enabled monitors *) + DOF_core.map_data_global(update_automatons) end diff --git a/examples/conceptual/Concept_ExampleInvariant.thy b/examples/conceptual/Concept_ExampleInvariant.thy index 0a7bcaa..114318e 100644 --- a/examples/conceptual/Concept_ExampleInvariant.thy +++ b/examples/conceptual/Concept_ExampleInvariant.thy @@ -36,13 +36,11 @@ ML\fun check_A_invariant oid {is_monitor:bool} ctxt = setup\DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\ -(* test : should fail : *) -subsection*[c::A, x = "6"] \ Lorem ipsum dolor sit amet, ... \ -subsection*[d::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ +subsection*[d::A, x = "4"] \ Lorem ipsum dolor sit amet, ... \ -(* test : update should fail : *) +(* test : update should not fail, invariant still valid *) update_instance*[d::A, x += "1"] @@ -63,7 +61,7 @@ that instances of class C occur more often as those of class D; note that this i to take sub-classing into account: \ -ML\fun check_M_invariant oid {is_monitor} ctxt = +ML\fun check_M_invariant oid {is_monitor} ctxt = let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here} fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) val string_pair_list = map conv (HOLogic.dest_list term) @@ -94,6 +92,7 @@ section*[f::E] \ Lectus accumsan velit ultrices, ... }\ Lectus accumsan velit ultrices, ... }\ *) + ML\val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here}; fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) val string_pair_list = map conv (HOLogic.dest_list term) diff --git a/test/cenelec/Example.thy b/test/cenelec/Example.thy index bdadced..7efa37e 100644 --- a/test/cenelec/Example.thy +++ b/test/cenelec/Example.thy @@ -97,8 +97,7 @@ text{* @{test_specification \ass122\} -- wrong: "reference ontologi text{* Here is a reference to @{docref \sedf\} *} -(* works currently only in connection with the above label-hack. - Try to hover over the sedf - link and activate it !!! *) +(* shouldn't work: label exists, but definition was finally rejected to to errors. *) section \Miscellaneous\ diff --git a/test/conceptual/Attributes.thy b/test/conceptual/Attributes.thy index 1d46c1d..3a9e917 100644 --- a/test/conceptual/Attributes.thy +++ b/test/conceptual/Attributes.thy @@ -10,10 +10,11 @@ print_doc_items (* corresponds to low-level accesses : *) ML\ -val ({tab = x, ...},y,_)= DOF_core.get_data @{context}; -Symtab.dest x; +val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...} + = DOF_core.get_data @{context}; +Symtab.dest docitem_tab; "=============================================="; -Symtab.dest y; +Symtab.dest docclass_tab; \ text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\ sdfsdfs sdfsdf sdfsdf @{thm refl} \ @@ -63,34 +64,34 @@ text\A not too trivial test: default y -> []. The latter wins at access time. Then @{term "t"}: creation of a multi inheritance object omega, triple updates, the last one wins.\ -ML\val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg}); - val t = HOLogic.dest_string (@{docitem_attr x::omega}); \ +ML\val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::dfgdfg}); + val t = HOLogic.dest_string (@{docitem_attribute x::omega}); \ section\Mutation of Attibutes in DocItems\ -ML\ val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attr a2::omega} \ +ML\ val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attribute a2::omega} \ update_instance*[omega::E, a2+="1"] -ML\ val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attr a2::omega} \ +ML\ val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attribute a2::omega} \ update_instance*[omega::E, a2+="6"] -ML\ @{docitem_attr a2::omega} \ -ML\ HOLogic.dest_number @{docitem_attr a2::omega} \ +ML\ @{docitem_attribute a2::omega} \ +ML\ HOLogic.dest_number @{docitem_attribute a2::omega} \ update_instance*[omega::E, x+="''inition''"] -ML\ val s = HOLogic.dest_string ( @{docitem_attr x::omega}) \ +ML\ val s = HOLogic.dest_string ( @{docitem_attribute x::omega}) \ update_instance*[omega::E, y+="[''defini'',''tion'']"] update_instance*[omega::E, y+="[''en'']"] -ML\ val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::omega}); \ +ML\ val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::omega}); \ section\Simulation of a Monitor\ @@ -98,19 +99,18 @@ open_monitor*[figs1::figure_group, anchor="''fig-demo''", caption="''Sample ''"] -figure*[fig_A::figure, spawn_columns=False,relative_width="''90''", +figure*[fig_A::figure, spawn_columns=False,relative_width="90", src="''figures/A.png''"] \ The A train \ldots \ -update_instance*[figs1::figure_group, trace+="[figure]"](* simulation : will disappear *) -figure*[fig_B::figure, spawn_columns=False,relative_width="''90''", +figure*[fig_B::figure, spawn_columns=False,relative_width="90", src="''figures/B.png''"] \ The B train \ldots \ -update_instance*[figs1::figure_group, trace+="[figure]"](* simulation : will disappear *) -close_monitor*[fig1] +close_monitor*[figs1] -ML\ map (fn Const(s,_) => s) (HOLogic.dest_list @{docitem_attr trace::figs1}) \ +text\Resulting trace in figs1: \ +ML\@{trace_attribute figs1}\ print_doc_items diff --git a/test/conceptual/Concept_ExampleInvariant.thy b/test/conceptual/Concept_ExampleInvariant.thy new file mode 100644 index 0000000..1650d01 --- /dev/null +++ b/test/conceptual/Concept_ExampleInvariant.thy @@ -0,0 +1,109 @@ +chapter\Setting and modifying attributes of doc-items\ + +theory Concept_ExampleInvariant + imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *) +begin + +section\Example: Standard Class Invariant\ + +text\Status:\ +print_doc_classes +print_doc_items + + +text\Watch out: The current programming interface to document class invariants is pretty low-level: +\<^item> No inheritance principle +\<^item> No high-level notation in HOL +\<^item> Typing on ML level is assumed to be correct. +The implementor of an ontology must know what he does ... +\ + +text\Setting a sample invariant, which simply produces some side-effect:\ +setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => + fn {is_monitor = b} => + fn ctxt => + (writeln ("sample echo : "^oid); true))\ + +subsection*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ + + +text\Setting a sample invariant, referring to attribute value "x":\ +ML\fun check_A_invariant oid {is_monitor:bool} ctxt = + let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here} + val (@{typ "int"},x_value) = HOLogic.dest_number term + in if x_value > 5 then error("class A invariant violation") else true end +\ + +setup\DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\ + +(* test : should fail : *) +subsection*[c::A, x = "6"] \ Lorem ipsum dolor sit amet, ... \ + + +subsection*[d::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ + +(* test : update should fail : *) +update_instance*[d::A, x += "1"] + + +section\Example: Monitor Class Invariant\ + +text\Of particular interest are class invariants attached to monitor classes: since the +latter manage a trace-attribute, a class invariant on them can assure a global form of consistency. +It is possible to express: +\<^item> that attributes of a document element must satisfy particular conditions depending on the + prior document elements --- as long they have been observed in a monitor. +\<^item> non-regular properties on a trace not expressible in a regular expression + (like balanced ness of opening and closing text elements) +\<^item> etc. +\ + +text\A simple global trace-invariant is expressed in the following: it requires +that instances of class C occur more often as those of class D; note that this is meant +to take sub-classing into account: +\ + +ML\fun check_M_invariant oid {is_monitor} ctxt = + let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here} + fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) + val string_pair_list = map conv (HOLogic.dest_list term) + val cid_list = map fst string_pair_list + val ctxt' = Proof_Context.init_global(Context.theory_of ctxt) + fun is_C x = DOF_core.is_subclass ctxt' x "Conceptual.C" + fun is_D x = DOF_core.is_subclass ctxt' x "Conceptual.D" + val n = length (filter is_C cid_list) + val m = length (filter is_D cid_list) + in if m > n then error("class M invariant violation") else true end +\ + +setup\DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\ + +open_monitor*[struct::M] + + +section*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ + +text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ + +text*[d1::E, a1 = "X3"] \ ... phasellus amet id massa nunc, pede suscipit repellendus, ... \ + +text*[c2::C, x = "''delta''"] \ ... in ut tortor eleifend augue pretium consectetuer... \ + +section*[f::E] \ Lectus accumsan velit ultrices, ... }\ + +(* test : close_monitor should fail : *) +section*[f2::E] \ Lectus accumsan velit ultrices, ... }\ + +ML\val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here}; + fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) + val string_pair_list = map conv (HOLogic.dest_list term) + \ +(* trace example *) +text\Setting a sample invariant, referring to attribute value "x":\ + + +close_monitor*[struct] + + +end + \ No newline at end of file diff --git a/test/simple/Example.thy b/test/simple/Example.thy index 963d5e2..583bb5e 100644 --- a/test/simple/Example.thy +++ b/test/simple/Example.thy @@ -95,8 +95,7 @@ section*[sedf::requirement, long_name = "None::string option"] jump to its definition. *} text\\label{sedf}\ (* Hack to make the LaTeX-ing running. Should disappear. *) -section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting, -but wrong doc_class constraint. *} +section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with undefined attributes. *} section{* Text Antiquotation Infrastructure ... *} From a5f9442c6ea7d4ed9fb38652a6ff8a87c3acc425 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 4 Dec 2018 15:04:50 +0100 Subject: [PATCH 13/13] Added global command: check_doc_global (* checking unresolved forward references for the moment *) --- Isa_DOF.thy | 23 +++++++++++++++++++---- examples/simple/Concept_Example.thy | 2 +- ontologies/Conceptual.thy | 24 ++++++++++++------------ test/cenelec/Example.thy | 1 + test/conceptual/Attributes.thy | 2 ++ 5 files changed, 35 insertions(+), 17 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index eed052e..3645256 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -22,10 +22,10 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) keywords "+=" ":=" "accepts" "rejects" - and "title*" "subtitle*" - "chapter*" "section*" "subsection*" "subsubsection*" - "text*" + and "title*" "subtitle*" + "chapter*" "section*" "subsection*" "subsubsection*" "paragraph*" "subparagraph*" + "text*" "figure*" "side_by_side_figure*" :: document_body @@ -35,7 +35,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) and "lemma*" "theorem*" "assert*" ::thy_decl - and "print_doc_classes" "print_doc_items" "gen_sty_template" :: diag + and "print_doc_classes" "print_doc_items" "gen_sty_template" "check_doc_global" :: diag begin @@ -563,6 +563,14 @@ fun print_doc_classes b ctxt = writeln "=====================================\n\n\n" end; +fun check_doc_global (strict_checking : bool) ctxt = + let val {docobj_tab={tab = x, ...}, ...} = get_data ctxt; + val S = map_filter (fn (s,NONE) => SOME s | _ => NONE) (Symtab.dest x) + in if null S + then () + else error("Global consistency error - Unresolved forward references: "^ String.concatWith "," S) + end + val _ = Outer_Syntax.command @{command_keyword print_doc_classes} "print document classes" @@ -575,6 +583,13 @@ val _ = (Parse.opt_bang >> (fn b => Toplevel.keep (print_doc_items b o Toplevel.context_of))); +val _ = + Outer_Syntax.command @{command_keyword check_doc_global} + "check global document consistency" + (Parse.opt_bang >> (fn b => + Toplevel.keep (check_doc_global b o Toplevel.context_of))); + + fun toStringLaTeXNewKeyCommand env long_name = "\\expandafter\\newkeycommand\\csname"^" "^"isaDof."^env^"."^long_name^"\\endcsname%\n" diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy index d8c3cdb..1f468b6 100644 --- a/examples/simple/Concept_Example.thy +++ b/examples/simple/Concept_Example.thy @@ -44,7 +44,7 @@ ML\@{trace_attribute struct}\ print_doc_classes print_doc_items - +check_doc_global end \ No newline at end of file diff --git a/ontologies/Conceptual.thy b/ontologies/Conceptual.thy index 0cbcc64..5a9237c 100644 --- a/ontologies/Conceptual.thy +++ b/ontologies/Conceptual.thy @@ -6,14 +6,14 @@ doc_class A = x :: int doc_class B = - x :: "string" (* attributes live in their own name-space *) - y :: "string list" <= "[]" (* and can have arbitrary type constructors *) - (* LaTeX may have problems with this, though *) - -doc_class C = B + - z :: "A option" <= None (* A LINK, i.e. an attribute that has a type - referring to a document class. Mathematical - relations over document items can be modeled. *) + x :: "string" (* attributes live in their own name-space *) + y :: "string list" <= "[]" (* and can have arbitrary type constructors *) + (* LaTeX may have problems with this, though *) + +doc_class C = B + + z :: "A option" <= None (* A LINK, i.e. an attribute that has a type + referring to a document class. Mathematical + relations over document items can be modeled. *) g :: "thm" datatype enum = X1 | X2 | X3 @@ -26,15 +26,15 @@ doc_class D = B + a2 :: int <= 0 doc_class E = D + - x :: "string" <= "''qed''" (* overriding default *) + x :: "string" <= "''qed''" (* overriding default *) doc_class F = r :: "thm list" u :: "file" s :: "typ list" - b :: "(A \ C) set" <= "{}" (* This is a relation link, roughly corresponding - to an association class. It can be used to track - claims to result - relations, for example.*) + b :: "(A \ C) set" <= "{}" (* This is a relation link, roughly corresponding + to an association class. It can be used to track + claims to result - relations, for example.*) doc_class G = C + g :: "thm" <= "@{thm ''HOL.refl''}" diff --git a/test/cenelec/Example.thy b/test/cenelec/Example.thy index 7efa37e..d91134d 100644 --- a/test/cenelec/Example.thy +++ b/test/cenelec/Example.thy @@ -99,6 +99,7 @@ text{* @{test_specification \ass122\} -- wrong: "reference ontologi text{* Here is a reference to @{docref \sedf\} *} (* shouldn't work: label exists, but definition was finally rejected to to errors. *) +check_doc_global (* shoudn't work : Unresolved forward references: lalala,blablabla *) section \Miscellaneous\ diff --git a/test/conceptual/Attributes.thy b/test/conceptual/Attributes.thy index 3a9e917..273ea96 100644 --- a/test/conceptual/Attributes.thy +++ b/test/conceptual/Attributes.thy @@ -114,4 +114,6 @@ ML\@{trace_attribute figs1}\ print_doc_items +check_doc_global + end \ No newline at end of file