139 in |
139 in |
140 (bn_funs', bn_eqs') |
140 (bn_funs', bn_eqs') |
141 end |
141 end |
142 *} |
142 *} |
143 |
143 |
|
144 ML {* |
|
145 fun apfst3 f (a, b, c) = (f a, b, c) |
|
146 *} |
|
147 |
144 ML {* |
148 ML {* |
145 fun rawify_binds dts_env cnstrs_env bn_fun_env binds = |
149 fun rawify_binds dts_env cnstrs_env bn_fun_env binds = |
146 map (map (map (map (fn (opt_trm, i, j) => |
150 map (map (map (map (fn (opt_trm, i, j, aty) => |
147 (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds |
151 (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j, aty))))) binds |
148 *} |
152 *} |
149 |
153 |
150 ML {* |
154 ML {* |
151 fun find [] _ = error ("cannot find element") |
155 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 |
156 | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y |
153 *} |
157 *} |
154 |
158 |
155 ML {* @{term "{x, y}"} *} |
|
156 ML range_type |
|
157 ML {* |
159 ML {* |
158 fun strip_union t = |
160 fun strip_union t = |
159 case t of |
161 case t of |
160 Const (@{const_name sup}, _) $ l $ r => strip_union l @ strip_union r |
162 Const (@{const_name sup}, _) $ l $ r => strip_union l @ strip_union r |
161 | (h as (Const (@{const_name insert}, T))) $ x $ y => |
163 | (h as (Const (@{const_name insert}, T))) $ x $ y => |
288 |
290 |
289 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
291 ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *} |
290 ML {* val cheat_equivp = Unsynchronized.ref false *} |
292 ML {* val cheat_equivp = Unsynchronized.ref false *} |
291 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
293 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
292 ML {* val cheat_const_rsp = Unsynchronized.ref false *} |
294 ML {* val cheat_const_rsp = Unsynchronized.ref false *} |
293 |
|
294 ML {* fun map_option _ NONE = NONE |
|
295 | map_option f (SOME x) = SOME (f x) *} |
|
296 |
295 |
297 (* nominal_datatype2 does the following things in order: |
296 (* nominal_datatype2 does the following things in order: |
298 1) define the raw datatype |
297 1) define the raw datatype |
299 2) define the raw binding functions |
298 2) define the raw binding functions |
300 3) define permutations of the raw datatype and show that raw type is in the pt typeclass |
299 3) define permutations of the raw datatype and show that raw type is in the pt typeclass |
338 val thy = ProofContext.theory_of lthy |
337 val thy = ProofContext.theory_of lthy |
339 val thy_name = Context.theory_name thy |
338 val thy_name = Context.theory_name thy |
340 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
339 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) = |
341 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
340 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
342 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
341 val morphism_2_1 = ProofContext.export_morphism lthy2 lthy |
343 fun export_fun f (t, l) = (f t, map (map (apsnd (map_option f))) l); |
342 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
344 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_1)))) raw_bns; |
343 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_1)))) raw_bns; |
345 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
344 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
346 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
345 val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc |
347 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
346 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
348 |
347 |
600 in |
600 in |
601 map_index (prep_typ binds) annos |
601 map_index (prep_typ binds) annos |
602 end |
602 end |
603 |
603 |
604 in |
604 in |
605 map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)) |
605 map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type))))) |
|
606 (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) |
606 end |
607 end |
607 *} |
608 *} |
608 |
609 |
609 ML {* |
610 ML {* |
610 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
611 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |