How do I define syntax and translations for this datatype?

So currently I have the following datatype:

datatype ('a) action = Action (name: string) "int option" "int option" "'a option" "bool option" "string option"

I want to define syntax such that the term example(3, 4, True) will be translated to Action ''example'' (Some 3) (Some 4) None (Some True) None.

What I've done so far is the following:

syntax
  "_example" :: "[int, int, bool] ⇒ 'a action" ("3example'((_), (_), (_)')" [60, 60, 60] 60)
translations
  "_example a b c"  ⇌ "CONST Action ''example'' (Some a) (Some b) None (Some True) None"

Unfortunately, Isabelle complains that the right hand side contains too many variables.

Error in syntax translation rule: rhs contains extra variables
("_example" a b c) ↝
  ("\<^const>Scratch.action.Action" ("_String" ''example'')
    (Some a) (Some b) None (Some True) None)

I've seen other syntax that uses variables in the left hand side and their translations work. May I know why doesn't mine work and how can I fix this?

Thanks in advance!

Solution

There are a couple of issues in your example that explain the error message you get:

Given an AST rewrite rule (lhs, rhs), it must hold that all variables in rhs must also occur in lhs. Since you are defining two AST rewrite rules simultaneously via ⇌, namely a parse rule (⇀) and a print rule (↽), it turns out that variable c does not occur in the lhs of the print rule. I would guess that the intended purpose of c was to use it in the rhs instead of True.
While processing the rhs, Isabelle assumes Some and None to be variables instead of constants, so you need to use the CONST prefix to enforce treatment as constants (e.g., CONST None and CONST Some a).
String literals such as ''example'' are also treated as variables. In this case, adding CONST would not do, so you could use [CHR 0x65, CHR 0x78, CHR 0x61, CHR 0x6d, CHR 0x70, CHR 0x6c, CHR 0x65] instead, which is cumbersome. I'm not aware of any alternative.
You need to add outermost parentheses when using block indentation in your mixfix annotation, i.e., you need to write "(3example'((_), (_), (_)'))" instead of "3example'((_), (_), (_)')".

So, for your particular example my suggestion is to use an abbreviation as follows:

abbreviation example :: "[int, int, bool] ⇒ 'a action" ("(3example'((_), (_), (_)'))" [60, 60, 60] 60) where
  "example(a, b, c) ≡ Action ''example'' (Some a) (Some b) None (Some c) None"

For further information on syntax transformations and mixfix annotations please refer to Sections 8.5 and 8.2 respectively in The Isabelle/Isar Reference Manual