Improve options display

src/typing_rules.rs

@@ -83,12 +83,12 @@ impl RuleOptions {
     pub const OPTIONS_DOC: &[(&str, &[&str], &str)] = &[
         (
             "match_constructor_through_ref",
-            &["true", "false"],
+            &["false", "true"],
             "whether `[p]` can match on `&[T]`; the heart of match ergonomics.",
         ),
         (
             "eat_inherited_ref_alone",
-            &["true", "false"],
+            &["false", "true"],
             "whether `&p`/`&mut p` is allowed on an inherited reference if the underlying type isn't also a reference type",
         ),
         (
@@ -99,44 +99,44 @@ impl RuleOptions {
         ),
         (
             "fallback_to_outer",
-            &["true", "false"],
+            &["false", "true"],
             "whether to try again in `EatOuter` mode when a `EatBoth` or `EatInner` case has a mutability mismatch",
         ),
         (
-            "allow_ref_pat_on_ref_mut",
-            &["true", "false"],
-            "whether to allow `&p: &mut T`",
-        ),
-        (
-            "simplify_deref_mut",
+            "dont_eat_mut_inside_shared",
             &["true", "false"],
-            "whether to simplify `*&mut expr`, which removes some borrow errors",
+            "in `EatInner` or `EatBoth`, disallow eating an inner `&mut T` with `&mut p` from under a `&`",
         ),
         (
-            "always_inspect_bm",
-            &["true", "false"],
-            "whether to always branch on the binding mode when computing rules. this is required for the `SequentBindingMode` style",
+            "allow_ref_pat_on_ref_mut",
+            &["false", "true"],
+            "whether to allow `&p: &mut T`",
         ),
         (
             "downgrade_mut_inside_shared",
-            &["true", "false"],
+            &["false", "true"],
             "RFC3627 rule 3: downgrade `&mut` inherited references to `&` inside a shared deref",
         ),
-        (
-            "dont_eat_mut_inside_shared",
-            &["true", "false"],
-            "in `EatInner` or `EatBoth`, disallow eating an inner `&mut T` with `&mut p` from under a `&`",
-        ),
         (
             "ref_binding_on_inherited",
-            &["ResetBindingMode", "AllocTemporary", "Error"],
+            &["Error", "ResetBindingMode", "AllocTemporary"],
             "how to handle a `ref x` binding on an inherited reference",
         ),
         (
             "mut_binding_on_inherited",
-            &["ResetBindingMode", "Keep", "Error"],
+            &["Error", "ResetBindingMode", "Keep"],
             "how to handle a `mut x` binding on an inherited reference",
         ),
+        (
+            "simplify_deref_mut",
+            &["false", "true"],
+            "whether to simplify `*&mut expr`, which removes some borrow errors",
+        ),
+        (
+            "always_inspect_bm",
+            &["false", "true"],
+            "whether to always branch on the binding mode when computing rules. this is required for the `SequentBindingMode` style",
+        ),
     ];
 
     pub fn to_map(&self) -> serde_json::Map<String, serde_json::Value> {

tests/snapshots/trace_cli@11515459865669657874.snap

@@ -2,31 +2,31 @@
 source: tests/trace_cli.rs
 info: set ref_binding_on_inherited true
 ---
-Error: unknown value `true` for option `ref_binding_on_inherited`; options are: ResetBindingMode, AllocTemporary, Error
+Error: unknown value `true` for option `ref_binding_on_inherited`; options are: Error, ResetBindingMode, AllocTemporary
 
 Options are:
-- match_constructor_through_ref: true | false
+- match_constructor_through_ref: false | true
     whether `[p]` can match on `&[T]`; the heart of match ergonomics.
-- eat_inherited_ref_alone: true | false
+- eat_inherited_ref_alone: false | true
     whether `&p`/`&mut p` is allowed on an inherited reference if the underlying type isn't also a reference type
 - inherited_ref_on_ref: EatOuter | EatInner | EatBoth
     how to handle a reference pattern on a double reference when the outer one is inherited
-- fallback_to_outer: true | false
+- fallback_to_outer: false | true
     whether to try again in `EatOuter` mode when a `EatBoth` or `EatInner` case has a mutability mismatch
-- allow_ref_pat_on_ref_mut: true | false
-    whether to allow `&p: &mut T`
-- simplify_deref_mut: true | false
-    whether to simplify `*&mut expr`, which removes some borrow errors
-- always_inspect_bm: true | false
-    whether to always branch on the binding mode when computing rules. this is required for the `SequentBindingMode` style
-- downgrade_mut_inside_shared: true | false
-    RFC3627 rule 3: downgrade `&mut` inherited references to `&` inside a shared deref
 - dont_eat_mut_inside_shared: true | false
     in `EatInner` or `EatBoth`, disallow eating an inner `&mut T` with `&mut p` from under a `&`
-- ref_binding_on_inherited: ResetBindingMode | AllocTemporary | Error
+- allow_ref_pat_on_ref_mut: false | true
+    whether to allow `&p: &mut T`
+- downgrade_mut_inside_shared: false | true
+    RFC3627 rule 3: downgrade `&mut` inherited references to `&` inside a shared deref
+- ref_binding_on_inherited: Error | ResetBindingMode | AllocTemporary
     how to handle a `ref x` binding on an inherited reference
-- mut_binding_on_inherited: ResetBindingMode | Keep | Error
+- mut_binding_on_inherited: Error | ResetBindingMode | Keep
     how to handle a `mut x` binding on an inherited reference
+- simplify_deref_mut: false | true
+    whether to simplify `*&mut expr`, which removes some borrow errors
+- always_inspect_bm: false | true
+    whether to always branch on the binding mode when computing rules. this is required for the `SequentBindingMode` style
 - predicate_style: Expression | Sequent | BindingMode | SequentBindingMode | Stateless
     the style of the typing predicate; not all rulesets can be expressed in all styles, only `Expression` is compatible with all rulesets
 

tests/snapshots/trace_cli@16736406663811832092.snap

@@ -5,28 +5,28 @@ info: set mistyped val
 Error: unknown option `mistyped`
 
 Options are:
-- match_constructor_through_ref: true | false
+- match_constructor_through_ref: false | true
     whether `[p]` can match on `&[T]`; the heart of match ergonomics.
-- eat_inherited_ref_alone: true | false
+- eat_inherited_ref_alone: false | true
     whether `&p`/`&mut p` is allowed on an inherited reference if the underlying type isn't also a reference type
 - inherited_ref_on_ref: EatOuter | EatInner | EatBoth
     how to handle a reference pattern on a double reference when the outer one is inherited
-- fallback_to_outer: true | false
+- fallback_to_outer: false | true
     whether to try again in `EatOuter` mode when a `EatBoth` or `EatInner` case has a mutability mismatch
-- allow_ref_pat_on_ref_mut: true | false
-    whether to allow `&p: &mut T`
-- simplify_deref_mut: true | false
-    whether to simplify `*&mut expr`, which removes some borrow errors
-- always_inspect_bm: true | false
-    whether to always branch on the binding mode when computing rules. this is required for the `SequentBindingMode` style
-- downgrade_mut_inside_shared: true | false
-    RFC3627 rule 3: downgrade `&mut` inherited references to `&` inside a shared deref
 - dont_eat_mut_inside_shared: true | false
     in `EatInner` or `EatBoth`, disallow eating an inner `&mut T` with `&mut p` from under a `&`
-- ref_binding_on_inherited: ResetBindingMode | AllocTemporary | Error
+- allow_ref_pat_on_ref_mut: false | true
+    whether to allow `&p: &mut T`
+- downgrade_mut_inside_shared: false | true
+    RFC3627 rule 3: downgrade `&mut` inherited references to `&` inside a shared deref
+- ref_binding_on_inherited: Error | ResetBindingMode | AllocTemporary
     how to handle a `ref x` binding on an inherited reference
-- mut_binding_on_inherited: ResetBindingMode | Keep | Error
+- mut_binding_on_inherited: Error | ResetBindingMode | Keep
     how to handle a `mut x` binding on an inherited reference
+- simplify_deref_mut: false | true
+    whether to simplify `*&mut expr`, which removes some borrow errors
+- always_inspect_bm: false | true
+    whether to always branch on the binding mode when computing rules. this is required for the `SequentBindingMode` style
 - predicate_style: Expression | Sequent | BindingMode | SequentBindingMode | Stateless
     the style of the typing predicate; not all rulesets can be expressed in all styles, only `Expression` is compatible with all rulesets
 

tests/snapshots/trace_cli@17515479014605656910.snap

@@ -5,28 +5,28 @@ info: set
 Error: Syntax is `set option value`.
 
 Options are:
-- match_constructor_through_ref: true | false
+- match_constructor_through_ref: false | true
     whether `[p]` can match on `&[T]`; the heart of match ergonomics.
-- eat_inherited_ref_alone: true | false
+- eat_inherited_ref_alone: false | true
     whether `&p`/`&mut p` is allowed on an inherited reference if the underlying type isn't also a reference type
 - inherited_ref_on_ref: EatOuter | EatInner | EatBoth
     how to handle a reference pattern on a double reference when the outer one is inherited
-- fallback_to_outer: true | false
+- fallback_to_outer: false | true
     whether to try again in `EatOuter` mode when a `EatBoth` or `EatInner` case has a mutability mismatch
-- allow_ref_pat_on_ref_mut: true | false
-    whether to allow `&p: &mut T`
-- simplify_deref_mut: true | false
-    whether to simplify `*&mut expr`, which removes some borrow errors
-- always_inspect_bm: true | false
-    whether to always branch on the binding mode when computing rules. this is required for the `SequentBindingMode` style
-- downgrade_mut_inside_shared: true | false
-    RFC3627 rule 3: downgrade `&mut` inherited references to `&` inside a shared deref
 - dont_eat_mut_inside_shared: true | false
     in `EatInner` or `EatBoth`, disallow eating an inner `&mut T` with `&mut p` from under a `&`
-- ref_binding_on_inherited: ResetBindingMode | AllocTemporary | Error
+- allow_ref_pat_on_ref_mut: false | true
+    whether to allow `&p: &mut T`
+- downgrade_mut_inside_shared: false | true
+    RFC3627 rule 3: downgrade `&mut` inherited references to `&` inside a shared deref
+- ref_binding_on_inherited: Error | ResetBindingMode | AllocTemporary
     how to handle a `ref x` binding on an inherited reference
-- mut_binding_on_inherited: ResetBindingMode | Keep | Error
+- mut_binding_on_inherited: Error | ResetBindingMode | Keep
     how to handle a `mut x` binding on an inherited reference
+- simplify_deref_mut: false | true
+    whether to simplify `*&mut expr`, which removes some borrow errors
+- always_inspect_bm: false | true
+    whether to always branch on the binding mode when computing rules. this is required for the `SequentBindingMode` style
 - predicate_style: Expression | Sequent | BindingMode | SequentBindingMode | Stateless
     the style of the typing predicate; not all rulesets can be expressed in all styles, only `Expression` is compatible with all rulesets
 

tests/snapshots/trace_cli@3615762548608754050.snap

@@ -6,28 +6,28 @@ Error: couldn't parse `set` command.
 Syntax is `set option value`.
 
 Options are:
-- match_constructor_through_ref: true | false
+- match_constructor_through_ref: false | true
     whether `[p]` can match on `&[T]`; the heart of match ergonomics.
-- eat_inherited_ref_alone: true | false
+- eat_inherited_ref_alone: false | true
     whether `&p`/`&mut p` is allowed on an inherited reference if the underlying type isn't also a reference type
 - inherited_ref_on_ref: EatOuter | EatInner | EatBoth
     how to handle a reference pattern on a double reference when the outer one is inherited
-- fallback_to_outer: true | false
+- fallback_to_outer: false | true
     whether to try again in `EatOuter` mode when a `EatBoth` or `EatInner` case has a mutability mismatch
-- allow_ref_pat_on_ref_mut: true | false
-    whether to allow `&p: &mut T`
-- simplify_deref_mut: true | false
-    whether to simplify `*&mut expr`, which removes some borrow errors
-- always_inspect_bm: true | false
-    whether to always branch on the binding mode when computing rules. this is required for the `SequentBindingMode` style
-- downgrade_mut_inside_shared: true | false
-    RFC3627 rule 3: downgrade `&mut` inherited references to `&` inside a shared deref
 - dont_eat_mut_inside_shared: true | false
     in `EatInner` or `EatBoth`, disallow eating an inner `&mut T` with `&mut p` from under a `&`
-- ref_binding_on_inherited: ResetBindingMode | AllocTemporary | Error
+- allow_ref_pat_on_ref_mut: false | true
+    whether to allow `&p: &mut T`
+- downgrade_mut_inside_shared: false | true
+    RFC3627 rule 3: downgrade `&mut` inherited references to `&` inside a shared deref
+- ref_binding_on_inherited: Error | ResetBindingMode | AllocTemporary
     how to handle a `ref x` binding on an inherited reference
-- mut_binding_on_inherited: ResetBindingMode | Keep | Error
+- mut_binding_on_inherited: Error | ResetBindingMode | Keep
     how to handle a `mut x` binding on an inherited reference
+- simplify_deref_mut: false | true
+    whether to simplify `*&mut expr`, which removes some borrow errors
+- always_inspect_bm: false | true
+    whether to always branch on the binding mode when computing rules. this is required for the `SequentBindingMode` style
 - predicate_style: Expression | Sequent | BindingMode | SequentBindingMode | Stateless
     the style of the typing predicate; not all rulesets can be expressed in all styles, only `Expression` is compatible with all rulesets
 

web/src/components/Solver.jsx

@@ -46,9 +46,9 @@ const prettyOptions = {
         true: "❌",
     },
     downgrade_mut_inside_shared: {
-        question: <>&...&mut T</>,
-        true: <>&...&T</>,
-        false: <>&...&mut T</>,
+        question: <>p: &...&mut T</>,
+        true: <>p: &...&T</>,
+        false: <>p: &...&mut T</>,
     },
     allow_ref_pat_on_ref_mut: {
         question: <>&p: &mut T</>,
@@ -91,11 +91,12 @@ export default function Solver() {
         const current_val = options.get_key(option.name);
         const prettyOption = prettyOptions[option.name] || null;
         const question = prettyOption ? prettyOption.question : option.name;
-        const label = <label key={option.name} htmlFor={option.name} title={option.name}>{question}</label>;
+        const label = <label key={option.name} htmlFor={option.name} title={option.doc}>{question}</label>;
         const buttons = option.values.map((v) => {
             const name = prettyOption ? prettyOption[v] : v;
             return <Button variant="light"
                 key={v}
+                title={v}
                 active={current_val == v}
                 onClick={() => setKey(option.name, v)}
             >
@@ -104,7 +105,7 @@ export default function Solver() {
         });
         return <tr key={option.name}>
             <td style={{width: "fit-content"}}>{label}</td>
-            <td style={{textAlign: "center"}}><ButtonGroup>{buttons}</ButtonGroup></td>
+            <td style={{textAlign: "left"}}><ButtonGroup>{buttons}</ButtonGroup></td>
         </tr>
     });