Le 01.05.13 00:29, Bill Richter a écrit : > Thanks, Vince! It look like your q.ml and the HOL4 version are both > counterexamples to what I've been posting, that the only place where > retypecheck is used with a nonempty environment is in John & Freek's > Mizar-like code. I'm really happy to have been wrong! I can definitely see > some similarities between my code and yours, e.g. > > let CONTEXT_TAC ttac (asms,c as g) = > let vs = frees c @ freesl (map (concl o snd) asms) in > > although I don't know how to run your code and can't really read it. To run the code, just type: #use "q.ml";;
If you don't understand particular things, send me a private message. > Great! Thanks for not telling me about this before, Well, I told you about this module a while ago... > because I found writing my code to be a very interesting exercise! I do > prefer my code, at this point, maybe just because I can read mine. Can you > try to compare my code to yours? I'll do when I have the time. > Does yours do anything mine doesn't do, or vice versa? I only had a quick look so I can't really tell. It seems there are tactics that exist in my code but not in yours, and vice versa. For EXISTS_TAC, my code also extracts the type of the bound variable and enforces the type of witness to be the same. For SUBGOAL_THEN, it enforces the type of the overall expression to be boolean (thanks to a remark by Michael Norrish, when I first submitted this module on this mailing list). Same thing for SUBGOAL_TAC. > Did I not check for some important error conditions? Are there bugs I > will run into? I think you said that yours isn't quite finished yet, and > that you were going to do a great deal more. No, I was talking about other tactics. Regarding this module, I just said that it would probably be better to use preterms instead of strings (or you special parser for strings). > Can you say anything about how you learned to write your code? Not really :-( I know Ocaml and I have read the sources of HOL Light. All the info is in here, but you have to dig to find it :-) > I looked at the HOL4 version > http://hol.sourceforge.net/kananaskis-8-helpdocs/help/src-sml/htmlsigs/Q.html > and can see some similarity: > > fun EXISTS_TAC q (g as (asl, w)) = > let val ctxt = free_varsl (w::asl) > [...] > fun ptm_with_ctxtty ctxt ty q = > let val q' = QUOTE "(" :: (q @ [QUOTE "):", ANTIQUOTE(ty_antiq ty), QUOTE > ""]) > in Parse.parse_in_context ctxt (normalise_quotation q') > end > > Perhaps you can help me with next stage of my project, to write a miz3-type > interface for general HOL Light code. The one thing I don't like about miz3 > is the "by" list, an unordered comma-separated list. Why not keep the rest > of the miz3 interface and use regular HOL Light proofs? It would be easier > to write, wouldn't it? I have a few questions and points: > > 1) Is there already an HOL4 version of anything like this? > > 2) Using my parser/`"[...]`/string idea, all I need is to write a function to > turn a huge string into from a miz3-looking proof to an HOL Light proof. It > seems to me that this an easy project if one has good regexp/replace > functions, and I think that's in the Ocaml str library, described e.g. in > Chapter 24 of the official ocaml manual. I don't believe that str is ever > used in HOL Light. Do you know why that is? I guess just because Jon did not need it. I guess you could load it live from the ocaml console though. > Does HOL4 use any fancy SML regexp/replace functions? No idea. > If we don't use str, I suspect the plan is to to use (lex o explode) and then > play lex games. I don't know the syntax of miz3 proofs so I can't tell. > I already did something like that in a different version of the code, > something that borrows from Marco's code: > > map (fun l -> match l with > Ident s -> s > | _ -> raise Noparse) ((lex o explode) vars) > > Do you have advice on how to learn more about how to use lexcode lists to > turn one type of proof to another? Not really... > 3) Your (asms,c as g) looks a lot like things I saw in tactics.ml. > Does this mean that g is equal to the ordered pair (asms,c)? Yes. > Do you know where that feature of "as" is explained? http://caml.inria.fr/pub/docs/manual-ocaml/patterns.html#@manual.kwd7 > 4) How can we debug code that explicitly uses the goal, as you do with (g as > (asl, w))? Give me a concrete situation. -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ ------------------------------------------------------------------------------ Introducing AppDynamics Lite, a free troubleshooting tool for Java/.NET Get 100% visibility into your production application - at no cost. Code-level diagnostics for performance bottlenecks with <2% overhead Download for free and get started troubleshooting in minutes. http://p.sf.net/sfu/appdyn_d2d_ap1 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
