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

in oppg05.maude .
in oppg06.maude .

fmod MY-QID-SET is
    protecting QID .

    sort MyQidSet .
    subsort Qid < MyQidSet .

  op empQS : -> MyQidSet [ctor] .
  op _U_ : MyQidSet MyQidSet -> 
        MyQidSet [ctor assoc comm id: empQS] .   
  op _ isElementIn _ : Qid MyQidSet -> Bool .  
  *** set difference A remove B = A/B .
  op _ remove _ : MyQidSet MyQidSet -> MyQidSet .

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

  vars Q Q' : Qid . vars QS QS2 : MyQidSet .

  eq Q isElementIn empQS = false .
  eq Q isElementIn (Q' U QS) = (Q == Q') or (Q isElementIn (QS)) .

  eq QS remove empQS = QS .
  eq (Q U QS) remove (Q U QS2) = (QS remove QS2) .
  ceq (Q U QS) remove (QS2) = (Q U (QS remove QS2)) 
        if not (Q isElementIn QS2) .
        
  --- alternative definition with owise
  --- eq (Q U QS) remove (Q U QS2) = (QS remove QS2) .
  --- eq QS remove QS2 = QS [owise] .
        
        
endfm


mod NEW-VARS is 
  protecting META-LEVEL . 
  pr MY-QID-SET .
  pr TEST-META1 .
  pr TEST-META2 .

  op newVarInRHS : RuleSet -> Bool . *** NB. set of rules!
  op newVarInRHS : Module -> Bool .

  op getVars : TermList -> MyQidSet . *** generalized to TermList

  var OS : OpDeclSet .
  var I : ImportList . 
  var S1 : SortSet .
  var S2 : SubsortDeclSet .
  var MA : MembAxSet .
  var E : EquationSet .
  var A : AttrSet .
  var Q : Qid .
  vars T1 T2 : Term .         
  vars TL TL2 : NeTermList .
  var C : Constant .
  var V : Variable .
  var R : Rule .              vars RS : RuleSet . 
  var COND : Condition .

  *** Modules:
  eq newVarInRHS (mod Q is I sorts S1 . S2 OS MA E RS endm)
          = newVarInRHS (RS) .

  eq newVarInRHS (none) = false .
  ceq newVarInRHS ((R RS)) 
          = (newVarInRHS (R)) or (newVarInRHS (RS)) 
     if RS =/= none . ---necessary to avoid infinite recursion          

--- NB if the following equations are used instead of the two above then
--- Fatal error: stack overflow.
--- since a single rule R can be matched by the RuleSet (R none)
--- yieadling an infinite recursion
---  eq newVarInRHS ((R RS)) 
---          = (newVarInRHS (R)) or (newVarInRHS (RS)) .
---  eq newVarInRHS (none) = false .

  --- alternative working solution with owise
  ---(
  eq newVarInRHS ((R RS)) 
          = (newVarInRHS (R)) or (newVarInRHS (RS)) [owise] .
  eq newVarInRHS (none) = false .
  )

  *** Single rules are covered by these two cases:
  eq newVarInRHS (rl T1 => T2 [ A ] .) 
          = ((getVars (T2)) remove (getVars (T1)) =/= empQS) .

  *** Ignores new vars in COND ...
  eq newVarInRHS (crl T1 => T2 if COND [ A ] .) 
          = ((getVars (T2)) remove (getVars (T1)) =/= empQS) .

  *** Uses the function getName : Variable -> Qid from the prelude.
  eq getVars (C) = empQS . *** constant Term
  eq getVars (V) = getName(V) .  *** returns a Qid for a Variable Term
  eq getVars (Q [ TL ]) = getVars (TL) . *** coumpund Term
  eq getVars ((TL , TL2)) = (getVars (TL2)) U (getVars (TL)) .


endm

--- red newVarInRHS  (META-MATCH) .
--- red newVarInRHS  (META-MATCH2) .