front: Hide unused predicate state automatically

src/analyses/compute_rules.rs

@@ -170,6 +170,20 @@ pub enum TypeOfInterest {
     InMemory,
 }
 
+impl TypeOfInterest {
+    pub fn to_str(&self) -> String {
+        format!("{self:?}")
+    }
+
+    pub fn from_str(name: &str) -> anyhow::Result<Self> {
+        Ok(match name {
+            "UserVisible" => TypeOfInterest::UserVisible,
+            "InMemory" => TypeOfInterest::InMemory,
+            _ => anyhow::bail!("unknown type of interest `{name}`"),
+        })
+    }
+}
+
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encode, Decode)]
 pub enum PredicateStyle {
     /// `pattern @ expression : ty`
@@ -226,7 +240,7 @@ impl PredicateStyle {
             .find(|(n, _)| *n == name)
         {
             Some((_, style)) => Ok(*style),
-            None => anyhow::bail!("unknown style {name}"),
+            None => anyhow::bail!("unknown style `{name}`"),
         }
     }
 

src/rulesets/mod.rs

@@ -71,10 +71,26 @@ impl RuleSet {
     }
 
     /// List options that can be changed without affecting the current rules.
-    pub fn irrelevant_options(self) -> &'static [&'static str] {
+    pub fn irrelevant_options(&self) -> &'static [&'static str] {
         match self {
             RuleSet::TypeBased(o) => o.irrelevant_options(),
-            RuleSet::BindingModeBased(c) => bm_based_irrelevant_options(c),
+            RuleSet::BindingModeBased(c) => bm_based_irrelevant_options(*c),
+        }
+    }
+
+    /// Whether this ruleset cares about scrutinee mutability.
+    pub fn tracks_scrut_mutability(&self) -> bool {
+        match self {
+            RuleSet::TypeBased(opts) => opts.tracks_scrut_mutability(),
+            RuleSet::BindingModeBased(_) => true,
+        }
+    }
+
+    /// Whether this ruleset tracks some state related to inherited references/binding mode.
+    pub fn tracks_reference_state(&self, ty: TypeOfInterest) -> bool {
+        match self {
+            RuleSet::TypeBased(opts) => opts.tracks_reference_state(ty),
+            RuleSet::BindingModeBased(_) => true,
         }
     }
 

src/rulesets/ty_based.rs

@@ -97,6 +97,55 @@ impl RuleOptions {
         }
     }
 
+    /// Whether this ruleset cares about scrutinee mutability.
+    /// Warning: will cause `IncompatibleStyle` crashes if incorrect.
+    pub fn tracks_scrut_mutability(&self) -> bool {
+        self.downgrade_mut_inside_shared
+    }
+
+    /// Whether this ruleset tracks some state related to inherited references/binding mode.
+    /// Warning: will cause `IncompatibleStyle` crashes if incorrect.
+    pub fn tracks_reference_state(&self, ty: TypeOfInterest) -> bool {
+        match ty {
+            // We always inspect the binding mode. More work would be needed to be able
+            // to represent rulesets that handle the binding mode generically.
+            TypeOfInterest::InMemory => true,
+            // We carefully inspect each rule to see if it inspects the expression. If
+            // it only inspects the type, that doesn't count as extra state.
+            TypeOfInterest::UserVisible => {
+                let RuleOptions {
+                    match_constructor_through_ref,
+                    eat_inherited_ref_alone,
+                    inherited_ref_on_ref,
+                    fallback_to_outer: _,
+                    allow_ref_pat_on_ref_mut: _,
+                    simplify_deref_mut: _,
+                    downgrade_mut_inside_shared: _,
+                    eat_mut_inside_shared: _,
+                    ref_binding_on_inherited,
+                    mut_binding_on_inherited,
+                } = *self;
+                if !match_constructor_through_ref {
+                    false
+                } else if matches!(inherited_ref_on_ref, InheritedRefOnRefBehavior::EatOuter)
+                    && matches!(
+                        ref_binding_on_inherited,
+                        RefBindingOnInheritedBehavior::AllocTemporary
+                    )
+                    && matches!(
+                        mut_binding_on_inherited,
+                        MutBindingOnInheritedBehavior::Keep
+                    )
+                    && eat_inherited_ref_alone
+                {
+                    false
+                } else {
+                    true
+                }
+            }
+        }
+    }
+
     pub fn to_map(&self) -> serde_json::Map<String, serde_json::Value> {
         let serde_json::Value::Object(map) = serde_json::to_value(self).unwrap() else {
             panic!()

src/wasm.rs

@@ -176,12 +176,32 @@ pub struct PredicateStyleJs(PredicateStyle);
 
 #[wasm_bindgen]
 impl PredicateStyleJs {
-    pub fn from_name(name: &str) -> Option<PredicateStyleJs> {
-        Some(PredicateStyleJs(PredicateStyle::from_name(name).ok()?))
+    pub fn from_name_and_option(name: &str, ruleset: &RuleSetJs) -> Option<PredicateStyleJs> {
+        // Silly but DRY
+        Self::from_name_and_options(name, ruleset, ruleset)
+    }
+
+    /// Constructs a sequent-style style based on the given name (reflecting the type of interest)
+    /// and the passed rulesets (reflecting )
+    pub fn from_name_and_options(
+        name: &str,
+        left: &RuleSetJs,
+        right: &RuleSetJs,
+    ) -> Option<PredicateStyleJs> {
+        let ty = TypeOfInterest::from_str(name).ok()?;
+        let left = left.as_ruleset();
+        let right = right.as_ruleset();
+        let style = PredicateStyle::Sequent {
+            ty,
+            show_reference_state: left.tracks_reference_state(ty)
+                || right.tracks_reference_state(ty),
+            show_scrut_access: left.tracks_scrut_mutability() || right.tracks_scrut_mutability(),
+        };
+        Some(PredicateStyleJs(style))
     }
 
     pub fn to_name(&self) -> String {
-        self.0.to_name().unwrap().to_string()
+        self.0.type_of_interest().to_str()
     }
 
     pub fn doc(&self) -> String {

web/src/components/Solver.jsx

@@ -95,9 +95,9 @@ export function Help({show, setShow, style}) {
     </>
 }
 
-const availableStyles = ['Sequent', 'SequentBindingMode'];
+const availableStyles = ['UserVisible', 'InMemory'];
 
-export function MainNavBar({compare, setCompare, style, setStyle}) {
+export function MainNavBar({compare, setCompare, style, setStyleName, styleMap}) {
     const navigate = useNavigate()
     const [searchParams, setSearchParams] = useSearchParams();
     function resetSearchParams() {
@@ -114,11 +114,11 @@ export function MainNavBar({compare, setCompare, style, setStyle}) {
 
     const currentStyle = style;
     const styles = availableStyles.map(style_name => {
-        let style = PredicateStyleJs.from_name(style_name);
+        let style = styleMap[style_name];
         return <OverlayTrigger key={style_name} placement="bottom" overlay={<Tooltip>{style.doc()}</Tooltip>}>
             <Button
                 active={currentStyle.to_name() == style_name}
-                onClick={() => setStyle(style)}
+                onClick={() => setStyleName(style_name)}
                 dangerouslySetInnerHTML={{__html: style.display_generic_predicate()}}
             ></Button>
         </OverlayTrigger>
@@ -399,17 +399,34 @@ export default function Solver() {
     const [searchParams, setSearchParams] = useSearchParams();
     const sp = {searchParams, setSearchParams};
     const [compare, setCompare] = useStateInParams(sp, 'compare', false, (x) => x == 'true');
-    const defaultStyle = PredicateStyleJs.from_name('Sequent');
-    const [style, setStyle] = useStateInParams(sp, 'style', defaultStyle, PredicateStyleJs.from_name, (style) => style.to_name());
     const [optionsLeft, setOptionsLeft] = useStateInParams(sp, 'opts1', RuleSetJs.from_bundle_name('nadri', 'stable'), RuleSetJs.decode, (o) => o.encode());
     const [optionsRight, setOptionsRight] = useStateInParams(sp, 'opts2', RuleSetJs.from_bundle_name('rfc3627', 'rfc3627'), RuleSetJs.decode, (o) => o.encode());
     const [inputQuery, setInputQuery] = useStateInParams(sp, 'q', "[&x]: &mut [&T]");
     const [mode, setMode] = useStateInParams(sp, 'mode', 'typechecker', validateIn(['typechecker', 'rules', 'compare']));
+    const [styleName, setStyleName] = useStateInParams(sp, 'style', 'UserVisible',  validateIn(['UserVisible', 'InMemory', 'Sequent', 'SequentBindingMode']));
+
+    // Map from style name to predicate style. Takes into account the selected
+    // options to hide parts of the predicate we don't care about.
+    const styleMap = useMemo(() => {
+        var map = availableStyles.reduce(function(map, style_name) {
+            if(compare) {
+                map[style_name] = PredicateStyleJs.from_name_and_options(style_name, optionsLeft, optionsRight);
+            } else {
+                map[style_name] = PredicateStyleJs.from_name_and_option(style_name, optionsLeft);
+            }
+            return map;
+        }, {});
+        // Back-compat with permalinks that used the old style names.
+        map['Sequent'] = map['UserVisible'];
+        map['SequentBindingMode'] = map['InMemory'];
+        return map;
+    }, [compare, optionsLeft, optionsRight]);
+    const style = styleMap[styleName];
 
     return (
         <>
             <div className="sticky-top">
-                <MainNavBar {...{compare, setCompare, style, setStyle}}/>
+                <MainNavBar {...{compare, setCompare, style, setStyleName, styleMap}}/>
                 <SolverOptions options={optionsLeft} setOptions={setOptionsLeft} title={compare ? <>Left&nbsp;&nbsp;&nbsp;</> : null}/>
                 {compare ? <SolverOptions options={optionsRight} setOptions={setOptionsRight} title="Right"/> : null}
             </div>