是否可以为语法规则定义上下文？

Question

我正在尝试为类 C 语言定义语法。为了简单起见，它只有算术表达式、变量声明和语句块：

type_synonym vname = nat

datatype aexp =
  IntConst int
| IntVar vname
| Plus aexp aexp
| Minus aexp aexp

datatype com =
  Skip
| Let vname aexp
| Seq com com

变量声明的语法：

syntax
  "_let" :: "vname ⇒ aexp ⇒ com" ("let _ = _")

translations
  "_let v init" ⇌ "CONST Let v init"

term "let x = y"

语句块的语法：

nonterminal stmts

syntax
  "_no_stmts" :: "stmts" ("")
  "_single_stmt" :: "com ⇒ stmts" ("_")
  "_stmts" :: "com ⇒ stmts ⇒ stmts" ("_; _")

translations
  "_no_stmts" ⇀ "CONST Skip"
  "_single_stmt x" ⇀ "CONST Seq x CONST Skip"
  "_stmts x xs" ⇀ "CONST Seq x xs"

syntax
  "_stmt_block" :: "stmts ⇒ com" ("{{_}")

translations
  "_stmt_block xs" ⇀ "xs"

term "{{}"
term "{{a}"
term "{{let a = x; let b = y;}"
term "{{let a = x; let b = y; c}"

我必须使用双括号

{{

，因为单括号用于集合。

当然，我可以使用粗体大括号，这样它们就不会与集合的语法冲突。或者我可以禁用集合的语法。

但是是否可以为语法规则定义类似上下文之类的东西？例如，如果我将表达式包含在

```c ... ```

块中，则仅使用特定的语法规则：

term "```c {let a = x; let b = y;} ```"

Answer 1

我想我已经明白了：

nonterminal stmt and stmts

syntax
  "_c_code" :: "stmts ⇒ com" ("```c _ ```")
  "_empty_stmt" :: "stmts" ("")
  "_single_stmt" :: "stmt ⇒ stmts" ("_")
  "_stmts" :: "stmt ⇒ stmts ⇒ stmts" ("_; _")
  "_block" :: "stmts ⇒ stmt" ("{_}")
  "_let" :: "vname ⇒ aexp ⇒ stmt" ("let _ = _")

translations
  "_c_code c" ⇀ "_block c"
  "_block (_empty_stmt)" ⇌ "CONST Skip"
  "_block (_single_stmt c)" ⇀ "c"
  "_block (_stmts c (_empty_stmt))" ⇀ "c"
  "_block (_stmts c (_single_stmt xs))" ⇌ "CONST Seq c xs"
  "_block (_stmts c (_stmts x xs))" ⇌ "CONST Seq c (_block (_stmts x xs))"
  "_let v init" ⇌ "CONST Let v init"

您可以使用

print_syntax

命令来调试语法规则。

_c_code

可以为空 (

_empty_stmt

)，可以包含单个语句 (

_single_stmt

)，也可以包含

;

分隔的语句列表 (

_stmts

)。

单个语句可以是

let

或

{ }

块。

一些例子：

term "```c ```"
term "```c let a = x ```"
term "```c let a = x; let b = y ```"
term "```c let a = x; let b = y; let c = z ```"
term "```c { } ```"
term "```c { let a = x } ```"
term "```c { let a = x; let b = y } ```"
term "```c { let a = x; let b = y; let c = z } ```"
term "```c let a = x; { let b = y } ```"
term "```c let a = x; { let b = y; let c = z } ```"
term "```c { { { let a = x } }; let b = y; }; let c = z ```"