Theory PCompilerRefine

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

    Tabulation for the compiler

theory PCompilerRefine

subsection @{term "compP"}

text ‹
  Applying the compiler to a tabulated program either compiles every
  method twice (once for the program itself and once for method lookup)
  or recomputes the class and method lookup tabulation from scratch.
  We follow the second approach.

fun compP_code' :: "(cname  mname  ty list  ty  'a  'b)  'a prog_impl'  'b prog_impl'"
  "compP_code' f (P, Cs, s, F, m) = 
  (let P' = map (compC f) P
   in (P', tabulate_class P', s, F, tabulate_Method P'))"

definition compP_code :: "(cname  mname  ty list  ty  'a  'b)  'a prog_impl  'b prog_impl"
where "compP_code f P = ProgRefine (compP_code' f (impl_of P))"

declare compP.simps [simp del] compP.simps[symmetric, simp]

lemma compP_code_code [code abstract]:
  "impl_of (compP_code f P) = compP_code' f (impl_of P)"
apply(cases P)
apply(simp add: compP_code_def)
apply(subst ProgRefine_inverse)
apply(auto simp add: tabulate_subcls_def tabulate_sees_field_def Mapping_inject intro!: ext)

declare compP.simps [simp] compP.simps[symmetric, simp del]

lemma compP_program [code]:
  "compP f (program P) = program (compP_code f P)"
by(cases P)(clarsimp simp add: program_def compP_code_code)

text ‹Merge module names to avoid cycles in module dependency›

  code_module PCompiler 
    (SML) PCompiler and (OCaml) PCompiler and (Haskell) PCompiler 
| code_module PCompilerRefine 
    (SML) PCompiler and (OCaml) PCompiler and (Haskell) PCompiler 

ML_val @{code compP}