Hi Bill, | Can someone explain the point of HOL Light parsers, as in the | reference manual entry for many:
There is an approach to writing parsers in functional languages where you can make functional code look almost like an abstract grammar. These HOL Light functions are a pretty simple version of such techniques. There are some general references here: http://en.wikipedia.org/wiki/Parser_combinator To see some examples, you might look at the function "parse_preterm" in the core HOL Light file "parser.ml". For example, from a suitably charitable point of view the following fragment: ... || a (Resword "(") ++ preterm ++ a (Resword ")") >> (snd o fst) || a (Resword "if") ++ preterm ++ a (Resword "then") ++ preterm ++ a (Resword "else") ++ preterm >> lmk_ite || a (Resword "[") ++ elistof preterm (a (Resword ";")) "term" ++ a (Resword "]") >> (pmk_list o snd o fst) ... looks very much like a grammar for preterms: ... | "(" preterm ")" | "if" preterm "then" preterm "else" preterm | "[" preterm [;preterm]* "]" ... | Here's another question, unfortunately stated without an example. | Suppose we have a goal g which we want to prove with | | MESON_TAC[th1; th2; th3];; | | What's the difference between this and instead using MP_TAC to | make the goal | | th3 ==> g | | and trying to prove this with | | MESON_TAC[th1; th2];; | | I have evidence that sometimes the 1st works when the 2nd does not. | I don't have an example when the 2nd works and the 1st does not. | Why are the two approaches not identical? The difference is that after MP_TAC any free variables or free type variables effectively get "frozen" so they cannot be instantiated, whereas when given directly to MESON_TAC, they can be generalized and instantiated. This makes a difference in general where the theorem concerned is either not universally generalized or contains polymorphic types. Sometimes it can be positively beneficial to "freeze" things, to reduce search space or otherwise constrain later steps, and there is a little-used theorem-tactical FREEZE_THEN to do this directly. John. ------------------------------------------------------------------------------ Get 100% visibility into Java/.NET code with AppDynamics Lite It's a free troubleshooting tool designed for production Get down to code-level detail for bottlenecks, with <2% overhead. Download for free and get started troubleshooting in minutes. http://p.sf.net/sfu/appdyn_d2d_ap2 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
