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