Add an associative function symbol

[charlie-j]

Introduce a builtin with an associative function.
Terms are extended with an Associative function application constructor. It
relies on the associative unficiation feature of maude.

As associative unification is not finitary, maude may return a non complete
set of unifiers, in which case tamarin fails with a warning. When no such
warning is return at any point, soundness and completeness are preserved.

[jdreier]

This PR (silently) fixes the DH-neutral problem also covered in this PR: #494

[charlie-j]

Oh shit, I indeed forgot to mention it. For the associative operator, we add the fact that maude warnings are now caught by Tamarin, so the DH issue became visible when running the regression tests.

[jdreier]

No problem. But both PR currently fail the regression test because some files are impacted by DH-neutral. I guess we need to update the regression targets once #495 is accepted (to avoid having spurious warnings, see also #496).

[charlie-j]

Updated based on the merge of #495

[charlie-j]

This should be put on hold until #507 is merged.
The yellow coloring should then be also used here.

[charlie-j]

As #507 was merged, I updated this branch.

So ideally, I'd like to use the same yellow coloring in the incomplete case.

HOWEVER, the incomplete cases here are exceptions returned by the Maude/Process.hs file, using the error function. Unless we strongly change the structure of the code, I think it may be too difficult to make it so that this is properly caught.

@rsasse @jdreier do you have any intuition on this? Do you think there's no chance I can get this to work kind of cleanly?

[charlie-j]

I've tried a first option, which is to add a wrapper for the result, using

-- | Values that depend on a 'MaudeHandle'.
type WithMaude a = Reader MaudeHandle (MaudeResult a)

where

data MaudeResult a =  IncompleteUnification  | Result a
  deriving Show

This creates batshit crazy propagation, going from the bottom, I tried to update everything for several hours, but it is just completely unreasonable. Many utility functions, the simplest being folds, all test, setAny etc have to be recoded to account for the new type.

At some point I tried the other option, to use an exception carried by the Reader monade of WithMaude. Here, the advantage is that we don't have to update all functions that work in the WithMaude monade. However, doing a grep runReader gives an idea of the number of points where the exception needs to be handled, and then from those points ir should go all the way up to rankProofMethods. Once again, it was becoming crazy.

So, after losing quite a lot of time on it, my two core observations:

• any solution (that I can reasonably try given my poor Haskell skills) appears to imply a huge number of ugly changes in the code, complexifying the code a lot.
• I don't think the goal is worth both the time and the added complexity in the code.

TLDR, I give up on going for the nice integration. I let you decide if you want to keep it in or out as is.