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

in oppg05.maude .
in oppg06.maude .

mod REMOVE-RULE is
  protecting META-LEVEL .
  pr TEST-META1 .
  pr TEST-META2 .

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

  *** Add new rule to module
  op addRl : Module Rule -> Module .
  eq addRl (mod Q is I sorts S1 . S2 OS MA E RS endm, R)
         = (mod Q is I sorts S1 . S2 OS MA E (R RS) endm) .

  op removeRl : Module Qid -> Module .
  eq removeRl (mod Q is I sorts S1 . S2 OS MA E RS endm, Q2)
          = (mod Q is I sorts S1 . S2 OS MA E 
              removeRlFromRuleSet (RS, Q2) 
             endm) .

  op removeRlFromRuleSet : RuleSet Qid -> RuleSet .

  eq removeRlFromRuleSet (none, Q) = none .
  ceq removeRlFromRuleSet ((R RS), Q)
       = (removeRlFromRuleSet (R, Q) removeRlFromRuleSet (RS, Q)) 
    if RS =/= none . ---same considerations as in oppg08.maude

  eq removeRlFromRuleSet ((rl T1 => T2 [ label(Q) A ].), Q) = none .
  ceq removeRlFromRuleSet ((rl T1 => T2 [ label(Q2) A ].), Q) 
       = (rl T1 => T2 [ label(Q2) A ].) if Q2 =/= Q .

  eq removeRlFromRuleSet ((crl T1 => T2 if COND [ label(Q) A ].), Q) 
       = none .
  ceq removeRlFromRuleSet ((crl T1 => T2 if COND [ label(Q2) A ].), Q) 
       = (crl T1 => T2 if COND [ label(Q2) A ].) if Q2 =/= Q .

endm


red addRl (META-MATCH, 
     (crl '_-__:_['L1:String,'L2:String,'M:Nat,'N:Nat] 
           => '_-__:_['L1:String,'L2:String, 'M:Nat,'_+_['N:Nat,'Q:Nat]] 
           if '_and_['_<_['N:Nat,'s_^5['0.Zero]],
                      '_>_['Q:Nat,'s_^7['0.Zero]]] 
                            = 'true.Bool [label('extrarule)] .)) .

red removeRl (META-MATCH, 'homegoal) .

red removeRl (META-MATCH2, 'awaygoal) .