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 <[email protected]> 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. ------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
