Is it possible to define a context for syntax rules?

Question

I'm trying to define a syntax for a C-like language. Let's for the sake of simplicity it has only arithmetic expressions, variable declarations and blocks of statements:

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

The syntax for variable declarations:

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

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

term "let x = y"

The syntax for blocks of statements:

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}"

I have to use double braces {{ because single braces are used for sets.

For sure, I can use bold braces so they will not confilct with a syntax for sets. Or I can disable syntax for sets.

But is it possible to define something like a context for syntax rules? For instance if I enclose an expression into ```c ... ``` block then only particular syntax rules are used:

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

Answer 1

I think I've got it:

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"

You can use print_syntax command to debug the grammar rules.

_c_code can be empty (_empty_stmt), can contain single statement (_single_stmt), or can contain a ;-separated list of statements (_stmts).

A single statement can be either let, or { }-block.

Some examples:

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 ```"