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