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

fmod MY-NAT is
  sort Nat .
  op 0 : -> Nat [ctor] .
  op _+_ : Nat Nat -> Nat [assoc comm] .
  op s : Nat -> Nat .
  vars M N : Nat .
  eq 0 + M = M .
  eq s(M) + N = s(M + N) .
endfm

fmod TEST-META is 
  protecting META-LEVEL . 

  op META-MY-NAT : -> Module .
  eq META-MY-NAT = (fmod 'MY-NAT is
  nil 
  sorts 'Nat .
  none
  op '0 : nil -> 'Nat [ctor] .
  op '_+_ : 'Nat 'Nat -> 'Nat [assoc comm] .
  op 's : 'Nat -> 'Nat [none] .
  none
  eq '_+_['0.Nat,'M:Nat] = 'M:Nat [none] .
  eq '_+_['N:Nat,'s['M:Nat]] = 's['_+_['N:Nat,'M:Nat]] [none] .
endfm) .

endfm


red META-MY-NAT .


***( 
    op fmod_is_sorts_.____endfm : Qid ImportList
	SortSet SubsortDeclSet OpDeclSet MembAxSet
	EquationSet -> FModule [...] .
    op mod_is_sorts_._____endm : Qid ImportList
	SortSet SubsortDeclSet OpDeclSet MembAxSet
	EquationSet RuleSet -> Module [...] .
)***


---red in META-LEVEL : upModule('MY-NAT, false) .

---red in TEST-META : upModule('MY-NAT, false) == META-MY-NAT . 



fmod TEST-META-B is 
    including TEST-META .

    *** here I copied the result from upModule
    op META-MY-NAT-B : -> Module .
    eq META-MY-NAT-B = 
(fmod 'MY-NAT is
    including 'BOOL .   *** Maude automatically includes BOOL in a Module, while on our attempt by hand we intuitively put 'nil'
    sorts 'Nat .
    none
    op '0 : nil -> 'Nat [ctor] .
    op '_+_ : 'Nat 'Nat -> 'Nat [assoc comm] .
    op 's : 'Nat -> 'Nat [none] .
    none
    eq '_+_['0.Nat,'M:Nat] = 'M:Nat [none] .
    eq '_+_['N:Nat,'s['M:Nat]] = 's['_+_['N:Nat,'M:Nat]] [none] .
endfm) .

endfm

---red in TEST-META-B : upModule('MY-NAT, false) == META-MY-NAT-B .
red in TEST-META-B : upTerm(0 + M:Nat) .
red in TEST-META-B : upTerm(upTerm(0 + M:Nat)) .