simple widget

Author: kmill

LeanTeX.lean

@@ -5,3 +5,4 @@ import LeanTeX.LatexChar
 import LeanTeX.LatexCmd
 import LeanTeX.MkAppN
 import LeanTeX.RuleSyntax
+import LeanTeX.Widget

LeanTeX/Widget.lean

@@ -0,0 +1,46 @@
+import LeanTeX.Basic
+import ProofWidgets.Component.HtmlDisplay
+
+namespace LeanTeX
+
+open Lean Elab Tactic ProofWidgets ProofWidgets.Jsx
+
+/-- Displays the markdown source in `md` in a widget when the cursor is placed at `stx`. -/
+def displayMarkdown (md : String) (stx : Syntax) : CoreM Unit := do
+  let html : Html := <MarkdownDisplay contents={md}/>
+  Widget.savePanelWidgetInfo
+    (hash HtmlDisplayPanel.javascript)
+    (return json% { html: $(← Server.RpcEncodable.rpcEncode html) })
+    stx
+
+/--
+Command for displaying an expression in LaTeX form.
+-/
+elab tk:"#texify " e:term : command => do
+  Elab.Command.runTermElabM fun _ => do
+    let e ← Elab.Term.elabTerm e none
+    Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    let e ← instantiateMVars e
+    let res ← run_latexPP e {}
+    displayMarkdown s!"$\\displaystyle {res}$" tk
+
+/--
+Tactic for displaying the goal in LaTeX form.
+-/
+elab tk:"texify" : tactic => withMainContext do
+  let mut lines : Array String := #[]
+  for decl in (← getLCtx) do
+    unless decl.isImplementationDetail do
+      let var ← run_latexPP decl.toExpr {}
+      let type ← run_latexPP (← instantiateMVars decl.type) {}
+      if let some value := decl.value? then
+        let val ← run_latexPP (← instantiateMVars value) {}
+        lines := lines.push s!"{var} : {type} := {val}"
+      else
+        lines := lines.push s!"{var} : {type}"
+  let goal ← run_latexPP (← instantiateMVars (← getMainTarget)).consumeMData {}
+  lines := lines.push s!"\\vdash {goal}"
+  let md := String.intercalate "\n\n" (lines
+    |>.map (fun line => s!"$\\displaystyle {line}$")
+    |>.toList)
+  displayMarkdown md tk

lake-manifest.json

@@ -1,5 +1,25 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.53",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "092b30de8e7ee78e96b24c235d99e26f2942d77e",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.18.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "LeanTeX",
  "lakeDir": ".lake"}

lakefile.lean

@@ -1,6 +1,8 @@
 import Lake
 open Lake DSL
 
+require "leanprover-community" / "proofwidgets" @ git "v0.0.53"
+
 package LeanTeX { }
 
 @[default_target]

test/widget_basic.lean

@@ -0,0 +1,98 @@
+import LeanTeX
+
+set_option linter.unusedVariables false
+
+open Lean
+
+def a : Nat := 22
+
+abbrev Real : Type := Nat
+def Real.pi : Real := 3
+
+open LeanTeX in
+latex_pp_const_rule Real.pi := LatexData.atomString "\\pi" |>.maybeWithTooltip "Real.pi"
+
+def f : Nat → Nat → Nat := λ x y => x + y
+
+def g : Unit → Nat := λ _ => 22
+
+section
+
+variable (b : Nat) (c : Nat → Real → Real) (x : Real)
+
+#texify 1 + 2 + 3
+#texify 1 + (2 + 3)
+#texify (1 + 2) + 3
+#texify b * (1 + 2 * 3 * 4 + 5) + 1
+#texify f (Real.pi + a + f b 22) 2
+#texify (1, (2, 3), a, Real.pi)
+#texify Nat × Nat × Nat × Fin 37
+#texify Nat × (n : Nat) × Fin n × Nat
+#texify (⟨1, 1, 1⟩ : (n : Nat) × Fin n × Nat)
+#texify ()
+#texify g ()
+#texify (λ (x : Nat) => x + 1)
+#texify (λ (x y : Nat) => x + y + 1)
+#texify (1 + 2) / 3
+#texify (1 + 2/3)/4
+#texify 1+1/(1+1/(1+1/(1+1/(1+1/(1+1)))))
+#texify 2^2
+#texify 4/2
+#texify 2^(4/2)
+#texify (1+2)^(3+4)
+#texify 2^2^2
+#texify (2^2)^2
+#texify (1/2)^3
+#texify Nat → Nat
+#texify Prop
+#texify (n : Nat) → Nat → Fin n
+#texify (m n : Nat) → Fin (m + n)
+#texify ∀ (n m : Nat), n < m → n < m + 1
+#texify ∀ (n : Nat), 1 = 1
+#texify {α : Type} → {β : Type} → {γ : Type} → [self : HAdd α β γ] → α → β → γ
+#texify (α β : Type) → (f : α → β) → ∀ {x y : α}, f x = f y → x = y
+#texify (p q r : Prop) → (p → q) → (p → q → r) → p → r
+#texify (p₁ p₂ : Prop) → p₁ → (p₂ → p₁)
+#texify (p p' : Prop) → p → (p' → p)
+#texify c 1 x
+
+#texify ∃ (n : Nat), 1 < n
+#texify ∃ (n : Nat), ¬ n < 10
+#texify ∃ (n : Nat), ¬ n = 0
+
+def foo (n : Nat) : Prop := true
+#texify Exists foo
+
+#texify True ∧ True ∧ True
+#texify ¬True ∨ True
+
+variable (f_1 f_2 : Nat → Nat)
+
+#texify (f_1 ∘ f_2) 37
+
+#texify fun (_ : Nat) => 1
+
+#texify 1 = 2
+
+#texify ((1 = 1) = (2 = 2))
+
+def Set (α : Type u) := α → Prop
+instance : Membership α (Set α) := ⟨fun s x => s x⟩
+
+variable (X : Type) (U : Set X) (x : X)
+
+#texify x ∈ U
+
+#texify x ∉ U
+
+#texify Prod.mk 1
+
+end
+
+/-!
+### Tactic
+-/
+
+example (x y : Nat) (h : x < y) : 2 * x < 2 * y := by
+  texify
+  sorry

test/widget_bigop.lean

@@ -0,0 +1,48 @@
+import LeanTeX
+import Lean.Elab.Tactic.Guard
+--import Mathlib.Algebra.BigOperators.Basic
+
+set_option linter.unusedVariables false
+
+open Lean
+
+def a : Nat := 22
+
+abbrev Real := Nat
+def Real.pi : Nat := 3
+
+open Real LeanTeX in
+latex_pp_const_rule pi := LatexData.atomString "\\pi" |>.maybeWithTooltip "real.pi"
+
+def f : Nat → Nat → Nat := λ x y => x + y
+
+def g : Unit → Nat := λ _ => 22
+
+def Finset (α : Type u) : Type u := α
+def Finset.sum {α : Type u} {β : Type v} [Inhabited β] (s : Finset α) (f : α → β) : β := default
+
+variable (b : Nat) (s : Finset Nat) (t : Nat → Finset Nat) (c : Nat → Real → Real) (x : Real)
+
+#texify s.sum (λ x => x + 1)
+#texify s.sum (λ x => 2 * x)
+#texify s.sum (λ x => x + 1) * a
+#texify a * s.sum (λ x => x + 1)
+#texify s.sum (λ x => x + 1) + a
+#texify a + s.sum (λ x => x + 1)
+#texify s.sum (λ x => x + 1) * s.sum (λ x => 2 * x)
+#texify λ (c : Nat) => c * s.sum (λ x => (t x).sum (λ y => x * y))
+#texify s.sum id
+
+open LeanTeX in
+/-- An experiment: use a subscript for an argument. Represents `Fin n` as `\mathbb{N}_{<n}` -/
+-- TODO make work for multi-argument like Nat → Nat → Real → Real
+latex_pp_app_rules (kind := any) (paramKinds := params)
+  | f, #[n] => do
+    if params[0]!.bInfo.isExplicit && params[0]!.type.isConstOf `Nat then
+      let f ← latexPP f
+      let n ← withExtraSmallness 2 <| latexPP n
+      return f.sub n
+    else
+      failure
+
+#texify λ (f : Nat → Nat) => (s.sum f)^2