sorted out type issue with sort constraints
authorblanchet
Wed Mar 23 16:37:13 2016 +0100 (2016-03-23)
changeset 62699add334b71e16
parent 62698 9d706e37ddab
child 62700 e3ca8dc01c4f
sorted out type issue with sort constraints
src/HOL/Tools/BNF/bnf_gfp_grec.ML
src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue Mar 22 13:44:50 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Wed Mar 23 16:37:13 2016 +0100
     1.3 @@ -555,8 +555,9 @@
     1.4  
     1.5      val T_name = Local_Theory.full_name lthy T_b;
     1.6  
     1.7 -    val tyargs = map2 (fn alive => pair (if alive then SOME Binding.empty else NONE)
     1.8 -      o rpair @{sort type}) (fp_alives @ [true]) (Es @ [Y]);
     1.9 +    val tyargs = map2 (fn alive => fn T =>
    1.10 +        (if alive then SOME Binding.empty else NONE, (T, Type.sort_of_atyp T)))
    1.11 +      (fp_alives @ [true]) (Es @ [Y]);
    1.12      val ctr_specs = [(((Binding.empty, ctr_b), [(sel_b, rhsT)]), NoSyn)];
    1.13      val spec = (((((tyargs, T_b), NoSyn), ctr_specs),
    1.14        (Binding.empty, Binding.empty, Binding.empty)), []);
    1.15 @@ -590,8 +591,9 @@
    1.16      val As = Es @ [Y];
    1.17      val ssig_sig_T = Type (sig_T_name, Es @ [Type (T_name, As)]);
    1.18  
    1.19 -    val tyargs = map2 (fn alive => pair (if alive then SOME Binding.empty else NONE)
    1.20 -      o rpair @{sort type}) (fp_alives @ [true]) As;
    1.21 +    val tyargs = map2 (fn alive => fn T =>
    1.22 +        (if alive then SOME Binding.empty else NONE, (T, Type.sort_of_atyp T)))
    1.23 +      (fp_alives @ [true]) (Es @ [Y]);
    1.24      val ctr_specs =
    1.25        [(((Binding.empty, Oper_b), [(Binding.empty, ssig_sig_T)]), NoSyn),
    1.26         (((Binding.empty, VLeaf_b), [(Binding.empty, Y)]), NoSyn),
    1.27 @@ -2066,12 +2068,12 @@
    1.28    let
    1.29      val fp_sugar as {T = Type (_, fpT_args0), pre_bnf, fp_bnf, fp_res, ...} =
    1.30        checked_fp_sugar_of lthy fpT_name;
    1.31 -    val num_fp_tyargs = length fpT_args0;
    1.32 -    val fp_alives = liveness_of_fp_bnf num_fp_tyargs fp_bnf;
    1.33 +    val fpT_Ss = map Type.sort_of_atyp fpT_args0;
    1.34 +    val fp_alives = liveness_of_fp_bnf (length fpT_args0) fp_bnf;
    1.35  
    1.36      val (((Es, Fs0), [Y, Z]), names_lthy) = lthy
    1.37 -      |> mk_TFrees num_fp_tyargs
    1.38 -      ||>> mk_TFrees num_fp_tyargs
    1.39 +      |> mk_TFrees' fpT_Ss
    1.40 +      ||>> mk_TFrees' fpT_Ss
    1.41        ||>> mk_TFrees 2;
    1.42      val Fs = @{map 3} (fn alive => fn E => fn F => if alive then F else E) fp_alives Es Fs0;
    1.43  
    1.44 @@ -2602,13 +2604,13 @@
    1.45       : corec_info)
    1.46      lthy =
    1.47    let
    1.48 -    val {pre_bnf = live_pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
    1.49 +    val {T = Type (_, fpT_args0), pre_bnf = live_pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
    1.50        checked_fp_sugar_of lthy fpT_name;
    1.51 -    val num_fp_tyargs = length res_Ds;
    1.52 -    val live_fp_alives = liveness_of_fp_bnf num_fp_tyargs live_fp_bnf;
    1.53 +    val fpT_Ss = map Type.sort_of_atyp fpT_args0;
    1.54 +    val live_fp_alives = liveness_of_fp_bnf (length fpT_args0) live_fp_bnf;
    1.55  
    1.56      val ((Ds, [Y, Z]), names_lthy) = lthy
    1.57 -      |> mk_TFrees num_fp_tyargs
    1.58 +      |> mk_TFrees' fpT_Ss
    1.59        ||>> mk_TFrees 2;
    1.60  
    1.61      (* FIXME *)
    1.62 @@ -3077,12 +3079,12 @@
    1.63      val _ = not (null arg_Ts) orelse
    1.64        error "Function with no argument cannot be registered as friend";
    1.65  
    1.66 -    val {pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} = checked_fp_sugar_of lthy fpT_name;
    1.67 -    val num_fp_tyargs = length res_Ds;
    1.68 +    val {T = Type (fpT_name, fpT_args0), pre_bnf, fp_bnf = live_fp_bnf, fp_res, ...} =
    1.69 +      checked_fp_sugar_of lthy fpT_name;
    1.70 +    val num_fp_tyargs = length fpT_args0;
    1.71 +    val fpT_Ss = map Type.sort_of_atyp fpT_args0;
    1.72      val live_fp_alives = liveness_of_fp_bnf num_fp_tyargs live_fp_bnf;
    1.73  
    1.74 -    val fpT_name = fst (dest_Type res_T);
    1.75 -
    1.76      val (old_info as {friend_names = old_friend_names, sig_fp_sugars = old_sig_fp_sugar :: _,
    1.77             buffer = old_buffer, ...}, lthy) =
    1.78        corec_info_of res_T lthy;
    1.79 @@ -3099,7 +3101,7 @@
    1.80  
    1.81      val lthy = lthy |> Variable.declare_typ friend_T;
    1.82      val ((Ds, [Y, Z]), _) = lthy
    1.83 -      |> mk_TFrees num_fp_tyargs
    1.84 +      |> mk_TFrees' fpT_Ss
    1.85        ||>> mk_TFrees 2;
    1.86  
    1.87      (* FIXME *)
     2.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Mar 22 13:44:50 2016 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Mar 23 16:37:13 2016 +0100
     2.3 @@ -225,12 +225,12 @@
     2.4    let
     2.5      val thy = Proof_Context.theory_of ctxt;
     2.6  
     2.7 -    val SOME ({fp_res_index, fp_res = {dtors, dtor_ctors, ...},
     2.8 +    val SOME ({fp_res_index, fp_res = {dtors = dtors0, dtor_ctors, ...},
     2.9          absT_info = {rep = rep0, abs_inverse, ...},
    2.10          fp_ctr_sugar = {ctr_defs, ctr_sugar = {casex, exhaust, case_thms, ...}, ...}, ...}) =
    2.11        fp_sugar_of ctxt fpT_name;
    2.12  
    2.13 -    val (f_Ts, Type (_, [fpT, _])) = strip_fun_type (fastype_of casex);
    2.14 +    val (f_Ts, Type (_, [fpT as Type (_, As), _])) = strip_fun_type (fastype_of casex);
    2.15      val x_Tss = map binder_types f_Ts;
    2.16  
    2.17      val (((u, fs), xss), _) = ctxt
    2.18 @@ -238,7 +238,9 @@
    2.19        ||>> mk_Frees "f" f_Ts
    2.20        ||>> mk_Freess "x" x_Tss;
    2.21  
    2.22 -    val dtor = nth dtors fp_res_index;
    2.23 +    val dtor0 = nth dtors0 fp_res_index;
    2.24 +    val dtor = mk_dtor As dtor0;
    2.25 +
    2.26      val u' = dtor $ u;
    2.27  
    2.28      val absT = fastype_of u';
    2.29 @@ -264,7 +266,7 @@
    2.30      val fpT0 as Type (_, As0) = domain_type (body_fun_type (fastype_of casex));
    2.31  
    2.32      val (As, _) = ctxt
    2.33 -      |> mk_TFrees (length As0);
    2.34 +      |> mk_TFrees' (map Type.sort_of_atyp As0);
    2.35      val fpT = Type (fpT_name, As);
    2.36  
    2.37      val (var_name, ()) = singleton (Variable.variant_frees ctxt []) ("x", ());
    2.38 @@ -666,7 +668,7 @@
    2.39      Symtab.make_list (names ~~ thms)
    2.40    end;
    2.41  
    2.42 -fun derive_coinduct ctxt (fpT as Type (fpT_name, _)) dtor_coinduct =
    2.43 +fun derive_coinduct ctxt (fpT as Type (fpT_name, fpT_args)) dtor_coinduct =
    2.44    let
    2.45      val thy = Proof_Context.theory_of ctxt;
    2.46  
    2.47 @@ -677,14 +679,15 @@
    2.48      val SOME {X as TVar ((X_s, _), _), fp_res = {dtor_ctors, ...}, pre_bnf,
    2.49          absT_info = {abs_inverse, ...}, live_nesting_bnfs,
    2.50          fp_ctr_sugar = {ctrXs_Tss, ctr_defs,
    2.51 -          ctr_sugar = ctr_sugar0 as {T = T0, ctrs = ctrs0, discs = discs0, ...}, ...}, ...} =
    2.52 +          ctr_sugar = ctr_sugar0 as {T = Type (_, T0_args), ctrs = ctrs0, discs = discs0, ...},
    2.53 +            ...}, ...} =
    2.54        fp_sugar_of ctxt fpT_name;
    2.55  
    2.56      val n = length ctrXs_Tss;
    2.57      val ms = map length ctrXs_Tss;
    2.58  
    2.59      val X' = TVar ((X_s, maxidx_of_typ fpT + 1), @{sort type});
    2.60 -    val As_rho = tvar_subst thy [T0] [fpT];
    2.61 +    val As_rho = tvar_subst thy T0_args fpT_args;
    2.62      val substXAT = Term.typ_subst_TVars As_rho o Tsubst X X';
    2.63      val substXA = Term.subst_TVars As_rho o substT X X';
    2.64      val phi = Morphism.typ_morphism "BNF" substXAT $> Morphism.term_morphism "BNF" substXA;
    2.65 @@ -1970,9 +1973,7 @@
    2.66    end;
    2.67  
    2.68  fun update_coinduct_cong_intross_dynamic fpT_name lthy =
    2.69 -  let
    2.70 -    val all_corec_infos = corec_infos_of lthy fpT_name;
    2.71 -  in
    2.72 +  let val all_corec_infos = corec_infos_of lthy fpT_name in
    2.73      lthy
    2.74      |> fold_map (apfst snd oo derive_coinduct_cong_intros) all_corec_infos
    2.75      |> snd