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. c⋅a)"

definition
  cont2val :: "'a Cont → 'a" where
  "cont2val ≡ (Λ f. f⋅ID)"

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⋅(Val⋅n) = Just⋅n"
| "eval⋅(Add⋅x⋅y) = mliftM2 (Λ a b. a + b)⋅(eval⋅x)⋅(eval⋅y)"
| "eval⋅Throw = mfail"
| "eval⋅(Catch⋅x⋅y) = mcatch⋅(eval⋅x)⋅(eval⋅y)"

fixrec eval_body :: "(Expr → Nat Maybe) → Expr → Nat Maybe"
where
  "eval_body⋅r⋅(Val⋅n) = Just⋅n"
| "eval_body⋅r⋅(Add⋅x⋅y) = mliftM2 (Λ a b. a + b)⋅(r⋅x)⋅(r⋅y)"
| "eval_body⋅r⋅Throw = mfail"
| "eval_body⋅r⋅(Catch⋅x⋅y) = mcatch⋅(r⋅x)⋅(r⋅y)"

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

lemma eval_eval_body_eq: "eval = fix⋅eval_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 g⋅e of Nothing ⇒ f | Just⋅n ⇒ s⋅n"

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. g⋅e⋅Just⋅Nothing"

lemma wrapC_unwrapC_id: "wrapC oo unwrapC = ID"
proof(intro cfun_eqI)
  fix g e
  show "(wrapC oo unwrapC)⋅g⋅e = ID⋅g⋅e"
    by (cases "g⋅e", 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 ≡ wrapC⋅eval_work"

fixrec eval_body' :: "(Expr → (Nat → Nat Maybe) → Nat Maybe → Nat Maybe)
                    → Expr → (Nat → Nat Maybe) → Nat Maybe → Nat Maybe"
where
  "eval_body'⋅r⋅(Val⋅n)⋅s⋅f = s⋅n"
| "eval_body'⋅r⋅(Add⋅x⋅y)⋅s⋅f = (case wrapC⋅r⋅x of
                                     Nothing ⇒ f
                                   | Just⋅n ⇒ (case wrapC⋅r⋅y of
                                                    Nothing ⇒ f
                                                  | Just⋅m ⇒ s⋅(n + m)))"
| "eval_body'⋅r⋅Throw⋅s⋅f = f"
| "eval_body'⋅r⋅(Catch⋅x⋅y)⋅s⋅f = (case wrapC⋅r⋅x of
                                       Nothing ⇒ (case wrapC⋅r⋅y of
                                                      Nothing ⇒ f
                                                    | Just⋅n ⇒ s⋅n)
                                     | Just⋅n ⇒ s⋅n)"

lemma eval_body'_strictExpr[simp]: "eval_body'⋅r⋅⊥⋅s⋅f = ⊥"
  by (subst eval_body'.unfold, simp)

definition
  eval_work' :: "Expr → (Nat → Nat Maybe) → Nat Maybe → Nat Maybe" where
  "eval_work' ≡ fix⋅eval_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 "x⋅Expr1⋅Just⋅Nothing")
     apply simp_all
    apply (case_tac "x⋅Expr2⋅Just⋅Nothing")
     apply simp_all
   apply (simp add: mfail_def)
  apply (simp add: mcatch_def wrapC_def)
  apply (case_tac "x⋅Expr1⋅Just⋅Nothing")
   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_final⋅r⋅(Val⋅n)⋅s⋅f = s⋅n"
| "eval_body_final⋅r⋅(Add⋅x⋅y)⋅s⋅f = r⋅x⋅(Λ n. r⋅y⋅(Λ m. s⋅(n + m))⋅f)⋅f"
| "eval_body_final⋅r⋅Throw⋅s⋅f = f"
| "eval_body_final⋅r⋅(Catch⋅x⋅y)⋅s⋅f = r⋅x⋅s⋅(r⋅y⋅s⋅f)"

lemma eval_body_final_strictExpr[simp]: "eval_body_final⋅r⋅⊥⋅s⋅f = ⊥"
  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 ≡ fix⋅eval_body_final"

definition
  eval_final :: "Expr → Nat Maybe" where
  "eval_final ≡ (Λ e. eval_work_final⋅e⋅Just⋅Nothing)"

lemma "eval = eval_final"
proof -
  have "eval = fix⋅eval_body" by (rule eval_eval_body_eq)
  also from wrapC_unwrapC_id unwrapC_strict have "… = wrapC⋅(fix⋅eval_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
(*>*)