-- ========================================================================
--    the module GENcases for generating patterns (terms with variables)
--        by combinatorial expansion of alternatives
--        and checking validities of predicates on them
-- ========================================================================

-- ========================================================================
-- a comment starts with '-- ' or '** ' and ends at the end of line
--
-- a convention for commenting:
--   '-- ' is used before the commented CafeOBJ text
--   '** ' is used after the commented CafeOBJ text
-- ========================================================================

-- ========================================================================
-- the module GENcasesNp describe an algorithm 
-- for generating and checking a finite set of patterns 
-- that indicate necessary cases to be analyzed
-- by expanding alternatives indicated by (_;_) 
mod! GENcases {
-- sequences of values (_,_)
[Val < ValSq] op _,_ : ValSq ValSq -> ValSq {assoc} 
** Val is supposed to be a super sort for all the sorts 
** that appears in the generations of the patterns

-- sequences of values indicating alternatives (_;_) 
[Val < VlSq] op _;_ : VlSq VlSq -> VlSq {assoc}

-- sequence of ValSeq or VlSeq
[ValSq VlSq < SqSq]
op empSS : -> SqSq .
op _,_ : SqSq SqSq -> SqSq {assoc id: empSS} 

-- SqSq enclosures SqSqEn and their trees SqSqTr
[SqSqEn < SqSqTr]
op [_] : SqSq -> SqSqEn .
op _||_ : SqSqTr SqSqTr -> SqSqTr {assoc} 

-- expand all combinations of alternatives 
-- indicated by (_;_) into (_||_) 
eq [(SS1:SqSq,(V:Val;VS:VlSq),SS2:SqSq)] 
   = [(SS1,V,SS2)] || [(SS1,VS,SS2)] .

-- importing the built-in module STRING of character strings
-- for indicating the kinds of the following constructors
pr(STRING)
-- constructing terms
op t__ : String ValSq -> Val .
-- generating t_ temrs from SqSqTr
op g__ : String SqSqTr -> VlSq .
eq g(S:String)(SST1:SqSqTr || SST2:SqSqTr) = (g(S) SST1);(g(S) SST2) .
eq g(S:String)[VSQ:ValSq] = t(S)(VSQ) .

-- indicators and their trees
[Ind < IndTr]
op $ : -> Ind .
op _|_ : IndTr IndTr -> IndTr {assoc}

-- indicator constructor
[Info] op i__ : Bool Info -> Ind .
-- making all indicators with "true" disappear 
eq (i true II:Info) | IT:IndTr = IT .
eq IT:IndTr | (i true II:Info) = IT .

-- information constructor
op ii_ : ValSq -> Info .
-- the predicate to be checked for all state patterns
-- should be reified before checking
pred v_ : ValSq .

-- make indicator for v_
op mi_ : ValSq -> Ind .
eq mi(VSQ:ValSq) = (i v(VSQ) ii(VSQ)) .

-- make make indicators (mmi):
-- translating a tree of SqSq (SqSqTr)
-- into a tree of indicators
op mmi_ : SqSqTr -> IndTr .
eq mmi(SST1:SqSqTr || SST2:SqSqTr) = (mmi SST1) | (mmi SST2) .
-- if all _;_ in SqSq disappear
-- then translate mmi to mi
eq mmi[VSQ:ValSq] = mi(VSQ) .

-- checking v_ for all the patterns defined by SST:SqSqTr
-- if it returns '($):IndTr', 
-- it means that the check has succeeded 
-- for all the cases specified by the patterns
op check_ : SqSqTr -> IndTr .
eq check(SST:SqSqTr) = ($ | mmi(SST)) .
}

-- ========================================================================
provide genCases

-- ========================================================================
eof