Export equations (#429)

Exports the equations defined in `Equations.lean` and `AllEquations.lean` to a JSON file `data/magma_equations.json`. Depends on PR #427. --------- Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
teorth · Oct 9, 2024 · 345f865 · 345f865
1 parent adc92cb
commit 345f865
Show file tree

Hide file tree

Showing 3 changed files with 43 additions and 0 deletions.
diff --git a/equational_theories/MagmaLaw.lean b/equational_theories/MagmaLaw.lean
@@ -14,6 +14,10 @@ infix:60 " ≃ " => MagmaLaw.mk
 
 abbrev NatMagmaLaw := MagmaLaw Nat
 
+open Lean in
+instance {α} [ToJson α] : ToJson (MagmaLaw α) where
+  toJson := fun ⟨lhs, rhs⟩ => .mkObj [("lhs", Lean.toJson lhs), ("rhs", Lean.toJson rhs)]
+
 end Law
 
 open Law

diff --git a/lakefile.toml b/lakefile.toml
@@ -26,3 +26,8 @@ name = "equational_theories"
 name = "extract_implications"
 root = "scripts.extract_implications"
 supportInterpreter = true
+
+[[lean_exe]]
+name = "export_equations"
+root = "scripts.export_equations"
+supportInterpreter = true
diff --git a/scripts/export_equations.lean b/scripts/export_equations.lean
@@ -0,0 +1,34 @@
+import equational_theories.Equations
+import equational_theories.AllEquations
+
+open Lean Elab Command Meta
+
+/-!
+
+# Exporting magma equations
+
+This script exports all the magma equations defined in the `Equations` and `AllEquations` files
+to the JSON file `data/magma_equations.json`.
+
+The format is
+```
+{
+  "equation": "EquationName",
+  "law": {
+    "lhs": { ... },
+    "rhs": { ... }
+  }
+}
+-/
+
+def main : IO Unit := do
+  searchPathRef.set compile_time_search_path%
+  let env ← importModules #[
+    { module := `equational_theories.Equations },
+    { module := `equational_theories.AllEquations }] .empty
+  let laws := magmaLawExt.getState env
+  let jsonOutput : Json := Json.arr <| laws.map fun ⟨lawName, law⟩ => .mkObj [
+    ("equation", "Equation" ++ (lawName.toString.drop "Law".length)),
+    ("law", ToJson.toJson law)
+  ]
+  IO.FS.writeFile ("data" / "magma_equations.json") jsonOutput.pretty