148 *} |
148 *} |
149 |
149 |
150 ML {* |
150 ML {* |
151 fun find [] _ = error ("cannot find element") |
151 fun find [] _ = error ("cannot find element") |
152 | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y |
152 | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y |
|
153 *} |
|
154 |
|
155 ML {* @{term "{x, y}"} *} |
|
156 ML range_type |
|
157 ML {* |
|
158 fun strip_union t = |
|
159 case t of |
|
160 Const (@{const_name sup}, _) $ l $ r => strip_union l @ strip_union r |
|
161 | (h as (Const (@{const_name insert}, T))) $ x $ y => |
|
162 (h $ x $ Const (@{const_name bot}, range_type (range_type T))) :: strip_union y |
|
163 | Const (@{const_name bot}, _) => [] |
|
164 | _ => [t] |
|
165 *} |
|
166 |
|
167 ML {* |
|
168 fun bn_or_atom t = |
|
169 case t of |
|
170 Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ |
|
171 Const (@{const_name bot}, _) => (i, NONE) |
|
172 | f $ Bound i => (i, SOME f) |
|
173 | _ => error "Unsupported binding function" |
153 *} |
174 *} |
154 |
175 |
155 ML {* |
176 ML {* |
156 fun prep_bn dt_names dts eqs = |
177 fun prep_bn dt_names dts eqs = |
157 let |
178 let |
164 val (bn_fun, [cnstr]) = strip_comb lhs |
185 val (bn_fun, [cnstr]) = strip_comb lhs |
165 val (_, ty) = dest_Free bn_fun |
186 val (_, ty) = dest_Free bn_fun |
166 val (ty_name, _) = dest_Type (domain_type ty) |
187 val (ty_name, _) = dest_Type (domain_type ty) |
167 val dt_index = find_index (fn x => x = ty_name) dt_names |
188 val dt_index = find_index (fn x => x = ty_name) dt_names |
168 val (cnstr_head, cnstr_args) = strip_comb cnstr |
189 val (cnstr_head, cnstr_args) = strip_comb cnstr |
169 val included = map (fn i => length (cnstr_args) - i - 1) (loose_bnos rhs) |
190 val rhs_elements = map bn_or_atom (strip_union rhs) |
|
191 val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements |
170 in |
192 in |
171 (dt_index, (bn_fun, (cnstr_head, included))) |
193 (dt_index, (bn_fun, (cnstr_head, included))) |
172 end |
194 end |
173 |
|
174 fun order dts i ts = |
195 fun order dts i ts = |
175 let |
196 let |
176 val dt = nth dts i |
197 val dt = nth dts i |
177 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) |
198 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) |
178 val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts |
199 val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts |
272 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
293 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
273 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
294 ML {* val cheat_fv_eqvt = Unsynchronized.ref false *} |
274 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
295 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
275 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
296 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
276 |
297 |
|
298 ML {* fun map_option _ NONE = NONE |
|
299 | map_option f (SOME x) = SOME (f x) *} |
277 |
300 |
278 ML {* |
301 ML {* |
279 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
302 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
280 let |
303 let |
281 val _ = tracing "Raw declarations"; |
304 val _ = tracing "Raw declarations"; |
282 val thy = ProofContext.theory_of lthy |
305 val thy = ProofContext.theory_of lthy |
283 val thy_name = Context.theory_name thy |
306 val thy_name = Context.theory_name thy |
284 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
307 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
285 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
308 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
286 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
309 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
287 val raw_bns_exp = map (apsnd (map (apfst (Morphism.term morphism_2_1)))) raw_bns; |
310 fun export_fun f (t, l) = (f t, map (map (apsnd (map_option f))) l); |
|
311 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_1)))) raw_bns; |
288 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
312 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
289 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
313 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
290 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
314 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
291 |
315 |
292 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
316 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |