Vince, you recommended replacing the lines
let quotexpander s =
if String.sub s 0 1 = ":" then
"parse_type \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else "parse_term \""^(String.escaped s)^"\"";;
in system.ml by:
let quotexpander s =
if String.sub s 0 1 = ":" then
"parse_type \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else if String.sub s 0 1 = ";" then
"(fst o parse_preterm o lex o explode) \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else "parse_term \""^(String.escaped s)^"\"";;
I couldn't get this to work. I think you have an old version of HOL Light. In
the current subversion (159), or I think any subversion since Wed 2nd Jan 2013,
system.ml reads
let quotexpander s =
if s = "" then failwith "Empty quotation" else
let c = String.sub s 0 1 in
if c = ":" then
"parse_type \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else if c = ";" then "parse_qproof \""^(String.escaped s)^"\""
else "parse_term \""^(String.escaped s)^"\"";;
And that means, I think, that as long as we're not using miz3, we can just
redefine parse_qproof, which is defined in hol_light/miz3/miz3.ml. So instead
of modifying system.ml, let's define
let parse_qproof string = (fst o parse_preterm o lex o explode) string;;
# parse_qproof "1 + 1";;
val it : preterm =
Combp (Combp (Varp ("+", Ptycon ("", [])), Varp ("1", Ptycon ("", []))),
Varp ("1", Ptycon ("", [])))
# parse_qproof "&1 + 1";;
val it : preterm =
Combp
(Combp (Varp ("+", Ptycon ("", [])),
Combp (Varp ("&", Ptycon ("", [])), Varp ("1", Ptycon ("", [])))),
Varp ("1", Ptycon ("", [])))
So according to my understanding of quotexpander, I should get the same answer
like this, but I don't:
# `;&1 + 1`;;
Exception: Noparse.
What am I missing? The only 2 places where quotexpander is ever used are in
system.ml: the definition of quotexpander and then the next standalone line
Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander));;
I see these Quotation functions are discussed in the Camlp4 Tutorial, and I'll
got read up on it. I think I understand this now:
In addition, parse_term can be decomposed (roughly) as:
term_of_preterm o retypecheck [] o parse_preterm o lex o explode
where:
- explode simply turns a string into a list of characters
- lex turns this list of characters into a list of lexcodes (i.e., a
list of atomic words w.r.t. HOL Light understanding of what is a word)
- parse_preterm turns this into a preterm (i.e., almost like a term but
without any type checking)
- retypecheck checks the types
- term_of_preterm gets the term out the preterm
As you see, type checking only appears after parse_preterm.
That's why in my last email, the hack I suggested was to do the work
only until this phase.
In parser.ml, we have the definition
let parse_term s =
let ptm,l = (parse_preterm o lex o explode) s in
if l = [] then
(term_of_preterm o (retypecheck [])) ptm
else failwith "Unparsed input following term";;
That means that for a good string s,
parse_term s = (term_of_preterm o (retypecheck []) o fst o parse_preterm o lex
o explode) s
and I think that's what you wrote. And parse_term occurs in exactly one other
place, in the def of quotexpander above. So doesn't that mean that the
(fun x -> quotexpander)
line above says that parse_term is called on the string created by
Quotation.add and Quotation.ExStr
from a backquoted quotation? Now all I really want is to access the string
created this way. I'm happy to go through term_of_preterm, as a learning
exercise, but it seems like it would be simpler to just use this string.
Here's a question about retypecheck, about which the manual says
This is the main HOL Light typechecking function. Given an
environment env of pretype assignments for variables, it assigns a
pretype to all variables and constants, including performing
resolution of overloaded constants based on what type information
there is. Normally, this happens implicitly when a term is entered
in the quotation parser.
I believe that other than Freek's miz3.ml etc, retypecheck is only used once,
in parse_term, and the environment is the empty list. In miz3.ml, Freek is
clearly using a nonempty environment, called env'. Why don't we learn how to
do that ourselves?
--
Best,
Bill
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
