Theory Syntax

(*  Title:       CoreC++
    ID:          $Id: Syntax.thy,v 1.7 2008-06-23 21:24:36 makarius Exp $
    Author:      Tobias Nipkow, Daniel Wasserrab 
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

    Extracted from the Jinja theory J/Expr.thy by Tobias Nipkow
*)


header {* \isaheader{Syntax} *}

theory Syntax imports Exceptions begin


text{*Syntactic sugar*}

abbreviation (input)
  InitBlock :: "vname => ty => expr => expr => expr"   ("(1'{_:_ := _;/ _})") where
  "InitBlock V T e1 e2 == {V:T; V := e1;; e2}"

abbreviation unit where "unit == Val Unit"
abbreviation null where "null == Val Null"
abbreviation "ref r == Val(Ref r)"
abbreviation "true == Val(Bool True)"
abbreviation "false == Val(Bool False)"

abbreviation
  Throw :: "reference => expr" where
  "Throw r == throw(ref r)"

abbreviation (input)
  THROW :: "cname => expr" where
  "THROW xc == Throw(addr_of_sys_xcpt xc,[xc])"

end