refactored triplicated functionality
authorblanchet
Tue May 28 22:20:25 2013 +0200 (2013-05-28)
changeset 52208ff8725b21a43
parent 52207 21026c312cc3
child 52209 8b2c3e548a20
refactored triplicated functionality
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 28 21:17:48 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 28 22:20:25 2013 +0200
     1.3 @@ -245,6 +245,9 @@
     1.4  
     1.5  val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
     1.6  
     1.7 +fun meta_unzip_rec getT proj1 proj2 fpTs y =
     1.8 +  if exists_subtype_in fpTs (getT y) then ([proj1 y], [proj2 y]) else ([y], []);
     1.9 +
    1.10  fun unzip_recT fpTs T =
    1.11    let
    1.12      fun project_recT proj =
    1.13 @@ -255,7 +258,7 @@
    1.14            | project T = T;
    1.15        in project end;
    1.16    in
    1.17 -    if exists_subtype_in fpTs T then ([project_recT fst T], [project_recT snd T]) else ([T], [])
    1.18 +    meta_unzip_rec I (project_recT fst) (project_recT snd) fpTs T
    1.19    end;
    1.20  
    1.21  fun mk_fold_fun_typess y_Tsss Cs = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
    1.22 @@ -452,12 +455,10 @@
    1.23        | mk_U proj (Type (s, Ts)) = Type (s, map (mk_U proj) Ts)
    1.24        | mk_U _ T = T;
    1.25  
    1.26 -    fun unzip_rec (x as Free (_, T)) =
    1.27 -      if exists_subtype_in fpTs T then
    1.28 -        ([build_prod_proj fst_const (T, mk_U fst T) $ x],
    1.29 -         [build_prod_proj snd_const (T, mk_U snd T) $ x])
    1.30 -      else
    1.31 -        ([x], []);
    1.32 +    val unzip_rec =
    1.33 +      meta_unzip_rec (snd o dest_Free)
    1.34 +        (fn x as Free (_, T) => build_prod_proj fst_const (T, mk_U fst T) $ x)
    1.35 +        (fn x as Free (_, T) => build_prod_proj snd_const (T, mk_U snd T) $ x) fpTs;
    1.36  
    1.37      fun mk_iter_arg f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f (flat_rec unzip_rec xs);
    1.38    in
    1.39 @@ -683,14 +684,14 @@
    1.40  
    1.41          val mk_U = typ_subst_nonatomic (map2 pair fpTs Cs);
    1.42  
    1.43 -        fun unzip_iters fiters combine (x as Free (_, T)) =
    1.44 -          if exists_subtype_in fpTs T then
    1.45 -            combine (x, build_map lthy (indexify_fst fpTs (K o nth fiters)) (T, mk_U T) $ x)
    1.46 -          else
    1.47 -            ([x], []);
    1.48 +        fun unzip_iters fiters =
    1.49 +          meta_unzip_rec (snd o dest_Free) I
    1.50 +            (fn x as Free (_, T) => build_map lthy (indexify_fst fpTs (K o nth fiters))
    1.51 +              (T, mk_U T) $ x) fpTs;
    1.52  
    1.53 -        val gxsss = map (map (flat_rec (unzip_iters gfolds (fn (_, t) => ([t], []))))) xsss;
    1.54 -        val hxsss = map (map (flat_rec (unzip_iters hrecs (pairself single)))) xsss;
    1.55 +        val gxsss = map (map (flat_rec ((fn (ts, ts') => ([hd (ts' @ ts)], [])) o
    1.56 +          unzip_iters gfolds))) xsss;
    1.57 +        val hxsss = map (map (flat_rec (unzip_iters hrecs))) xsss;
    1.58  
    1.59          val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
    1.60          val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;