Theory AutoCorres2.PrettyProgs

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section "Prettier Printing for Programs"

theory PrettyProgs
imports "Simpl.Vcg"
begin

syntax (output)
  "_Assign"      :: "'b => 'b => ('a,'p,'f) com"    ("(2_ :==/ _)" [30, 30] 23)

  "_seq"::"('s,'p,'f) com ⇒ ('s,'p,'f) com ⇒ ('s,'p,'f) com" ("_;;//_" [20, 21] 20)

  "_While_inv"   :: "'a bexp => 'a assn => bdy => ('a,'p,'f) com"
        ("(0WHILE (_)//INV (_)//_)"  [25, 0, 81] 71)

  "_Do" :: "('a,'p,'f) com ⇒ bdy" ("DO//  (_)//OD" [0] 1000)

  "_Cond"        :: "'a bexp => ('a,'p,'f) com => ('a,'p,'f) com => ('a,'p,'f) com"
        ("(0IF _ THEN//  (_)//ELSE//  (_)//FI)" [0, 0, 0] 71)
  "_Cond_no_else":: "'a bexp => ('a,'p,'f) com => ('a,'p,'f) com"
        ("(0IF _ THEN//  (_)//FI)" [0, 0] 71)

  "_Try_Catch":: "('a,'p,'f) com ⇒('a,'p,'f) com ⇒ ('a,'p,'f) com"
        ("(0TRY//  (_)//CATCH _//END)"  [0,0] 71)

end