Account Options

  1. Sign in
The old Google Groups will be going away soon, but your browser is incompatible with the new version.
Google Groups Home
« Groups Home
Message from discussion How to disambiguate infix operators?
The group you are posting to is a Usenet group. Messages posted to this group will make your email address visible to anyone on the Internet.
Your reply message has not been sent.
Your post was successful
 
From:
To:
Cc:
Followup To:
Add Cc | Add Followup-to | Edit Subject
Subject:
Validation:
For verification purposes please type the characters you see in the picture below or the numbers you hear by clicking the accessibility icon. Listen and type the numbers you hear
 
Dirk Ullrich  
View profile  
 More options Aug 10 2012, 6:14 pm
From: Dirk Ullrich <dirk.ullr...@gmail.com>
Date: Sat, 11 Aug 2012 00:14:48 +0200
Local: Fri, Aug 10 2012 6:14 pm
Subject: Re: [Idris] How to disambiguate infix operators?

Hi,

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

> Hello,

> 2012/8/7 Edwin Brady <edwin.br...@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

  ns_op_front.diff
4K Download

 
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.