--- 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
--- 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
--- 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
--- 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);
--- 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)
--- 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;