How to disambiguate infix operators?

[Dirk Ullrich]

Hello,

I just playing with namespaces and export modifiers. I will use that
stuff to have different definitions for one name, but then choose one
of these definitions for export. For coexistence of the definitions of
the same name I use explicit namespaces, and exporting I control by
export modifiers.

For illustration a simple example using functions. Consider the
following module wer we define a Boolean NOR:

module mod
%access public

namespace one {
private nor_ : Bool -> Bool -> Bool
nor_ True _ = False
nor_ _ True = False
nor_ _ _ = True
}
namespace two {
private nor_ : Bool -> Bool -> Bool
nor_ False False = True
nor_ _ _ = False
}

nor : Bool -> Bool -> Bool
nor = two.nor_ -- (*)

If I try to use, an infix operator, say `~', instead of the `nor_', I
get a problem: In line (*) I have disambiguate `~' - but I do not know
how:
Both `two,(~)' (prefix notation) and `two.~' (infix notation) fail.

Did I miss something, or is it Idris' missing / bug?

Dirk

[Edwin Brady]

Hi Dirk,
It is, alas, missing, for now. The only thing you can do is write a wrapper function with a normal name and disambiguate that way. However, it is not a hard feature to add so I'll fix it properly when I get a moment.

Edwin.

[Dirk Ullrich]

Hi Edwin,

2012/7/27 Edwin Brady <edwin...@gmail.com>:

> Hi Dirk,
> It is, alas, missing, for now. The only thing you can do is write a wrapper function with a normal name and disambiguate that way. However, it is not a hard feature to add so I'll fix it properly when I get a moment.

such a feature would be very nice! I, as always, tried to figure it
out by looking into the Idris code. But this time I did not get it
:-(. So I will have a look into your changes when done to learn a bit
more about Idris' internals.

Thanks
Dirk

[Dirk Ullrich]

Hello,

2012/7/27 Dirk Ullrich <dirk.u...@gmail.com>:

In the meantime, I had another look at the problem. To get started
I've investigated the interplay of operators and namespaces (without
any accessibility stuff). It seems that Idris does parse / elaborate
type declarations for infix operators correctly: At least you can do
things like:

infixl ~, 4
namespace ns {
~: SomeType -> SomeType -> SomeType
...}
foo : SomeType -> SomeType -> SomeType
foo x y = x ~ y

and in the `foo' clause the `~' is correctly elaborated as
`module.ns.~' where `module' is name of module containing the code
listed above. The trouble begins if want to use the namespace in the
`foo'
clause: The elaboration of this clause fails - neither:

foo x y = x ns.~ y

nor

foo x y = ns.(~) x y

nor

foo x y = (ns.~) x y

works.

Before trying my hand to fix this I have a question:
@Edwin: Would you consider `ns.(~)' or `(ns.~)' the correct syntax for
using an infix operator `~' together with an namespace `ns' in
ordinary function (i.e. prefix) position?

By the way - even hacking Idris itself seems to be funny.

Dirk

[Edwin Brady]

On 7 Aug 2012, at 13:18, Dirk Ullrich wrote:

> Before trying my hand to fix this I have a question:
> @Edwin: Would you consider `ns.(~)' or `(ns.~)' the correct syntax for
> using an infix operator `~' together with an namespace `ns' in
> ordinary function (i.e. prefix) position?

I would think ns.(~) is the most natural prefic syntax for this - I'm not sure there is a natural infix syntax. But to be honest, I don't really mind, because they both seem to make sense.

It should be that all that needs changing is the pfName function in Idris/Parser.hs. It may also be worth looking at Core/CoreParser.hs (which implements a basic parser for the core language, some of which is inherited by the main parser).

Edwin.

[Dirk Ullrich]

Hello Edwin,

2012/8/7 Edwin Brady <edwin...@gmail.com>:

thank your for the quick answer and the hints! I'll do my best.

Dirk

[Dirk Ullrich]

Hello,

2012/8/7 Edwin Brady <edwin...@gmail.com>:

I've tried to add enhance `pfName' to support operators in front
position with a namespace in the form `ns.(~)', too. The new `pfName'
seems okay when using in an sandboxed test environment. But it does
not work with Idris - it isn't even backwards compatible. In the patch
attached the line where the new `pfName' fails even when checking
Idris' libraries is marked by a `--FixMe'.

At the moment I have no clue what's wrong here. Maybe someone spots
the problem? Otherwise I will start a fresh attempt in a few days.

Dirk

[Dirk Ullrich]

Hi,

2012/8/8 Dirk Ullrich <dirk.u...@gmail.com>:

> Hello,
>
> 2012/8/7 Edwin Brady <edwin...@gmail.com>:
>> On 7 Aug 2012, at 13:18, Dirk Ullrich wrote:
>>
>>> Before trying my hand to fix this I have a question:
>>> @Edwin: Would you consider `ns.(~)' or `(ns.~)' the correct syntax for
>>> using an infix operator `~' together with an namespace `ns' in
>>> ordinary function (i.e. prefix) position?
>>
>> I would think ns.(~) is the most natural prefic syntax for this - I'm not sure there is a natural infix syntax. But to be honest, I don't really mind, because they both seem to make sense.
>>
>> It should be that all that needs changing is the pfName function in Idris/Parser.hs. It may also be worth looking at Core/CoreParser.hs (which implements a basic parser for the core language, some of which is inherited by the main parser).
> I've tried to add enhance `pfName' to support operators in front
> position with a namespace in the form `ns.(~)', too. The new `pfName'
> seems okay when using in an sandboxed test environment. But it does
> not work with Idris - it isn't even backwards compatible. In the patch
> attached the line where the new `pfName' fails even when checking
> Idris' libraries is marked by a `--FixMe'.

[...]

I hope I've got it now. The patch appended can be applied to Git
master, and should make Idris to support operators with namespaces in
front position in the form of `ns.(~)'. (My failure with the patch
before was not to check that the namespace prefix ends in a `.' This
merged the type declaration of an operator with its first pattern
declaration.)

Next I would try to add support for infix oparators with namespaces in
infix position, i.e. something like `x ns.~ y'. Looking forward to
such funny things like distinguishing `ns..' - operator `.' with
namespace `ns' - from an identifier ...

Dirk

[Dirk Ullrich]

Hi again,

2012/8/11 Dirk Ullrich <dirk.u...@gmail.com>:

here comes my next iteration for working on namespaced operators. I've
redone my last patch to generalize `maybeWithNS' the parsing of
namespaces. This has the following effects:

(1) `iName' can be now based on `maybeWithNS', too.
There is one difference to the previous `iName': identifiers with a
trailing `.' are not parsed as pure namespaces: e.g. "a.b." is parsed
as `NS (UN "b.") ["a"]' (instead of `NS (UN "") ["b", "a"]').
@Edwin: Is this a problem?
(If it is a problem for a call to `iName' where it is used to parse a
namespace, we could use `maybeWithNS' instead.)

(2) Operators with namespaces in function position are handled correctly.

(3) Operators with namespaces in infix position are not handled yet -
but we are closer. For instance
pOpInfix = maybeWithNS operator True []
would properly parse infix operators with optional namespace -- even
such funny nones like `ns...' - this would become `..' with namespace
`ns'. There is only one restriction to the namespace here: it cannot
contain two consecutive dots, i.e. something like `..'.
@Edwin, again: Is this a problem?
For implementing namespace support for infix operators imho one have
to use `maybeWithNS' in the `table' / `toTable' definition in
`Idris/Parser.hs'. I could try this when I am back from holiday in
about a week.

The patch appended is for current Git master (so, please, throw my
older patches with the same name away).

Dirk