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
------------------------------------------------------------------------------
ThinkGeek and WIRED's GeekDad team up for the Ultimate
GeekDad Father's Day Giveaway. ONE MASSIVE PRIZE to the
lucky parental unit. See the prize list and enter to win:
http://p.sf.net/sfu/thinkgeek-promo
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
