# Theory OG_Syntax

theory OG_Syntax
imports OG_Tactics Quote_Antiquote
```theory OG_Syntax
imports OG_Tactics Quote_Antiquote
begin

text‹Syntax for commands and for assertions and boolean expressions in
commands ‹com› and annotated commands ‹ann_com›.›

abbreviation Skip :: "'a com"  ("SKIP" 63)
where "SKIP ≡ Basic id"

abbreviation AnnSkip :: "'a assn ⇒ 'a ann_com"  ("_//SKIP" [90] 63)
where "r SKIP ≡ AnnBasic r id"

notation
Seq  ("_,,/ _" [55, 56] 55) and
AnnSeq  ("_;;/ _" [60,61] 60)

syntax
"_Assign"      :: "idt ⇒ 'b ⇒ 'a com"    ("(´_ :=/ _)" [70, 65] 61)
"_AnnAssign"   :: "'a assn ⇒ idt ⇒ 'b ⇒ 'a com"    ("(_ ´_ :=/ _)" [90,70,65] 61)

translations
"´x := a" ⇀ "CONST Basic «´(_update_name x (λ_. a))»"
"r ´x := a" ⇀ "CONST AnnBasic r «´(_update_name x (λ_. a))»"

syntax
"_AnnCond1"    :: "'a assn ⇒ 'a bexp  ⇒ 'a ann_com  ⇒ 'a ann_com ⇒ 'a ann_com"
("_ //IF _ /THEN _ /ELSE _ /FI"  [90,0,0,0] 61)
"_AnnCond2"    :: "'a assn ⇒ 'a bexp  ⇒ 'a ann_com ⇒ 'a ann_com"
("_ //IF _ /THEN _ /FI"  [90,0,0] 61)
"_AnnWhile"    :: "'a assn ⇒ 'a bexp  ⇒ 'a assn ⇒ 'a ann_com ⇒ 'a ann_com"
("_ //WHILE _ /INV _ //DO _//OD"  [90,0,0,0] 61)
"_AnnAwait"    :: "'a assn ⇒ 'a bexp  ⇒ 'a com ⇒ 'a ann_com"
("_ //AWAIT _ /THEN /_ /END"  [90,0,0] 61)
"_AnnAtom"     :: "'a assn  ⇒ 'a com ⇒ 'a ann_com"   ("_//⟨_⟩" [90,0] 61)
"_AnnWait"     :: "'a assn ⇒ 'a bexp ⇒ 'a ann_com"   ("_//WAIT _ END" [90,0] 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"   ("IF _ THEN _ FI" [0,0] 56)
"_While_inv"   :: "'a bexp ⇒ 'a assn ⇒ 'a com ⇒ 'a com"
("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
"_While"       :: "'a bexp ⇒ 'a com ⇒ 'a com"
("(0WHILE _ //DO _ /OD)"  [0, 0] 61)

translations
"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 INV i DO c OD" ⇀ "CONST While ⦃b⦄ i c"
"WHILE b DO c OD" ⇌ "WHILE b INV CONST undefined DO c OD"

"r IF b THEN c1 ELSE c2 FI" ⇀ "CONST AnnCond1 r ⦃b⦄ c1 c2"
"r IF b THEN c FI" ⇀ "CONST AnnCond2 r ⦃b⦄ c"
"r WHILE b INV i DO c OD" ⇀ "CONST AnnWhile r ⦃b⦄ i c"
"r AWAIT b THEN c END" ⇀ "CONST AnnAwait r ⦃b⦄ c"
"r ⟨c⟩" ⇌ "r AWAIT CONST True THEN c END"
"r WAIT b END" ⇌ "r AWAIT b THEN SKIP END"

nonterminal prgs

syntax
"_PAR" :: "prgs ⇒ 'a"              ("COBEGIN//_//COEND" [57] 56)
"_prg" :: "['a, 'a] ⇒ prgs"        ("_//_" [60, 90] 57)
"_prgs" :: "['a, 'a, prgs] ⇒ prgs"  ("_//_//∥//_" [60,90,57] 57)

"_prg_scheme" :: "['a, 'a, 'a, 'a, 'a] ⇒ prgs"
("SCHEME [_ ≤ _ < _] _// _" [0,0,0,60, 90] 57)

translations
"_prg c q" ⇌ "[(CONST Some c, q)]"
"_prgs c q ps" ⇌ "(CONST Some c, q) # ps"
"_PAR ps" ⇌ "CONST Parallel ps"

"_prg_scheme j i k c q" ⇌ "CONST map (λi. (CONST Some c, q)) [j..<k]"

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;

fun annquote_tr' f (r :: t :: ts) =
Term.list_comb (f \$ r \$ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
| annquote_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 annbexp_tr' name (r :: (Const (@{const_syntax Collect}, _) \$ t) :: ts) =
annquote_tr' (Syntax.const name) (r :: t :: ts)
| annbexp_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;

fun annassign_tr' (r :: Abs (x, _, f \$ k \$ Bound 0) :: ts) =
quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} \$ r \$ Syntax_Trans.update_name_tr' f)
(Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
| annassign_tr' _ = raise Match;

fun Parallel_PAR [(Const (@{const_syntax Cons}, _) \$
(Const (@{const_syntax Pair}, _) \$ (Const (@{const_syntax Some},_) \$ t1 ) \$ t2) \$
Const (@{const_syntax Nil}, _))] = Syntax.const @{syntax_const "_prg"} \$ t1 \$ t2
| Parallel_PAR [(Const (@{const_syntax Cons}, _) \$
(Const (@{const_syntax Pair}, _) \$ (Const (@{const_syntax Some}, _) \$ t1) \$ t2) \$ ts)] =
Syntax.const @{syntax_const "_prgs"} \$ t1 \$ t2 \$ Parallel_PAR [ts]
| Parallel_PAR _ = raise Match;

fun Parallel_tr' ts = Syntax.const @{syntax_const "_PAR"} \$ Parallel_PAR ts;
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_inv"})),
(@{const_syntax AnnBasic}, K annassign_tr'),
(@{const_syntax AnnWhile}, K (annbexp_tr' @{syntax_const "_AnnWhile"})),
(@{const_syntax AnnAwait}, K (annbexp_tr' @{syntax_const "_AnnAwait"})),
(@{const_syntax AnnCond1}, K (annbexp_tr' @{syntax_const "_AnnCond1"})),
(@{const_syntax AnnCond2}, K (annbexp_tr' @{syntax_const "_AnnCond2"}))]
end;
›

end
```