16 (** parse translation **) |
16 (** parse translation **) |
17 |
17 |
18 local |
18 local |
19 |
19 |
20 fun idt_name (Free (x, _)) = SOME x |
20 fun idt_name (Free (x, _)) = SOME x |
21 | idt_name (Const (@{syntax_const "_constrain"}, _) $ t $ _) = idt_name t |
21 | idt_name (Const (\<^syntax_const>\<open>_constrain\<close>, _) $ t $ _) = idt_name t |
22 | idt_name _ = NONE; |
22 | idt_name _ = NONE; |
23 |
23 |
24 fun eq_idt tu = |
24 fun eq_idt tu = |
25 (case apply2 idt_name tu of |
25 (case apply2 idt_name tu of |
26 (SOME x, SOME y) => x = y |
26 (SOME x, SOME y) => x = y |
27 | _ => false); |
27 | _ => false); |
28 |
28 |
29 fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body] |
29 fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body] |
30 | mk_abstuple (x :: xs) body = |
30 | mk_abstuple (x :: xs) body = |
31 Syntax.const @{const_syntax case_prod} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body]; |
31 Syntax.const \<^const_syntax>\<open>case_prod\<close> $ Syntax_Trans.abs_tr [x, mk_abstuple xs body]; |
32 |
32 |
33 fun mk_fbody x e [y] = if eq_idt (x, y) then e else y |
33 fun mk_fbody x e [y] = if eq_idt (x, y) then e else y |
34 | mk_fbody x e (y :: xs) = |
34 | mk_fbody x e (y :: xs) = |
35 Syntax.const @{const_syntax Pair} $ |
35 Syntax.const \<^const_syntax>\<open>Pair\<close> $ |
36 (if eq_idt (x, y) then e else y) $ mk_fbody x e xs; |
36 (if eq_idt (x, y) then e else y) $ mk_fbody x e xs; |
37 |
37 |
38 fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs); |
38 fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs); |
39 |
39 |
40 |
40 |
41 (* bexp_tr & assn_tr *) |
41 (* bexp_tr & assn_tr *) |
42 (*all meta-variables for bexp except for TRUE are translated as if they |
42 (*all meta-variables for bexp except for TRUE are translated as if they |
43 were boolean expressions*) |
43 were boolean expressions*) |
44 |
44 |
45 fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE" (* FIXME !? *) |
45 fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE" (* FIXME !? *) |
46 | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b; |
46 | bexp_tr b xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs b; |
47 |
47 |
48 fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r; |
48 fun assn_tr r xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs r; |
49 |
49 |
50 |
50 |
51 (* com_tr *) |
51 (* com_tr *) |
52 |
52 |
53 fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs = |
53 fun com_tr (Const (\<^syntax_const>\<open>_assign\<close>, _) $ x $ e) xs = |
54 Syntax.const @{const_syntax Basic} $ mk_fexp x e xs |
54 Syntax.const \<^const_syntax>\<open>Basic\<close> $ mk_fexp x e xs |
55 | com_tr (Const (@{const_syntax Basic},_) $ f) _ = Syntax.const @{const_syntax Basic} $ f |
55 | com_tr (Const (\<^const_syntax>\<open>Basic\<close>,_) $ f) _ = Syntax.const \<^const_syntax>\<open>Basic\<close> $ f |
56 | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs = |
56 | com_tr (Const (\<^const_syntax>\<open>Seq\<close>,_) $ c1 $ c2) xs = |
57 Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs |
57 Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr c1 xs $ com_tr c2 xs |
58 | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs = |
58 | com_tr (Const (\<^const_syntax>\<open>Cond\<close>,_) $ b $ c1 $ c2) xs = |
59 Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs |
59 Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs |
60 | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs = |
60 | com_tr (Const (\<^const_syntax>\<open>While\<close>,_) $ b $ I $ c) xs = |
61 Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs |
61 Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs |
62 | com_tr t _ = t; |
62 | com_tr t _ = t; |
63 |
63 |
64 fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars |
64 fun vars_tr (Const (\<^syntax_const>\<open>_idts\<close>, _) $ idt $ vars) = idt :: vars_tr vars |
65 | vars_tr t = [t]; |
65 | vars_tr t = [t]; |
66 |
66 |
67 in |
67 in |
68 |
68 |
69 fun hoare_vars_tr [vars, pre, prg, post] = |
69 fun hoare_vars_tr [vars, pre, prg, post] = |
70 let val xs = vars_tr vars |
70 let val xs = vars_tr vars |
71 in Syntax.const @{const_syntax Valid} $ |
71 in Syntax.const \<^const_syntax>\<open>Valid\<close> $ |
72 assn_tr pre xs $ com_tr prg xs $ assn_tr post xs |
72 assn_tr pre xs $ com_tr prg xs $ assn_tr post xs |
73 end |
73 end |
74 | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); |
74 | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); |
75 |
75 |
76 end; |
76 end; |
80 (** print translation **) |
80 (** print translation **) |
81 |
81 |
82 local |
82 local |
83 |
83 |
84 fun dest_abstuple |
84 fun dest_abstuple |
85 (Const (@{const_syntax case_prod}, _) $ Abs (v, _, body)) = |
85 (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (v, _, body)) = |
86 subst_bound (Syntax.free v, dest_abstuple body) |
86 subst_bound (Syntax.free v, dest_abstuple body) |
87 | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body) |
87 | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body) |
88 | dest_abstuple tm = tm; |
88 | dest_abstuple tm = tm; |
89 |
89 |
90 fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t |
90 fun abs2list (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t |
91 | abs2list (Abs (x, T, _)) = [Free (x, T)] |
91 | abs2list (Abs (x, T, _)) = [Free (x, T)] |
92 | abs2list _ = []; |
92 | abs2list _ = []; |
93 |
93 |
94 fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (_, _, t)) = mk_ts t |
94 fun mk_ts (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (_, _, t)) = mk_ts t |
95 | mk_ts (Abs (_, _, t)) = mk_ts t |
95 | mk_ts (Abs (_, _, t)) = mk_ts t |
96 | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b |
96 | mk_ts (Const (\<^const_syntax>\<open>Pair\<close>, _) $ a $ b) = a :: mk_ts b |
97 | mk_ts t = [t]; |
97 | mk_ts t = [t]; |
98 |
98 |
99 fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) = |
99 fun mk_vts (Const (\<^const_syntax>\<open>case_prod\<close>,_) $ Abs (x, _, t)) = |
100 (Syntax.free x :: abs2list t, mk_ts t) |
100 (Syntax.free x :: abs2list t, mk_ts t) |
101 | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t]) |
101 | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t]) |
102 | mk_vts _ = raise Match; |
102 | mk_vts _ = raise Match; |
103 |
103 |
104 fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) (* FIXME no_ch!? *) |
104 fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) (* FIXME no_ch!? *) |
105 | find_ch ((v, t) :: vts) i xs = |
105 | find_ch ((v, t) :: vts) i xs = |
106 if t = Bound i then find_ch vts (i - 1) xs |
106 if t = Bound i then find_ch vts (i - 1) xs |
107 else (true, (v, subst_bounds (xs, t))); |
107 else (true, (v, subst_bounds (xs, t))); |
108 |
108 |
109 fun is_f (Const (@{const_syntax case_prod}, _) $ Abs _) = true |
109 fun is_f (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs _) = true |
110 | is_f (Abs _) = true |
110 | is_f (Abs _) = true |
111 | is_f _ = false; |
111 | is_f _ = false; |
112 |
112 |
113 |
113 |
114 (* assn_tr' & bexp_tr'*) |
114 (* assn_tr' & bexp_tr'*) |
115 |
115 |
116 fun assn_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T |
116 fun assn_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T |
117 | assn_tr' (Const (@{const_syntax inter}, _) $ |
117 | assn_tr' (Const (\<^const_syntax>\<open>inter\<close>, _) $ |
118 (Const (@{const_syntax Collect}, _) $ T1) $ (Const (@{const_syntax Collect}, _) $ T2)) = |
118 (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T1) $ (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T2)) = |
119 Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2 |
119 Syntax.const \<^const_syntax>\<open>inter\<close> $ dest_abstuple T1 $ dest_abstuple T2 |
120 | assn_tr' t = t; |
120 | assn_tr' t = t; |
121 |
121 |
122 fun bexp_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T |
122 fun bexp_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T |
123 | bexp_tr' t = t; |
123 | bexp_tr' t = t; |
124 |
124 |
125 |
125 |
126 (* com_tr' *) |
126 (* com_tr' *) |
127 |
127 |
129 let |
129 let |
130 val (vs, ts) = mk_vts f; |
130 val (vs, ts) = mk_vts f; |
131 val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs); |
131 val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs); |
132 in |
132 in |
133 if ch |
133 if ch |
134 then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which |
134 then Syntax.const \<^syntax_const>\<open>_assign\<close> $ fst which $ snd which |
135 else Syntax.const @{const_syntax annskip} |
135 else Syntax.const \<^const_syntax>\<open>annskip\<close> |
136 end; |
136 end; |
137 |
137 |
138 fun com_tr' (Const (@{const_syntax Basic}, _) $ f) = |
138 fun com_tr' (Const (\<^const_syntax>\<open>Basic\<close>, _) $ f) = |
139 if is_f f then mk_assign f |
139 if is_f f then mk_assign f |
140 else Syntax.const @{const_syntax Basic} $ f |
140 else Syntax.const \<^const_syntax>\<open>Basic\<close> $ f |
141 | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) = |
141 | com_tr' (Const (\<^const_syntax>\<open>Seq\<close>,_) $ c1 $ c2) = |
142 Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2 |
142 Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr' c1 $ com_tr' c2 |
143 | com_tr' (Const (@{const_syntax Cond}, _) $ b $ c1 $ c2) = |
143 | com_tr' (Const (\<^const_syntax>\<open>Cond\<close>, _) $ b $ c1 $ c2) = |
144 Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 |
144 Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 |
145 | com_tr' (Const (@{const_syntax While}, _) $ b $ I $ c) = |
145 | com_tr' (Const (\<^const_syntax>\<open>While\<close>, _) $ b $ I $ c) = |
146 Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c |
146 Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr' b $ assn_tr' I $ com_tr' c |
147 | com_tr' t = t; |
147 | com_tr' t = t; |
148 |
148 |
149 in |
149 in |
150 |
150 |
151 fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q; |
151 fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q; |