скрывать операторов, чтобы избежать двусмысленности в AST

Question

Я пробовал пример из официального руководства Isabelle. Я заменил # на : и @ с ++, чтобы иметь тот же синтаксис, что и Haskell. Теперь я получаю предупреждения о двусмысленности в АСТ. Я знаю, что я могу скрывать функции с hide_const, но это не работает для операторов в нотации infix. Как я могу скрыть операторов в Изабель?

Точное предупреждающее сообщение:

Ambiguous input⌂ produces 2 parse trees: 
    ("\<^const>HOL.Trueprop" 
    ("\<^const>HOL.eq" ("\<^const>Map.map_add" ("/<^const>toylist.list.Nil") ("_position" ys)) 
     ("_position" ys))) 
    ("\<^const>HOL.Trueprop" 
    ("\<^const>HOL.eq" ("\<^fixed>app" ("\<^const>toylist.list.Nil") ("_position" ys)) ("_position" ys))) 
Fortunately, only one parse tree is well-formed and type-correct, 
but you may still want to disambiguate your grammar or your input. 

Answer 1

Скрытие оператора не удаляет его обозначения. Для удаления существующих обозначений имеется отдельная команда no_notation. В Isabelle/HOL ++ привязан к map_add, как видно из предупреждения о двусмысленности. Вы можете удалить его следующим образом.

no_notation map_add (infixl "++" 100) 

Обратите внимание, что вы должны повторить точные параметры приоритета, с которыми была объявлена ​​нотация, подлежащая удалению. Нет простого способа найти декларацию обозначений для константы, но это хороший стиль для объявления нотации, близкой к объявлению константы; Ctrl -clicking на константе приводит вас к его объявлению.

Относительно :, это по умолчанию связано с Set.member. Вы можете удалить его с помощью no_notation Set.member ("(_/ : _)" [51, 51] 50).

Если только для демонстрационных или поисковых целей, я рекомендую не слишком сильно менять синтаксис по умолчанию Isabelle. В противном случае другим пользователям Isabelle будет сложно читать ваш код, и ваши теории не будут совместимы с другими. Причина в том, что при импорте различных теорий нотации сливаются аддитивно. Таким образом, если вы удалите запись ++ для map_add в теории A и теория B импортирует теорию A и некоторые другие теории, производных от Main, но не A, то неоднозначность для ++ возвращается в теории B.

Answer 2

Вы можете использовать команду no_notation, которая принимает те же аргументы, которые использовались во время объявления нотации с командой notation (или в пределах постоянного определения).

Оба символа : и ++ уже используются Set.member и map_add соответственно. Таким образом, вы должны найти эти объявления нотации и использовать их в no_notation:

no_notation Set.member ("(_/ : _)" [51, 51] 50) 
no_notation map_add (infixl "++" 100) 

Затем вы можете продолжить так же, как вы, конечно, уже есть, и путем удаления теперь уже устаревшего синтаксиса для списка:

no_notation Cons (infixr "#" 65) 
notation Cons (infixr ":" 65) 

no_notation List.append (infixr "@" 65) 
notation List.append (infixr "++" 65) 

term "x : (xs ++ ys)" 

Обозначение для Set.member: не пропустит, так как уже есть xsymbol/utf-8 нотация ∈. Я думаю, что map_add не используется, но тогда вы можете использовать бесплатную нотацию @.