# Theory OCL_Syntax

```(*  Title:       Safe OCL
Author:      Denis Nikiforov, March 2019
Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
*)
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)

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.›

```