How to check for List equality

[omarzd]

I have two Lists of Int with the same items in the same order, yet List1 ==K List2 returns false. How do I do it?

[omarzd]

I just tried ==KList but it's the same result. I'm doing this Obs[Index] ==KList BI , where Obs is a list of lists and BI is a list.

[omarzd]

==KList is found in the file k-equal.k but is not implemented. I tried to do the following but I can't use the -Int operator in this module because I can't import INT-HOOKS because that will create a circularity:

  // equality over KList
  syntax Bool ::= KList "==KList" KList    [function, hook(KEqual:_==KList_)]
  rule LK1:KList ==KList LK2:KList => 
    LK1[0] ==K LK2[0] andBool 
    range(LK1, 1, size(LK1) -Int 1) ==K range(LK2, 1, size(LK2) -Int 1)
  when size(LK1) >Int 0 andBool size(LK2) >Int 0 
  rule .List ==K .List => true

Now what?!

[omarzd]

OK that's my mistake. The latest master does implement ==KList. I depended on the latest release.

[andreistefanescu]

I would recommend using ==K, which works as well in the latest master.

[omarzd]

This is what I get when use ==K or even ==KList

[Error] Critical: Warning: "builtins.maude", line 9 (mod ORC-BUILTINS): bad
token _==K_.
Warning: "builtins.maude", line 9 (mod ORC-BUILTINS): no parse for statement
eq '_==K_ (GeneratedAnonVar132:K,, GeneratedAnonVar133:K) = _`(_`) (# _==K_
(GeneratedAnonVar132:K, GeneratedAnonVar133:K), .KList) .
Warning: "builtins.maude", line 10 (mod ORC-BUILTINS): bad token _==K_.
Warning: "builtins.maude", line 10 (mod ORC-BUILTINS): no parse for statement
eq '_==K_ (GeneratedAnonVar132:K,, GeneratedAnonVar133:K) = _`(_`) (# _==K_
(GeneratedAnonVar132:K, GeneratedAnonVar133:K), .KList) .

[dwightguth]

Can you please show me the exact code that you have which is generating the incorrect inequality result?

[omarzd]

I'm sorry I just tried reproducing it but I couldn't because there is another error, the one I reported in #1284. It was in 3.6. Now i'm back to 3.5. I'm not getting this error but instead I always get false on list equality. Here is the code

check(Index:Int) => 
        #if Obs[Index] ==K BI
          #then true 
        #else #if Index ==Int size(Obs) 
          #then false 
        #else 
          check(Index +Int 1) 
        #fi #fi

[dwightguth]

I'd prefer to see the entire rule if I can, as well as the configuration that the rule is being applied on. The issue I have here is that I don't know what Obs and BI are supposed to be referring to, so I have a hard time knowing why it may not have worked.

[omarzd]

The code is very messy. I changed it several times today and I went back to 3.5. Plus this was just a workaround; I was trying to implement the in operator myself because it wasn't working. But now that #1280 already solved that problem, I don't need to do this anymore. Thank you very much.