Theory execute_WellType

(*  Title:      Jinja/J/execute_WellType.thy
    Author:     Christoph Petzinger
    Copyright   2004 Technische Universitaet Muenchen
*)

section ‹Code Generation For WellType›

theory execute_WellType
imports
  WellType Examples
begin

(* Replace WT_WTs.WTCond with new intros WT_WTs.WTCond1 and WT_WTs.WTCond2 *)

lemma WTCond1:
  "⟦P,E ⊢ e :: Boolean;  P,E ⊢ e⇩1::T⇩1;  P,E ⊢ e⇩2::T⇩2; P ⊢ T⇩1 ≤ T⇩2;
    P ⊢ T⇩2 ≤ T⇩1 ⟶ T⇩2 = T⇩1 ⟧ ⟹ P,E ⊢ if (e) e⇩1 else e⇩2 :: T⇩2"
by (fastforce)

lemma WTCond2:
  "⟦P,E ⊢ e :: Boolean;  P,E ⊢ e⇩1::T⇩1;  P,E ⊢ e⇩2::T⇩2; P ⊢ T⇩2 ≤ T⇩1;
    P ⊢ T⇩1 ≤ T⇩2 ⟶ T⇩1 = T⇩2 ⟧ ⟹ P,E ⊢ if (e) e⇩1 else e⇩2 :: T⇩1"
by (fastforce)

lemmas [code_pred_intro] =
  WT_WTs.WTNew
  WT_WTs.WTCast
  WT_WTs.WTVal
  WT_WTs.WTVar
  WT_WTs.WTBinOpEq
  WT_WTs.WTBinOpAdd
  WT_WTs.WTLAss
  WT_WTs.WTFAcc
  WT_WTs.WTFAss
  WT_WTs.WTCall
  WT_WTs.WTBlock
  WT_WTs.WTSeq

declare
  WTCond1 [code_pred_intro WTCond1]
  WTCond2 [code_pred_intro WTCond2]

lemmas [code_pred_intro] =
  WT_WTs.WTWhile
  WT_WTs.WTThrow
  WT_WTs.WTTry
  WT_WTs.WTNil
  WT_WTs.WTCons

code_pred
  (modes: i ⇒ i ⇒ i ⇒ i ⇒ bool as type_check, i ⇒ i ⇒ i ⇒ o ⇒ bool as infer_type)
  WT
proof -
  case WT
  from WT.prems show thesis
  proof(cases (no_simp))
    case (WTCond E e e1 T1 e2 T2 T)
    from ‹x ⊢ T1 ≤ T2 ∨ x ⊢ T2 ≤ T1› show thesis
    proof
      assume "x ⊢ T1 ≤ T2"
      with ‹x ⊢ T1 ≤ T2 ⟶ T = T2› have "T = T2" ..
      from ‹xa = E› ‹xb = if (e) e1 else e2› ‹xc = T› ‹x,E ⊢ e :: Boolean› 
        ‹x,E ⊢ e1 :: T1› ‹x,E ⊢ e2 :: T2› ‹x ⊢ T1 ≤ T2› ‹x ⊢ T2 ≤ T1 ⟶ T = T1›
      show ?thesis unfolding ‹T = T2› by(rule WT.WTCond1[OF refl])
    next
      assume "x ⊢ T2 ≤ T1"
      with ‹x ⊢ T2 ≤ T1 ⟶ T = T1› have "T = T1" ..
      from ‹xa = E› ‹xb = if (e) e1 else e2› ‹xc = T› ‹x,E ⊢ e :: Boolean› 
        ‹x,E ⊢ e1 :: T1› ‹x,E ⊢ e2 :: T2› ‹x ⊢ T2 ≤ T1› ‹x ⊢ T1 ≤ T2 ⟶ T = T2›
      show ?thesis unfolding ‹T = T1› by(rule WT.WTCond2[OF refl])
    qed
  qed(assumption|erule (2) WT.that[OF refl])+
next
  case WTs
  from WTs.prems show thesis
    by(cases (no_simp))(assumption|erule (2) WTs.that[OF refl])+
qed

notation infer_type ("_,_ ⊢ _ :: '_" [51,51,51]100)

definition test1 where "test1 = [],Map.empty ⊢ testExpr1 :: _"
definition test2 where "test2 = [], Map.empty  ⊢ testExpr2 :: _"
definition test3 where "test3 = [], Map.empty(''V'' ↦ Integer)  ⊢ testExpr3 :: _"
definition test4 where "test4 = [], Map.empty(''V'' ↦ Integer)  ⊢ testExpr4 :: _"
definition test5 where "test5 = [classObject, (''C'',(''Object'',[(''F'',Integer)],[]))], Map.empty  ⊢ testExpr5 :: _"
definition test6 where "test6 = [classObject, classI], Map.empty  ⊢ testExpr6 :: _"

ML_val ‹
  val SOME(@{code Integer}, _) = Predicate.yield @{code test1};
  val SOME(@{code Integer}, _) = Predicate.yield @{code test2};
  val SOME(@{code Integer}, _) = Predicate.yield @{code test3};
  val SOME(@{code Void}, _) = Predicate.yield @{code test4};
  val SOME(@{code Void}, _) = Predicate.yield @{code test5};
  val SOME(@{code Integer}, _) = Predicate.yield @{code test6};
›

definition testmb_isNull where "testmb_isNull = [classObject, classA], Map.empty([this] [↦] [Class ''A'']) ⊢ mb_isNull :: _"
definition testmb_add where "testmb_add = [classObject, classA], Map.empty([this,''i''] [↦] [Class ''A'',Integer]) ⊢ mb_add :: _"
definition testmb_mult_cond where "testmb_mult_cond = [classObject, classA], Map.empty([this,''j''] [↦] [Class ''A'',Integer]) ⊢ mb_mult_cond :: _"
definition testmb_mult_block where "testmb_mult_block = [classObject, classA], Map.empty([this,''i'',''j'',''temp''] [↦] [Class ''A'',Integer,Integer,Integer]) ⊢ mb_mult_block :: _"
definition testmb_mult where "testmb_mult = [classObject, classA], Map.empty([this,''i'',''j''] [↦] [Class ''A'',Integer,Integer]) ⊢ mb_mult :: _"

ML_val ‹
  val SOME(@{code Boolean}, _) = Predicate.yield @{code testmb_isNull};
  val SOME(@{code Integer}, _) = Predicate.yield @{code testmb_add};
  val SOME(@{code Boolean}, _) = Predicate.yield @{code testmb_mult_cond};
  val SOME(@{code Void}, _) = Predicate.yield @{code testmb_mult_block};
  val SOME(@{code Integer}, _) = Predicate.yield @{code testmb_mult};
›

definition test where "test = [classObject, classA], Map.empty ⊢ testExpr_ClassA :: _"

ML_val ‹
  val SOME(@{code Integer}, _) = Predicate.yield @{code test};
›

end