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:TsT=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›

declare subcls'.equation [code del]

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)

declare Method.equation[code del]
lemma Method_program [code]:
  "program Pi  C sees M:TsT=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)

declare sees_field.equation[code del]

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 [code del]: "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