Theory execute_Bigstep

(*  Title:      Jinja/J/execute_Bigstep.thy
    Author:     Tobias Nipkow
    Copyright   2004 Technische Universitaet Muenchen
*)

section ‹Code Generation For BigStep›

theory execute_Bigstep
imports
  BigStep Examples
  "HOL-Library.Code_Target_Numeral"
begin

inductive map_val :: "expr list  val list  bool"
where
  Nil: "map_val [] []"
| Cons: "map_val xs ys  map_val (Val y # xs) (y # ys)"

inductive map_val2 :: "expr list  val list  expr list  bool"
where
  Nil: "map_val2 [] [] []"
| Cons: "map_val2 xs ys zs  map_val2 (Val y # xs) (y # ys) zs"
| Throw: "map_val2 (throw e # xs) [] (throw e # xs)"

theorem map_val_conv: "(xs = map Val ys) = map_val xs ys"
(*<*)
proof -
  have "ys. xs = map Val ys  map_val xs ys"
    apply (induct xs type:list)
    apply (case_tac ys)
    apply simp
    apply (rule map_val.Nil)
    apply simp
    apply (case_tac ys)
    apply simp
    apply simp
    apply (rule map_val.Cons)
    apply simp
    done
  moreover have "map_val xs ys  xs = map Val ys"
    by (erule map_val.induct) simp+
  ultimately show ?thesis ..
qed
(*>*)

theorem map_val2_conv:
 "(xs = map Val ys @ throw e # zs) = map_val2 xs ys (throw e # zs)"
(*<*)
proof -
  have "ys. xs = map Val ys @ throw e # zs  map_val2 xs ys (throw e # zs)"
    apply (induct xs type:list)
    apply (case_tac ys)
    apply simp
    apply simp
    apply simp
    apply (case_tac ys)
    apply simp
    apply (rule map_val2.Throw)
    apply simp
    apply (rule map_val2.Cons)
    apply simp
    done
  moreover have "map_val2 xs ys (throw e # zs)  xs = map Val ys @ throw e # zs"
    by (erule map_val2.induct) simp+
  ultimately show ?thesis ..
qed
(*>*)

lemma CallNull2:
  " P  e,s0  null,s1;  P  ps,s1 [⇒] evs,s2; map_val evs vs 
   P  eM(ps),s0  THROW NullPointer,s2"
apply(rule CallNull, assumption+)
apply(simp add: map_val_conv[symmetric])
done


lemma CallParamsThrow2:
  " P  e,s0  Val v,s1; P  es,s1 [⇒] evs,s2;
     map_val2 evs vs (throw ex # es'') 
    P  eM(es),s0  throw ex,s2"
apply(rule eval_evals.CallParamsThrow, assumption+)
apply(simp add: map_val2_conv[symmetric])
done

lemma Call2:
  " P  e,s0  addr a,s1;  P  ps,s1 [⇒] evs,(h2,l2);
     map_val evs vs;
     h2 a = Some(C,fs);  P  C sees M:TsT = (pns,body) in D;
     length vs = length pns;  l2' = [thisAddr a, pns[↦]vs];
     P  body,(h2,l2')  e',(h3,l3) 
   P  eM(ps),s0  e',(h3,l2)"
apply(rule Call, assumption+)
apply(simp add: map_val_conv[symmetric])
apply assumption+
done

code_pred 
  (modes: i ⇒ o ⇒ bool)
  map_val 
.

code_pred
  (modes: i ⇒ o ⇒ o ⇒ bool)
  map_val2
.

lemmas [code_pred_intro] =
 eval_evals.New eval_evals.NewFail
 eval_evals.Cast eval_evals.CastNull eval_evals.CastFail eval_evals.CastThrow
 eval_evals.Val eval_evals.Var
 eval_evals.BinOp eval_evals.BinOpThrow1 eval_evals.BinOpThrow2
 eval_evals.LAss eval_evals.LAssThrow
 eval_evals.FAcc eval_evals.FAccNull eval_evals.FAccThrow
 eval_evals.FAss eval_evals.FAssNull
 eval_evals.FAssThrow1 eval_evals.FAssThrow2
 eval_evals.CallObjThrow

declare CallNull2 [code_pred_intro CallNull2]
declare CallParamsThrow2 [code_pred_intro CallParamsThrow2]
declare Call2 [code_pred_intro Call2]

lemmas [code_pred_intro] =
 eval_evals.Block
 eval_evals.Seq eval_evals.SeqThrow
 eval_evals.CondT eval_evals.CondF eval_evals.CondThrow
 eval_evals.WhileF eval_evals.WhileT
 eval_evals.WhileCondThrow

declare eval_evals.WhileBodyThrow [code_pred_intro WhileBodyThrow2]

lemmas [code_pred_intro] =
 eval_evals.Throw eval_evals.ThrowNull
 eval_evals.ThrowThrow
 eval_evals.Try eval_evals.TryCatch eval_evals.TryThrow
 eval_evals.Nil eval_evals.Cons eval_evals.ConsThrow

code_pred
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool as execute)
  eval
proof -
  case eval
  from eval.prems show thesis
  proof(cases (no_simp))
    case CallNull thus ?thesis
      by(rule eval.CallNull2[OF refl])(simp add: map_val_conv[symmetric])
  next
    case CallParamsThrow thus ?thesis
      by(rule eval.CallParamsThrow2[OF refl])(simp add: map_val2_conv[symmetric])
  next
    case Call thus ?thesis
      by -(rule eval.Call2[OF refl], simp_all add: map_val_conv[symmetric])
  next
    case WhileBodyThrow thus ?thesis by(rule eval.WhileBodyThrow2[OF refl])
  qed(assumption|erule (4) eval.that[OF refl]|erule (3) eval.that[OF refl])+
next
  case evals
  from evals.prems show thesis
    by(cases (no_simp))(assumption|erule (3) evals.that[OF refl])+
qed

notation execute ("_  ((1_,/_) / ⟨'_, '_⟩)" [51,0,0] 81)

definition "test1 = []  testExpr1,(Map.empty,Map.empty)  ⟨_,_⟩"
definition "test2 = []  testExpr2,(Map.empty,Map.empty)  ⟨_,_⟩"
definition "test3 = []  testExpr3,(Map.empty,Map.empty(''V''Intg 77))  ⟨_,_⟩"
definition "test4 = []  testExpr4,(Map.empty,Map.empty)  ⟨_,_⟩"
definition "test5 = [(''Object'',('''',[],[])),(''C'',(''Object'',[(''F'',Integer)],[]))]  testExpr5,(Map.empty,Map.empty)  ⟨_,_⟩"
definition "test6 = [(''Object'',('''',[],[])), classI]  testExpr6,(Map.empty,Map.empty)  ⟨_,_⟩"

definition "V = ''V''"
definition "C = ''C''"
definition "F = ''F''"

ML_val val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 5)), _), _) = Predicate.yield @{code test1};
  val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 11)), _), _) = Predicate.yield @{code test2};
  val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 83)), _), _) = Predicate.yield @{code test3};

  val SOME ((_, (_, l)), _) = Predicate.yield @{code test4};
  val SOME (@{code Intg} (@{code int_of_integer} 6)) = l @{code V};

  val SOME ((_, (h, _)), _) = Predicate.yield @{code test5};
  val SOME (c, fs) = h (@{code nat_of_integer} 1);
  val SOME (obj, _) = h (@{code nat_of_integer} 0);
  val SOME (@{code Intg} i) = fs (@{code F}, @{code C});
  @{assert} (c = @{code C} andalso obj = @{code Object} andalso i = @{code int_of_integer} 42);

  val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 160)), _), _) = Predicate.yield @{code test6};

definition "test7 = [classObject, classL]  testExpr_BuildList, (Map.empty,Map.empty)  ⟨_,_⟩"

definition "L = ''L''"
definition "N = ''N''"

ML_val val SOME ((_, (h, _)), _) = Predicate.yield @{code test7};
  val SOME (_, fs1) = h (@{code nat_of_integer} 0);
  val SOME (_, fs2) = h (@{code nat_of_integer} 1);
  val SOME (_, fs3) = h (@{code nat_of_integer} 2);
  val SOME (_, fs4) = h (@{code nat_of_integer} 3);

  val F = @{code "F"};
  val L = @{code "L"};
  val N = @{code "N"};

  @{assert} (fs1 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 1)) andalso
     fs1 (N, L) = SOME (@{code Addr} (@{code nat_of_integer} 1)) andalso
     fs2 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 2)) andalso
     fs2 (N, L) = SOME (@{code Addr} (@{code nat_of_integer} 2)) andalso
     fs3 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 3)) andalso
     fs3 (N, L) = SOME (@{code Addr} (@{code nat_of_integer} 3)) andalso
     fs4 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 4)) andalso
     fs4 (N, L) = SOME @{code Null});

definition "test8 = [classObject, classA]  testExpr_ClassA, (Map.empty,Map.empty)  ⟨_,_⟩"
definition "i = ''int''"
definition "t = ''test''"
definition "A = ''A''"

ML_val val SOME ((_, (h, l)), _) = Predicate.yield @{code test8};
  val SOME (_, fs1) = h (@{code nat_of_integer} 0);
  val SOME (_, fs2) = h (@{code nat_of_integer} 1);

  val i = @{code "i"};
  val t = @{code "t"};
  val A = @{code "A"};

  @{assert} (fs1 (i, A) = SOME (@{code Intg} (@{code int_of_integer} 10)) andalso 
     fs1 (t, A) = SOME @{code Null} andalso
     fs2 (i, A) = SOME (@{code Intg} (@{code int_of_integer} 50)) andalso 
     fs2 (t, A) = SOME @{code Null});

end