The printer prints spaces if the printing rules call for it, or if doing so would cause the lexer to lex the tokens badly. The token breaking up will pick the longest token in the current input. So, if it sees -b-> and -b- is a token, it will take that.
If the input stream is not a mish-mash, the longest alphanumeric
identifier is taken, or the longest symbolic identifier is taken,
regardless of whether or not the user has "reserved" them in advance.
This allow multi-character variable names to be lexed as one would want.
Michael
On 27/06/12 10:21 PM, "Mark" wrote:
> I see, and the printer always inserts spaces presumably. What about if
> there is no longest (e.g. if "-b-" and "b->" were both infixes, but not
> "-b->")?
>
> on 27/6/12 12:23 PM, Michael Norrish <michael.norr...@nicta.com.au> wrote:
>
>> By taking the longest match against the set of known "keywords". If you
>> want those other interpretations you introduce some extra spaces.
>>
>> x - b -> y
>>
>> for example.
>>
>> On 27/06/12 9:03 PM, "Mark" wrote:
>>> How does the HOL4 parser deal with the associated potential ambiguities?
>>> E.g. ``x -b-> y`` getting parsed as infix "-b->" applied to ``x`` and
>> ``y``,
>>> as opposed to (say) infix "->" applied to ``x - b`` and ``y``?
>>>
>>> Mark.
>>>
>>> on 27/6/12 11:22 AM, Michael Norrish <michael.norr...@nicta.com.au>
> wrote:
>>>
>>>> On 27/06/2012, at 18:21, "Mark" <m...@proof-technologies.com> wrote:
>>>>
>>>>> The name "seg<" is irregular, in that it combines both alpha-numeric
> and
>>>>> symbolic characters. Any names can be used for constants and variables
>>> in
>>>>> the HOL logic, but HOL Light (and HOL4 I think) have no mechanism for
>>>>> *parsing* irregular names. So defining a constant called "seg<" by
>>>>> supplying a term quotation won't work.
>>>>
>>>> As it happens HOL4 will parse "irregular names" of the sort you
> describe.
>>>> The trick is to define the underlying constant with a nice name, and to
>>> then
>>>> do something like
>>>>
>>>> val _ = overload_on ("seg<", ``seglt``)
>>>>
>>>> where seglt is the "nice name". For example, my theory of the lambda
>>>> calculus uses -b-> as an infix beta-reduction arrow. With Unicode on,
>> you
>>>> can get the same arrow with an inserted Greek beta.
>>>>
>>>> Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
