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
>>
>>
> ----------------------------------------------------------------------------
>> --
>> 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
>>
>>
>>
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
