set show timing off .
set show advisories off .

***
*** Test search in the meta-interpreter without and with path.
***

load metaInterpreter

mod SEARCH is
  sort State .
  ops a b c d e : -> State .

  rl [a-move1] : a => b .
  rl [a-move2] : a => c .
  rl [b-move] : b => d .
  rl [c-move] : c => e .
endm

mod SEARCH-TEST is
  pr META-INTERPRETER .

  op me : -> Oid .
  op User : -> Cid .
  op soln:_ : Nat -> Attribute .

  vars X Y Z : Oid .
  var AS : AttributeSet .
  var N : Nat .

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

  rl < X : User | soln: N, AS > insertedModule(X, Y) =>
     < X : User | AS > getSearchResult(Y, X, 'SEARCH, 'a.State, 'X:State, nil, '*, 20, N) .
endm

erew in SEARCH-TEST : <> 
< me : User | soln: 0 > 
createInterpreter(interpreterManager, me, none) .

erew in SEARCH-TEST : <> 
< me : User | soln: 1 > 
createInterpreter(interpreterManager, me, none) .

erew in SEARCH-TEST : <> 
< me : User | soln: 2 > 
createInterpreter(interpreterManager, me, none) .

erew in SEARCH-TEST : <> 
< me : User | soln: 3 > 
createInterpreter(interpreterManager, me, none) .

erew in SEARCH-TEST : <> 
< me : User | soln: 4 > 
createInterpreter(interpreterManager, me, none) .

erew in SEARCH-TEST : <> 
< me : User | soln: 5 > 
createInterpreter(interpreterManager, me, none) .

mod SEARCH-CACHE-TEST is
  pr META-INTERPRETER .

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

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

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

  rl < X : User | soln: N, AS > insertedModule(X, Y) =>
     < X : User | AS, soln: 1 > getSearchResult(Y, X, 'SEARCH, 'a.State, 'X:State, nil, '*, 20, 0) .

  rl < X : User | soln: N, AS > gotSearchResult(X, Y, M, T, TY, S) =>
     < X : User | AS, soln: (N + 1), got: gotSearchResult(X, Y, M, T, TY, S) >
     getSearchResult(Y, X, 'SEARCH, 'a.State, 'X:State, nil, '*, 20, N) .
endm

erew in SEARCH-CACHE-TEST : <> 
< me : User | soln: 0 > 
createInterpreter(interpreterManager, me, none) .


mod SEARCH-PATH-TEST is
  pr META-INTERPRETER .

  op me : -> Oid .
  op User : -> Cid .
  op soln:_ : Nat -> Attribute .

  vars X Y Z : Oid .
  var AS : AttributeSet .
  var N : Nat .

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

  rl < X : User | soln: N, AS > insertedModule(X, Y) =>
     < X : User | AS > getSearchResultAndPath(Y, X, 'SEARCH, 'a.State, 'X:State, nil, '*, 20, N) .
endm

erew in SEARCH-PATH-TEST : <> 
< me : User | soln: 0 > 
createInterpreter(interpreterManager, me, none) .

erew in SEARCH-PATH-TEST : <> 
< me : User | soln: 1 > 
createInterpreter(interpreterManager, me, none) .

erew in SEARCH-PATH-TEST : <> 
< me : User | soln: 2 > 
createInterpreter(interpreterManager, me, none) .

erew in SEARCH-PATH-TEST : <> 
< me : User | soln: 3 > 
createInterpreter(interpreterManager, me, none) .

erew in SEARCH-PATH-TEST : <> 
< me : User | soln: 4 > 
createInterpreter(interpreterManager, me, none) .

erew in SEARCH-PATH-TEST : <> 
< me : User | soln: 5 > 
createInterpreter(interpreterManager, me, none) .

mod SEARCH-PATH-CACHE-TEST is
  pr META-INTERPRETER .

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

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

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

  rl < X : User | soln: N, AS > insertedModule(X, Y) =>
     < X : User | AS, soln: 1 > getSearchResultAndPath(Y, X, 'SEARCH, 'a.State, 'X:State, nil, '*, 20, 0) .

  rl < X : User | soln: N, AS > gotSearchResultAndPath(X, Y, M, T, TY, S, TR) =>
     < X : User | AS, soln: (N + 1), got: gotSearchResultAndPath(X, Y, M, T, TY, S, TR) >
     getSearchResultAndPath(Y, X, 'SEARCH, 'a.State, 'X:State, nil, '*, 20, N) .
endm

erew in SEARCH-PATH-CACHE-TEST : <> 
< me : User | soln: 0 > 
createInterpreter(interpreterManager, me, none) .