set show timing off .
set show advisories off .

***
*** Test variant unification in the meta-interpreter.
***

load metaInterpreter

fmod XOR is
  sort XOR .

  sort Elem .
  ops c1 c2 c3 c4 : -> Elem .

  subsort Elem < XOR .
  op _+_ : XOR XOR -> XOR [ctor assoc comm] .
  op 0 : -> XOR .
  op a : -> XOR .

  vars X Y : XOR .

  eq Y + 0 = Y [variant] .
  eq X + X = 0 [variant] .
  eq X + X + Y = Y [variant] .
endfm

mod VARIANT-UNIFY-TEST is
  pr META-INTERPRETER .
  sort MsgList .
  subsort Msg < MsgList .
  op me : -> Oid .
  op User : -> Cid .
  op problem:(_,_) : UnificationProblem TermList -> Attribute .
  op soln:_ : Nat -> Attribute .
  op result : MsgList -> Attribute .
  op _,_ : MsgList MsgList -> MsgList [assoc id: nil] .
  op nil : -> MsgList .

  vars X Y Z : Oid .
  var AS : AttributeSet .
  var N : Nat .
  var V : Term .
  var TL : TermList .
  var S : Substitution .
  var Q : Qid .
  var B : Bool .
  var P : Parent .
  var R : RewriteCount .
  var ML : MsgList .
  var UP : UnificationProblem .

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

  rl < X : User | AS, problem:(UP, TL) > insertedModule(X, Y) =>
     < X : User | AS, problem:(UP, TL), soln: 1, result(nil) > getVariantUnifier(Y, X, 'XOR, UP, TL, '#, 0) .

  rl < X : User | AS, problem:(UP, TL), soln: N, result(ML) > gotVariantUnifier(X, Y, R, S, Q) =>
     < X : User | AS,  problem:(UP, TL), soln: (N + 1), result(ML, gotVariantUnifier(X, Y, R, S, Q)) >
     getVariantUnifier(Y, X, 'XOR, UP, TL, '#, N) .
endm

erew in VARIANT-UNIFY-TEST : <> 
< me : User | problem: ('_+_['X:XOR, 'c1.Elem] =? '_+_['Y:XOR, 'c2.Elem], empty) > 
createInterpreter(interpreterManager, me, none) .

variant unify in XOR : X:XOR + c1 =? Y:XOR + c2 .

erew in VARIANT-UNIFY-TEST : <> 
< me : User | problem: ('_+_['X:XOR, 'c1.Elem] =? '_+_['Y:XOR, 'c2.Elem], '_+_['X:XOR, 'c1.Elem]) > 
createInterpreter(interpreterManager, me, none) .

variant unify in XOR : X:XOR + c1 =? Y:XOR + c2 such that X:XOR + c1 irreducible .

mod DISJOINT-VARIANT-UNIFY-TEST is
  pr META-INTERPRETER .
  sort MsgList .
  subsort Msg < MsgList .
  op me : -> Oid .
  op User : -> Cid .
  op problem:(_,_) : UnificationProblem TermList -> Attribute .
  op soln:_ : Nat -> Attribute .
  op result : MsgList -> Attribute .
  op _,_ : MsgList MsgList -> MsgList [assoc id: nil] .
  op nil : -> MsgList .

  vars X Y Z : Oid .
  var AS : AttributeSet .
  var N : Nat .
  var V : Term .
  var TL : TermList .
  vars S S' : Substitution .
  var Q : Qid .
  var B : Bool .
  var P : Parent .
  var R : RewriteCount .
  var ML : MsgList .
  var UP : UnificationProblem .

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

  rl < X : User | AS, problem:(UP, TL) > insertedModule(X, Y) =>
     < X : User | AS, problem:(UP, TL), soln: 1, result(nil) > getDisjointVariantUnifier(Y, X, 'XOR, UP, TL, '#, 0) .

  rl < X : User | AS, problem:(UP, TL), soln: N, result(ML) > gotDisjointVariantUnifier(X, Y, R, S, S', Q) =>
     < X : User | AS,  problem:(UP, TL), soln: (N + 1), result(ML, gotDisjointVariantUnifier(X, Y, R, S, S', Q)) >
     getDisjointVariantUnifier(Y, X, 'XOR, UP, TL, '#, N) .
endm

erew in DISJOINT-VARIANT-UNIFY-TEST : <> 
< me : User | problem: ('_+_['X:XOR, 'c1.Elem] =? '_+_['Y:XOR, 'c2.Elem], empty) > 
createInterpreter(interpreterManager, me, none) .

erew in DISJOINT-VARIANT-UNIFY-TEST : <> 
< me : User | problem: ('_+_['X:XOR, 'c1.Elem] =? '_+_['Y:XOR, 'c2.Elem], '_+_['X:XOR, 'c1.Elem]) > 
createInterpreter(interpreterManager, me, none) .