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