# HG changeset patch # User haftmann # Date 1679682617 0 # Node ID 0262155d2743ac98d3522445165b5958a90c87ad # Parent b5fbe9837aee460b3703932d61f7d94f2529be3a more uniform approach towards satisfied applications diff -r b5fbe9837aee -r 0262155d2743 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 diff -r b5fbe9837aee -r 0262155d2743 src/Tools/Code/code_haskell.ML --- 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 diff -r b5fbe9837aee -r 0262155d2743 src/Tools/Code/code_ml.ML --- 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 "()" diff -r b5fbe9837aee -r 0262155d2743 src/Tools/Code/code_printer.ML --- 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); diff -r b5fbe9837aee -r 0262155d2743 src/Tools/Code/code_scala.ML --- 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 = [], ... } = diff -r b5fbe9837aee -r 0262155d2743 src/Tools/Code/code_thingol.ML --- 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