-- LR1Items.mesa -- last edit September 11, 1984 3:10:46 pm PDT DIRECTORY GrammarBasic USING[Symbol, Grammar], LR1ItemSetsBasic USING[LR1ItemSubset]; LR1Items: CEDAR DEFINITIONS = BEGIN OPEN GrammarBasic, LR1ItemSetsBasic; GenKernelV1EpsilonItemSubsets: PROC[Grammar, PROC[LR1ItemSubset]]; GenKernelGoTo1ItemSubsetsFromKernelItemSubset: PROC[LR1ItemSubset, PROC[Symbol, LR1ItemSubset]]; GenCloseOfLR1ItemSubset: PROC[firstSubset: LR1ItemSubset, for: PROC[LR1ItemSubset]]; END.. -- I choose to record some claims here that are not recorded elsewhere. Some of these claims are used to support the implementation, and some will be used at a future date. -- The first set of claims has to do with the computation of Close1(A). -- 1) Let Xt([A_a.b, u]) = (IF u = e THEN [A_a.b, t] ELSE [A_a.b, u]); where t is sequence of terminals and length(t) < 1. Extend Xt to sets in the usual way: Xt(A) = U{Xt(a) | a B A}. -- 2) Let Y(C) = {[B_.d, v] | (E A', a', b', u') ([A'_a'.Bb', u'] B C and v B FIRST1(b'u') and B_d a production)}. Notice that Close1(C) = C U Y(C) U Y2(C) U ... -- 3) Basic Claim: Xt(Y(C)) = Y(Xt(C)). Trivial if t = e, so assume t = e. --3A) lets prove that the right side is included in the left. Let [B_.d, v] B Y(Xt(C)). Thus we have A', a', b', u' such that [A'_a'.Bb', u'] B Xt(C), v B EFF1(b'u'), and B_d a production. Let [A'_a'.Bb', u'] = Xt([A'_a'.Bb', u'']), where [A'_a'.Bb', u''] B C. The goal is to find a v' such that [B_.d, v'] B Y(C) and Xt([B_.d, v']) = [B_.d, v], thus proving [B_.d, v] B Xt(Y(C)). There are several cases depending on u''. -- i) Assume u'' = t, hence u' = t also. Since u' = t = e, and v B EFF1(b'u'), we have v = e. So, v' = v will suffice. That is, [B_.d, v] B Y(C) as witnessed by (A', a', b', t=u''=u'), and [B_.d, v] = Xt([B_.d, v]), so [B_.d, v] B Xt(Y(C)). -- ii) Assume u'' = e, hence u' = t, and also [A'_a'.Bb', e] B C. As in case i, since u' = t = e, and v B EFF1(b'u'), we have v = e. Now we examine two sub cases, depending on whether v B EFF1(b'). -- iia) v B EFF1(b'). Hence, v B EFF1(b'e), so [B_.d, v] B Y(C) as witnessed by (A', a', b', e). Finally, v = e implies [B_.d, v] B Xt(Y(C)). -- iib) NOT v B EFF1(b'). Thus, because v B EFF1(b'u'), we have v = u' (= t = e) and e B EFF1(b') = EFF1(b'e). In this case, v' = e satisifies our requirements, because [B_.d, e] B Y(C) as witnessed by (A', a', b', e). FInally, v = t implies [B_.d, v] = Xt([B_.d, e]) B Xt(Y(C)). -- iii) Assume u'' = t and u'' = e. Hence u' = u'', so [A'_a'.Bb', u'] B C, thus [B_.d, v] B Y(C) as witnessed by (A', a', b', u'). Also, as in case i), u' = u'' = e and v B EFF1(b'u') implies v' = e. Thus, [B_.d, v] B Xt(Y(C)). -- 3B) lets prove that the left side is included in the right. Let [B_.d, u] B Xt(Y(C)). Since t = e, we have u = e. Let [B_.d, v] be the element of Y(C), such that Xt([B_.d, v]) = [B_.d, u]. Thus, we have A', a', b', u' such that [A'_a'.Bb', u'] B C, v B EFF1(b'u'), and B_d a production. There are two cases: v = e, and v = e. -- i) First, assume v = e implying that u = t. Also, e B EFF1(b'u'), so e B EFF1(b') and u' = e. So [A'_a'.Bb', t] B Xt(C). Also, t B EFF1(b't), so [B_.d, t] B Y(Xt(C)), as witnessed by (A', a', b', t). -- ii) second, assume v = e, implying that u = v. Thus, [B_.d, v] = [B_.d, u], and we shall prove [B_.d, v] B Y(Xt(C)). Now, cases on u'. -- iia) assume u' = e. [A'_a'.Bb', u'] B C, hence [A'_a'.Bb', u'] B Xt(C), and [B_.d, v] B Y(Xt(C)) as witnessed by (A', a', b', u'). -- iib) assume u' = e. Since v = e and v B EFF1(b'e), we have v B EFF1(b't). Further, [A'_a'.Bb', e] B C, so [A'_a'.Bb', t] B Xt(C). Thus, we have [B_.d, v] B Y(Xt(C)), as witnessed by (A', a', b', t). -- 4) Close1([A_a.b, t]) = Xt(U{Xt'(Close1([A'_.d, e]) | (E A', a', b', u') ([A'_a'.A'b', u'] B C and t' B EFF1(b'u') and A'_d a production)}). Hence, I can pre-tabulate Close1([A'_.d, e]), and make good headway. -- Proof: -- i) Using the basic claim: Xt(Close1(C)) = Xt(C U Y(C) U Y2(C) U ...) = Xt(C) U Xt(Y(C)) U Xt(Y2(C)) U ... = Xt(C) U Y(Xt(C)) U Y2(Xt(C)) U ... = Close1(Xt(C). -- ii) Thus: Close1([A_a.b, t]) = Close1(Xt([A_a.b, e])) = Xt(Close1([A_a.b, e])). -- iii) Further: Close1([A_a.b, e]) = U{Close1([A'_.d, t']) | (E A', a', b', u') ([A'_a'.A'b', u'] B C and t' B EFF1(b'u') and A'_d a production)} = U{Xt'(Close1([A'_.d, e]) | (E A', a', b', u') ([A'_a'.A'b', u'] B C and t' B EFF1(b'u') and A'_d a production)} -- iv) Thus: Close1([A_a.b, t]) = Xt(U{Xt'(Close1([A'_.d, e]) | (E A', a', b', u') ([A'_a'.A'b', u'] B C and t' B EFF1(b'u') and A'_d a production)}). -- 5) It is a fact that all of the sets of LR(0) items and LR(1) items occuring during the construction of the canonical LR(0) graph, the LRLR(1) graph, the canonical LR(1) graph, and the Split Node graphs, are of the form Close(InitialMembers). We choose to record only the InitialMembers, and whenever there is a need to generate the full set, we run the close algorithm. This results in elements occuring in the generation of the closure more than once, but this is no problem. (This choice is that the space savings is of more importance than the time loss.) Even for equality tests, it turns out that for the actual sets constructed, Close(InitialMembers1) = Close(InitialMembers2) IFF InitialMembers1 = InitialMembers2. Êô˜Jšœ˜J˜2J˜˜ Jšœ$˜$J˜&—J˜J˜Jšœ˜˜Jšœ*˜*J˜J˜J˜J˜J˜BJ˜J˜`J˜J˜TJ˜J˜J˜­J˜JšœBÏdœ˜GJ˜Jšœ Ïgœžœžœžœ žœžœFÏmœ žœžœŸœžœŸœ˜ºJ˜Jš&œ žœ žœŸœžœžœ žœžœŸœ Ÿœœžœ žœ#œŸœžœŸœžÏuœŸœ˜¢J˜šœžœžœžœžœžœŸœžœ˜KJ˜šFœGžœŸœžœžœžœžœžœžœŸœžœŸœœžœ žœžœžœ žœžœžœžœžœ Ÿœ,žœŸœžœžœžœ žœžœŸœžœžœ0˜¬J˜Jš)œ7ŸœžœŸœœžœŸœžœ*žœŸœžœžœžœžœžœžœžœŸœžœžœ˜óJ˜JšœžœžœžœžœŸœ ŸœžœŸœœžœŸœžœ8Ÿœœžœ˜Ç˜Jš(œ ŸœœžœŸœœžœžœ žœŸœžœžœžœžœŸœžœ žœŸœžœžœ˜J˜Jš?œŸœœžœŸœœžœŸœžœžœŸœœžœœžœžœžœ*žœžœŸœžœžœžœžœžœžœžœžœŸœžœžœ˜š—J˜Jš.œŸœ ŸœžœžœžœŸœ žœŸœžœžœžœ'ŸœžœŸœœžœŸœžœ žœŸœžœžœ˜è—J˜J˜J˜J˜šœ˜J˜—J˜š5œHžœŸœžœžœŸœžœ Ÿœžœ žœžœžœžœ žœžœžœžœžœŸœŸœœžœ žœ(žœŸœžœ˜ÌJ˜Jš1œžœžœŸœœžœ žœŸœœžœ žœ žœžœŸœžœŸœœžœ žœŸœžœžœžœžœ ˜ÒJ˜šœŸœžœ"žœ žœžœŸœžœžœ˜‹J˜Jš!œŸœžœžœžœŸœžœžœŸœžœ žœŸœžœžœžœžœ˜†J˜Jš3œžœ ŸœžœŸœœžœžœ ŸœœžœžœžœžœŸœ žœžœŸœžœžœŸœžœžœžœžœ˜Ë——J˜š/œ œžœžœžœŸœžœœžœžœŸœžœžœ žœžœŸœ Ÿœœžœ žœ2œžœžœ˜Õšœ ˜ JšAœžœœžœŸœžœŸœž œŸœžœŸœžœžœŸœžœž œŸœžœŸœžœžœŸœž œžœŸœ œžœ˜¡J˜Jšœœžœžœ œžœžœžœžœžœœžœžœžœ˜RJ˜Jš@œœžœžœžœŸœ žœ Ÿœžœžœ žœžœŸœ Ÿœœžœ žœŸœžœœžœžœŸœžœžœ žœžœŸœ Ÿœœžœ žœ˜…J˜Jš)œœžœžœžœŸœžœœžœžœŸœžœžœ žœžœŸœ Ÿœœžœ žœ˜–Jšœ˜——J˜š œ—œœœœ˜Û˜J˜———J˜J˜J˜——…—þø