Two minor followups:
- there is evidently a bug in the position information when the leading
delimiter is a Unicode quote mark (the number of bytes gets counted rather than
the number of "characters");
- the unquote filter is built by the process of "configuring" the system before
building; actually building the whole system (with the "build" executable) is
not necessary if all you want to do is to play around with the unquote filter.
Michael
On 28/8/18, 09:33, "Norrish, Michael (Data61, Acton)"
<michael.norr...@data61.csiro.au> wrote:
The quotation filter doesn't really do any tokenization other than to spot
occurrences of the magic term and quotation delimiters:
` .. ` (a quotation)
‘ .. ’ (also a quotation, but with non-identical delimiters)
``:ty`` (an application of the type parser to a quotation)
“:ty” ( ditto )
``term`` (an application of the term parser to a quotation)
“term” ( ditto )
The quotations produced by the filter get "pre-loaded" with line number
information. With HOL built you can see it all in action by running the
unquote program (built in HOL/bin) as a standard Unix filter. If file contains
foo bar
`foo bar`
“term p ∨ q”;
then the output of
unquote < file
will be
foo bar
[QUOTE " (*#loc 2 2*)foo bar"]
(Parse.Term [QUOTE " (*#loc 3 4*)term p \226\136\168 q"]);
You can see that it also converts the UTF8 character into something that is
a valid string.
Tokenization builds off the location information presented in the #loc
comments.
Michael
On 28/8/18, 07:41, "Makarius" <makar...@sketis.net> wrote:
Dear experts on antiquotations HOL4,
I've looked through tools/Holmake/QuoteFilter, but could not read the
input format -- I am used to functional parser combinators instead of
lex + yacc.
Is there a specification of the input syntax in the documentation? But
it is also changing occasionally, so it might be better to re-use the
existing implementation.
Ultimately I want to turn HOL4 ML source into tokens with precise source
positions, e.g. byte addresses of the original string.
The idea is to continue some experiments with HOL4 inside the Isabelle
Prover IDE, see also https://sketis.net/2015/hol4-workshop-at-cade-25
Makarius
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
