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 ⊢ ei → ei' ⟹ append el (ei # er) e' ⟹ append el (ei' # er) e'' ⟹
CT ⊢ MethodInvk e m e' → MethodInvk e m e''"
unfolding append_def by simp (rule reduction.intros(6))

lemma rc_new_arg': "CT ⊢ ei → ei' ⟹ append el (ei # er) e ⟹ append el (ei' # er) e'
   ==> CT ⊢ 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 "exampleProg ⊢ classA_Def OK"
value "exampleProg ⊢ classB_Def OK"
value "exampleProg ⊢ classPair_Def OK"


values "{x. exampleProg ⊢ MethodInvk (New cPair [New A [], New B []]) setfst [New B []] →* x}"
values "{x. exampleProg ⊢ FieldProj (FieldProj (New cPair [New cPair [New A [], New B []], New A []]) ffst) fsnd →* x}"


end