tuning
authorblanchet
Mon Sep 15 12:11:41 2014 +0200 (2014-09-15)
changeset 583405f6f48e87de6
parent 58339 f6af48bd7c04
child 58341 6c8b30b9f583
tuning
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Sep 15 11:54:47 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Sep 15 12:11:41 2014 +0200
     1.3 @@ -47,8 +47,8 @@
     1.4      Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
     1.5    end;
     1.6  
     1.7 -fun construct_mutualized_fp fp cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
     1.8 -    (absT_infos : absT_info list) lthy =
     1.9 +fun construct_mutualized_fp fp mutual_cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss)
    1.10 +    bnfs (absT_infos : absT_info list) lthy =
    1.11    let
    1.12      fun of_fp_res get =
    1.13        map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
    1.14 @@ -273,15 +273,15 @@
    1.15            map (typ_subst_nonatomic_sorted (map (rpair dummyT)
    1.16              (As @ sort (int_ord o pairself Term.size_of_typ) fpTs))) fold_preTs';
    1.17  
    1.18 -        val (clique, TUs) =
    1.19 +        val (mutual_clique, TUs) =
    1.20            map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
    1.21            |>> map subst
    1.22            |> `(fn (_, Ys) =>
    1.23 -            nth cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
    1.24 +            nth mutual_cliques (find_index (fn X => X = the (find_first (can dest_TFree) Ys)) Xs))
    1.25            ||> uncurry (map2 mk_co_algT);
    1.26 -        val cands = cliques ~~ map2 mk_co_algT fold_preTs' Xs;
    1.27 +        val cands = mutual_cliques ~~ map2 mk_co_algT fold_preTs' Xs;
    1.28          val js = find_indices (fn ((cl, cand), TU) =>
    1.29 -          cl = clique andalso Type.could_unify (TU, cand)) TUs cands;
    1.30 +          cl = mutual_clique andalso Type.could_unify (TU, cand)) TUs cands;
    1.31          val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
    1.32        in
    1.33          force_typ names_lthy (Tpats ---> TU) raw_rec
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 15 11:54:47 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 15 12:11:41 2014 +0200
     2.3 @@ -117,7 +117,7 @@
     2.4    |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
     2.5    |> map_filter I;
     2.6  
     2.7 -fun mutualize_fp_sugars plugins fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy =
     2.8 +fun mutualize_fp_sugars plugins fp mutual_cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy =
     2.9    let
    2.10      val thy = Proof_Context.theory_of no_defs_lthy;
    2.11  
    2.12 @@ -240,8 +240,8 @@
    2.13  
    2.14          val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
    2.15                 dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
    2.16 -          fp_bnf (construct_mutualized_fp fp cliques unsorted_fpTs fp_sugars0) fp_bs unsorted_As'
    2.17 -            killed_As' fp_eqs no_defs_lthy;
    2.18 +          fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_sugars0) fp_bs
    2.19 +            unsorted_As' killed_As' fp_eqs no_defs_lthy;
    2.20  
    2.21          val fp_abs_inverses = map #abs_inverse fp_absT_infos;
    2.22          val fp_type_definitions = map #type_definition fp_absT_infos;
    2.23 @@ -421,7 +421,7 @@
    2.24        | gather_types _ _ _ _ (T :: _) = not_co_datatype T;
    2.25  
    2.26      val (perm_Tss, perm_gen_Ts) = gather_types lthy [] [] [] sorted_actual_Ts;
    2.27 -    val (perm_cliques, perm_Ts) =
    2.28 +    val (perm_mutual_cliques, perm_Ts) =
    2.29        split_list (flat (map_index (fn (i, perm_Ts) => map (pair i) perm_Ts) perm_Tss));
    2.30  
    2.31      val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts;
    2.32 @@ -441,10 +441,10 @@
    2.33      fun permute xs = permute_like (op =) Ts perm_Ts xs;
    2.34      fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs;
    2.35  
    2.36 -    (* The assignment of callers to cliques is incorrect in general. This code would need to inspect
    2.37 -       the actual calls to discover the correct cliques in the presence of type duplicates. However,
    2.38 -       the naive scheme implemented here supports "prim(co)rec" specifications following reasonable
    2.39 -       ordering of the duplicates (e.g., keeping the cliques together). *)
    2.40 +    (* The assignment of callers to mutual cliques is incorrect in general. This code would need to
    2.41 +       inspect the actual calls to discover the correct cliques in the presence of type duplicates.
    2.42 +       However, the naive scheme implemented here supports "prim(co)rec" specifications following
    2.43 +       reasonable ordering of the duplicates (e.g., keeping the cliques together). *)
    2.44      val perm_bs = permute bs;
    2.45      val perm_callers = permute callers;
    2.46      val perm_kks = permute kks;
    2.47 @@ -457,7 +457,7 @@
    2.48        if length perm_Tss = 1 then
    2.49          ((perm_fp_sugars0, (NONE, NONE)), lthy)
    2.50        else
    2.51 -        mutualize_fp_sugars plugins fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers
    2.52 +        mutualize_fp_sugars plugins fp perm_mutual_cliques perm_bs perm_frozen_gen_Ts perm_callers
    2.53            perm_callssss perm_fp_sugars0 lthy;
    2.54  
    2.55      val fp_sugars = unpermute perm_fp_sugars;
     3.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 15 11:54:47 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 15 12:11:41 2014 +0200
     3.3 @@ -262,7 +262,7 @@
     3.4  
     3.5      (* put nested types before the types that nest them, as needed for N2M *)
     3.6      val descrs = burrow reindex_desc (orig_descr' :: rev nested_descrs);
     3.7 -    val (cliques, descr) =
     3.8 +    val (mutual_cliques, descr) =
     3.9        split_list (flat (map_index (fn (i, descr) => map (pair i) descr)
    3.10          (maps cliquify_descr descrs)));
    3.11  
    3.12 @@ -286,8 +286,8 @@
    3.13  
    3.14      val ((fp_sugars', (lfp_sugar_thms', _)), lthy') =
    3.15        if nn > nn_fp then
    3.16 -        mutualize_fp_sugars (K true) Least_FP cliques compat_bs fpTs' callers callssss fp_sugars
    3.17 -          lthy
    3.18 +        mutualize_fp_sugars (K true) Least_FP mutual_cliques compat_bs fpTs' callers callssss
    3.19 +          fp_sugars lthy
    3.20        else
    3.21          ((fp_sugars, (NONE, NONE)), lthy);
    3.22