I did look at monadsyntax.sml at the very beginning. I should have
revisit this file when I started to implement my postprocessor...
I decided to keep the global grammar free from any extensions
(especially while experimenting), so I did not use
add_absyn_postprocessor. I call my parser with single quotation, like
"Monad`do ... od`".
-- Piotr
On Thu, Mar 12, 2015 at 11:54 PM, Michael Norrish
<michael.norr...@nicta.com.au> wrote:
> I’m glad you got something to work.
>
> Was the post-processing you did beyond the capabilities of the types
> permitted by
>
> Parse.{temp_,}add_absyn_postprocessor
>
> ?
>
> That facility allows a grammar to include functions for arbitrarily
> transforming the Absyn ASTs before type checking occurs. There is an example
> of its use in src/monad/monadsyntax.sml, implementing a do-notation syntax.
> The advantage would be that you could avoid having to call a custom function
> to do the parsing yourself, and that you would have a grammar value embodying
> your syntax.
>
> Michael
>
>> On 13 Mar 2015, at 10:26 am, Piotr Trojanek <piotr.troja...@gmail.com> wrote:
>>
>> Just to close this thread -- I finally got a customized HOL parser by
>> creating a temporary grammar on top of the current one and then
>> calling a sequence of "absyn -> my_absyn_post_process -> absyn_to_term".
>>
>> Thank you for your guidelines!
>>
>> -- Piotr
>>
>> On Fri, Oct 24, 2014 at 12:31 AM, Michael Norrish
>> <michael.norr...@nicta.com.au> wrote:
>>> On 23/10/14 22:00, Piotr Trojanek wrote:
>>>> Dear all,
>>>
>>>> is it possible to use HOL4 parser in a similar way to `parse_preterm`
>>>> from HOL Light?
>>>
>>>> In HOL Light one can easily build a parser for HOL terms embedded in a
>>>> custom language (see hol_light/Examples/prog.ml). In HOL4 it seems
>>>> only possible to modify the term grammar (e.g. with add_rule), which
>>>> is much less flexible.
>>>
>>> See the description of parsing and pretty-printing in the DESCRIPTION manual
>>> (§5.1) for more on the various phases of HOL parsing. As Konrad said,
>>> there is
>>> a preterm type (see src/parse). There is also an “abstract syntax” type
>>> (Absyn)
>>> so that the parsing process actually goes through the following stages:
>>>
>>> string/quotation -> tokens -> Absyn -> Preterm -> Term
>>>
>>> The nearest equivalent to parse_preterm in HOL4 is probably
>>> parse_term.parse_term, which (roughly) consumes a qbuf (“quotation buffer”,
>>> from
>>> src/parse/qbuf) to produce a value of type Absyn. A qbuf is given a
>>> quotation,
>>> and produces a sequence of tokens.
>>>
>>> I hope this helps,
>>> Michael
>>>
>>> ________________________________
>>>
>>> The information in this e-mail may be confidential and subject to legal
>>> professional privilege and/or copyright. National ICT Australia Limited
>>> accepts no liability for any damage caused by this email or its attachments.
>
--
Piotr Trojanek
------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
