# Theory OCL_Normalization

(*  Title:       Safe OCL
Author:      Denis Nikiforov, March 2019
Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
*)
chapter ‹Normalization›
theory OCL_Normalization
imports OCL_Typing
begin

(*** Normalization Rules ****************************************************)

section ‹Normalization Rules›

text ‹
The following expression normalization rules includes two kinds of an
abstract syntax tree transformations:
\begin{itemize}
\item determination of implicit types of variables, iterators, and
tuple elements,
described in \autoref{tab:norm_rules}.
\end{itemize}

The following variables are used in the table:
\begin{itemize}
\item ▩‹x› is a non-nullable value,
\item ▩‹n› is a nullable value,
\item ▩‹xs› is a collection of non-nullable values,
\item ▩‹ns› is a collection of nullable values.
\end{itemize}

\begin{table}[h!]
\begin{center}
\caption{Expression Normalization Rules}
\label{tab:norm_rules}
\begin{threeparttable}
\begin{tabular}{c|c}
\textbf{Orig. expr.} & \textbf{Normalized expression}\\
\hline
▩‹x.op()› & ▩‹x.op()›\\
▩‹n.op()› & ▩‹n.op()›\tnote{*}\\
▩‹x?.op()› & ---\\
▩‹n?.op()› & ▩‹if n <> null then n.oclAsType(T[1]).op() else null endif›\tnote{**}\\
▩‹x->op()› & ▩‹x.oclAsSet()->op()›\\
▩‹n->op()› & ▩‹n.oclAsSet()->op()›\\
▩‹x?->op()› & ---\\
▩‹n?->op()› & ---\\
\hline
▩‹xs.op()› & ▩‹xs->collect(x | x.op())›\\
▩‹ns.op()› & ▩‹ns->collect(n | n.op())›\tnote{*}\\
▩‹xs?.op()› & ---\\
▩‹ns?.op()› & ▩‹ns->selectByKind(T[1])->collect(x | x.op())›\\
▩‹xs->op()› & ▩‹xs->op()›\\
▩‹ns->op()› & ▩‹ns->op()›\\
▩‹xs?->op()› & ---\\
▩‹ns?->op()› & ▩‹ns->selectByKind(T[1])->op()›\\
\end{tabular}
\begin{tablenotes}
\item[*] The resulting expression will be ill-typed if the operation is unsafe.
An unsafe operation is an operation which is well-typed for
a non-nullable source only.
\item[**] It would be a good idea to prohibit such a transformation
for safe operations. A safe operation is an operation which is well-typed
for a nullable source. However, it is hard to define safe operations
operation parameters types (please see the typing rules for the equality
operator), and user-defined operations.
\end{tablenotes}
\end{threeparttable}
\end{center}
\end{table}

Please take a note that name resolution of variables, types,
attributes, and associations is out of scope of this section.
It should be done on a previous phase during transformation
of a concrete syntax tree to an abstract syntax tree.›

fun string_of_nat :: "nat ⇒ string" where
"string_of_nat n = (if n < 10 then [char_of (48 + n)]
else string_of_nat (n div 10) @ [char_of (48 + (n mod 10))])"

definition "new_vname ≡ String.implode ∘ string_of_nat ∘ fcard ∘ fmdom"

inductive normalize
:: "('a :: ocl_object_model) type env ⇒ 'a expr ⇒ 'a expr ⇒ bool"
("_ ⊢ _ ⇛/ _" [51,51,51] 50) and
normalize_call ("_ ⊢⇩C _ ⇛/ _" [51,51,51] 50) and
normalize_expr_list ("_ ⊢⇩L _ ⇛/ _" [51,51,51] 50)
where
LiteralN:
"Γ ⊢ Literal a ⇛ Literal a"
|ExplicitlyTypedLetN:
"Γ ⊢ init⇩1 ⇛ init⇩2 ⟹
Γ(v ↦⇩f τ) ⊢ body⇩1 ⇛ body⇩2 ⟹
Γ ⊢ Let v (Some τ) init⇩1 body⇩1 ⇛ Let v (Some τ) init⇩2 body⇩2"
|ImplicitlyTypedLetN:
"Γ ⊢ init⇩1 ⇛ init⇩2 ⟹
Γ ⊢⇩E init⇩2 : τ ⟹
Γ(v ↦⇩f τ) ⊢ body⇩1 ⇛ body⇩2 ⟹
Γ ⊢ Let v None init⇩1 body⇩1 ⇛ Let v (Some τ) init⇩2 body⇩2"
|VarN:
"Γ ⊢ Var v ⇛ Var v"
|IfN:
"Γ ⊢ a⇩1 ⇛ a⇩2 ⟹
Γ ⊢ b⇩1 ⇛ b⇩2 ⟹
Γ ⊢ c⇩1 ⇛ c⇩2 ⟹
Γ ⊢ If a⇩1 b⇩1 c⇩1 ⇛ If a⇩2 b⇩2 c⇩2"

|MetaOperationCallN:
"Γ ⊢ MetaOperationCall τ op ⇛ MetaOperationCall τ op"
|StaticOperationCallN:
"Γ ⊢⇩L params⇩1 ⇛ params⇩2 ⟹
Γ ⊢ StaticOperationCall τ op params⇩1 ⇛ StaticOperationCall τ op params⇩2"

|OclAnyDotCallN:
"Γ ⊢ src⇩1 ⇛ src⇩2 ⟹
Γ ⊢⇩E src⇩2 : τ ⟹
τ ≤ OclAny[?] ∨ τ ≤ Tuple fmempty ⟹
(Γ, τ) ⊢⇩C call⇩1 ⇛ call⇩2 ⟹
Γ ⊢ Call src⇩1 DotCall call⇩1 ⇛ Call src⇩2 DotCall call⇩2"
|OclAnySafeDotCallN:
"Γ ⊢ src⇩1 ⇛ src⇩2 ⟹
Γ ⊢⇩E src⇩2 : τ ⟹
OclVoid[?] ≤ τ ⟹
(Γ, to_required_type τ) ⊢⇩C call⇩1 ⇛ call⇩2 ⟹
src⇩3 = TypeOperationCall src⇩2 DotCall OclAsTypeOp (to_required_type τ) ⟹
Γ ⊢ Call src⇩1 SafeDotCall call⇩1 ⇛
If (OperationCall src⇩2 DotCall NotEqualOp [NullLiteral])
(Call src⇩3 DotCall call⇩2)
NullLiteral"
|OclAnyArrowCallN:
"Γ ⊢ src⇩1 ⇛ src⇩2 ⟹
Γ ⊢⇩E src⇩2 : τ ⟹
τ ≤ OclAny[?] ∨ τ ≤ Tuple fmempty ⟹
src⇩3 = OperationCall src⇩2 DotCall OclAsSetOp [] ⟹
Γ ⊢⇩E src⇩3 : σ ⟹
(Γ, σ) ⊢⇩C call⇩1 ⇛ call⇩2 ⟹
Γ ⊢ Call src⇩1 ArrowCall call⇩1 ⇛ Call src⇩3 ArrowCall call⇩2"

|CollectionArrowCallN:
"Γ ⊢ src⇩1 ⇛ src⇩2 ⟹
Γ ⊢⇩E src⇩2 : τ ⟹
element_type τ _ ⟹
(Γ, τ) ⊢⇩C call⇩1 ⇛ call⇩2 ⟹
Γ ⊢ Call src⇩1 ArrowCall call⇩1 ⇛ Call src⇩2 ArrowCall call⇩2"
|CollectionSafeArrowCallN:
"Γ ⊢ src⇩1 ⇛ src⇩2 ⟹
Γ ⊢⇩E src⇩2 : τ ⟹
element_type τ σ ⟹
OclVoid[?] ≤ σ ⟹
src⇩3 = TypeOperationCall src⇩2 ArrowCall SelectByKindOp
(to_required_type σ) ⟹
Γ ⊢⇩E src⇩3 : ρ ⟹
(Γ, ρ) ⊢⇩C call⇩1 ⇛ call⇩2 ⟹
Γ ⊢ Call src⇩1 SafeArrowCall call⇩1 ⇛ Call src⇩3 ArrowCall call⇩2"
|CollectionDotCallN:
"Γ ⊢ src⇩1 ⇛ src⇩2 ⟹
Γ ⊢⇩E src⇩2 : τ ⟹
element_type τ σ ⟹
(Γ, σ) ⊢⇩C call⇩1 ⇛ call⇩2 ⟹
it = new_vname Γ ⟹
Γ ⊢ Call src⇩1 DotCall call⇩1 ⇛
CollectIteratorCall src⇩2 ArrowCall [it] (Some σ) (Call (Var it) DotCall call⇩2)"
|CollectionSafeDotCallN:
"Γ ⊢ src⇩1 ⇛ src⇩2 ⟹
Γ ⊢⇩E src⇩2 : τ ⟹
element_type τ σ ⟹
OclVoid[?] ≤ σ ⟹
ρ = to_required_type σ ⟹
src⇩3 = TypeOperationCall src⇩2 ArrowCall SelectByKindOp ρ ⟹
(Γ, ρ) ⊢⇩C call⇩1 ⇛ call⇩2 ⟹
it = new_vname Γ ⟹
Γ ⊢ Call src⇩1 SafeDotCall call⇩1 ⇛
CollectIteratorCall src⇩3 ArrowCall [it] (Some ρ) (Call (Var it) DotCall call⇩2)"

|TypeOperationN:
"(Γ, τ) ⊢⇩C TypeOperation op ty ⇛ TypeOperation op ty"
|AttributeN:
"(Γ, τ) ⊢⇩C Attribute attr ⇛ Attribute attr"
|AssociationEndN:
"(Γ, τ) ⊢⇩C AssociationEnd role from ⇛ AssociationEnd role from"
|AssociationClassN:
"(Γ, τ) ⊢⇩C AssociationClass 𝒜 from ⇛ AssociationClass 𝒜 from"
|AssociationClassEndN:
"(Γ, τ) ⊢⇩C AssociationClassEnd role ⇛ AssociationClassEnd role"
|OperationN:
"Γ ⊢⇩L params⇩1 ⇛ params⇩2 ⟹
(Γ, τ) ⊢⇩C Operation op params⇩1 ⇛ Operation op params⇩2"
|TupleElementN:
"(Γ, τ) ⊢⇩C TupleElement elem ⇛ TupleElement elem"

|ExplicitlyTypedIterateN:
"Γ ⊢ res_init⇩1 ⇛ res_init⇩2 ⟹
Γ ++⇩f fmap_of_list (map (λit. (it, σ)) its) ⊢
Let res res_t⇩1 res_init⇩1 body⇩1 ⇛ Let res res_t⇩2 res_init⇩2 body⇩2 ⟹
(Γ, τ) ⊢⇩C Iterate its (Some σ) res res_t⇩1 res_init⇩1 body⇩1 ⇛
Iterate its (Some σ) res res_t⇩2 res_init⇩2 body⇩2"
|ImplicitlyTypedIterateN:
"element_type τ σ ⟹
Γ ⊢ res_init⇩1 ⇛ res_init⇩2 ⟹
Γ ++⇩f fmap_of_list (map (λit. (it, σ)) its) ⊢
Let res res_t⇩1 res_init⇩1 body⇩1 ⇛ Let res res_t⇩2 res_init⇩2 body⇩2 ⟹
(Γ, τ) ⊢⇩C Iterate its None res res_t⇩1 res_init⇩1 body⇩1 ⇛
Iterate its (Some σ) res res_t⇩2 res_init⇩2 body⇩2"

|ExplicitlyTypedIteratorN:
"Γ ++⇩f fmap_of_list (map (λit. (it, σ)) its) ⊢ body⇩1 ⇛ body⇩2  ⟹
(Γ, τ) ⊢⇩C Iterator iter its (Some σ) body⇩1 ⇛ Iterator iter its (Some σ) body⇩2"
|ImplicitlyTypedIteratorN:
"element_type τ σ ⟹
Γ ++⇩f fmap_of_list (map (λit. (it, σ)) its) ⊢ body⇩1 ⇛ body⇩2  ⟹
(Γ, τ) ⊢⇩C Iterator iter its None body⇩1 ⇛ Iterator iter its (Some σ) body⇩2"

|ExprListNilN:
"Γ ⊢⇩L [] ⇛ []"
|ExprListConsN:
"Γ ⊢ x ⇛ y ⟹
Γ ⊢⇩L xs ⇛ ys ⟹
Γ ⊢⇩L x # xs ⇛ y # ys"

(*** Elimination Rules ******************************************************)

section ‹Elimination Rules›

inductive_cases LiteralNE [elim]: "Γ ⊢ Literal a ⇛ b"
inductive_cases LetNE [elim]: "Γ ⊢ Let v t init body ⇛ b"
inductive_cases VarNE [elim]: "Γ ⊢ Var v ⇛ b"
inductive_cases IfNE [elim]: "Γ ⊢ If a b c ⇛ d"

inductive_cases MetaOperationCallNE [elim]: "Γ ⊢ MetaOperationCall τ op ⇛ b"
inductive_cases StaticOperationCallNE [elim]: "Γ ⊢ StaticOperationCall τ op as ⇛ b"
inductive_cases DotCallNE [elim]: "Γ ⊢ Call src DotCall call ⇛ b"
inductive_cases SafeDotCallNE [elim]: "Γ ⊢ Call src SafeDotCall call ⇛ b"
inductive_cases ArrowCallNE [elim]: "Γ ⊢ Call src ArrowCall call ⇛ b"
inductive_cases SafeArrowCallNE [elim]: "Γ ⊢ Call src SafeArrowCall call ⇛ b"

inductive_cases CallNE [elim]: "(Γ, τ) ⊢⇩C call ⇛ b"
inductive_cases OperationCallNE [elim]: "(Γ, τ) ⊢⇩C Operation op as ⇛ call"
inductive_cases IterateCallNE [elim]: "(Γ, τ) ⊢⇩C Iterate its its_ty res res_t res_init body ⇛ call"
inductive_cases IteratorCallNE [elim]: "(Γ, τ) ⊢⇩C Iterator iter its its_ty body ⇛ call"

inductive_cases ExprListNE [elim]: "Γ ⊢⇩L xs ⇛ ys"

(*** Simplification Rules ***************************************************)

section ‹Simplification Rules›

inductive_simps normalize_alt_simps:
"Γ ⊢ Literal a ⇛ b"
"Γ ⊢ Let v t init body ⇛ b"
"Γ ⊢ Var v ⇛ b"
"Γ ⊢ If a b c ⇛ d"

"Γ ⊢ MetaOperationCall τ op ⇛ b"
"Γ ⊢ StaticOperationCall τ op as ⇛ b"
"Γ ⊢ Call src DotCall call ⇛ b"
"Γ ⊢ Call src SafeDotCall call ⇛ b"
"Γ ⊢ Call src ArrowCall call ⇛ b"
"Γ ⊢ Call src SafeArrowCall call ⇛ b"

"(Γ, τ) ⊢⇩C call ⇛ b"
"(Γ, τ) ⊢⇩C Operation op as ⇛ call"
"(Γ, τ) ⊢⇩C Iterate its its_ty res res_t res_init body ⇛ call"
"(Γ, τ) ⊢⇩C Iterator iter its its_ty body ⇛ call"

"Γ ⊢⇩L [] ⇛ ys"
"Γ ⊢⇩L x # xs ⇛ ys"

(*** Determinism ************************************************************)

section ‹Determinism›

lemma any_has_not_element_type:
"element_type τ σ ⟹ τ ≤ OclAny[?] ∨ τ ≤ Tuple fmempty ⟹ False"
by (erule element_type.cases; auto)

lemma any_has_not_element_type':
"element_type τ σ ⟹ OclVoid[?] ≤ τ ⟹ False"
by (erule element_type.cases; auto)

lemma
normalize_det:
"Γ ⊢ expr ⇛ expr⇩1 ⟹
Γ ⊢ expr ⇛ expr⇩2 ⟹ expr⇩1 = expr⇩2" and
normalize_call_det:
"Γ_τ ⊢⇩C call ⇛ call⇩1 ⟹
Γ_τ ⊢⇩C call ⇛ call⇩2 ⟹ call⇩1 = call⇩2" and
normalize_expr_list_det:
"Γ ⊢⇩L xs ⇛ ys ⟹
Γ ⊢⇩L xs ⇛ zs ⟹ ys = zs"
for Γ :: "('a :: ocl_object_model) type env"
and Γ_τ :: "('a :: ocl_object_model) type env × 'a type"
proof (induct arbitrary: expr⇩2 and call⇩2 and zs
rule: normalize_normalize_call_normalize_expr_list.inducts)
case (LiteralN Γ a) thus ?case by auto
next
case (ExplicitlyTypedLetN Γ init⇩1 init⇩2 v τ body⇩1 body⇩2) thus ?case
by blast
next
case (ImplicitlyTypedLetN Γ init⇩1 init⇩2 τ v body⇩1 body⇩2) thus ?case
by (metis (mono_tags, lifting) LetNE option.distinct(1) typing_det)
next
case (VarN Γ v) thus ?case by auto
next
case (IfN Γ a⇩1 a⇩2 b⇩1 b⇩2 c⇩1 c⇩2) thus ?case
apply (insert IfN.prems)
apply (erule IfNE)
next
case (MetaOperationCallN Γ τ op) thus ?case by auto
next
case (StaticOperationCallN Γ params⇩1 params⇩2 τ op) thus ?case by blast
next
case (OclAnyDotCallN Γ src⇩1 src⇩2 τ call⇩1 call⇩2) show ?case
apply (insert OclAnyDotCallN.prems)
apply (erule DotCallNE)
using OclAnyDotCallN.hyps typing_det apply metis
using OclAnyDotCallN.hyps any_has_not_element_type typing_det by metis
next
case (OclAnySafeDotCallN Γ src⇩1 src⇩2 τ call⇩1 call⇩2) show ?case
apply (insert OclAnySafeDotCallN.prems)
apply (erule SafeDotCallNE)
using OclAnySafeDotCallN.hyps typing_det comp_apply
apply (metis (no_types, lifting) list.simps(8) list.simps(9))
using OclAnySafeDotCallN.hyps typing_det any_has_not_element_type'
by metis
next
case (OclAnyArrowCallN Γ src⇩1 src⇩2 τ src⇩3 σ call⇩1 call⇩2) show ?case
apply (insert OclAnyArrowCallN.prems)
apply (erule ArrowCallNE)
using OclAnyArrowCallN.hyps typing_det comp_apply apply metis
using OclAnyArrowCallN.hyps typing_det any_has_not_element_type
by metis
next
case (CollectionArrowCallN Γ src⇩1 src⇩2 τ uu call⇩1 call⇩2) show ?case
apply (insert CollectionArrowCallN.prems)
apply (erule ArrowCallNE)
using CollectionArrowCallN.hyps typing_det any_has_not_element_type
apply metis
using CollectionArrowCallN.hyps typing_det by metis
next
case (CollectionSafeArrowCallN Γ src⇩1 src⇩2 τ σ src⇩3 ρ call⇩1 call⇩2) show ?case
apply (insert CollectionSafeArrowCallN.prems)
apply (erule SafeArrowCallNE)
using CollectionSafeArrowCallN.hyps typing_det element_type_det by metis
next
case (CollectionDotCallN Γ src⇩1 src⇩2 τ σ call⇩1 call⇩2 it) show ?case
apply (insert CollectionDotCallN.prems)
apply (erule DotCallNE)
using CollectionDotCallN.hyps typing_det any_has_not_element_type
apply metis
using CollectionDotCallN.hyps typing_det element_type_det by metis
next
case (CollectionSafeDotCallN Γ src⇩1 src⇩2 τ σ src⇩3 call⇩1 call⇩2 it) show ?case
apply (insert CollectionSafeDotCallN.prems)
apply (erule SafeDotCallNE)
using CollectionSafeDotCallN.hyps typing_det any_has_not_element_type'
apply metis
using CollectionSafeDotCallN.hyps typing_det element_type_det by metis
next
case (TypeOperationN Γ τ op ty) thus ?case by auto
next
case (AttributeN Γ τ attr) thus ?case by auto
next
case (AssociationEndN Γ τ role "from") thus ?case by auto
next
case (AssociationClassN Γ τ 𝒜 "from") thus ?case by auto
next
case (AssociationClassEndN Γ τ role) thus ?case by auto
next
case (OperationN Γ params⇩1 params⇩2 τ op) thus ?case by blast
next
case (TupleElementN Γ τ elem) thus ?case by auto
next
case (ExplicitlyTypedIterateN
Γ res_init⇩1 res_init⇩2 σ its res res_t⇩1 body⇩1 res_t⇩2 body⇩2 τ)
show ?case
apply (insert ExplicitlyTypedIterateN.prems)
apply (erule IterateCallNE)
using ExplicitlyTypedIterateN.hyps element_type_det by blast+
next
case (ImplicitlyTypedIterateN
τ σ Γ res_init⇩1 res_init⇩2 its res res_t⇩1 body⇩1 res_t⇩2 body⇩2)
show ?case
apply (insert ImplicitlyTypedIterateN.prems)
apply (erule IterateCallNE)
using ImplicitlyTypedIterateN.hyps element_type_det by blast+
next
case (ExplicitlyTypedIteratorN Γ σ its body⇩1 body⇩2 τ iter)
show ?case
apply (insert ExplicitlyTypedIteratorN.prems)
apply (erule IteratorCallNE)
using ExplicitlyTypedIteratorN.hyps element_type_det by blast+
next
case (ImplicitlyTypedIteratorN τ σ Γ its body⇩1 body⇩2 iter)
show ?case
apply (insert ImplicitlyTypedIteratorN.prems)
apply (erule IteratorCallNE)
using ImplicitlyTypedIteratorN.hyps element_type_det by blast+
next
case (ExprListNilN Γ) thus ?case
using normalize_expr_list.cases by auto
next
case (ExprListConsN Γ x y xs ys) thus ?case by blast
qed

(*** Normalized Expressions Typing ******************************************)

section ‹Normalized Expressions Typing›

text ‹
Here is the final typing rules.›

inductive nf_typing ("(1_/ ⊢/ (_ :/ _))" [51,51,51] 50) where
"Γ ⊢ expr ⇛ expr⇩N ⟹
Γ ⊢⇩E expr⇩N : τ ⟹
Γ ⊢ expr : τ"

lemma nf_typing_det:
"Γ ⊢ expr : τ ⟹
Γ ⊢ expr : σ ⟹ τ = σ"
by (metis nf_typing.cases normalize_det typing_det)

(*** Code Setup *************************************************************)

section ‹Code Setup›

code_pred normalize .

code_pred nf_typing .

definition "check_type Γ expr τ ≡
Predicate.eval (nf_typing_i_i_i Γ expr τ) ()"

definition "synthesize_type Γ expr ≡
Predicate.singleton (λ_. OclInvalid)
(Predicate.map errorable (nf_typing_i_i_o Γ expr))"

text ‹
It is the only usage of the @{text OclInvalid} type.
This type is not required to define typing rules.
It is only required to make the typing function total.›

end