Skip to content

Commit 1d6f71e

Browse files
NadrierilNadrieril
committed
Replace "Expression" style with more-legible "Let" style
1 parent cd31811 commit 1d6f71e

File tree

100 files changed

+1103
-1108
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

100 files changed

+1103
-1108
lines changed

‎src/analyses/compute_rules.rs

+13-13
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ pub fn compute_rules<'a>(ctx: TypingCtx<'a>) -> Vec<TypingRule<'a>> {
4646
match pred.typing_rule(ctx) {
4747
Ok(rule) => {
4848
if TRACE {
49-
let rule_str = rule.display(PredicateStyle::Expression).unwrap();
49+
let rule_str = rule.display(PredicateStyle::Let).unwrap();
5050
let rule_str = rule_str.replace("\n", "\n ");
5151
println!(" Pushing rule:\n {rule_str}");
5252
}
@@ -185,8 +185,8 @@ impl TypeOfInterest {
185185

186186
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encode, Decode)]
187187
pub enum PredicateStyle {
188-
/// `pattern @ expression : ty`
189-
Expression,
188+
/// `let pattern : ty = expression`
189+
Let,
190190
/// `state ⊢ pattern : ty`
191191
Sequent {
192192
/// Which type is shown in the sequent.
@@ -207,7 +207,7 @@ pub struct PredicateExplanation {
207207

208208
impl PredicateStyle {
209209
pub(crate) const KNOWN_PREDICATE_STYLES: &[(&str, PredicateStyle)] = &[
210-
("Expression", PredicateStyle::Expression),
210+
("Let", PredicateStyle::Let),
211211
(
212212
"SequentUserVisible",
213213
PredicateStyle::Sequent {
@@ -228,7 +228,7 @@ impl PredicateStyle {
228228

229229
pub fn to_name(&self) -> &str {
230230
match self {
231-
PredicateStyle::Expression => "Expression",
231+
PredicateStyle::Let => "Let",
232232
PredicateStyle::Sequent {
233233
ty: TypeOfInterest::UserVisible,
234234
..
@@ -252,7 +252,7 @@ impl PredicateStyle {
252252

253253
pub fn type_of_interest(self) -> TypeOfInterest {
254254
match self {
255-
PredicateStyle::Expression => TypeOfInterest::UserVisible,
255+
PredicateStyle::Let => TypeOfInterest::UserVisible,
256256
PredicateStyle::Sequent { ty, .. } => ty,
257257
}
258258
}
@@ -271,7 +271,7 @@ impl PredicateStyle {
271271
/// Same as `self` but displays all the bits of state we know about.
272272
pub fn with_maximal_state(self) -> Self {
273273
match self {
274-
PredicateStyle::Expression => PredicateStyle::Expression,
274+
PredicateStyle::Let => PredicateStyle::Let,
275275
PredicateStyle::Sequent { ty, .. } => PredicateStyle::Sequent {
276276
ty,
277277
show_reference_state: true,
@@ -285,7 +285,7 @@ impl PredicateStyle {
285285

286286
let mut components = vec![];
287287
match self {
288-
PredicateStyle::Expression => {
288+
PredicateStyle::Let => {
289289
components.push(format!("{} is an expression", "e".code()));
290290
}
291291
PredicateStyle::Sequent {
@@ -401,7 +401,7 @@ impl<'a> TypingRule<'a> {
401401
// selected style.
402402
match style {
403403
// This style can display all expressions.
404-
Expression => {}
404+
Let => {}
405405
// In this style, only a few select expressions can be branched on (i.e. in the
406406
// postcondition). We error if the expression is not of an appropriate shape.
407407
Sequent {
@@ -445,7 +445,7 @@ impl<'a> TypingRule<'a> {
445445
let cstrs = self.collect_side_constraints();
446446
let mut postconditions = vec![RenderablePredicate::Pred(self.postcondition)];
447447
match style {
448-
Expression => {
448+
Let => {
449449
if cstrs.abstract_expr_is_not_ref {
450450
postconditions.push(RenderablePredicate::ExprNotRef(abstract_expr));
451451
}
@@ -457,7 +457,7 @@ impl<'a> TypingRule<'a> {
457457
}
458458
if let Some(mtbl) = cstrs.scrutinee_mutability {
459459
match style {
460-
Expression => {
460+
Let => {
461461
postconditions.push(RenderablePredicate::Mutability(abstract_expr, mtbl));
462462
}
463463
Sequent {
@@ -558,7 +558,7 @@ fn bundle_rules() -> anyhow::Result<()> {
558558

559559
for ((name, options), toi) in bundles {
560560
let style = match toi {
561-
None => PredicateStyle::Expression,
561+
None => PredicateStyle::Let,
562562
Some(ty) => {
563563
PredicateStyle::sequent_with_minimal_state(ty, options.into(), options.into())
564564
}
@@ -579,7 +579,7 @@ fn bundle_rules() -> anyhow::Result<()> {
579579
let _ = writeln!(&mut rules_str, "{rule}\n");
580580
}
581581
Err(err) => {
582-
let rule = rule.display(PredicateStyle::Expression).unwrap();
582+
let rule = rule.display(PredicateStyle::Let).unwrap();
583583
let _ = writeln!(
584584
&mut rules_str,
585585
"ERROR can't display the following rule with the requested style ({err:?})"

‎src/ast/printer.rs

+5-13
Original file line numberDiff line numberDiff line change
@@ -215,15 +215,6 @@ impl TypingResult<'_> {
215215
}
216216

217217
impl<'a> TypingPredicate<'a> {
218-
/// Display as `let ...`.
219-
pub fn display_as_let<'d>(&self, a: &'d Arenas<'d>) -> DisplayTree<'d> {
220-
self.pat
221-
.to_display_tree(a)
222-
.sep_then(a, ": ", self.expr.ty)
223-
.sep_then(a, " = ", self.expr.to_string())
224-
.preceded(a, "let ")
225-
}
226-
227218
pub fn display(&self, style: PredicateStyle) -> String {
228219
let a = &Arenas::default();
229220
self.display_to_tree(a, style).to_string()
@@ -232,11 +223,12 @@ impl<'a> TypingPredicate<'a> {
232223
/// Display according to the given predicate style.
233224
pub fn display_to_tree<'d>(&self, a: &'d Arenas<'d>, style: PredicateStyle) -> DisplayTree<'d> {
234225
match style {
235-
PredicateStyle::Expression => self
226+
PredicateStyle::Let => self
236227
.pat
237228
.to_display_tree(a)
238-
.sep_then(a, " @ ", self.expr.to_string())
239-
.sep_then(a, ": ", self.expr.ty),
229+
.sep_then(a, ": ", self.expr.ty)
230+
.sep_then(a, " = ", self.expr.to_string())
231+
.preceded(a, "let "),
240232
PredicateStyle::Sequent {
241233
ty: toi,
242234
show_reference_state,
@@ -424,7 +416,7 @@ impl Display for TypingRequest<'_> {
424416

425417
impl Display for TypingPredicate<'_> {
426418
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
427-
write!(f, "{}", self.display(PredicateStyle::Expression))
419+
write!(f, "{}", self.display(PredicateStyle::Let))
428420
}
429421
}
430422

‎src/cli.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ impl CliState {
4141
name: "predicate_style",
4242
values: &[
4343
OptionValue {
44-
name: "Expression",
44+
name: "Let",
4545
doc: "TODO",
4646
},
4747
OptionValue {
@@ -54,7 +54,7 @@ impl CliState {
5454
},
5555
],
5656
doc: "the style of the typing predicate; not all rulesets can be expressed in all styles, \
57-
only `Expression` is compatible with all rulesets",
57+
only `Let` is compatible with all rulesets",
5858
}];
5959

6060
pub fn new() -> Self {

‎src/solvers/ty_based.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ impl<'a> TypingSolver<'a> {
6060
"\n",
6161
self.done_predicates
6262
.iter()
63-
.map(|p| p.display_as_let(a))
63+
.map(|p| p.display_to_tree(a, PredicateStyle::Let))
6464
.chain(self.predicates.iter().map(|p| p.display_to_tree(a, style))),
6565
)
6666
}
@@ -82,7 +82,7 @@ impl<'a> TypingSolver<'a> {
8282
.err()
8383
.map(|err| format!(" // Borrow-check error: {err:?}"))
8484
.unwrap_or_default();
85-
let p = p.display_as_let(a);
85+
let p = p.display_to_tree(a, PredicateStyle::Let);
8686
p.sep_then(a, ";", bck)
8787
}),
8888
)

‎src/wasm.rs

+7-4
Original file line numberDiff line numberDiff line change
@@ -193,8 +193,8 @@ impl PredicateStyleJs {
193193
left: &RuleSetJs,
194194
right: &RuleSetJs,
195195
) -> Option<PredicateStyleJs> {
196-
let style = if name == "Expression" {
197-
PredicateStyle::Expression
196+
let style = if name == "Let" {
197+
PredicateStyle::Let
198198
} else {
199199
let ty = TypeOfInterest::from_str(name).ok()?;
200200
let left = left.as_ruleset();
@@ -205,13 +205,16 @@ impl PredicateStyleJs {
205205
}
206206

207207
pub fn to_name(&self) -> String {
208-
self.0.type_of_interest().to_str()
208+
match self.0 {
209+
PredicateStyle::Let => "Let".to_string(),
210+
PredicateStyle::Sequent { ty, .. } => ty.to_str(),
211+
}
209212
}
210213

211214
pub fn doc(&self) -> String {
212215
let mut out = String::new();
213216
match self.0 {
214-
PredicateStyle::Expression => {
217+
PredicateStyle::Let => {
215218
let _ = write!(
216219
&mut out,
217220
"Track the user-observable type along with the expression being matched on"

‎tests/generate_design_doc.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ fn generate_design_doc() -> anyhow::Result<()> {
2929
let a = &Arenas::default();
3030
for (example, comment) in examples {
3131
let req = TypingRequest::parse(a, &example).unwrap();
32-
let (trace, _) = trace_solver(a, req, options, PredicateStyle::Expression);
32+
let (trace, _) = trace_solver(a, req, options, PredicateStyle::Let);
3333
writeln!(&mut doc, "- `{example}` => {comment}")?;
3434
writeln!(&mut doc, "```rust")?;
3535
writeln!(&mut doc, "{trace}```")?;

‎tests/snapshots/bundle_rules@min_ergonomics-Expression.snap

-67
This file was deleted.

‎tests/snapshots/bundle_rules@min_ergonomics-Let.snap

+67
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
---
2+
source: src/analyses/compute_rules.rs
3+
info:
4+
bundle_name: min_ergonomics
5+
options:
6+
match_constructor_through_ref: true
7+
eat_inherited_ref_alone: false
8+
inherited_ref_on_ref: Error
9+
fallback_to_outer: "No"
10+
allow_ref_pat_on_ref_mut: false
11+
simplify_deref_mut: true
12+
downgrade_mut_inside_shared: false
13+
eat_mut_inside_shared: false
14+
ref_binding_on_inherited: Error
15+
mut_binding_on_inherited: Error
16+
---
17+
let p0: T0 = e.0, let p1: T1 = e.1
18+
----------------------------------- "Constructor"
19+
let [p0, p1]: [T0, T1] = e
20+
21+
let p0: &T0 = &(*e).0, let p1: &T1 = &(*e).1
22+
--------------------------------------------- "ConstructorRef"
23+
let [p0, p1]: &[T0, T1] = e
24+
25+
let p0: &mut T0 = &mut (*e).0, let p1: &mut T1 = &mut (*e).1
26+
------------------------------------------------------------- "ConstructorRef"
27+
let [p0, p1]: &mut [T0, T1] = e
28+
29+
let [p0, p1]: &T = &**e
30+
----------------------- "ConstructorMultiRef"
31+
let [p0, p1]: &&T = e
32+
33+
let [p0, p1]: &T = &**e
34+
------------------------- "ConstructorMultiRef"
35+
let [p0, p1]: &&mut T = e
36+
37+
let [p0, p1]: &T = &**e
38+
------------------------- "ConstructorMultiRef"
39+
let [p0, p1]: &mut &T = e
40+
41+
let [p0, p1]: &mut T = &mut **e
42+
------------------------------- "ConstructorMultiRef"
43+
let [p0, p1]: &mut &mut T = e
44+
45+
let p: T = *e
46+
------------------------------------ "Deref"
47+
let &p: &T = e, e is not a reference
48+
49+
let p: T = *e
50+
-------------------------------------------- "Deref"
51+
let &mut p: &mut T = e, e is not a reference
52+
53+
let x: &T = &e
54+
-------------------------------------- "BindingBorrow"
55+
let ref x: T = e, e is not a reference
56+
57+
let x: &mut T = &mut e
58+
------------------------------------------ "BindingBorrow"
59+
let ref mut x: T = e, e is not a reference
60+
61+
62+
------------ "Binding"
63+
let x: T = e
64+
65+
66+
-------------------------------------- "Binding"
67+
let mut x: T = e, e is not a reference

0 commit comments

Comments
 (0)