set show timing off .
set show advisories off .

***
*** Test applyRule() in the meta-interpreter without and with extension.
***

load metaInterpreter

mod APPLY is
  sorts Foo .
  ops a b : -> Foo .
  op f : Foo Foo -> Foo [comm] .

  rl f(X:Foo, Y:Foo) => X:Foo [label k] .
endm

mod APPLY-TEST is
  pr META-INTERPRETER .

  op me : -> Oid .
  op User : -> Cid .
  op soln:_ : Nat -> Attribute .
  op got:_  : Msg -> Attribute .
  op subst:_ : Substitution -> Attribute .

  vars X Y Z : Oid .
  var AS : AttributeSet .
  vars N M : Nat .
  vars IS S : Substitution .
  var T : Term .
  var TY : Type .

  rl < X : User | AS > createdInterpreter(X, Y, Z) =>
     < X : User | AS > insertModule(Z, X, upModule('APPLY, true)) .

  rl < X : User | AS, subst: IS > insertedModule(X, Y) =>
     < X : User | AS, soln: 1, subst: IS > applyRule(Y, X, 'APPLY, 'f['a.Foo, 'b.Foo], 'k, IS, 0) .

  rl < X : User | AS, soln: N, subst: IS > appliedRule(X, Y, M, T, TY, S) =>
     < X : User | AS, soln: (N + 1),  subst: IS, got: appliedRule(X, Y, M, T, TY, S) >
     applyRule(Y, X, 'APPLY, 'f['a.Foo, 'b.Foo], 'k, IS, N) .
endm

set show breakdown on .

erew in APPLY-TEST : <> 
< me : User | subst: none > 
createInterpreter(interpreterManager, me, none) .

erew in APPLY-TEST : <> 
< me : User | subst: ('Y:Foo <- 'b.Foo) > 
createInterpreter(interpreterManager, me, none) .


mod APPLY2 is
  sorts Foo .
  ops a b c  : -> Foo .
  op f : Foo Foo -> Foo [assoc comm] .
  op g : Foo -> Foo .

  rl f(X:Foo, Y:Foo) => X:Foo [label k] .
endm

mod APPLY-TEST2 is
  pr META-INTERPRETER .

  op me : -> Oid .
  op User : -> Cid .
  op soln:_ : Nat -> Attribute .
  op got:_  : Msg -> Attribute .
  op subst:_ : Substitution -> Attribute .

  vars X Y Z : Oid .
  var AS : AttributeSet .
  vars N M : Nat .
  vars IS S : Substitution .
  var T : Term .
  var TY : Type .
  var C : Context .

  rl < X : User | AS > createdInterpreter(X, Y, Z) =>
     < X : User | AS > insertModule(Z, X, upModule('APPLY2, true)) .

  rl < X : User | AS, subst: IS > insertedModule(X, Y) =>
     < X : User | AS, soln: 1, subst: IS > applyRule(Y, X, 'APPLY2, 'g['g['f['a.Foo, 'b.Foo, 'c.Foo]]], 'k, IS, 0, unbounded, 0) .

  rl < X : User | AS, soln: N, subst: IS > appliedRule(X, Y, M, T, TY, S, C) =>
     < X : User | AS, soln: (N + 1),  subst: IS, got: appliedRule(X, Y, M, T, TY, S, C) >
     applyRule(Y, X, 'APPLY2, 'g['g['f['a.Foo, 'b.Foo, 'c.Foo]]], 'k, IS, 0, unbounded, N) .
endm

erew in APPLY-TEST2 : <> 
< me : User | subst: none > 
createInterpreter(interpreterManager, me, none) .

erew in APPLY-TEST2 : <> 
< me : User | subst: ('X:Foo <- 'a.Foo) > 
createInterpreter(interpreterManager, me, none) .