Lu Zhao wrote:
> Hi,
>
> When I use match_term with some types unspecified, HOL always generates
> a message similar to the following:
>
> <<HOL message: inventing new type variable names: 'a, 'b>>
>
> Is there a way to depress the message so that I don't have to see a long
> list of messages. Specifying the types is not a good option since the
> matched terms have multiple types at the same sub-term position.
Those messages are not being emitted by match_term, but rather by the
parser. I expect your code looks something like
fun mycode t =
... match_term ``pattern term`` t ...
Every time you call the mycode function, the parser is run on the string
between the `` ... `` . There are two ways around this. Best practice
would be to avoid calling the parser at all. You might also lift the
parsing out of the function so that the pattern is parsed just once:
val pattern = ``pattern term``
fun mycode t = ... match_term pattern t ...
This would give one message as the SML code was loaded. Finally, you
can turn that particular message off, by using
set_trace "notify type variable guesses" 0
at some stage. This call adjusts a global variable that is consulted
when parsing occurs. If you wanted to change your code the absolute
least, you could do
fun myfun t = trace ("notify type variable guesses", 0) mycode t
This would call mycode on the given argument while temporarily setting
the trace to zero (and resetting it to its old value when the call
returned).
Michael.
------------------------------------------------------------------------------
Register Now for Creativity and Technology (CaT), June 3rd, NYC. CaT
is a gathering of tech-side developers & brand creativity professionals. Meet
the minds behind Google Creative Lab, Visual Complexity, Processing, &
iPhoneDevCamp as they present alongside digital heavyweights like Barbarian
Group, R/GA, & Big Spaceship. http://p.sf.net/sfu/creativitycat-com
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
