Replace "Expression" style with more-legible "Let" style

src/analyses/compute_rules.rs

@@ -46,7 +46,7 @@ pub fn compute_rules<'a>(ctx: TypingCtx<'a>) -> Vec<TypingRule<'a>> {
         match pred.typing_rule(ctx) {
             Ok(rule) => {
                 if TRACE {
-                    let rule_str = rule.display(PredicateStyle::Expression).unwrap();
+                    let rule_str = rule.display(PredicateStyle::Let).unwrap();
                     let rule_str = rule_str.replace("\n", "\n    ");
                     println!("  Pushing rule:\n    {rule_str}");
                 }
@@ -185,8 +185,8 @@ impl TypeOfInterest {
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encode, Decode)]
 pub enum PredicateStyle {
-    /// `pattern @ expression : ty`
-    Expression,
+    /// `let pattern : ty = expression`
+    Let,
     /// `state ⊢ pattern : ty`
     Sequent {
         /// Which type is shown in the sequent.
@@ -207,7 +207,7 @@ pub struct PredicateExplanation {
 
 impl PredicateStyle {
     pub(crate) const KNOWN_PREDICATE_STYLES: &[(&str, PredicateStyle)] = &[
-        ("Expression", PredicateStyle::Expression),
+        ("Let", PredicateStyle::Let),
         (
             "SequentUserVisible",
             PredicateStyle::Sequent {
@@ -228,7 +228,7 @@ impl PredicateStyle {
 
     pub fn to_name(&self) -> &str {
         match self {
-            PredicateStyle::Expression => "Expression",
+            PredicateStyle::Let => "Let",
             PredicateStyle::Sequent {
                 ty: TypeOfInterest::UserVisible,
                 ..
@@ -252,7 +252,7 @@ impl PredicateStyle {
 
     pub fn type_of_interest(self) -> TypeOfInterest {
         match self {
-            PredicateStyle::Expression => TypeOfInterest::UserVisible,
+            PredicateStyle::Let => TypeOfInterest::UserVisible,
             PredicateStyle::Sequent { ty, .. } => ty,
         }
     }
@@ -271,7 +271,7 @@ impl PredicateStyle {
     /// Same as `self` but displays all the bits of state we know about.
     pub fn with_maximal_state(self) -> Self {
         match self {
-            PredicateStyle::Expression => PredicateStyle::Expression,
+            PredicateStyle::Let => PredicateStyle::Let,
             PredicateStyle::Sequent { ty, .. } => PredicateStyle::Sequent {
                 ty,
                 show_reference_state: true,
@@ -285,7 +285,7 @@ impl PredicateStyle {
 
         let mut components = vec![];
         match self {
-            PredicateStyle::Expression => {
+            PredicateStyle::Let => {
                 components.push(format!("{} is an expression", "e".code()));
             }
             PredicateStyle::Sequent {
@@ -401,7 +401,7 @@ impl<'a> TypingRule<'a> {
         // selected style.
         match style {
             // This style can display all expressions.
-            Expression => {}
+            Let => {}
             // In this style, only a few select expressions can be branched on (i.e. in the
             // postcondition). We error if the expression is not of an appropriate shape.
             Sequent {
@@ -445,7 +445,7 @@ impl<'a> TypingRule<'a> {
         let cstrs = self.collect_side_constraints();
         let mut postconditions = vec![RenderablePredicate::Pred(self.postcondition)];
         match style {
-            Expression => {
+            Let => {
                 if cstrs.abstract_expr_is_not_ref {
                     postconditions.push(RenderablePredicate::ExprNotRef(abstract_expr));
                 }
@@ -457,7 +457,7 @@ impl<'a> TypingRule<'a> {
         }
         if let Some(mtbl) = cstrs.scrutinee_mutability {
             match style {
-                Expression => {
+                Let => {
                     postconditions.push(RenderablePredicate::Mutability(abstract_expr, mtbl));
                 }
                 Sequent {
@@ -558,7 +558,7 @@ fn bundle_rules() -> anyhow::Result<()> {
 
     for ((name, options), toi) in bundles {
         let style = match toi {
-            None => PredicateStyle::Expression,
+            None => PredicateStyle::Let,
             Some(ty) => {
                 PredicateStyle::sequent_with_minimal_state(ty, options.into(), options.into())
             }
@@ -579,7 +579,7 @@ fn bundle_rules() -> anyhow::Result<()> {
                     let _ = writeln!(&mut rules_str, "{rule}\n");
                 }
                 Err(err) => {
-                    let rule = rule.display(PredicateStyle::Expression).unwrap();
+                    let rule = rule.display(PredicateStyle::Let).unwrap();
                     let _ = writeln!(
                         &mut rules_str,
                         "ERROR can't display the following rule with the requested style ({err:?})"

src/ast/printer.rs

@@ -215,15 +215,6 @@ impl TypingResult<'_> {
 }
 
 impl<'a> TypingPredicate<'a> {
-    /// Display as `let ...`.
-    pub fn display_as_let<'d>(&self, a: &'d Arenas<'d>) -> DisplayTree<'d> {
-        self.pat
-            .to_display_tree(a)
-            .sep_then(a, ": ", self.expr.ty)
-            .sep_then(a, " = ", self.expr.to_string())
-            .preceded(a, "let ")
-    }
-
     pub fn display(&self, style: PredicateStyle) -> String {
         let a = &Arenas::default();
         self.display_to_tree(a, style).to_string()
@@ -232,11 +223,12 @@ impl<'a> TypingPredicate<'a> {
     /// Display according to the given predicate style.
     pub fn display_to_tree<'d>(&self, a: &'d Arenas<'d>, style: PredicateStyle) -> DisplayTree<'d> {
         match style {
-            PredicateStyle::Expression => self
+            PredicateStyle::Let => self
                 .pat
                 .to_display_tree(a)
-                .sep_then(a, " @ ", self.expr.to_string())
-                .sep_then(a, ": ", self.expr.ty),
+                .sep_then(a, ": ", self.expr.ty)
+                .sep_then(a, " = ", self.expr.to_string())
+                .preceded(a, "let "),
             PredicateStyle::Sequent {
                 ty: toi,
                 show_reference_state,
@@ -424,7 +416,7 @@ impl Display for TypingRequest<'_> {
 
 impl Display for TypingPredicate<'_> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "{}", self.display(PredicateStyle::Expression))
+        write!(f, "{}", self.display(PredicateStyle::Let))
     }
 }
 

src/cli.rs

@@ -41,7 +41,7 @@ impl CliState {
         name: "predicate_style",
         values: &[
             OptionValue {
-                name: "Expression",
+                name: "Let",
                 doc: "TODO",
             },
             OptionValue {
@@ -54,7 +54,7 @@ impl CliState {
             },
         ],
         doc: "the style of the typing predicate; not all rulesets can be expressed in all styles, \
-        only `Expression` is compatible with all rulesets",
+                only `Let` is compatible with all rulesets",
     }];
 
     pub fn new() -> Self {

src/solvers/ty_based.rs

@@ -60,7 +60,7 @@ impl<'a> TypingSolver<'a> {
             "\n",
             self.done_predicates
                 .iter()
-                .map(|p| p.display_as_let(a))
+                .map(|p| p.display_to_tree(a, PredicateStyle::Let))
                 .chain(self.predicates.iter().map(|p| p.display_to_tree(a, style))),
         )
     }
@@ -82,7 +82,7 @@ impl<'a> TypingSolver<'a> {
                     .err()
                     .map(|err| format!(" // Borrow-check error: {err:?}"))
                     .unwrap_or_default();
-                let p = p.display_as_let(a);
+                let p = p.display_to_tree(a, PredicateStyle::Let);
                 p.sep_then(a, ";", bck)
             }),
         )

src/wasm.rs

@@ -193,8 +193,8 @@ impl PredicateStyleJs {
         left: &RuleSetJs,
         right: &RuleSetJs,
     ) -> Option<PredicateStyleJs> {
-        let style = if name == "Expression" {
-            PredicateStyle::Expression
+        let style = if name == "Let" {
+            PredicateStyle::Let
         } else {
             let ty = TypeOfInterest::from_str(name).ok()?;
             let left = left.as_ruleset();
@@ -205,13 +205,16 @@ impl PredicateStyleJs {
     }
 
     pub fn to_name(&self) -> String {
-        self.0.type_of_interest().to_str()
+        match self.0 {
+            PredicateStyle::Let => "Let".to_string(),
+            PredicateStyle::Sequent { ty, .. } => ty.to_str(),
+        }
     }
 
     pub fn doc(&self) -> String {
         let mut out = String::new();
         match self.0 {
-            PredicateStyle::Expression => {
+            PredicateStyle::Let => {
                 let _ = write!(
                     &mut out,
                     "Track the user-observable type along with the expression being matched on"

tests/generate_design_doc.rs

@@ -29,7 +29,7 @@ fn generate_design_doc() -> anyhow::Result<()> {
     let a = &Arenas::default();
     for (example, comment) in examples {
         let req = TypingRequest::parse(a, &example).unwrap();
-        let (trace, _) = trace_solver(a, req, options, PredicateStyle::Expression);
+        let (trace, _) = trace_solver(a, req, options, PredicateStyle::Let);
         writeln!(&mut doc, "- `{example}` => {comment}")?;
         writeln!(&mut doc, "```rust")?;
         writeln!(&mut doc, "{trace}```")?;

tests/snapshots/bundle_rules@min_ergonomics-Let.snap

@@ -0,0 +1,67 @@
+---
+source: src/analyses/compute_rules.rs
+info:
+  bundle_name: min_ergonomics
+  options:
+    match_constructor_through_ref: true
+    eat_inherited_ref_alone: false
+    inherited_ref_on_ref: Error
+    fallback_to_outer: "No"
+    allow_ref_pat_on_ref_mut: false
+    simplify_deref_mut: true
+    downgrade_mut_inside_shared: false
+    eat_mut_inside_shared: false
+    ref_binding_on_inherited: Error
+    mut_binding_on_inherited: Error
+---
+let p0: T0 = e.0,  let p1: T1 = e.1
+----------------------------------- "Constructor"
+let [p0, p1]: [T0, T1] = e
+
+let p0: &T0 = &(*e).0,  let p1: &T1 = &(*e).1
+--------------------------------------------- "ConstructorRef"
+let [p0, p1]: &[T0, T1] = e
+
+let p0: &mut T0 = &mut (*e).0,  let p1: &mut T1 = &mut (*e).1
+------------------------------------------------------------- "ConstructorRef"
+let [p0, p1]: &mut [T0, T1] = e
+
+let [p0, p1]: &T = &**e
+----------------------- "ConstructorMultiRef"
+let [p0, p1]: &&T = e
+
+let [p0, p1]: &T = &**e
+------------------------- "ConstructorMultiRef"
+let [p0, p1]: &&mut T = e
+
+let [p0, p1]: &T = &**e
+------------------------- "ConstructorMultiRef"
+let [p0, p1]: &mut &T = e
+
+let [p0, p1]: &mut T = &mut **e
+------------------------------- "ConstructorMultiRef"
+let [p0, p1]: &mut &mut T = e
+
+let p: T = *e
+------------------------------------ "Deref"
+let &p: &T = e, e is not a reference
+
+let p: T = *e
+-------------------------------------------- "Deref"
+let &mut p: &mut T = e, e is not a reference
+
+let x: &T = &e
+-------------------------------------- "BindingBorrow"
+let ref x: T = e, e is not a reference
+
+let x: &mut T = &mut e
+------------------------------------------ "BindingBorrow"
+let ref mut x: T = e, e is not a reference
+
+
+------------ "Binding"
+let x: T = e
+
+
+-------------------------------------- "Binding"
+let mut x: T = e, e is not a reference