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