Skip to content

Commit

Permalink
Apply all clippy warning
Browse files Browse the repository at this point in the history
  • Loading branch information
obeis committed Sep 20, 2023
1 parent 13b4ad8 commit afe8d65
Show file tree
Hide file tree
Showing 23 changed files with 68 additions and 79 deletions.
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

0 comments on commit afe8d65

Please sign in to comment.