Theory Continuations

(*<*)
(*
 * The worker/wrapper transformation, following Gill and Hutton.
 * (C)opyright 2009-2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Continuations
imports
  HOLCF
  Maybe
  Nats
  WorkerWrapperNew
begin
(*>*)

section‹Tagless interpreter via double-barreled continuations›

text‹\label{sec:continuations}›

type_synonym 'a Cont = "('a  'a)  'a"

definition
  val2cont :: "'a  'a Cont" where
  "val2cont  (Λ a c. ca)"

definition
  cont2val :: "'a Cont  'a" where
  "cont2val  (Λ f. fID)"

lemma cont2val_val2cont_id: "cont2val oo val2cont = ID"
  by (rule cfun_eqI, simp add: val2cont_def cont2val_def)

domain Expr =
    Val (lazy val::"Nat")
  | Add (lazy addl::"Expr") (lazy addr::"Expr")
  | Throw
  | Catch (lazy cbody::"Expr") (lazy chandler::"Expr")

fixrec eval :: "Expr  Nat Maybe"
where
  "eval(Valn) = Justn"
| "eval(Addxy) = mliftM2 (Λ a b. a + b)(evalx)(evaly)"
| "evalThrow = mfail"
| "eval(Catchxy) = mcatch(evalx)(evaly)"

fixrec eval_body :: "(Expr  Nat Maybe)  Expr  Nat Maybe"
where
  "eval_bodyr(Valn) = Justn"
| "eval_bodyr(Addxy) = mliftM2 (Λ a b. a + b)(rx)(ry)"
| "eval_bodyrThrow = mfail"
| "eval_bodyr(Catchxy) = mcatch(rx)(ry)"

lemma eval_body_strictExpr[simp]: "eval_bodyr = "
  by (subst eval_body.unfold, simp)

lemma eval_eval_body_eq: "eval = fixeval_body"
  by (rule cfun_eqI, subst eval_def, subst eval_body.unfold, simp)

subsection‹Worker/wrapper›

definition
  unwrapC :: "(Expr  Nat Maybe)  (Expr  (Nat  Nat Maybe)  Nat Maybe  Nat Maybe)" where
  "unwrapC  Λ g e s f. case ge of Nothing  f | Justn  sn"

lemma unwrapC_strict[simp]: "unwrapC = "
  unfolding unwrapC_def by (rule cfun_eqI)+ simp

definition
  wrapC :: "(Expr  (Nat  Nat Maybe)  Nat Maybe  Nat Maybe)  (Expr  Nat Maybe)" where
  "wrapC  Λ g e. geJustNothing"

lemma wrapC_unwrapC_id: "wrapC oo unwrapC = ID"
proof(intro cfun_eqI)
  fix g e
  show "(wrapC oo unwrapC)ge = IDge"
    by (cases "ge", simp_all add: wrapC_def unwrapC_def)
qed

definition
  eval_work :: "Expr  (Nat  Nat Maybe)  Nat Maybe  Nat Maybe" where
  "eval_work  fix(unwrapC oo eval_body oo wrapC)"

definition
  eval_wrap :: "Expr  Nat Maybe" where
  "eval_wrap  wrapCeval_work"

fixrec eval_body' :: "(Expr  (Nat  Nat Maybe)  Nat Maybe  Nat Maybe)
                     Expr  (Nat  Nat Maybe)  Nat Maybe  Nat Maybe"
where
  "eval_body'r(Valn)sf = sn"
| "eval_body'r(Addxy)sf = (case wrapCrx of
                                     Nothing  f
                                   | Justn  (case wrapCry of
                                                    Nothing  f
                                                  | Justm  s(n + m)))"
| "eval_body'rThrowsf = f"
| "eval_body'r(Catchxy)sf = (case wrapCrx of
                                       Nothing  (case wrapCry of
                                                      Nothing  f
                                                    | Justn  sn)
                                     | Justn  sn)"

lemma eval_body'_strictExpr[simp]: "eval_body'rsf = "
  by (subst eval_body'.unfold, simp)

definition
  eval_work' :: "Expr  (Nat  Nat Maybe)  Nat Maybe  Nat Maybe" where
  "eval_work'  fixeval_body'"

text‹This proof is unfortunately quite messy, due to the
simplifier's inability to cope with HOLCF's case distinctions.›

lemma eval_body'_eval_body_eq: "eval_body' = unwrapC oo eval_body oo wrapC"
  apply (intro cfun_eqI)
  apply (unfold unwrapC_def wrapC_def)
  apply (case_tac xa)
      apply simp_all
    apply (simp add: wrapC_def)
    apply (case_tac "xExpr1JustNothing")
     apply simp_all
    apply (case_tac "xExpr2JustNothing")
     apply simp_all
   apply (simp add: mfail_def)
  apply (simp add: mcatch_def wrapC_def)
  apply (case_tac "xExpr1JustNothing")
   apply simp_all
  done

fixrec eval_body_final :: "(Expr  (Nat  Nat Maybe)  Nat Maybe  Nat Maybe)
                          Expr  (Nat  Nat Maybe)  Nat Maybe  Nat Maybe"
where
  "eval_body_finalr(Valn)sf = sn"
| "eval_body_finalr(Addxy)sf = rx(Λ n. ry(Λ m. s(n + m))f)f"
| "eval_body_finalrThrowsf = f"
| "eval_body_finalr(Catchxy)sf = rxs(rysf)"

lemma eval_body_final_strictExpr[simp]: "eval_body_finalrsf = "
  by (subst eval_body_final.unfold, simp)

lemma eval_body'_eval_body_final_eq: "eval_body_final oo unwrapC oo wrapC = eval_body'"
  apply (rule cfun_eqI)+
  apply (case_tac xa)
     apply (simp_all add: unwrapC_def)
  done

definition
  eval_work_final :: "Expr  (Nat  Nat Maybe)  Nat Maybe  Nat Maybe" where
  "eval_work_final  fixeval_body_final"

definition
  eval_final :: "Expr  Nat Maybe" where
  "eval_final  (Λ e. eval_work_finaleJustNothing)"

lemma "eval = eval_final"
proof -
  have "eval = fixeval_body" by (rule eval_eval_body_eq)
  also from wrapC_unwrapC_id unwrapC_strict have " = wrapC(fixeval_body_final)"
    apply (rule worker_wrapper_fusion_new)
    using eval_body'_eval_body_final_eq eval_body'_eval_body_eq by simp
  also have " = eval_final"
    unfolding eval_final_def eval_work_final_def wrapC_def
    by simp
  finally show ?thesis .
qed

(*<*)
end
(*>*)