*** Solution to Exercise 5, Lecture 3, INF5130
*** Einar B. Johnsen 09.09.09
*** Modified by Daniela Lepri 26.09.2013.

mod MATCH is
  protecting NAT .
  protecting STRING .

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

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

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

  crl [awaygoal] :  L1 - L2 M : N => L1 - L2 M : (N + 1) if N < 5 .

endm


fmod TEST-META1 is 
  protecting META-LEVEL . 

  op META-MATCH : -> Module .
  eq META-MATCH = (mod 'MATCH 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,'s_['0.Zero]]] 
      if '_<_['N:Nat,'s_^5['0.Zero]] = 'true.Bool [label('awaygoal)] .
  endm) .
endfm



--- red META-MATCH .

--- red upModule('MATCH, false) .
--- red upModule('MATCH, false) == META-MATCH .