11import LeanPlot.Plot
22import LeanPlot.API
3+ import LeanPlot.Constants
34import Lean
45import ProofWidgets.Component.HtmlDisplay
56
@@ -11,6 +12,7 @@ This module implements the ergonomic plotting syntax:
1112```
1213#plot (fun x => x^2) -- default 200 samples
1314#plot (fun t => Float.sin t) using 400
15+ #plot (fun x => x^2) domain=(-2, 2) steps=100 -- named params
1416```
1517
1618With doc comments as captions:
@@ -20,6 +22,13 @@ With doc comments as captions:
2022#plot (fun t => Float.exp (-t) * Float.sin (5 * t)) using 200
2123```
2224
25+ ## Named Parameters
26+
27+ The `#plot` command supports named parameters for full control:
28+ - `domain=(lo, hi)` : x-axis range (default: 0 to 1)
29+ - `steps=n` : number of sample points (default: 200)
30+ - `size=(w, h)` : chart dimensions in pixels (default: 400×300)
31+
2332
2433a function. If so, we wrap it with {name}`LeanPlot.API.plot` automatically.
2534-/
@@ -29,6 +38,7 @@ namespace LeanPlot.DSL
2938open Lean Elab Command Term
3039open ProofWidgets
3140open LeanPlot.PlotCommand (withCaption)
41+ open LeanPlot.Constants
3242
3343-- Store the original elaborator before removing it
3444private def originalElabPlotCmd := LeanPlot.PlotCommand.elabPlotCmd
@@ -39,6 +49,61 @@ attribute [-command_elab] LeanPlot.PlotCommand.elabPlotCmd
3949/-- Syntax for `#plot` with explicit sample count: `#plot f using 400` -/
4050syntax (name := plotCmdUsing) (docComment)? "#plot " term " using " num : command
4151
52+ /-- Syntax for `#plot` with named parameters: `#plot f domain=(-2, 2) steps=100 size=(500, 300)` -/
53+ syntax (name := plotCmdNamed) (docComment)? "#plot " term
54+ ("domain=" "(" term "," term ")" )?
55+ ("steps=" num)?
56+ ("size=" "(" num "," num ")" )? : command
57+
58+ /-- Parse a term as a Float, handling negative numbers and various formats -/
59+ private def termToFloat (t : TSyntax `term) (default : Float := 0 .0 ) : Float :=
60+ -- Try natural literal first
61+ match t.raw.isNatLit? with
62+ | some n => n.toFloat
63+ | none =>
64+ -- Try negative number (like -2)
65+ if t.raw.isOfKind `Lean.Parser.Term.app then
66+ -- Check if it's a negation: (- n)
67+ let args := t.raw.getArgs
68+ if args.size >= 2 then
69+ let fn := args[0 ]!
70+ let arg := args[1 ]!
71+ if fn.isOfKind `Lean.Parser.Term.paren then
72+ -- Check for prefix negation
73+ match arg.isNatLit? with
74+ | some n => - (n.toFloat)
75+ | none => default
76+ else if fn.getId == ``Neg.neg || toString fn == "-" then
77+ match arg.isNatLit? with
78+ | some n => - (n.toFloat)
79+ | none => default
80+ else default
81+ else default
82+ else if t.raw.isOfKind `Lean.Parser.Term.negNum then
83+ -- Direct negNum syntax (rare but possible)
84+ match t.raw[1 ]!.isNatLit? with
85+ | some n => - (n.toFloat)
86+ | none => default
87+ else if t.raw.isOfKind `Lean.Parser.Term.paren then
88+ -- Parenthesized expression - try to extract inner
89+ let inner := t.raw[1 ]!
90+ match inner.isNatLit? with
91+ | some n => n.toFloat
92+ | none => default
93+ else
94+ -- Try to get it as a string and parse manually
95+ let s := t.raw.reprint.getD ""
96+ let trimmed := s.trim
97+ -- Simple integer parsing fallback
98+ if trimmed.startsWith "-" then
99+ match trimmed.drop 1 |>.toNat? with
100+ | some n => - (n.toFloat)
101+ | none => default
102+ else
103+ match trimmed.toNat? with
104+ | some n => n.toFloat
105+ | none => default
106+
42107/-- Elaborator for the basic `#plot` command. Wraps functions with `LeanPlot.API.plot`. -/
43108@[command_elab LeanPlot.PlotCommand.plotCmd]
44109def elabPlotNew : CommandElab := fun stx => do
@@ -88,6 +153,58 @@ def elabPlotUsing : CommandElab := fun stx => do
88153 (return json% { html: $(← Server.rpcEncode finalHtml) })
89154 stx
90155
156+ /-- Elaborator for the `#plot` command with named parameters. -/
157+ @[command_elab plotCmdNamed]
158+ def elabPlotNamed : CommandElab := fun stx => do
159+ -- Extract doc comment, term, and named parameters from syntax
160+ let (doc?, term, loT?, hiT?, stepsN?, widthN?, heightN?) ← match stx with
161+ | `($doc:docComment #plot $t:term $[domain=($lo:term, $hi:term)]? $[steps=$n:num]? $[size=($w:num, $h:num)]?) =>
162+ pure (some doc, t, lo, hi, n, w, h)
163+ | `(#plot $t:term $[domain=($lo:term, $hi:term)]? $[steps=$n:num]? $[size=($w:num, $h:num)]?) =>
164+ pure (none, t, lo, hi, n, w, h)
165+ | _ => throwUnsupportedSyntax
166+
167+ -- Parse domain if provided
168+ let domainOpt : Option (Float × Float) := match loT?, hiT? with
169+ | some lo, some hi => some (termToFloat lo, termToFloat hi)
170+ | _, _ => none
171+
172+ -- Parse steps
173+ let steps := stepsN?.map (·.getNat) |>.getD 200
174+
175+ -- Parse size
176+ let width := widthN?.map (·.getNat) |>.getD defaultW
177+ let height := heightN?.map (·.getNat) |>.getD defaultH
178+
179+ -- Build the wrapped term based on what's provided
180+ let wrappedStx ← match domainOpt with
181+ | some (lo, hi) =>
182+ let loLit := Syntax.mkNumLit (toString lo)
183+ let hiLit := Syntax.mkNumLit (toString hi)
184+ let stepsLit := Syntax.mkNumLit (toString steps)
185+ let wLit := Syntax.mkNumLit (toString width)
186+ let hLit := Syntax.mkNumLit (toString height)
187+ `(LeanPlot.API.plot $term (steps := $stepsLit) (domain := some ($loLit, $hiLit)) (w := $wLit) (h := $hLit))
188+ | none =>
189+ let stepsLit := Syntax.mkNumLit (toString steps)
190+ let wLit := Syntax.mkNumLit (toString width)
191+ let hLit := Syntax.mkNumLit (toString height)
192+ `(LeanPlot.API.plot $term (steps := $stepsLit) (w := $wLit) (h := $hLit))
193+
194+ -- Evaluate it directly as Html
195+ let htX ← liftTermElabM <| HtmlCommand.evalCommandMHtml <| ← ``(ProofWidgets.HtmlEval.eval $wrappedStx)
196+ let ht ← htX
197+
198+ -- Wrap with caption if doc comment present
199+ let finalHtml := match doc? with
200+ | some doc => withCaption doc.getDocString ht
201+ | none => ht
202+
203+ liftCoreM <| Widget.savePanelWidgetInfo
204+ (hash ProofWidgets.HtmlDisplayPanel.javascript)
205+ (return json% { html: $(← Server.rpcEncode finalHtml) })
206+ stx
207+
91208end LeanPlot.DSL
92209
93210-- Re-export for convenience
0 commit comments