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),
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
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. Ther
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 singl
I am sure the technologies are fairly similar. In particular,
the type of preterms exists in HOL-4 and all kinds of
syntax manipulation can take place there before typechecking
and term construction.
Konrad.
On Thu, Oct 23, 2014 at 6:00 AM, Piotr Trojanek
wrote:
> Dear all,
>
> is it possible
Should have mentioned that you should have a look at
src/parse/Preterm.{sig,sml}
to start.
Konrad.
On Thu, Oct 23, 2014 at 4:59 PM, Konrad Slind
wrote:
> I am sure the technologies are fairly similar. In particular,
> the type of preterms exists in HOL-4 and all kinds of
> syntax manipula
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 possi
