*** Solution to Exercise 10, Lecture 3, INF5130
*** Einar B. Johnsen 09.09.09

in oppg05.maude .
in oppg06.maude .

mod UNION is
  protecting META-LEVEL .
  pr TEST-META1 .
  pr TEST-META2 .

  op _union_ : Module Module -> Module .

  vars Q1 Q2 : Qid .
  vars I1 I2 : ImportList . 
  vars S1 S2 : SortSet .
  vars SD1 SD2 : SubsortDeclSet .
  vars OS1 OS2 : OpDeclSet .
  vars MA1 MA2 : MembAxSet .
  vars E1 E2 : EquationSet .
  vars R1 R2 : RuleSet .

  *** Note: We use the name of module1 for the new module
  *** Note: ImportList can be simplified ... 
  ***       the duplicates are not removed automatically as it happens 
  ***       for sets, since it's a list

  eq  mod Q1 is I1 sorts S1 . SD1 OS1 MA1 E1 R1 endm 
      union
      mod Q2 is I2 sorts S2 . SD2 OS2 MA2 E2 R2 endm
      = mod Q1 is (I1 I2) sorts (S1 ; S2) . (SD1 SD2) (OS1 OS2) 
                                       (MA1 MA2) (E1 E2) (R1 R2) endm .

endm


red (META-MATCH union META-MATCH2) .

*** two rules with the same label
*** the homegoal rule appears only once since it is a set of rules...