doc(tactic/ring2): document parts of ring2 #1208
Conversation
There was a problem hiding this comment.
Thanks! I appreciate the effort to document things. This looks accurate to me, but perhaps @digama0 (who wrote ring2) can take a quick look before merging.
src/tactic/ring2.lean
Outdated
| @@ -39,21 +42,34 @@ def tree.index_of {α} (lt : α → α → Prop) [decidable_rel lt] | |||
| | ordering.gt := pos_num.bit1 <$> tree.index_of t₂ | |||
| end | |||
|
|
|||
| /-- Reflects a tree of expressions into an expression that, | |||
| when evaluated, yields the original tree. -/ | |||
There was a problem hiding this comment.
This isn't clear to me. What do you mean the "original tree"? What is the type of the resulting expr?
src/tactic/ring2.lean
Outdated
| /-- An efficient representation of expressions in a commutative | ||
| semiring using the sparse Horner normal form. This type admits | ||
| non-optimal instantiations (e.g. `P` can be represented as `P+0+0`), | ||
| so care must be taken to maintain an optimal, *canonical* form.-/ |
There was a problem hiding this comment.
Care must be taken where? In the ring2 tactic, I suppose, but this comment reads a little strange as a doc string.
src/tactic/ring2.lean
Outdated
| | horner : horner_expr → pos_num → num → horner_expr → horner_expr | ||
|
|
||
| namespace horner_expr | ||
|
|
||
| /-- "Is this `horner_expr` a valid `csring_expr`?" Basically all constants | ||
| must be non-negative. -/ |
There was a problem hiding this comment.
Can this be made declarative? "Tests whether a horner_expr is a valid csring_expr, i.e. whether all constants are non-negative."
|
I rewrote some comments - hopefully they should be clearer. I also refactored the binary tree type |
Vtec234
force-pushed
the
ring2_doc
branch
2 times, most recently
from
89219d2
to
2aa5773
Compare
src/tactic/ring2.lean
Outdated
| meta def tree.reflect' (u : level) (α : expr) : tree expr → expr | ||
| /-- `(reflect' t u α)` turns a tree `(t: tree expr)` of reflected values | ||
| of type `α` at level `u` into an `expr` which concretizes to a `tree α` | ||
| containing the concretizations of the `expr`s from the original `t`. -/ |
There was a problem hiding this comment.
Hm, this comment reads a bit convoluted. The way I would explain this is that we can quasiquote a tree expr, with unquotations at the leaves, where the leaves represent elements of type alpha (at level u).
There was a problem hiding this comment.
I am also not too happy with this comment. The issue here is that the terminology around quoting is varied and inconsistent. I've heard the terms reflection, reification, quotation and concretization all used in this context and they always confuse me. Perhaps "quoting" is closest to existing Lean terminology, so I will use that instead.
There was a problem hiding this comment.
I changed it to use "(quasi)quotation"/"reification" but avoided the use of "unquotation". The reason is that a quick search for "unquotation" comes up with nothing, while the former terms have some explanations on the Haskell wiki.
There was a problem hiding this comment.
(One nitpick, this tree type has values at every node rather than just the leaves).
robertylewis
added
the
ready-to-merge
* doc(tactic/ring2): document parts of ring2 * feat(data/tree): refactor binary trees into their own module * feat(tactic/ring2): resolve correct correctness * chore(tactic/ring2): move copyright into comment * doc(tactic/ring2): wording
* doc(tactic/ring2): document parts of ring2 * feat(data/tree): refactor binary trees into their own module * feat(tactic/ring2): resolve correct correctness * chore(tactic/ring2): move copyright into comment * doc(tactic/ring2): wording
cc @digama0