Implement const generics

Author: oli-obk

crates/formality-check/src/where_clauses.rs

@@ -22,7 +22,7 @@ impl super::Check<'_> {
         Ok(())
     }
 
-    #[context("prove_where_clauses_well_formed({where_clause:?})")]
+    #[context("prove_where_clause_well_formed({where_clause:?})")]
     fn prove_where_clause_well_formed(
         &self,
         in_env: &Env,
@@ -45,6 +45,10 @@ impl super::Check<'_> {
                 let wc = e.instantiate_universally(binder);
                 self.prove_where_clause_well_formed(&e, assumptions, &wc)
             }
+            WhereClauseData::TypeOfConst(ct, ty) => {
+                self.prove_parameter_well_formed(in_env, &assumptions, ct.clone())?;
+                self.prove_parameter_well_formed(in_env, assumptions, ty.clone())
+            }
         }
     }
 

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

@@ -32,5 +32,11 @@ 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)
+        )
     }
 }

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,25 @@ impl Fold for Ty {
     }
 }
 
+impl Fold for Const {
+    fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self {
+        match self.data() {
+            ConstData::Value(v) => Self::new(v.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::*;

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

@@ -0,0 +1,68 @@
+mod valtree;
+
+use crate::cast::{Upcast, UpcastFrom};
+
+use super::{Parameter, Variable};
+use formality_macros::{term, Visit};
+use std::sync::Arc;
+pub use valtree::*;
+
+#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
+pub struct Const {
+    data: Arc<ConstData>,
+}
+impl Const {
+    pub fn data(&self) -> &ConstData {
+        &self.data
+    }
+
+    pub fn new(data: impl Upcast<ConstData>) -> Self {
+        Self {
+            data: Arc::new(data.upcast()),
+        }
+    }
+    pub fn as_variable(&self) -> Option<Variable> {
+        match self.data() {
+            ConstData::Value(_) => None,
+            ConstData::Variable(var) => Some(var.clone()),
+        }
+    }
+}
+
+#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
+pub enum ConstData {
+    Value(ValTree),
+    Variable(Variable),
+}
+
+#[term]
+pub enum Bool {
+    #[grammar(true)]
+    True,
+    #[grammar(false)]
+    False,
+}
+
+impl UpcastFrom<Bool> for Const {
+    fn upcast_from(term: Bool) -> Self {
+        Self::new(ValTree::upcast_from(term))
+    }
+}
+
+impl UpcastFrom<ValTree> for ConstData {
+    fn upcast_from(v: ValTree) -> Self {
+        Self::Value(v)
+    }
+}
+
+impl UpcastFrom<Variable> for ConstData {
+    fn upcast_from(v: Variable) -> Self {
+        Self::Variable(v)
+    }
+}
+
+impl UpcastFrom<Const> for Parameter {
+    fn upcast_from(term: Const) -> Self {
+        Self::Const(term)
+    }
+}

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

@@ -0,0 +1,61 @@
+use formality_macros::Visit;
+
+use crate::cast::{Upcast, UpcastFrom};
+
+use super::{Bool, ConstData};
+
+#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
+pub enum ValTree {
+    Leaf(Scalar),
+    Branches(Vec<ValTree>),
+}
+
+impl std::fmt::Debug for ValTree {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        match self {
+            Self::Leaf(s) => s.fmt(f),
+            Self::Branches(branches) => branches.fmt(f),
+        }
+    }
+}
+
+#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
+pub struct Scalar {
+    bits: u128,
+}
+
+impl std::fmt::Debug for Scalar {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        self.bits.fmt(f)
+    }
+}
+
+impl Scalar {
+    pub fn new(bits: u128) -> Self {
+        Self { bits }
+    }
+}
+
+impl UpcastFrom<Bool> for ValTree {
+    fn upcast_from(term: Bool) -> Self {
+        Scalar::upcast_from(term).upcast()
+    }
+}
+
+impl UpcastFrom<Scalar> for ValTree {
+    fn upcast_from(s: Scalar) -> Self {
+        Self::Leaf(s)
+    }
+}
+
+impl UpcastFrom<Scalar> for ConstData {
+    fn upcast_from(s: Scalar) -> Self {
+        ValTree::upcast_from(s).upcast()
+    }
+}
+
+impl UpcastFrom<Bool> for Scalar {
+    fn upcast_from(term: Bool) -> Self {
+        Scalar { bits: term as u128 }
+    }
+}

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

@@ -4,6 +4,7 @@ use crate::cast::To;
 use crate::cast::Upcast;
 use crate::cast_impl;
 
+use super::Const;
 use super::Parameter;
 use super::Parameters;
 use super::TraitId;
@@ -27,6 +28,9 @@ pub enum Predicate {
 
     #[grammar(@IsLocal($v0))]
     IsLocal(TraitRef),
+
+    #[grammar(@ConstHasType($v0, $v1))]
+    ConstHasType(Const, Ty),
 }
 
 /// A coinductive predicate is one that can be proven via a cycle.
@@ -79,6 +83,7 @@ pub enum Skeleton {
     WellFormed,
     WellFormedTraitRef(TraitId),
     IsLocal(TraitId),
+    ConstHasType,
 
     Equals,
     Sub,
@@ -115,6 +120,10 @@ impl Predicate {
                 trait_id,
                 parameters,
             }) => (Skeleton::IsLocal(trait_id.clone()), parameters.clone()),
+            Predicate::ConstHasType(ct, ty) => (
+                Skeleton::ConstHasType,
+                vec![ct.clone().upcast(), ty.clone().upcast()],
+            ),
         }
     }
 }

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

@@ -13,7 +13,10 @@ use crate::{
     fold::Fold,
 };
 
-use super::{AdtId, AssociatedItemId, Binder, FnId, TraitId};
+use super::{
+    consts::{Const, ConstData},
+    AdtId, AssociatedItemId, Binder, FnId, TraitId,
+};
 
 #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct Ty {
@@ -263,13 +266,16 @@ pub enum Parameter {
     Ty(Ty),
     #[cast]
     Lt(Lt),
+    #[grammar(const $v0)]
+    Const(Const),
 }
 
 impl Parameter {
     pub fn kind(&self) -> ParameterKind {
         match self {
             Parameter::Ty(_) => ParameterKind::Ty,
             Parameter::Lt(_) => ParameterKind::Lt,
+            Parameter::Const(_) => ParameterKind::Const,
         }
     }
 
@@ -281,13 +287,15 @@ impl Parameter {
         match self {
             Parameter::Ty(v) => v.as_variable(),
             Parameter::Lt(v) => v.as_variable(),
+            Parameter::Const(v) => v.as_variable(),
         }
     }
 
     pub fn data(&self) -> ParameterData<'_> {
         match self {
             Parameter::Ty(v) => ParameterData::Ty(v.data()),
             Parameter::Lt(v) => ParameterData::Lt(v.data()),
+            Parameter::Const(v) => ParameterData::Const(v.data()),
         }
     }
 }
@@ -297,13 +305,15 @@ pub type Parameters = Vec<Parameter>;
 pub enum ParameterData<'me> {
     Ty(&'me TyData),
     Lt(&'me LtData),
+    Const(&'me ConstData),
 }
 
 #[term]
 #[derive(Copy)]
 pub enum ParameterKind {
     Ty,
     Lt,
+    Const,
 }
 
 #[term]
@@ -517,6 +527,7 @@ impl UpcastFrom<Variable> for Parameter {
         match v.kind() {
             ParameterKind::Lt => Lt::new(v).upcast(),
             ParameterKind::Ty => Ty::new(v).upcast(),
+            ParameterKind::Const => Const::new(v).upcast(),
         }
     }
 }