Quelle  OG_Syntax.thy

(*
 * Copyright 2016, Data61, CSIRO
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)
section ‹Shallowly-embedded syntax for COMPLX programs›
theory OG_Syntax
imports
  OG_Hoare
  OG_Tactics
begin

datatype ('s, 'p, 'f) ann_com =
  AnnCom "('s, 'p, 'f) ann" "('s,'p,'f) com"

fun ann where "ann (AnnCom p q) = p"
fun com where "com (AnnCom p q) = q"

lemmas ann.simps[oghoare_simps] com.simps[oghoare_simps]

syntax
  "_quote"     :: "'b ==> ('a ==> 'b)"                (‹(«_¬)› [0] 1000)
  "_antiquote" :: "('a ==> 'b) ==> 'b"                (‹🍋_› [1000] 1000)
  "_Assert"    :: "'a ==> 'a set"                    (‹({_})› [0] 1000)

translations
  "{b}" ⇀ "CONST Collect «b¬"

parse_translation ‹
 let
 fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
 | quote_tr ts = raise TERM ("quote_tr", ts);
 in [(@{syntax_const "_quote"}, K quote_tr)] end
 ›

syntax
  "_fst" :: "'a × 'b ==> 'a"  (‹__,› [60] 61)
  "_snd" :: "'a × 'b ==> 'b"  (‹__.› [60] 61)

parse_translation ‹
 let
 fun fst_tr ((Const (@{const_syntax Pair}, _) $ p $ c)
 :: ts) = p;

 fun snd_tr ((Const (@{const_syntax Pair}, _) $ p $ c)
 :: ts) = c;
 in
 [(@{syntax_const "_fst"}, K fst_tr),
 (@{syntax_const "_snd"}, K snd_tr)]
 end
 ›

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

syntax
  "_Annotation" :: "('s,'p,'f) ann_com ==> ('s, 'p, 'f) ann"  (‹__?› [60] 61)
  "_Command" :: "('s,'p,'f) ann_com ==> ('s,'p,'f) com"  (‹__!› [60] 61)

parse_translation ‹
 let
 fun ann_tr ((Const (@{const_syntax AnnCom}, _) $ p $ c)
 :: ts) = p
 | ann_tr (p :: ts) =
 Const (@{const_syntax ann}, dummyT) $ p
 | ann_tr x = raise TERM ("ann_tr", x);

 fun com_tr ((Const (@{const_syntax AnnCom}, _) $ p $ c)
 :: ts) = c
 | com_tr (c :: ts) =
 Const (@{const_syntax com}, dummyT) $ c
 | com_tr x = raise TERM ("com_tr", x);
 in
 [(@{syntax_const "_Annotation"}, K ann_tr),
 (@{syntax_const "_Command"}, K com_tr)]
 end
 ›

syntax
  "_Seq"  :: "('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                   (‹(_,,/ _)› [55, 56] 55)
  "_AnnSeq"  :: "('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                   (‹(_;;//_)› [55, 56] 55)

translations
  "_Seq c1 c2" ⇀ "CONST AnnCom (CONST AnnComp (c1_?) (c2_?)) (CONST Seq (c1_!) (c2_!))"
  "_AnnSeq c1 c2" ⇀ "CONST AnnCom (CONST AnnComp (c1_?) (c2_?)) (CONST Seq (c1_!) (c2_!))"

syntax
  "_Assign"    :: "idt ==> 'b ==> ('s,'p,'f) ann_com"
                   (‹(🍋_ :=/ _)› [70, 65] 61)
  "_AnnAssign" :: "'s assn ==> idt ==> 'b ==> ('s,'p,'f) ann_com"
                   (‹(_//🍋_ :=/ _)› [90,70,65] 61)

definition "FAKE_ANN ≡ UNIV"

translations
  "r 🍋x := a" ⇀ "CONST AnnCom (CONST AnnExpr r)
                               (CONST Basic «🍋(_update_name x (λ_. a))¬)"
  "🍋x := a" ⇌ "CONST FAKE_ANN 🍋x := a"

abbreviation
  "update_var f S s ≡ (λv. f (λ_. v) s) ` S"

abbreviation
  "fun_to_rel f ≡ ∪ ((λs. (λv. (s, v)) ` f s) ` UNIV)"

syntax
  "_Spec"      :: "idt ==> 'b ==> ('s,'p,'f) ann_com"
                   (‹(🍋_ :∈/ _)› [70, 65] 61)
  "_AnnSpec"   :: "'a assn ==> idt ==> 'b ==> ('s,'p,'f) ann_com"
                   (‹(_//🍋_ :∈/ _)› [90,70,65] 61)

translations
  "r 🍋x :∈ S" ⇀ "CONST AnnCom (CONST AnnExpr r)
                               (CONST Spec (CONST fun_to_rel «🍋(CONST update_var (_update_name x) S)¬))"
  "🍋x :∈ S" ⇌ "CONST FAKE_ANN 🍋x :∈ S"


nonterminal grds and grd

syntax
  "_AnnCond1"    :: "'s assn ==> 's bexp ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹(_//IF _//(2THEN/ (_))//(2ELSE/ (_))//FI)›  [90,0,0,0] 61)
  "_AnnCond2"    :: "'s assn ==> 's bexp ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹(_//IF _//(2THEN/ (_))//FI)›  [90,0,0] 61)
  "_AnnWhile"    :: "'s assn ==> 's bexp ==> 's assn ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com" 
                    (‹(_//WHILE _/ INV _//(2DO/ (_))//OD)›  [90,0,0,0] 61)
  "_AnnAwait"    :: "'s assn ==> 's bexp ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹(_//AWAIT _/ (2THEN/ (_))/ END)›  [90,0,0] 61)
  "_AnnAtom"     :: "'s assn ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹(_//⟨_⟩)› [90,0] 61)
  "_AnnWait"     :: "'s assn ==> 's bexp ==> ('s,'p,'f) ann_com"
                    (‹(_//WAIT _/ END)› [90,0] 61)

  "_Cond"        :: "'s bexp ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com" 
                    (‹(IF _//(2THEN/ (_))//(2ELSE/ (_))//FI)› [0, 0, 0] 61)
  "_Cond2"       :: "'s bexp ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹(IF _//(2THEN/ (_))//FI)› [0,0] 56)
  "_While_inv"   :: "'s bexp ==> 's assn ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹(WHILE _/ INV _//(2DO/ (_))//OD)›  [0, 0, 0] 61)
  "_While"       :: "'s bexp ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹(WHILE _//(2DO/ (_))//OD)›  [0, 0] 61)
  "_Await"       :: "'s bexp ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹(AWAIT _/ (2THEN/ (_))/ END)›  [0,0] 61)
  "_Atom"        :: "('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹(⟨_⟩)› [0] 61)
  "_Wait"        :: "'s bexp ==> ('s,'p,'f) ann_com"
                    (‹(WAIT _/ END)› [0] 61)
  "_grd"         :: "'f ==> 's bexp ==> grd"
                    (‹'(_, _')› [1000] 1000)
  "_last_grd"    :: "grd ==> grds"   (‹_› 1000)
  "_grds"        :: "[grd, grds] ==> grds"
                    (‹(_,/ _)› [999,1000] 1000)
  "_guards"      :: "'s assn ==> grds ==> ('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹(_//(2_ ⟼/ (_)))› [90, 0, 56] 61)
  "_Throw"       :: "('s,'p,'f) ann_com"
                    (‹THROW› 61)
  "_AnnThrow"    :: "'s assn ==> ('s,'p,'f) ann_com"
                    (‹(_/ THROW)› [90] 61)
  "_Try_Catch"   :: "('s,'p,'f) ann_com ==>('s,'p,'f) ann_com ==> ('s,'p,'f) ann_com"
                    (‹((2TRY/ (_))//(2CATCH/ (_))/ END)›  [0,0] 71)
  "_AnnCallX"    :: "'s assn ==> ('s ==> 's) ==> 's assn ==> 'p ==> nat ==> ('s ==> 's ==> 's) ==> ('s==>'s==>('s,'p,'f) com) ==> 's assn ==> 's assn ==> 's assn ==> 's assn ==> ('s,'p,'f) ann_com"
                    (‹(_//(2CALLX/ (_)//_/ _/ _//_/ _//_/ _//_/ _))›
                      [90,1000,0,1000,0,1000,1000,0,0,0,0] 61)
  "_AnnSCall"    :: "'s assn ==> 'p ==> nat ==> ('s,'p,'f) ann_com"
                    (‹(_//SCALL _/ _)› [90,0,0] 61)
  "_Skip"        :: "('s,'p,'f) ann_com"
                    (‹SKIP› 61)
  "_AnnSkip"     :: "'s assn ==> ('s,'p,'f) ann_com"
                    (‹(_/ SKIP)› [90] 61)

translations
  "r IF b THEN c1 ELSE c2 FI" ⇀
    "CONST AnnCom (CONST AnnBin r (c1_?) (c2_?)) (CONST Cond {b} (c1_!) (c2_!))"
  "r IF b THEN c FI" ⇀ "r IF b THEN c ELSE SKIP FI"
  "r WHILE b INV i DO c OD" ⇀
    "CONST AnnCom (CONST AnnWhile r i (c_?)) (CONST While {b} (c_!))"
  "r AWAIT b THEN c END" ⇀
    "CONST AnnCom (CONST AnnRec r (c_?)) (CONST Await {b} (c_!))"
  "r ⟨c⟩" ⇌ "r AWAIT CONST True THEN c END"
  "r WAIT b END" ⇌ "r AWAIT b THEN SKIP END"

  "IF b THEN c1 ELSE c2 FI" ⇌ "CONST FAKE_ANN IF b THEN c1 ELSE c2 FI"
  "IF b THEN c FI" ⇌ "CONST FAKE_ANN IF b THEN c ELSE SKIP FI"
  "WHILE b DO c OD" ⇌ "CONST FAKE_ANN WHILE b INV CONST FAKE_ANN DO c OD"
  "WHILE b INV i DO c OD" ⇌ "CONST FAKE_ANN WHILE b INV i DO c OD"
  "AWAIT b THEN c END" ⇌ "CONST FAKE_ANN AWAIT b THEN c END"
  "⟨c⟩" ⇌ "CONST FAKE_ANN AWAIT CONST True THEN c END"
  "WAIT b END" ⇌ "AWAIT b THEN SKIP END"

  "_grd f g" ⇀ "(f, g)"
  "_grds g gs" ⇀ "g#gs"
  "_last_grd g" ⇀ "[g]"
  "_guards r gs c" ⇀
    "CONST AnnCom (CONST ann_guards r gs (c_?)) (CONST guards gs (c_!))"

  "ai CALLX init r p n restore return arestoreq areturn arestorea A" ⇀
    "CONST AnnCom (CONST ann_call ai r n arestoreq areturn arestorea A)
                  (CONST call init p restore return)"
  "r SCALL p n" ⇀ "CONST AnnCom (CONST AnnCall r n) (CONST Call p)"

  "r THROW" ⇌ "CONST AnnCom (CONST AnnExpr r) (CONST Throw)"
  "THROW" ⇌ "CONST FAKE_ANN THROW"
  "TRY c1 CATCH c2 END" ⇀ "CONST AnnCom (CONST AnnComp (c1_?) (c2_?))
                                         (CONST Catch (c1_!) (c2_!))"

  "r SKIP" ⇌ "CONST AnnCom (CONST AnnExpr r) (CONST Skip)"
  "SKIP" ⇌ "CONST FAKE_ANN SKIP"

nonterminal prgs

syntax
  "_PAR" :: "prgs ==> 'a"              (‹(COBEGIN//_//COEND)› [57] 56)
  "_prg" :: "['a, 'a, 'a] ==> prgs"        (‹(2 _//_,/ _)› [60, 90, 90] 57)
  "_prgs" :: "['a, 'a, 'a, prgs] ==> prgs"  (‹(2 _//_,/ _)//∥//_› [60,90,90,57] 57)

  "_prg_scheme" :: "['a, 'a, 'a, 'a, 'a, 'a] ==> prgs"  
                  (‹ (2SCHEME [_ ≤ _ < _]//_//_,/ _)› [0,0,0,60, 90,90] 57)

translations
  "_prg c q a" ⇀ "([((c_?), q, a)], [(c_!)])"
  "_prgs c q a ps" ⇀ "(((c_?), q, a) # (ps_,), (c_!) # (ps_.))"
  "_PAR ps" ⇀ "CONST AnnCom (CONST AnnPar (ps_,)) (CONST Parallel (ps_.))"

  "_prg_scheme j i k c q a" ⇀ "(CONST map (λi. ((c_?), q, a)) [j..<k], CONST map (λi. (c_!)) [j..<k])"

syntax
  "_oghoare" :: "('s,'p,'f) body ==> ('s,'p,'f) proc_assns ==> 'f set
              ==> ('s,'p,'f) ann_com ==> 's assn ==> 's assn ==> bool"  
    (‹(4_),/ (4_)/ (|⊨_{/_} (_//_, _))› [60,60,60,20,1000,1000]60)

  "_oghoare_seq" :: "('s,'p,'f) body ==> ('s,'p,'f) proc_assns ==> 'f set
              ==>'s assn ==> ('s,'p,'f) ann_com ==> 's assn ==> 's assn ==> bool"  
    (‹(4_),/ (4_)/ (|⊨!!!_{/_} (_//_//_, _))› [60,60,60,1000,20,1000,1000]60)

translations
  "_oghoare Γ Θ F c Q A" ⇀ "Γ, Θ ⊨_F (c_?) (c_!) Q, A"
  "_oghoare_seq Γ Θ F P c Q A" ⇀ "Γ, Θ ⊨!!!_F P (c_?) (c_!) Q, A"

ML ‹val syntax_debug = false›
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 annbexp_tr' name (r :: (Const (@{const_syntax Collect}, _) $ t) :: ts) =
 annquote_tr' (Syntax.const name) (r :: t :: ts)
 | annbexp_tr' name (r :: Const (@{const_syntax UNIV}, _) :: ts) =
 annquote_tr' (Syntax.const name)
 (r :: Abs ("s", dummyT, Const (@{const_syntax True}, dummyT)) :: ts)
 | annbexp_tr' name (r :: Const (@{const_syntax Set.empty}, _) :: ts) =
 annquote_tr' (Syntax.const name)
 (r :: Abs ("s", dummyT, Const (@{const_syntax False}, dummyT)) :: ts)
 | annbexp_tr' name x =
 let val _ = if syntax_debug then writeln ("annbexp_tr'\n " ^ @{make_string} x) else () in
 raise Match end;

 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' r = let val _ = writeln ("annassign_tr'\n " ^ @{make_string} r) in
 raise Match end;

 fun dest_list (Const (@{const_syntax Nil}, _)) = []
 | dest_list (Const (@{const_syntax Cons}, _) $ x $ xs) = x :: dest_list xs
 | dest_list _ = raise Match;

 fun guards_lst_tr' [fg] = fg
 | guards_lst_tr' (t :: ts) =
 Syntax.const @{syntax_const "_grds"} $ t $ guards_lst_tr' ts
 | guards_lst_tr' [] = raise Match;

 fun new_AnnCom r c =
 (Const (@{const_syntax AnnCom}, dummyT) $ r $ c)

 fun new_Pair a b =
 (Const (@{const_syntax Pair}, dummyT) $ a $ b)

 fun dest_prod (Const (@{const_syntax Pair}, _) $ a $ b) = (a, b)
 | dest_prod _ = raise Match;

 fun prgs_tr' f pqa c =
 let val (p, qa) = dest_prod pqa
 val (q, a) = dest_prod qa
 in [new_AnnCom (f p) (f c), f q, f a] end

 fun prgs_lst_tr' [p] [c] =
 list_comb (Syntax.const @{syntax_const "_prg"},
 prgs_tr' I p c)
 | prgs_lst_tr' (p :: ps) (c :: cs) =
 list_comb (Syntax.const @{syntax_const "_prgs"},
 prgs_tr' I p c) $ prgs_lst_tr' ps cs
 | prgs_lst_tr' _ _= raise Match;

 fun AnnCom_tr (Const (@{const_syntax AnnPar}, _) $
 (Const (@{const_syntax map}, _) $
 Abs (i, T, p) $ (Const _ $ j $ k)) ::
 Const (@{const_syntax Parallel}, _) $
 (Const (@{const_syntax map}, _) $
 Abs (_, _, c) $ _) :: ts) =
 let val _ = if syntax_debug then writeln "prg_scheme" else ()
 fun dest_abs body = snd (Term.dest_abs_global (Abs (i, T, body))) in
 Syntax.const @{syntax_const "_PAR"} $
 list_comb (Syntax.const @{syntax_const "_prg_scheme"} $
 j $ Free (i, T) $ k, prgs_tr' dest_abs p c)
 end
 | AnnCom_tr (Const (@{const_syntax AnnPar}, _) $ ps ::
 Const (@{const_syntax Parallel}, _) $ cs :: ts) =
 let val _ = if syntax_debug then writeln "Par" else ()
 val (ps', cs') = (dest_list ps, dest_list cs)
 in Syntax.const @{syntax_const "_PAR"} $
 prgs_lst_tr' ps' cs' end
 | AnnCom_tr (Const (@{const_syntax AnnExpr}, _) $ r ::
 Const (@{const_syntax Basic}, _) $ Abs (x, _, f $ k $ Bound 0) :: ts) =
 let val _ = if syntax_debug then writeln "Basic'" else () in
 quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f)
 (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) end
 | AnnCom_tr (Const (@{const_syntax AnnExpr}, _) $ r ::
 Const (@{const_syntax Basic}, _) $ (f $ k) :: ts) =
 let val _ = if syntax_debug then writeln "Basic" else () in
 quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f)
 (k :: ts) end
 | AnnCom_tr (Const (@{const_syntax AnnExpr}, _) $ r ::
 Const (@{const_syntax Spec}, _) $ (_ $ _ $ Abs (_,_, _ $ _ $ ((_ $ f) $ S $ _))) :: ts) =
 let val _ = if syntax_debug then writeln ("Spec") else () in
 (Syntax.const @{syntax_const "_AnnSpec"} $ r $
 Syntax_Trans.update_name_tr' f $
 Syntax_Trans.antiquote_tr' @{syntax_const "_antiquote"} S)
 end
 | AnnCom_tr (Const (@{const_syntax AnnComp}, _) $ r $ r' ::
 Const (@{const_syntax Seq}, _) $ c $ c' :: ts) =
 let val _ = if syntax_debug then writeln "Seq" else ()
 in Syntax.const @{syntax_const "_AnnSeq"} $
 new_AnnCom r c $ new_AnnCom r' c' end
 | AnnCom_tr (Const (@{const_syntax AnnRec}, _) $ r $ p ::
 Const (@{const_syntax Await}, _) $ b $ c :: ts) =
 let val _ = if syntax_debug then writeln "Await" else ()
 in annbexp_tr' @{syntax_const "_AnnAwait"}
 (r :: b :: new_AnnCom p c :: ts) end
 | AnnCom_tr (Const (@{const_syntax AnnWhile}, _) $ r $ i $ p ::
 Const (@{const_syntax While}, _) $ b $ c :: ts) =
 let val _ = if syntax_debug then writeln "While" else ()
 in annbexp_tr' @{syntax_const "_AnnWhile"}
 (r :: b :: i :: new_AnnCom p c :: ts) end
 | AnnCom_tr (Const (@{const_syntax AnnBin}, _) $ r $ p $ p' ::
 Const (@{const_syntax Cond}, _) $ b $ c $ c':: ts) =
 let val _ = if syntax_debug then writeln "Cond" else ()
 in annbexp_tr' @{syntax_const "_AnnCond1"}
 (r :: b :: new_AnnCom p c :: new_AnnCom p' c' :: ts) end
 | AnnCom_tr (Const (@{const_syntax ann_guards}, _) $ r $ gs $ p ::
 Const (@{const_syntax guards}, _) $ _ $ c :: ts) =
 let val _ = if syntax_debug then writeln "guards" else ()
 in Syntax.const @{syntax_const "_guards"} $ r $
 guards_lst_tr' (dest_list gs) $ new_AnnCom p c end
 | AnnCom_tr (Const (@{const_syntax AnnRec}, _) $ r $ p ::
 Const (@{const_syntax Guard}, _) $ f $ g $ c :: ts) =
 let val _ = if syntax_debug then writeln "guards'" else ()
 in Syntax.const @{syntax_const "_guards"} $ r $
 new_Pair f g $ new_AnnCom p c end
 | AnnCom_tr (Const (@{const_syntax AnnCall}, _) $ r $ n ::
 Const (@{const_syntax Call}, _) $ p :: ts) =
 let val _ = if syntax_debug then writeln "SCall" else ()
 in Syntax.const @{syntax_const "_AnnSCall"} $ r $ p $ n end
 | AnnCom_tr (Const (@{const_syntax ann_call}, _) $
 ai $ r $ n $ arestoreq $ areturn $ arestorea $ A ::
 Const (@{const_syntax call}, _) $
 init $ p $ restore $ return :: ts) =
 let val _ = if syntax_debug then writeln "CallX" else ()
 in Syntax.const @{syntax_const "_AnnCallX"} $ ai $ init $
 r $ p $ n $ restore $ return $ arestoreq $ areturn $
 arestorea $ A end
 | AnnCom_tr (Const (@{const_syntax AnnComp}, _) $ r $ r' ::
 Const (@{const_syntax Catch}, _) $ c $ c' :: ts) =
 let val _ = if syntax_debug then writeln "Catch" else ()
 in Syntax.const @{syntax_const "_Try_Catch"} $
 new_AnnCom r c $ new_AnnCom r' c' end
 | AnnCom_tr (Const (@{const_syntax ann}, _) $ p ::
 Const (@{const_syntax com}, _) $ p' :: ts) =
 let val _ = if syntax_debug then writeln "ann_com" else ()
 in if p = p' then p else raise Match end
 | AnnCom_tr x = let val _ = if syntax_debug then writeln ("AnnCom_tr\n " ^ @{make_string} x) else ()
 in raise Match end;

 fun oghoare_tr (gamma :: sigma :: F :: r :: c :: Q :: A :: ts) =
 let val _ = if syntax_debug then writeln "oghoare" else ()
 in Syntax.const @{syntax_const "_oghoare"} $
 gamma $ sigma $ F $ new_AnnCom r c $ Q $ A
 end
 | oghoare_tr x = let val _ = writeln ("oghoare_tr\n " ^ @{make_string} x)
 in raise Match end;

 fun oghoare_seq_tr (gamma :: sigma :: F :: P :: r :: c :: Q :: A :: ts) =
 let val _ = if syntax_debug then writeln "oghoare_seq" else ()
 in Syntax.const @{syntax_const "_oghoare_seq"} $
 gamma $ sigma $ F $ P $ new_AnnCom r c $ Q $ A
 end
 | oghoare_seq_tr x = let val _ = writeln ("oghoare_seq_tr\n " ^ @{make_string} x)
 in raise Match end;

 in
 [(@{const_syntax Collect}, K assert_tr'),
 (@{const_syntax AnnCom}, K AnnCom_tr),
 (@{const_syntax oghoare}, K oghoare_tr),
 (@{const_syntax oghoare_seq}, K oghoare_seq_tr)]

 end
 ›

end