diff --git a/.github/workflows/ci-rs.yml b/.github/workflows/ci-rs.yml index c3e6fc740..b975b4e16 100644 --- a/.github/workflows/ci-rs.yml +++ b/.github/workflows/ci-rs.yml @@ -117,7 +117,7 @@ jobs: - name: Build with no features run: cargo test --verbose --no-default-features --no-run - name: Tests with no features - run: cargo test --verbose --no-default-features + run: RUST_MIN_STACK=10485760 cargo test --verbose --no-default-features # Run tests on Rust stable tests-stable-all-features: @@ -140,7 +140,7 @@ jobs: - name: Build with all features run: cargo test --verbose --all-features --no-run - name: Tests with all features - run: cargo test --verbose --all-features + run: RUST_MIN_STACK=10485760 cargo test --verbose --all-features - name: Build HUGR binary run: cargo build -p hugr-cli - name: Upload the binary to the artifacts @@ -175,11 +175,11 @@ jobs: - name: Build with no features run: cargo test --verbose --no-default-features --no-run - name: Tests with no features - run: cargo test --verbose --no-default-features + run: RUST_MIN_STACK=10485760 cargo test --verbose --no-default-features - name: Build with all features run: cargo test --verbose --all-features --no-run - name: Tests with all features - run: cargo test --verbose --all-features + run: RUST_MIN_STACK=10485760 cargo test --verbose --all-features # Ensure that serialized extensions match rust implementation std-extensions: @@ -277,7 +277,7 @@ jobs: - name: Build run: cargo test -p hugr-llvm --verbose --features llvm${{ matrix.llvm-version[1] }} --no-run - name: Tests with no features - run: cargo test -p hugr-llvm --verbose --features llvm${{ matrix.llvm-version[1] }} + run: cargo test -p hugr-llvm --verbose --features llvm${{ matrix.llvm-version[1] }} --exclude test_type_substitution # This is a meta job to mark successful completion of the required checks, # even if they are skipped due to no changes in the relevant files. diff --git a/hugr-core/src/types.rs b/hugr-core/src/types.rs index c285f3db6..a8b57ac22 100644 --- a/hugr-core/src/types.rs +++ b/hugr-core/src/types.rs @@ -746,4 +746,385 @@ pub(crate) mod test { } } } + + mod proptest2 { + use std::{iter::once, sync::Arc}; + + use crate::extension::{ExtensionRegistry, ExtensionSet}; + use crate::proptest::RecursionDepth; + use crate::std_extensions::std_reg; + use crate::types::Substitution; + use crate::types::{ + type_param::TypeParam, FuncValueType, Type, TypeArg, TypeBound, TypeRow, + }; + use itertools::Itertools; + use proptest::{ + collection::vec, + prelude::{any, Just, Strategy}, + prop_assert, prop_oneof, proptest, + sample::{select, Index}, + string::string_regex, + }; + + trait VarEnvState: Send + Sync { + fn with_env( + self, + vars: Vec, + depth: RecursionDepth, + reg: Arc, + ) -> impl Strategy)> + Clone; + } + + fn make_type_var( + kind: TypeParam, + vars: Vec, + ) -> impl Strategy)> + Clone { + let mut opts = vars + .iter() + .enumerate() + .filter(|(_, p)| kind.contains(p)) + .map(|(i, p)| (TypeArg::new_var_use(i, p.clone()), vars.clone())) + .collect_vec(); + let mut env_with_new = vars; + env_with_new.push(kind.clone()); + opts.push(( + TypeArg::new_var_use(env_with_new.len() - 1, kind), + env_with_new, + )); + select(opts) + } + + #[derive(Debug, Clone)] + struct MakeType(TypeBound); + + impl VarEnvState for MakeType { + fn with_env( + self, + vars: Vec, + depth: RecursionDepth, + reg: Arc, + ) -> impl Strategy)> + Clone { + let non_leaf = (!depth.leaf()) as u32; + let depth = depth.descend(); + prop_oneof![ + // no Alias + 1 => MakeCustomType + .with_env(vars.clone(), depth, reg.clone()) + .prop_filter("Must fit TypeBound", move |(ct, _)| self + .0 + .contains(ct.least_upper_bound())), + non_leaf => MakeFuncType.with_env(vars.clone(), depth, reg.clone()), + 1 => make_type_var(self.0.into(), vars.clone()).prop_map(|(ta, vars)| match ta { + TypeArg::Type { ty } => (ty, vars), + _ => panic!("Passed in a TypeBound, expected a Type"), + }), + // Type has no row_variable; consider joining with TypeRV + 1 => MakeSumType(self.0).with_env(vars, depth, reg) + ] + } + } + + struct MakeSumType(TypeBound); + const MAX_NUM_VARIANTS: u8 = 5; + impl VarEnvState for MakeSumType { + fn with_env( + self, + vars: Vec, + depth: RecursionDepth, + reg: Arc, + ) -> impl Strategy)> + Clone { + let b = self.0; + if depth.leaf() { + (1..MAX_NUM_VARIANTS) + .prop_map(move |nv| (Type::new_unit_sum(nv), vars.clone())) + .sboxed() + } else { + (1..MAX_NUM_VARIANTS) + .prop_flat_map(move |nv| { + MakeVec(vec![MakeTypeRow(b); nv as usize]).with_env( + vars.clone(), + depth, + reg.clone(), + ) + }) + .prop_map(|(rows, vars)| (Type::new_sum(rows), vars)) + .sboxed() + } + } + } + + #[derive(Clone, Debug)] + struct MakeTypeArg(TypeParam); + const MAX_LIST_LEN: usize = 4; + impl VarEnvState for MakeTypeArg { + fn with_env( + self, + vars: Vec, + depth: RecursionDepth, + reg: Arc, + ) -> impl Strategy)> + Clone { + match &self.0 { + TypeParam::Type { b } => MakeType(*b) + .with_env(vars, depth, reg) + .prop_map(|(ty, vars)| (TypeArg::Type { ty }, vars)) + .sboxed(), + TypeParam::BoundedNat { bound } => { + let vars2 = vars.clone(); + prop_oneof![ + match bound.value() { + Some(max) => (0..max.get()).sboxed(), + None => proptest::num::u64::ANY.sboxed(), + } + .prop_map(move |n| (TypeArg::BoundedNat { n }, vars.clone())), + make_type_var(self.0, vars2) + ] + .sboxed() + } + TypeParam::String => { + let vars2 = vars.clone(); + prop_oneof![ + string_regex("[a-z]+") + .unwrap() + .prop_map(move |arg| (TypeArg::String { arg }, vars.clone())), + make_type_var(self.0, vars2) + ] + .sboxed() + } + TypeParam::List { param } => { + if depth.leaf() { + Just((TypeArg::Sequence { elems: vec![] }, vars)).sboxed() + } else { + fold_n( + MakeTypeArg((**param).clone()), + 0..MAX_LIST_LEN, + vars, + depth.descend(), + reg, + ) + .prop_map(|(elems, vars)| (TypeArg::Sequence { elems }, vars)) + .sboxed() + } + } + TypeParam::Tuple { params } => { + MakeVec(params.iter().cloned().map(MakeTypeArg).collect()) + .with_env(vars, depth, reg) + .prop_map(|(elems, vars)| (TypeArg::Sequence { elems }, vars)) + .sboxed() + } + TypeParam::Extensions => make_extensions(vars, reg) + .prop_map(|(es, vars)| (TypeArg::Extensions { es }, vars)) + .sboxed(), + } + } + } + + struct MakeFuncType; + const MAX_TYPE_ROW_LEN: usize = 5; + impl VarEnvState for MakeFuncType { + fn with_env( + self, + vars: Vec, + depth: RecursionDepth, + reg: Arc, + ) -> impl Strategy)> + Clone { + MakeTypeRow(TypeBound::Any) + .with_env(vars, depth, reg.clone()) + .prop_flat_map(move |(inputs, vars)| { + let reg2 = reg.clone(); + MakeTypeRow(TypeBound::Any) + .with_env(vars, depth, reg.clone()) + .prop_flat_map(move |(outputs, vars)| { + let inputs = inputs.clone(); + make_extensions(vars, reg2.clone()).prop_map(move |(exts, vars)| { + ( + Type::new_function( + FuncValueType::new(inputs.clone(), outputs.clone()) + .with_extension_delta(exts), + ), + vars, + ) + }) + }) + }) + } + } + + fn make_extensions( + vars: Vec, + reg: Arc, + ) -> impl Strategy)> { + // Some number of extensions from the registry + let es = vec( + select( + reg.iter() + .map(|e| ExtensionSet::singleton(e.name().clone())) + .collect_vec(), + ), + 0..2, + ) + .prop_map(ExtensionSet::union_over); + let vars2 = vars.clone(); + prop_oneof![ + es.clone().prop_map(move |es| (es, vars2.clone())), + es.prop_flat_map( + move |es2| make_type_var(TypeParam::Extensions, vars.clone()).prop_map( + move |(ta, vars)| ( + match ta { + TypeArg::Extensions { es } => es2.clone().union(es), + _ => panic!("Asked for TypeParam::Extensions"), + }, + vars + ) + ) + ) + ] + } + + struct MakeCustomType; + + impl VarEnvState for MakeCustomType { + fn with_env( + self, + vars: Vec, + depth: RecursionDepth, + reg: Arc, + ) -> impl Strategy)> + Clone { + any::().prop_flat_map(move |idx| { + let (ext, typ) = *idx.get( + ®.iter() + .flat_map(|e| { + e.types() + .filter(|t| !depth.leaf() || t.1.params().is_empty()) + .map(|(name, _)| (e.name(), name)) + }) + .collect_vec(), + ); + let typedef = reg.get(ext).unwrap().get_type(typ).unwrap(); + // Make unborrowed things that inner closure can take ownership op: + let (ext, typ, reg) = (ext.clone(), typ.clone(), reg.clone()); + MakeVec(typedef.params().iter().cloned().map(MakeTypeArg).collect()) + .with_env(vars.clone(), depth, reg.clone()) + .prop_map(move |(v, vars)| { + ( + Type::new_extension( + reg.get(&ext) + .unwrap() + .get_type(&typ) + .unwrap() + .instantiate(v) + .unwrap(), + ), + vars, + ) + }) + }) + } + } + + #[derive(Clone)] + struct MakeTypeRow(TypeBound); + + impl VarEnvState for MakeTypeRow { + fn with_env( + self, + vars: Vec, + depth: RecursionDepth, + reg: Arc, + ) -> impl Strategy)> + Clone { + (0..MAX_TYPE_ROW_LEN) + .prop_flat_map(move |sz| { + MakeVec(vec![MakeType(self.0); sz]).with_env( + vars.clone(), + depth, + reg.clone(), + ) + }) + .prop_map(|(vec, vars)| (TypeRow::from(vec), vars)) + } + } + + fn fold_n< + E: Clone + std::fmt::Debug + 'static + Send + Sync, + T: VarEnvState + Clone + Send + Sync + 'static, + >( + elem_strat: T, + size_strat: impl Strategy, + params: Vec, + depth: RecursionDepth, + reg: Arc, + ) -> impl Strategy, Vec)> { + size_strat.prop_flat_map(move |sz| { + MakeVec(vec![elem_strat.clone(); sz]).with_env(params.clone(), depth, reg.clone()) + }) + } + + struct MakeVec(Vec); + + impl> VarEnvState> for MakeVec + where + E: Clone + std::fmt::Debug + 'static + Send + Sync, + T: VarEnvState + Clone + Send + Sync + 'static, + { + fn with_env( + self, + vars: Vec, + depth: RecursionDepth, + reg: Arc, + ) -> impl Strategy, Vec)> + Clone { + let mut s = Just((Vec::::new(), vars)).sboxed(); + for strat in self.0 { + let reg2 = reg.clone(); + s = s + .prop_flat_map(move |(v, vars)| { + strat.clone().with_env(vars, depth, reg2.clone()).prop_map( + move |(elem, vars)| { + (v.iter().cloned().chain(once(elem)).collect(), vars) + }, + ) + }) + .sboxed(); + } + s + } + } + + /// Given a VarEnvState that builds a T with an environment, + /// Builds (a T, the environment for that T, and a TypeArg for each TypeParam in that environment) + /// with the environment making the TypeArgs valid + fn with_substitution( + content: impl VarEnvState, + content_depth: RecursionDepth, + subst_depth: RecursionDepth, + reg: Arc, + ) -> impl Strategy), Vec, Vec)> { + content + .with_env(vec![], content_depth, reg.clone()) + .prop_flat_map(move |(val, val_env)| { + MakeVec(val_env.iter().cloned().map(MakeTypeArg).collect()) + .with_env(vec![], subst_depth, reg.clone()) + .prop_map(move |(subst, subst_env)| { + ((val.clone(), val_env.clone()), subst, subst_env) + }) + }) + } + + proptest! { + #[test] + // We override the RecursionDepth from default 4 down to 3 because otherwise we overflow the stack. + // It doesn't seem to be an infinite loop, I infer that the folding etc. in the VarEnvState methods + // just use a lot more stack than the simpler, original, proptests. + fn test_type_substitution(((t,t_env), s, s_env) in with_substitution( + MakeType(TypeBound::Any), + 3.into(), + 3.into(), + Arc::new(std_reg()))) { + prop_assert!(t.validate(&t_env).is_ok()); + for s1 in s.iter() { + prop_assert!(s1.validate(&s_env).is_ok()); + } + let ts = t.substitute1(&Substitution::new(&s)); + prop_assert!(ts.validate(&s_env).is_ok()); + } + } + } } diff --git a/hugr-core/src/types/type_param.rs b/hugr-core/src/types/type_param.rs index b81a20ace..070f7ea72 100644 --- a/hugr-core/src/types/type_param.rs +++ b/hugr-core/src/types/type_param.rs @@ -107,7 +107,7 @@ impl TypeParam { } } - fn contains(&self, other: &TypeParam) -> bool { + pub(super) fn contains(&self, other: &TypeParam) -> bool { match (self, other) { (TypeParam::Type { b: b1 }, TypeParam::Type { b: b2 }) => b1.contains(*b2), (TypeParam::BoundedNat { bound: b1 }, TypeParam::BoundedNat { bound: b2 }) => {