Theory OCL_Syntax

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
chapter ‹Abstract Syntax›
theory OCL_Syntax
  imports Complex_Main Object_Model OCL_Types
begin

section ‹Preliminaries›

type_synonym vname = "String.literal"
type_synonym 'a env = "vname ⇀f 'a"

text ‹
  In OCL @{text "1 + ∞ = ⊥"}. So we do not use @{typ enat} and
  define the new data type.›

typedef unat = "UNIV :: nat option set" ..

definition "unat x ≡ Abs_unat (Some x)"

instantiation unat :: infinity
begin
definition "∞ ≡ Abs_unat None"
instance ..
end

free_constructors cases_unat for
  unat
| "∞ :: unat"
  unfolding unat_def infinity_unat_def
  apply (metis Rep_unat_inverse option.collapse)
  apply (metis Abs_unat_inverse UNIV_I option.sel)
  by (simp add: Abs_unat_inject)

section ‹Standard Library Operations›

datatype metaop = AllInstancesOp

datatype typeop = OclAsTypeOp | OclIsTypeOfOp | OclIsKindOfOp
| SelectByKindOp | SelectByTypeOp

datatype super_binop = EqualOp | NotEqualOp

datatype any_unop = OclAsSetOp | OclIsNewOp
| OclIsUndefinedOp | OclIsInvalidOp | OclLocaleOp | ToStringOp

datatype boolean_unop = NotOp
datatype boolean_binop = AndOp | OrOp | XorOp | ImpliesOp

datatype numeric_unop = UMinusOp | AbsOp | FloorOp | RoundOp | ToIntegerOp
datatype numeric_binop = PlusOp | MinusOp | MultOp | DivideOp
| DivOp | ModOp | MaxOp | MinOp
| LessOp | LessEqOp | GreaterOp | GreaterEqOp

datatype string_unop = SizeOp | ToUpperCaseOp | ToLowerCaseOp | CharactersOp
| ToBooleanOp | ToIntegerOp | ToRealOp
datatype string_binop = ConcatOp | IndexOfOp | EqualsIgnoreCaseOp | AtOp
| LessOp | LessEqOp | GreaterOp | GreaterEqOp
datatype string_ternop = SubstringOp

datatype collection_unop = CollectionSizeOp | IsEmptyOp | NotEmptyOp
| CollectionMaxOp | CollectionMinOp | SumOp
| AsSetOp | AsOrderedSetOp | AsSequenceOp | AsBagOp | FlattenOp
| FirstOp | LastOp | ReverseOp
datatype collection_binop = IncludesOp | ExcludesOp
| CountOp| IncludesAllOp | ExcludesAllOp | ProductOp
| UnionOp | IntersectionOp | SetMinusOp | SymmetricDifferenceOp
| IncludingOp | ExcludingOp
| AppendOp | PrependOp | CollectionAtOp | CollectionIndexOfOp
datatype collection_ternop = InsertAtOp | SubOrderedSetOp | SubSequenceOp

type_synonym unop = "any_unop + boolean_unop + numeric_unop + string_unop + collection_unop"

declare [[coercion "Inl :: any_unop ⇒ unop"]]
declare [[coercion "Inr ∘ Inl :: boolean_unop ⇒ unop"]]
declare [[coercion "Inr ∘ Inr ∘ Inl :: numeric_unop ⇒ unop"]]
declare [[coercion "Inr ∘ Inr ∘ Inr ∘ Inl :: string_unop ⇒ unop"]]
declare [[coercion "Inr ∘ Inr ∘ Inr ∘ Inr :: collection_unop ⇒ unop"]]

type_synonym binop = "super_binop + boolean_binop + numeric_binop + string_binop + collection_binop"

declare [[coercion "Inl :: super_binop ⇒ binop"]]
declare [[coercion "Inr ∘ Inl :: boolean_binop ⇒ binop"]]
declare [[coercion "Inr ∘ Inr ∘ Inl :: numeric_binop ⇒ binop"]]
declare [[coercion "Inr ∘ Inr ∘ Inr ∘ Inl :: string_binop ⇒ binop"]]
declare [[coercion "Inr ∘ Inr ∘ Inr ∘ Inr :: collection_binop ⇒ binop"]]

type_synonym ternop = "string_ternop + collection_ternop"

declare [[coercion "Inl :: string_ternop ⇒ ternop"]]
declare [[coercion "Inr :: collection_ternop ⇒ ternop"]]

type_synonym op = "unop + binop + ternop + oper"

declare [[coercion "Inl ∘ Inl :: any_unop ⇒ op"]]
declare [[coercion "Inl ∘ Inr ∘ Inl :: boolean_unop ⇒ op"]]
declare [[coercion "Inl ∘ Inr ∘ Inr ∘ Inl :: numeric_unop ⇒ op"]]
declare [[coercion "Inl ∘ Inr ∘ Inr ∘ Inr ∘ Inl :: string_unop ⇒ op"]]
declare [[coercion "Inl ∘ Inr ∘ Inr ∘ Inr ∘ Inr :: collection_unop ⇒ op"]]

declare [[coercion "Inr ∘ Inl ∘ Inl :: super_binop ⇒ op"]]
declare [[coercion "Inr ∘ Inl ∘ Inr ∘ Inl :: boolean_binop ⇒ op"]]
declare [[coercion "Inr ∘ Inl ∘ Inr ∘ Inr ∘ Inl :: numeric_binop ⇒ op"]]
declare [[coercion "Inr ∘ Inl ∘ Inr ∘ Inr ∘ Inr ∘ Inl :: string_binop ⇒ op"]]
declare [[coercion "Inr ∘ Inl ∘ Inr ∘ Inr ∘ Inr ∘ Inr :: collection_binop ⇒ op"]]

declare [[coercion "Inr ∘ Inr ∘ Inl ∘ Inl :: string_ternop ⇒ op"]]
declare [[coercion "Inr ∘ Inr ∘ Inl ∘ Inr :: collection_ternop ⇒ op"]]

declare [[coercion "Inr ∘ Inr ∘ Inr :: oper ⇒ op"]]

datatype iterator = AnyIter | ClosureIter | CollectIter | CollectNestedIter
| ExistsIter | ForAllIter | OneIter | IsUniqueIter
| SelectIter | RejectIter | SortedByIter

section ‹Expressions›

datatype collection_literal_kind =
  CollectionKind | SetKind | OrderedSetKind | BagKind | SequenceKind

text ‹
  A call kind could be defined as two boolean values (@{text "is_arrow_call"},
  @{text "is_safe_call"}). Also we could derive @{text "is_arrow_call"}
  value automatically based on an operation kind.
  However, it is much easier and more natural to use the following enumeration.›

datatype call_kind = DotCall | ArrowCall | SafeDotCall | SafeArrowCall

text ‹
  We do not define a @{text Classifier} type (a type of all types),
  because it will add unnecessary complications to the theory.
  So we have to define type operations as a pure syntactic constructs.
  We do not define @{text Type} expressions either.

  We do not define @{text InvalidLiteral}, because it allows us to
  exclude @{text OclInvalid} type from typing rules. It simplifies
  the types system.

  Please take a note that for @{text AssociationEnd} and
  @{text AssociationClass} call expressions one can specify an
  optional role of a source class (@{text from_role}).
  It differs from the OCL specification, which allows one to specify
  a role of a destination class. However, the latter one does not
  allow one to determine uniquely a set of linked objects, for example,
  in a ternary self relation.›