1 header {* CPS transformation of Danvy and Nielsen *} |
|
2 theory CPS2_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 binds 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> = Lam 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 (eqvt) by lexicographic_order |
|
33 |
|
34 nominal_primrec |
|
35 ccomp :: "cpsctxt => cpsctxt => cpsctxt" |
|
36 where |
|
37 "ccomp Hole C = C" |
|
38 | "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')" |
|
39 | "ccomp (CArg N C) C' = CArg N (ccomp C C')" |
|
40 | "ccomp (CFun C N) C' = CFun (ccomp C C') N" |
|
41 unfolding eqvt_def ccomp_graph_def |
|
42 apply perm_simp |
|
43 apply auto |
|
44 apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) |
|
45 apply (auto simp add: fresh_star_def) |
|
46 apply blast+ |
|
47 apply (erule Abs_lst1_fcb) |
|
48 apply (simp_all add: Abs_fresh_iff) |
|
49 apply (erule fresh_eqvt_at) |
|
50 apply (simp add: finite_supp) |
|
51 apply (simp add: fresh_Pair) |
|
52 apply (simp add: eqvt_at_def swap_fresh_fresh) |
|
53 done |
|
54 |
|
55 termination (eqvt) by lexicographic_order |
|
56 |
|
57 nominal_primrec |
|
58 CPSv :: "lt => lt" |
|
59 and CPS :: "lt => cpsctxt" where |
|
60 "CPSv (Var x) = x~" |
|
61 | "CPS (Var x) = CFun Hole (x~)" |
|
62 | "atom b \<sharp> M \<Longrightarrow> CPSv (Lam y M) = Lam y (Lam b ((CPS M)<Var b>))" |
|
63 | "atom b \<sharp> M \<Longrightarrow> CPS (Lam y M) = CFun Hole (Lam y (Lam b ((CPS M)<Var b>)))" |
|
64 | "CPSv (M $ N) = Lam x (Var x)" |
|
65 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole" |
|
66 | "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<Longrightarrow> CPS (M $ N) = |
|
67 ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))" |
|
68 | "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) = |
|
69 ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))" |
|
70 | "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $ N) = |
|
71 ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $ Var b) Hole))))" |
|
72 apply auto |
|
73 defer |
|
74 apply (case_tac x) |
|
75 apply (rule_tac y="a" in lt.exhaust) |
|
76 apply auto |
|
77 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
|
78 apply (simp add: Abs1_eq_iff) |
|
79 apply blast+ |
|
80 apply (rule_tac y="b" in lt.exhaust) |
|
81 apply auto |
|
82 apply (rule_tac x="lt" and ?'a="name" in obtain_fresh) |
|
83 apply (simp add: Abs1_eq_iff) |
|
84 apply blast |
|
85 apply (rule_tac ?'a="name" in obtain_fresh) |
|
86 apply (rule_tac x="(lt1, lt2, a)" and ?'a="name" in obtain_fresh) |
|
87 apply (simp add: fresh_Pair_elim) |
|
88 apply (case_tac "isValue lt1", case_tac [!] "isValue lt2")[1] |
|
89 apply (simp_all add: fresh_Pair)[4] |
|
90 --"" |
|
91 apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh) |
|
92 apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)") |
|
93 apply (subgoal_tac "Lam ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)") |
|
94 apply (simp only:) |
|
95 apply (erule Abs_lst1_fcb) |
|
96 apply (simp add: Abs_fresh_iff) |
|
97 apply (simp_all add: Abs_fresh_iff lt.fresh fresh_Pair_elim fresh_at_base swap_fresh_fresh)[2] |
|
98 (* need an invariant to get eqvt_at (Proj) *) |
|
99 defer defer |
|
100 apply simp |
|
101 apply (simp_all add: Abs1_eq_iff fresh_Pair_elim fresh_at_base)[2] |
|
102 defer defer |
|
103 defer |
|
104 apply (simp add: Abs1_eq_iff fresh_at_base lt.fresh) |
|
105 apply (rule arg_cong) back |
|
106 defer |
|
107 apply (rule arg_cong) back |
|
108 defer |
|
109 apply (rule arg_cong) back |
|
110 defer |
|
111 oops --"The goals seem reasonable" |
|
112 |
|
113 end |
|