*** Solution to Exercise 07, Lecture 3, INF5130
*** Einar B. Johnsen 09.09.09
*** slightly changed by Daniela Lepri 2011.09.14

in oppg04.maude .
in oppg05.maude .
in oppg06.maude .


fmod MY-QID-SET is
    protecting QID .

	---sort QidSet . ---This sort is already defined in prelude.maude ... sort Set{Qid} to QidSet
    sort MyQidSet .
    subsort Qid < MyQidSet .

    op empQS : -> MyQidSet [ctor] .
    op _U_ : MyQidSet MyQidSet -> 
         MyQidSet [ctor assoc comm id: empQS] .

    eq Q:Qid U Q:Qid = Q:Qid .

endfm

mod COLLECT-SYMBS is 
  pr MY-QID-SET .
  pr META-LEVEL . 
  pr TEST-META1 .
  pr TEST-META2 .
  pr TEST-META .

  op getOpSymbs : OpDeclSet -> MyQidSet .
  op functionSymbols : Module -> MyQidSet .

  var Q : Qid .
  var OS : OpDeclSet .
  var I : ImportList . 
  vars T1 T2 : TypeList .
  var A : AttrSet .
  var S1 : SortSet .
  var S2 : SubsortDeclSet .
  var MA : MembAxSet .
  var E : EquationSet .
  var R : RuleSet .

  eq getOpSymbs (none) = empQS .
  eq getOpSymbs ((op Q : T1 -> T2 [ A ] .) OS) 
         = Q U (getOpSymbs (OS)) .

  eq functionSymbols 
       (mod Q is I sorts S1 . S2 OS MA E R endm) 
       =  getOpSymbs (OS) .

  eq functionSymbols 
       (fmod Q is I sorts S1 . S2 OS MA E endfm) 
       =  getOpSymbs (OS) .
endm


---red functionSymbols (META-MATCH) .

---red functionSymbols (META-MATCH2) .

---red functionSymbols (META-MY-NAT) .