export more ML functions
authorblanchet
Mon Mar 16 23:00:38 2015 +0100 (2015-03-16)
changeset 59725e5dc7e7744f0
parent 59724 5ec903bf0eae
child 59726 64c2bb331035
export more ML functions
src/HOL/Tools/BNF/bnf_comp.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 16 17:47:46 2015 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 16 23:00:38 2015 +0100
     1.3 @@ -26,10 +26,30 @@
     1.4      (string * sort) list -> typ -> (comp_cache * unfold_set) * local_theory ->
     1.5      (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory)
     1.6    val default_comp_sort: (string * sort) list list -> (string * sort) list
     1.7 +  val clean_compose_bnf: BNF_Def.inline_policy -> (binding -> binding) -> binding -> BNF_Def.bnf ->
     1.8 +    BNF_Def.bnf list -> unfold_set * local_theory -> BNF_Def.bnf * (unfold_set * local_theory)
     1.9 +  val kill_bnf: (binding -> binding) -> int -> BNF_Def.bnf ->
    1.10 +    (comp_cache * unfold_set) * local_theory ->
    1.11 +    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
    1.12 +  val lift_bnf: (binding -> binding) -> int -> BNF_Def.bnf ->
    1.13 +    (comp_cache * unfold_set) * local_theory ->
    1.14 +    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
    1.15 +  val permute_bnf: (binding -> binding) -> int list -> int list -> BNF_Def.bnf ->
    1.16 +    (comp_cache * unfold_set) * local_theory ->
    1.17 +    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
    1.18 +  val permute_and_kill_bnf: (binding -> binding) -> int -> int list -> int list -> BNF_Def.bnf ->
    1.19 +    (comp_cache * unfold_set) * local_theory ->
    1.20 +    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
    1.21 +  val lift_and_permute_bnf: (binding -> binding) -> int -> int list -> int list -> BNF_Def.bnf ->
    1.22 +    (comp_cache * unfold_set) * local_theory ->
    1.23 +    BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory)
    1.24    val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
    1.25      (''a list list -> ''a list) -> BNF_Def.bnf list -> (comp_cache * unfold_set) * local_theory ->
    1.26      (int list list * ''a list) * (BNF_Def.bnf list * ((comp_cache * unfold_set) * local_theory))
    1.27 -
    1.28 +  val compose_bnf: BNF_Def.inline_policy -> (int -> binding -> binding) ->
    1.29 +    ((string * sort) list list -> (string * sort) list) -> BNF_Def.bnf -> BNF_Def.bnf list ->
    1.30 +    typ list -> typ list list -> typ list list -> (comp_cache * unfold_set) * local_theory ->
    1.31 +    (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory)
    1.32    type absT_info =
    1.33      {absT: typ,
    1.34       repT: typ,
    1.35 @@ -625,11 +645,11 @@
    1.36  
    1.37  (* Composition pipeline *)
    1.38  
    1.39 -fun permute_and_kill qualify n src dest bnf =
    1.40 +fun permute_and_kill_bnf qualify n src dest bnf =
    1.41    permute_bnf qualify src dest bnf
    1.42    #> uncurry (kill_bnf qualify n);
    1.43  
    1.44 -fun lift_and_permute qualify n src dest bnf =
    1.45 +fun lift_and_permute_bnf qualify n src dest bnf =
    1.46    lift_bnf qualify n bnf
    1.47    #> uncurry (permute_bnf qualify src dest);
    1.48  
    1.49 @@ -641,8 +661,8 @@
    1.50      val before_kill_dest = map2 append kill_poss live_poss;
    1.51      val kill_ns = map length kill_poss;
    1.52      val (inners', accum') =
    1.53 -      @{fold_map 5} (fn i => permute_and_kill (qualify i))
    1.54 -        (if length bnfs = 1 then [0] else (1 upto length bnfs))
    1.55 +      @{fold_map 5} (permute_and_kill_bnf o qualify)
    1.56 +        (if length bnfs = 1 then [0] else 1 upto length bnfs)
    1.57          kill_ns before_kill_src before_kill_dest bnfs accum;
    1.58  
    1.59      val Ass' = map2 (map o nth) Ass live_poss;
    1.60 @@ -653,7 +673,7 @@
    1.61      val after_lift_src = map2 append new_poss old_poss;
    1.62      val lift_ns = map (fn xs => length As - length xs) Ass';
    1.63    in
    1.64 -    ((kill_poss, As), @{fold_map 5} (fn i => lift_and_permute (qualify i))
    1.65 +    ((kill_poss, As), @{fold_map 5} (lift_and_permute_bnf o qualify)
    1.66        (if length bnfs = 1 then [0] else 1 upto length bnfs)
    1.67        lift_ns after_lift_src after_lift_dest inners' accum')
    1.68    end;
    1.69 @@ -881,7 +901,7 @@
    1.70      val map_b = def_qualify (mk_prefix_binding mapN);
    1.71      val rel_b = def_qualify (mk_prefix_binding relN);
    1.72      val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)]
    1.73 -      else map (fn i => def_qualify (mk_prefix_binding (mk_setN i))) (1 upto live);
    1.74 +      else map (def_qualify o mk_prefix_binding o mk_setN) (1 upto live);
    1.75  
    1.76      val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs)
    1.77        |> map (fn (b, def) => ((b, []), [([def], [])]))
    1.78 @@ -938,7 +958,7 @@
    1.79              val ((inners, (Dss, Ass)), (accum', lthy')) =
    1.80                apfst (apsnd split_list o split_list)
    1.81                  (@{fold_map 2} (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
    1.82 -                (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' accum);
    1.83 +                (if length Ts' = 1 then [0] else 1 upto length Ts') Ts' accum);
    1.84            in
    1.85              compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy')
    1.86            end)