with patterns and where clauses are mutually exclusive

[HuStmpHrrr]

trafficstars

It appears that with patterns and where clauses are mutual exclusive. Namely

Equations foo arg1 : ret :=
foo pat1 with (bar arg2) => {
 blah
}
where baz arg3 := blah

is not admitted. However, it's a useful pattern in general. In particular, if with pattern generates multiple branches, then baz becomes visible for all of them if the above syntax is allowed. otherwise, there doesn't seem to be workaround. i.e.

Equations foo arg1 : ret :=
foo pat1 with (bar arg2) => {
  | branch1 => baz hi;
  | branch 2 => baz hello
}
where baz arg3 := blah

V.S.

Equations foo arg1 : ret :=
foo pat1 with (bar arg2) => {
  | branch1 => baz hi
    where baz arg3 := blah;
  | branch 2 => baz hello
    where baz arg3 := blah
}

[HuStmpHrrr]

I suppose the mutually exclusive behavior is coming from this line of grammar:

user clause c ::= f up n 

and

user node n ::= := t where | :=! x | with t , t := clauses

[mattam82]

IIUC you expect pat1 variables to be bound in baz in that case?

[HuStmpHrrr]

yes I do. is that possible? do you think it's better to make baz a higher level up definition?

[mattam82]

Putting it up like this should work, modulo the fact Equations doesn't support the simpler non-recursive top-level definitions yet, maybe you hit that issue?

Equations foo arg1 : ret :=
{ foo pat1 with (bar arg2) => {
  | branch1 => baz hi;
  | branch 2 => baz hello
} }
where baz arg3 := blah

In that case though, the variables of pat1 are not available in the definition of baz. In principle the intermediate language can support an intermediate baz definition under pat1 and before the with, as it supports let-bindings anywhere in the context. It sounds like a useful feature in general indeed.