Theory utp_easy_parser

section ‹ UTP Easy Expression Parser ›

theory utp_easy_parser
  imports utp_full
begin

subsection ‹ Replacing the Expression Grammar ›

text ‹ The following theory provides an easy to use expression parser that is primarily targetted
  towards expressing programs. Unlike the built-in UTP expression syntax, this uses a closed grammar
  separate to the HOL \emph{logic} nonterminal, that gives more freedom in what can be expressed.
  In particular, identifiers are interpreted as UTP variables rather than HOL variables and functions
  do not require subscripts and other strange decorations. 

  The first step is to remove the from the UTP parse the following grammar rule that uses arbitrary
  HOL logic to represent expressions. Instead, we will populate the \emph{uexp} grammar manually.
›

purge_syntax
  "_uexp_l"  :: "logic ⇒ uexp" (‹_› [64] 64)

subsection ‹ Expression Operators ›

syntax
  "_ue_quote" :: "uexp ⇒ logic" (‹'(_')⇩e›)
  "_ue_tuple" :: "uexprs ⇒ uexp" (‹'(_')›)
  "_ue_lit"   :: "logic ⇒ uexp" (‹«_»›)
  "_ue_var"   :: "svid ⇒ uexp" (‹_›)
  "_ue_eq"    :: "uexp ⇒ uexp ⇒ uexp" (infix ‹=› 150)
  "_ue_uop"   :: "id   ⇒ uexp ⇒ uexp" (‹_'(_')› [999,0] 999)
  "_ue_bop"   :: "id   ⇒ uexp ⇒ uexp ⇒ uexp" (‹_'(_, _')› [999,0,0] 999)
  "_ue_trop"  :: "id   ⇒ uexp ⇒ uexp ⇒ uexp ⇒ uexp" (‹_'(_, _, _')› [999,0,0,0] 999)
  "_ue_apply" :: "uexp ⇒ uexp ⇒ uexp" (‹_[_]› [999] 999)

translations
  "_ue_quote e" => "e"
  "_ue_tuple (_uexprs x (_uexprs y z))" => "_ue_tuple (_uexprs x (_ue_tuple (_uexprs y z)))"
  "_ue_tuple (_uexprs x y)" => "CONST bop CONST Pair x y"
  "_ue_tuple x" => "x"
  "_ue_lit x"    => "CONST lit x"
  "_ue_var x"    => "CONST utp_expr.var (CONST pr_var x)"
  "_ue_eq x y"   => "x =⇩u y"
  "_ue_uop f x"   => "CONST uop f x"
  "_ue_bop f x y" => "CONST bop f x y"
  "_ue_trop f x y" => "CONST trop f x y"
  "_ue_apply f x" => "f(x)⇩a"

subsection ‹ Predicate Operators ›

syntax
  "_ue_true"  :: "uexp" (‹true›)
  "_ue_false" :: "uexp" (‹false›)
  "_ue_not"   :: "uexp ⇒ uexp" (‹¬ _› [40] 40)
  "_ue_conj"  :: "uexp ⇒ uexp ⇒ uexp" (infixr ‹∧› 135)
  "_ue_disj"  :: "uexp ⇒ uexp ⇒ uexp" (infixr ‹∨› 130)
  "_ue_impl"  :: "uexp ⇒ uexp ⇒ uexp" (infixr ‹⇒› 125)
  "_ue_iff"   :: "uexp ⇒ uexp ⇒ uexp" (infixr ‹⇒› 125)
  "_ue_mem"   :: "uexp ⇒ uexp ⇒ uexp" (‹(_/ ∈ _)› [151, 151] 150)
  "_ue_nmem"  :: "uexp ⇒ uexp ⇒ uexp" (‹(_/ ∉ _)› [151, 151] 150)

translations
  "_ue_true" => "CONST true_upred"
  "_ue_false" => "CONST false_upred"
  "_ue_not p" => "CONST not_upred p"
  "_ue_conj p q" => "p ∧⇩p q"
  "_ue_disj p q" => "p ∨⇩p q"
  "_ue_impl p q" => "p ⇒ q"
  "_ue_iff p q"  => "p ⇔ q"
  "_ue_mem x A"  => "x ∈⇩u A"
  "_ue_nmem x A" => "x ∉⇩u A"

subsection ‹ Arithmetic Operators ›

syntax
  "_ue_num"    :: "num_const ⇒ uexp" (‹_›)
  "_ue_size"   :: "uexp ⇒ uexp" (‹#_› [999] 999)
  "_ue_eq"     :: "uexp ⇒ uexp ⇒ uexp" (infix ‹=› 150)
  "_ue_le"     :: "uexp ⇒ uexp ⇒ uexp" (infix ‹≤› 150)
  "_ue_lt"     :: "uexp ⇒ uexp ⇒ uexp" (infix ‹<› 150)
  "_ue_ge"     :: "uexp ⇒ uexp ⇒ uexp" (infix ‹≥› 150)
  "_ue_gt"     :: "uexp ⇒ uexp ⇒ uexp" (infix ‹>› 150)
  "_ue_zero"   :: "uexp" (‹0›)
  "_ue_one"    :: "uexp" (‹1›)
  "_ue_plus"   :: "uexp ⇒ uexp ⇒ uexp" (infixl ‹+› 165)
  "_ue_uminus" :: "uexp ⇒ uexp" (‹- _› [181] 180)
  "_ue_minus"  :: "uexp ⇒ uexp ⇒ uexp" (infixl ‹-› 165)
  "_ue_times"  :: "uexp ⇒ uexp ⇒ uexp" (infixl ‹*› 170)
  "_ue_div"    :: "uexp ⇒ uexp ⇒ uexp" (infixl ‹div› 170)

translations
  "_ue_num x"    => "_Numeral x"
  "_ue_size e"   => "#⇩u(e)"
  "_ue_le x y"   => "x ≤⇩u y"
  "_ue_lt x y"   => "x <⇩u y"
  "_ue_ge x y"   => "x ≥⇩u y"
  "_ue_gt x y"   => "x >⇩u y"
  "_ue_zero"     => "0" 
  "_ue_one"      => "1"
  "_ue_plus x y" => "x + y"
  "_ue_uminus x" => "- x"
  "_ue_minus x y" => "x - y"
  "_ue_times x y" => "x * y"
  "_ue_div x y"   => "CONST divide x y"

subsection ‹ Sets ›

syntax
  "_ue_empset"          :: "uexp" (‹{}›)
  "_ue_setprod"         :: "uexp ⇒ uexp ⇒ uexp" (infixr ‹×› 80)
  "_ue_atLeastAtMost"   :: "uexp ⇒ uexp ⇒ uexp" (‹(1{_.._})›)
  "_ue_atLeastLessThan" :: "uexp ⇒ uexp ⇒ uexp" (‹(1{_..<_})›)

translations
  "_ue_empset" => "{}⇩u"
  "_ue_setprod e f" =>  "CONST bop (CONST Product_Type.Times) e f"
  "_ue_atLeastAtMost m n" => "{m..n}⇩u"
  "_ue_atLeastLessThan m n" => "{m..<n}⇩u"

subsection ‹ Imperative Program Syntax ›

syntax
  "_ue_if_then"    :: "uexp ⇒ logic ⇒ logic ⇒ logic" (‹if _ then _ else _ fi›)
  "_ue_hoare"      :: "uexp ⇒ logic ⇒ uexp ⇒ logic" (‹{{_}} / _ / {{_}}›)
  "_ue_wp"         :: "logic ⇒ uexp ⇒ uexp" (infix ‹wp› 60)

translations
  "_ue_if_then b P Q" => "P ◃ b ▹⇩r Q"
  "_ue_hoare b P c" => "⦃b⦄P⦃c⦄⇩u"
  "_ue_wp P b" => "P wp b"

end