From 13d18f963d7342cfeddf17f3ae222ff1b14404a8 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 16 Jun 2004 09:39:15 +0000 Subject: [PATCH] first moogle commit --- helm/searchEngine/html/moogle.html | 78 +-- helm/searchEngine/html/moogle.png | Bin 0 -> 16808 bytes helm/searchEngine/html/moogle_chat.html | 19 + helm/searchEngine/html/moogle_chat1.html | 83 +++ helm/searchEngine/html/moogle_chat2.html | 22 + .../html/moogle_constraints_choice.html | 90 +++ helm/searchEngine/html/moogle_help.html | 85 +++ helm/searchEngine/html/moogle_init.html | 52 ++ helm/searchEngine/html/moogle_small.png | Bin 0 -> 7599 bytes helm/searchEngine/searchEngine.ml | 654 +++++++++++------- 10 files changed, 770 insertions(+), 313 deletions(-) create mode 100644 helm/searchEngine/html/moogle.png create mode 100644 helm/searchEngine/html/moogle_chat.html create mode 100644 helm/searchEngine/html/moogle_chat1.html create mode 100644 helm/searchEngine/html/moogle_chat2.html create mode 100644 helm/searchEngine/html/moogle_constraints_choice.html create mode 100644 helm/searchEngine/html/moogle_help.html create mode 100644 helm/searchEngine/html/moogle_init.html create mode 100644 helm/searchEngine/html/moogle_small.png diff --git a/helm/searchEngine/html/moogle.html b/helm/searchEngine/html/moogle.html index 298193f44..f608b9d28 100644 --- a/helm/searchEngine/html/moogle.html +++ b/helm/searchEngine/html/moogle.html @@ -4,65 +4,53 @@ Moogle -
- - - -
matita
-
-
- - - - - - - - - - - - - - - - - - - - - + + + + - + + + - + + - + + + + + +
moogle   - -
- - - - + 		+ + + + + +     - Advanced search
- Preferences + Help
+ Input Syntax
+
- - - - + + + +
- -
+ +
+ @RESULTS@ + diff --git a/helm/searchEngine/html/moogle.png b/helm/searchEngine/html/moogle.png new file mode 100644 index 0000000000000000000000000000000000000000..07570d07a9f9771b3afbcc59b4d551e928e5b14a GIT binary patch literal 16808 zcmXt=b97u^w8!tnw$WG(8{4+osIhIcaT+(a)1NIuE}wOJWf5t#a=oiBxK}Jx+%l}Co3bXs zllj0!3qz69>Oq0fasNU?UlnNGMqO7d+!>^;A_}473it25MUumfkV`8&2K_*T7&c93 zsHdvGwauRa_bD>=iuO26G%#zVF4Xb=Dy$F-m2#cx^+!HETNjLaE`?-T@l0! z5wEr^E$+WBCSCkwZo1v&14y4_NBrJC0v0AidVxNcL9@g$20ZgY8|0Ah4X{_Oh=Brq z#Kf?CfRU#bM1Wg=1%0>A`$J~tw?U_h)zh^M;+p=cvL>&~;u?}i&i9t8CbO=^U{4@W zU~0N95Be%l+H*4_7tXfGbP;+8GlwWGmghcQ8ogN6N;lx*=E;ChHS;PN*z{C6JMF0j z|H@j;X@}>LgoRA09cR-P#b@cq@VF3SX~bR9hpFwjq zDDQMW)x5D#?y75MN&iq#9JHzB5!Pz-V~2ayonf>K=SN=nTRfu`u-H0En+YS>I}8Ya z1oChVyzO_j0zErbiwoA8^(HWdri(ycX>@a?ho>7QF8p|J@k79~pl?0HXegS5N*p4O zBXC&>iwfDZiU$iQ#6khQ?U0C>17{uYAQ#KUQ>7_~Ri5isy$qeyJ#G;+?zkP#9Oe|+ zmXEmM-|~m&U%paqvO7Ms&jLVu(e{fW^pLqI!=P?f&ovP$5kS=UG!|EgW{t%lTi;L= z9ux$Q`4GIBgB&HsUn%L($7p}ip{oXbgQu6e&X>EK_w5P&f%*U?3QF*=IyP?>D&aV^ z2_gd!%rL?J-5aO?|Kv)OU)5ihQIO(*Uw^bDE@W;i4-{}Rp@G8zn&-GgkJhdl4&FTo z%7pHV4E_#Lh9yjNIviu%Qw;t3CAX9m0z`fpEKd2GR(kg_u(#Bg)y`njZQ@?+xi5^{i#VCy$J>A$(nvZ-caqGal`@$>J5vN-PNteVw7z(-|) z6B3r@W^*S9q#~T=$F3W*T%o_tf~nHhpP`}2(b0iGv~So7IXeua8GGL`t;cZn?uDiH zP8@J?v92Xlh*sW0hX!NuM;PWRnN)my=DY0^Rh+J^sk!}M9HrKfgB-;{K*C)u!>AL{ zXx(5Gk^3pTZpM6ed){XZVACa69{(vXK}nWesazaxOD7c~kTh{g!6O)%932`6>_KCw zv|D0Z1z)WFcV)bS@qtK2bm(DdqLkn2IU&ccK#(JMs^ye$SypwFq&0lF?`^}9qId+H zqwo7m2Pf5?Z3{Pc60_`nf+Pk9hl3OPFoD6|x>Ok8Q6dR&J+J4H%1*G0i)zCF+UvFW zar3_BgVUrz1nMZG4cyf7^mgH@iXo0egHJ%nEh>Ho) zdrjqDM*{#L73FLc&}gKnS}SK0cE(oo0v$qh3>d5(E`mP8~GGQdjNge&WbIo)X z%z?mGrvsiHHJ~SaC|Yj^_#sICUNQMJW3=5OmQng z0tvN}cXH(DLJ88Oct0ZkUT2-?W)ss)81X;bP_aR2M;G$~XrK-vXQG}S7NpNS45PA% zlyIWlL`+VmjfpQaU?92xq$!f0(2X{eh? z(%eJ{&u^eeG;$e#ae^AIGO&7oO-K^@H%2%wREyPAIZiaNF}2Tln9x9*I}K6H1(%K9&guU?gNM zvUvmt^;S|a8gS37a--BqqaYO-tP*hDW+gDIQq&xP#x3y_erKKw&$b5ifRotG0*X8e zB=AGr|I}uzEnd+vH<2f`K+BvhBBqd8MV8oR>n{k>+pS|K>dsfg{J+T~A-9yoz4l@+ zWE{-^@gPwl#tSAK3yOnp_XR`BOo_quipsrXYnmi%2xbW3;m_le*ou~!A_!i{mNnxn zFnG>cVkKP_ycnZF^hKb}Z8tA16A`PkXYJ`2rd{NaV@t_Nc?Ho~uNOrGfXjdAvn~!f zsBqIPB!zs>&?FUK@ic+XyaVQzJ3K9T$6s)Iu87s#h}-5(VrNF;>)?mWWONx_KEA+C zVBdtkJGU8a%jdRudY$D%~_ zh@DKF3rSw%k5NB5adwkk8iVNx}6>1K)Wu> zSFx-0E5+tpPpmTvmjVk~WKa}VC;h)0R6zu>K68D>g$o(pzm~TnW}6w)1+?&gl3B~} z!|8C&q;jS2P=C71_`Oh#$2#e2++_7!2yChow8HQ1%oPFnlSuD$jCvLEf=@K&qb^4w z#K-GvTNxR*5q+Lp83eFa9C!bQNcGf645n0hy^ebN7dSb%I?cDDtNyv5Can`~=bYOt zfbxtJx@+_tw0AFT76@^kK)`LO$af3?sV7cA$iRE6_#5f7T1gcmPa_2)cS~?GW2S~cf!!j>Y0>_!GnSLl*NgI^d`Z@ z7PmY#>}O0Y(z9o|k@XlZKbCZuK=gS|=Qy1#5)n=t*g$4K$D3!i1y-CLI1`k^hB3gt zg5|gWy@1;aHI{`8V^W+r2jV8^Q0anRgzL5N{@bQL&r94vkI+yyf zw3+oxLOR*J#p^TfQmhgwl6$Nv#B|yFQDz2i4ch@zm9bn#JXS-|4}$g14~O^Mk7_Sd zC`o7}!S}287cKs`#S0MBo5AD8dSH4Y*0gUhj~JpgsBd!Y(B>ypkwkc}8pY?(Q?c=Ceo%wDOLPY)p! z$dfewOtys}A`YR3S9HYm(9C7Xc~N+wx3Y>wkA-0JG79xaB(r9+k~-yrt7hEsZ^ch_ zlDBCOm1?&oh(NT+{>}Z9ll^fRicT?L=Vy)ZeI`A^d|61Vi zSbzrWch-g&QfyJBWeN?%1S`-rGQd5$fV!*3^h@tQh7sY_a{+L?>xt|kTNvw0JYcYl zSKQaXae^1i}LKK#Rt4qM@E@no%CLo3BvH@OHK+EMFD3~hl3z5 zM5Q)Mvx_eOyWQ5C`@2fulH@|jZ9K}H!;bP96Ud`Qzyg{5wp&3i4v+ltpS(gJPOuA~ zCaj2EpSo|2wfT5+x#BV;_`%&b<>C!5D`~7F(q;6vKDzGnSY5OD;+_`p;Me|8BLwMx z=XrBvL4uEDpJhB3MgRd!3St?spizJMC4>M~W9%6ou@U ziy#9=<@V@8a(7v0kbx2lepMGSZ0%hSXO5roQ^d?pS}rPF<{bh8#x*W7K^P4=D}B!k zDq|EF$IOSZ3+NP;)G!*n8Ld{zec4EX%(~sY@PzIjt4$sK?oXiF+V+s3xF^@QiIP;R z**fwj4_3lv6#iFKWT0%>f1)6NMX>IESK#mZBn7 zd+VhW(Ul^N*UXCu-Be514A|Mg$_HO(irnG*qyvbWHF{CKtGtLJ`z5nyyYM zmfAlSI`aqi7OFl*^b>Q7=6c0z&h-U=viN>g!w#3-Ad)^c)Ga@GYm~da#NoFEeH0~o z#+~nU{rLRHNsm{kR@L!twrRq<;9A;Mz-BkveE9S3O>0%$^x-gacy>Dyd$yAOF#Es_ zo&f-?n4Xx7h*!_EI;hTbL%xmsjinv{d1B+F82>(Qw=$O7nwpvtw#Yb&aT+MA3CMf@ z6u^}v*ZW;>bF}Jp{fHA!(uL8Ql8|6ZKYdYZP0y zon(GAzjb|Ip81X$SzX;V(bcsssG)&uJ;kqJG1Jha9Ku@mjcD2&tt2osHvTck_wWA& z`E5jBnH8f`f4HdLm39pvwRkBL@ft1t`nEM8SL5VR@F0ldzw4YaUnWvYU~xHs$xVU? zoPT1RrN);Qcx!&LUpL7AIcRxH`Qnu>h z55dLhd~<`vrF#ZK?U#_3a*^+CdSo*SW|W)n^>cR%dWIsXwLM17z+G-6#_@!A}Z4!7?-3QpKE zR+wj35Nl#DQ)ys`qf2(i2U^|}A2V^0zl4cAbo(@t2u!~$9C+|{O+!Ha#7M1x@5l=s zZt*=WBs4$K6o&wcU|=xl7qa|U0oV8)61afJV9Oxz60nfBm(-&^<#YV~^20=> z>MIjABcvOpDBMm`he)%PS5gdk`kMF;n23O^m$jEFe%CvX{CpfVxnLp*PLCRj1aIF0 z>(AJcsrfb&+U;+%T>a-A3olMiC>Yd0&lYND=gaV~@!0X|bZs{tyA>v}Kj-!~XT>Da zgh9K~xf%>;B;{H0;*^2jlzzHKd8U>bnns#5#*jS+=#VBE7{E3e*0~B+nEaG!f74m- z)|>z#@zUIE=0s_`eW!JLMR{Zp)MxX2Bfx_V9e!NxM`71D5U}pI)q%T=*tE%ju7*ds zWzL=*@H;`Li<>Q=*Y^R{Od>TxoYGmIAZV#+yy)dut{*Be1IuS%#RpzmvLEJ2j(PMo zW|QOegkR62sz@c2Wy?jZa%L)PzLWTMUTy%odEr?u~ z6CPQeM(@f2xCpX0DFco;?ln{ACw<0!|Cr)mpqD#7&MBDVvLUdN<-0^r= zvk3u8@px}jn@qa_yeM8}>x6!7m)Z*e~R;0w> zRw7Su6ej~oz+;jFzoC9#5;&A0Rg_RG^6BZ+5v@hSW46h5F|8*wt&l7$yWE@s$v}F} zc+Vqc&Uoj=@iA9l_)xxq&O*JVWc!|jGGjSmyVN}mEhJrxQA-J%Cfy^X3r!t9^_T){ z@9U03Z@r^_M}xbHfWovqZ-@u3x8Po8eQ$gY4wYM_{Ts09hcgjaMs7f{4y_7TRmVVyMcyRv&1Qv6EYcX+3v`DBB zV=u+82`Qe$*7&j=2AZbDt>sH3mo-AAPgw)mCb(F~puo^f&?a-uZW}B|KXWYPP3=%~ zz1@oK+VRRl_zWWl%T&Ky$cbRGA|E22k*utE0yd9F9#0`ODA%WXlcU? zQNP&9=bd@uZGPyIg@cxH#%d7>==l;>fDHtmtP2dsPjx zzsGRA7nqSTItpr%`*%|wwZ0#DCix!P8NtAwKI1WE?UY&a2WS)Gi07bT#P`bxmxqdk zX54%SR^OTu*@k-`I&DLFu-K9-yp;>GI=< zV(S@3Cn4oGRG~g4bp|+|vf7E*tzK7&j5L zK_%@m`TrvRP{oQ0Dn*KCF={Ylf;%QV2od7q)5?Z=%=FjY`b#ln5hGWdY@HSMM1+Vz zgg$>*7#65O)LW;oB(D;3!E+wAd#tisyF6PI@+_7UqT<}3Qg;El&O2GikepFnw%M|w>j$$p&Az3Xh6`Pt?t4%!bk`&L7|-Qr>6txTrl%RM1%v0H+pW+N zYwP8opV(R`zT(oa6rS@{rgo=Lxjo$Ce(C5Dw*F7JyJ<;n>!j|)O`Q~1a1AfkK^q4u zQYMot5W{9?i^Fl+W^QNq{0i*+xjSz`TNunpo+7(5dKSjgsmr0^LV+$j-veI^atx< z5Rc7v#dKk?Ly;0VwATTE;33S&AA#G_307C!a@%fEes_1^7C=#08BvtW4#Rix02&}r zq7%zd1`$whKSToH!o-+LmB{C*m(!4F!Zhv5qC(f!G!HgA4?Rc_olI$+A&#Z19oQXQ z3Z$n%5>VXRBSZeq)1R>m9a46u`1nPUD@rQU>{0f^ONlM=lJV~l+{^H_I_dV<55hHz zp)tq){kmOgM)~S)KdDbR*V*n7Ys!i3YkGIw?7!dUCgk7pRR7VLM|Sv&RkRi(7QMj8BO7 zdmtr3(}ogot@c2T>`Jp80%<^OmGy@LgQ@_nH%Ej-i5%Tp`1G{#auc;vr`qI`je+(0 z)i>XBQ7U=hO$b=-5%w$?EBeZbg(6dk43t(HV@3|~A1y!Jldf_am%VI8v*Sp?D^Mol z6(C|eUMWldhT-@|=`J4pM>1i&*3(aYP`(QtPDN>qtT=;RDbh4hA~075WTC?+;L>eU zQ;Ox>&v zUZtJV$Ph@FWiv2evlCcHWiYM(H zGiU>>ey3>GRxWrcKc&nUqT+}_+%ccV!gNZZ8_KE0;PNW_k_YbA7PshL||6%!OSw9Bxj;Ll6`nOOxsmV5!X z`P0X<>&LVP;7vwQ2D%Y2+ZL#s@kiw2vWd@tK-&vdzm=Rf0Bz4J4%bnZ(}s^=y7Ay) z^?FOo-{+$`VXQg<$>sX`QOiEy;NLx>kZ)SYzVDgiw=x%897QO|US)1|`h^KY7Q=Ea zYwHsTDZlx`;LImuh&juAMnNf3j>#j54nm&WFw0N?$6v~Y?k zaDq(O0Vl}d9)XWuwIx4i|Cx2tm9_w|pQxkxy8_@XjojKn*#36t`@OX>9y1_hU&dNmjO2Cg*9c zQNsofBdpu6f|?RGb*OlmI^4u%(5-%wSXIW8vz7X2{5aNZ^_-GNyPnH~NsykeG{!xr z^B*r(_dpJpW(bcX?MYpO7;@R}Rd)PXPa_QY2)y5=I7&dLVH6@Ts}9hb-F5@3Z3KYM z?NWHdzFvFC)CCaa$AIR7jQNBG1swAKbcb5z!{KytG5I=QWX}-5cHJ+p`2c$(sj@Af zbnpb0(?0SC0|mw23Kpku;mGGSYCD5mP(x;SEI3^AgFQR$j*F=--YVZb&ha1LBgA_` zOZrc$XgKRQ?ovin!80g_N&_LfN(ys+jrP#6;4NwQX)QSacYTid&sN+-R;*O_sOP_` zoTaKESixcP=BI2d2Uz{B>dh7Ho!F#;j1vuZK1UFNxHOKoSW?Kw(X9U(IE23!%J+zC z=@AC1bT0TP$??S26s078 zg7go<{al#E){L*6+Q@Jcd_&}17V}?K=FNGQM#&K1!ghnhInOn4Q<34(he*VX&@tpB ziq9x-a1@>#ET>5)@zntXxQyX(!R3a%ex;sEUd-^u!-p3yWZ^Fn!}*n%>CVd(U9NAq zzWsM7m9tm)<=?A}oG`}bVYvM6TWfP@dQH2`+B!PoThI)lRgP{+zY9^I&c8CX3O#55 zycEdu?od<6PY=UTnc05@0@u!VlILp&Jf(PAzL;w2298VY>{*al9&-=flUPUg^D=b~ z1YBp`MV=z!1{57Ns6k?IC60ZQWj)rXRfFdFyqOPO_-lFe+k6uIFdZx8%uf-YRQ1zWs9^)(je z>;!E56=x2KLp+*Y)|l@^D4&kCeXqZ%UzTiJ)Z6Ky@ZQ;TAk0?sa`r_@fR>aTKU8Gt z5-NCWY333TGz2XRc;=XR3!g>^2{SWxRQ8fdLF6mc401Ndj^tkik#nHYc4=eG<@0%= zSn@Z(ef{t+H|l6#*_K~uIK?~kO>eV6f$3g~Dl4$-0_MCs(|rEJ(+P2>XSWqHf^^x6 zS}Ej!5&ye9UFp*l>QG{#l^B(8_{aaV0Kt@>!0qk%n0shb8nO;ch^Hr5(k(}y@qWSSuYW6~-j6lshRZU6?1`|BFPlK2*fOX5{{5X7Zq{n8pCu;M z?N3!_Htbiu4y)-3Bhm;uj3m!t>KHb-J(vb9i+V|z&I`N6W@3*f*&rNYVp-Qa*8!ehLehPbR%@NZ)Hybd#Gu-T4%68g7oXIR!CFjv?*1tAz<6%S zhL?@u>g7$12UIqeX_`TG@yD2sP4&18#UzLZ+1>nXA`-ACDnt<4V;{>OB+<{zmvNr-5ig2sLxiR(?XuQe%&M+XoQ#p0?`4gH=!q^Ll6LSn zGc)7Mq%6wl&zdhhcf{CiMz}9-HpMap(}2-#w4~z7v~jzHotz?s!yG>F3L0kC5TbIr zUZn)!ps+8NQ)0IgK)pTFA#MLLJ?zA3)K&eCx;KN9>HNkZPqq%_hp|0@lj3Dxm`CGAwv; zl7nTW2F#3;$@EkL<9?@=nA0pO|%MeESc zeVAL;8~}11vI_KdV7XuvqYc^!CahLk{NnD@g3rbJw3G)M4;m#k55B@0GYU^>8qik9!dP*j@y;f zaJ|}oSz#l-qr!oa@LqEF3?YxwjmPH8dqmnwB$FRRv- zUM*1tnG^emBN-Zq9+DK6oZaT)EY3F9D%xd^S1}er^gisB%w<^P2KQ}C7=$?4S$qZg z7;|pE7^$6$J`WBq(DHFUNwGfa&Ly${5N+*u6d<7JT_HNSlFrD=??*}!5j zcvR_`)l-2lJ2nx+Ww8zf=AKy2!Bx0y)I z(B`>uU@I75v>tvoS*zN(Ti@PC3=;#@?xH?|^3*@?rMahi@uzXsmeGN8-jw>dQwLW3 zi0#iqE&l*vw5P1Iz8f~DtN_+dx3>sH$c%Fgn+Z|>yrXK5H!bIdpisj6$~r2BlX;ZK zrP=2QYa7^H5lY{y0k_C3B%oKAg*26=N-@G$J_^6?MzLZpL3v=Bn6KfjCNU7A@ae4O z#p1`hGedeWvDR0da%)Ks;zV#)=Dg#(7|qN!4hb{R1n<&^xaEk~hp1s?48C=OaP3Bw zQ?np)!mZ7!GB)n;;G|ZZqmA(#C}eAT(PIBu%%o?XVg8Nifv*}TIDM%kn3^!)pOcJl zqsZ}*)y2OFEUjtmL8N7f6z`E*_qr+vw^AcQh5w8%K8@~u_wcQKTTr@FkH5mdtsPIV zd94dzNtc8^a#{GbdRb1-l0r~V2*vZ6KIiK#KFJ8@vzD{A|9jQ^`eR9RBIVW8TSoQ7 zU+n;ebdcFot3@QH8=U_>$;oMARGRmJ*>}2P^L*_gLhZSIRB0e^E36{G|F0~UO0qP2 zbygG3l`^!VQnx9#1`Qm`tjN*N2Tl%_O&ocdG($Wjs4wvtvM>X!*b*Y$G}j@Se4)EN zMW{y4FxqSupN-(WlU4`V$|&fj>AxV_Ro$ZZG})1(lP_KbEYN}7qRD6wv(~D&*2|vZ z(Z`*dogFMMY&iSb?|W<5*LUc%RKvqXWB9dl!{^O{QDz=`GfO6n?W-0rH?f$6^>tkC z%P;S6)oFX(4*LQhS&!4h=anQRnpim;f5sl=VWdR@6AXpngB!1L%LhtWyfc{ysf?Ph zI5Nev<*v&%y!8xv^R77~Jyr8ObpexY%|0i{9jc+{i_^37FjUrf&oLaB6*d~#gpJV? zL;H0Fg=A>_%5s$74&Ezi+SI`UOYBWwxu5~)F|+VI89VM&#;x*>_7E)VIg{gRd8s+o8@C|OgnY`8_VOncXSg*gj%+-}!R0yd!V_$Q7pgCbS)Z*e# z6xRjoxjJ&p1ll_1zjF(8^K6dxK%|xDjb3e{DY>(B3?)(XjLkTbTjN)=;uT6k%^G}x zlI2u&c5Gnt)#bV^Xa26rhIglM<07}<=<7U~dZ4Pr3b-jA8y=-!Y1^F2^%SP(_RF#0 z4DN*e8Um`U1Q{LG^-o)NQbYhz{5ioq3@mWlDl#**{YZxFZ*Zy^aX=WQaqU8O!d+TwL8!UhH~)uHb4|(kkF{KW%-hoP&ya&ZQmOWH7|kvXb-} zOfSXv6s85>3PQKSC^9CJ9u%CrU`~<_hPD|EGo+)C_@94gNE40Arnl=&j~^&J4C%iz zE%bh`CS-l4+C@7`%lQNg8DBTY<5|PY@5l}#&-no1xjfm@02Jz+*xQ?X4MIxfETHAk ze@|;-4*=%^l5X$$wDms!Yx0*Q+$9GC_S@-t?~VG3*0ZIx83PQ97C z)gkb*<+O>?;*ylKb*wVc8Rf8RBgg<|g!s3#>iCg-*@;0udVzQ41&50rp7WnX#ey2f z{5))VUzv4Y!wwF$I`E3|8AMzR8j$wH*;CShlweR*ia6T+}D~6isnl5)le-7j7-WmDyM>vV%N6oY}2= z?_Sf)auus*_;!REAKCmo)b1!{^L=HelG~|WI^5VZ-}MUoj|eF+fIKpL&oJHtlg@On z+0RC0|G3~WUHAIA{5XjtHT(N|3Q@bC=iV45y`uL@>(KGT(GC4MZ)Ok;bhX=Tolb8F zv%?bmOnBkBN?M1>W(fW8zij@^7nnY5`qez6uV-YPzv0Y6Y42ft-`=fTMk-OLh)4Dr z{@iy2_0LuyTIsZ;=ldT|enBmi!JR7}7b5JyR7*YPjy9VzA(3fy7H9m0<%uG;bl335 ztZyn3?j0{`S@)rweNdxuT5-{d#4*5Q)Nm^bQ}}}(V$Z}DAr2Kik-1^%cZUd%c^QEJ31Z{r zeqErw_so?&r2`3btdIGd3G1nBc!O~DTj&_|*P3r;yD67Y49j)DMRcx8Wu1kkk?ws- zr&l;2artNd43r|P|M+KVlbYp~ezMZrRm+|G8F4fSFM>7-BYq;X|C^fv1epffx(|T zwE!^J2k{LB5FfaH2?0pK*xO&3KZqK0*b(x7kqV>Q8PKi9+icSH94frSzOq`a-A{{? zi#*a<#AM7p51`K5Wp+q&KeRu@uBnSgNLLhDI|B^p++_R##^vsP;%Owl?=gSDgaLtF zjNHq1T;r5oqgx0@XX4kFNENvlA?K9{m3;b1a96l!NR|O7dT<*Yf^miMXxv6H&N9f@ zu6#kwD$v-K4OB#cJ!6Gh-xtwl?p06KAe*V#xDNH`(;HyLxH*iPc!mQu`ci>wUp z!DhL{D_gFBZ{joGX!_3G^l5)2iWc%&u5`= zUo?5rTZ*>G-NLI$6as)c40Q3^GEG!wZR!??duxc zr$TX4*v|2Q2a#6Zt*$RrJNPbxT|!a}#qQ0{bKfal$K@{yzi`#WBWa@whN8&nuRQq; zO20P9>em-c2qg7-S+t~wX1;9NHLvP(XN~-|8AAFIs1)u&^#dObBSTS4L?|IbB(~y- zb;$XeN-Je;R#rMxP3H06uN7v2xBiQb>AUOb`LjOt+@-epmY2-`&R*m`FW!6jdV>A= zzU#JQhf2dmUfC*=jt>@}98PSEM3Wg)G}w1XEzli4wg zB_Zyw^VBql;$;hTF(CFBl>kQK@_(ZCw9wWNkxQns>wBtk2_JmCLhv< z%*Lf%HAnyjRVl0J>m9M;qxx_EKVzS6E)_Q}B|J~Dt)*PFHlFtD(@vJycZp25eY1Rv zj>`5IUm-jpB-$EUy^JgO1$vP(E8Bz&KJ<4|`)->a6vf26rG3zNKna_ykUT?cOlwXj zn=}*ol_wdxvJxwUUs7zOk!3wU=oVI+h);Kb>{E8)-HePMLSDZma8c0y_oWQ zTG7E3QeFQWGSc$F)s$m?pWhiT%{pU|LH{{|g*zI0vBm}flkWm=yOPK^@)wV~7{F`( zZw!?AxqnioJb1S^{D!UZ<;JCV+vNwRXG+SnZYG{v6>`KoWV&jGhFYbxvJ3_!2w_kn zWgT!ihc|^UFnsNZYu^v=vm1m&^lw6f<~+LQKK&|xcnLwo8H<-Jj4B8fGd9>n&zj3S zl5caMwA#xzaX1-L;+!Jp>##5Wg4%n%cR#<7TYKJd+L4q+RP#00>-Wa$T87tU>0)Wq zD9-OCyYblOMh2bv+4+5#%z{Kxt})c_f3!JR6T}A#f_t}m`zrj)Y`VdUNaoo}Lz=;% zR;-c}2q1>X5H-zoQv}U>pTnORdQ6`7p7)m;UamhO?xUh0spn3raPu;bTH6tJ9oZxE z4{D^$mMDLKSL%62mrTmpKG=Z9iT=3i4dFKGVv{oO!s;rk z^r3ymIS2GdVFd2@7$deN_v& zg&X4$s}VSYeF|E|?E&%eW~m+(_wQWUwFvCL?3CRODCk-5<+4Y7OISJiSsV`>P(Z>| z7+K6I=iVpfLAib>0{K&>y~X+Y`PlKf2Jj(HX#`3-Turb{;#jS!R5^1Wa^o>q@Ao&o8NKW1sy8$os*@fT{dK zr6RxxtYoXy@9lfT6m~o6bteUH8o=t@Oa}$(4J?~Z@RdcJRa9uP-kXM74v90ruwC#O z-s3+NR9n2g8#Pet68=gs!*A`^JGWiAzuel6%N_uOs}>&l&R}lWHiA1|a8K-F-T6Mf z^p{TWzqx;~!TvJW(FL1|)Jiuk9}P$frAfN1bVT0vYA;5o34`22@W6F3sATN9Zr@W|s}8_V(Phm1wI6b!*_lfqd@?G(w#_U!!G{{OOaV7qA+ zBI)pAPW^1?CVj#YrIQ1uP3^BV4H(;c@Nacv&6F*hjJGv#9g*mMZTNj#6o$E^zml{< zLj0swrT_po0fKUnzhWnI8-}3*A#HekAqqQTmio7)CjA4rRSg4ubqsx0n$~=xSgRkV zdOP)UdI*>M z*-dX}Wsi@s@%(^~#Z}>{i-(um?-&CJXsD@XI;oAfx43-mM;7)d`tHVp*{ZR=UocQG zMUPEtmzT@ZwC~RsI$dZ@AU#l0?5T)s6w^O0nTx<0*%2ZkA|AY>K#u_n%xv*CeK_Oj zjaV&xbysw*?7FygZ#q271_92q-`jLL%Mr6h>10 z^R?krG(XScuKK)MoIF9sqOP^dyx)uy1n8>Um}-T>>uF(9<--}{zZz&L@n4N3%WEzq z4%;$i%A>&Kyc6H!>VfOeCCsC1M5S8KqZqaw8>SzH312x4S@=U)mRZHX!2OQP^4*6! zn&j+J$2ZSJH(UFPfKx6vf0>FX*p;T6r`LG@3cvekJ_Bz_CS6U=(#$Y&f6AHQ4JBo% zI(hD?^6s;!`=bft7%I|6yBpc`AF}*d3bUUxBE^IE%PT6%lg*t$&1i$TKl(ybc+hss z$kBn{RAF$OfMtbCNzy@;NYB4BJX>-Ic`m11RUlI}q~bfKZbn6gES-cj9QnquD`P`u z|8$Z=Aljd3XJH6H*T_=w7cWVqbR4wMUXpW}$jbBZz%NKJ%85)pE6`~*7p6SZp4kO@ zUxjtB2^8`u(xV=PjKe(_ENrFYjGQmBJ|4Q9x|GJy-~)t(paiAHXUY9n3(u`s_l#I* zftFWcHLN%Mtu`;(BlheO|AHedV1NFf(NiUD9BN-YCkmvfspu-I^IVZ=zVhc3*X;cp z7>?^U<094197K`TCpvSFpq>j<$v?(Akzo1%emSMN9O%hp*K38nrTw=hvv%x<=8RN-OTm=iC z>=PUe6=dPJ9>1xB)Az9$0?C&b!^dEOaFY+?cZ~g9`Y%xq z;wQN4H;#OH5Iv~}3ydo2EMuuq>5y^eg_m2*!lImZ-qg^qiAGes{yt2O=JeM|wfUA3 z=-QiSMNs|GvKikm3CRy&{ZgepB%%4$H!l~q>ch*zVx$a7_GLe4LPG{ha&GIIytDA@ zjc8oRG*elLRfc&G!IS8h8jD#xXB_e2A>1$W`%t5Qod)S1CFU`9MSB@+LJrK$^irup z81TN4ZkV)n7Tl1!>@UaqP+fj`Q3_9a6(G{ zf43i9%GENQWbGtEM@qwRyn+HGnRTp5fV_y}WKoc?V_d8=Vd`&n++A8UItC1Kh%3HW zkGKJTGdyZ6gykj$T4SD6sAN&W{%v2%Ui2qu;9u+BIS#XKDjx}RJ!B8o3$fjW>G@Jw z`)#yN8Re?)joD3ghpCF#+Y!ScLUE!>-7G!{V0xRVq;#EH^Mjem()MZld7}Fa^?fge z=v`w^s=;By^JVhj?V#H*aPUCAO$we0yd|ZyUjgG84c@sXX`QvUj{s19QIbs-m)?-3 z?$PCmMvfaG(f6W>=x{*_qvw|t>K`qOv0EwI#zlbEUvMi-E~OK&_}TAET}eUNQJQSB z<4GP#yZ@F5rZ%vs)P261|F&ya|D0bW)dT{_BN;~9*tenMJy253if65|#HQ4$pPuw4gOkos6p!RhQFy;Bj%J`rq^%`6~0+myb z)LA!XoTKs$R!L33kub{3kq-t&JxN(&SdXeioqar!@EiRkE0#pu4Sa`oQ+KBz)rA?T zhaHiK1`cA-DGQe~#bJO42(-roHnT%?##}nIdBA^Iq+aLNy?JDy;V zkB^r%Z(7X)n?!s96-*iZqSJLm>M`EyE4*!8PkNQAhN3JTcXK^TUH)!vy~ezB#-TI~ z(!B*e7zgM^r^DPhvoEI5vPYwMqr{BS^|1EC;Q~#ok653>b^1QVzKx1srSb$HEwaR^jzZjo$)USP5 zcfUTW)Eu-Ks55*ZX&gC`n;F2O*0}sbRR0X_fp&E zSfy9zX!fsRWkwYH^%6Z|vyjfZ%RfA8fw}Q&ODp-8!k!r!#UVkF-pzAD4>^UovVt)~ zc8QPSIRQqs^gdUb%NicrmGu@kG+{8skh7t-+~h{6&t*!|V}BwIH70Rglehof zMyetV4+SZckcBH<`Q7JYg};U&7Im_I#LNYP2Ix6~LtQ=X@)C@QW^b~rV}OI*uA6I zGM`TZ=d;OoUtWdaK9EBKJGpV&ymct#CY-kVCX}}DNulxBChY?O=7@6@uzg~==3B3K z5X*%ZzO*5>CWicF>rcXxB+e*Hgfv8Npo{P(5==s*crwpbGrKMGi-PzT%YbdVCg^&w zVr}ieO~>-#KEJI?KexaN?Ho}iV*P#pR!9C_%=i!H0D;4tg5AZoaiFs{Cq?P@@RX%M zyVPUHr$Gk1^}s^@aJFS%A1xmgNt5F^LA9#Gac;8|__LrVbnJlz{+3uy1CNYH@HZnu zRDnY!W%;3yY0Fym=3^tnRO!EV?;h&e-2lVrv))4s=fgrr@hAEVbMWx9fIcYx5@b{k z*GZ?otB_bEjzjIr=R&nZx3wN7lXE9zL;}6KR)#AcyiATfi@~dAd?sBGMa9}|ru!Se z{pabmfJ2Pce+*Kkef;mf@he52073t|&poDApv$r-9Y}9?qJ>`2Xq{Z<(6vNie`JnJ z<$u-OeVf$#OuzH#be0JeP~+Z{t;DhzJ`cXypOF!#b$iZVgYobe^8Im;>UTVmzo3Cv z2`8EsuR-E~-(9aPrNxcuk#;Lhu;C40x1_t2E1P7=7OBzyye*|P*B?h05nV=;90C2b zyt$G`g$UK~WqHB8d4kYk*Q%>T5ubPb z^7CI*nEOw71FX|}>n_WDOkX+q`E7NI!3YdtC31LhzEQ*uPu!k?)OBk5uI2BgtF}+e z#tI6vlN(oq-5rVaY=i@*9m+xh29L)sdmg#aR|MOiF7#56ui4`zL?>TOriRR}DKceR zp4v&~7OJd{&SYmX#t*D0w}}=Ut9bv71sl5)g>13gjNm_f*uTW*9NxW;L?h^xr9qGZ zWhy^8=#T$#AVUOV#c}nU0*9Zb0AOdyQyCH`Zy#edXhV+94N_nQ|oVZwdt20_>jOc~~zPnDjk9HVYX}{K8xwfdb6`Jr_Wpx;AN}SBzMPz>*N&y}8-F zNbfT;yu$~gUYSs-(}52CHho6ezU0!1K+oBx`ah`yH;d0>!CQtXsO!~wn^sIkN9@HJ zRK|kuWn*N=#uZ~^u}+)>n_|7dAR;AJem}pt7gmF*&I54D%$?$o^WOjl1585*cl*_68t?S!VbbwWr4#MveAw9n*XY zKucpS%!rS;Y~XgG15ayJI8( literal 0 HcmV?d00001 diff --git a/helm/searchEngine/html/moogle_chat.html b/helm/searchEngine/html/moogle_chat.html new file mode 100644 index 000000000..627c625a6 --- /dev/null +++ b/helm/searchEngine/html/moogle_chat.html @@ -0,0 +1,19 @@ + + + + + + + +

+ + + +
+
Andrea Asperti
+ + +Last modified: Fri Jun 11 12:47:42 CEST 2004 + + + diff --git a/helm/searchEngine/html/moogle_chat1.html b/helm/searchEngine/html/moogle_chat1.html new file mode 100644 index 000000000..eb48d3d30 --- /dev/null +++ b/helm/searchEngine/html/moogle_chat1.html @@ -0,0 +1,83 @@ + + + +Moogle_chat1 + + +

There are more than one possible interpretations.

+
Please select one or more of the following: +
+
+ @CHOICES@ + + + + + + + + +

+ + + + + diff --git a/helm/searchEngine/html/moogle_chat2.html b/helm/searchEngine/html/moogle_chat2.html new file mode 100644 index 000000000..d3253f4fa --- /dev/null +++ b/helm/searchEngine/html/moogle_chat2.html @@ -0,0 +1,22 @@ + + + +Moogle_chat2 + + +

There are more than one possible interpretations.

+
Please choose one of the following. +
+ + + + + + + + @INTERPRETATIONS@ +

+ + + + diff --git a/helm/searchEngine/html/moogle_constraints_choice.html b/helm/searchEngine/html/moogle_constraints_choice.html new file mode 100644 index 000000000..b27dd93f1 --- /dev/null +++ b/helm/searchEngine/html/moogle_constraints_choice.html @@ -0,0 +1,90 @@ + + + +Moogle_constraints_choice + + +
+ + + + + + + + You can now proceed using the default generated constraints or you + can refine them by hand before going on.

+ + @FORM@ +
+ + + diff --git a/helm/searchEngine/html/moogle_help.html b/helm/searchEngine/html/moogle_help.html new file mode 100644 index 000000000..e6252cc28 --- /dev/null +++ b/helm/searchEngine/html/moogle_help.html @@ -0,0 +1,85 @@ + + + +Moogle_help + + + + + + + + + + + + + + + + + + + + + + + + +
moogle   + + + + + + +     + + Help
+ Input Syntax + +
+ + + + + + +
+ +
+ +
    + +
  • hint +
  • +
  • +
  • + +

    ccccccccccccc

    +
+ +

+ + Locate and display an object by its short name.
+ For instance + locating the identifier "nat" gives you back the definition of + natural numbers, and locating "plus" returns several (axiomatic and + concrete) definitions of the sum. +

+ +

+ + Given a closed statement G of the form +

+ \forall x1:T1...xn:Tn.body +
+ returns all theorems in the library whose conclusion is a generalization + of body, that is all theorems which can be used (as a last step) to prove G + (for tecnical reasons, the actual result may be a superset of + the expected one). +

+ + + + diff --git a/helm/searchEngine/html/moogle_init.html b/helm/searchEngine/html/moogle_init.html new file mode 100644 index 000000000..af4c26c26 --- /dev/null +++ b/helm/searchEngine/html/moogle_init.html @@ -0,0 +1,52 @@ + + + +Moogle + + +
+ + + +
moogle
+
+ + + + + + + + + + + + +
+ +
+ + + + + 		+ + Help
+ Input Syntax + +
+ + + + + + +
+ +
+ +@RESULTS@ + + + + diff --git a/helm/searchEngine/html/moogle_small.png b/helm/searchEngine/html/moogle_small.png new file mode 100644 index 0000000000000000000000000000000000000000..a387d9a937fcf72480f0ef245c530908f782a798 GIT binary patch literal 7599 zcmV;g9Z=$lP)=_NtkT&LMHQlS;$N#lYNq5UJ^nwVX^^X zCnSW;1{*M5@h01{t-YmIuhrGH*RA(Q3)z-sL*V1RNyz#1NuNs9N4M@dzjJ=)oZF3} zD1txBtCq4;d0_g%{f&c8WDgY&6=tT4A!F^5cYO7#TN#FV&1%`^kCPY!A@u6io!qE@ zkgETN^85Xd-)}r3aYPn0C$z`v6MMGrT%)Z1{Dq(KY*!!zv-q`XM)y5je)O@LrZI^a zjevI?Ix^;Md#Ul$+qB-^gdp%N%f1>rM-jZV+j{;*b9}o zLEw0fWm$~zAGIZX*K;eur}CfKRoJzC>vnIy^@)|Ay5{V^Y-ww0YiVNz_BEp6oof?s zIaPRZOZ9h81cKl@F5UK$wR?~8A9olZyWU8p(|RI~F@8ly4uWXc9=liyx9_x`f6*+K z3TL0@-Ec$f)Me^SVOrHb*F9_0&7wq%>px&f zqS-K05=jzC`P0Y^JkMv-$#$#tfN-#RCBaCdC`yuqS@t!n#Q=aYCWM@RTDmRADKhq4 zih!%u@cQSf(}iins0TstiV+Pt-4nl406SG!ZKRsA3!gd}ubQxuNp{@8N^ z0Pq4YisI2%v~;H;i2}#H9<>-D#4wB~im_NM*TQ*z1OR|o0QRX3Qn^&FRx6I(Y752Gvbk zuLoCNf>f1NRTdC=_Jx>f8s$pGbsb9SiIVdZ>y0Zf34P!1>)|T0RSQ9PX-6G zZU>=&#fEP;(ZF&%#u#3or?Kg~&~yK*rA_)h3j8vxwUCBRak zCkof$j!o4&Z>v82`>N|JJfp_q496ml50|bKZ~lC|y=%@A>`|QtXwoFi;)_??Bjb{; zbCY>;;E+BxG11aev9no12zM+q+q9)IxW9h$-yp|zM1mZb^87JD=~xRuxb>N-uYY0x zrcLZ+SEs&z52LrZzGqAy9>4RBmY1GaxCvwH=KAel@BZii%w2HdNitq!JlHsR)4pAK zQ+Qu?@i#~;W!sH%b$V+2_5`|5*LPL-eA3zXz0|<>5{oW7A;GH#-@JSJfpvv;b*7`E zb*AQ4T|Jv2Jjax)_UKqS%Z&w2AsHwC^pRD)-Ps@rScdhHE8ruXmBkAbRZ+ce-*)SP z`|lagcJ|-$b-AbCtCn|eSl9B)+v0=|Mu&&*y({}~clNBkdI2;5Kor>+*riK?)|SBc z+5D7f+2)H|aetpttJM@mVOe$#5K#n=JXWn%%jcYxu#=&`51 z3R7QNzdn&$^^0u$w1!cw7s_E6c!7lU8xI$kLHWzF2qZkT>-TGOXaB5k<$I4`%(`9v zx9=XG8Xdar#@s;n3dgqUX7s{f{@eFi0hcx#L0CWZ?kmV8=d2JI>^bH96xH=~I;Fed zHqmgzgO6Pwt<2QF{ONrgHx|!YGw^r+SgjVR=Lak=y>-oa*J9%vx9GORdG5}?d9QT$ z?=t7UZ2=C0fCB)QVb5R1a~x_W>h&+g%jIIVIzLg5j@O@9XIym!LCAp!R8>C4qQ?d$ z@8P?g2Y@Md&UVnzfrf-Gvi}4LUBFW+TPjI-IZ!>&-7k3=6||jL&FA%L__PYJ+$lI zdHmwJz4rGXt!&+X;7ixVbkQ3d8!eW~LEx=uk3RW!yI!86o&f;g{q^DBK0RpLHqSCd zAgU}K?-TQrbKnL)_(pAL|K4~@>xXX`Ke*p98$^;bt?eys?XAmB#n=CDj%7HODSE*} zH(zhoO`yjm_z3)FK)Gl&2LLS@9)O*kB7;M;R;ik17KrxuCA``Mcu9K9bH{r{mYhR-t$p!<=Ftx z3~Y~m`o{9qIHh#%$s^+tq4wp22mR-U&gR9q>o~J|I=ebMJ6qd37WZ}c_Vl(dzYfF| z03eG109zjYOm${v&X&{F;Fr%@`Fy!cIzW(Bs#GOO?d)jp?&<07TeAABCD&fS0wW`m zV_A+Rgir0=I(m3yza3N801GCX!IaZbxUXTG`E=A7;rC|4VsMp314vku_B#ELV zrP3McIL|@|$+Fyg?&@giN&t{J1_1K+{%odH349L#{PNEkI(+b;zh{_=TDPnydP*mf za(rl&R84PP%_uzpAdv_F@`LwJ4~RUPM_qi55co?sCYEn9eg3$9eE^|~1Z zK@>$#t~Z89i&tGL1wlXv(PApk^UZe1G36UX-nLE1^Xd%?06baL6S|^GCz_B*T0FVt zig;32I0gU;<;vj~H(Is>072~u0C24k09c}Es-~*y-1f~AEv{kxYC*)Z2r@w>V{&R} zt7TdFa$x(|YHM{XesamU4t5w&ri>2V+hbot^VHn1vlq#~UC^E+AXf(_^NJ#my zgYL|9xl{%KU|3mTB|$n-7Yrk?&cBdLWfXNb(~ND|T&vXrKVaR*0br&I0D!Teiag;@ zSQfAhR^rzPA|t=-xO)$b7>3bsgNnlxiXPB#v??xGd0~u~_uy<&lSBx869B4p({}B- zH6Me9qeN^N;CldIH7tf>8vFL{|Hw7l*POoVk%z;ZZpq&NeCN%dwK+0f$j9RGQVf7_YrlolDe*M##|NuvRS_^~UornuGf*YgQA-b~u((RaFoOM)+tn zG=maC6xmjDaR4AVJ^(OmbfR2`F-~b6^1V`U? z3>xSWG=OC`%jP%@MmGMQ*}L7n=KU={`c2nQ9_G)vxNOwSYMB*CS6A24WlNXzEpBUT zi^XG@d8MXXX9qd=Y?HKMmjGt4SO~tMhr*8ldWGA z6_%tlodXmVt59!*j_u@PP_DZ5M#zd8%*&5&DFwj-W-wjsy0l(AM7_pY%e$h8vOGWM zI`hyl$A&}Kjyz8U3INGmtMHfCrdFI+OJ}C1CoQu^B(<$;(c=DruC9)xp5#Tsa_oYn zcLCqL;$oHKkfJbv$d;E{ipBcYoz`Pd)GxVEuxuM+tSG7^iF1|Yyz-6bN#NK{af$#X z5p@d_fS4c*PSO_U1rmu8iR%DRVK^p}_WaNfBi9b=WiOqGGI30e9e`h9(t;T_h;#sG zI1vEI$|*q*(1^b0951lT0KiMRhn{Q96sw-=&3o<8gu8ct-YyTWIk&4tjWk)|817_D z2><|Uyd0P{0+ayQ&pd8fR^U5?=W{K&zWybP`+D2jIuuo5Iey-=zk(SMLKm#oVk)C2 zID|yoQMT>m?|y(zPL-}$6M3E|2!g6Aga~uMoX3<9#x*q-SQd{Ujv{%_wnnYIpaUKo z+Bwtl!XN+uu`S0S;CPM(t6Y25@2ZtOj%9kjce0K&GrJPYMl)5AlkE%w%&;F^yQnki zQO}?>tU25#zB|}(>c@1N?dS)O8im6zymcvh?}ZsfOX%sebX1$`7&IJ}qUCH$P&ZTz z2~3SmFLEtY9u(7@TTf9CC< zeC~-Ym1?bCtq0HSZrt$g$xWMgUVmlcBmd(JUW~VPc4X6O%(8RbbOAI_0D$u8=a|JA z07zrd8ui2X-N`Tv%kr4PC!Yu%OVl`Ye1`;My!O&qGf}H5J2J+gsC4d`v{)>%4A#_` zD3YU@`#h$E5y0hFSKPo4LKQC+O+CHc*1dBXjB5DmY*qB5Yv9v`8>xfio|dX zDDQJ^+GIZII2s-Nv1L0n@=plmpu(VXxg5?^p{-{v%dm=~U<@qB_IGFh{ZmWdeLj;A zDl~8oj8ty=_UPyD^8V$X%6A?xo_%iH^=pDlR_QdNU5mQf+uMmO0Xni<3)Br50HAfn z*_CV;04Nv|D5~81%dy=%eb4^`#y$uE$D!sVd7kw3kW-g2JdZq=LS%|!xVWzzh9MCp zS&@03KbrQ9xN zysYo5H!l19`}j}2BfRC(2>_^Bux-aUYi>DfKyux%ySt~ir#GER&#MsUpf<}L@&4SG` ztg5K8EFInE6$v`N(Tz~l`9D8q^beR603e6y;V*u?Rbf!9uovI2Zb*$z&#*ZR(lbGM3F|)4hFt%a^Zs%b91MvV6HB z^9?6p#H`P>{@40Yi)k?}wqQ&ju1*#vrUAfI%n$%GM|#zgL~>vJw|uTOA3!Mt9)U7` z@Wm@u?fmS=rU!Q)i2;Ed?%y@^&!5e2cnYJViujRH*KsHU?%7S?I*#YMK@c9Xzr+_s?CKb};B#M7y8ALoy|b$`olea? zBoRqld#`@#4?X6hh7&cM$SOUz{ee@Bk)L`_vjgb)m7iBPuip05?T>9c_nde9Fp+M} zrc>>m9SJ>oykGN#q%-MkF1KL_`Q;yfZ|stlhtBWW za`md=E6>_|dgre$I}fioBXhx}j$@%HiYzO9X}9%@d#3Msz?{sN;+l2+br^-pez^bR1<8NQ67;8N0>>uvA-`}cgNH`WapXh;i%!oh=w58n6liHGl^r80?V934Sx z6*0LhuYAiVzM$wS8qq{7hQ9gl`8)0`)=hV0)P$&tzy)9mFIbe zVSL{|{jHmC{RfJntZ76E5v&C0+u&BF9drCO0hG1r>Y zG>u^x8b*HLRjWp^Tq+f2rVCRIvthdqhDg)mdP2`+Gs#pksV9j@5JHw|&J;`e=|ZD4 z;{oCrjwd`33HUx@7>ux@sd_S%OeW`Q{RJ{x7+RJ!l`oV_#YU~{hQP8c$8)^EBZP1i zaTv*QJ(W(WvdRq zJdXym#ik_7s;b7cSSFiEr_z!v&6=TBt5+%&t6|!XOM{@9!DLB{#bR1aYnlNe-(Q}KYB^=wat$MX)I<7|pABBF1SzaJL)UdZ&kI9JDWxIBEDI6E7&8negfxRvGeHGG5QZVcFc{;xi*p+MfI>7&253l| zYhoD8aXcZyy!SWIkWxwkj%**s?1|_Ens?nO|Q= zK!c#k|0$&`1Ay40$rS*w&7;JUB#ELpciyJy;|QU7?RbO`%d*V?HTS0lHOwh#*5Pwk z=CSP8w&@GCp!fw(Ud@wVJ!@kc9^AElMQb^xwA)UjE!UdOwZya-5ede#>k0fIrp08L z81Bp+Pw@a?)Qq9QeeD@tPw0Q>TY4}8%(1V0YOlFFukwiFg17xa8vcLD;Yq7vc#}mZ zKRNZ*RXhS{Z*TAJ>ek}gJa1q*HlEZ)QTWhW{^7mRzC4WjujEJ$)kN7wRp9{@zg<~SOLVMOVl&G5PeMbX5J z=Y^P+l9Lr)kyU{Rz`%kh(q=6o3Jj4@*yv1!N^=bL#%$P|#tanV3fi;3WHthpPizPwILi9!oF`euI$uW_f!$rF74}v8zA*c+KXU1wl;o-gDKN z*ItzDYa^Ipk7m-(?RRhe@z~ZaTW@{`w`!^8xX!@9z$+Zw`?DEdr5H71^NxeJ{>Rfh zMj6Z!mQP?_W2BaBl0UUGlq3~1OsQ(`n+Qe@?mf5H_{6m%zPiA)badgBbu=+EQB4qrU5H?dhacnwg0LU(@y0 z*4A_?{lpU0(=+3vT3EW@!#ATl9@7kG#O-uULg{{=FHNWUAv RIQjqp002ovPDHLkV1oMj;e7xA literal 0 HcmV?d00001 diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 87bcad36a..4c9f34989 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -39,25 +39,39 @@ open Printf;; let daemon_name = "Search Engine";; +let string_tail s = + let len = String.length s in + String.sub s 1 (len-1) + (* First of all we load the configuration *) let _ = - let configuration_file = "/projects/helm/etc/searchEngine.conf.xml" in + let configuration_file = "searchEngine.conf.xml" in Helm_registry.load_from configuration_file ;; +let port = Helm_registry.get_int "search_engine.port";; + let pages_dir = Helm_registry.get "search_engine.html_dir";; (** accepted HTTP servers for ask_uwobo method forwarding *) let valid_servers= Helm_registry.get_string_list "search_engine.valid_servers";; - -let interactive_user_uri_choice_TPL = pages_dir ^ "/templateambigpdq1.html";; -let interactive_interpretation_choice_TPL = - pages_dir ^ "/templateambigpdq2.html";; -let constraints_choice_TPL = pages_dir ^ "/constraints_choice_template.html";; -let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";; +let interactive_user_uri_choice_TPL = pages_dir ^ "/moogle_chat1.html";; +let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html";; +let constraints_choice_TPL = pages_dir ^ "/moogle_constraints_choice.html";; +(* let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";; *) +let start_TPL = pages_dir ^ "/moogle.html";; +let final_results_TPL = pages_dir ^ "/moogle.html";; + +let my_own_url = + let ic = Unix.open_process_in "hostname -f" in + let hostname = input_line ic in + ignore (Unix.close_process_in ic); + sprintf "http://%s:%d" hostname port +;; exception Chat_unfinished +exception Invalid_action of string (* invalid action for "/search" method *) let javascript_quote s = let rex = Pcre.regexp "'" in @@ -121,9 +135,9 @@ let theory_of_result result = "" ^ string_of_int !idx ^ "." ^ i ) result "" in - "

Query Results:

" ^ results ^ "
" + "Query Results:" ^ results ^ "
" else - "

Query Results:

No results found!

" + "Query Results:

No results found!

" ;; let pp_result result = @@ -150,19 +164,26 @@ let fold_file f init fname = (** iter like function on files *) let iter_file f = fold_file (fun _ line -> f line) () -let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE, - interpretations_RE, interpretations_labels_RE, results_RE, new_aliases_RE, - form_RE, variables_initialization_RE) +let (expression_tag_RE, + action_tag_RE, + advanced_tag_RE, + title_tag_RE, no_choices_tag_RE, current_choices_tag_RE, + choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE, iden_tag_RE, + interpretations_RE, interpretations_labels_RE, results_RE, new_aliases_RE, + form_RE, variables_initialization_RE, search_engine_url_RE) = - (Pcre.regexp "@TITLE@", Pcre.regexp "@CHOICES@", Pcre.regexp "@MSG@", - Pcre.regexp "@ID_TO_URIS@", Pcre.regexp "@ID@", - Pcre.regexp "@INTERPRETATIONS@", Pcre.regexp "@INTERPRETATIONS_LABELS@", - Pcre.regexp "@RESULTS@", Pcre.regexp "@NEW_ALIASES@", Pcre.regexp "@FORM@", - Pcre.regexp "@VARIABLES_INITIALIZATION@") + (Pcre.regexp "@EXPRESSION@", + Pcre.regexp "@ACTION@", + Pcre.regexp "@ADVANCED@", + Pcre.regexp "@TITLE@", Pcre.regexp "@NO_CHOICES@", + Pcre.regexp "@CURRENT_CHOICES@", + Pcre.regexp "@CHOICES@", Pcre.regexp "@MSG@", + Pcre.regexp "@ID_TO_URIS@", Pcre.regexp "@ID@", Pcre.regexp "@IDEN@", + Pcre.regexp "@INTERPRETATIONS@", Pcre.regexp "@INTERPRETATIONS_LABELS@", + Pcre.regexp "@RESULTS@", Pcre.regexp "@NEW_ALIASES@", Pcre.regexp "@FORM@", + Pcre.regexp "@VARIABLES_INITIALIZATION@", Pcre.regexp "@SEARCH_ENGINE_URL@") let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$" -let port = Helm_registry.get_int "search_engine.port";; - let pp_error = sprintf "

Error: %s

";; let bad_request body outchan = @@ -176,17 +197,17 @@ let contype = "Content-Type", "text/html";; let get_constraints term = function - | "/locateInductivePrinciple" -> + | "/elim" -> None, (CGLocateInductive.get_constraints term), (None,None,None) - | "/searchPattern" -> + | "/match" -> let constr_obj, constr_rel, constr_sort = CGSearchPattern.get_constraints term in (Some CGSearchPattern.universe), (constr_obj, constr_rel, constr_sort), (Some constr_obj, Some constr_rel, Some constr_sort) - | "/matchConclusion" -> + | "/hint" -> let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in (* FG: there is no way to choose the block number ***************************) let block = pred (List.length list_of_must) in @@ -268,13 +289,343 @@ let add_user_constraints ~constraints | _ -> failwith ("Can't parse constraint string: " ^ constraints) in +let send_results results + ?(id_to_uris = DisambiguatingParser.EnvironmentP3.of_string "") + (req: Http_types.request) outchan + = + Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; + Http_daemon.send_header "Content-Type" "text/xml" outchan; + Http_daemon.send_CRLF outchan ; + let subst = + (search_engine_url_RE, my_own_url) :: + (results_RE, theory_of_result results):: + (advanced_tag_RE, req#param "advanced"):: + (expression_tag_RE, req#param "expression"):: + (List.map + (function (key,value) -> + let key' = (Pcre.extract ~pat:"param\\.(.*)" key).(1) in + Pcre.regexp ("@" ^ key' ^ "@"), value) + (List.filter + (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key) + req#params)) + in + iter_file + (fun line -> + let new_aliases = + DisambiguatingParser.EnvironmentP3.to_string id_to_uris + in + let processed_line = + apply_substs + (* CSC: Bug here: this is a string, not an array! *) + ((new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'")::subst) + line + in + output_string outchan (processed_line ^ "\n")) + final_results_TPL +in + +let exec_action mqi_handle (req: Http_types.request) outchan = + let term_string = req#param "expression" in + let (context, metasenv) = ([], []) in + let id_to_uris_raw = + try req#param "aliases" + with Http_types.Param_not_found _ -> "" + in + let parse_interpretation_choices choices = + List.map int_of_string (Pcre.split ~pat:" " choices) in + let parse_choices choices_raw = + let choices = Pcre.split ~pat:";" choices_raw in + List.fold_left + (fun f x -> + match Pcre.split ~pat:"\\s" x with + | ""::id::tail + | id::tail when id<>"" -> + (fun id' -> + if id = id' then + Some (List.map (fun u -> Netencoding.Url.decode u) tail) + else + f id') + | _ -> failwith "Can't parse choices") + (fun _ -> None) + choices + in + let id_to_uris = + DisambiguatingParser.EnvironmentP3.of_string id_to_uris_raw in + let id_to_choices = + try + let choices_raw = req#param "choices" in + parse_choices choices_raw + with Http_types.Param_not_found _ -> (fun _ -> None) + in + let interpretation_choices = + try + let choices_raw = req#param "interpretation_choices" in + if choices_raw = "" then None + else Some (parse_interpretation_choices choices_raw) + with Http_types.Param_not_found _ -> None + in + let module Chat: DisambiguateTypes.Callbacks = + struct + + let interactive_user_uri_choice + ~selection_mode ?ok + ?enable_button_for_non_vars ~(title: string) ~(msg: string) + ~(id: string) (choices: string list) + = + (match id_to_choices id with + | Some choices -> choices + | None -> + if req#param "advanced" = "no" then + let isvar s = + let len = String.length s in + let suffix = String.sub s (len-4) 4 in + not (suffix = ".var") in + List.filter isvar choices + else + let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in + (match selection_mode with + | `SINGLE -> assert false + | `MULTIPLE -> + Http_daemon.send_basic_headers ~code:(`Code 200) outchan; + Http_daemon.send_CRLF outchan ; + let check_box uri = + "" ^ "" ^ uri ^ "" in +(* aggiungere gli hyperlinks? *) + let check_boxes = + String.concat "
" + (List.map check_box choices) in + iter_file + (fun line -> + let processed_line = + apply_substs + [advanced_tag_RE, req#param "advanced"; + choices_tag_RE, check_boxes; + no_choices_tag_RE, + string_of_int (List.length choices); + iden_tag_RE, id; + current_choices_tag_RE, req#param "choices"; + expression_tag_RE, req#param "expression"; + action_tag_RE, string_tail req#path ] + line + in + output_string outchan (processed_line ^ "\n")) + interactive_user_uri_choice_TPL; + raise Chat_unfinished)) + + let interactive_interpretation_choice interpretations = + match interpretation_choices with + Some l -> prerr_endline "CARRAMBA" ; l + | None -> + let html_interpretations = + let radio_button n = + "" in + let text interp = + String.concat "
" + (List.map + (fun (id, value) -> + sprintf "%s = %s" id value) + interp) in + let rec aux n = + function + [] -> [] + | interp::tl -> + ((radio_button n)^(text interp))::(aux (n+1) tl) in + String.concat "
" (aux 0 interpretations) + in + Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; + Http_daemon.send_CRLF outchan ; + iter_file + (fun line -> + let processed_line = + apply_substs + [advanced_tag_RE, req#param "advanced"; + interpretations_RE, html_interpretations; + current_choices_tag_RE, req#param "choices"; + expression_tag_RE, req#param "expression"; + action_tag_RE, string_tail req#path ] + line + in + output_string outchan (processed_line ^ "\n")) + interactive_interpretation_choice_TPL; + raise Chat_unfinished + + let input_or_locate_uri ~title ?id () = + assert false + + end + in + let module Disambiguate' = DisambiguatingParser.Make(Chat) in + let (id_to_uris', metasenv', term') = + match + Disambiguate'.disambiguate_term mqi_handle + context metasenv term_string id_to_uris + with + [id_to_uris',metasenv',term'] -> id_to_uris',metasenv',term' + | _ -> assert false + in + let universe, + ((must_obj, must_rel, must_sort) as must'), + ((only_obj, only_rel, only_sort) as only) = + get_constraints term' req#path + in + let must'', only' = + (try + add_user_constraints + ~constraints:(req#param "constraints") + (must', only) + with Http_types.Param_not_found _ -> + if req#param "advanced" = "no" then + (must',only) + else + let variables = + "var aliases = '" ^ id_to_uris_raw ^ "';\n" ^ + "var constr_obj_len = " ^ + string_of_int (List.length must_obj) ^ ";\n" ^ + "var constr_rel_len = " ^ + string_of_int (List.length must_rel) ^ ";\n" ^ + "var constr_sort_len = " ^ + string_of_int (List.length must_sort) ^ ";\n" in + let form = + (if must_obj = [] then "" else + "

Obj constraints

" ^ + "" ^ + (String.concat "\n" (List.map html_of_r_obj must_obj)) ^ + "
" ^ + (* The following three lines to make Javascript create *) + (* the constr_obj[] and obj_depth[] arrays even if we *) + (* have only one real entry. *) + "" ^ + "") ^ + (if must_rel = [] then "" else + "

Rel constraints

" ^ + "" ^ + (String.concat "\n" (List.map html_of_r_rel must_rel)) ^ + "
" ^ + (* The following two lines to make Javascript create *) + (* the constr_rel[] and rel_depth[] arrays even if *) + (* we have only one real entry. *) + "" ^ + "") ^ + (if must_sort = [] then "" else + "

Sort constraints

" ^ + "" ^ + (String.concat "\n" (List.map html_of_r_sort must_sort)) ^ + "
" ^ + (* The following two lines to make Javascript create *) + (* the constr_sort[] and sort_depth[] arrays even if *) + (* we have only one real entry. *) + "" ^ + "") ^ + "

Only constraints

" ^ + "Enforce Only constraints for objects: " ^ + "
" ^ + "Enforce Rel constraints for objects: " ^ + "
" ^ + "Enforce Sort constraints for objects: " ^ + "
" + in + Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; + Http_daemon.send_CRLF outchan ; + iter_file + (fun line -> + let processed_line = + apply_substs + [form_RE, form ; + variables_initialization_RE, variables; + advanced_tag_RE, req#param "advanced"; + current_choices_tag_RE, req#param "choices"; + interpretations_RE, req#param "interpretation_choices"; + expression_tag_RE, req#param "expression"; + action_tag_RE, string_tail req#path] line + in + output_string outchan (processed_line ^ "\n")) + constraints_choice_TPL; + raise Chat_unfinished) + in + let query = + G.query_of_constraints universe must'' only' + in + let results = MQueryInterpreter.execute mqi_handle query in + send_results results ~id_to_uris:id_to_uris' req outchan +in + (* HTTP DAEMON CALLBACK *) +let build_dynamic_uri url params = + let p = + String.concat "&" (List.map (fun (key,value) -> (key ^ "=" ^ (Netencoding.Url.encode value))) params) in + url ^ "?" ^ p +in + +let build_uwobo_request (req: Http_types.request) outchan = + prerr_endline ("ECCOLO: " ^ req#param "param.SEARCH_ENGINE_URL"); + let xmluri = build_dynamic_uri ((req#param "param.SEARCH_ENGINE_URL") ^ "/search") req#params in + prerr_endline ("xmluri: " ^ xmluri); + (*let xmluri = Netencoding.Url.encode xmluri in*) + let server_and_port = req#param "param.processorURL" in + let newreq = + build_dynamic_uri + (server_and_port ^ "apply") + (("xmluri",xmluri)::("keys",(req#param "param.thkeys"))::req#params) in + (* if List.mem server_and_port valid_servers then *) + prerr_endline newreq; + if true then + Http_daemon.respond + ~headers:["Content-Type", "text/html"] + ~body:(Http_client.http_get newreq) + outchan + else + Http_daemon.respond + ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port ^ + (String.concat "\n" valid_servers))) + outchan +in + +let proxy url outchan = + let server_and_port = + (Pcre.extract ~rex:server_and_port_url_RE url).(1) + in + if List.mem server_and_port valid_servers then + Http_daemon.respond + ~headers:["Content-Type", "text/html"] + ~body:(Http_client.http_get url) + outchan + else + Http_daemon.respond + ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port)) + outchan +in + let callback mqi_handle (req: Http_types.request) outchan = try debug_print (sprintf "Received request: %s" req#path); (match req#path with | "/help" -> Http_daemon.respond ~body:"HELM Search Engine" outchan + | "/locate" -> + let initial_expression = + try req#param "expression" with Http_types.Param_not_found _ -> "" + in + let expression = + Pcre.replace ~pat:"\\s*$" + (Pcre.replace ~pat:"^\\s*" initial_expression) + in + if expression = "" then + send_results [] req outchan + else + let results = + let query = G.locate expression in + MQueryInterpreter.execute mqi_handle query + in + send_results results req outchan | "/execute" -> let query_string = req#param "query" in let lexbuf = Lexing.from_string query_string in @@ -282,11 +633,7 @@ let callback mqi_handle (req: Http_types.request) outchan = let result = MQueryInterpreter.execute mqi_handle query in let result_string = pp_result result in Http_daemon.respond ~body:result_string ~headers:[contype] outchan - | "/locate" -> - let id = req#param "id" in - let query = G.locate id in - let result = MQueryInterpreter.execute mqi_handle query in - Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan +(* Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan *) | "/unreferred" -> let target = req#param "target" in let source = req#param "source" in @@ -295,6 +642,8 @@ let callback mqi_handle (req: Http_types.request) outchan = Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan | "/getpage" -> (* TODO implement "is_permitted" *) + let _ = prerr_endline + (Netencoding.Url.encode "http://mowgli.cs.unibo.it:38080/") in (let is_permitted _ = true in let remove_fragment uri = Pcre.replace ~pat:"#.*" uri in let page = remove_fragment (req#param "url") in @@ -314,6 +663,9 @@ let callback mqi_handle (req: Http_types.request) outchan = (fun line -> output_string outchan ((apply_substs + ((search_engine_url_RE, my_own_url) :: + (advanced_tag_RE, "no") :: + (results_RE, "") :: (List.map (function (key,value) -> let key' = @@ -324,253 +676,19 @@ let callback mqi_handle (req: Http_types.request) outchan = (List.filter (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key) req#params) - ) + )) line) ^ "\n")) fname end else Http_daemon.send_file ~src:(FileSrc fname) outchan) | page -> Http_daemon.respond_forbidden ~url:page outchan)) - | "/ask_uwobo" -> - let url = req#param "url" in - let server_and_port = - (Pcre.extract ~rex:server_and_port_url_RE url).(1) - in - if List.mem server_and_port valid_servers then - Http_daemon.respond - ~headers:["Content-Type", "text/html"] - ~body:(Http_client.http_get url) - outchan - else - Http_daemon.respond - ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port)) - outchan - | "/searchPattern" - | "/matchConclusion" - | "/locateInductivePrinciple" -> - let term_string = req#param "term" in - let (context, metasenv) = ([], []) in - let id_to_uris_raw = req#param "aliases" in - let parse_interpretation_choices choices = - List.map int_of_string (Pcre.split ~pat:" " choices) in - let parse_choices choices_raw = - let choices = Pcre.split ~pat:";" choices_raw in - List.fold_left - (fun f x -> - match Pcre.split ~pat:"\\s" x with - | ""::id::tail - | id::tail when id<>"" -> - (fun id' -> - if id = id' then - Some (List.map (fun u -> Netencoding.Url.decode u) tail) - else - f id') - | _ -> failwith "Can't parse choices") - (fun _ -> None) - choices - in - let id_to_uris = - DisambiguatingParser.EnvironmentP3.of_string id_to_uris_raw in - let id_to_choices = - try - let choices_raw = req#param "choices" in - parse_choices choices_raw - with Http_types.Param_not_found _ -> (fun _ -> None) - in - let interpretation_choices = - try - let choices_raw = req#param "interpretation_choices" in - Some (parse_interpretation_choices choices_raw) - with Http_types.Param_not_found _ -> None - in - let module Chat: DisambiguateTypes.Callbacks = - struct - - let interactive_user_uri_choice - ~selection_mode ?ok - ?enable_button_for_non_vars ~(title: string) ~(msg: string) - ~(id: string) (choices: string list) - = - (match id_to_choices id with - | Some choices -> choices - | None -> - let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in - (match selection_mode with - | `SINGLE -> assert false - | `MULTIPLE -> - Http_daemon.send_basic_headers ~code:(`Code 200) outchan; - Http_daemon.send_CRLF outchan ; - iter_file - (fun line -> - let formatted_choices = - String.concat "," - (List.map (fun uri -> sprintf "\'%s\'" uri) - choices) - in - let processed_line = - apply_substs - [title_tag_RE, title; - choices_tag_RE, formatted_choices; - msg_tag_RE, msg; - id_to_uris_RE, id_to_uris_raw; - id_RE, id] - line - in - output_string outchan (processed_line ^ "\n")) - interactive_user_uri_choice_TPL; - raise Chat_unfinished)) - - let interactive_interpretation_choice interpretations = - match interpretation_choices with - Some l -> prerr_endline "CARRAMBA" ; l - | None -> - let html_interpretations_labels = - String.concat ", " - (List.map - (fun l -> - "\'" ^ - (String.concat "
" - (List.map - (fun (id, value) -> - let id = javascript_quote id in - let value = javascript_quote value in - sprintf "%s = %s" id value) - l)) ^ - "\'") - interpretations) - in - let html_interpretations = - let rec aux n = - function - [] -> [] - | _::tl -> ("'" ^ string_of_int n ^ "'")::(aux (n+1) tl) - in - String.concat ", " (aux 0 interpretations) - in - Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; - Http_daemon.send_CRLF outchan ; - iter_file - (fun line -> - let processed_line = - apply_substs - [interpretations_RE, html_interpretations; - interpretations_labels_RE, html_interpretations_labels] - line - in - output_string outchan (processed_line ^ "\n")) - interactive_interpretation_choice_TPL; - raise Chat_unfinished - - let input_or_locate_uri ~title ?id () = - assert false - - end - in - let module Disambiguate' = DisambiguatingParser.Make(Chat) in - let (id_to_uris', metasenv', term') = - match - Disambiguate'.disambiguate_term mqi_handle - context metasenv term_string id_to_uris - with - [id_to_uris',metasenv',term'] -> id_to_uris',metasenv',term' - | _ -> assert false - in - let universe, - ((must_obj, must_rel, must_sort) as must'), - ((only_obj, only_rel, only_sort) as only) = - get_constraints term' req#path - in - let must'', only' = - (try - add_user_constraints - ~constraints:(req#param "constraints") - (must', only) - with Http_types.Param_not_found _ -> - let variables = - "var aliases = '" ^ id_to_uris_raw ^ "';\n" ^ - "var constr_obj_len = " ^ - string_of_int (List.length must_obj) ^ ";\n" ^ - "var constr_rel_len = " ^ - string_of_int (List.length must_rel) ^ ";\n" ^ - "var constr_sort_len = " ^ - string_of_int (List.length must_sort) ^ ";\n" in - let form = - (if must_obj = [] then "" else - "

Obj constraints

" ^ - "" ^ - (String.concat "\n" (List.map html_of_r_obj must_obj)) ^ - "
" ^ - (* The following three lines to make Javascript create *) - (* the constr_obj[] and obj_depth[] arrays even if we *) - (* have only one real entry. *) - "" ^ - "") ^ - (if must_rel = [] then "" else - "

Rel constraints

" ^ - "" ^ - (String.concat "\n" (List.map html_of_r_rel must_rel)) ^ - "
" ^ - (* The following two lines to make Javascript create *) - (* the constr_rel[] and rel_depth[] arrays even if *) - (* we have only one real entry. *) - "" ^ - "") ^ - (if must_sort = [] then "" else - "

Sort constraints

" ^ - "" ^ - (String.concat "\n" (List.map html_of_r_sort must_sort)) ^ - "
" ^ - (* The following two lines to make Javascript create *) - (* the constr_sort[] and sort_depth[] arrays even if *) - (* we have only one real entry. *) - "" ^ - "") ^ - "

Only constraints

" ^ - "Enforce Only constraints for objects: " ^ - "
" ^ - "Enforce Rel constraints for objects: " ^ - "
" ^ - "Enforce Sort constraints for objects: " ^ - "
" - in - Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; - Http_daemon.send_CRLF outchan ; - iter_file - (fun line -> - let processed_line = - apply_substs - [form_RE, form ; - variables_initialization_RE, variables] line - in - output_string outchan (processed_line ^ "\n")) - constraints_choice_TPL; - raise Chat_unfinished) - in - let query = - G.query_of_constraints universe must'' only' - in - let results = MQueryInterpreter.execute mqi_handle query in - Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; - Http_daemon.send_CRLF outchan ; - iter_file - (fun line -> - let new_aliases = - DisambiguatingParser.EnvironmentP3.to_string id_to_uris' in - let processed_line = - apply_substs - [results_RE, theory_of_result results ; - (* CSC: Bug here: this is a string, not an array! *) - new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'"] - line - in - output_string outchan (processed_line ^ "\n")) - final_results_TPL + (* OLD | "/ask_uwobo" -> proxy (req#param "url") outchan *) + | "/ask_uwobo" -> build_uwobo_request req outchan + | "/hint" + | "/match" + | "/elim" -> + exec_action mqi_handle req outchan | invalid_request -> Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) outchan); -- 2.39.2