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