Theory Execute

(*  Author:      Lukas Bulwahn, TU Muenchen, 2009  *)

theory Execute
imports FJSound
begin

section {* Executing FeatherweightJava programs *}
text {* We execute FeatherweightJava programs using the predicate compiler. *}

code_pred (modes: i => i => i => bool,
  i => i => o => bool as supertypes_of) subtyping .

thm subtyping.equation

text {* The reduction relation requires that we inverse the @{term List.append} function.
Therefore, we define a new predicate append and derive introduction rules. *}

definition append where "append xs ys zs = (zs = xs @ ys)"

lemma [code_pred_intro]: "append [] xs xs"
unfolding append_def by simp

lemma [code_pred_intro]: "append xs ys zs ==> append (x#xs) ys (x#zs)"
unfolding append_def by simp

text {* With this at hand, we derive new introduction rules for the reduction relation: *}

lemma rc_invk_arg': "CT \<turnstile> ei -> ei' ==> append el (ei # er) e' ==> append el (ei' # er) e'' ==>
CT \<turnstile> MethodInvk e m e' -> MethodInvk e m e''"
unfolding append_def by simp (rule reduction.intros(6))

lemma rc_new_arg': "CT \<turnstile> ei -> ei' ==> append el (ei # er) e ==> append el (ei' # er) e'
   ==> CT \<turnstile> New C e -> New C e'"
unfolding append_def by simp (rule reduction.intros(7))

lemmas [code_pred_intro] = reduction.intros(1-5)
  rc_invk_arg' rc_new_arg' reduction.intros(8)

code_pred (modes: i => i => i => bool, i => i => o => bool as reduce) reduction
proof -
  case append
  from this show thesis
    unfolding append_def by (cases xa) fastforce+
next
  case reduction
  from reduction.prems show thesis
  proof (cases rule: reduction.cases)
    case r_field
    with reduction(1) show thesis by fastforce
  next
    case r_invk
    with reduction(2) show thesis by fastforce
  next
    case r_cast
    with reduction(3) show thesis by fastforce
  next
    case rc_field
    with reduction(4) show thesis by fastforce
  next
    case rc_invk_recv
    with reduction(5) show thesis by fastforce
  next
    case rc_invk_arg
    with reduction(6) show thesis
      unfolding append_def by fastforce
  next
    case rc_new_arg
    with reduction(7) show thesis
      unfolding append_def by fastforce
  next
    case rc_cast
    with reduction(8) show thesis by fastforce
  qed
qed

thm reduction.equation

code_pred reductions .

thm reductions.equation

text {* We also make the class typing executable: this requires that
  we derive rules for @{term "method_typing"}. *}

definition method_typing_aux
where
  "method_typing_aux CT m D Cs C = (¬ (∀Ds D0. mtype(CT,m,D) = Ds -> D0 --> Cs = Ds ∧ C = D0))"

lemma method_typing_aux:
  "(∀Ds D0. mtype(CT,m,D) = Ds -> D0 --> Cs = Ds ∧ C = D0) = (¬ method_typing_aux CT m D Cs C)"
unfolding method_typing_aux_def by auto

lemma [code_pred_intro]:
  "mtype(CT,m,D) = Ds -> D0 ==> Cs ≠ Ds ==> method_typing_aux CT m D Cs C"
unfolding method_typing_aux_def by auto

lemma [code_pred_intro]:
  "mtype(CT,m,D) = Ds -> D0 ==> C ≠ D0 ==> method_typing_aux CT m D Cs C"
unfolding method_typing_aux_def by auto

declare method_typing.intros[unfolded method_typing_aux, code_pred_intro]

declare class_typing.intros[unfolded append_def[symmetric], code_pred_intro]

code_pred (modes: i => i => bool) class_typing
proof -
  case class_typing
  from class_typing.cases[OF class_typing.prems, of thesis] this(1) show thesis
    unfolding append_def by fastforce
next
  case method_typing
  from method_typing.cases[OF method_typing.prems, of thesis] this(1) show thesis
    unfolding append_def method_typing_aux_def by fastforce
next
  case method_typing_aux
  from this show thesis
    unfolding method_typing_aux_def by auto
qed

subsection {* A simple example *}

text {* We now execute a simple FJ example program: *}

abbreviation A :: className
where "A == Suc 0"

abbreviation B :: className
where "B == 2"

abbreviation cPair :: className
where "cPair == 3"

definition classA_Def :: classDef
where
  "classA_Def = (| cName = A, cSuper = Object, cFields = [], cConstructor = (|kName = A, kParams = [], kSuper = [], kInits = []|)),, cMethods = []|)),"

definition
  "classB_Def = (| cName = B, cSuper = Object, cFields = [], cConstructor = (|kName = B, kParams = [], kSuper = [], kInits = []|)),, cMethods = []|)),"

abbreviation ffst :: varName
where
  "ffst == 4"

abbreviation fsnd :: varName
where
  "fsnd == 5"

abbreviation setfst :: methodName
where
  "setfst == 6"

abbreviation newfst :: varName
where
  "newfst == 7"

definition classPair_Def :: classDef
where
  "classPair_Def = (| cName = cPair, cSuper = Object,
    cFields = [(| vdName = ffst, vdType = Object |)),, (| vdName = fsnd, vdType = Object |)),],
    cConstructor = (| kName = cPair, kParams = [(| vdName = ffst, vdType = Object |)),, (| vdName = fsnd, vdType = Object |)),], kSuper = [], kInits = [ffst, fsnd]|)), ,
    cMethods = [(| mReturn = cPair, mName = setfst, mParams = [(|vdName = newfst, vdType = Object |)),],
      mBody = New cPair [Var newfst, FieldProj (Var this) fsnd]  |)),]|)),"

definition exampleProg :: classTable
  where "exampleProg = (((%x. None)(A := Some classA_Def))(B := Some classB_Def))(cPair := Some classPair_Def)"


value [code] "exampleProg \<turnstile> classA_Def OK"
value [code] "exampleProg \<turnstile> classB_Def OK"
value [code] "exampleProg \<turnstile> classPair_Def OK"


values "{x. exampleProg \<turnstile> MethodInvk (New cPair [New A [], New B []]) setfst [New B []] ->* x}"
values "{x. exampleProg \<turnstile> FieldProj (FieldProj (New cPair [New cPair [New A [], New B []], New A []]) ffst) fsnd ->* x}"


end