started working on compatibility with old package's recursor
authorblanchet
Fri Apr 26 14:14:52 2013 +0200 (2013-04-26)
changeset 5179322f22172a361
parent 51790 22517d04d20b
child 51794 a1ffbc36323a
started working on compatibility with old package's recursor
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 12:09:51 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 14:14:52 2013 +0200
     1.3 @@ -76,6 +76,12 @@
     1.4  fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
     1.5  fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
     1.6  
     1.7 +(* This order is for compatibility with the old datatype package. *)
     1.8 +fun unzip_rec curryf xs =
     1.9 +  let val ps = map curryf xs in
    1.10 +    map fst ps @ map_filter snd ps
    1.11 +  end;
    1.12 +
    1.13  fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
    1.14    Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1));
    1.15  
    1.16 @@ -358,13 +364,13 @@
    1.17              | proj_recT proj (Type (s, Ts)) = Type (s, map (proj_recT proj) Ts)
    1.18              | proj_recT _ T = T;
    1.19  
    1.20 -          fun unzip_recT T =
    1.21 -            if exists_fp_subtype T then [proj_recT fst T, proj_recT snd T] else [T];
    1.22 +          fun curry_recT T =
    1.23 +            if exists_fp_subtype T then (proj_recT fst T, SOME (proj_recT snd T)) else (T, NONE);
    1.24  
    1.25            val z_Tsss =
    1.26              map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type)
    1.27                ns mss fp_rec_fun_Ts;
    1.28 -          val z_Tssss = map (map (map unzip_recT)) z_Tsss;
    1.29 +          val z_Tssss = map (map (unzip_rec curry_recT)) z_Tsss;
    1.30            val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css;
    1.31  
    1.32            val hss = map2 (map2 retype_free) h_Tss gss;
    1.33 @@ -636,14 +642,15 @@
    1.34                | mk_U proj (Type (s, Ts)) = Type (s, map (mk_U proj) Ts)
    1.35                | mk_U _ T = T;
    1.36  
    1.37 -            fun unzip_rec (x as Free (_, T)) =
    1.38 +            fun curry_rec (x as Free (_, T)) =
    1.39                if exists_fp_subtype T then
    1.40 -                [build_prod_proj fst_const (T, mk_U fst T) $ x,
    1.41 -                 build_prod_proj snd_const (T, mk_U snd T) $ x]
    1.42 +                (build_prod_proj fst_const (T, mk_U fst T) $ x,
    1.43 +                 SOME (build_prod_proj snd_const (T, mk_U snd T) $ x))
    1.44                else
    1.45 -                [x];
    1.46 +                (x, NONE);
    1.47  
    1.48 -            fun mk_rec_like_arg f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f (maps unzip_rec xs);
    1.49 +            fun mk_rec_like_arg f xs =
    1.50 +              mk_tupled_fun (HOLogic.mk_tuple xs) f (flat (unzip_rec curry_rec xs));
    1.51  
    1.52              fun generate_rec_like (suf, fp_rec_like, (fss, f_Tss, xsss)) =
    1.53                let