Theory TypeRelRefine
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›
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: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)
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