Thanks, Ramana! I think it would be good to compare what I'm doing with how things are in HOL4, because 1) John has always stressed the importance of readability in formal proofs, and 2) my code looks like it will be a lot simpler than John's mizar.ml or Freek's miz.ml. I know nothing of HOL4, and there is a lot I don't know in general, so you can teach me a lot.
As you expressed reservations about the theorems assoc list in database.ml, tell me how DB.fetch is implemented. You can't detect matching braces with regular expressions. Thanks! I looked at your link, and I'll study it later. I think I realized that for the emulating the miz3 code that I've actually written, I don't actually need this, so I'll write that version first. What you probably need is to define your tactic language with a grammar and write a parser for it. I think I'm done with the HOL Light campl parser, and that Vince already told me everything I need. There's a line else if c = ";" then "parse_qproof \""^(String.escaped s)^"\"" in quotexpander in system.ml, and I just write one line let parse_qproof s = (String.sub s 1 (String.length s - 1));; Now every back-quoted expression `;[...]` becomes a string with no newline or bacsklash problems. Following Freek's miz3.ml, an entire theorem/proof will be such an expression `;[...]`, and I'll just write code to turn this string into a HOL Light proof. That doesn't sound very hard to me, but maybe it is, as I'm not done yet. But maybe I'm missing something, because I don't know what tactic language, grammar or parser means. I looked at your link and got confused right away! I know about syntax and semantics, but grammar is something different! I'll try to learn it about grammar. You're going down a route that I think many people do by accident and end up in a dead end or with a broken solution. Thanks for the warning. Maybe it would be more helpful if you told me how I'm replicating work that's already been done in HOL and HOL Light, so I can profit from this work instead of reinventing the wheel. HOL4 does not have a separate tactic language. Proof scripts are written in SML directly. (The SML implementation will have a parser etc. though.) HOL4 does have a sophisticated parser for the object language of HOL terms and types, which I think I've mentioned before. I don't know what this means, but it sounds relevant and important. -- Best, Bill ------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. This 200-page book is written by three acclaimed leaders in the field. The early access version is available now. Download your free book today! http://p.sf.net/sfu/neotech_d2d_may _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
