Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

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

Closed
wants to merge 4 commits into from
Closed

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

Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3f72454
refactor(tactic/polyrith): use the autogenerated json parser
eric-wieser Jul 16, 2022
33fbddd
docstrings
eric-wieser Jul 17, 2022
10e5577
fix linter
eric-wieser Jul 17, 2022
7c994a6
use decorate_ex and option.mmap
eric-wieser Jul 18, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
59 changes: 35 additions & 24 deletions src/tactic/polyrith.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Authors: Dhruv Bhatia, Eric Wieser
-/
import tactic.linear_combination
import data.buffer.parser.numeral
import data.json

/-!

Expand Down Expand Up @@ -275,34 +276,44 @@ 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})
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member Author

@eric-wieser eric-wieser Jul 18, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

(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}"

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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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!

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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!


/-!
# Parsing context into poly
Expand Down