Theory OCL_Normalization

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
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,
\item unfolding of navigation shorthands and safe navigation operators,
      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
    formally considering operations overloading, complex relations between
    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)
    by (simp add: IfN.hyps)
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