I'm trying to learn how to write an interface for HOL Light that's basically 
miz3 without the the "by" justification lists, so proofs of the statements 
would be normal HOL Light proofs.  I figure that's the easy part of miz3, the 
part that doesn't really have anything to do with Mizar, which is all about a 
nice FOL mathematical formula that limits the size of inference leaps.  Has 
anyone besides Freek every done such a thing?  More specifically, 

A standard Scheme exercise is to write a Scheme meta-interpreter, and that's 
pretty easy because of the quote function, which allows you to read a Scheme 
program as text, which you can then write simple parser for.  Does Ocaml have a 
feature similar to the Scheme quote?

What amazes me most about Freek's miz2 & miz3 is that his interface doesn't use 
backquotes, and miz3 doesn't require the extra type annotations of variables 
put in the backquotes that Petros taught me about.  How do you do something 
like that?  parse_context_term at the top of Mizarlight/miz2a.ml uses the 
functions 
parse_preterm, term_of_preterm, retypecheck and pretype_of_type
whose documentation say things like 

   These are parsing function are not normally of concern to users.
   User manipulation of pretypes is not usually necessary, unless you seek to 
radically change aspects of parsing and typechecking.

I think what Freek's doing runs something like this.  We have many functions 
that deal with strings, e.g. lex & explode. HOL Light deals with pretypes and 
preterms as intermediate representations.   We can use parse_term and  
parse_type to eventually get actual terms and types.

Here's something simple I haven't yet learned how to do: transform a term to a 
string and then back again, and vice versa.

-- 
Best,
Bill 

------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_mar
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to