Theory TypeRelRefine

(*  Title:      JinjaThreads/Execute/TypeRelRefine.thy
    Author:     Andreas Lochbihler

    Tabulation for lookup functions
*)

section ‹Tabulation for lookup functions›

theory TypeRelRefine
imports
  "../Common/TypeRel"
  "HOL-Library.AList_Mapping"
begin

subsection ‹Auxiliary lemmata›

lemma rtranclp_tranclpE:
  assumes "r^** x y"
  obtains (refl) "x = y"
  | (trancl) "r^++ x y"
using assms
by(cases)(blast dest: rtranclp_into_tranclp1)+

lemma map_of_map2: "map_of (map (λ(k, v). (k, f k v)) xs) k = map_option (f k) (map_of xs k)"
by(induct xs) auto

lemma map_of_map_K: "map_of (map (λk. (k, c)) xs) k = (if k ∈ set xs then Some c else None)"
by(induct xs) auto

lift_definition map_values :: "('a ⇒ 'b ⇒ 'c) ⇒ ('a, 'b) mapping ⇒ ('a, 'c) mapping"
is "λf m k. map_option (f k) (m k)" .

lemma map_values_Mapping [simp]: 
  "map_values f (Mapping.Mapping m) = Mapping.Mapping (λk. map_option (f k) (m k))"
by(rule map_values.abs_eq)

lemma map_Mapping: "Mapping.map f g (Mapping.Mapping m) = Mapping.Mapping (map_option g ∘ m ∘ f)"
by(rule map.abs_eq)

abbreviation subclst :: "'m prog ⇒ cname ⇒ cname ⇒ bool"
where "subclst P ≡ (subcls1 P)^++"

subsection ‹Representation type for tabulated lookup functions›

type_synonym
  'm prog_impl' = 
  "'m cdecl list ×
   (cname, 'm class) mapping ×
   (cname, cname set) mapping × 
   (cname, (vname, cname × ty × fmod) mapping) mapping × 
   (cname, (mname, cname × ty list × ty × 'm option) mapping) mapping"

lift_definition tabulate_class :: "'m cdecl list ⇒ (cname, 'm class) mapping"
is "class ∘ Program" .

lift_definition tabulate_subcls :: "'m cdecl list ⇒ (cname, cname set) mapping"
is "λP C. if is_class (Program P) C then Some {D. Program P ⊢ C ≼⇧* D} else None" .

lift_definition tabulate_sees_field :: "'m cdecl list ⇒ (cname, (vname, cname × ty × fmod) mapping) mapping"
is "λP C. if is_class (Program P) C then
        Some (λF. if ∃T fm D. Program P ⊢ C sees F:T (fm) in D then Some (field (Program P) C F) else None)
      else None" .

lift_definition tabulate_Method :: "'m cdecl list ⇒ (cname, (mname, cname × ty list × ty × 'm option) mapping) mapping"
is "λP C. if is_class (Program P) C then
         Some (λM. if ∃Ts T mthd D. Program P ⊢ C sees M:Ts→T=mthd in D then Some (method (Program P) C M) else None)
      else None" .

fun wf_prog_impl' :: "'m prog_impl' ⇒ bool"
where
  "wf_prog_impl' (P, c, s, f, m) ⟷
  c = tabulate_class P ∧
  s = tabulate_subcls P ∧
  f = tabulate_sees_field P ∧
  m = tabulate_Method P"

subsection ‹Implementation type for tabulated lookup functions›

typedef 'm prog_impl = "{P :: 'm prog_impl'. wf_prog_impl' P}"
  morphisms impl_of ProgRefine 
proof
  show "([], Mapping.empty, Mapping.empty, Mapping.empty, Mapping.empty) ∈ ?prog_impl"
    apply clarsimp
    by transfer (simp_all add: fun_eq_iff is_class_def rel_funI)
qed

lemma impl_of_ProgImpl [simp]:
  "wf_prog_impl' Pfsm ⟹ impl_of (ProgRefine Pfsm) = Pfsm"
by(simp add: ProgRefine_inverse)

definition program :: "'m prog_impl ⇒ 'm prog"
where "program = Program ∘ fst ∘ impl_of"

code_datatype program

lemma prog_impl_eq_iff:
  "Pi = Pi' ⟷ program Pi = program Pi'" for Pi Pi'
apply(cases Pi)
apply(cases Pi')
apply(auto simp add: ProgRefine_inverse program_def ProgRefine_inject)
done

lemma wf_prog_impl'_impl_of [simp, intro!]:
  "wf_prog_impl' (impl_of Pi)" for Pi
using impl_of[of Pi] by simp

lemma ProgImpl_impl_of [simp, code abstype]:
  "ProgRefine (impl_of Pi) = Pi" for Pi
by(rule impl_of_inverse)

lemma program_ProgRefine [simp]: "wf_prog_impl' Psfm ⟹ program (ProgRefine Psfm) = Program (fst Psfm)"
by(simp add: program_def)

lemma classes_program [code]: "classes (program P) = fst (impl_of P)"
by(simp add: program_def)

lemma class_program [code]: "class (program Pi) = Mapping.lookup (fst (snd (impl_of Pi)))" for Pi
by(cases Pi)(clarsimp simp add: tabulate_class_def lookup.rep_eq Mapping_inverse)

subsection ‹Refining sub class and lookup functions to use precomputed mappings›

lemma subcls'_program [code]: 
  "subcls' (program Pi) C D ⟷ 
  C = D ∨
  (case Mapping.lookup (fst (snd (snd (impl_of Pi)))) C of None ⇒ False
   | Some m ⇒ D ∈ m)" for Pi
apply(cases Pi)
apply(clarsimp simp add: subcls'_def tabulate_subcls_def lookup.rep_eq Mapping_inverse)
apply(auto elim!: rtranclp_tranclpE dest: subcls_is_class intro: tranclp_into_rtranclp)
done

lemma subcls'_i_i_i_program [code]:
  "subcls'_i_i_i P C D = (if subcls' P C D then Predicate.single () else bot)"
by(rule pred_eqI)(auto elim: subcls'_i_i_iE intro: subcls'_i_i_iI)

lemma subcls'_i_i_o_program [code]:
  "subcls'_i_i_o (program Pi) C = 
  sup (Predicate.single C) (case Mapping.lookup (fst (snd (snd (impl_of Pi)))) C of None ⇒ bot | Some m ⇒ pred_of_set m)" for Pi
by(cases Pi)(fastforce simp add: subcls'_i_i_o_def subcls'_def tabulate_subcls_def lookup.rep_eq Mapping_inverse intro!: pred_eqI split: if_split_asm elim: rtranclp_tranclpE dest: subcls_is_class intro: tranclp_into_rtranclp)

lemma rtranclp_FioB_i_i_subcls1_i_i_o_code [code_unfold]:
  "rtranclp_FioB_i_i (subcls1_i_i_o P) = subcls'_i_i_i P"
by(auto simp add: fun_eq_iff subcls1_i_i_o_def subcls'_def rtranclp_FioB_i_i_def subcls'_i_i_i_def)

lemma Method_program [code]:
  "program Pi ⊢ C sees M:Ts→T=meth in D ⟷ 
  (case Mapping.lookup (snd (snd (snd (snd (impl_of Pi))))) C of 
    None ⇒ False
  | Some m ⇒ 
    (case Mapping.lookup m M of 
       None ⇒ False
     | Some (D', Ts', T', meth') ⇒ Ts = Ts' ∧ T = T' ∧ meth = meth' ∧ D = D'))" for Pi
by(cases Pi)(auto split: if_split_asm dest: sees_method_is_class simp add: tabulate_Method_def lookup.rep_eq Mapping_inverse)

lemma Method_i_i_i_o_o_o_o_program [code]:
  "Method_i_i_i_o_o_o_o (program Pi) C M = 
  (case Mapping.lookup (snd (snd (snd (snd (impl_of Pi))))) C of
    None ⇒ bot
  | Some m ⇒
    (case Mapping.lookup m M of
      None ⇒ bot
    | Some (D, Ts, T, meth) ⇒ Predicate.single (Ts, T, meth, D)))" for Pi
by(auto simp add: Method_i_i_i_o_o_o_o_def Method_program intro!: pred_eqI)

lemma Method_i_i_i_o_o_o_i_program [code]:
  "Method_i_i_i_o_o_o_i (program Pi) C M D = 
  (case Mapping.lookup (snd (snd (snd (snd (impl_of Pi))))) C of
    None ⇒ bot
  | Some m ⇒
    (case Mapping.lookup m M of
      None ⇒ bot
    | Some (D', Ts, T, meth) ⇒ if D = D' then Predicate.single (Ts, T, meth) else bot))" for Pi
by(auto simp add: Method_i_i_i_o_o_o_i_def Method_program intro!: pred_eqI)

lemma sees_field_program [code]:
  "program Pi ⊢ C sees F:T (fd) in D ⟷
  (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of
    None ⇒ False
  | Some m ⇒ 
    (case Mapping.lookup m F of 
       None ⇒ False
     | Some (D', T', fd') ⇒ T = T' ∧ fd = fd' ∧ D = D'))" for Pi
by(cases Pi)(auto split: if_split_asm dest: has_visible_field[THEN has_field_is_class] simp add: tabulate_sees_field_def lookup.rep_eq Mapping_inverse)

lemma sees_field_i_i_i_o_o_o_program [code]:
  "sees_field_i_i_i_o_o_o (program Pi) C F =
  (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of
    None ⇒ bot
  | Some m ⇒
    (case Mapping.lookup m F of
       None ⇒ bot
    | Some (D, T, fd) ⇒ Predicate.single(T, fd, D)))" for Pi
by(auto simp add: sees_field_program sees_field_i_i_i_o_o_o_def intro: pred_eqI)

lemma sees_field_i_i_i_o_o_i_program [code]:
  "sees_field_i_i_i_o_o_i (program Pi) C F D =
  (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of
    None ⇒ bot
  | Some m ⇒
    (case Mapping.lookup m F of
       None ⇒ bot
    | Some (D', T, fd) ⇒ if D = D' then Predicate.single(T, fd) else bot))" for Pi
by(auto simp add: sees_field_program sees_field_i_i_i_o_o_i_def intro: pred_eqI)

lemma field_program [code]:
  "field (program Pi) C F = 
  (case Mapping.lookup (fst (snd (snd (snd (impl_of Pi))))) C of 
    None ⇒ Code.abort (STR ''not_unique'') (λ_. Predicate.the bot)
  | Some m ⇒ 
    (case Mapping.lookup m F of
       None ⇒ Code.abort (STR ''not_unique'') (λ_. Predicate.the bot)
     | Some (D', T, fd) ⇒ (D', T, fd)))" for Pi
unfolding field_def
by(cases Pi)(fastforce simp add: Predicate.the_def tabulate_sees_field_def lookup.rep_eq Mapping_inverse split: if_split_asm intro: arg_cong[where f=The] dest: has_visible_field[THEN has_field_is_class] sees_field_fun)

subsection ‹Implementation for precomputing mappings›

definition tabulate_program :: "'m cdecl list ⇒ 'm prog_impl"
where "tabulate_program P = ProgRefine (P, tabulate_class P, tabulate_subcls P, tabulate_sees_field P, tabulate_Method P)"

lemma impl_of_tabulate_program [code abstract]:
  "impl_of (tabulate_program P) = (P, tabulate_class P, tabulate_subcls P, tabulate_sees_field P, tabulate_Method P)"
by(simp add: tabulate_program_def)

lemma Program_code [code]:
  "Program = program ∘ tabulate_program"
by(simp add: program_def fun_eq_iff tabulate_program_def)

subsubsection ‹@{term "class" }›

lemma tabulate_class_code [code]:
  "tabulate_class = Mapping.of_alist"
  by transfer (simp add: fun_eq_iff)

subsubsection ‹@{term "subcls" }›

inductive subcls1' :: "'m cdecl list ⇒ cname ⇒ cname ⇒ bool"
where 
  find: "C ≠ Object ⟹ subcls1' ((C, D, rest) # P) C D"
| step: "⟦ C ≠ Object; C ≠ C'; subcls1' P C D  ⟧ ⟹ subcls1' ((C', D', rest) # P) C D"

code_pred
  (modes: i ⇒ i ⇒ o ⇒ bool)
  subcls1' .

lemma subcls1_into_subcls1':
  assumes "subcls1 (Program P) C D"
  shows "subcls1' P C D"
proof -
  from assms obtain rest where "map_of P C = ⌊(D, rest)⌋" "C ≠ Object" by cases simp
  thus ?thesis by(induct P)(auto split: if_split_asm intro: subcls1'.intros)
qed

lemma subcls1'_into_subcls1:
  assumes "subcls1' P C D"
  shows "subcls1 (Program P) C D"
using assms
proof(induct)
  case find thus ?case by(auto intro: subcls1.intros)
next
  case step thus ?case by(auto elim!: subcls1.cases intro: subcls1.intros)
qed

lemma subcls1_eq_subcls1':
  "subcls1 (Program P) = subcls1' P"
by(auto simp add: fun_eq_iff intro: subcls1_into_subcls1' subcls1'_into_subcls1)

definition subcls'' :: "'m cdecl list ⇒ cname ⇒ cname ⇒ bool"
where "subcls'' P = (subcls1' P)^**"

code_pred
  (modes: i ⇒ i ⇒ i ⇒ bool)
  [inductify] 
  subcls'' .

lemma subcls''_eq_subcls: "subcls'' P = subcls (Program P)"
by(simp add: subcls''_def subcls1_eq_subcls1')

lemma subclst_snd_classD: 
  assumes "subclst (Program P) C D"
  shows "D ∈ fst ` snd ` set P"
using assms
by(induct)(fastforce elim!: subcls1.cases dest!: map_of_SomeD intro: rev_image_eqI)+

definition check_acyclicity :: "(cname, cname set) mapping ⇒ 'm cdecl list ⇒ unit"
where "check_acyclicity _ _ = ()"

definition cyclic_class_hierarchy :: unit 
where "cyclic_class_hierarchy = ()"

declare [[code abort: cyclic_class_hierarchy]]

lemma check_acyclicity_code:
  "check_acyclicity mapping P =
   (let _ = 
     map (λ(C, D, _).
       if C = Object then () 
       else
         (case Mapping.lookup mapping D of 
            None ⇒ ()
          | Some Cs ⇒ if C ∈ Cs then cyclic_class_hierarchy else ()))
       P
    in ())"
by simp

lemma tablulate_subcls_code [code]:
  "tabulate_subcls P = 
  (let cnames = map fst P;
       cnames' = map (fst ∘ snd) P;
       mapping = Mapping.tabulate cnames (λC. set (C # [D ← cnames'. subcls'' P C D]));
       _ = check_acyclicity mapping P
   in mapping
  )"
apply(auto simp add: tabulate_subcls_def Mapping.tabulate_def fun_eq_iff is_class_def o_def map_of_map2[simplified split_def] Mapping_inject)
 apply(subst map_of_map2[simplified split_def])
 apply(auto simp add: fun_eq_iff subcls''_eq_subcls map_of_map_K dest: subclst_snd_classD elim: rtranclp_tranclpE)[1]
apply(subst map_of_map2[simplified split_def])
apply(rule sym)
apply simp
apply(case_tac "map_of P x")
apply auto
done

subsubsection ‹@{term Fields}›

text ‹
  Problem: Does not terminate for cyclic class hierarchies!
  This problem already occurs in Jinja's well-formedness checker: 
  ‹wf_cdecl› calls ‹wf_mdecl› before checking for acyclicity, 
  but ‹wf_J_mdecl› involves the type judgements, 
  which in turn requires @{term "Fields"} (via @{term sees_field}).
  Checking acyclicity before executing @{term "Fields'"} for tabulation is difficult
  because we would have to intertwine tabulation and well-formedness checking.
  Possible (local) solution:
  additional termination parameter (like memoisation for @{term "rtranclp"}) 
  and list option as error return parameter.
›
inductive
  Fields' :: "'m cdecl list ⇒ cname ⇒ ((vname × cname) × (ty × fmod)) list ⇒ bool"
for P :: "'m cdecl list"
where 
  rec:
  "⟦ map_of P C = Some(D,fs,ms); C ≠ Object; Fields' P D FDTs;
     FDTs' = map (λ(F,Tm). ((F,C),Tm)) fs @ FDTs ⟧
  ⟹ Fields' P C FDTs'"
| Object:
  "⟦ map_of P Object = Some(D,fs,ms); FDTs = map (λ(F,T). ((F,Object),T)) fs ⟧
  ⟹ Fields' P Object FDTs"

lemma Fields'_into_Fields:
  assumes "Fields' P C FDTs"
  shows "Program P ⊢ C has_fields FDTs"
using assms
by induct(auto intro: Fields.intros)

lemma Fields_into_Fields':
  assumes "Program P ⊢ C has_fields FDTs"
  shows "Fields' P C FDTs"
using assms
by induct(auto intro: Fields'.intros)

lemma Fields'_eq_Fields:
  "Fields' P = Fields (Program P)"
by(auto simp add: fun_eq_iff intro: Fields'_into_Fields Fields_into_Fields')

code_pred 
  (modes: i ⇒ i ⇒ o ⇒ bool)
  Fields' .

definition fields' :: "'m cdecl list ⇒ cname ⇒ ((vname × cname) × (ty × fmod)) list"
where "fields' P C = (if ∃FDTs. Fields' P C FDTs then THE FDTs. Fields' P C FDTs else [])"

lemma eval_Fields'_conv:
  "Predicate.eval (Fields'_i_i_o P C) = Fields' P C"
by(auto intro: Fields'_i_i_oI elim: Fields'_i_i_oE intro!: ext)

lemma fields'_code [code]:
  "fields' P C = 
  (let FDTs = Fields'_i_i_o P C in if Predicate.holds (FDTs ⤜ (λ_. Predicate.single ())) then Predicate.the FDTs else [])"
by(auto simp add: fields'_def holds_eq Fields'_i_i_o_def intro: Fields'_i_i_oI Predicate.the_eqI[THEN sym])

lemma The_Fields [simp]:
  "P ⊢ C has_fields FDTs ⟹ The (Fields P C) = FDTs"
by(auto dest: has_fields_fun)

lemma tabulate_sees_field_code [code]:
  "tabulate_sees_field P =
   Mapping.tabulate (map fst P) (λC. Mapping.of_alist (map (λ((F, D), Tfm). (F, (D, Tfm))) (fields' P C)))"
apply(simp add: tabulate_sees_field_def tabulate_def is_class_def fields'_def Fields'_eq_Fields Mapping_inject)
apply(rule ext)
apply clarsimp
apply(rule conjI)
 apply(clarsimp simp add: o_def)
 apply(subst map_of_map2[unfolded split_def])
 apply simp
 apply transfer
 apply(rule conjI)
  apply clarsimp
  apply(rule ext)
  apply clarsimp
  apply(rule conjI)
   apply(clarsimp simp add: sees_field_def Fields'_eq_Fields)
   apply(drule (1) has_fields_fun, clarsimp)
  apply clarify
  apply(rule sym)
  apply(rule ccontr)
  apply(clarsimp simp add: sees_field_def Fields'_eq_Fields)
 apply clarsimp
 apply(rule ext)
 apply(clarsimp simp add: sees_field_def)
apply(clarsimp simp add: o_def)
apply(subst map_of_map2[simplified split_def])
apply(rule sym)
apply(clarsimp)
apply(rule ccontr)
apply simp
done

subsubsection ‹@{term "Methods" }›

text ‹Same termination problem as for @{term Fields'}›
inductive Methods' :: "'m cdecl list ⇒ cname ⇒ (mname × (ty list × ty × 'm option) × cname) list ⇒ bool"
  for P :: "'m cdecl list"
where 
  "⟦ map_of P Object = Some(D,fs,ms); Mm = map (λ(M, rest). (M, (rest, Object))) ms ⟧
   ⟹ Methods' P Object Mm"
| "⟦ map_of P C = Some(D,fs,ms); C ≠ Object; Methods' P D Mm;
     Mm' = map (λ(M, rest). (M, (rest, C))) ms @ Mm ⟧
   ⟹ Methods' P C Mm'"

lemma Methods'_into_Methods:
  assumes "Methods' P C Mm"
  shows "Program P ⊢ C sees_methods (map_of Mm)"
using assms
apply induct
 apply(clarsimp simp add: o_def split_def)
 apply(rule sees_methods_Object)
  apply fastforce
 apply(rule ext)
 apply(subst map_of_map2[unfolded split_def])
 apply(simp add: o_def)

apply(rule sees_methods_rec)
   apply fastforce
  apply simp
 apply assumption
apply(clarsimp simp add: map_add_def map_of_map2)
done

lemma Methods_into_Methods':
  assumes "Program P ⊢ C sees_methods Mm"
  shows "∃Mm'. Methods' P C Mm' ∧ Mm = map_of Mm'"
using assms
by induct(auto intro: Methods'.intros simp add: map_of_map2 map_add_def)

code_pred 
  (modes: i ⇒ i ⇒ o ⇒ bool)
  Methods'
.

definition methods' :: "'m cdecl list ⇒ cname ⇒ (mname × (ty list × ty × 'm option) × cname) list"
where "methods' P C = (if ∃Mm. Methods' P C Mm then THE Mm. Methods' P C Mm else [])"

lemma methods'_code [code]:
  "methods' P C =
  (let Mm = Methods'_i_i_o P C
   in if Predicate.holds (Mm ⤜ (λ_. Predicate.single ())) then Predicate.the Mm else [])"
unfolding methods'_def
by(auto simp add: holds_eq Methods'_i_i_o_def Predicate.the_def)

lemma Methods'_fun:
  assumes "Methods' P C Mm"
  shows "Methods' P C Mm' ⟹ Mm = Mm'"
using assms
apply(induct arbitrary: Mm')
 apply(fastforce elim: Methods'.cases)
apply(rotate_tac -1)
apply(erule Methods'.cases)
 apply(fastforce)
apply clarify
apply(simp)
done

lemma The_Methods' [simp]: "Methods' P C Mm ⟹ The (Methods' P C) = Mm"
by(auto dest: Methods'_fun)

lemma methods_def2 [simp]: "Methods' P C Mm ⟹ methods' P C = Mm"
by(auto simp add: methods'_def)

lemma tabulate_Method_code [code]:
  "tabulate_Method P =
   Mapping.tabulate (map fst P) (λC. Mapping.of_alist (map (λ(M, (rest, D)). (M, D, rest)) (methods' P C)))"
apply(simp add: tabulate_Method_def tabulate_def o_def lookup.rep_eq Mapping_inject)
apply(rule ext)
apply clarsimp
apply(rule conjI)
 apply clarify
 apply(rule sym)
 apply(subst map_of_map2[unfolded split_def])
 apply(simp add: is_class_def)
 apply transfer
 apply(rule ext)
 apply(simp add: map_of_map2)
 apply(rule conjI)
  apply(clarsimp simp add: map_of_map2 Method_def)
  apply(drule Methods_into_Methods')
  apply clarsimp
  apply(simp add: split_def)
  apply(subst map_of_map2[unfolded split_def])
  apply simp
 apply clarify
 apply(clarsimp simp add: methods'_def)
 apply(frule Methods'_into_Methods)
 apply(clarsimp simp add: Method_def)
 apply(simp add: split_def)
 apply(subst map_of_map2[unfolded split_def])
 apply(fastforce intro: ccontr)
apply clarify
apply(rule sym)
apply(simp add: map_of_eq_None_iff is_class_def)
apply(simp only: set_map[symmetric] map_map o_def fst_conv)
apply simp
done

text ‹Merge modules TypeRel, Decl and TypeRelRefine to avoid cyclic modules›

code_identifier
  code_module TypeRel ⇀
    (SML) TypeRel and (Haskell) TypeRel and (OCaml) TypeRel
| code_module TypeRelRefine ⇀
    (SML) TypeRel and (Haskell) TypeRel and (OCaml) TypeRel
| code_module Decl ⇀
    (SML) TypeRel and (Haskell) TypeRel and (OCaml) TypeRel

ML_val ‹@{code Program}›

end