I am trying to understand the code of Rely Guarantee in Isabelle/HOL and feel confused about the syntax
and translation
keyword in
https://isabelle.in.tum.de/library/HOL/HOL-Hoare_Parallel/RG_Syntax.html
syntax
"_Assign" :: "idt ⇒ 'b ⇒ 'a com" ("(´_ :=/ _)" [70, 65] 61)
"_Cond" :: "'a bexp ⇒ 'a com ⇒ 'a com ⇒ 'a com" ("(0IF _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61)
"_Cond2" :: "'a bexp ⇒ 'a com ⇒ 'a com" ("(0IF _ THEN _ FI)" [0,0] 56)
"_While" :: "'a bexp ⇒ 'a com ⇒ 'a com" ("(0WHILE _ /DO _ /OD)" [0, 0] 61)
"_Await" :: "'a bexp ⇒ 'a com ⇒ 'a com" ("(0AWAIT _ /THEN /_ /END)" [0,0] 61)
"_Atom" :: "'a com ⇒ 'a com" ("(⟨_⟩)" 61)
"_Wait" :: "'a bexp ⇒ 'a com" ("(0WAIT _ END)" 61)
"_PAR" :: "prgs ⇒ 'a" ("COBEGIN//_//COEND" 60)
I am confused about three questions
(1) Why there always be an underscore _Assign
before the name?
(2) What's the meaning of slash and single quote in(´_ :=/ _)
and double slash in COBEGIN//_//COEND
(3) Why there is a zero before the mixfix symbol 0IF _ THEN _ FI
translations
"´x := a" ⇀ "CONST Basic «´(_update_name x (λ_. a))»"
"IF b THEN c1 ELSE c2 FI" ⇀ "CONST Cond ⦃b⦄ c1 c2"
"IF b THEN c FI" ⇌ "IF b THEN c ELSE SKIP FI"
"WHILE b DO c OD" ⇀ "CONST While ⦃b⦄ c"
"AWAIT b THEN c END" ⇌ "CONST Await ⦃b⦄ c"
"⟨c⟩" ⇌ "AWAIT CONST True THEN c END"
"WAIT b END" ⇌ "AWAIT b THEN SKIP END"
print_translation ‹
let
fun quote_tr' f (t :: ts) =
Term.list_comb (f $ Syntax_Trans.quote_tr' \<^syntax_const>‹_antiquote› t, ts)
| quote_tr' _ _ = raise Match;
val assert_tr' = quote_tr' (Syntax.const \<^syntax_const>‹_Assert›);
fun bexp_tr' name ((Const (\<^const_syntax>‹Collect›, _) $ t) :: ts) =
quote_tr' (Syntax.const name) (t :: ts)
| bexp_tr' _ _ = raise Match;
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const \<^syntax_const>‹_Assign› $ Syntax_Trans.update_name_tr' f)
(Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
[(\<^const_syntax>‹Collect›, K assert_tr'),
(\<^const_syntax>‹Basic›, K assign_tr'),
(\<^const_syntax>‹Cond›, K (bexp_tr' \<^syntax_const>‹_Cond›)),
(\<^const_syntax>‹While›, K (bexp_tr' \<^syntax_const>‹_While›))]
end
›
And I can't understand the meaning of code above. Where can I find reference about the use of translations
and print_translation
The information that you seek can be found in chapter 8 of the standard reference manual of Isabelle (Isar-ref or The Isabelle/Isar Reference Manual by Makarius Wenzel). More specifically, see subsections 8.2, 8.4 and 8.5 in the reference manual.
Personally, I am not familiar with the implementation details of the syntax transformations in Isabelle, so my answer will rely on what is already stated in the documentation. Thus, my advice is to use the reference manual as the primary source of information. If, having studied the reference manual, you still have further questions, you may wish to try the mailing list of Isabelle or Zulip chat.
syntax
is explained in subsection 8.5.2 of the reference manual. In your question, _Assign
is a syntax constant of the syntax declaration, which is merely a name among the syntactic entities of the Isar language (see subsection 3.2 in the reference manual). Technically, the underscore should have no special meaning, but the use of an underscore at the beginning of the names of the syntax constants is a convention and it seems that only the names of the syntax constants can start with an underscore.´
in the mixfix template (´_ :=/ _)
does not have any special meaning. However, /
allows (but does not force) a line break and //
forces a line break during pretty printing.(n
with n
being a natural number, opens a pretty printing block in mixfix annotations. The number n
specifies the block indentation (that is, the number of spaces that are added when a line break occurs in the block). However, if n
is not specified, it should default to 0
. So, I am not entirely certain why 0
was, indeed, needed in this instance. You may wish to investigate further.The commands translations
and print_translation
are explained in subsections 8.5.2 and 8.5.3, respectively. Thus, translations
can be used for the specification of the rewrite rules on ASTs, whereas print_translations
allow arbitrary manipulations of inner syntax for printing (keep in mind the rough “term->AST->pretty printed text” sequence). In this instance, you can examine the effects of the invocation of the print_translation
directly as follows
lemma "´a := b = c"
(*Basic (a_update (λ_. b)) = c*)
oops
print_translation ‹…›
lemma "´a := b = c"
(*´a := b = c*)
oops
Hope this helps, or, at least, points you in the direction of the relevant resources.