Hi Bill,
(sorry for the late answer)
Le 08.04.13 23:59, Bill Richter a écrit :
> Vince, you recommended replacing the lines
>
> (...)
> 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)^"\"";;
Indeed, use instead:
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 if c = "'" 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 changed again the trigger character for the quotation, it is now " '
". So for instance:
# `'&1+1`;;
val it : preterm =
Combp
(Combp (Combp (Varp ("&", Ptycon ("", [])), Varp ("1", Ptycon ("",
[]))),
Varp ("+", Ptycon ("", []))),
Varp ("1", Ptycon ("", [])))
> 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.
Indeed, however in my opinion, it is a better long-term solution to
modify system.ml since others might benefit from having quotations
dedicated to preterms (as it is the case for instance in HOL4).
> 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?
If you have a careful look at quotexpander, you will see that, contrary
to both other parsers, the string is passed to parse_qproof without
removing the ";".
The problem is solved if you thus define parse_qproof as follows:
# let parse_qproof s = (fst o parse_preterm o lex o explode) (String.sub
s 1 (String.length s - 1));;
> 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.
Indeed.
> 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?
>
I don't get what you mean, here...
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
------------------------------------------------------------------------------
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
