Skip to content

Commit 0397678

Browse files
W95PspW95Psp
authored
Merge pull request #1540 from cryspen/rengine-lean-fix-warning
chore(rengine/lean): fix warnings
2 parents e96f858 + bd80280 commit 0397678

File tree

2 files changed

+91
-74
lines changed

2 files changed

+91
-74
lines changed

‎rust-engine/src/ast/identifiers.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,7 @@ pub mod global_id {
120120
})
121121
.collect::<Vec<String>>()
122122
.join("_"),
123-
GlobalId::Projector(concrete_id) => todo!(),
123+
GlobalId::Projector(_concrete_id) => todo!(),
124124
}
125125
}
126126
}

‎rust-engine/src/lean.rs‎

Lines changed: 90 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -36,10 +36,10 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ItemKind {
3636
match self {
3737
ItemKind::Fn {
3838
name,
39-
generics,
39+
generics: _,
4040
body,
4141
params,
42-
safety,
42+
safety: _,
4343
} => {
4444
// Generics are ignored for now
4545
docs![
@@ -59,37 +59,42 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ItemKind {
5959
.nest(INDENT)
6060
.group()
6161
}
62-
ItemKind::TyAlias { name, generics, ty } => {
63-
docs![allocator, "abbrev ", name, allocator.reflow(" := "), ty].group()
64-
}
65-
ItemKind::Type {
62+
ItemKind::TyAlias {
6663
name,
67-
generics,
68-
variants,
69-
is_struct,
64+
generics: _,
65+
ty,
66+
} => docs![allocator, "abbrev ", name, allocator.reflow(" := "), ty].group(),
67+
ItemKind::Type {
68+
name: _,
69+
generics: _,
70+
variants: _,
71+
is_struct: _,
7072
} => print_todo!(allocator),
7173
ItemKind::Trait {
72-
name,
73-
generics,
74-
items,
74+
name: _,
75+
generics: _,
76+
items: _,
7577
} => print_todo!(allocator),
7678
ItemKind::Impl {
77-
generics,
78-
self_ty,
79-
of_trait,
80-
items,
81-
parent_bounds,
82-
safety,
79+
generics: _,
80+
self_ty: _,
81+
of_trait: _,
82+
items: _,
83+
parent_bounds: _,
84+
safety: _,
8385
} => print_todo!(allocator),
84-
ItemKind::Alias { name, item } => print_todo!(allocator),
86+
ItemKind::Alias { name: _, item: _ } => print_todo!(allocator),
8587
ItemKind::Use {
86-
path,
87-
is_external,
88-
rename,
88+
path: _,
89+
is_external: _,
90+
rename: _,
8991
} => allocator.nil(),
90-
ItemKind::Quote { quote, origin } => print_todo!(allocator),
91-
ItemKind::Error(diagnostic) => print_todo!(allocator),
92-
ItemKind::Resugared(resugared_ty_kind) => print_todo!(allocator),
92+
ItemKind::Quote {
93+
quote: _,
94+
origin: _,
95+
} => print_todo!(allocator),
96+
ItemKind::Error(_diagnostic) => print_todo!(allocator),
97+
ItemKind::Resugared(_resugared_ty_kind) => print_todo!(allocator),
9398
ItemKind::NotImplementedYet => allocator.text("-- unimplemented yet"),
9499
}
95100
}
@@ -124,9 +129,9 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b TyKind {
124129
)
125130
.parens(),
126131
TyKind::Ref {
127-
inner,
128-
mutable,
129-
region,
132+
inner: _,
133+
mutable: _,
134+
region: _,
130135
} => print_todo!(allocator),
131136
TyKind::Param(local_id) => local_id.pretty(allocator),
132137
TyKind::Slice(ty) => docs![allocator, "Array ", ty].parens(),
@@ -136,11 +141,11 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b TyKind {
136141
.group()
137142
}
138143
TyKind::RawPointer => print_todo!(allocator),
139-
TyKind::AssociatedType { impl_, item } => print_todo!(allocator),
140-
TyKind::Opaque(global_id) => print_todo!(allocator),
141-
TyKind::Dyn(dyn_trait_goals) => print_todo!(allocator),
142-
TyKind::Resugared(resugared_ty_kind) => print_todo!(allocator),
143-
TyKind::Error(diagnostic) => print_todo!(allocator),
144+
TyKind::AssociatedType { impl_: _, item: _ } => print_todo!(allocator),
145+
TyKind::Opaque(_global_id) => print_todo!(allocator),
146+
TyKind::Dyn(_dyn_trait_goals) => print_todo!(allocator),
147+
TyKind::Resugared(_resugared_ty_kind) => print_todo!(allocator),
148+
TyKind::Error(_diagnostic) => print_todo!(allocator),
144149
}
145150
}
146151
}
@@ -184,10 +189,10 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b PatKind {
184189
.nest(INDENT)
185190
.group()
186191
}
187-
PatKind::Or { sub_pats } => print_todo!(allocator),
188-
PatKind::Array { args } => print_todo!(allocator),
189-
PatKind::Deref { sub_pat } => print_todo!(allocator),
190-
PatKind::Constant { lit } => print_todo!(allocator),
192+
PatKind::Or { sub_pats: _ } => print_todo!(allocator),
193+
PatKind::Array { args: _ } => print_todo!(allocator),
194+
PatKind::Deref { sub_pat: _ } => print_todo!(allocator),
195+
PatKind::Constant { lit: _ } => print_todo!(allocator),
191196
PatKind::Binding {
192197
mutable,
193198
var,
@@ -198,13 +203,13 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b PatKind {
198203
_ => panic!(),
199204
},
200205
PatKind::Construct {
201-
constructor,
202-
is_record,
203-
is_struct,
204-
fields,
206+
constructor: _,
207+
is_record: _,
208+
is_struct: _,
209+
fields: _,
205210
} => print_todo!(allocator),
206-
PatKind::Resugared(resugared_pat_kind) => print_todo!(allocator),
207-
PatKind::Error(diagnostic) => print_todo!(allocator),
211+
PatKind::Resugared(_resugared_pat_kind) => print_todo!(allocator),
212+
PatKind::Error(_diagnostic) => print_todo!(allocator),
208213
}
209214
}
210215
}
@@ -238,9 +243,9 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ExprKind {
238243
ExprKind::App {
239244
head,
240245
args,
241-
generic_args,
242-
bounds_impls,
243-
trait_,
246+
generic_args: _,
247+
bounds_impls: _,
248+
trait_: _,
244249
} => {
245250
let separator = allocator.line();
246251
head.pretty(allocator)
@@ -261,10 +266,10 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ExprKind {
261266
.group(),
262267
ExprKind::Construct {
263268
constructor,
264-
is_record,
265-
is_struct,
269+
is_record: _,
270+
is_struct: _,
266271
fields,
267-
base,
272+
base: _,
268273
} => {
269274
// Should be turned into a resugaring once https://github.com/cryspen/hax/pull/1528 have been merged
270275
let record_args = if fields.len() > 0 {
@@ -295,11 +300,20 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ExprKind {
295300
.group()
296301
.nest(INDENT)
297302
}
298-
ExprKind::Match { scrutinee, arms } => print_todo!(allocator),
299-
ExprKind::Tuple(exprs) => print_todo!(allocator),
300-
ExprKind::Borrow { mutable, inner } => print_todo!(allocator),
301-
ExprKind::AddressOf { mutable, inner } => print_todo!(allocator),
302-
ExprKind::Deref(expr) => print_todo!(allocator),
303+
ExprKind::Match {
304+
scrutinee: _,
305+
arms: _,
306+
} => print_todo!(allocator),
307+
ExprKind::Tuple(_exprs) => print_todo!(allocator),
308+
ExprKind::Borrow {
309+
mutable: _,
310+
inner: _,
311+
} => print_todo!(allocator),
312+
ExprKind::AddressOf {
313+
mutable: _,
314+
inner: _,
315+
} => print_todo!(allocator),
316+
ExprKind::Deref(_expr) => print_todo!(allocator),
303317
ExprKind::Let { lhs, rhs, body } => {
304318
docs![
305319
allocator,
@@ -319,21 +333,21 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ExprKind {
319333
.nest(INDENT)
320334
.parens()
321335
.group(),
322-
ExprKind::Assign { lhs, value } => print_todo!(allocator),
336+
ExprKind::Assign { lhs: _, value: _ } => print_todo!(allocator),
323337
ExprKind::Loop {
324-
body,
325-
kind,
326-
state,
327-
control_flow,
328-
label,
338+
body: _,
339+
kind: _,
340+
state: _,
341+
control_flow: _,
342+
label: _,
329343
} => print_todo!(allocator),
330-
ExprKind::Break { value, label } => print_todo!(allocator),
331-
ExprKind::Return { value } => print_todo!(allocator),
332-
ExprKind::Continue { label } => print_todo!(allocator),
344+
ExprKind::Break { value: _, label: _ } => print_todo!(allocator),
345+
ExprKind::Return { value: _ } => print_todo!(allocator),
346+
ExprKind::Continue { label: _ } => print_todo!(allocator),
333347
ExprKind::Closure {
334348
params,
335349
body,
336-
captures,
350+
captures: _,
337351
} => docs![
338352
allocator,
339353
allocator.reflow("fun "),
@@ -345,10 +359,13 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b ExprKind {
345359
.nest(INDENT)
346360
.group()
347361
.parens(),
348-
ExprKind::Block { body, safety_mode } => print_todo!(allocator),
349-
ExprKind::Quote { contents } => print_todo!(allocator),
350-
ExprKind::Resugared(resugared_expr_kind) => print_todo!(allocator),
351-
ExprKind::Error(diagnostic) => print_todo!(allocator),
362+
ExprKind::Block {
363+
body: _,
364+
safety_mode: _,
365+
} => print_todo!(allocator),
366+
ExprKind::Quote { contents: _ } => print_todo!(allocator),
367+
ExprKind::Resugared(_resugared_expr_kind) => print_todo!(allocator),
368+
ExprKind::Error(_diagnostic) => print_todo!(allocator),
352369
}
353370
}
354371
}
@@ -363,13 +380,13 @@ impl<'a, 'b> Pretty<'a, Allocator<Lean>, Span> for &'b Literal {
363380
Literal::Bool(b) => format!("{}", b),
364381
Literal::Int {
365382
value,
366-
negative,
367-
kind,
383+
negative: _,
384+
kind: _,
368385
} => format!("{}", value),
369386
Literal::Float {
370-
value,
371-
negative,
372-
kind,
387+
value: _,
388+
negative: _,
389+
kind: _,
373390
} => todo!(),
374391
}
375392
]

0 commit comments

Comments
 (0)