1.1 --- a/src/HOL/BNF/Examples/Misc_Codatatype.thy Thu Sep 12 18:09:17 2013 -0700
1.2 +++ b/src/HOL/BNF/Examples/Misc_Codatatype.thy Thu Sep 12 18:09:56 2013 -0700
1.3 @@ -43,6 +43,8 @@
1.4 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
1.5 *)
1.6
1.7 +codatatype 'a p = P "'a + 'a p"
1.8 +
1.9 codatatype 'a J1 = J11 'a "'a J1" | J12 'a "'a J2"
1.10 and 'a J2 = J21 | J22 "'a J1" "'a J2"
1.11
2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Sep 12 18:09:17 2013 -0700
2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Sep 12 18:09:56 2013 -0700
2.3 @@ -44,8 +44,8 @@
2.4 val build_rel: local_theory -> (typ * typ -> term) -> typ * typ -> term
2.5 val dest_map: Proof.context -> string -> term -> term * term list
2.6 val dest_ctr: Proof.context -> string -> term -> term * term list
2.7 - val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list ->
2.8 - int list list -> term list list -> Proof.context ->
2.9 + val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list list list -> typ list -> typ list ->
2.10 + int list -> int list list -> term list list -> Proof.context ->
2.11 (term list list
2.12 * (typ list list * typ list list list list * term list list
2.13 * term list list list list) list option
2.14 @@ -53,9 +53,9 @@
2.15 * ((term list list * term list list list) * (typ list * typ list list)) list) option)
2.16 * Proof.context
2.17
2.18 - val mk_iter_fun_arg_types: typ list -> int list -> int list list -> term ->
2.19 + val mk_iter_fun_arg_types: typ list list list -> int list -> int list list -> term ->
2.20 typ list list list list
2.21 - val mk_coiter_fun_arg_types: typ list -> int list -> int list list -> term ->
2.22 + val mk_coiter_fun_arg_types: typ list list list -> typ list -> int list -> term ->
2.23 typ list list
2.24 * (typ list list list list * typ list list list * typ list list list list * typ list)
2.25 val define_iters: string list ->
2.26 @@ -268,12 +268,12 @@
2.27
2.28 val mk_fp_iter_fun_types = binder_fun_types o fastype_of;
2.29
2.30 -fun unzip_recT Cs (T as Type (@{type_name prod}, Ts as [_, U])) =
2.31 - if member (op =) Cs U then Ts else [T]
2.32 +fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
2.33 + | unzip_recT _ (T as Type (@{type_name prod}, Ts)) = Ts
2.34 | unzip_recT _ T = [T];
2.35
2.36 -fun unzip_corecT Cs (T as Type (@{type_name sum}, Ts as [_, U])) =
2.37 - if member (op =) Cs U then Ts else [T]
2.38 +fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
2.39 + | unzip_corecT _ (T as Type (@{type_name sum}, Ts)) = Ts
2.40 | unzip_corecT _ T = [T];
2.41
2.42 fun mk_map live Ts Us t =
2.43 @@ -398,12 +398,12 @@
2.44
2.45 fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
2.46
2.47 -fun mk_iter_fun_arg_types Cs ns mss =
2.48 +fun mk_iter_fun_arg_types ctr_Tsss ns mss =
2.49 mk_fp_iter_fun_types
2.50 #> map3 mk_iter_fun_arg_types0 ns mss
2.51 - #> map (map (map (unzip_recT Cs)));
2.52 + #> map2 (map2 (map2 unzip_recT)) ctr_Tsss;
2.53
2.54 -fun mk_iters_args_types Cs ns mss ctor_iter_fun_Tss lthy =
2.55 +fun mk_iters_args_types ctr_Tsss Cs ns mss ctor_iter_fun_Tss lthy =
2.56 let
2.57 val Css = map2 replicate ns Cs;
2.58 val y_Tsss = map3 mk_iter_fun_arg_types0 ns mss (map un_fold_of ctor_iter_fun_Tss);
2.59 @@ -418,8 +418,11 @@
2.60 val yssss = map (map (map single)) ysss;
2.61
2.62 val z_Tssss =
2.63 - map3 (fn n => fn ms => map2 (map (unzip_recT Cs) oo dest_tupleT) ms o
2.64 - dest_sumTN_balanced n o domain_type o co_rec_of) ns mss ctor_iter_fun_Tss;
2.65 + map4 (fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts =>
2.66 + map3 (fn m => fn ctr_Ts => fn ctor_iter_fun_T =>
2.67 + map2 unzip_recT ctr_Ts (dest_tupleT m ctor_iter_fun_T))
2.68 + ms ctr_Tss (dest_sumTN_balanced n (domain_type (co_rec_of ctor_iter_fun_Ts))))
2.69 + ns mss ctr_Tsss ctor_iter_fun_Tss;
2.70
2.71 val z_Tsss' = map (map flat_rec_arg_args) z_Tssss;
2.72 val h_Tss = map2 (map2 (curry op --->)) z_Tsss' Css;
2.73 @@ -434,16 +437,18 @@
2.74 ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
2.75 end;
2.76
2.77 -fun mk_coiter_fun_arg_types0 Cs ns mss fun_Ts =
2.78 +fun mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts =
2.79 let
2.80 - (*avoid "'a itself" arguments in coiterators and corecursors*)
2.81 - fun repair_arity [0] = [1]
2.82 - | repair_arity ms = ms;
2.83 + (*avoid "'a itself" arguments in coiterators*)
2.84 + fun repair_arity [[]] = [[@{typ unit}]]
2.85 + | repair_arity Tss = Tss;
2.86
2.87 + val ctr_Tsss' = map repair_arity ctr_Tsss;
2.88 val f_sum_prod_Ts = map range_type fun_Ts;
2.89 val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
2.90 - val f_Tsss = map2 (map2 dest_tupleT o repair_arity) mss f_prod_Tss;
2.91 - val f_Tssss = map2 (fn C => map (map (map (curry op --> C) o unzip_corecT Cs))) Cs f_Tsss;
2.92 + val f_Tsss = map2 (map2 (dest_tupleT o length)) ctr_Tsss' f_prod_Tss;
2.93 + val f_Tssss = map3 (fn C => map2 (map2 (map (curry op --> C) oo unzip_corecT)))
2.94 + Cs ctr_Tsss' f_Tsss;
2.95 val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
2.96 in
2.97 (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts)
2.98 @@ -451,18 +456,18 @@
2.99
2.100 fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
2.101
2.102 -fun mk_coiter_fun_arg_types Cs ns mss dtor_coiter =
2.103 +fun mk_coiter_fun_arg_types ctr_Tsss Cs ns dtor_coiter =
2.104 (mk_coiter_p_pred_types Cs ns,
2.105 - mk_fp_iter_fun_types dtor_coiter |> mk_coiter_fun_arg_types0 Cs ns mss);
2.106 + mk_fp_iter_fun_types dtor_coiter |> mk_coiter_fun_arg_types0 ctr_Tsss Cs ns);
2.107
2.108 -fun mk_coiters_args_types Cs ns mss dtor_coiter_fun_Tss lthy =
2.109 +fun mk_coiters_args_types ctr_Tsss Cs ns mss dtor_coiter_fun_Tss lthy =
2.110 let
2.111 val p_Tss = mk_coiter_p_pred_types Cs ns;
2.112
2.113 fun mk_types get_Ts =
2.114 let
2.115 val fun_Ts = map get_Ts dtor_coiter_fun_Tss;
2.116 - val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) = mk_coiter_fun_arg_types0 Cs ns mss fun_Ts;
2.117 + val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) = mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts;
2.118 val pf_Tss = map3 flat_corec_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
2.119 in
2.120 (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss))
2.121 @@ -509,7 +514,7 @@
2.122 ((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
2.123 end;
2.124
2.125 -fun mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy =
2.126 +fun mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy =
2.127 let
2.128 val thy = Proof_Context.theory_of lthy;
2.129
2.130 @@ -519,9 +524,9 @@
2.131
2.132 val ((iters_args_types, coiters_args_types), lthy') =
2.133 if fp = Least_FP then
2.134 - mk_iters_args_types Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME)
2.135 + mk_iters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME)
2.136 else
2.137 - mk_coiters_args_types Cs ns mss xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME)
2.138 + mk_coiters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME)
2.139 in
2.140 ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy')
2.141 end;
2.142 @@ -1224,7 +1229,7 @@
2.143 val mss = map (map length) ctr_Tsss;
2.144
2.145 val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') =
2.146 - mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
2.147 + mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
2.148
2.149 fun define_ctrs_dtrs_for_type (((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
2.150 xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
3.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Thu Sep 12 18:09:17 2013 -0700
3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Thu Sep 12 18:09:56 2013 -0700
3.3 @@ -127,7 +127,7 @@
3.4 val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
3.5
3.6 val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
3.7 - mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
3.8 + mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
3.9
3.10 fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
3.11
4.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Sep 12 18:09:17 2013 -0700
4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Sep 12 18:09:56 2013 -0700
4.3 @@ -312,7 +312,8 @@
4.4
4.5 val perm_Cs = map (body_type o fastype_of o co_rec_of o of_fp_sugar (#xtor_co_iterss o #fp_res))
4.6 perm_fp_sugars;
4.7 - val perm_fun_arg_Tssss = mk_iter_fun_arg_types perm_Cs perm_ns perm_mss (co_rec_of ctor_iters1);
4.8 + val perm_fun_arg_Tssss =
4.9 + mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1);
4.10
4.11 fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
4.12 fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
4.13 @@ -389,12 +390,11 @@
4.14 val nn = length perm_fpTs;
4.15 val kks = 0 upto nn - 1;
4.16 val perm_ns = map length perm_ctr_Tsss;
4.17 - val perm_mss = map (map length) perm_ctr_Tsss;
4.18
4.19 val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
4.20 of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
4.21 val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
4.22 - mk_coiter_fun_arg_types perm_Cs perm_ns perm_mss (co_rec_of dtor_coiters1);
4.23 + mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
4.24
4.25 val (perm_p_hss, h) = indexedd perm_p_Tss 0;
4.26 val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;