-- 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 

-- 2) Let Close1(C) = C 

-- 3) Basic Claim: 

--3A) lets prove that the right side is included in the left.  Let [B_.[A'_There are several cases depending on u''.

-- i) Assume u'' = t, hence u' = t also.  Since u' = t [B_.

-- ii) Assume u'' = 

-- iia) v 

-- iib) NOT v 

-- iii) Assume u'' u').  Also, as in case i), u' = u'' 




   


-- 3B) lets prove that the left side is included in the right.  Let [B_.v] be the element of EFF1(

-- i) First, assume v = t 

-- ii) second, assume v cases on u'.

-- iia) assume u' u').

-- iib) assume u' = 

-- 4) Close1([A_production)}).  Hence, I can pre-tabulate Close1([A'_.
-- Proof:
-- i) Using the basic claim: 

-- ii) Thus: Close1([A_

-- iii)  Further: Close1([A_A'_production)}

-- iv) Thus: Close1([A_A'_
 

-- 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.