set show timing off .
set show advisories off .

***
*** Test gotOneStepNarrowing() in the meta-interpreter.
***

load metaInterpreter

mod NARROW is
  sort Foo .
  op f : Foo Foo -> Foo [assoc comm] .
  ops g h : Foo -> Foo .
  ops a b c d e : -> Foo .

vars X Y Z W : Foo .
  rl g(f(X, X)) => h(X) [narrowing].
endm

mod NARROW-TEST is
  pr META-INTERPRETER .
  sort MsgList .
  subsort Msg < MsgList .
  op empty : -> MsgList .
  op _;_ : MsgList MsgList -> MsgList [assoc id: empty] .

  op me : -> Oid .
  op User : -> Cid .
  op soln:_ : Nat -> Attribute .
  op got:_  : MsgList -> Attribute .
  op start:_ : Term -> Attribute .
  op irred:_ : TermList -> Attribute .

  vars X Y Z : Oid .
  var AS : AttributeSet .
  vars N M : Nat .
  vars S S' : Substitution .
  var ST T : Term .
  var TY : Type .
  var C : Context .
  var Q L : Qid .
  var ML : MsgList .
  var TL : TermList .

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

  rl < X : User | AS, start: ST, irred: TL > insertedModule(X, Y) =>
     < X : User | AS, soln: 1, start: ST, irred: TL, got: empty > getOneStepNarrowing(Y, X, 'NARROW, ST, TL, '#, 0) .

  rl < X : User | AS, soln: N, start: ST, irred: TL, got: ML >
     gotOneStepNarrowing(X, Y, M, T, TY, C, L, S, S', Q) =>
     < X : User | AS, soln: (N + 1),  start: ST, irred: TL, got: (ML ; gotOneStepNarrowing(X, Y, M, T, TY, C, L, S, S', Q)) >
      getOneStepNarrowing(Y, X, 'NARROW, ST, TL, '#, N) .

endm

set show breakdown on .

erew in NARROW-TEST : <> 
< me : User | start: ('g['f['#22:Foo, '#21:Foo, '#23:Foo]]), irred: empty > 
createInterpreter(interpreterManager, me, none) .

mod NARROW is
  sort Foo .
  op f : Foo Foo -> Foo [assoc] .
  ops g h : Foo -> Foo .
  ops a b c d e : -> Foo .

vars X Y Z W : Foo .
  rl g(f(X, X)) => h(X) [narrowing].
endm

erew in NARROW-TEST : <> 
< me : User | start: ('g['f['#22:Foo, '#21:Foo, '#23:Foo]]), irred: empty > 
createInterpreter(interpreterManager, me, none) .

erew in NARROW-TEST : <> 
< me : User | start: ('g['f['#22:Foo, '#22:Foo, '#23:Foo]]), irred: empty > 
createInterpreter(interpreterManager, me, none) .

erew in NARROW-TEST : <> 
< me : User | start: ('g['f['#22:Foo, '#23:Foo, '#23:Foo]]), irred: empty > 
createInterpreter(interpreterManager, me, none) .


mod XOR is
  sorts Elt Expr .
  subsort Elt < Expr .
  ops a b c d e : -> Elt .
  op _+_ : Expr Expr -> Expr [assoc comm] .
  op 0 : -> Elt .

vars W X Y Z : Expr .
  eq Y + 0 = Y [variant] .
  eq X + X = 0 [variant] .
  eq X + X + Y = Y [variant] .
endm

mod NARROW is inc XOR .
  ops g h : Expr -> Expr .
  op f : Expr Expr -> Expr .

vars W X Y Z : Expr .
  rl g(Y + a) => h(Y) [narrowing label one] .
endm

*** bound variable in irreducibility constraint

erew in NARROW-TEST : <> 
< me : User | start: ('f['g['_+_['W:Expr, 'b.Elt]], 'Z:Expr]), irred: ('_+_['W:Expr, 'b.Elt]) > 
createInterpreter(interpreterManager, me, none) .

*** unbound variable in irreducibility constraint

erew in NARROW-TEST : <> 
< me : User | start: ('f['g['_+_['W:Expr, 'b.Elt]], 'Z:Expr]), irred: ('_+_['X:Expr, 'b.Elt]) > 
createInterpreter(interpreterManager, me, none) .

*** # variable in input
erew in NARROW-TEST : <> 
< me : User | start: ('f['g['_+_['#1:Expr, 'b.Elt]], '#2:Expr]), irred: ('_+_['#3:Expr, 'b.Elt]) > 
createInterpreter(interpreterManager, me, none) .