140 syntax |
140 syntax |
141 "_match" :: "'a" |
141 "_match" :: "'a" |
142 |
142 |
143 print_translation \<open> |
143 print_translation \<open> |
144 let |
144 let |
145 fun dest_LAM (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>unit_when\<close>,_) $ t) = |
145 fun dest_LAM _ (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>unit_when\<close>,_) $ t) = |
146 (Syntax.const \<^syntax_const>\<open>_noargs\<close>, t) |
146 (Syntax.const \<^syntax_const>\<open>_noargs\<close>, t) |
147 | dest_LAM (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>csplit\<close>,_) $ t) = |
147 | dest_LAM ctxt (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>csplit\<close>,_) $ t) = |
148 let |
148 let |
149 val (v1, t1) = dest_LAM t; |
149 val (v1, t1) = dest_LAM ctxt t; |
150 val (v2, t2) = dest_LAM t1; |
150 val (v2, t2) = dest_LAM ctxt t1; |
151 in (Syntax.const \<^syntax_const>\<open>_args\<close> $ v1 $ v2, t2) end |
151 in (Syntax.const \<^syntax_const>\<open>_args\<close> $ v1 $ v2, t2) end |
152 | dest_LAM (Const (\<^const_syntax>\<open>Abs_cfun\<close>,_) $ t) = |
152 | dest_LAM ctxt (Const (\<^const_syntax>\<open>Abs_cfun\<close>,_) $ t) = |
153 let |
153 let |
154 val abs = |
154 val abs = |
155 case t of Abs abs => abs |
155 case t of Abs abs => abs |
156 | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0); |
156 | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0); |
157 val (x, t') = Syntax_Trans.atomic_abs_tr' abs; |
157 val (x, t') = Syntax_Trans.atomic_abs_tr' ctxt abs; |
158 in (Syntax.const \<^syntax_const>\<open>_variable\<close> $ x, t') end |
158 in (Syntax.const \<^syntax_const>\<open>_variable\<close> $ x, t') end |
159 | dest_LAM _ = raise Match; (* too few vars: abort translation *) |
159 | dest_LAM _ _ = raise Match; (* too few vars: abort translation *) |
160 |
160 |
161 fun Case1_tr' [Const(\<^const_syntax>\<open>branch\<close>,_) $ p, r] = |
161 fun Case1_tr' ctxt [Const(\<^const_syntax>\<open>branch\<close>,_) $ p, r] = |
162 let val (v, t) = dest_LAM r in |
162 let val (v, t) = dest_LAM ctxt r in |
163 Syntax.const \<^syntax_const>\<open>_Case1\<close> $ |
163 Syntax.const \<^syntax_const>\<open>_Case1\<close> $ |
164 (Syntax.const \<^syntax_const>\<open>_match\<close> $ p $ v) $ t |
164 (Syntax.const \<^syntax_const>\<open>_match\<close> $ p $ v) $ t |
165 end; |
165 end; |
166 |
166 |
167 in [(\<^const_syntax>\<open>Rep_cfun\<close>, K Case1_tr')] end |
167 in [(\<^const_syntax>\<open>Rep_cfun\<close>, Case1_tr')] end |
168 \<close> |
168 \<close> |
169 |
169 |
170 translations |
170 translations |
171 "x" <= "_match (CONST succeed) (_variable x)" |
171 "x" <= "_match (CONST succeed) (_variable x)" |
172 |
172 |