add predicates to class defn and prove them

src/grammar.rs

@@ -37,8 +37,9 @@ pub struct ClassDecl {
     pub binder: Binder<ClassDeclBoundData>,
 }
 
-#[term({ $*fields $*methods })]
+#[term($:where $,predicates { $*fields $*methods })]
 pub struct ClassDeclBoundData {
+    pub predicates: Vec<Predicate>,
     pub fields: Vec<FieldDecl>,
     pub methods: Vec<MethodDecl>,
 }

src/grammar/test_parse.rs

@@ -24,6 +24,7 @@ fn test_parse_program() {
                         binder: Binder {
                             kinds: [],
                             term: ClassDeclBoundData {
+                                predicates: [],
                                 fields: [
                                     FieldDecl {
                                         atomic: No,

src/type_system/classes.rs

@@ -5,17 +5,28 @@ use formality_core::Fallible;
 
 use crate::grammar::{Atomic, ClassDecl, ClassDeclBoundData, FieldDecl, NamedTy, Program, Var};
 
-use super::{env::Env, methods::check_method, types::check_type};
+use super::{env::Env, methods::check_method, predicates::check_predicate, types::check_type};
 
 #[context("check class named `{:?}`", decl.name)]
 pub fn check_class(program: &Arc<Program>, decl: &ClassDecl) -> Fallible<()> {
     let mut env = Env::new(program);
 
     let ClassDecl { name, binder } = decl;
-    let (substitution, ClassDeclBoundData { fields, methods }) = env.open_universally(binder);
+    let (
+        substitution,
+        ClassDeclBoundData {
+            predicates,
+            fields,
+            methods,
+        },
+    ) = env.open_universally(binder);
 
     let class_ty = NamedTy::new(name, &substitution);
 
+    for predicate in predicates {
+        check_predicate(&env, &predicate)?;
+    }
+
     for field in fields {
         check_field(&class_ty, &env, &field)?;
     }

src/type_system/expressions.rs

@@ -107,14 +107,16 @@ judgment_fn! {
 
         (
             (env.program().class_named(&class_name) => class_decl)
-            (class_decl.binder.instantiate_with(&parameters) => ClassDeclBoundData { fields, methods: _ })
+            (let ClassDeclBoundData { predicates, fields, methods: _ } = class_decl.binder.instantiate_with(&parameters)?)
             (if fields.len() == exprs.len())
             (let this_ty = NamedTy::new(&class_name, &parameters))
 
+            (prove_predicates(&env, predicates) => ())
+
             (let (env, temp_var) = env.push_fresh_variable(&this_ty))
 
             // FIXME: what if `parameters` reference variables impacted by moves etc?
-            (type_field_exprs_as(&env, &live_after, &temp_var, &exprs, fields) => env)
+            (type_field_exprs_as(&env, &live_after, &temp_var, &exprs, &fields) => env)
 
             // After the above judgment, `Temp(0)` represents the "this" value under construction.
             // Map it to `@in_flight`.
@@ -179,7 +181,7 @@ judgment_fn! {
         (
             (if let NamedTy { name: TypeName::Id(class_name), parameters: class_parameters } = &named_ty)!
             (env.program().class_named(&class_name) => class_decl)
-            (let ClassDeclBoundData { fields: _, methods } = class_decl.binder.instantiate_with(&class_parameters)?)
+            (let ClassDeclBoundData { predicates: _, fields: _, methods } = class_decl.binder.instantiate_with(&class_parameters)?)
             (methods.into_iter().filter(|m| m.name == method_name) => MethodDecl { name: _, binder })
             (let () = tracing::debug!("found method in class {:?}: {:?}", class_name, binder))
             (let MethodDeclBoundData { this: ThisDecl { perm }, inputs, output, predicates, body: _ } = binder.instantiate_with(&method_parameters)?)

src/type_system/places.rs

@@ -123,7 +123,7 @@ judgment_fn! {
 
         (
             (env.program().class_named(&id) => class_decl)
-            (let ClassDeclBoundData { fields, methods: _ } = class_decl.binder.instantiate_with(&parameters).unwrap())
+            (let ClassDeclBoundData { predicates: _, fields, methods: _ } = class_decl.binder.instantiate_with(&parameters).unwrap())
             ----------------------------------- ("named-ty")
             (fields(_env, NamedTy { name: TypeName::Id(id), parameters }) => fields)
         )

src/type_system/tests.rs

@@ -5,6 +5,7 @@ use super::check_program;
 
 mod assignment;
 mod cancellation;
+mod class_defn_wf;
 mod fn_calls;
 mod move_check;
 mod move_tracking;

src/type_system/tests/class_defn_wf.rs

@@ -0,0 +1,104 @@
+use crate::{dada_lang::term, type_system::check_program};
+use formality_core::{test, test_util::ResultTestExt};
+
+#[test]
+#[allow(non_snake_case)]
+fn create_PairSh_with_non_shared_type() {
+    check_program(&term(
+        "
+        class Data {}
+        class PairSh[ty T]
+        where
+            shared(T),
+        {
+        }
+        class Main {
+            fn test(my self) {
+                new PairSh[Data]();
+                ();
+            }
+        }
+        ",
+    ))
+    .assert_err(expect_test::expect![[r#"
+        check program `class Data { } class PairSh [ty] where shared(^ty0_0) { } class Main { fn test (my self) -> () { new PairSh [Data] () ; () ; } }`
+
+        Caused by:
+            0: check class named `Main`
+            1: check method named `test`
+            2: check function body
+            3: judgment `can_type_expr_as { expr: { new PairSh [Data] () ; () ; }, as_ty: (), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
+                 the rule "can_type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
+                   judgment `type_expr_as { expr: { new PairSh [Data] () ; () ; }, as_ty: (), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
+                     the rule "type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
+                       judgment `type_expr { expr: { new PairSh [Data] () ; () ; }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
+                         the rule "block" failed at step #0 (src/file.rs:LL:CC) because
+                           judgment `type_block { block: { new PairSh [Data] () ; () ; }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
+                             the rule "place" failed at step #0 (src/file.rs:LL:CC) because
+                               judgment `type_statements_with_final_ty { statements: [new PairSh [Data] () ;, () ;], ty: (), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
+                                 the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
+                                   judgment `type_statement { statement: new PairSh [Data] () ;, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
+                                     the rule "expr" failed at step #0 (src/file.rs:LL:CC) because
+                                       judgment `type_expr { expr: new PairSh [Data] (), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
+                                         the rule "new" failed at step #4 (src/file.rs:LL:CC) because
+                                           judgment `prove_predicates { predicate: [shared(Data)], env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
+                                             the rule "prove_predicates" failed at step #0 (src/file.rs:LL:CC) because
+                                               judgment `prove_predicate { predicate: shared(Data), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
+                                                 the rule "shared" failed at step #0 (src/file.rs:LL:CC) because
+                                                   judgment `is_shared { a: Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
+                                                     the rule "is_shared" failed at step #1 (src/file.rs:LL:CC) because
+                                                       judgment had no applicable rules: `lien_chain_is_shared { chain: my, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main}, assumptions: {}, fresh: 0 } }`"#]]);
+}
+
+#[test]
+#[allow(non_snake_case)]
+fn take_PairSh_with_non_shared_type() {
+    check_program(&term(
+        "
+        class Data {}
+        class PairSh[ty T]
+        where
+            shared(T),
+        {
+        }
+        class Main {
+            fn test(my self, input: PairSh[Data]) {
+                ();
+            }
+        }
+        ",
+    ))
+    .assert_err(expect_test::expect![[r#"
+        check program `class Data { } class PairSh [ty] where shared(^ty0_0) { } class Main { fn test (my self input : PairSh[Data]) -> () { () ; } }`
+
+        Caused by:
+            0: check class named `Main`
+            1: check method named `test`
+            2: check type `PairSh[Data]`
+            3: judgment `prove_predicate { predicate: shared(Data), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, input: PairSh[Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
+                 the rule "shared" failed at step #0 (src/file.rs:LL:CC) because
+                   judgment `is_shared { a: Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, input: PairSh[Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
+                     the rule "is_shared" failed at step #1 (src/file.rs:LL:CC) because
+                       judgment had no applicable rules: `lien_chain_is_shared { chain: my, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, input: PairSh[Data]}, assumptions: {}, fresh: 0 } }`"#]]);
+}
+
+#[test]
+#[allow(non_snake_case)]
+fn take_PairSh_with_shared_type() {
+    check_program(&term(
+        "
+        class Data {}
+        class PairSh[ty T]
+        where
+            shared(T),
+        {
+        }
+        class Main {
+            fn test(my self, input: PairSh[our Data]) {
+                ();
+            }
+        }
+        ",
+    ))
+    .assert_ok(expect_test::expect![["()"]]);
+}

src/type_system/tests/new_with_self_references.rs

@@ -125,7 +125,7 @@ fn choice_with_non_self_ref() {
                                                        judgment `type_statement { statement: let choice = new Choice (pair . give, r . give) ;, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, d1: Data, d2: Data, d3: Data, pair: Pair, r: shared {d3} Data}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
                                                          the rule "let" failed at step #0 (src/file.rs:LL:CC) because
                                                            judgment `type_expr { expr: new Choice (pair . give, r . give), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, d1: Data, d2: Data, d3: Data, pair: Pair, r: shared {d3} Data}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
-                                                             the rule "new" failed at step #5 (src/file.rs:LL:CC) because
+                                                             the rule "new" failed at step #6 (src/file.rs:LL:CC) because
                                                                judgment `type_field_exprs_as { temp_var: @ fresh(0), exprs: [pair . give, r . give], fields: [pair : Pair ;, data : shared {self . pair} Data ;], env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): Choice, d1: Data, d2: Data, d3: Data, pair: Pair, r: shared {d3} Data}, assumptions: {}, fresh: 1 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
                                                                  the rule "cons" failed at step #7 (src/file.rs:LL:CC) because
                                                                    judgment `type_field_exprs_as { temp_var: @ fresh(0), exprs: [r . give], fields: [data : shared {self . pair} Data ;], env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): Choice, d1: Data, d2: Data, d3: Data, pair: Pair, r: shared {d3} Data}, assumptions: {}, fresh: 1 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):

src/type_system/types.rs

@@ -2,9 +2,12 @@ use anyhow::bail;
 use fn_error_context::context;
 use formality_core::Fallible;
 
-use crate::grammar::{NamedTy, Parameter, Perm, Place, Program, Ty, TypeName};
+use crate::{
+    dada_lang::grammar::{Binder, BoundVar},
+    grammar::{Kind, NamedTy, Parameter, Perm, Place, Predicate, Program, Ty, TypeName},
+};
 
-use super::{env::Env, places::place_ty};
+use super::{env::Env, places::place_ty, predicates::prove_predicate};
 
 pub fn check_parameter(env: &Env, parameter: &Parameter) -> Fallible<()> {
     match parameter {
@@ -17,16 +20,22 @@ pub fn check_parameter(env: &Env, parameter: &Parameter) -> Fallible<()> {
 pub fn check_type(env: &Env, ty: &Ty) -> Fallible<()> {
     match ty {
         Ty::NamedTy(NamedTy { name, parameters }) => {
-            let arity = check_class_name(env.program(), name)?;
-            if parameters.len() != arity {
+            let predicates = check_class_name(env.program(), name)?;
+            if parameters.len() != predicates.len() {
                 bail!(
                     "class `{:?}` expects {} parameters, but found {}",
                     name,
-                    arity,
+                    predicates.len(),
                     parameters.len(),
                 )
             }
 
+            let predicates = predicates.instantiate_with(&parameters)?;
+
+            for predicate in predicates {
+                prove_predicate(env, predicate).check_proven()?;
+            }
+
             for parameter in parameters {
                 check_parameter(env, parameter)?;
             }
@@ -83,13 +92,16 @@ fn check_perm(env: &Env, perm: &Perm) -> Fallible<()> {
 }
 
 #[context("check class name `{:?}`", name)]
-fn check_class_name(program: &Program, name: &TypeName) -> Fallible<usize> {
+fn check_class_name(program: &Program, name: &TypeName) -> Fallible<Binder<Vec<Predicate>>> {
     match name {
-        TypeName::Tuple(n) => Ok(*n),
-        TypeName::Int => Ok(0),
+        TypeName::Tuple(n) => {
+            let parameters: Vec<_> = (0..*n).map(|_| BoundVar::fresh(Kind::Ty)).collect();
+            Ok(Binder::new(parameters, vec![]))
+        }
+        TypeName::Int => Ok(Binder::dummy(vec![])),
         TypeName::Id(id) => {
             let decl = program.class_named(id)?;
-            Ok(decl.binder.len())
+            Ok(decl.binder.map(|b| b.predicates.clone()))
         }
     }
 }