# HG changeset patch
# User blanchet
# Date 1482320955 -3600
# Node ID 8d7cb22482e399357d7a758f5316804561e93365
# Parent  f6d0578b46c9b4f36f4c495dc54d6717a45958a0
generalized ML function (towards nonuniform datatypes)

diff -r f6d0578b46c9 -r 8d7cb22482e3 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Dec 21 11:45:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Dec 21 12:49:15 2016 +0100
@@ -122,9 +122,9 @@
   val mk_pred: typ list -> term -> term
   val mk_rel: int -> typ list -> typ list -> term -> term
   val mk_set: typ list -> term -> term
-  val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term
-  val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> (typ * typ -> term) ->
-    typ * typ -> term
+  val build_map: Proof.context -> typ list -> typ list -> (typ * typ -> term) -> typ * typ -> term
+  val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> typ list ->
+    (typ * typ -> term) -> typ * typ -> term
   val build_set: Proof.context -> typ -> typ -> term
   val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list
   val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list ->
@@ -744,12 +744,13 @@
     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   end;
 
-fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simple_Ts build_simple =
+fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simple_Ts simple_Us build_simple =
   let
     fun build (TU as (T, U)) =
-      if exists (curry (op =) T) simple_Ts then
+      if exists (curry (op =) T) simple_Ts orelse exists (curry (op =) U) simple_Us then
         build_simple TU
-      else if T = U andalso not (exists_subtype_in simple_Ts T) then
+      else if T = U andalso not (exists_subtype_in simple_Ts T) andalso
+          not (exists_subtype_in simple_Us U) then
         const T
       else
         (case TU of
diff -r f6d0578b46c9 -r 8d7cb22482e3 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Dec 21 11:45:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Dec 21 12:49:15 2016 +0100
@@ -530,7 +530,7 @@
   Option.map (rapp u o rapp t) (choose_binary_fun fs (fastype_of t, fastype_of u));
 
 fun build_the_rel ctxt Rs Ts A B =
-  build_rel [] ctxt Ts (the o choose_binary_fun Rs) (A, B);
+  build_rel [] ctxt Ts [] (the o choose_binary_fun Rs) (A, B);
 fun build_rel_app ctxt Rs Ts t u =
   build_the_rel ctxt Rs Ts (fastype_of t) (fastype_of u) $ t $ u;
 
@@ -860,7 +860,7 @@
 
                 fun mk_arg (x as Free (_, T)) (Free (_, U)) =
                   if T = U then x
-                  else build_map lthy [] (the o AList.lookup (op =) ABfs) (T, U) $ x;
+                  else build_map lthy [] [] (the o AList.lookup (op =) ABfs) (T, U) $ x;
 
                 val xs' = map2 mk_arg xs ys;
               in
@@ -1242,7 +1242,7 @@
                 val lhsT = fastype_of lhs;
                 val map_rhsT =
                   map_atyps (perhaps (AList.lookup (op =) (map swap live_AsBs))) lhsT;
-                val map_rhs = build_map lthy []
+                val map_rhs = build_map lthy [] []
                   (the o (AList.lookup (op =) (live_AsBs ~~ fs))) (map_rhsT, lhsT);
                 val rhs = (case map_rhs of
                     Const (@{const_name id}, _) => selA $ ta
@@ -1539,7 +1539,7 @@
 
     val cpss = map2 (map o rapp) cs pss;
 
-    fun build_sum_inj mk_inj = build_map ctxt [] (uncurry mk_inj o dest_sumT o snd);
+    fun build_sum_inj mk_inj = build_map ctxt [] [] (uncurry mk_inj o dest_sumT o snd);
 
     fun build_dtor_corec_arg _ [] [cg] = cg
       | build_dtor_corec_arg T [cq] [cg, cg'] =
@@ -1796,7 +1796,7 @@
                 indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
                   (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk));
             in
-              build_map lthy [] build_simple (T, U) $ x
+              build_map lthy [] [] build_simple (T, U) $ x
             end;
 
         val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
@@ -2070,7 +2070,7 @@
         fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
 
     fun build_the_rel rs' T Xs_T =
-      build_rel [] ctxt [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
+      build_rel [] ctxt [] [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
       |> Term.subst_atomic_types (Xs ~~ fpTs);
 
     fun build_rel_app rs' usel vsel Xs_T =
@@ -2181,7 +2181,7 @@
                   indexify fst (map2 (curry mk_sumT) fpTs Cs)
                     (fn kk => fn _ => tack (nth cs kk, nth us kk) (nth gcorecs kk));
               in
-                build_map ctxt [] build_simple (T, U) $ cqg
+                build_map ctxt [] [] build_simple (T, U) $ cqg
               end
             else
               cqg
@@ -2594,7 +2594,7 @@
 
           fun mk_rec_arg_arg (x as Free (_, T)) =
             let val U = B_ify_T T in
-              if T = U then x else build_map lthy [] (the o AList.lookup (op =) ABfs) (T, U) $ x
+              if T = U then x else build_map lthy [] [] (the o AList.lookup (op =) ABfs) (T, U) $ x
             end;
 
           fun mk_rec_o_map_arg rec_arg_T h =
@@ -2747,8 +2747,10 @@
               val T = range_type (fastype_of g);
               val U = range_type corec_argB_T;
             in
-              if T = U then g
-              else HOLogic.mk_comp (build_map lthy2 [] (the o AList.lookup (op =) ABfs) (T, U), g)
+              if T = U then
+                g
+              else
+                HOLogic.mk_comp (build_map lthy2 [] [] (the o AList.lookup (op =) ABfs) (T, U), g)
             end;
 
           fun mk_map_o_corec_rhs corecx =
diff -r f6d0578b46c9 -r 8d7cb22482e3 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Wed Dec 21 11:45:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Wed Dec 21 12:49:15 2016 +0100
@@ -1005,8 +1005,8 @@
 
     val simple_Ts = map fst simple_T_mapfs;
 
-    val t_map = build_map ctxt simple_Ts build_simple (apply2 (range_type o fastype_of) (t, u));
-    val u_map = build_map ctxt simple_Ts build_simple (apply2 (domain_type o fastype_of) (t, u));
+    val t_map = build_map ctxt simple_Ts [] build_simple (apply2 (range_type o fastype_of) (t, u));
+    val u_map = build_map ctxt simple_Ts [] build_simple (apply2 (domain_type o fastype_of) (t, u));
   in
     mk_Trueprop_eq (HOLogic.mk_comp (u, u_map), HOLogic.mk_comp (t_map, t))
   end;
diff -r f6d0578b46c9 -r 8d7cb22482e3 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Dec 21 11:45:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Dec 21 12:49:15 2016 +0100
@@ -587,7 +587,7 @@
       ||>> mk_Frees "y" xy_Ts;
 
     fun mk_prem xy_T x y =
-      build_rel [] ctxt [fpT] (fn (T, _) => if T = fpT then Rcong else HOLogic.eq_const T)
+      build_rel [] ctxt [fpT] [] (fn (T, _) => if T = fpT then Rcong else HOLogic.eq_const T)
         (xy_T, xy_T) $ x $ y;
 
     val prems = @{map 3} mk_prem xy_Ts xs ys;
@@ -713,7 +713,7 @@
         |> explore {bound_Us = T :: bound_Us, bound_Ts = T :: bound_Ts, U = U, T = T}
         |> (fn t => Abs (Name.uu, T, t));
   in
-    betapply (build_map lthy [] build_simple (T, U), t)
+    betapply (build_map lthy [] [] build_simple (T, U), t)
   end;
 
 fun add_boundvar t = betapply (incr_boundvars 1 t, Bound 0);
@@ -1047,7 +1047,7 @@
         val param2_T = Type_Infer.paramify_vars param1_T;
 
         val deadfixed_T =
-          build_map lthy [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
+          build_map lthy [] [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
           |> singleton (Type_Infer_Context.infer_types lthy)
           |> singleton (Type_Infer.fixate lthy false)
           |> type_of
diff -r f6d0578b46c9 -r 8d7cb22482e3 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Wed Dec 21 11:45:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Wed Dec 21 12:49:15 2016 +0100
@@ -209,7 +209,7 @@
       if op = TU then
         t
       else
-        (case try (build_map ctxt [] (the o AList.lookup (op =) AB_fs)) TU of
+        (case try (build_map ctxt [] [] (the o AList.lookup (op =) AB_fs)) TU of
           SOME mapx => mapx $ t
         | NONE => raise UNNATURAL ());
 
@@ -356,7 +356,7 @@
     fun mk_friend_spec () =
       let
         fun encapsulate_nested U T free =
-          betapply (build_map ctxt [] (fn (T, _) =>
+          betapply (build_map ctxt [] [] (fn (T, _) =>
               if T = domain_type VLeaf0_T then Abs (Name.uu, T, VLeaf0 $ Bound 0)
               else Abs (Name.uu, T, Bound 0)) (T, U),
             free);
diff -r f6d0578b46c9 -r 8d7cb22482e3 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Dec 21 11:45:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Dec 21 12:49:15 2016 +0100
@@ -962,7 +962,7 @@
           end;
 
       fun massage_noncall U T t =
-        build_map ctxt [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t;
+        build_map ctxt [] [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t;
 
       val bound_Ts = List.rev (map fastype_of fun_args);
     in
diff -r f6d0578b46c9 -r 8d7cb22482e3 src/HOL/Tools/BNF/bnf_lfp_countable.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Wed Dec 21 11:45:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Wed Dec 21 12:49:15 2016 +0100
@@ -106,7 +106,7 @@
         NONE
       else if exists_subtype_in fpTs T then
         let val U = mk_U T in
-          SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
+          SOME (mk_to_nat_checked U $ (build_map ctxt [] [] (snd_const o fst) (T, U) $ Bound j))
         end
       else
         SOME (mk_to_nat_checked T $ Bound j);
diff -r f6d0578b46c9 -r 8d7cb22482e3 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Wed Dec 21 11:45:16 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Wed Dec 21 12:49:15 2016 +0100
@@ -86,7 +86,7 @@
     fun check_no_call t = if has_call t then unexpected_rec_call ctxt [t0] t else ();
 
     val typof = curry fastype_of1 bound_Ts;
-    val massage_no_call = build_map ctxt [] massage_nonfun;
+    val massage_no_call = build_map ctxt [] [] massage_nonfun;
 
     val yT = typof y;
     val yU = typof y';