** -------------------------------------------------------
**   Specification of the type list
** -------------------------------------------------------


module! ElementSpec
{
  [element]
}

module! SimpleListSpec( E :: ElementSpec )
{

  imports { protecting (NAT) }

  signature {
    [list]
  
    op [] : -> list { constr }
    op AddToSimpleList : element.E list -> list { constr }
    ** op [_] : element.E -> list
    op Head : list -> element.E
    op Tail : list -> list
    op _+_ : list list -> list
    op _in_ : element.E list -> Bool
    op Length : list -> Nat 
  }
  axioms {
    vars l m n : list
    vars f e : element.E

    eq Head(AddToSimpleList(e,l)) = e .
    eq Tail(AddToSimpleList(e,l)) = l .

    ** eq [e] = AddToSimpleList(e,[]) .
	
    eq [] + l = l .
    eq AddToSimpleList(e,l) + m = AddToSimpleList(e,l + m) .
  
    eq (e in []) = false .
    ceq (e in AddToSimpleList(f, l)) = true if (e == f) .
    ceq (e in AddToSimpleList(f, l)) = (e in l) if not(e == f) .   
  
    eq Length([]) = 0 .
    eq Length(AddToSimpleList(e,l)) = Length(l) + 1 .
  }
}


module! ListSpec
{
  protecting (SimpleListSpec)

  signature {
    op AddToList : element.E list -> list
  }

 axioms {
   vars e : element.E
   vars l : list

   ceq AddToList(e,l) = AddToSimpleList(e,l) if not(e in l) .
   ceq AddToList(e,l) = l if (e in l) . 
  }
}


** -------------------------------------------------------
**  Specification of the type charorder
** -------------------------------------------------------

module! CharacterOrderSpec
{
  protecting (ListSpec(CHARACTER { sort element -> Character }) * 
  {  
    sort list -> charorder ,
    op AddToList -> AddToOrder ,
    op AddToSimpleList -> NewChar ,
    op [] -> coEmpty
  })
}

** ---------------------------------------------------------------
**   Specification of the type String
**   (StringSpec extends the cafeObj specification of String, i.e.
**   the lexicographical order for strings is taken from cafeObj.)
** ---------------------------------------------------------------

module! StringSpec
{
  imports {
    protecting (STRING)
    protecting (NAT)
    protecting (CharacterOrderSpec)
  }

  signature {
    op Tail : String -> String 
    op Head : String -> Character
    op CheckAlphabet : String charorder -> Bool
    op CheckAlphabetInternal : String charorder -> Bool
    op IsStringSmaller : String String -> Bool 

    op ErrorNoStringLeft : -> String { constr }
 }

  axioms {
    vars s1 s2 : String
    vars co : charorder
 
    eq Head(s1) = schar(s1,0) .
    eq Tail(s1) = substring(s1,1) .

    eq IsStringSmaller(s1,s2) = string<(s1,s2) .

    ceq CheckAlphabet(s1,co) = false if length(s1) == 0 .
    ceq CheckAlphabet(s1,co) = (Head(s1) in co) if length(s1) == 1 .
    ceq CheckAlphabet(s1,co) = CheckAlphabetInternal(s1,co) if length(s1) > 1 .

    ceq CheckAlphabetInternal(s1,co) = false if not (Head(s1) in co) .
    ceq CheckAlphabetInternal(s1,co) = CheckAlphabet(Tail(s1),co) if Head(s1) in co .
 
   
  }
}


** ---------------------------------------------------------------------
**   Specification of the type rules
**   (In the cafeObj implementation there is the following restriction
**   according to our loose specification: a rule must consist of 
**   exactly two characters.
** ---------------------------------------------------------------------

module! SimpleRuleSpec
{
  protecting (ListSpec(StringSpec { sort element -> String }) * 
  { 
    sort list -> rules , 
    op AddToSimpleList -> NewRule , 
    op [] -> rEmpty,
    op AddToList -> AddFlexibleRule 
  })
}

module! RuleSpec
{
  imports {
    protecting (SimpleRuleSpec)
    protecting (BOOL)
    protecting (NAT)
  }

  signature {

    op AddToRules : String rules -> rules
    op MatchRule : String rules -> Bool  

    op FindPatternIntern : String String -> Bool
    op IsPatternIntern : String String -> Bool

  }

  axioms {
    vars str r : String
    vars R : rules

    ceq AddToRules(str,R) = AddFlexibleRule(str,R) if length(str) == s(1) .
    ceq AddToRules(str,R) = R if not length(str) == s(1) .

    eq MatchRule(str,rEmpty) = false .
    ceq MatchRule(str,NewRule(r,R)) = true if IsPatternIntern(str,r) == true .
    ceq MatchRule(str,NewRule(r,R)) = MatchRule(str,R) 
          if not IsPatternIntern(str,r) == true .

    ceq IsPatternIntern(str,r) = false if length(str) <= 1 .
    ceq IsPatternIntern(str,r) = FindPatternIntern(str,r) if length(str) > 1 .

    ceq FindPatternIntern(str,r) = true 
         if Head(str) == Head(r) and Head(Tail(str)) == Head(Tail(r)) .
    ceq FindPatternIntern(str,r) = IsPatternIntern(Tail(str),r) 
         if not (Head(str) == Head(r) and Head(Tail(str)) == Head(Tail(r))) . 
 
  }
}

** -----------------------------------------------------------
**   Specification of the type language
** -----------------------------------------------------------

module! LanguageSpec
{
  imports {
    protecting (CharacterOrderSpec)
    protecting (RuleSpec)
  }

  signature {
    [language]

    op MakeLanguage : rules charorder -> language
    op GetRules : language -> rules
    op GetCharacterOrder : language -> charorder
  }

  axioms {
    vars co : charorder
    vars r : rules

    eq GetRules(MakeLanguage(r,co)) = r .
    eq GetCharacterOrder(MakeLanguage(r,co)) = co .
  }
}


** -----------------------------------------------------------
**   Specification of the type word
** -----------------------------------------------------------

module! WordSpec
{
  imports {
    protecting (StringSpec)
    protecting (LanguageSpec)
  }

  signature {
    [word]

    op MakeWord : String language -> word
    op GetString : word -> String 

    op ErrorMisspelled : -> word { constr }
    op ErrorNoWordLeft : -> word { constr }
    op DummyValue : -> word { constr }

    op CorrectWord : String -> word { constr }
  }

  axioms {
    vars s : String
    vars l : language

    eq GetString(CorrectWord(s)) = s .
    eq GetString(ErrorNoWordLeft) = ErrorNoStringLeft .

    ceq MakeWord(s,l) = CorrectWord(s) 
          if (not MatchRule(s,GetRules(l))) and CheckAlphabet(s,GetCharacterOrder(l)) .

    ceq MakeWord(s,l) = ErrorMisspelled 
          if not ((not MatchRule(s,GetRules(l))) and CheckAlphabet(s,GetCharacterOrder(l))) .
  }
}


** ----------------------------------------------------------------
**  Specification of the type pair, pairlist, and listofpairlist
** ----------------------------------------------------------------

module! PairSpec
{
  imports {
    protecting (StringSpec)
    protecting (WordSpec)
  }

  signature {
    [pair]
    op MakePair : word word -> pair { constr }
    op GetNative : pair -> String
    op GetForeign : pair -> String

    op CheckWords : word word -> Bool
  }

  axioms {
    vars n f : word


    ceq CheckWords(n,f) = true
          if not n == ErrorMisspelled and not f == ErrorMisspelled .
    ceq CheckWords(n,f) = false
          if n == ErrorMisspelled or f == ErrorMisspelled .


    ceq GetNative(MakePair(n,f)) = GetString(n) if CheckWords(n,f) . 
    ceq GetForeign(MakePair(n,f)) = GetString(f) if CheckWords(n,f) .

  }
}

module! PairListSpec
{
  protecting (ListSpec(PairSpec { sort element -> pair }) * 
  { 
    sort list -> pairlist , 
    op AddToList -> AddPair ,
    op AddToSimpleList -> NewPair,
    op [] -> plEmpty

  })
}

module! ListOfPairListsSpec
{
  protecting (ListSpec(PairListSpec { sort element -> pairlist }) * 
  { 
    sort list -> listofpairlists , 
    op AddToList -> AddPairList ,
    op [] -> lplEmpty,
    op AddToSimpleList -> NewPairList
  })
}


** ------------------------------------------------------
**   Specification of the type vocitem and listofitems
** ------------------------------------------------------

module! VocItemSpec
{
  imports {
    protecting (PairSpec)
  }

  signature {
    [vocitem]
    op MakeItem : pair Bool -> vocitem
    op GetPair : vocitem -> pair
    op GetFlag : vocitem -> Bool
    op ErrorOutOfEntries : -> vocitem
  }

  axioms {
    vars vi : vocitem
    vars p : pair
    vars f : Bool

    eq GetFlag(MakeItem(p,f)) = f .
    eq GetPair(MakeItem(p,f)) = p .
  }
}
 

module! ListOfItemsSpec
{
  protecting (ListSpec(VocItemSpec { sort element -> vocitem }) * 
  { 
    sort list -> listofitems , 
    op AddToList -> AddItem ,
    op [] -> liEmpty,
    op AddToSimpleList -> NewItem ,
  })
}

** ---------------------------------------
** Specification of the ListOfStringsSpec
** (needed for the user interface when the
**  user enters translations in the test
**  suite).
** ---------------------------------------

module! ListOfStringsSpec
{
  protecting (ListSpec(StringSpec { sort element -> String }) *
  {
    sort list -> listofstrings ,
    op AddToList -> AddString ,
    op [] -> lsEmpty,
    op AddToSimpleList -> NewString
  })
}

module ListOfStringListSpec
{
  protecting (ListSpec(ListOfStringsSpec { sort element -> listofstrings }) *
  {
    sort list -> listofstringlist ,
    op AddToList -> AddStringList ,
    op [] -> lslEmpty,
    op AddToSimpleList -> NewStringList
  })
}

module! ListOfListOfItemsSpec
{
  protecting (ListSpec(ListOfItemsSpec { sort element -> listofitems }) * 
  { 
    sort list -> listoflistofitems , 
    op [] -> lliEmpty,
    op AddToList -> AddToItemListsList ,
    op AddToSimpleList -> NewItemListsList
  })
}