From ea6c99c69f7bde9f2778e68bb1c50acf3a927799 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sat, 27 Jun 2009 13:47:02 +0000 Subject: [PATCH] accidentally committed some changes on the branch, now moving back to trunk (w/ some conflicts, argh!): fixed a bug in the way redex expanded metafunctions (it had old code left in there) and improved error messages for domain failures in reduction relations svn: r15317 --- collects/redex/private/bitmap-test.ss | 15 +- .../bmps/metafunction-Name-vertical.png | Bin 4795 -> 4844 bytes collects/redex/private/pict.ss | 36 +- collects/redex/private/reduction-semantics.ss | 345 +++++++++--------- collects/redex/private/struct.ss | 52 +-- collects/redex/private/tl-test.ss | 27 +- 6 files changed, 258 insertions(+), 217 deletions(-) diff --git a/collects/redex/private/bitmap-test.ss b/collects/redex/private/bitmap-test.ss index 7f92db36d4..5240b252cd 100644 --- a/collects/redex/private/bitmap-test.ss +++ b/collects/redex/private/bitmap-test.ss @@ -36,6 +36,20 @@ (extend-reduction-relation red lang (--> 1 2))) "extended-reduction-relation.png") +;; this test should fail because it gets the order wrong +;; for the where/side-conditions +(define red2 + (reduction-relation + lang + (--> (number_a number_b number_c) + any_z + (where (any_x any_y) (number_a number_b)) + (side-condition (= (term number_c) 5)) + (where any_z any_x)))) + +(test (render-reduction-relation red2) + "red2.png") + (define-metafunction lang [(S x v e) e]) @@ -92,7 +106,6 @@ (render-metafunction Name)) "metafunction-Name-vertical.png") - ;; makes sure that there is no overlap inside or across metafunction calls ;; or when there are unquotes involved (define-metafunction lang diff --git a/collects/redex/private/bmps/metafunction-Name-vertical.png b/collects/redex/private/bmps/metafunction-Name-vertical.png index cde38b7b0f9323367c1547623680abc12e2c96c6..6d1d9f74ce463f999b53d5471c402c434aea1bbf 100644 GIT binary patch literal 4844 zcmW-l2RzjOAIHBxkxPf`jAWCLjB`fWoDp$cMVE186lG@bd6B|pMD|J|o0QB#vYpJr ziR_WR>Hq2fc|2}C9-sT(_w#wbU$58mbCEdx>-2Q&bPxp5>u77-04em;{(jnvV25o~qWh7ohFis}vL3#`88!sBd_){7#rA9UhX zG-i+03~@zN7($r?%~<)Z);wRkcbfL)!U$F7D+peP(->_ug=cg7LUUXj!w`kXn^JeU znqGG}(N#z3;yQ!)Qe7=eLql`v(xo*C0c4~qFWXfo&b?sE|IR^8Ht6?NRUgg7?;LbW zGzwq2^5Me=#@Jy4<$as|jhW=+oj&PEv6ofx;kwEB+}5(F#JdE%a<=pOG}H3#p2sFsE96LcFW)9weG7F zvl`c#gY6}POh-ot6&2Oi_O_#=;|Hg4kyvdAGB!323=F({`LdL4k4@$1a0#K-cYCob zSt>dzih)a>NJx#1wY0Za@K`jou%Lv8hfln7T^^CNwYA+cS@Tx3wVhjDcDTS5t6k-{ z>%_sqp|0LM_zs`+@@4kMEvl$U6lUq* zAR4VzSy_4bD}rZiY|KtNB|F>F%xtXM@h1csWGIFp-sIH1ftq?$!V37@w1)~EZw*fsq` zxqEt=+`a36ygiH)fm@Z2^!An(7ScT|CDaaecAmwsad7BnI^ zLY@ixtgWLHf?#K3bC{^RK-in@=Frq^1^4eh;>gBJ1l^&*FDWZ~M@{Y5utm^{$@s^Q zAJ3i_=arL?AZZKS5J1AR-@SVm8+$HJg78Trm(0%2{vxHeR^fT;7tt+b_|cL7wz!Ln z3tQ7l>sjQE$qVh*dwY9wZnL5m4V+g%qk`e%<8$WBnfv$epBFcKr4pnpp9ii8?j2GM zx@oVy*V9u{Qqt4h+}zr#siPCw zJC}P~njL#!l1z5Aw!R3d3Ls@%Di3tM(gSH?7cJt=V*x1<3 z+3w1Uii5pr66pHpgr|i5u`xx{1mg>`vhF!M^B@qxH{#;sx3{NEq#I`spEOB@|DJrTZ1C34=jn!_kl7x6ABqW4{+6D(%NCb59 z(f(X!rlL8 zwTS1fva+(1l-RiZe4!^8^1uLCsE~ddu)eW!>ozNEYum0@AzS3`)=!UtLs+-PsKM+X zJz8E_iPXq>_Uu_=;!us-9P0eIC;8;$L{G5t{d*S7U2}8&yj!_BIX0gvh(zN0bemMN z9zA_@S6A2N+i$KZD5%4LGQE~ZLJICbc%Yx5Xso98xuwOXGf`}4XlSH>tZ*ytIq(%= zH5Y42N>;m5uU;$G6+kjXxcxl|V7>`gicVO|0tWN;t+ptuI*f)&4U3JA3RUHubge;P zlrtIm6kR5pp0QjhtIU;xYbZLygeRk8HkxB^2dDJlL~7=*iZtAAi1;U;i(S!wAy_l3Be94j3i9Wyh|#os=P=HRWS zCQWAVbt-*QGepH1$#^g|H8nJJ2ZECIR+pElp;xJ?Ui3zdv1w_XTwDYb6Zywe8Y(J{ zz@Mlf^Lk$+0zqsA6b`ShZe5nfKz)%Z{Fj=k>Cd}-k(7rCYaifBYP<;eDf}}g_4B6& z2HTC8VAR*>PgLOivGc&P=8d>uNG2xo+!k!=S93&7O^v#3V?lwAvGM+BrEUGZjje4` zLIU&o^OS}F4ic6hQWa$_wP*}npK5KE*5bA@`{?p(?N{?f(}=aTHNV|eY^L%t*l6HZ z8xp|?K_MX?d3P9QZ`_L_CnpCasRrX@cPH=P-BbF5w zKH6Cx#bUAZe*Bj&xBvJ7;vfjfbL9QP!UAY9UtixV_>!X1((6yu)YL$lPy!E&-@bKpEKYt7BhY%f+P_LjkiOr+%);`L<}B;vmZ^n>v#qVy(oiw@$adj^ zBc;VF*3p%t`FRLsMxg3w%;@* zD;yzi_OY*}Nr{5X%4?E73hT^=u?LoW+Upg=eC!PYYFE}G3P5xMfCVb{* zH!@O#K;Q~s1d^epjlibLs=M{+GxRt1&qm#ow z+F~*?Mp!I;YEBbx5}c8d(aX(E9nIY+3~z65*Txzc^peTv+CxG@Mt)Kp*?cRU9URgU z5{Mm)fD{Jvgm8`dL$Iyvh5}OuyuBfQ!Mb?`) zvr|){zt1oUDh3=>m6xBh?gzVZ)qY4+aYxe5-aaWYac4s2#h$;i)hcRBU#7OE=8~Xb z&nwC1iHQj^ncUWv53;DD0{K0buPH>apX2-7x;HSN5$_}oe#akG1*V@GciDFaorl$v z8FkRfQKLyGW6e6VQfzQ;((pE3JIv1a*LL1VX?<|0Mxkbtn46MZCD3w28aBwCB@t_p}`! z#SCEmf5e|292_vyd`FVLWfU$s;j*gB#RrnH|A8sh}vU3JNLR#Qq zwE6Pwf&q}XukYNxZT;}!mh%U7N~I;UjX$I%JXU-frp{7|=qBzFV;LIKify z22TY)`0>}@hb=A*mx3LUPmjq!O9#fE&R|#eUQ-1|Y--ApZ!w^WH#E#r2bGmB3Pu22 z^h|%AxSHcv(P-PtJ@6I-Q&Lj;GhRDPXggwsFeCl_p@Ihy%u2BnXn=x@JjyLvGsj^# zVFw3?<#S&+FH(1I25Weh~Kd_p>i8a54y?(MT5MfCEDV1LuRS1r`<-mE$d@ z5Y@Gv9VcgJm7tTliVAeJ*5<}WVNsETo!#B{k656|d2%k$3r0AXciR5ndUJo;#I&?% zEId9R(QH{cDuC26GTLqmIRyo8Y`DVsZg@8O@4KoTc`}`LKm638qy|>2o^W#cTPx(o zen4H*&IuR*ToAjV7<6K0Y<$58j(HUyAC^+kK!s0fpTF+txB{p|!n|%|bkx|)tSCR< zYvXr2-^L7pQ8u;_FviA~r>Cb^S7SQB5v0Gr|G;)r>C7qO8VFTZR@NIgZUD~jj~>jL z2K*u}F77U$uAd)tu#hh-=O64%c@q#WmYT17$ohG+;YoH7h>qM_1?p8#P7}-Q zKNZ5iHdXb`x8vs{)&Zw1e9zx?;*5$!MP>LuX)p)01!C9e?p)}Q7m_0;y6`jMm_JQOgxK|6gUX=r3LGdo*iRuiWu z*eJGAzr^+^sufHGm;6fXg&F7J`v@_R$5T-UKCsc#qa?CLkwP6Y6dN1)F z5vy^+QIU}gyJ`F1A}ql)VrHMR|K1uvHFBtDHg072a+aj3yR|9pc)j2Gqgs!?fB%a} zK95JXRWm#TVgw-27#QH^r@$%~oZ1&dB3+e{nc3W*nVA8t3+iGgO{U$-Rk@%Mby6Jm zdunm;UBCVAHyhVsW|bQ6%mSsSB;=p@d0`Qe9GoynhGt`>hjqP{Z0dWe52EOf7`0X< VH&7ie0^naPNJmp&qXcs=^nV8pON0Ob literal 4795 zcmWky2RM{}9DgNTQ7(I>v$D7Bd51I4ri>B_83~yg>5QYYLgWa^3fU{8vqhXZRAhHH zk^Y(gU+?qWz3+3+`~24Tv%ZHj#h@>o=Qs~R&;@-xZF6uB0v{vT8SpKp zT9!fC8}{y&7HG~K>{*6$ye}hT-uGQ3XlYUzDXsUF2$j=HFeMfXxrsK8u)x=z7Z+cr z>S}hJI^XDAIB%^~JDy*6oe74BzjF>w(v0NaJ$_l)Abr+1uR8cqI63rZ+aLVgP^+w8 zZtx}?fyLwT=g*%vFff?C64&kYSX1gY;p{fW7EBw061tsaGVLW;MUVgf%uP#6YiVwd zDIq1QAGmeLGiPRI?(gsSxp{eAe%mZ{w9|X#=V$zvFJEZs>Cw869v%7E#6ONZVNB?L zrEs6S%9a8O4-ao^YvX4)$6i`m+UZbGSNBj;GqSZ+EukApjrD01?cP4sj`%%pGf{b~ z{o$JRt;Aoye!YH;2n!1f4L#iW)&Q0RXW! zKaY&~3}szgT3RYrm6MYb7Z+Dm{SID+I+lDhByV}&yT`%C7PRrT?ir_o(g)NZ8g)D=nm1|Lob&_a?vHU%w=7e&}`hq zAjdKE@#Ea#R{Nj5y*EU+n3$NIogFhXGbqw^I7bTx&dpuUR$E)!+q)toBcrJ)`2KxK zEF9T)x5m%cm;VBcC$aa-*x1q0?l2G5W1`}ktSlq!?6wz|qK_sT{d0Y)=FirTKfiw2 zR=b=N`Ln$}GCqDyT3TOE502ALPfy2SFzoE?CnqN&A|lJn%h$1YKBePTgUv_T*pFV3 zXJ&318h(;&KVmT8x8-M`qNcXCvEkeLy*6=paDap@%+Cukoloq20zWx9+=3$i`!5KV zcU|nR6q~THFdRuq`J~*gA)i)7S(%BM+0W09m^Y}6g2~Ft;>Zh9BVZ2w(g-y9qq`|DFrj>gBvax@~;12?}@a90W#roVanHU^8u#>6NqDnbyb zmy?sz$P_w}n~H|U#@f24tLsHZ#*gNQw7;EUv@Bwp4q9er$yHTV&CSXpfqs4}q5EPv zvEO=nsHf#pOf4b<9%j}QM8Fu?MjJVBvQPZ}B;T3T9CQW$cF z(M4`@S&Mb%ejk^Y??RELLZ0sKS^|J1EG#U(oY;BCkC{eqQ&SnM&z(gY85#Ne?|lf~ zeOF%YI+RrxejKunTu&j9NcyQ)Z!ghNqr3}YOy_k>Oz4Yt9ko)F)q}QQ<8b}`se;5g zuz+0kuz@+B+PXRl2<-c#Qsn#VVpLRAXml^&mt{(J_PfeTjcqGHyy1a?__(+@9PY-4 zpsKVq=2t^^Yo^HWOodbf)+bMn4;4HoA*j)RC1ntytgMW~;gESr+PoA{j(S*p(MKqf zKp;d$LM2FN=Y<4T$@!;J&>KeMqAvvn1yw51Mpprall9I*jbVoY7|iq7Sel$h7n$Id z(L&eH*$)B&NaN!=3;go>Nx1s@`q|mpq@<*z2QBm0*e%IOC8;i_yyLYd8YTcp;WBgKTt_#Nq_zLFlyHZHcDRtq(1(R$= z3Z8dmWq$tt{0ulCUPf1U=erZGGt1C)K3pSJU4OT~9{{_pqeGQu@C=7b<}hbqWE8|? z_c>JoNs*D2t*fp5{{1@w%gxRGa`p2Qd~u#q3!6EBQa@P!Tm3Rmtn?ViFQ8IBhr*9D|LG;1U83YqXcZ zCJp~Y!RWbF8-14y*4Nzxvf_SLxK>>Ud(x4|V|q{JfOer!ol`Zg7A2M?7GP?wi)b+x zKFWu%Ak9Map`jt1HZP>9udi=mVKISO}==rns~d1RjA6JW{{H zuITYd5Ychz(S>ePbMw)enTrr2wZFBs6@qAK6WTO-l9IEtxi~rPtgYpPe=T-&bl_D2 z&pP3qyA+otVTo zVT^z~?w>M>Go3fdQN?i=pGLiT!@n1=7$0=>-ve*&&F${{?(SyR*5Nzz-H`g!)D&2x zfPlcC&1sZ?HWaDH|F!YK0w~vysq6=q5B~mIDnKVb_vYl~E5ln4#=gu8={X0$ZKqDZ2u4FUy-R0H8pkb^UJ_;B_t#+U%sp<#=^3r{QQd}d8pUT%~{&KJW-bh_(Zy$r12Q^ zR*)FWr~ZETPwC=t0szd&i0KPAP{^nGweR1@J$n{?Z1FZ_Z#h-a1cE?;IDHL`jje2K zdWAgcd`rf_(o9TDToy`L1(cPP*qc^XR+Lm!_*4`X*+Qf4Ty1XuucxP{$Rt;H39xB@ zZ;v0~SelLQsYr^UWphglD-+XTwo(nKw4&mFeaU=KBn>^c<8*#b4!5ou2CrP#))wwK zz*L|>OG_)vG+?4}jAaP{(h{tC)4}0#LU+pg$znZxx9f&vR9)RQnX&Ql>FMcYHTTgs zKZkP_6cn84hJknjtA8e_PVMEjQC%(b&jPY9#XQCtn3xO$NZZ-jq0wkpSJ#M$(}973 z(o&H@bi6v%FCmM;+};IY5fP^v6a%jI&L@^k|LqQOF3;95`of#|J{K95TfeAi1epgN zrGiws`^Uy=tEw*XG1FWXp@4wmXlZEy&41wU58x*!C8g+3hQAu(b{vgQmBGt<*@lLO z1_deNF*N_w^k!=a^HfUGH^N7fD61TYxV$`zO4n$-tU5>^L?RD}Iu=4N4h}-L<;_;+ z=d14yag@BetfL?$r3Xmi?|&9jR8h%Q3HqJ zoDdfWtA)qL7GvSwUu$u?1$nnc)YL9R+l&2-{st-PI?fkuvFnL4Y55BGr<=PSr7SHi zNAOY0$dryR1mNYw6@M^g_V4_U@2jgBE`Obzd`-cHWaH+Z2^=!@m0FiPnQ09*o1o#@ z+u7+K9;Sg4>g(le7nR?U!I)8+2%t66@`jf=LPA2aUcI8R+DancIwFy*A8T$e4{=6B zM8xe7b#!!6zMs;3V3d=W2Z_QzFc1Yhy|Z=i-o0W=5!=y|$iOH701$8TZuA@)r9Ky) zwY~i}^7J`9j+=*$m#C(uHu-&Jw}(A)8fyz-^!+qZA@9u_nA z>GIc-LO8<(+1QQc!uyz>+-eCB7ZM^5q=|xLeCN&`H~~23jqBG3Uny*T#;YW-h=&{> z)E$jXt~ZyK4uG`VpCa%`T|-RF$k4 z#>U>=Z2j8X>)IJ}!Cs=FynLhMF{R(~puVy39VxcIfB%|aG`BcNCTcIl8c7EMBX}Wf zLH0j*Yy1ju1E8+oQHp_qA-|yDh8Rn--qBiR`=V~RVF?qM#%B%*pBLKr>zy9X%%A z_qkM?3W-TdP7sN>xVWTy5?3kGRz_I)UgLTS!eWjSK3Z8?CJ{*_YN$iqEC0)i;={qw z>S^E|4vjt^2M5LE<>diBczFpE6AkSN8HY`I!uQG~z(ola4k9xXIfxIgpM^J*%N)c)|{ zLz@cw8^HVR>=MqN0YSpl!lJWcbq#?7Cx7MYixP9hedd9a{Z zHFt;3K#rnQY(@4rZj`)v1G<255-B|+16^odct8dr_0|DYcn%dFuAXV6%O7;}CigSl z!@VyiW>>_OYOAL_Sy@>x#_q0;i`It69gsl?1%d7N-d^8&!JWPUN=nM)*|g3%Z8W-o z0K{}{Wo784bU}6Xuih&W{BRfu%nl9?84?cW*4A%{ZlJ>il{7XsF0-kmhPX7sxvYej z5LOfaDu;T@W-mhIx)?ijH&u@xG;mL7=+8i)H9%m=yCa~h>VGQ6M@(tgk7!SPp&|dB zen?B=q~L0ZX_6>)Wmy@RSxfE|I4!UavrYt7NlD4vcyLbndw; zVomuOo>9(6tdsGva8*G;*Pf^Bk~crF(crjMLVkX{X=P{k$wek1J{}_P5@ZN$f#AoJ z$7H_v{QP_~%wEu#3jKL!0iqArDt^vUKD&cK+*st9Y7c&fozA@zM>LURyC32z_2z=0 zt_E=dvqcwEJJ%&7XuC5tB38!`_j*c1jo`M;6jYj*; z&FK~j=-+<;S1M;gKm_4Y+&V88+q-bX*0v4xS3TxrzM-xTc2-q4|9Ki|Cb^YS1GocnVI7agxn^h+Ul&2Vsvyg2uh** z>+G?eO5sP1Mh#||TKjA6ckeC>=01vA-`m?$@>_l#R`KIQaOd5cD$GL5R$C45YAGqr zUF)-%p~nX9rhrim-qZJhUpYJTHJM0-`zU7fp`W|CxxLKFs<3Y|Uw+;VJ>94MH2I^^ z$+XdDju3N!(TwkZ7)4}95_+o5PEtNmRY2mYsvA6(}phoA|NY&vL2hHQ1ri( z?BukWEkcEcggoa`lIi%mOco3gyKnzE_o7 pict +;; the elements of pattern-binds/sc that are pairs are bindings (ie "x = ") +;; and the elements of pattern-binds/sc that are just picts are just plain side-conditions +(define (side-condition-pict fresh-vars pattern-binds/sc max-w) (let* ([frsh (if (null? fresh-vars) null @@ -264,16 +267,17 @@ fresh-vars)) (basic-text " fresh" (default-style)))))] [binds (map (lambda (b) - (htl-append - (car b) - (make-=) - (cdr b))) - pattern-binds)] + (if (pair? b) + (htl-append + (car b) + (make-=) + (cdr b)) + b)) + pattern-binds/sc)] [lst (add-between 'comma (append binds - side-conditions frsh))]) (if (null? lst) (blank) @@ -293,8 +297,8 @@ (define (rp->side-condition-pict rp max-w) (side-condition-pict (rule-pict-fresh-vars rp) - (rule-pict-side-conditions rp) - (rule-pict-pattern-binds rp) + (append (rule-pict-side-conditions rp) + (rule-pict-pattern-binds rp)) max-w)) (define (rp->pict-label rp) @@ -737,21 +741,21 @@ [eqns (select-cases all-eqns)] [lhss (select-cases all-lhss)] [scs (map (lambda (eqn) - (if (and (null? (list-ref eqn 1)) - (null? (list-ref eqn 2))) + (if (null? (list-ref eqn 1)) #f (side-condition-pict null - (map wrapper->pict (list-ref eqn 1)) (map (lambda (p) - (cons (wrapper->pict (car p)) - (wrapper->pict (cdr p)))) - (list-ref eqn 2)) + (if (pair? p) + (cons (wrapper->pict (car p)) + (wrapper->pict (cdr p))) + (wrapper->pict p))) + (list-ref eqn 1)) (if (memq style '(up-down/vertical-side-conditions left-right/vertical-side-conditions)) 0 +inf.0)))) eqns)] - [rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 3))) eqns)] + [rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 2))) eqns)] [linebreak-list (or current-linebreaks (map (lambda (x) #f) eqns))] [=-pict (make-=)] diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss index ed3744370d..f0ae73e8d7 100644 --- a/collects/redex/private/reduction-semantics.ss +++ b/collects/redex/private/reduction-semantics.ss @@ -1074,177 +1074,180 @@ (raise-syntax-error syn-error-name "no clauses" orig-stx)) (prune-syntax (let ([lang-nts (language-id-nts #'lang 'define-metafunction)]) ;; keep this near the beginning, so it signals the first error (PR 10062) - (let-values ([(contract-name dom-ctcs codom-contract pats) - (split-out-contract orig-stx syn-error-name #'rest relation?)]) - (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats] - [(lhs-for-lw ...) - (with-syntax ([((lhs-for-lw _ ...) ...) pats]) - (map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x))) - (syntax->list #'(lhs-for-lw ...))))]) - (with-syntax ([((rhs stuff ...) ...) (if relation? - #'((,(and (term raw-rhses) ...)) ...) - #'((raw-rhses ...) ...))]) - (parameterize ([is-term-fn? - (let ([names (syntax->list #'(original-names ...))]) - (λ (x) (and (not (null? names)) - (identifier? (car names)) - (free-identifier=? x (car names)))))]) - (with-syntax ([(rhs/lw ...) (map to-lw/proc (syntax->list #'(rhs ...)))] - [(lhs ...) #'((lhs-clauses ...) ...)] - [name (let loop ([name (if contract-name - contract-name - (car (syntax->list #'(original-names ...))))] - [names (if contract-name - (syntax->list #'(original-names ...)) - (cdr (syntax->list #'(original-names ...))))]) - (cond - [(null? names) name] - [else - (unless (eq? (syntax-e name) (syntax-e (car names))) - (raise - (make-exn:fail:syntax - (if contract-name - "define-metafunction: expected each clause and the contract to use the same name" - "define-metafunction: expected each clause to use the same name") - (current-continuation-marks) - (list name - (car names))))) - (loop name (cdr names))]))]) - - (with-syntax ([(((tl-side-conds ...) ...) - (tl-bindings ...) - (tl-side-cond/binds ...)) - (parse-extras #'((stuff ...) ...))]) - (with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...) - (map (λ (sc/b rhs) - (let-values ([(body-code cp-let-bindings) - (bind-withs - syn-error-name '() - #'lang lang-nts - sc/b 'flatten - #`(list (term #,rhs)))]) - (list cp-let-bindings body-code))) - (syntax->list #'(tl-side-cond/binds ...)) - (syntax->list #'(rhs ...)))] - [(((rg-cp-let-bindings ...) rg-rhs/wheres) ...) - (map (λ (sc/b rhs) - (let-values ([(body-code cp-let-bindings) - (bind-withs - syn-error-name '() - #'lang lang-nts - sc/b 'predicate - #`#t)]) - (list cp-let-bindings body-code))) - (syntax->list #'(tl-side-cond/binds ...)) + (let-values ([(contract-name dom-ctcs codom-contract pats) + (split-out-contract orig-stx syn-error-name #'rest relation?)]) + (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats] + [(lhs-for-lw ...) + (with-syntax ([((lhs-for-lw _ ...) ...) pats]) + (map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x))) + (syntax->list #'(lhs-for-lw ...))))]) + (with-syntax ([((rhs stuff ...) ...) (if relation? + #'((,(and (term raw-rhses) ...)) ...) + #'((raw-rhses ...) ...))]) + (parameterize ([is-term-fn? + (let ([names (syntax->list #'(original-names ...))]) + (λ (x) (and (not (null? names)) + (identifier? (car names)) + (free-identifier=? x (car names)))))]) + (with-syntax ([(rhs/lw ...) (map to-lw/proc (syntax->list #'(rhs ...)))] + [(lhs ...) #'((lhs-clauses ...) ...)] + [name (let loop ([name (if contract-name + contract-name + (car (syntax->list #'(original-names ...))))] + [names (if contract-name + (syntax->list #'(original-names ...)) + (cdr (syntax->list #'(original-names ...))))]) + (cond + [(null? names) name] + [else + (unless (eq? (syntax-e name) (syntax-e (car names))) + (raise + (make-exn:fail:syntax + (if contract-name + "define-metafunction: expected each clause and the contract to use the same name" + "define-metafunction: expected each clause to use the same name") + (current-continuation-marks) + (list name + (car names))))) + (loop name (cdr names))]))]) + + (with-syntax ([(((tl-side-conds ...) ...) + (tl-bindings ...) + (tl-side-cond/binds ...)) + (parse-extras #'((stuff ...) ...))]) + (with-syntax ([(((cp-let-bindings ...) rhs/wheres) ...) + (map (λ (sc/b rhs) + (let-values ([(body-code cp-let-bindings) + (bind-withs + syn-error-name '() + #'lang lang-nts + sc/b 'flatten + #`(list (term #,rhs)))]) + (list cp-let-bindings body-code))) + (syntax->list #'(tl-side-cond/binds ...)) + (syntax->list #'(rhs ...)))] + [(((rg-cp-let-bindings ...) rg-rhs/wheres) ...) + (map (λ (sc/b rhs) + (let-values ([(body-code cp-let-bindings) + (bind-withs + syn-error-name '() + #'lang lang-nts + sc/b 'predicate + #`#t)]) + (list cp-let-bindings body-code))) + (syntax->list #'(tl-side-cond/binds ...)) + (syntax->list #'(rhs ...)))]) + (with-syntax ([(side-conditions-rewritten ...) + (map (λ (x) (rewrite-side-conditions/check-errs + lang-nts + syn-error-name + #t + x)) + (syntax->list (syntax (lhs ...))))] + [(rg-side-conditions-rewritten ...) + (map (λ (x) (rewrite-side-conditions/check-errs + lang-nts + syn-error-name + #t + x)) + (syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))] + [dom-side-conditions-rewritten + (and dom-ctcs + (rewrite-side-conditions/check-errs + lang-nts + syn-error-name + #f + dom-ctcs))] + [codom-side-conditions-rewritten + (rewrite-side-conditions/check-errs + lang-nts + syn-error-name + #f + codom-contract)] + [(rhs-fns ...) + (map (λ (lhs rhs/where) + (let-values ([(names names/ellipses) + (extract-names lang-nts syn-error-name #t lhs)]) + (with-syntax ([(names ...) names] + [(names/ellipses ...) names/ellipses] + [rhs/where rhs/where]) + (syntax + (λ (name bindings) + (term-let-fn ((name name)) + (term-let ([names/ellipses (lookup-binding bindings 'names)] ...) + rhs/where))))))) + (syntax->list (syntax (lhs ...))) + (syntax->list (syntax (rhs/wheres ...))))] + [(name2 name-predicate) (generate-temporaries (syntax (name name)))] + [(((bind-id/lw . bind-pat/lw) ...) ...) + ;; Also for pict, extract pattern bindings + (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x)))) + (extract-pattern-binds x))) + (syntax->list #'(lhs ...)))] + + + [((where/sc/lw ...) ...) + ;; Also for pict, extract where bindings + (map (λ (hm) + (map + (λ (lst) + (syntax-case lst (side-condition where) + [(where pat exp) + #`(cons #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))] + [(side-condition x) + (to-lw/uq/proc #'x)])) + (syntax->list hm))) + (syntax->list #'(tl-side-cond/binds ...)))] + + [(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...) + ;; Also for pict, extract pattern bindings + (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x)))) + (extract-term-let-binds x))) (syntax->list #'(rhs ...)))]) - (with-syntax ([(side-conditions-rewritten ...) - (map (λ (x) (rewrite-side-conditions/check-errs - lang-nts - syn-error-name - #t - x)) - (syntax->list (syntax (lhs ...))))] - [(rg-side-conditions-rewritten ...) - (map (λ (x) (rewrite-side-conditions/check-errs - lang-nts - syn-error-name - #t - x)) - (syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))] - [dom-side-conditions-rewritten - (and dom-ctcs - (rewrite-side-conditions/check-errs - lang-nts - syn-error-name - #f - dom-ctcs))] - [codom-side-conditions-rewritten - (rewrite-side-conditions/check-errs - lang-nts - syn-error-name - #f - codom-contract)] - [(rhs-fns ...) - (map (λ (lhs rhs/where bindings) - (let-values ([(names names/ellipses) - (extract-names lang-nts syn-error-name #t lhs)]) - (with-syntax ([(names ...) names] - [(names/ellipses ...) names/ellipses] - [rhs/where rhs/where] - [((tl-var tl-exp) ...) bindings]) - (syntax - (λ (name bindings) - (term-let-fn ((name name)) - (term-let ([names/ellipses (lookup-binding bindings 'names)] ...) - (term-let ([tl-var (term tl-exp)] ...) - rhs/where)))))))) - (syntax->list (syntax (lhs ...))) - (syntax->list (syntax (rhs/wheres ...))) - (syntax->list (syntax (tl-bindings ...))))] - [(name2 name-predicate) (generate-temporaries (syntax (name name)))] - [((side-cond/lw/uq ...) ...) - (map (lambda (scs) (map to-lw/uq/proc (syntax->list scs))) - (syntax->list #'((tl-side-conds ...) ...)))] - [(((bind-id/lw . bind-pat/lw) ...) ...) - ;; Also for pict, extract pattern bindings - (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x)))) - (extract-pattern-binds x))) - (syntax->list #'(lhs ...)))] - [(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...) - ;; Also for pict, extract pattern bindings - (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x)))) - (extract-term-let-binds x))) - (syntax->list #'(rhs ...)))] - [(((where-id/lw where-pat/lw) ...) ...) - ;; Also for pict, extract where bindings - (map (λ (lst) (map (λ (ab) (map to-lw/proc (syntax->list ab))) - (syntax->list lst))) - (syntax->list #'(tl-bindings ...)))]) - (syntax-property - #`(begin - (define-values (name2 name-predicate) - (let ([sc `(side-conditions-rewritten ...)] - [dsc `dom-side-conditions-rewritten] - cp-let-bindings ... ... - rg-cp-let-bindings ... ...) - (let ([rg-sc `(rg-side-conditions-rewritten ...)]) - (build-metafunction - lang - sc - (list rhs-fns ...) - #,(if prev-metafunction - (let ([term-fn (syntax-local-value prev-metafunction)]) - #`(metafunc-proc-cps #,(term-fn-get-id term-fn))) - #''()) - #,(if prev-metafunction - (let ([term-fn (syntax-local-value prev-metafunction)]) - #`(metafunc-proc-rhss #,(term-fn-get-id term-fn))) - #''()) - (λ (f/dom cps rhss) - (make-metafunc-proc - (let ([name (lambda (x) (f/dom x))]) name) - (list (list lhs-for-lw - (list side-cond/lw/uq ...) - (list (cons bind-id/lw bind-pat/lw) ... - (cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ... - (cons where-id/lw where-pat/lw) ...) - rhs/lw) - ...) - lang - #t ;; multi-args? - 'name - cps - rhss - (let ([name (lambda (x) (name-predicate x))]) name) - dsc - rg-sc)) - dsc - `codom-side-conditions-rewritten - 'name - #,relation?)))) - (term-define-fn name name2)) - 'disappeared-use - (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))] + (syntax-property + #`(begin + (define-values (name2 name-predicate) + (let ([sc `(side-conditions-rewritten ...)] + [dsc `dom-side-conditions-rewritten] + cp-let-bindings ... ... + rg-cp-let-bindings ... ...) + (let ([rg-sc `(rg-side-conditions-rewritten ...)]) + (build-metafunction + lang + sc + (list rhs-fns ...) + #,(if prev-metafunction + (let ([term-fn (syntax-local-value prev-metafunction)]) + #`(metafunc-proc-cps #,(term-fn-get-id term-fn))) + #''()) + #,(if prev-metafunction + (let ([term-fn (syntax-local-value prev-metafunction)]) + #`(metafunc-proc-rhss #,(term-fn-get-id term-fn))) + #''()) + (λ (f/dom cps rhss) + (make-metafunc-proc + (let ([name (lambda (x) (f/dom x))]) name) + (list (list lhs-for-lw + (list (cons bind-id/lw bind-pat/lw) ... + (cons rhs-bind-id/lw rhs-bind-pat/lw/uq) ... + where/sc/lw ...) + rhs/lw) + ...) + lang + #t ;; multi-args? + 'name + cps + rhss + (let ([name (lambda (x) (name-predicate x))]) name) + dsc + rg-sc)) + dsc + `codom-side-conditions-rewritten + 'name + #,relation?)))) + (term-define-fn name name2)) + 'disappeared-use + (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))] [(_ prev-metafunction name lang clauses ...) (begin (unless (identifier? #'name) @@ -1430,7 +1433,7 @@ (redex-error name "~a matched ~s ~a different ways and returned different results" (if (< num 0) "a clause from an extended metafunction" - (format "clause ~a" num)) + (format "clause #~a (counting from 0)" num)) `(,name ,@exp) (length mtchs))] [else diff --git a/collects/redex/private/struct.ss b/collects/redex/private/struct.ss index 0627ffa9c3..d080348826 100644 --- a/collects/redex/private/struct.ss +++ b/collects/redex/private/struct.ss @@ -50,27 +50,37 @@ ;; I started to add it, but didn't finish. -robby (define (build-reduction-relation orig-reduction-relation lang make-procs rule-names lws domain-pattern) (let* ([make-procs/check-domain - (map (λ (make-proc) - (make-rewrite-proc - (λ (lang) - (let ([compiled-domain-pat (compile-pattern lang domain-pattern #f)] - [proc (make-proc lang)]) - (λ (tl-exp exp f acc) - (unless (match-pattern compiled-domain-pat tl-exp) - (error 'reduction-relation "relation not defined for ~s" tl-exp)) - (let ([ress (proc tl-exp exp f acc)]) - (for-each - (λ (res) - (let ([term (cadr res)]) - (unless (match-pattern compiled-domain-pat term) - (error 'reduction-relation "relation reduced to ~s, which is outside its domain" - term)))) - ress) - ress)))) - (rewrite-proc-name make-proc) - (rewrite-proc-lhs make-proc) - (rewrite-proc-id make-proc))) - make-procs)]) + (let loop ([make-procs make-procs] + [i 0]) + (cond + [(null? make-procs) null] + [else + (let ([make-proc (car make-procs)]) + (cons (make-rewrite-proc + (λ (lang) + (let ([compiled-domain-pat (compile-pattern lang domain-pattern #f)] + [proc (make-proc lang)]) + (λ (tl-exp exp f acc) + (unless (match-pattern compiled-domain-pat tl-exp) + (error 'reduction-relation "relation not defined for ~s" tl-exp)) + (let ([ress (proc tl-exp exp f acc)]) + (for-each + (λ (res) + (let ([term (cadr res)]) + (unless (match-pattern compiled-domain-pat term) + (error 'reduction-relation "relation reduced to ~s via ~a, which is outside its domain" + term + (let ([name (rewrite-proc-name make-proc)]) + (if name + (format "the rule named ~a" name) + (format "rule #~a (counting from 0)" i))))))) + ress) + ress)))) + (rewrite-proc-name make-proc) + (rewrite-proc-lhs make-proc) + (rewrite-proc-id make-proc)) + (loop (cdr make-procs) + (+ i 1))))]))]) (cond [orig-reduction-relation (let* ([new-names (map rewrite-proc-name make-procs)] diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss index f03ef20d4c..e52093a7f8 100644 --- a/collects/redex/private/tl-test.ss +++ b/collects/redex/private/tl-test.ss @@ -639,14 +639,25 @@ (test (term (f 1 1 1 1 1)) (term 1))) - (let () - (define-metafunction empty-language - [(ex variable_x) - variable_x - (where quote variable_x)]) - - (test (term (ex quote)) (term quote))) + (let () + (define-metafunction empty-language + [(ex variable_x) + variable_x + (where quote variable_x)]) + + (test (term (ex quote)) (term quote))) + (let () + (define-metafunction empty-language + [(f any ...) + (any ...) + (where variable_1 x) + (side-condition #f) + (where (number ...) y)] + [(f any ...) + 12345]) + + (test (term (f 8)) 12345)) ; @@ -924,7 +935,7 @@ (with-handlers ((exn? exn-message)) (apply-reduction-relation red 1) 'no-exception-raised)) - "reduction-relation: relation reduced to x, which is outside its domain") + "reduction-relation: relation reduced to x via rule #0 (counting from 0), which is outside its domain") (let* ([red1 (reduction-relation