Theory VIMP_Syntax

theory VIMP_Syntax
  imports Main "HOL-Library.Countable" "Deriving.Compare_Order_Instances"
begin

section ‹Source-language expressions›

text ‹
  One integer-valued expression language, as in C: comparisons and logical
  operators are ordinary constructors evaluating to ‹0›/‹1›, and source
  ‹true›/‹false› lower to ‹N 1›/‹N 0› in the grammar.
›

type_synonym vname = String.literal
type_synonym store = "vname ⇒ int"

datatype exp =
    N (exp_lit: int)
  | V (exp_var: vname)
  | Plus  (exp_lhs: exp) (exp_rhs: exp)
  | Minus (exp_lhs: exp) (exp_rhs: exp)
  | Times (exp_lhs: exp) (exp_rhs: exp)
  | Div (exp_lhs: exp) (exp_rhs: exp)
  | Mod (exp_lhs: exp) (exp_rhs: exp)
  | Less (cmp_lhs: exp) (cmp_rhs: exp)
  | LessEq (cmp_lhs: exp) (cmp_rhs: exp)
  | Greater (cmp_lhs: exp) (cmp_rhs: exp)
  | GreaterEq (cmp_lhs: exp) (cmp_rhs: exp)
  | NotEq (cmp_lhs: exp) (cmp_rhs: exp)
  | Eq (cmp_lhs: exp) (cmp_rhs: exp)
  | Not (exp_arg: exp)
  | And (exp_lhs: exp) (exp_rhs: exp)
  | Or (exp_lhs: exp) (exp_rhs: exp)

instance exp :: countable
  by countable_datatype

text ‹The executable linear order gives @{const sorted_list_of_set} a
  deterministic representation of CFG edge sets; @{class compare_order} on
  typ‹String.literal› makes it a usable leaf for the derivation.›
derive (linorder) compare_order String.literal
derive linorder exp

end