1 header {* CPS transformation of Danvy and Nielsen *}

     2 theory DanvyNielsen

     3 imports Lt

     4 begin

     5 

     6 nominal_datatype cpsctxt =

     7   Hole

     8 | CFun cpsctxt lt

     9 | CArg lt cpsctxt

    10 | CAbs x::name c::cpsctxt bind x in c

    11 

    12 nominal_primrec

    13   fill   :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt"         ("_<_>" [200, 200] 100)

    14 where

    15   fill_hole : "Hole<M> = M"

    16 | fill_fun  : "(CFun C N)<M> = (C<M>) $ N"

    17 | fill_arg  : "(CArg N C)<M> = N $ (C<M>)"

    18 | fill_abs  : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Abs x (C<M>)"

    19   unfolding eqvt_def fill_graph_def

    20   apply perm_simp

    21   apply auto

    22   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)

    23   apply (auto simp add: fresh_star_def)

    24   apply (erule Abs_lst1_fcb)

    25   apply (simp_all add: Abs_fresh_iff)

    26   apply (erule fresh_eqvt_at)

    27   apply (simp add: finite_supp)

    28   apply (simp add: fresh_Pair)

    29   apply (simp add: eqvt_at_def swap_fresh_fresh)

    30   done

    31 

    32 termination

    33   by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)

    34 

    35 lemma [eqvt]: "p \<bullet> fill c t = fill (p \<bullet> c) (p \<bullet> t)"

    36   by (nominal_induct c avoiding: t rule: cpsctxt.strong_induct) simp_all

    37 

    38 nominal_primrec

    39   ccomp :: "cpsctxt => cpsctxt => cpsctxt"

    40 where

    41   "ccomp Hole C  = C"

    42 | "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')"

    43 | "ccomp (CArg N C) C' = CArg N (ccomp C C')"

    44 | "ccomp (CFun C N) C'  = CFun (ccomp C C') N"

    45   unfolding eqvt_def ccomp_graph_def

    46   apply perm_simp

    47   apply auto

    48   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)

    49   apply (auto simp add: fresh_star_def)

    50   apply blast+

    51   apply (erule Abs_lst1_fcb)

    52   apply (simp_all add: Abs_fresh_iff)

    53   apply (erule fresh_eqvt_at)

    54   apply (simp add: finite_supp)

    55   apply (simp add: fresh_Pair)

    56   apply (simp add: eqvt_at_def swap_fresh_fresh)

    57   done

    58 

    59 termination

    60   by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)

    61 

    62 lemma [eqvt]: "p \<bullet> ccomp c c' = ccomp (p \<bullet> c) (p \<bullet> c')"

    63   by (nominal_induct c avoiding: c' rule: cpsctxt.strong_induct) simp_all

    64 

    65 nominal_primrec

    66     CPSv :: "lt => lt"

    67 and CPS :: "lt => cpsctxt" where

    68   "CPSv (Var x) = x~"

    69 | "CPS (Var x) = CFun Hole (x~)"

    70 | "atom b \<sharp> M \<Longrightarrow> CPSv (Abs y M) = Abs y (Abs b ((CPS M)<Var b>))"

    71 | "atom b \<sharp> M \<Longrightarrow> CPS (Abs y M) = CFun Hole (Abs y (Abs b ((CPS M)<Var b>)))"

    72 | "CPSv (M $ N) = Abs x (Var x)"

    73 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole"

    74 | "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) =

    75      ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))"

    76 | "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) =

    77      ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))"

    78 | "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $ N) =

    79      ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $ Var b) Hole))))"

    80   apply auto

    81   oops --"The goals seem reasonable"

    82 

    83 end