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
