refactor(tactic/polyrith): use the autogenerated json parser (#15429)

This acts as a nice demonstration of how to use `@[derive non_null_json_serializable]`

src/tactic/polyrith.lean

@@ -5,6 +5,7 @@ Authors: Dhruv Bhatia, Eric Wieser
 -/
 import tactic.linear_combination
 import data.buffer.parser.numeral
+import data.json
 
 /-!
 
@@ -275,34 +276,43 @@ ch '('
     <|> sub_parser poly_parser <|> mul_parser poly_parser <|> pow_parser poly_parser)
   <* ch ')'
 
+meta instance : non_null_json_serializable poly :=
+{ to_json := λ p, json.null,  -- we don't actually need this, but the typeclass asks for it
+  of_json := λ j, do
+    s ← of_json string j,
+    match poly_parser.run_string s with
+    | sum.inl s := exceptional.fail format!"unable to parse polynomial from.\n\n{s}"
+    | sum.inr p := pure p
+    end}
+
+/-- A schema for success messages from the python script -/
+@[derive [non_null_json_serializable, inhabited]]
+structure sage_json_success :=
+(success : {b : bool // b = tt})
+(trace : option string := none)
+(data : option (list poly) := none)
+
+/-- A schema for failure messages from the python script -/
+@[derive [non_null_json_serializable, inhabited]]
+structure sage_json_failure :=
+(success : {b : bool // b = ff})
+(error_name : string)
+(error_value : string)
+
 /-- Parse the json output from `scripts/polyrith.py` into either an error message, a list of `poly`
 objects, or `none` if only trace output was requested. -/
 meta def convert_sage_output (j : json) : tactic (option (list poly)) :=
 do
-  json.object obj ← pure j | fail!"Must be an object",
-  let obj := rbmap.from_list obj,
-  json.of_bool success ← obj.find "success" | fail!"internal error: missing success field",
-  if success then do
-    do
-    { some t ← pure (obj.find "trace") | skip,
-      json.of_string t ← pure t | fail!"internal error: trace must be a string",
-      tactic.trace t },
-    do
-    { some d ← pure (obj.find "data") | pure none,
-      json.array l ← some d | fail!"internal error: data field must be a string",
-      l ← l.mmap $ λ x, do
-      { json.of_string poly_s ← pure x | fail!"internal error: entries must be strings",
-        pure poly_s },
-      l ← l.mmap $ λ x, match poly_parser.run_string x with
-        | sum.inl s := fail!"internal error: unable to parse polynomial from.\n\n{s}"
-        | sum.inr p := pure p
-        end,
-      pure l }
-  else do
-    json.of_string kind ← obj.find "error_name",
-    json.of_string message ← obj.find "error_value",
-    fail!"polyrith failed to retrieve a solution from Sage! {kind}: {message}"
-
+  r : sage_json_success ⊕ sage_json_failure ← decorate_ex "internal json error: "
+    -- try the error format first, so that if both fail we get the message from the success parser
+    (sum.inr <$> of_json sage_json_failure j <|> sum.inl <$> of_json sage_json_success j),
+  match r with
+  | sum.inr f :=
+      fail!"polyrith failed to retrieve a solution from Sage! {f.error_name}: {f.error_value}"
+  | sum.inl s := do
+      s.trace.mmap trace,
+      pure s.data
+  end
 
 /-!
 # Parsing context into poly