[Caml-list] Agda-style parser

[Caml-list] Agda-style parser

[Andrej Bauer]

If I wanted a parser in Ocaml that can parse things in teh style of
Agda (with the cool underscore thingy), where would I start looking?

With kind regards,

Andrej

Re: [Caml-list] Agda-style parser

[Fabrice Le Fessant]

Could you give more details about what you are looking for, for those
ones who are not familiar with Agda "cool underscore thingy" ?

Thx,
-Fabrice

On Fri, Jul 6, 2012 at 2:52 PM, Andrej Bauer <andrej.bauer@andrej.com> wrote:
> If I wanted a parser in Ocaml that can parse things in teh style of
> Agda (with the cool underscore thingy), where would I start looking?
>
> With kind regards,
>
> Andrej
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>



-- 
Fabrice LE FESSANT
Chercheur en Informatique
INRIA Saclay -- Ile-de-France
Programming Languages and Distributed Systems

Re: [Caml-list] Agda-style parser

[Anil Madhavapeddy]

Andrej is probably referring to mixfix operators in Agda:
http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Mixfix

To quote:

> A name containing more than one name part can be used as an operator where the arguments go in place of the _. For instance, an application of the name if_then_else_ to arguments x, y, and z can be written either as a normal application if_then_else_ x y z or as an operator application if x then y else z.

-anil

On 6 Jul 2012, at 14:17, Fabrice Le Fessant wrote:

> Could you give more details about what you are looking for, for those
> ones who are not familiar with Agda "cool underscore thingy" ?
> 
> Thx,
> -Fabrice
> 
> On Fri, Jul 6, 2012 at 2:52 PM, Andrej Bauer <andrej.bauer@andrej.com> wrote:
>> If I wanted a parser in Ocaml that can parse things in teh style of
>> Agda (with the cool underscore thingy), where would I start looking?
>> 
>> With kind regards,
>> 
>> Andrej
>> 
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa-roc.inria.fr/wws/info/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>> 
> 
> 
> 
> -- 
> Fabrice LE FESSANT
> Chercheur en Informatique
> INRIA Saclay -- Ile-de-France
> Programming Languages and Distributed Systems
> 
> -- 
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
> 

Re: [Caml-list] Agda-style parser

[Wojciech Meyer]

Hi,

I think his talking about "mix-fix" notation.

Basically the underscores are placeholders for expression in "mix-fix"
operator that can be subsitutied by any expression:

if _ then _ else _ = fun cond yes no -> if cond then yes else no

please note that under strict evaulation like in OCaml it will not be correct.

Another example:

_ ++ _ = List.append

In Coq there is support for mix-fix operators via. Notation.

Wojciech


On Fri, Jul 6, 2012 at 2:17 PM, Fabrice Le Fessant
<Fabrice.Le_fessant@inria.fr> wrote:
> Could you give more details about what you are looking for, for those
> ones who are not familiar with Agda "cool underscore thingy" ?
>
> Thx,
> -Fabrice
>
> On Fri, Jul 6, 2012 at 2:52 PM, Andrej Bauer <andrej.bauer@andrej.com> wrote:
>> If I wanted a parser in Ocaml that can parse things in teh style of
>> Agda (with the cool underscore thingy), where would I start looking?
>>
>> With kind regards,
>>
>> Andrej
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa-roc.inria.fr/wws/info/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>>
>
>
>
> --
> Fabrice LE FESSANT
> Chercheur en Informatique
> INRIA Saclay -- Ile-de-France
> Programming Languages and Distributed Systems
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Agda-style parser

[Gabriel Scherer]

My advice would be to mimic Agda's conceptual two-pass process: parse
only the static Context-Free Language structure of your language,
parsing "expressions" (or any syntactic class that admits mixfixes)
into just a list of non-terminals (plus parenthesing, if you assume
your mixfixes are all well-balanced wrt. symmetric delimitors). This
can be done easily with existing OCaml parser or parser generator
technology (menhir). Then, in a later pass, you compute mixfix
definitions/scopes and add this structure to the parsetree, using a
custom algorithm that has been described in the Agda literature (or
non-Agda previous work), eg.
http://www.cse.chalmers.se/~nad/publications/danielsson-norell-mixfix.html
.

This is a clean way to handle this and, I believe, one of the simplest
to use, understand and debug.

On Fri, Jul 6, 2012 at 2:52 PM, Andrej Bauer <andrej.bauer@andrej.com> wrote:
> If I wanted a parser in Ocaml that can parse things in teh style of
> Agda (with the cool underscore thingy), where would I start looking?
>
> With kind regards,
>
> Andrej
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] Agda-style parser

[Jérémie Dimino]

Le Fri, 6 Jul 2012 14:52:39 +0200,
Andrej Bauer <andrej.bauer@andrej.com> a écrit :

> If I wanted a parser in Ocaml that can parse things in teh style of
> Agda (with the cool underscore thingy), where would I start looking?

You can have a look at dypgen [1]. Actions can extend the grammar.

  [1] http://dypgen.free.fr/

Jérémie

Re: [Caml-list] Agda-style parser

[Andrej Bauer]

Dear Jérémie and Gabriel, thanks for your answers, they're both very useful!

I wonder if the Agda-style "let's use crazy utf-8 characters and any
kind of notation we think of" is the future of programming language
syntax. It's certainly appealing to mathematicians.

With kind regards,

Andrej