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

mod MATCH2 is
  protecting NAT .
  protecting STRING .

  op _-__:_ : String String Nat Nat -> Match [ctor] .
  sort Match .

  vars L1 L2 : String .   
  vars M N Q : Nat .

  rl [homegoal] : 
     L1 - L2 M : N => L1 - L2 (M + 1) : N .

*** Note that the exercise asks for this rule, 
*** but Maude does not like it... it is not executable
  crl [awaygoal] :  
     L1 - L2 M : N => L1 - L2 M : (N + Q)
       if N < 5 and Q > 7 .
endm





mod TEST-META2 is 
  protecting META-LEVEL . 

  op META-MATCH2 : -> Module .
  eq META-MATCH2 = (mod 'MATCH2 is
  including 'BOOL .
  protecting 'NAT .
  protecting 'STRING .
  sorts 'Match .
  none
  op '_-__:_ : 'String 'String 'Nat 'Nat -> 'Match [ctor] .
  none
  none
  rl '_-__:_['L1:String,'L2:String,'M:Nat,'N:Nat] => 
     '_-__:_['L1:String,'L2:String,'_+_['M:Nat,
             's_['0.Zero]],'N:Nat] [label('homegoal)] .
  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('awaygoal)] .
endm) .

endm

*** it parses correctly and has non-error sort SModule
*** red META-MATCH2 .
eof


---red in META-LEVEL : upModule('MATCH2, false) .
---red in TEST-META2 : upModule('MATCH2, false) == META-MATCH2 . 







--- NB: the result is false! because of the nonexec attribute 
--- which is added automatically by Maude in the second rule












*** the difference between upModule('MATCH2, false) and META-MATCH2 is
*** the 'nonexec' attribute of the second rule