Theory Expressions_Tests

section ‹ Expression Test Cases and Examples ›

theory Expressions_Tests
  imports Expressions Named_Expressions
begin

text ‹ Some examples of lifted expressions follow. For now, we turn off the pretty printer so that 
  we can see the results of the parser.›

declare [[pretty_print_exprs=false]]

term "(f + g)e" ― ‹ Lift an expression and insert @{const SEXP} for pretty printing ›
term "(f + g)e" ― ‹ Lift an expression and don't insert @{const SEXP} ›

text ‹ The default behaviour of our parser is to recognise identifiers as expression variables.
  So, the above expression becomes the term @{term "[λ𝗌. f 𝗌 + g 𝗌]e"}. We can easily change
  this using the attribute @{attribute literal_variables}: ›

declare [[literal_variables]]

term "(f + g)e"

text ‹ Now, @{term f} and @{term g} are both parsed as literals, and so the term is 
  @{term "[λ𝗌. f + g]e"}. Alternatively, we could have a lens in the expression, by marking
  a free variable with a dollar : ›

term "($x + g)e"

text ‹ This gives the term @{term "[λ𝗌. get⇘x⇙ 𝗌 + g]e"}. Although we have default behaviours
  for parsing, we can use different markup to coerce identifiers to particular variable kinds. ›

term "($x + @g)e"

text ‹ This gives @{term "[λ𝗌. get⇘x⇙ 𝗌 + g 𝗌]e"}, the we have requested that @{term "g"} is 
  treated as an expression variable. We can do similar with literal, as show below. ›

term "(f + «x»)e"

text ‹ Some further examples follow. ›

term "(«f» (@e))e"

term "(@f + @g)e"

term "(@x)e"

term "($x:y:z)e"

term "(($x:y):z)e"

term "(x::nat)e"

term "(∀ x::nat. x > 2)e"

term "SEXP(λ 𝗌. get⇘x⇙ 𝗌 + e 𝗌 + v)"

term "(v ∈ $xs ∪ ($f) ys ∪ {} ∧ @e)e"

text ‹ We now turn pretty printing back on, so we can see how the user sees expressions. ›

declare [[pretty_print_exprs, literal_variables=false]]

term "($x< = $x>)e"

term "($x.1 = $y.2)e"

text ‹ The pretty printer works even when we don't use the parser, as shown below. ›

term "[λ 𝗌. get⇘x⇙ 𝗌 + e 𝗌 + v]e"

text ‹ By default, dollars are printed next to free variables that are lenses. However, we can
  alter this behaviour with the attribute @{attribute mark_state_variables}: ›

declare [[mark_state_variables=false]]

term "($x + e + v)e"

text ‹ This way, the @{term "x"} variable is indistinguishable when printed from the @{term "e"}
  and @{term "v"}. Usually, this information can be inferred from the types of the entities: ›

alphabet st = 
  x :: int

term "(x + e + v)e"

expression x_is_big over st is "x > 1000"

term "(x_is_big ⟶ x > 0)e"

text ‹ Here, @{term x} is a lens defined by the @{command alphabet} command, and so the lifting
  translation treats it as a state variable. This is hidden from the user. ›

dataspace testspace =
   variables z :: int

declare [[literal_variables]]

context testspace
begin

edefinition "z_is_bigger y = (z > y)"

term "(z_is_bigger (z + 1))e"

end

end