[tools] Preserve negated miaou list wrapper

[relokin]

Keep negated composite lists wrapped in a dedicated node instead of reusing the original list operator.

Without this, miaou can flatten the negated sub-list into the enclosing conjunction and lose the intended 'it is not the case that all of the following apply' structure.

For example:

let rel1 = [A]; rel2; [B \ range([C]; rel; [D])]

should render as:

  - E1 is an A effect.
  - E1 is rel2-before E2.
  - E2 is a B effect.
  - It is not the case that all of the following apply:
    - E2 is a D effect.
    - E3 is rel-before E2.
    - E3 is a C effect.

Assisted-by: OpenAI Codex

[relokin]

@maranget @HadrienRenaud, this PR adds regressions for miaou. On my laptop the overhead is a few seconds but I wanted to check that you are ok with that.

[HadrienRenaud]

Hi @relokin,
Thanks for checking. It's fine by me.

[fsestini]

Thanks @relokin . I see why this fixes the issue, but the representation of negated lists still feels slightly off to me.

As far as I can tell, the original issue is that flatten_out merges nested List nodes when their operators match. This patch avoids that by rewriting a negated composite list to List (Diff, ...).

That works in practice, but it means the op field is no longer describing the meaning of the node. In the case of notItem, the list being produced is not necessarily a difference, but the op field will be set to Diff regardless; that is because Diff is just being used as a sentinel to opt out of flattening. I think that makes the code harder to understand locally, because the reason for setting Diff here only becomes clear once the reader knows about this specific bug and how flatten_out happens to behave.

Since the intent here is to preserve negated composite lists as their own node, IMO that would be better represented explicitly in t, rather than encoded indirectly through the AST.op2 field.

For example, this could be a dedicated constructor for negated t terms:

type t =
  ...
  | Negated of t
  ...

or a separate flattenable flag on the existing List constructor that controls whether that list participates in flattening:

type t =
  ...
  | List of { op : AST.op2; flattenable : bool; intro_txt : string; sep_txt : string * string; children : t list; }
  ...

then functions like flatten_out and rm_dump can selectively ignore negated/non-flattenable lists:

let rec flatten_out = function
  | List ({ op = Inter|Union|Seq ; flattenable = true; intro_txt ; sep_txt ; children } as l) ->
     List { l with children = flatten_op l.op l.children }
  | List l ->
     List { l with children = List.map flatten_out l.children }
  | ...

[fsestini]

Thanks @relokin for addressing my concerns. I left a couple of minor non-blocking thoughts/comments, but this LGTM already.

[fsestini]

Thanks @relokin , feel free to squash/rebase/merge at any time!