# HG changeset patch
# User haftmann
# Date 1676184359 0
# Node ID 6cad6ed2700abf2d7e1540ecb854a85ca2096dc4
# Parent  04571037ed3310a32c03d8f6c5e82284120d8d3b
somehow more clear terminology

diff -r 04571037ed33 -r 6cad6ed2700a src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Feb 12 06:45:58 2023 +0000
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Feb 12 06:45:59 2023 +0000
@@ -671,7 +671,7 @@
     fun imp_monad_bind' (const as { sym = Code_Symbol.Constant c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
        of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
         | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
-        | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
+        | (ts, _) => imp_monad_bind (satisfied_application 2 (const, ts))
       else IConst const `$$ map imp_monad_bind ts
     and imp_monad_bind (IConst const) = imp_monad_bind' const []
       | imp_monad_bind (t as IVar _) = t
diff -r 04571037ed33 -r 6cad6ed2700a src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sun Feb 12 06:45:58 2023 +0000
+++ b/src/Tools/Code/code_haskell.ML	Sun Feb 12 06:45:59 2023 +0000
@@ -241,11 +241,11 @@
                     str "=",
                     print_app tyvars (SOME thm) reserved NOBR (const, [])
                   ]
-              | SOME (k, Code_Printer.Complex_printer _) =>
+              | SOME (wanted, Code_Printer.Complex_printer _) =>
                   let
                     val { sym = Constant c, dom, ... } = const;
                     val (vs, rhs) = (apfst o map) fst
-                      (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
+                      (Code_Thingol.unfold_abs (Code_Thingol.satisfied_application wanted (const, [])));
                     val s = if (is_some o const_syntax) c
                       then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
                     val vars = reserved
diff -r 04571037ed33 -r 6cad6ed2700a src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Feb 12 06:45:58 2023 +0000
+++ b/src/Tools/Code/code_ml.ML	Sun Feb 12 06:45:59 2023 +0000
@@ -123,17 +123,17 @@
                 then print_case is_pseudo_fun some_thm vars fxy case_expr
                 else print_app is_pseudo_fun some_thm vars fxy app
             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
-    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) =
       if is_constr sym then
-        let val k = length dom in
-          if k < 2 orelse length ts = k
+        let val wanted = length dom in
+          if wanted < 2 orelse length ts = wanted
           then (str o deresolve) sym
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
-          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
+          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.satisfied_application wanted app)]
         end
       else if is_pseudo_fun sym
         then (str o deresolve) sym @@ str "()"
-      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
+      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
         @ map (print_term is_pseudo_fun some_thm vars BR) ts
     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
       (print_term is_pseudo_fun) const_syntax some_thm vars
@@ -446,17 +446,17 @@
                 then print_case is_pseudo_fun some_thm vars fxy case_expr
                 else print_app is_pseudo_fun some_thm vars fxy app
             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
-    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts = dss, dom = dom, ... }, ts)) =
+    and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) =
       if is_constr sym then
-        let val k = length dom in
-          if length ts = k
+        let val wanted = length dom in
+          if length ts = wanted
           then (str o deresolve) sym
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
-          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
+          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.satisfied_application wanted app)]
         end
       else if is_pseudo_fun sym
         then (str o deresolve) sym @@ str "()"
-      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dss
+      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
         @ map (print_term is_pseudo_fun some_thm vars BR) ts
     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
       (print_term is_pseudo_fun) const_syntax some_thm vars
diff -r 04571037ed33 -r 6cad6ed2700a src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Sun Feb 12 06:45:58 2023 +0000
+++ b/src/Tools/Code/code_printer.ML	Sun Feb 12 06:45:59 2023 +0000
@@ -325,17 +325,17 @@
       NONE => brackify fxy (print_app_expr some_thm vars app)
     | SOME (_, Plain_printer s) =>
         brackify fxy (str s :: map (print_term some_thm vars BR) ts)
-    | SOME (k, Complex_printer print) =>
+    | SOME (wanted, Complex_printer print) =>
         let
           fun print' fxy ts =
-            print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
+            print (print_term some_thm) some_thm vars fxy (ts ~~ take wanted dom);
         in
-          if k = length ts
+          if wanted = length ts
           then print' fxy ts
-          else if k < length ts
-          then case chop k ts of (ts1, ts2) =>
+          else if wanted < length ts
+          then case chop wanted ts of (ts1, ts2) =>
             brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
-          else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
+          else print_term some_thm vars fxy (Code_Thingol.satisfied_application wanted app)
         end)
   | _ => brackify fxy (print_app_expr some_thm vars app);
 
diff -r 04571037ed33 -r 6cad6ed2700a src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sun Feb 12 06:45:58 2023 +0000
+++ b/src/Tools/Code/code_scala.ML	Sun Feb 12 06:45:59 2023 +0000
@@ -117,7 +117,6 @@
     and print_app tyvars is_pat some_thm vars fxy
         (app as ({ sym, typargs, dom, dicts, ... }, ts)) =
       let
-        val k = length ts;
         val typargs' = if is_pat then [] else typargs;
         val syntax = case sym of
             Constant const => const_syntax const
@@ -127,7 +126,7 @@
             orelse Code_Thingol.unambiguous_dictss dicts
           then fn p => K p
           else applify_dictss tyvars;
-        val (l, print') = case syntax of
+        val (wanted, print') = case syntax of
             NONE => (args_num sym, fn fxy => fn ts => applify_dicts
               (gen_applify (is_constr sym) "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
@@ -141,11 +140,11 @@
           | SOME (k, Complex_printer print) =>
               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
                 (ts ~~ take k dom))
-      in if k = l then print' fxy ts
-      else if k < l then
-        print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
+      in if length ts = wanted then print' fxy ts
+      else if length ts < wanted then
+        print_term tyvars is_pat some_thm vars fxy (Code_Thingol.satisfied_application wanted app)
       else let
-        val (ts1, ts23) = chop l ts;
+        val (ts1, ts23) = chop wanted ts;
       in
         Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
           [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
diff -r 04571037ed33 -r 6cad6ed2700a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Feb 12 06:45:58 2023 +0000
+++ b/src/Tools/Code/code_thingol.ML	Sun Feb 12 06:45:59 2023 +0000
@@ -57,7 +57,7 @@
   val unfold_const_app: iterm -> (const * iterm list) option
   val is_IVar: iterm -> bool
   val is_IAbs: iterm -> bool
-  val eta_expand: int -> const * iterm list -> iterm
+  val satisfied_application: int -> const * iterm list -> iterm
   val contains_dict_var: iterm -> bool
   val unambiguous_dictss: dict list list -> bool
   val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list
@@ -266,7 +266,7 @@
         val vs = map fst (invent_params (declare_varnames t) tys);
       in (vs, t `$$ map IVar vs) end;
 
-fun eta_expand wanted (const as { dom = tys, ... }, ts) =
+fun satisfied_application wanted (const as { dom = tys, ... }, ts) =
   let
     val given = length ts;
     val delta = wanted - given;