Thanks, Freek, Ramana and Vincent! I think (assoc thm !theorems) gives a nicer solution:
RK> In HOL Light I guess there's no database of theorems indexed by RK> names? That would be one way to avoid having to use Obj.magic. Yes! The database is an association listtheorems, which is 2212 lines in hol_light/database.ml. We can access the database without Obj.magic or Toploop by e.g. # assoc "ODD" !theorems;; val it : thm = |- (ODD 0 <=> F) /\ (!n. ODD (SUC n) <=> ~ODD n) We can get MESON_TAC by building a similar association list: let thmlist_tactics = ref([]: (string * (thm list -> tactic))list);; thmlist_tactics := [ "MESON_TAC",MESON_TAC; "SIMP_TAC",SIMP_TAC; "REWRITE_TAC",REWRITE_TAC; "SET_TAC",SET_TAC ];; assoc "MESON_TAC" !thmlist_tactics;; A larger version of thmlist_tactics (and thm_tactics and tactics), ought to be be in the HOL_Light distribution, I think. I'll post in bit my first shot at a miz3 interface for HOL Light. Freek, I think I'll need some help making design decisions, and maybe coding too. Vince, thanks for explaining the magic features (which Freek only uses in exec_phrase, and only Toploop.parse_toplevel_phrase) are undocumented: VA> It makes use of some quite undocumented features of Ocaml VA> (Obj.magic and Toploop.getvalue). John uses this somewhere VA> (help.ml if I remember well). It's update_database.ml, which I was reading while fighting through exec_phrase of miz3.ml last night, and that's how I stumbled onto database (so thanks, Freek!): (poisson)hol_light> grep Toploop.execute_phrase * update_database.ml:let exec = ignore o Toploop.execute_phrase false Format.std_formatter (poisson)hol_light> grep Toploop.getvalue * update_database.ml: Obj.magic (Toploop.getvalue "buf__");; The Obj.magic/Toploop stuff doesn't seem crucial, but rather a speedup feature, as we can update the theorems database with :=. VA> That's precisely the difference between the object language (HOL) VA> and the meta language (ocaml): ocaml is the meta language of HOL VA> Light so you can control HOL Light through ocaml, but ocaml is not VA> its own meta language Thanks, Vince, that's very helpful. VA> (that's why we have to go through tricky undocumented features to VA> allow such a behavior). Did I show this wasn't true in this theorem biz here, and did Ramana show it wasn't true in HOL4 with DB.fetch? RK> (Side note: some languages are their own meta-languages, like RK> Scheme, where a quoted expression is a value I didn't know to call it a meta-language, Ramana, but the lure of Scheme has been bugging me for a while, as a standard exercise in Scheme is to write a Scheme->Scheme interpreter using quotes. Would it be easy for HOL to get a similar quote feature? -- Best, Bill ------------------------------------------------------------------------------ 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
