diff --git a/docs/src/learn/07-collections.md b/docs/src/learn/07-collections.md index 39811cb..5678be8 100644 --- a/docs/src/learn/07-collections.md +++ b/docs/src/learn/07-collections.md @@ -115,7 +115,7 @@ note: hole `?` has type `int -> int -> int` — try: min, max, const — or: fli 3 | let total = List.fold ? 0 ns | ^ -note: hole `?` has type `int` — try: total — or: List.sum ?, Seq.sum ?, String.len ?, round ? +note: hole `?` has type `int` — try: total — or: List.sum ?, Seq.sum ?, String.len ?, round ?, and 13 more --> 4:32 | 4 | let atTen = Option.withDefault ? (List.get 10 ns) diff --git a/docs/src/learn/09-typed-holes.md b/docs/src/learn/09-typed-holes.md index 13ed12c..8470baf 100644 --- a/docs/src/learn/09-typed-holes.md +++ b/docs/src/learn/09-typed-holes.md @@ -18,7 +18,7 @@ names |> headline |> print Running `pyfun check` reports the gap rather than a failure: ```console -note: hole `?upper` has type `'a -> string` — try: String.upper, input, String.trimStart, String.trimEnd, String.rev, String.ofList, and 9 more — or: String.repeat ?, String.concat ?, String.join ?, Option.withDefault ? +note: hole `?upper` has type `'a -> string` — try: String.upper, input, String.trimStart, String.trimEnd, String.rev, String.ofList, and 9 more — or: String.repeat ?, String.concat ?, String.join ?, Option.withDefault ?, and 18 more --> 5:15 | 5 | |> List.map ?upper @@ -27,7 +27,7 @@ note: hole `?upper` has type `'a -> string` — try: String.upper, input, String The hole needs a function producing a string, and `String.upper` is first under `try:`. It comes first because of the hole's name: a fit whose name matches the hole's goes to the front of the list, so naming a hole after what you want is a way of asking for it. The `or:` list names functions that would also fit if you filled their own holes. Replace `?upper` with `String.upper` and the program compiles and prints `ADA, GRACE, ALAN`. -The `try:` list shows six fits, and `and 9 more` says how many it left out. Hovering the module in your editor, or `:type` in the REPL, gives you the full surface. +The `try:` list shows six fits and the `or:` list shows four. The `and 9 more` and `and 18 more` at their ends say how many each one left out. Hovering the module in your editor, or `:type` in the REPL, gives you the full surface. This is the workflow: sketch the whole pipeline with holes, let the compiler name each gap's type, and fill inward from the types and the suggested fits. You never have to guess a function's signature, because the hole reports it for you, and a hole blocks compilation by design, so nothing runs until every blank is filled. @@ -36,7 +36,7 @@ This is the workflow: sketch the whole pipeline with holes, let the compiler nam Fill both holes. `report` looks a score up in a map, supplies a fallback when the name is absent, and turns the number into a string. `pyfun check` reports each hole with a `try:` value that fits. The first report is: ```console -note: hole `?render` has type `int -> 'a` — try: List.range, Seq.range, String.get, String.repeat, String.fromInt, String.fromFloat, and 59 more — or: String.slice ?, List.replicate ?, List.updateAt ?, List.insertAt ? +note: hole `?render` has type `int -> 'a` — try: List.range, Seq.range, String.get, String.repeat, String.fromInt, String.fromFloat, and 59 more — or: String.slice ?, List.replicate ?, List.updateAt ?, List.insertAt ?, and 16 more ``` ```pyfun diff --git a/docs/src/notebooks/07-collections.ipynb b/docs/src/notebooks/07-collections.ipynb index 86d6144..8e5268f 100644 --- a/docs/src/notebooks/07-collections.ipynb +++ b/docs/src/notebooks/07-collections.ipynb @@ -165,7 +165,7 @@ "3 | let total = List.fold ? 0 ns\n", " | ^\n", "\n", - "note: hole `?` has type `int` — try: total — or: List.sum ?, Seq.sum ?, String.len ?, round ?\n", + "note: hole `?` has type `int` — try: total — or: List.sum ?, Seq.sum ?, String.len ?, round ?, and 13 more\n", " --> 4:32\n", " |\n", "4 | let atTen = Option.withDefault ? (List.get 10 ns)\n", diff --git a/docs/src/notebooks/09-typed-holes.ipynb b/docs/src/notebooks/09-typed-holes.ipynb index 3c86b99..b825a6b 100644 --- a/docs/src/notebooks/09-typed-holes.ipynb +++ b/docs/src/notebooks/09-typed-holes.ipynb @@ -44,7 +44,7 @@ "Running `pyfun check` reports the gap rather than a failure:\n", "\n", "```console\n", - "note: hole `?upper` has type `'a -> string` — try: String.upper, input, String.trimStart, String.trimEnd, String.rev, String.ofList, and 9 more — or: String.repeat ?, String.concat ?, String.join ?, Option.withDefault ?\n", + "note: hole `?upper` has type `'a -> string` — try: String.upper, input, String.trimStart, String.trimEnd, String.rev, String.ofList, and 9 more — or: String.repeat ?, String.concat ?, String.join ?, Option.withDefault ?, and 18 more\n", " --> 5:15\n", " |\n", "5 | |> List.map ?upper\n", @@ -53,7 +53,7 @@ "\n", "The hole needs a function producing a string, and `String.upper` is first under `try:`. It comes first because of the hole's name: a fit whose name matches the hole's goes to the front of the list, so naming a hole after what you want is a way of asking for it. The `or:` list names functions that would also fit if you filled their own holes. Replace `?upper` with `String.upper` and the program compiles and prints `ADA, GRACE, ALAN`.\n", "\n", - "The `try:` list shows six fits, and `and 9 more` says how many it left out. Hovering the module in your editor, or `:type` in the REPL, gives you the full surface.\n", + "The `try:` list shows six fits and the `or:` list shows four. The `and 9 more` and `and 18 more` at their ends say how many each one left out. Hovering the module in your editor, or `:type` in the REPL, gives you the full surface.\n", "\n", "This is the workflow: sketch the whole pipeline with holes, let the compiler name each gap's type, and fill inward from the types and the suggested fits. You never have to guess a function's signature, because the hole reports it for you, and a hole blocks compilation by design, so nothing runs until every blank is filled.\n", "\n", @@ -62,7 +62,7 @@ "Fill both holes. `report` looks a score up in a map, supplies a fallback when the name is absent, and turns the number into a string. `pyfun check` reports each hole with a `try:` value that fits. The first report is:\n", "\n", "```console\n", - "note: hole `?render` has type `int -> 'a` — try: List.range, Seq.range, String.get, String.repeat, String.fromInt, String.fromFloat, and 59 more — or: String.slice ?, List.replicate ?, List.updateAt ?, List.insertAt ?\n", + "note: hole `?render` has type `int -> 'a` — try: List.range, Seq.range, String.get, String.repeat, String.fromInt, String.fromFloat, and 59 more — or: String.slice ?, List.replicate ?, List.updateAt ?, List.insertAt ?, and 16 more\n", "```" ], "id": "09-003" diff --git a/src/types/mod.rs b/src/types/mod.rs index 0189c12..209107a 100644 --- a/src/types/mod.rs +++ b/src/types/mod.rs @@ -1752,6 +1752,8 @@ pub struct Hole { /// more arguments) unifies with the hole's type — shown applied to further holes /// (`String.upper ?`, `String.concat ? ?`). Fewest-holes-first, capped. pub refinements: Vec, + /// How many further refinement fits the cap left out of `refinements`. + pub more_refinements: usize, pub span: Span, } @@ -1771,7 +1773,11 @@ impl Hole { parts.push(format!("try: {}{more}", self.fits.join(", "))); } if !self.refinements.is_empty() { - parts.push(format!("or: {}", self.refinements.join(", "))); + let more = match self.more_refinements { + 0 => String::new(), + n => format!(", and {n} more"), + }; + parts.push(format!("or: {}{more}", self.refinements.join(", "))); } parts.join(" — ") } @@ -2458,13 +2464,15 @@ fn run(module: &Module, record: bool, imports: &HashMap) .map(|(span, name, ty, env)| { let (fits, more_fits) = inf.hole_fits(&env, &ty, name.as_deref()); let direct: std::collections::HashSet = fits.iter().cloned().collect(); - let refinements = inf.hole_refinements(&env, &ty, &direct, name.as_deref()); + let (refinements, more_refinements) = + inf.hole_refinements(&env, &ty, &direct, name.as_deref()); Hole { name, ty: show(&inf.apply(&ty)), fits, more_fits, refinements, + more_refinements, span, } }) @@ -9576,16 +9584,17 @@ impl Infer { /// keeps out trivially-general combinators (`id`, `const`) that would otherwise /// "refine" into every hole. `direct` is the set already reported as direct fits. /// Fewest-holes-first, then fewest generalized vars, then unqualified, then name. + /// Returns the shortlist and how many further refinements the cap left out. fn hole_refinements( &mut self, env: &Env, target: &Ty, direct: &std::collections::HashSet, hole: Option<&str>, - ) -> Vec { + ) -> (Vec, usize) { let target = self.apply(target); if matches!(target, Ty::Var(_)) { - return Vec::new(); + return (Vec::new(), 0); } let snap = self.subst_snapshot(); let mut out: Vec<(u8, usize, usize, bool, usize, String)> = Vec::new(); @@ -9633,10 +9642,13 @@ impl Infer { } } out.sort(); - out.into_iter() + let more = out.len().saturating_sub(REFINE_CAP); + let shown = out + .into_iter() .map(|(_, _, _, _, _, s)| s) .take(REFINE_CAP) - .collect() + .collect(); + (shown, more) } fn instantiate(&mut self, scheme: &Scheme) -> Ty { diff --git a/tests/typecheck.rs b/tests/typecheck.rs index 3f9cceb..48c7d22 100644 --- a/tests/typecheck.rs +++ b/tests/typecheck.rs @@ -3928,6 +3928,36 @@ fn a_truncated_fit_list_says_how_many_it_left_out() { ); } +#[test] +fn a_truncated_refinement_list_says_how_many_it_left_out() { + // Same string->string hole as the truncated direct-fit case: many functions + // refine into it (String.lower ?, String.upper ?, …), so the refinement + // shortlist is capped and must say how many it left out. + let module = + pyfun::parse("let r = [\"a\"] |> List.map ?f |> String.join \",\"").expect("parse"); + let (_e, _t, holes, _ordered, _codecs) = pyfun::types::check_collecting(&module); + let hole = &holes[0]; + assert_eq!(hole.refinements.len(), 4); + assert!(hole.more_refinements > 0); + // The "and N more" for refinements sits on the `or:` clause; pin that the + // message reports the leftover count (the try: clause also has one for fits). + assert!( + hole.message() + .contains(&format!("or: {}", hole.refinements.join(", "))), + "{}", + hole.message() + ); + assert!( + hole.message().contains(&format!( + "or: {}, and {} more", + hole.refinements.join(", "), + hole.more_refinements + )), + "{}", + hole.message() + ); +} + #[test] fn an_unconstrained_hole_lists_no_fits() { // A bare, fully-polymorphic hole (`'a`) would match everything — unhelpful, so