Add type prop to AxisProps

[mars0i]

One of the props missing from AxisProps in ProofWidgets/Components/Recharts.lean is type, with options number and category. The number option causes x values to be spaced according to numeric distances, but Recharts apparently defaults to category. The type=category default means, for example, that all x values are treated as categorical--even if they are numeric--and will be evenly spaced. This is illustrated by the following revised version of the Plot function from `ProofWidgets/Demo/Plot.lean:

open scoped ProofWidgets.Jsx in
def HoleyPlot (fn : Float → Float) (steps := 100) : Html :=
  let fullsteps := Array.range (steps + 1)
  let reducedsteps := fullsteps[:10] ++ fullsteps[90:]
  let jsonData : Array Json :=
    reducedsteps
    |> Array.map (fun (x : Nat) => let x : Float := x.toFloat / steps.toFloat;  (x, fn x))
    |> Array.map (fun (x,y) => json% {x: $(toJson x) , y: $(toJson y)});
  <LineChart width={400} height={400} data={jsonData}>
    <XAxis domain?={#[toJson 0, toJson 1]} dataKey?="x" />
    <YAxis domain?={#[toJson (-1), toJson 1]} allowDataOverflow={Bool.false} />
    <Line type={.monotone} dataKey="y" stroke="#8884d8" dot?={Bool.false} />
  </LineChart>

#html HoleyPlot (fn 0)

The key change is that 80 elements in the middle of the steps array are removed. Notice that in the plot, the gap between the "0.08" and "0.9" ticks is the same as all of the other gap sizes; it should be much wider, perhaps filled in by other tick marks:

[mars0i]

This seems like a good solution:

inductive AxisType where
  | number | category
  deriving FromJson, ToJson

structure AxisProps where
  dataKey? : Option Json := none
  domain? : Option (Array Json) := none
  allowDataOverflow : Bool := false
  type : AxisType := .number
  -- TODO: There are many more props
  deriving FromJson, ToJson

type='category' is the Recharts default, but given the focus on mathematics in Lean, making AxisType.number the default seems more sensible to me. Comparing the HoleyPlot above with the Plot example in Demo/Plot.lean shows that the Recharts default category setting can produce unexpected results when the x axis elements are numbers: with type='category': a plot that appears to be correct when x elements are equally spaced will become incorrect or misleading when the equal spacing is removed.

On the other hand, if number is the default axis type for ProofWidget, then if one uses non-numeric elements for an axis, it will be necessary to add type={.category} to <XAxis ...> or <YAxis ...>. Most of the line plot examples on recharts.org are of this kind, so if someone tried to reproduce those examples, having a different default might be confusing. I still think type={.number} would be better for ProofWidgets.

I can submit a PR if this seems like a good idea. I don't fully understand why this code works, but it seems to in my testing. I copied methods I saw in other parts of the source file.

[Vtec234]

Thanks! Yeah, this seems like a reasonable PR to make and we can merge it if it works. However, see also my response in #96.

[mars0i]

On Zulip I'm being advised to base a ProofWidgets PR by creating a branch of Mathlib. Is that the right strategy? Might be a lot for a simple addition, given that I now realize based on #96 that I'm probably not going to use Recharts.