front: describe display styles programmatically

Author: Nadrieril

src/wasm.rs

@@ -184,6 +184,46 @@ impl PredicateStyleJs {
         self.0.to_name().unwrap().to_string()
     }
 
+    pub fn doc(&self) -> String {
+        let mut out = String::new();
+        match self.0 {
+            PredicateStyle::Expression => {
+                todo!("explain expression style")
+            }
+            PredicateStyle::Sequent {
+                ty: type_of_interest,
+                show_reference_state,
+                ..
+            } => {
+                let _ = write!(&mut out, "Track the type ");
+                match type_of_interest {
+                    TypeOfInterest::UserVisible => {
+                        let _ = write!(&mut out, "that the user observes");
+                        if show_reference_state {
+                            let _ = write!(&mut out, " and whether the outermost reference in the type is real or inherited");
+                        }
+                    }
+                    TypeOfInterest::InMemory => {
+                        let _ = write!(&mut out, "of the matched place");
+                        if show_reference_state {
+                            let _ = write!(&mut out, " and the current binding mode");
+                        }
+                    }
+                }
+            }
+        }
+        out
+    }
+
+    pub fn display_generic_predicate(&self) -> String {
+        let a = &Arenas::default();
+        TypingPredicate {
+            pat: &Pattern::ABSTRACT,
+            expr: Expression::ABSTRACT.borrow(a, Mutability::Shared),
+        }
+        .display(self.0)
+    }
+
     pub fn explain_predicate(&self) -> String {
         let explanation = self.0.explain_predicate();
         let mut out = String::new();

web/src/components/Solver.jsx

@@ -50,19 +50,6 @@ function InhRef() {
     return <span className="inherited-ref" title="inherited reference">&</span>
 }
 
-const availableStyles = [
-    {
-        name: 'Sequent',
-        display: <>inh, _ ⊢ p: <InhRef/>T</>,
-        doc: "Track the type that the user observes and whether the outermost reference in the type is real or inherited"
-    },
-    {
-        name: 'SequentBindingMode',
-        display: <>ref, _ ⊢ p: T</>,
-        doc: "Track the type of the matched place and the current binding mode"
-    },
-];
-
 export function Help({show, setShow, style}) {
     return <>
         <Offcanvas placement="end" scroll show={show} onHide={() => setShow(false)}>
@@ -108,6 +95,8 @@ export function Help({show, setShow, style}) {
     </>
 }
 
+const availableStyles = ['Sequent', 'SequentBindingMode'];
+
 export function MainNavBar({compare, setCompare, style, setStyle}) {
     const navigate = useNavigate()
     const [searchParams, setSearchParams] = useSearchParams();
@@ -124,14 +113,14 @@ export function MainNavBar({compare, setCompare, style, setStyle}) {
     const [helpShow, setHelpShow] = useState(false);
 
     const currentStyle = style;
-    const styles = availableStyles.map(style => {
-        return <OverlayTrigger key={style.name} placement="bottom" overlay={<Tooltip>{style.doc}</Tooltip>}>
+    const styles = availableStyles.map(style_name => {
+        let style = PredicateStyleJs.from_name(style_name);
+        return <OverlayTrigger key={style_name} placement="bottom" overlay={<Tooltip>{style.doc()}</Tooltip>}>
             <Button
-                active={currentStyle.to_name() == style.name}
-                onClick={() => setStyle(PredicateStyleJs.from_name(style.name))}
-            >
-                {style.display}
-            </Button>
+                active={currentStyle.to_name() == style_name}
+                onClick={() => setStyle(style)}
+                dangerouslySetInnerHTML={{__html: style.display_generic_predicate()}}
+            ></Button>
         </OverlayTrigger>
     });