Isabelle中能否为语法规则定义上下文以规避语法冲突？

Isabelle支持通过局部语法修改、上下文限定翻译等方式，实现类似代码块的专属语法环境，让你在特定范围内用单花括号编写语句块，同时不干扰全局的集合语法。以下是几种可行方案：

方案1：局部Locale语法重载（推荐） #

通过定义Locale封装类C语法规则，激活后即可在局部使用单花括号，退出后自动恢复原语法：

(* 假设你已定义的基础datatype *)
datatype var = Var string
datatype exp = Num int | VarExp var
datatype stmt = Block "stmt list" | Declare var | Assign var exp

(* 全局默认的双花括号语句块语法 *)
syntax
  "_block" :: "stmt list ⇒ stmt"  ("{{_}}")
translations
  "{{s}}" ⇌ "CONST Block s"

(* 定义类C语法的Locale *)
locale c_syntax =
begin
  syntax
    "_c_block" :: "stmt list ⇒ stmt"  ("{_}")
  translations
    "{s}" ⇌ "CONST Block s"
end

(* 激活Locale，进入类C语法上下文 *)
interpretation c_syntax .

(* 直接用单花括号编写语句块 *)
term "{Declare (Var ''x''), Assign (Var ''x'') (Num 5)}"

(* 退出上下文，恢复原集合语法 *)
no_notation "_c_block" ("{_}")

方案2：自定义标记式代码块 #

模拟你想要的代码块风格，定义一对标记包裹代码块，内部自动启用单花括号解析：

(* 定义代码块的起始和结束标记 *)
syntax
  "_c_code_start" :: "unit ⇒ 'a"  ("c⟨")
  "_c_code_end" :: "'a ⇒ stmt"  ("⟩")

(* 定义翻译规则，将标记内的{...}映射为语句块 *)
translations
  "c⟨ {s} ⟩" ⇌ "CONST Block s"
  (* 可选：添加分号分隔语句的支持 *)
  "c⟨ stmt ; stmts ⟩" ⇌ "CONST Seq stmt (c⟨ stmts ⟩)"

(* 使用示例 *)
term "c⟨ {Declare (Var ''x''), Assign (Var ''x'') (Num 5)} ⟩"

方案3：临时屏蔽集合语法 #

如果只是短代码片段需要单花括号，可以临时禁用集合的单花括号解析：

(* 关闭歧义警告，临时移除集合的单花括号符号 *)
declare [[syntax_ambiguity_warnings=false]]
no_notation Set.set ("{_}")

(* 临时绑定单花括号到你的语句块 *)
syntax
  "_block" :: "stmt list ⇒ stmt"  ("{_}")
translations
  "{s}" ⇌ "CONST Block s"

(* 编写类C风格代码 *)
term "{Declare (Var ''x''), Assign (Var ''x'') (Num 5)}"

(* 恢复原集合语法和警告 *)
notation Set.set ("{_}")
declare [[syntax_ambiguity_warnings=true]]

关键注意点 #

• 方案1的Locale方式最安全，完全隔离局部和全局语法，不会引发歧义。
• 方案2的标记式代码块更贴近你想要的代码块风格，但需要额外处理语句分隔逻辑。
• 方案3适合临时快速测试，但需注意及时恢复原语法，避免影响后续代码。

内容的提问来源于stack exchange，提问作者Denis