Le 02.04.13 21:19, Bill Richter a écrit : > Vincent, thanks for explaining this, and for your new stuff, which I haven't > understood. I had thought that preterm_of_term wouldn't go through type > inference, but it does: > > # preterm_of_term `&1 + 1`;; > > Exception: Failure "typechecking error (overload resolution)". > > So I was wrong. Thanks. No you were right, preterm_of_term indeed does no inference. Here the exception does not occur in preterm_of_term but in the parsing of `&1 + 1`. Actually, if you just type`&1 + 1`, you still get the exception:
# `&1 + 1`;; Exception: Failure "typechecking error (overload resolution)". To understand better let's say that you can turn any expression of the form: `bla` into: parse_term "bla" So your above example: preterm_of_term `&1 + 1`;; is turned into: preterm_of_term (parse_term "&1 + 1");; In the above, the type checking occurs in the call to parse_term, not in preterm_of_term. In addition, parse_term can be decomposed (roughly) as: term_of_preterm o retypecheck [] o parse_preterm o lex o explode where: - explode simply turns a string into a list of characters - lex turns this list of characters into a list of lexcodes (i.e., a list of atomic words w.r.t. HOL Light understanding of what is a word) - parse_preterm turns this into a preterm (i.e., almost like a term but without any type checking) - retypecheck checks the types - term_of_preterm gets the term out the preterm As you see, type checking only appears after parse_preterm. That's why in my last email, the hack I suggested was to do the work only until this phase. -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ ------------------------------------------------------------------------------ Minimize network downtime and maximize team effectiveness. Reduce network management and security costs.Learn how to hire the most talented Cisco Certified professionals. Visit the Employer Resources Portal http://www.cisco.com/web/learning/employer_resources/index.html _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
