--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Mar 24 18:30:17 2023 +0000
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Mar 24 18:30:17 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 (satisfied_application 2 (const, ts))
+ | (ts, _) => imp_monad_bind (saturated_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 Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_haskell.ML Fri Mar 24 18:30:17 2023 +0000
@@ -244,8 +244,9 @@
| SOME (wanted, Code_Printer.Complex_printer _) =>
let
val { sym = Constant c, dom, range, ... } = const;
- val (vs, rhs) = (apfst o map) fst
- (Code_Thingol.unfold_abs (Code_Thingol.satisfied_application wanted (const, [])));
+ val ((vs_tys, (ts, _)), _) = Code_Thingol.satisfied_application wanted (const, []);
+ val vs = map fst vs_tys;
+ val rhs = IConst const `$$ ts;
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 Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_ml.ML Fri Mar 24 18:30:17 2023 +0000
@@ -129,7 +129,7 @@
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.satisfied_application wanted app)]
+ else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)]
end
else if is_pseudo_fun sym
then (str o deresolve) sym @@ str "()"
@@ -452,7 +452,7 @@
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.satisfied_application wanted app)]
+ else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)]
end
else if is_pseudo_fun sym
then (str o deresolve) sym @@ str "()"
--- a/src/Tools/Code/code_printer.ML Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_printer.ML Fri Mar 24 18:30:17 2023 +0000
@@ -319,23 +319,26 @@
(n, Complex_printer (f literals));
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
- (app as ({ sym, dom, ... }, ts)) =
+ (app as (const as { sym, dom, ... }, ts)) =
case sym of
- Constant const => (case const_syntax const of
+ Constant name => (case const_syntax name of
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 (wanted, Complex_printer print) =>
let
- fun print' fxy ts =
- print (print_term some_thm) some_thm vars fxy (ts ~~ take wanted dom);
+ val ((vs_tys, (ts1, rty)), ts2) =
+ Code_Thingol.satisfied_application wanted app;
+ fun print' fxy =
+ print (print_term some_thm) some_thm vars fxy (ts1 ~~ take wanted dom);
in
- if wanted = length ts
- then print' fxy ts
- 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.satisfied_application wanted app)
+ if null vs_tys then
+ if null ts2 then
+ print' fxy
+ else
+ brackify fxy (print' APP :: map (print_term some_thm vars BR) ts2)
+ else
+ print_term some_thm vars fxy (vs_tys `|==> (IConst const `$$ ts1, rty))
end)
| _ => brackify fxy (print_app_expr some_thm vars app);
--- a/src/Tools/Code/code_scala.ML Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_scala.ML Fri Mar 24 18:30:17 2023 +0000
@@ -115,7 +115,7 @@
], vars')
end
and print_app tyvars is_pat some_thm vars fxy
- (app as ({ sym, typargs, dom, dicts, ... }, ts)) =
+ (app as (const as { sym, typargs, dom, dicts, ... }, ts)) =
let
val typargs' = if is_pat then [] else typargs;
val syntax = case sym of
@@ -140,15 +140,18 @@
| 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 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 wanted ts;
+ val ((vs_tys, (ts1, rty)), ts2) =
+ Code_Thingol.satisfied_application wanted app;
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)
- end end
+ if null vs_tys then
+ if null ts2 then
+ print' fxy ts
+ else
+ Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
+ [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts2)
+ else
+ print_term tyvars is_pat some_thm vars fxy (vs_tys `|==> (IConst const `$$ ts1, rty))
+ end
and print_bind tyvars some_thm fxy p =
gen_print_bind (print_term tyvars true) some_thm fxy p
and print_case tyvars some_thm vars fxy { clauses = [], ... } =
--- a/src/Tools/Code/code_thingol.ML Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_thingol.ML Fri Mar 24 18:30:17 2023 +0000
@@ -58,7 +58,9 @@
val unfold_const_app: iterm -> (const * iterm list) option
val is_IVar: iterm -> bool
val is_IAbs: iterm -> bool
- val satisfied_application: int -> const * iterm list -> iterm
+ val satisfied_application: int -> const * iterm list
+ -> ((vname option * itype) list * (iterm list * itype)) * iterm list
+ val saturated_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
@@ -277,14 +279,29 @@
val vs = map fst (invent_params (declare_varnames t) tys);
in (vs, t `$$ map IVar vs) end;
-fun satisfied_application wanted (const as { dom, range, ... }, ts) =
+fun satisfied_application wanted ({ dom, range, ... }, ts) =
let
val given = length ts;
val delta = wanted - given;
- val vs_tys = invent_params (fold declare_varnames ts)
- (((take delta o drop given) dom));
val (_, rty) = unfold_fun_n wanted range;
- in vs_tys `|==> (IConst const `$$ ts @ map (IVar o fst) vs_tys, rty) end;
+ in
+ if delta = 0 then
+ (([], (ts, rty)), [])
+ else if delta < 0 then
+ let
+ val (ts1, ts2) = chop wanted ts
+ in (([], (ts1, rty)), ts2) end
+ else
+ let
+ val vs_tys = invent_params (fold declare_varnames ts)
+ (((take delta o drop given) dom));
+ in ((vs_tys, (ts @ map (IVar o fst) vs_tys, rty)), []) end
+ end
+
+fun saturated_application wanted (const, ts) =
+ let
+ val ((vs_tys, (ts', rty)), []) = satisfied_application wanted (const, ts)
+ in vs_tys `|==> (IConst const `$$ ts', rty) end
fun map_terms_bottom_up f (t as IConst _) = f t
| map_terms_bottom_up f (t as IVar _) = f t