Merge branch 'main' into uniq

book/src/formality_core/judgment_fn.md

@@ -1,6 +1,6 @@
 # Judgment functions and inference rules
 
-The next thing is the `judgement_fn!` macro. This lets you write a *judgment* using *inference rules*. A "judgment" just means some kind of predicate that the computer can judge to hold or not hold. Inference rules are those rules you may have seen in papers and things:
+The next thing is the `judgment_fn!` macro. This lets you write a *judgment* using *inference rules*. A "judgment" just means some kind of predicate that the computer can judge to hold or not hold. Inference rules are those rules you may have seen in papers and things:
 
 ```
 premise1

book/src/formality_core/lang.md

@@ -23,7 +23,7 @@ The language module you create has various items in it:
 
 ## Specifying the language for a crate
 
-That module will contain a language struct named `FormalityLang`. It 
+That module will contain a language struct named `FormalityLang`. 
 Other parts of the formality system (e.g., autoderives and the like) 
 will need to know the current language you are defining,
 and they expect to find it at `crate::FormalityLang`. 

crates/formality-check/src/coherence.rs

@@ -53,11 +53,14 @@ impl Check<'_> {
         let a = env.instantiate_universally(&impl_a.binder);
         let trait_ref = a.trait_ref();
 
-        self.prove_goal(
-            &env.with_coherence_mode(true),
-            &a.where_clauses,
-            trait_ref.is_local(),
-        )
+        // The orphan check passes if
+        // ∀P. ⌐ (coherence_mode => (wf(Ts) && cannot_be_proven(is_local_trait_ref)))
+        //
+        // TODO: feels like we do want a general "not goal", flipping existentials
+        // and universals and the coherence mode
+        // self.prove_not_goal(&env, &(Wcs::wf))
+
+        self.prove_goal(&env, &a.where_clauses, trait_ref.is_local())
     }
 
     #[context("orphan_check_neg({impl_a:?})")]
@@ -67,11 +70,7 @@ impl Check<'_> {
         let a = env.instantiate_universally(&impl_a.binder);
         let trait_ref = a.trait_ref();
 
-        self.prove_goal(
-            &env.with_coherence_mode(true),
-            &a.where_clauses,
-            trait_ref.is_local(),
-        )
+        self.prove_goal(&env, &a.where_clauses, trait_ref.is_local())
     }
 
     #[tracing::instrument(level = "Debug", skip(self))]
@@ -100,7 +99,7 @@ impl Check<'_> {
         //
         // ∀P_a, ∀P_b. ⌐ (coherence_mode => (Ts_a = Ts_b && WC_a && WC_b))
         if let Ok(()) = self.prove_not_goal(
-            &env.with_coherence_mode(true),
+            &env,
             (),
             (
                 Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),

crates/formality-check/src/lib.rs

@@ -3,12 +3,12 @@
 use std::{collections::VecDeque, fmt::Debug};
 
 use anyhow::bail;
-use formality_prove::{Decls, Env};
+use formality_prove::{is_definitely_not_proveable, Decls, Env};
 use formality_rust::{
     grammar::{Crate, CrateItem, Program, Test, TestBoundData},
     prove::ToWcs,
 };
-use formality_types::grammar::{Fallible, Substitution, Wcs};
+use formality_types::grammar::{Fallible, Wcs};
 
 /// Check all crates in the program. The crates must be in dependency order
 /// such that any prefix of the crates is a complete program.
@@ -115,58 +115,24 @@ impl Check<'_> {
     }
 
     #[tracing::instrument(level = "Debug", skip(self, assumptions, goal))]
-    fn prove_not_goal(
-        &self,
-        env: &Env,
-        assumptions: impl ToWcs,
-        goal: impl ToWcs + Debug,
-    ) -> Fallible<()> {
+    fn prove_not_goal(&self, env: &Env, assumptions: impl ToWcs, goal: impl ToWcs) -> Fallible<()> {
         let goal: Wcs = goal.to_wcs();
         let assumptions: Wcs = assumptions.to_wcs();
 
-        tracing::debug!("assumptions = {assumptions:?}");
-        tracing::debug!("goal = {goal:?}");
-
         assert!(env.only_universal_variables());
         assert!(env.encloses((&assumptions, &goal)));
 
-        // Proving `∀X. not(F(X))` is the same as proving: `not(∃X. F(X))`.
-        // Therefore, since we have only universal variables, we can change them all to
-        // existential and then try to prove. If we get back no solutions, we know that
-        // we've proven the negation. (This is called the "negation as failure" property,
-        // and it relies on our solver being complete -- i.e., if there is a solution,
-        // we'll find it, or at least return ambiguous.)
-        let mut existential_env = Env::default().with_coherence_mode(env.is_in_coherence_mode());
-        let universal_to_existential: Substitution = env
-            .variables()
-            .iter()
-            .map(|v| {
-                assert!(v.is_universal());
-                let v1 = existential_env.fresh_existential(v.kind());
-                (v, v1)
-            })
-            .collect();
-
-        let existential_assumptions = universal_to_existential.apply(&assumptions);
-        let existential_goal = universal_to_existential.apply(&goal);
-
-        let cs = formality_prove::prove(
-            self.decls,
-            &existential_env,
-            existential_assumptions.to_wcs(),
-            &existential_goal,
+        let cs = is_definitely_not_proveable(
+            env,
+            &assumptions,
+            goal.clone(),
+            |env, assumptions, goal| formality_prove::prove(self.decls, env, &assumptions, &goal),
         );
-
-        match cs.into_set() {
-            Ok(proofs) => {
-                bail!(
-                    "failed to disprove\n    {goal:?}\ngiven\n    {assumptions:?}\ngot\n{proofs:?}"
-                )
-            }
-            Err(err) => {
-                tracing::debug!("Proved not goal, error = {err}");
-                return Ok(());
-            }
+        let cs = cs.into_set()?;
+        if cs.iter().any(|c| c.unconditionally_true()) {
+            return Ok(());
         }
+
+        bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}")
     }
 }

crates/formality-check/src/traits.rs

@@ -1,4 +1,6 @@
+use anyhow::bail;
 use fn_error_context::context;
+use formality_core::Set;
 use formality_prove::Env;
 use formality_rust::grammar::{
     AssociatedTy, AssociatedTyBoundData, Fn, Trait, TraitBoundData, TraitItem, WhereClause,
@@ -31,8 +33,27 @@ impl super::Check<'_> {
         Ok(())
     }
 
-    fn check_trait_items_have_unique_names(&self, _trait_items: &[TraitItem]) -> Fallible<()> {
-        // FIXME:
+    fn check_trait_items_have_unique_names(&self, trait_items: &[TraitItem]) -> Fallible<()> {
+        let mut functions = Set::new();
+        let mut associated_types = Set::new();
+        for trait_item in trait_items {
+            match trait_item {
+                TraitItem::Fn(f) => {
+                    if !functions.insert(&f.id) {
+                        bail!("the function name `{:?}` is defined multiple times", f.id);
+                    }
+                }
+                TraitItem::AssociatedTy(associated_ty) => {
+                    let AssociatedTy { id, .. } = associated_ty;
+                    if !associated_types.insert(id) {
+                        bail!(
+                            "the associated type name `{:?}` is defined multiple times",
+                            id
+                        );
+                    }
+                }
+            }
+        }
         Ok(())
     }
 

crates/formality-check/src/where_clauses.rs

@@ -1,85 +1,20 @@
 use fn_error_context::context;
-use formality_core::Upcast;
 use formality_prove::Env;
-use formality_rust::{
-    grammar::{WhereClause, WhereClauseData},
-    prove::ToWcs,
-};
-use formality_types::grammar::{ConstData, Fallible, Parameter, Relation, TraitRef};
+use formality_rust::{grammar::WhereClause, prove::ToWcs};
+use formality_types::grammar::{Fallible, Wcs};
 
 impl super::Check<'_> {
+    #[context("prove_where_clauses_well_formed({where_clauses:?})")]
     pub(crate) fn prove_where_clauses_well_formed(
         &self,
         env: &Env,
         assumptions: impl ToWcs,
         where_clauses: &[WhereClause],
     ) -> Fallible<()> {
-        for where_clause in where_clauses {
-            self.prove_where_clause_well_formed(env, &assumptions, where_clause)?;
-        }
-        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,
-        assumptions: impl ToWcs,
-        where_clause: &WhereClause,
-    ) -> Fallible<()> {
-        match where_clause.data() {
-            WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => self
-                .prove_trait_ref_well_formed(
-                    in_env,
-                    assumptions,
-                    trait_id.with(self_ty, parameters),
-                ),
-            WhereClauseData::AliasEq(alias_ty, ty) => {
-                self.prove_parameter_well_formed(in_env, &assumptions, alias_ty)?;
-                self.prove_parameter_well_formed(in_env, &assumptions, ty)
-            }
-            WhereClauseData::Outlives(a, b) => {
-                self.prove_parameter_well_formed(in_env, &assumptions, a)?;
-                self.prove_parameter_well_formed(in_env, assumptions, b)
-            }
-            WhereClauseData::ForAll(binder) => {
-                let mut e = in_env.clone();
-                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::equals(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())
-            }
-        }
-    }
-
-    fn prove_parameter_well_formed(
-        &self,
-        env: &Env,
-        assumptions: impl ToWcs,
-        parameter: impl Upcast<Parameter>,
-    ) -> Fallible<()> {
-        let parameter: Parameter = parameter.upcast();
-        self.prove_goal(env, assumptions, parameter.well_formed())
-    }
-
-    fn prove_trait_ref_well_formed(
-        &self,
-        env: &Env,
-        assumptions: impl ToWcs,
-        trait_ref: impl Upcast<TraitRef>,
-    ) -> Fallible<()> {
-        let trait_ref: TraitRef = trait_ref.upcast();
-        self.prove_goal(env, assumptions, trait_ref.well_formed())?;
-        Ok(())
+        let wcs: Wcs = where_clauses
+            .into_iter()
+            .flat_map(|wc| wc.well_formed().into_iter())
+            .collect();
+        self.prove_goal(env, assumptions, wcs)
     }
 }

crates/formality-core/src/test_util.rs

@@ -41,7 +41,7 @@ use std::fmt::{Debug, Display};
 /// with `"src/file.rs:LL:CC"`. This makes error messages resilient against changes to the source code.
 pub fn normalize_paths(s: impl Display) -> String {
     let s = s.to_string();
-    let re = regex::Regex::new(r"\([^():]+.rs:\d+:\d+\)").unwrap();
+    let re = regex::Regex::new(r"\([^()]+.rs:\d+:\d+\)").unwrap();
     re.replace_all(&s, "(src/file.rs:LL:CC)").to_string()
 }
 

crates/formality-core/src/visit.rs

@@ -2,7 +2,7 @@ use std::sync::Arc;
 
 use crate::{collections::Set, language::Language, variable::CoreVariable};
 
-pub trait CoreVisit<L: Language> {
+pub trait CoreVisit<L: Language>: std::fmt::Debug {
     /// Extract the list of free variables (for the purposes of this function, defined by `Variable::is_free`).
     /// The list may contain duplicates and must be in a determinstic order (though the order itself isn't important).
     fn free_variables(&self) -> Vec<CoreVariable<L>>;

crates/formality-prove/src/decls.rs

@@ -2,7 +2,7 @@ use formality_core::{set, Set, Upcast};
 use formality_macros::term;
 use formality_types::grammar::{
     AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc,
-    Wcs, PR,
+    Wcs,
 };
 
 #[term]
@@ -175,13 +175,14 @@ impl TraitDecl {
 
         fn is_supertrait(self_var: &Parameter, wc: &Wc) -> bool {
             match wc.data() {
-                formality_types::grammar::WcData::PR(PR::Predicate(Predicate::IsImplemented(
+                formality_types::grammar::WcData::Predicate(Predicate::IsImplemented(
                     trait_ref,
-                ))) => trait_ref.parameters[0] == *self_var,
-                formality_types::grammar::WcData::PR(PR::Relation(Relation::Outlives(a, _))) => {
+                )) => trait_ref.parameters[0] == *self_var,
+                formality_types::grammar::WcData::Relation(Relation::Outlives(a, _)) => {
                     *a == *self_var
                 }
-                formality_types::grammar::WcData::PR(_) => false,
+                formality_types::grammar::WcData::Predicate(_) => false,
+                formality_types::grammar::WcData::Relation(_) => false,
                 formality_types::grammar::WcData::ForAll(binder) => {
                     is_supertrait(self_var, binder.peek())
                 }

crates/formality-prove/src/lib.rs

@@ -8,7 +8,8 @@ mod prove;
 pub use decls::*;
 pub use prove::prove;
 pub use prove::Constraints;
-pub use prove::Env;
+pub use prove::{is_definitely_not_proveable, may_not_be_provable, negation_via_failure};
+pub use prove::{Bias, Env};
 
 #[cfg(test)]
 mod test;

crates/formality-prove/src/prove.rs

@@ -3,6 +3,7 @@ mod constraints;
 mod env;
 mod is_local;
 mod minimize;
+mod negation;
 mod prove_after;
 mod prove_eq;
 mod prove_normalize;
@@ -19,8 +20,9 @@ use tracing::Level;
 
 use crate::decls::Decls;
 
-pub use self::env::Env;
+pub use self::env::{Bias, Env};
 use self::prove_wc_list::prove_wc_list;
+pub use negation::{is_definitely_not_proveable, may_not_be_provable, negation_via_failure};
 
 /// Top-level entry point for proving things; other rules recurse to this one.
 pub fn prove(

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

@@ -30,13 +30,6 @@ impl Constraints {
         Self::from(env, v)
     }
 
-    pub fn with_coherence_mode(self, b: bool) -> Self {
-        Self {
-            env: self.env.with_coherence_mode(b),
-            ..self
-        }
-    }
-
     pub fn unconditionally_true(&self) -> bool {
         self.known_true && self.substitution.is_empty()
     }