Theory bpel_translator

(*
Created by Yongwang Zhao (zhaoyw@buaa.edu.cn)
School of Computer Science & Engineering, Beihang University, China
*)

section ‹Compiling BPEL v2.0 language into Picore›

theory bpel_translator
imports "../../adapter_SIMP/picore_SIMP_Syntax" bpel_ast
begin

primrec NEXTs :: "nat ⇒ (string, 'k, ('s,'l) State, (('s,'l) State com) option) esys
                      ⇒ (string, 'k, ('s,'l) State, (('s,'l) State com) option) esys"
where "NEXTs 0 P = P" |
      "NEXTs (Suc n) P = P NEXT (NEXTs n P)"

datatype ('s,'l) EventLabel = ActL "('s,'l) Activity" | EvtHdlL "('s,'l) EventHandler"

fun compile :: "('s,'l) Activity ⇒ (('s,'l) EventLabel, 'k, ('s,'l) State, (('s,'l) State com) option) esys" and
    compile_eh :: "('s,'l) EventHandler ⇒ (('s,'l) EventLabel, 'k, ('s,'l) State, (('s,'l) State com) option) esys"
    where
(*
three cases to simulate Invoke:
(1) invoke remote services successfully
(2) exception occurs and be caught
(3) exception occurs and but not be caught
However, we assume that exceptions will be caught.
 *)
"compile (Invoke fls ptl ptt opn spc cts cta) =
  (if cta = None ∧ cts = [] then
     EVENT⇩A (ActL (Invoke fls ptl ptt opn spc cts cta))
      WHEN (´(λs. targets_sat (targets fls) s))
      THEN
        (Basic spc);;
        (Basic (λs. fire_sources (sources fls) s))
      END
   else
     (EVENT⇩A (ActL (Invoke fls ptl ptt opn spc cts cta))
      WHEN (´(λs. targets_sat (targets fls) s))
      THEN
        (Basic spc);;
        (Basic (λs. fire_sources (sources fls) s))
      END) OR
     ( OR_list (
        if cta ≠ None then
          ((EVENT⇩A (ActL (Invoke fls ptl ptt opn spc cts cta))
            WHEN (´(λs. targets_sat (targets fls) s))
            THEN
              (Basic (λs. fire_sources (sources fls) s))
            END) NEXT compile (the cta))#(map (ESeq (EVENT⇩A (ActL (Invoke fls ptl ptt opn spc cts cta))
                                                      WHEN (´(λs. targets_sat (targets fls) s))
                                                      THEN
                                                        (Basic (λs. fire_sources (sources fls) s))
                                                      END) ∘ compile) (map snd cts))
        else
          (map (ESeq (EVENT⇩A (ActL (Invoke fls ptl ptt opn spc cts cta))
                        WHEN (´(λs. targets_sat (targets fls) s))
                        THEN
                          (Basic (λs. fire_sources (sources fls) s))
                        END) ∘ compile) (map snd cts))) )
  )" |

"compile (Receive fls ptl ptt opn spc) =
    EVENT⇩A (ActL (Receive fls ptl ptt opn spc))
    WHEN (´(λs. targets_sat (targets fls) s))
    THEN
      (Basic spc);;
      (Basic (λs. fire_sources (sources fls) s))
    END" |
"compile (Reply fls ptl ptt opn)  =
    EVENT⇩A (ActL (Reply fls ptl ptt opn))
    WHEN (´(λs. targets_sat (targets fls) s))
    THEN
      (Basic (λs. fire_sources (sources fls) s))
    END" |
"compile (Assign fls spc) =
    EVENT⇩A (ActL (Assign fls spc))
    WHEN (´(λs. targets_sat (targets fls) s))
    THEN
      (Basic spc);;
      (Basic (λs. fire_sources (sources fls) s))
    END" |
"compile (Wait fls t)  =
    EVENT⇩A (ActL (Wait fls t))
    WHEN t > ´tick ∧ (´(λs. targets_sat (targets fls) s))
    THEN
      (Basic (λs. fire_sources (sources fls) s))
    END" |
"compile (Empty fls)  =
    EVENT⇩A (ActL (Empty fls))
    WHEN (´(λs. targets_sat (targets fls) s))
    THEN
      (Basic (λs. fire_sources (sources fls) s))
    END" |
"compile (Seqb p1 p2)  = (compile p1) NEXT (compile p2)" |
"compile (If c p1 p2) =
    ((EVENT⇩A (ActL (If c p1 p2)) WHEN (´(λs. s∈c)) THEN SKIP END) NEXT (compile p1))
    OR
    ((EVENT⇩A (ActL (If c p1 p2)) WHEN (´(λs. s∉c)) THEN SKIP END) NEXT (compile p2))" |
"compile (While c p)  =
    (EWhile c (compile p) )" |
"compile (Pick a b) = (compile_eh a) OR (compile_eh b)" |
"compile (Flow a b) = (compile a) ⋈ (compile b)" |
"compile (ActTerminator) = fin" |
"compile_eh (OnMessage ptl ptt opn spc at) =
  (EVENT⇩A (EvtHdlL (OnMessage ptl ptt opn spc at)) WHEN True THEN (Basic spc) END) NEXT (compile at)" |
"compile_eh (OnAlarm t at) = (EVENT⇩A (EvtHdlL (OnAlarm t at)) WHEN t > ´tick THEN SKIP END) NEXT (compile at)"

thm OR_list.simps
thm AND_list.simps

lemma inj_compile_eh: "compile_eh a = compile_eh b ⟹ a = b"
  apply(induct a) apply simp+
    apply(induct b) apply simp+
  apply(induct b) apply simp+
  done

lemma OR_eq: "x OR y = a OR b ⟹ x = a ∧ y = b"
  by simp

lemma comp_pick_eq: "compile (Pick a b) = compile (Pick x y) ⟹ a = x ∧ b = y" (*Pick x = Pick y*)
  apply(induct a arbitrary: b x y) apply simp+
  subgoal for x1 x2 x3 x4 x5 b x y apply(induct x) apply simp+ using inj_compile_eh apply blast by auto
  subgoal for x1 x2 b x y apply auto apply(induct x) apply simp+ using inj_compile_eh by blast
  done

lemma comp_eq_pick: "compile (Pick x y) = compile b ⟹ Pick x y = b"
  apply(induct x) apply simp+
    apply(induct b) apply simp_all
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    using inj_compile_eh apply auto[1]
    apply(induct b) apply simp_all
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    using inj_compile_eh apply auto[1]
  done

(*
lemma comp_eq_flow:
  "(⋀b2. compile a = compile b2 ⟹ a = b2) ⟹
   (⋀b2. compile b = compile b2 ⟹ b = b2) ⟹
   compile (Flow a b) = compile c ⟹ Flow a b = c"
  apply auto apply(induct c) apply(case_tac "x6 = [] ∧ x7 = None") by auto
*)

lemma compile_inj: "compile b1 = compile b2 ⟹ b1 = b2"
  apply(induct b1 arbitrary:b2)
  prefer 14 apply simp prefer 13 apply simp

  (* Invoke *)
  subgoal for x1 x2 x3 x4 x5 x6 x7 b2 apply(induct b2)
    prefer 14 apply simp prefer 13 apply simp
    subgoal for y1 y2 y3 y4 y5 y6 y7
      apply(case_tac "x6 = [] ∧ x7 = None")
       apply(case_tac "y6 = [] ∧ y7 = None") apply simp apply auto[1]
      apply(case_tac "y6 = [] ∧ y7 = None") apply force by auto[1]

    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp
      subgoal for x y apply(induct x) apply simp+
        apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
        apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1] done
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
  done

  (* Receive *)
  subgoal for x1 x2 x3 x4 x5 b2 apply(induct b2)
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1] by simp+

  (* Reply *)
  subgoal for x1 x2 x3 x4 b2 apply(induct b2)
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1] by simp+

  (* Assign *)
  subgoal for x1 x2 b2 apply(induct b2)
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1] by simp+

  (* Wait *)
  subgoal for x1 x2 b2 apply(induct b2)
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1] by simp+

  (* Empty *)
  subgoal for x b2 apply(induct b2)
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1] by simp+

  (* Seq *)
  subgoal for x y b apply(induct b)
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1] by simp+

  (* If *)
  subgoal for x y p b apply(induct b) apply simp_all
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
    subgoal for x1 x2 apply(induct x1)
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1] by simp+
    done

  (* While *)
  subgoal for x y b apply(induct b)
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1] by simp+

  (* Pick *)
  using comp_eq_pick apply auto[1]

  (* Flow *)
  subgoal for a b c
    apply auto apply(induct c) apply(case_tac "x6 = [] ∧ x7 = None") by auto

  (* ActTerminator *)
  subgoal for b apply(induct b) apply simp_all
    apply(case_tac "x6 = [] ∧ x7 = None") apply simp apply auto[1]
  done
  done

definition "Tick ≡ EVENT⇩A (ActL ActTerminator) WHEN True THEN ´tick := ´tick + 1 END"

datatype sys = T | BPEL

definition BPELProc2PiCore :: "('s,'l) BPELProc ⇒ (('s,'l) EventLabel, sys, ('s,'l) State, (('s,'l) State com) option) paresys"
where "BPELProc2PiCore bpel ≡ (λk. case k of T ⇒ (EWhile ⦃True⦄ Tick) | BPEL ⇒ compile bpel)"

end