Re: [Hol-info] infix exception

[Michael N. <Mic...@ni...>]

On 22/06/10 13:09, xiaoyu xu wrote:
> I met an exception when I "set_fixity "divides" (Infixr 450)"

> I checked the exception.
> It said
> Exception raised at Parse.add_rule:
> Grammer error: Attempt to have differently associated infixes (RIGHT and
> NONASSOC) at same level(450)

> I looked into the kananaskis-5-reference, I found that I couldn't define
> an infix at this level, because this was where other notation was. I
> solved it, use "set_fixity "divides" (Infixr 451)" or "set_fixity
> "divides" (Infix(NONASSOC, 450))" instead.

Great; both of these are plausible.

> My questions are:

> 1.what are the differences between (Infixr 450) and (Infix(NONASSOC,
> 450))? Which file introduces this?

These functions are defined in src/parse/Parse.sig and src/parse/Parse.sml.  Behaviourally, the difference between Infixr 450 and Infix(NONASSOC, 450) is that the former will make the infix be right-associated, and the latter will cause an error if you attempt to have multiple infixes in a row.

Thus, if divides is right-associative

   3 divides 4 divides 12

this would parse to mean

   3 divides (4 divides 12)

This is nonsense because 4 divides 12 is true, of boolean type.  Thus the expression would be

   3 divides T

So, it's appropriate for divides to be NONASSOC.  So, if you write

   3 divides 4 divides 12

you will get a parse error.  For example, the equality constant is also non-associative, and if I write

   > ``3 = 4 = 12``;

I get back

   Don't expect to find a = in this position after a =
   at line 14, character 8 and at line 14, character 4.
   Exception- [...]

> 2.How can I know at which level I can define an infix, at which I can't?

Look at the output of

   term_grammar()

I see, among other things

   (450)  TM  ::=  TM "≼" TM  [<<=] | TM "<<=" TM | TM "⊂" TM  [PSUBSET] |
                   TM "⊆" TM  [SUBSET] | TM "PSUBSET" TM | TM "SUBSET" TM |
                   TM "≥" TM  [>=] | TM "≤" TM  [<=] | TM ">=" TM |
                   TM "<=" TM | TM ">" TM | TM "<" TM | TM "RSUBSET" TM |
                   TM "≠" TM | TM "<>" TM
                   (non-associative)

This tells you what is at the 450 level, and also tells you that this level is non-associative.

> 3.Should I clear the definitions after my work, how can I clear
> that?  Thank you very much!

This depends.  Sometimes you want fixity declarations to affect future theories.  In this case, use set_fixity and other similar functions, and do export_theory() at the end of your file.  If you don't want the effect to last, you can use temp_set_fixity, which changes the grammar, but does not cause the change to be exported with the theory.  There are also functions like remove_termtok that will allow you to reverse changes.  For more on remove_termtok, see the Reference manual, or do

   help "remove_termtok";

I hope this helps,
Michael