Merge pull request #130 from oli-obk/const_generics_without_inherent_types

Implement const generics take 2

Author: nikomatsakis

.github/workflows/ci.yaml

@@ -9,11 +9,14 @@ on:
 
 jobs:
   rust-test:
-    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
+    runs-on: ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v2
       - name: Run cargo test
         uses: actions-rs/cargo@v1
         with:
           command: test
-          args: --all
+          args: --all

crates/formality-check/src/lib.rs

@@ -1,6 +1,6 @@
 #![allow(dead_code)]
 
-use std::collections::VecDeque;
+use std::{collections::VecDeque, fmt::Debug};
 
 use anyhow::bail;
 use formality_prove::{Decls, Env};
@@ -86,7 +86,12 @@ impl Check<'_> {
         }
     }
 
-    fn prove_goal(&self, env: &Env, assumptions: impl ToWcs, goal: impl ToWcs) -> Fallible<()> {
+    fn prove_goal(
+        &self,
+        env: &Env,
+        assumptions: impl ToWcs,
+        goal: impl ToWcs + Debug,
+    ) -> Fallible<()> {
         let goal: Wcs = goal.to_wcs();
         let assumptions: Wcs = assumptions.to_wcs();
 
@@ -101,7 +106,12 @@ impl Check<'_> {
         bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}")
     }
 
-    fn prove_not_goal(&self, env: &Env, assumptions: impl ToWcs, goal: impl ToWcs) -> Fallible<()> {
+    fn prove_not_goal(
+        &self,
+        env: &Env,
+        assumptions: impl ToWcs,
+        goal: impl ToWcs + Debug,
+    ) -> Fallible<()> {
         let goal: Wcs = goal.to_wcs();
         let assumptions: Wcs = assumptions.to_wcs();
 

crates/formality-check/src/where_clauses.rs

@@ -1,11 +1,12 @@
+use fn_error_context::context;
 use formality_prove::Env;
 use formality_rust::{
     grammar::{WhereClause, WhereClauseData},
     prove::ToWcs,
 };
 use formality_types::{
     cast::Upcast,
-    grammar::{Fallible, Parameter, TraitRef},
+    grammar::{ConstData, Fallible, Parameter, Relation, TraitRef},
 };
 
 impl super::Check<'_> {
@@ -21,6 +22,8 @@ impl super::Check<'_> {
         Ok(())
     }
 
+    #[context("prove_where_clause_well_formed({where_clause:?})")]
+    // FIXME(oli-obk): figure out why is this a function and not a `judgment_fn`.
     fn prove_where_clause_well_formed(
         &self,
         in_env: &Env,
@@ -43,6 +46,17 @@ impl super::Check<'_> {
                 let wc = e.instantiate_universally(binder);
                 self.prove_where_clause_well_formed(&e, assumptions, &wc)
             }
+            WhereClauseData::TypeOfConst(ct, ty) => {
+                match ct.data() {
+                    ConstData::Value(_, t) => {
+                        self.prove_goal(in_env, &assumptions, Relation::eq(ty, t))?
+                    }
+                    ConstData::Variable(_) => {}
+                }
+                // FIXME(oli-obk): prove that there is no `TypeOfConst` bound for a different type.
+                self.prove_parameter_well_formed(in_env, &assumptions, ct.clone())?;
+                self.prove_parameter_well_formed(in_env, assumptions, ty.clone())
+            }
         }
     }
 

crates/formality-macros/src/test.rs

@@ -1,15 +1,11 @@
 use proc_macro::TokenStream;
-use quote::quote;
 
 pub(crate) fn test(_args: TokenStream, mut item_fn: syn::ItemFn) -> syn::Result<syn::ItemFn> {
     let original_fn_body = item_fn.block.clone();
-    item_fn.block = syn::parse2(quote! {
-        {
-            formality_core::with_tracing_logs(move || {
-                #original_fn_body
-            })
-        }
-    })
-    .unwrap();
+    item_fn.block = syn::parse_quote!({
+        formality_core::with_tracing_logs(move || {
+            #original_fn_body
+        })
+    });
     Ok(item_fn)
 }

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

@@ -114,5 +114,12 @@ judgment_fn! {
             ----------------------------- ("trait ref is local")
             (prove_wc(decls, env, assumptions, Relation::WellFormed(p)) => c)
         )
+
+        (
+            (if let Some((_, const_ty)) = ct.as_value())
+            (prove(decls, env, assumptions, Wcs::all_eq(vec![const_ty], vec![ty])) => c)
+            ----------------------------- ("const has ty")
+            (prove_wc(decls, env, assumptions, Predicate::ConstHasType(ct, ty)) => c)
+        )
     }
 }

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

@@ -1,5 +1,5 @@
 use formality_types::{
-    grammar::{Parameter, RigidName, RigidTy, UniversalVar, Wcs},
+    grammar::{ConstData, Parameter, RigidName, RigidTy, UniversalVar, Wcs},
     judgment_fn,
 };
 
@@ -32,5 +32,17 @@ judgment_fn! {
             --- ("tuples")
             (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Tuple(_), parameters }) => c)
         )
+
+        (
+            (for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
+            --- ("integers and booleans")
+            (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::ScalarId(_), parameters }) => c)
+        )
+
+        (
+            (prove_wf(&decls, &env, &assumptions, ty) => c)
+            --- ("rigid constants")
+            (prove_wf(decls, env, assumptions, ConstData::Value(_, ty)) => c)
+        )
     }
 }

crates/formality-rust/src/grammar.rs

@@ -4,8 +4,8 @@ use formality_macros::term;
 use formality_types::{
     cast::Upcast,
     grammar::{
-        AdtId, AssociatedItemId, Binder, CrateId, Fallible, FieldId, FnId, Lt, Parameter, TraitId,
-        TraitRef, Ty, Wc,
+        AdtId, AssociatedItemId, Binder, Const, CrateId, Fallible, FieldId, FnId, Lt, Parameter,
+        TraitId, TraitRef, Ty, Wc,
     },
     term::Term,
 };
@@ -331,6 +331,7 @@ impl WhereClause {
                 let wc = where_clause.invert()?;
                 Some(Wc::for_all(&vars, wc))
             }
+            WhereClauseData::TypeOfConst(_, _) => None,
         }
     }
 }
@@ -345,6 +346,9 @@ pub enum WhereClauseData {
 
     #[grammar(for $v0)]
     ForAll(Binder<WhereClause>),
+
+    #[grammar(type_of_const $v0 is $v1)]
+    TypeOfConst(Const, Ty),
 }
 
 #[term($data)]

crates/formality-rust/src/prove.rs

@@ -386,6 +386,9 @@ impl ToWcs for WhereClause {
                     .map(|wc| Wc::for_all(&vars, wc))
                     .collect()
             }
+            WhereClauseData::TypeOfConst(ct, ty) => {
+                Predicate::ConstHasType(ct.clone(), ty.clone()).upcast()
+            }
         }
     }
 }

crates/formality-types/src/fold.rs

@@ -3,7 +3,7 @@ use std::sync::Arc;
 use crate::{
     cast::Upcast,
     collections::Set,
-    grammar::{Lt, LtData, Parameter, Ty, TyData, Variable},
+    grammar::{Const, ConstData, Lt, LtData, Parameter, Ty, TyData, ValTree, Variable},
     visit::Visit,
 };
 
@@ -73,6 +73,28 @@ impl Fold for Ty {
     }
 }
 
+impl Fold for Const {
+    fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self {
+        match self.data() {
+            ConstData::Value(v, ty) => Self::valtree(
+                v.substitute(substitution_fn),
+                ty.substitute(substitution_fn),
+            ),
+            ConstData::Variable(v) => match substitution_fn(v.clone()) {
+                None => self.clone(),
+                Some(Parameter::Const(c)) => c,
+                Some(param) => panic!("ill-kinded substitute: expected const, got {param:?}"),
+            },
+        }
+    }
+}
+
+impl Fold for ValTree {
+    fn substitute(&self, _substitution_fn: SubstitutionFn<'_>) -> Self {
+        self.clone()
+    }
+}
+
 impl Fold for Lt {
     fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self {
         match self.data() {

crates/formality-types/src/grammar.rs

@@ -1,11 +1,13 @@
 mod binder;
+mod consts;
 mod formulas;
 mod ids;
 mod kinded;
 mod ty;
 mod wc;
 
 pub use binder::*;
+pub use consts::*;
 pub use formulas::*;
 pub use ids::*;
 pub use kinded::*;