Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Apply all clippy warning #140

Merged
merged 1 commit into from
Oct 8, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion crates/formality-check/src/coherence.rs
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ impl Check<'_> {
&a.where_clauses,
&b.where_clauses,
),
&inverted_wc,
inverted_wc,
)
.is_ok()
}) {
Expand Down
6 changes: 3 additions & 3 deletions crates/formality-macros/src/cast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ pub(crate) fn upcast_impls(s: synstructure::Structure) -> Vec<TokenStream> {
let num_variants = s.variants().len();
s.variants()
.iter()
.filter(|v| num_variants == 1 || has_cast_attr(&v.ast().attrs))
.filter(|v| num_variants == 1 || has_cast_attr(v.ast().attrs))
.map(|v| upcast_to_variant(&s, v))
.chain(Some(self_upcast(&s)))
.collect()
Expand Down Expand Up @@ -46,7 +46,7 @@ pub(crate) fn downcast_impls(s: synstructure::Structure) -> Vec<TokenStream> {
let num_variants = s.variants().len();
s.variants()
.iter()
.filter(|v| num_variants == 1 || has_cast_attr(&v.ast().attrs))
.filter(|v| num_variants == 1 || has_cast_attr(v.ast().attrs))
.map(|v| downcast_to_variant(&s, v))
.chain(Some(self_downcast(&s)))
.collect()
Expand Down Expand Up @@ -91,5 +91,5 @@ fn downcast_to_variant(s: &synstructure::Structure, v: &VariantInfo) -> TokenStr
}

pub(crate) fn has_cast_attr(attrs: &[Attribute]) -> bool {
attrs.iter().find(|a| a.path.is_ident("cast")).is_some()
attrs.iter().any(|a| a.path.is_ident("cast"))
}
6 changes: 3 additions & 3 deletions crates/formality-macros/src/debug.rs
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ fn debug_variant(

// When invoked like `#[term(foo)]`, use the spec from `foo`
if let Some(spec) = external_spec {
return debug_variant_with_attr(variant, &spec);
return debug_variant_with_attr(variant, spec);
}

// Else, look for a `#[grammar]` attribute on the variant
Expand All @@ -58,7 +58,7 @@ fn debug_variant(

if variant.bindings().is_empty() {
// No bindings (e.g., `Foo`) -- just parse a keyword `foo`
let literal = Literal::string(&to_parse_ident(&ast.ident));
let literal = Literal::string(&to_parse_ident(ast.ident));
quote! {
write!(fmt, #literal)?;
}
Expand All @@ -79,7 +79,7 @@ fn debug_variant(
quote!(#(#streams)*)
} else {
// Otherwise -- parse `variant(binding0, ..., bindingN)`
let literal = Literal::string(&to_parse_ident(&ast.ident));
let literal = Literal::string(&to_parse_ident(ast.ident));
let binding_names: Vec<_> = variant.bindings().iter().map(|b| &b.binding).collect();
quote! {
fmt.debug_tuple(#literal)
Expand Down
26 changes: 11 additions & 15 deletions crates/formality-macros/src/fixed_point.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ impl syn::parse::Parse for FixedPointArgs {
while !input.is_empty() {
let ident: syn::Ident = input.parse()?;
let _: syn::Token!(=) = input.parse()?;
if ident.to_string() == "default" {
if ident == "default" {
let expr: syn::Expr = input.parse()?;
args.default = Some(expr);
} else {
Expand Down Expand Up @@ -226,7 +226,7 @@ fn validate_arg_pattern(pat: &syn::Pat) -> syn::Result<(syn::Ident, Option<syn::
));
}

Ok((ident.ident.clone(), ident.mutability.clone()))
Ok((ident.ident.clone(), ident.mutability))
}
_ => Err(syn::Error::new_spanned(
pat,
Expand All @@ -245,7 +245,7 @@ fn validate_arg_ty(ty: &syn::Type) -> syn::Result<(bool, syn::Type)> {
));
}

if let Some(_) = &r.lifetime {
if r.lifetime.is_some() {
return Err(syn::Error::new_spanned(
ty,
"named lifetimes not permitted in fixed-point functions",
Expand All @@ -265,19 +265,15 @@ fn validate_arg_ty(ty: &syn::Type) -> syn::Result<(bool, syn::Type)> {

fn validate_ty(ty: &syn::Type) -> syn::Result<()> {
match ty {
syn::Type::ImplTrait(_) => {
return Err(syn::Error::new_spanned(
ty,
"impl Trait types not allowed in fixed-point functions",
));
}
syn::Type::ImplTrait(_) => Err(syn::Error::new_spanned(
ty,
"impl Trait types not allowed in fixed-point functions",
)),

syn::Type::Reference(_) => {
return Err(syn::Error::new_spanned(
ty,
"reference types only allowed at the top-level in fixed-point functions",
));
}
syn::Type::Reference(_) => Err(syn::Error::new_spanned(
ty,
"reference types only allowed at the top-level in fixed-point functions",
)),

_ => Ok(()),
}
Expand Down
10 changes: 5 additions & 5 deletions crates/formality-macros/src/parse.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ pub(crate) fn derive_parse_with_spec(
let mut __results = vec![];
});
for variant in s.variants() {
let variant_name = as_literal(&variant.ast().ident);
let variant_name = as_literal(variant.ast().ident);
let v = parse_variant(variant, None)?;
stream.extend(quote! {
__results.push({
Expand Down Expand Up @@ -69,7 +69,7 @@ fn parse_variant(

// When invoked like `#[term(foo)]`, use the spec from `foo`
if let Some(spec) = external_spec {
return parse_variant_with_attr(variant, &spec);
return parse_variant_with_attr(variant, spec);
}

// Else, look for a `#[grammar]` attribute on the variant
Expand All @@ -81,7 +81,7 @@ fn parse_variant(

if variant.bindings().is_empty() {
// No bindings (e.g., `Foo`) -- just parse a keyword `foo`
let literal = Literal::string(&to_parse_ident(&ast.ident));
let literal = Literal::string(&to_parse_ident(ast.ident));
let construct = variant.construct(|_, _| quote! {});
Ok(quote! {
let ((), text) = parse::expect_keyword(#literal, text)?;
Expand All @@ -97,7 +97,7 @@ fn parse_variant(
})
} else {
// Otherwise -- parse `variant(binding0, ..., bindingN)`
let literal = Literal::string(&to_parse_ident(&ast.ident));
let literal = Literal::string(&to_parse_ident(ast.ident));
let build: Vec<TokenStream> = parse_bindings(variant.bindings());
let construct = variant.construct(field_ident);
Ok(quote! {
Expand Down Expand Up @@ -199,7 +199,7 @@ fn lookahead(for_field: &Ident, op: Option<&FormalitySpecOp>) -> syn::Result<Lit
Some(FormalitySpecOp::Keyword { .. }) | Some(FormalitySpecOp::Field { .. }) | None => {
Err(syn::Error::new_spanned(
for_field,
format!("cannot use `*` or `,` without lookahead"),
"cannot use `*` or `,` without lookahead".to_string(),
))
}
}
Expand Down
2 changes: 1 addition & 1 deletion crates/formality-macros/src/spec.rs
Original file line number Diff line number Diff line change
Expand Up @@ -129,5 +129,5 @@ fn parse_variable_binding(
_ => return error(),
};

Ok(FormalitySpecOp::Field { name, mode: mode })
Ok(FormalitySpecOp::Field { name, mode })
}
4 changes: 2 additions & 2 deletions crates/formality-prove/src/prove/combinators.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ where
let context = c1.substitution().apply(context);
let a = c1.substitution().apply(&a);
let b = c1.substitution().apply(&b);
zip(&decls, c1.env(), &context, a, b, op)
zip(decls, c1.env(), &context, a, b, op)
.into_iter()
.map(move |c2| c1.seq(c2))
})
Expand Down Expand Up @@ -60,7 +60,7 @@ where
.flat_map(|c1| {
let context = c1.substitution().apply(context);
let a_remaining = c1.substitution().apply(&a_remaining);
for_all(&decls, c1.env(), &context, &a_remaining, op)
for_all(decls, c1.env(), &context, &a_remaining, op)
.into_iter()
.map(move |c2| c1.seq(c2))
})
Expand Down
4 changes: 2 additions & 2 deletions crates/formality-prove/src/prove/env.rs
Original file line number Diff line number Diff line change
Expand Up @@ -186,8 +186,8 @@ impl Env {

let p0 = v[0];
let universe_p0 = self.universe(p0);
for i in 1..v.len() {
assert_eq!(self.universe(v[i]).index, universe_p0.index + i);
for (i, item) in v.iter().enumerate().skip(1) {
assert_eq!(self.universe(item).index, universe_p0.index + i);
}

self.variables.drain(universe_p0.index..).collect()
Expand Down
4 changes: 2 additions & 2 deletions crates/formality-prove/src/prove/prove_wc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -54,8 +54,8 @@ judgment_fn! {
(let i = i.binder.instantiate_with(&subst).unwrap())
(let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap())
(let co_assumptions = (&assumptions, &trait_ref))
(prove(&decls, env, &co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
(prove_after(&decls, c, &co_assumptions, &i.where_clause) => c)
(prove(&decls, env, co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
(prove_after(&decls, c, co_assumptions, &i.where_clause) => c)
(prove_after(&decls, c, &assumptions, &t.where_clause) => c)
----------------------------- ("positive impl")
(prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
Expand Down
6 changes: 3 additions & 3 deletions crates/formality-rust/src/grammar.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ impl Program {
_ => None,
})
.collect();
if traits.len() < 1 {
if traits.is_empty() {
anyhow::bail!("no trait named `{trait_id:?}`")
} else if traits.len() > 1 {
anyhow::bail!("multiple traits named `{trait_id:?}`")
Expand Down Expand Up @@ -84,9 +84,9 @@ impl Struct {
Adt {
id: self.id.clone(),
binder: Binder::new(
&vars,
vars,
AdtBoundData {
where_clauses: where_clauses,
where_clauses,
variants: vec![Variant {
name: VariantId::for_struct(),
fields,
Expand Down
9 changes: 4 additions & 5 deletions crates/formality-rust/src/prove.rs
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ impl Crate {
Some(prove::TraitDecl {
id: id.clone(),
binder: Binder::new(
&vars,
vars,
prove::TraitDeclBoundData {
where_clause: where_clauses
.iter()
Expand Down Expand Up @@ -123,7 +123,7 @@ impl Crate {
) = binder.open();
Some(prove::ImplDecl {
binder: Binder::new(
&vars,
vars,
prove::ImplDeclBoundData {
trait_ref: trait_id.with(self_ty, trait_parameters),
where_clause: where_clauses.to_wcs(),
Expand Down Expand Up @@ -152,7 +152,7 @@ impl Crate {
) = binder.open();
Some(prove::NegImplDecl {
binder: Binder::new(
&vars,
vars,
prove::NegImplDeclBoundData {
trait_ref: trait_id.with(self_ty, trait_parameters),
where_clause: where_clauses.to_wcs(),
Expand Down Expand Up @@ -259,8 +259,7 @@ impl Crate {
.iter()
.map(|e| {
let fresh_var = fresh_bound_var(ParameterKind::Ty);
let ensures =
Binder::new(&vec![fresh_var], e.to_wc(&fresh_var));
let ensures = Binder::new(vec![fresh_var], e.to_wc(fresh_var));

prove::AliasBoundDecl {
binder: Binder::new(
Expand Down
2 changes: 1 addition & 1 deletion crates/formality-rust/src/trait_binder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ where
let (data, text) = T::parse(&scope1, text)?;

let bound_vars: Vec<BoundVar> = bindings.iter().map(|b| b.bound_var).collect();
let explicit_binder = Binder::new(&bound_vars, data);
let explicit_binder = Binder::new(bound_vars, data);

Ok((TraitBinder { explicit_binder }, text))
}
Expand Down
2 changes: 1 addition & 1 deletion crates/formality-types/src/cast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -203,7 +203,7 @@ where
T: Upcast<U>,
{
fn upcast_from(term: &[T]) -> Self {
term.into_iter().map(|t| t.upcast()).collect()
term.iter().map(|t| t.upcast()).collect()
}
}

Expand Down
6 changes: 1 addition & 5 deletions crates/formality-types/src/collections.rs
Original file line number Diff line number Diff line change
Expand Up @@ -69,11 +69,7 @@ pub trait SetExt<T>: Sized {
impl<T: Ord + Clone> SetExt<T> for Set<T> {
fn split_first(self) -> Option<(T, Set<T>)> {
let mut iter = self.into_iter();
if let Some(e) = iter.next() {
Some((e, iter.collect()))
} else {
None
}
iter.next().map(|e| (e, iter.collect()))
}

fn union_with(mut self, other: Self) -> Self {
Expand Down
2 changes: 1 addition & 1 deletion crates/formality-types/src/fixed_point/stack.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ where
}

top.output = output;
return top.has_dependents;
top.has_dependents
}

/// Pops the top entry from the stack, returning the saved outputs.
Expand Down
6 changes: 2 additions & 4 deletions crates/formality-types/src/fold.rs
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ impl Fold for Const {
v.substitute(substitution_fn),
ty.substitute(substitution_fn),
),
ConstData::Variable(v) => match substitution_fn(v.clone()) {
ConstData::Variable(v) => match substitution_fn(*v) {
None => self.clone(),
Some(Parameter::Const(c)) => c,
Some(param) => panic!("ill-kinded substitute: expected const, got {param:?}"),
Expand Down Expand Up @@ -121,9 +121,7 @@ impl Fold for u32 {
}

impl Fold for () {
fn substitute(&self, _substitution_fn: SubstitutionFn<'_>) -> Self {
()
}
fn substitute(&self, _substitution_fn: SubstitutionFn<'_>) -> Self {}
}

impl<A: Fold, B: Fold> Fold for (A, B) {
Expand Down
14 changes: 9 additions & 5 deletions crates/formality-types/src/grammar/binder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ impl<T: Fold> Binder<T> {

pub fn dummy(term: T) -> Self {
let v: Vec<Variable> = vec![];
Self::new(&v, term)
Self::new(v, term)
}

/// Given a set of variables (X, Y, Z) and a term referecing some subset of them,
Expand Down Expand Up @@ -81,9 +81,9 @@ impl<T: Fold> Binder<T> {
pub fn mentioned(variables: impl Upcast<Vec<Variable>>, term: T) -> Self {
let mut variables: Vec<Variable> = variables.upcast();
let fv = term.free_variables();
variables.retain(|v| fv.contains(&v));
variables.retain(|v| fv.contains(v));
let variables: Vec<Variable> = variables.into_iter().collect();
Binder::new(&variables, term)
Binder::new(variables, term)
}

pub fn into<U>(self) -> Binder<U>
Expand All @@ -101,6 +101,10 @@ impl<T: Fold> Binder<T> {
self.kinds.len()
}

pub fn is_empty(&self) -> bool {
self.kinds.is_empty()
}

/// Instantiate the binder with the given parameters, returning an err if the parameters
/// are the wrong number or ill-kinded.
pub fn instantiate_with(&self, parameters: &[impl Upcast<Parameter>]) -> Fallible<T> {
Expand Down Expand Up @@ -136,7 +140,7 @@ impl<T: Fold> Binder<T> {
debruijn: Some(DebruijnIndex::INNERMOST),
var_index,
kind: _,
}) => Some(substitution[var_index.index as usize].clone()),
}) => Some(substitution[var_index.index].clone()),

_ => None,
})
Expand All @@ -156,7 +160,7 @@ impl<T: Fold> Binder<T> {
pub fn map<U: Fold>(&self, op: impl FnOnce(T) -> U) -> Binder<U> {
let (vars, t) = self.open();
let u = op(t);
Binder::new(&vars, u)
Binder::new(vars, u)
}
}

Expand Down
2 changes: 1 addition & 1 deletion crates/formality-types/src/grammar/consts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ impl Const {
pub fn as_variable(&self) -> Option<Variable> {
match self.data() {
ConstData::Value(_, _) => None,
ConstData::Variable(var) => Some(var.clone()),
ConstData::Variable(var) => Some(*var),
}
}

Expand Down
Loading
Loading