auto-generate constructors for structs, variants

Author: nikomatsakis

crates/formality-check/src/where_clauses.rs

@@ -51,7 +51,7 @@ impl super::Check<'_> {
             WhereClauseData::TypeOfConst(ct, ty) => {
                 match ct.data() {
                     ConstData::Value(_, t) => {
-                        self.prove_goal(in_env, &assumptions, Relation::eq(ty, t))?
+                        self.prove_goal(in_env, &assumptions, Relation::equals(ty, t))?
                     }
                     ConstData::Variable(_) => {}
                 }

crates/formality-macros/src/constructors.rs

@@ -0,0 +1,78 @@
+use convert_case::{Case, Casing};
+use proc_macro2::{Ident, TokenStream};
+use quote::quote_spanned;
+use synstructure::VariantInfo;
+
+const RUST_KEYWORDS: &[&str] = &[
+    "mut", "true", "false", "const", "static", "ref", "struct", "enum", "trait", "union", "fn",
+    "use", "return", "move", "let", "break", "loop", "continue", "await", "if", "for",
+];
+
+/// Create methods to build this type.
+///
+/// For a struct, we create a single `new` method that takes each field.
+///
+/// For an enum, we create methods named after each variant.
+pub(crate) fn constructor_methods(s: synstructure::Structure) -> TokenStream {
+    match s.ast().data {
+        syn::Data::Struct(_) => derive_new_for_struct(s),
+        syn::Data::Enum(_) => derive_new_for_variants(s),
+        syn::Data::Union(_) => return Default::default(),
+    }
+}
+
+fn derive_new_for_struct(s: synstructure::Structure<'_>) -> TokenStream {
+    derive_new_for_variant(
+        &s,
+        &s.variants()[0],
+        &Ident::new("new", s.ast().ident.span()),
+    )
+}
+
+fn derive_new_for_variants(s: synstructure::Structure<'_>) -> TokenStream {
+    s.variants()
+        .iter()
+        .map(|v| {
+            let mut fn_name = v.ast().ident.to_string().to_case(Case::Snake);
+            if RUST_KEYWORDS.iter().any(|&kw| kw == fn_name) {
+                fn_name.push('_');
+            }
+            let fn_name = Ident::new(&fn_name, v.ast().ident.span());
+            derive_new_for_variant(&s, v, &fn_name)
+        })
+        .collect()
+}
+
+fn derive_new_for_variant(
+    s: &synstructure::Structure<'_>,
+    v: &VariantInfo<'_>,
+    fn_name: &Ident,
+) -> TokenStream {
+    let type_name = &s.ast().ident;
+    let (impl_generics, type_generics, where_clauses) = s.ast().generics.split_for_impl();
+
+    let binding_names = v.bindings().iter().map(|b| &b.binding).collect::<Vec<_>>();
+    let binding_types = v.bindings().iter().map(|b| &b.ast().ty).collect::<Vec<_>>();
+    let construct = v.construct(|_b, i| {
+        let name = binding_names[i];
+        quote_spanned!(
+            binding_names[i].span() =>
+            formality_core::Upcast::upcast(#name)
+        )
+    });
+
+    quote_spanned! { v.ast().ident.span() =>
+        #[allow(dead_code)]
+        impl #impl_generics #type_name #type_generics
+        where #where_clauses
+        {
+            pub fn #fn_name(
+                #(
+                    #binding_names: impl formality_core::Upcast<#binding_types>,
+                )*
+            ) -> Self {
+                #construct
+            }
+        }
+    }
+}

crates/formality-macros/src/custom.rs

@@ -4,6 +4,7 @@ use proc_macro2::TokenStream;
 pub(crate) struct Customize {
     pub parse: bool,
     pub debug: bool,
+    pub constructors: bool,
 }
 
 impl syn::parse::Parse for Customize {
@@ -28,6 +29,13 @@ impl syn::parse::Parse for Customize {
                     result.debug = true;
                 }
 
+                proc_macro2::TokenTree::Ident(ident) if ident == "constructors" => {
+                    if result.constructors {
+                        return Err(syn::Error::new(ident.span(), "already customizing debug"));
+                    }
+                    result.constructors = true;
+                }
+
                 _ => {
                     return Err(syn::Error::new(
                         token.span(),

crates/formality-macros/src/lib.rs

@@ -8,6 +8,7 @@ extern crate proc_macro;
 mod as_methods;
 mod attrs;
 mod cast;
+mod constructors;
 mod custom;
 mod debug;
 mod fixed_point;

crates/formality-macros/src/term.rs

@@ -5,6 +5,7 @@ use syn::DeriveInput;
 use crate::{
     attrs::{self, remove_formality_attributes},
     cast::{downcast_impls, upcast_impls},
+    constructors::constructor_methods,
     debug::derive_debug_with_spec,
     fold::derive_fold,
     parse::derive_parse_with_spec,
@@ -35,6 +36,11 @@ pub fn term(spec: Option<FormalitySpec>, mut input: DeriveInput) -> syn::Result<
     let term_impl = derive_term(synstructure::Structure::new(&input));
     let downcast_impls = downcast_impls(synstructure::Structure::new(&input));
     let upcast_impls = upcast_impls(synstructure::Structure::new(&input));
+    let constructors = if customize.constructors {
+        None
+    } else {
+        Some(constructor_methods(synstructure::Structure::new(&input)))
+    };
     remove_formality_attributes(&mut input);
 
     Ok(quote! {
@@ -48,6 +54,7 @@ pub fn term(spec: Option<FormalitySpec>, mut input: DeriveInput) -> syn::Result<
         #term_impl
         #(#downcast_impls)*
         #(#upcast_impls)*
+        #constructors
     })
 }
 

crates/formality-prove/src/prove/prove_eq.rs

@@ -17,7 +17,7 @@ use super::{constraints::Constraints, env::Env};
 
 /// Goal(s) to prove `a` and `b` are equal
 pub fn eq(a: impl Upcast<Parameter>, b: impl Upcast<Parameter>) -> Relation {
-    Relation::eq(a, b)
+    Relation::equals(a, b)
 }
 
 judgment_fn! {

crates/formality-types/src/grammar/consts.rs

@@ -7,6 +7,7 @@ pub use valtree::*;
 
 #[term]
 #[cast]
+#[customize(constructors)] // FIXME: figure out upcasts with arc or special-case
 pub struct Const {
     data: Arc<ConstData>,
 }

crates/formality-types/src/grammar/formulas.rs

@@ -171,18 +171,6 @@ pub enum Relation {
 }
 
 impl Relation {
-    pub fn eq(p1: impl Upcast<Parameter>, p2: impl Upcast<Parameter>) -> Self {
-        Self::Equals(p1.upcast(), p2.upcast())
-    }
-
-    pub fn outlives(p1: impl Upcast<Parameter>, p2: impl Upcast<Parameter>) -> Self {
-        Self::Outlives(p1.upcast(), p2.upcast())
-    }
-
-    pub fn sub(p1: impl Upcast<Parameter>, p2: impl Upcast<Parameter>) -> Self {
-        Self::Sub(p1.upcast(), p2.upcast())
-    }
-
     #[tracing::instrument(level = "trace", ret)]
     pub fn debone(&self) -> (Skeleton, Vec<Parameter>) {
         match self {
@@ -200,15 +188,6 @@ pub struct TraitRef {
     pub parameters: Parameters,
 }
 
-impl TraitRef {
-    pub fn new(id: &TraitId, parameters: impl Upcast<Vec<Parameter>>) -> Self {
-        Self {
-            trait_id: id.clone(),
-            parameters: parameters.upcast(),
-        }
-    }
-}
-
 impl TraitId {
     pub fn with(
         &self,

crates/formality-types/src/grammar/ty.rs

@@ -13,6 +13,7 @@ use super::{
 
 #[term]
 #[cast]
+#[customize(constructors)] // FIXME: figure out upcasts with arc or special-case
 pub struct Ty {
     data: Arc<TyData>,
 }
@@ -294,6 +295,7 @@ pub enum Variance {
 
 #[term]
 #[cast]
+#[customize(constructors)] // FIXME: figure out upcasts with arc or special-case
 pub struct Lt {
     data: Arc<LtData>,
 }

crates/formality-types/src/grammar/wc.rs

@@ -26,7 +26,7 @@ impl Wcs {
         assert_eq!(a.len(), b.len());
         a.into_iter()
             .zip(b)
-            .map(|(a, b)| Relation::eq(a, b))
+            .map(|(a, b)| Relation::equals(a, b))
             .upcasted()
             .collect()
     }