Le 17.04.13 00:31, Bill Richter a écrit : > > That's great you're changing your Q-like module right now to use > > the parser instead of strings. > > I'll do it if the new preterm parser gets integrated in HOL Light. > > Wow, I meant it was great you were using the parser in HOL4! But that's even > better, if you're porting your HOL4 Q-like module to HOL Light. Am I getting > something wrong?
Let me clarify: - HOL4 has a module called "Q" (not developped by me) which basically replaces some tactics taking a term as input by the same tactics taking a preterm as input: * taking preterms as input can be done easily because HOL4 contains a preterm parser by default * the benefit is that it allows to remove type annotations (for the same reasons you would like a preterm parser) in many contexts; for instance, consider a proof where you use EXISTS_TAC as follows: # EXISTS_TAC `f (x:A) (y:B) :C` If f already appears in the context of the goal (either the assumptions or the conclusion) then there is somehow a way to know that f has type `:A->B->C` and thus we would reasonably like HOL(4/Light) to find it itself rather than provide it explicitly. This precisely what the Q module does in HOL4, it allows you to do instead: # Q.EXISTS_TAC `'f x y` (note that I used my notation with a " ' " at the beginning to show that we are using the a preter parser here; the notation is actually different in HOL4, but it is not important for your understanding) And similarly for many other tactics which require a term as input - I did recently a module which does the same job for HOL Light (this is why I always refer to it as the "Q-like module"). For reasons that do not need to be mentionned here, this module is called "Pa" (for *Pa*rse/er/ing/whatever), but, right now instead of working with preterms, it works with strings; precisely because there is no preterm dedicated parser in HOL Light. Therefore it has the same problems as what you mentionned in the post at the origin of this conversation: problems in case of new lines and backslashes must be doubled. If the preterm parser was present by default in HOL Light, I could update my Pa module to take preterms instead of strings as input, and these problems would be solved. -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ ------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
