[Merged by Bors] - refactor(tactic/polyrith): use the autogenerated json parser

[eric-wieser]

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

---

[robertylewis]

Thanks for this! This will conflict with #15425 and should be merged first. I'm closing Lean for a bit but will review soon -- it looks like a huge improvement!

[robertylewis]

Suggested change

	let e : exceptional (sage_json_success ⊕ sage_json_failure) :=
	-- 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 e with
	| exceptional.exception f := exceptional.exception (λ s, format!"internal json error: " ++ f s)
	| exceptional.success (sum.inr f) :=
	fail!"polyrith failed to retrieve a solution from Sage! {f.error_name}: {f.error_value}"
	| exceptional.success (sum.inl s) := do
	do { some t ← pure s.trace | skip, tactic.trace t},
	pure s.data
	end
	(do f ← of_json sage_json_failure j,
	fail!"polyrith failed to retrieve a solution from Sage! {f.error_name}: {f.error_value}") <|>
	(do s ← decorate_ex "internal json error: " $ of_json sage_json_success j,
	s.trace.mmap trace,
	pure s.data)

I think this is a slicker version of the same thing!

[eric-wieser]

That doesn't work correctly, because if an error message is recieved the failure is treated as a parsing failure, and then it tries to reparse as a success message. Still a helpful comment though, I didn't know about decorate_ex and didn't think of option.mmap!

[robertylewis]

I trust this is right (also because it works), but what's the significance of this weird subtype? Is the idea that only json data with success: false should be parsed into this type? Is the non_null_json_serializable derive handler the part that's taking this into account?

[eric-wieser]

The subtype.non_null_json_serializable parser is the one that handles this; it parses the value, and uses decidability for the proof.

I could also have used

Suggested change

	(success : {b : bool // b = ff})
	(success : bool)
	(success_eq_ff : success = ff)

and then the derive handler would have handled it; but then the inhabited derive handler (which I'm using only to appease the linter) wouldn't have worked.

[robertylewis]

Thanks!

[robertylewis]

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

This PR was included in a batch that was canceled, it will be automatically retried

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests