1open HolKernel Parse boolLib
2
3val _ = new_theory "mergeGrammarsA1";
4
5(* demonstrating what should happen when a theory ancestry graph looks like
6
7        bool
8        / \
9       A1  A2
10        \ /
11         B
12
13   and
14
15   - A1 sets the fixity of equality (using set_fixity) to something
16     other than its default;
17   - A2 doesn't mention the parsing of equality at all
18
19   Q: What should happen in B?
20
21   A #1: the behaviour, as of 3 October 2016 is to "merge" the
22   ancestral grammars by taking what is effectively a union operation
23   over the rules. This results in a grammar with two rules for
24   equality, and one that will report ambiguities at every computation
25   of the precedence matrix.
26
27   A #2: I believe the desired behaviour should be to merge the
28   history of changes to the grammars. Assuming A2 doesn't do anything
29   to equality, this should result in B's grammar being the same as
30   A1's.
31
32   - -
33
34   Note that it's harder to see a problematic behaviour in the global
35   grammar because this is updated by a sequence of calls that are
36   made as the theories load. Instead, the problem is apparent in the
37   value of
38
39      #2 mergeGrammarsBTheory.mergeGrammarsB_grammars
40
41*)
42
43val _ = set_fixity "=" (Infix(NONASSOC, 450));
44
45val a_theorem = store_thm(
46  "a_theorem",
47  ``x:bool = x /\ y = y``,
48  REWRITE_TAC[]);
49
50val _ = export_theory();
51