# HG changeset patch
# User blanchet
# Date 1381735902 -7200
# Node ID 82ada0a92ddea10b59e532e6ec0b9a8430dc63cb
# Parent  94f2dc9aea7a28496b14ad33beecf16dedd93f11
tuned names

diff -r 94f2dc9aea7a -r 82ada0a92dde src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 14 09:17:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 14 09:31:42 2013 +0200
@@ -168,13 +168,13 @@
     subst (SOME ~1)
   end;
 
-fun subst_rec_calls lthy get_ctr_pos has_call ctr_args direct_calls indirect_calls t =
+fun subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls t =
   let
     fun subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
       | subst bound_Ts (t as g' $ y) =
         let
-          val maybe_direct_y' = AList.lookup (op =) direct_calls y;
-          val maybe_indirect_y' = AList.lookup (op =) indirect_calls y;
+          val maybe_mutual_y' = AList.lookup (op =) mutual_calls y;
+          val maybe_nested_y' = AList.lookup (op =) nested_calls y;
           val (g, g_args) = strip_comb g';
           val ctr_pos = try (get_ctr_pos o the) (free_name g) |> the_default ~1;
           val _ = ctr_pos < 0 orelse length g_args >= ctr_pos orelse
@@ -183,11 +183,11 @@
           if not (member (op =) ctr_args y) then
             pairself (subst bound_Ts) (g', y) |> (op $)
           else if ctr_pos >= 0 then
-            list_comb (the maybe_direct_y', g_args)
-          else if is_some maybe_indirect_y' then
+            list_comb (the maybe_mutual_y', g_args)
+          else if is_some maybe_nested_y' then
             (if has_call g' then t else y)
-            |> massage_indirect_rec_call lthy has_call
-              (rewrite_map_arg get_ctr_pos) bound_Ts y (the maybe_indirect_y')
+            |> massage_nested_rec_call lthy has_call
+              (rewrite_map_arg get_ctr_pos) bound_Ts y (the maybe_nested_y')
             |> (if has_call g' then I else curry (op $) g')
           else
             t
@@ -208,25 +208,25 @@
       val ctr_args = #ctr_args eqn_data;
 
       val calls = #calls ctr_spec;
-      val n_args = fold (curry (op +) o (fn Direct_Rec _ => 2 | _ => 1)) calls 0;
+      val n_args = fold (curry (op +) o (fn Mutual_Rec _ => 2 | _ => 1)) calls 0;
 
       val no_calls' = tag_list 0 calls
-        |> map_filter (try (apsnd (fn No_Rec n => n | Direct_Rec (n, _) => n)));
-      val direct_calls' = tag_list 0 calls
-        |> map_filter (try (apsnd (fn Direct_Rec (_, n) => n)));
-      val indirect_calls' = tag_list 0 calls
-        |> map_filter (try (apsnd (fn Indirect_Rec n => n)));
+        |> map_filter (try (apsnd (fn No_Rec n => n | Mutual_Rec (n, _) => n)));
+      val mutual_calls' = tag_list 0 calls
+        |> map_filter (try (apsnd (fn Mutual_Rec (_, n) => n)));
+      val nested_calls' = tag_list 0 calls
+        |> map_filter (try (apsnd (fn Nested_Rec n => n)));
 
-      fun make_direct_type _ = dummyT; (* FIXME? *)
+      fun make_mutual_type _ = dummyT; (* FIXME? *)
 
       val rec_res_type_list = map (fn (x :: _) => (#rec_type x, #res_type x)) funs_data;
 
-      fun make_indirect_type (Type (Tname, Ts)) = Type (Tname, Ts |> map (fn T =>
+      fun make_nested_type (Type (Tname, Ts)) = Type (Tname, Ts |> map (fn T =>
         let val maybe_res_type = AList.lookup (op =) rec_res_type_list T in
           if is_some maybe_res_type
           then HOLogic.mk_prodT (T, the maybe_res_type)
-          else make_indirect_type T end))
-        | make_indirect_type T = T;
+          else make_nested_type T end))
+        | make_nested_type T = T;
 
       val args = replicate n_args ("", dummyT)
         |> Term.rename_wrt_term t
@@ -235,22 +235,22 @@
             nth_map arg_idx (K (nth ctr_args ctr_arg_idx)))
           no_calls'
         |> fold (fn (ctr_arg_idx, arg_idx) =>
-            nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_direct_type)))
-          direct_calls'
+            nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_mutual_type)))
+          mutual_calls'
         |> fold (fn (ctr_arg_idx, arg_idx) =>
-            nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_indirect_type)))
-          indirect_calls';
+            nth_map arg_idx (K (nth ctr_args ctr_arg_idx |> map_types make_nested_type)))
+          nested_calls';
 
       val fun_name_ctr_pos_list =
         map (fn (x :: _) => (#fun_name x, length (#left_args x))) funs_data;
       val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1;
-      val direct_calls = map (apfst (nth ctr_args) o apsnd (nth args)) direct_calls';
-      val indirect_calls = map (apfst (nth ctr_args) o apsnd (nth args)) indirect_calls';
+      val mutual_calls = map (apfst (nth ctr_args) o apsnd (nth args)) mutual_calls';
+      val nested_calls = map (apfst (nth ctr_args) o apsnd (nth args)) nested_calls';
 
       val abstractions = args @ #left_args eqn_data @ #right_args eqn_data;
     in
       t
-      |> subst_rec_calls lthy get_ctr_pos has_call ctr_args direct_calls indirect_calls
+      |> subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls
       |> fold_rev lambda abstractions
     end;
 
@@ -671,7 +671,7 @@
   |> the_default undef_const
   |> K;
 
-fun build_corec_args_direct_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
+fun build_corec_args_mutual_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
   let
     val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
   in
@@ -683,7 +683,7 @@
       fun rewrite_g _ t = if has_call t then undef_const else t;
       fun rewrite_h bound_Ts t =
         if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const;
-      fun massage f _ = massage_direct_corec_call lthy has_call f bound_Ts rhs_term
+      fun massage f _ = massage_mutual_corec_call lthy has_call f bound_Ts rhs_term
         |> abs_tuple fun_args;
     in
       (massage rewrite_q,
@@ -692,7 +692,7 @@
     end
   end;
 
-fun build_corec_arg_indirect_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
+fun build_corec_arg_nested_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
   let
     val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
   in
@@ -714,7 +714,7 @@
           if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t;
       fun massage t =
         rhs_term
-        |> massage_indirect_corec_call lthy has_call rewrite bound_Ts (range_type (fastype_of t))
+        |> massage_nested_corec_call lthy has_call rewrite bound_Ts (range_type (fastype_of t))
         |> abs_tuple fun_args;
     in
       massage
@@ -729,16 +729,16 @@
         val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
 
         val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
-        val direct_calls' = map_filter (try (apsnd (fn Direct_Corec n => n))) sel_call_list;
-        val indirect_calls' = map_filter (try (apsnd (fn Indirect_Corec n => n))) sel_call_list;
+        val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list;
+        val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list;
       in
         I
         #> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls'
         #> fold (fn (sel, (q, g, h)) =>
-          let val (fq, fg, fh) = build_corec_args_direct_call lthy has_call sel_eqns sel in
-            nth_map q fq o nth_map g fg o nth_map h fh end) direct_calls'
+          let val (fq, fg, fh) = build_corec_args_mutual_call lthy has_call sel_eqns sel in
+            nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls'
         #> fold (fn (sel, n) => nth_map n
-          (build_corec_arg_indirect_call lthy has_call sel_eqns sel)) indirect_calls'
+          (build_corec_arg_nested_call lthy has_call sel_eqns sel)) nested_calls'
       end
   end;
 
diff -r 94f2dc9aea7a -r 82ada0a92dde src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Oct 14 09:17:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Oct 14 09:31:42 2013 +0200
@@ -10,14 +10,14 @@
 sig
   datatype rec_call =
     No_Rec of int |
-    Direct_Rec of int (*before*) * int (*after*) |
-    Indirect_Rec of int
+    Mutual_Rec of int (*before*) * int (*after*) |
+    Nested_Rec of int
 
   datatype corec_call =
     Dummy_No_Corec of int |
     No_Corec of int |
-    Direct_Corec of int (*stop?*) * int (*end*) * int (*continue*) |
-    Indirect_Corec of int
+    Mutual_Corec of int (*stop?*) * int (*end*) * int (*continue*) |
+    Nested_Corec of int
 
   type rec_ctr_spec =
     {ctr: term,
@@ -57,12 +57,12 @@
   val s_disjs: term list -> term
   val s_dnf: term list list -> term list
 
-  val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
+  val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     typ list -> term -> term -> term -> term
   val unfold_let: term -> term
-  val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
+  val massage_mutual_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
     typ list -> term -> term
-  val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
+  val massage_nested_corec_call: Proof.context -> (term -> bool) ->
     (typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term
   val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
   val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
@@ -92,14 +92,14 @@
 
 datatype rec_call =
   No_Rec of int |
-  Direct_Rec of int * int |
-  Indirect_Rec of int;
+  Mutual_Rec of int * int |
+  Nested_Rec of int;
 
 datatype corec_call =
   Dummy_No_Corec of int |
   No_Corec of int |
-  Direct_Corec of int * int * int |
-  Indirect_Corec of int;
+  Mutual_Corec of int * int * int |
+  Nested_Corec of int;
 
 type rec_ctr_spec =
   {ctr: term,
@@ -210,7 +210,7 @@
     permute_like (op aconv) flat_fs fs flat_fs'
   end;
 
-fun massage_indirect_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
+fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
   let
     val typof = curry fastype_of1 bound_Ts;
     val build_map_fst = build_map ctxt (fst_const o fst);
@@ -221,7 +221,7 @@
     fun y_of_y' () = build_map_fst (yU, yT) $ y';
     val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
 
-    fun massage_direct_fun U T t =
+    fun massage_mutual_fun U T t =
       if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
       else HOLogic.mk_comp (t, build_map_fst (U, T));
 
@@ -242,7 +242,7 @@
         if has_call t then unexpected_rec_call ctxt t else t
       else
         massage_map U T t
-        handle AINT_NO_MAP _ => massage_direct_fun U T t;
+        handle AINT_NO_MAP _ => massage_mutual_fun U T t;
 
     fun massage_call (t as t1 $ t2) =
         if t2 = y then
@@ -341,24 +341,24 @@
     massage_rec
   end;
 
-val massage_direct_corec_call = massage_let_if_case;
+val massage_mutual_corec_call = massage_let_if_case;
 
 fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T;
 
-fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
+fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t =
   let
     val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
 
-    fun massage_direct_call bound_Ts U T t =
+    fun massage_mutual_call bound_Ts U T t =
       if has_call t then factor_out_types ctxt (raw_massage_call bound_Ts) dest_sumT U T t
       else build_map_Inl (T, U) $ t;
 
-    fun massage_direct_fun bound_Ts U T t =
+    fun massage_mutual_fun bound_Ts U T t =
       let
         val var = Var ((Name.uu, Term.maxidx_of_term t + 1),
           domain_type (fastype_of1 (bound_Ts, t)));
       in
-        Term.lambda var (massage_direct_call bound_Ts U T (t $ var))
+        Term.lambda var (massage_mutual_call bound_Ts U T (t $ var))
       end;
 
     fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =
@@ -379,7 +379,7 @@
         if has_call t then unexpected_corec_call ctxt t else t
       else
         massage_map bound_Ts U T t
-        handle AINT_NO_MAP _ => massage_direct_fun bound_Ts U T t;
+        handle AINT_NO_MAP _ => massage_mutual_fun bound_Ts U T t;
 
     fun massage_call bound_Ts U T =
       massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
@@ -407,13 +407,13 @@
                 end
               | t1 $ t2 =>
                 (if has_call t2 then
-                  massage_direct_call bound_Ts U T t
+                  massage_mutual_call bound_Ts U T t
                 else
                   massage_map bound_Ts U T t1 $ t2
-                  handle AINT_NO_MAP _ => massage_direct_call bound_Ts U T t)
+                  handle AINT_NO_MAP _ => massage_mutual_call bound_Ts U T t)
               | Abs (s, T', t') =>
                 Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
-              | _ => massage_direct_call bound_Ts U T t))
+              | _ => massage_mutual_call bound_Ts U T t))
           | _ => ill_formed_corec_call ctxt t)
         else
           build_map_Inl (T, U) $ t) bound_Ts;
@@ -521,8 +521,8 @@
       | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
         length ctrs + offset_of_ctr (n - 1) ctr_sugars;
 
-    fun call_of [i] [T] = (if exists_subtype_in Cs T then Indirect_Rec else No_Rec) i
-      | call_of [i, i'] _ = Direct_Rec (i, i');
+    fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) i
+      | call_of [i, i'] _ = Mutual_Rec (i, i');
 
     fun mk_ctr_spec ctr offset fun_arg_Tss rec_thm =
       let
@@ -613,10 +613,10 @@
     val perm_Cs' = map substCT perm_Cs;
 
     fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] =
-        (if exists_subtype_in Cs T then Indirect_Corec
+        (if exists_subtype_in Cs T then Nested_Corec
          else if nullary then Dummy_No_Corec
          else No_Corec) g_i
-      | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
+      | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
 
     fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm
         disc_corec sel_corecs =